@@ -1,9 +1,8 @@
1−{-# LANGUAGE PatternGuards #-}
1+{-# LANGUAGE PatternGuards, ViewPatterns #-}
2module Idris.Elab.Record(elabRecord) where
2module Idris.Elab.Record(elabRecord) where
4import Idris.AbsSyntax
4import Idris.AbsSyntax
5−import Idris.ASTUtils
5+import Idris.Docstrings
7import Idris.Error
6import Idris.Error
8import Idris.Delaborate
7import Idris.Delaborate
9import Idris.Imports
8import Idris.Imports
@@ -18,225 +17,429 @@ import Idris.DeepSeq
18import Idris.Output (iputStrLn, pshow, iWarn)
17import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
18import IRTS.Lang
20+import Idris.ParseExpr (tryFullExpr)
21import Idris.Elab.Type
22import Idris.Elab.Type
22import Idris.Elab.Data
23import Idris.Elab.Data
23import Idris.Elab.Utils
24import Idris.Elab.Utils
25import Idris.Core.TT
26import Idris.Core.TT
26−import Idris.Core.Elaborate hiding (Tactic(..))
27import Idris.Core.Evaluate
27import Idris.Core.Evaluate
28−import Idris.Core.Execute
29−import Idris.Core.Typecheck
30−import Idris.Core.CaseTree
32−import Idris.Docstrings
34−import Prelude hiding (id, (.))
29+import Idris.Elab.Data
35−import Control.Category
37−import Control.Applicative hiding (Const)
38−import Control.DeepSeq
40−import Control.Monad.State.Strict as State
42import Data.Maybe
31import Data.Maybe
43−import Debug.Trace
32+import Data.List
44−
33+import Control.Monad
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)
51−import Util.Pretty(pretty, text)
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
61− -- get bound implicits and propagate to setters (in case they
62− -- provide useful information for inference)
63− let extraImpls = getBoundImpls cty'
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
78− let paramNames = getPNames recty ppos
80− -- rename indices when we generate the getter/setter types, so
81− -- that they don't clash with the names of the projections
83− let index_names_in = getRecNameMap "_in" ppos recty
84− let recty_in = substMatches index_names_in recty
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)]))
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'
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)
110−-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
112− isNonImp (PExp _ _ _ _, a) = Just a
35+-- | Elaborate a record declaration
113− isNonImp _ = Nothing
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
47+elabRecord info doc rsyn fc opts tyn params paramDocs fields cname cdoc csyn
48+ = do logLvl 1 $ "Building data declaration for " ++ show tyn
50+ let tycon = generateTyConType params
51+ logLvl 1 $ "Type constructor " ++ showTmImpls tycon
54+ dconName <- generateDConName cname
55+ let dconTy = generateDConType params fieldsWithNameAndDoc
56+ logLvl 1 $ "Data constructor: " ++ showTmImpls dconTy
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
63+ iLOG $ "fieldsWithName " ++ show fieldsWithName
64+ iLOG $ "fieldsWIthNameAndDoc " ++ show fieldsWithNameAndDoc
65+ elabRecordFunctions info rsyn fc tyn paramsAndDoc fieldsWithNameAndDoc dconName target
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
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))))
77+ uniqueName :: Name -> Idris Name
78+ uniqueName n = do i <- getIState
79+ case lookupTyNameExact n (tt_ctxt i) of
80+ Just _ -> uniqueName (nextName n)
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
89+ -- | The target for the constructor and projection functions. Also the source of the update functions.
91+ target = PApp fc (PRef fc tyn) $ map (uncurry asPRefArg) [(p, n) | (n, p, _) <- params]
93+ paramsAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
94+ paramsAndDoc = pad params paramDocs
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
100+ Nothing -> emptyDocstring
101+ in (n, p, t, d) : (pad rest docs)
104+ dconsArgDocs :: [(Name, Docstring (Either Err PTerm))]
105+ dconsArgDocs = paramDocs ++ (dcad fieldsWithName)
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
115− getPNames (PApp _ _ as) ppos = getpn as ppos
112+ fieldsWithName :: [(Name, Plicity, PTerm, Maybe (Docstring (Either Err PTerm)))]
113+ fieldsWithName = fwn [] fields
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
119+ Nothing -> newName ns baseName
120+ in (expandNS rsyn $ nn, p, t, d) : (fwn (nn : ns) rest)
123+ baseName = sUN "__pi_arg"
125+ newName :: [Name] -> Name -> Name
127+ | n `elem` ns = newName ns (nextName n)
130+ fieldsWithNameAndDoc :: [(Name, Plicity, PTerm, Docstring (Either Err PTerm))]
131+ fieldsWithNameAndDoc = fwnad fieldsWithName
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)
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
146+elabRecordFunctions info rsyn fc tyn params fields dconName target
147+ = do logLvl 1 $ "Elaborating helper functions for record " ++ show tyn
149+ iLOG $ "Fields: " ++ show fieldNames
150+ iLOG $ "Params: " ++ show paramNames
151+ -- The elaborated constructor type for the data declaration
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."))
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)
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]
169+ -- The fields (written by the user) with their documentation.
170+ let userFieldsForElab = [((nsroot n), n, p, t, d) | (n, p, t, d) <- fields]
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
177+ logLvl 1 $ "Dependencies: " ++ show fieldDependencies
179+ logLvl 1 $ "Depended on: " ++ show dependedOn
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
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
190+ -- | Root names of all fields in the current record declarations
191+ fieldNames :: [Name]
192+ fieldNames = [nsroot n | (n, _, _, _) <- fields]
194+ paramNames :: [Name]
195+ paramNames = [nsroot n | (n, _, _, _) <- params]
197+ isFieldOrParam :: Name -> Bool
198+ isFieldOrParam n = n `elem` (fieldNames ++ paramNames)
200+ isFieldOrParam' :: (Name, a) -> Bool
201+ isFieldOrParam' = isFieldOrParam . fst
203+ isField :: Name -> Bool
204+ isField = flip elem fieldNames
206+ isField' :: (Name, a, b, c, d, f) -> Bool
207+ isField' (n, _, _, _, _, _) = isField n
209+ fieldTerms :: [PTerm]
210+ fieldTerms = [t | (_, _, t, _) <- fields]
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)
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
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 _ [] [] = []
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
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
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)
260+ -- | Decides whether a setter should be generated for a field or not.
261+ optionalSetter :: Name -> Bool
262+ optionalSetter n = n `elem` dependedOn
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]
268+ fieldDep :: Name -> PTerm -> (Name, [Name])
269+ fieldDep n t = ((nsroot n), paramNames ++ fieldNames `intersect` allNamesIn t)
271+ -- | A list of fields depending on another field.
272+ dependentFields :: [Name]
273+ dependentFields = filter depends fieldNames
275+ depends :: Name -> Bool
276+ depends n = case lookup n fieldDependencies of
277+ Just xs -> not $ null xs
280+ -- | A list of fields depended on by other fields.
281+ dependedOn :: [Name]
282+ dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))
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
298+elabProjection info cname pname plicity projTy pdoc psyn fc targetTy cn phArgs fnames index
299+ = do logLvl 1 $ "Generating Projection for " ++ show pname
302+ logLvl 1 $ "Type of " ++ show pname ++ ": " ++ show ty
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
309+ rec_elabDecl info EAll info ty
311+ let clause = PClause fc pname lhs [] rhs []
312+ rec_elabDecl info EAll info $ PClauses fc [] pname [clause]
314+ -- | The type of the projection function.
316+ generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName targetTy projTy
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)]
117− getpn as [] = []
323+ lhsArgs :: Int -> [PArg] -> [PArg]
118− getpn as (i:is) | length as > i,
324+ lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
119− PRef _ n <- getTm (as!!i) = n : getpn as is
325+ lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)
120− | otherwise = getpn as is
326+ lhsArgs _ [] = []
121− getPNames _ _ = []
327+
122−
328+ -- | The "_in" name. Used for the lhs.
123− tryElabDecl info (fn, ty, val)
329+ pname_in :: Name
124− = do i <- getIState
330+ pname_in = rootname -- in_name rootname
333+ rootname = nsroot cname
335+ -- | The right hand side of the projection function.
336+ generateRhs :: PTerm
337+ generateRhs = PRef fc pname_in
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
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
359+ logLvl 1 $ "Type of " ++ show set_pname ++ ": " ++ show ty
361+ let lhs = generateLhs
362+ logLvl 1 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs
364+ let rhs = generateRhs
365+ logLvl 1 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs
367+ let clause = PClause fc set_pname lhs [] rhs []
125− idrisCatch (do rec_elabDecl info EAll info ty
369+ idrisCatch (do rec_elabDecl info EAll info ty
126− rec_elabDecl info EAll info val)
370+ rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])
127− (\v -> do iputStrLn $ show fc ++
371+ (\err -> logLvl 1 $ "Could not generate update function for " ++ show pname)
128− ":Warning - can't generate setter for " ++
372+ {-if optional
129− show fn ++ " (" ++ show ty ++ ")"
373+ then logLvl 1 $ "Could not generate update function for " ++ show pname
130−-- ++ "\n" ++ pshow i v
374+ else tclift $ tfail $ At fc (Elaborating "record update function " pname err)) -}
131− putIState i)
375+ where
132−
376+ -- | The type of the udpate function.
133− getBoundImpls (PPi (Imp _ _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
377+ generateTy :: PDecl
134− getBoundImpls _ = []
378+ generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) pty (PPi expl recName sty (substInput sty))
135−
379+ where substInput = substMatches [(cname, PRef fc (nsroot pname))]
136− getImplB k (PPi (Imp l s _ _) n Placeholder sc)
380+
137− = getImplB k sc
381+ -- | The "_set" name.
138− getImplB k (PPi (Imp l s p fa) n ty sc)
382+ set_pname :: Name
139− = getImplB (\x -> k (PPi (Imp l s p fa) n ty x)) sc
383+ set_pname = set_name pname
140− getImplB k (PPi _ n ty sc)
384+
141− = getImplB k sc
385+ set_name :: Name -> Name
142− getImplB k _ = k
386+ set_name (UN n) = sUN ("set_" ++ str n)
143−
387+ set_name (MN i n) = sMN i ("set_" ++ str n)
144− renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
388+ set_name (NS n s) = NS (set_name n) s
145− = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
389+ set_name n = n
146− renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
390+
147− renameBs _ t = t
391+ -- | The left-hand side of the update function.
148−
392+ generateLhs :: PTerm
149− getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
393+ generateLhs = PApp fc (PRef fc set_pname) [pexp $ PRef fc pname_in, pexp constructorPattern]
150− getProjs acc r = reverse acc
394+ where
151−
395+ constructorPattern :: PTerm
152− getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
396+ constructorPattern = PApp fc (PRef fc cn) args
153− getFieldNames (PPi _ _ _ s) = getFieldNames s
397+
154− getFieldNames _ = []
398+ -- | The "_in" name.
155−
399+ pname_in :: Name
156− getRecTy (PPi _ n ty s) = getRecTy s
400+ pname_in = in_name rootname
158−
402+ rootname :: Name
159− -- make sure we pick a consistent name for parameters; any name will do
403+ rootname = nsroot pname
161− getRecNameMap x ppos (PApp fc t args)
405+ -- | The right-hand side of the update function.
162− = mapMaybe toMN (zip [0..] (map getTm args))
406+ generateRhs :: PTerm
407+ generateRhs = PApp fc (PRef fc cn) (newArgs i args)
164− toMN (i, PRef fc n)
409+ newArgs :: Int -> [PArg] -> [PArg]
165− | i `elem` ppos = Just (n, PRef fc (mkp n))
410+ newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
166− | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))
411+ newArgs i (x : rest) = x : (newArgs (i-1) rest)
167− toMN _ = Nothing
412+ newArgs _ [] = []
168− getRecNameMap x _ _ = []
413+
169−
414+-- | Post-fixes a name with "_in".
170− rec = sMN 0 "rec"
415+in_name :: Name -> Name
171−
416+in_name (UN n) = sMN 0 (str n ++ "_in")
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)
417+in_name (MN i n) = sMN i (str n ++ "_in")
175− mkp (NS n s) = NS (mkp n) s
418+in_name (NS n s) = NS (in_name n) s
177− mkImp (UN n) = sUN ("implicit_" ++ str n)
420+
178− mkImp (MN i n) = sMN i ("implicit_" ++ str n)
421+-- | Creates a PArg with a given plicity, name, and term.
179− mkImp (NS n s) = NS (mkImp n) s
422+asArg :: Plicity -> Name -> PTerm -> PArg
180−
423+asArg (Imp os _ _ _) n t = PImp 0 False os n t
181− mkType (UN n) = sUN ("set_" ++ str n)
424+asArg (Exp os _ _) n t = PExp 0 os n t
182− mkType (MN i n) = sMN i ("set_" ++ str n)
425+asArg (Constraint os _) n t = PConstraint 0 os n t
183− mkType (NS n s) = NS (mkType n) s
426+asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t
185− mkProj recty substs cimp ((pn_in, pty), pos)
428+-- | Machine name "rec".
186− = do let pn = expandNS syn pn_in -- projection name
429+recName :: Name
187− -- use pn_in in the indices, consistently, to avoid clash
430+recName = sMN 0 "rec"
188− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
431+
189− (PPi expl rec recty
432+recRef = PRef emptyFC recName
190− (substMatches substs pty))
433+
191− let pls = repeat Placeholder
434+projectInType :: [(Name, Name)] -> PTerm -> PTerm
192− let before = pos
435+projectInType xs = mapPT st
193− let after = length substs - (pos + 1)
436+ where
194− let args = take before pls ++ PRef fc (mkp pn_in) : take after pls
437+ st :: PTerm -> PTerm
195− let iargs = map implicitise (zip cimp args)
438+ st (PRef fc n)
196− let lhs = PApp fc (PRef fc pn)
439+ | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
197− [pexp (PApp fc (PRef fc cn) iargs)]
440+ st t = t
198− let rhs = PRef fc (mkp pn_in)
441+
199− let pclause = PClause fc pn lhs [] rhs []
442+-- | Creates an PArg from a plicity and a name where the term is a PRef.
200− return [pfnTy, PClauses fc [] pn [pclause]]
443+asPRefArg :: Plicity -> Name -> PArg
201−
444+asPRefArg p n = asArg p (nsroot n) $ PRef emptyFC (nsroot n)
202− implicitise (pa, t) = pa { getTm = t }
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
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
222− let rhsArgs = take pos pls ++ (PRef fc valname) :
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))])
230− (PApp fc (PRef fc cn)
231− (map pexp rhsArgs)) []
232− return (pn, pfnTy, PClauses fc [] setname [pclause])
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
239− if n `elem` allNamesIn t
240− then PPi impl n' ty (implBindUp ns is t)
241− else implBindUp ns is t