Non finished attemped to translate a local

function defintion from abstract to internal

1 files changed, 15 insertions, 0 deletions

diff --git a/source/Meaning.hs b/source/Meaning.hs
index 834d8a6..30e13f8 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -605,9 +605,24 @@ glossProof = \case
         if domVar == argVar
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
+    
+    Raw.DefineFunctionMathy funVar domVar ranVar funVar2 argVar definitions proof -> do
+        if funVar /= funVar2
+            then error "missmatched function names"
+            else Sem.DefineFunctionMathy funVar domVar ranVar argVar <*> glossLocalFunctionExprEach definitions <*> glossProof proof
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
 
+glossLocalFunctionExprEach :: NonEmpty [(Raw.Expr, Raw.Formula)]-> Gloss [(Sem.Term, Sem.Formula)]
+glossLocalFunctionExprEach def = pure ( glossLocalFunctionExpr `each` def )
+
+glossLocalFunctionExpr :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula)
+glossLocalFunctionExpr (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