From d79c85d70fc907858e3af5715bb94e8fdc202155 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 26 Aug 2024 15:33:04 +0200
Subject: I implemented a parsing rule in concrete.hs for local functions and a
 abstract type in abstract.hs for the proof data structure.

---
 source/Syntax/Abstract.hs |  2 +-
 source/Syntax/Concrete.hs | 36 ++++++++++++++++++++++--------------
 2 files changed, 23 insertions(+), 15 deletions(-)

diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index f775b69..6457d42 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -373,7 +373,7 @@ data Proof
     
     
     
-    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol [VarSymbol Expr [VarSymbol] Expr ] Proof
+    | DefineFunctionMathy VarSymbol VarSymbol VarSymbol VarSymbol VarSymbol (NonEmpty [(Expr, Formula)]) Proof
     -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
     -- 
     deriving (Show, Eq, Ord)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index 51cc013..f414ea6 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -354,17 +354,36 @@ grammar lexicon@Lexicon{..} = mdo
     
 
 
+
+
+
     -- Define $f $\fromTo{X}{Y} such that,         
     -- Define function $f: X \to Y$,
     -- \begin{align}
     --      &x \mapsto 3*x      &,  
-    --      &x \mapsto 4*k+x    &, 
+    --      &x \mapsto 4*k    &,    \forall k \in \N. x \in \Set{k}
     -- \end{align}
     -- 
+
+    -- Follwing is the definition right now.
+    -- Define function $f: X \to Y$ such that,
+    -- \begin{cases}
+    --     1 & \text{if } x \in \mathbb{Q}\\
+    --     0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q}
+    --     3 & \text{else}     
+    -- \end{cases}
+
+    functionDefineCase <- rule $ (:[]) <$> ((,) <$> expr <*> (_ampersand *> formula))
     defineFunctionMathy <-  rule    $ DefineFunctionMathy 
                                     <$> (_define *> beginMath *> varSymbol)           -- Define $ f
-                                    <*> _colon *> varSymbol <*> _to *> varSymbol      -- : 'var' \to 'var'
-                                    <*> localFunctionDefinitionAlign 
+                                    <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
+                                    <*> (_to *> varSymbol <* endMath <* _suchThat) 
+                                    -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
+                                    -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
+                                    <*> varSymbol <*> varSymbol <* symbol "="
+                                    <*> many1 functionDefineCase
+                                    <*> proof 
+
 
 
     proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionMathy, qed]
@@ -450,17 +469,6 @@ enumeratedMarked1 :: Prod r Text (Located Token) a -> Prod r Text (Located Token
 enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> label) <*> p) <* end "enumerate" <?> "\"\\begin{enumerate}\\item\\label{...}...\""
 
 
--- &x \mapsto 'someexpr'  &, for x
-localFunctionDefinitionAlign :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (Marker, a)
-localFunctionDefinitionAlign p =    begin "align" *> many1 funDefExp <* end "align" 
-                                    <?> "\"\\begin{algin} &x \\mapsto x+2 , x \\in X \\ \\end{algin}\""
-
-
-funDefExp :: Prod r Text (Located Token) a -> Prod r Text (Located Token) [(Marker, a)]
-funDefExp p = NonEmpty.toList <$> ( _ampersand *> varSymbol <*> funDefExpRange <*> (_ampersand *> varSymbol <* _in) <*> varSymbol) -- the last var should be a expression
-
-funDefRange :: Prod r Text (Located Token) a -> Prod r Text (Located Token) (NonEmpty (Marker, a))
-funDefRange p = _mapsto *> varSymbol -- TODO: this Var has to be changed to a expression
 
 -- This function could be rewritten, so that it can be used directly in the grammar,
 -- instead of with specialized variants.
-- 
cgit v1.2.3