@@ -1,281 +1,359 @@
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
9−import Idris.Imports
10−import Idris.ElabTerm
11−import Idris.Coverage
12−import Idris.DataOpts
13−import Idris.Providers
14−import Idris.Primitives
15−import Idris.Inliner
16−import Idris.PartialEval
17−import Idris.DeepSeq
18−import Idris.Output (iputStrLn, pshow, iWarn)
19−import IRTS.Lang
20−import Idris.ParseHelpers (opChars)
21−
22−import Idris.Elab.Type
23−import Idris.Elab.Data
24−import Idris.Elab.Utils
8+
9+import Idris.ParseExpr -- Remove me
2510
2611import Idris.Core.TT
27−import Idris.Core.Elaborate hiding (Tactic(..))
2812import Idris.Core.Evaluate
29−import Idris.Core.Execute
30−import Idris.Core.Typecheck
31−import Idris.Core.CaseTree
32−
33−import Idris.Docstrings
3413
35−import Prelude hiding (id, (.))
36−import Control.Category
14+import Idris.Elab.Data
3715
38−import Control.Applicative hiding (Const)
39−import Control.DeepSeq
40−import Control.Monad
41−import Control.Monad.State.Strict as State
42−import Data.List
4316import Data.Maybe
44−import Debug.Trace
45−
46−import qualified Data.Map as Map
47−import qualified Data.Set as S
48−import qualified Data.Text as T
49−import Data.Char(isLetter, toLower)
50−import Data.List.Split (splitOn)
51−
52−import Util.Pretty(pretty, text)
53−
54−elabRecord :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> FC -> Name ->
55− PTerm -> DataOpts -> Docstring (Either Err PTerm) -> Maybe Name -> [(Name, Plicity)] -> PTerm -> Idris ()
56−elabRecord info syn doc fc tyn ty opts cdoc mcn args cty_in
57− = do cn <- liftM (expandNS syn) (case mcn of
58− Just cn' -> return (nsroot cn')
59− Nothing -> if isOp tyn
60− then generateConsNameOp
61− else generateConsName (sUN $ "Mk" ++ (show (nsroot tyn))))
62−
63− elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
64− -- TODO think: something more in info?
65− cty' <- implicit info syn cn cty_in
66− i <- getIState
67−
68− -- get bound implicits and propagate to setters (in case they
69− -- provide useful information for inference)
70− let extraImpls = getBoundImpls cty'
71−
72− cty <- case lookupTy cn (tt_ctxt i) of
73− [t] -> return (delab i t)
74− _ -> ifail "Something went inexplicably wrong"
75− cimp <- case lookupCtxt cn (idris_implicits i) of
76− [imps] -> return imps
77− ppos <- case lookupCtxt tyn (idris_datatypes i) of
78− [ti] -> return $ param_pos ti
79− let cty_imp = renameBs cimp cty
80− let ptys = getProjs [] cty_imp
81− let ptys_u = getProjs [] cty
82− let recty = getRecTy cty_imp
83− let recty_u = getRecTy cty
84−
85− let paramNames = getPNames recty ppos
86−
87− -- rename indices when we generate the getter/setter types, so
88− -- that they don't clash with the names of the projections
89− -- we're generating
90− let index_names_in = getRecNameMap "_in" ppos recty
91− let recty_in = substMatches index_names_in recty
92−
93− logLvl 3 $ show (recty, recty_u, ppos, paramNames, ptys)
94− -- Substitute indices with projection functions, and parameters with
95− -- the updated parameter name
96− let substs = map (\ (n, _) ->
97− if n `elem` paramNames
98− then (n, PRef fc (mkp n))
99− else (n, PApp fc (PRef fc n)
100− [pexp (PRef fc rec)]))
101− ptys
102−
103− -- Generate projection functions
104− proj_decls <- mapM (mkProj recty_in substs cimp cn) (zip ptys [0..])
105− logLvl 3 $ show proj_decls
106− let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
107− let implBinds = getImplB id cty'
108− mapM_ (rec_elabDecl info EAll info) (concat proj_decls)
109− -- Generate update functions
110− when (Codata `notElem` opts)
111− (do update_decls <- mapM (mkUpdate recty_u index_names_in extraImpls
112− (getFieldNames cty')
113− implBinds (length nonImp) cn) (zip nonImp [0..])
114− logLvl 3 $ show update_decls
115− mapM_ (tryElabDecl info) (update_decls))
17+import Data.List
18+import Control.Monad
19+
20+-- TODO:
21+-- Consider what to do about type parameters in projection that do not occur as a parameter.
22+-- I.e. set_bar : Foo n -> Vect n a
23+
24+elabRecord :: ElabInfo ->
25+ (Docstring (Either Err PTerm)) ->
26+ SyntaxInfo ->
27+ FC ->
28+ DataOpts ->
29+ Name -> -- ^ Record Type Name
30+ [(Name, Plicity, PTerm)] -> -- ^ Parameters
31+ [(Name, Docstring (Either Err PTerm))] -> -- ^ Parameter Docs
32+ [(Name, Plicity, PTerm)] -> -- ^ Fields
33+ [(Name, Docstring (Either Err PTerm))] -> -- ^ Field Docs
34+ Maybe Name -> -- ^ Constructor Name
35+ (Docstring (Either Err PTerm)) -> -- ^ Constructor Doc
36+ SyntaxInfo -> -- ^ Constructor SyntaxInfo
37+ Idris ()
38+elabRecord info doc rsyn fc opts tyn params paramDocs fields fieldDocs cname cdoc csyn
39+ = do logLvl 2 $ "Building data declaration for " ++ show tyn
40+ -- Type constructor
41+ let tycon = generateTyCon params
42+ logLvl 4 $ "Type constructor " ++ showTmImpls tycon
43+
44+ -- Data constructor
45+ dconName <- liftM (expandNS csyn) $ generateDConName cname
46+ let dcon = generateDCon params fields
47+ logLvl 4 $ "Data constructor: " ++ showTmImpls dcon
48+
49+ -- Build data declaration for elaboration
50+ let datadecl = PDatadecl tyn tycon [(cdoc, [], dconName, dcon, fc, [])]
51+ elabData info rsyn doc [] fc opts datadecl
52+
53+ i <- getIState
54+
55+ -- The elaborated constructor for the data declaration
56+ ttCons <-
57+ case lookupTyExact dconName (tt_ctxt i) of
58+ Just as -> return as
59+ Nothing -> tclift $ tfail $ At fc (Elaborating "record" tyn (Msg "It seems like the constructor for this record has disappeared. :( \n This is a bug. Please report."))
60+
61+ -- The arguments to the constructor
62+ let constructorArgs = getArgTys ttCons
63+ -- The parameters for elaboration with their documentation
64+ paramsForElab = [((nsroot n), (param_name n), impl, t, d) | (n, t, d) <- zip' i params paramDocs]
65+ -- If elaborating the constructor has resulted in some new implicit fields we make a projeciton functions for them.
66+ freeFieldsForElab = map (freeField i) (filter (not . isFieldOrParam') constructorArgs)
67+ -- The fields (written by the user) with their documentation.
68+ userFieldsForElab = [((nsroot n), n, p, t, d) | ((n, p, t), (_, d)) <- zip fields fieldDocs]
69+ -- All things we need to elaborate projection functions for, together with a number denoting their position in the constructor.
70+ fieldsForElab = [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (freeFieldsForElab ++ paramsForElab ++ userFieldsForElab) [0..]]
71+
72+ -- Build projection functions
73+ elabProj dconName fieldsForElab
74+ -- Build update functions
75+ elabUp dconName fieldsForElab -- [(n, n', p, t, d, i) | ((n, n', p, t, d), i) <- zip (paramsForElab ++ userFieldsForElab) [0..]]
11676 where
117−-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
118− customizeConstructor :: [(Name, Plicity)] -> PTerm -> Idris PTerm
119− customizeConstructor [] t = return t
120− customizeConstructor ns t = cc ns t
77+ -- | Generates a type constructor.
78+ generateTyCon :: [(Name, Plicity, PTerm)] -> PTerm
79+ generateTyCon ((n, p, t) : rest) = PPi p (nsroot n) t (generateTyCon rest)
80+ generateTyCon [] = PType
81+
82+ -- | Generates a name for the data constructor if none was specified.
83+ generateDConName :: Maybe Name -> Idris Name
84+ generateDConName (Just n) = return $ expandNS csyn n
85+ generateDConName Nothing = uniqueName (expandNS csyn $ sMN 0 ("Mk" ++ (show (nsroot tyn))))
12186 where
122− cc names (PPi _ n t t')
123− | Just p <- lookup n names = do r <- cc (deleteAssoc n names) t'
124− return $ PPi p n t r
125− | otherwise = tclift $ tfail (At fc (Elaborating recString tyn (Msg ("Argument " ++ show n ++ " missing."))))
126− where
127− deleteAssoc :: Eq a => a -> [(a, b)] -> [(a, b)]
128− deleteAssoc y (x@(z,_) : xs)
129− | z == y = xs
130− | otherwise = x : (deleteAssoc y xs)
131− deleteAssoc _ [] = []
132− cc [] t = return t
133− cc _ _ = tclift $ tfail (At fc (Elaborating recString tyn (Msg ("Not the right of arguments to constructor. You must mention either all or none."))))
134−
135− recString = (if Codata `elem` opts then "co" else "") ++ "record "
136−
137− generateConsNameOp :: Idris Name
138− generateConsNameOp = generateConsName $ sUN "Mk_Operator_Record0"
139−
140− generateConsName :: Name -> Idris Name
141− generateConsName n = do i <- getIState
142− case lookupTyNameExact (expandNS syn n) (tt_ctxt i) of
143− Just _ -> generateConsName (nextName n)
144− Nothing -> return n
145−
146− isOp :: Name -> Bool
147− isOp (UN t) = foldr (||) False (map (\x -> x `elem` opChars) (str t))
148− isOp (NS n _) = isOp n
149− isOp _ = True
150−
151− isNonImp (PExp _ _ _ _, a) = Just a
152− isNonImp _ = Nothing
87+ uniqueName :: Name -> Idris Name
88+ uniqueName n = do i <- getIState
89+ case lookupTyNameExact n (tt_ctxt i) of
90+ Just _ -> uniqueName (nextName n)
91+ Nothing -> return n
92+
93+ -- | Generates the data constructor type.
94+ generateDCon :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
95+ generateDCon ((n, _, t) : ps) as = PPi impl (nsroot n) t (generateDCon ps as)
96+ generateDCon [] ((n, p, t) : as) = PPi p (nsroot n) t (generateDCon [] as)
97+ generateDCon [] [] = target
98+
99+ -- | Creates an PArg from a plicity and a name where the term is a PRef.
100+ paramAsArg :: Plicity -> Name -> PArg
101+ paramAsArg p n = asArg p (nsroot n) $ PRef fc (nsroot n)
102+
103+ -- | The target for the constructor and projection functions. Also the source of the update functions.
104+ target :: PTerm
105+ target = PApp fc (PRef fc tyn) $ map (uncurry paramAsArg) [(p, n) | (n, p, t) <- params]
153106
154− getPNames (PApp _ _ as) ppos = getpn as ppos
107+ -- | Creates a PArg from a plicity and a name where the term is a Placeholder.
108+ placeholderArg :: Plicity -> Name -> PArg
109+ placeholderArg p n = asArg p (nsroot n) Placeholder
110+
111+ -- | Root names of all fields in the current record declarations
112+ fieldNames :: [Name]
113+ fieldNames = [nsroot n | (n, _, _) <- fields]
114+
115+ paramNames :: [Name]
116+ paramNames = [nsroot n | (n, _, _) <- params]
117+
118+ isFieldOrParam :: Name -> Bool
119+ isFieldOrParam = flip elem (fieldNames ++ paramNames)
120+
121+ isFieldOrParam' :: (Name, a) -> Bool
122+ isFieldOrParam' = isFieldOrParam . fst
123+
124+ isField :: Name -> Bool
125+ isField = flip elem fieldNames
126+
127+ isField' :: (Name, a, b, c, d, f) -> Bool
128+ isField' (n, _, _, _, _, _) = isField n
129+
130+ fieldTerms :: [PTerm]
131+ fieldTerms = [t | (_, _, t) <- fields]
132+
133+ projectInType :: [(Name, Name)] -> PTerm -> PTerm
134+ projectInType xs = mapPT st
155135 where
156− getpn as [] = []
157− getpn as (i:is) | length as > i,
158− PRef _ n <- getTm (as!!i) = n : getpn as is
159− | otherwise = getpn as is
160− getPNames _ _ = []
161−
162− tryElabDecl info (fn, ty, val)
163− = do i <- getIState
164− idrisCatch (do rec_elabDecl info EAll info ty
165− rec_elabDecl info EAll info val)
166− (\v -> do iputStrLn $ show fc ++
167− ":Warning - can't generate setter for " ++
168− show fn ++ " (" ++ show ty ++ ")"
169−-- ++ "\n" ++ pshow i v
170− putIState i)
171−
172− getBoundImpls (PPi (Imp _ _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
173− getBoundImpls _ = []
174−
175− getImplB k (PPi (Imp l s _ _) n Placeholder sc)
176− = getImplB k sc
177− getImplB k (PPi (Imp l s p fa) n ty sc)
178− = getImplB (\x -> k (PPi (Imp l s p fa) n ty x)) sc
179− getImplB k (PPi _ n ty sc)
180− = getImplB k sc
181− getImplB k _ = k
182−
183− renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)
184− = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
185− renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
186− renameBs _ t = t
187−
188− getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
189− getProjs acc r = reverse acc
190−
191− getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
192− getFieldNames (PPi _ _ _ s) = getFieldNames s
193− getFieldNames _ = []
194−
195− getRecTy (PPi _ n ty s) = getRecTy s
196− getRecTy t = t
197−
198− -- make sure we pick a consistent name for parameters; any name will do
199− -- otherwise
200− getRecNameMap x ppos (PApp fc t args)
201− = mapMaybe toMN (zip [0..] (map getTm args))
136+ st :: PTerm -> PTerm
137+ st (PRef fc n)
138+ | Just pn <- lookup n xs = PApp fc (PRef fc pn) [pexp recRef]
139+ st t = t
140+
141+ -- Delabs the TT to PTerm
142+ -- This is not good.
143+ -- However, for machine generated implicits, there seems to be no PTerm available.
144+ -- Is there a better way to do this without building the setters and getters as TT?
145+ freeField :: IState -> (Name, TT Name) -> (Name, Name, Plicity, PTerm, Docstring (Either Err PTerm))
146+ freeField i arg = (fst arg, (expandNS rsyn (free_name $ fst arg)), impl, (delab i (snd arg)), emptyDocstring)
147+
148+ free_name :: Name -> Name
149+ free_name (UN n) = sUN ("free_" ++ str n)
150+ free_name (MN i n) = sMN i ("free_" ++ str n)
151+ free_name (NS n s) = NS (free_name n) s
152+ free_name n = n
153+
154+ zip' :: IState -> [(Name, Plicity, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [(Name, PTerm, Docstring (Either Err PTerm))]
155+ zip' i ((n, _, t) : rest) ((_, d) : rest') = (n, t, d) : (zip' i rest rest')
156+ zip' i ((n, _, t) : rest) [] = (n, t, emptyDoc) : (zip' i rest [])
157+ where emptyDoc = annotCode (tryFullExpr rsyn i) emptyDocstring
158+ zip' _ [] [] = []
159+
160+ param_name :: Name -> Name
161+ param_name (UN n) = sUN ("param_" ++ str n)
162+ param_name (MN i n) = sMN i ("param_" ++ str n)
163+ param_name (NS n s) = NS (param_name n) s
164+ param_name n = n
165+
166+ -- | Elaborate the projection functions.
167+ elabProj :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
168+ elabProj cn fs = let phArgs = map (uncurry placeholderArg) [(p, n) | (n, _, p, _, _, _) <- fs]
169+ elab = \(n, n', p, t, doc, i) ->
170+ do let t' = projectInType [(m, m') | (m, m', _, _, _, _) <- fs] t
171+ elabProjection info n n' p t' doc rsyn fc target cn phArgs fieldNames i
172+ in mapM_ elab fs
173+
174+ -- | Elaborate the update functions.
175+ elabUp :: Name -> [(Name, Name, Plicity, PTerm, Docstring (Either Err PTerm), Int)] -> Idris ()
176+ elabUp cn fs = let args = map (uncurry paramAsArg) [(p, n) | (n, _, p, _, _, _) <- fs]
177+ elab = \(n, n', p, t, doc, i) -> elabUpdate info n n' p t doc rsyn fc target cn args fieldNames i (optionalSetter n)
178+ in mapM_ elab fs
179+
180+ -- | Decides whether a setter should be generated for a field or not.
181+ optionalSetter :: Name -> Bool
182+ optionalSetter n = n `notElem` dependentFields && n `notElem` dependedOn
183+
184+ -- | A map from a field name to the other fields it depends on.
185+ fieldDependencies :: [(Name, [Name])]
186+ fieldDependencies = map (uncurry fieldDep) [(n, t) | (n, _, t) <- fields]
187+ where
188+ fieldDep :: Name -> PTerm -> (Name, [Name])
189+ fieldDep n t = ((nsroot n), fieldNames `intersect` allNamesIn t)
190+
191+ -- | A list of fields depending on another field.
192+ dependentFields :: [Name]
193+ dependentFields = filter depends fieldNames
194+ where
195+ depends :: Name -> Bool
196+ depends n = case lookup n fieldDependencies of
197+ Just xs -> not $ null xs
198+ Nothing -> False
199+
200+ -- | A list of fields depended on by other fields.
201+ dependedOn :: [Name]
202+ dependedOn = concat ((catMaybes (map (\x -> lookup x fieldDependencies) fieldNames)))
203+
204+-- | Creates and elaborates a projection function.
205+elabProjection :: ElabInfo ->
206+ Name -> -- ^ Name of the argument in the constructor
207+ Name -> -- ^ Projection Name
208+ Plicity -> -- ^ Projection Plicity
209+ PTerm -> -- ^ Projection Type
210+ (Docstring (Either Err PTerm)) -> -- ^ Projection Documentation
211+ SyntaxInfo -> -- ^ Projection SyntaxInfo
212+ FC ->
213+ PTerm -> -- ^ Projection Target Type
214+ Name -> -- ^ Data Constructor Name
215+ [PArg] -> -- ^ Placeholder Arguments to constructor
216+ [Name] -> -- ^ All Field Names
217+ Int -> -- ^ Argument Index
218+ Idris ()
219+elabProjection info cname pname plicity pty pdoc psyn fc tty cn phArgs fnames index
220+ = do logLvl 2 $ "Generating Projection for " ++ show pname
221+
222+ let ty = generateTy
223+ logLvl 4 $ "Type of " ++ show pname ++ ": " ++ show ty
224+
225+ let lhs = generateLhs
226+ logLvl 4 $ "LHS of " ++ show pname ++ ": " ++ showTmImpls lhs
227+ let rhs = generateRhs
228+ logLvl 4 $ "RHS of " ++ show pname ++ ": " ++ showTmImpls rhs
229+
230+ rec_elabDecl info EAll info ty
231+
232+ let clause = PClause fc pname lhs [] rhs []
233+ rec_elabDecl info EAll info $ PClauses fc [] pname [clause]
234+ where
235+ -- | The type of the projection function.
236+ generateTy :: PDecl
237+ generateTy = PTy pdoc [] psyn fc [] pname $ PPi expl recName tty (mapPT applyProjs pty)
238+
239+ -- | Applies all fields to "rec".
240+ applyProjs :: PTerm -> PTerm
241+ applyProjs t@(PRef fc name)
242+ | (nsroot name) `elem` fnames = PApp fc t [pexp recRef]
243+ applyProjs t = t
244+
245+ -- | The left hand side of the projection function.
246+ generateLhs :: PTerm
247+ generateLhs = let args = lhsArgs index phArgs
248+ in PApp fc (PRef fc pname) [pexp (PApp fc (PRef fc cn) args)]
249+ where
250+ lhsArgs :: Int -> [PArg] -> [PArg]
251+ lhsArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
252+ lhsArgs i (x : rest) = x : (lhsArgs (i-1) rest)
253+ lhsArgs _ [] = []
254+
255+ -- | The "_in" name. Used for the lhs.
256+ pname_in :: Name
257+ pname_in = rootname -- in_name rootname
258+
259+ rootname :: Name
260+ rootname = nsroot cname
261+
262+ -- | The right hand side of the projection function.
263+ generateRhs :: PTerm
264+ generateRhs = PRef fc pname_in
265+
266+-- | Creates and elaborates an update function.
267+-- If 'optional' is true, we will not fail if we can't elaborate the update function.
268+elabUpdate :: ElabInfo ->
269+ Name -> -- ^ Name of the argument in the constructor
270+ Name -> -- ^ Field Name
271+ Plicity -> -- ^ Field Plicity
272+ PTerm -> -- ^ Field Type
273+ (Docstring (Either Err PTerm)) -> -- ^ Field Documentation
274+ SyntaxInfo -> -- ^ Field SyntaxInfo
275+ FC ->
276+ PTerm -> -- ^ Projection Source Type
277+ Name -> -- ^ Data Constructor Name
278+ [PArg] -> -- ^ Arguments to constructor
279+ [Name] -> -- ^ All fields
280+ Int -> -- ^ Argument Index
281+ Bool -> -- ^ Optional
282+ Idris ()
283+elabUpdate info cname pname plicity pty pdoc psyn fc sty cn args fnames i optional
284+ = do logLvl 2 $ "Generating Update for " ++ show pname
285+
286+ let ty = generateTy
287+ logLvl 4 $ "Type of " ++ show set_pname ++ ": " ++ show ty
288+
289+ let lhs = generateLhs
290+ logLvl 4 $ "LHS of " ++ show set_pname ++ ": " ++ showTmImpls lhs
291+
292+ let rhs = generateRhs
293+ logLvl 4 $ "RHS of " ++ show set_pname ++ ": " ++ showTmImpls rhs
294+
295+ let clause = PClause fc set_pname lhs [] rhs []
296+
297+ idrisCatch (do rec_elabDecl info EAll info ty
298+ rec_elabDecl info EAll info $ PClauses fc [] set_pname [clause])
299+ (\err -> if optional
300+ then logLvl 2 $ "Could not generate update function for " ++ show pname
301+ else tclift $ tfail $ At fc (Elaborating "record update function" pname err))
302+ where
303+ -- | The type of the udpate function.
304+ generateTy :: PDecl
305+ generateTy = PTy pdoc [] psyn fc [] set_pname $ PPi expl (nsroot pname) pty (PPi expl recName sty (substInput sty))
306+ where substInput = substMatches [(cname, PRef fc (nsroot pname))]
307+
308+ -- | The "_set" name.
309+ set_pname :: Name
310+ set_pname = set_name pname
311+
312+ set_name :: Name -> Name
313+ set_name (UN n) = sUN ("set_" ++ str n)
314+ set_name (MN i n) = sMN i ("set_" ++ str n)
315+ set_name (NS n s) = NS (set_name n) s
316+ set_name n = n
317+
318+ -- | The left-hand side of the update function.
319+ generateLhs :: PTerm
320+ generateLhs = PApp fc (PRef fc set_pname) [pexp $ PRef fc pname_in, pexp constructorPattern]
202321 where
203− toMN (i, PRef fc n)
204− | i `elem` ppos = Just (n, PRef fc (mkp n))
205− | otherwise = Just (n, PRef fc (sMN 0 (show n ++ x)))
206− toMN _ = Nothing
207− getRecNameMap x _ _ = []
208−
209− rec = sMN 0 "rec"
210−
211− -- only UNs propagate properly as parameters (bit of a hack then...)
212− mkp (UN n) = sUN ("_p_" ++ str n)
213− mkp (MN i n) = sMN i ("p_" ++ str n)
214− mkp (NS n s) = NS (mkp n) s
215−
216− mkImp (UN n) = sUN ("implicit_" ++ str n)
217− mkImp (MN i n) = sMN i ("implicit_" ++ str n)
218− mkImp (NS n s) = NS (mkImp n) s
219−
220− mkType (UN n) = sUN ("set_" ++ str n)
221− mkType (MN i n) = sMN i ("set_" ++ str n)
222− mkType (NS n s) = NS (mkType n) s
223−
224− mkProj recty substs cimp cn ((pn_in, pty), pos)
225− = do let pn = expandNS syn pn_in -- projection name
226− -- use pn_in in the indices, consistently, to avoid clash
227− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] pn
228− (PPi expl rec recty
229− (substMatches substs pty))
230− let pls = repeat Placeholder
231− let before = pos
232− let after = length substs - (pos + 1)
233− let args = take before pls ++ PRef fc (mkp pn_in) : take after pls
234− let iargs = map implicitise (zip cimp args)
235− let lhs = PApp fc (PRef fc pn)
236− [pexp (PApp fc (PRef fc cn) iargs)]
237− let rhs = PRef fc (mkp pn_in)
238− let pclause = PClause fc pn lhs [] rhs []
239− return [pfnTy, PClauses fc [] pn [pclause]]
240−
241− implicitise (pa, t) = pa { getTm = t }
242−
243− -- If the 'pty' we're updating includes anything in 'substs', we're
244− -- updating the type as well, so use recty', otherwise just use
245− -- recty
246− mkUpdate recty inames extras fnames k num cn ((pn, pty), pos)
247− = do let setname = expandNS syn $ mkType pn
248− let valname = sMN 0 "updateval"
249− let pn_out = sMN 0 (show pn ++ "_out")
250− let pn_in = sMN 0 (show pn ++ "_in")
251− let recty_in = substMatches [(pn, PRef fc pn_in)] recty
252− let recty_out = substMatches [(pn, PRef fc pn_out)] recty
253− let pt = substMatches inames $
254− k (implBindUp extras inames (PPi expl pn_out pty
255− (PPi expl rec recty_in recty_out)))
256− let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
257−-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
258− let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
259− let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames
260− let lhsArgs = pls
261− let rhsArgs = take pos pls ++ (PRef fc valname) :
262− drop (pos + 1) pls
263− let before = pos
264− let pclause = PClause fc setname (PApp fc (PRef fc setname)
265− [pexp (PRef fc valname),
266− pexp (PApp fc (PRef fc cn)
267− (map pexp lhsArgs))])
268− []
269− (PApp fc (PRef fc cn)
270− (map pexp rhsArgs)) []
271− return (pn, pfnTy, PClauses fc [] setname [pclause])
272−
273− implBindUp [] is t = t
274− implBindUp ((n, ty):ns) is t
275− = let n' = case lookup n is of
276− Just (PRef _ x) -> x
277− _ -> n in
278− if n `elem` allNamesIn t
279− then PPi impl n' ty (implBindUp ns is t)
280− else implBindUp ns is t
322+ constructorPattern :: PTerm
323+ constructorPattern = PApp fc (PRef fc cn) args
281324
325+ -- | The "_in" name.
326+ pname_in :: Name
327+ pname_in = in_name rootname
328+
329+ rootname :: Name
330+ rootname = nsroot pname
331+
332+ -- | The right-hand side of the update function.
333+ generateRhs :: PTerm
334+ generateRhs = PApp fc (PRef fc cn) (newArgs i args)
335+ where
336+ newArgs :: Int -> [PArg] -> [PArg]
337+ newArgs 0 (_ : rest) = (asArg plicity (nsroot cname) (PRef fc pname_in)) : rest
338+ newArgs i (x : rest) = x : (newArgs (i-1) rest)
339+ newArgs _ [] = []
340+
341+-- | Post-fixes a name with "_in".
342+in_name :: Name -> Name
343+in_name (UN n) = sMN 0 (str n ++ "_in")
344+in_name (MN i n) = sMN i (str n ++ "_in")
345+in_name (NS n s) = NS (in_name n) s
346+in_name n = n
347+
348+-- | Creates a PArg with a given plicity, name, and term.
349+asArg :: Plicity -> Name -> PTerm -> PArg
350+asArg (Imp os _ _ _) n t = PImp 0 False os n t
351+asArg (Exp os _ _) n t = PExp 0 os n t
352+asArg (Constraint os _) n t = PConstraint 0 os n t
353+asArg (TacImp os _ s) n t = PTacImplicit 0 os n s t
354+
355+-- | Machine name "rec".
356+recName :: Name
357+recName = sMN 0 "rec"
358+
359+recRef = PRef emptyFC recName