Exp serialization

4 files changed, 206 insertions, 63 deletions

diff --git a/src/LambdaCube/Compiler.hs b/src/LambdaCube/Compiler.hs
index 4d5213c3..e92688d6 100644
--- a/src/LambdaCube/Compiler.hs
+++ b/src/LambdaCube/Compiler.hs
@@ -23,7 +23,11 @@ module LambdaCube.Compiler
     , plainShow
     , prettyShowUnlines
     ) where
+import qualified Data.ByteString.Char8 as BS
 
+import Data.Binary
+import Data.Time.Clock
+import Text.Printf
 import Data.List
 import Data.Maybe
 import Data.Function
@@ -37,19 +41,21 @@ import Control.Monad.Except
 import Control.Monad.Catch
 import Control.Arrow hiding ((<+>))
 import System.FilePath
+import System.Directory
+import System.IO.Unsafe
 --import Debug.Trace
 
 import LambdaCube.IR as IR
 import LambdaCube.Compiler.Pretty hiding ((</>))
 import LambdaCube.Compiler.DesugaredSource (Module_(..), Export(..), ImportItems (..), Stmt)
 import LambdaCube.Compiler.Parser (runDefParser, parseLC, DesugarInfo, Module)
-import LambdaCube.Compiler.InferMonad (GlobalEnv, initEnv)
+import LambdaCube.Compiler.InferMonad (GlobalEnv, initEnv, closeGlobalEnv)
 import LambdaCube.Compiler.Infer (inference)
 import LambdaCube.Compiler.CoreToIR
 
 import LambdaCube.Compiler.Utils
 import LambdaCube.Compiler.DesugaredSource as Exported (FileInfo(..), Range(..), SPos(..), pattern SPos, SIName(..), pattern SIName, sName, SI(..))
-import LambdaCube.Compiler.Core as Exported (mkDoc, Exp, ExpType(..), pattern ET, outputType, boolType, trueExp, hnf)
+import LambdaCube.Compiler.Core as Exported (mkDoc, Exp, ExpType(..), pattern ET, outputType, boolType, trueExp, hnf, closeExp)
 import LambdaCube.Compiler.InferMonad as Exported (errorRange, listAllInfos, listAllInfos', listTypeInfos, listErrors, listWarnings, listTraceInfos, Infos, Info(..))
 --import LambdaCube.Compiler.Infer as Exported ()
 
@@ -89,7 +95,7 @@ type ModuleFetcher m = Maybe FilePath -> Either FilePath MName -> m (Either Doc
 ioFetch :: MonadIO m => [FilePath] -> ModuleFetcher (MMT m x)
 ioFetch paths' imp n = do
     preludePath <- (</> "lc") <$> liftIO getDataDir
-    let paths = map (id &&& id) paths' ++ [(preludePath, preludePath)]
+    let paths = map (id &&& id) paths' ++ [(preludePath, {-"<<installed-prelude-path>>"-}preludePath)]
         find ((x, (x', mn)): xs) = liftIO (readFileIfExists x) >>= maybe (find xs) (\src -> return $ Right (x', mn, liftIO src))
         find [] = return $ Left $ "can't find" <+> either (("lc file" <+>) . text) (("module" <+>) . text) n
                                   <+> "in path" <+> hsep (text . snd <$> paths)
@@ -155,33 +161,98 @@ loadModule ex imp mname_ = do
                                     (\(ds, ge) -> Right (ds{-todo: filter-}, Map.filterWithKey (\k _ -> filterImports is k) ge))
                                     e)
                                 dsge
-
-            let (res, err) = case sequence ms of
-                  Left err -> (ex mempty, Left $ pShow err)
+            ---------------
+            let (res, err, g_env, defs) = case sequence ms of
+                  Left err -> (ex mempty, Left $ pShow err, mempty, mempty)
                   Right ms@(mconcat -> (ds, ge)) -> case runExcept $ runDefParser ds $ definitions e of
-                    Left err -> (ex mempty, Left $ pShow err)
-                    Right (defs, warnings, dsinfo) -> (,) (ex (map ParseWarning warnings ++ is, defs)) $ case res of
-                      Left err -> Left $ pShow err
-                      Right (mconcat -> newge) ->
-                        right mconcat $ forM (fromMaybe [ExportModule $ SIName mempty mname] $ moduleExports e) $ \case
-                            ExportId (sName -> d) -> case Map.lookup d newge of
-                                Just def -> Right (mempty{-TODO-}, Map.singleton d def)
-                                Nothing  -> Left $ text d <+> "is not defined"
-                            ExportModule (sName -> m) | m == mname -> Right (dsinfo, newge)
-                            ExportModule m -> case [ x | ((m', _), x) <- zip (moduleImports e) ms, m' == m] of
-                                [x] -> Right x
-                                []  -> Left $ "empty export list in module" <+> text fname -- m, map fst $ moduleImports e, mname)
-                                _   -> error "export list: internal error"
+                    Left err -> (ex mempty, Left $ pShow err, mempty, mempty)
+                    Right (defs, warnings, dsinfo) -> ((ex (map ParseWarning warnings ++ is, defs)), res_1, g_env_1, defs) -- defs g_env_1
                      where
-                        (res, is) = runWriter . flip runReaderT (extensions e, initEnv <> ge) . runExceptT $ inference defs
-
-            return $ Right (e, res, err)
+                        defs_cached = unsafePerformIO $ do
+                          let filename = printf "%s.def_bin" $ takeFileName fname :: String
+                          doesFileExist filename >>= \case
+                            True  -> do
+                              BS.putStrLn $ BS.pack $ printf "load %s" filename
+                              decodeFile filename
+                            False -> do
+                              BS.putStrLn $ BS.pack $ printf "save %s" filename
+                              encodeFile filename defs
+                              pure defs
+                        (res, is) = runWriter . flip runReaderT (extensions e, initEnv <> ge) . runExceptT $ inference defs --_cached
+
+                        (g_env_1, res_1) = case res of
+                              Left err -> (mempty, Left $ pShow err)
+                              Right (mconcat -> newge) -> --do
+                                --writeFile (printf "%s.exp" fname) $ show newge
+                                (newge, right mconcat $ forM (fromMaybe [ExportModule $ SIName mempty mname] $ moduleExports e) $ \case
+                                    ExportId (sName -> d) -> case Map.lookup d newge of
+                                        Just def -> Right (mempty{-TODO-}, Map.singleton d def)
+                                        Nothing  -> Left $ text d <+> "is not defined"
+                                    ExportModule (sName -> m) | m == mname -> Right (dsinfo, newge)
+                                    ExportModule m -> case [ x | ((m', _), x) <- zip (moduleImports e) ms, m' == m] of
+                                        [x] -> Right x
+                                        []  -> Left $ "empty export list in module" <+> text fname -- m, map fst $ moduleImports e, mname)
+                                        _   -> error "export list: internal error")
+            ---------------
+            let writeResult = do
+                  let filename = printf "%s.exp" $ takeFileName fname :: String
+                      filename_closed = printf "%s.exp.closed" $ takeFileName fname :: String
+                      filename_closed_tr = printf "%s.exp.closed.tr" $ takeFileName fname :: String
+                      filename_keys = printf "%s.exp.keys" $ takeFileName fname :: String
+                  --putStrLn $ printf "write result! %d %s" ({-Map.size-}length g_env) filename
+                  writeFile filename_keys $ unlines $ map show $ Map.keys g_env
+                  let (g_env_ok, g_env_closed, g_env_closed_tr) = unzip3
+                        [ ( printf "%s :: %s\n%s = %s\n\n" k ty_s k v_s :: String
+                          , printf "%s :: %s\n%s = %s\n\n" k c_ty_s k c_v_s :: String
+                          , printf "%s :: %s\n%s = %s\n\n" k tr_c_ty_s k tr_c_v_s :: String
+                          )
+                        | (k,(v, v_ty, v_si)) <- Map.toList g_env
+                        , let ty_s = show $ mkDoc (False,False) $ v_ty
+                        , let v_s = show $ mkDoc (False,True) $ v
+                        , let c_v_ty = closeExp v_ty
+                        , let c_v = closeExp v
+                        , let c_ty_s = show $ mkDoc (False,False) c_v_ty
+                        , let c_v_s = show $ mkDoc (False,True) $ c_v
+                        , let tr_c_ty_s = show $ mkDoc (False,False) $ tr_exp c_v_ty
+                        , let tr_c_v_s = show $ mkDoc (False,True) $ tr_exp c_v
+                        ]
+                      tr_exp :: Exp -> Exp
+                      tr_exp = decode . encode
+                  {-
+                  writeFile filename (concat $ g_env_ok :: String)
+                  writeFile filename_closed (concat $ g_env_closed :: String)
+                  writeFile filename_closed_tr (concat $ g_env_closed_tr :: String)
+                  -}
+                  BS.putStrLn $ BS.pack $ printf "write %s" (printf "%s.env_bin - START" $ takeFileName fname :: String)
+                  encodeFile (printf "%s.env_bin" $ takeFileName fname :: String) $ closeGlobalEnv g_env
+                  BS.putStrLn $ BS.pack $ printf "write %s" (printf "%s.env_bin - DONE" $ takeFileName fname :: String)
+                  
+                  -- TODO: guarded pShow save to file for g_env exps and closed g_env exps
+
+                writeParsedDefs = do
+                  BS.putStrLn $ BS.pack $ printf "defs count: %d" (length defs)
+                  let filename = printf "%s.defs" $ takeFileName fname :: String
+                  writeFile filename $ unlines $ map ((++ "\n"). show . pShow) defs
+                  encodeFile (printf "%s.def_bin" $ takeFileName fname :: String) defs
+                  {-
+                    Experiment:
+                      Stmt/SExp - can be serialized
+                      Exp - explodes ; must be the inference algorithm
+                  -}
+                debugAction = do
+                  printTimeDiff (fname ++ " Defs") writeParsedDefs
+                  printTimeDiff (fname ++ " Exp") writeResult
+                  --when (fname == "./SampleMaterial.lc") $
+                  --  fail "stop"
+            return $ unsafePerformIO (debugAction >> pure (Right (e, res, err)))
+            --return (Right (e, res, err))
         modify $ \(Modules nm im ni) -> Modules nm (IM.insert fid (fi, (src, res)) im) ni
         return $ Right (fi, (src, res))
   where
     filterImports (ImportAllBut ns) = not . (`elem` map sName ns)
     filterImports (ImportJust ns) = (`elem` map sName ns)
 
+
 -- used in runTests
 getDef :: MonadMask m => FilePath -> SName -> Maybe Exp -> MMT m (Infos, [Stmt]) ((Infos, [Stmt]), Either Doc (FileInfo, Either Doc ExpType))
 getDef = getDef_ id
@@ -224,7 +295,7 @@ preCompile paths paths' backend mod = do
       where
         compile src = runMM fetch $ do
             let pname = "." </> "Prelude.lc"
-            modify $ \(Modules nm im ni) -> Modules (Map.insert pname ni nm) (IM.insert ni (FileInfo ni pname "Prelude", prelude) im) (ni+1)
+            modify $ \(Modules nm im ni) -> Modules (Map.insert pname ni nm) (IM.insert ni (FileInfo ni pname "Prelude" , prelude) im) (ni+1)
             (snd &&& fst) <$> compilePipeline' ex backend "Main"
           where
             fetch imp = \case
diff --git a/src/LambdaCube/Compiler/Core.hs b/src/LambdaCube/Compiler/Core.hs
index 8e97c6b2..02dd6c50 100644
--- a/src/LambdaCube/Compiler/Core.hs
+++ b/src/LambdaCube/Compiler/Core.hs
@@ -13,6 +13,8 @@
 --{-# OPTIONS_GHC -fno-warn-unused-binds #-}  -- TODO: remove
 module LambdaCube.Compiler.Core where
 
+import Text.Printf
+--import Debug.Trace
 import Data.Binary
 import GHC.Generics (Generic)
 
@@ -88,7 +90,7 @@ data Exp
     | RHS    Exp{-always in hnf-}
     | Let_   FreeVars ExpType Exp
     | Up_    FreeVars [Int] Exp
-    | STOP
+    | STOP   String
     deriving Generic
 
 data Neutral
@@ -195,21 +197,21 @@ tCon_ k s i t a     = Con (ConName (FTag s) i t) k a
 pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a
 
 pattern TTyCon0 s  <- TyCon (TyConName (FTag s) _ _ _ _) []
-tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) []
+tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (FTag s) (STOP "TTyCon0-B") 0) []
 
 pattern a :~> b = Pi Visible a b
 
 delta = ELit (LString "<<delta function>>") -- TODO: build an error call
 
-pattern TConstraint <- TTyCon0 F'Constraint where TConstraint = tTyCon0 F'Constraint $ error "cs 1"
+pattern TConstraint <- TTyCon0 F'Constraint where TConstraint = tTyCon0 F'Constraint []
 pattern Unit        <- TTyCon0 F'Unit      where Unit        = tTyCon0 F'Unit [Unit]
-pattern TInt        <- TTyCon0 F'Int       where TInt        = tTyCon0 F'Int $ error "cs 1"
-pattern TNat        <- TTyCon0 F'Nat       where TNat        = tTyCon0 F'Nat $ error "cs 3"
-pattern TBool       <- TTyCon0 F'Bool      where TBool       = tTyCon0 F'Bool $ error "cs 4"
-pattern TFloat      <- TTyCon0 F'Float     where TFloat      = tTyCon0 F'Float $ error "cs 5"
-pattern TString     <- TTyCon0 F'String    where TString     = tTyCon0 F'String $ error "cs 6"
-pattern TChar       <- TTyCon0 F'Char      where TChar       = tTyCon0 F'Char $ error "cs 7"
-pattern TOrdering   <- TTyCon0 F'Ordering  where TOrdering   = tTyCon0 F'Ordering $ error "cs 8"
+pattern TInt        <- TTyCon0 F'Int       where TInt        = tTyCon0 F'Int []
+pattern TNat        <- TTyCon0 F'Nat       where TNat        = tTyCon0 F'Nat []
+pattern TBool       <- TTyCon0 F'Bool      where TBool       = tTyCon0 F'Bool []
+pattern TFloat      <- TTyCon0 F'Float     where TFloat      = tTyCon0 F'Float []
+pattern TString     <- TTyCon0 F'String    where TString     = tTyCon0 F'String []
+pattern TChar       <- TTyCon0 F'Char      where TChar       = tTyCon0 F'Char []
+pattern TOrdering   <- TTyCon0 F'Ordering  where TOrdering   = tTyCon0 F'Ordering []
 pattern TVec a b    <- TyConN (FTag F'VecS) [a, b]
 
 pattern Empty s    <- TyCon (TyConName (FTag F'Empty) _ _ _ _) (HString{-hnf?-} s: _)
@@ -263,7 +265,7 @@ mkOrdering x = case x of
     GT -> tCon FGT 2 TOrdering []
 
 conTypeName :: ConName -> TyConName
-conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n
+conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n ; STOP m -> error $ "STOP " ++ m
 
 mkFun_ md (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f md as
 mkFun_ md f@(FunName _ _ (ExpDef e) _) xs _ = Neut $ Fun_ md f xs $ hnf $ foldlrev app_ e xs
@@ -283,7 +285,7 @@ reduce _ = Nothing
 hnf (Reduced y) = hnf y  -- TODO: review hnf call here
 hnf a = a
 
-outputType = tTyCon0 F'Output $ error "cs 9"
+outputType = tTyCon0 F'Output []
 
 -- TODO: remove
 boolType = TBool
@@ -390,6 +392,7 @@ instance HasFreeVars Exp where
         TyCon_ c _ _ -> c
         Let_ c _ _ -> c
 
+        STOP{} -> mempty
         TType_ _ -> mempty
         ELit{} -> mempty
         Neut x -> getFreeVars x
@@ -438,6 +441,7 @@ instance MkDoc Exp where
         Neut x          -> mkDoc pr x
         Let a b         -> shLet_ (pShow a) (pShow b)
         RHS x           -> text "_rhs" `DApp` mkDoc pr x
+        STOP x          -> text $ "STOP " ++ x
 
 pattern FFix f <- Fun (FunName (FTag FprimFix) _ _ _) [f, _] _
 
@@ -692,40 +696,71 @@ instance NType Lit where
         LString _ -> TString
         LChar _   -> TChar
 
+{-
+data ConName       = ConName       FName Int  Type
+data TyConName     = TyConName     FName Int  Type   [(ConName, Type)] CaseFunName
+data FunName       = FunName       FName Int  FunDef Type
+data CaseFunName   = CaseFunName   FName Type Int
+data TyCaseFunName = TyCaseFunName FName Type
+data FunDef
+    = DeltaDef !Int (FreeVars -> [Exp] -> Exp)
+    | NoDef
+    | ExpDef Exp
+-}
 
-closeTyConName (TyConName fname ints type_ cons caseFunName)
- -- = TyConName fname ints (closeExp type_) [(closeConName n, closeExp t) | (n,t) <- cons] (closeCaseFunName caseFunName)
-  = TyConName fname ints STOP [(closeConName n, STOP) | (n,t) <- cons] (closeCaseFunName caseFunName)
+trace :: String -> a -> a
+trace _ = id
 
-closeTyCaseFunName (TyCaseFunName fname type_)
- -- = TyCaseFunName fname (closeExp type_)
-  = TyCaseFunName fname STOP
+closeType_ msg fuel _ = STOP $ msg ++ " " ++ show fuel
 
-closeConName (ConName fname ordinal type_)
- -- = ConName fname ordinal (closeExp type_)
-  = ConName fname ordinal STOP
+-- TODO: check MkDoc 
+closeTyConName fuel (TyConName fname ints type_ cons caseFunName)
+  = trace (printf "TyConName %s %d" (show fname) fuel) $ TyConName fname ints (closeType_ "TyConName" fuel type_) [{-(closeConName fuel n, closeType_ "TyConName con" fuel t) | (n,t) <- cons-}] (closeCaseFunName fuel caseFunName)
 
-closeCaseFunName (CaseFunName fname type_ int)
- -- = CaseFunName fname (closeExp type_) int
-  = CaseFunName fname STOP int
+closeTyCaseFunName fuel (TyCaseFunName fname type_)
+  = trace (printf "TyCaseFunName %s %d" (show fname) fuel) $ TyCaseFunName fname (closeType_ "TyCaseFunName" fuel type_)
 
-closeFunName (FunName fname int funDef type_)
- -- = FunName fname int (closeFunDef funDef) (closeExp type_)
-  = FunName fname int (closeFunDef funDef) STOP
+closeConName fuel (ConName fname ordinal type_)
+  = trace (printf "ConName %s %d" (show fname) fuel) $ ConName fname ordinal (closeType fuel type_) --(STOP "ConName")
+
+closeCaseFunName fuel (CaseFunName fname type_ int)
+  = trace (printf "CaseFunName %s %d" (show fname) fuel) $ CaseFunName fname (closeType_ "CaseFunName" fuel type_) int
+
+closeFunName fuel (FunName fname int funDef type_)
+  = trace (printf "FunName %s %d" (show fname) fuel) $ FunName fname int (closeFunDef funDef) (closeType_ "FunName" fuel type_)
 
 closeFunDef = \case
-  ExpDef exp -> ExpDef STOP
-  --ExpDef exp -> ExpDef (closeExp exp)
+  ExpDef exp -> ExpDef (closeExp exp)
   x -> x
 
+_maxFuel = 25 :: Int -- 6
+
+closeType :: Int -> Exp -> Exp
+--closeType fuel | fuel <= 0 = \_ -> STOP "out of fuel"
+closeType fuel = \case
+  Lam_   freeVars exp -> tr "Lam_" $ Lam_ freeVars (closeType_ "Lam_" _fuel exp)
+  Con_   freeVars conName noErasedApplied argsReversed -> tr "Con_" $ Con_ freeVars (closeConName _fuel conName) noErasedApplied []
+  TyCon_ freeVars tyConName argsReversed -> tr "TyCon_" $ TyCon_ freeVars (closeTyConName _fuel tyConName) []
+  Pi_    freeVars visibility exp1 exp2 -> tr "Pi_" $ Pi_ freeVars visibility (closeType_ "Pi_ 1" _fuel exp1) (closeType _fuel exp2)
+  Neut   neutral -> STOP "Neut"
+  RHS    exp -> tr "RHS" $ RHS (closeType_ "RHS" _fuel exp)
+  Let_   freeVars expType exp -> (STOP "Let_")
+  Up_    freeVars ints exp -> tr "Up_" $ Up_ freeVars ints (closeType_ "Up_" _fuel exp)
+  e -> e
+ where
+  _fuel = pred fuel
+  tr :: String -> a -> a
+  tr msg = trace (printf "%s %d" msg fuel)
+
+
 closeExp :: Exp -> Exp
 closeExp = \case
   Lam_   freeVars exp -> Lam_ freeVars $ closeExp exp
-  Con_   freeVars conName noErasedApplied argsReversed -> Con_ freeVars (closeConName conName) noErasedApplied (map closeExp argsReversed)
-  TyCon_ freeVars tyConName argsReversed -> TyCon_ freeVars (closeTyConName tyConName) (map closeExp argsReversed)
+  Con_   freeVars conName noErasedApplied argsReversed -> Con_ freeVars (closeConName _maxFuel conName) noErasedApplied (map closeExp argsReversed)
+  TyCon_ freeVars tyConName argsReversed -> TyCon_ freeVars (closeTyConName _maxFuel tyConName) (map closeExp argsReversed)
   Pi_    freeVars visibility exp1 exp2 -> Pi_ freeVars visibility (closeExp exp1) (closeExp exp2)
   Neut   neutral -> Neut $ closeNeutral neutral
-  RHS    whnf -> STOP
+  RHS    exp -> RHS $ closeExp exp
   Let_   freeVars expType exp -> Let_ freeVars (closeExpType expType) (closeExp exp)
   Up_    freeVars ints exp -> Up_ freeVars ints (closeExp exp)
   e -> e
@@ -733,14 +768,14 @@ closeExp = \case
 closeNeutral :: Neutral -> Neutral
 closeNeutral = \case
   App__       freeVars neutral exp -> App__ freeVars (closeNeutral neutral) (closeExp exp)
-  CaseFun__   freeVars caseFunName   exps neutral -> CaseFun__ freeVars (closeCaseFunName caseFunName) (map closeExp exps) (closeNeutral neutral)
-  TyCaseFun__ freeVars tyCaseFunName exps neutral -> TyCaseFun__ freeVars (closeTyCaseFunName tyCaseFunName) (map closeExp exps) (closeNeutral neutral)
-  Fun_        freeVars funName exps exp -> Fun_ freeVars (closeFunName funName) (map closeExp exps) (closeExp exp)
+  CaseFun__   freeVars caseFunName   exps neutral -> CaseFun__ freeVars (closeCaseFunName _maxFuel caseFunName) (map closeExp exps) (closeNeutral neutral)
+  TyCaseFun__ freeVars tyCaseFunName exps neutral -> TyCaseFun__ freeVars (closeTyCaseFunName _maxFuel tyCaseFunName) (map closeExp exps) (closeNeutral neutral)
+  Fun_        freeVars funName exps exp -> Fun_ freeVars (closeFunName _maxFuel funName) (map closeExp exps) (STOP "Fun_") --(closeExp exp)
   UpN_        freeVars ints neutral -> UpN_ freeVars ints (closeNeutral neutral)
   n -> n
 
 closeExpType :: ExpType -> ExpType
-closeExpType (ET e t) = ET (closeExp e) (closeExp t)
+closeExpType (ET e t) = ET (closeExp e) (closeType_ "ExpType Type" _maxFuel t)
 
 instance Binary ExpType
 instance Binary Exp
@@ -754,9 +789,18 @@ instance Binary TyCaseFunName
 instance Binary FunName where -- do FunName/FunDef instance together
   put (FunName fName int funDef type_) = do
     put fName
+    put int
     put type_
+    case funDef of
+      NoDef       -> put (0 :: Word8)
+      DeltaDef{}  -> put (1 :: Word8)
+      ExpDef exp  -> put (2 :: Word8) >> put exp
 
   get = do
     fName <- get
+    int <- get
     type_ <- get
-    pure $ mkFunDef fName type_
+    (get :: Get Word8) >>= \case
+      0 -> pure $ FunName fName int NoDef type_
+      1 -> pure $ mkFunDef fName type_
+      2 -> (\exp -> FunName fName int (ExpDef exp) type_) <$> get
diff --git a/src/LambdaCube/Compiler/InferMonad.hs b/src/LambdaCube/Compiler/InferMonad.hs
index 2499fa5c..8db4eeed 100644
--- a/src/LambdaCube/Compiler/InferMonad.hs
+++ b/src/LambdaCube/Compiler/InferMonad.hs
@@ -214,5 +214,5 @@ dependentVars ie = cycle mempty
         a <-> b = (a --> b) <> (b --> a)
 
 
---closeGlobalEnv :: GlobalEnv -> GlobalEnv
-closeGlobalEnv = fmap (\(exp, type_, si) -> (closeExp exp {-, closeExp type_, si)-})) -- HINT: type should be finite
+closeGlobalEnv :: GlobalEnv -> GlobalEnv
+closeGlobalEnv = fmap (\(exp, type_, si) -> (closeExp exp , closeExp type_, si)) -- HINT: type should be finite
diff --git a/src/LambdaCube/Compiler/Utils.hs b/src/LambdaCube/Compiler/Utils.hs
index 3d1dc1ec..4e9eab27 100644
--- a/src/LambdaCube/Compiler/Utils.hs
+++ b/src/LambdaCube/Compiler/Utils.hs
@@ -8,6 +8,10 @@
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 module LambdaCube.Compiler.Utils where
 
+import Data.Time.Clock
+import Text.Printf
+import qualified Data.ByteString.Char8 as BS
+
 import Data.Binary (Binary(..))
 import GHC.Generics (Generic)
 
@@ -147,4 +151,28 @@ instance (Monoid w, P.MonadParsec e s m) => P.MonadParsec e s (RWST r w st m) wh
     getParserState              = lift P.getParserState
     updateParserState f         = lift $ P.updateParserState f
 
--}
\ No newline at end of file
+-}
+
+showTime delta
+    | t > 1e-1  = printf "%.3fs" t
+    | t > 1e-3  = printf "%.1fms" (t/1e-3)
+    | otherwise = printf "%.0fus" (t/1e-6)
+  where
+    t = realToFrac delta :: Double
+
+timeDiff msg m = (\s x e -> (diffUTCTime e s, x))
+  <$> getCurrentTime
+  <*> ( do
+    BS.putStrLn $ BS.pack $ msg ++ " START"
+    x <- m
+    BS.putStrLn $ BS.pack $ msg ++ " END"
+    pure x
+  )
+  <*> getCurrentTime
+
+printTimeDiff message m = do
+  (t,r) <- timeDiff message m
+  let msg = message ++ " TIME: " ++ showTime t ++ "\n"
+  BS.putStrLn $ BS.pack msg
+  appendFile "timing.log" msg
+  return r