diff options
Diffstat (limited to 'source/Meaning.hs')
| -rw-r--r-- | source/Meaning.hs | 1772 |
1 files changed, 0 insertions, 1772 deletions
diff --git a/source/Meaning.hs b/source/Meaning.hs deleted file mode 100644 index 04979ce..0000000 --- a/source/Meaning.hs +++ /dev/null @@ -1,1772 +0,0 @@ -{-# LANGUAGE ApplicativeDo #-} -{-# LANGUAGE FunctionalDependencies #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE MultiWayIf #-} -{-# LANGUAGE TupleSections #-} - - -module Meaning where - - -import Base -import Syntax.Abstract (Sign(..)) -import Syntax.Abstract qualified as Raw -import Syntax.Internal (VarSymbol(..), pattern FreshVar) -import Syntax.Internal qualified as Sem -import Syntax.LexicalPhrase (unsafeReadPhrase) -import 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 (foldr cons (Sem.EmptySet loc) es') - where - cons x y = Sem.TermSymbol loc (Sem.SymbolMixfix Raw.ConsSymbol) [x, y] - - -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 |