bf6c327 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow mutually recursive records

Fixes #2248. The record type can be used anywhere in the mutual block, but not the projections which are considered part of the definition.

commitbf6c327105d0cd4dcf449fac58350a9f942bded2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 9 Aug 2015, 16:33 (11 years ago) parent57ba18d

2 files changed+14−11

compare with master

unifiedsplit

src/Idris/Elab/Record.hs+13−9 src/Idris/ElabDecls.hs+1−2

src/Idris/Elab/Record.hs+13−9

@@ -34,6 +34,7 @@ import Control.Monad

3434

3535-- | Elaborate a record declaration

3636elabRecord :: ElabInfo

37+ -> ElabWhat

3738 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration

3839 -> SyntaxInfo -> FC -> DataOpts

3940 -> Name -- ^ The name of the type being defined

@@ -45,7 +46,7 @@ elabRecord :: ElabInfo

4546 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc

4647 -> SyntaxInfo -- ^ Constructor SyntaxInfo

4748 -> 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

4950 = do logLvl 1 $ "Building data declaration for " ++ show tyn

5051 -- Type constructor

5152 let tycon = generateTyConType params

@@ -58,17 +59,20 @@ elabRecord info doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn

5859

5960 -- Build data declaration for elaboration

6061 logLvl 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)

61− let datadecl = PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

62+ let datadecl = case what of

63+ ETypes -> PLaterdecl tyn NoFC tycon

64+ _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]

6265 elabData info rsyn doc paramDocs fc opts datadecl

6366

64− logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

65− logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

66− elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

67+ when (what /= ETypes) $ do

68+ logLvl 1 $ "fieldsWithName " ++ show fieldsWithName

69+ logLvl 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc

70+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target

6771

68− sendHighlighting $

69− [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

70− maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

71− [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

72+ sendHighlighting $

73+ [(nfc, AnnName tyn Nothing Nothing Nothing)] ++

74+ maybe [] (\(_, cnfc) -> [(cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++

75+ [(ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]

7276

7377 where

7478 -- | 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)

245245 = do logLvl 1 $ "Elaborating instance " ++ show n

246246 elabInstance info s doc argDocs what f cs n nfc ps t expn ds

247247elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

248− | what /= ETypes

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

251250{-

252251 | otherwise

253252 = do logLvl 1 $ "Elaborating [type of] " ++ show tyn