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

git.iko.soy/Idris-dev

Add support to keep track of records in IBC files

commit3f31e4efd56cd0ddf86f0904bee12fb9cac99e6b authorGuglielmo Fachini <guglielmo@fachini.net> dateTue 1 Sep 2015, 23:33 (11 years ago) parent555feb5

4 files changed+32−1

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/DeepSeq.hs+4 src/Idris/Elab/Record.hs+1 src/Idris/IBC.hs+26−1

src/Idris/AbsSyntaxTree.hs+1

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

291291 | IBCImp Name

292292 | IBCStatic Name

293293 | IBCClass Name

294+ | IBCRecord Name

294295 | IBCInstance Bool Bool Name Name

295296 | IBCDSL Name

296297 | IBCData Name

src/Idris/DeepSeq.hs+4

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

346346 = rnf x1 `seq`

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

348348

349+instance NFData RecordInfo where

350+ rnf (RI x1 x2 x3)

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

352+

349353instance NFData OptInfo where

350354 rnf (Optimise x1 x2)

351355 = 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

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

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

7070 addRecord tyn (RI parameters dconName projections)

71+ addIBC (IBCRecord tyn)

7172

7273 when (what /= ETypes) $ do

7374 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

src/Idris/IBC.hs+26−1

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

5050 ibc_fixes :: ![FixDecl],

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

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

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

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

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

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

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

9394!-}

9495

9596initIBC :: IBCFile

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

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

9798

9899hasValidIBCVersion :: FilePath -> Idris Bool

99100hasValidIBCVersion fp = do

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

142143 makeEntry "ibc_fixes" (ibc_fixes i),

143144 makeEntry "ibc_statics" (ibc_statics i),

144145 makeEntry "ibc_classes" (ibc_classes i),

146+ makeEntry "ibc_records" (ibc_records i),

145147 makeEntry "ibc_instances" (ibc_instances i),

146148 makeEntry "ibc_dsls" (ibc_dsls i),

147149 makeEntry "ibc_datatypes" (ibc_datatypes i),

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

234236 = case lookupCtxtExact n (idris_classes i) of

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

236238 _ -> 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"

237243ibc i (IBCInstance int res n ins) f

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

239245ibc i (IBCDSL n) f

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

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

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

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

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

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

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

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

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

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

443450 cs

444451

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+

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

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

447461

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

21302144 x6 <- get

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

21322146

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+

21332158instance Binary OptInfo where

21342159 put (Optimise x1 x2)

21352160 = do put x1