update: some further Eval functions

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

app/Main.hs

@@ -1,3 +1,6 @@
+{-
+
+-}
 module Main (main) where
 import FMCt (parseFMC, eval1, printStack, printOutput)
 import Control.Monad(void, forM_)

cabal.project

@@ -1,6 +1,9 @@
 packages: ./.
 
-documentation:       True
-haddock-html:        True
-haddock-executables: True
-profiling: True                
+documentation:        True                    
+
+haddock-html:         True
+
+haddock-executables:  True
+
+profiling:            True                

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

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)

src/FMCt/Evaluator.hs

@@ -2,19 +2,25 @@
 module FMCt.Evaluator
   ( eval
   , eval1
+  , tCheck'
+  , eval1'
+  , evalToString
   , tryEval1
   , State
   , Binds
   , Memory
   , 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

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.