diff options
author | Csaba Hruska <csaba.hruska@gmail.com> | 2017-09-23 02:39:28 +0100 |
---|---|---|
committer | Csaba Hruska <csaba.hruska@gmail.com> | 2017-09-23 02:39:28 +0100 |
commit | 2cf8d916e4305a7e77c8577ca85d23afee15700c (patch) | |
tree | 764db9021e4add642f47f30dabf630609ba54f61 /src | |
parent | e205a839ce8cf1e0f71b88a7a9c7a793848b8f8e (diff) |
Exp serialization
Diffstat (limited to 'src')
-rw-r--r-- | src/LambdaCube/Compiler.hs | 117 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Core.hs | 118 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/InferMonad.hs | 4 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Utils.hs | 30 |
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 | |||
23 | , plainShow | 23 | , plainShow |
24 | , prettyShowUnlines | 24 | , prettyShowUnlines |
25 | ) where | 25 | ) where |
26 | import qualified Data.ByteString.Char8 as BS | ||
26 | 27 | ||
28 | import Data.Binary | ||
29 | import Data.Time.Clock | ||
30 | import Text.Printf | ||
27 | import Data.List | 31 | import Data.List |
28 | import Data.Maybe | 32 | import Data.Maybe |
29 | import Data.Function | 33 | import Data.Function |
@@ -37,19 +41,21 @@ import Control.Monad.Except | |||
37 | import Control.Monad.Catch | 41 | import Control.Monad.Catch |
38 | import Control.Arrow hiding ((<+>)) | 42 | import Control.Arrow hiding ((<+>)) |
39 | import System.FilePath | 43 | import System.FilePath |
44 | import System.Directory | ||
45 | import System.IO.Unsafe | ||
40 | --import Debug.Trace | 46 | --import Debug.Trace |
41 | 47 | ||
42 | import LambdaCube.IR as IR | 48 | import LambdaCube.IR as IR |
43 | import LambdaCube.Compiler.Pretty hiding ((</>)) | 49 | import LambdaCube.Compiler.Pretty hiding ((</>)) |
44 | import LambdaCube.Compiler.DesugaredSource (Module_(..), Export(..), ImportItems (..), Stmt) | 50 | import LambdaCube.Compiler.DesugaredSource (Module_(..), Export(..), ImportItems (..), Stmt) |
45 | import LambdaCube.Compiler.Parser (runDefParser, parseLC, DesugarInfo, Module) | 51 | import LambdaCube.Compiler.Parser (runDefParser, parseLC, DesugarInfo, Module) |
46 | import LambdaCube.Compiler.InferMonad (GlobalEnv, initEnv) | 52 | import LambdaCube.Compiler.InferMonad (GlobalEnv, initEnv, closeGlobalEnv) |
47 | import LambdaCube.Compiler.Infer (inference) | 53 | import LambdaCube.Compiler.Infer (inference) |
48 | import LambdaCube.Compiler.CoreToIR | 54 | import LambdaCube.Compiler.CoreToIR |
49 | 55 | ||
50 | import LambdaCube.Compiler.Utils | 56 | import LambdaCube.Compiler.Utils |
51 | import LambdaCube.Compiler.DesugaredSource as Exported (FileInfo(..), Range(..), SPos(..), pattern SPos, SIName(..), pattern SIName, sName, SI(..)) | 57 | import LambdaCube.Compiler.DesugaredSource as Exported (FileInfo(..), Range(..), SPos(..), pattern SPos, SIName(..), pattern SIName, sName, SI(..)) |
52 | import LambdaCube.Compiler.Core as Exported (mkDoc, Exp, ExpType(..), pattern ET, outputType, boolType, trueExp, hnf) | 58 | import LambdaCube.Compiler.Core as Exported (mkDoc, Exp, ExpType(..), pattern ET, outputType, boolType, trueExp, hnf, closeExp) |
53 | import LambdaCube.Compiler.InferMonad as Exported (errorRange, listAllInfos, listAllInfos', listTypeInfos, listErrors, listWarnings, listTraceInfos, Infos, Info(..)) | 59 | import LambdaCube.Compiler.InferMonad as Exported (errorRange, listAllInfos, listAllInfos', listTypeInfos, listErrors, listWarnings, listTraceInfos, Infos, Info(..)) |
54 | --import LambdaCube.Compiler.Infer as Exported () | 60 | --import LambdaCube.Compiler.Infer as Exported () |
55 | 61 | ||
@@ -89,7 +95,7 @@ type ModuleFetcher m = Maybe FilePath -> Either FilePath MName -> m (Either Doc | |||
89 | ioFetch :: MonadIO m => [FilePath] -> ModuleFetcher (MMT m x) | 95 | ioFetch :: MonadIO m => [FilePath] -> ModuleFetcher (MMT m x) |
90 | ioFetch paths' imp n = do | 96 | ioFetch paths' imp n = do |
91 | preludePath <- (</> "lc") <$> liftIO getDataDir | 97 | preludePath <- (</> "lc") <$> liftIO getDataDir |
92 | let paths = map (id &&& id) paths' ++ [(preludePath, preludePath)] | 98 | let paths = map (id &&& id) paths' ++ [(preludePath, {-"<<installed-prelude-path>>"-}preludePath)] |
93 | find ((x, (x', mn)): xs) = liftIO (readFileIfExists x) >>= maybe (find xs) (\src -> return $ Right (x', mn, liftIO src)) | 99 | find ((x, (x', mn)): xs) = liftIO (readFileIfExists x) >>= maybe (find xs) (\src -> return $ Right (x', mn, liftIO src)) |
94 | find [] = return $ Left $ "can't find" <+> either (("lc file" <+>) . text) (("module" <+>) . text) n | 100 | find [] = return $ Left $ "can't find" <+> either (("lc file" <+>) . text) (("module" <+>) . text) n |
95 | <+> "in path" <+> hsep (text . snd <$> paths) | 101 | <+> "in path" <+> hsep (text . snd <$> paths) |
@@ -155,33 +161,98 @@ loadModule ex imp mname_ = do | |||
155 | (\(ds, ge) -> Right (ds{-todo: filter-}, Map.filterWithKey (\k _ -> filterImports is k) ge)) | 161 | (\(ds, ge) -> Right (ds{-todo: filter-}, Map.filterWithKey (\k _ -> filterImports is k) ge)) |
156 | e) | 162 | e) |
157 | dsge | 163 | dsge |
158 | 164 | --------------- | |
159 | let (res, err) = case sequence ms of | 165 | let (res, err, g_env, defs) = case sequence ms of |
160 | Left err -> (ex mempty, Left $ pShow err) | 166 | Left err -> (ex mempty, Left $ pShow err, mempty, mempty) |
161 | Right ms@(mconcat -> (ds, ge)) -> case runExcept $ runDefParser ds $ definitions e of | 167 | Right ms@(mconcat -> (ds, ge)) -> case runExcept $ runDefParser ds $ definitions e of |
162 | Left err -> (ex mempty, Left $ pShow err) | 168 | Left err -> (ex mempty, Left $ pShow err, mempty, mempty) |
163 | Right (defs, warnings, dsinfo) -> (,) (ex (map ParseWarning warnings ++ is, defs)) $ case res of | 169 | Right (defs, warnings, dsinfo) -> ((ex (map ParseWarning warnings ++ is, defs)), res_1, g_env_1, defs) -- defs g_env_1 |
164 | Left err -> Left $ pShow err | ||
165 | Right (mconcat -> newge) -> | ||
166 | right mconcat $ forM (fromMaybe [ExportModule $ SIName mempty mname] $ moduleExports e) $ \case | ||
167 | ExportId (sName -> d) -> case Map.lookup d newge of | ||
168 | Just def -> Right (mempty{-TODO-}, Map.singleton d def) | ||
169 | Nothing -> Left $ text d <+> "is not defined" | ||
170 | ExportModule (sName -> m) | m == mname -> Right (dsinfo, newge) | ||
171 | ExportModule m -> case [ x | ((m', _), x) <- zip (moduleImports e) ms, m' == m] of | ||
172 | [x] -> Right x | ||
173 | [] -> Left $ "empty export list in module" <+> text fname -- m, map fst $ moduleImports e, mname) | ||
174 | _ -> error "export list: internal error" | ||
175 | where | 170 | where |
176 | (res, is) = runWriter . flip runReaderT (extensions e, initEnv <> ge) . runExceptT $ inference defs | 171 | defs_cached = unsafePerformIO $ do |
177 | 172 | let filename = printf "%s.def_bin" $ takeFileName fname :: String | |
178 | return $ Right (e, res, err) | 173 | doesFileExist filename >>= \case |
174 | True -> do | ||
175 | BS.putStrLn $ BS.pack $ printf "load %s" filename | ||
176 | decodeFile filename | ||
177 | False -> do | ||
178 | BS.putStrLn $ BS.pack $ printf "save %s" filename | ||
179 | encodeFile filename defs | ||
180 | pure defs | ||
181 | (res, is) = runWriter . flip runReaderT (extensions e, initEnv <> ge) . runExceptT $ inference defs --_cached | ||
182 | |||
183 | (g_env_1, res_1) = case res of | ||
184 | Left err -> (mempty, Left $ pShow err) | ||
185 | Right (mconcat -> newge) -> --do | ||
186 | --writeFile (printf "%s.exp" fname) $ show newge | ||
187 | (newge, right mconcat $ forM (fromMaybe [ExportModule $ SIName mempty mname] $ moduleExports e) $ \case | ||
188 | ExportId (sName -> d) -> case Map.lookup d newge of | ||
189 | Just def -> Right (mempty{-TODO-}, Map.singleton d def) | ||
190 | Nothing -> Left $ text d <+> "is not defined" | ||
191 | ExportModule (sName -> m) | m == mname -> Right (dsinfo, newge) | ||
192 | ExportModule m -> case [ x | ((m', _), x) <- zip (moduleImports e) ms, m' == m] of | ||
193 | [x] -> Right x | ||
194 | [] -> Left $ "empty export list in module" <+> text fname -- m, map fst $ moduleImports e, mname) | ||
195 | _ -> error "export list: internal error") | ||
196 | --------------- | ||
197 | let writeResult = do | ||
198 | let filename = printf "%s.exp" $ takeFileName fname :: String | ||
199 | filename_closed = printf "%s.exp.closed" $ takeFileName fname :: String | ||
200 | filename_closed_tr = printf "%s.exp.closed.tr" $ takeFileName fname :: String | ||
201 | filename_keys = printf "%s.exp.keys" $ takeFileName fname :: String | ||
202 | --putStrLn $ printf "write result! %d %s" ({-Map.size-}length g_env) filename | ||
203 | writeFile filename_keys $ unlines $ map show $ Map.keys g_env | ||
204 | let (g_env_ok, g_env_closed, g_env_closed_tr) = unzip3 | ||
205 | [ ( printf "%s :: %s\n%s = %s\n\n" k ty_s k v_s :: String | ||
206 | , printf "%s :: %s\n%s = %s\n\n" k c_ty_s k c_v_s :: String | ||
207 | , printf "%s :: %s\n%s = %s\n\n" k tr_c_ty_s k tr_c_v_s :: String | ||
208 | ) | ||
209 | | (k,(v, v_ty, v_si)) <- Map.toList g_env | ||
210 | , let ty_s = show $ mkDoc (False,False) $ v_ty | ||
211 | , let v_s = show $ mkDoc (False,True) $ v | ||
212 | , let c_v_ty = closeExp v_ty | ||
213 | , let c_v = closeExp v | ||
214 | , let c_ty_s = show $ mkDoc (False,False) c_v_ty | ||
215 | , let c_v_s = show $ mkDoc (False,True) $ c_v | ||
216 | , let tr_c_ty_s = show $ mkDoc (False,False) $ tr_exp c_v_ty | ||
217 | , let tr_c_v_s = show $ mkDoc (False,True) $ tr_exp c_v | ||
218 | ] | ||
219 | tr_exp :: Exp -> Exp | ||
220 | tr_exp = decode . encode | ||
221 | {- | ||
222 | writeFile filename (concat $ g_env_ok :: String) | ||
223 | writeFile filename_closed (concat $ g_env_closed :: String) | ||
224 | writeFile filename_closed_tr (concat $ g_env_closed_tr :: String) | ||
225 | -} | ||
226 | BS.putStrLn $ BS.pack $ printf "write %s" (printf "%s.env_bin - START" $ takeFileName fname :: String) | ||
227 | encodeFile (printf "%s.env_bin" $ takeFileName fname :: String) $ closeGlobalEnv g_env | ||
228 | BS.putStrLn $ BS.pack $ printf "write %s" (printf "%s.env_bin - DONE" $ takeFileName fname :: String) | ||
229 | |||
230 | -- TODO: guarded pShow save to file for g_env exps and closed g_env exps | ||
231 | |||
232 | writeParsedDefs = do | ||
233 | BS.putStrLn $ BS.pack $ printf "defs count: %d" (length defs) | ||
234 | let filename = printf "%s.defs" $ takeFileName fname :: String | ||
235 | writeFile filename $ unlines $ map ((++ "\n"). show . pShow) defs | ||
236 | encodeFile (printf "%s.def_bin" $ takeFileName fname :: String) defs | ||
237 | {- | ||
238 | Experiment: | ||
239 | Stmt/SExp - can be serialized | ||
240 | Exp - explodes ; must be the inference algorithm | ||
241 | -} | ||
242 | debugAction = do | ||
243 | printTimeDiff (fname ++ " Defs") writeParsedDefs | ||
244 | printTimeDiff (fname ++ " Exp") writeResult | ||
245 | --when (fname == "./SampleMaterial.lc") $ | ||
246 | -- fail "stop" | ||
247 | return $ unsafePerformIO (debugAction >> pure (Right (e, res, err))) | ||
248 | --return (Right (e, res, err)) | ||
179 | modify $ \(Modules nm im ni) -> Modules nm (IM.insert fid (fi, (src, res)) im) ni | 249 | modify $ \(Modules nm im ni) -> Modules nm (IM.insert fid (fi, (src, res)) im) ni |
180 | return $ Right (fi, (src, res)) | 250 | return $ Right (fi, (src, res)) |
181 | where | 251 | where |
182 | filterImports (ImportAllBut ns) = not . (`elem` map sName ns) | 252 | filterImports (ImportAllBut ns) = not . (`elem` map sName ns) |
183 | filterImports (ImportJust ns) = (`elem` map sName ns) | 253 | filterImports (ImportJust ns) = (`elem` map sName ns) |
184 | 254 | ||
255 | |||
185 | -- used in runTests | 256 | -- used in runTests |
186 | getDef :: MonadMask m => FilePath -> SName -> Maybe Exp -> MMT m (Infos, [Stmt]) ((Infos, [Stmt]), Either Doc (FileInfo, Either Doc ExpType)) | 257 | getDef :: MonadMask m => FilePath -> SName -> Maybe Exp -> MMT m (Infos, [Stmt]) ((Infos, [Stmt]), Either Doc (FileInfo, Either Doc ExpType)) |
187 | getDef = getDef_ id | 258 | getDef = getDef_ id |
@@ -224,7 +295,7 @@ preCompile paths paths' backend mod = do | |||
224 | where | 295 | where |
225 | compile src = runMM fetch $ do | 296 | compile src = runMM fetch $ do |
226 | let pname = "." </> "Prelude.lc" | 297 | let pname = "." </> "Prelude.lc" |
227 | modify $ \(Modules nm im ni) -> Modules (Map.insert pname ni nm) (IM.insert ni (FileInfo ni pname "Prelude", prelude) im) (ni+1) | 298 | modify $ \(Modules nm im ni) -> Modules (Map.insert pname ni nm) (IM.insert ni (FileInfo ni pname "Prelude" , prelude) im) (ni+1) |
228 | (snd &&& fst) <$> compilePipeline' ex backend "Main" | 299 | (snd &&& fst) <$> compilePipeline' ex backend "Main" |
229 | where | 300 | where |
230 | fetch imp = \case | 301 | 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 @@ | |||
13 | --{-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove | 13 | --{-# OPTIONS_GHC -fno-warn-unused-binds #-} -- TODO: remove |
14 | module LambdaCube.Compiler.Core where | 14 | module LambdaCube.Compiler.Core where |
15 | 15 | ||
16 | import Text.Printf | ||
17 | --import Debug.Trace | ||
16 | import Data.Binary | 18 | import Data.Binary |
17 | import GHC.Generics (Generic) | 19 | import GHC.Generics (Generic) |
18 | 20 | ||
@@ -88,7 +90,7 @@ data Exp | |||
88 | | RHS Exp{-always in hnf-} | 90 | | RHS Exp{-always in hnf-} |
89 | | Let_ FreeVars ExpType Exp | 91 | | Let_ FreeVars ExpType Exp |
90 | | Up_ FreeVars [Int] Exp | 92 | | Up_ FreeVars [Int] Exp |
91 | | STOP | 93 | | STOP String |
92 | deriving Generic | 94 | deriving Generic |
93 | 95 | ||
94 | data Neutral | 96 | data Neutral |
@@ -195,21 +197,21 @@ tCon_ k s i t a = Con (ConName (FTag s) i t) k a | |||
195 | pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a | 197 | pattern TyConN s a <- TyCon (TyConName s _ _ _ _) a |
196 | 198 | ||
197 | pattern TTyCon0 s <- TyCon (TyConName (FTag s) _ _ _ _) [] | 199 | pattern TTyCon0 s <- TyCon (TyConName (FTag s) _ _ _ _) [] |
198 | tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (error "TTyCon0-A") (error "TTyCon0-B") 0) [] | 200 | tTyCon0 s cs = TyCon (TyConName (FTag s) 0 TType (map ((,) (error "tTyCon0")) cs) $ CaseFunName (FTag s) (STOP "TTyCon0-B") 0) [] |
199 | 201 | ||
200 | pattern a :~> b = Pi Visible a b | 202 | pattern a :~> b = Pi Visible a b |
201 | 203 | ||
202 | delta = ELit (LString "<<delta function>>") -- TODO: build an error call | 204 | delta = ELit (LString "<<delta function>>") -- TODO: build an error call |
203 | 205 | ||
204 | pattern TConstraint <- TTyCon0 F'Constraint where TConstraint = tTyCon0 F'Constraint $ error "cs 1" | 206 | pattern TConstraint <- TTyCon0 F'Constraint where TConstraint = tTyCon0 F'Constraint [] |
205 | pattern Unit <- TTyCon0 F'Unit where Unit = tTyCon0 F'Unit [Unit] | 207 | pattern Unit <- TTyCon0 F'Unit where Unit = tTyCon0 F'Unit [Unit] |
206 | pattern TInt <- TTyCon0 F'Int where TInt = tTyCon0 F'Int $ error "cs 1" | 208 | pattern TInt <- TTyCon0 F'Int where TInt = tTyCon0 F'Int [] |
207 | pattern TNat <- TTyCon0 F'Nat where TNat = tTyCon0 F'Nat $ error "cs 3" | 209 | pattern TNat <- TTyCon0 F'Nat where TNat = tTyCon0 F'Nat [] |
208 | pattern TBool <- TTyCon0 F'Bool where TBool = tTyCon0 F'Bool $ error "cs 4" | 210 | pattern TBool <- TTyCon0 F'Bool where TBool = tTyCon0 F'Bool [] |
209 | pattern TFloat <- TTyCon0 F'Float where TFloat = tTyCon0 F'Float $ error "cs 5" | 211 | pattern TFloat <- TTyCon0 F'Float where TFloat = tTyCon0 F'Float [] |
210 | pattern TString <- TTyCon0 F'String where TString = tTyCon0 F'String $ error "cs 6" | 212 | pattern TString <- TTyCon0 F'String where TString = tTyCon0 F'String [] |
211 | pattern TChar <- TTyCon0 F'Char where TChar = tTyCon0 F'Char $ error "cs 7" | 213 | pattern TChar <- TTyCon0 F'Char where TChar = tTyCon0 F'Char [] |
212 | pattern TOrdering <- TTyCon0 F'Ordering where TOrdering = tTyCon0 F'Ordering $ error "cs 8" | 214 | pattern TOrdering <- TTyCon0 F'Ordering where TOrdering = tTyCon0 F'Ordering [] |
213 | pattern TVec a b <- TyConN (FTag F'VecS) [a, b] | 215 | pattern TVec a b <- TyConN (FTag F'VecS) [a, b] |
214 | 216 | ||
215 | pattern Empty s <- TyCon (TyConName (FTag F'Empty) _ _ _ _) (HString{-hnf?-} s: _) | 217 | pattern Empty s <- TyCon (TyConName (FTag F'Empty) _ _ _ _) (HString{-hnf?-} s: _) |
@@ -263,7 +265,7 @@ mkOrdering x = case x of | |||
263 | GT -> tCon FGT 2 TOrdering [] | 265 | GT -> tCon FGT 2 TOrdering [] |
264 | 266 | ||
265 | conTypeName :: ConName -> TyConName | 267 | conTypeName :: ConName -> TyConName |
266 | conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n | 268 | conTypeName (ConName _ _ t) = case snd $ getParams t of TyCon n _ -> n ; STOP m -> error $ "STOP " ++ m |
267 | 269 | ||
268 | mkFun_ md (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f md as | 270 | mkFun_ md (FunName _ _ (DeltaDef ar f) _) as _ | length as == ar = f md as |
269 | mkFun_ md f@(FunName _ _ (ExpDef e) _) xs _ = Neut $ Fun_ md f xs $ hnf $ foldlrev app_ e xs | 271 | mkFun_ md f@(FunName _ _ (ExpDef e) _) xs _ = Neut $ Fun_ md f xs $ hnf $ foldlrev app_ e xs |
@@ -283,7 +285,7 @@ reduce _ = Nothing | |||
283 | hnf (Reduced y) = hnf y -- TODO: review hnf call here | 285 | hnf (Reduced y) = hnf y -- TODO: review hnf call here |
284 | hnf a = a | 286 | hnf a = a |
285 | 287 | ||
286 | outputType = tTyCon0 F'Output $ error "cs 9" | 288 | outputType = tTyCon0 F'Output [] |
287 | 289 | ||
288 | -- TODO: remove | 290 | -- TODO: remove |
289 | boolType = TBool | 291 | boolType = TBool |
@@ -390,6 +392,7 @@ instance HasFreeVars Exp where | |||
390 | TyCon_ c _ _ -> c | 392 | TyCon_ c _ _ -> c |
391 | Let_ c _ _ -> c | 393 | Let_ c _ _ -> c |
392 | 394 | ||
395 | STOP{} -> mempty | ||
393 | TType_ _ -> mempty | 396 | TType_ _ -> mempty |
394 | ELit{} -> mempty | 397 | ELit{} -> mempty |
395 | Neut x -> getFreeVars x | 398 | Neut x -> getFreeVars x |
@@ -438,6 +441,7 @@ instance MkDoc Exp where | |||
438 | Neut x -> mkDoc pr x | 441 | Neut x -> mkDoc pr x |
439 | Let a b -> shLet_ (pShow a) (pShow b) | 442 | Let a b -> shLet_ (pShow a) (pShow b) |
440 | RHS x -> text "_rhs" `DApp` mkDoc pr x | 443 | RHS x -> text "_rhs" `DApp` mkDoc pr x |
444 | STOP x -> text $ "STOP " ++ x | ||
441 | 445 | ||
442 | pattern FFix f <- Fun (FunName (FTag FprimFix) _ _ _) [f, _] _ | 446 | pattern FFix f <- Fun (FunName (FTag FprimFix) _ _ _) [f, _] _ |
443 | 447 | ||
@@ -692,40 +696,71 @@ instance NType Lit where | |||
692 | LString _ -> TString | 696 | LString _ -> TString |
693 | LChar _ -> TChar | 697 | LChar _ -> TChar |
694 | 698 | ||
699 | {- | ||
700 | data ConName = ConName FName Int Type | ||
701 | data TyConName = TyConName FName Int Type [(ConName, Type)] CaseFunName | ||
702 | data FunName = FunName FName Int FunDef Type | ||
703 | data CaseFunName = CaseFunName FName Type Int | ||
704 | data TyCaseFunName = TyCaseFunName FName Type | ||
705 | data FunDef | ||
706 | = DeltaDef !Int (FreeVars -> [Exp] -> Exp) | ||
707 | | NoDef | ||
708 | | ExpDef Exp | ||
709 | -} | ||
695 | 710 | ||
696 | closeTyConName (TyConName fname ints type_ cons caseFunName) | 711 | trace :: String -> a -> a |
697 | -- = TyConName fname ints (closeExp type_) [(closeConName n, closeExp t) | (n,t) <- cons] (closeCaseFunName caseFunName) | 712 | trace _ = id |
698 | = TyConName fname ints STOP [(closeConName n, STOP) | (n,t) <- cons] (closeCaseFunName caseFunName) | ||
699 | 713 | ||
700 | closeTyCaseFunName (TyCaseFunName fname type_) | 714 | closeType_ msg fuel _ = STOP $ msg ++ " " ++ show fuel |
701 | -- = TyCaseFunName fname (closeExp type_) | ||
702 | = TyCaseFunName fname STOP | ||
703 | 715 | ||
704 | closeConName (ConName fname ordinal type_) | 716 | -- TODO: check MkDoc |
705 | -- = ConName fname ordinal (closeExp type_) | 717 | closeTyConName fuel (TyConName fname ints type_ cons caseFunName) |
706 | = ConName fname ordinal STOP | 718 | = 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) |
707 | 719 | ||
708 | closeCaseFunName (CaseFunName fname type_ int) | 720 | closeTyCaseFunName fuel (TyCaseFunName fname type_) |
709 | -- = CaseFunName fname (closeExp type_) int | 721 | = trace (printf "TyCaseFunName %s %d" (show fname) fuel) $ TyCaseFunName fname (closeType_ "TyCaseFunName" fuel type_) |
710 | = CaseFunName fname STOP int | ||
711 | 722 | ||
712 | closeFunName (FunName fname int funDef type_) | 723 | closeConName fuel (ConName fname ordinal type_) |
713 | -- = FunName fname int (closeFunDef funDef) (closeExp type_) | 724 | = trace (printf "ConName %s %d" (show fname) fuel) $ ConName fname ordinal (closeType fuel type_) --(STOP "ConName") |
714 | = FunName fname int (closeFunDef funDef) STOP | 725 | |
726 | closeCaseFunName fuel (CaseFunName fname type_ int) | ||
727 | = trace (printf "CaseFunName %s %d" (show fname) fuel) $ CaseFunName fname (closeType_ "CaseFunName" fuel type_) int | ||
728 | |||
729 | closeFunName fuel (FunName fname int funDef type_) | ||
730 | = trace (printf "FunName %s %d" (show fname) fuel) $ FunName fname int (closeFunDef funDef) (closeType_ "FunName" fuel type_) | ||
715 | 731 | ||
716 | closeFunDef = \case | 732 | closeFunDef = \case |
717 | ExpDef exp -> ExpDef STOP | 733 | ExpDef exp -> ExpDef (closeExp exp) |
718 | --ExpDef exp -> ExpDef (closeExp exp) | ||
719 | x -> x | 734 | x -> x |
720 | 735 | ||
736 | _maxFuel = 25 :: Int -- 6 | ||
737 | |||
738 | closeType :: Int -> Exp -> Exp | ||
739 | --closeType fuel | fuel <= 0 = \_ -> STOP "out of fuel" | ||
740 | closeType fuel = \case | ||
741 | Lam_ freeVars exp -> tr "Lam_" $ Lam_ freeVars (closeType_ "Lam_" _fuel exp) | ||
742 | Con_ freeVars conName noErasedApplied argsReversed -> tr "Con_" $ Con_ freeVars (closeConName _fuel conName) noErasedApplied [] | ||
743 | TyCon_ freeVars tyConName argsReversed -> tr "TyCon_" $ TyCon_ freeVars (closeTyConName _fuel tyConName) [] | ||
744 | Pi_ freeVars visibility exp1 exp2 -> tr "Pi_" $ Pi_ freeVars visibility (closeType_ "Pi_ 1" _fuel exp1) (closeType _fuel exp2) | ||
745 | Neut neutral -> STOP "Neut" | ||
746 | RHS exp -> tr "RHS" $ RHS (closeType_ "RHS" _fuel exp) | ||
747 | Let_ freeVars expType exp -> (STOP "Let_") | ||
748 | Up_ freeVars ints exp -> tr "Up_" $ Up_ freeVars ints (closeType_ "Up_" _fuel exp) | ||
749 | e -> e | ||
750 | where | ||
751 | _fuel = pred fuel | ||
752 | tr :: String -> a -> a | ||
753 | tr msg = trace (printf "%s %d" msg fuel) | ||
754 | |||
755 | |||
721 | closeExp :: Exp -> Exp | 756 | closeExp :: Exp -> Exp |
722 | closeExp = \case | 757 | closeExp = \case |
723 | Lam_ freeVars exp -> Lam_ freeVars $ closeExp exp | 758 | Lam_ freeVars exp -> Lam_ freeVars $ closeExp exp |
724 | Con_ freeVars conName noErasedApplied argsReversed -> Con_ freeVars (closeConName conName) noErasedApplied (map closeExp argsReversed) | 759 | Con_ freeVars conName noErasedApplied argsReversed -> Con_ freeVars (closeConName _maxFuel conName) noErasedApplied (map closeExp argsReversed) |
725 | TyCon_ freeVars tyConName argsReversed -> TyCon_ freeVars (closeTyConName tyConName) (map closeExp argsReversed) | 760 | TyCon_ freeVars tyConName argsReversed -> TyCon_ freeVars (closeTyConName _maxFuel tyConName) (map closeExp argsReversed) |
726 | Pi_ freeVars visibility exp1 exp2 -> Pi_ freeVars visibility (closeExp exp1) (closeExp exp2) | 761 | Pi_ freeVars visibility exp1 exp2 -> Pi_ freeVars visibility (closeExp exp1) (closeExp exp2) |
727 | Neut neutral -> Neut $ closeNeutral neutral | 762 | Neut neutral -> Neut $ closeNeutral neutral |
728 | RHS whnf -> STOP | 763 | RHS exp -> RHS $ closeExp exp |
729 | Let_ freeVars expType exp -> Let_ freeVars (closeExpType expType) (closeExp exp) | 764 | Let_ freeVars expType exp -> Let_ freeVars (closeExpType expType) (closeExp exp) |
730 | Up_ freeVars ints exp -> Up_ freeVars ints (closeExp exp) | 765 | Up_ freeVars ints exp -> Up_ freeVars ints (closeExp exp) |
731 | e -> e | 766 | e -> e |
@@ -733,14 +768,14 @@ closeExp = \case | |||
733 | closeNeutral :: Neutral -> Neutral | 768 | closeNeutral :: Neutral -> Neutral |
734 | closeNeutral = \case | 769 | closeNeutral = \case |
735 | App__ freeVars neutral exp -> App__ freeVars (closeNeutral neutral) (closeExp exp) | 770 | App__ freeVars neutral exp -> App__ freeVars (closeNeutral neutral) (closeExp exp) |
736 | CaseFun__ freeVars caseFunName exps neutral -> CaseFun__ freeVars (closeCaseFunName caseFunName) (map closeExp exps) (closeNeutral neutral) | 771 | CaseFun__ freeVars caseFunName exps neutral -> CaseFun__ freeVars (closeCaseFunName _maxFuel caseFunName) (map closeExp exps) (closeNeutral neutral) |
737 | TyCaseFun__ freeVars tyCaseFunName exps neutral -> TyCaseFun__ freeVars (closeTyCaseFunName tyCaseFunName) (map closeExp exps) (closeNeutral neutral) | 772 | TyCaseFun__ freeVars tyCaseFunName exps neutral -> TyCaseFun__ freeVars (closeTyCaseFunName _maxFuel tyCaseFunName) (map closeExp exps) (closeNeutral neutral) |
738 | Fun_ freeVars funName exps exp -> Fun_ freeVars (closeFunName funName) (map closeExp exps) (closeExp exp) | 773 | Fun_ freeVars funName exps exp -> Fun_ freeVars (closeFunName _maxFuel funName) (map closeExp exps) (STOP "Fun_") --(closeExp exp) |
739 | UpN_ freeVars ints neutral -> UpN_ freeVars ints (closeNeutral neutral) | 774 | UpN_ freeVars ints neutral -> UpN_ freeVars ints (closeNeutral neutral) |
740 | n -> n | 775 | n -> n |
741 | 776 | ||
742 | closeExpType :: ExpType -> ExpType | 777 | closeExpType :: ExpType -> ExpType |
743 | closeExpType (ET e t) = ET (closeExp e) (closeExp t) | 778 | closeExpType (ET e t) = ET (closeExp e) (closeType_ "ExpType Type" _maxFuel t) |
744 | 779 | ||
745 | instance Binary ExpType | 780 | instance Binary ExpType |
746 | instance Binary Exp | 781 | instance Binary Exp |
@@ -754,9 +789,18 @@ instance Binary TyCaseFunName | |||
754 | instance Binary FunName where -- do FunName/FunDef instance together | 789 | instance Binary FunName where -- do FunName/FunDef instance together |
755 | put (FunName fName int funDef type_) = do | 790 | put (FunName fName int funDef type_) = do |
756 | put fName | 791 | put fName |
792 | put int | ||
757 | put type_ | 793 | put type_ |
794 | case funDef of | ||
795 | NoDef -> put (0 :: Word8) | ||
796 | DeltaDef{} -> put (1 :: Word8) | ||
797 | ExpDef exp -> put (2 :: Word8) >> put exp | ||
758 | 798 | ||
759 | get = do | 799 | get = do |
760 | fName <- get | 800 | fName <- get |
801 | int <- get | ||
761 | type_ <- get | 802 | type_ <- get |
762 | pure $ mkFunDef fName type_ | 803 | (get :: Get Word8) >>= \case |
804 | 0 -> pure $ FunName fName int NoDef type_ | ||
805 | 1 -> pure $ mkFunDef fName type_ | ||
806 | 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 | |||
214 | a <-> b = (a --> b) <> (b --> a) | 214 | a <-> b = (a --> b) <> (b --> a) |
215 | 215 | ||
216 | 216 | ||
217 | --closeGlobalEnv :: GlobalEnv -> GlobalEnv | 217 | closeGlobalEnv :: GlobalEnv -> GlobalEnv |
218 | closeGlobalEnv = fmap (\(exp, type_, si) -> (closeExp exp {-, closeExp type_, si)-})) -- HINT: type should be finite | 218 | 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 @@ | |||
8 | {-# OPTIONS_GHC -fno-warn-orphans #-} | 8 | {-# OPTIONS_GHC -fno-warn-orphans #-} |
9 | module LambdaCube.Compiler.Utils where | 9 | module LambdaCube.Compiler.Utils where |
10 | 10 | ||
11 | import Data.Time.Clock | ||
12 | import Text.Printf | ||
13 | import qualified Data.ByteString.Char8 as BS | ||
14 | |||
11 | import Data.Binary (Binary(..)) | 15 | import Data.Binary (Binary(..)) |
12 | import GHC.Generics (Generic) | 16 | import GHC.Generics (Generic) |
13 | 17 | ||
@@ -147,4 +151,28 @@ instance (Monoid w, P.MonadParsec e s m) => P.MonadParsec e s (RWST r w st m) wh | |||
147 | getParserState = lift P.getParserState | 151 | getParserState = lift P.getParserState |
148 | updateParserState f = lift $ P.updateParserState f | 152 | updateParserState f = lift $ P.updateParserState f |
149 | 153 | ||
150 | -} \ No newline at end of file | 154 | -} |
155 | |||
156 | showTime delta | ||
157 | | t > 1e-1 = printf "%.3fs" t | ||
158 | | t > 1e-3 = printf "%.1fms" (t/1e-3) | ||
159 | | otherwise = printf "%.0fus" (t/1e-6) | ||
160 | where | ||
161 | t = realToFrac delta :: Double | ||
162 | |||
163 | timeDiff msg m = (\s x e -> (diffUTCTime e s, x)) | ||
164 | <$> getCurrentTime | ||
165 | <*> ( do | ||
166 | BS.putStrLn $ BS.pack $ msg ++ " START" | ||
167 | x <- m | ||
168 | BS.putStrLn $ BS.pack $ msg ++ " END" | ||
169 | pure x | ||
170 | ) | ||
171 | <*> getCurrentTime | ||
172 | |||
173 | printTimeDiff message m = do | ||
174 | (t,r) <- timeDiff message m | ||
175 | let msg = message ++ " TIME: " ++ showTime t ++ "\n" | ||
176 | BS.putStrLn $ BS.pack msg | ||
177 | appendFile "timing.log" msg | ||
178 | return r | ||