diff options
Diffstat (limited to 'source')
| -rw-r--r-- | source/Meaning.hs | 15 | ||||
| -rw-r--r-- | source/Syntax/Internal.hs | 2 |
2 files changed, 17 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 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 |