git.iko.soy/Idris-dev
on master help sign in
Add support to keep track of records in IState

- Define a new data type to store information about records (RecordInfo) In particular: parameters, constructor and projections - Add a new field to IState (idris_records) - Update record elaboration so that the elaborated record is added to idris_records

commit555feb5dbf22428c4b69258eb2c3fa6e0c0395c3 authorGuglielmo Fachini <guglielmo@fachini.net> dateTue 1 Sep 2015, 22:59 (11 years ago) parent4932d1c
3 files changed+17−1
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+4 src/Idris/AbsSyntaxTree.hs+8−1 src/Idris/Elab/Record.hs+5
src/Idris/AbsSyntax.hs+4
@@ -397,6 +397,10 @@ addClass n i
397397 _ -> i
398398 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
399399
400+addRecord :: Name -> RecordInfo -> Idris ()
401+addRecord n ri = do ist <- getIState
402+ putIState $ ist { idris_records = addDef n ri (idris_records ist) }
403+
400404addAutoHint :: Name -> Name -> Idris ()
401405addAutoHint n hint =
402406 do ist <- getIState
src/Idris/AbsSyntaxTree.hs+8−1
@@ -177,6 +177,7 @@ data IState = IState {
177177 idris_implicits :: Ctxt [PArg],
178178 idris_statics :: Ctxt [Bool],
179179 idris_classes :: Ctxt ClassInfo,
180+ idris_records :: Ctxt RecordInfo,
180181 idris_dsls :: Ctxt DSL,
181182 idris_optimisation :: Ctxt OptInfo,
182183 idris_datatypes :: Ctxt TypeInfo,
@@ -336,7 +337,7 @@ idrisInit = IState initContext S.empty []
336337 emptyContext emptyContext emptyContext emptyContext
337338 emptyContext emptyContext emptyContext emptyContext
338339 emptyContext emptyContext emptyContext emptyContext
339− emptyContext
340+ emptyContext emptyContext
340341 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
341342 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
342343 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
@@ -1277,6 +1278,12 @@ deriving instance Binary ClassInfo
12771278deriving instance NFData ClassInfo
12781279!-}
12791280
1281+-- Record data
1282+data RecordInfo = RI { record_parameters :: [(Name,PTerm)],
1283+ record_constructor :: Name,
1284+ record_projections :: [Name] }
1285+ deriving Show
1286+
12801287-- Type inference data
12811288
12821289data TIData = TIPartial -- ^ a function with a partially defined type
src/Idris/Elab/Record.hs+5
@@ -64,6 +64,11 @@ elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc
6464 _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
6565 elabData info rsyn doc paramDocs fc opts datadecl
6666
67+ -- Keep track of the record
68+ let parameters = [(n,pt) | (n, _, _, pt) <- params]
69+ let projections = [n | (n, _, _, _, _) <- fieldsWithName]
70+ addRecord tyn (RI parameters dconName projections)
71+
6772 when (what /= ETypes) $ do
6873 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
6974 logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc