{-# 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