diff options
Diffstat (limited to 'source/Syntax/Abstract.hs')
| -rw-r--r-- | source/Syntax/Abstract.hs | 850 |
1 files changed, 0 insertions, 850 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs deleted file mode 100644 index f589283..0000000 --- a/source/Syntax/Abstract.hs +++ /dev/null @@ -1,850 +0,0 @@ -{-# 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 Syntax.Abstract - ( module Syntax.Abstract - , module Syntax.LexicalPhrase - , module Syntax.Token - ) where - - -import Base -import Syntax.LexicalPhrase (LexicalPhrase, SgPl(..), unsafeReadPhraseSgPl, unsafeReadPhrase) -import Syntax.Token (Token(..), Located(..)) -import 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 predefined @cons@ function symbol used for desugaring finite set expressions. -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 - --- | 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 |