diff options
Diffstat (limited to 'source/Syntax/Internal.hs')
| -rw-r--r-- | source/Syntax/Internal.hs | 23 |
1 files changed, 19 insertions, 4 deletions
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 |