git.iko.soy/Idris-dev
on master help sign in
Small record fix for implicit arguments
db08df4Edwin Brady
src/Idris/ElabDecls.hs+14−7
compare with master
unifiedsplit
@@ -88,7 +88,7 @@ elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
88 PTerm -> Name -> PTerm -> Idris ()
88 PTerm -> Name -> PTerm -> Idris ()
89elabRecord info syn fc tyn ty cn cty
89elabRecord info syn fc tyn ty cn cty
90 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])
90 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])
91− cty <- implicit syn cn cty
91+ cty' <- implicit syn cn cty
92 i <- get
92 i <- get
93 cty <- case lookupTy Nothing cn (tt_ctxt i) of
93 cty <- case lookupTy Nothing cn (tt_ctxt i) of
94 [t] -> return (delab i t)
94 [t] -> return (delab i t)
@@ -103,7 +103,8 @@ elabRecord info syn fc tyn ty cn cty
103 [pexp (PRef fc rec)])) ptys
103 [pexp (PRef fc rec)])) ptys
104 proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
104 proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
105 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
105 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
106+ let implBinds = getImplB id cty'
106− update_decls <- mapM (mkUpdate recty (length nonImp)) (zip nonImp [0..])
107+ update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])
107 mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))
108 mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))
108 where
109 where
109-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
110-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
@@ -111,6 +112,12 @@ elabRecord info syn fc tyn ty cn cty
111 isNonImp (PExp _ _ _, a) = Just a
112 isNonImp (PExp _ _ _, a) = Just a
112 isNonImp _ = Nothing
113 isNonImp _ = Nothing
113
114
115+ getImplB k (PPi (Imp l s) n ty sc)
116+ = getImplB (\x -> k (PPi (Imp l s) n ty x)) sc
117+ getImplB k (PPi _ n ty sc)
118+ = getImplB k sc
119+ getImplB k _ = k
120+
114 renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
121 renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
115 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
122 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
116 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
123 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
@@ -140,7 +147,7 @@ elabRecord info syn fc tyn ty cn cty
140 = do let pn = expandNS syn pn_in
147 = do let pn = expandNS syn pn_in
141 let pfnTy = PTy defaultSyntax fc [] pn
148 let pfnTy = PTy defaultSyntax fc [] pn
142 (PPi expl rec recty
149 (PPi expl rec recty
143− (substMatches substs pty))
150+ (substMatches substs pty))
144 let pls = repeat Placeholder
151 let pls = repeat Placeholder
145 let before = pos
152 let before = pos
146 let after = length substs - (pos + 1)
153 let after = length substs - (pos + 1)
@@ -154,12 +161,12 @@ elabRecord info syn fc tyn ty cn cty
154
161
155 implicitise (pa, t) = pa { getTm = t }
162 implicitise (pa, t) = pa { getTm = t }
156
163
157− mkUpdate recty num ((pn, pty), pos)
164+ mkUpdate recty k num ((pn, pty), pos)
158 = do let setname = expandNS syn $ mkSet pn
165 = do let setname = expandNS syn $ mkSet pn
159 let valname = MN 0 "updateval"
166 let valname = MN 0 "updateval"
167+ let pt = k (PPi expl pn pty
168+ (PPi expl rec recty recty))
160− let pfnTy = PTy defaultSyntax fc [] setname
169+ let pfnTy = PTy defaultSyntax fc [] setname pt
161− (PPi expl pn pty
162− (PPi expl rec recty recty))
163 let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]
170 let pls = map (\x -> PRef fc (MN x "field")) [0..num-1]
164 let lhsArgs = pls
171 let lhsArgs = pls
165 let rhsArgs = take pos pls ++ (PRef fc valname) :
172 let rhsArgs = take pos pls ++ (PRef fc valname) :