@@ -785,14 +785,26 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
785 let ptys = getProjs [] (renameBs cimp cty)
785 let ptys = getProjs [] (renameBs cimp cty)
786 let ptys_u = getProjs [] cty
786 let ptys_u = getProjs [] cty
787 let recty = getRecTy cty
787 let recty = getRecTy cty
789+ -- rename indices when we generate the getter/setter types, so
790+ -- that they don't clash with the names of the projections
792+ let index_names_in = getRecNameMap "_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
788− logLvl 6 $ show (recty, ptys)
798+ logLvl 1 $ show (recty, ptys)
789 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
799 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
790 [pexp (PRef fc rec)])) ptys
800 [pexp (PRef fc rec)])) ptys
791− proj_decls <- mapM (mkProj recty substs cimp) (zip ptys [0..])
801+ proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
792 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
802 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
793 let implBinds = getImplB id cty'
803 let implBinds = getImplB id cty'
804+ update_decls <- mapM (mkUpdate recty
794− update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])
805+ implBinds (length nonImp)) (zip nonImp [0..])
795 mapM_ (elabDecl EAll info) (concat proj_decls)
806 mapM_ (elabDecl EAll info) (concat proj_decls)
807+ logLvl 1 $ show update_decls
796 mapM_ (tryElabDecl info) (update_decls)
808 mapM_ (tryElabDecl info) (update_decls)
798-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
810-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
@@ -807,6 +819,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
807 (\v -> do iputStrLn $ show fc ++
819 (\v -> do iputStrLn $ show fc ++
808 ":Warning - can't generate setter for " ++
820 ":Warning - can't generate setter for " ++
809 show fn ++ " (" ++ show ty ++ ")"
821 show fn ++ " (" ++ show ty ++ ")"
822+-- ++ "\n" ++ pshow i v
810 putIState i)
823 putIState i)
812 getImplB k (PPi (Imp l s _) n Placeholder sc)
825 getImplB k (PPi (Imp l s _) n Placeholder sc)
@@ -828,6 +841,12 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
828 getRecTy (PPi _ n ty s) = getRecTy s
841 getRecTy (PPi _ n ty s) = getRecTy s
829 getRecTy t = t
842 getRecTy t = t
844+ getRecNameMap x (PApp fc t args) = mapMaybe (toMN . getTm) args
846+ toMN (PRef fc n) = Just (n, PRef fc (sMN 0 (show n ++ x)))
848+ getRecNameMap x _ = []
831 rec = sMN 0 "rec"
850 rec = sMN 0 "rec"
833 mkp (UN n) = sMN 0 ("p_" ++ str n)
852 mkp (UN n) = sMN 0 ("p_" ++ str n)
@@ -860,13 +879,16 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
861 implicitise (pa, t) = pa { getTm = t }
880 implicitise (pa, t) = pa { getTm = t }
882+ -- If the 'pty' we're updating includes anything in 'substs', we're
883+ -- updating the type as well, so use recty', otherwise just use
863 mkUpdate recty k num ((pn, pty), pos)
885 mkUpdate recty k num ((pn, pty), pos)
864 = do let setname = expandNS syn $ mkType pn
886 = do let setname = expandNS syn $ mkType pn
865 let valname = sMN 0 "updateval"
887 let valname = sMN 0 "updateval"
866 let pt = k (PPi expl pn pty
888 let pt = k (PPi expl pn pty
867 (PPi expl rec recty recty))
889 (PPi expl rec recty recty))
868 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
890 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
869− let pls = map (\x -> PRef fc (sMN x "field")) [0..num-1]
891+ let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
870 let lhsArgs = pls
892 let lhsArgs = pls
871 let rhsArgs = take pos pls ++ (PRef fc valname) :
893 let rhsArgs = take pos pls ++ (PRef fc valname) :
872 drop (pos + 1) pls
894 drop (pos + 1) pls