git.iko.soy/Idris-dev
on master help sign in
Idris-dev/src/Idris/Elab/Record.hs
446 lines 21 kB history raw
1{-|
2Module : Idris.Elab.Record
3Description : Code to elaborate records.
5License : BSD3
6Maintainer : The Idris Community.
7-}
8{-# LANGUAGE PatternGuards #-}
9module Idris.Elab.Record(elabRecord) where
11import Idris.AbsSyntax
12import Idris.Core.Evaluate
13import Idris.Core.TT
14import Idris.Delaborate
15import Idris.Docstrings
16import Idris.Elab.Data
17import Idris.Error
18import Idris.Output (sendHighlighting)
20import Control.Monad
21import Data.List
22import Data.Maybe
23import qualified Data.Set as S
25-- | Elaborate a record declaration
26elabRecord :: ElabInfo
27 -> ElabWhat
28 -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
29 -> SyntaxInfo
30 -> FC
31 -> DataOpts
32 -> Name -- ^ The name of the type being defined
33 -> FC -- ^ The precise source location of the tycon name
34 -> [(Name, FC, Plicity, PTerm)] -- ^ Parameters
35 -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs
36 -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields
37 -> Maybe (Name, FC) -- ^ Constructor Name
38 -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc
39 -> SyntaxInfo -- ^ Constructor SyntaxInfo
40 -> Idris ()
41elabRecord info what doc rsyn fc opts tyn nfc params paramDocs fields cname cdoc csyn
42 = do logElab 1 $ "Building data declaration for " ++ show tyn
43 -- Type constructor
44 let tycon = generateTyConType params
45 logElab 1 $ "Type constructor " ++ showTmImpls tycon
47 -- Data constructor
48 dconName <- generateDConName (fmap fst cname)
49 let dconTy = generateDConType params fieldsWithNameAndDoc
50 logElab 1 $ "Data constructor: " ++ showTmImpls dconTy
52 -- Build data declaration for elaboration
53 logElab 1 $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)
54 let datadecl = case what of
55 ETypes -> PLaterdecl tyn NoFC tycon
56 _ -> PDatadecl tyn NoFC tycon [(cdoc, dconsArgDocs, dconName, NoFC, dconTy, fc, [])]
57 elabData info rsyn doc paramDocs fc opts datadecl
59 -- Keep track of the record
60 let parameters = [(n,pt) | (n, _, _, pt) <- params]
61 let projections = [n | (n, _, _, _, _) <- fieldsWithName]
62 addRecord tyn (RI parameters dconName projections)
63 addIBC (IBCRecord tyn)
65 when (what /= ETypes) $ do
66 logElab 1 $ "fieldsWithName " ++ show fieldsWithName
67 logElab 1 $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
68 elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
70 sendHighlighting $ S.fromList $
71 [(FC' nfc, AnnName tyn Nothing Nothing Nothing)] ++
72 maybe [] (\(_, cnfc) -> [(FC' cnfc, AnnName dconName Nothing Nothing Nothing)]) cname ++
73 [(FC' ffc, AnnBoundName fn False) | (fn, ffc, _, _, _) <- fieldsWithName]
75 where
76 -- | Generates a type constructor.
77 generateTyConType :: [(Name, FC, Plicity, PTerm)] -> PTerm
78 generateTyConType ((n, nfc, p, t) : rest) = PPi p (nsroot n) nfc t (generateTyConType rest)
79 generateTyConType [] = (PType fc)
81 -- | Generates a name for the data constructor if none was specified.
82 generateDConName :: Maybe Name -> Idris Name
83 generateDConName (Just n) = return $ expandNS csyn n
84 generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
85 where
86 uniqueName :: Name -> Idris Name
87 uniqueName n = do i <- getIState
88 case lookupTyNameExact n (tt_ctxt i) of
89 Just _ -> uniqueName (nextName n)
90 Nothing -> return n
92 -- | Generates the data constructor type.
93 generateDConType :: [(Name, FC, Plicity, PTerm)] -> [(Name, FC, Plicity, PTerm, a)] -> PTerm
94 generateDConType ((n, nfc, _, t) : ps) as = PPi impl (nsroot n) NoFC t (generateDConType ps as)
95 generateDConType [] ((n, _, p, t, _) : as) = PPi p (nsroot n) NoFC t (generateDConType [] as)
96 generateDConType [] [] = target
98 -- | The target for the constructor and projection functions. Also the source of the update functions.
99 target :: PTerm
100 target = PApp fc (PRef fc [] tyn) $ map (uncurry asPRefArg) [(p, n) | (n, _, p, _) <- params]
102 paramsAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
103 paramsAndDoc = pad params paramDocs
104 where
105 pad :: [(Name, FC, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
106 pad ((n, fc, p, t) : rest) docs
107 = let d = case lookup n docs of
108 Just d' -> d
109 Nothing -> emptyDocstring
110 in (n, fc, p, t, d) : (pad rest docs)
111 pad _ _ = []
113 dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
114 dconsArgDocs = paramDocs ++ (dcad fieldsWithName)
115 where
116 dcad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]
117 dcad ((n, _, _, _, (Just d)) : rest) = ((nsroot n), d) : (dcad rest)
118 dcad (_ : rest) = dcad rest
119 dcad [] = []
121 fieldsWithName :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
122 fieldsWithName = fwn [] fields
123 where
124 fwn :: [Name] -> [(Maybe (Name, FC), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
125 fwn ns ((n, p, t, d) : rest)
126 = let nn = case n of
127 Just n' -> n'
128 Nothing -> newName ns baseName
129 withNS = expandNS rsyn (fst nn)
130 in (withNS, snd nn, p, t, d) : (fwn (fst nn : ns) rest)
131 fwn _ _ = []
133 baseName = (sUN "__pi_arg", NoFC)
135 newName :: [Name] -> (Name, FC) -> (Name, FC)
136 newName ns (n, nfc)
137 | n `elem` ns = newName ns (nextName n, nfc)
138 | otherwise = (n, nfc)
140 fieldsWithNameAndDoc :: [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
141 fieldsWithNameAndDoc = fwnad fieldsWithName
142 where
143 fwnad :: [(Name, FC, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))]
144 fwnad ((n, nfc, p, t, d) : rest)
145 = let doc = fromMaybe emptyDocstring d
146 in (n, nfc, p, t, doc) : (fwnad rest)
147 fwnad [] = []
149elabRecordFunctions :: ElabInfo
150 -> SyntaxInfo
151 -> FC
152 -> Name -- ^ Record type name
153 -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters
154 -> [(Name, FC, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields
155 -> Name -- ^ Constructor Name
156 -> PTerm -- ^ Target type
157 -> Idris ()
158elabRecordFunctions info rsyn fc tyn params fields dconName target
159 = do logElab 1 $ "Elaborating helper functions for record " ++ show tyn
161 logElab 3 $ "Fields: " ++ show fieldNames
162 logElab 3 $ "Params: " ++ show paramNames
163 -- The elaborated constructor type for the data declaration
164 i <- getIState
165 ttConsTy <-
166 case lookupTyExact dconName (tt_ctxt i) of
167 Just as -> return as
168 Nothing -> tclift $ tfail $ At fc (Elaborating "record " tyn Nothing (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))
170 -- The arguments to the constructor
171 let constructorArgs = getArgTys ttConsTy
172 logElab 3 $ "Cons args: " ++ show constructorArgs
173 logElab 3 $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)
174 -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
175 let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
177 -- The parameters for elaboration with their documentation
178 -- Parameter functions are all prefixed with "param_".
179 let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, _, t, d) <- params] -- zipParams i params paramDocs]
181 -- The fields (written by the user) with their documentation.
182 let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, nfc, p, t, d) <- fields]
184 -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
185 let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
186 -- Build and elaborate projection functions
187 elabProj dconName paramNames projectors
189 logElab 3 $ "Dependencies: " ++ show fieldDependencies
191 logElab 3 $ "Depended on: " ++ show dependedOn
193 -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.
194 let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
195 -- Build and elaborate update functions
196 elabUp dconName paramNames updaters
197 where
198 -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
199 placeholderArg :: Plicity -> Name -> PArg
200 placeholderArg p n = asArg p (nsroot n) Placeholder
202 -- | Root names of all fields in the current record declarations
203 fieldNames :: [Name]
204 fieldNames = [nsroot n | (n, _, _, _, _) <- fields]
206 paramNames :: [Name]
207 paramNames = [nsroot n | (n, _, _, _, _) <- params]
209 isFieldOrParam :: Name -> Bool
210 isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
212 isFieldOrParam' :: (Name, a) -> Bool
213 isFieldOrParam' = isFieldOrParam . fst
215 -- Delabs the TT to PTerm
216 -- This is not good.
217 -- However, for machine generated implicits, there seems to be no PTerm available.
218 -- Is there a better way to do this without building the setters and getters as TT?
219 freeField :: IState -> (Name, TT Name) -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
220 freeField i arg = let nameInCons = fst arg -- The name as it appears in the constructor
221 nameFree = expandNS rsyn (freeName $ fst arg) -- The name prefixed with "free_"
222 plicity = impl -- All free fields are implicit as they are machine generated
223 fieldType = delab i (snd arg) -- The type of the field
224 doc = emptyDocstring -- No docmentation for machine generated fields
225 in (nameInCons, nameFree, plicity, fieldType, doc)
227 freeName :: Name -> Name
228 freeName (UN n) = sUN ("free_" ++ str n)
229 freeName (MN i n) = sMN i ("free_" ++ str n)
230 freeName (NS n s) = NS (freeName n) s
231 freeName n = n
233 paramName :: Name -> Name
234 paramName (UN n) = sUN ("param_" ++ str n)
235 paramName (MN i n) = sMN i ("param_" ++ str n)
236 paramName (NS n s) = NS (paramName n) s
237 paramName n = n
239 -- | Elaborate the projection functions.
240 elabProj :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
241 elabProj cn paramnames fs
242 = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]
243 elab = \(n, n', p, t, doc, i) ->
244 -- Use projections in types
245 do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs
246 -- Parameters are already in scope, so just use them
247 , not (m `elem` paramNames)] t
248 elabProjection info n paramnames n' p t' doc rsyn fc target cn phArgs fieldNames i
249 in mapM_ elab fs
251 -- | Elaborate the update functions.
252 elabUp :: Name -> [Name] -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
253 elabUp cn paramnames fs
254 = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]
255 elab = \(n, n', p, t, doc, i) -> elabUpdate info n paramnames n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)
256 in mapM_ elab fs
258 -- | Decides whether a setter should be generated for a field or not.
259 optionalSetter :: Name -> Bool
260 optionalSetter n = n `elem` dependedOn
262 -- | A map from a field name to the other fields it depends on.
263 fieldDependencies :: [(Name, [Name])]
264 fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, _, t, _) <- fields ++ params]
265 where
266 fieldDep :: Name -> PTerm -> (Name, [Name])
267 fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
269 -- | A list of fields depended on by other fields.
270 dependedOn :: [Name]
271 dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))
273-- | Creates and elaborates a projection function.
274elabProjection :: ElabInfo
275 -> Name -- ^ Name of the argument in the constructor
276 -> [Name] -- ^ Parameter names
277 -> Name -- ^ Projection Name
278 -> Plicity -- ^ Projection Plicity
279 -> PTerm -- ^ Projection Type
280 -> (Docstring (Either Err PTerm)) -- ^ Projection Documentation
281 -> SyntaxInfo -- ^ Projection SyntaxInfo
282 -> FC -> PTerm -- ^ Projection target type
283 -> Name -- ^ Data constructor tame
284 -> [PArg] -- ^ Placeholder Arguments to constructor
285 -> [Name] -- ^ All Field Names
286 -> Int -- ^ Argument Index
287 -> Idris ()
288elabProjection info cname paramnames pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
289 = do logElab 1 $ "Generating Projection for " ++ show pname
291 let ty = generateTy
292 logElab 1 $ "Type of " ++ show pname ++ ": " ++ show ty
294 let lhs = generateLhs
295 logElab 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs
296 let rhs = generateRhs
297 logElab 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs
299 rec_elabDecl info EAll info ty
301 let clause = PClause fc pname lhs [] rhs []
302 rec_elabDecl info EAll info $ PClauses fc [] pname [clause]
303 where
304 -- | The type of the projection function.
305 generateTy :: PDecl
306 generateTy = PTy pdoc [] psyn fc [] pname NoFC $
307 bindParams paramnames $
308 PPi expl recName NoFC targetTy projTy
310 bindParams [] t = t
311 bindParams (n : ns) ty = PPi impl n NoFC Placeholder (bindParams ns ty)
313 -- | The left hand side of the projection function.
314 generateLhs :: PTerm
315 generateLhs = let args = lhsArgs index phArgs
316 in PApp fc (PRef fc [] pname) [pexp (PApp fc (PRef fc [] cn) args)]
317 where
318 lhsArgs :: Int -> [PArg] -> [PArg]
319 lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc [] pname_in)) : rest
320 lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)
321 lhsArgs _ [] = []
323 -- | The "_in" name. Used for the lhs.
324 pname_in :: Name
325 pname_in = rootname -- in_name rootname
327 rootname :: Name
328 rootname = nsroot cname
330 -- | The right hand side of the projection function.
331 generateRhs :: PTerm
332 generateRhs = PRef fc [] pname_in
334-- | Creates and elaborates an update function.
335-- If 'optional' is true, we will not fail if we can't elaborate the update function.
336elabUpdate :: ElabInfo
337 -> Name -- ^ Name of the argument in the constructor
338 -> [Name] -- ^ Parameter names
339 -> Name -- ^ Field Name
340 -> Plicity -- ^ Field Plicity
341 -> PTerm -- ^ Field Type
342 -> (Docstring (Either Err PTerm)) -- ^ Field Documentation
343 -> SyntaxInfo -- ^ Field SyntaxInfo
344 -> FC -> PTerm -- ^ Projection Source Type
345 -> Name -- ^ Data Constructor Name
346 -> [PArg] -- ^ Arguments to constructor
347 -> [Name] -- ^ All fields
348 -> Int -- ^ Argument Index
349 -> Bool -- ^ Optional
350 -> Idris ()
351elabUpdate info cname paramnames pname plicity pty pdoc psyn fc sty cn args fnames i optional
352 = do logElab 1 $ "Generating Update for " ++ show pname
354 let ty = generateTy
355 logElab 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty
357 let lhs = generateLhs
358 logElab 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs
360 let rhs = generateRhs
361 logElab 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs
363 let clause = PClause fc set_pname lhs [] rhs []
365 idrisCatch (do rec_elabDecl info EAll info ty
366 rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])
367 (\err -> logElab 1 $ "Could not generate update function for " ++ show pname)
368 {-if optional
369 then logElab 1 $ "Could not generate update function for " ++ show pname
370 else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}
371 where
372 -- | The type of the update function.
373 generateTy :: PDecl
374 generateTy = PTy pdoc [] psyn fc [] set_pname NoFC $
375 bindParams paramnames $
376 PPi expl (nsroot pname) NoFC pty $
377 PPi expl recName NoFC sty (substInput sty)
378 where substInput = substMatches [(cname, PRef fc [] (nsroot pname))]
380 bindParams [] t = t
381 bindParams (n : ns) ty = PPi impl n NoFC Placeholder (bindParams ns ty)
383 -- | The "_set" name.
384 set_pname :: Name
385 set_pname = set_name pname
387 set_name :: Name -> Name
388 set_name (UN n) = sUN ("set_" ++ str n)
389 set_name (MN i n) = sMN i ("set_" ++ str n)
390 set_name (NS n s) = NS (set_name n) s
391 set_name n = n
393 -- | The left-hand side of the update function.
394 generateLhs :: PTerm
395 generateLhs = PApp fc (PRef fc [] set_pname) [pexp $ PRef fc [] pname_in, pexp constructorPattern]
396 where
397 constructorPattern :: PTerm
398 constructorPattern = PApp fc (PRef fc [] cn) args
400 -- | The "_in" name.
401 pname_in :: Name
402 pname_in = in_name rootname
404 rootname :: Name
405 rootname = nsroot pname
407 -- | The right-hand side of the update function.
408 generateRhs :: PTerm
409 generateRhs = PApp fc (PRef fc [] cn) (newArgs i args)
410 where
411 newArgs :: Int -> [PArg] -> [PArg]
412 newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc [] pname_in)) : rest
413 newArgs i (x : rest) = x : (newArgs (i-1) rest)
414 newArgs _ [] = []
416-- | Post-fixes a name with "_in".
417in_name :: Name -> Name
418in_name (UN n) = sMN 0 (str n ++ "_in")
419in_name (MN i n) = sMN i (str n ++ "_in")
420in_name (NS n s) = NS (in_name n) s
421in_name n = n
423-- | Creates a PArg with a given plicity, name, and term.
424asArg :: Plicity -> Name -> PTerm -> PArg
425asArg (Imp os _ _ _ _ _) n t = PImp 0 False os n t
426asArg (Exp os _ _ _) n t = PExp 0 os n t
427asArg (Constraint os _ _) n t = PConstraint 0 os n t
428asArg (TacImp os _ s _) n t = PTacImplicit 0 os n s t
430-- | Machine name "rec".
431recName :: Name
432recName = sMN 0 "rec"
434recRef = PRef emptyFC [] recName
436projectInType :: [(Name, Name)] -> PTerm -> PTerm
437projectInType xs = mapPT st
438 where
439 st :: PTerm -> PTerm
440 st (PRef fc hls n)
441 | Just pn <- lookup n xs = PApp fc (PRef fc hls pn) [pexp recRef]
442 st t = t
444-- | Creates an PArg from a plicity and a name where the term is a PRef.
445asPRefArg :: Plicity -> Name -> PArg
446asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC [] (nsroot n)