summaryrefslogtreecommitdiff
path: root/source/Meaning.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Meaning.hs')
-rw-r--r--source/Meaning.hs13
1 files changed, 13 insertions, 0 deletions
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 834d8a6..00a944f 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -605,9 +605,22 @@ glossProof = \case
if domVar == argVar
then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
else error "mismatched variables in function definition."
+
+ Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do
+ if funVar == funVar2
+ then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+ else error "missmatched function names"
Raw.Calc calc proof ->
Sem.Calc <$> glossCalc calc <*> glossProof proof
+
+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