git.iko.soy/Idris-dev
on master help sign in
Allow mutually recursive records
bf6c327Edwin Brady
src/Idris/Elab/Record.hs+13−9
compare with master
unifiedsplit
@@ -34,6 +34,7 @@ import Control.Monad
34
34
35-- | Elaborate a record declaration
35-- | Elaborate a record declaration
36elabRecord :: ElabInfo
36elabRecord :: ElabInfo
37+ -> ElabWhat
37 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
38 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
38 -> SyntaxInfo -> FC -> DataOpts
39 -> SyntaxInfo -> FC -> DataOpts
39 -> Name -- ^ The name of the type being defined
40 -> Name -- ^ The name of the type being defined
@@ -45,7 +46,7 @@ elabRecord :: ElabInfo
45 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc
46 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc
46 -> SyntaxInfo -- ^ Constructor SyntaxInfo
47 -> SyntaxInfo -- ^ Constructor SyntaxInfo
47 -> Idris ()
48 -> Idris ()
48−elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
49+elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
49 = do logLvl 1 $ "Building data declaration for " ++ show tyn
50 = do logLvl 1 $ "Building data declaration for " ++ show tyn
50 -- Type constructor
51 -- Type constructor
51 let tycon = generateTyConType params
52 let tycon = generateTyConType params
@@ -58,17 +59,20 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
58
59
59 -- Build data declaration for elaboration
60 -- Build data declaration for elaboration
60 logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)
61 logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)
62+ let datadecl = case what of
63+ ETypes -> PLaterdecl tyn NoFC tycon
61− let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
64+ _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
62 elabData info rsyn doc paramDocs fc opts datadecl
65 elabData info rsyn doc paramDocs fc opts datadecl
63
66
67+ when (what /= ETypes) $ do
64− logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
68+ logLvl 1 $ "fieldsWithName " ++ show fieldsWithName
65− logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
69+ logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
66− elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
70+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
67
71
68− sendHighlighting $
72+ sendHighlighting $
69− [(nfc, AnnName tyn Nothing Nothing Nothing)] ++
73+ [(nfc, AnnName tyn Nothing Nothing Nothing)] ++
70− maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++
74+ maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++
71− [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]
75+ [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]
72
76
73 where
77 where
74 -- | Generates a type constructor.
78 -- | Generates a type constructor.
src/Idris/ElabDecls.hs+1−2
@@ -245,9 +245,8 @@ elabDecl' what info (PInstance doc argDocs s f cs n nfc ps t expn ds)
245 = do logLvl 1 $ "Elaborating instance " ++ show n
245 = do logLvl 1 $ "Elaborating instance " ++ show n
246 elabInstance info s doc argDocs what f cs n nfc ps t expn ds
246 elabInstance info s doc argDocs what f cs n nfc ps t expn ds
247elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)
247elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)
248− | what /= ETypes
249 = do logLvl 1 $ "Elaborating record " ++ show name
248 = do logLvl 1 $ "Elaborating record " ++ show name
250− elabRecord info doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn
249+ elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn
251{-
250{-
252 | otherwise
251 | otherwise
253 = do logLvl 1 $ "Elaborating [type of] " ++ show tyn
252 = do logLvl 1 $ "Elaborating [type of] " ++ show tyn