Copyright	(c) Leon Vatthauer 2026
License	GPL-3
Maintainer	Leon Vatthauer <leon.vatthauer@fau.de>
Stability	experimental
Portability	non-portable (ghc-wasm-meta)
Safe Haskell	None
Language	GHC2024

Specification.Types

Contents

Rule specifications
Term and Formula specifications

Description

This module defines specification types that mirror Term, Formula, tAssumption and Proof for describing Fitch proof rules.

Synopsis

type ProofSpec = ([AssumptionSpec], FormulaSpec)
data RuleSpec = RuleSpec [FormulaSpec] [ProofSpec] FormulaSpec
ruleSpecTex :: RuleSpec -> Text
data Subst a = Subst Name a
(~>) :: Name -> a -> Subst a
data TermSpec
- = TVar Name
- | TFun Name [TermSpec]
- | TPlaceholder Name
data FormulaSpec
- = FSubst Name (Subst Name)
- | FPlaceholder Name
- | FPred Name [TermSpec]
- | FInfixPred Name TermSpec TermSpec
- | FOpr Text [FormulaSpec]
- | FQuantifier Name Name FormulaSpec
data AssumptionSpec
- = AssumptionSpec FormulaSpec
- | FFreshVar Name

Rule specifications

type ProofSpec = ([AssumptionSpec], FormulaSpec) Source #

Specification of a referenced Proof premise, containing the specification of its Assumptions and its conclusion.

data RuleSpec Source #

The specification of a Fitch rule.

Constructors

RuleSpec	A `RuleSpec` consists of a list of `FormulaSpec` premises, a list of `ProofSpec` premises, and a conclusion.
Fields [FormulaSpec] `Formula` premises. [ProofSpec] `Proof` premises. FormulaSpec The conclusion derived by the rule.

Instances

Instances details

Show RuleSpec Source #
Instance details Defined in Specification.Types Methods showsPrec :: Int -> RuleSpec -> ShowS # show :: RuleSpec -> String # showList :: [RuleSpec] -> ShowS #
Eq RuleSpec Source #
Instance details Defined in Specification.Types Methods (==) :: RuleSpec -> RuleSpec -> Bool # (/=) :: RuleSpec -> RuleSpec -> Bool #

ruleSpecTex :: RuleSpec -> Text Source #

Renders a RuleSpec as TeX for displaying via MathJAX.

Term and Formula specifications

data Subst a Source #

A substitution of a named placeholder by some value.

Constructors

Subst Name a

Subst name value replaces the placeholder name with value.

Instances

Instances details

PrettyPrint a => PrettyPrint (Subst a) Source #
Instance details Defined in Specification.Types Methods prettyPrint :: Subst a -> Text Source #
Show a => Show (Subst a) Source #
Instance details Defined in Specification.Types Methods showsPrec :: Int -> Subst a -> ShowS # show :: Subst a -> String # showList :: [Subst a] -> ShowS #
Eq a => Eq (Subst a) Source #
Instance details Defined in Specification.Types Methods (==) :: Subst a -> Subst a -> Bool # (/=) :: Subst a -> Subst a -> Bool #

(~>) :: Name -> a -> Subst a infixl 9 Source #

Smart constructor for Subst.

data TermSpec Source #

A Term specification used in RuleSpec specifications.

Constructors

TVar Name	A term variable.
TFun Name [TermSpec]	A function application.
TPlaceholder Name	A placeholder for `Term`s `T`.

Instances

Instances details

PrettyPrint TermSpec Source #
Instance details Defined in Specification.Types Methods prettyPrint :: TermSpec -> Text Source #
Show TermSpec Source #
Instance details Defined in Specification.Types Methods showsPrec :: Int -> TermSpec -> ShowS # show :: TermSpec -> String # showList :: [TermSpec] -> ShowS #
Eq TermSpec Source #
Instance details Defined in Specification.Types Methods (==) :: TermSpec -> TermSpec -> Bool # (/=) :: TermSpec -> TermSpec -> Bool #

data FormulaSpec Source #

A Formula specification used in RuleSpec specifications.

Constructors

FSubst Name (Subst Name)	A substitution `φ[n ↦ t]`: formula `φ` with variable `n` replaced by term `t`.
FPlaceholder Name	A placeholder for `Formula`e `φ`.
FPred Name [TermSpec]	A predicate.
FInfixPred Name TermSpec TermSpec	An infix predicate.
FOpr Text [FormulaSpec]	An n-ary operator.
FQuantifier Name Name FormulaSpec	A quantifier `∀x.φ`.

Instances

Instances details

PrettyPrint FormulaSpec Source #
Instance details Defined in Specification.Types Methods prettyPrint :: FormulaSpec -> Text Source #
Show FormulaSpec Source #
Instance details Defined in Specification.Types Methods showsPrec :: Int -> FormulaSpec -> ShowS # show :: FormulaSpec -> String # showList :: [FormulaSpec] -> ShowS #
Eq FormulaSpec Source #
Instance details Defined in Specification.Types Methods (==) :: FormulaSpec -> FormulaSpec -> Bool # (/=) :: FormulaSpec -> FormulaSpec -> Bool #

data AssumptionSpec Source #

An Assumption specification used in RuleSpec specifications.

Constructors

AssumptionSpec FormulaSpec	Regular `FormulaSpec`.
FFreshVar Name	A fresh-variable constraint `[c]`.

Instances

Instances details

PrettyPrint AssumptionSpec Source #
Instance details Defined in Specification.Types Methods prettyPrint :: AssumptionSpec -> Text Source #
Show AssumptionSpec Source #
Instance details Defined in Specification.Types Methods showsPrec :: Int -> AssumptionSpec -> ShowS # show :: AssumptionSpec -> String # showList :: [AssumptionSpec] -> ShowS #
Eq AssumptionSpec Source #
Instance details Defined in Specification.Types Methods (==) :: AssumptionSpec -> AssumptionSpec -> Bool # (/=) :: AssumptionSpec -> AssumptionSpec -> Bool #