diff options
Diffstat (limited to 'source/Meaning.hs')
| -rw-r--r-- | source/Meaning.hs | 740 |
1 files changed, 740 insertions, 0 deletions
diff --git a/source/Meaning.hs b/source/Meaning.hs new file mode 100644 index 0000000..d32e8ac --- /dev/null +++ b/source/Meaning.hs @@ -0,0 +1,740 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TupleSections #-} + + +module Meaning where + + +import Base +import Serial +import Syntax.Abstract (Sign(..)) +import Syntax.Abstract qualified as Raw +import Syntax.Internal (VarSymbol(..)) +import Syntax.Internal qualified as Sem +import Syntax.LexicalPhrase (unsafeReadPhrase) +import Syntax.Lexicon + + +import Bound +import Bound.Scope (abstractEither) +import Control.Monad.Except +import Control.Monad.State +import Data.List qualified as List +import Data.List.NonEmpty qualified as NonEmpty +import Data.Map qualified as Map +import Data.Set qualified as Set + + +-- | The 'Gloss' monad. Basic elaboration, desugaring, and validation +-- computations take place in this monad, using 'ExceptT' to log +-- validation errors and 'State' to keep track of the surrounding context. +type Gloss = ExceptT GlossError (State GlossState) +-- This monad previously used 'ValidationT' for validation so that multiple +-- validation errors could be reported. Using only 'ExceptT' we fail immediately +-- on the first error. If we ever swich back to 'ValidateT' for error reporting, +-- then we should re-enable {-# OPTIONS_GHC -foptimal-applicative-do #-}, +-- as 'ValidateT' can report more errors when used with applicative combinators. + +-- | Errors that can be detected during glossing. +data GlossError + = GlossDefnError DefnError String + | GlossInductionError + deriving (Show, Eq, Ord) + + +-- | Specialization of 'traverse' to 'Gloss'. +each :: (Traversable t) => (a -> Gloss b) -> t a -> Gloss (t b) +explain `each` as = traverse explain as +infix 7 `each` -- In particular, 'each' has precedence over '(<$>)'. + +-- | Wellformedness check for definitions. +-- The following conditions need to be met. +-- +-- * Variables occurring in the lexical phrases on the left side must be linear, +-- i.e. each variable can only occur once. +-- * The arguments of the lexical phrases must be variables, not complex terms. +-- This is statically guaranteed by the grammar. +-- * The optional typing noun may not have any free variables. +-- * The rhs side may not have any free variables not occurring on the lhs. +-- * If a variable on the lhs does not occur on the rhs, a warning should we issued. +-- +isWellformedDefn :: Sem.Defn -> Either DefnError Sem.Defn +isWellformedDefn defn = lhsLinear defn + + +lhsVars :: Sem.Defn -> [VarSymbol] +lhsVars = \case + Sem.DefnPredicate _ _ vs _ -> toList vs + Sem.DefnFun _ _ vs _ -> vs + Sem.DefnOp _ vs _ -> vs + +lhsLinear :: Sem.Defn -> Either DefnError Sem.Defn +lhsLinear defn' = let vs = lhsVars defn' in + if nubOrd vs /= vs + then Left DefnErrorLhsNotLinear + else Right defn' + + +-- | Validation errors for top-level definitions. +data DefnError + = DefnWarnLhsFree + | DefnErrorLhsNotLinear + | DefnErrorLhsTypeFree + | DefnErrorRhsFree + deriving (Show, Eq, Ord) + + +-- | Context for 'Gloss' computations. +data GlossState = GlossState + { varCount :: Int + -- ^ Counter for generating variables names for the output. + , lemmaCount :: Serial + -- ^ Counter for generating names for unlabelled lemmas. + , lexicon :: Lexicon + , pretypings :: Map VarSymbol Sem.Formula + -- ^ Keeps track of variable constraints. We lookup and insert constraints + -- when quantifying. Each variable maps to a predicate that the variables + -- must (implicitly) satisfy. Multiple constraints are represented as + -- a conjunction. + -- CONDITION: For convenience the keys are 'VarSymbol's, but variable constraints + -- should not be used for 'FreshVar's. + } deriving (Show, Eq) + + +freshLemmaId :: Gloss Serial +freshLemmaId = do + i <- gets lemmaCount + modify $ \s -> s {lemmaCount = Serial.next (lemmaCount s)} + pure i + +freshVar :: Gloss VarSymbol +freshVar = do + i <- gets varCount + modify $ \s -> s {varCount = varCount s + 1} + pure $ FreshVar i + + +meaning :: [Raw.Block] -> Either GlossError [Sem.Block] +meaning a = evalState (runExceptT (glossBlocks a)) initialGlossState + where + initialGlossState = GlossState + { varCount = 0 + , lemmaCount = Serial.start + , lexicon = builtins + , pretypings = mempty + } + +glossExpr :: Raw.Expr -> Gloss (Sem.ExprOf VarSymbol) +glossExpr = \case + Raw.ExprVar v -> + pure $ Sem.TermVar v + Raw.ExprInteger n -> + pure $ Sem.TermSymbol (Sem.SymbolInteger n) [] + Raw.ExprOp f es -> + Sem.TermSymbol <$> pure (Sem.SymbolMixfix f) <*> (glossExpr `each` es) + Raw.ExprStructOp tok maybeLabel -> do + maybeLabel' <- traverse glossExpr maybeLabel + pure $ Sem.TermSymbolStruct tok maybeLabel' + Raw.ExprSep x t phi -> do + t' <- glossExpr t + phi' <- glossStmt phi + pure (Sem.TermSep x t' (abstract1 x phi')) + Raw.ExprReplacePred y x xBound stmt -> do + xBound' <- glossExpr xBound + stmt' <- glossStmt stmt + let toReplacementVar z = if + | z == x -> Just Sem.ReplacementDomVar + | z == y -> Just Sem.ReplacementRangeVar + | otherwise -> Nothing + let scope = abstract toReplacementVar stmt' + pure (Sem.ReplacePred y x xBound' scope) + Raw.ExprReplace e bounds phi -> do + e' <- glossExpr e + bounds' <- glossReplaceBound `each` bounds + let xs = fst <$> bounds' + phi'' <- case phi of + Just phi' -> glossStmt phi' + Nothing -> pure Sem.Top + let abstractBoundVars = abstract (\x -> List.find (== x) (toList xs)) + pure $ Sem.ReplaceFun bounds' (abstractBoundVars e') (abstractBoundVars phi'') + where + glossReplaceBound :: (VarSymbol, Raw.Expr) -> Gloss (VarSymbol, Sem.Term) + glossReplaceBound (x, b) = (x,) <$> glossExpr b + Raw.ExprFiniteSet es -> + Sem.finiteSet <$> glossExpr `each` es + + +glossFormula :: Raw.Formula -> Gloss (Sem.ExprOf VarSymbol) +glossFormula = \case + Raw.FormulaChain ch -> + glossChain ch + Raw.Connected conn phi psi -> + glossConnective conn <*> glossFormula phi <*> glossFormula psi + Raw.FormulaNeg f -> + Sem.Not <$> glossFormula f + Raw.FormulaPredicate predi es -> + Sem.Atomic <$> glossPrefixPredicate predi <*> glossExpr `each` toList es + Raw.PropositionalConstant c -> + pure $ Sem.PropositionalConstant c + Raw.FormulaQuantified quantifier xs bound phi -> do + bound' <- glossBound bound + phi' <- glossFormula phi + quantify <- glossQuantifier quantifier + pure (quantify xs (bound' (toList xs)) phi') + +glossChain :: Sem.Chain -> Gloss (Sem.ExprOf VarSymbol) +glossChain ch = Sem.makeConjunction <$> makeRels (conjuncts (splat ch)) + where + -- | Separate each link of the chain into separate triples. + splat :: Raw.Chain -> [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)] + splat = \case + Raw.ChainBase es sign rel es' + -> [(es, sign, rel, es')] + Raw.ChainCons es sign rel ch'@(Raw.ChainBase es' _ _ _) + -> (es, sign, rel, es') : splat ch' + Raw.ChainCons es sign rel ch'@(Raw.ChainCons es' _ _ _) + -> (es, sign, rel, es') : splat ch' + + -- | Take each triple and combine the lhs/rhs to make all the conjuncts. + conjuncts :: [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)] -> [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)] + conjuncts triples = do + (e1s, sign, rel, e2s) <- triples + e1 <- toList e1s + e2 <- toList e2s + pure (sign, rel, e1, e2) + + makeRels :: [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)] -> Gloss [Sem.Formula] + makeRels triples = for triples makeRel + + makeRel :: (Sign, Raw.Relation, Raw.Expr, Raw.Expr) -> Gloss Sem.Formula + makeRel (sign, rel, e1, e2) = do + e1' <- glossExpr e1 + e2' <- glossExpr e2 + case rel of + Raw.RelationSymbol tok -> + pure $ sign' $ Sem.Relation tok (e1' : [e2']) + Raw.RelationExpr e -> do + e' <- glossExpr e + pure $ sign' $ Sem.TermPair e1' e2' `Sem.IsElementOf` e' + where + sign' = case sign of + Positive -> id + Negative -> Sem.Not + + +glossPrefixPredicate :: Raw.PrefixPredicate -> Gloss Sem.Predicate +glossPrefixPredicate (Raw.PrefixPredicate symb _ar) = pure (Sem.PredicateSymbol symb) + + +glossNPNonEmpty :: Raw.NounPhrase NonEmpty -> Gloss (NonEmpty VarSymbol, Sem.Formula) +glossNPNonEmpty (Raw.NounPhrase leftAdjs noun vars rightAdjs maySuchThat) = do + -- We interpret the noun as a predicate. + noun' <- glossNoun noun + -- Now we turn the noun and all its modifiers into statements. + let typings = (\v' -> noun' (Sem.TermVar v')) <$> vars + leftAdjs' <- forEach (toList vars) <$> glossAdjL `each` leftAdjs + rightAdjs' <- forEach (toList vars) <$> glossAdjR `each` rightAdjs + suchThat <- maybeToList <$> glossStmt `each` maySuchThat + let constraints = toList typings <> leftAdjs' <> rightAdjs' <> suchThat + pure (vars, Sem.makeConjunction constraints) + + +-- | If needed, we introduce a fresh variable to reduce this to the case @NounPhrase NonEmpty@. +glossNPList :: Raw.NounPhrase [] -> Gloss (NonEmpty VarSymbol, Sem.Formula) +glossNPList (Raw.NounPhrase leftAdjs noun vars rightAdjs maySuchThat) = do + vars' <- case vars of + [] -> (:| []) <$> freshVar + v:vs -> pure (v :| vs) + glossNPNonEmpty $ Raw.NounPhrase leftAdjs noun vars' rightAdjs maySuchThat + +-- Returns a predicate for a term (the constraints) and the optional such-that clause. +-- We treat suchThat separately since multiple terms can share the same such-that clause. +glossNPMaybe :: Raw.NounPhrase Maybe -> Gloss (Sem.Term -> Sem.Formula, Maybe Sem.Formula) +glossNPMaybe (Raw.NounPhrase leftAdjs noun mayVar rightAdjs maySuchThat) = do + case mayVar of + Nothing -> do + glossNP leftAdjs noun rightAdjs maySuchThat + Just v' -> do + -- Next we desugar all the modifiers into statements. + leftAdjs' <- apply v' <$> glossAdjL `each` leftAdjs + rightAdjs' <- apply v' <$> glossAdjR `each` rightAdjs + maySuchThat' <- glossStmt `each` maySuchThat + let constraints = leftAdjs' <> rightAdjs' + -- Finally we translate the noun itself. + noun' <- glossNoun noun + pure case constraints of + [] -> (\t -> noun' t, maySuchThat') + _ -> (\t -> noun' t `Sem.And` Sem.makeConjunction (eq t v' : constraints), maySuchThat') + where + eq t v = t `Sem.Equals` Sem.TermVar v + apply :: VarSymbol -> [Sem.Term -> Sem.Formula] -> [Sem.Formula] + apply v stmts = [stmt (Sem.TermVar v) | stmt <- stmts] + +-- | Gloss a noun without a variable name. +-- Returns a predicate for a term (the constraints) and the optional such-that clause. +-- We treat suchThat separately since multiple terms can share the same such-that clause. +glossNP :: [Raw.AdjL] -> Raw.Noun -> [Raw.AdjR] -> Maybe Raw.Stmt -> Gloss (Sem.Term -> Sem.ExprOf VarSymbol, Maybe Sem.Formula) +glossNP leftAdjs noun rightAdjs maySuchThat = do + noun' <- glossNoun noun + leftAdjs' <- glossAdjL `each` leftAdjs + rightAdjs' <- glossAdjR `each` rightAdjs + maySuchThat' <- glossStmt `each` maySuchThat + let constraints = [noun'] <> leftAdjs' <> rightAdjs' + pure (\t -> Sem.makeConjunction (flap constraints t), maySuchThat') + + +-- | If we have a plural noun with multiple variables, then we need to desugar +-- adjectives to apply to each individual variable. +forEach :: Applicative t => t VarSymbol -> t (Sem.Term -> a) -> t a +forEach vs'' stmts = do + v <- vs'' + stmt <- stmts + pure $ stmt (Sem.TermVar v) + + +glossAdjL :: Raw.AdjL -> Gloss (Sem.Term -> Sem.Formula) +glossAdjL (Raw.AdjL pat es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \t -> quantify $ Sem.FormulaAdj t pat es' + + +-- | Since we need to be able to remove negation in verb phrases, +-- we need to have 'Sem.Stmt' as the target. We do not yet have +-- the term representing the subject, hence the parameter 'Sem.Expr'. +glossAdjR :: Raw.AdjR -> Gloss (Sem.Term -> Sem.Formula) +glossAdjR = \case + Raw.AdjR pat [e] | pat == unsafeReadPhrase "equal to ?" -> do + (e', quantify) <- glossTerm e + pure $ \t -> quantify $ Sem.Equals t e' + Raw.AdjR pat es -> do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \t -> quantify $ Sem.FormulaAdj t pat es' + Raw.AttrRThat vp -> glossVP vp + + +glossAdj :: Raw.AdjOf Raw.Term -> Gloss (Sem.ExprOf VarSymbol -> Sem.Formula) +glossAdj adj = case adj of + Raw.Adj pat [e] | pat == unsafeReadPhrase "equal to ?" -> do + (e', quantify) <- glossTerm e + pure $ \t -> quantify $ Sem.Equals t e' + Raw.Adj pat es -> do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \t -> quantify $ Sem.FormulaAdj t pat es' + +glossVP :: Raw.VerbPhrase -> Gloss (Sem.Term -> Sem.Formula) +glossVP = \case + Raw.VPVerb verb -> glossVerb verb + Raw.VPAdj adjs -> do + mkAdjs <- glossAdj `each` toList adjs + pure (\x -> Sem.makeConjunction [mkAdj x | mkAdj <- mkAdjs]) + Raw.VPVerbNot verb -> (Sem.Not .) <$> glossVerb verb + Raw.VPAdjNot adjs -> (Sem.Not .) <$> glossVP (Raw.VPAdj adjs) + + +glossVerb :: Raw.Verb -> Gloss (Sem.Term -> Sem.Formula) +glossVerb (Raw.Verb pat es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \ t -> quantify $ Sem.FormulaVerb t pat es' + + +glossNoun :: Raw.Noun -> Gloss (Sem.Term -> Sem.Formula) +glossNoun (Raw.Noun pat es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure case Sem.sg pat of + -- Everything is a set + [Just (Sem.Word "set")] -> const Sem.Top + _ -> \e' -> quantify (Sem.FormulaNoun e' pat es') + + +glossFun :: Raw.Fun -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula) +glossFun (Raw.Fun phrase es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure (Sem.TermSymbol (Sem.SymbolFun phrase) es', quantify) + + +glossTerm :: Raw.Term -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula) +glossTerm = \case + Raw.TermExpr e -> + (, id) <$> glossExpr e + Raw.TermFun f -> + glossFun f + Raw.TermIota x stmt -> do + stmt' <- glossStmt stmt + pure (Sem.Iota x (abstract1 x stmt'), id) + Raw.TermQuantified quantifier np -> do + quantify <- glossQuantifier quantifier + (mkConstraint, maySuchThat) <- glossNPMaybe np + v <- freshVar + let e = Sem.TermVar v + let constraints = [mkConstraint e] + pure (e, quantify (v:|[]) (maybeToList maySuchThat <> constraints)) + + + +glossStmt :: Raw.Stmt -> Gloss Sem.Formula +glossStmt = \case + Raw.StmtFormula f -> glossFormula f + Raw.StmtNeg s -> Sem.Not <$> glossStmt s + Raw.StmtVerbPhrase ts vp -> do + (ts', quantifies) <- NonEmpty.unzip <$> glossTerm `each` ts + vp' <- glossVP vp + let phi = Sem.makeConjunction (vp' <$> toList ts') + pure (compose quantifies phi) + Raw.StmtNoun t np -> do + (t', quantify) <- glossTerm t + (np', maySuchThat) <- glossNPMaybe np + let andSuchThat phi = case maySuchThat of + Just suchThat -> phi `Sem.And` suchThat + Nothing -> phi + pure (quantify (andSuchThat (np' t'))) + Raw.StmtStruct t sp -> do + (t', quantify) <- glossTerm t + pure (quantify (Sem.TermSymbol (Sem.SymbolPredicate (Sem.PredicateNounStruct sp)) [t'])) + Raw.StmtConnected conn s1 s2 -> glossConnective conn <*> glossStmt s1 <*> glossStmt s2 + Raw.StmtQuantPhrase (Raw.QuantPhrase quantifier np) f -> do + (vars, constraints) <- glossNPList np + f' <- glossStmt f + quantify <- glossQuantifier quantifier + pure (quantify vars [constraints] f') + Raw.StmtExists np -> do + (vars, constraints) <- glossNPList np + pure (Sem.makeExists vars constraints) + Raw.SymbolicQuantified quant vs bound suchThat have -> do + quantify <- glossQuantifier quant + bound' <- glossBound bound + suchThatConstraints <- maybeToList <$> glossStmt `each` suchThat + let boundConstraints = bound' (toList vs) + have' <- glossStmt have + pure (quantify vs (boundConstraints <> suchThatConstraints) have') + +-- | A bound applies to all listed variables. Note the use of '<**>'. +-- +-- >>> ([1, 2, 3] <**> [(+ 10)]) == [11, 12, 13] +-- +glossBound :: Raw.Bound -> Gloss ([VarSymbol] -> [Sem.Formula]) +glossBound = \case + Raw.Unbounded -> pure (const []) + Raw.Bounded sign rel term -> do + term' <- glossExpr term + let sign' = case sign of + Positive -> id + Negative -> Sem.Not + bound <- case rel of + Raw.RelationSymbol rel' -> + pure $ \v -> sign' $ + Sem.Relation rel' (Sem.TermVar v : [term']) + Raw.RelationExpr e -> do + e' <- glossExpr e + pure $ \v -> sign' $ + Sem.TermPair (Sem.TermVar v) term' `Sem.IsElementOf` e' + pure \vs -> vs <**> [bound] + + +gatherGuards :: Traversable t => t VarSymbol -> Gloss (Maybe (t Sem.Formula)) +gatherGuards vs = do + info <- gets pretypings + pure $ for vs $ \v -> Map.lookup v info + + +glossConnective :: Raw.Connective -> Gloss (Sem.Formula -> Sem.Formula -> Sem.Formula) +glossConnective conn = pure (Sem.Connected conn) + + +glossAsm :: Raw.Asm -> Gloss [Sem.Asm] +glossAsm = \case + Raw.AsmSuppose s -> do + s' <- glossStmt s + pure [Sem.Asm s'] + Raw.AsmLetNoun vs np -> do + (np', maySuchThat) <- glossNPMaybe np + let f v = Sem.Asm (np' (Sem.TermVar v) ) + let suchThat = Sem.Asm <$> maybeToList maySuchThat + pure (suchThat <> fmap f (toList vs)) + Raw.AsmLetIn vs e -> do + e' <- glossExpr e + let f v = Sem.Asm (Sem.TermVar v `Sem.IsElementOf` e') + pure $ fmap f (toList vs) + Raw.AsmLetStruct structLabel structPhrase -> + pure [Sem.AsmStruct structLabel structPhrase] + Raw.AsmLetThe _ _ -> + _TODO "glossAsm AsmLetThe" + Raw.AsmLetEq _ _ -> + _TODO "glossAsm AsmLetEq" + + +-- | A quantifier is interpreted as a quantification function that takes a nonempty list of variables, +-- a list of formulas expressing the constraints, and the formula to be quantified as arguments. +-- It then returns the quantification with the correct connective for the constraints. +glossQuantifier + :: (Foldable t, Applicative f) + => Raw.Quantifier + -> f (t VarSymbol + -> [Sem.ExprOf VarSymbol] + -> Sem.Formula + -> Sem.Formula) +glossQuantifier quantifier = pure quantify + where + quantify vs constraints f = case (quantifier, constraints) of + (Raw.Universally, []) -> + Sem.makeForall vs f + (Raw.Existentially, []) -> + Sem.makeExists vs f + (Raw.Nonexistentially, []) -> + Sem.Not (Sem.makeExists vs f) + (Raw.Universally, _) -> + Sem.makeForall vs (Sem.makeConjunction constraints `Sem.Implies` f) + (Raw.Existentially, _) -> + Sem.makeExists vs (Sem.makeConjunction constraints `Sem.And` f) + (Raw.Nonexistentially, _) -> + Sem.Not (Sem.makeExists vs (Sem.makeConjunction constraints `Sem.And` f)) + + +glossAsms :: [Raw.Asm] -> Gloss [Sem.Asm] +glossAsms asms = do + asms' <- glossAsm `each` asms + pure $ concat asms' + + +glossAxiom :: Raw.Axiom -> Gloss Sem.Axiom +glossAxiom (Raw.Axiom asms f) = Sem.Axiom <$> glossAsms asms <*> glossStmt f + + +glossLemma :: Raw.Lemma -> Gloss Sem.Lemma +glossLemma (Raw.Lemma asms f) = Sem.Lemma <$> glossAsms asms <*> glossStmt f + + +glossDefn :: Raw.Defn -> Gloss Sem.Defn +glossDefn = \case + Raw.Defn asms h f -> glossDefnHead h <*> glossAsms asms <*> glossStmt f + Raw.DefnFun asms (Raw.Fun fun vs) _ e -> do + asms' <- glossAsms asms + e' <- case e of + -- TODO improve error handling or make grammar stricter + Raw.TermQuantified _ _ -> error $ "Quantified term in definition: " <> show e + _ -> fst <$> glossTerm e + pure $ Sem.DefnFun asms' fun vs e' + Raw.DefnOp (Raw.SymbolPattern op vs) e -> + Sem.DefnOp op vs <$> glossExpr e + + +-- | A definition head is interpreted as a builder of a definition, +-- depending on a previous assumptions and on a rhs. +glossDefnHead :: Raw.DefnHead -> Gloss ([Sem.Asm] -> Sem.Formula -> Sem.Defn) +glossDefnHead = \case + -- TODO add info from NP. + Raw.DefnAdj _mnp v (Raw.Adj adj vs) -> do + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj) (v :| vs) f + --mnp' <- glossNPMaybe `each` mnp + --pure $ case mnp' of + -- Nothing -> \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj') (v :| vs) f + -- Just np' -> \asms f -> Sem.DefnPredicate asms (Sem.PredicateAdj adj') (v :| vs) (Sem.FormulaAnd (np' v) f) + Raw.DefnVerb _mnp v (Raw.Verb verb vs) -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f + Raw.DefnNoun v (Raw.Noun noun vs) -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f + Raw.DefnRel v1 rel v2 -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateRelation rel) (v1 :| [v2]) f + Raw.DefnSymbolicPredicate (Raw.PrefixPredicate symb _ar) vs -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateSymbol symb) vs f + + +glossProof :: Raw.Proof -> Gloss Sem.Proof +glossProof = \case + Raw.Omitted -> + pure Sem.Omitted + Raw.Qed by -> + pure (Sem.Qed by) + Raw.ByContradiction proof -> + Sem.ByContradiction <$> glossProof proof + Raw.BySetInduction mt proof -> + Sem.BySetInduction <$> mmt' <*> glossProof proof + where + mmt' = case mt of + Nothing -> pure Nothing + Just (Raw.TermExpr (Raw.ExprVar x)) -> pure (Just (Sem.TermVar x)) + Just _t -> throwError GlossInductionError + Raw.ByOrdInduction proof -> + Sem.ByOrdInduction <$> glossProof proof + Raw.ByCase cases -> Sem.ByCase <$> glossCase `each` cases + Raw.Have _ms s by proof -> case s of + -- Pragmatics: an existential @Have@ implicitly + -- introduces the witness and is interpreted as a @Take@ construct. + Raw.SymbolicExists vs bound suchThat -> do + bound' <- glossBound bound + suchThat' <- glossStmt suchThat + proof' <- glossProof proof + pure (Sem.Take vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof') + _otherwise -> + Sem.Have <$> glossStmt s <*> pure by <*> glossProof proof + Raw.Assume stmt proof -> + Sem.Assume <$> glossStmt stmt <*> glossProof proof + Raw.FixSymbolic xs bound proof -> do + bound' <- glossBound bound + proof' <- glossProof proof + pure (Sem.Fix xs (Sem.makeConjunction (bound' (toList xs))) proof') + Raw.FixSuchThat xs stmt proof -> do + stmt' <- glossStmt stmt + proof' <- glossProof proof + pure (Sem.Fix xs stmt' proof') + Raw.TakeVar vs bound suchThat by proof -> do + bound' <- glossBound bound + suchThat' <- glossStmt suchThat + proof' <- glossProof proof + pure (Sem.Take vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof') + Raw.TakeNoun np by proof -> do + (vs, constraints) <- glossNPList np + proof' <- glossProof proof + pure $ Sem.Take vs constraints by proof' + Raw.Subclaim subclaim subproof proof -> + Sem.Subclaim <$> glossStmt subclaim <*> glossProof subproof <*> glossProof proof + Raw.Suffices reduction by proof -> + Sem.Suffices <$> glossStmt reduction <*> pure by <*> glossProof proof + Raw.Define var term proof -> + Sem.Define var <$> glossExpr term <*> glossProof proof + Raw.DefineFunction funVar argVar valueExpr domVar domExpr proof -> + if domVar == argVar + then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof + else error "mismatched variables in function definition." + Raw.Calc calc proof -> + Sem.Calc <$> glossCalc calc <*> glossProof proof + +glossCase :: Raw.Case -> Gloss Sem.Case +glossCase (Raw.Case caseOf proof) = Sem.Case <$> glossStmt caseOf <*> glossProof proof + +glossCalc :: Raw.Calc -> Gloss Sem.Calc +glossCalc = \case + Raw.Equation e eqns -> do + e' <- glossExpr e + eqns' <- (\(ei, ji) -> (,ji) <$> glossExpr ei) `each` eqns + pure (Sem.Equation e' eqns') + Raw.Biconditionals p ps -> do + p' <- glossFormula p + ps' <- (\(pi, ji) -> (,ji) <$> glossFormula pi) `each` ps + pure (Sem.Biconditionals p' ps') + +glossSignature :: Raw.Signature -> Gloss Sem.Signature +glossSignature sig = case sig of + Raw.SignatureAdj v (Raw.Adj adj vs) -> + pure $ Sem.SignaturePredicate (Sem.PredicateAdj adj) (v :| vs) + Raw.SignatureVerb v (Raw.Verb verb vs) -> + pure $ Sem.SignaturePredicate (Sem.PredicateVerb verb) (v :| vs) + Raw.SignatureNoun v (Raw.Noun noun vs) -> + pure $ Sem.SignaturePredicate (Sem.PredicateNoun noun) (v :| vs) + Raw.SignatureSymbolic (Raw.SymbolPattern op vs) np -> do + (np', maySuchThat) <- glossNPMaybe np + let andSuchThat phi = case maySuchThat of + Just suchThat -> phi `Sem.And` suchThat + Nothing -> phi + let op' = Sem.TermOp op (Sem.TermVar <$> vs) + v <- freshVar + let v' = Sem.TermVar v + pure $ Sem.SignatureFormula $ Sem.makeForall [v] ((v' `Sem.Equals` op') `Sem.Implies` andSuchThat (np' v')) + + +glossStructDefn :: Raw.StructDefn -> Gloss Sem.StructDefn +glossStructDefn (Raw.StructDefn phrase base carrier fixes assumes) = do + assumes' <- (\(m, stmt) -> (m,) <$> glossStmt stmt) `each` assumes + -- We substitute occurrences of the bare label with the builtin symbol @\carrier@. + -- let assumes'' = fmap (annotateCarrierFormula carrier) assumes' + let assumes'' = [(m, annotateCarrierFormula carrier phi) |(m, phi) <- assumes'] + let base' = Set.fromList base + let fixes' = Set.fromList fixes + pure $ Sem.StructDefn phrase base' carrier fixes' assumes'' + +-- | Replace free variables corresponding to the label of a structure +-- with the abstract carrier symbol. +annotateCarrierFormula :: Sem.VarSymbol -> Sem.Term -> Sem.Term +annotateCarrierFormula lbl = \case + a `Sem.IsElementOf` Sem.TermVar x | x == lbl -> a `Sem.IsElementOf` Sem.TermSymbolStruct CarrierSymbol (Just (Sem.TermVar lbl)) + x -> x + + +glossAbbreviation :: Raw.Abbreviation -> Gloss Sem.Abbreviation +glossAbbreviation = \case + Raw.AbbreviationAdj x (Raw.Adj adj xs) stmt -> + makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateAdj adj)) (x : xs) stmt + Raw.AbbreviationVerb x (Raw.Verb verb xs) stmt -> + makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateVerb verb)) (x : xs) stmt + Raw.AbbreviationNoun x (Raw.Noun noun xs) stmt -> + makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateNoun noun)) (x : xs) stmt + Raw.AbbreviationRel x rel y stmt -> + makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) [x, y] stmt + Raw.AbbreviationFun (Raw.Fun fun xs) t -> + makeAbbrTerm (Sem.SymbolFun fun) xs t + Raw.AbbreviationEq (Raw.SymbolPattern op xs) e -> + makeAbbrExpr (Sem.SymbolMixfix op) xs e + + +makeAbbrStmt :: Sem.Symbol -> [VarSymbol] -> Raw.Stmt -> Gloss (Sem.Abbreviation) +makeAbbrStmt symbol zs stmt = do + stmt' <- glossStmt stmt + let aux y = case y `List.elemIndex` zs of + Nothing -> error ("free variable " <> show y <> " in abbreviation " <> show symbol) + Just k -> Left k + let scope = abstractEither aux stmt' :: Scope Int Sem.ExprOf Void + pure (Sem.Abbreviation symbol scope) + +makeAbbrTerm :: Sem.Symbol -> [VarSymbol] -> Raw.Term -> Gloss (Sem.Abbreviation) +makeAbbrTerm symbol zs t = do + (t', _quantify) <- glossTerm t + -- TODO replace "glossTerm t" with a more specific interpretation function + -- that checks if no indefinite terms are part of the term (erroring out if the term is indefinite). + let aux y = case y `List.elemIndex` zs of + Nothing -> error ("free variable " <> show y <> " in abbreviation " <> show symbol) + Just k -> Left k + let scope = abstractEither aux t' :: Scope Int Sem.ExprOf Void + pure (Sem.Abbreviation symbol scope) + +makeAbbrExpr :: Sem.Symbol -> [VarSymbol] -> Raw.Expr -> Gloss (Sem.Abbreviation) +makeAbbrExpr symbol zs e = do + e' <- glossExpr e + -- TODO replace "glossTerm t" with a more specific interpretation function + -- that checks if no indefinite terms are part of the term (erroring out if the term is indefinite). + let aux y = case y `List.elemIndex` zs of + Nothing -> error ("free variable " <> show y <> " in abbreviation " <> show symbol) + Just k -> Left k + let scope = abstractEither aux e' :: Scope Int Sem.ExprOf Void + pure (Sem.Abbreviation symbol scope) + + +glossInductive :: Raw.Inductive -> Gloss Sem.Inductive +glossInductive (Raw.Inductive (Raw.SymbolPattern symbol args) domain rules) = + Sem.Inductive symbol args <$> glossExpr domain <*> (glossRule `each` rules) + where + glossRule (Raw.IntroRule phis psi) = Sem.IntroRule <$> (glossFormula `each` phis) <*> glossFormula psi + +glossBlock :: Raw.Block -> Gloss Sem.Block +glossBlock = \case + Raw.BlockAxiom pos marker axiom -> + Sem.BlockAxiom pos marker <$> glossAxiom axiom + Raw.BlockLemma pos marker lemma -> + Sem.BlockLemma pos marker <$> glossLemma lemma + Raw.BlockProof pos proof -> + Sem.BlockProof pos <$> glossProof proof + Raw.BlockDefn pos marker defn -> do + defn' <- glossDefn defn + whenLeft (isWellformedDefn defn') (\err -> throwError (GlossDefnError err (show defn'))) + pure $ Sem.BlockDefn pos marker defn' + Raw.BlockAbbr pos marker abbr -> + Sem.BlockAbbr pos marker <$> glossAbbreviation abbr + Raw.BlockSig pos asms sig -> + Sem.BlockSig pos <$> glossAsms asms <*> glossSignature sig + Raw.BlockStruct pos m structDefn -> + Sem.BlockStruct pos m <$> glossStructDefn structDefn + Raw.BlockData _pos _ -> + _TODO "glossBlock datatype definitions" + Raw.BlockInductive pos marker ind -> + Sem.BlockInductive pos marker <$> glossInductive ind + + +glossBlocks :: [Raw.Block] -> Gloss [Sem.Block] +glossBlocks blocks = glossBlock `each` blocks |