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

git.iko.soy/Idris-dev

on master help sign in

Store metavariables in ibc files

2df0a7fEdwin Brady13 years ago

src/Idris/AbsSyntax.hs+7−1

compare with master

unifiedsplit

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

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

461addDeferred' nt ns

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

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

463 i <- getIState

464 i <- getIState

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

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

465 idris_metavars i }

466 idris_metavars i }

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

475solveDeferred n = do i <- getIState

476solveDeferred n = do i <- getIState

476 putIState $ i { idris_metavars =

477 putIState $ i { idris_metavars =

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

478 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

479

485

480getUndefined :: Idris [Name]

486getUndefined :: Idris [Name]

481getUndefined = do i <- getIState

487getUndefined = do i <- getIState

src/Idris/AbsSyntaxTree.hs+1

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

189 | IBCDSL Name

190 | IBCData Name

191 | IBCOpt Name

192+ | IBCMetavar Name

192 | IBCSyntax Syntax

193 | IBCSyntax Syntax

193 | IBCKeyword String

194 | IBCKeyword String

194 | IBCImport FilePath

195 | IBCImport FilePath

src/Idris/IBC.hs+22−10

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

24import Codec.Compression.Zlib (compress)

25import Util.Zlib (decompressEither)

27−

28ibcVersion :: Word8

27ibcVersion :: Word8

29−ibcVersion = 60

28+ibcVersion = 61

32data IBCFile = IBCFile { ver :: Word8,

31data IBCFile = IBCFile { ver :: Word8,

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

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

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

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

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

63 ibc_errorhandlers :: [Name],

62 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))]

65 }

66 deriving Show

67{-!

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

69!-}

71initIBC :: IBCFile

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

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

73−

75loadIBC :: FilePath -> Idris ()

74loadIBC :: FilePath -> Idris ()

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

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

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

91writeIBC src f

90writeIBC src f

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

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

93 i <- getIState

92 i <- getIState

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

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

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

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

96− [] -> return ()

95+-- [] -> return ()

97 resetNameIdx

96 resetNameIdx

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

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

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

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

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

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

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

223ibc i (IBCFunctionErrorHandler fn a n) f =

222ibc i (IBCFunctionErrorHandler fn a n) f =

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

223 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 }

225

228

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

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

227process i fn

230process i fn

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

262 pMetaInformation (ibc_metainformation i)

265 pMetaInformation (ibc_metainformation i)

263 pErrorHandlers (ibc_errorhandlers i)

266 pErrorHandlers (ibc_errorhandlers i)

264 pFunctionErrorHandlers (ibc_function_errorhandlers i)

267 pFunctionErrorHandlers (ibc_function_errorhandlers i)

268+ pMetavars (ibc_metavars i)

265

269

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

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

267timestampOlder src ibc = do srct <- getModificationTime src

271timestampOlder src ibc = do srct <- getModificationTime src

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

451pFunctionErrorHandlers [] = return ()

455pFunctionErrorHandlers [] = return ()

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

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

453 pFunctionErrorHandlers ns

457 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+

454----- Generated by 'derive'

464----- Generated by 'derive'

455

465

456instance Binary SizeChange where

466instance Binary SizeChange where

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

1037 return (DataMI x1)

1047 return (DataMI x1)

1038

1048

1039instance Binary IBCFile where

1049instance 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)

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

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

1042 do put x1

1052 do put x1

1043 put x2

1053 put x2

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

1072 put x31

1082 put x31

1073 put x32

1083 put x32

1074 put x33

1084 put x33

1085+ put x34

1075

1086

1076 get

1087 get

1077 = do x1 <- get

1088 = do x1 <- get

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

1108 x31 <- get

1119 x31 <- get

1109 x32 <- get

1120 x32 <- get

1110 x33 <- get

1121 x33 <- get

1122+ x34 <- 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)

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)

1112 else return (initIBC { ver = x1 })

1124 else return (initIBC { ver = x1 })

1113

1125

1114instance Binary DataOpt where

1126instance Binary DataOpt where

src/Idris/Parser.hs+54−50

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

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

1220 let syntax = defaultSyntax{ syn_namespace = reverse mname }

1221 ds' <- parseProg syntax f file pos

1222− unless (null ds') $ do

1222+

1223+ -- Parsing done, now process declarations

1224+

1223− let ds = namespaces mname ds'

1225+ let ds = namespaces mname ds'

1224− logLvl 3 (show $ showDecls True ds)

1226+ logLvl 3 (show $ showDecls True ds)

1225− i <- getIState

1227+ i <- getIState

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

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

1227− logLvl 3 (show (idris_infixes i))

1229+ logLvl 3 (show (idris_infixes i))

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

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

1229− v <- verbose

1231+ v <- verbose

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

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

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

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

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

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

1233− -- mutual block on its own

1235+ -- mutual block on its own

1234− elabDecls toplevel (map toMutual ds)

1236+ elabDecls toplevel (map toMutual ds)

1235− i <- getIState

1237+ i <- getIState

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

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

1237− -- a better chance

1239+ -- a better chance

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

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

1239− updateContext (simplifyCasedef n))

1241+ updateContext (simplifyCasedef n))

1240− (map snd (idris_totcheck i))

1242+ (map snd (idris_totcheck i))

1241− -- build size change graph from simplified definitions

1243+ -- build size change graph from simplified definitions

1242− iLOG "Totality checking"

1244+ iLOG "Totality checking"

1243− i <- getIState

1245+ i <- getIState

1244− mapM_ buildSCG (idris_totcheck i)

1246+ mapM_ buildSCG (idris_totcheck i)

1245− mapM_ checkDeclTotality (idris_totcheck i)

1247+ mapM_ checkDeclTotality (idris_totcheck i)

1246−

1248+

1247− -- Redo totality check for deferred names

1249+ -- Redo totality check for deferred names

1248− let deftots = idris_defertotcheck i

1250+ let deftots = idris_defertotcheck i

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

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

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

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

1251− case tot of

1253+ case tot of

1252− Total _ -> setTotality x Unchecked

1254+ Total _ -> setTotality x Unchecked

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

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

1254− mapM_ buildSCG deftots

1256+ mapM_ buildSCG deftots

1255− mapM_ checkDeclTotality deftots

1257+ mapM_ checkDeclTotality deftots

1256−

1258+

1257− iLOG ("Finished " ++ f)

1259+ iLOG ("Finished " ++ f)

1258− ibcsd <- valIBCSubDir i

1260+ ibcsd <- valIBCSubDir i

1259− iLOG "Universe checking"

1261+ iLOG "Universe checking"

1260− iucheck

1262+ iucheck

1261− let ibc = ibcPathNoFallback ibcsd f

1263+ let ibc = ibcPathNoFallback ibcsd f

1262− i <- getIState

1264+ i <- getIState

1263− addHides (hide_list i)

1265+ addHides (hide_list i)

1266+

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

1268+

1264− ok <- noErrors

1269+ ok <- noErrors

1265− when ok $

1270+ when ok $

1266− idrisCatch (do writeIBC f ibc; clearIBC)

1271+ idrisCatch (do writeIBC f ibc; clearIBC)

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

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

1268− i <- getIState

1273+ i <- getIState

1269− putIState (i { default_total = def_total,

1274+ putIState (i { default_total = def_total,

1270− hide_list = [] })

1275+ hide_list = [] })

1271− return ()

1272 return ()

1276 return ()

1273 where

1277 where

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

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

src/Pkg/Package.hs+6−6

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

57 _ -> return ()

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

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

60− [] -> when install $ installPkg pkgdesc

60+ _ -> when install $ installPkg pkgdesc

61− ms -> do if install

61+-- ms -> do if install

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

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

63− else putStrLn "There are undefined metavariables:"

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

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

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

65− exitWith (ExitFailure 1)

65+-- exitWith (ExitFailure 1)

67-- | Type check packages only

68--