{- |
Module      : Specification.FOL
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 provides the specification of first-order logic, i.e. its
operators, rules and some examples. This module extends "Specification.Prop"
-}
module Specification.FOL (
  operatorsFOL,
  infixPredsFOL,
  quantifiersFOL,
  rulesFOL,
  exampleProofsFOL,
  initialModelFOL,
) where

import Miso.Router (URI)

import App.Model
import Fitch.Proof
import Parser.Proof (parseProof)
import Specification.Prop
import Specification.Types

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

-- * Operators

{- | Operators of first-order logic.

Each entry is a triple @(alias, operator, arity)@, where @alias@ is
ASCII text the parser also accepts and the operator is usually a unicode symbol.

Operators are inherited from 'operatorsProp'.
-}
operatorsFOL :: [(Text, Text, Int)]
operatorsFOL :: [(Text, Text, Int)]
operatorsFOL = [(Text, Text, Int)]
operatorsProp

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

-- * Infix Predicates

{- | Infix predicates of first-order logic.

Each entry is a pair @(alias, predicate)@, where @alias@ is ASCII text
the parser also accepts.
-}
infixPredsFOL :: [(Text, Text)]
infixPredsFOL :: [(Text, Text)]
infixPredsFOL = [(Text
"", Text
"=")]

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

-- * Quantifiers

{- | Quantifiers of first-order logic.

Each entry is a pair @(alias, quantifier)@, where @alias@ is ASCII text
the parser also accepts and @quantifier@ is a unicode symbol.
-}
quantifiersFOL :: [(Text, Text)]
quantifiersFOL :: [(Text, Text)]
quantifiersFOL = [(Text
"forall", Text
"∀"), (Text
"exists", Text
"∃")]

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

-- * Rules

{- | The standard Fitch-style natural deduction rules for first-order logic.

Extends 'rulesProp' with rules for @∀@, @∃@ and @=@.
-}
rulesFOL :: [(Text, RuleSpec)]
rulesFOL :: [(Text, RuleSpec)]
rulesFOL =
  [(Text, RuleSpec)]
rulesProp
    [(Text, RuleSpec)] -> [(Text, RuleSpec)] -> [(Text, RuleSpec)]
forall a. Semigroup a => a -> a -> a
<> [
         ( Text
"∀I"
         , [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec
             []
             [([Text -> AssumptionSpec
FFreshVar Text
"c"], Text -> Subst Text -> FormulaSpec
FSubst Text
"φ" (Text
"x" Text -> Text -> Subst Text
forall a. Text -> a -> Subst a
~> Text
"c"))]
             (Text -> Text -> FormulaSpec -> FormulaSpec
FQuantifier Text
"∀" Text
"x" FormulaSpec
phi)
         )
       , (Text
"∀E", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Text -> Text -> FormulaSpec -> FormulaSpec
FQuantifier Text
"∀" Text
"x" FormulaSpec
phi] [] (Text -> Subst Text -> FormulaSpec
FSubst Text
"φ" (Text
"x" Text -> Text -> Subst Text
forall a. Text -> a -> Subst a
~> Text
"E")))
       , (Text
"∃I", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Text -> Subst Text -> FormulaSpec
FSubst Text
"φ" (Text
"x" Text -> Text -> Subst Text
forall a. Text -> a -> Subst a
~> Text
"E")] [] (Text -> Text -> FormulaSpec -> FormulaSpec
FQuantifier Text
"∃" Text
"x" FormulaSpec
phi))
       ,
         ( Text
"∃E"
         , [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec
             [Text -> Text -> FormulaSpec -> FormulaSpec
FQuantifier Text
"∃" Text
"x" FormulaSpec
phi]
             [([Text -> AssumptionSpec
FFreshVar Text
"c", FormulaSpec -> AssumptionSpec
AssumptionSpec (FormulaSpec -> AssumptionSpec) -> FormulaSpec -> AssumptionSpec
forall a b. (a -> b) -> a -> b
$ Text -> Subst Text -> FormulaSpec
FSubst Text
"φ" (Text
"x" Text -> Text -> Subst Text
forall a. Text -> a -> Subst a
~> Text
"c")], FormulaSpec
psi)]
             FormulaSpec
psi
         )
       , (Text
"=I", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [] [] (Text -> TermSpec -> TermSpec -> FormulaSpec
FInfixPred Text
"=" (Text -> TermSpec
TPlaceholder Text
"E") (Text -> TermSpec
TPlaceholder Text
"E")))
       ,
         ( Text
"=E"
         , [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec
             [ Text -> Subst Text -> FormulaSpec
FSubst Text
"φ" (Text
"x" Text -> Text -> Subst Text
forall a. Text -> a -> Subst a
~> Text
"E")
             , Text -> TermSpec -> TermSpec -> FormulaSpec
FInfixPred Text
"=" (Text -> TermSpec
TPlaceholder Text
"E") (Text -> TermSpec
TPlaceholder Text
"D")
             ]
             []
             (Text -> Subst Text -> FormulaSpec
FSubst Text
"φ" (Text
"x" Text -> Text -> Subst Text
forall a. Text -> a -> Subst a
~> Text
"D"))
         )
       ]
 where
  phi :: FormulaSpec
phi = Text -> FormulaSpec
FPlaceholder Text
"φ"
  psi :: FormulaSpec
psi = Text -> FormulaSpec
FPlaceholder Text
"ψ"

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

-- * Parser

{- | Parses a t'Proof' of first-order logic.

__Note:__ Should not be used outside of this module, because it uses 'error'.
-}
readProof :: Text -> Proof
readProof :: Text -> Proof
readProof Text
proofText =
  case [(Text, Text, Int)]
-> [(Text, Text)] -> [(Text, Text)] -> Text -> Either Text Proof
parseProof [(Text, Text, Int)]
operatorsFOL [(Text, Text)]
infixPredsFOL [(Text, Text)]
quantifiersFOL Text
proofText of
    Left Text
err -> Text -> Proof
forall a t. (HasCallStack, IsText t) => t -> a
error (Text -> Proof) -> Text -> Proof
forall a b. (a -> b) -> a -> b
$ Text
"Could not parse proof:\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
proofText Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nError:\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
err
    Right Proof
p -> Proof
p

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

-- * Examples

-- | A list of example t'Proof's shown in the sidebar, each paired with a display name.
exampleProofsFOL :: [(Text, Proof)]
exampleProofsFOL :: [(Text, Proof)]
exampleProofsFOL =
  [
    ( Text
"∀-Transitivity"
    , Text -> Proof
readProof
        Text
"""
        |∀x. P(x) → Q(x)
        |∀z. Q(z) → R(z)
        |---
        ||[d]
        ||---
        |||P(d)
        |||---
        |||P(d) → Q(d)  (∀E) 1
        |||Q(d)         (→E) 5,4
        |||Q(d) → R(d)  (∀E) 2
        |||R(d)         (→E) 7,6
        ||P(d) → R(d)   (→I) 4-8
        |∀x.P(x) → R(x) (∀I) 3-9
        """
    )
  ,
    ( Text
"=-Symmetry"
    , Text -> Proof
readProof
        Text
"""
        |e = d
        |---
        |e = e (=I)
        |d = e (=E) 2,1
        """
    )
  ,
    ( Text
"∀-to-∃"
    , Text -> Proof
readProof
        Text
"""
        |¬∀x.¬P(x)
        |---
        ||¬∃x.P(x)
        ||---
        |||[c]
        |||---
        ||||P(c)
        ||||---
        ||||∃x.P(x) (∃I) 4
        ||||⊥       (¬E) 5,2
        |||¬P(c)    (¬I) 4-6
        ||∀x.¬P(x)  (∀I) 3-7
        ||⊥         (¬E) 8,1
        |¬¬∃x.P(x)  (¬I) 2-9
        |∃x.P(x)    (¬¬E) 10
        """
    )
  ,
    ( Text
"∃-to-∀"
    , Text -> Proof
readProof
        Text
"""
        |∃x.P(x)
        |---
        ||[c]
        ||P(c)
        ||---
        |||∀x.¬P(x)
        |||---
        |||¬P(c)    (∀E) 4
        |||⊥        (¬E) 3,5
        ||¬∀x.¬P(x) (¬I) 4-6
        |¬∀x.¬P(x)  (∃E) 1, 2-7
        """
    )
  ,
    ( Text
"∃∀-to-∀∃"
    , Text -> Proof
readProof
        Text
"""
        |∃x.∀y.P(x,y)
        |---
        ||[c]
        ||∀y.P(c,y)
        ||---
        |||[d]
        |||---
        |||P(c,d)      (∀E) 3
        |||∃x.P(x,d)   (∃I) 5
        ||∀y.∃x.P(x,y) (∀I) 4-6
        |∀y.∃x.P(x,y)  (∃E) 1, 2-7
        """
    )
  ,
    ( Text
"∃∀-transfer"
    , Text -> Proof
readProof
        Text
"""
        |∃x.P(f(x)) ∧ Q(x)
        |∀y.Q(y) → Q(f(y))
        |---
        ||[c]
        ||P(f(c)) ∧ Q(c)
        ||---
        ||P(f(c))           (∧E1) 4
        ||Q(c)              (∧E2) 4
        ||Q(c) → Q(f(c))    (∀E) 2
        ||Q(f(c))           (→E) 7,6
        ||P(f(c)) ∧ Q(f(c)) (∧I) 5, 8
        ||∃z.P(z) ∧ Q(z)    (∃I) 9
        |∃z.P(z) ∧ Q(z)     (∃E) 1,3-10
        """
    )
  ]

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

-- * Model

-- | Constructs the initial t'Model' for first-order-logic.
initialModelFOL ::
  -- | The current t'URI' of the application.
  URI ->
  -- | An optional t'Proof' decoded from the URL; falls back to the first example proof.
  Maybe Proof ->
  -- | Initial state of onMobile
  Maybe Bool ->
  -- | Possibly a previous sidebarToggle state.
  Bool ->
  Model
initialModelFOL :: URI -> Maybe Proof -> Maybe Bool -> Bool -> Model
initialModelFOL URI
uri Maybe Proof
mp =
  Derivation
-> Proof
-> [(Text, Proof)]
-> [(Text, Text, Int)]
-> [(Text, Text)]
-> [(Text, Text)]
-> [(Text, RuleSpec)]
-> URI
-> Logic
-> Maybe Bool
-> Bool
-> Model
initialModel
    ( Formula -> Wrapper RuleApplication -> Derivation
Derivation
        (Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
"⊤" (Text -> [RawFormula] -> RawFormula
Opr Text
"⊤" []))
        ( Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> a -> Wrapper a
ParsedValid
            Text
"(⊤I)"
            (Text -> [Reference] -> RuleApplication
RuleApplication Text
"⊤I" [])
        )
    )
    (Proof -> Maybe Proof -> Proof
forall a. a -> Maybe a -> a
fromMaybe Proof
initialP Maybe Proof
mp)
    [(Text, Proof)]
exampleProofsFOL
    [(Text, Text, Int)]
operatorsFOL
    [(Text, Text)]
infixPredsFOL
    [(Text, Text)]
quantifiersFOL
    [(Text, RuleSpec)]
rulesFOL
    URI
uri
    Logic
FOL
 where
  (Text
_, Proof
initialP) : [(Text, Proof)]
_ = [(Text, Proof)]
exampleProofsFOL