3f31e4e · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add support to keep track of records in IBC files

3f31e4eGuglielmo Fachini11 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

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

291 | IBCImp Name

292 | IBCStatic Name

293 | IBCClass Name

294+ | IBCRecord Name

294 | IBCInstance Bool Bool Name Name

295 | IBCInstance Bool Bool Name Name

295 | IBCDSL Name

296 | IBCDSL Name

296 | IBCData Name

297 | IBCData Name

src/Idris/DeepSeq.hs+4

@@ -346,6 +346,10 @@ instance NFData ClassInfo where

346 = rnf x1 `seq`

347 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

348

349+instance NFData RecordInfo where

350+ rnf (RI x1 x2 x3)

351+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

352+

349instance NFData OptInfo where

353instance NFData OptInfo where

350 rnf (Optimise x1 x2)

354 rnf (Optimise x1 x2)

351 = rnf x1 `seq` rnf x2 `seq` ()

355 = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Elab/Record.hs+1

@@ -68,6 +68,7 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc

68 let parameters = [(n,pt) | (n, _, _, pt) <- params]

69 let projections = [n | (n, _, _, _, _) <- fieldsWithName]

70 addRecord tyn (RI parameters dconName projections)

71+ addIBC (IBCRecord tyn)

72 when (what /= ETypes) $ do

73 when (what /= ETypes) $ do

73 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

74 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

src/Idris/IBC.hs+26−1

@@ -50,6 +50,7 @@ data IBCFile = IBCFile { ver :: Word16,

50 ibc_fixes :: ![FixDecl],

51 ibc_statics :: ![(Name, [Bool])],

52 ibc_classes :: ![(Name, ClassInfo)],

53+ ibc_records :: ![(Name, RecordInfo)],

53 ibc_instances :: ![(Bool, Bool, Name, Name)],

54 ibc_instances :: ![(Bool, Bool, Name, Name)],

54 ibc_dsls :: ![(Name, DSL)],

55 ibc_dsls :: ![(Name, DSL)],

55 ibc_datatypes :: ![(Name, TypeInfo)],

56 ibc_datatypes :: ![(Name, TypeInfo)],

@@ -93,7 +94,7 @@ deriving instance Binary IBCFile

93!-}

94!-}

95initIBC :: IBCFile

96initIBC :: IBCFile

96−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

97+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] Nothing [] [] []

98hasValidIBCVersion :: FilePath -> Idris Bool

99hasValidIBCVersion :: FilePath -> Idris Bool

99hasValidIBCVersion fp = do

100hasValidIBCVersion fp = do

@@ -142,6 +143,7 @@ entries i = catMaybes [Just $ toEntry "ver" 0 (encode $ ver i),

142 makeEntry "ibc_fixes" (ibc_fixes i),

143 makeEntry "ibc_fixes" (ibc_fixes i),

143 makeEntry "ibc_statics" (ibc_statics i),

144 makeEntry "ibc_statics" (ibc_statics i),

144 makeEntry "ibc_classes" (ibc_classes i),

145 makeEntry "ibc_classes" (ibc_classes i),

146+ makeEntry "ibc_records" (ibc_records i),

145 makeEntry "ibc_instances" (ibc_instances i),

147 makeEntry "ibc_instances" (ibc_instances i),

146 makeEntry "ibc_dsls" (ibc_dsls i),

148 makeEntry "ibc_dsls" (ibc_dsls i),

147 makeEntry "ibc_datatypes" (ibc_datatypes i),

149 makeEntry "ibc_datatypes" (ibc_datatypes i),

@@ -234,6 +236,10 @@ ibc i (IBCClass n) f

234 = case lookupCtxtExact n (idris_classes i) of

236 = case lookupCtxtExact n (idris_classes i) of

235 Just v -> return f { ibc_classes = (n,v): ibc_classes f }

237 Just v -> return f { ibc_classes = (n,v): ibc_classes f }

236 _ -> ifail "IBC write failed"

238 _ -> ifail "IBC write failed"

239+ibc i (IBCRecord n) f

240+ = case lookupCtxtExact n (idris_records i) of

241+ Just v -> return f { ibc_records = (n,v): ibc_records f }

242+ _ -> ifail "IBC write failed"

237ibc i (IBCInstance int res n ins) f

243ibc i (IBCInstance int res n ins) f

238 = return f { ibc_instances = (int, res, n, ins) : ibc_instances f }

244 = return f { ibc_instances = (int, res, n, ins) : ibc_instances f }

239ibc i (IBCDSL n) f

245ibc i (IBCDSL n) f

@@ -324,6 +330,7 @@ process reexp i fn = do

324 pFixes =<< getEntry [] "ibc_fixes" i

330 pFixes =<< getEntry [] "ibc_fixes" i

325 pStatics =<< getEntry [] "ibc_statics" i

331 pStatics =<< getEntry [] "ibc_statics" i

326 pClasses =<< getEntry [] "ibc_classes" i

332 pClasses =<< getEntry [] "ibc_classes" i

333+ pRecords =<< getEntry [] "ibc_records" i

327 pInstances =<< getEntry [] "ibc_instances" i

334 pInstances =<< getEntry [] "ibc_instances" i

328 pDSLs =<< getEntry [] "ibc_dsls" i

335 pDSLs =<< getEntry [] "ibc_dsls" i

329 pDatatypes =<< getEntry [] "ibc_datatypes" i

336 pDatatypes =<< getEntry [] "ibc_datatypes" i

@@ -442,6 +449,13 @@ pClasses cs = mapM_ (\ (n, c) ->

442 = addDef n c' (idris_classes i) }))

449 = addDef n c' (idris_classes i) }))

443 cs

450 cs

444

451

452+pRecords :: [(Name, RecordInfo)] -> Idris ()

453+pRecords rs = mapM_ (\ (n, r) ->

454+ do i <- getIState

455+ putIState (i { idris_records

456+ = addDef n r (idris_records i) }))

457+ rs

458+

445pInstances :: [(Bool, Bool, Name, Name)] -> Idris ()

459pInstances :: [(Bool, Bool, Name, Name)] -> Idris ()

446pInstances cs = mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs

460pInstances cs = mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs

447

461

@@ -2130,6 +2144,17 @@ instance Binary ClassInfo where

2130 x6 <- get

2144 x6 <- get

2131 return (CI x1 x2 x3 x4 x5 [] x6)

2145 return (CI x1 x2 x3 x4 x5 [] x6)

2132

2146

2147+instance Binary RecordInfo where

2148+ put (RI x1 x2 x3)

2149+ = do put x1

2150+ put x2

2151+ put x3

2152+ get

2153+ = do x1 <- get

2154+ x2 <- get

2155+ x3 <- get

2156+ return (RI x1 x2 x3)

2157+

2133instance Binary OptInfo where

2158instance Binary OptInfo where

2134 put (Optimise x1 x2)

2159 put (Optimise x1 x2)

2135 = do put x1

2160 = do put x1