@@ -1,9 +1,8 @@
1−{-# LANGUAGE PatternGuards #-}
1+{-# LANGUAGE PatternGuards, ViewPatterns #-}
22module Idris.Elab.Record(elabRecord) where
33
44import Idris.AbsSyntax
5−import Idris.ASTUtils
6−import Idris.DSL
5+import Idris.Docstrings
76import Idris.Error
87import Idris.Delaborate
98import Idris.Imports
@@ -18,225 +17,429 @@ import Idris.DeepSeq
1817import Idris.Output (iputStrLn, pshow, iWarn)
1918import IRTS.Lang
2019
20+import Idris.ParseExpr (tryFullExpr)
21+
2122import Idris.Elab.Type
2223import Idris.Elab.Data
2324import Idris.Elab.Utils
2425
2526import Idris.Core.TT
26−import Idris.Core.Elaborate hiding (Tactic(..))
2727import Idris.Core.Evaluate
28−import Idris.Core.Execute
29−import Idris.Core.Typecheck
30−import Idris.Core.CaseTree
31−
32−import Idris.Docstrings
3328
34−import Prelude hiding (id, (.))
35−import Control.Category
29+import Idris.Elab.Data
3630
37−import Control.Applicative hiding (Const)
38−import Control.DeepSeq
39−import Control.Monad
40−import Control.Monad.State.Strict as State
41−import Data.List
4231import Data.Maybe
43−import Debug.Trace
44−
45−import qualified Data.Map as Map
46−import qualified Data.Set as S
47−import qualified Data.Text as T
48−import Data.Char(isLetter, toLower)
49−import Data.List.Split (splitOn)
50−
51−import Util.Pretty(pretty, text)
52−
53−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> Name ->
54− PTerm -> DataOpts -> Docstring (Either Err PTerm) -> Name -> PTerm -> Idris ()
55−elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
56− = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
57− -- TODO think: something more in info?
58− cty' <- implicit info syn cn cty_in
59− i <- getIState
60−
61− -- get bound implicits and propagate to setters (in case they
62− -- provide useful information for inference)
63− let extraImpls = getBoundImpls cty'
64−
65− cty <- case lookupTy cn (tt_ctxt i) of
66− [t] -> return (delab i t)
67− _ -> ifail "Something went inexplicably wrong"
68− cimp <- case lookupCtxt cn (idris_implicits i) of
69− [imps] -> return imps
70− ppos <- case lookupCtxt tyn (idris_datatypes i) of
71− [ti] -> return $ param_pos ti
72− let cty_imp = renameBs cimp cty
73− let ptys = getProjs [] cty_imp
74− let ptys_u = getProjs [] cty
75− let recty = getRecTy cty_imp
76− let recty_u = getRecTy cty
77−
78− let paramNames = getPNames recty ppos
79−
80− -- rename indices when we generate the getter/setter types, so
81− -- that they don't clash with the names of the projections
82− -- we're generating
83− let index_names_in = getRecNameMap "_in" ppos recty
84− let recty_in = substMatches index_names_in recty
85−
86− logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)
87− -- Substitute indices with projection functions, and parameters with
88− -- the updated parameter name
89− let substs = map (\ (n, _) ->
90− if n `elem` paramNames
91− then (n, PRef fc (mkp n))
92− else (n, PApp fc (PRef fc n)
93− [pexp (PRef fc rec)]))
94− ptys
95−
96− -- Generate projection functions
97− proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
98− logLvl 3 $ show proj_decls
99− let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
100− let implBinds = getImplB id cty'
101−
102− -- Generate update functions
103− update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls
104− (getFieldNames cty')
105− implBinds (length nonImp)) (zip nonImp [0..])
106− mapM_ (rec_elabDecl info EAll info) (concat proj_decls)
107− logLvl 3 $ show update_decls
108− mapM_ (tryElabDecl info) (update_decls)
109− where
110−-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
32+import Data.List
33+import Control.Monad
11134
112− isNonImp (PExp _ _ _ _, a) = Just a
113− isNonImp _ = Nothing
35+-- | Elaborate a record declaration
36+elabRecord :: ElabInfo
37+ -> (Docstring (Either Err PTerm)) -- ^ The documentation for the whole declaration
38+ -> SyntaxInfo -> FC -> DataOpts
39+ -> Name -- ^ The name of the type being defined
40+ -> [(Name, Plicity, PTerm)] -- ^ Parameters
41+ -> [(Name, Docstring (Either Err PTerm))] -- ^ Parameter Docs
42+ -> [((Maybe Name), Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -- ^ Fields
43+ -> Maybe Name -- ^ Constructor Name
44+ -> (Docstring (Either Err PTerm)) -- ^ Constructor Doc
45+ -> SyntaxInfo -- ^ Constructor SyntaxInfo
46+ -> Idris ()
47+elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
48+ = do logLvl 1 $ "Building data declaration for " ++ show tyn
49+ -- Type constructor
50+ let tycon = generateTyConType params
51+ logLvl 1 $ "Type constructor " ++ showTmImpls tycon
52+
53+ -- Data constructor
54+ dconName <- generateDConName cname
55+ let dconTy = generateDConType params fieldsWithNameAndDoc
56+ logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy
57+
58+ -- Build data declaration for elaboration
59+ iLOG $ foldr (++) "" $ intersperse "\n" (map show dconsArgDocs)
60+ let datadecl = PDatadecl tyn tycon [(cdoc, dconsArgDocs, dconName, dconTy, fc, [])]
61+ elabData info rsyn doc paramDocs fc opts datadecl
62+
63+ iLOG $ "fieldsWithName " ++ show fieldsWithName
64+ iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
65+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
66+ where
67+ -- | Generates a type constructor.
68+ generateTyConType :: [(Name, Plicity, PTerm)] -> PTerm
69+ generateTyConType ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyConType rest)
70+ generateTyConType [] = PType
71+
72+ -- | Generates a name for the data constructor if none was specified.
73+ generateDConName :: Maybe Name -> Idris Name
74+ generateDConName (Just n) = return $ expandNS csyn n
75+ generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
76+ where
77+ uniqueName :: Name -> Idris Name
78+ uniqueName n = do i <- getIState
79+ case lookupTyNameExact n (tt_ctxt i) of
80+ Just _ -> uniqueName (nextName n)
81+ Nothing -> return n
82+
83+ -- | Generates the data constructor type.
84+ generateDConType :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm, a)] -> PTerm
85+ generateDConType ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDConType ps as)
86+ generateDConType [] ((n, p, t, _) : as) = PPi p (nsroot n) t (generateDConType [] as)
87+ generateDConType [] [] = target
88+
89+ -- | The target for the constructor and projection functions. Also the source of the update functions.
90+ target :: PTerm
91+ target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, _) <- params]
92+
93+ paramsAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
94+ paramsAndDoc = pad params paramDocs
95+ where
96+ pad :: [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
97+ pad ((n, p, t) : rest) docs
98+ = let d = case lookup n docs of
99+ Just d' -> d
100+ Nothing -> emptyDocstring
101+ in (n, p, t, d) : (pad rest docs)
102+ pad _ _ = []
103+
104+ dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
105+ dconsArgDocs = paramDocs ++ (dcad fieldsWithName)
106+ where
107+ dcad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Docstring (Either Err PTerm))]
108+ dcad ((n, _, _, (Just d)) : rest) = ((nsroot n), d) : (dcad rest)
109+ dcad (_ : rest) = dcad rest
110+ dcad [] = []
114111
115− getPNames (PApp _ _ as) ppos = getpn as ppos
112+ fieldsWithName :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
113+ fieldsWithName = fwn [] fields
114+ where
115+ fwn :: [Name] -> [(Maybe Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
116+ fwn ns ((n, p, t, d) : rest)
117+ = let nn = case n of
118+ Just n' -> n'
119+ Nothing -> newName ns baseName
120+ in (expandNS rsyn $ nn, p, t, d) : (fwn (nn : ns) rest)
121+ fwn _ _ = []
122+
123+ baseName = sUN "__pi_arg"
124+
125+ newName :: [Name] -> Name -> Name
126+ newName ns n
127+ | n `elem` ns = newName ns (nextName n)
128+ | otherwise = n
129+
130+ fieldsWithNameAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
131+ fieldsWithNameAndDoc = fwnad fieldsWithName
132+ where
133+ fwnad :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))] -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
134+ fwnad ((n, p, t, d) : rest)
135+ = let doc = fromMaybe emptyDocstring d
136+ in (n, p, t, doc) : (fwnad rest)
137+ fwnad [] = []
138+
139+elabRecordFunctions :: ElabInfo -> SyntaxInfo -> FC
140+ -> Name -- ^ Record type name
141+ -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Parameters
142+ -> [(Name, Plicity, PTerm, Docstring (Either Err PTerm))] -- ^ Fields
143+ -> Name -- ^ Constructor Name
144+ -> PTerm -- ^ Target type
145+ -> Idris ()
146+elabRecordFunctions info rsyn fc tyn params fields dconName target
147+ = do logLvl 1 $ "Elaborating helper functions for record " ++ show tyn
148+
149+ iLOG $ "Fields: " ++ show fieldNames
150+ iLOG $ "Params: " ++ show paramNames
151+ -- The elaborated constructor type for the data declaration
152+ i <- getIState
153+ ttConsTy <-
154+ case lookupTyExact dconName (tt_ctxt i) of
155+ Just as -> return as
156+ Nothing -> tclift $ tfail $ At fc (Elaborating "record " tyn (InternalMsg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))
157+
158+ -- The arguments to the constructor
159+ let constructorArgs = getArgTys ttConsTy
160+ iLOG $ "Cons args: " ++ show constructorArgs
161+ iLOG $ "Free fields: " ++ show (filter (not . isFieldOrParam') constructorArgs)
162+ -- If elaborating the constructor has resulted in some new implicit fields we make projection functions for them.
163+ let freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
164+
165+ -- The parameters for elaboration with their documentation
166+ -- Parameter functions are all prefixed with "param_".
167+ let paramsForElab = [((nsroot n), (paramName n), impl, t, d) | (n, _, t, d) <- params] -- zipParams i params paramDocs]
168+
169+ -- The fields (written by the user) with their documentation.
170+ let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, p, t, d) <- fields]
171+
172+ -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
173+ let projectors = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
174+ -- Build and elaborate projection functions
175+ elabProj dconName projectors
176+
177+ logLvl 1 $ "Dependencies: " ++ show fieldDependencies
178+
179+ logLvl 1 $ "Depended on: " ++ show dependedOn
180+
181+ -- All things we need to elaborate update functions for, together with a number denoting their position in the constructor.
182+ let updaters = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
183+ -- Build and elaborate update functions
184+ elabUp dconName updaters
185+ where
186+ -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
187+ placeholderArg :: Plicity -> Name -> PArg
188+ placeholderArg p n = asArg p (nsroot n) Placeholder
189+
190+ -- | Root names of all fields in the current record declarations
191+ fieldNames :: [Name]
192+ fieldNames = [nsroot n | (n, _, _, _) <- fields]
193+
194+ paramNames :: [Name]
195+ paramNames = [nsroot n | (n, _, _, _) <- params]
196+
197+ isFieldOrParam :: Name -> Bool
198+ isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
199+
200+ isFieldOrParam' :: (Name, a) -> Bool
201+ isFieldOrParam' = isFieldOrParam . fst
202+
203+ isField :: Name -> Bool
204+ isField = flip elem fieldNames
205+
206+ isField' :: (Name, a, b, c, d, f) -> Bool
207+ isField' (n, _, _, _, _, _) = isField n
208+
209+ fieldTerms :: [PTerm]
210+ fieldTerms = [t | (_, _, t, _) <- fields]
211+
212+ -- Delabs the TT to PTerm
213+ -- This is not good.
214+ -- However, for machine generated implicits, there seems to be no PTerm available.
215+ -- Is there a better way to do this without building the setters and getters as TT?
216+ freeField :: IState -> (Name, TT Name) -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
217+ freeField i arg = let nameInCons = fst arg -- The name as it appears in the constructor
218+ nameFree = expandNS rsyn (freeName $ fst arg) -- The name prefixed with "free_"
219+ plicity = impl -- All free fields are implicit as they are machine generated
220+ fieldType = delab i (snd arg) -- The type of the field
221+ doc = emptyDocstring -- No docmentation for machine generated fields
222+ in (nameInCons, nameFree, plicity, fieldType, doc)
223+
224+ freeName :: Name -> Name
225+ freeName (UN n) = sUN ("free_" ++ str n)
226+ freeName (MN i n) = sMN i ("free_" ++ str n)
227+ freeName (NS n s) = NS (freeName n) s
228+ freeName n = n
229+
230+ -- | Zips together parameters with their documentation. If no documentation for a given field exists, an empty docstring is used.
231+ zipParams :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]
232+ zipParams i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zipParams i rest rest')
233+ zipParams i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zipParams i rest [])
234+ where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring
235+ zipParams _ [] [] = []
236+
237+ paramName :: Name -> Name
238+ paramName (UN n) = sUN ("param_" ++ str n)
239+ paramName (MN i n) = sMN i ("param_" ++ str n)
240+ paramName (NS n s) = NS (paramName n) s
241+ paramName n = n
242+
243+ -- | Elaborate the projection functions.
244+ elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
245+ elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]
246+ elab = \(n, n', p, t, doc, i) ->
247+ -- Use projections in types
248+ do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs
249+ -- Parameters are already in scope, so just use them
250+ , not (m `elem` paramNames)] t
251+ elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i
252+ in mapM_ elab fs
253+
254+ -- | Elaborate the update functions.
255+ elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
256+ elabUp cn fs = let args = map (uncurry asPRefArg) [(p, n) | (n, _, p, _, _, _) <- fs]
257+ elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)
258+ in mapM_ elab fs
259+
260+ -- | Decides whether a setter should be generated for a field or not.
261+ optionalSetter :: Name -> Bool
262+ optionalSetter n = n `elem` dependedOn
263+
264+ -- | A map from a field name to the other fields it depends on.
265+ fieldDependencies :: [(Name, [Name])]
266+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t, _) <- fields ++ params]
267+ where
268+ fieldDep :: Name -> PTerm -> (Name, [Name])
269+ fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
270+
271+ -- | A list of fields depending on another field.
272+ dependentFields :: [Name]
273+ dependentFields = filter depends fieldNames
274+ where
275+ depends :: Name -> Bool
276+ depends n = case lookup n fieldDependencies of
277+ Just xs -> not $ null xs
278+ Nothing -> False
279+
280+ -- | A list of fields depended on by other fields.
281+ dependedOn :: [Name]
282+ dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))
283+
284+-- | Creates and elaborates a projection function.
285+elabProjection :: ElabInfo
286+ -> Name -- ^ Name of the argument in the constructor
287+ -> Name -- ^ Projection Name
288+ -> Plicity -- ^ Projection Plicity
289+ -> PTerm -- ^ Projection Type
290+ -> (Docstring (Either Err PTerm)) -- ^ Projection Documentation
291+ -> SyntaxInfo -- ^ Projection SyntaxInfo
292+ -> FC -> PTerm -- ^ Projection target type
293+ -> Name -- ^ Data constructor tame
294+ -> [PArg] -- ^ Placeholder Arguments to constructor
295+ -> [Name] -- ^ All Field Names
296+ -> Int -- ^ Argument Index
297+ -> Idris ()
298+elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
299+ = do logLvl 1 $ "Generating Projection for " ++ show pname
300+
301+ let ty = generateTy
302+ logLvl 1 $ "Type of " ++ show pname ++ ": " ++ show ty
303+
304+ let lhs = generateLhs
305+ logLvl 1 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs
306+ let rhs = generateRhs
307+ logLvl 1 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs
308+
309+ rec_elabDecl info EAll info ty
310+
311+ let clause = PClause fc pname lhs [] rhs []
312+ rec_elabDecl info EAll info $ PClauses fc [] pname [clause]
313+ where
314+ -- | The type of the projection function.
315+ generateTy :: PDecl
316+ generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName targetTy projTy
317+
318+ -- | The left hand side of the projection function.
319+ generateLhs :: PTerm
320+ generateLhs = let args = lhsArgs index phArgs
321+ in PApp fc (PRef fc pname) [pexp (PApp fc (PRef fc cn) args)]
116322 where
117− getpn as [] = []
118− getpn as (i:is) | length as > i,
119− PRef _ n <- getTm (as!!i) = n : getpn as is
120− | otherwise = getpn as is
121− getPNames _ _ = []
122−
123− tryElabDecl info (fn, ty, val)
124− = do i <- getIState
125− idrisCatch (do rec_elabDecl info EAll info ty
126− rec_elabDecl info EAll info val)
127− (\v -> do iputStrLn $ show fc ++
128− ":Warning - can't generate setter for " ++
129− show fn ++ " (" ++ show ty ++ ")"
130−-- ++ "\n" ++ pshow i v
131− putIState i)
132−
133− getBoundImpls (PPi (Imp _ _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
134− getBoundImpls _ = []
135−
136− getImplB k (PPi (Imp l s _ _) n Placeholder sc)
137− = getImplB k sc
138− getImplB k (PPi (Imp l s p fa) n ty sc)
139− = getImplB (\x -> k (PPi (Imp l s p fa) n ty x)) sc
140− getImplB k (PPi _ n ty sc)
141− = getImplB k sc
142− getImplB k _ = k
143−
144− renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
145− = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
146− renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
147− renameBs _ t = t
148−
149− getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
150− getProjs acc r = reverse acc
151−
152− getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
153− getFieldNames (PPi _ _ _ s) = getFieldNames s
154− getFieldNames _ = []
155−
156− getRecTy (PPi _ n ty s) = getRecTy s
157− getRecTy t = t
158−
159− -- make sure we pick a consistent name for parameters; any name will do
160− -- otherwise
161− getRecNameMap x ppos (PApp fc t args)
162− = mapMaybe toMN (zip [0..] (map getTm args))
323+ lhsArgs :: Int -> [PArg] -> [PArg]
324+ lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
325+ lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)
326+ lhsArgs _ [] = []
327+
328+ -- | The "_in" name. Used for the lhs.
329+ pname_in :: Name
330+ pname_in = rootname -- in_name rootname
331+
332+ rootname :: Name
333+ rootname = nsroot cname
334+
335+ -- | The right hand side of the projection function.
336+ generateRhs :: PTerm
337+ generateRhs = PRef fc pname_in
338+
339+-- | Creates and elaborates an update function.
340+-- If 'optional' is true, we will not fail if we can't elaborate the update function.
341+elabUpdate :: ElabInfo
342+ -> Name -- ^ Name of the argument in the constructor
343+ -> Name -- ^ Field Name
344+ -> Plicity -- ^ Field Plicity
345+ -> PTerm -- ^ Field Type
346+ -> (Docstring (Either Err PTerm)) -- ^ Field Documentation
347+ -> SyntaxInfo -- ^ Field SyntaxInfo
348+ -> FC -> PTerm -- ^ Projection Source Type
349+ -> Name -- ^ Data Constructor Name
350+ -> [PArg] -- ^ Arguments to constructor
351+ -> [Name] -- ^ All fields
352+ -> Int -- ^ Argument Index
353+ -> Bool -- ^ Optional
354+ -> Idris ()
355+elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional
356+ = do logLvl 1 $ "Generating Update for " ++ show pname
357+
358+ let ty = generateTy
359+ logLvl 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty
360+
361+ let lhs = generateLhs
362+ logLvl 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs
363+
364+ let rhs = generateRhs
365+ logLvl 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs
366+
367+ let clause = PClause fc set_pname lhs [] rhs []
368+
369+ idrisCatch (do rec_elabDecl info EAll info ty
370+ rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])
371+ (\err -> logLvl 1 $ "Could not generate update function for " ++ show pname)
372+ {-if optional
373+ then logLvl 1 $ "Could not generate update function for " ++ show pname
374+ else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}
375+ where
376+ -- | The type of the udpate function.
377+ generateTy :: PDecl
378+ generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) pty (PPi expl recName sty (substInput sty))
379+ where substInput = substMatches [(cname, PRef fc (nsroot pname))]
380+
381+ -- | The "_set" name.
382+ set_pname :: Name
383+ set_pname = set_name pname
384+
385+ set_name :: Name -> Name
386+ set_name (UN n) = sUN ("set_" ++ str n)
387+ set_name (MN i n) = sMN i ("set_" ++ str n)
388+ set_name (NS n s) = NS (set_name n) s
389+ set_name n = n
390+
391+ -- | The left-hand side of the update function.
392+ generateLhs :: PTerm
393+ generateLhs = PApp fc (PRef fc set_pname) [pexp $ PRef fc pname_in, pexp constructorPattern]
394+ where
395+ constructorPattern :: PTerm
396+ constructorPattern = PApp fc (PRef fc cn) args
397+
398+ -- | The "_in" name.
399+ pname_in :: Name
400+ pname_in = in_name rootname
401+
402+ rootname :: Name
403+ rootname = nsroot pname
404+
405+ -- | The right-hand side of the update function.
406+ generateRhs :: PTerm
407+ generateRhs = PApp fc (PRef fc cn) (newArgs i args)
163408 where
164− toMN (i, PRef fc n)
165− | i `elem` ppos = Just (n, PRef fc (mkp n))
166− | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))
167− toMN _ = Nothing
168− getRecNameMap x _ _ = []
169−
170− rec = sMN 0 "rec"
171−
172− -- only UNs propagate properly as parameters (bit of a hack then...)
173− mkp (UN n) = sUN ("_p_" ++ str n)
174− mkp (MN i n) = sMN i ("p_" ++ str n)
175− mkp (NS n s) = NS (mkp n) s
176−
177− mkImp (UN n) = sUN ("implicit_" ++ str n)
178− mkImp (MN i n) = sMN i ("implicit_" ++ str n)
179− mkImp (NS n s) = NS (mkImp n) s
180−
181− mkType (UN n) = sUN ("set_" ++ str n)
182− mkType (MN i n) = sMN i ("set_" ++ str n)
183− mkType (NS n s) = NS (mkType n) s
184−
185− mkProj recty substs cimp ((pn_in, pty), pos)
186− = do let pn = expandNS syn pn_in -- projection name
187− -- use pn_in in the indices, consistently, to avoid clash
188− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
189− (PPi expl rec recty
190− (substMatches substs pty))
191− let pls = repeat Placeholder
192− let before = pos
193− let after = length substs - (pos + 1)
194− let args = take before pls ++ PRef fc (mkp pn_in) : take after pls
195− let iargs = map implicitise (zip cimp args)
196− let lhs = PApp fc (PRef fc pn)
197− [pexp (PApp fc (PRef fc cn) iargs)]
198− let rhs = PRef fc (mkp pn_in)
199− let pclause = PClause fc pn lhs [] rhs []
200− return [pfnTy, PClauses fc [] pn [pclause]]
201−
202− implicitise (pa, t) = pa { getTm = t }
203−
204− -- If the 'pty' we're updating includes anything in 'substs', we're
205− -- updating the type as well, so use recty', otherwise just use
206− -- recty
207− mkUpdate recty inames extras fnames k num ((pn, pty), pos)
208− = do let setname = expandNS syn $ mkType pn
209− let valname = sMN 0 "updateval"
210− let pn_out = sMN 0 (show pn ++ "_out")
211− let pn_in = sMN 0 (show pn ++ "_in")
212− let recty_in = substMatches [(pn, PRef fc pn_in)] recty
213− let recty_out = substMatches [(pn, PRef fc pn_out)] recty
214− let pt = substMatches inames $
215− k (implBindUp extras inames (PPi expl pn_out pty
216− (PPi expl rec recty_in recty_out)))
217− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
218−-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
219− let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
220− let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames
221− let lhsArgs = pls
222− let rhsArgs = take pos pls ++ (PRef fc valname) :
223− drop (pos + 1) pls
224− let before = pos
225− let pclause = PClause fc setname (PApp fc (PRef fc setname)
226− [pexp (PRef fc valname),
227− pexp (PApp fc (PRef fc cn)
228− (map pexp lhsArgs))])
229− []
230− (PApp fc (PRef fc cn)
231− (map pexp rhsArgs)) []
232− return (pn, pfnTy, PClauses fc [] setname [pclause])
233−
234− implBindUp [] is t = t
235− implBindUp ((n, ty):ns) is t
236− = let n' = case lookup n is of
237− Just (PRef _ x) -> x
238− _ -> n in
239− if n `elem` allNamesIn t
240− then PPi impl n' ty (implBindUp ns is t)
241− else implBindUp ns is t
409+ newArgs :: Int -> [PArg] -> [PArg]
410+ newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
411+ newArgs i (x : rest) = x : (newArgs (i-1) rest)
412+ newArgs _ [] = []
413+
414+-- | Post-fixes a name with "_in".
415+in_name :: Name -> Name
416+in_name (UN n) = sMN 0 (str n ++ "_in")
417+in_name (MN i n) = sMN i (str n ++ "_in")
418+in_name (NS n s) = NS (in_name n) s
419+in_name n = n
420+
421+-- | Creates a PArg with a given plicity, name, and term.
422+asArg :: Plicity -> Name -> PTerm -> PArg
423+asArg (Imp os _ _ _) n t = PImp 0 False os n t
424+asArg (Exp os _ _) n t = PExp 0 os n t
425+asArg (Constraint os _) n t = PConstraint 0 os n t
426+asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t
427+
428+-- | Machine name "rec".
429+recName :: Name
430+recName = sMN 0 "rec"
431+
432+recRef = PRef emptyFC recName
433+
434+projectInType :: [(Name, Name)] -> PTerm -> PTerm
435+projectInType xs = mapPT st
436+ where
437+ st :: PTerm -> PTerm
438+ st (PRef fc n)
439+ | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
440+ st t = t
441+
442+-- | Creates an PArg from a plicity and a name where the term is a PRef.
443+asPRefArg :: Plicity -> Name -> PArg
444+asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC (nsroot n)
242445