diff options
Diffstat (limited to 'source/Syntax')
| -rw-r--r-- | source/Syntax/Abstract.hs | 15 | ||||
| -rw-r--r-- | source/Syntax/Concrete.hs | 1 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 23 | ||||
| -rw-r--r-- | source/Syntax/Lexicon.hs | 15 |
4 files changed, 45 insertions, 9 deletions
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index f589283..76ce6b6 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -168,7 +168,9 @@ pattern NeqSymbol = pattern SubseteqSymbol = RelationSymbol (Command "subseteq") (ParameterArity 0) "subseteq" --- | The predefined @cons@ function symbol used for desugaring finite set expressions. +-- | 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 @@ -220,6 +222,17 @@ pattern UpairSymbol = "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 = diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index a2eb2dc..62d1f92 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -382,7 +382,6 @@ grammar lexicon@Lexicon{..} = mdo defnFun <- rule $ DefnFun <$> asms <*> (optional _the *> funVar) <*> optional defnFunSymb <* _is <*> term <* _dot symbolicPatternEqTerm <- rule do - asms -- NB assumptions are currently ignored! pat <- beginMath *> symbolicPattern <* _eq e <- expr <* endMath <* _dot pure (pat, e) diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index d769afe..5a8cb65 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -15,7 +15,11 @@ module Syntax.Internal import Base -import Syntax.Lexicon (pattern PairSymbol, pattern ConsSymbol) +import Syntax.Lexicon + ( pattern PairSymbol + , pattern UnionsSymbol + , pattern UpairSymbol + ) import Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl) import Syntax.Token (Token(..)) import Report.Location @@ -536,10 +540,21 @@ makeXor = \case [] -> Bottom es -> List.foldl1' Xor es -finiteSet :: NonEmpty (ExprOf a) -> ExprOf a -finiteSet = foldr cons (EmptySet Nowhere) +-- | 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 - cons x y = TermSymbol Nowhere (SymbolMixfix ConsSymbol) [x, y] + insert element set = + TermSymbol location (SymbolMixfix UnionsSymbol) + [ TermSymbol location (SymbolMixfix UpairSymbol) + [ TermSymbol location (SymbolMixfix UpairSymbol) + [element, element] + , set + ] + ] isPositive :: ExprOf a -> Bool isPositive = \case diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 7ee44ae..3e815c7 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -14,6 +14,7 @@ module Syntax.Lexicon , pattern ConsSymbol , pattern PairSymbol , pattern UpairSymbol + , pattern UnionsSymbol , pattern CarrierSymbol , pattern ApplySymbol , pattern DomSymbol @@ -121,7 +122,7 @@ 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 - , mkMixfixItem [Just (Command "unions"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] "unions" 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 @@ -179,14 +180,22 @@ binOp' tok assoc = ([Nothing, Just tok, Nothing], assoc) builtinAdjRs :: [LexicalItem] builtinAdjRs = - [ mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" + [ builtinEqualityRightAdjective ] +builtinEqualityRightAdjective :: LexicalItem +builtinEqualityRightAdjective = + mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" + builtinVerbs :: [LexicalItemSgPl] builtinVerbs = - [ mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq" + [ 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. |