From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- toplevel/obligations.ml | 43 +++++++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 16 deletions(-) (limited to 'toplevel/obligations.ml') diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 9019f486..314789ce 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -318,8 +318,9 @@ type program_info_aux = { prg_notations : notations ; prg_kind : definition_kind; prg_reduce : constr -> constr; - prg_hook : unit Lemmas.declaration_hook; + prg_hook : (Evd.evar_universe_context -> unit) Lemmas.declaration_hook; prg_opaque : bool; + prg_sign: named_context_val; } type program_info = program_info_aux Ephemeron.key @@ -517,7 +518,7 @@ let declare_definition prg = progmap_remove prg; !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits - (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r)) + (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r)) open Pp @@ -582,6 +583,7 @@ let declare_mutual_definition l = in (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in + let fix_exn = Stm.get_fix_exn () in let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) @@ -589,8 +591,8 @@ let declare_mutual_definition l = Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames; let gr = List.hd kns in let kn = match gr with ConstRef kn -> kn | _ -> assert false in - Lemmas.call_hook (fun exn -> exn) first.prg_hook local gr; - List.iter progmap_remove l; kn + Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx; + List.iter progmap_remove l; kn let shrink_body c = let ctx, b = decompose_lam c in @@ -642,7 +644,7 @@ let declare_obligation prg obl body ty uctx = else Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) } -let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls kind reduce hook = +let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook = let obls', b = match b with | None -> @@ -666,8 +668,8 @@ let init_prog_info ?(opaque = false) n b t ctx deps fixkind notations obls impls prg_obligations = (obls', Array.length obls'); prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ; prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; - prg_hook = hook; - prg_opaque = opaque; } + prg_hook = hook; prg_opaque = opaque; + prg_sign = sign } let map_cardinal m = let i = ref 0 in @@ -822,7 +824,9 @@ let obligation_hook prg obl num auto ctx' _ gr = if not (pi2 prg.prg_kind) (* Not polymorphic *) then (* The universe context was declared globally, we continue from the new global environment. *) - Evd.evar_universe_context (Evd.from_env (Global.env ())) + let evd = Evd.from_env (Global.env ()) in + let ctx' = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx')) in + Evd.evar_universe_context ctx' else ctx' in let prg = { prg with prg_ctx = ctx' } in @@ -853,9 +857,10 @@ let rec solve_obligation prg num tac = let obl = subst_deps_obl obls obl in let kind = kind_of_obligation (pi2 prg.prg_kind) obl.obl_status in let evd = Evd.from_ctx prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n tac oblset = auto_solve_obligations n ~oblset tac in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in - let () = Lemmas.start_proof_univs obl.obl_name kind evd obl.obl_type hook in + let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in let _ = Pfedit.by (snd (get_default_tactic ())) in @@ -889,17 +894,21 @@ and solve_obligation_by_tac prg obls i tac = | Some t -> t | None -> snd (get_default_tactic ()) in + let evd = Evd.from_ctx !prg.prg_ctx in + let evd = Evd.update_sigma_env evd (Global.env ()) in let t, ty, ctx = solve_by_tac obl.obl_name (evar_of_obligation obl) tac - (pi2 !prg.prg_kind) !prg.prg_ctx + (pi2 !prg.prg_kind) (Evd.evar_universe_context evd) in let uctx = Evd.evar_context_universe_context ctx in let () = prg := {!prg with prg_ctx = ctx} in let def, obl' = declare_obligation !prg obl t ty uctx in obls.(i) <- obl'; if def && not (pi2 !prg.prg_kind) then ( - (* Declare the term constraints with the first obligation only *) - let ctx' = Evd.evar_universe_context (Evd.from_env (Global.env ())) in + (* Declare the term constraints with the first obligation only *) + let evd = Evd.from_env (Global.env ()) in + let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in + let ctx' = Evd.evar_universe_context evd in prg := {!prg with prg_ctx = ctx'}); true else false @@ -987,9 +996,10 @@ let show_term n = ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body) let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic - ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) obls = + ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls = + let sign = Decls.initialize_named_context_for_proof () in let info = str (Id.to_string n) ++ str " has type-checked" in - let prg = init_prog_info ~opaque n term t ctx [] None [] obls implicits kind reduce hook in + let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose msg_info (info ++ str "."); @@ -1005,11 +1015,12 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) | _ -> res) let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce) - ?(hook=Lemmas.mk_hook (fun _ _ -> ())) ?(opaque = false) notations fixkind = + ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind = + let sign = Decls.initialize_named_context_for_proof () in let deps = List.map (fun (n, b, t, imps, obls) -> n) l in List.iter (fun (n, b, t, imps, obls) -> - let prg = init_prog_info ~opaque n (Some b) t ctx deps (Some fixkind) + let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind) notations obls imps kind reduce hook in progmap_add n (Ephemeron.create prg)) l; let _defined = -- cgit v1.2.3