{- |
Module      : Specification.Types
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (ghc-wasm-meta)

This module defines specification types that mirror t'Term', t'Formula',
t'Assumption' and t'Proof' for describing Fitch proof rules.
-}
module Specification.Types where

import Data.Text qualified as T
import Fitch.Proof

------------------------------------------------------------------------------------------

-- * Rule specifications

{- | Specification of a referenced t'Proof' premise,
containing the specification of its t'Assumption's and its conclusion.
-}
type ProofSpec = ([AssumptionSpec], FormulaSpec)

-- | The specification of a Fitch rule.
data RuleSpec
  = {- | A t'RuleSpec' consists of
    a list of t'FormulaSpec' premises, a list of t'ProofSpec' premises, and a conclusion.
    -}
    RuleSpec
      -- | t'Formula' premises.
      [FormulaSpec]
      -- | t'Proof' premises.
      [ProofSpec]
      -- | The conclusion derived by the rule.
      FormulaSpec
  deriving (Int -> RuleSpec -> ShowS
[RuleSpec] -> ShowS
RuleSpec -> String
(Int -> RuleSpec -> ShowS)
-> (RuleSpec -> String) -> ([RuleSpec] -> ShowS) -> Show RuleSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuleSpec -> ShowS
showsPrec :: Int -> RuleSpec -> ShowS
$cshow :: RuleSpec -> String
show :: RuleSpec -> String
$cshowList :: [RuleSpec] -> ShowS
showList :: [RuleSpec] -> ShowS
Show, RuleSpec -> RuleSpec -> Bool
(RuleSpec -> RuleSpec -> Bool)
-> (RuleSpec -> RuleSpec -> Bool) -> Eq RuleSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RuleSpec -> RuleSpec -> Bool
== :: RuleSpec -> RuleSpec -> Bool
$c/= :: RuleSpec -> RuleSpec -> Bool
/= :: RuleSpec -> RuleSpec -> Bool
Eq)

-- | Renders a t'RuleSpec' as TeX for displaying via MathJAX.
ruleSpecTex :: RuleSpec -> Text
ruleSpecTex :: RuleSpec -> Text
ruleSpecTex (RuleSpec [FormulaSpec]
fs [ProofSpec]
ps FormulaSpec
conclusion) =
  Text
"\\frac{"
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
showFsPs
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}{"
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint FormulaSpec
conclusion
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
 where
  formulaSpecTex :: FormulaSpec -> Text
  formulaSpecTex :: FormulaSpec -> Text
formulaSpecTex = FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint
  proofSpecTex :: ProofSpec -> Text
  proofSpecTex :: ProofSpec -> Text
proofSpecTex ([AssumptionSpec]
as, FormulaSpec
f) =
    Text
"\\begin{array}{|l}"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
showAs
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\\\\ \\hline \\vdots \\\\ "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint FormulaSpec
f
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\\end{array}"
   where
    showAs :: Text
showAs = Text -> [Text] -> Text
T.intercalate Text
"\\;" ((AssumptionSpec -> Text) -> [AssumptionSpec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map AssumptionSpec -> Text
assumptionSpecTex [AssumptionSpec]
as)
    assumptionSpecTex :: AssumptionSpec -> Text
    assumptionSpecTex :: AssumptionSpec -> Text
assumptionSpecTex (FFreshVar Text
v) = Text
"\\boxed{" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"}"
    assumptionSpecTex (AssumptionSpec FormulaSpec
frm) = FormulaSpec -> Text
formulaSpecTex FormulaSpec
frm
  showFsPs :: Text
showFsPs = Text -> [Text] -> Text
T.intercalate Text
"\\quad " ((FormulaSpec -> Text) -> [FormulaSpec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map FormulaSpec -> Text
formulaSpecTex [FormulaSpec]
fs [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (ProofSpec -> Text) -> [ProofSpec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map ProofSpec -> Text
proofSpecTex [ProofSpec]
ps)

------------------------------------------------------------------------------------------

-- * Term and Formula specifications

-- | A substitution of a named placeholder by some value.
data Subst a
  = -- | @v'Subst' name value@ replaces the placeholder @name@ with @value@.
    Subst Name a
  deriving (Int -> Subst a -> ShowS
[Subst a] -> ShowS
Subst a -> String
(Int -> Subst a -> ShowS)
-> (Subst a -> String) -> ([Subst a] -> ShowS) -> Show (Subst a)
forall a. Show a => Int -> Subst a -> ShowS
forall a. Show a => [Subst a] -> ShowS
forall a. Show a => Subst a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Subst a -> ShowS
showsPrec :: Int -> Subst a -> ShowS
$cshow :: forall a. Show a => Subst a -> String
show :: Subst a -> String
$cshowList :: forall a. Show a => [Subst a] -> ShowS
showList :: [Subst a] -> ShowS
Show, Subst a -> Subst a -> Bool
(Subst a -> Subst a -> Bool)
-> (Subst a -> Subst a -> Bool) -> Eq (Subst a)
forall a. Eq a => Subst a -> Subst a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Subst a -> Subst a -> Bool
== :: Subst a -> Subst a -> Bool
$c/= :: forall a. Eq a => Subst a -> Subst a -> Bool
/= :: Subst a -> Subst a -> Bool
Eq)

instance (PrettyPrint a) => PrettyPrint (Subst a) where
  prettyPrint :: (PrettyPrint a) => Subst a -> Text
  prettyPrint :: PrettyPrint a => Subst a -> Text
prettyPrint (Subst Text
n a
t) = Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint a
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"/" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"

infixl 9 ~>

-- | Smart constructor for t'Subst'.
(~>) :: Name -> a -> Subst a
~> :: forall a. Text -> a -> Subst a
(~>) = Text -> a -> Subst a
forall a. Text -> a -> Subst a
Subst

-- | A t'Term' specification used in t'RuleSpec' specifications.
data TermSpec
  = -- | A term variable.
    TVar Name
  | -- | A function application.
    TFun Name [TermSpec]
  | -- | A placeholder for t'Term's @T@.
    TPlaceholder Name
  deriving (TermSpec -> TermSpec -> Bool
(TermSpec -> TermSpec -> Bool)
-> (TermSpec -> TermSpec -> Bool) -> Eq TermSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TermSpec -> TermSpec -> Bool
== :: TermSpec -> TermSpec -> Bool
$c/= :: TermSpec -> TermSpec -> Bool
/= :: TermSpec -> TermSpec -> Bool
Eq, Int -> TermSpec -> ShowS
[TermSpec] -> ShowS
TermSpec -> String
(Int -> TermSpec -> ShowS)
-> (TermSpec -> String) -> ([TermSpec] -> ShowS) -> Show TermSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TermSpec -> ShowS
showsPrec :: Int -> TermSpec -> ShowS
$cshow :: TermSpec -> String
show :: TermSpec -> String
$cshowList :: [TermSpec] -> ShowS
showList :: [TermSpec] -> ShowS
Show)

instance PrettyPrint TermSpec where
  prettyPrint :: TermSpec -> Text
  prettyPrint :: TermSpec -> Text
prettyPrint (TVar Text
n) = Text
n
  prettyPrint (TFun Text
f [TermSpec]
ts) = Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((TermSpec -> Text) -> [TermSpec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map TermSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [TermSpec]
ts) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
  prettyPrint (TPlaceholder Text
n) = Text
n

-- | A t'Formula' specification used in t'RuleSpec' specifications.
data FormulaSpec
  = -- | A substitution @φ[n ↦ t]@: formula @φ@ with variable @n@ replaced by term @t@.
    FSubst Name (Subst Name)
  | -- | A placeholder for t'Formula'e @φ@.
    FPlaceholder Name
  | -- | A predicate.
    FPred Name [TermSpec]
  | -- | An infix predicate.
    FInfixPred Name TermSpec TermSpec
  | -- | An n-ary operator.
    FOpr Text [FormulaSpec]
  | -- | A quantifier @∀x.φ@.
    FQuantifier Name Name FormulaSpec
  deriving (FormulaSpec -> FormulaSpec -> Bool
(FormulaSpec -> FormulaSpec -> Bool)
-> (FormulaSpec -> FormulaSpec -> Bool) -> Eq FormulaSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FormulaSpec -> FormulaSpec -> Bool
== :: FormulaSpec -> FormulaSpec -> Bool
$c/= :: FormulaSpec -> FormulaSpec -> Bool
/= :: FormulaSpec -> FormulaSpec -> Bool
Eq, Int -> FormulaSpec -> ShowS
[FormulaSpec] -> ShowS
FormulaSpec -> String
(Int -> FormulaSpec -> ShowS)
-> (FormulaSpec -> String)
-> ([FormulaSpec] -> ShowS)
-> Show FormulaSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FormulaSpec -> ShowS
showsPrec :: Int -> FormulaSpec -> ShowS
$cshow :: FormulaSpec -> String
show :: FormulaSpec -> String
$cshowList :: [FormulaSpec] -> ShowS
showList :: [FormulaSpec] -> ShowS
Show)

-- | An t'Assumption' specification used in t'RuleSpec' specifications.
data AssumptionSpec
  = -- | Regular t'FormulaSpec'.
    AssumptionSpec FormulaSpec
  | -- | A fresh-variable constraint @[c]@.
    FFreshVar Name
  deriving (AssumptionSpec -> AssumptionSpec -> Bool
(AssumptionSpec -> AssumptionSpec -> Bool)
-> (AssumptionSpec -> AssumptionSpec -> Bool) -> Eq AssumptionSpec
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssumptionSpec -> AssumptionSpec -> Bool
== :: AssumptionSpec -> AssumptionSpec -> Bool
$c/= :: AssumptionSpec -> AssumptionSpec -> Bool
/= :: AssumptionSpec -> AssumptionSpec -> Bool
Eq, Int -> AssumptionSpec -> ShowS
[AssumptionSpec] -> ShowS
AssumptionSpec -> String
(Int -> AssumptionSpec -> ShowS)
-> (AssumptionSpec -> String)
-> ([AssumptionSpec] -> ShowS)
-> Show AssumptionSpec
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AssumptionSpec -> ShowS
showsPrec :: Int -> AssumptionSpec -> ShowS
$cshow :: AssumptionSpec -> String
show :: AssumptionSpec -> String
$cshowList :: [AssumptionSpec] -> ShowS
showList :: [AssumptionSpec] -> ShowS
Show)

instance PrettyPrint FormulaSpec where
  prettyPrint :: FormulaSpec -> Text
  prettyPrint :: FormulaSpec -> Text
prettyPrint FormulaSpec
f = Bool -> FormulaSpec -> Text
go Bool
False FormulaSpec
f
   where
    go :: Bool -> FormulaSpec -> Text
    go :: Bool -> FormulaSpec -> Text
go Bool
_ (FPred Text
p []) = Text
p
    go Bool
_ (FPred Text
p [TermSpec]
ts) = Text
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((TermSpec -> Text) -> [TermSpec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map TermSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [TermSpec]
ts) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    go Bool
_ (FPlaceholder Text
n) = Text
n
    go Bool
_ (FSubst Text
f (Subst Text
n Text
t)) = Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" ↦ " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"
    go Bool
True FormulaSpec
f = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> FormulaSpec -> Text
go Bool
False FormulaSpec
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    go Bool
False (FInfixPred Text
p TermSpec
t1 TermSpec
t2) = TermSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint TermSpec
t1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TermSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint TermSpec
t2
    go Bool
False (FOpr Text
op []) = Text
op
    go Bool
False (FOpr Text
op [Item [FormulaSpec]
f]) = Text
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> FormulaSpec -> Text
go Bool
True Item [FormulaSpec]
FormulaSpec
f
    go Bool
False (FOpr Text
op [Item [FormulaSpec]
f1, Item [FormulaSpec]
f2]) = Bool -> FormulaSpec -> Text
go Bool
True Item [FormulaSpec]
FormulaSpec
f1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> FormulaSpec -> Text
go Bool
True Item [FormulaSpec]
FormulaSpec
f2
    go Bool
False (FOpr Text
op [FormulaSpec]
fs) = Text
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((FormulaSpec -> Text) -> [FormulaSpec] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [FormulaSpec]
fs) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    go Bool
False (FQuantifier Text
q Text
v FormulaSpec
f) = Text
q Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint FormulaSpec
f

instance PrettyPrint AssumptionSpec where
  prettyPrint :: AssumptionSpec -> Text
  prettyPrint :: AssumptionSpec -> Text
prettyPrint (AssumptionSpec FormulaSpec
fSpec) = FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint FormulaSpec
fSpec
  prettyPrint (FFreshVar Text
n) = Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"

------------------------------------------------------------------------------------------