Abgabe

Submission of Formalisation

7 files changed, 99 insertions, 7 deletions

diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 4aa8623..c8022c7 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -369,6 +369,13 @@ data Proof
     -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
     -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
     -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).
+    
+    
+    
+    
+    | DefineFunctionLocal VarSymbol VarSymbol Expr 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)
 
 -- | An inline justification.
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 3a8b3d6..4b43bc6 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -27,13 +27,15 @@ scanChunk ltoks =
         matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos)
     in case ltoks of
         Located{startPos = pos, unLocated = BeginEnv "definition"} : _ ->
-            matchOrErr definition "definition" (pos)
+            matchOrErr definition "definition" pos
         Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
             matchOrErr abbreviation "abbreviation" pos
         Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ ->
             matchOrErr struct "struct definition" pos
         Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
             matchOrErr inductive "inductive definition" pos
+        --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
+        --    matchOrErr signatureIntro "signature" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
@@ -85,6 +87,18 @@ abbreviation = do
     skipUntilNextLexicalEnv
     pure [lexicalItem m]
 
+signatureIntro ::  RE Token [ScannedLexicalItem]  --since signiture is a used word of haskell we have to name it diffrentliy 
+signatureIntro = do
+    sym (BeginEnv "signature")
+    few notEndOfLexicalEnvToken
+    m <- label
+    few anySym
+    lexicalItem <- head
+    few anySym
+    sym (EndEnv "signature")
+    skipUntilNextLexicalEnv
+    pure [lexicalItem m]
+
 label :: RE Token Marker
 label = msym \case
     Label m -> Just (Marker m)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index b51b738..9b947b0 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -351,8 +351,42 @@ grammar lexicon@Lexicon{..} = mdo
 
     define           <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof
     defineFunction   <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*>  expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof
+    
 
-    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed]
+
+
+
+
+    -- Define $f $\fromTo{X}{Y} such that,         
+    -- Define function $f: X \to Y$,
+    -- \begin{align}
+    --      &x \mapsto 3*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 $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
+    defineFunctionLocal <-  rule    $ DefineFunctionLocal 
+                                    <$> (_define *> beginMath *> varSymbol)           -- Define $ f
+                                    <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
+                                    <*> (_to *> expr <* endMath <* _suchThat) 
+                                    -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
+                                    -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
+                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq )
+                                    <*> cases (many1 functionDefineCase) <* endMath <* optional _dot 
+                                    <*> proof
+
+
+
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed]
 
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
@@ -436,7 +470,6 @@ enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> lab
 
 
 
-
 -- This function could be rewritten, so that it can be used directly in the grammar,
 -- instead of with specialized variants.
 --
@@ -611,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}
 align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 align body = begin "align*" *> body <* end "align*"
 
+cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+cases body = begin "cases" *> body <* end "cases"
+
 
 maybeVarToken :: Located Token -> Maybe VarSymbol
 maybeVarToken ltok = case unLocated ltok of
diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs
index 135cdac..b507e7e 100644
--- a/source/Syntax/Concrete/Keywords.hs
+++ b/source/Syntax/Concrete/Keywords.hs
@@ -108,7 +108,7 @@ _either = word "either" ? "either"
 _equipped :: Prod r Text (Located Token) SourcePos
 _equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with"
 _every :: Prod r Text (Located Token) SourcePos
-_every = (word "every") ? "every"
+_every = word "every" ? "every"
 _exist :: Prod r Text (Located Token) SourcePos
 _exist = word "there" <* word "exist" ? "there exist"
 _exists :: Prod r Text (Located Token) SourcePos
@@ -124,7 +124,7 @@ _for = word "for" ? "for"
 _forAll :: Prod r Text (Located Token) SourcePos
 _forAll = (word "for" <* word "all") <|> word "all" ? "all"
 _forEvery :: Prod r Text (Located Token) SourcePos
-_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every"
+_forEvery = (word "for" <* word "every") <|> word "every" ? "for every"
 _have :: Prod r Text (Located Token) SourcePos
 _have = word "we" <* word "have" <* optional (word "that") ? "we have"
 _if :: Prod r Text (Located Token) SourcePos
@@ -220,3 +220,9 @@ _in :: Prod r Text (Located Token) SourcePos
 _in = symbol "∈" <|> command "in" ? "\\in"
 _subseteq :: Prod r Text (Located Token) SourcePos
 _subseteq = command "subseteq" ? "\\subseteq"
+_to :: Prod r Text (Located Token) SourcePos
+_to = command "to" ? "\\to"
+_mapsto :: Prod r Text (Located Token) SourcePos
+_mapsto = command "mapsto" ? "\\mapsto"
+_ampersand :: Prod r Text (Located Token) SourcePos
+_ampersand = symbol "&" ? "&"
\ No newline at end of file
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 44603ad..c098380 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -324,6 +324,16 @@ makeDisjunction = \case
     [] -> Bottom
     es -> List.foldl1' Or es
 
+makeIff :: [ExprOf a] -> ExprOf a
+makeIff = \case
+    [] -> Bottom
+    es -> List.foldl1' Iff es
+    
+makeXor :: [ExprOf a] -> ExprOf a
+makeXor = \case
+    [] -> Bottom
+    es -> List.foldl1' Xor es
+
 finiteSet :: NonEmpty (ExprOf a) -> ExprOf a
 finiteSet = foldr cons EmptySet
     where
@@ -436,6 +446,8 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
+    | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
+
 deriving instance Show Proof
 deriving instance Eq   Proof
 deriving instance Ord  Proof
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index b5e4f58..4fe8730 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -95,6 +95,7 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>)
         builtinIdentifiers = identifier <$>
             [ "emptyset"
             , "naturals"
+            , "integers"
             , "rationals"
             , "reals"
             , "unit"
@@ -109,6 +110,9 @@ prefixOps =
     , ([Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "fst"))
     , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd"))
     , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
+    , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
+    , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv"))
+    , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs"))    
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index cb3f4cb..53e1e6a 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:))
                 Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:))
+                --Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
@@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:))
+                --Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:))
                 Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:))
                 Just t -> goMath (f . (t:))
@@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof
 -- | Parses a single normal mode token.
 tok :: Lexer (Located Token)
 tok =
-    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
+    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
 
 -- | Parses a single math mode token.
 mathToken :: Lexer (Located Token)
 mathToken =
-    var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
+    var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
 
 beginText :: Lexer (Located Token)
 beginText = lexeme do
@@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do
     setMathMode
     pure (BeginEnv "align*")
 
+casesBegin :: Lexer (Located Token)
+casesBegin = guardM isTextMode *> lexeme do
+    Char.string "\\begin{cases}"
+    --setMathMode
+    pure (BeginEnv "cases")
 
 -- | Parses a single end math token.
 mathEnd :: Lexer (Located Token)
@@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do
     setTextMode
     pure (EndEnv "align*")
 
+casesEnd :: Lexer (Located Token)
+casesEnd = guardM isMathMode *> lexeme do
+    Char.string "\\end{cases}"
+    --setTextMode
+    pure (EndEnv "cases")
+
 
 -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on.
 word :: Lexer (Located Token)