diff options
Diffstat (limited to 'source/Syntax')
| -rw-r--r-- | source/Syntax/Abstract.hs | 863 | ||||
| -rw-r--r-- | source/Syntax/Adapt.hs | 928 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 1032 | ||||
| -rw-r--r-- | source/Syntax/Concrete/Keywords.hs | 228 | ||||
| -rw-r--r-- | source/Syntax/Interface.hs | 887 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 830 | ||||
| -rw-r--r-- | source/Syntax/LexicalPhrase.hs | 95 | ||||
| -rw-r--r-- | source/Syntax/Lexicon.hs | 330 | ||||
| -rw-r--r-- | source/Syntax/Mixfix.hs | 139 | ||||
| -rw-r--r-- | source/Syntax/Pragma.hs | 250 | ||||
| -rw-r--r-- | source/Syntax/Token.hs | 633 |
11 files changed, 0 insertions, 6215 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs deleted file mode 100644 index 76ce6b6..0000000 --- a/source/Syntax/Abstract.hs +++ /dev/null @@ -1,863 +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 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 diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs deleted file mode 100644 index f496ead..0000000 --- a/source/Syntax/Adapt.hs +++ /dev/null @@ -1,928 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE ApplicativeDo #-} -{-# LANGUAGE RecordWildCards #-} - -module Syntax.Adapt - ( FunctionPatternError(..) - , LexicalScanError(..) - , ScannedLexicalItem(..) - , scannedItemMarker - , canonicalScannedItem - , SyntaxMaterializationError(..) - , materializeSyntaxDelta - , scanChunk - ) where - -import Base -import Syntax.Abstract -import Syntax.Interface -import Syntax.Lexicon -import Report.Location - -import Control.Monad (foldM) -import Data.Bifunctor qualified as Bifunctor -import Data.Map.Strict qualified as Map -import Data.Maybe (catMaybes) -import Data.Set qualified as Set -import Data.Sequence qualified as Seq -import Data.Text qualified as Text -import Numeric.Natural (Natural) -import Text.Regex.Applicative qualified as RE -import Text.Regex.Applicative (RE) - -data FunctionPatternError - = FunctionPatternEmpty - | FunctionPatternBareVariable - | FunctionPatternReservedApplication - deriving (Show, Eq) - -data LexicalScanError - = MalformedLexicalEnvironment !Location !Text - | InvalidFunctionPattern !Location !FunctionPatternError - | MalformedDatatype !Location !Text - deriving (Eq) - -instance Show LexicalScanError where - show = \case - MalformedLexicalEnvironment location environment -> - "could not find a lexical pattern in " - <> Text.unpack environment - <> " at " - <> prettyLocation location - InvalidFunctionPattern location problem -> - functionPatternErrorMessage problem - <> " at " - <> prettyLocation location - MalformedDatatype location problem -> - "malformed datatype declaration at " - <> prettyLocation location - <> ": " - <> Text.unpack problem - -scanChunk - :: [Located Token] - -> Either LexicalScanError [Located ScannedLexicalItem] -scanChunk ltoks = - case ltoks of - first@Located{startPos = pos, unLocated = BeginEnv "definition"} : _ -> - locateAt first - <$> (matchOrErr (definition pos) "definition" pos >>= id) - first@Located{startPos = pos, unLocated = BeginEnv "signature"} : _ -> - locateAt first - <$> (matchOrErr (signatureExtension pos) "signature" pos >>= id) - first@Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ -> - locateAt first - <$> (matchOrErr (abbreviation pos) "abbreviation" pos >>= id) - first@Located{startPos = pos, unLocated = BeginEnv "struct"} : _ -> - locateStructItems first ltoks - <$> matchOrErr structRE "struct definition" pos - first@Located{startPos = pos, unLocated = BeginEnv "inductive"} : _ -> - locateAt first - <$> (matchOrErr (inductive pos) "inductive definition" pos >>= id) - Located{startPos = pos, unLocated = BeginEnv "datatype"} : _ -> - scanDatatypeChunk pos ltoks - _ -> - Right [] - where - toks = unLocated <$> ltoks - - matchOrErr - :: RE Token a - -> Text - -> Location - -> Either LexicalScanError a - matchOrErr re environment location = - case RE.match re toks of - Nothing -> - Left - (MalformedLexicalEnvironment - location - environment) - Just result -> - Right result - - locateAt first items = - [item <$ first | item <- items] - -data ScannedLexicalItem - = ScanAdj LexicalPhrase Marker - | ScanFun LexicalPhrase Marker - | ScanNoun LexicalPhrase Marker - | ScanStructNoun LexicalPhrase Marker - | ScanVerb LexicalPhrase Marker - | ScanRelationSymbol Token ParameterArity Marker - | ScanFunctionSymbol Pattern Marker - | ScanPrefixPredicate PrefixPredicate Marker - | ScanStructOp Text -- we an use the command text as export name. - deriving (Show, Eq, Ord) - -scannedItemMarker :: ScannedLexicalItem -> Marker -scannedItemMarker = \case - ScanAdj _item marker -> - marker - ScanFun _item marker -> - marker - ScanNoun _item marker -> - marker - ScanStructNoun _item marker -> - marker - ScanVerb _item marker -> - marker - ScanRelationSymbol _token _arity marker -> - marker - ScanFunctionSymbol _pattern marker -> - marker - ScanPrefixPredicate _predicate marker -> - marker - ScanStructOp commandText -> - Marker commandText - -canonicalScannedItem - :: Fixity - -> ScannedLexicalItem - -> CanonicalLexicalEntry -canonicalScannedItem fixity = \case - ScanAdj phrase marker - | isAdjR phrase -> - CanonicalRightAdjective - (patternFromHoley phrase) - marker - | otherwise -> - CanonicalLeftAdjective - (patternFromHoley phrase) - marker - ScanFun phrase marker -> - canonicalSgPl - CanonicalFunctionPhrase - (guessNounPlural phrase) - marker - ScanNoun phrase marker -> - canonicalSgPl - CanonicalNoun - (guessNounPlural phrase) - marker - ScanStructNoun phrase marker -> - canonicalSgPl - CanonicalStructureNoun - (guessNounPlural phrase) - marker - ScanVerb phrase marker -> - canonicalSgPl - CanonicalVerb - (guessVerbPlural phrase) - marker - ScanRelationSymbol token arity marker -> - CanonicalRelation token arity marker - ScanFunctionSymbol pat marker -> - CanonicalExpressionFunction - (if pat == tupleSurfacePattern - then mixfixPattern PairSymbol - else pat) - marker - fixity - ScanPrefixPredicate - (PrefixPredicate commandText arity) - marker -> - CanonicalPrefixPredicate - commandText - (fromIntegral arity) - marker - ScanStructOp commandText -> - CanonicalStructureOperation commandText - where - canonicalSgPl constructor phrases marker = - constructor - (patternFromHoley (sg phrases)) - (patternFromHoley (pl phrases)) - marker - -data SyntaxMaterializationError - = MaterializedSyntaxCollision !CanonicalSyntaxCollision - | PrefixPredicateArityOutOfRange !Natural - deriving (Show, Eq) - -materializeSyntaxDelta - :: CanonicalSyntaxDelta - -> Either SyntaxMaterializationError Lexicon -materializeSyntaxDelta delta = do - combined <- - Bifunctor.first MaterializedSyntaxCollision - (canonicalSyntaxDelta - (fixedBaseSyntaxEntries - <> canonicalSyntaxDeltaEntries delta)) - foldM - insertCanonicalEntry - builtins - [ entry - | entry <- canonicalSyntaxDeltaEntries combined - , entry `Set.notMember` fixedEntries - ] - where - fixedEntries = - Set.fromList fixedBaseSyntaxEntries - -insertCanonicalEntry - :: Lexicon - -> CanonicalLexicalEntry - -> Either SyntaxMaterializationError Lexicon -insertCanonicalEntry lexicon@Lexicon{..} entry = do - extended <- case entry of - CanonicalLeftAdjective pat marker -> - pure - lexicon - { lexiconAdjLs = - lexicalItem pat marker : lexiconAdjLs - } - CanonicalRightAdjective pat marker -> - pure - lexicon - { lexiconAdjRs = - lexicalItem pat marker : lexiconAdjRs - } - CanonicalFunctionPhrase singular plural marker -> - pure - lexicon - { lexiconFuns = - lexicalItemSgPl singular plural marker - : lexiconFuns - } - CanonicalNoun singular plural marker -> - pure - lexicon - { lexiconNouns = - lexicalItemSgPl singular plural marker - : lexiconNouns - } - CanonicalStructureNoun singular plural marker -> - pure - lexicon - { lexiconStructNouns = - lexicalItemSgPl singular plural marker - : lexiconStructNouns - } - CanonicalVerb singular plural marker -> - pure - lexicon - { lexiconVerbs = - lexicalItemSgPl singular plural marker - : lexiconVerbs - } - CanonicalRelation token arity marker -> - pure - lexicon - { lexiconRelationSymbols = - RelationSymbol token arity marker - : lexiconRelationSymbols - } - CanonicalExpressionFunction - pat - marker - (Fixity associativity level) -> - pure - lexicon - { lexiconMixfixTable = - Seq.adjust - (Map.insert - pat - (MixfixItem - pat - marker - associativity)) - (fromIntegral - (mixfixLevelValue level)) - lexiconMixfixTable - } - CanonicalPrefixPredicate commandText arity marker -> do - runtimeArity <- - if arity <= fromIntegral (maxBound :: Int) - then pure (fromIntegral arity) - else - Left - (PrefixPredicateArityOutOfRange arity) - pure - lexicon - { lexiconPrefixPredicates = - (PrefixPredicate commandText runtimeArity, marker) - : lexiconPrefixPredicates - } - CanonicalStructureOperation commandText -> - pure - lexicon - { lexiconStructFun = - StructSymbol commandText : lexiconStructFun - } - pure extended - where - lexicalItem pat marker = - mkLexicalItem (patternToHoley pat) marker - - lexicalItemSgPl singular plural marker = - mkLexicalItemSgPl - (SgPl - (patternToHoley singular) - (patternToHoley plural)) - marker - -skipUntilNextLexicalEnv :: RE Token [Token] -skipUntilNextLexicalEnv = many (RE.psym otherToken) - where - otherToken tok = tok /= BeginEnv "definition" && tok /= BeginEnv "struct" && tok /= BeginEnv "abbreviation" - -notEndOfLexicalEnvToken :: RE Token Token -notEndOfLexicalEnvToken = RE.psym innerToken - where - innerToken tok = tok /= EndEnv "definition" && tok /= EndEnv "struct" && tok /= EndEnv "abbreviation" - -notEndOfSignatureSentenceToken :: RE Token Token -notEndOfSignatureSentenceToken = RE.psym \case - Symbol "." -> False - EndEnv "signature" -> False - _ -> True - -definition - :: Location - -> RE Token (Either LexicalScanError [ScannedLexicalItem]) -definition location = do - RE.sym (BeginEnv "definition") - RE.few notEndOfLexicalEnvToken - m <- labelRE - RE.few RE.anySym - lexicalItem <- headRE location - RE.few RE.anySym - RE.sym (EndEnv "definition") - skipUntilNextLexicalEnv - pure ((: []) <$> lexicalItem m) - -abbreviation - :: Location - -> RE Token (Either LexicalScanError [ScannedLexicalItem]) -abbreviation location = do - RE.sym (BeginEnv "abbreviation") - RE.few RE.anySym - m <- labelRE - RE.few RE.anySym - lexicalItem <- headRE location - RE.few RE.anySym - RE.sym (EndEnv "abbreviation") - skipUntilNextLexicalEnv - pure ((: []) <$> lexicalItem m) - -signatureExtension - :: Location - -> RE Token (Either LexicalScanError [ScannedLexicalItem]) -signatureExtension location = do - RE.sym (BeginEnv "signature") - RE.few notEndOfLexicalEnvToken - m <- labelRE - RE.few RE.anySym - lexicalItem <- sigHeadRE location - RE.few notEndOfSignatureSentenceToken - RE.sym (Symbol ".") - RE.sym (EndEnv "signature") - skipUntilNextLexicalEnv - pure ((: []) <$> lexicalItem m) - -labelRE :: RE Token Marker -labelRE = RE.msym \case - Label m -> Just (Marker m) - _ -> Nothing - --- | 'RE' that matches the head of a definition. -headRE - :: Location - -> RE Token (Marker -> Either LexicalScanError ScannedLexicalItem) --- Note that @<|>@ is left biased for 'RE', so we can just --- place 'adj' before 'verb' and do not have to worry about --- overlapping patterns. -headRE location = - pureScan ScanNoun <$> nounRE - <|> pureScan ScanAdj <$> adjRE - <|> pureScan ScanVerb <$> verbRE - <|> pureScan ScanFun <$> funRE - <|> relationScan <$> relationSymbolRE - <|> functionScan <$> functionSymbolRE location - <|> pureScan ScanPrefixPredicate <$> prefixPredicate - where - pureScan constructor value marker = - Right (constructor value marker) - - relationScan (token, arity) marker = - Right (ScanRelationSymbol token arity marker) - - functionScan patternResult marker = - (`ScanFunctionSymbol` marker) <$> patternResult - -sigHeadRE - :: Location - -> RE Token (Marker -> Either LexicalScanError ScannedLexicalItem) -sigHeadRE location = - asum - [ signatureHeadRE form - | form <- concreteSignatureHeadForms - ] - where - signatureHeadRE = \case - AdjectiveSignatureHead -> - pureScan ScanAdj <$> sigAdjectiveRE - SymbolicSignatureHead -> - functionScan <$> sigFunctionSymbolRE location - - pureScan constructor value marker = - Right (constructor value marker) - - functionScan patternResult marker = - (`ScanFunctionSymbol` marker) <$> patternResult - -sigAdjectiveRE :: RE Token LexicalPhrase -sigAdjectiveRE = - toLexicalPhrase - <$> ( math var - *> RE.sym (Word "can") - *> RE.sym (Word "be") - *> RE.some - (RE.psym isLexicalPhraseToken <|> math var) - ) - -sigFunctionSymbolRE :: Location -> RE Token (Either LexicalScanError Pattern) -sigFunctionSymbolRE location = do - RE.sym (BeginEnv "math") - toks <- RE.few nonDefinitionKeyword - RE.sym (EndEnv "math") - pure (makeFunctionSymbol location toks) - -inductive - :: Location - -> RE Token (Either LexicalScanError [ScannedLexicalItem]) -inductive location = do - RE.sym (BeginEnv "inductive") - RE.few notEndOfLexicalEnvToken - m <- labelRE - RE.few RE.anySym - lexicalItem <- functionSymbolInductive location - RE.few RE.anySym - RE.sym (EndEnv "inductive") - skipUntilNextLexicalEnv - pure (((: []) . (`ScanFunctionSymbol` m)) <$> lexicalItem) - -scanDatatypeChunk - :: Location - -> [Located Token] - -> Either LexicalScanError [Located ScannedLexicalItem] -scanDatatypeChunk = datatypeLexicalItems - -datatypeLexicalItems - :: Location - -> [Located Token] - -> Either LexicalScanError [Located ScannedLexicalItem] -datatypeLexicalItems environmentLocation toks = do - marker <- requireDatatype - environmentLocation - "missing declaration label" - (findDatatypeLabel toks) - datatypeHeadToks <- requireDatatype - environmentLocation - "missing datatype head" - (findDatatypeHead toks) - constructorToks <- requireDatatype - environmentLocation - "missing constructor enumeration" - (findDatatypeConstructors toks) - let datatypeLocation = - maybe environmentLocation startPos (listToMaybe datatypeHeadToks) - datatypePattern <- makeFunctionSymbol - datatypeLocation - (unLocated <$> datatypeHeadToks) - constructorItems <- traverse makeConstructor constructorToks - pure - ((ScanFunctionSymbol datatypePattern marker - <$ locationTemplate datatypeLocation toks) - : constructorItems) - where - makeConstructor (itemLocation, raw) = do - constructorToks <- requireDatatype - itemLocation - "constructor item has no symbolic declaration" - (itemConstructorToks raw) - let stripped = stripOuterParens constructorToks - markerToken <- constructorMarker itemLocation stripped - constructorPattern <- makeFunctionSymbol - (startPos markerToken) - (unLocated <$> stripped) - pure - (ScanFunctionSymbol - constructorPattern - (markerFromToken (unLocated markerToken)) - <$ markerToken) - -requireDatatype - :: Location - -> Text - -> Maybe a - -> Either LexicalScanError a -requireDatatype location problem = - maybe (Left (MalformedDatatype location problem)) Right - -locationTemplate :: Location -> [Located Token] -> Located Token -locationTemplate location = \case - token : _ -> - token{startPos = location} - [] -> - impossible "datatype scanner has no environment token" - -findDatatypeLabel :: [Located Token] -> Maybe Marker -findDatatypeLabel = \case - [] -> Nothing - Located{unLocated = Label m} : _ -> Just (Marker m) - _ : toks -> findDatatypeLabel toks - -findDatatypeHead :: [Located Token] -> Maybe [Located Token] -findDatatypeHead toks = do - afterLabel <- tailMay =<< dropUntil (isLabel . unLocated) toks - defineToks <- dropUntil ((== Word "define") . unLocated) afterLabel - case defineToks of - _define : Located{unLocated = BeginEnv "math"} : rest -> - takeUntilToken (EndEnv "math") rest - _ -> Nothing - -findDatatypeConstructors - :: [Located Token] - -> Maybe [(Location, [Located Token])] -findDatatypeConstructors toks = do - afterEnumerate <- tailMay - =<< dropUntil ((== BeginEnv "enumerate") . unLocated) toks - enumerateBody <- takeUntilToken (EndEnv "enumerate") afterEnumerate - let items = splitDatatypeItems enumerateBody - guard (not (null items)) - pure items - -splitDatatypeItems - :: [Located Token] - -> [(Location, [Located Token])] -splitDatatypeItems = \case - [] -> - [] - Located{startPos = itemLocation, unLocated = Command "item"} : rest -> - let (item, remaining) = - break ((== Command "item") . unLocated) rest - in (itemLocation, item) : splitDatatypeItems remaining - _ : rest -> - splitDatatypeItems rest - -itemConstructorToks :: [Located Token] -> Maybe [Located Token] -itemConstructorToks toks = do - afterMath <- tailMay =<< dropUntil ((== BeginEnv "math") . unLocated) toks - mathBody <- takeUntilToken (EndEnv "math") afterMath - takeUntilToken (Command "in") mathBody - -constructorMarker - :: Location - -> [Located Token] - -> Either LexicalScanError (Located Token) -constructorMarker fallback = - maybe - (Left - (MalformedDatatype - fallback - "constructor has no marker-bearing head token")) - Right - . find (isConstructorMarkerToken . unLocated) - -isConstructorMarkerToken :: Token -> Bool -isConstructorMarkerToken = \case - Word _ -> True - Symbol _ -> True - Command _ -> True - Integer _ -> True - _ -> False - -stripOuterParens :: [Located Token] -> [Located Token] -stripOuterParens toks - | hasOuterParens toks = case toks of - Located{unLocated = ParenL} : rest -> case reverse rest of - Located{unLocated = ParenR} : innerRev -> reverse innerRev - _ -> toks - _ -> toks - | otherwise = toks - -hasOuterParens :: [Located Token] -> Bool -hasOuterParens = \case - Located{unLocated = ParenL} : rest -> go (1 :: Int) rest - _ -> False - where - go _ [] = False - go depth [Located{unLocated = ParenR}] = depth == 1 - go depth (Located{unLocated = ParenL} : rest) = - go (depth + 1) rest - go depth (Located{unLocated = ParenR} : rest) - | depth <= 0 = False - | otherwise = go (depth - 1) rest - go depth (_ : rest) = go depth rest - -isLabel :: Token -> Bool -isLabel = \case - Label _ -> True - _ -> False - -dropUntil :: (a -> Bool) -> [a] -> Maybe [a] -dropUntil predicate = \case - [] -> Nothing - xs@(x : rest) - | predicate x -> Just xs - | otherwise -> dropUntil predicate rest - -takeUntilToken :: Token -> [Located Token] -> Maybe [Located Token] -takeUntilToken stop = \case - [] -> Nothing - x : xs - | unLocated x == stop -> Just [] - | otherwise -> (x :) <$> takeUntilToken stop xs - -tailMay :: [a] -> Maybe [a] -tailMay = \case - [] -> Nothing - _ : xs -> Just xs - -structRE :: RE Token [ScannedLexicalItem] -structRE = do - RE.sym (BeginEnv "struct") - RE.few RE.anySym - m <- labelRE - RE.few RE.anySym - lexicalItem <- ScanStructNoun . toLexicalPhrase <$> (an *> structPat <* math var) - RE.few RE.anySym - lexicalItems <- structOps <|> pure [] - RE.sym (EndEnv "struct") - skipUntilNextLexicalEnv - pure (lexicalItem m : lexicalItems) - -structOps :: RE Token [ScannedLexicalItem] -structOps = do - RE.sym (BeginEnv "enumerate") - lexicalItems <- many structOp - RE.sym (EndEnv "enumerate") - RE.few RE.anySym - pure lexicalItems - -structOp :: RE Token ScannedLexicalItem -structOp = do - RE.sym (Command "item") - op <- math command - pure (ScanStructOp op) - -locateStructItems - :: Located Token - -> [Located Token] - -> [ScannedLexicalItem] - -> [Located ScannedLexicalItem] -locateStructItems environmentToken toks = \case - [] -> - [] - structureNoun : operations -> - (structureNoun <$ environmentToken) - : zipWith locateOperation operations operationTokens - where - operationTokens = - structOperationTokens toks - <> repeat environmentToken - - locateOperation operation token = - operation <$ token - -structOperationTokens :: [Located Token] -> [Located Token] -structOperationTokens = \case - Located{unLocated = Command "item"} - : Located{unLocated = BeginEnv "math"} - : commandToken@Located{unLocated = Command _} - : Located{unLocated = EndEnv "math"} - : rest -> - commandToken : structOperationTokens rest - _ : rest -> - structOperationTokens rest - [] -> - [] - -nounRE :: RE Token LexicalPhrase -nounRE = toLexicalPhrase <$> (math var *> is *> an *> patRE <* iff) - -adjRE :: RE Token LexicalPhrase -adjRE = toLexicalPhrase <$> (math var *> is *> patRE <* iff) - -verbRE :: RE Token LexicalPhrase -verbRE = toLexicalPhrase <$> (math var *> patRE <* iff) - -funRE :: RE Token LexicalPhrase -funRE = toLexicalPhrase <$> (the *> patRE <* (is <|> comma)) - -relationSymbolRE :: RE Token (Token, ParameterArity) -relationSymbolRE = do - beginMath - var - rel <- symbol - k <- params - var - endMath - iff - pure (rel, k) - where - params :: RE Token ParameterArity - params = do - vars <- many (RE.sym InvisibleBraceL *> var <* RE.sym InvisibleBraceR) - pure (parameterArityOf vars) - -functionSymbolRE - :: Location - -> RE Token (Either LexicalScanError Pattern) -functionSymbolRE location = do - RE.sym (BeginEnv "math") - toks <- RE.few nonDefinitionKeyword - RE.sym (Symbol "=") - pure (makeFunctionSymbol location toks) - -makeFunctionSymbol - :: Location - -> [Token] - -> Either LexicalScanError Pattern -makeFunctionSymbol location = \case - [] -> - Left (InvalidFunctionPattern location FunctionPatternEmpty) - [Variable _] -> - Left (InvalidFunctionPattern location FunctionPatternBareVariable) - [Variable _, ParenL, Variable _, ParenR] -> - Left - (InvalidFunctionPattern - location - FunctionPatternReservedApplication) - toks -> - Right (patternFromHoley (fromToken <$> toks)) - where - fromToken = \case - Variable _ -> Nothing -- Variables become slots. - tok -> Just tok -- Everything else is part of the pattern. - -functionPatternErrorMessage :: FunctionPatternError -> String -functionPatternErrorMessage = \case - FunctionPatternEmpty -> - "malformed function pattern: no pattern" - FunctionPatternBareVariable -> - "malformed function pattern: a bare variable would cause infinite left recursion" - FunctionPatternReservedApplication -> - "malformed function pattern: _(_) is reserved for set-theoretic function application" - -functionSymbolInductive - :: Location - -> RE Token (Either LexicalScanError Pattern) -functionSymbolInductive location = do - RE.sym (BeginEnv "math") - toks <- RE.few nonDefinitionKeyword - RE.sym (Command "subseteq") - pure (makeFunctionSymbol location toks) - -prefixPredicate :: RE Token PrefixPredicate -prefixPredicate = math prfx <* iff - where - prfx = do - r <- command - args <- many (RE.sym InvisibleBraceL *> var <* RE.sym InvisibleBraceR) - pure (PrefixPredicate r (length args)) - - -command :: RE Token Text -command = RE.msym \case - Command cmd -> Just cmd - _ -> Nothing - -var :: RE Token Token -var = RE.psym isVar - - -nonDefinitionKeyword :: RE Token Token -nonDefinitionKeyword = RE.psym (`notElem` keywords) - where - keywords = - [ Word "if" - , Word "iff" - , Symbol "=" - , Command "iff" - , BeginEnv "math" - , EndEnv "math" - ] - - -patRE :: RE Token [Token] -patRE = many (RE.psym isLexicalPhraseToken <|> math var) - -structPat :: RE Token [Token] -structPat = many (RE.psym isLexicalPhraseToken) - -beginMath, endMath :: RE Token () -beginMath = void (RE.sym (BeginEnv "math")) -endMath = void (RE.sym (EndEnv "math")) - -math :: RE Token a -> RE Token a -math re = beginMath *> re <* endMath - --- | We allow /conditional perfection/: the first /@if@/ in a definition is interpreted as /@iff@/. -iff :: RE Token () -iff = void (RE.sym (Word "if")) -- Using @void@ is faster (only requires recognition). - <|> void (RE.sym (Word "iff")) - <|> void (RE.string [Word "if", Word "and", Word "only", Word "if"]) - <|> void (RE.sym (Word "denote")) - <|> void (RE.sym (Word "stand") *> RE.sym (Word "for")) -{-# INLINE iff #-} - -an :: RE Token () -an = void (RE.sym (Word "a")) - <|> void (RE.sym (Word "an")) -{-# INLINE an #-} - -is :: RE Token () -is = void (RE.sym (Word "is") <|> RE.sym (Word "denotes")) -{-# INLINE is #-} - -the :: RE Token () -the = void (RE.sym (Word "the")) -{-# INLINE the #-} - -comma :: RE Token () -comma = void (RE.sym (Symbol ",")) -{-# INLINE comma #-} - - -isVar :: Token -> Bool -isVar = \case - Variable _ -> True - _token -> False - -isLexicalPhraseToken :: Token -> Bool -isLexicalPhraseToken = \case - Word w -> w `Set.notMember` keywords - -- - -- Simple commands (outside of math-mode) are allowed. This is useful - -- for defining lexical phrases containing symbolic expressions such as - -- `X is \Ttwo{}`, where `\Ttwo` is a macro that expands to `T_2`. - -- We also allow these macros to take arguments, hence the need to - -- allow grouping delimiters. They can also be used to escape the end - -- of the command for correct spacing, as in the above example. - -- - Command _cmd -> True - InvisibleBraceL -> True - InvisibleBraceR -> True - -- - -- No other tokens may occur in lexical phrases. In particular, no `_dot` - -- token may occur, limiting the lexical phrase to a single sentence. - -- Commas occurring in variable lists should be placed - -- within the math environment. Thus `$a,b$ are coprime iff`, - -- not `$a$,`$b$` are coprime iff`. - -- - _token -> False - where - keywords = Set.fromList ["a", "an", "is", "are", "if", "iff", "denote", "stand", "let"] - - -toLexicalPhrase :: [Token] -> LexicalPhrase -toLexicalPhrase toks = component <$> toks - where - component = \case - Variable _ -> Nothing - tok -> Just tok - - -symbol :: RE Token Token -symbol = RE.msym $ \tok -> case tok of - Command _ -> Just tok - Symbol _ -> Just tok - _tok -> Nothing - - --- | Basic paradigms for pluralizations of nominals. -guessNounPlural :: LexicalPhrase -> SgPl LexicalPhrase -guessNounPlural item = SgPl item (pluralize item) - where - pluralize :: LexicalPhrase -> LexicalPhrase - pluralize = \case - Just (Word w) : pat'@(Just w' : _) | isPreposition w' -> Just (Word (Text.snoc w 's')) : pat' - tok : Just (Word w) : pat'@(Just w' : _) | isPreposition w' -> tok : Just (Word (Text.snoc w 's')) : pat' - tok1 : tok2 : Just (Word w) : pat'@(Just w' : _) | isPreposition w' -> tok1 : tok2 : Just (Word (Text.snoc w 's')) : pat' - [Just (Word w)] -> [Just (Word (Text.snoc w 's'))] - [tok, Just (Word w)] -> [tok, Just (Word (Text.snoc w 's'))] - [tok, tok', Just (Word w)] -> [tok, tok', Just (Word (Text.snoc w 's'))] - pat' -> pat' - -guessVerbPlural :: LexicalPhrase -> SgPl LexicalPhrase -guessVerbPlural item = SgPl item itemPl - where - itemPl = case item of - Just (Word v) : rest -> case Text.unsnoc v of - Just (v', 's') -> Just (Word v') : rest - _ -> item - _ -> item - -isAdjR :: LexicalPhrase -> Bool -isAdjR item = containsPreposition item || containsSlot item - where - containsPreposition, containsSlot :: LexicalPhrase -> Bool - containsPreposition = any isPreposition . catMaybes - containsSlot = (Nothing `elem`) - -isPreposition :: Token -> Bool -isPreposition w = Set.member w (Set.map Word prepositions) diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs deleted file mode 100644 index 62d1f92..0000000 --- a/source/Syntax/Concrete.hs +++ /dev/null @@ -1,1032 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE RecursiveDo #-} - --- | Concrete syntax of the surface language. -module Syntax.Concrete where - -import Base -import Syntax.Abstract -import Syntax.Concrete.Keywords -import Syntax.Lexicon - ( Lexicon(..) - , SignatureHeadForm(..) - , concreteSignatureHeadForms - , lexiconAdjs - , splitOnVariableSlot - ) -import Syntax.Token -import Report.Location - -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Text.Earley (Grammar, Prod, (<?>), rule, satisfy, terminal) -import Syntax.Mixfix - - -grammar :: Lexicon -> Grammar r (Prod r Text (Located Token) Block) -grammar lexicon@Lexicon{..} = mdo - let patternToProd :: Pattern -> Holey (Prod r Text (Located Token) (Located Token)) - patternToProd pat = map (fmap tokenLocated) (patternToHoley pat) - makeMixfixOp item = (patternToProd (mixfixPattern item), mixfixAssoc item, \parts args -> ExprOp (mixfixLoc parts args) item args) - mixfixItems = toList (Map.elems <$> lexiconMixfixTable) - mixfixOps = map (map makeMixfixOp) mixfixItems - makeConn (pat, assoc) = (map (fmap tokenLocated) pat, assoc) - conns = map (map makeConn) lexiconConnectives - - integerWithLoc <- rule (terminal maybeIntTokenWithLoc <?> "integer") - relatorWithLoc <- rule $ asum - [ (,) <$> tokenPos (relationSymbolToken item) <*> pure item - | item <- lexiconRelationSymbols - ] <?> "relator" - relator <- rule (snd <$> relatorWithLoc) - varSymbol <- rule (terminal maybeVarToken <?> "variable") - varSymbols <- rule (commaList varSymbol) - cmd <- rule (terminal maybeCmdToken <?> "TEX command") --- --- Formulas have three levels: --- --- + Expressions: atoms or operators applied to atoms. --- + Chains: comma-lists of expressions, separated by relators. --- + Formulas: chains or connectives applied to chains. --- --- For example, the formula @x, y < z \implies x, y < z + 1@ consist of the --- connective @\implies@ applied to two chains @x, y < z@ and @x, y < z + 1@. --- In turn, the chain @x, y < z + 1@ consist of three expressions, --- @x@, @y@, and @z + 1@. Finally, @z + 1@ consist the operator @+@ --- applied to two atoms, the variable @z@ and the number literal @1@. --- --- This split is due to the different behaviour of relators compared to --- operators and connectives. Relators can chain (@x < y < z@) and allow --- lists as arguments, as in the above example. Operators and connectives --- instead have precedence and fixity. The only syntactic difference between --- an operator and a connective is the relative precedence compared to relators. --- - replaceBound <- rule $ (,) <$> varSymbol <* _in <*> expr - replaceBounds <- rule $ commaList replaceBound - comprStmt <- rule $ (StmtFormula <$> formula) <|> text stmt - - let replaceFun = (\e bounds mstmt loc -> ExprReplace loc e bounds mstmt) <$> expr <* _pipe <*> replaceBounds <*> optional (_pipe *> comprStmt) - replacePredSymbolic = (\y x xBound st loc -> ExprReplacePred loc y x xBound st) <$> varSymbol <* _pipe <*> (command "exists" *> varSymbol) <* _in <*> expr <* _dot <*> (StmtFormula <$> formula) - replacePredText = (\y x xBound st loc -> ExprReplacePred loc y x xBound st) <$> varSymbol <* _pipe <*> (begin "text" *> _exists *> beginMath *> varSymbol <* _in) <*> expr <* endMath <* _suchThat <*> stmt <* end "text" - replacePred = replacePredSymbolic <|> replacePredText - - let exprStructOpOf ann = foldr alg empty lexiconStructFun - where - alg s prod = prod <|> (uncurry ExprStructOp <$> structSymbolPos s <*> ann) - - exprStructOp <- rule (exprStructOpOf (optional (bracket expr))) - - let bracedArgs1 ar arg = count1 ar $ group arg - let prefixPredicateOf f arg symb@(PrefixPredicate c ar) = f <$> pure symb <* command c <*> bracedArgs1 ar arg - - - exprParen <- rule $ paren expr - exprInteger <- rule $ uncurry ExprInteger <$> integerWithLoc - exprVar <- rule $ ExprVar <$> varSymbol - exprTuple <- rule do - loc <- tokenPos ParenL - es <- commaList2 expr <* token ParenR - pure (makeTuple loc es) - exprSep <- rule do - loc <- tokenPos VisibleBraceL - x <- varSymbol <* _in - bound <- expr <* _pipe - phi <- comprStmt <* token VisibleBraceR - pure (ExprSep loc x bound phi) - exprReplace <- rule do - (\loc mk -> mk loc) <$> tokenPos VisibleBraceL <*> (replaceFun <|> replacePred) <* token VisibleBraceR - exprFinSet <- rule do - loc <- tokenPos VisibleBraceL - es <- exprs <* token VisibleBraceR - pure (ExprFiniteSet loc es) - exprBase <- rule $ asum [exprVar, exprInteger, exprStructOp, exprParen, exprTuple, exprSep, exprReplace, exprFinSet] - exprApp <- rule $ (\e1 e2 -> ExprApp (locate e1) e1 e2) <$> exprBase <*> (paren expr <|> exprTuple) - expr <- mixfixExpressionSeparate mixfixOps (exprBase <|> exprApp) - exprs <- rule $ commaList expr - - relationSign <- rule $ pure Positive <|> (Negative <$ command "not") - relationExpr <- rule $ RelationExpr <$> command "mathrel" <*> group expr - relation <- rule $ (uncurry Relation <$> relatorWithLoc <*> many (group expr)) <|> relationExpr - chainBase <- rule $ (\es sign rel es' -> ChainBase es sign rel es') <$> exprs <*> relationSign <*> relation <*> exprs - chainCons <- rule $ (\es sign rel ch -> ChainCons es sign rel ch) <$> exprs <*> relationSign <*> relation <*> chain - chain <- rule $ chainCons <|> chainBase - - formulaPredicate <- rule $ asum - [ (\loc es -> FormulaPredicate loc symb marker es) <$> command c <*> bracedArgs1 ar expr - | (symb@(PrefixPredicate c ar), marker) <- lexiconPrefixPredicates - ] - formulaChain <- rule $ FormulaChain <$> chain - formulaBottom <- rule $ PropositionalConstant <$> command "bot" <*> pure IsBottom <?> "\"\\bot\"" - formulaTop <- rule $ PropositionalConstant <$> command "top" <*> pure IsTop <?> "\"\\top\"" - formulaExists <- rule $ FormulaQuantified <$> command "exists" <*> pure Existentially <*> varSymbols <*> maybeBounded <* _dot <*> formula - formulaAll <- rule $ FormulaQuantified <$> command "forall" <*> pure Universally <*> varSymbols <*> maybeBounded <* _dot <*> formula - formulaQuantified <- rule $ formulaExists <|> formulaAll - formulaBase <- rule $ asum [formulaChain, formulaPredicate, formulaBottom, formulaTop, paren formula] - formulaConn <- mixfixExpression conns formulaBase makeConnective - formula <- rule $ formulaQuantified <|> formulaConn - --- These are asymmetric formulas (only variables are allowed on one side). --- They express judgements. --- - assignment <- rule $ (,) <$> varSymbol <* (_eq <|> _defeq) <*> expr - typing <- rule $ (,) <$> varSymbols <* (_in <|> _colon) <*> expr - - adjL <- rule $ adjLOf lexicon term - adjR <- rule $ adjROf lexicon term - adj <- rule $ adjOf lexicon term - adjVar <- rule $ adjOf lexicon var - - var <- rule $ math varSymbol - vars <- rule $ math varSymbols - - verb <- rule $ verbOf lexicon sg term - verbPl <- rule $ verbOf lexicon pl term - verbVar <- rule $ verbOf lexicon sg var - - let nounTrieSg = nounTrieOf sg lexiconNouns - nounTriePl = nounTrieOf pl lexiconNouns - structNounTrieSg = nounTrieOf sg lexiconStructNouns - - noun <- rule $ nounOfTrie nounTrieSg term nounName -- Noun with optional variable name. - nounList <- rule $ nounOfTrie nounTrieSg term nounNames -- Noun with a list of names. - nounVar <- rule $ fst <$> nounOfTrie nounTrieSg var (pure Nameless) -- No names in defined nouns. - nounPl <- rule $ nounOfTrie nounTriePl term nounNames - nounPlMay <- rule $ nounOfTrie nounTriePl term nounName - - - structNoun <- rule $ structNounOfTrie structNounTrieSg var var - structNounNameless <- rule $ fst <$> structNounOfTrie structNounTrieSg var (pure Nameless) - - - fun <- rule $ funOf lexicon sg term - funVar <- rule $ funOf lexicon sg var - - attrRThat <- rule $ AttrRThat <$> thatVerbPhrase - attrRThats <- rule $ ((:[]) <$> attrRThat) <|> ((\a a' -> [a,a']) <$> attrRThat <* _and <*> attrRThat) <|> pure [] - attrRs <- rule $ ((:[]) <$> adjR) <|> ((\a a' -> [a,a']) <$> adjR <* _and <*> adjR) <|> pure [] - attrRight <- rule $ (<>) <$> attrRs <*> attrRThats - - verbPhraseVerbSg <- rule $ VPVerb <$> verb - verbPhraseVerbNotSg <- rule $ VPVerbNot <$> (_does *> _not *> verbPl) - verbPhraseAdjSg <- rule $ VPAdj . (:|[]) <$> (_is *> adj) - verbPhraseAdjAnd <- rule do {_is; a1 <- adj; _and; a2 <- adj; pure (VPAdj (a1 :| [a2]))} - verbPhraseAdjNotSg <- rule $ VPAdjNot . (:|[]) <$> (_is *> _not *> adj) - verbPhraseNotSg <- rule $ verbPhraseVerbNotSg <|> verbPhraseAdjNotSg - verbPhraseSg <- rule $ verbPhraseVerbSg <|> verbPhraseAdjSg <|> verbPhraseAdjAnd <|> verbPhraseNotSg - - -- LATER can cause technical ambiguities? verbPhraseVerbPl <- rule $ VPVerb <$> verbPl - verbPhraseVerbNotPl <- rule $ VPVerbNot <$> (_do *> _not *> verbPl) - verbPhraseAdjPl <- rule $ VPAdj . (:|[]) <$> (_are *> adj) - verbPhraseAdjNotPl <- rule $ VPAdjNot . (:|[]) <$> (_are *> _not *> adj) - verbPhraseNotPl <- rule $ verbPhraseVerbNotPl <|> verbPhraseAdjNotPl - verbPhrasePl <- rule $ verbPhraseAdjPl <|> verbPhraseNotPl -- LATER <|> verbPhraseVerbPl - - - - thatVerbPhrase <- rule $ _that *> verbPhraseSg - - nounName <- rule $ optional (math varSymbol) - nounNames <- rule $ math (commaList_ varSymbol) <|> pure [] - nounPhrase <- rule $ makeNounPhrase <$> many adjL <*> noun <*> attrRight <*> optional suchStmt - nounPhrase' <- rule $ makeNounPhrase <$> many adjL <*> nounList <*> attrRight <*> optional suchStmt - nounPhrasePl <- rule $ makeNounPhrase <$> many adjL <*> nounPl <*> attrRight <*> optional suchStmt - nounPhrasePlMay <- rule $ makeNounPhrase <$> many adjL <*> nounPlMay <*> attrRight <*> optional suchStmt - nounPhraseMay <- rule $ makeNounPhrase <$> many adjL <*> noun <*> attrRight <*> optional suchStmt - - -- Quantification phrases for quantification and indfinite terms. - quantAll <- rule $ QuantPhrase Universally <$> (_forEvery *> nounPhrase' <|> _forAll *> nounPhrasePl) - quantSome <- rule $ QuantPhrase Existentially <$> (_some *> (nounPhrase' <|> nounPhrasePl)) - quantNone <- rule $ QuantPhrase Nonexistentially <$> (_no *> (nounPhrase' <|> nounPhrasePl)) - quant <- rule $ quantAll <|> quantSome <|> quantNone -- <|> quantUniq - - - termExpr <- rule $ math do - e <- expr - pure (TermExpr e) - termFun <- rule $ TermFun <$> (optional _the *> fun) - termIota <- rule $ TermIota <$> _the <*> var <* _suchThat <*> stmt - termAll <- rule $ TermQuantified Universally <$> _every <*> nounPhraseMay - termSome <- rule $ TermQuantified Existentially <$> _some <*> nounPhraseMay - termNo <- rule $ TermQuantified Nonexistentially <$> _no <*> nounPhraseMay - termQuantified <- rule $ termAll <|> termSome <|> termNo - term <- rule $ termExpr <|> termFun <|> termQuantified <|> termIota - --- Basic statements @stmt'@ are statements without any conjunctions or quantifiers. --- - let singletonTerm = (:| []) <$> term - nonemptyTerms = andList1 term - stmtVerbSg <- rule $ StmtVerbPhrase <$> singletonTerm <*> verbPhraseSg - stmtVerbPl <-rule $ StmtVerbPhrase <$> andList1 term <*> verbPhrasePl - stmtVerb <- rule $ stmtVerbSg <|> stmtVerbPl - stmtNounIs <- rule do - ts <- singletonTerm - np <- _is *> _an *> nounPhrase - pure (StmtNoun ts np) - stmtNounAre <- rule do - ts <- nonemptyTerms <* _are - np <- nounPhrasePlMay - pure (StmtNoun ts np) - stmtNounIsNot <- rule do - ts <- singletonTerm - np <- _is *> _not *> _an *> nounPhrase - pure let t :| _ = ts in (StmtNeg (locate t) (StmtNoun ts np)) - stmtNounAreNot <- rule do - ts <- nonemptyTerms - np <- _are *> _not *> nounPhrasePlMay - pure let t :| _ = ts in (StmtNeg (locate t) (StmtNoun ts np)) - stmtNoun <- rule $ stmtNounIs <|> stmtNounIsNot <|> stmtNounAre <|> stmtNounAreNot - stmtStruct <- rule do - t <- term - s <- _is *> _an *> structNounNameless - pure (StmtStruct t s) - stmtExists <- rule $ StmtExists <$> _exists <*> (_an *> nounPhrase') - stmtExist <- rule $ StmtExists <$> _exist <*> nounPhrasePl - stmtExistsNot <- rule do - p <- _exists *> _no - np <- nounPhrase' - pure (StmtNeg p (StmtExists p np)) - stmtFormula <- rule $ math do - phi <- formula - pure (StmtFormula phi) - stmtFormualNeg <- rule do - loc <- _not - phi <- math formula - pure (StmtNeg loc (StmtFormula phi)) - stmtAtom <- rule $ - stmtVerb - <|> stmtNoun - <|> stmtStruct - <|> stmtFormula - <|> stmtFormualNeg - <|> paren stmt - - -- Textual connectives use the same precedence and associativity as - -- symbolic connectives. Prefix negation and quantifiers scope over the - -- complete statement that follows them. - let connect conn lhs rhs = - StmtConnected conn Nothing lhs rhs - appendScoped conn lhs rhs scoped = - let connected = foldl' (connect conn) lhs rhs - in maybe connected (connect conn connected) scoped - stmtAnd <- rule do - lhs <- stmtAtom - rhs <- many (_and *> stmtAtom) - scoped <- optional (_and *> stmtScoped) - pure (appendScoped Conjunction lhs rhs scoped) - stmtXor <- rule $ - StmtConnected ExclusiveOr - <$> (Just <$> _either) - <*> stmtAnd - <* _or - <*> stmtAnd - stmtNor <- rule $ - StmtConnected NegatedDisjunction - <$> (Just <$> _neither) - <*> stmtAnd - <* _nor - <*> stmtAnd - stmtOrBase <- rule $ stmtXor <|> stmtNor <|> stmtAnd - stmtOr <- rule do - lhs <- stmtOrBase - rhs <- many (_or *> stmtOrBase) - scoped <- optional (_or *> stmtScoped) - pure (appendScoped Disjunction lhs rhs scoped) - stmtIf <- rule $ - StmtConnected Implication - <$> (Just <$> _if) - <*> stmtIfAntecedent - <* optional _comma - <* _then - <*> stmtImpRhs - stmtImp <- rule $ stmtIf <|> stmtOr - stmtIff <- rule do - lhs <- stmtImp - rhs <- optional (_iff *> stmtImpRhs) - pure case rhs of - Nothing -> lhs - Just rhs' -> connect Equivalence lhs rhs' - stmtNeg <- rule $ StmtNeg <$> _itIsWrong <*> stmt - - stmtQuantPhrase <- rule $ StmtQuantPhrase <$> _for <*> quant <* optional _comma <* optional _have <*> stmt - - suchStmt <- rule $ _suchThat *> stmt <* optional _comma - - -- Symbolic quantifications with or without generalized bounds. - symbolicForall <- rule do - p <- _forAll <|> _forEvery - xs <- beginMath *> varSymbols - b <- maybeBounded <* endMath - ms <- optional suchStmt - s <- optional _have *> stmt - pure (SymbolicForall p xs b ms s) - symbolicExists <- rule do - loc1 <- _exists <|> _exist - xs <- beginMath *> varSymbols - b <- maybeBounded - loc2 <- endMath - ms <- optional (_suchThat *> stmt) - pure (SymbolicExists loc1 xs b (ms ?? StmtFormula (PropositionalConstant loc2 IsTop))) - symbolicNotExists <- rule do - p <- _exists *> _no - xs <- beginMath *> varSymbols - b <- maybeBounded <* endMath - s <- _suchThat *> stmt - pure (makeSymbolicNotExists p xs b s) - symbolicBound <- rule $ (\sign rel e -> Bounded (locate rel) sign rel e) <$> relationSign <*> relation <*> expr - maybeBounded <- rule (pure Unbounded <|> symbolicBound) - - symbolicQuantified <- rule $ symbolicForall <|> symbolicExists <|> symbolicNotExists - - stmtScoped <- rule $ - asum - [ stmtNeg - , stmtExists - , stmtExist - , stmtExistsNot - , stmtQuantPhrase - , symbolicQuantified - ] - stmtIfAntecedent <- rule $ stmtScoped <|> stmtOr - stmtImpRhs <- rule $ stmtScoped <|> stmtImp - stmt :: Prod r Text (Located Token) Stmt <- rule $ - (stmtScoped <|> stmtIff) <?> "a statement" - - - asmLetIn <- rule $ uncurry AsmLetIn <$> (_let *> math typing) - asmLetNoun <- rule $ AsmLetNoun <$> (_let *> fmap pure var <* (_be <|> _denote) <* _an) <*> nounPhrase - asmLetNouns <- rule $ AsmLetNoun <$> (_let *> vars <* (_be <|> _denote)) <*> nounPhrasePlMay - asmLetEq <- rule $ uncurry AsmLetEq <$> (_let *> math assignment) - asmLetThe <- rule $ AsmLetThe <$> (_let *> var <* _be <* _the) <*> fun - asmLetStruct <- rule $ AsmLetStruct <$> (_let *> var <* _be <* _an) <*> structNounNameless - asmLet <- rule $ asmLetNoun <|> asmLetNouns <|> asmLetIn <|> asmLetEq <|> asmLetThe <|> asmLetStruct - asmSuppose <- rule $ AsmSuppose <$> (_suppose *> stmt) - asm <- rule $ andList1_ (asmLet <|> asmSuppose) <* _dot - asms <- rule $ concat <$> many asm - - axiom <- rule $ Axiom <$> asms <* optional _then <*> stmt <* _dot - - claim <- rule $ (,) <$> asms <* optional _then <*> stmt <* _dot - - defnAdj <- rule $ DefnAdj <$> optional (_an *> nounPhrase) <*> var <* _is <*> adjVar - defnVerb <- rule $ DefnVerb <$> optional (_an *> nounPhrase) <*> var <*> verbVar - defnNoun <- rule $ DefnNoun <$> var <* _is <* _an <*> nounVar - defnRel <- rule $ DefnRel <$> (beginMath *> varSymbol) <*> relator <*> many (group varSymbol) <*> varSymbol <* endMath - defnSymbolicPredicate <- rule $ math $ asum $ do - (predi, marker) <- lexiconPrefixPredicates - pure (prefixPredicateOf (\predi' args -> DefnSymbolicPredicate predi' marker args) varSymbol predi) - defnHead <- rule $ optional _write *> asum [defnAdj, defnVerb, defnNoun, defnRel, defnSymbolicPredicate] - - defnIf <- rule $ Defn <$> asms <*> defnHead <* (_iff <|> _if) <*> stmt <* _dot - defnFunSymb <- rule $ _comma *> termExpr <* _comma -- Optional symbolic equivalent. - defnFun <- rule $ DefnFun <$> asms <*> (optional _the *> funVar) <*> optional defnFunSymb <* _is <*> term <* _dot - - symbolicPatternEqTerm <- rule do - pat <- beginMath *> symbolicPattern <* _eq - e <- expr <* endMath <* _dot - pure (pat, e) - defnOp <- rule $ uncurry DefnOp <$> symbolicPatternEqTerm - - defn <- rule $ defnIf <|> defnFun <|> defnOp - - abbreviationVerb <- rule $ AbbreviationVerb <$> var <*> verbVar <* (_iff <|> _if) <*> stmt <* _dot - abbreviationAdj <- rule $ AbbreviationAdj <$> var <* _is <*> adjVar <* (_iff <|> _if) <*> stmt <* _dot - abbreviationNoun <- rule $ AbbreviationNoun <$> var <* _is <* _an <*> nounVar <* (_iff <|> _if) <*> stmt <* _dot - abbreviationRel <- rule $ AbbreviationRel <$> (beginMath *> varSymbol) <*> relator <*> many (group varSymbol) <*> varSymbol <* endMath <* (_iff <|> _if) <*> stmt <* _dot - abbreviationFun <- rule $ AbbreviationFun <$> (_the *> funVar) <* (_is <|> _denotes) <*> term <* _dot - abbreviationEq <- rule $ uncurry AbbreviationEq <$> symbolicPatternEqTerm - abbreviation <- rule $ (abbreviationVerb <|> abbreviationAdj <|> abbreviationNoun <|> abbreviationRel <|> abbreviationFun <|> abbreviationEq) - - datatypePremise <- rule $ math $ (,) <$> varSymbol <* _in <*> expr - datatypeClause <- rule $ - (\(constructorExpr, targetExpr) premises -> DatatypeClause - { datatypeClauseConstructorExpr = constructorExpr - , datatypeClauseTargetExpr = targetExpr - , datatypeClausePremises = premises ?? [] - }) <$> math ((,) <$> expr <* _in <*> expr) - <*> optional (_for *> andList1_ datatypePremise) - <* _dot - datatypeHead <- rule $ _define *> math expr <* optional _inductively <* optional _asFollows <* _dot - datatype <- rule $ Datatype <$> datatypeHead <*> enumerated1 datatypeClause - - unconditionalIntro <- rule $ IntroRule [] <$> math formula - conditionalIntro <- rule $ IntroRule <$> (_if *> andList1_ (math formula)) <* _comma <* _then <*> math formula - inductiveIntro <- rule $ (unconditionalIntro <|> conditionalIntro) <* _dot - inductiveDomain <- rule $ math $ (,) <$> symbolicPattern <* _subseteq <*> expr - inductiveHead <- rule $ _define *> inductiveDomain <* optional _inductively <* optional _asFollows <* _dot - inductive <- rule $ uncurry Inductive <$> inductiveHead <*> enumerated1 inductiveIntro - - signatureAdj <- rule $ SignatureAdj <$> var <* _can <* _be <*> adjOf lexicon var - symbolicPattern <- symbolicPatternOf mixfixItems varSymbol - signatureSymbolic <- rule $ SignatureSymbolic <$> math symbolicPattern <* _is <* _an <*> nounPhrase - signatureHead <- rule $ asum - [ case form of - AdjectiveSignatureHead -> signatureAdj - SymbolicSignatureHead -> signatureSymbolic - | form <- concreteSignatureHeadForms - ] - signature <- rule $ - (,) <$> asms <* optional _then <*> signatureHead <* _dot - - structFix <- rule do - beginMath - rawCmd <- cmd - endMath - pure (StructSymbol rawCmd) - structDefn <- rule $ do - _an - ~(structPhrase, structLabel) <- structNoun - _extends - structParents <- andList1_ (_an *> structNounNameless) - maybeFixes <- optional (_equipped *> enumerated structFix) - structAssumes <- (_suchThat *> enumeratedMarked (stmt <* _dot)) <|> ([] <$ _dot) - pure StructDefn - { structPhrase = structPhrase - , structLabel = structLabel - , structParents = structParents - , structFixes = maybeFixes ?? [] - , structAssumes = structAssumes - } - - justificationSet <- rule $ JustificationSetExt <$ _bySetExt - justificationRef <- rule $ JustificationRef <$> (_by *> ref) - justificationLocal <- rule $ JustificationLocal <$ (_by *> (_assumption <|> _definition)) - justification <- rule (justificationSet <|> justificationRef <|> justificationLocal <|> pure JustificationEmpty) - - trivial <- rule $ Qed . Just <$> _trivial <* _dot <*> pure JustificationEmpty - omitted <- rule $ Omitted <$> _omitted <* _dot - qedJustified <- rule $ Qed . Just <$> _follows <*> (justification <* _dot) - qed <- rule $ qedJustified <|> trivial <|> omitted <|> pure (Qed Nothing JustificationEmpty) - contradiction <- rule $ Contradiction <$> _contradiction <*> justification <* _dot - - let alignedEq = symbol "&=" <?> "\"&=\"" - explanation <- rule $ (text justification) <|> pure JustificationEmpty - equationItem <- rule $ (,) <$> (alignedEq *> expr) <*> explanation - equations <- rule $ Equation <$> expr <*> (many1 equationItem) - - let alignedIff = symbol "&" *> command "iff" <?> "\"&\\iff\"" - biconditionalItem <- rule $ (,) <$> (alignedIff *> formula) <*> explanation - biconditionals <- rule $ Biconditionals <$> formula <*> (many1 biconditionalItem) <* optional _dot - - - calcQuantifier <- rule do - loc <- _forAll <|> _forEvery - xs <- beginMath *> varSymbols - mb <- maybeBounded <* endMath - st <- optional suchStmt - optional _have - pure (loc, CalcQuantifier xs mb st) - - calc <- rule do - mquant <- optional calcQuantifier - psteps <- align (equations <|> biconditionals) - pf <- proof - pure let (loc2, steps) = psteps in case mquant of - Nothing -> Calc loc2 Nothing steps pf - Just (loc, q) -> Calc loc (Just q) steps pf - - caseOf <- rule $ command "caseOf" *> token InvisibleBraceL *> stmt <* _dot <* token InvisibleBraceR - byCases <- rule $ uncurry ByCase <$> envPos_ "byCase" (many1_ (Case <$> caseOf <*> proof)) - byContradiction <- rule $ ByContradiction <$> _suppose <* _not <* _dot <*> proof - bySetInduction <- rule $ uncurry BySetInduction <$> proofBy (_in *> word "-induction" *> optional (word "on" *> term)) <*> proof - byOrdInduction <- rule $ ByOrdInduction . fst <$> proofBy (word "transfinite" *> word "induction") <*> proof - assume <- rule $ Assume <$> _suppose <*> (stmt <* _dot) <*> proof - - fixSymbolic <- rule $ FixSymbolic <$> _fix <*> (beginMath *> varSymbols) <*> maybeBounded <* endMath <* _dot <*> proof - fixSuchThat <- rule $ FixSuchThat <$> _fix <*> math varSymbols <* _suchThat <*> stmt <* _dot <*> proof - fix <- rule $ fixSymbolic <|> fixSuchThat - - takeVar <- rule $ TakeVar <$> _take <*> (beginMath *> varSymbols) <*> maybeBounded <* endMath <* _suchThat <*> stmt <*> justification <* _dot <*> proof - takeNoun <- rule $ TakeNoun <$> _take <*> (_an *> (nounPhrase' <|> nounPhrasePl)) <*> justification <* _dot <*> proof - take <- rule $ takeVar <|> takeNoun - suffices <- rule $ Suffices <$> _sufficesThat <*> stmt <*> (justification <* _dot) <*> proof - subclaim <- rule $ Subclaim <$> _show <*> (stmt <* _dot) <*> env_ "subproof" proof <*> proof - have <- rule do - msince <- optional ((,) <$> _since <*> stmt <* _comma <* _have) - mpos <- optional _haveIntro - s <- stmt - j <- justification <* _dot - pf <- proof - pure - let pos = case (msince, mpos) of - (Just (p, _), _) -> p - (_, Just p) -> p - _ -> locate s - in (Have pos (snd <$> msince) s j pf) - - - define <- rule $ Define <$> _let <*> (beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof - defineFunction <- rule $ DefineFunction <$> _let <*> (beginMath *> varSymbol) <*> paren varSymbol <* _eq <*> expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof - - proof <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, contradiction, qed] - - - blockAxiom <- rule $ (\(p, title, m, a) -> BlockAxiom p title m a) <$> envPos "axiom" axiom - blockClaim <- rule $ claimEnv claim - blockProof <- rule $ uncurry3 BlockProof <$> envStartEndLocation "proof" proof - blockDefn <- rule $ (\(p, title, m, d) -> BlockDefn p title m d) <$> envPos "definition" defn - blockAbbr <- rule $ (\(p, title, m, a) -> BlockAbbr p title m a) <$> envPos "abbreviation" abbreviation - blockData <- rule $ (\(p, title, m, d) -> BlockData p title m d) <$> envPos "datatype" datatype - blockInd <- rule $ (\(p, title, m, i) -> BlockInductive p title m i) <$> envPos "inductive" inductive - blockSig <- rule $ (\(p, title, m, (a, s)) -> BlockSig p title m a s) <$> envPos "signature" signature - blockStruct <- rule $ (\(p, title, m, s) -> BlockStruct p title m s) <$> envPos "struct" structDefn - block <- rule $ asum [blockAxiom, blockClaim, blockDefn, blockAbbr, blockData, blockInd, blockSig, blockStruct, blockProof] - - -- Starting category. - pure block - - -proofBy :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a) -proofBy method = bracket do - pos <- word "proof" *> word "by" - a <- method - pure (pos, a) - -claimEnv :: Prod r Text (Located Token) (([Asm], Stmt)) -> Prod r Text (Located Token) Block -claimEnv content = asum - [ make Theorem <$> envPos "theorem" content - , make Lemma <$> envPos "lemma" content - , make Corollary <$> envPos "corollary" content - , make PlainClaim <$> envPos "claim" content - , make Proposition <$> envPos "proposition" content - ] - where - make kind = (\ (loc, title, m, (asms, stmt)) -> BlockClaim kind loc title m (Claim asms stmt)) - --- | A disjunctive list with at least two items: --- * 'a or b' --- * 'a, b, or c' --- * 'a, b, c, or d' --- -orList2 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a) -orList2 item = ((:|) <$> item <*> many (_commaOr *> item)) - <|> ((\i j -> i:|[j]) <$> item <* _or <*> item) - - --- | Nonempty textual lists of the form "a, b, c, and d". --- The final comma is mandatory, 'and' is not. --- Also allows "a and b". Should therefore be avoided in contexts where --- a logical conjunction would also be possible. --- Currently also allows additional 'and's after each comma... --- -andList1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a) -andList1 item = ((:|) <$> item <*> many (_commaAnd *> item)) - <|> ((\i j -> i:|[j]) <$> item <* _and <*> item) - --- | Like 'andList1', but drops the information about nonemptiness. -andList1_ :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a] -andList1_ item = NonEmpty.toList <$> andList1 item - - -commaList :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a) -commaList item = (:|) <$> item <*> many (_comma *> item) - --- | Like 'commaList', but drops the information about nonemptiness. -commaList_ :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a] -commaList_ item = NonEmpty.toList <$> commaList item - --- | Like 'commaList', but requires at least two items (and hence at least one comma). -commaList2 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a) -commaList2 item = (:|) <$> item <* _comma <*> commaList_ item - - -enumerated :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [a] -enumerated p = NonEmpty.toList <$> enumerated1 p - -enumerated1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty a) -enumerated1 p = begin "enumerate" *> many1 (command "item" *> p) <* end "enumerate" <?> "\"\\begin{enumerate} ...\"" - - -enumeratedMarked :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)] -enumeratedMarked p = NonEmpty.toList <$> enumeratedMarked1 p - -enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a)) -enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" <?> "\"\\begin{enumerate}\\item\\label{...}...\"" - - - --- This function could be rewritten, so that it can be used directly in the grammar, --- instead of with specialized variants. --- -phraseOf - :: forall pat a b r. Locatable a - => (Location -> pat -> [a] -> b) - -> Lexicon - -> (Lexicon -> [pat]) - -> (pat -> LexicalPhrase) - -> Prod r Text (Located Token) a - -> Prod r Text (Located Token) b -phraseOf constr lexicon selector proj arg = - uncurry3 constr <$> buildPhraseTrie arg trie - where - pats :: [pat] - pats = selector lexicon - - trie :: Trie PhraseStep pat - trie = trieFromList - [ (phraseSteps (proj pat), pat) - | pat <- pats - ] - -adjLOf :: Locatable arg => Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjLOf arg) -adjLOf lexicon arg = phraseOf AdjL lexicon lexiconAdjLs lexicalItemPhrase arg <?> "a left adjective" - -adjROf :: Locatable arg =>Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjROf arg) -adjROf lexicon arg = phraseOf AdjR lexicon lexiconAdjRs lexicalItemPhrase arg <?> "a right adjective" - -adjOf :: Locatable arg =>Lexicon -> Prod r Text (Located Token) arg -> Prod r Text (Located Token) (AdjOf arg) -adjOf lexicon arg = phraseOf Adj lexicon lexiconAdjs lexicalItemPhrase arg <?> "an adjective" - -verbOf - :: Locatable a => Lexicon - -> (SgPl LexicalPhrase -> LexicalPhrase) - -> Prod r Text (Located Token) a - -> Prod r Text (Located Token) (VerbOf a) -verbOf lexicon proj arg = phraseOf Verb lexicon lexiconVerbs (proj . lexicalItemSgPlPhrase) arg - -funOf - :: Locatable a => Lexicon - -> (SgPl LexicalPhrase -> LexicalPhrase) - -> Prod r Text (Located Token) a - -> Prod r Text (Located Token) (FunOf a) -funOf lexicon proj arg = phraseOf Fun lexicon lexiconFuns (proj . lexicalItemSgPlPhrase) arg <?> "functional phrase" - - --- | A noun with a @t VarSymbol@ as name(s). -nounOf - :: Locatable arg => Lexicon - -> (SgPl LexicalPhrase -> LexicalPhrase) - -> Prod r Text (Located Token) arg - -> Prod r Text (Located Token) (t VarSymbol) - -> Prod r Text (Located Token) (NounOf arg, t VarSymbol) -nounOf lexicon proj arg vars = - nounOfTrie (nounTrieOf proj (lexiconNouns lexicon)) arg vars - -nounOfTrie - :: Locatable arg => Trie NounStep LexicalItemSgPl - -> Prod r Text (Located Token) arg - -> Prod r Text (Located Token) (t VarSymbol) - -> Prod r Text (Located Token) (NounOf arg, t VarSymbol) -nounOfTrie trie arg vars = - (\(loc, pat, args, xs) -> (Noun loc pat args, xs)) - <$> buildNounTrie arg vars trie - <?> "a noun" - -nounTrieOf - :: (SgPl LexicalPhrase -> LexicalPhrase) - -> [LexicalItemSgPl] - -> Trie NounStep LexicalItemSgPl -nounTrieOf proj pats = trieFromList - [ (nounStepsWithSlot (proj (lexicalItemSgPlPhrase pat)), pat) - | pat <- pats - ] - -structNounOfTrie - :: Locatable arg => Trie NounStep LexicalItemSgPl - -> Prod r Text (Located Token) arg - -> Prod r Text (Located Token) name - -> Prod r Text (Located Token) (StructPhrase, name) -structNounOfTrie trie arg name = - (\(_loc, pat, _args, xs) -> (pat, xs)) - <$> buildNounTrie arg name trie - <?> "a structure noun" - -structNounOf - :: Locatable arg => Lexicon - -> (SgPl LexicalPhrase -> LexicalPhrase) - -> Prod r Text (Located Token) arg - -> Prod r Text (Located Token) name - -> Prod r Text (Located Token) (StructPhrase, name) -structNounOf lexicon proj arg name = - structNounOfTrie (nounTrieOf proj (lexiconStructNouns lexicon)) arg name - --- Trie helpers for lexically-defined phrases. - -data PhraseStep - = PhraseTok Token - | PhraseHole - deriving (Eq, Ord) - -data NounStep - = NounTok Token - | NounHole - | NounVar - deriving (Eq, Ord) - -data Trie k v = Trie - { trieValues :: [v] - , trieEdges :: [(k, Trie k v)] - } - -emptyTrie :: Trie k v -emptyTrie = Trie [] [] - -insertTrie :: Eq k => [k] -> v -> Trie k v -> Trie k v -insertTrie [] v Trie{trieValues = vs, trieEdges = es} = - Trie (vs <> [v]) es -insertTrie (k:ks) v Trie{trieValues = vs, trieEdges = es} = - Trie vs (go es) - where - go = \case - [] -> [(k, insertTrie ks v emptyTrie)] - (k', child) : rest - | k == k' -> (k', insertTrie ks v child) : rest - | otherwise -> (k', child) : go rest - -trieFromList :: Eq k => [([k], v)] -> Trie k v -trieFromList = foldl' (\tr (k, v) -> insertTrie k v tr) emptyTrie - -phraseSteps :: LexicalPhrase -> [PhraseStep] -phraseSteps = map \case - Just tok -> PhraseTok tok - Nothing -> PhraseHole - -nounSteps :: LexicalPhrase -> [NounStep] -nounSteps = map \case - Just tok -> NounTok tok - Nothing -> NounHole - -nounStepsWithSlot :: LexicalPhrase -> [NounStep] -nounStepsWithSlot pat = - let (pat1, pat2) = splitOnVariableSlot pat - in nounSteps pat1 <> [NounVar] <> nounSteps pat2 - -data PhraseAcc a = PhraseAcc - { phraseLoc :: Maybe Location - , phraseArgs :: [a] -> [a] - } - -emptyPhraseAcc :: PhraseAcc a -emptyPhraseAcc = PhraseAcc Nothing id - -setPhraseLoc :: Location -> PhraseAcc a -> PhraseAcc a -setPhraseLoc Nowhere acc = acc -setPhraseLoc _loc acc@PhraseAcc{phraseLoc = Just _} = acc -setPhraseLoc loc PhraseAcc{phraseLoc = Nothing, phraseArgs = args} = - PhraseAcc (Just loc) args - -addPhraseArg :: Locatable a => a -> PhraseAcc a -> PhraseAcc a -addPhraseArg a acc@PhraseAcc{phraseLoc = loc, phraseArgs = args} - | locate a == Nowhere = acc{phraseArgs = args . (a :)} - | otherwise = PhraseAcc (loc <|> Just (locate a)) (args . (a :)) - -finalizePhraseAcc :: PhraseAcc a -> (Location, [a]) -finalizePhraseAcc PhraseAcc{phraseLoc = Just loc, phraseArgs = args} = - (loc, args []) -finalizePhraseAcc PhraseAcc{phraseLoc = Nothing} = - impossible "phraseOf: empty phrase" - -data NounAcc a name = NounAcc - { nounLoc :: Maybe Location - , nounArgs :: [a] -> [a] - , nounName :: Maybe name - } - -emptyNounAcc :: NounAcc a name -emptyNounAcc = NounAcc Nothing id Nothing - -setNounLoc :: Location -> NounAcc a name -> NounAcc a name -setNounLoc Nowhere acc = acc -setNounLoc _loc acc@NounAcc{nounLoc = Just _} = acc -setNounLoc loc NounAcc{nounLoc = Nothing, nounArgs = args, nounName = name} = - NounAcc (Just loc) args name - -addNounArg :: Locatable a => a -> NounAcc a name -> NounAcc a name -addNounArg a acc@NounAcc{nounLoc = loc, nounArgs = args, nounName = name} - | locate a == Nowhere = acc{nounArgs = args . (a :)} - | otherwise = NounAcc (loc <|> Just (locate a)) (args . (a :)) name - -setNounName :: name -> NounAcc a name -> NounAcc a name -setNounName name NounAcc{nounLoc = loc, nounArgs = args, nounName = Nothing} = - NounAcc loc args (Just name) -setNounName _ acc@NounAcc{nounName = Just _} = acc - -finalizeNounAcc :: NounAcc a name -> (Location, [a], name) -finalizeNounAcc NounAcc{nounLoc = Just loc, nounArgs = args, nounName = Just name} = - (loc, args [], name) -finalizeNounAcc NounAcc{nounName = Nothing} = - impossible "nounOf: missing variable slot" -finalizeNounAcc NounAcc{nounLoc = Nothing} = - impossible "nounOf: empty noun phrase" - -buildPhraseTrie - :: Locatable a - => Prod r Text (Located Token) a - -> Trie PhraseStep pat - -> Prod r Text (Located Token) (Location, pat, [a]) -buildPhraseTrie arg trie = - let stepParser = \case - PhraseTok tok -> setPhraseLoc <$> tokenPos tok - PhraseHole -> addPhraseArg <$> arg - finish f = - let (acc, pat) = f emptyPhraseAcc - (loc, args) = finalizePhraseAcc acc - in (loc, pat, args) - in finish <$> buildTrieProd stepParser trie - -buildTrieProd - :: (step -> Prod r Text (Located Token) (acc -> acc)) - -> Trie step pat - -> Prod r Text (Located Token) (acc -> (acc, pat)) -buildTrieProd stepParser = go - where - go Trie{trieValues = pats, trieEdges = edges} = - let leafs = asum [pure (\acc -> (acc, pat)) | pat <- pats] - edgesProds = asum - [ liftA2 (\f g -> g . f) (stepParser step) (go sub) - | (step, sub) <- edges - ] - in leafs <|> edgesProds - -buildNounTrie - :: Locatable a - => Prod r Text (Located Token) a - -> Prod r Text (Located Token) name - -> Trie NounStep pat - -> Prod r Text (Located Token) (Location, pat, [a], name) -buildNounTrie arg vars trie = - let stepParser = \case - NounTok tok -> setNounLoc <$> tokenPos tok - NounHole -> addNounArg <$> arg - NounVar -> setNounName <$> vars - finish f = - let (acc, pat) = f emptyNounAcc - (loc, args, name) = finalizeNounAcc acc - in (loc, pat, args, name) - in finish <$> buildTrieProd stepParser trie - - -symbolicPatternOf - :: forall r. [[MixfixItem]] - -> Prod r Text (Located Token) VarSymbol - -> Grammar r (Prod r Text (Located Token) SymbolPattern) -symbolicPatternOf ops varSymbol = rule $ - (tuplePattern <|> asum - [ go item - | ops' <- ops - , item <- ops' - ]) <?> "a symbolic pattern" - where - tuplePattern = do - token ParenL - first <- varSymbol <* token (Symbol ",") - second <- varSymbol <* token ParenR - pure (SymbolPattern PairSymbol [first, second]) - - go :: MixfixItem -> Prod r Text (Located Token) SymbolPattern - go item = SymbolPattern item <$> parseVars (mixfixPattern item) - - parseVars :: Pattern -> Prod r Text (Located Token) [VarSymbol] - parseVars = \case - End -> pure [] - TokenCons tok pat -> token tok *> parseVars pat - HoleCons pat -> (:) <$> varSymbol <*> parseVars pat - - -makeNounPhrase - :: [AdjL] - -> (Noun, t VarSymbol) - -> [AdjR] - -> Maybe Stmt - -> NounPhrase t -makeNounPhrase ls (n, vs) rs ms = NounPhrase ls n vs rs ms - - - - -begin, end :: Text -> Prod r Text (Located Token) Location -begin kind = tokenPos (BeginEnv kind) <?> ("\"\\begin{" <> kind <> "}\"") -end kind = tokenPos (EndEnv kind) <?> ("\"\\end{" <> kind <> "}\"") - --- | Surround a production rule @body@ with an environment of a certain @kind@ requiring a marker specified in a @\\label@. -envPos :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, Maybe [Token], Marker, a) -envPos kind body = do - p <- begin kind <?> ("start of a \"" <> kind <> "\" environment") - mt <- optional title - m <- label - a <- body <* end kind - pure (p, mt, m, a) - where - title :: Prod r Text (Located Token) [Token] - title = bracket (many (unLocated <$> satisfy (\ltok -> unLocated ltok /= BracketR))) - --- 'env_' is like 'env', but without allowing titles. --- -envPos_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a) -envPos_ kind body = (,) <$> begin kind <*> (optional label *> body) <* end kind - -envStartEndLocation :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a, Location) -envStartEndLocation kind body = (,,) <$> begin kind <*> (optional label *> body) <*> end kind - -env_ :: Text -> Prod r Text (Located Token) a -> Prod r Text (Located Token) a -env_ kind body = begin kind *> optional label *> body <* end kind - --- | A label specifying a marker for referencing via /@\\label{...}@/. Returns the marker text. -label :: Prod r Text (Located Token) Marker -label = label_ <?> "\"\\label{...}\"" - where - label_ = terminal \ltok -> case unLocated ltok of - Label m -> Just (Marker m) - _tok -> Nothing - --- | A reference via /@\\ref{...}@/. Returns the markers as text. -ref :: Prod r Text (Located Token) (NonEmpty Marker) -ref = terminal \ltok -> case unLocated ltok of - Ref ms -> Just (Marker <$> ms) - _tok -> Nothing - -math :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -math body = beginMath *> body <* endMath - -mathPos :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a) -mathPos body = (,) <$> beginMath <*> body <* endMath - -text :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -text body = begin "text" *> body <* end "text" <?> "\"\\text{...}\"" - -beginMath, endMath :: Prod r Text (Located Token) Location -beginMath = begin "math" <?> "start of a formula, e.g. \"$\"" -endMath = end "math" <?> "end of a formula, e.g. \"$\"" - -paren :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -paren body = token ParenL *> body <* token ParenR <?> "\"(...)\"" - -bracket :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -bracket body = token BracketL *> body <* token BracketR <?> "\"[...]\"" - -brace :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -brace body = token VisibleBraceL *> body <* token VisibleBraceR <?> "\"\\{...\\}\"" - -group :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}\"" - -align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Location, a) -align body = (,) <$> begin "align*" <*> body <* end "align*" - -cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a -cases body = begin "cases" *> body <* end "cases" - - -maybeVarToken :: Located Token -> Maybe VarSymbol -maybeVarToken ltok = case unLocated ltok of - Variable x -> Just (NamedVarAt (startPos ltok) x) - _tok -> Nothing - -maybeWordToken :: Located Token -> Maybe Text -maybeWordToken ltok = case unLocated ltok of - Word n -> Just n - _tok -> Nothing - -maybeIntToken :: Located Token -> Maybe Int -maybeIntToken ltok = case unLocated ltok of - Integer n -> Just n - _tok -> Nothing - -maybeIntTokenWithLoc :: Located Token -> Maybe (Location, Int) -maybeIntTokenWithLoc ltok = case unLocated ltok of - Integer n -> Just (startPos ltok, n) - _tok -> Nothing - -maybeCmdToken :: Located Token -> Maybe Text -maybeCmdToken ltok = case unLocated ltok of - Command n -> Just n - _tok -> Nothing - -structSymbol :: StructSymbol -> Prod r Text (Located Token) StructSymbol -structSymbol s@(StructSymbol c) = terminal \ltok -> case unLocated ltok of - Command c' | c == c' -> Just s - _ -> Nothing - -structSymbolPos :: StructSymbol -> Prod r Text (Located Token) (Location, StructSymbol) -structSymbolPos s@(StructSymbol c) = terminal \ltok -> case unLocated ltok of - Command c' | c == c' -> Just (startPos ltok, s) - _ -> Nothing - --- | Tokens that are allowed to appear in labels of environments. -maybeTagToken :: Located Token -> Maybe Text -maybeTagToken ltok = case unLocated ltok of - Symbol "'" ->Just "'" - Symbol "-" -> Just "" - _ -> maybeWordToken ltok - - -token :: Token -> Prod r Text (Located Token) Token -token tok = terminal maybeToken <?> tokToText tok - where - maybeToken ltok = case unLocated ltok of - tok' | tok == tok' -> Just tok - _ -> Nothing - -tokenLocated :: Token -> Prod r Text (Located Token) (Located Token) -tokenLocated tok = terminal maybeToken <?> tokToText tok - where - maybeToken ltok = case unLocated ltok of - tok' | tok == tok' -> Just ltok - _ -> Nothing - -tokenPos :: Token -> Prod r Text (Located Token) Location -tokenPos tok = terminal maybeToken <?> tokToText tok - where - maybeToken ltok = case unLocated ltok of - tok' | tok == tok' -> Just (startPos ltok) - _ -> Nothing diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs deleted file mode 100644 index a7ac169..0000000 --- a/source/Syntax/Concrete/Keywords.hs +++ /dev/null @@ -1,228 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} -{-| -This module defines lots of keywords and various filler -phrases. The prefix underscore indicates that we do not -care about the parse result (analogous to discarding -like @...; _ <- action; ...@ in do-notation). Moreover, -this convention allows the use of short names that would -otherwise be Haskell keywords or clash with other definitions. -Care should be taken with introducing too many variants of -a keyword, lest the grammar becomes needlessly ambiguous! - -The names are chosen using the following criteria: - - * As short as possible (e.g.: @_since@ over @_because@). - - * Sound like a keyword (e.g.: @_show@). - -This module also defines symbols that have special uses -(such as @_colon@ for its use in type signatures). --} -module Syntax.Concrete.Keywords where - - -import Base -import Syntax.Token -import Report.Location - -import Text.Earley (Prod, (<?>), terminal) - -infixr 0 ? --- | Variant of '<?>' for annotating literal tokens. -(?) :: Prod r Text t a -> Text -> Prod r Text t a -p ? e = p <?> ("\"" <> e <> "\"") - -word :: Text -> Prod r Text (Located Token) Location -word w = terminal maybeToken - where - maybeToken ltok = case unLocated ltok of - Word w' | w == w' -> Just (startPos ltok) - _ -> Nothing - -symbol :: Text -> Prod r Text (Located Token) Location -symbol s = terminal maybeToken - where - maybeToken ltok = case unLocated ltok of - Symbol s' | s == s' -> Just (startPos ltok) - _ -> Nothing - -command :: Text -> Prod r Text (Located Token) Location -command cmd = terminal maybeToken - where - maybeToken ltok = case unLocated ltok of - Command cmd' | cmd == cmd' -> Just (startPos ltok) - _ -> Nothing - -_arity :: Prod r Text (Located Token) Int -_arity = asum - [ 1 <$ word "unary" - , 2 <$ word "binary" - , 3 <$ word "ternary" - , 4 <$ word "quaternary" - , 5 <$ word "quinary" - , 6 <$ word "senary" - , 7 <$ word "septenary" - , 8 <$ word "octonary" - , 9 <$ word "nonary" - , 10 <$ word "denary" - ] <?> "\"unary\", \"binary\', ..." - --- * Keywords - -_an :: Prod r Text (Located Token) Location -_an = word "a" <|> word "an" <?> "indefinite article" -_and :: Prod r Text (Located Token) Location -_and = word "and" ? "and" -_are :: Prod r Text (Located Token) Location -_are = word "are" ? "are" -_asFollows :: Prod r Text (Located Token) Location -_asFollows = word "as" <* word "follows" ? "as follows" -_assumption :: Prod r Text (Located Token) Location -_assumption = word "assumption" ? "assumption" -_be :: Prod r Text (Located Token) Location -_be = word "be" ? "be" -_by :: Prod r Text (Located Token) Location -_by = word "by" ? "by" -_bySetExt :: Prod r Text (Located Token) Location -_bySetExt = word "by" <* ((word "set" ? "set") <* word "extensionality") ? "by set extensionality" -_can :: Prod r Text (Located Token) Location -_can = word "can" ? "can" -_consistsOf :: Prod r Text (Located Token) Location -_consistsOf = word "consists" <* word "of" ? "consists of" -_contradiction :: Prod r Text (Located Token) Location -_contradiction = optional (word "a") *> word "contradiction" ? "a contradiction" -_define :: Prod r Text (Located Token) Location -_define = word "define" ? "define" -_definition :: Prod r Text (Located Token) Location -_definition = word "definition" ? "definition" -_denote :: Prod r Text (Located Token) Location -_denote = word "denote" <|> (word "stand" <* word "for") ? "denote" -_denotes :: Prod r Text (Located Token) Location -_denotes = word "denotes" ? "denotes" -_do :: Prod r Text (Located Token) Location -_do = word "do" ? "do" -_does :: Prod r Text (Located Token) Location -_does = word "does" ? "does" -_either :: Prod r Text (Located Token) Location -_either = word "either" ? "either" -_equipped :: Prod r Text (Located Token) Location -_equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with" -_every :: Prod r Text (Located Token) Location -_every = word "every" ? "every" -_exist :: Prod r Text (Located Token) Location -_exist = word "there" <* word "exist" ? "there exist" -_exists :: Prod r Text (Located Token) Location -_exists = word "there" <* word "exists" ? "there exists" -_extends :: Prod r Text (Located Token) Location -_extends = (_is) <|> (word "consists" <* word "of") ? "consists of" -_fix :: Prod r Text (Located Token) Location -_fix = word "fix" ? "fix" -_follows :: Prod r Text (Located Token) Location -_follows = word "follows" ? "follows" -_for :: Prod r Text (Located Token) Location -_for = word "for" ? "for" -_forAll :: Prod r Text (Located Token) Location -_forAll = (word "for" <* word "all") <|> word "all" ? "all" -_forEvery :: Prod r Text (Located Token) Location -_forEvery = (word "for" <* word "every") <|> word "every" ? "for every" -_have :: Prod r Text (Located Token) Location -_have = word "we" <* word "have" <* optional (word "that") ? "we have" -_if :: Prod r Text (Located Token) Location -_if = word "if" ? "if" -_iff :: Prod r Text (Located Token) Location -_iff = word "iff" <|> (word "if" <* word "and" <* word "only" <* word "if") ? "iff" -_inductively :: Prod r Text (Located Token) Location -_inductively = word "inductively" ? "inductively" -_is :: Prod r Text (Located Token) Location -_is = word "is" ? "is" -_itIsWrong :: Prod r Text (Located Token) Location -_itIsWrong = word "it" <* word "is" <* (word "not" <* word "the" <* word "case" <|> word "wrong") <* word "that" ? "it is wrong that" -_let :: Prod r Text (Located Token) Location -_let = word "let" ? "let" -_neither :: Prod r Text (Located Token) Location -_neither = word "neither" ? "neither" -_no :: Prod r Text (Located Token) Location -_no = word "no" ? "no" -_nor :: Prod r Text (Located Token) Location -_nor = word "nor" ? "nor" -_not :: Prod r Text (Located Token) Location -_not = word "not" ? "not" -_omitted :: Prod r Text (Located Token) Location -_omitted = word "omitted" ? "omitted" -_on :: Prod r Text (Located Token) Location -_on = word "on" ? "on" -_oneOf :: Prod r Text (Located Token) Location -_oneOf = word "one" <* word "of" ? "one of" -_or :: Prod r Text (Located Token) Location -_or = word "or" ? "or" -_particularly :: Prod r Text (Located Token) Location -_particularly = (word "particularly" <|> (word "in" *> word "particular")) <* _comma ? "particularly" -_relation :: Prod r Text (Located Token) Location -_relation = word "relation" ? "relation" -_satisfying :: Prod r Text (Located Token) Location -_satisfying = _suchThat <|> word "satisfying" ? "satisfying" -_setOf :: Prod r Text (Located Token) Location -_setOf = word "set" <* word "of" ? "set of" -_now :: Prod r Text (Located Token) Location -_now = (word "then" <|> word "next" <|> word "now" <|> word "first" <|> word "finally" <|> word "subsequently" <|> word "ultimately") -_show :: Prod r Text (Located Token) Location -_show = optional _now *> optional (word "we") *> word "show" <* optional (word "that") -_since :: Prod r Text (Located Token) Location -_since = word "since" <|> word "because" ? "since" -_some :: Prod r Text (Located Token) Location -_some = word "some" ? "some" -_suchThat :: Prod r Text (Located Token) Location -_suchThat = ((word "such" <* word "that") <|> (word "s" <* _dot <* word "t" <* _dot)) ? "such that" -_sufficesThat :: Prod r Text (Located Token) Location -_sufficesThat = word "it" <* word "suffices" <* word "to" <* word "show" <* word "that" ? "it suffices to show" -_suppose :: Prod r Text (Located Token) Location -_suppose = (word "suppose" <|> word "assume") <* optional (word "that") ? "assume" -_take :: Prod r Text (Located Token) Location -_take = optional _now *> (word "take" <|> word "consider") ? "take" -_that :: Prod r Text (Located Token) Location -_that = word "that" ? "that" -_the :: Prod r Text (Located Token) Location -_the = word "the" ? "the" -_then :: Prod r Text (Located Token) Location -_then = word "then" ? "then" -_thus :: Prod r Text (Located Token) Location -_thus = word "thus" <|> word "hence" <|> _now <|> word "therefore" ? "thus" -_trivial :: Prod r Text (Located Token) Location -_trivial = word "straightforward" <|> word "trivial" ? "trivial" -_unique :: Prod r Text (Located Token) Location -_unique = word "unique" ? "unique" -_write :: Prod r Text (Located Token) Location -_write = (optional (word "we") *> word "say" <* optional (word "that")) <|> (optional (word "we") *> word "write") ? "write" - --- | Introducing plain claims in proofs. -_haveIntro :: Prod r Text (Located Token) Location -_haveIntro = _thus <|> _particularly <|> _have - --- * Symbols - -_colon :: Prod r Text (Located Token) Location -_colon = symbol ":" ? ":" -_pipe :: Prod r Text (Located Token) Location -_pipe = (optional (command "middle") *> symbol "|") <|> command "mid" ? "\\mid" -_comma :: Prod r Text (Located Token) Location -_comma = symbol "," ? "," -_commaAnd :: Prod r Text (Located Token) Location -_commaAnd = symbol "," <* optional (word "and") ? ", and" -_commaOr :: Prod r Text (Located Token) Location -_commaOr = symbol "," <* optional (word "or") ? ", or" -_defeq :: Prod r Text (Located Token) Location -_defeq = symbol ":=" ? ":=" -- Should use `\coloneq` from unicode-math as display. -_dot :: Prod r Text (Located Token) Location -_dot = symbol "." ? "." -_eq :: Prod r Text (Located Token) Location -_eq = symbol "=" ? "=" -_in :: Prod r Text (Located Token) Location -_in = command "in" ? "\\in" -_subseteq :: Prod r Text (Located Token) Location -_subseteq = command "subseteq" ? "\\subseteq" -_to :: Prod r Text (Located Token) Location -_to = command "to" ? "\\to" -_mapsto :: Prod r Text (Located Token) Location -_mapsto = command "mapsto" ? "\\mapsto" -_ampersand :: Prod r Text (Located Token) Location -_ampersand = symbol "&" ? "&" diff --git a/source/Syntax/Interface.hs b/source/Syntax/Interface.hs deleted file mode 100644 index 4b84cec..0000000 --- a/source/Syntax/Interface.hs +++ /dev/null @@ -1,887 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - -module Syntax.Interface - ( MixfixLevel - , mixfixLevel - , mixfixLevelValue - , MixfixLevelError(..) - , Fixity(..) - , sourcePragmaFixity - , CanonicalLexicalEntry(..) - , canonicalLexicalSurfacePatterns - , eligibleExpressionPattern - , CanonicalSyntaxDelta - , canonicalSyntaxDelta - , canonicalSyntaxDeltaEntries - , canonicalSyntaxDeltaSize - , CanonicalSyntaxCollision - , canonicalCollisionPattern - , canonicalCollisionEntries - , CanonicalSyntaxDeltaId - , canonicalSyntaxDeltaId - , canonicalSyntaxDeltaIdDigest - , BaseSyntaxInterfaceId - , baseSyntaxInterfaceId - , baseSyntaxInterfaceIdDigest - , baseSyntaxManifest - , fixedBaseSyntaxEntries - , SyntaxInterfaceId - , syntaxInterfaceIdDigest - , ModuleSyntaxInterface - , moduleSyntaxInterface - , moduleSyntaxBase - , moduleSyntaxDirectInputs - , moduleSyntaxLocalDelta - , moduleSyntaxAssertedId - , SyntaxInterfaceError(..) - , validateModuleSyntaxInterface - , putCanonicalLexicalEntryCache - , getCanonicalLexicalEntryCache - , putPatternCache - , getPatternCache - , putTokenCache - , getTokenCache - , putCanonicalSyntaxDeltaCache - , getCanonicalSyntaxDeltaCache - , putModuleSyntaxInterfaceCache - , getModuleSyntaxInterfaceCache - , putBaseSyntaxInterfaceIdCache - , getBaseSyntaxInterfaceIdCache - , putSyntaxInterfaceIdCache - , getSyntaxInterfaceIdCache - ) where - -import Base - -import Felix.Cache.Codec -import Syntax.Abstract -import Syntax.Lexicon -import Syntax.Pragma - -import Control.DeepSeq (NFData) -import Control.Monad (unless) -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Word (Word8) -import Numeric.Natural (Natural) - - -newtype MixfixLevel = MixfixLevel Word8 - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -data MixfixLevelError - = MixfixLevelOutOfRange !Word8 - deriving stock (Show, Eq) - -mixfixLevel :: Word8 -> Either MixfixLevelError MixfixLevel -mixfixLevel supplied - | supplied <= 9 = - Right (MixfixLevel supplied) - | otherwise = - Left (MixfixLevelOutOfRange supplied) - -mixfixLevelValue :: MixfixLevel -> Word8 -mixfixLevelValue (MixfixLevel level) = - level - -data Fixity = Fixity - { fixityAssociativity :: !Associativity - , fixityLevel :: !MixfixLevel - } deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -sourcePragmaFixity :: SyntaxPragma -> Fixity -sourcePragmaFixity pragma = - Fixity - (syntaxPragmaAssociativity pragma) - (MixfixLevel - (sourceMixfixLevelValue - (syntaxPragmaLevel pragma))) - --- | Complete origin-free lexical semantics produced by scanning. -data CanonicalLexicalEntry - = CanonicalLeftAdjective !Pattern !Marker - | CanonicalRightAdjective !Pattern !Marker - | CanonicalFunctionPhrase !Pattern !Pattern !Marker - | CanonicalNoun !Pattern !Pattern !Marker - | CanonicalStructureNoun !Pattern !Pattern !Marker - | CanonicalVerb !Pattern !Pattern !Marker - | CanonicalRelation !Token !ParameterArity !Marker - | CanonicalExpressionFunction !Pattern !Marker !Fixity - | CanonicalPrefixPredicate !Text !Natural !Marker - | CanonicalStructureOperation !Text - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - --- | Every surface pattern through which the concrete parser can select an --- entry. Equal singular and plural surfaces are returned only once. -canonicalLexicalSurfacePatterns - :: CanonicalLexicalEntry - -> NonEmpty Pattern -canonicalLexicalSurfacePatterns = - deduplicatePatterns . \case - CanonicalLeftAdjective pat _marker -> - [pat] - CanonicalRightAdjective pat _marker -> - [pat] - CanonicalFunctionPhrase singular _plural _marker -> - [singular] - CanonicalNoun singular plural _marker -> - [singular, plural] - CanonicalStructureNoun singular _plural _marker -> - [singular] - CanonicalVerb singular plural _marker -> - [singular, plural] - CanonicalRelation token arity marker -> - [ relationSymbolPattern - (RelationSymbol token arity marker) - ] - CanonicalExpressionFunction pat _marker _fixity -> - [pat] - CanonicalPrefixPredicate command _arity _marker -> - [ prefixPredicatePattern - (PrefixPredicate command 0) - ] - CanonicalStructureOperation command -> - [structSymbolPattern (StructSymbol command)] - where - deduplicatePatterns patterns = - case NonEmpty.nonEmpty - (Set.toList (Set.fromList patterns)) of - Just nonempty -> - nonempty - Nothing -> - impossible - "canonical lexical entry has no parser surface" - -eligibleExpressionPattern :: Pattern -> Bool -eligibleExpressionPattern pat = - case patternToHoley pat of - Nothing : rest -> - case reverse rest of - Nothing : middleReversed -> - let middle = - reverse middleReversed - in - countHoles middle == 0 - && any isJust middle - _ -> - False - _ -> - False - where - countHoles = - length . List.filter isNothing - -newtype CanonicalSyntaxDelta = - CanonicalSyntaxDelta - [CanonicalLexicalEntry] - deriving stock (Show, Eq, Generic) - deriving anyclass (NFData) - -data CanonicalSyntaxCollision = CanonicalSyntaxCollision - { canonicalCollisionPattern :: !Pattern - , canonicalCollisionEntries - :: !(NonEmpty CanonicalLexicalEntry) - } deriving stock (Show, Eq) - -canonicalSyntaxDelta - :: [CanonicalLexicalEntry] - -> Either CanonicalSyntaxCollision CanonicalSyntaxDelta -canonicalSyntaxDelta supplied = - case orderedCollisions of - [] -> - Right (CanonicalSyntaxDelta orderedEntries) - (_encodedPattern, pat, entries) : _ -> - Left - (CanonicalSyntaxCollision - pat - (case NonEmpty.nonEmpty - (canonicalEntryOrder - (Set.toList entries)) of - Just collisionEntries -> - collisionEntries - Nothing -> - impossible - "canonical syntax collision has no entries")) - where - orderedEntries = - canonicalEntryOrder - (Set.toList (Set.fromList supplied)) - - grouped = - foldl' - (\entries entry -> - foldl' - (\indexed pat -> - Map.insertWith - Set.union - pat - (Set.singleton entry) - indexed) - entries - (canonicalLexicalSurfacePatterns entry)) - mempty - orderedEntries - - orderedCollisions = - List.sortOn - (\(encodedPattern, _pattern, _entries) -> - encodedPattern) - [ ( encodeCache (putPatternCache pat) - , pat - , entries - ) - | (pat, entries) <- Map.toList grouped - , Set.size entries > 1 - ] - -canonicalSyntaxDeltaEntries - :: CanonicalSyntaxDelta - -> [CanonicalLexicalEntry] -canonicalSyntaxDeltaEntries - (CanonicalSyntaxDelta entries) = - entries - -canonicalSyntaxDeltaSize :: CanonicalSyntaxDelta -> Int -canonicalSyntaxDeltaSize - (CanonicalSyntaxDelta entries) = - length entries - -canonicalEntryOrder - :: [CanonicalLexicalEntry] - -> [CanonicalLexicalEntry] -canonicalEntryOrder = - List.sortOn - (encodeCache . putCanonicalLexicalEntryCache) - -newtype CanonicalSyntaxDeltaId = - CanonicalSyntaxDeltaId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -canonicalSyntaxDeltaId - :: CanonicalSyntaxDelta - -> CanonicalSyntaxDeltaId -canonicalSyntaxDeltaId delta = - CanonicalSyntaxDeltaId - (hashCacheFields - "felix-syntax-delta-v1" - [encodeCache - (putCanonicalSyntaxDeltaCache delta)]) - -canonicalSyntaxDeltaIdDigest - :: CanonicalSyntaxDeltaId - -> CacheDigest -canonicalSyntaxDeltaIdDigest - (CanonicalSyntaxDeltaId digest) = - digest - -newtype BaseSyntaxInterfaceId = - BaseSyntaxInterfaceId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -baseSyntaxInterfaceId :: BaseSyntaxInterfaceId -baseSyntaxInterfaceId = - BaseSyntaxInterfaceId - (hashCacheFields - "felix-base-syntax-interface-v1" - [encodeCache - (putCacheList - putManifestRow - baseSyntaxManifest)]) - where - putManifestRow = - putCacheList putCanonicalLexicalEntryCache - . canonicalEntryOrder - -baseSyntaxInterfaceIdDigest - :: BaseSyntaxInterfaceId - -> CacheDigest -baseSyntaxInterfaceIdDigest - (BaseSyntaxInterfaceId digest) = - digest - -baseSyntaxManifest :: [[CanonicalLexicalEntry]] -baseSyntaxManifest = - case traverse makeRow - (zip [0 :: Word8 ..] builtinMixfixLevels) of - Right rows - | length rows == 10 -> - rows - _ -> - impossible - "the fixed mixfix manifest does not have ten valid rows" - where - makeRow (row, entries) = do - level <- mixfixLevel row - pure - [ CanonicalExpressionFunction - pat - marker - (Fixity associativity level) - | MixfixItem pat marker associativity <- - entries - ] - --- | Every fixed lexical entry consulted by the concrete parser. The base --- syntax identity above commits to the ten expression rows; the remaining --- fixed categories are compiler input covered by the cache epoch. -fixedBaseSyntaxEntries :: [CanonicalLexicalEntry] -fixedBaseSyntaxEntries = - case canonicalSyntaxDelta rawEntries of - Right delta -> - canonicalSyntaxDeltaEntries delta - Left collision -> - impossible - ("fixed base syntax contains a collision: " - <> show collision) - where - rawEntries = - concat baseSyntaxManifest - <> (canonicalAdjective CanonicalLeftAdjective - <$> lexiconAdjLs builtins) - <> (canonicalAdjective CanonicalRightAdjective - <$> lexiconAdjRs builtins) - <> (canonicalSgPl CanonicalFunctionPhrase - <$> lexiconFuns builtins) - <> (canonicalSgPl CanonicalNoun - <$> lexiconNouns builtins) - <> (canonicalSgPl CanonicalStructureNoun - <$> lexiconStructNouns builtins) - <> (canonicalSgPl CanonicalVerb - <$> lexiconVerbs builtins) - <> (canonicalRelation - <$> lexiconRelationSymbols builtins) - <> (canonicalPrefix - <$> lexiconPrefixPredicates builtins) - <> (canonicalStructure - <$> lexiconStructFun builtins) - - canonicalAdjective constructor item = - constructor - (lexicalItemPattern item) - (lexicalItemMarker item) - - canonicalSgPl constructor item = - let patterns = - lexicalItemSgPlPattern item - in - constructor - (sg patterns) - (pl patterns) - (lexicalItemSgPlMarker item) - - canonicalRelation relation = - CanonicalRelation - (relationSymbolToken relation) - (relationSymbolParameterArity relation) - (relationSymbolMarker relation) - - canonicalPrefix - (PrefixPredicate command arity, marker) = - CanonicalPrefixPredicate - command - (fromIntegral arity) - marker - - canonicalStructure (StructSymbol command) = - CanonicalStructureOperation command - -newtype SyntaxInterfaceId = - SyntaxInterfaceId CacheDigest - deriving stock (Show, Eq, Ord, Generic) - deriving newtype (Hashable, NFData) - -syntaxInterfaceIdDigest :: SyntaxInterfaceId -> CacheDigest -syntaxInterfaceIdDigest (SyntaxInterfaceId digest) = - digest - -data ModuleSyntaxInterface = ModuleSyntaxInterface - !BaseSyntaxInterfaceId - ![SyntaxInterfaceId] - !CanonicalSyntaxDelta - !SyntaxInterfaceId - deriving stock (Show, Eq, Generic) - deriving anyclass (NFData) - -moduleSyntaxBase - :: ModuleSyntaxInterface - -> BaseSyntaxInterfaceId -moduleSyntaxBase - (ModuleSyntaxInterface base _direct _delta _asserted) = - base - -moduleSyntaxDirectInputs - :: ModuleSyntaxInterface - -> [SyntaxInterfaceId] -moduleSyntaxDirectInputs - (ModuleSyntaxInterface _base direct _delta _asserted) = - direct - -moduleSyntaxLocalDelta - :: ModuleSyntaxInterface - -> CanonicalSyntaxDelta -moduleSyntaxLocalDelta - (ModuleSyntaxInterface _base _direct delta _asserted) = - delta - -moduleSyntaxAssertedId - :: ModuleSyntaxInterface - -> SyntaxInterfaceId -moduleSyntaxAssertedId - (ModuleSyntaxInterface _base _direct _delta asserted) = - asserted - -data SyntaxInterfaceError - = DuplicateDirectSyntaxInterface !SyntaxInterfaceId - | UnexpectedBaseSyntaxInterface - !BaseSyntaxInterfaceId - !BaseSyntaxInterfaceId - | SyntaxInterfaceIdMismatch - !SyntaxInterfaceId - !SyntaxInterfaceId - deriving stock (Show, Eq) - -moduleSyntaxInterface - :: [SyntaxInterfaceId] - -> CanonicalSyntaxDelta - -> Either SyntaxInterfaceError ModuleSyntaxInterface -moduleSyntaxInterface direct delta = - validateModuleSyntaxInterface - baseSyntaxInterfaceId - direct - delta - (computeSyntaxInterfaceId - baseSyntaxInterfaceId - direct - delta) - -validateModuleSyntaxInterface - :: BaseSyntaxInterfaceId - -> [SyntaxInterfaceId] - -> CanonicalSyntaxDelta - -> SyntaxInterfaceId - -> Either SyntaxInterfaceError ModuleSyntaxInterface -validateModuleSyntaxInterface base direct delta asserted = do - unless - (base == baseSyntaxInterfaceId) - (Left - (UnexpectedBaseSyntaxInterface - base - baseSyntaxInterfaceId)) - case firstDuplicate direct of - Just duplicate -> - Left - (DuplicateDirectSyntaxInterface duplicate) - Nothing -> - pure () - let computed = - computeSyntaxInterfaceId base direct delta - unless - (asserted == computed) - (Left - (SyntaxInterfaceIdMismatch - asserted - computed)) - Right - (ModuleSyntaxInterface - base - direct - delta - asserted) - -computeSyntaxInterfaceId - :: BaseSyntaxInterfaceId - -> [SyntaxInterfaceId] - -> CanonicalSyntaxDelta - -> SyntaxInterfaceId -computeSyntaxInterfaceId base direct delta = - SyntaxInterfaceId - (hashCacheFields - "felix-syntax-interface-v1" - [ cacheDigestBytes - (baseSyntaxInterfaceIdDigest base) - , encodeCache - (putCacheList - putSyntaxInterfaceIdCache - direct) - , cacheDigestBytes - (canonicalSyntaxDeltaIdDigest - (canonicalSyntaxDeltaId delta)) - ]) - -firstDuplicate :: Ord value => [value] -> Maybe value -firstDuplicate = - go mempty - where - go _seen [] = - Nothing - go seen (value : rest) - | value `Set.member` seen = - Just value - | otherwise = - go (Set.insert value seen) rest - -putCanonicalLexicalEntryCache - :: CanonicalLexicalEntry - -> CachePut -putCanonicalLexicalEntryCache = \case - CanonicalLeftAdjective pat marker -> do - putCacheTag 0x00 - putPatternCache pat - putMarkerCache marker - CanonicalRightAdjective pat marker -> do - putCacheTag 0x01 - putPatternCache pat - putMarkerCache marker - CanonicalFunctionPhrase singular plural marker -> do - putCacheTag 0x02 - putPatternCache singular - putPatternCache plural - putMarkerCache marker - CanonicalNoun singular plural marker -> do - putCacheTag 0x03 - putPatternCache singular - putPatternCache plural - putMarkerCache marker - CanonicalStructureNoun singular plural marker -> do - putCacheTag 0x04 - putPatternCache singular - putPatternCache plural - putMarkerCache marker - CanonicalVerb singular plural marker -> do - putCacheTag 0x05 - putPatternCache singular - putPatternCache plural - putMarkerCache marker - CanonicalRelation token arity marker -> do - putCacheTag 0x06 - putTokenCache token - putCacheNatural (parameterArityValue arity) - putMarkerCache marker - CanonicalExpressionFunction pat marker fixity -> do - putCacheTag 0x07 - putPatternCache pat - putMarkerCache marker - putFixityCache fixity - CanonicalPrefixPredicate command arity marker -> do - putCacheTag 0x08 - putCacheText command - putCacheNatural arity - putMarkerCache marker - CanonicalStructureOperation command -> do - putCacheTag 0x09 - putCacheText command - -getCanonicalLexicalEntryCache - :: CacheGet CanonicalLexicalEntry -getCanonicalLexicalEntryCache = - getCacheTag >>= \case - 0x00 -> - CanonicalLeftAdjective - <$> getPatternCache - <*> getMarkerCache - 0x01 -> - CanonicalRightAdjective - <$> getPatternCache - <*> getMarkerCache - 0x02 -> - CanonicalFunctionPhrase - <$> getPatternCache - <*> getPatternCache - <*> getMarkerCache - 0x03 -> - CanonicalNoun - <$> getPatternCache - <*> getPatternCache - <*> getMarkerCache - 0x04 -> - CanonicalStructureNoun - <$> getPatternCache - <*> getPatternCache - <*> getMarkerCache - 0x05 -> - CanonicalVerb - <$> getPatternCache - <*> getPatternCache - <*> getMarkerCache - 0x06 -> - CanonicalRelation - <$> getTokenCache - <*> (ParameterArity <$> getCacheNatural) - <*> getMarkerCache - 0x07 -> - CanonicalExpressionFunction - <$> getPatternCache - <*> getMarkerCache - <*> getFixityCache - 0x08 -> - CanonicalPrefixPredicate - <$> getCacheText - <*> getCacheNatural - <*> getMarkerCache - 0x09 -> - CanonicalStructureOperation - <$> getCacheText - tag -> - fail - ("unknown canonical lexical entry tag " - <> show tag) - -putCanonicalSyntaxDeltaCache - :: CanonicalSyntaxDelta - -> CachePut -putCanonicalSyntaxDeltaCache - (CanonicalSyntaxDelta entries) = - putCacheList putCanonicalLexicalEntryCache entries - -getCanonicalSyntaxDeltaCache - :: CacheGet CanonicalSyntaxDelta -getCanonicalSyntaxDeltaCache = do - supplied <- getCacheList getCanonicalLexicalEntryCache - case canonicalSyntaxDelta supplied of - Left collision -> - fail - ("colliding cached canonical syntax entries: " - <> show collision) - Right delta - | canonicalSyntaxDeltaEntries delta == supplied -> - pure delta - | otherwise -> - fail - "cached canonical syntax entries are not in canonical order" - -putModuleSyntaxInterfaceCache - :: ModuleSyntaxInterface - -> CachePut -putModuleSyntaxInterfaceCache - (ModuleSyntaxInterface base direct delta asserted) = do - putBaseSyntaxInterfaceIdCache base - putCacheList putSyntaxInterfaceIdCache direct - putCanonicalSyntaxDeltaCache delta - putSyntaxInterfaceIdCache asserted - -getModuleSyntaxInterfaceCache - :: CacheGet ModuleSyntaxInterface -getModuleSyntaxInterfaceCache = do - base <- getBaseSyntaxInterfaceIdCache - direct <- getCacheList getSyntaxInterfaceIdCache - delta <- getCanonicalSyntaxDeltaCache - asserted <- getSyntaxInterfaceIdCache - case - validateModuleSyntaxInterface - base - direct - delta - asserted of - Left err -> - fail - ("invalid module syntax interface: " - <> show err) - Right interface -> - pure interface - -putBaseSyntaxInterfaceIdCache - :: BaseSyntaxInterfaceId - -> CachePut -putBaseSyntaxInterfaceIdCache - (BaseSyntaxInterfaceId digest) = - putCacheDigest digest - -getBaseSyntaxInterfaceIdCache - :: CacheGet BaseSyntaxInterfaceId -getBaseSyntaxInterfaceIdCache = - BaseSyntaxInterfaceId <$> getCacheDigest - -putSyntaxInterfaceIdCache - :: SyntaxInterfaceId - -> CachePut -putSyntaxInterfaceIdCache - (SyntaxInterfaceId digest) = - putCacheDigest digest - -getSyntaxInterfaceIdCache - :: CacheGet SyntaxInterfaceId -getSyntaxInterfaceIdCache = - SyntaxInterfaceId <$> getCacheDigest - -putFixityCache :: Fixity -> CachePut -putFixityCache (Fixity associativity level) = do - putAssociativityCache associativity - putCacheTag (mixfixLevelValue level) - -getFixityCache :: CacheGet Fixity -getFixityCache = do - associativity <- getAssociativityCache - suppliedLevel <- getCacheTag - case mixfixLevel suppliedLevel of - Left err -> - fail ("invalid cached mixfix level: " <> show err) - Right level -> - pure (Fixity associativity level) - -putAssociativityCache :: Associativity -> CachePut -putAssociativityCache = - putCacheTag . \case - LeftAssoc -> - 0x00 - RightAssoc -> - 0x01 - NonAssoc -> - 0x02 - -getAssociativityCache :: CacheGet Associativity -getAssociativityCache = - getCacheTag >>= \case - 0x00 -> - pure LeftAssoc - 0x01 -> - pure RightAssoc - 0x02 -> - pure NonAssoc - tag -> - fail - ("unknown associativity tag " <> show tag) - -putMarkerCache :: Marker -> CachePut -putMarkerCache (Marker marker) = - putCacheText marker - -getMarkerCache :: CacheGet Marker -getMarkerCache = - Marker <$> getCacheText - -putPatternCache :: Pattern -> CachePut -putPatternCache = \case - End -> - putCacheTag 0x00 - HoleCons rest -> do - putCacheTag 0x01 - putPatternCache rest - TokenCons token rest -> do - putCacheTag 0x02 - putTokenCache token - putPatternCache rest - -getPatternCache :: CacheGet Pattern -getPatternCache = - getCacheTag >>= \case - 0x00 -> - pure End - 0x01 -> - HoleCons <$> getPatternCache - 0x02 -> - TokenCons - <$> getTokenCache - <*> getPatternCache - tag -> - fail - ("unknown lexical pattern tag " <> show tag) - -putTokenCache :: Token -> CachePut -putTokenCache = \case - Word text -> do - putCacheTag 0x00 - putCacheText text - Variable text -> do - putCacheTag 0x01 - putCacheText text - Symbol text -> do - putCacheTag 0x02 - putCacheText text - Integer integer -> do - putCacheTag 0x03 - putCacheInteger (toInteger integer) - Command text -> do - putCacheTag 0x04 - putCacheText text - Label text -> do - putCacheTag 0x05 - putCacheText text - Ref references -> do - putCacheTag 0x06 - putCacheList putCacheText (toList references) - BeginEnv text -> do - putCacheTag 0x07 - putCacheText text - EndEnv text -> do - putCacheTag 0x08 - putCacheText text - ParenL -> - putCacheTag 0x09 - ParenR -> - putCacheTag 0x0a - BracketL -> - putCacheTag 0x0b - BracketR -> - putCacheTag 0x0c - VisibleBraceL -> - putCacheTag 0x0d - VisibleBraceR -> - putCacheTag 0x0e - InvisibleBraceL -> - putCacheTag 0x0f - InvisibleBraceR -> - putCacheTag 0x10 - -getTokenCache :: CacheGet Token -getTokenCache = - getCacheTag >>= \case - 0x00 -> - Word <$> getCacheText - 0x01 -> - Variable <$> getCacheText - 0x02 -> - Symbol <$> getCacheText - 0x03 -> - Integer <$> getCacheInt - 0x04 -> - Command <$> getCacheText - 0x05 -> - Label <$> getCacheText - 0x06 -> do - references <- getCacheList getCacheText - case NonEmpty.nonEmpty references of - Nothing -> - fail "cached reference token has no marker" - Just nonempty -> - pure (Ref nonempty) - 0x07 -> - BeginEnv <$> getCacheText - 0x08 -> - EndEnv <$> getCacheText - 0x09 -> - pure ParenL - 0x0a -> - pure ParenR - 0x0b -> - pure BracketL - 0x0c -> - pure BracketR - 0x0d -> - pure VisibleBraceL - 0x0e -> - pure VisibleBraceR - 0x0f -> - pure InvisibleBraceL - 0x10 -> - pure InvisibleBraceR - tag -> - fail ("unknown lexical token tag " <> show tag) - -getCacheInt :: CacheGet Int -getCacheInt = do - integer <- getCacheInteger - if integer < toInteger (minBound :: Int) - || integer > toInteger (maxBound :: Int) - then - fail "cached integer token exceeds Int" - else - pure (fromInteger integer) diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs deleted file mode 100644 index 5a8cb65..0000000 --- a/source/Syntax/Internal.hs +++ /dev/null @@ -1,830 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE ViewPatterns #-} - --- | Data types for the internal (semantic) syntax tree. -module Syntax.Internal - ( module Syntax.Internal - , module Syntax.Abstract - , module Syntax.LexicalPhrase - , module Syntax.Token - ) where - - -import Base -import Syntax.Lexicon - ( pattern PairSymbol - , pattern UnionsSymbol - , pattern UpairSymbol - ) -import Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl) -import Syntax.Token (Token(..)) -import Report.Location - -import Syntax.Abstract - ( Chain(..) - , Associativity(..) - , Connective(..) - , VarSymbol(..) - , pattern NamedVar - , pattern FreshVar - , FunctionSymbol - , SymbolPattern(..) - , MixfixItem(..) - , Pattern(..) - , LexicalItem - , LexicalItemSgPl - , RelationSymbol(..) - , ParameterArity(..) - , PrefixPredicate(..) - , StructSymbol (..) - , Relation - , PropositionalConstant(..) - , StructPhrase - , Justification(..) - , Marker(..) - , markerFromToken - , lexicalItemMarker - , lexicalItemSgPlMarker - , mkLexicalItem - , mkLexicalItemSgPl - , relationSymbolMarker - , relationSymbolParameterArity - , relationSymbolToken - , parameterArityOf - , parameterArityValue - , zeroParameterArity - , mixfixMarker - , mkMixfixItem - , pattern CarrierSymbol, pattern ConsSymbol, pattern ElementSymbol - , pattern NotElementSymbol, pattern EqSymbol, pattern NeqSymbol, pattern SubseteqSymbol - ) - -import Bound -import Bound.Scope -import Data.Deriving (deriveShow1, deriveEq1, deriveOrd1) -import Data.Hashable.Lifted -import Data.HashMap.Strict qualified as HM -import Data.List qualified as List -import Data.List.NonEmpty qualified as NonEmpty -import Data.Set qualified as Set - --- | 'Symbol's can be used as function and relation symbols. -data Symbol - = SymbolMixfix FunctionSymbol - | SymbolFun LexicalItemSgPl - | SymbolInteger Int - | SymbolPredicate Predicate - deriving (Show, Eq, Ord, Generic, Hashable) - - -data Predicate - = PredicateAdj LexicalItem - | PredicateVerb LexicalItemSgPl - | PredicateNoun LexicalItemSgPl -- ^ /@\<...\> is a \<...\>@/. - | PredicateRelation RelationSymbol - | PredicateSymbol Text - | PredicateNounStruct LexicalItemSgPl -- ^ /@\<...\> is a \<...\>@/. - deriving (Show, Eq, Ord, Generic, Hashable) - - --- | The object-language marker of an ownable symbol. -objectSymbolMarker :: Symbol -> Maybe Marker -objectSymbolMarker = \case - SymbolMixfix symbol -> - Just (mixfixMarker symbol) - SymbolFun symbol -> - Just (lexicalItemSgPlMarker symbol) - SymbolInteger{} -> - Nothing - SymbolPredicate predicate -> - Just (predicateObjectMarker predicate) - --- | The object-language marker of a predicate. -predicateObjectMarker :: Predicate -> Marker -predicateObjectMarker = \case - PredicateAdj item -> - lexicalItemMarker item - PredicateVerb item -> - lexicalItemSgPlMarker item - PredicateNoun item -> - lexicalItemSgPlMarker item - PredicateRelation relation -> - relationSymbolMarker relation - PredicateSymbol text -> - Marker text - PredicateNounStruct item -> - lexicalItemSgPlMarker item - - -data Quantifier - = Universally - | Existentially - deriving (Show, Eq, Ord, Generic, Hashable) - -type Formula = Term -type Term = Expr -type Expr = ExprOf VarSymbol - - --- | Internal higher-order expressions. -data ExprOf a - = TermVar a - -- ^ Fresh constants disjoint from all user-named identifiers. - -- These can be used to eliminate higher-order constructs. - -- - | TermSymbol Location Symbol [ExprOf a] - -- ^ Application of a symbol (including function and predicate symbols). - | TermSymbolStruct StructSymbol (Maybe (ExprOf a)) - -- - | Apply (ExprOf a) (NonEmpty (ExprOf a)) - -- ^ Higher-order application. - -- - | TermSep VarSymbol (ExprOf a) (Scope () ExprOf a) - -- ^ Set comprehension using seperation, e.g.: /@{ x ∈ X | P(x) }@/. - -- - | ReplacePred VarSymbol VarSymbol (ExprOf a) (Scope ReplacementVar ExprOf a) - -- ^ Replacement for single-valued predicates. The concrete syntax for these - -- syntactically requires a bounded existential quantifier in the condition: - -- - -- /@$\\{ y | \\exists x\\in A. P(x,y) \\}$@/ - -- - -- In definitions the single-valuedness of @P@ becomes a proof obligation. - -- In other cases we could instead add it as constraint - -- - -- /@$b\\in \\{ y | \\exists x\\in A. P(x,y) \\}$@/ - -- /@iff@/ - -- /@$\\exists x\\in A. P(x,y)$ and $P$ is single valued@/ - -- - -- - | ReplaceFun (NonEmpty (VarSymbol, ExprOf a)) (Scope VarSymbol ExprOf a) (Scope VarSymbol ExprOf a) - -- ^ Set comprehension using functional replacement, - -- e.g.: /@{ f(x, y) | x ∈ X; y ∈ Y; P(x, y) }@/. - -- The list of pairs gives the domains, the integers in the scope point to list indices. - -- The first scope is the lhs, the optional scope can be used for additional constraints - -- on the variables (i.e. implicit separation over the product of the domains). - -- An out-of-bound index is an error, since otherwise replacement becomes unsound. - -- - | Connected Connective (ExprOf a) (ExprOf a) - | Lambda (Scope VarSymbol ExprOf a) - | Quantified Quantifier (Scope VarSymbol ExprOf a) - | PropositionalConstant PropositionalConstant - | Not Location (ExprOf a) - deriving (Functor, Foldable, Traversable) - --- | Best source location carried by an elaborated expression. -exprLocation :: Expr -> Location -exprLocation = \case - TermVar variable -> locate variable - TermSymbol location _symbol _arguments -> location - TermSymbolStruct _symbol expression -> - maybe Nowhere exprLocation expression - Apply function _arguments -> exprLocation function - TermSep variable _bound _predicate -> locate variable - ReplacePred value _domain _bound _predicate -> locate value - ReplaceFun ((variable, _domain) :| _remaining) _value _condition -> - locate variable - Connected _connective left _right -> exprLocation left - Lambda{} -> Nowhere - Quantified{} -> Nowhere - PropositionalConstant{} -> Nowhere - Not location _term -> location - -data ReplacementVar = ReplacementDomVar | ReplacementRangeVar deriving (Show, Eq, Ord, Generic, Hashable) - -makeBound ''ExprOf - -deriveShow1 ''ExprOf -deriveEq1 ''ExprOf -deriveOrd1 ''ExprOf - -deriving instance Show a => Show (ExprOf a) -deriving instance Eq a => Eq (ExprOf a) -deriving instance Ord a => Ord (ExprOf a) - -deriving instance Generic (ExprOf a) -deriving instance Generic1 ExprOf - -deriving instance Hashable1 ExprOf - -deriving instance Hashable a => Hashable (ExprOf a) - -mentionedSymbols :: ExprOf a -> Set Symbol -mentionedSymbols = \case - TermVar{} -> - mempty - TermSymbol _loc symbol args -> - Set.insert symbol (Set.unions (mentionedSymbols <$> args)) - TermSymbolStruct _symbol expr -> - maybe mempty mentionedSymbols expr - Apply expr args -> - mentionedSymbols expr <> Set.unions (mentionedSymbols <$> toList args) - TermSep _x bound scope -> - mentionedSymbols bound <> mentionedSymbols (fromScope scope) - ReplacePred _y _x bound scope -> - mentionedSymbols bound <> mentionedSymbols (fromScope scope) - ReplaceFun bounds lhs cond -> - Set.unions (mentionedSymbols . snd <$> toList bounds) - <> mentionedSymbols (fromScope lhs) - <> mentionedSymbols (fromScope cond) - Connected _conn left right -> - mentionedSymbols left <> mentionedSymbols right - Lambda scope -> - mentionedSymbols (fromScope scope) - Quantified _quant scope -> - mentionedSymbols (fromScope scope) - PropositionalConstant{} -> - mempty - Not _loc expr -> - mentionedSymbols expr - -abstractVarSymbol :: VarSymbol -> ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol -abstractVarSymbol x = abstract (\y -> if x == y then Just x else Nothing) - -abstractVarSymbols :: Foldable t => t VarSymbol -> ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol -abstractVarSymbols xs = abstract (\y -> if y `elem` xs then Just y else Nothing) - - -forgetLocation :: forall a. ExprOf a -> ExprOf a -forgetLocation = \case - TermVar a -> - TermVar a - - TermSymbol _loc symb args -> - TermSymbol Nowhere symb (map forgetLocation args) - - TermSymbolStruct ss me -> - TermSymbolStruct ss (forgetLocation <$> me) - - Apply f args -> - Apply (forgetLocation f) (forgetLocation <$> args) - - TermSep v dom sc -> - TermSep v (forgetLocation dom) (hoistScope forgetLocation sc) - - ReplacePred v1 v2 dom sc -> - ReplacePred v1 v2 (forgetLocation dom) (hoistScope forgetLocation sc) - - ReplaceFun doms lhs rhs -> - ReplaceFun - (fmap (fmap forgetLocation) doms) - (hoistScope forgetLocation lhs) - (hoistScope forgetLocation rhs) - - Connected c e1 e2 -> - Connected c (forgetLocation e1) (forgetLocation e2) - - Lambda sc -> - Lambda (hoistScope forgetLocation sc) - - Quantified q sc -> - Quantified q (hoistScope forgetLocation sc) - - PropositionalConstant pc -> - PropositionalConstant pc - - Not _loc e -> - Not Nowhere (forgetLocation e) - - -equivalent :: Eq a => ExprOf a -> ExprOf a -> Bool -equivalent e1 e2 = forgetLocation e1 == forgetLocation e2 - --- | Use the given set of in scope structures to cast them to their carriers --- when occurring on the rhs of the element relation. --- Use the given 'Map' to annotate (unannotated) structure operations --- with the most recent inscope appropriate label. -annotateWith :: Set VarSymbol -> HashMap StructSymbol VarSymbol -> Formula -> Formula -annotateWith = go - where - go :: (Ord a) => Set a -> HashMap StructSymbol a -> ExprOf a -> ExprOf a - go labels ops = \case - TermSymbolStruct symb Nothing -> - -- TODO error if symbol is not instantiated, but only in theorems? - TermSymbolStruct symb (TermVar <$> HM.lookup symb ops) - TermSymbolStruct symb (Just e) -> - TermSymbolStruct symb (Just (go labels ops e)) - IsElementOf loc1 a (TermVar x) | x `Set.member` labels -> - IsElementOf loc1 (go labels ops a) (TermSymbolStruct CarrierSymbol (Just (TermVar x))) - Not loc a -> - Not loc (go labels ops a) - Connected conn a b -> - Connected conn (go labels ops a) (go labels ops b) - Quantified quant body -> - Quantified quant (toScope (go (Set.map F labels) (F <$> ops) (fromScope body))) - e@TermVar{} -> e - TermSymbol loc symb args -> - TermSymbol loc symb (go labels ops <$> args) - Apply e1 args -> - Apply (go labels ops e1) (go labels ops <$> args) - TermSep vs e scope -> - TermSep vs (go labels ops e) (toScope (go (Set.map F labels) (F <$> ops) (fromScope scope))) - ReplacePred y x xB scope -> - ReplacePred y x (go labels ops xB) (toScope (go (Set.map F labels) (F <$> ops) (fromScope scope))) - ReplaceFun bounds ap cond -> - ReplaceFun - (fmap (\(x, e) -> (x, go labels ops e)) bounds) - (toScope (go (Set.map F labels) (F <$> ops) (fromScope ap))) - (toScope (go (Set.map F labels) (F <$> ops) (fromScope cond))) - Lambda body -> - Lambda (toScope (go (Set.map F labels) (F <$> ops) (fromScope body))) - e@PropositionalConstant{} -> e - -containsHigherOrderConstructs :: ExprOf a -> Bool -containsHigherOrderConstructs = \case - TermSep {} -> True - ReplacePred{}-> True - ReplaceFun{}-> True - Lambda{} -> True - Apply{} -> False -- FIXME: this is a lie in general; we need to add sortchecking to determine this. - TermVar{} -> False - PropositionalConstant{} -> False - TermSymbol _loc _s es -> any containsHigherOrderConstructs es - Not _loc e -> containsHigherOrderConstructs e - Connected _ e1 e2 -> containsHigherOrderConstructs e1 || containsHigherOrderConstructs e2 - Quantified _ scope -> containsHigherOrderConstructs (fromScope scope) - TermSymbolStruct _ _ -> False - -pattern TermOp :: Location -> FunctionSymbol -> [ExprOf a] -> ExprOf a -pattern TermOp loc op es = TermSymbol loc (SymbolMixfix op) es - -pattern TermConst :: Location -> Token -> ExprOf a -pattern TermConst loc c <- TermOp loc (MixfixItem (TokenCons c End) _ NonAssoc) [] - where - TermConst loc c = - TermOp loc (MixfixItem (TokenCons c End) (markerFromToken c) NonAssoc) [] - -pattern TermPair :: Location -> ExprOf a -> ExprOf a -> ExprOf a -pattern TermPair loc e1 e2 = TermOp loc PairSymbol [e1, e2] - -pattern Atomic :: Location -> Predicate -> [ExprOf a] -> ExprOf a -pattern Atomic loc symbol args = TermSymbol loc (SymbolPredicate symbol) args - - -pattern FormulaAdj :: Location -> ExprOf a -> LexicalItem -> [ExprOf a] -> ExprOf a -pattern FormulaAdj loc e adj es = Atomic loc (PredicateAdj adj) (e:es) - -pattern FormulaVerb :: Location -> ExprOf a -> LexicalItemSgPl -> [ExprOf a] -> ExprOf a -pattern FormulaVerb loc e verb es = Atomic loc (PredicateVerb verb) (e:es) - -pattern FormulaNoun :: Location -> ExprOf a -> LexicalItemSgPl -> [ExprOf a] -> ExprOf a -pattern FormulaNoun loc e noun es = Atomic loc (PredicateNoun noun) (e:es) - -relationNoun :: Location -> Expr -> Formula -relationNoun loc arg = FormulaNoun loc arg (mkLexicalItemSgPl (unsafeReadPhraseSgPl "relation[/s]") "relation") [] - -rightUniqueAdj :: Location -> Expr -> Formula -rightUniqueAdj loc arg = FormulaAdj loc arg (mkLexicalItem (unsafeReadPhrase "right-unique") "rightunique") [] - --- | Untyped quantification. -pattern Forall, Exists :: Scope VarSymbol ExprOf a -> ExprOf a -pattern Forall scope = Quantified Universally scope -pattern Exists scope = Quantified Existentially scope - -makeForall, makeExists :: Foldable t => t VarSymbol -> Formula -> Formula -makeForall xs e = Quantified Universally (abstractVarSymbols xs e) -makeExists xs e = Quantified Existentially (abstractVarSymbols xs e) - -instantiateSome :: NonEmpty VarSymbol -> Scope VarSymbol ExprOf VarSymbol -> Scope VarSymbol ExprOf VarSymbol -instantiateSome xs scope = toScope (instantiateEither inst scope) - where - inst (Left x) | x `elem` xs = TermVar (F x) - inst (Left b) = TermVar (B b) - inst (Right fv) = TermVar (F fv) - --- | Bind all free variables not occuring in the given set universally -forallClosure :: Set VarSymbol -> Formula -> Formula -forallClosure xs phi = if isClosed phi - then phi - else Quantified Universally (abstract isNamedVar phi) - where - isNamedVar :: VarSymbol -> Maybe VarSymbol - isNamedVar x = if x `Set.member` xs then Nothing else Just x - -freeVars :: ExprOf VarSymbol -> Set VarSymbol -freeVars = Set.fromList . toList - -pattern And :: ExprOf a -> ExprOf a -> ExprOf a -pattern And e1 e2 = Connected Conjunction e1 e2 - -pattern Or :: ExprOf a -> ExprOf a -> ExprOf a -pattern Or e1 e2 = Connected Disjunction e1 e2 - -pattern Implies :: ExprOf a -> ExprOf a -> ExprOf a -pattern Implies e1 e2 = Connected Implication e1 e2 - -pattern Iff :: ExprOf a -> ExprOf a -> ExprOf a -pattern Iff e1 e2 = Connected Equivalence e1 e2 - -pattern Xor :: ExprOf a -> ExprOf a -> ExprOf a -pattern Xor e1 e2 = Connected ExclusiveOr e1 e2 - - -pattern Bottom :: ExprOf a -pattern Bottom = PropositionalConstant IsBottom - -pattern Top :: ExprOf a -pattern Top = PropositionalConstant IsTop - - -data RelationApplicationError - = RelationParameterArityMismatch - { relationApplicationLocation :: Location - , relationApplicationSymbol :: RelationSymbol - , relationApplicationExpectedParameters :: ParameterArity - , relationApplicationActualParameters :: ParameterArity - } - deriving (Show, Eq, Ord) - -checkRelationParameterArity - :: Foldable f - => Location - -> RelationSymbol - -> f a - -> Either RelationApplicationError () -checkRelationParameterArity loc relation parameters - | expected == actual = - Right () - | otherwise = - Left RelationParameterArityMismatch - { relationApplicationLocation = loc - , relationApplicationSymbol = relation - , relationApplicationExpectedParameters = expected - , relationApplicationActualParameters = actual - } - where - expected = relationSymbolParameterArity relation - actual = parameterArityOf parameters - -makeRelationApplication - :: Location - -> RelationSymbol - -> [ExprOf a] - -> Either - RelationApplicationError - (ExprOf a -> ExprOf a -> ExprOf a) -makeRelationApplication loc relation parameters = do - checkRelationParameterArity loc relation parameters - pure \left right -> - Atomic loc (PredicateRelation relation) (parameters <> [left, right]) - -pattern Relation :: Location -> RelationSymbol -> [ExprOf a] -> ExprOf a -pattern Relation loc rel es <- Atomic loc (PredicateRelation rel) es - --- | Membership. -pattern IsElementOf :: Location -> ExprOf a -> ExprOf a -> ExprOf a -pattern IsElementOf loc e1 e2 = - Atomic loc (PredicateRelation ElementSymbol) [e1, e2] - -isElementOf :: ExprOf a -> ExprOf a -> ExprOf a -isElementOf e1 e2 = - Atomic Nowhere (PredicateRelation ElementSymbol) [e1, e2] - --- | Membership. -isNotElementOf :: Location -> ExprOf a -> ExprOf a -> ExprOf a -isNotElementOf loc e1 e2 = Not loc (IsElementOf loc e1 e2) - --- | Subset relation (non-strict). -pattern IsSubsetOf :: Location -> ExprOf a -> ExprOf a -> ExprOf a -pattern IsSubsetOf loc e1 e2 = Atomic loc (PredicateRelation SubseteqSymbol) (e1 : [e2]) - -ordinalNoun :: LexicalItemSgPl -ordinalNoun = mkLexicalItemSgPl (unsafeReadPhraseSgPl "ordinal[/s]") "ordinal" - -isOrdinalNoun :: LexicalItemSgPl -> Bool -isOrdinalNoun noun = noun == ordinalNoun - --- | Ordinal predicate. -pattern IsOrd :: Location -> ExprOf a -> ExprOf a -pattern IsOrd loc e1 <- Atomic loc (PredicateNoun (isOrdinalNoun -> True)) [e1] - where - IsOrd loc e1 = Atomic loc (PredicateNoun ordinalNoun) [e1] - --- | Equality. -pattern Equals :: Location -> ExprOf a -> ExprOf a -> ExprOf a -pattern Equals loc e1 e2 = Atomic loc (PredicateRelation EqSymbol) (e1 : [e2]) - -equals :: ExprOf a -> ExprOf a -> ExprOf a -equals e1 e2 = Atomic Nowhere (PredicateRelation EqSymbol) (e1 : [e2]) - --- | Disequality. -pattern NotEquals :: Location -> ExprOf a -> ExprOf a -> ExprOf a -pattern NotEquals loc e1 e2 = Atomic loc (PredicateRelation NeqSymbol) (e1 : [e2]) - -pattern EmptySet :: Location -> ExprOf a -pattern EmptySet loc = - TermSymbol loc - (SymbolMixfix (MixfixItem (TokenCons (Command "emptyset") End) "emptyset" NonAssoc)) - [] - -makeConjunction :: [ExprOf a] -> ExprOf a -makeConjunction = \case - [] -> Top - es -> List.foldl1' And es - -makeDisjunction :: [ExprOf a] -> ExprOf a -makeDisjunction = \case - [] -> Bottom - es -> List.foldl1' Or es - -makeIff :: [ExprOf a] -> ExprOf a -makeIff = \case - [] -> Bottom - es -> List.foldl1' Iff es - -makeXor :: [ExprOf a] -> ExprOf a -makeXor = \case - [] -> Bottom - es -> List.foldl1' Xor es - --- | Source-ordered HOTG finite-set adjunction. --- --- This deliberately uses only fixed operations. In particular, finite-set --- notation is independent of the ordinary source-owned 'ConsSymbol'. -finiteSet :: Location -> NonEmpty (ExprOf a) -> ExprOf a -finiteSet location = foldr insert (EmptySet location) - where - insert element set = - TermSymbol location (SymbolMixfix UnionsSymbol) - [ TermSymbol location (SymbolMixfix UpairSymbol) - [ TermSymbol location (SymbolMixfix UpairSymbol) - [element, element] - , set - ] - ] - -isPositive :: ExprOf a -> Bool -isPositive = \case - Not _ _ -> False - _ -> True - -dual :: ExprOf a -> ExprOf a -dual = \case - Not _loc f -> f - f -> Not Nowhere f - - - --- | Local assumptions. -data Asm - = Asm Formula - | AsmStruct VarSymbol StructPhrase - - -deriving instance Show Asm -deriving instance Eq Asm -deriving instance Ord Asm - -data StructAsm - = StructAsm VarSymbol StructPhrase - - - -data Axiom = Axiom [Asm] Formula - -deriving instance Show Axiom -deriving instance Eq Axiom -deriving instance Ord Axiom - - -data Lemma = Lemma [Asm] Formula - -deriving instance Show Lemma -deriving instance Eq Lemma -deriving instance Ord Lemma - - -data Defn - = DefnPredicate [Asm] Predicate (NonEmpty VarSymbol) Formula - | DefnFun [Asm] LexicalItemSgPl [VarSymbol] Term - | DefnOp FunctionSymbol [VarSymbol] Term - -deriving instance Show Defn -deriving instance Eq Defn -deriving instance Ord Defn - -data Inductive = Inductive - { inductiveSymbol :: FunctionSymbol - , inductiveParams :: [VarSymbol] - , inductiveDomain :: Expr - , inductiveIntros :: NonEmpty IntroRule - } - deriving (Show, Eq, Ord) - -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) - -data CalcQuantifier - = CalcForall (NonEmpty VarSymbol) (Maybe Formula) - | CalcUnquantified - deriving (Show, Eq, Ord) - -data Proof - = Omitted Location - -- ^ Ends a proof without further verification. - -- This results in a “gap” in the formalization. - | Qed {mloc :: Maybe Location, by :: 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. - | ByContradiction Location Proof - -- ^ Take the dual of the current goal as an assumption and - -- set the goal to absurdity. - | BySetInduction Location (Maybe Term) Proof - -- ^ ∈-induction. - | ByOrdInduction Location Proof - -- ^ Transfinite induction for ordinals. - | Assume Location Formula Proof - -- ^ Simplify goals that are implications or disjunctions. - | Fix Location (NonEmpty VarSymbol) Formula Proof - -- ^ Simplify universal goals (with an optional bound or such that statement) - | Take Location (NonEmpty VarSymbol) Formula Justification Proof - -- ^ Use existential assumptions. - | Suffices Location Formula Justification Proof - | ByCase Location [Case] - -- ^ Proof by case. Disjunction of the case hypotheses 'Case' - -- must hold for this step to succeed. Each case starts a subproof, - -- keeping the same goal but adding the case hypothesis as an assumption. - -- Often this will be a classical split between /@P@/ and /@not P@/, in - -- which case the proof that /@P or not P@/ holds is easy. - -- - | Have Location Formula Justification Proof - -- ^ An affirmation, e.g.: /@We have \<stmt\> by \<ref\>@/. - -- - | Calc Location CalcQuantifier Calc Proof - | Subclaim Location Formula Proof Proof - -- ^ A claim is a sublemma with its own proof: - -- - -- /@Show \<goal stmt\>. \<steps\>. \<continue other proof\>.@/ - -- - -- A successful first proof adds the claimed formula as an assumption - -- for the remaining proof. - -- - | Define Location VarSymbol Term Proof - | DefineFunction Location VarSymbol VarSymbol Term Term Proof - - | DefineFunctionLocal Location VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof - -deriving instance Show Proof -deriving instance Eq Proof -deriving instance Ord Proof - - - --- | A case of a case split. -data Case = Case - { caseOf :: Formula - , caseProof :: Proof - } - -deriving instance Show Case -deriving instance Eq Case -deriving instance Ord Case - --- | See 'Syntax.Abstract.Calc'. -data Calc - = Equation Term (NonEmpty (Term, Justification)) - | Biconditionals Term (NonEmpty (Term, Justification)) - -deriving instance Show Calc -deriving instance Eq Calc -deriving instance Ord Calc - -calcQuant :: CalcQuantifier -> (Formula -> Formula) -calcQuant = \case - CalcUnquantified -> id - CalcForall xs maySuchThat -> case maySuchThat of - Nothing -> makeForall xs - Just suchThat -> \phi -> makeForall xs (suchThat `Implies` phi) - -calcResult :: CalcQuantifier -> Calc -> ExprOf VarSymbol -calcResult quant = \case - Equation e eqns -> calcQuant quant (Equals Nowhere e (fst (NonEmpty.last eqns))) - Biconditionals phi phis -> calcQuant quant (phi `Iff` fst (NonEmpty.last phis)) - -calculation :: CalcQuantifier -> Calc -> [(ExprOf VarSymbol, Justification)] -calculation quant = \case - Equation e1 eqns@((e2, jst) :| _) -> (calcQuant quant (Equals Nowhere e1 e2), jst) : collectEquations quant (toList eqns) - Biconditionals p1 ps@((p2, jst) :| _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant (toList ps) - - -collectEquations :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)] -collectEquations quant = \case - (e1, _) : eqns'@((e2, jst) : _) -> (calcQuant quant (Equals Nowhere e1 e2), jst) : collectEquations quant eqns' - _ -> [] - -collectBiconditionals :: CalcQuantifier -> [(Formula, j)] -> [(Formula, j)] -collectBiconditionals quant = \case - (p1, _) : ps@((p2, jst) : _) -> (calcQuant quant (p1 `Iff` p2), jst) : collectBiconditionals quant ps - _ -> [] - - -data Datatype - = Datatype - { datatypeHead :: SymbolPattern - , datatypeClauses :: NonEmpty DatatypeClause - } - deriving (Show, Eq, Ord) - -data DatatypeClause = DatatypeClause - { datatypeClauseConstructor :: SymbolPattern - , datatypeClausePremises :: [(VarSymbol, Expr)] - } - deriving (Show, Eq, Ord) - - -data Signature - = SignaturePredicate Predicate (NonEmpty VarSymbol) - | SignatureFormula Formula - -- TODO: This is a lossy encoding of a symbolic signature declaration. - -- The checker currently recovers the declared mixfix symbol heuristically - -- from the generated formula in order to assign ownership. Replace this - -- with a precise signature representation that carries the declared symbol - -- directly. - -deriving instance Show Signature -deriving instance Eq Signature -deriving instance Ord Signature - -data StructDefn = StructDefn - { structPhrase :: StructPhrase - -- ^ The noun phrase naming the structure, e.g.: @partial order@ or @abelian group@. - , structParents :: Set StructPhrase - , structDefnLabel :: VarSymbol - , structDefnFixes :: Set StructSymbol - -- ^ List of commands representing operations, - -- e.g.: @\\contained@ or @\\inv@. These are used as default operation names - -- in instantiations such as @Let $G$ be a group@. - -- The commands should be set up to handle an optional struct label - -- which would typically be rendered as a sub- or superscript, e.g.: - -- @\\contained[A]@ could render as ”⊑ᴬ“. - -- -- - , structDefnAssumes :: [(Marker, Formula)] - -- ^ The assumption or axioms of the structure. - -- To be instantiate with the @structFixes@ of a given structure. - } - -deriving instance Show StructDefn -deriving instance Eq StructDefn -deriving instance Ord StructDefn - - -data Abbreviation - = Abbreviation Symbol (Scope Int ExprOf Void) - deriving (Show, Eq, Ord) - -data Block - = BlockAxiom Location Marker Axiom - | BlockLemma Location Marker Lemma - | BlockProof Location Location Proof - | BlockDefn Location Marker Defn - | BlockAbbr Location Marker Abbreviation - | BlockStruct Location Marker StructDefn - | BlockInductive Location Marker Inductive - | BlockSig Location Marker [Asm] Signature - | BlockData Location Marker Datatype - deriving (Show, Eq, Ord) - - --- | Full boolean contraction. -contraction :: ExprOf a -> ExprOf a -contraction = \case - Connected conn f1 f2 -> atomicContraction (Connected conn (contraction f1) (contraction f2)) - Quantified quant scope -> atomicContraction (Quantified quant (hoistScope contraction scope)) - Not loc f -> Not loc (contraction f) - f -> f - - --- | Atomic boolean contraction. -atomicContraction :: ExprOf a -> ExprOf a -atomicContraction = \case - Top `Iff` f -> f - Bottom `Iff` f -> Not Nowhere f - f `Iff` Top -> f - f `Iff` Bottom -> Not Nowhere f - - Top `Implies` f -> f - Bottom `Implies` _ -> Top - _ `Implies` Top -> Top - f `Implies` Bottom -> Not Nowhere f - - Top `And` f -> f - Bottom `And` _ -> Bottom - f `And` Top -> f - _ `And` Bottom -> Bottom - - phi@(Quantified _quant scope) -> case unscope scope of - Top -> Top - Bottom -> Bottom - _ -> phi - - Not _ Top -> Bottom - Not _ Bottom -> Top - - f -> f diff --git a/source/Syntax/LexicalPhrase.hs b/source/Syntax/LexicalPhrase.hs deleted file mode 100644 index a0e0f19..0000000 --- a/source/Syntax/LexicalPhrase.hs +++ /dev/null @@ -1,95 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE NoImplicitPrelude #-} - -module Syntax.LexicalPhrase where - - -import Base -import Syntax.Token (Token(..)) - -import Control.DeepSeq (NFData) -import Data.Char (isAlpha) -import Data.Text qualified as Text -import Text.Earley.Mixfix (Holey) -import Text.Earley (Grammar, Prod, (<?>), fullParses, parser, rule, token, satisfy) - - - --- | 'LexicalPhrase's should be nonempty lists with at least one proper word token. --- Hyphens and quotes in words are treated as letters. --- Thus /@manifold-with-boundary@/ is a singleton lexical phrase (one word). --- -type LexicalPhrase = Holey Token - --- MAYBE Add this instance by making LexicalPhrase a proper Type? --- Until then we can use the default instance for lists of prettyprintable things. --- --- instance Pretty LexicalPhrase where --- pretty components = hsep (prettyComponent <$> components) --- where --- prettyComponent = \case --- Nothing -> "_" --- Just tok -> pretty tok - - - --- | Split data by grammatical number (singular/plural). --- The 'Eq' and 'Ord' instances only consider the singular --- form so that we can prefer known irregular plurals over --- guessed irregular plurals when inserting items into --- the 'Lexicon'. -data SgPl a - = SgPl {sg :: a, pl :: a} - deriving (Show, Functor, Generic, Hashable, NFData) - -instance Eq a => Eq (SgPl a) where (==) = (==) `on` sg -instance Ord a => Ord (SgPl a) where compare = compare `on` sg - - --- These readers parse only Felix-owned lexical literals. -unsafeReadPhrase :: String -> LexicalPhrase -unsafeReadPhrase spec = case fst (fullParses (parser lexicalPhraseSpec) spec) of - pat : _ -> pat - _ -> error "unsafeReadPhrase failed" - -unsafeReadPhraseSgPl :: String -> SgPl LexicalPhrase -unsafeReadPhraseSgPl spec = case fst (fullParses (parser lexicalPhraseSpecSgPl) spec) of - pat : _ -> pat - _ -> error "unsafeReadPhraseSgPl failed" - - -lexicalPhraseSpec :: Grammar r (Prod r String Char LexicalPhrase) -lexicalPhraseSpec = do - hole <- rule $ Nothing <$ token '?' <?> "hole" - word <- rule $ Just <$> many (satisfy (\c -> isAlpha c || c == '-')) - space <- rule $ Just . (:[]) <$> token ' ' - segment <- rule $ hole <|> word - rule $ (\s ss -> makePhrase (s:ss)) <$> segment <*> many (space *> segment) - where - makePhrase :: [Maybe String] -> LexicalPhrase - makePhrase pat = fmap makeWord pat - - -lexicalPhraseSpecSgPl :: Grammar r (Prod r String Char (SgPl LexicalPhrase)) -lexicalPhraseSpecSgPl = do - space <- rule $ Just . (:[]) <$> token ' ' - hole <- rule $ (Nothing, Nothing) <$ token '?'<?> "hole" - - word <- rule (many (satisfy isAlpha) <?> "word") - wordSgPl <- rule $ (,) <$> (token '[' *> word) <* token '/' <*> word <* token ']' - complexWord <- rule $ (\(a,b) -> (Just a, Just b)) . fuse <$> - many ((<>) <$> (dup <$> word) <*> wordSgPl) <?> "word" - segment <- rule (hole <|> (dup . Just <$> word) <|> complexWord ) - rule $ (\s ss -> makePhrase (s:ss)) <$> segment <*> many (space *> segment) - where - dup x = (x,x) - fuse = \case - (a, b) : (c, d) : rest -> fuse ((a <> c, b <> d) : rest) - [(a, b)] -> (a, b) - _ -> error "Syntax.Abstract.fuse" - - makePhrase :: [(Maybe String, Maybe String)] -> SgPl LexicalPhrase - makePhrase = (\(patSg, patPl) -> SgPl (fmap makeWord patSg) (fmap makeWord patPl)) . unzip - -makeWord :: Maybe String -> Maybe Token -makeWord = fmap (Word . Text.pack) diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs deleted file mode 100644 index 3e815c7..0000000 --- a/source/Syntax/Lexicon.hs +++ /dev/null @@ -1,330 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - --- | The 'Lexicon' describes the part of the grammar that extensible/dynamic. --- --- The items of the 'Lexicon' are organized by their meaning and their --- syntactic behaviour. They are typically represented as some kind of --- pattern data which is then used to generate various production rules --- for the concrete grammar. This representation makes inspection and --- extension easier. --- - -module Syntax.Lexicon - ( module Syntax.Lexicon - , pattern ConsSymbol - , pattern PairSymbol - , pattern UpairSymbol - , pattern UnionsSymbol - , pattern CarrierSymbol - , pattern ApplySymbol - , pattern DomSymbol - ) where - - -import Base -import Syntax.Abstract - -import Data.List qualified as List -import Data.Sequence qualified as Seq -import Data.Set qualified as Set -import Data.Map.Strict qualified as Map -import Data.Text qualified as Text -import Syntax.Mixfix (Holey) - - -data SignatureHeadForm - = AdjectiveSignatureHead - | SymbolicSignatureHead - deriving (Show, Eq, Ord) - --- Adjective heads must precede symbolic heads because both start with a math --- variable. -concreteSignatureHeadForms :: [SignatureHeadForm] -concreteSignatureHeadForms = - [ AdjectiveSignatureHead - , SymbolicSignatureHead - ] - -data Lexicon = Lexicon - { lexiconMixfixTable :: Seq (Map Pattern MixfixItem) - , lexiconConnectives :: [[(Holey Token, Associativity)]] - , lexiconPrefixPredicates :: [(PrefixPredicate, Marker)] - , lexiconStructFun :: [StructSymbol] - , lexiconRelationSymbols :: [RelationSymbol] - , lexiconVerbs :: [LexicalItemSgPl] - , lexiconAdjLs :: [LexicalItem] - , lexiconAdjRs :: [LexicalItem] - , lexiconNouns :: [LexicalItemSgPl] - , lexiconStructNouns :: [LexicalItemSgPl] - , lexiconFuns :: [LexicalItemSgPl] - } deriving (Show, Eq) - --- Projection returning the union of both left and right attributes. --- -lexiconAdjs :: Lexicon -> [LexicalItem] -lexiconAdjs lexicon = lexiconAdjLs lexicon <> lexiconAdjRs lexicon - - -builtins :: Lexicon -builtins = - Lexicon - { lexiconMixfixTable = builtinMixfixTable - , lexiconPrefixPredicates = builtinPrefixPredicates - , lexiconStructFun = builtinStructOps - , lexiconConnectives = builtinConnectives - , lexiconRelationSymbols = builtinRelationSymbols - , lexiconAdjLs = [] - , lexiconAdjRs = builtinAdjRs - , lexiconVerbs = builtinVerbs - , lexiconNouns = builtinNouns - , lexiconStructNouns = builtinStructNouns - , lexiconFuns = [] - } - -prefixPredicatePattern :: PrefixPredicate -> Pattern -prefixPredicatePattern (PrefixPredicate command _arity) = - TokenCons (Command command) End - -builtinMixfixTable :: Seq (Map Pattern MixfixItem) -builtinMixfixTable = Seq.fromList $ Map.fromList . fmap toEntry <$> builtinMixfixLevels - where - toEntry item@(MixfixItem pat _ _) = (pat, item) - --- INVARIANT: 10 precedence levels for now. -builtinMixfixLevels :: [[MixfixItem]] -builtinMixfixLevels = - [ [] - , [binOp (Symbol "+") LeftAssoc "add", binOp (Command "union") LeftAssoc "union", binOp (Symbol "-") LeftAssoc "minus", binOp (Command "rminus") LeftAssoc "rminus", binOp (Command "monus") LeftAssoc "monus"] - , [binOp (Command "relcomp") LeftAssoc "relcomp"] - , [binOp (Command "circ") LeftAssoc "circ"] - , [binOp (Command "mul") LeftAssoc "mul", binOp (Command "inter") LeftAssoc "inter", binOp (Command "rmul") LeftAssoc "rmul"] - , [binOp (Command "setminus") LeftAssoc "setminus"] - , [binOp (Command "times") RightAssoc "times"] - , [] - , prefixOps - , builtinIdentifiers - ] - where - builtinIdentifiers :: [MixfixItem] - builtinIdentifiers = identifier <$> - [ "emptyset" - , "naturals" - , "naturalsPlus" - , "integers" - , "rationals" - , "reals" - , "unit" - , "zero" - ] - - -prefixOps :: [MixfixItem] -prefixOps = - [ mkMixfixItem [Just (Command "rfrac"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "rfrac" NonAssoc - , mkMixfixItem [Just (Command "exp"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR, Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "exp" NonAssoc - , UnionsSymbol - , mkMixfixItem [Just (Command "cumul"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "cumul" NonAssoc - , mkMixfixItem [Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "fst" NonAssoc - , mkMixfixItem [Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "snd" NonAssoc - , mkMixfixItem [Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "pow" NonAssoc - , mkMixfixItem [Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "neg" NonAssoc - , mkMixfixItem [Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "inv" NonAssoc - , mkMixfixItem [Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "abs" NonAssoc - , ConsSymbol - , PairSymbol - , UpairSymbol - -- NOTE Is now defined and hence no longer necessary , ApplySymbol - ] - - -builtinStructOps :: [StructSymbol] -builtinStructOps = - [ CarrierSymbol - ] - -identifier :: Text -> MixfixItem -identifier cmd = mkMixfixItem [Just (Command cmd)] (Marker cmd) NonAssoc - - -builtinRelationSymbols :: [RelationSymbol] -builtinRelationSymbols = - [ RelationSymbol (Symbol "=") zeroParameterArity "eq" - , RelationSymbol (Command "rless") zeroParameterArity "rless" - , RelationSymbol (Command "neq") zeroParameterArity "neq" - , ElementSymbol - , NotElementSymbol -- Alternative to @\not\in@. - ] - -builtinPrefixPredicates :: [(PrefixPredicate, Marker)] -builtinPrefixPredicates = - [ (PrefixPredicate "Cong" 4, "cong") - , (PrefixPredicate "Betw" 3, "betw") - ] - - -builtinConnectives :: [[(Holey Token, Associativity)]] -builtinConnectives = - [ [binOp' (Command "iff") NonAssoc] - , [binOp' (Command "implies") RightAssoc] - , [binOp' (Command "lor") LeftAssoc] - , [binOp' (Command "land") LeftAssoc] - , [([Just (Command "lnot"), Nothing], NonAssoc)] - ] - - -binOp :: Token -> Associativity -> Marker -> MixfixItem -binOp tok assoc m = mkMixfixItem [Nothing, Just tok, Nothing] m assoc - -binOp' :: Token -> Associativity -> (Holey Token, Associativity) -binOp' tok assoc = ([Nothing, Just tok, Nothing], assoc) - -builtinAdjRs :: [LexicalItem] -builtinAdjRs = - [ builtinEqualityRightAdjective - ] - -builtinEqualityRightAdjective :: LexicalItem -builtinEqualityRightAdjective = - mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" - -builtinVerbs :: [LexicalItemSgPl] -builtinVerbs = - [ builtinEqualityVerb - ] - -builtinEqualityVerb :: LexicalItemSgPl -builtinEqualityVerb = - mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq" - - --- Some of these do/should correspond to mathlib structures, --- e.g.: lattice, complete lattice, ring, etc. --- -builtinNouns :: [LexicalItemSgPl] -builtinNouns = - [ builtinSetNoun - , mkLexicalItemSgPl (unsafeReadPhraseSgPl "point[/s]") "point" - , builtinElementNoun - ] - -builtinSetNoun :: LexicalItemSgPl -builtinSetNoun = - mkLexicalItemSgPl - (unsafeReadPhraseSgPl "set[/s]") - "set" - -builtinElementNoun :: LexicalItemSgPl -builtinElementNoun = - mkLexicalItemSgPl - (unsafeReadPhraseSgPl "element[/s] of ?") - "elem" - --- | Match the complete fixed-base identity, including the plural surface and --- authoritative marker. The ordinary 'Eq' instance intentionally compares --- only singular patterns. -isBuiltinSetNoun :: LexicalItemSgPl -> Bool -isBuiltinSetNoun item = - let actual = lexicalItemSgPlPattern item - expected = lexicalItemSgPlPattern builtinSetNoun - in sg actual == sg expected - && pl actual == pl expected - && lexicalItemSgPlMarker item - == lexicalItemSgPlMarker builtinSetNoun - -_Onesorted :: LexicalItemSgPl -_Onesorted = mkLexicalItemSgPl (unsafeReadPhraseSgPl "onesorted structure[/s]") "onesorted_structure" - -builtinStructNouns :: [LexicalItemSgPl] -builtinStructNouns = [_Onesorted] - - --- | Naïve splitting of lexical phrases to insert a variable slot for names in noun phrases, --- as in /@there exists a linear form $h$ on $E$@/, where the underlying pattern is --- /@linear form on ?@/. In this case we would get: --- --- > splitOnVariableSlot (sg (unsafeReadPhraseSgPl "linear form[/s] on ?")) --- > == --- > (unsafeReadPhrase "linear form", unsafeReadPhrase "on ?") --- -splitOnVariableSlot :: LexicalPhrase -> (LexicalPhrase, LexicalPhrase) -splitOnVariableSlot pat = case prepositionIndices <> nonhyphenatedSlotIndices of - [] -> (pat, []) -- Place variable slot at the end. - is -> List.splitAt (minimum is) pat - where - prepositionIndices, slotIndices, nonhyphenatedSlotIndices :: [Int] -- Ascending. - prepositionIndices = List.findIndices isPreposition pat - slotIndices = List.findIndices isNothing pat - nonhyphenatedSlotIndices = [i | i <- slotIndices, noHyphen (nth (i + 1) pat)] - - isPreposition :: Maybe Token -> Bool - isPreposition = \case - Just (Word w) -> w `Set.member` prepositions - _ -> False - - noHyphen :: Maybe (Maybe Token) -> Bool - noHyphen = \case - Just (Just (Word w)) -> Text.head w /= '-' - -- If we arrive here, either the pattern is over (`Nothing`) or the next - -- part of the pattern is not a word that starts with a hyphen. - _ -> True - - --- Preposition are a closed class, but this list is not yet exhaustive. --- It can and should be extended when needed. The following list is a --- selection of the prepositions found at --- https://en.wikipedia.org/wiki/List_of_English_prepositions. --- -prepositions :: Set Text -prepositions = Set.fromList - [ "about" - , "above" - , "across" - , "after" - , "against" - , "along", "alongside" - , "amid", "amidst" - , "among" - , "around" - , "as" - , "at" - , "atop" - , "before" - , "behind" - , "below" - , "beneath" - , "beside", "besides" - , "between" - , "beyond" - , "but" - , "by" - , "except" - , "for" - , "from" - , "in", "inside", "into" - , "like" - , "modulo", "mod" - , "near" - , "next" - , "of" - , "off" - , "on" - , "onto" - , "opposite" - , "out" - , "over" - , "past" - , "per" - , "sans" - , "till" - , "to" - , "under" - , "underneath" - , "unlike" - , "unto" - , "up", "upon" - , "versus" - , "via" - , "with" - , "within" - , "without" - ] diff --git a/source/Syntax/Mixfix.hs b/source/Syntax/Mixfix.hs deleted file mode 100644 index 6489d46..0000000 --- a/source/Syntax/Mixfix.hs +++ /dev/null @@ -1,139 +0,0 @@ -{-# LANGUAGE RecursiveDo #-} - -module Syntax.Mixfix where - -{- -Original code Copyright (c) 2014-2019, Olle Fredriksson - -All rights reserved. - -Redistribution and use in source and binary forms, with or without -modification, are permitted provided that the following conditions are met: - - * Redistributions of source code must retain the above copyright - notice, this list of conditions and the following disclaimer. - - * Redistributions in binary form must reproduce the above - copyright notice, this list of conditions and the following - disclaimer in the documentation and/or other materials provided - with the distribution. - - * Neither the name of Olle Fredriksson nor the names of other - contributors may be used to endorse or promote products derived - from this software without specific prior written permission. - -THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT -OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, -SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT -LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, -DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY -THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT -(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE -OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. --} - - -import Base -import Text.Earley -import Data.Either -import Syntax.Abstract - - -replicateA :: Applicative f => Int -> f a -> f [a] -replicateA n = sequenceA . replicate n - -consA :: Applicative f => f a -> f [a] -> f [a] -consA p q = (:) <$> p <*> q - - --- | An identifier with identifier parts ('Just's), and holes ('Nothing's) --- representing the positions of its arguments. --- --- Example (commonly written "if_then_else_"): --- @['Just' "if", 'Nothing', 'Just' "then", 'Nothing', 'Just' "else", 'Nothing'] :: 'Holey' 'String'@ -type Holey a = [Maybe a] - - --- | Create a grammar for parsing mixfix expressions. -mixfixExpression - :: [[(Holey (Prod r e t ident), Associativity)]] - -- ^ A table of holey identifier parsers, with associativity information. - -- The identifiers should be in groups of precedence levels listed from - -- binding the least to the most tightly. - -- - -- The associativity is taken into account when an identifier starts or ends - -- with holes, or both. Internal holes (e.g. after "if" in "if_then_else_") - -- start from the beginning of the table. - -- - -- Note that this rule also applies to identifiers with multiple consecutive - -- holes, e.g. "if__" --- the associativity then applies to both holes. - -> Prod r e t expr - -- ^ An atom, i.e. what is parsed at the lowest level. This will - -- commonly be a (non-mixfix) identifier or a parenthesised expression. - -> (Holey ident -> [expr] -> expr) - -- ^ How to combine the successful application of a holey identifier to its - -- arguments into an expression. - -> Grammar r (Prod r e t expr) -mixfixExpression table atom app = mixfixExpressionSeparate table' atom - where - table' = [[(holey, assoc, app) | (holey, assoc) <- row] | row <- table] - --- | A version of 'mixfixExpression' with a separate semantic action for each --- individual 'Holey' identifier. -mixfixExpressionSeparate - :: [[(Holey (Prod r e t ident), Associativity, Holey ident -> [expr] -> expr)]] - -- ^ A table of holey identifier parsers, with associativity information and - -- semantic actions. The identifiers should be in groups of precedence - -- levels listed from binding the least to the most tightly. - -- - -- The associativity is taken into account when an identifier starts or ends - -- with holes, or both. Internal holes (e.g. after "if" in "if_then_else_") - -- start from the beginning of the table. - -- - -- Note that this rule also applies to identifiers with multiple consecutive - -- holes, e.g. "if__" --- the associativity then applies to both holes. - -> Prod r e t expr - -- ^ An atom, i.e. what is parsed at the lowest level. This will - -- commonly be a (non-mixfix) identifier or a parenthesised expression. - -> Grammar r (Prod r e t expr) -mixfixExpressionSeparate table atom = mdo - expr <- foldrM ($) atom $ map (level expr) table - return expr - where - level expr idents next = mdo - same <- rule $ asum $ next : map (mixfixIdent same) idents - return same - where - -- Group consecutive holes and ident parts. - grp [] = [] - grp (Nothing:ps) = case grp ps of - Left n:rest -> (Left $! (n + 1)) : rest - rest -> Left 1 : rest - grp (Just p:ps) = case grp ps of - Right ps':rest -> Right (consA p ps') : rest - rest -> Right (consA p $ pure []) : rest - - mixfixIdent same (ps, a, f) = f' <$> go (grp ps) - where - f' xs = f (concatMap (either (map $ const Nothing) $ map Just) xs) - $ concat $ lefts xs - go ps' = case ps' of - [] -> pure [] - [Right p] -> pure . Right <$> p - Left n:rest -> consA - (Left <$> replicateA n (if a == RightAssoc then next - else same)) - $ go rest - [Right p, Left n] -> consA - (Right <$> p) - $ pure . Left <$> replicateA n (if a == LeftAssoc then next - else same) - Right p:Left n:rest -> consA (Right <$> p) - $ consA (Left <$> replicateA n expr) - $ go rest - Right _:Right _:_ -> error - $ "Earley.mixfixExpression: The impossible happened. " - ++ "Please report this as a bug." diff --git a/source/Syntax/Pragma.hs b/source/Syntax/Pragma.hs deleted file mode 100644 index 94c0d46..0000000 --- a/source/Syntax/Pragma.hs +++ /dev/null @@ -1,250 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - -module Syntax.Pragma - ( SourceMixfixLevel - , sourceMixfixLevelValue - , SyntaxPragma(..) - , SyntaxPragmaProblem(..) - , SyntaxPragmaError(..) - , renderSyntaxPragmaError - , extractSyntaxPragmas - ) where - -import Base - -import Report.Location -import Syntax.Abstract (Associativity(..)) - -import Control.DeepSeq (NFData) -import Control.Monad (unless, when) -import Data.Bifunctor (first) -import Data.Char (ord) -import Data.Text qualified as Text -import Data.Word (Word8) - - -newtype SourceMixfixLevel = SourceMixfixLevel Word8 - deriving stock (Show, Eq, Ord, Generic) - deriving anyclass (NFData) - -sourceMixfixLevelValue :: SourceMixfixLevel -> Word8 -sourceMixfixLevelValue (SourceMixfixLevel level) = - level - -data SyntaxPragma = LocatedFixityPragma - { syntaxPragmaLocation :: !Location - , syntaxPragmaAssociativity :: !Associativity - , syntaxPragmaLevel :: !SourceMixfixLevel - } deriving stock (Show, Eq) - -instance Locatable SyntaxPragma where - locate = syntaxPragmaLocation - -data SyntaxPragmaProblem - = SyntaxPragmaMissingSpaceAfterPrefix - | SyntaxPragmaMissingKeyword - | SyntaxPragmaUnknownKeyword !Text - | SyntaxPragmaMissingLevel - | SyntaxPragmaInvalidLevel - | SyntaxPragmaLevelOutOfRange - | SyntaxPragmaTrailingContent - | SyntaxPragmaLoneCarriageReturn - deriving stock (Show, Eq) - -data SyntaxPragmaError - = InvalidSyntaxPragma !Location !SyntaxPragmaProblem - | SyntaxPragmaLocationOutOfRange !FilePath !Int !Int - deriving stock (Show, Eq) - -renderSyntaxPragmaError :: SyntaxPragmaError -> Text -renderSyntaxPragmaError = \case - InvalidSyntaxPragma location problem -> - locationToText location - <> ": " - <> renderSyntaxPragmaProblem problem - SyntaxPragmaLocationOutOfRange file line column -> - Text.pack file - <> ": syntax pragma location is out of range at " - <> Text.pack (show line) - <> ":" - <> Text.pack (show column) - -renderSyntaxPragmaProblem :: SyntaxPragmaProblem -> Text -renderSyntaxPragmaProblem = \case - SyntaxPragmaMissingSpaceAfterPrefix -> - "expected horizontal space after %!" - SyntaxPragmaMissingKeyword -> - "missing syntax pragma keyword" - SyntaxPragmaUnknownKeyword keyword -> - "unknown syntax pragma keyword " <> Text.pack (show keyword) - SyntaxPragmaMissingLevel -> - "missing syntax pragma level" - SyntaxPragmaInvalidLevel -> - "syntax pragma level must use ASCII decimal digits" - SyntaxPragmaLevelOutOfRange -> - "syntax pragma level must be between 0 and 7" - SyntaxPragmaTrailingContent -> - "unexpected trailing syntax pragma content" - SyntaxPragmaLoneCarriageReturn -> - "a syntax pragma line must end with LF, CRLF, or end of file" - -extractSyntaxPragmas - :: FileId - -> FilePath - -> Text - -> Either SyntaxPragmaError [SyntaxPragma] -extractSyntaxPragmas fileId file = - go 1 - where - go lineNumber source - | Text.null source = - Right [] - | otherwise = do - let (rawLine, suffix) = - Text.break (== '\n') source - hasLineFeed = - not (Text.null suffix) - (line, lineEnding) = - if hasLineFeed && Text.isSuffixOf "\r" rawLine - then - (Text.dropEnd 1 rawLine, CrLf) - else if hasLineFeed - then - (rawLine, LineFeed) - else - (rawLine, EndOfFile) - remaining = - if hasLineFeed - then Text.drop 1 suffix - else "" - reserved = - Text.isPrefixOf "%!" - (Text.dropWhile isHorizontalSpace line) - pragma <- - if reserved - then Just <$> parsePragmaLine - fileId - file - lineNumber - lineEnding - line - else - Right Nothing - rest <- go (lineNumber + 1) remaining - pure (maybe rest (: rest) pragma) - -data LineEnding - = LineFeed - | CrLf - | EndOfFile - deriving stock (Show, Eq) - -parsePragmaLine - :: FileId - -> FilePath - -> Int - -> LineEnding - -> Text - -> Either SyntaxPragmaError SyntaxPragma -parsePragmaLine fileId file lineNumber lineEnding rawLine = do - let horizontalPrefix = - Text.takeWhile isHorizontalSpace rawLine - column = - Text.length horizontalPrefix + 1 - location <- - first - (const - (SyntaxPragmaLocationOutOfRange - file - lineNumber - column)) - (mkLocationChecked fileId lineNumber column) - let invalid - :: SyntaxPragmaProblem - -> Either SyntaxPragmaError a - invalid = - Left . InvalidSyntaxPragma location - afterPrefix = - Text.drop 2 - (Text.dropWhile isHorizontalSpace rawLine) - when - (lineEnding == EndOfFile - && Text.isSuffixOf "\r" rawLine) - (invalid SyntaxPragmaLoneCarriageReturn) - afterPrefixSpace <- - case Text.uncons afterPrefix of - Nothing -> - invalid SyntaxPragmaMissingKeyword - Just (char, _) - | not (isHorizontalSpace char) -> - invalid SyntaxPragmaMissingSpaceAfterPrefix - Just{} -> - Right (Text.dropWhile isHorizontalSpace afterPrefix) - when - (Text.null afterPrefixSpace) - (invalid SyntaxPragmaMissingKeyword) - let (keyword, afterKeyword) = - Text.break isHorizontalSpace afterPrefixSpace - associativity <- - case keyword of - "infixl" -> - Right LeftAssoc - "infixr" -> - Right RightAssoc - "infix" -> - Right NonAssoc - _ -> - invalid (SyntaxPragmaUnknownKeyword keyword) - afterKeywordSpace <- - case Text.uncons afterKeyword of - Nothing -> - invalid SyntaxPragmaMissingLevel - Just{} -> - Right (Text.dropWhile isHorizontalSpace afterKeyword) - when - (Text.null afterKeywordSpace) - (invalid SyntaxPragmaMissingLevel) - let (digits, trailing) = - Text.span isAsciiDigit afterKeywordSpace - when - (Text.null digits) - (invalid SyntaxPragmaInvalidLevel) - level <- - maybe - (invalid SyntaxPragmaLevelOutOfRange) - (Right . SourceMixfixLevel) - (sourceLevel digits) - unless - (Text.null (Text.dropWhile isHorizontalSpace trailing)) - (invalid SyntaxPragmaTrailingContent) - pure - LocatedFixityPragma - { syntaxPragmaLocation = location - , syntaxPragmaAssociativity = associativity - , syntaxPragmaLevel = level - } - -isHorizontalSpace :: Char -> Bool -isHorizontalSpace char = - char == ' ' || char == '\t' - -isAsciiDigit :: Char -> Bool -isAsciiDigit char = - '0' <= char && char <= '9' - -sourceLevel :: Text -> Maybe Word8 -sourceLevel = - Text.foldl' step (Just 0) - where - step Nothing _ = - Nothing - step (Just current) char = - let next = - current * 10 - + fromIntegral (ord char - ord '0') - in - if next <= 7 - then Just next - else Nothing diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs deleted file mode 100644 index b16379b..0000000 --- a/source/Syntax/Token.hs +++ /dev/null @@ -1,633 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | --- This module defines the lexer and its associated data types. --- The lexer takes `Text` as input and produces a stream of tokens --- annotated with positional information. This information is bundled --- together with the original raw input for producing error messages. --- --- The lexer perfoms some normalizations to make describing the grammar easier. --- Words outside of math environments are case-folded. Some commands are analysed --- as variable tokens and are equivalent to their respective unicode variants --- (α, β, γ, ..., 𝔸, 𝔹, ℂ, ...). Similarly, @\\begin{...}@ and @\\end{...}@ commands --- are each parsed as single tokens. --- -module Syntax.Token - ( Token(..) - , VariableDisplay(..) - , VariableSuffix(..) - , displayVariable - , renderVariableText - , tokToString - , tokToText - , TokStream(..) - , Located(..) - , runLexer - , gatherImports - ) where - - -import Base hiding (many) - -import Report.Location - -import Control.DeepSeq (NFData) -import Control.Monad.Combinators -import Control.Monad.State.Strict -import Data.List.NonEmpty qualified as NonEmpty -import Data.Text qualified as Text -import Prettyprinter (Pretty(..)) -import Text.Megaparsec hiding (Token, Label, label) -import Text.Megaparsec.Char qualified as Char -import Text.Megaparsec.Char.Lexer qualified as Lexer -import Tptp.UnsortedFirstOrder (isAsciiLetter, isAsciiAlphaNumOrUnderscore) - - -runLexer :: FileId -> String -> Text -> Either (ParseErrorBundle Text Void) ([FilePath], [[Located Token]]) -runLexer fileId file raw = runParser (evalStateT document (initLexerState fileId)) file raw - - -type Lexer = StateT LexerState (Parsec Void Text) - - -data LexerState = LexerState - { frames :: !(NonEmpty Frame) - , currentFileId :: !FileId - } deriving (Show, Eq) - -data Frame - = TopText - | MathFrame !Text - | TextFrame !Int - deriving (Show, Eq) - -initLexerState :: FileId -> LexerState -initLexerState fileId = LexerState (TopText :| []) fileId - -topFrameOf :: LexerState -> Frame -topFrameOf LexerState{frames = frame :| _} = frame - -topFrame :: Lexer Frame -topFrame = gets topFrameOf - -pushFrame :: Frame -> LexerState -> LexerState -pushFrame frame st@LexerState{frames = top :| rest} = - st{frames = frame :| (top : rest)} - -popFrame :: LexerState -> LexerState -popFrame st@LexerState{frames = _ :| []} = st -popFrame st@LexerState{frames = _ :| (top : rest)} = - st{frames = top :| rest} - -modifyTopFrame :: (Frame -> Frame) -> LexerState -> LexerState -modifyTopFrame f st@LexerState{frames = top :| rest} = - st{frames = f top :| rest} - --- Token recognizers only emit tokens; this is the single place that changes --- lexical context. -advance :: Token -> LexerState -> LexerState -advance tok st = - case (topFrameOf st, tok) of - (TopText, BeginEnv "math") -> - pushFrame (MathFrame "math") st - (TextFrame{}, BeginEnv "math") -> - pushFrame (MathFrame "math") st - (TopText, BeginEnv "align*") -> - pushFrame (MathFrame "align*") st - (TextFrame{}, BeginEnv "align*") -> - pushFrame (MathFrame "align*") st - (MathFrame env, EndEnv env') - | env == env' -> - popFrame st - (MathFrame{}, BeginEnv "text") -> - pushFrame (TextFrame 1) st - (TextFrame n, InvisibleBraceL) -> - modifyTopFrame (const (TextFrame (n + 1))) st - (TextFrame n, InvisibleBraceR) - | n > 1 -> - modifyTopFrame (const (TextFrame (n - 1))) st - (TextFrame 1, EndEnv "text") -> - popFrame st - _ -> - st - --- | --- A token stream as input stream for a parser. Contains the raw input --- before tokenization as 'Text' for showing error messages. --- -data TokStream = TokStream - { rawInput :: !Text - , unTokStream :: ![[Located Token]] - } deriving (Show, Eq) - -instance Semigroup TokStream where - TokStream raw1 toks1 <> TokStream raw2 toks2 = TokStream (raw1 <> raw2) (toks1 <> toks2) - -instance Monoid TokStream where - mempty = TokStream mempty mempty - --- | A LaTeX token. --- Invisible delimiters 'InvisibleBraceL' and 'InvisibleBraceR' are --- unescaped braces used for grouping in TEX (@{@), --- visibles braces are escaped braces (@\\{@). -data Token - = Word !Text - | Variable !Text - | Symbol !Text - | Integer !Int - | Command !Text - | Label Text -- ^ A /@\\label{...}@/ command (case-sensitive). - | Ref (NonEmpty Text) -- ^ A /@\\ref{...}@/ command (case-sensitive). - | BeginEnv !Text - | EndEnv !Text - | ParenL | ParenR - | BracketL | BracketR - | VisibleBraceL | VisibleBraceR - | InvisibleBraceL | InvisibleBraceR - deriving (Show, Eq, Ord, Generic, Hashable, NFData) - -instance IsString Token where - fromString w = Word (Text.pack w) - -data VariableDisplay = VariableDisplay - { variableBaseText :: !Text - , variableSuffix :: !(Maybe VariableSuffix) - } deriving (Show, Eq, Ord) - -data VariableSuffix - = VariableSubscript !Text - | VariableTicks !Int - deriving (Show, Eq, Ord) - -displayVariable :: Text -> VariableDisplay -displayVariable rawName = - case splitVariableBase rawName of - Nothing -> - VariableDisplay rawName Nothing - Just (baseText, suffixText) -> - VariableDisplay baseText (displayVariableSuffix suffixText) - -renderVariableText :: Text -> Text -renderVariableText rawName = - case displayVariable rawName of - VariableDisplay baseText Nothing -> - baseText - VariableDisplay baseText (Just (VariableTicks n)) -> - baseText <> Text.replicate n "'" - VariableDisplay baseText (Just (VariableSubscript subscriptText)) -> - baseText <> renderSubscriptText subscriptText - -splitVariableBase :: Text -> Maybe (Text, Text) -splitVariableBase rawName = - matchBlackboardBase rawName <|> matchGreekBase rawName <|> matchSingleLetterBase rawName - -matchBlackboardBase :: Text -> Maybe (Text, Text) -matchBlackboardBase rawName = do - suffixText <- Text.stripPrefix "bb" rawName - case Text.uncons suffixText of - Just (upper, rest) - | 'A' <= upper && upper <= 'Z' -> - Just ("bb" <> Text.singleton upper, rest) - _ -> - Nothing - -matchGreekBase :: Text -> Maybe (Text, Text) -matchGreekBase rawName = - asum - [ (\suffixText -> (rendered, suffixText)) <$> Text.stripPrefix prefix rawName - | (prefix, rendered) <- greekVariables - ] - -matchSingleLetterBase :: Text -> Maybe (Text, Text) -matchSingleLetterBase rawName = do - (baseChar, suffixText) <- Text.uncons rawName - pure (Text.singleton baseChar, suffixText) - -displayVariableSuffix :: Text -> Maybe VariableSuffix -displayVariableSuffix suffixText - | Text.null suffixText = - Nothing - | Text.all (== '_') suffixText = - Just (VariableTicks (Text.length suffixText)) - | otherwise = - Just (VariableSubscript (Text.replace "_" "'" suffixText)) - -renderSubscriptText :: Text -> Text -renderSubscriptText subscriptText - | Text.length subscriptText == 1 = - "_" <> subscriptText - | otherwise = - "_{" <> subscriptText <> "}" - -greekVariables :: [(Text, Text)] -greekVariables = - [ ("alpha", "α"), ("beta", "β"), ("gamma", "γ"), ("delta", "δ") - , ("epsilon", "ε"), ("zeta", "ζ"), ("eta", "η"), ("theta", "θ") - , ("iota", "ι"), ("kappa", "κ"), ("lambda", "λ"), ("mu", "μ") - , ("nu", "ν"), ("xi", "ξ"), ("pi", "π"), ("rho", "ρ"), ("sigma", "σ") - , ("tau", "τ"), ("upsilon", "υ"), ("phi", "φ"), ("chi", "χ") - , ("psi", "ψ"), ("omega", "ω") - , ("Gamma", "Γ"), ("Delta", "Δ"), ("Theta", "Θ"), ("Lambda", "Λ") - , ("Xi", "Ξ"), ("Pi", "Π"), ("Sigma", "Σ"), ("Upsilon", "Υ") - , ("Phi", "Φ"), ("Psi", "Ψ"), ("Omega", "Ω") - ] - -tokToText :: Token -> Text -tokToText = \case - Word w -> w - Variable v -> renderVariableText v - Symbol s -> s - Integer n -> Text.pack (show n) - Command cmd -> Text.cons '\\' cmd - Label m -> "\\label{" <> m <> "}" - Ref ms -> "\\ref{" <> Text.intercalate ", " (toList ms) <> "}" - BeginEnv "math" -> "$" - EndEnv "math" -> "$" - BeginEnv env -> "\\begin{" <> env <> "}" - EndEnv env -> "\\end{" <> env <> "}" - ParenL -> "(" - ParenR -> ")" - BracketL -> "[" - BracketR -> "]" - VisibleBraceL -> "\\{" - VisibleBraceR -> "\\}" - InvisibleBraceL -> "{" - InvisibleBraceR -> "}" - -tokToString :: Token -> String -tokToString = Text.unpack . tokToText - -instance Pretty Token where - pretty = \case - Word w -> pretty w - Variable v -> pretty (renderVariableText v) - Symbol s -> pretty s - Integer n -> pretty n - Command cmd -> "\\" <> pretty cmd - Label m -> "\\label{" <> pretty m <> "}" - Ref m -> "\\ref{" <> pretty m <> "}" - BeginEnv env -> "\\begin{" <> pretty env <> "}" - EndEnv env -> "\\end{" <> pretty env <> "}" - ParenL -> "(" - ParenR -> ")" - BracketL -> "[" - BracketR -> "]" - VisibleBraceL -> "\\{" - VisibleBraceR -> "\\}" - InvisibleBraceL -> "{" - InvisibleBraceR -> "}" - - -data Located a = Located - { startPos :: !Location - , unLocated :: !a - , postWhitespace :: Whitespace - } deriving (Show, Functor) - -data Whitespace = NoSpace | Space deriving (Show) - -collapseWhitespace :: [Whitespace] -> Whitespace -collapseWhitespace = \case - Space : _ -> Space - NoSpace : ws -> collapseWhitespace ws - [] -> NoSpace - -instance Eq a => Eq (Located a) where (==) = (==) `on` unLocated -instance Ord a => Ord (Located a) where compare = compare `on` unLocated - - -document :: Lexer ([FilePath], [[Located Token]]) -document = do - is <- importBlock - es <- many environment - eof - return (unLocated <$> is, es) - - -importBlock :: Lexer [Located FilePath] -importBlock = do - void (skipManyTill skipChar importLineOrBeginEnvOrEof) - many importLine - where - -- When skipping to the import block, we first need to try parsing whitespace to properly handle comments and avoid picking up a commented import line at the start of the import block. - skipChar, importLineOrBeginEnvOrEof :: Lexer () - skipChar = comment <|> void anySingle - importLineOrBeginEnvOrEof = - lookAhead - (void (Char.string "\\import{") - <|> void beginToplevelEnvironment) - <|> eof - - importLine :: Lexer (Located FilePath) = lexeme do - Char.string "\\import{" - path <- some (satisfy isTheoryNameChar) - Char.char '}' - pure path - - isTheoryNameChar :: Char -> Bool - isTheoryNameChar c = - c /= '}' && c /= '\n' && c /= '\r' && c /= '\0' - --- | Scan only the leading import block. Source-graph construction uses this --- authority-free pass before parsing modules under their composed syntax. -gatherImports - :: FileId - -> String - -> Text - -> Either (ParseErrorBundle Text Void) [Located FilePath] -gatherImports fileId file = - runParser (evalStateT importBlock (initLexerState fileId)) file - - -beginToplevelEnvironment :: Lexer (Located Text) -beginToplevelEnvironment = lexeme do - Char.string "\\begin{" - env :: Text <- asum (Char.string <$> ["definition", "theorem", "lemma", "axiom", "proof", "corollary", "proposition", "claim", "abbreviation", "datatype", "inductive", "signature", "struct"]) - Char.char '}' - pure env - --- | Parses tokens, switching tokenizing frames when encountering math and text environments. -environment :: Lexer [Located Token] -environment = do - env <- skipManyTill (comment <|> void anySingle) beginToplevelEnvironment - lts <- go (unLocated env) id - pure ((BeginEnv <$> env) : lts) - where - go env f = do - frame <- topFrame - r <- optional (nextTokenFor frame) - case r of - Nothing -> - pure (f []) - Just t@Located{unLocated = EndEnv env'} - | frame == TopText && env == env' -> - pure (f [t]) - Just t -> do - modify' (advance (unLocated t)) - go env (f . (t:)) -{-# INLINE environment #-} - -nextTokenFor :: Frame -> Lexer (Located Token) -nextTokenFor = \case - TopText -> normalToken - MathFrame{} -> mathToken - TextFrame n -> textToken n - --- | Parses a single normal-mode token. -normalToken :: Lexer (Located Token) -normalToken = - word <|> symbol <|> beginMath <|> beginAlign <|> subEnvironment <|> opening <|> closing <|> label <|> ref <|> end <|> command - --- | Parses a single math mode token. -mathToken :: Lexer (Located Token) -mathToken = - var <|> symbol <|> number <|> beginCases <|> endAlign <|> endCases <|> opening <|> closing <|> beginText <|> beginExplanation <|> endMath <|> command - -beginText :: Lexer (Located Token) -beginText = lexeme do - Char.string "\\text{" <|> Char.string "\\textbox{" - pure (BeginEnv "text") - --- | Same as text modulo spacing, so we treat it synonymously -beginExplanation :: Lexer (Located Token) -beginExplanation = lexeme do - Char.string "\\explanation{" - pure (BeginEnv "text") - -subEnvironment :: Lexer (Located Token) -subEnvironment = beginOrEnd ["enumerate", "subproof", "byCase"] - where - beginOrEnd envs = asum [beginEnv env <|> endEnv env | env <- envs] - beginEnv env = lexeme do - Char.string ("\\begin{" <> env <> "}") - pure (BeginEnv env) - endEnv env = lexeme do - Char.string ("\\end{" <> env <> "}") - pure (EndEnv env) - --- | Normal mode embedded into math mode via @\text{...}@. -textToken :: Int -> Lexer (Located Token) -textToken n = word <|> symbol <|> textEnd <|> beginMath <|> beginAlign <|> opening' <|> closing' <|> ref <|> command - where - textEnd = lexeme do - guard (n == 1) - Char.char '}' - pure (EndEnv "text") - - opening' = lexeme (group <|> optional (Char.string "\\left") *> (brace <|> paren <|> bracket)) - where - brace = VisibleBraceL <$ lexeme (Char.string "\\{") - group = InvisibleBraceL <$ lexeme (Char.char '{') - paren = ParenL <$ lexeme (Char.char '(') - bracket = BracketL <$ lexeme (Char.char '[') - - closing' = lexeme (group <|> optional (Char.string "\\right") *> (brace <|> paren <|> bracket)) - where - brace = VisibleBraceR <$ lexeme (Char.string "\\}") - group = InvisibleBraceR <$ lexeme (Char.char '}') - paren = ParenR <$ lexeme (Char.char ')') - bracket = BracketR <$ lexeme (Char.char ']') - - --- | Parses a single begin math token. -beginMath :: Lexer (Located Token) -beginMath = lexeme do - Char.string "\\(" <|> Char.string "\\[" <|> Char.string "$" - pure (BeginEnv "math") - -beginAlign :: Lexer (Located Token) -beginAlign = lexeme do - Char.string "\\begin{align*}" - pure (BeginEnv "align*") - -beginCases :: Lexer (Located Token) -beginCases = lexeme do - Char.string "\\begin{cases}" - pure (BeginEnv "cases") - --- | Parses a single end math token. -endMath :: Lexer (Located Token) -endMath = lexeme do - Char.string "\\)" <|> Char.string "\\]" <|> Char.string "$" - pure (EndEnv "math") - -endAlign :: Lexer (Located Token) -endAlign = lexeme do - Char.string "\\end{align*}" - pure (EndEnv "align*") - -endCases :: Lexer (Located Token) -endCases = lexeme do - Char.string "\\end{cases}" - pure (EndEnv "cases") - - --- | Parses the end of an environment. --- Commits only after having seen "\end{". -end :: Lexer (Located Token) -end = lexeme do - notFollowedBy (Char.string "\\end{cases}") - Char.string "\\end{" - env <- some (Char.letterChar <|> Char.char '*') - Char.char '}' - pure (EndEnv (Text.pack env)) - - - --- | Parses a word. Words are returned casefolded, since we want to ignore their case later on. -word :: Lexer (Located Token) -word = lexeme do - w <- some (Char.letterChar <|> Char.char '\'' <|> Char.char '-') - let t = Word (Text.toCaseFold (Text.pack w)) - pure t - -number :: Lexer (Located Token) -number = lexeme $ Integer <$> Lexer.decimal - - -var :: Lexer (Located Token) -var = lexeme (fmap Variable var') - where - var' = do - alphabeticPart <- letter <|> bb <|> greek - variationPart <- subscript <|> ticked <|> pure "" - pure (alphabeticPart <> variationPart) - - subscript :: Lexer Text - subscript = do - Char.char '_' - unbraced <|> braced <|> text - where - unbraced = Text.singleton <$> Char.alphaNumChar - braced = Text.pack <$> (Char.char '{' *> some (Char.alphaNumChar <|> tick) <* Char.char '}') - text = Char.string "\\text" *> braced -- for rendering the subscript in roman type - - -- A bit of a hack to fit the TPTP format. - tick :: Lexer Char - tick = '_' <$ Char.char '\'' - - ticked :: Lexer Text - ticked = do - ticks <- some tick - pure (Text.pack ticks) - - letter :: Lexer Text - letter = fmap Text.singleton Char.letterChar - - greek :: Lexer Text - greek = try do - Char.char '\\' - l <- symbolParser greeks - notFollowedBy Char.letterChar - pure l - - greeks :: [Text] - greeks = - [ "alpha", "beta", "gamma", "delta", "epsilon", "zeta", "eta", "theta" - , "iota", "kappa", "lambda", "mu", "nu", "xi", "pi", "rho", "sigma" - , "tau", "upsilon", "phi", "chi", "psi", "omega" - , "Gamma", "Delta", "Theta", "Lambda", "Xi", "Pi", "Sigma", "Upsilon" - , "Phi", "Psi", "Omega" - ] - - bb :: Lexer Text - bb = do - Char.string "\\mathbb{" - l <- symbolParser bbs - Char.char '}' - pure $ "bb" <> l - - bbs :: [Text] - bbs = Text.singleton <$> ['A'..'Z'] - - - symbolParser :: [Text] -> Lexer Text - symbolParser symbols = asum (fmap Char.string symbols) - - -symbol :: Lexer (Located Token) -symbol = lexeme do - symb <- some (satisfy (`elem` symbols)) - pure (Symbol (Text.pack symb)) - where - symbols :: [Char] - symbols = ".,:;!?@=≠+-/|^><≤≥*&≈⊂⊃⊆⊇∈“”‘’" - --- | Parses a TEX-style command. -command :: Lexer (Located Token) -command = lexeme do - Char.char '\\' - cmd <- some Char.letterChar - pure (Command (Text.pack cmd)) - --- | Parses a label command and extracts its marker. -label :: Lexer (Located Token) -label = lexeme do - Char.string "\\label{" - m <- marker - Char.char '}' - pure (Label m) - --- | Parses a label command and extracts its marker. -ref :: Lexer (Located Token) -ref = lexeme do - -- @\\cref@ is from @cleveref@ and @\\hyperref@ is from @hyperref@ - cmd <- Char.string "\\ref{" <|> Char.string "\\cref{" <|> Char.string "\\hyperref[" - ms <- NonEmpty.fromList <$> marker `sepBy1` Char.char ',' - case cmd of - "\\hyperref[" -> Char.string "]{" *> some (satisfy (/= '}')) *> Char.char '}' *> pure (Ref ms) - _ -> Char.char '}' *> pure (Ref ms) - -marker :: Lexer Text -marker = do - c <- satisfy isAsciiLetter - cs <- takeWhileP Nothing isAsciiAlphaNumOrUnderscore - pure (Text.cons c cs) - --- | Parses an opening delimiter. -opening :: Lexer (Located Token) -opening = lexeme (group <|> optional (Char.string "\\left") *> (paren <|> brace <|> bracket)) - where - brace = VisibleBraceL <$ lexeme (Char.string "\\{") - group = InvisibleBraceL <$ lexeme (Char.char '{') - paren = ParenL <$ lexeme (Char.char '(') - bracket = BracketL <$ lexeme (Char.char '[') - --- | Parses a closing delimiter. -closing :: Lexer (Located Token) -closing = lexeme (group <|> optional (Char.string "\\right") *> (paren <|> brace <|> bracket)) - where - brace = VisibleBraceR <$ lexeme (Char.string "\\}") - group = InvisibleBraceR <$ lexeme (Char.char '}') - paren = ParenR <$ lexeme (Char.char ')') - bracket = BracketR <$ lexeme (Char.char ']') - --- | Turns a Lexer into one that tracks the source position of the token --- and consumes trailing whitespace. -lexeme :: Lexer a -> Lexer (Located a) -lexeme p = do - fileId <- gets currentFileId - start <- getSourcePos - location <- - either - (fail . show) - pure - (fromSourcePosChecked fileId start) - t <- p - w <- whitespace - pure (Located location t w) - -space :: Lexer Whitespace -space = Space <$ (Char.char ' ' <|> Char.char '\n' <|> Char.char '\r') - <|> Space <$ (Char.string "\\ " <|> Char.string "\\\\" <|> Char.string "\\!" <|> Char.string "\\," <|> Char.string "\\:" <|> Char.string "\\;" <|> Char.string "\\;") - -whitespace :: Lexer Whitespace -whitespace = do - ws <- many (spaces <|> NoSpace <$ comment) - pure (collapseWhitespace ws) - where - spaces = collapseWhitespace <$> some space - -comment :: Lexer () -comment = Lexer.skipLineComment "%" |