2df0a7f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Store metavariables in ibc files

There's really no reason not to, and it means you can import something unfinished without having to wait for it to typecheck every time.

commit2df0a7f7ae6063ce50d52271631d75db6c2d4775 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 27 Feb 2014, 19:07 (13 years ago) parent1f897b1

5 files changed+90−67

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+7−1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/IBC.hs+22−10 src/Idris/Parser.hs+54−50 src/Pkg/Package.hs+6−6

src/Idris/AbsSyntax.hs+7−1

@@ -460,6 +460,7 @@ addDeferredTyCon = addDeferred' (TCon 0 0)

460460addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

461461addDeferred' nt ns

462462 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames [] t))) ns

463+ mapM_ (\(n, _) -> addIBC (IBCMetavar n)) ns

463464 i <- getIState

464465 putIState $ i { idris_metavars = map (\(n, (i, top, _, isTopLevel)) -> (n, (top, i, isTopLevel))) ns ++

465466 idris_metavars i }

@@ -475,7 +476,12 @@ solveDeferred :: Name -> Idris ()

475476solveDeferred n = do i <- getIState

476477 putIState $ i { idris_metavars =

477478 filter (\(n', _) -> n/=n')

478− (idris_metavars i) }

479+ (idris_metavars i),

480+ ibc_write =

481+ filter (notMV n) (ibc_write i)

482+ }

483+ where notMV n (IBCMetavar n') = not (n == n')

484+ notMV n _ = True

479485

480486getUndefined :: Idris [Name]

481487getUndefined = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1

@@ -189,6 +189,7 @@ data IBCWrite = IBCFix FixDecl

189189 | IBCDSL Name

190190 | IBCData Name

191191 | IBCOpt Name

192+ | IBCMetavar Name

192193 | IBCSyntax Syntax

193194 | IBCKeyword String

194195 | IBCImport FilePath

src/Idris/IBC.hs+22−10

@@ -24,9 +24,8 @@ import System.Directory

2424import Codec.Compression.Zlib (compress)

2525import Util.Zlib (decompressEither)

2626

27−

2827ibcVersion :: Word8

29−ibcVersion = 60

28+ibcVersion = 61

3029

3130

3231data IBCFile = IBCFile { ver :: Word8,

@@ -61,7 +60,8 @@ data IBCFile = IBCFile { ver :: Word8,

6160 ibc_namehints :: [(Name, Name)],

6261 ibc_metainformation :: [(Name, MetaInformation)],

6362 ibc_errorhandlers :: [Name],

64− ibc_function_errorhandlers :: [(Name, Name, Name)] -- fn, arg, handler

63+ ibc_function_errorhandlers :: [(Name, Name, Name)], -- fn, arg, handler

64+ ibc_metavars :: [(Name, (Maybe Name, Int, Bool))]

6565 }

6666 deriving Show

6767{-!

@@ -69,8 +69,7 @@ deriving instance Binary IBCFile

6969!-}

7070

7171initIBC :: IBCFile

72−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

73−

72+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] []

7473

7574loadIBC :: FilePath -> Idris ()

7675loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -91,9 +90,9 @@ writeIBC :: FilePath -> FilePath -> Idris ()

9190writeIBC src f

9291 = do iLOG $ "Writing ibc " ++ show f

9392 i <- getIState

94− case (Data.List.map fst (idris_metavars i)) \\ primDefs of

95− (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

96− [] -> return ()

93+-- case (Data.List.map fst (idris_metavars i)) \\ primDefs of

94+-- (_:_) -> ifail "Can't write ibc when there are unsolved metavariables"

95+-- [] -> return ()

9796 resetNameIdx

9897 ibcf <- mkIBC (ibc_write i) (initIBC { sourcefile = src })

9998 idrisCatch (do runIO $ createDirectoryIfMissing True (dropFileName f)

@@ -222,6 +221,10 @@ ibc i (IBCMetaInformation n m) f = return f { ibc_metainformation = (n,m) : ibc_

222221ibc i (IBCErrorHandler n) f = return f { ibc_errorhandlers = n : ibc_errorhandlers f }

223222ibc i (IBCFunctionErrorHandler fn a n) f =

224223 return f { ibc_function_errorhandlers = (fn, a, n) : ibc_function_errorhandlers f }

224+ibc i (IBCMetavar n) f =

225+ case lookup n (idris_metavars i) of

226+ Nothing -> return f

227+ Just t -> return f { ibc_metavars = (n, t) : ibc_metavars f }

225228

226229process :: IBCFile -> FilePath -> Idris ()

227230process i fn

@@ -262,6 +265,7 @@ process i fn

262265 pMetaInformation (ibc_metainformation i)

263266 pErrorHandlers (ibc_errorhandlers i)

264267 pFunctionErrorHandlers (ibc_function_errorhandlers i)

268+ pMetavars (ibc_metavars i)

265269

266270timestampOlder :: FilePath -> FilePath -> IO ()

267271timestampOlder src ibc = do srct <- getModificationTime src

@@ -451,6 +455,12 @@ pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

451455pFunctionErrorHandlers [] = return ()

452456pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]

453457 pFunctionErrorHandlers ns

458+

459+pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

460+pMetavars ns = do i <- getIState

461+ putIState $ i { idris_metavars = Data.List.reverse ns

462+ ++ idris_metavars i }

463+

454464----- Generated by 'derive'

455465

456466instance Binary SizeChange where

@@ -1037,7 +1047,7 @@ instance Binary MetaInformation where

10371047 return (DataMI x1)

10381048

10391049instance Binary IBCFile where

1040− put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33)

1050+ put x@(IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34)

10411051 = {-# SCC "putIBCFile" #-}

10421052 do put x1

10431053 put x2

@@ -1072,6 +1082,7 @@ instance Binary IBCFile where

10721082 put x31

10731083 put x32

10741084 put x33

1085+ put x34

10751086

10761087 get

10771088 = do x1 <- get

@@ -1108,7 +1119,8 @@ instance Binary IBCFile where

11081119 x31 <- get

11091120 x32 <- get

11101121 x33 <- get

1111− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33)

1122+ x34 <- get

1123+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34)

11121124 else return (initIBC { ver = x1 })

11131125

11141126instance Binary DataOpt where

src/Idris/Parser.hs+54−50

@@ -1219,56 +1219,60 @@ loadSource h lidr f

12191219 mapM_ (addIBC . IBCImport) [realName | (realName, alias, fc) <- imports]

12201220 let syntax = defaultSyntax{ syn_namespace = reverse mname }

12211221 ds' <- parseProg syntax f file pos

1222− unless (null ds') $ do

1223− let ds = namespaces mname ds'

1224− logLvl 3 (show $ showDecls True ds)

1225− i <- getIState

1226− logLvl 10 (show (toAlist (idris_implicits i)))

1227− logLvl 3 (show (idris_infixes i))

1228− -- Now add all the declarations to the context

1229− v <- verbose

1230− when v $ ihputStrLn h $ "Type checking " ++ f

1231− -- we totality check after every Mutual block, so if

1232− -- anything is a single definition, wrap it in a

1233− -- mutual block on its own

1234− elabDecls toplevel (map toMutual ds)

1235− i <- getIState

1236− -- simplify every definition do give the totality checker

1237− -- a better chance

1238− mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1239− updateContext (simplifyCasedef n))

1240− (map snd (idris_totcheck i))

1241− -- build size change graph from simplified definitions

1242− iLOG "Totality checking"

1243− i <- getIState

1244− mapM_ buildSCG (idris_totcheck i)

1245− mapM_ checkDeclTotality (idris_totcheck i)

1246−

1247− -- Redo totality check for deferred names

1248− let deftots = idris_defertotcheck i

1249− iLOG $ "Totality checking " ++ show deftots

1250− mapM_ (\x -> do tot <- getTotality x

1251− case tot of

1252− Total _ -> setTotality x Unchecked

1253− _ -> return ()) (map snd deftots)

1254− mapM_ buildSCG deftots

1255− mapM_ checkDeclTotality deftots

1256−

1257− iLOG ("Finished " ++ f)

1258− ibcsd <- valIBCSubDir i

1259− iLOG "Universe checking"

1260− iucheck

1261− let ibc = ibcPathNoFallback ibcsd f

1262− i <- getIState

1263− addHides (hide_list i)

1264− ok <- noErrors

1265− when ok $

1266− idrisCatch (do writeIBC f ibc; clearIBC)

1267− (\c -> return ()) -- failure is harmless

1268− i <- getIState

1269− putIState (i { default_total = def_total,

1270− hide_list = [] })

1271− return ()

1222+

1223+ -- Parsing done, now process declarations

1224+

1225+ let ds = namespaces mname ds'

1226+ logLvl 3 (show $ showDecls True ds)

1227+ i <- getIState

1228+ logLvl 10 (show (toAlist (idris_implicits i)))

1229+ logLvl 3 (show (idris_infixes i))

1230+ -- Now add all the declarations to the context

1231+ v <- verbose

1232+ when v $ ihputStrLn h $ "Type checking " ++ f

1233+ -- we totality check after every Mutual block, so if

1234+ -- anything is a single definition, wrap it in a

1235+ -- mutual block on its own

1236+ elabDecls toplevel (map toMutual ds)

1237+ i <- getIState

1238+ -- simplify every definition do give the totality checker

1239+ -- a better chance

1240+ mapM_ (\n -> do logLvl 5 $ "Simplifying " ++ show n

1241+ updateContext (simplifyCasedef n))

1242+ (map snd (idris_totcheck i))

1243+ -- build size change graph from simplified definitions

1244+ iLOG "Totality checking"

1245+ i <- getIState

1246+ mapM_ buildSCG (idris_totcheck i)

1247+ mapM_ checkDeclTotality (idris_totcheck i)

1248+

1249+ -- Redo totality check for deferred names

1250+ let deftots = idris_defertotcheck i

1251+ iLOG $ "Totality checking " ++ show deftots

1252+ mapM_ (\x -> do tot <- getTotality x

1253+ case tot of

1254+ Total _ -> setTotality x Unchecked

1255+ _ -> return ()) (map snd deftots)

1256+ mapM_ buildSCG deftots

1257+ mapM_ checkDeclTotality deftots

1258+

1259+ iLOG ("Finished " ++ f)

1260+ ibcsd <- valIBCSubDir i

1261+ iLOG "Universe checking"

1262+ iucheck

1263+ let ibc = ibcPathNoFallback ibcsd f

1264+ i <- getIState

1265+ addHides (hide_list i)

1266+

1267+ -- Finally, write an ibc if checking was successful

1268+

1269+ ok <- noErrors

1270+ when ok $

1271+ idrisCatch (do writeIBC f ibc; clearIBC)

1272+ (\c -> return ()) -- failure is harmless

1273+ i <- getIState

1274+ putIState (i { default_total = def_total,

1275+ hide_list = [] })

12721276 return ()

12731277 where

12741278 namespaces :: [String] -> [PDecl] -> [PDecl]

src/Pkg/Package.hs+6−6

@@ -57,12 +57,12 @@ buildPkg warnonly (install, fp)

5757 _ -> return ()

5858 -- Also give up if there are metavariables to solve

5959 case (map fst (idris_metavars ist) \\ primDefs) of

60− [] -> when install $ installPkg pkgdesc

61− ms -> do if install

62− then putStrLn "Can't install: there are undefined metavariables:"

63− else putStrLn "There are undefined metavariables:"

64− putStrLn $ "\t" ++ show ms

65− exitWith (ExitFailure 1)

60+ _ -> when install $ installPkg pkgdesc

61+-- ms -> do if install

62+-- then putStrLn "Can't install: there are undefined metavariables:"

63+-- else putStrLn "There are undefined metavariables:"

64+-- putStrLn $ "\t" ++ show ms

65+-- exitWith (ExitFailure 1)

6666

6767-- | Type check packages only

6868--