{- |
Module      : Specification.Prop
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 propositional logic, i.e. its
operators, rules and some examples.
-}
module Specification.Prop (
  operatorsProp,
  rulesProp,
  exampleProofsProp,
  initialModelProp,
) where

import App.Model (Logic (Prop), Model, initialModel)
import Fitch.Proof
import Miso.Router (URI)
import Parser.Proof
import Specification.Types

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

-- * Operators

{- | Operators of propositional 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.
-}
operatorsProp :: [(Text, Text, Int)]
operatorsProp :: [(Text, Text, Int)]
operatorsProp =
  [ (Text
"bot", Text
"⊥", Int
0)
  , (Text
"top", Text
"⊤", Int
0)
  , (Text
"~", Text
"¬", Int
1)
  , (Text
"/\\", Text
"∧", Int
2)
  , (Text
"\\/", Text
"∨", Int
2)
  , (Text
"->", Text
"→", Int
2)
  ]

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

-- * Rules

-- | The standard Fitch-style natural deduction rules for propositional logic.
rulesProp :: [(Text, RuleSpec)]
rulesProp :: [(Text, RuleSpec)]
rulesProp =
  [ (Text
"R", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Item [FormulaSpec]
FormulaSpec
phi] [] FormulaSpec
phi)
  , (Text
"⊥E", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"⊥" []] [] FormulaSpec
phi)
  , (Text
"⊤I", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [] [] (Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"⊤" []))
  , (Text
"¬I", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [] [([FormulaSpec -> AssumptionSpec
AssumptionSpec FormulaSpec
phi], FormulaSpec
bot)] (FormulaSpec -> FormulaSpec
neg FormulaSpec
phi))
  , (Text
"¬E", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Item [FormulaSpec]
FormulaSpec
phi, FormulaSpec -> FormulaSpec
neg FormulaSpec
phi] [] FormulaSpec
bot)
  , (Text
"¬¬E", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [FormulaSpec -> FormulaSpec
neg (FormulaSpec -> FormulaSpec) -> FormulaSpec -> FormulaSpec
forall a b. (a -> b) -> a -> b
$ FormulaSpec -> FormulaSpec
neg FormulaSpec
phi] [] FormulaSpec
phi)
  , (Text
"∧I", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Item [FormulaSpec]
FormulaSpec
phi, Item [FormulaSpec]
FormulaSpec
psi] [] (FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
∧ FormulaSpec
psi))
  , (Text
"∧E1", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
∧ FormulaSpec
psi] [] FormulaSpec
phi)
  , (Text
"∧E2", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
∧ FormulaSpec
psi] [] FormulaSpec
psi)
  , (Text
"∨I1", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Item [FormulaSpec]
FormulaSpec
phi] [] (FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
∨ FormulaSpec
psi))
  , (Text
"∨I2", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [Item [FormulaSpec]
FormulaSpec
psi] [] (FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
∨ FormulaSpec
psi))
  ,
    ( Text
"∨E"
    , [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
∨ FormulaSpec
psi] [([FormulaSpec -> AssumptionSpec
AssumptionSpec FormulaSpec
phi], FormulaSpec
chi), ([FormulaSpec -> AssumptionSpec
AssumptionSpec FormulaSpec
psi], FormulaSpec
chi)] FormulaSpec
chi
    )
  , (Text
"→I", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [] [([FormulaSpec -> AssumptionSpec
AssumptionSpec FormulaSpec
phi], FormulaSpec
psi)] (FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
↝ FormulaSpec
psi))
  , (Text
"→E", [FormulaSpec] -> [ProofSpec] -> FormulaSpec -> RuleSpec
RuleSpec [FormulaSpec
phi FormulaSpec -> FormulaSpec -> FormulaSpec
↝ FormulaSpec
psi, Item [FormulaSpec]
FormulaSpec
phi] [] FormulaSpec
psi)
  ]
 where
  phi :: FormulaSpec
phi = Text -> FormulaSpec
FPlaceholder Text
"φ"
  psi :: FormulaSpec
psi = Text -> FormulaSpec
FPlaceholder Text
"ψ"
  chi :: FormulaSpec
chi = Text -> FormulaSpec
FPlaceholder Text
"χ"
  top :: FormulaSpec
top = Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"⊤" []
  bot :: FormulaSpec
bot = Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"⊥" []
  neg :: FormulaSpec -> FormulaSpec
neg FormulaSpec
f = Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"¬" [Item [FormulaSpec]
FormulaSpec
f]
  FormulaSpec
f1 ∧ :: FormulaSpec -> FormulaSpec -> FormulaSpec
∧ FormulaSpec
f2 = Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"∧" [Item [FormulaSpec]
FormulaSpec
f1, Item [FormulaSpec]
FormulaSpec
f2]
  FormulaSpec
f1 ∨ :: FormulaSpec -> FormulaSpec -> FormulaSpec
∨ FormulaSpec
f2 = Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"∨" [Item [FormulaSpec]
FormulaSpec
f1, Item [FormulaSpec]
FormulaSpec
f2]
  FormulaSpec
f1 ↝ :: FormulaSpec -> FormulaSpec -> FormulaSpec
↝ FormulaSpec
f2 = Text -> [FormulaSpec] -> FormulaSpec
FOpr Text
"→" [Item [FormulaSpec]
FormulaSpec
f1, Item [FormulaSpec]
FormulaSpec
f2]

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

-- * Parser

{- | Parses a t'Proof' of propositional 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)]
operatorsProp [] [] 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.
exampleProofsProp :: [(Text, Proof)]
exampleProofsProp :: [(Text, Proof)]
exampleProofsProp =
  [
    ( Text
"∧-Symmetry"
    , Text -> Proof
readProof
        Text
"""
        |A ∧ B
        |---
        |B     (∧E2) 1
        |A     (∧E1) 1
        |B ∧ A (∧I) 2,3
        """
    )
  ,
    ( Text
"→-Weakening"
    , Text -> Proof
readProof
        Text
"""
        |A → B ∧ C
        |---
        ||A
        ||---
        ||B ∧ C (→E) 1,2
        ||B     (∧E1) 3
        |A → B  (→I) 2-4
        """
    )
  ,
    ( Text
"Contraposition"
    , Text -> Proof
readProof
        Text
"""
        |¬B → ¬A
        |---
        ||A
        ||---
        |||¬B
        |||---
        |||¬A   (→E) 1,3
        |||⊥    (¬E) 2,4
        ||¬¬B   (¬I) 3-5
        ||B     (¬¬E) 6
        | A → B (→I) 2-7
        """
    )
  ]

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

-- * Model

-- | Constructs the initial t'Model' for propositional logic.
initialModelProp ::
  -- | 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
initialModelProp :: URI -> Maybe Proof -> Maybe Bool -> Bool -> Model
initialModelProp 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)]
exampleProofsProp
    [(Text, Text, Int)]
operatorsProp
    []
    []
    [(Text, RuleSpec)]
rulesProp
    URI
uri
    Logic
Prop
 where
  (Text
_, Proof
initialP) : [(Text, Proof)]
_ = [(Text, Proof)]
exampleProofsProp