Abgabe

Submission of Formalisation

14 files changed, 240 insertions, 32 deletions

diff --git a/source/Api.hs b/source/Api.hs
index 95d5c8c..1bdf615 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -17,6 +17,7 @@ module Api
     , dumpTask
     , verify, ProverAnswer(..), VerificationResult(..)
     , exportMegalodon
+    , showFailedTask
     , WithCache(..)
     , WithFilter(..)
     , WithOmissions(..)
@@ -29,6 +30,7 @@ module Api
     , WithParseOnly(..)
     , Options(..)
     , WithDumpPremselTraining(..)
+    , WithFailList(..)
     ) where
 
 
@@ -65,6 +67,7 @@ import Text.Megaparsec hiding (parse, Token)
 import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment
+import Syntax.Abstract (Formula)
 
 -- | Follow all @\\import@ statements recursively and build a theory graph from them.
 -- The @\\import@ statements should be on their own separate line and precede all
@@ -200,7 +203,9 @@ describeToken = \case
     EndEnv _ -> "end of environment"
     _ -> "delimiter"
 
-
+-- | gloss generates internal represantation of the LaTeX files.
+-- First the file will be parsed and therefore checkt for grammer.
+-- 'meaning' then transfer the raw parsed grammer to the internal semantics.
 gloss :: MonadIO io => FilePath -> io ([Internal.Block], Lexicon)
 gloss file = do
     (blocks, lexicon) <- parse file
@@ -285,6 +290,17 @@ exportMegalodon file = do
     pure (Megalodon.encodeBlocks lexicon blocks)
 
 
+
+-- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use
+showFailedTask :: (a, ProverAnswer) -> IO()
+showFailedTask (_, Yes ) = Text.putStrLn ""
+showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("\ESC[31mProver found countermodel: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("\ESC[31mContradictory axioms: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("\ESC[31mOut of resources: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("\ESC[31mError at: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+--showFailedTask (_, _) = Text.putStrLn "Error!"
+
+
 -- | Should we use caching?
 data WithCache = WithoutCache | WithCache deriving (Show, Eq)
 
@@ -312,6 +328,8 @@ pattern WithoutDump = WithDump ""
 
 data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq)
 
+data WithFailList = WithoutFailList | WithFailList deriving (Show, Eq)
+
 
 data Options = Options
     { inputPath :: FilePath
@@ -327,4 +345,5 @@ data Options = Options
     , withVersion :: WithVersion
     , withMegalodon :: WithMegalodon
     , withDumpPremselTraining :: WithDumpPremselTraining
+    , withFailList :: WithFailList
     }
diff --git a/source/Checking.hs b/source/Checking.hs
index dc90264..8bc38a4 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -28,6 +28,7 @@ import Data.HashSet qualified as HS
 import Data.InsOrdMap (InsOrdMap)
 import Data.InsOrdMap qualified as InsOrdMap
 import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Text.IO qualified as Text
@@ -149,7 +150,7 @@ assume asms = traverse_ go asms
         go :: Asm -> Checking
         go = \case
             Asm phi -> do
-                phi' <-  (canonicalize phi)
+                phi' <- canonicalize phi
                 modify \st ->
                     st{ checkingAssumptions = phi' : checkingAssumptions st
                     , fixedVars = freeVars phi' <> fixedVars st
@@ -542,6 +543,56 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
+    DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do
+        -- We have f: X \to Y and x \mapsto ...  
+        -- definition is a nonempty list of (expresssion e, formula phi)
+        -- such that f(x) =  e if phi(x)
+        -- since we do a case deduction in the definition there has to be a check that,
+        -- our domains in the case are a disjunct union of dom(f)
+        assume 
+            [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar)
+            ,Asm (rightUniqueAdj (TermVar funVar))
+            ,Asm (relationNoun (TermVar funVar))]
+
+        goals <- gets checkingGoals
+        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)]
+        tellTasks
+
+        fixed <- gets fixedVars
+        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f)
+        assume (functionSubdomianExpression funVar argVar domVar fixed (NonEmpty.toList definitions)) --behavior on the subdomians
+        setGoals goals
+        checkProof continue
+
+-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..)))
+--  where the phi_{i} are the subdomain statments
+localFunctionGoal :: NonEmpty (Term,Formula) -> Formula
+localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs
+
+
+-- We have our list of expr and forumlas, in this case normaly someone would write
+-- f(x) =  ....cases
+--      & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\)
+--
+-- since we have to bind all globaly free Varibels we generate following asumptions.
+--
+-- For    x \mapsto  expr(x,ys,cs) , if formula(x,ys)        ; here cs are just global constants
+--          ->   \forall x,ys: ( formula(x,ys) => expr(x,ys,cs))
+ 
+
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs
+functionSubdomianExpression _ _ _ _ [] = []
+
+singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> (Term, Formula) -> Asm
+singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let
+    -- boundVar = Set.toList (freeVars expr) in
+    -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)
+    boundVar = fixedV in    
+    let def = forallClosure boundVar (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr))
+    in Asm def
+    
+
 
 checkCalc :: Calc -> Checking
 checkCalc calc = locally do
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index a9fb00d..b8c170e 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -18,7 +18,7 @@ import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment (lookupEnv)
 import System.FilePath.Posix
-
+import qualified Tptp.UnsortedFirstOrder as Syntax.Internal
 
 runCommandLine :: IO ()
 runCommandLine = do
@@ -43,10 +43,12 @@ run = do
     case withDump opts of
         WithoutDump -> skip
         WithDump dir -> do
+            liftIO (Text.putStrLn "\ESC[1;36mCreating Dumpfiles.\ESC[0m")
             let serials = [dir </> show n <.> "p" | n :: Int <- [1..]]
             tasks <- zip serials <$> encodeTasks (inputPath opts)
             createDirectoryIfMissing True dir
             forM_ tasks (uncurry dumpTask)
+            liftIO (Text.putStrLn "\ESC[35mDump ready.\ESC[0m")
     case (withParseOnly opts, withMegalodon opts) of
         (WithParseOnly, _) -> do
             ast <- parse (inputPath opts)
@@ -60,6 +62,7 @@ run = do
             -- A custom E executable can be configured using environment variables.
             -- If the environment variable is undefined we fall back to the
             -- a globally installed E executable.
+            liftIO (Text.putStrLn "\ESC[1;96mStart of verification.\ESC[0m")
             vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE"
             eproverPath <- (?? "eprover") <$> lookupEnv "NAPROCHE_EPROVER"
             let prover = case withProver opts of
@@ -69,23 +72,43 @@ run = do
                     WithDefaultProver -> Provers.vampire vampirePathPath
             let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts)
             result <- verify proverInstance (inputPath opts)
-            liftIO case result of
-                VerificationSuccess -> (Text.putStrLn "Verification successful.")
-                VerificationFailure [] -> error "Empty verification fail"
-                VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of
-                    Yes ->
-                        skip
-                    No tptp -> do
-                        putStrLn "Verification failed: prover found countermodel"
-                        Text.hPutStrLn stderr tptp
-                    ContradictoryAxioms tptp -> do
-                        putStrLn "Verification failed: contradictory axioms"
-                        Text.hPutStrLn stderr tptp
-                    Uncertain tptp -> do
-                        putStrLn "Verification failed: out of resources"
-                        Text.hPutStrLn stderr tptp
-                    Error err ->
-                        Text.hPutStrLn stderr err
+            case withFailList opts of
+                WithoutFailList -> liftIO case result of
+                    VerificationSuccess -> putStrLn "Verification successful."
+                    VerificationFailure [] -> error "Empty verification fail"
+                    VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of
+                        Yes ->
+                            skip
+                        No tptp -> do
+                            putStrLn "Verification failed: prover found countermodel"
+                            Text.hPutStrLn stderr tptp
+                        ContradictoryAxioms tptp -> do
+                            putStrLn "Verification failed: contradictory axioms"
+                            Text.hPutStrLn stderr tptp
+                        Uncertain tptp -> do
+                            putStrLn "Verification failed: out of resources"
+                            Text.hPutStrLn stderr tptp
+                        Error err tptp task -> do
+                            putStr "Error at:"
+
+                            Text.putStrLn task
+                            Text.putStrLn err
+                            Text.putStrLn tptp
+                            
+                WithFailList -> liftIO case result of
+                    VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m"
+                    VerificationFailure [] -> error "Empty verification fail"
+                    VerificationFailure fails -> do
+                        putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m"
+                        traverse_ showFailedTask fails
+                        Text.hPutStrLn stderr "Don't give up!"
+
+
+
+
+
+
+
 
 
 
@@ -104,6 +127,7 @@ parseOptions = do
     withVersion <- withVersionParser
     withMegalodon <- withMegalodonParser
     withDumpPremselTraining <- withDumpPremselTrainingParser
+    withFailList <- withFailListParser
     pure Options{..}
 
 withTimeLimitParser :: Parser Provers.TimeLimit
@@ -160,3 +184,7 @@ withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump
 withMegalodonParser :: Parser WithMegalodon
 withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to Megalodon.")
     <|> pure WithoutMegalodon -- Default to using the cache.
+
+withFailListParser :: Parser WithFailList
+withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.")
+    <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 834d8a6..00a944f 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -605,9 +605,22 @@ glossProof = \case
         if domVar == argVar
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
+    
+    Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do
+        if funVar == funVar2
+            then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
 
+
+glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula)
+glossLocalFunctionExprDef (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/Provers.hs b/source/Provers.hs
index 203ee82..37e02ca 100644
--- a/source/Provers.hs
+++ b/source/Provers.hs
@@ -110,7 +110,7 @@ data ProverAnswer
     | No Text
     | ContradictoryAxioms Text
     | Uncertain Text
-    | Error Text
+    | Error Text Text Text
     deriving (Show, Eq)
 
 nominalDiffTimeToText :: NominalDiffTime -> Text
@@ -163,4 +163,4 @@ recognizeAnswer Prover{..} task tptp answer answerErr =
         | saidNo -> No tptp
         | doesNotKnow -> Uncertain tptp
         | warned -> ContradictoryAxioms tptp
-        | otherwise -> Error (answer <> answerErr)
+        | otherwise -> Error (answer <> answerErr) tptp (Text.pack(show (taskConjectureLabel task)))
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)
diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs
index 705aaa5..c01c249 100644
--- a/source/Test/Golden.hs
+++ b/source/Test/Golden.hs
@@ -39,6 +39,7 @@ testOptions = Api.Options
     , withTimeLimit = Provers.defaultTimeLimit
     , withVersion = Api.WithoutVersion
     , withMegalodon = Api.WithoutMegalodon
+    , withFailList = Api.WithoutFailList
     }
 
 goldenTests :: IO TestTree
diff --git a/source/TheoryGraph.hs b/source/TheoryGraph.hs
index c4887ea..e49bc1f 100644
--- a/source/TheoryGraph.hs
+++ b/source/TheoryGraph.hs
@@ -67,12 +67,12 @@ member :: FilePath -> TheoryGraph -> Bool
 member n (TheoryGraph g) = Map.member n g
 
 
--- | Add a node to the TheoryGraph. This is a noop if the node is already present in the graph.
+-- | Add a node to the TheoryGraph.
 addNode :: FilePath -> TheoryGraph -> TheoryGraph
 addNode a (TheoryGraph g) = TheoryGraph (Map.insertWith Set.union a Set.empty g)
 
 
--- | Add an edge to the TheoryGraph. This is a noop if the edge is already present in the graph.
+-- | Add an edge to the TheoryGraph. This is a loop if the edge is already present in the graph.
 addPrecedes :: Precedes FilePath -> TheoryGraph -> TheoryGraph
 addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertTail e g))
     where
@@ -85,7 +85,9 @@ addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertT
 singleton :: FilePath -> TheoryGraph
 singleton a = TheoryGraph (Map.singleton a Set.empty)
 
-
+-- | Construct a graph, from a list of nodes and edges. 
+-- It takes all nodes a and add the pair (a, emptyset) to the Theorygraph,
+-- afterwards it add all edges between the nodes.
 makeTheoryGraph :: [Precedes FilePath] -> [FilePath] -> TheoryGraph
 makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es
     where
@@ -94,6 +96,8 @@ makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es
 {-# INLINE makeTheoryGraph #-}
 
 
+-- | Construct a graph, from a list @x:xs@,
+-- where @x@ is a pair of theorys @(a,b)@ with @a@ gets imported in @b@.
 fromList :: [Precedes FilePath] -> TheoryGraph
 fromList es = TheoryGraph (Map.fromListWith Set.union es')
     where