From a253d06a0755c41dd321fc2e235c3332de63a8c7 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 26 Aug 2024 16:55:39 +0200
Subject: Non finished attemped to translate a local function defintion from
 abstract to internal

---
 source/Meaning.hs         | 15 +++++++++++++++
 source/Syntax/Internal.hs |  2 ++
 2 files changed, 17 insertions(+)

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
 
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 44603ad..872ae06 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -436,6 +436,8 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol [(Term, Formula)] Proof
+
 deriving instance Show Proof
 deriving instance Eq   Proof
 deriving instance Ord  Proof
-- 
cgit v1.2.3