path: root/source/Felix/Syntax/Abstract.hs

{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE DuplicateRecordFields #-}

-- | Data types for the abstract syntax tree and helper functions
-- for constructing the lexicon.
--
module Felix.Syntax.Abstract
    ( module Felix.Syntax.Abstract
    , module Felix.Syntax.LexicalPhrase
    , module Felix.Syntax.Token
    ) where


import Base
import Felix.Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase)
import Felix.Syntax.Token (Token(..), Located(..))
import Felix.Report.Location

import Control.DeepSeq (NFData)
import Text.Earley.Mixfix (Holey)
import Data.Text qualified as Text
import Numeric.Natural (Natural)

-- | Local "variable-like" symbols that can be captured by binders.
data VarSymbol
    = NamedVarAt Location Text -- ^ A named variable.
    | FreshVarAt Location Int -- ^ A nameless (implicit) variable. Should only come from desugaring.
    deriving (Generic, NFData)

pattern NamedVar :: Text -> VarSymbol
pattern NamedVar x <- NamedVarAt _ x where
    NamedVar x = NamedVarAt Nowhere x

pattern FreshVar :: Int -> VarSymbol
pattern FreshVar n <- FreshVarAt _ n where
    FreshVar n = FreshVarAt Nowhere n

{-# COMPLETE NamedVarAt, FreshVarAt #-}
{-# COMPLETE NamedVar, FreshVar #-}

instance Show VarSymbol where
    showsPrec d = \case
        NamedVarAt _ x ->
            showParen (d > 10) (showString "NamedVar " . showsPrec 11 x)
        FreshVarAt _ n ->
            showParen (d > 10) (showString "FreshVar " . showsPrec 11 n)

instance Eq VarSymbol where
    NamedVarAt _ x == NamedVarAt _ y = x == y
    FreshVarAt _ n == FreshVarAt _ m = n == m
    _ == _ = False

instance Ord VarSymbol where
    compare (NamedVarAt _ x) (NamedVarAt _ y) = compare x y
    compare NamedVarAt{} FreshVarAt{} = LT
    compare FreshVarAt{} NamedVarAt{} = GT
    compare (FreshVarAt _ n) (FreshVarAt _ m) = compare n m

instance Hashable VarSymbol where
    hashWithSalt s = \case
        NamedVarAt _ x -> hashWithSalt s (0 :: Int, x)
        FreshVarAt _ n -> hashWithSalt s (1 :: Int, n)

instance IsString VarSymbol where
    fromString v = NamedVar $ Text.pack v

instance Locatable VarSymbol where
    locate = \case
        NamedVarAt l _ -> l
        FreshVarAt l _ -> l

data Expr
    = ExprVar VarSymbol
    | ExprInteger Location Int
    | ExprOp Location MixfixItem [Expr]
    | ExprStructOp Location StructSymbol (Maybe Expr)
    | ExprFiniteSet Location (NonEmpty Expr)
    | ExprSep Location VarSymbol Expr Stmt
    -- ^ Of the form /@{x ∈ X | P(x)}@/.
    | ExprReplace Location Expr (NonEmpty (VarSymbol,Expr)) (Maybe Stmt)
    -- ^ E.g.: /@{ f(x, y) | x ∈ X, y ∈ Y | P(x, y) }@/.
    | ExprReplacePred Location VarSymbol VarSymbol Expr Stmt
    -- ^ E.g.: /@{ y | \\exists x\\in X. P(x, y) }@/.
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Expr where
    locate = \case
        ExprVar x -> locate x
        ExprInteger l _ -> l
        ExprOp l _ _ -> l
        ExprStructOp l _ _ -> l
        ExprFiniteSet l _ -> l
        ExprSep l _ _ _ -> l
        ExprReplace l _ _ _ -> l
        ExprReplacePred l _ _ _ _ -> l


data LexicalItem = LexicalItem Pattern Marker deriving (Show, Generic, NFData)

instance Eq LexicalItem where
    LexicalItem p _ == LexicalItem p' _ = p == p'

instance Ord LexicalItem where
    compare (LexicalItem p _) (LexicalItem p' _) = compare p p'

instance Hashable LexicalItem where
    hashWithSalt s (LexicalItem p _) = hashWithSalt s p

data LexicalItemSgPl = LexicalItemSgPl (SgPl Pattern) Marker deriving (Show, Generic, NFData)

instance Eq LexicalItemSgPl where
    LexicalItemSgPl p _ == LexicalItemSgPl p' _ = sg p == sg p'

instance Ord LexicalItemSgPl where
    compare (LexicalItemSgPl p _) (LexicalItemSgPl p' _) = compare (sg p) (sg p')

instance Hashable LexicalItemSgPl where
    hashWithSalt s (LexicalItemSgPl p _) = hashWithSalt s (sg p)

data Associativity
  = LeftAssoc
  | NonAssoc
  | RightAssoc
  deriving (Eq, Show, Ord, Generic, Hashable, NFData)

data MixfixItem = MixfixItem Pattern Marker Associativity deriving (Eq, Show, Ord, Generic, Hashable, NFData)

data Pattern = End | HoleCons Pattern | TokenCons Token Pattern deriving (Eq, Show, Ord, Generic, Hashable, NFData)

type FunctionSymbol = MixfixItem

newtype ParameterArity = ParameterArity Natural
    deriving stock (Show, Eq, Ord, Generic)
    deriving newtype (Hashable, NFData)

zeroParameterArity :: ParameterArity
zeroParameterArity = ParameterArity 0

parameterArityOf :: Foldable f => f a -> ParameterArity
parameterArityOf = ParameterArity . fromIntegral . length

parameterArityValue :: ParameterArity -> Natural
parameterArityValue (ParameterArity arity) = arity

data RelationSymbol
    = RelationSymbol Token ParameterArity Marker
    deriving (Show, Eq, Ord, Generic, Hashable, NFData)

newtype StructSymbol = StructSymbol { unStructSymbol :: Text }
    deriving newtype (Show, Eq, Ord, Hashable, NFData)

pattern ElementSymbol, NotElementSymbol :: RelationSymbol
pattern ElementSymbol =
    RelationSymbol (Command "in") (ParameterArity 0) "elem"
pattern NotElementSymbol =
    RelationSymbol (Command "notin") (ParameterArity 0) "notelem"

pattern EqSymbol, NeqSymbol, SubseteqSymbol :: RelationSymbol
pattern EqSymbol =
    RelationSymbol (Symbol "=") (ParameterArity 0) "eq"
pattern NeqSymbol =
    RelationSymbol (Command "neq") (ParameterArity 0) "neq"
pattern SubseteqSymbol =
    RelationSymbol (Command "subseteq") (ParameterArity 0) "subseteq"

-- | The ordinary source-level @cons@ function symbol.
--
-- Finite-set notation is intrinsic and does not desugar through this symbol.
pattern ConsSymbol :: FunctionSymbol
pattern ConsSymbol =
    MixfixItem
        (TokenCons (Command "cons")
            (TokenCons InvisibleBraceL
                (HoleCons
                    (TokenCons InvisibleBraceR
                        (TokenCons InvisibleBraceL
                            (HoleCons
                                (TokenCons InvisibleBraceR End)))))))
        "cons"
        NonAssoc

-- | The predefined @pair@ function symbol used for desugaring tuple notation..
pattern PairSymbol :: FunctionSymbol
pattern PairSymbol =
    MixfixItem
        (TokenCons (Command "pair")
            (TokenCons InvisibleBraceL
                (HoleCons
                    (TokenCons InvisibleBraceR
                        (TokenCons InvisibleBraceL
                            (HoleCons
                                (TokenCons InvisibleBraceR End)))))))
        "pair"
        NonAssoc

-- | The concrete binary-tuple surface recognized by the dedicated tuple
-- grammar. It lowers to 'PairSymbol'.
tupleSurfacePattern :: Pattern
tupleSurfacePattern =
    TokenCons ParenL
        (HoleCons
            (TokenCons (Symbol ",")
                (HoleCons
                    (TokenCons ParenR End))))

-- | The predefined unordered-pair function symbol.
pattern UpairSymbol :: FunctionSymbol
pattern UpairSymbol =
    MixfixItem
        (TokenCons (Command "upair")
            (TokenCons InvisibleBraceL
                (HoleCons
                    (TokenCons InvisibleBraceR
                        (TokenCons InvisibleBraceL
                            (HoleCons
                                (TokenCons InvisibleBraceR End)))))))
        "upair"
        NonAssoc

-- | The fixed family-union function symbol.
pattern UnionsSymbol :: FunctionSymbol
pattern UnionsSymbol =
    MixfixItem
        (TokenCons (Command "unions")
            (TokenCons InvisibleBraceL
                (HoleCons
                    (TokenCons InvisibleBraceR End))))
        "unions"
        NonAssoc

-- | Function application /@f(x)@/ desugars to /@\apply{f}{x}@/.
pattern ApplySymbol :: FunctionSymbol
pattern ApplySymbol =
    MixfixItem
        (TokenCons (Command "apply")
            (TokenCons InvisibleBraceL
                (HoleCons
                    (TokenCons InvisibleBraceR
                        (TokenCons InvisibleBraceL
                            (HoleCons
                                (TokenCons InvisibleBraceR End)))))))
        "apply"
        NonAssoc

pattern DomSymbol :: FunctionSymbol
pattern DomSymbol =
    MixfixItem
        (TokenCons (Command "dom")
            (TokenCons InvisibleBraceL
                (HoleCons
                    (TokenCons InvisibleBraceR End))))
        "dom"
        NonAssoc

pattern CarrierSymbol :: StructSymbol
pattern CarrierSymbol = StructSymbol "carrier"

patternFromHoley :: Holey Token -> Pattern
patternFromHoley = foldr step End
    where
        step = \case
            Nothing -> HoleCons
            Just tok -> TokenCons tok

patternToHoley :: Pattern -> Holey Token
patternToHoley = \case
    End -> []
    HoleCons pat -> Nothing : patternToHoley pat
    TokenCons tok pat -> Just tok : patternToHoley pat

mixfixPattern :: MixfixItem -> Pattern
mixfixPattern (MixfixItem pat _ _) = pat

mixfixMarker :: MixfixItem -> Marker
mixfixMarker (MixfixItem _ m _) = m

mixfixAssoc :: MixfixItem -> Associativity
mixfixAssoc (MixfixItem _ _ assoc) = assoc

mkMixfixItem :: Holey Token -> Marker -> Associativity -> MixfixItem
mkMixfixItem pat m assoc = MixfixItem (patternFromHoley pat) m assoc

lexicalItemPattern :: LexicalItem -> Pattern
lexicalItemPattern (LexicalItem pat _) = pat

lexicalItemMarker :: LexicalItem -> Marker
lexicalItemMarker (LexicalItem _ m) = m

lexicalItemPhrase :: LexicalItem -> LexicalPhrase
lexicalItemPhrase = patternToHoley . lexicalItemPattern

lexicalItemSgPlPattern :: LexicalItemSgPl -> SgPl Pattern
lexicalItemSgPlPattern (LexicalItemSgPl pat _) = pat

lexicalItemSgPlMarker :: LexicalItemSgPl -> Marker
lexicalItemSgPlMarker (LexicalItemSgPl _ m) = m

lexicalItemSgPlPhrase :: LexicalItemSgPl -> SgPl LexicalPhrase
lexicalItemSgPlPhrase = fmap patternToHoley . lexicalItemSgPlPattern

mkLexicalItem :: LexicalPhrase -> Marker -> LexicalItem
mkLexicalItem pat m = LexicalItem (patternFromHoley pat) m

mkLexicalItemSgPl :: SgPl LexicalPhrase -> Marker -> LexicalItemSgPl
mkLexicalItemSgPl pat m = LexicalItemSgPl (patternFromHoley <$> pat) m

relationSymbolToken :: RelationSymbol -> Token
relationSymbolToken (RelationSymbol tok _ _) = tok

relationSymbolParameterArity :: RelationSymbol -> ParameterArity
relationSymbolParameterArity (RelationSymbol _ arity _) = arity

relationSymbolMarker :: RelationSymbol -> Marker
relationSymbolMarker (RelationSymbol _ _ m) = m

relationSymbolPattern :: RelationSymbol -> Pattern
relationSymbolPattern rel =
    HoleCons (TokenCons (relationSymbolToken rel) (HoleCons End))

structSymbolPattern :: StructSymbol -> Pattern
structSymbolPattern (StructSymbol c) = TokenCons (Command c) End

patternToken :: Pattern -> Maybe Token
patternToken = \case
    TokenCons tok End -> Just tok
    _ -> Nothing

markerFromToken :: Token -> Marker
markerFromToken = \case
    Word w -> Marker w
    Symbol s -> Marker s
    Command c -> Marker c
    Integer n -> Marker (Text.pack (show n))
    tok -> error ("markerFromToken: unsupported token " <> show tok)

pattern ExprConst :: Location -> Token -> Expr
pattern ExprConst l c <- ExprOp l (MixfixItem (TokenCons c End) _ NonAssoc) []
    where
        ExprConst l c = ExprOp l (MixfixItem (TokenCons c End) (markerFromToken c) NonAssoc) []

pattern ExprApp :: Location -> Expr -> Expr -> Expr
pattern ExprApp loc e1 e2 = ExprOp loc ApplySymbol [e1, e2]

pattern ExprPair :: Location -> Expr -> Expr -> Expr
pattern ExprPair loc e1 e2 = ExprOp loc PairSymbol [e1, e2]

-- | Tuples are interpreted as nested pairs:
-- the triple /@(a, b, c)@/ is interpreted as
-- /@(a, (b, c))@/.
-- This means that the product operation should also
-- be right associative, so that /@(a, b, c)@/ can
-- form elements of /@A\times B\times C@/.
makeTuple :: Location -> NonEmpty Expr -> Expr
makeTuple l = \case
    e :| [] -> e
    e :| (e' : es) -> ExprPair l e (makeTuple l (e' :| es))


data Chain
    = ChainBase (NonEmpty Expr) Sign Relation (NonEmpty Expr) -- left arguments, possibly empty list of parameters, right arguments
    | ChainCons (NonEmpty Expr) Sign Relation Chain
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Chain where
    locate (ChainBase lhs _ _ _) = locate lhs
    locate (ChainCons lhs _ _ _) = locate lhs

data Relation
    = Relation Location RelationSymbol [Expr] -- ^  E.g.: /@x \in X@/, potentially with parameters in braces
    | RelationExpr Location Expr   -- ^  E.g.: /@x \mathrel{R} y@/
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Relation where
    locate = \case
        Relation l _ _ -> l
        RelationExpr l _ -> l

data Sign = Positive | Negative deriving (Show, Eq, Ord, Generic, NFData)

data Formula
    = FormulaChain Chain
    | FormulaPredicate Location PrefixPredicate Marker (NonEmpty Expr)
    | Connected Location Connective Formula Formula
    | FormulaNeg Location Formula
    | FormulaQuantified Location Quantifier (NonEmpty VarSymbol) Bound Formula
    | PropositionalConstant Location PropositionalConstant
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Formula where
    locate = \case
        FormulaChain chain -> locate chain
        FormulaPredicate l _ _ _ -> l
        Connected l _ _ _ -> l
        FormulaNeg l _ -> l
        FormulaQuantified l _ _ _ _ -> l
        PropositionalConstant l _ -> l

data PropositionalConstant = IsBottom | IsTop
    deriving (Show, Eq, Ord, Generic, Hashable, NFData)

data PrefixPredicate
    = PrefixPredicate Text Int
    deriving (Show, Eq, Ord, Generic, Hashable, NFData)


data Connective
    = Conjunction
    | Disjunction
    | Implication
    | Equivalence
    | ExclusiveOr
    | NegatedDisjunction
    deriving (Show, Eq, Ord, Generic, Hashable, NFData)



mixfixLoc :: Locatable a => Holey (Located Token) -> [a] -> Location
mixfixLoc parts args0 = go parts args0
    where
        go [] _ = Nowhere
        go (Just ltok : _parts') _args' = startPos ltok
        go (Nothing : parts') (a : args')
            | locate a == Nowhere = go parts' args'
            | otherwise = locate a
        go (Nothing : parts') [] = go parts' []

makeConnective :: Holey (Located Token) -> [Formula] -> Formula
makeConnective parts@[Nothing, Just Located{unLocated = Command "implies"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Implication  f1 f2
makeConnective parts@[Nothing, Just Located{unLocated = Command "land"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Conjunction f1 f2
makeConnective parts@[Nothing, Just Located{unLocated = Command "lor"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Disjunction f1 f2
makeConnective parts@[Nothing, Just Located{unLocated = Command "iff"}, Nothing] [f1, f2] = Connected (mixfixLoc parts [f1, f2]) Equivalence f1 f2
makeConnective parts@[Just Located{unLocated = Command "lnot"}, Nothing] [f1] = FormulaNeg (mixfixLoc parts [f1]) f1
makeConnective pat _ = error ("makeConnective does not handle the following connective correctly: " <> show pat)



type StructPhrase = LexicalItemSgPl

-- | For example 'an integer' would be
-- > Noun (unsafeReadPhrase "integer[/s]") []
type Noun = NounOf Term
data NounOf a
    = Noun Location LexicalItemSgPl [a]
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (NounOf a) where
    locate (Noun l _ _) = l




type NounPhrase t = NounPhraseOf t Term
-- NOTE: 'NounPhraseOf' is only used with arguments of type 'Term',
-- but keeping the argument parameter @a@ allows the 'Show' and 'Eq'
-- instances to remain decidable.
data NounPhraseOf t a
    = NounPhrase [AdjLOf a] (NounOf a) (t VarSymbol) [AdjROf a] (Maybe Stmt)
    deriving (Generic)

instance (Show a, Show (t VarSymbol)) => Show (NounPhraseOf t a) where
    show (NounPhrase ls n vs rs ms) =
        "NounPhrase ("
            <> show ls <> ") ("
            <> show n <> ") ("
            <> show vs <> ") ("
            <> show rs <> ") ("
            <> show ms <> ")"

instance (Eq a, Eq (t VarSymbol)) => Eq (NounPhraseOf t a) where
    NounPhrase ls n vs rs ms == NounPhrase ls' n' vs' rs' ms' =
        ls == ls' && n == n' && vs == vs' && rs == rs' && ms == ms'

-- Raw syntax uses this lexicographic order for deterministic deduplication.
instance (Ord a, Ord (t VarSymbol)) => Ord (NounPhraseOf t a) where
    NounPhrase ls n vs rs ms `compare` NounPhrase ls' n' vs' rs' ms' =
        compare
            (ls, n, vs, rs, ms)
            (ls', n', vs', rs', ms')

instance
    (NFData a, NFData (t VarSymbol))
    => NFData (NounPhraseOf t a)

-- | @Nameless a@ is quivalent to @Const () a@ (from "Data.Functor.Const").
-- It describes a container that is unwilling to actually contain something.
-- @Nameless@ lets us treat nouns with no names, one name, or many names uniformly.
-- Thus @NounPhraseOf Nameless a@ is a noun phrase without a name and with arguments
-- of type @a@.
data Nameless a = Nameless deriving (Show, Eq, Ord, Generic, NFData)


-- | Left adjectives modify nouns from the left side,
-- e.g. /@even@/, /@continuous@/, and /@σ-finite@/.
type AdjL = AdjLOf Term
data AdjLOf a
    = AdjL Location LexicalItem [a]
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (AdjLOf a) where
    locate (AdjL l _ _) = l


-- | Right attributes consist of basic right adjectives, e.g.
-- /@divisible by ?@/, or /@of finite type@/ and verb phrases
-- marked with /@that@/, such as /@integer that divides n@/.
-- In some cases these right attributes may be followed
-- by an additional such-that phrase.
type AdjR = AdjROf Term
data AdjROf a
    = AdjR Location LexicalItem [a]
    | AttrRThat VerbPhrase
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (AdjROf a) where
    locate (AdjR l _ _) = l
    locate (AttrRThat vp) = locate vp

-- | Adjectives for parts of the AST where adjectives are not used
-- to modify nouns and the L/R distinction does not matter, such as
-- when then are used together with a copula (like /@n is even@/).
type Adj = AdjOf Term
data AdjOf a
    = Adj Location LexicalItem [a]
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (AdjOf a) where
    locate (Adj l _ _) = l


type Verb = VerbOf Term
data VerbOf a
    = Verb Location LexicalItemSgPl [a]
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (VerbOf a) where
    locate (Verb l _ _) = l


type Fun = FunOf Term
data FunOf a
    = Fun {loc :: Location, phrase :: LexicalItemSgPl, funArgs :: [a]}
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (FunOf a) where
    locate = (.loc)


type VerbPhrase = VerbPhraseOf Term
data VerbPhraseOf a
    = VPVerb (VerbOf a)
    | VPAdj (NonEmpty (AdjOf a)) -- ^ @x is foo@ / @x is foo and bar@
    | VPVerbNot (VerbOf a)
    | VPAdjNot (NonEmpty (AdjOf a)) -- ^ @x is not foo@ / @x is neither foo nor bar@
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable (VerbPhraseOf a) where
    locate = \case
        VPVerb v -> locate v
        VPAdj adjs -> locate adjs
        VPVerbNot v -> locate v
        VPAdjNot adjs -> locate adjs


data Quantifier
    = Universally
    | Existentially
    | Nonexistentially
    deriving (Show, Eq, Ord, Generic, NFData)

data QuantPhrase = QuantPhrase Quantifier (NounPhrase []) deriving (Show, Eq, Ord, Generic, NFData)


data Term
    = TermExpr Expr
    -- ^ A symbolic expression.
    | TermFun Fun
    -- ^ Definite noun phrase, e.g. /@the derivative of $f$@/.
    | TermIota Location VarSymbol Stmt
    -- ^ Definite descriptor, e.g. /@an $x$ such that ...@//
    | TermQuantified Quantifier Location (NounPhrase Maybe)
    -- ^ Indefinite quantified notion, e.g. /@every even integer that divides $k$ ...@/.
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Term where
    locate :: Term -> Location
    locate (TermExpr e) = locate e
    locate (TermFun f) = f.loc
    locate (TermIota l _ _) = l
    locate (TermQuantified _ l _) = l


data Stmt
    = StmtFormula {formula :: Formula} -- ^ E.g.: /@We have \<Formula\>@/.
    | StmtVerbPhrase {args :: NonEmpty Term, verb :: VerbPhrase} -- ^ E.g.: /@\<Term\> and \<Term\> \<verb\>@/.
    | StmtNoun {args :: NonEmpty Term, noun :: (NounPhrase Maybe)} -- ^ E.g.: /@\<Term\> is a(n) \<NP\>@/.
    | StmtStruct {arg :: Term, struct :: StructPhrase}
    | StmtNeg {loc :: Location, stmt :: Stmt} -- ^ E.g.: /@It is not the case that \<Stmt\>@/.
    | StmtExists {loc :: Location, np :: NounPhrase []} -- ^ E.g.: /@There exists a(n) \<NP\>@/.
    | StmtConnected {conn :: Connective, mloc :: Maybe Location, stmt1 :: Stmt, stmt2 :: Stmt}
    | StmtQuantPhrase {loc :: Location, qp :: QuantPhrase, stmt :: Stmt}
    | SymbolicQuantified {loc :: Location, quant :: Quantifier, vars :: NonEmpty VarSymbol, b :: Bound, suchThat :: Maybe Stmt, stmt :: Stmt}
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Stmt where
    locate :: Stmt -> Location
    locate StmtFormula{formula = phi} = locate phi
    locate StmtConnected{mloc = Just p} = p
    locate StmtConnected{mloc = Nothing, stmt1 = s} = locate s
    locate StmtVerbPhrase{args = a :| _} = locate a
    locate StmtNoun{args = a :| _} = locate a
    locate StmtStruct{arg = a} = locate a
    locate StmtNeg{loc = p} = p
    locate StmtExists{loc = p} = p
    locate StmtQuantPhrase{loc = p} = p
    locate SymbolicQuantified{loc = p} = p

data Bound = Unbounded | Bounded Location Sign Relation Expr deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Bound where
    locate = \case
        Unbounded -> Nowhere
        Bounded l _ _ _ -> l

pattern SymbolicForall :: Location -> NonEmpty VarSymbol -> Bound -> Maybe Stmt -> Stmt -> Stmt
pattern SymbolicForall loc vs bound suchThat have = SymbolicQuantified loc Universally vs bound suchThat have

pattern SymbolicExists :: Location -> NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
pattern SymbolicExists loc vs bound suchThat = SymbolicQuantified loc Existentially vs bound Nothing suchThat

makeSymbolicNotExists :: Location -> NonEmpty VarSymbol -> Bound -> Stmt -> Stmt
makeSymbolicNotExists p vs bound st = StmtNeg p (SymbolicExists p vs bound st)

data Asm
    = AsmSuppose Stmt
    | AsmLetNoun (NonEmpty VarSymbol) (NounPhrase Maybe) -- ^ E.g.: /@let k be an integer@/
    | AsmLetIn (NonEmpty VarSymbol) Expr -- ^ E.g.: /@let $k\in\integers$@/
    | AsmLetThe VarSymbol Fun -- ^ E.g.: /@let $g$ be the derivative of $f$@/
    | AsmLetEq VarSymbol Expr -- ^ E.g.: /@let $m = n + k$@/
    | AsmLetStruct VarSymbol StructPhrase -- ^ E.g.: /@let $A$ be a monoid@/
    deriving (Show, Eq, Ord, Generic, NFData)

data Axiom = Axiom [Asm] Stmt
    deriving (Show, Eq, Ord, Generic, NFData)

data Claim = Claim [Asm] Stmt
    deriving (Show, Eq, Ord, Generic, NFData)

-- | The head of the definition describes the part before the /@iff@/,
-- i.e. the definiendum. An optional noun-phrase corresponds to an optional
-- type annotation for the 'Term' of the head. The last part of the head
-- is the lexical phrase that is defined.
--
-- > "A natural number   $n$        divides $m$   iff   ..."
-- >  ^^^^^^^^^^^^^^^^   ^^^        ^^^^^^^^^^^         ^^^
-- >  type annotation    variable   verb                definiens
-- >  (a noun phrase)               (all args are vars) (a statement)
--
data DefnHead
    = DefnAdj (Maybe (NounPhrase Maybe)) VarSymbol (AdjOf VarSymbol)
    | DefnVerb (Maybe (NounPhrase Maybe)) VarSymbol (VerbOf VarSymbol)
    | DefnNoun VarSymbol (NounOf VarSymbol)
    | DefnSymbolicPredicate PrefixPredicate Marker (NonEmpty VarSymbol)
    | DefnRel VarSymbol RelationSymbol [VarSymbol] VarSymbol
    -- ^ E.g.: /@$x \subseteq y$ iff [...@/
    deriving (Show, Eq, Ord, Generic, NFData)

data Defn
    = Defn [Asm] DefnHead Stmt
    | DefnFun [Asm] (FunOf VarSymbol) (Maybe Term) Term
    -- ^ A 'DefnFun' consists of the functional noun (which must start with /@the@/)
    -- and an optional specification of a symbolic equivalent. The symbolic equivalent
    -- does not need to have the same variables as the full functional noun pattern.
    --
    -- > "The tensor product of $U$ and $V$ over $K$, $U\tensor V$, is ..."
    -- >  ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^  ^^^^^^^^^^^^     ^^^
    -- >  definiendum                                 symbolic eqv.    definiens
    -- >  (a functional noun)                         (an exression)   (a term)
    --
    | DefnOp SymbolPattern Expr
    deriving (Show, Eq, Ord, Generic, NFData)

data CalcQuantifier
    = CalcQuantifier (NonEmpty VarSymbol) Bound (Maybe Stmt)
    deriving (Show, Eq, Ord, Generic, NFData)

data Proof
    = Omitted Location
    | Qed (Maybe Location) Justification
    -- ^ Ends of a proof, leaving automation to discharge the current goal using the given justification.
    | Contradiction Location Justification
    -- ^ Ends a proof by deriving absurdity using the given justification.
    | ByCase Location [Case]
    | ByContradiction Location Proof
    | BySetInduction Location (Maybe Term) Proof
    -- ^ ∈-induction.
    | ByOrdInduction Location Proof
    -- ^ Transfinite induction for ordinals.
    | Assume Location Stmt Proof
    | FixSymbolic Location (NonEmpty VarSymbol) Bound Proof
    | FixSuchThat Location (NonEmpty VarSymbol) Stmt Proof
    | Calc Location (Maybe CalcQuantifier) Calc Proof
    -- ^ Simplify goals that are implications or disjunctions.
    | TakeVar Location (NonEmpty VarSymbol) Bound Stmt Justification Proof
    | TakeNoun Location (NounPhrase []) Justification Proof
    | Have Location (Maybe Stmt) Stmt Justification Proof
    -- ^ /@Since \<stmt\>, we have \<stmt\> by \<ref\>.@/
    | Suffices Location Stmt Justification Proof
    -- ^ /@It suffices to show that [...]. [...]@/
    | Subclaim Location Stmt Proof Proof
    -- ^ A claim is a sublemma with its own proof:
    --  /@Show \<goal stmt\>. \<steps\>. \<continue other proof\>.@/
    | Define Location VarSymbol Expr Proof
    -- ^ Local definition.
    --
    | DefineFunction Location VarSymbol VarSymbol Expr VarSymbol Expr Proof
    -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
    -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
    -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).




    | DefineFunctionLocal Location VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
    -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
    --
    deriving (Show, Eq, Ord, Generic, NFData)

-- | An inline justification.
data Justification
    = JustificationRef (NonEmpty Marker)
    | JustificationSetExt
    | JustificationEmpty
    | JustificationLocal -- ^ Use only local assumptions
    deriving (Show, Eq, Ord, Generic, NFData)


-- | A case of a case split.
data Case = Case
    { caseOf :: Stmt
    , caseProof :: Proof
    } deriving (Show, Eq, Ord, Generic, NFData)

data Calc
    = Equation Expr (NonEmpty (Expr, Justification))
    -- ^ A chain of equalities. Each claimed equality has a (potentially empty) justification.
    -- For example: @a &= b \\explanation{by \\cref{a_eq_b}} &= c@
    -- would be (modulo expr constructors)
    -- @Equation "a" [("b", JustificationRef "a_eq_b"), ("c", JustificationEmpty)]@.
    | Biconditionals Formula (NonEmpty (Formula, Justification))
    deriving (Show, Eq, Ord, Generic, NFData)


data Abbreviation
    = AbbreviationAdj VarSymbol (AdjOf VarSymbol) Stmt
    | AbbreviationVerb VarSymbol (VerbOf VarSymbol) Stmt
    | AbbreviationNoun VarSymbol (NounOf VarSymbol) Stmt
    | AbbreviationRel VarSymbol RelationSymbol [VarSymbol] VarSymbol Stmt
    | AbbreviationFun (FunOf VarSymbol) Term
    | AbbreviationEq SymbolPattern Expr
    deriving (Show, Eq, Ord, Generic, NFData)

data Datatype
    = Datatype
        { datatypeHeadExpr :: Expr
        , datatypeClauses :: NonEmpty DatatypeClause
        }
    deriving (Show, Eq, Ord, Generic, NFData)

data DatatypeClause = DatatypeClause
    { datatypeClauseConstructorExpr :: Expr
    , datatypeClauseTargetExpr :: Expr
    , datatypeClausePremises :: [(VarSymbol, Expr)]
    }
    deriving (Show, Eq, Ord, Generic, NFData)

data Inductive = Inductive
    { inductiveSymbolPattern :: SymbolPattern
    , inductiveDomain :: Expr
    , inductiveIntros :: NonEmpty IntroRule
    }
    deriving (Show, Eq, Ord, Generic, NFData)

data IntroRule = IntroRule
    { introConditions :: [Formula] -- The inductively defined set may only appear as an argument of monotone operations on the rhs.
    , introResult :: Formula -- TODO Refine.
    }
    deriving (Show, Eq, Ord, Generic, NFData)


data SymbolPattern = SymbolPattern FunctionSymbol [VarSymbol]
    deriving (Show, Eq, Ord, Generic, NFData)

data Signature
    = SignatureAdj  VarSymbol (AdjOf  VarSymbol)
    -- The verb and noun forms are available to programmatic AST consumers but
    -- have no concrete source syntax.
    | SignatureVerb VarSymbol (VerbOf VarSymbol)
    | SignatureNoun VarSymbol (NounOf VarSymbol)
    | SignatureSymbolic SymbolPattern (NounPhrase Maybe)
    -- ^ /@$\<symbol\>(\<vars\>)$ is a \<noun\>@/
    deriving (Show, Eq, Ord, Generic, NFData)


data StructDefn = StructDefn
    { structPhrase :: StructPhrase
    -- ^ E.g.: @partial order@ or @abelian group@.\
    , structParents :: [StructPhrase]
    -- ^ Structural parents
    , structLabel :: VarSymbol
    , structFixes :: [StructSymbol]
    -- ^ List of text for commands representing constants not inherited from its parents,
    -- e.g.: @\sqsubseteq@ or @\inv@.
    , structAssumes :: [(Marker, Stmt)]
    }
    deriving (Show, Eq, Ord, Generic, NFData)

newtype Marker = Marker Text
    deriving stock (Show, Eq, Ord, Generic)

deriving newtype instance Hashable Marker
deriving newtype instance NFData Marker

instance IsString Marker where
    fromString str = Marker (Text.pack str)

type BlockTitle = [Token]

data ClaimKind
    = Proposition
    | Theorem
    | Lemma
    | Corollary
    | PlainClaim
    deriving (Show, Eq, Ord, Generic, NFData)

data Block
    = BlockAxiom Location (Maybe BlockTitle) Marker Axiom
    | BlockClaim ClaimKind Location (Maybe BlockTitle) Marker Claim
    | BlockProof Location Proof Location -- ^ Proof start and ending location.
    | BlockDefn Location (Maybe BlockTitle) Marker Defn
    | BlockAbbr Location (Maybe BlockTitle) Marker Abbreviation
    | BlockData Location (Maybe BlockTitle) Marker Datatype
    | BlockInductive Location (Maybe BlockTitle) Marker Inductive
    | BlockSig Location (Maybe BlockTitle) Marker [Asm] Signature
    | BlockStruct Location (Maybe BlockTitle) Marker StructDefn
    deriving (Show, Eq, Ord, Generic, NFData)

instance Locatable Block where
    locate = \case
        BlockAxiom location _title _marker _axiom -> location
        BlockClaim _kind location _title _marker _claim -> location
        BlockProof location _proof _end -> location
        BlockDefn location _title _marker _definition -> location
        BlockAbbr location _title _marker _abbreviation -> location
        BlockData location _title _marker _datatype -> location
        BlockInductive location _title _marker _inductive -> location
        BlockSig location _title _marker _assumptions _signature -> location
        BlockStruct location _title _marker _structure -> location