diff options
Diffstat (limited to 'source/Felix/Meaning.hs')
| -rw-r--r-- | source/Felix/Meaning.hs | 1770 |
1 files changed, 1770 insertions, 0 deletions
diff --git a/source/Felix/Meaning.hs b/source/Felix/Meaning.hs new file mode 100644 index 0000000..268a1a6 --- /dev/null +++ b/source/Felix/Meaning.hs @@ -0,0 +1,1770 @@ +{-# LANGUAGE ApplicativeDo #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE TupleSections #-} + + +module Felix.Meaning where + + +import Base +import Felix.Syntax.Abstract (Sign(..)) +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Internal (VarSymbol(..), pattern FreshVar) +import Felix.Syntax.Internal qualified as Sem +import Felix.Syntax.LexicalPhrase (unsafeReadPhrase) +import Felix.Report.Location + +import Bound +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 +import Control.Exception (Exception) + + +-- | 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. + +-- These types are a private bridge to the current VarSymbol-based core. +newtype LocalId = LocalId Int + deriving (Show, Eq, Ord) + +data BinderTrivia = BinderTrivia + { binderDisplayHint :: Maybe Text + , binderDeclarationLocation :: Location + } deriving (Show, Eq, Ord) + +data ResolvedLocalRef + = AmbientRef VarSymbol + | LocalRef LocalId + deriving (Show, Eq, Ord) + +data H0ResolvedBinder = H0ResolvedBinder + { h0BinderId :: LocalId + , h0BinderTrivia :: BinderTrivia + } deriving (Show, Eq, Ord) + +data ResolvedBinderAdapterError + = UnknownResolvedLocal LocalId + | DuplicateResolvedLocalAssignment LocalId + | ResolvedLocalTokenCollision LocalId VarSymbol + deriving (Show, Eq, Ord) + +-- | Errors that can be detected during glossing. +data GlossError + = GlossDefnError Location DefnError Sem.Marker + | GlossInductionError Location + | GlossRelationExprWithParams Location + | GlossRelationApplicationError Sem.RelationApplicationError + | GlossDatatypeHeadError Location + | GlossDatatypeClauseTargetError Location + | GlossDatatypeConstructorError Location + | DependentReplacementDomainNotSupported Location + | QuantifiedTermRequiresResolvedContext Location + | IotaTermNotSupported Location + | DefiniteFunctionAssumptionNotSupported Location + | GlossProofFunctionArgumentMismatch + Location + VarSymbol + VarSymbol + | GlossProofFunctionNameMismatch + Location + VarSymbol + VarSymbol + | GlossAbbreviationError + Location + Sem.Marker + AbbreviationParameterError + | DuplicateQuantifiedNounBinder + Location + Location + Text + | GlossResolvedBinderAdapterError + Location + ResolvedBinderAdapterError + deriving (Eq, Ord) + +data AbbreviationParameterError + = DuplicateAbbreviationParameters (NonEmpty VarSymbol) + | FreeAbbreviationBodyVariables (NonEmpty VarSymbol) + deriving (Show, Eq, Ord) + +instance Exception GlossError +instance Show GlossError where show = explainGlossError + +explainGlossError :: GlossError -> String +explainGlossError = \case + GlossDefnError loc defnError marker -> + "Definition error at " <> prettyLocation loc <> " (in " <> show marker <> "): " <> case defnError of + DefnWarnLhsFree xs -> + "The variables " <> show xs <> " in the pattern being defined (definiendum) do not occur in the body of the definition (definiens). Remove them or use them in the body." + DefnErrorLhsNotLinear -> + "The left-hand side of the definition is not linear (a variable occurs multiple times)." + DefnErrorLhsTypeFree -> + "The defintion contains variables with no typing constraints or assumptions placed on them." + DefnErrorRhsFree xs -> + "The variables " <> show xs <> " on the right-hand side of the definition do not occurring on the left-hand side." + DefnErrorQuantifiedRhsTerm -> + "A quantified term cannot be the right-hand side of a functional definition." + GlossInductionError loc -> + "Error at " <> prettyLocation loc <> ": Induction over a non-variable is not supported." + GlossRelationExprWithParams loc -> + "Error at " <> prettyLocation loc <> ": A relation defined by an expression cannot have parameters." + GlossRelationApplicationError + (Sem.RelationParameterArityMismatch loc relation expected actual) -> + "Relation " + <> show (Sem.relationSymbolToken relation) + <> " at " + <> prettyLocation loc + <> " expects " + <> show (Sem.parameterArityValue expected) + <> " parameter(s), but received " + <> show (Sem.parameterArityValue actual) + <> "." + GlossDatatypeHeadError loc -> + "Error at " <> prettyLocation loc <> ": A datatype head must be a constant symbolic term." + GlossDatatypeClauseTargetError loc -> + "Error at " <> prettyLocation loc <> ": Every datatype clause must target the datatype being defined." + GlossDatatypeConstructorError loc -> + "Error at " <> prettyLocation loc <> ": Datatype constructors must be symbolic terms with bare variable arguments." + DependentReplacementDomainNotSupported loc -> + "Error at " + <> prettyLocation loc + <> ": dependent replacement domains are not yet supported." + QuantifiedTermRequiresResolvedContext loc -> + "Error at " + <> prettyLocation loc + <> ": a quantified term requires a resolved binding context." + IotaTermNotSupported loc -> + "Error at " + <> prettyLocation loc + <> ": definite-description terms are not supported." + DefiniteFunctionAssumptionNotSupported loc -> + "Error at " + <> prettyLocation loc + <> ": definite-function assumptions are not supported." + GlossProofFunctionArgumentMismatch loc valueArgument domainArgument -> + "Function definition error at " + <> prettyLocation loc + <> ": value argument " + <> show valueArgument + <> " does not match domain argument " + <> show domainArgument + <> "." + GlossProofFunctionNameMismatch loc declaredFunction definedFunction -> + "Function definition error at " + <> prettyLocation loc + <> ": declared function " + <> show declaredFunction + <> " does not match defined function " + <> show definedFunction + <> "." + GlossAbbreviationError loc marker abbreviationError -> + "Abbreviation error at " + <> prettyLocation loc + <> " (in " + <> show marker + <> "): " + <> case abbreviationError of + DuplicateAbbreviationParameters variables -> + "The parameters " + <> show (NonEmpty.toList variables) + <> " occur more than once." + FreeAbbreviationBodyVariables variables -> + "The body contains free variables not present in the head: " + <> show (NonEmpty.toList variables) + <> "." + DuplicateQuantifiedNounBinder firstLocation secondLocation name -> + "Quantified noun binder " + <> show name + <> " at " + <> prettyLocation secondLocation + <> " duplicates the overlapping binder at " + <> prettyLocation firstLocation + <> "." + GlossResolvedBinderAdapterError location adapterError -> + "Resolved binder adapter error at " + <> prettyLocation location + <> ": " + <> case adapterError of + UnknownResolvedLocal localId -> + "unknown local reference " <> show localId <> "." + DuplicateResolvedLocalAssignment localId -> + "duplicate legacy assignment for " <> show localId <> "." + ResolvedLocalTokenCollision localId token -> + "legacy token " + <> show token + <> " for " + <> show localId + <> " is not fresh." + +liftRelationApplication + :: Either Sem.RelationApplicationError a + -> Gloss a +liftRelationApplication = + either (throwError . GlossRelationApplicationError) pure + +-- | 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 = + if | ls' /= ls -> Left DefnErrorLhsNotLinear + | not (null rdiff) -> Left (DefnErrorRhsFree (toList rdiff)) + | not (null ldiff) -> case defn of + Sem.DefnPredicate{} -> Left (DefnWarnLhsFree (toList ldiff)) + _ -> Right defn + | otherwise -> Right defn + where + ls = lhsVars defn + ls' = nubOrd ls + rs = rhsVars defn + (ldiff, rdiff) = symmetricDifferenceDecompose (Set.fromList ls') rs + + +lhsVars :: Sem.Defn -> [VarSymbol] +lhsVars = \case + Sem.DefnPredicate _ _ vs _ -> toList vs + Sem.DefnFun _ _ vs _ -> vs + Sem.DefnOp _ vs _ -> vs + +rhsVars :: Sem.Defn -> Set VarSymbol +rhsVars = \case + Sem.DefnPredicate _ _ _ f -> Sem.freeVars f + Sem.DefnFun _ _ _ e -> Sem.freeVars e + Sem.DefnOp _ _ e -> Sem.freeVars e + + +-- | Validation errors for top-level definitions. +data DefnError + = DefnWarnLhsFree [VarSymbol] + | DefnErrorLhsNotLinear + | DefnErrorLhsTypeFree + | DefnErrorRhsFree [VarSymbol] + | DefnErrorQuantifiedRhsTerm + deriving (Show, Eq, Ord) + + +-- | Context for 'Gloss' computations. +data GlossState = GlossState + { varCount :: Int + -- ^ Counter for generating variables names for the output. + , localCount :: Int + -- ^ Counter for resolved quantified-noun binders. + , localBinderTrivia :: Map LocalId BinderTrivia + , legacyLocalTokens :: Map LocalId VarSymbol + } deriving (Show, Eq) + +freshVar :: Gloss VarSymbol +freshVar = do + i <- gets varCount + modify $ \s -> s {varCount = varCount s + 1} + pure $ FreshVar i + +type H0LexicalEnvironment = [H0ResolvedBinder] + +type H0Expr = Sem.ExprOf ResolvedLocalRef + +freshH0Binder + :: Location + -> Maybe VarSymbol + -> Gloss H0ResolvedBinder +freshH0Binder termLocation writtenName = do + nextLocal <- gets localCount + let localId = LocalId nextLocal + trivia = BinderTrivia + { binderDisplayHint = writtenName >>= displayedVariableName + , binderDeclarationLocation = + maybe termLocation locate writtenName + } + binder = H0ResolvedBinder localId trivia + modify \glossState -> + glossState + { localCount = nextLocal + 1 + , localBinderTrivia = + Map.insert localId trivia (localBinderTrivia glossState) + } + pure binder + where + displayedVariableName = \case + NamedVarAt _ name -> Just name + FreshVarAt{} -> Nothing + +pushH0Binder + :: H0ResolvedBinder + -> H0LexicalEnvironment + -> H0LexicalEnvironment +pushH0Binder = (:) + +resolveH0Reference + :: H0LexicalEnvironment + -> VarSymbol + -> ResolvedLocalRef +resolveH0Reference environment variable = case variable of + NamedVarAt _ name -> + maybe + (AmbientRef variable) + (LocalRef . h0BinderId) + (List.find hasDisplayName environment) + where + hasDisplayName binder = + binderDisplayHint (h0BinderTrivia binder) == Just name + FreshVarAt{} -> + AmbientRef variable + +resolveH0Expr + :: H0LexicalEnvironment + -> Sem.Expr + -> H0Expr +resolveH0Expr environment = + fmap (resolveH0Reference environment) + +lowerH0Expr :: H0Expr -> Gloss Sem.Expr +lowerH0Expr = + traverse \case + AmbientRef variable -> + pure variable + LocalRef localId -> do + trivia <- gets (Map.lookup localId . localBinderTrivia) + throwError + (GlossResolvedBinderAdapterError + (maybe Nowhere binderDeclarationLocation trivia) + (UnknownResolvedLocal localId)) + +abstractH0Binder + :: H0ResolvedBinder + -> H0Expr + -> Gloss (Scope VarSymbol Sem.ExprOf ResolvedLocalRef) +abstractH0Binder binder body = do + token <- allocateLegacyLocalToken binder body + pure + (abstract + (\case + LocalRef localId + | localId == h0BinderId binder -> + Just token + _ -> + Nothing) + body) + +allocateLegacyLocalToken + :: H0ResolvedBinder + -> H0Expr + -> Gloss VarSymbol +allocateLegacyLocalToken binder body = do + assignments <- gets legacyLocalTokens + case Map.lookup localId assignments of + Just _ -> + throwAdapterError + (DuplicateResolvedLocalAssignment localId) + Nothing -> do + let ambientTokens = + Set.fromList + [ token + | AmbientRef token <- toList body + ] + assignedTokens = + Set.fromList (Map.elems assignments) + forbiddenTokens = + ambientTokens <> assignedTokens + token <- freshTokenOutside forbiddenTokens + if token `Set.member` forbiddenTokens + then + throwAdapterError + (ResolvedLocalTokenCollision localId token) + else do + modify \glossState -> + glossState + { legacyLocalTokens = + Map.insert + localId + token + (legacyLocalTokens glossState) + } + pure token + where + localId = h0BinderId binder + binderLocation = + binderDeclarationLocation (h0BinderTrivia binder) + throwAdapterError = + throwError + . GlossResolvedBinderAdapterError binderLocation + + freshTokenOutside forbidden = do + candidate <- freshVar + if candidate `Set.member` forbidden + then freshTokenOutside forbidden + else pure candidate + +initialGlossState :: GlossState +initialGlossState = GlossState + { varCount = 0 + , localCount = 0 + , localBinderTrivia = mempty + , legacyLocalTokens = mempty + } + +glossStep :: GlossState -> Raw.Block -> Either GlossError (Sem.Block, GlossState) +glossStep glossState block = case runState (runExceptT (glossBlock block)) glossState of + (Left err, _nextGlossState) -> Left err + (Right glossedBlock, nextGlossState) -> Right (glossedBlock, nextGlossState) + +meaning :: [Raw.Block] -> Either GlossError [Sem.Block] +meaning blocks = evalState (runExceptT (glossBlocks blocks)) initialGlossState + +glossExpr :: Raw.Expr -> Gloss (Sem.ExprOf VarSymbol) +glossExpr = \case + Raw.ExprVar v -> + pure $ Sem.TermVar v + Raw.ExprInteger loc n -> + pure $ Sem.TermSymbol loc (Sem.SymbolInteger n) [] + Raw.ExprOp loc f es -> + Sem.TermSymbol loc <$> pure (Sem.SymbolMixfix f) <*> (glossExpr `each` es) + Raw.ExprStructOp _loc tok maybeLabel -> do + maybeLabel' <- traverse glossExpr maybeLabel + pure $ Sem.TermSymbolStruct tok maybeLabel' + Raw.ExprSep _loc x t phi -> do + t' <- glossExpr t + phi' <- glossStmt phi + pure (Sem.TermSep x t' (abstract1 x phi')) + Raw.ExprReplacePred _loc 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 _loc e bounds phi -> do + e' <- glossExpr e + bounds' <- glossReplaceBounds 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 + glossReplaceBounds + :: NonEmpty (VarSymbol, Raw.Expr) + -> Gloss (NonEmpty (VarSymbol, Sem.Term)) + glossReplaceBounds + ((firstBinder, firstDomain) :| remainingBounds) = do + firstDomain' <- glossExpr firstDomain + remainingBounds' <- + go (Set.singleton firstBinder) remainingBounds + pure ((firstBinder, firstDomain') :| remainingBounds') + where + go + :: Set VarSymbol + -> [(VarSymbol, Raw.Expr)] + -> Gloss [(VarSymbol, Sem.Term)] + go _precedingBinders [] = pure [] + go precedingBinders ((binder, domain) : laterBounds) = do + domain' <- glossExpr domain + -- Folding a glossed domain visits only free occurrences. + case List.find + (`Set.member` precedingBinders) + (toList domain') of + Just occurrence -> + throwError + (DependentReplacementDomainNotSupported + (locate occurrence)) + Nothing -> do + laterBounds' <- + go + (Set.insert binder precedingBinders) + laterBounds + pure ((binder, domain') : laterBounds') + Raw.ExprFiniteSet loc es -> do + es' <- glossExpr `each` es + pure (Sem.finiteSet loc es') + + +glossFormula :: Raw.Formula -> Gloss (Sem.ExprOf VarSymbol) +glossFormula = \case + Raw.FormulaChain ch -> + glossChain ch + Raw.Connected _loc conn phi psi -> + glossConnective conn <*> glossFormula phi <*> glossFormula psi + Raw.FormulaNeg loc f -> + Sem.Not loc <$> glossFormula f + Raw.FormulaPredicate loc predi _marker es -> + Sem.Atomic loc <$> glossPrefixPredicate predi <*> glossExpr `each` toList es + Raw.PropositionalConstant _loc c -> + pure $ Sem.PropositionalConstant c + Raw.FormulaQuantified _loc 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.Relation loc rel' params -> do + params' <- glossExpr `each` params + buildRelation <- + liftRelationApplication + (Sem.makeRelationApplication loc rel' params') + pure $ sign' loc $ buildRelation e1' e2' + Raw.RelationExpr loc e -> do + e' <- glossExpr e + pure (sign' loc (Sem.IsElementOf loc (Sem.TermPair loc e1' e2') 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 = Sem.Equals Nowhere t (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 loc pat es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \t -> quantify $ Sem.FormulaAdj loc 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 _loc pat [e] | pat == Raw.mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" -> do + (e', quantify) <- glossTerm e + pure $ \t -> quantify $ Sem.Equals Nowhere t e' + Raw.AdjR _loc pat es -> do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \t -> quantify $ Sem.FormulaAdj Nowhere 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 loc pat [e] | pat == Raw.mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" -> do + (e', quantify) <- glossTerm e + pure $ \t -> quantify $ Sem.Equals loc t e' + Raw.Adj loc pat es -> do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \t -> quantify $ Sem.FormulaAdj loc 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 Nowhere .) <$> glossVerb verb + Raw.VPAdjNot adjs -> (Sem.Not Nowhere .) <$> glossVP (Raw.VPAdj adjs) + + +glossVerb :: Raw.Verb -> Gloss (Sem.Term -> Sem.Formula) +glossVerb (Raw.Verb loc pat es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure $ \ t -> quantify $ Sem.FormulaVerb loc t pat es' + + +glossNoun :: Raw.Noun -> Gloss (Sem.Term -> Sem.Formula) +glossNoun (Raw.Noun loc pat es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure case Raw.sg (Raw.lexicalItemSgPlPhrase pat) of + -- Everything is a set + [Just (Sem.Word "set")] -> const Sem.Top + _ -> \e' -> quantify (Sem.FormulaNoun loc e' pat es') + + +glossFun :: Raw.Fun -> Gloss (Sem.Term, Sem.Formula -> Sem.Formula) +glossFun (Raw.Fun loc phrase es) = do + (es', quantifies) <- unzip <$> glossTerm `each` es + let quantify = compose $ reverse quantifies + pure (Sem.TermSymbol loc (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 location _variable _statement -> + rejectIotaTerm location + Raw.TermQuantified _quantifier loc _nounPhrase -> + throwError (QuantifiedTermRequiresResolvedContext loc) + +rejectIotaTerm :: Location -> Gloss a +rejectIotaTerm = + throwError . IotaTermNotSupported + + +data H0QuantifiedTerm = H0QuantifiedTerm + { h0Quantifier :: Raw.Quantifier + , h0QuantifiedBinder :: H0ResolvedBinder + , h0QuantifiedConstraints :: [H0Expr] + } + +data H0TermPlan = H0TermPlan + { h0TermExpression :: H0Expr + , h0TermEnvironment :: H0LexicalEnvironment + , h0TermQuantifiers :: [H0QuantifiedTerm] + } + +data H0TermsPlan = H0TermsPlan + { h0TermExpressions :: [H0Expr] + , h0TermsEnvironment :: H0LexicalEnvironment + , h0TermsQuantifiers :: [H0QuantifiedTerm] + } + +glossH0Terms + :: H0LexicalEnvironment + -> [Raw.Term] + -> Gloss H0TermsPlan +glossH0Terms initialEnvironment = + go initialEnvironment mempty [] [] + where + go environment _seenBinders expressions quantifiers [] = + pure + H0TermsPlan + { h0TermExpressions = reverse expressions + , h0TermsEnvironment = environment + , h0TermsQuantifiers = reverse quantifiers + } + go environment seenBinders expressions quantifiers (term : terms) = do + termPlan <- glossH0Term environment term + nextSeenBinders <- + foldM + addSiblingBinder + seenBinders + (h0TermQuantifiers termPlan) + go + (h0TermEnvironment termPlan) + nextSeenBinders + (h0TermExpression termPlan : expressions) + (reverse (h0TermQuantifiers termPlan) <> quantifiers) + terms + + addSiblingBinder seenBinders quantifiedTerm = + case binderDisplayHint binderTrivia of + Nothing -> + pure seenBinders + Just displayName -> + case Map.lookup displayName seenBinders of + Nothing -> + pure + (Map.insert + displayName + binderTrivia + seenBinders) + Just firstBinderTrivia -> + throwError + (DuplicateQuantifiedNounBinder + (binderDeclarationLocation + firstBinderTrivia) + (binderDeclarationLocation + binderTrivia) + displayName) + where + binderTrivia = + h0BinderTrivia + (h0QuantifiedBinder quantifiedTerm) + +glossH0Term + :: H0LexicalEnvironment + -> Raw.Term + -> Gloss H0TermPlan +glossH0Term environment = \case + Raw.TermExpr expression -> do + expression' <- resolveH0Expr environment <$> glossExpr expression + pure + H0TermPlan + { h0TermExpression = expression' + , h0TermEnvironment = environment + , h0TermQuantifiers = [] + } + Raw.TermFun (Raw.Fun location symbol arguments) -> do + argumentsPlan <- glossH0Terms environment arguments + pure + H0TermPlan + { h0TermExpression = + Sem.TermSymbol + location + (Sem.SymbolFun symbol) + (h0TermExpressions argumentsPlan) + , h0TermEnvironment = + h0TermsEnvironment argumentsPlan + , h0TermQuantifiers = + h0TermsQuantifiers argumentsPlan + } + Raw.TermIota location _variable _statement -> + rejectIotaTerm location + Raw.TermQuantified quantifier location nounPhrase -> do + let writtenName = case nounPhrase of + Raw.NounPhrase _ _ name _ _ -> name + binder <- freshH0Binder location writtenName + let nextEnvironment = pushH0Binder binder environment + witness = Sem.TermVar (LocalRef (h0BinderId binder)) + constraints <- + glossH0QuantifiedNoun + nextEnvironment + witness + nounPhrase + pure + H0TermPlan + { h0TermExpression = witness + , h0TermEnvironment = nextEnvironment + , h0TermQuantifiers = + [ H0QuantifiedTerm + { h0Quantifier = quantifier + , h0QuantifiedBinder = binder + , h0QuantifiedConstraints = constraints + } + ] + } + +applyH0Quantifiers + :: [H0QuantifiedTerm] + -> H0Expr + -> Gloss H0Expr +applyH0Quantifiers quantifiers body = + foldrM applyQuantifier body quantifiers + where + applyQuantifier quantifiedTerm continuation = do + let constrainedBody = + applyQuantifierConstraints + (h0Quantifier quantifiedTerm) + (h0QuantifiedConstraints quantifiedTerm) + continuation + scope <- + abstractH0Binder + (h0QuantifiedBinder quantifiedTerm) + constrainedBody + pure case h0Quantifier quantifiedTerm of + Raw.Universally -> + Sem.Quantified Sem.Universally scope + Raw.Existentially -> + Sem.Quantified Sem.Existentially scope + Raw.Nonexistentially -> + Sem.Not + Nowhere + (Sem.Quantified Sem.Existentially scope) + +glossH0QuantifiedNoun + :: H0LexicalEnvironment + -> H0Expr + -> Raw.NounPhrase Maybe + -> Gloss [H0Expr] +glossH0QuantifiedNoun + environment + witness + (Raw.NounPhrase leftAdjectives noun _name rightAdjectives maySuchThat) = do + nounConstraint <- glossH0Noun environment witness noun + leftConstraints <- + for leftAdjectives (glossH0AdjL environment witness) + rightConstraints <- + for rightAdjectives (glossH0AdjR environment witness) + suchThatConstraint <- + traverse (glossH0Stmt environment) maySuchThat + pure + ( maybeToList suchThatConstraint + <> [ Sem.makeConjunction + ( nounConstraint + : leftConstraints + <> rightConstraints + ) + ] + ) + +glossH0NPMaybe + :: H0LexicalEnvironment + -> H0Expr + -> Raw.NounPhrase Maybe + -> Gloss (H0Expr, Maybe H0Expr) +glossH0NPMaybe + environment + subject + (Raw.NounPhrase leftAdjectives noun mayName rightAdjectives maySuchThat) = do + nounConstraint <- glossH0Noun environment subject noun + suchThatConstraint <- + traverse (glossH0Stmt environment) maySuchThat + case mayName of + Nothing -> do + leftConstraints <- + for leftAdjectives (glossH0AdjL environment subject) + rightConstraints <- + for rightAdjectives (glossH0AdjR environment subject) + pure + ( Sem.makeConjunction + ( nounConstraint + : leftConstraints + <> rightConstraints + ) + , suchThatConstraint + ) + Just name -> do + let namedSubject = + Sem.TermVar + (resolveH0Reference environment name) + leftConstraints <- + for leftAdjectives + (glossH0AdjL environment namedSubject) + rightConstraints <- + for rightAdjectives + (glossH0AdjR environment namedSubject) + let modifierConstraints = + leftConstraints <> rightConstraints + constraint = case modifierConstraints of + [] -> + nounConstraint + _ -> + nounConstraint + `Sem.And` + Sem.makeConjunction + ( Sem.Equals + Nowhere + subject + namedSubject + : modifierConstraints + ) + pure (constraint, suchThatConstraint) + +glossH0AdjL + :: H0LexicalEnvironment + -> H0Expr + -> Raw.AdjL + -> Gloss H0Expr +glossH0AdjL environment subject (Raw.AdjL location lexicalPattern arguments) = do + argumentsPlan <- glossH0Terms environment arguments + applyH0Quantifiers + (h0TermsQuantifiers argumentsPlan) + (Sem.FormulaAdj + location + subject + lexicalPattern + (h0TermExpressions argumentsPlan)) + +glossH0AdjR + :: H0LexicalEnvironment + -> H0Expr + -> Raw.AdjR + -> Gloss H0Expr +glossH0AdjR environment subject = \case + Raw.AdjR _location lexicalPattern [argument] + | lexicalPattern + == Raw.mkLexicalItem + (unsafeReadPhrase "equal to ?") + "eq" -> do + argumentPlan <- + glossH0Term environment argument + applyH0Quantifiers + (h0TermQuantifiers argumentPlan) + (Sem.Equals + Nowhere + subject + (h0TermExpression argumentPlan)) + Raw.AdjR _location lexicalPattern arguments -> do + argumentsPlan <- glossH0Terms environment arguments + applyH0Quantifiers + (h0TermsQuantifiers argumentsPlan) + (Sem.FormulaAdj + Nowhere + subject + lexicalPattern + (h0TermExpressions argumentsPlan)) + Raw.AttrRThat verbPhrase -> + glossH0VP environment subject verbPhrase + +glossH0Adj + :: H0LexicalEnvironment + -> H0Expr + -> Raw.Adj + -> Gloss H0Expr +glossH0Adj environment subject = \case + Raw.Adj location lexicalPattern [argument] + | lexicalPattern + == Raw.mkLexicalItem + (unsafeReadPhrase "equal to ?") + "eq" -> do + argumentPlan <- + glossH0Term environment argument + applyH0Quantifiers + (h0TermQuantifiers argumentPlan) + (Sem.Equals + location + subject + (h0TermExpression argumentPlan)) + Raw.Adj location lexicalPattern arguments -> do + argumentsPlan <- glossH0Terms environment arguments + applyH0Quantifiers + (h0TermsQuantifiers argumentsPlan) + (Sem.FormulaAdj + location + subject + lexicalPattern + (h0TermExpressions argumentsPlan)) + +glossH0VP + :: H0LexicalEnvironment + -> H0Expr + -> Raw.VerbPhrase + -> Gloss H0Expr +glossH0VP environment subject = \case + Raw.VPVerb verb -> + glossH0Verb environment subject verb + Raw.VPAdj adjectives -> + Sem.makeConjunction + <$> for + (toList adjectives) + (glossH0Adj environment subject) + Raw.VPVerbNot verb -> + Sem.Not Nowhere + <$> glossH0Verb environment subject verb + Raw.VPAdjNot adjectives -> + Sem.Not Nowhere + <$> glossH0VP + environment + subject + (Raw.VPAdj adjectives) + +glossH0Verb + :: H0LexicalEnvironment + -> H0Expr + -> Raw.Verb + -> Gloss H0Expr +glossH0Verb environment subject (Raw.Verb location lexicalPattern arguments) = do + argumentsPlan <- glossH0Terms environment arguments + applyH0Quantifiers + (h0TermsQuantifiers argumentsPlan) + (Sem.FormulaVerb + location + subject + lexicalPattern + (h0TermExpressions argumentsPlan)) + +glossH0Noun + :: H0LexicalEnvironment + -> H0Expr + -> Raw.Noun + -> Gloss H0Expr +glossH0Noun environment subject (Raw.Noun location lexicalPattern arguments) = do + argumentsPlan <- glossH0Terms environment arguments + let constraint = case Raw.sg (Raw.lexicalItemSgPlPhrase lexicalPattern) of + [Just (Sem.Word "set")] -> + Sem.Top + _ -> + Sem.FormulaNoun + location + subject + lexicalPattern + (h0TermExpressions argumentsPlan) + applyH0Quantifiers + (h0TermsQuantifiers argumentsPlan) + constraint + + + +glossStmt :: Raw.Stmt -> Gloss Sem.Formula +glossStmt statement = do + resolvedStatement <- glossH0Stmt [] statement + lowerH0Expr resolvedStatement + +glossH0Stmt + :: H0LexicalEnvironment + -> Raw.Stmt + -> Gloss H0Expr +glossH0Stmt environment = \case + Raw.StmtFormula formula -> + resolveH0Expr environment <$> glossFormula formula + Raw.StmtNeg location statement -> + Sem.Not location <$> glossH0Stmt environment statement + Raw.StmtVerbPhrase ts vp -> do + termsPlan <- glossH0Terms environment (toList ts) + statements <- + for + (h0TermExpressions termsPlan) + (\term -> + glossH0VP + (h0TermsEnvironment termsPlan) + term + vp) + applyH0Quantifiers + (h0TermsQuantifiers termsPlan) + (Sem.makeConjunction statements) + Raw.StmtNoun ts np -> do + termsPlan <- glossH0Terms environment (toList ts) + statements <- + for (h0TermExpressions termsPlan) \term -> do + (nounConstraint, maySuchThat) <- + glossH0NPMaybe + (h0TermsEnvironment termsPlan) + term + np + pure case maySuchThat of + Just suchThat -> + nounConstraint `Sem.And` suchThat + Nothing -> + nounConstraint + applyH0Quantifiers + (h0TermsQuantifiers termsPlan) + (Sem.makeConjunction statements) + Raw.StmtStruct t sp -> do + termPlan <- glossH0Term environment t + applyH0Quantifiers + (h0TermQuantifiers termPlan) + (Sem.TermSymbol + (locate t) + (Sem.SymbolPredicate + (Sem.PredicateNounStruct sp)) + [h0TermExpression termPlan]) + Raw.StmtConnected connective _location left right -> + Sem.Connected connective + <$> glossH0Stmt environment left + <*> glossH0Stmt environment right + Raw.StmtQuantPhrase _location (Raw.QuantPhrase quantifier np) statement -> do + (vars, constraints) <- glossNPList np + let nestedEnvironment = + hideH0Binders vars environment + constraints' = + resolveH0Expr nestedEnvironment constraints + statement' <- + glossH0Stmt nestedEnvironment statement + pure + (quantifyH0Ambient + quantifier + vars + [constraints'] + statement') + Raw.StmtExists _location np -> do + (vars, constraints) <- glossNPList np + let nestedEnvironment = + hideH0Binders vars environment + pure + (quantifyH0Ambient + Raw.Existentially + vars + [] + (resolveH0Expr nestedEnvironment constraints)) + Raw.SymbolicQuantified _loc quant vs bound suchThat have -> do + let nestedEnvironment = + hideH0Binders vs environment + bound' <- glossBound bound + let boundConstraints = + resolveH0Expr nestedEnvironment + <$> bound' (toList vs) + suchThatConstraints <- + maybeToList + <$> traverse + (glossH0Stmt nestedEnvironment) + suchThat + have' <- glossH0Stmt nestedEnvironment have + pure + (quantifyH0Ambient + quant + vs + (boundConstraints <> suchThatConstraints) + have') + +-- Other binder forms stay on the legacy path and only mask outer H0 names. +hideH0Binders + :: Foldable f + => f VarSymbol + -> H0LexicalEnvironment + -> H0LexicalEnvironment +hideH0Binders variables = + List.filter \binder -> + maybe + True + (`Set.notMember` displayedNames) + (binderDisplayHint (h0BinderTrivia binder)) + where + displayedNames = + Set.fromList + [ name + | NamedVarAt _ name <- toList variables + ] + +quantifyH0Ambient + :: Foldable f + => Raw.Quantifier + -> f VarSymbol + -> [H0Expr] + -> H0Expr + -> H0Expr +quantifyH0Ambient quantifier variables constraints body = + case quantifier of + Raw.Universally -> + Sem.Quantified Sem.Universally scope + Raw.Existentially -> + Sem.Quantified Sem.Existentially scope + Raw.Nonexistentially -> + Sem.Not + Nowhere + (Sem.Quantified Sem.Existentially scope) + where + constrainedBody = + applyQuantifierConstraints quantifier constraints body + scope = + abstract + (\case + AmbientRef variable + | variable `elem` variables -> + Just variable + _ -> + Nothing) + constrainedBody + +-- | 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 loc sign rel term -> do + term' <- glossExpr term + let sign' = case sign of + Positive -> id + Negative -> Sem.Not loc + bound <- case rel of + Raw.Relation loc' rel' params -> do + params' <- glossExpr `each` params + buildRelation <- + liftRelationApplication + (Sem.makeRelationApplication loc' rel' params') + pure $ \v -> sign' $ + buildRelation (Sem.TermVar v) term' + Raw.RelationExpr loc' e -> do + e' <- glossExpr e + pure $ \v -> sign' $ + Sem.IsElementOf loc' (Sem.TermPair loc' (Sem.TermVar v) term') e' + pure \vs -> vs <**> [bound] + + +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.IsElementOf Nowhere (Sem.TermVar v) e') + pure $ fmap f (toList vs) + Raw.AsmLetStruct structLabel structPhrase -> + pure [Sem.AsmStruct structLabel structPhrase] + Raw.AsmLetThe _variable fun -> + throwError + (DefiniteFunctionAssumptionNotSupported + (locate fun)) + Raw.AsmLetEq x e -> do + e' <- glossExpr e + pure (Sem.Asm (Sem.Equals Nowhere (Sem.TermVar x) e') : []) + + +-- | 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 body = case quantifier of + Raw.Universally -> + Sem.makeForall + vs + (applyQuantifierConstraints + quantifier + constraints + body) + Raw.Existentially -> + Sem.makeExists + vs + (applyQuantifierConstraints + quantifier + constraints + body) + Raw.Nonexistentially -> + Sem.Not + Nowhere + (Sem.makeExists + vs + (applyQuantifierConstraints + quantifier + constraints + body)) + +applyQuantifierConstraints + :: Raw.Quantifier + -> [Sem.ExprOf a] + -> Sem.ExprOf a + -> Sem.ExprOf a +applyQuantifierConstraints _quantifier [] body = + body +applyQuantifierConstraints quantifier constraints body = + case quantifier of + Raw.Universally -> + Sem.makeConjunction constraints `Sem.Implies` body + Raw.Existentially -> + Sem.makeConjunction constraints `Sem.And` body + Raw.Nonexistentially -> + Sem.makeConjunction constraints `Sem.And` body + + +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.Claim -> Gloss Sem.Lemma +glossLemma (Raw.Claim asms f) = Sem.Lemma <$> glossAsms asms <*> glossStmt f + + +glossDefn + :: Location + -> Sem.Marker + -> Raw.Defn + -> Gloss Sem.Defn +glossDefn blockLocation blockMarker = \case + Raw.Defn asms h f -> + glossDefnHead blockLocation h <*> glossAsms asms <*> glossStmt f + Raw.DefnFun asms (Raw.Fun _loc fun vs) _ e -> do + asms' <- glossAsms asms + e' <- case e of + Raw.TermQuantified _ loc _ -> + throwError + (GlossDefnError + loc + DefnErrorQuantifiedRhsTerm + blockMarker) + _ -> 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 + :: Location + -> Raw.DefnHead + -> Gloss ([Sem.Asm] -> Sem.Formula -> Sem.Defn) +glossDefnHead blockLocation = \case + -- TODO add info from NP. + Raw.DefnAdj _mnp v (Raw.Adj _loc 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 _loc verb vs) -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f + Raw.DefnNoun v (Raw.Noun _loc noun vs) -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f + Raw.DefnRel v1 rel params v2 -> do + liftRelationApplication + (Sem.checkRelationParameterArity + blockLocation + rel + params) + pure \asms f -> + let args = case params of + p : ps -> p :| (ps <> [v1, v2]) + [] -> v1 :| [v2] + in Sem.DefnPredicate asms (Sem.PredicateRelation rel) args f + Raw.DefnSymbolicPredicate (Raw.PrefixPredicate symb _ar) _marker vs -> + pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateSymbol symb) vs f + + +glossProof :: Raw.Proof -> Gloss Sem.Proof +glossProof = \case + Raw.Omitted loc -> + pure (Sem.Omitted loc) + Raw.Qed loc by -> + pure (Sem.Qed loc by) + Raw.Contradiction loc by -> + pure (Sem.Contradiction loc by) + Raw.ByContradiction loc proof -> + Sem.ByContradiction loc <$> glossProof proof + Raw.BySetInduction loc mt proof -> + Sem.BySetInduction loc <$> 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 loc) + Raw.ByOrdInduction loc proof -> + Sem.ByOrdInduction loc <$> glossProof proof + Raw.ByCase loc cases -> Sem.ByCase loc <$> glossCase `each` cases + Raw.Have loc _ms s by proof -> case s of + -- Pragmatics: an existential @Have@ implicitly + -- introduces the witness and is interpreted as a @Take@ construct. + Raw.SymbolicExists _loc vs bound suchThat -> do + bound' <- glossBound bound + suchThat' <- glossStmt suchThat + proof' <- glossProof proof + pure (Sem.Take loc vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof') + _otherwise -> + Sem.Have loc <$> glossStmt s <*> pure by <*> glossProof proof + Raw.Assume loc stmt proof -> + Sem.Assume loc <$> glossStmt stmt <*> glossProof proof + Raw.FixSymbolic loc xs bound proof -> do + bound' <- glossBound bound + proof' <- glossProof proof + pure (Sem.Fix loc xs (Sem.makeConjunction (bound' (toList xs))) proof') + Raw.FixSuchThat loc xs stmt proof -> do + stmt' <- glossStmt stmt + proof' <- glossProof proof + pure (Sem.Fix loc xs stmt' proof') + Raw.TakeVar loc vs bound suchThat by proof -> do + bound' <- glossBound bound + suchThat' <- glossStmt suchThat + proof' <- glossProof proof + pure (Sem.Take loc vs (Sem.makeConjunction (suchThat' : bound' (toList vs))) by proof') + Raw.TakeNoun loc np by proof -> do + (vs, constraints) <- glossNPList np + proof' <- glossProof proof + pure $ Sem.Take loc vs constraints by proof' + Raw.Subclaim loc subclaim subproof proof -> + Sem.Subclaim loc <$> glossStmt subclaim <*> glossProof subproof <*> glossProof proof + Raw.Suffices loc reduction by proof -> + Sem.Suffices loc <$> glossStmt reduction <*> pure by <*> glossProof proof + Raw.Define loc var term proof -> + Sem.Define loc var <$> glossExpr term <*> glossProof proof + Raw.DefineFunction loc funVar argVar valueExpr domVar domExpr proof -> + if domVar == argVar + then Sem.DefineFunction loc funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof + else + throwError + (GlossProofFunctionArgumentMismatch + loc + argVar + domVar) + + Raw.DefineFunctionLocal loc funVar domVar ranExpr funVar2 argVar definitions proof -> do + if funVar == funVar2 + then Sem.DefineFunctionLocal loc funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof + else + throwError + (GlossProofFunctionNameMismatch + loc + funVar + funVar2) + Raw.Calc loc calcQuant calc proof -> + Sem.Calc loc <$> glossCalcQuantifier calcQuant <*> glossCalc calc <*> glossProof proof + +glossCalcQuantifier :: Maybe Raw.CalcQuantifier -> Gloss Sem.CalcQuantifier +glossCalcQuantifier Nothing = pure Sem.CalcUnquantified +glossCalcQuantifier (Just (Raw.CalcQuantifier xs bound maySuchThat)) = do + bound' <- glossBound bound + maySuchThat' <- glossStmt `each` maySuchThat + let constraints = bound' (toList xs) <> maybeToList maySuchThat' + let calcGuard = case constraints of + [] -> Nothing + _ -> Just (Sem.makeConjunction constraints) + pure (Sem.CalcForall xs calcGuard) + +glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula) +glossLocalFunctionExprDef (definingExpression, localDomain) = do + e <- glossExpr definingExpression + d <- glossFormula localDomain + pure (e,d) + + +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 _loc adj vs) -> + pure $ Sem.SignaturePredicate (Sem.PredicateAdj adj) (v :| vs) + Raw.SignatureVerb v (Raw.Verb _loc verb vs) -> + pure $ Sem.SignaturePredicate (Sem.PredicateVerb verb) (v :| vs) + Raw.SignatureNoun v (Raw.Noun _loc 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 Nowhere op (Sem.TermVar <$> vs) + v <- freshVar + let v' = Sem.TermVar v + pure $ Sem.SignatureFormula $ Sem.makeForall [v] ((Sem.Equals Nowhere v' 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 + let base' = Set.fromList base + let fixes' = Set.fromList fixes + pure $ Sem.StructDefn phrase base' carrier fixes' assumes' + + +glossAbbreviation + :: Location + -> Sem.Marker + -> Raw.Abbreviation + -> Gloss Sem.Abbreviation +glossAbbreviation blockLocation blockMarker = \case + Raw.AbbreviationAdj x (Raw.Adj _loc adj xs) stmt -> + build + (Sem.SymbolPredicate (Sem.PredicateAdj adj)) + (x : xs) + (glossStmt stmt) + Raw.AbbreviationVerb x (Raw.Verb _loc verb xs) stmt -> + build + (Sem.SymbolPredicate (Sem.PredicateVerb verb)) + (x : xs) + (glossStmt stmt) + Raw.AbbreviationNoun x (Raw.Noun _loc noun xs) stmt -> + build + (Sem.SymbolPredicate (Sem.PredicateNoun noun)) + (x : xs) + (glossStmt stmt) + Raw.AbbreviationRel x rel params y stmt -> do + liftRelationApplication + (Sem.checkRelationParameterArity + blockLocation + rel + params) + build + (Sem.SymbolPredicate (Sem.PredicateRelation rel)) + (params <> [x, y]) + (glossStmt stmt) + Raw.AbbreviationFun (Raw.Fun _loc fun xs) t -> + build + (Sem.SymbolFun fun) + xs + (fst <$> glossTerm t) + Raw.AbbreviationEq (Raw.SymbolPattern op xs) e -> + build + (Sem.SymbolMixfix op) + xs + (glossExpr e) + where + build = + makeAbbreviation blockLocation blockMarker + +makeAbbreviation + :: Location + -> Sem.Marker + -> Sem.Symbol + -> [VarSymbol] + -> Gloss Sem.Expr + -> Gloss Sem.Abbreviation +makeAbbreviation blockLocation blockMarker symbol rawParameters elaborateBody = do + parameters <- + either + (throwError + . GlossAbbreviationError + blockLocation + blockMarker + . DuplicateAbbreviationParameters) + pure + (validateAbbreviationParameters rawParameters) + body <- elaborateBody + scope <- + either + (throwError + . GlossAbbreviationError + blockLocation + blockMarker + . FreeAbbreviationBodyVariables) + pure + (abstractClosedAbbreviation parameters body) + pure (Sem.Abbreviation symbol scope) + where + validateAbbreviationParameters + :: [VarSymbol] + -> Either + (NonEmpty VarSymbol) + (Map VarSymbol Int) + validateAbbreviationParameters parameters = + case NonEmpty.nonEmpty (duplicateParameters parameters) of + Just duplicates -> + Left duplicates + Nothing -> + Right (Map.fromList (zip parameters [0 ..])) + + abstractClosedAbbreviation + :: Map VarSymbol Int + -> Sem.Expr + -> Either + (NonEmpty VarSymbol) + (Scope Int Sem.ExprOf Void) + abstractClosedAbbreviation parameterIndices body = + case NonEmpty.nonEmpty unknownVariables of + Just variables -> + Left variables + Nothing -> + case traverse bindParameter body of + Left variable -> + Left (variable :| []) + Right scopedBody -> + Right (toScope scopedBody) + where + unknownVariables = + Set.toAscList + ( Sem.freeVars body + `Set.difference` + Map.keysSet parameterIndices + ) + + bindParameter + :: VarSymbol + -> Either + VarSymbol + (Var Int Void) + bindParameter variable = + case Map.lookup variable parameterIndices of + Nothing -> + Left variable + Just parameterIndex -> + Right (B parameterIndex) + + duplicateParameters :: [VarSymbol] -> [VarSymbol] + duplicateParameters = + reverse . third . foldl' step (mempty, mempty, []) + where + step (seen, reported, duplicates) variable + | variable `Set.notMember` seen = + (Set.insert variable seen, reported, duplicates) + | variable `Set.member` reported = + (seen, reported, duplicates) + | otherwise = + ( seen + , Set.insert variable reported + , variable : duplicates + ) + + third (_seen, _reported, duplicates) = + duplicates + +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 + +glossDatatype :: Raw.Datatype -> Gloss Sem.Datatype +glossDatatype rawDatatype = do + let datatypeHeadExpr = Raw.datatypeHeadExpr rawDatatype + rawClauses = Raw.datatypeClauses rawDatatype + datatypeHead <- glossDatatypeHead datatypeHeadExpr + datatypeClauses <- glossDatatypeClause datatypeHead `each` rawClauses + pure (Sem.Datatype datatypeHead datatypeClauses) + where + glossDatatypeHead :: Raw.Expr -> Gloss Sem.SymbolPattern + glossDatatypeHead expr = case expr of + Raw.ExprOp _loc item [] -> + pure (Sem.SymbolPattern item []) + _ -> + throwError (GlossDatatypeHeadError (locate expr)) + + glossDatatypeClause :: Sem.SymbolPattern -> Raw.DatatypeClause -> Gloss Sem.DatatypeClause + glossDatatypeClause datatypeHead rawClause = do + let constructorExpr = Raw.datatypeClauseConstructorExpr rawClause + targetExpr = Raw.datatypeClauseTargetExpr rawClause + rawPremises = Raw.datatypeClausePremises rawClause + datatypeTarget <- glossDatatypeHead targetExpr + unless (datatypeTarget == datatypeHead) do + throwError (GlossDatatypeClauseTargetError (locate targetExpr)) + datatypeClauseConstructor <- glossDatatypeConstructor constructorExpr + datatypeClausePremises <- traverse glossDatatypePremise rawPremises + pure (Sem.DatatypeClause datatypeClauseConstructor datatypeClausePremises) + + glossDatatypeConstructor :: Raw.Expr -> Gloss Sem.SymbolPattern + glossDatatypeConstructor expr = case expr of + Raw.ExprOp _loc item args -> do + vars <- traverse glossConstructorArg args + pure (Sem.SymbolPattern item vars) + _ -> + throwError (GlossDatatypeConstructorError (locate expr)) + + glossConstructorArg :: Raw.Expr -> Gloss VarSymbol + glossConstructorArg = \case + Raw.ExprVar x -> pure x + expr -> throwError (GlossDatatypeConstructorError (locate expr)) + + glossDatatypePremise :: (VarSymbol, Raw.Expr) -> Gloss (VarSymbol, Sem.Expr) + glossDatatypePremise (x, domain) = + (x,) <$> glossExpr domain + +glossBlock :: Raw.Block -> Gloss Sem.Block +glossBlock = \case + Raw.BlockAxiom loc _title marker axiom -> + Sem.BlockAxiom loc marker <$> glossAxiom axiom + Raw.BlockClaim _claimKind loc _title marker lemma -> + Sem.BlockLemma loc marker <$> glossLemma lemma + Raw.BlockProof startLoc proof endLoc -> + Sem.BlockProof startLoc endLoc <$> glossProof proof + Raw.BlockDefn loc _title marker defn -> do + defn' <- glossDefn loc marker defn + whenLeft (isWellformedDefn defn') (\err -> throwError (GlossDefnError loc err marker)) + pure $ Sem.BlockDefn loc marker defn' + Raw.BlockAbbr loc _title marker abbr -> + Sem.BlockAbbr loc marker + <$> glossAbbreviation loc marker abbr + Raw.BlockSig loc _title marker asms sig -> + Sem.BlockSig loc marker <$> glossAsms asms <*> glossSignature sig + Raw.BlockStruct loc _title m structDefn -> + Sem.BlockStruct loc m <$> glossStructDefn structDefn + Raw.BlockData loc _title marker datatype -> + Sem.BlockData loc marker <$> glossDatatype datatype + Raw.BlockInductive loc _title marker ind -> + Sem.BlockInductive loc marker <$> glossInductive ind + + +glossBlocks :: [Raw.Block] -> Gloss [Sem.Block] +glossBlocks blocks = glossBlock `each` blocks |