From 3869dab92bf7e89e1a70ef3956a7fbd1d0d2e555 Mon Sep 17 00:00:00 2001
From: cstml <cstmlcodes@gmail.com>
Date: Wed, 28 Jul 2021 14:46:05 +0100
Subject: [PATCH] update: some further Eval functions

---
 FMCt.cabal              | 10 +++-------
 app/Main.hs             |  3 +++
 cabal.project           | 11 +++++++----
 makefile                |  3 ++-
 src/FMCt.hs             |  2 +-
 src/FMCt/Evaluator.hs   | 33 +++++++++++++++++++++++++++++++++
 src/FMCt/TypeChecker.hs |  4 +++-
 7 files changed, 52 insertions(+), 14 deletions(-)

diff --git a/FMCt.cabal b/FMCt.cabal
index c375e18..ec9a539 100644
--- a/FMCt.cabal
+++ b/FMCt.cabal
@@ -1,6 +1,6 @@
 cabal-version:          2.4                      
 name:                   FMCt                      
-version:                0.1.0.0                      
+version:                0.2.0.0                      
 license:                BSD-3-Clause                      
 license-file:           LICENSE                      
 author:                 Vlad Posmangiu Luchian                     
@@ -26,7 +26,8 @@ common common-specs
                         mtl,
                         parsec,
                         text,
-                        transformers
+                        transformers,
+                        deepseq
                         
   default-extensions:   OverloadedStrings,
                         LambdaCase
@@ -45,11 +46,6 @@ library
                         FMCt.Pretty
                         FMCt.Syntax
                         FMCt.TypeChecker
-
-                        
-  main:                 FMCt
-
---  other-modules:        
                         
 executable FMCt         
   import:               common-specs
diff --git a/app/Main.hs b/app/Main.hs
index 0235b1c..ed86854 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,3 +1,6 @@
+{-
+
+-}
 module Main (main) where
 import FMCt (parseFMC, eval1, printStack, printOutput)
 import Control.Monad(void, forM_)
diff --git a/cabal.project b/cabal.project
index a82632d..c2ff3e4 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,6 +1,9 @@
 packages: ./.
   
-documentation:       True
-haddock-html:        True
-haddock-executables: True
-profiling: True                
\ No newline at end of file
+documentation:        True                    
+  
+haddock-html:         True
+                     
+haddock-executables:  True
+                     
+profiling:            True                
\ No newline at end of file
diff --git a/makefile b/makefile
index daa8d76..0287ca5 100644
--- a/makefile
+++ b/makefile
@@ -35,4 +35,5 @@ reformat:
 
 # Make the documentation
 haddock-generate:
-	cabal haddock ./src/**/*.hs -o ./doc -h && firefox ./doc/index.html
+	cabal new-haddock && \
+  firefox ./dist-newstyle/build/x86_64-linux/ghc-8.6.5/FMCt-0.1.0.0/doc/html/FMCt/index.html
diff --git a/src/FMCt.hs b/src/FMCt.hs
index c7f9a5e..b240c15 100644
--- a/src/FMCt.hs
+++ b/src/FMCt.hs
@@ -4,7 +4,7 @@ module FMCt
 where
 
 import FMCt.Parsing     as X ( parseFMC, parseType, parseFMCtoString )
-import FMCt.Evaluator   as X ( eval, eval1 ) 
+import FMCt.Evaluator   as X ( eval, eval1, eval1', tCheck', evalToString ) 
 import FMCt.Examples    as X ( examplesList )
 import FMCt.TypeChecker as X ( typeCheck )
 import FMCt.Pretty      as X ( printStack, printOutput)
diff --git a/src/FMCt/Evaluator.hs b/src/FMCt/Evaluator.hs
index 66ee5ce..1ef908a 100644
--- a/src/FMCt/Evaluator.hs
+++ b/src/FMCt/Evaluator.hs
@@ -2,6 +2,9 @@
 module FMCt.Evaluator
   ( eval
   , eval1
+  , tCheck'
+  , eval1'
+  , evalToString
   , tryEval1
   , State
   , Binds
@@ -9,12 +12,15 @@ module FMCt.Evaluator
   , emptyMem
   ) where
 
+import Control.DeepSeq
 import Control.Exception (try, IOException, catch)
 import Data.Map (Map, (!?))
 import FMCt.Syntax (Tm(..), Lo(..), Vv, Type(..))
 import Text.Read (readMaybe)
+import FMCt.TypeChecker (typeCheck, Derivation, TError)
 import qualified Control.Exception as E
 import qualified Data.Map as M
+import Control.Monad (void)
 
 -- | Memory is a Map between a location and a list of Terms.
 type Memory = Map Lo [Tm]
@@ -107,6 +113,33 @@ eval t = foldl1 (flip (.)) (evaluate <$> t) emptyMem
 eval1 :: Tm -> State
 eval1 t = evaluate t emptyMem
 
+-- | Takes 1 term, typechecks and type checks it. 
+tCheck' :: Tm
+        -- ^ Term to be TypeChecked
+        -> IO (Either TError Tm)
+        -- ^ IO Monad returning the result of the typecheck and the error or 
+tCheck' term = try $ do
+  res <- E.evaluate $ show $ typeCheck term
+  pure term
+
+-- | Evaluate with the typechecker and fail safely.
+eval1' :: Tm
+       -- ^ Term to be evaluated.
+       -> IO State
+       -- ^ Returns an empty state if the term cannot be typed checked.
+eval1' term = do
+  tc <- tCheck' term
+  case tc of
+    Left  e -> putStrLn "Caugh Error: " >> print  e >> pure emptyMem
+    Right _ -> pure $ eval1 term
+
+evalToString :: Tm -> IO String
+evalToString  term = do
+  tc <- tCheck' term
+  case tc of
+    Left e -> pure $ show e
+    Right x -> pure . show $ eval1 term
+
 -- | Evaluates a term and fails safely.
 tryEval1 :: Tm -> IO (Either IOException State)
 tryEval1 term = do
diff --git a/src/FMCt/TypeChecker.hs b/src/FMCt/TypeChecker.hs
index 2974648..25fcf14 100644
--- a/src/FMCt/TypeChecker.hs
+++ b/src/FMCt/TypeChecker.hs
@@ -7,9 +7,11 @@ module FMCt.TypeChecker
   , fuse
   , consumes
   , consume
+  , Derivation
   )
 where
 
+import Control.DeepSeq
 import FMCt.Syntax
 import Data.List (sort)
 import qualified Data.Map as M
@@ -19,7 +21,7 @@ import Data.Monoid
 import Control.Monad.State
 import Control.Exception
 
--- | TypeChecking Errors.
+-- | Typechecking Errors.
 data TError
   = ErrSimple   String          -- ^ A Simple Error.
   | ErrUndefT   String          -- ^ An undefined Type.