@@ -792,16 +792,14 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
792 let index_names_in = getRecNameMap "_in" recty
792 let index_names_in = getRecNameMap "_in" recty
793 let recty_in = substMatches index_names_in recty
793 let recty_in = substMatches index_names_in recty
795− let index_names_out = getRecNameMap "'" recty
796− let recty_out = substMatches index_names_out recty
798 logLvl 1 $ show (recty, ptys)
795 logLvl 1 $ show (recty, ptys)
799 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
796 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
800 [pexp (PRef fc rec)])) ptys
797 [pexp (PRef fc rec)])) ptys
801 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
798 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
802 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
799 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
803 let implBinds = getImplB id cty'
800 let implBinds = getImplB id cty'
804− update_decls <- mapM (mkUpdate recty
801+ update_decls <- mapM (mkUpdate recty index_names_in
802+ (getFieldNames cty')
805 implBinds (length nonImp)) (zip nonImp [0..])
803 implBinds (length nonImp)) (zip nonImp [0..])
806 mapM_ (elabDecl EAll info) (concat proj_decls)
804 mapM_ (elabDecl EAll info) (concat proj_decls)
807 logLvl 1 $ show update_decls
805 logLvl 1 $ show update_decls
@@ -838,6 +836,10 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
838 getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
836 getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
839 getProjs acc r = reverse acc
837 getProjs acc r = reverse acc
839+ getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s
840+ getFieldNames (PPi _ _ _ s) = getFieldNames s
841+ getFieldNames _ = []
841 getRecTy (PPi _ n ty s) = getRecTy s
843 getRecTy (PPi _ n ty s) = getRecTy s
842 getRecTy t = t
844 getRecTy t = t
@@ -882,13 +884,20 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
882 -- If the 'pty' we're updating includes anything in 'substs', we're
884 -- If the 'pty' we're updating includes anything in 'substs', we're
883 -- updating the type as well, so use recty', otherwise just use
885 -- updating the type as well, so use recty', otherwise just use
885− mkUpdate recty k num ((pn, pty), pos)
887+ mkUpdate recty inames fnames k num ((pn, pty), pos)
886 = do let setname = expandNS syn $ mkType pn
888 = do let setname = expandNS syn $ mkType pn
887 let valname = sMN 0 "updateval"
889 let valname = sMN 0 "updateval"
890+ let pn_out = sMN 0 (show pn ++ "_out")
891+ let pn_in = sMN 0 (show pn ++ "_in")
892+ let recty_in = substMatches [(pn, PRef fc pn_in)] recty
893+ let recty_out = substMatches [(pn, PRef fc pn_out)] recty
894+ let pt = substMatches inames $
888− let pt = k (PPi expl pn pty
895+ k (PPi expl pn_out pty
889− (PPi expl rec recty recty))
896+ (PPi expl rec recty_in recty_out))
890 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
897 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
891− let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
898+-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
899+ let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
900+ let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames
892 let lhsArgs = pls
901 let lhsArgs = pls
893 let rhsArgs = take pos pls ++ (PRef fc valname) :
902 let rhsArgs = take pos pls ++ (PRef fc valname) :
894 drop (pos + 1) pls
903 drop (pos + 1) pls