git.iko.soy/Idris-dev
on master help sign in
Add support to keep track of records in IState
555feb5Guglielmo Fachini
src/Idris/AbsSyntax.hs+4
compare with master
unifiedsplit
@@ -397,6 +397,10 @@ addClass n i
397 _ -> i
397 _ -> i
398 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
398 putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }
399
399
400+addRecord :: Name -> RecordInfo -> Idris ()
401+addRecord n ri = do ist <- getIState
402+ putIState $ ist { idris_records = addDef n ri (idris_records ist) }
403+
400addAutoHint :: Name -> Name -> Idris ()
404addAutoHint :: Name -> Name -> Idris ()
401addAutoHint n hint =
405addAutoHint n hint =
402 do ist <- getIState
406 do ist <- getIState
src/Idris/AbsSyntaxTree.hs+8−1
@@ -177,6 +177,7 @@ data IState = IState {
177 idris_implicits :: Ctxt [PArg],
177 idris_implicits :: Ctxt [PArg],
178 idris_statics :: Ctxt [Bool],
178 idris_statics :: Ctxt [Bool],
179 idris_classes :: Ctxt ClassInfo,
179 idris_classes :: Ctxt ClassInfo,
180+ idris_records :: Ctxt RecordInfo,
180 idris_dsls :: Ctxt DSL,
181 idris_dsls :: Ctxt DSL,
181 idris_optimisation :: Ctxt OptInfo,
182 idris_optimisation :: Ctxt OptInfo,
182 idris_datatypes :: Ctxt TypeInfo,
183 idris_datatypes :: Ctxt TypeInfo,
@@ -336,7 +337,7 @@ idrisInit = IState initContext S.empty []
336 emptyContext emptyContext emptyContext emptyContext
337 emptyContext emptyContext emptyContext emptyContext
337 emptyContext emptyContext emptyContext emptyContext
338 emptyContext emptyContext emptyContext emptyContext
338 emptyContext emptyContext emptyContext emptyContext
339 emptyContext emptyContext emptyContext emptyContext
339− emptyContext
340+ emptyContext emptyContext
340 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
341 [] [] [] defaultOpts 6 [] [] [] [] emptySyntaxRules [] [] [] [] [] [] []
341 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
342 [] [] Nothing [] Nothing [] [] Nothing Nothing [] Hidden False [] Nothing [] []
342 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
343 (RawOutput stdout) True defaultTheme [] (0, emptyContext) emptyContext M.empty
@@ -1277,6 +1278,12 @@ deriving instance Binary ClassInfo
1277deriving instance NFData ClassInfo
1278deriving instance NFData ClassInfo
1278!-}
1279!-}
1279
1280
1281+-- Record data
1282+data RecordInfo = RI { record_parameters :: [(Name,PTerm)],
1283+ record_constructor :: Name,
1284+ record_projections :: [Name] }
1285+ deriving Show
1286+
1280-- Type inference data
1287-- Type inference data
1281
1288
1282data TIData = TIPartial -- ^ a function with a partially defined type
1289data 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
64 _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
64 _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
65 elabData info rsyn doc paramDocs fc opts datadecl
65 elabData info rsyn doc paramDocs fc opts datadecl
66
66
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+
67 when (what /= ETypes) $ do
72 when (what /= ETypes) $ do
68 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
73 logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
69 logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
74 logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc