{-# 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 \@/. | StmtVerbPhrase {args :: NonEmpty Term, verb :: VerbPhrase} -- ^ E.g.: /@\ and \ \@/. | StmtNoun {args :: NonEmpty Term, noun :: (NounPhrase Maybe)} -- ^ E.g.: /@\ is a(n) \@/. | StmtStruct {arg :: Term, struct :: StructPhrase} | StmtNeg {loc :: Location, stmt :: Stmt} -- ^ E.g.: /@It is not the case that \@/. | StmtExists {loc :: Location, np :: NounPhrase []} -- ^ E.g.: /@There exists a(n) \@/. | 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 \, we have \ by \.@/ | 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 \. \. \.@/ | 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) -- ^ /@$\(\)$ is a \@/ 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