git.iko.soy/Idris-dev
on master help sign in
More record stuff.
0269d05Sune Alkaersig
src/Idris/AbsSyntax.hs+2−5
compare with master
unifiedsplit
@@ -1075,11 +1075,8 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)
1075 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1075 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)
1076 econ (doc, argDocs, n, t, fc, fs)
1076 econ (doc, argDocs, n, t, fc, fs)
1077 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1077 = (doc, argDocs, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)
1078−expandParamsD rhs ist dec ps ns (PRecord doc syn fc opts n prs pdocs fls fdocs cn cdoc csyn)
1078+expandParamsD rhs ist dec ps ns d@(PRecord doc rsyn fc opts name prs pdocs fls cn cdoc csyn)
1079− = PRecord doc syn fc opts n prs pdocs
1079+ = d
1080− fls fdocs
1081− cn cdoc csyn
1082−
1083expandParamsD rhs ist dec ps ns (PParams f params pds)
1080expandParamsD rhs ist dec ps ns (PParams f params pds)
1084 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1081 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)
1085 (map (expandParamsD True ist dec ps ns) pds)
1082 (map (expandParamsD True ist dec ps ns) pds)
src/Idris/AbsSyntaxTree.hs+5−9
@@ -599,9 +599,8 @@ data PDecl' t
599 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
599 | PRecord (Docstring (Either Err PTerm)) SyntaxInfo FC DataOpts
600 Name -- Record name
600 Name -- Record name
601 [(Name, Plicity, t)] -- Parameters
601 [(Name, Plicity, t)] -- Parameters
602− [(Name, Docstring (Either Err PTerm))] -- Parameter docs
602+ [(Name, Docstring (Either Err PTerm))] -- Param Docs
603− [(Name, Plicity, t)] -- Fields
604− [(Name, Docstring (Either Err PTerm))] -- Fields doc
603+ [((Maybe Name), Plicity, t, Maybe (Docstring (Either Err PTerm)))] -- Fields
605 (Maybe Name) -- Optional constructor name
604 (Maybe Name) -- Optional constructor name
606 (Docstring (Either Err PTerm)) -- Constructor doc
605 (Docstring (Either Err PTerm)) -- Constructor doc
607 SyntaxInfo -- Constructor SyntaxInfo
606 SyntaxInfo -- Constructor SyntaxInfo
@@ -707,8 +706,7 @@ declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
707declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
706declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]
708declared (PParams _ _ ds) = concatMap declared ds
707declared (PParams _ _ ds) = concatMap declared ds
709declared (PNamespace _ ds) = concatMap declared ds
708declared (PNamespace _ ds) = concatMap declared ds
710−declared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : maybeToList cn -- : (map fstt ps) ++ (map fstt fs) ++ maybeToList cn
709+declared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
711− where fstt (a, _, _) = a
712declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms
710declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms
713declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
711declared (PInstance _ _ _ _ _ _ _ _ _ _) = []
714declared (PDSL n _) = [n]
712declared (PDSL n _) = [n]
@@ -723,8 +721,7 @@ tldeclared (PFix _ _ _) = []
723tldeclared (PTy _ _ _ _ _ n t) = [n]
721tldeclared (PTy _ _ _ _ _ n t) = [n]
724tldeclared (PPostulate _ _ _ _ n t) = [n]
722tldeclared (PPostulate _ _ _ _ n t) = [n]
725tldeclared (PClauses _ _ n _) = [] -- not a declaration
723tldeclared (PClauses _ _ n _) = [] -- not a declaration
726−tldeclared (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : maybeToList cn -- (map fstt ps) ++ (map fstt fs) ++ maybeToList cn
724+tldeclared (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
727− where fstt (a, _, _) = a
728tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
725tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
729 where fstt (_, _, a, _, _, _) = a
726 where fstt (_, _, a, _, _, _) = a
730tldeclared (PParams _ _ ds) = []
727tldeclared (PParams _ _ ds) = []
@@ -745,8 +742,7 @@ defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts
745defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
742defined (PData _ _ _ _ _ (PLaterdecl n _)) = []
746defined (PParams _ _ ds) = concatMap defined ds
743defined (PParams _ _ ds) = concatMap defined ds
747defined (PNamespace _ ds) = concatMap defined ds
744defined (PNamespace _ ds) = concatMap defined ds
748−defined (PRecord _ _ _ _ n ps _ fs _ cn _ _) = n : maybeToList cn -- (map fstt ps) ++ (map fstt fs) ++ maybeToList cn
745+defined (PRecord _ _ _ _ n _ _ _ cn _ _) = n : maybeToList cn
749− where fstt (a, _, _) = a
750defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms
746defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms
751defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
747defined (PInstance _ _ _ _ _ _ _ _ _ _) = []
752defined (PDSL n _) = [n]
748defined (PDSL n _) = [n]
src/Idris/DeepSeq.hs+2−2
@@ -144,11 +144,11 @@ instance (NFData t) => NFData (PDecl' t) where
144 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
144 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
145 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
145 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()
146 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
146 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()
147− rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
147+ rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
148 = rnf x1 `seq`
148 = rnf x1 `seq`
149 rnf x2 `seq`
149 rnf x2 `seq`
150 rnf x3 `seq`
150 rnf x3 `seq`
151− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()
151+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()
152 rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)
152 rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)
153 = rnf x1 `seq`
153 = rnf x1 `seq`
154 rnf x2 `seq`
154 rnf x2 `seq`
src/Idris/Elab/Record.hs+109−45
@@ -15,7 +15,7 @@ import Data.Maybe
15import Data.List
15import Data.List
16import Control.Monad
16import Control.Monad
17
17
18−elabRecord :: ElabInfo ->
18+elabRecord :: ElabInfo ->
19 (Docstring (Either Err PTerm)) ->
19 (Docstring (Either Err PTerm)) ->
20 SyntaxInfo ->
20 SyntaxInfo ->
21 FC ->
21 FC ->
@@ -23,13 +23,12 @@ elabRecord :: ElabInfo ->
23 Name -> -- ^ Record Type Name
23 Name -> -- ^ Record Type Name
24 [(Name, Plicity, PTerm)] -> -- ^ Parameters
24 [(Name, Plicity, PTerm)] -> -- ^ Parameters
25 [(Name, Docstring (Either Err PTerm))] -> -- ^ Parameter Docs
25 [(Name, Docstring (Either Err PTerm))] -> -- ^ Parameter Docs
26− [(Name, Plicity, PTerm)] -> -- ^ Fields
27− [(Name, Docstring (Either Err PTerm))] -> -- ^ Field Docs
26+ [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> -- ^ Fields
28 Maybe Name -> -- ^ Constructor Name
27 Maybe Name -> -- ^ Constructor Name
29 (Docstring (Either Err PTerm)) -> -- ^ Constructor Doc
28 (Docstring (Either Err PTerm)) -> -- ^ Constructor Doc
30 SyntaxInfo -> -- ^ Constructor SyntaxInfo
29 SyntaxInfo -> -- ^ Constructor SyntaxInfo
31 Idris ()
30 Idris ()
32−elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdoc csyn
31+elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
33 = do logLvl 1 $ "Building data declaration for " ++ show tyn
32 = do logLvl 1 $ "Building data declaration for " ++ show tyn
34 -- Type constructor
33 -- Type constructor
35 let tycon = generateTyConType params
34 let tycon = generateTyConType params
@@ -37,16 +36,105 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
37
36
38 -- Data constructor
37 -- Data constructor
39 dconName <- generateDConName cname
38 dconName <- generateDConName cname
40− let dconTy = generateDConType params fields
39+ let dconTy = generateDConType params fieldsWithNameAndDoc
41 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy
40 logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy
42−
41+
43 -- Build data declaration for elaboration
42 -- Build data declaration for elaboration
44− let datadecl = PDatadecl tyn tycon [(cdoc, [], dconName, dconTy, fc, [])]
43+ let datadecl = PDatadecl tyn tycon [(cdoc, dconsArgDocs, dconName, dconTy, fc, [])]
45− elabData info rsyn doc [] fc opts datadecl
44+ elabData info rsyn doc paramDocs fc opts datadecl
45+
46+ iLOG $ "fieldsWithName " ++ show fieldsWithName
47+ iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
48+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
49+ where
50+ -- | Generates a type constructor.
51+ generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm
52+ generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)
53+ generateTyConType [] = PType
46
54
55+ -- | Generates a name for the data constructor if none was specified.
56+ generateDConName :: Maybe Name -> Idris Name
57+ generateDConName (Just n) = return $ expandNS csyn n
58+ generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
59+ where
60+ uniqueName :: Name -> Idris Name
47− i <- getIState
61+ uniqueName n = do i <- getIState
62+ case lookupTyNameExact n (tt_ctxt i) of
63+ Just _ -> uniqueName (nextName n)
64+ Nothing -> return n
65+
66+ -- | Generates the data constructor type.
67+ generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm
68+ generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)
69+ generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) t (generateDConType [] as)
70+ generateDConType [] [] = target
71+
72+ -- | The target for the constructor and projection functions. Also the source of the update functions.
73+ target :: PTerm
74+ target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, _) <- params]
75+
76+ paramsAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
77+ paramsAndDoc = pad params paramDocs
78+ where
79+ pad :: [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
80+ pad ((n, p, t) : rest) docs
81+ = let d = case lookup n docs of
82+ Just d' -> d
83+ Nothing -> emptyDocstring
84+ in (n, p, t, d) : (pad rest docs)
85+ pad _ _ = []
86+
87+ dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
88+ dconsArgDocs = paramDocs ++ (dcad fieldsWithName)
89+ where
90+ dcad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]
91+ dcad ((n, _, _, (Just d)) : rest) = (n, d) : (dcad rest)
92+ dcad (_ : rest) = dcad rest
93+ dcad [] = []
94+
95+ fieldsWithName :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
96+ fieldsWithName = fwn [] fields
97+ where
98+ fwn :: [Name] -> [(Maybe Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
99+ fwn ns ((n, p, t, d) : rest)
100+ = let nn = case n of
101+ Just n' -> n'
102+ Nothing -> newName ns baseName
103+ in (expandNS rsyn $ nn, p, t, d) : (fwn (nn : ns) rest)
104+ fwn _ _ = []
105+
106+ baseName = sUN "__pi_arg"
107+
108+ newName :: [Name] -> Name -> Name
109+ newName ns n
110+ | n `elem` ns = newName ns (nextName n)
111+ | otherwise = n
112+
113+ fieldsWithNameAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
114+ fieldsWithNameAndDoc = fwnad fieldsWithName
115+ where
116+ fwnad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
117+ fwnad ((n, p, t, d) : rest)
118+ = let doc = fromMaybe emptyDocstring d
119+ in (n, p, t, doc) : (fwnad rest)
120+ fwnad [] = []
48
121
122+elabRecordFunctions :: ElabInfo ->
123+ SyntaxInfo ->
124+ FC ->
125+ Name -> -- ^ Record Type Name
126+ [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -> -- ^ Parameters
127+ [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]-> -- ^ Fields
128+ Name -> -- ^ Constructor Name
129+ PTerm -> -- ^ Target Type
130+ Idris ()
131+elabRecordFunctions info rsyn fc tyn params fields dconName target
132+ = do logLvl 1 $ "Elaborating helper functions for record " ++ show tyn
133+
134+ iLOG $ "Fields: " ++ show fieldNames
135+ iLOG $ "Params: " ++ show paramNames
49 -- The elaborated constructor type for the data declaration
136 -- The elaborated constructor type for the data declaration
137+ i <- getIState
50 ttConsTy <-
138 ttConsTy <-
51 case lookupTyExact dconName (tt_ctxt i) of
139 case lookupTyExact dconName (tt_ctxt i) of
52 Just as -> return as
140 Just as -> return as
@@ -54,15 +142,17 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
54
142
55 -- The arguments to the constructor
143 -- The arguments to the constructor
56 let constructorArgs = getArgTys ttConsTy
144 let constructorArgs = getArgTys ttConsTy
145+ iLOG $ "Cons args: " ++ show constructorArgs
146+ iLOG $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)
57 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
147 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
58 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
148 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
59
149
60 -- The parameters for elaboration with their documentation
150 -- The parameters for elaboration with their documentation
61 -- Parameter functions are all prefixed with "param_".
151 -- Parameter functions are all prefixed with "param_".
62− let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, t, d) <- zipParams i params paramDocs]
152+ let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, t, d) <- params] -- zipParams i params paramDocs]
63
153
64 -- The fields (written by the user) with their documentation.
154 -- The fields (written by the user) with their documentation.
65− let userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
155+ let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, p, t, d) <- fields]
66
156
67 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
157 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
68 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
158 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
@@ -78,46 +168,16 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
78 -- Build and elaborate update functions
168 -- Build and elaborate update functions
79 elabUp dconName updaters
169 elabUp dconName updaters
80 where
170 where
81− -- | Generates a type constructor.
82− generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm
83− generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)
84− generateTyConType [] = PType
85−
86− -- | Generates a name for the data constructor if none was specified.
87− generateDConName :: Maybe Name -> Idris Name
88− generateDConName (Just n) = return $ expandNS csyn n
89− generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
90− where
91− uniqueName :: Name -> Idris Name
92− uniqueName n = do i <- getIState
93− case lookupTyNameExact n (tt_ctxt i) of
94− Just _ -> uniqueName (nextName n)
95− Nothing -> return n
96−
97− -- | Generates the data constructor type.
98− generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
99− generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)
100− generateDConType [] ((n, p, t) : as) = PPi p (nsroot n) t (generateDConType [] as)
101− generateDConType [] [] = target
102−
103− -- | Creates an PArg from a plicity and a name where the term is a PRef.
104− asPRefArg :: Plicity -> Name -> PArg
105− asPRefArg p n = asArg p (nsroot n) $ PRef fc (nsroot n)
106−
107− -- | The target for the constructor and projection functions. Also the source of the update functions.
108− target :: PTerm
109− target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, t) <- params]
110−
111 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
171 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
112 placeholderArg :: Plicity -> Name -> PArg
172 placeholderArg :: Plicity -> Name -> PArg
113 placeholderArg p n = asArg p (nsroot n) Placeholder
173 placeholderArg p n = asArg p (nsroot n) Placeholder
114
174
115 -- | Root names of all fields in the current record declarations
175 -- | Root names of all fields in the current record declarations
116 fieldNames :: [Name]
176 fieldNames :: [Name]
117− fieldNames = [nsroot n | (n, _, _) <- fields]
177+ fieldNames = [nsroot n | (n, _, _, _) <- fields]
118
178
119 paramNames :: [Name]
179 paramNames :: [Name]
120− paramNames = [nsroot n | (n, _, _) <- params]
180+ paramNames = [nsroot n | (n, _, _, _) <- params]
121
181
122 isFieldOrParam :: Name -> Bool
182 isFieldOrParam :: Name -> Bool
123 isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
183 isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
@@ -132,7 +192,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
132 isField' (n, _, _, _, _, _) = isField n
192 isField' (n, _, _, _, _, _) = isField n
133
193
134 fieldTerms :: [PTerm]
194 fieldTerms :: [PTerm]
135− fieldTerms = [t | (_, _, t) <- fields]
195+ fieldTerms = [t | (_, _, t, _) <- fields]
136
196
137 -- Delabs the TT to PTerm
197 -- Delabs the TT to PTerm
138 -- This is not good.
198 -- This is not good.
@@ -186,7 +246,7 @@ elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdo
186
246
187 -- | A map from a field name to the other fields it depends on.
247 -- | A map from a field name to the other fields it depends on.
188 fieldDependencies :: [(Name, [Name])]
248 fieldDependencies :: [(Name, [Name])]
189− fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields ++ params]
249+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t, _) <- fields ++ params]
190 where
250 where
191 fieldDep :: Name -> PTerm -> (Name, [Name])
251 fieldDep :: Name -> PTerm -> (Name, [Name])
192 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
252 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
@@ -363,3 +423,7 @@ projectInType xs = mapPT st
363 st (PRef fc n)
423 st (PRef fc n)
364 | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
424 | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
365 st t = t
425 st t = t
426+
427+-- | Creates an PArg from a plicity and a name where the term is a PRef.
428+asPRefArg :: Plicity -> Name -> PArg
429+asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC (nsroot n)
src/Idris/ElabDecls.hs+2−2
@@ -236,10 +236,10 @@ elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)
236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)
236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)
237 = do iLOG $ "Elaborating instance " ++ show n
237 = do iLOG $ "Elaborating instance " ++ show n
238 elabInstance info s doc argDocs what f cs n ps t expn ds
238 elabInstance info s doc argDocs what f cs n ps t expn ds
239−elabDecl' what info (PRecord doc rsyn fc opts name ps pdocs fs fdocs cname cdoc csyn)
239+elabDecl' what info (PRecord doc rsyn fc opts name ps pdocs fs cname cdoc csyn)
240 | what /= ETypes
240 | what /= ETypes
241 = do iLOG $ "Elaborating record " ++ show name
241 = do iLOG $ "Elaborating record " ++ show name
242− elabRecord info doc rsyn fc opts name ps pdocs fs fdocs cname cdoc csyn
242+ elabRecord info doc rsyn fc opts name ps pdocs fs cname cdoc csyn
243{-
243{-
244 | otherwise
244 | otherwise
245 = do iLOG $ "Elaborating [type of] " ++ show tyn
245 = do iLOG $ "Elaborating [type of] " ++ show tyn
src/Idris/IBC.hs+2−4
@@ -1227,7 +1227,7 @@ instance (Binary t) => Binary (PDecl' t) where
1227 PNamespace x1 x2 -> do putWord8 5
1227 PNamespace x1 x2 -> do putWord8 5
1228 put x1
1228 put x1
1229 put x2
1229 put x2
1230− PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ->
1230+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 ->
1231 do putWord8 6
1231 do putWord8 6
1232 put x1
1232 put x1
1233 put x2
1233 put x2
@@ -1240,7 +1240,6 @@ instance (Binary t) => Binary (PDecl' t) where
1240 put x9
1240 put x9
1241 put x10
1241 put x10
1242 put x11
1242 put x11
1243− put x12
1244 PClass x1 x2 x3 x4 x5 x6 x7 x8 x9
1243 PClass x1 x2 x3 x4 x5 x6 x7 x8 x9
1245 -> do putWord8 7
1244 -> do putWord8 7
1246 put x1
1245 put x1
@@ -1343,8 +1342,7 @@ instance (Binary t) => Binary (PDecl' t) where
1343 x9 <- get
1342 x9 <- get
1344 x10 <- get
1343 x10 <- get
1345 x11 <- get
1344 x11 <- get
1346− x12 <- get
1347− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)
1345+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)
1348 7 -> do x1 <- get
1346 7 -> do x1 <- get
1349 x2 <- get
1347 x2 <- get
1350 x3 <- get
1348 x3 <- get
src/Idris/ParseData.hs+15−13
@@ -37,8 +37,6 @@ import qualified Data.ByteString.UTF8 as UTF8
37
37
38import Debug.Trace
38import Debug.Trace
39
39
40−type Docs = Docstring (Either Err PTerm)
41−
42{- |Parses a record type declaration
40{- |Parses a record type declaration
43Record ::=
41Record ::=
44 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
42 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
@@ -60,11 +58,11 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
60 let rsyn = syn { syn_namespace = show (nsroot tyn) :
58 let rsyn = syn { syn_namespace = show (nsroot tyn) :
61 syn_namespace syn }
59 syn_namespace syn }
62 params <- manyTill (recordParameter rsyn) (reserved "where")
60 params <- manyTill (recordParameter rsyn) (reserved "where")
63− (fields, fieldDocs, cname, cdoc) <- indentedBlockS $ agdaStyleBody rsyn tyn
61+ (fields, cname, cdoc) <- indentedBlockS $ agdaStyleBody rsyn tyn
64 case cname of
62 case cname of
65 Just cn' -> accData acc tyn [cn']
63 Just cn' -> accData acc tyn [cn']
66 Nothing -> return ()
64 Nothing -> return ()
67− return $ PRecord doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdoc syn
65+ return $ PRecord doc rsyn fc opts tyn params paramDocs fields cname cdoc syn
68 <?> "record type declaration"
66 <?> "record type declaration"
69 where
67 where
70 getRecNames :: SyntaxInfo -> PTerm -> [Name]
68 getRecNames :: SyntaxInfo -> PTerm -> [Name]
@@ -76,7 +74,7 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
76 toFreeze (Just Frozen) = Just Hidden
74 toFreeze (Just Frozen) = Just Hidden
77 toFreeze x = x
75 toFreeze x = x
78
76
79− agdaStyleBody :: SyntaxInfo -> Name -> IdrisParser ([(Name, Plicity, PTerm)], [(Name, Docs)], Maybe Name, Docs)
77+ agdaStyleBody :: SyntaxInfo -> Name -> IdrisParser ([((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))], Maybe Name, Docstring (Either Err PTerm))
80 agdaStyleBody syn tyn = do
78 agdaStyleBody syn tyn = do
81 ist <- get
79 ist <- get
82 fc <- getFC
80 fc <- getFC
@@ -89,20 +87,24 @@ record syn = do (doc, paramDocs, acc, opts) <- try (do
89 let constructorDoc' = annotate syn ist constructorDoc
87 let constructorDoc' = annotate syn ist constructorDoc
90
88
91 fields <- many . indented $ field syn
89 fields <- many . indented $ field syn
92−
93− let fieldDocs = [(n, annotate syn ist doc) | (n, _, _, doc) <- fields]
94− let fields' = [(n, p, t) | (n, t, p, _) <- fields]
95
90
96− return (fields', fieldDocs, constructorName, constructorDoc')
91+ return (fields, constructorName, constructorDoc')
97 where
92 where
98− field :: SyntaxInfo -> IdrisParser (Name, PTerm, Plicity, Docstring ())
93+ field :: SyntaxInfo -> IdrisParser ((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))
99− field syn = do (doc, _) <- option noDocs docComment
94+ field syn = do doc <- optional docComment
100 c <- optional $ lchar '{'
95 c <- optional $ lchar '{'
96+ n <- (do n <- fnName
97+ return $ Just (expandNS syn n))
101− n <- fnName <|> do symbol "_"; return $ sUN "__pi_arg"
98+ <|> (do symbol "_"
99+ return Nothing)
102 lchar ':'
100 lchar ':'
103 t <- typeExpr (allowImp syn)
101 t <- typeExpr (allowImp syn)
104 p <- endPlicity c
102 p <- endPlicity c
105− return (expandNS syn n, t, p, doc)
103+ ist <- get
104+ let doc' = case doc of
105+ Just (d,_) -> Just $ annotate syn ist d
106+ Nothing -> Nothing
107+ return (n, p, t, doc')
106
108
107 constructor :: IdrisParser Name
109 constructor :: IdrisParser Name
108 constructor = (reserved "constructor") *> fnName
110 constructor = (reserved "constructor") *> fnName