Migrate to `Felix` namespaceHEADhotg

1 files changed, 830 insertions, 0 deletions

diff --git a/source/Felix/Syntax/Internal.hs b/source/Felix/Syntax/Internal.hs
new file mode 100644
index 0000000..d129947
--- /dev/null
+++ b/source/Felix/Syntax/Internal.hs
@@ -0,0 +1,830 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DeriveTraversable #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- | Data types for the internal (semantic) syntax tree.
+module Felix.Syntax.Internal
+    ( module Felix.Syntax.Internal
+    , module Felix.Syntax.Abstract
+    , module Felix.Syntax.LexicalPhrase
+    , module Felix.Syntax.Token
+    ) where
+
+
+import Base
+import Felix.Syntax.Lexicon
+    ( pattern PairSymbol
+    , pattern UnionsSymbol
+    , pattern UpairSymbol
+    )
+import Felix.Syntax.LexicalPhrase (unsafeReadPhrase, unsafeReadPhraseSgPl)
+import Felix.Syntax.Token (Token(..))
+import Felix.Report.Location
+
+import Felix.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