@@ -785,14 +785,26 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
785785 let ptys = getProjs [] (renameBs cimp cty)
786786 let ptys_u = getProjs [] cty
787787 let recty = getRecTy cty
788− logLvl 6 $ show (recty, ptys)
788+
789+ -- rename indices when we generate the getter/setter types, so
790+ -- that they don't clash with the names of the projections
791+ -- we're generating
792+ let index_names_in = getRecNameMap "_in" recty
793+ let recty_in = substMatches index_names_in recty
794+
795+ let index_names_out = getRecNameMap "'" recty
796+ let recty_out = substMatches index_names_out recty
797+
798+ logLvl 1 $ show (recty, ptys)
789799 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
790800 [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..])
792802 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
793803 let implBinds = getImplB id cty'
794− update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])
804+ update_decls <- mapM (mkUpdate recty
805+ implBinds (length nonImp)) (zip nonImp [0..])
795806 mapM_ (elabDecl EAll info) (concat proj_decls)
807+ logLvl 1 $ show update_decls
796808 mapM_ (tryElabDecl info) (update_decls)
797809 where
798810-- 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
807819 (\v -> do iputStrLn $ show fc ++
808820 ":Warning - can't generate setter for " ++
809821 show fn ++ " (" ++ show ty ++ ")"
822+-- ++ "\n" ++ pshow i v
810823 putIState i)
811824
812825 getImplB k (PPi (Imp l s _) n Placeholder sc)
@@ -828,6 +841,12 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
828841 getRecTy (PPi _ n ty s) = getRecTy s
829842 getRecTy t = t
830843
844+ getRecNameMap x (PApp fc t args) = mapMaybe (toMN . getTm) args
845+ where
846+ toMN (PRef fc n) = Just (n, PRef fc (sMN 0 (show n ++ x)))
847+ toMN _ = Nothing
848+ getRecNameMap x _ = []
849+
831850 rec = sMN 0 "rec"
832851
833852 mkp (UN n) = sMN 0 ("p_" ++ str n)
@@ -860,13 +879,16 @@ elabRecord info syn doc fc tyn ty cdoc cn cty
860879
861880 implicitise (pa, t) = pa { getTm = t }
862881
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
884+ -- recty
863885 mkUpdate recty k num ((pn, pty), pos)
864886 = do let setname = expandNS syn $ mkType pn
865887 let valname = sMN 0 "updateval"
866888 let pt = k (PPi expl pn pty
867889 (PPi expl rec recty recty))
868890 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]
870892 let lhsArgs = pls
871893 let rhsArgs = take pos pls ++ (PRef fc valname) :
872894 drop (pos + 1) pls