@@ -774,11 +774,16 @@ elabTransform info fc safe lhs_in rhs_in
775elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
775elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->
776 PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
776 PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()
777−elabRecord info syn doc fc tyn ty opts cdoc cn cty
777+elabRecord info syn doc fc tyn ty opts cdoc cn cty_in
778− = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])
778+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty_in, fc, [])])
779 -- TODO think: something more in info?
779 -- TODO think: something more in info?
780− cty' <- implicit info syn cn cty
780+ cty' <- implicit info syn cn cty_in
781 i <- getIState
781 i <- getIState
783+ -- get bound implicits and propagate to setters (in case they
784+ -- provide useful information for inference)
785+ let extraImpls = getBoundImpls cty'
782 cty <- case lookupTy cn (tt_ctxt i) of
787 cty <- case lookupTy cn (tt_ctxt i) of
783 [t] -> return (delab i t)
788 [t] -> return (delab i t)
784 _ -> ifail "Something went inexplicably wrong"
789 _ -> ifail "Something went inexplicably wrong"
@@ -797,14 +802,18 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
797 logLvl 1 $ show (recty, ptys)
802 logLvl 1 $ show (recty, ptys)
798 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
803 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
799 [pexp (PRef fc rec)])) ptys
804 [pexp (PRef fc rec)])) ptys
806+ -- Generate projection functions
800 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
807 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])
801 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
808 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)
802 let implBinds = getImplB id cty'
809 let implBinds = getImplB id cty'
811+ -- Generate update functions
803− update_decls <- mapM (mkUpdate recty index_names_in
812+ update_decls <- mapM (mkUpdate recty index_names_in extraImpls
804 (getFieldNames cty')
813 (getFieldNames cty')
805 implBinds (length nonImp)) (zip nonImp [0..])
814 implBinds (length nonImp)) (zip nonImp [0..])
806 mapM_ (elabDecl EAll info) (concat proj_decls)
815 mapM_ (elabDecl EAll info) (concat proj_decls)
807− logLvl 1 $ show update_decls
816+ logLvl 3 $ show update_decls
808 mapM_ (tryElabDecl info) (update_decls)
817 mapM_ (tryElabDecl info) (update_decls)
810-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
819-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }
@@ -819,9 +828,12 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
819 (\v -> do iputStrLn $ show fc ++
828 (\v -> do iputStrLn $ show fc ++
820 ":Warning - can't generate setter for " ++
829 ":Warning - can't generate setter for " ++
821 show fn ++ " (" ++ show ty ++ ")"
830 show fn ++ " (" ++ show ty ++ ")"
822−-- ++ "\n" ++ pshow i v
831+ ++ "\n" ++ pshow i v
823 putIState i)
832 putIState i)
834+ getBoundImpls (PPi (Imp _ _ _) n ty sc) = (n, ty) : getBoundImpls sc
835+ getBoundImpls _ = []
825 getImplB k (PPi (Imp l s _) n Placeholder sc)
837 getImplB k (PPi (Imp l s _) n Placeholder sc)
826 = getImplB k sc
838 = getImplB k sc
827 getImplB k (PPi (Imp l s p) n ty sc)
839 getImplB k (PPi (Imp l s p) n ty sc)
@@ -886,7 +898,7 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
886 -- If the 'pty' we're updating includes anything in 'substs', we're
898 -- If the 'pty' we're updating includes anything in 'substs', we're
887 -- updating the type as well, so use recty', otherwise just use
899 -- updating the type as well, so use recty', otherwise just use
889− mkUpdate recty inames fnames k num ((pn, pty), pos)
901+ mkUpdate recty inames extras fnames k num ((pn, pty), pos)
890 = do let setname = expandNS syn $ mkType pn
902 = do let setname = expandNS syn $ mkType pn
891 let valname = sMN 0 "updateval"
903 let valname = sMN 0 "updateval"
892 let pn_out = sMN 0 (show pn ++ "_out")
904 let pn_out = sMN 0 (show pn ++ "_out")
@@ -894,8 +906,8 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
894 let recty_in = substMatches [(pn, PRef fc pn_in)] recty
906 let recty_in = substMatches [(pn, PRef fc pn_in)] recty
895 let recty_out = substMatches [(pn, PRef fc pn_out)] recty
907 let recty_out = substMatches [(pn, PRef fc pn_out)] recty
896 let pt = substMatches inames $
908 let pt = substMatches inames $
897− k (PPi expl pn_out pty
909+ k (implBindUp extras inames (PPi expl pn_out pty
898− (PPi expl rec recty_in recty_out))
910+ (PPi expl rec recty_in recty_out)))
899 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
911 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt
900-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
912-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]
901 let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
913 let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames
@@ -913,6 +925,15 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty
913 (map pexp rhsArgs)) []
925 (map pexp rhsArgs)) []
914 return (pn, pfnTy, PClauses fc [] setname [pclause])
926 return (pn, pfnTy, PClauses fc [] setname [pclause])
928+ implBindUp [] is t = t
929+ implBindUp ((n, ty):ns) is t
930+ = let n' = case lookup n is of
931+ Just (PRef _ x) -> x
933+ if n `elem` allNamesIn t
934+ then PPi impl n' ty (implBindUp ns is t)
935+ else implBindUp ns is t
916-- FIXME: 'forcenames' is an almighty hack! Need a better way of
937-- FIXME: 'forcenames' is an almighty hack! Need a better way of
917-- erasing non-forceable things
938-- erasing non-forceable things