diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-04-01 19:19:22 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
commit | a2fce6d14d00a437466a1f7e3b53a77229f87980 (patch) | |
tree | 2e88133b978c67c222f0bfd7c13416609cdc84ac | |
parent | 4d7956a9b3f7f44aa9dae1bf22258b12dacab65f (diff) |
- Fix eq_constr_universes restricted to Sorts.equal
- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.
-rw-r--r-- | kernel/constr.ml | 2 | ||||
-rw-r--r-- | kernel/term_typing.ml | 6 | ||||
-rw-r--r-- | pretyping/evd.ml | 6 | ||||
-rw-r--r-- | pretyping/evd.mli | 1 | ||||
-rw-r--r-- | pretyping/unification.ml | 1 | ||||
-rw-r--r-- | proofs/pfedit.ml | 9 | ||||
-rw-r--r-- | proofs/pfedit.mli | 4 | ||||
-rw-r--r-- | proofs/proof_global.ml | 34 | ||||
-rw-r--r-- | proofs/proofview.ml | 2 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
-rw-r--r-- | tactics/tactics.ml | 25 | ||||
-rw-r--r-- | toplevel/obligations.ml | 4 |
12 files changed, 63 insertions, 37 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml index 4f2935be5..13e1abacc 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -471,7 +471,7 @@ let compare_head_gen eq_universes eq_sorts f t1 t2 = | Rel n1, Rel n2 -> Int.equal n1 n2 | Meta m1, Meta m2 -> Int.equal m1 m2 | Var id1, Var id2 -> Id.equal id1 id2 - | Sort s1, Sort s2 -> Sorts.equal s1 s2 + | Sort s1, Sort s2 -> eq_sorts s1 s2 | Cast (c1,_,_), _ -> f c1 t2 | _, Cast (c2,_,_) -> f t1 c2 | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0959fa703..8c4ec8cbf 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -146,7 +146,7 @@ let infer_declaration env kn dcl = let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let env = push_context_set ctx env in + assert(Univ.ContextSet.is_empty ctx); let body = handle_side_effects env body side_eff in let def, typ, proj = match c.const_entry_proj with @@ -172,9 +172,7 @@ let infer_declaration env kn dcl = let def = Def (Mod_subst.from_val j.uj_val) in def, typ, None in - let univs = Univ.UContext.union c.const_entry_universes - (Univ.ContextSet.to_context ctx) - in + let univs = c.const_entry_universes in feedback_completion_typecheck feedback_id; def, typ, proj, c.const_entry_polymorphic, univs, c.const_entry_inline_code, c.const_entry_secctx diff --git a/pretyping/evd.ml b/pretyping/evd.ml index eda5f66c1..d18568500 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -932,6 +932,12 @@ let merge_uctx rigid uctx ctx' = let merge_context_set rigid evd ctx' = {evd with universes = merge_uctx rigid evd.universes ctx'} +let merge_uctx_subst uctx s = + { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } + +let merge_universe_subst evd subst = + {evd with universes = merge_uctx_subst evd.universes subst } + let with_context_set rigid d (a, ctx) = (merge_context_set rigid d ctx, a) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 9be18bc8a..5cc554c26 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -469,6 +469,7 @@ val universes : evar_map -> Univ.universes val merge_universe_context : evar_map -> evar_universe_context -> evar_map val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map +val merge_universe_subst : evar_map -> Universes.universe_opt_subst -> evar_map val with_context_set : rigid -> evar_map -> 'a Univ.in_universe_context_set -> evar_map * 'a diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9e662150e..0ab886ca3 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -384,6 +384,7 @@ let is_rigid_head flags t = match kind_of_term t with | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta)) | Ind (i,u) -> true + | Fix _ | CoFix _ -> true | _ -> false let force_eqs c = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index eeb577025..077057f3c 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -119,13 +119,12 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac = - let substref = ref Univ.LMap.empty in (** FIXME: Something wrong here with subst *) start_proof id goal_kind sign typ (fun _ -> ()); try let status = by tac in - let _,(const,_,_) = cook_proof () in + let _,(const,univs,_) = cook_proof () in delete_current_proof (); - const, status, !substref + const, status, univs with reraise -> let reraise = Errors.push reraise in delete_current_proof (); @@ -135,11 +134,11 @@ let build_by_tactic env ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in - let ce, status, subst = build_constant_by_tactic id sign ~goal_kind:gk typ tac in + let ce, status, univs = build_constant_by_tactic id sign ~goal_kind:gk typ tac in let ce = Term_typing.handle_side_effects env ce in let cb, se = Future.force ce.const_entry_body in assert(Declareops.side_effects_is_empty se); - cb, status, subst + cb, status, fst univs (**********************************************************************) (* Support for resolution of evars in tactic interpretation, including diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index e3df619f8..615866c6a 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -149,7 +149,9 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> named_context_val -> ?goal_kind:goal_kind -> - types Univ.in_universe_context_set -> unit Proofview.tactic -> Entries.definition_entry * bool * Universes.universe_opt_subst + types Univ.in_universe_context_set -> unit Proofview.tactic -> + Entries.definition_entry * bool * Universes.universe_opt_subst Univ.in_universe_context + val build_by_tactic : env -> ?poly:polymorphic -> types Univ.in_universe_context_set -> unit Proofview.tactic -> constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 12700851a..e49a57af3 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -264,16 +264,12 @@ let get_open_goals () = (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + List.length shelf -let nf_body nf b = - let aux ((c, ctx), t) = ((nf c, ctx), t) in - Future.chain ~pure:true b aux - let close_proof ?feedback_id ~now fpl = let { pid; section_vars; strength; proof; terminator } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let fpl, univs = Future.split2 fpl in - let (subst, univs as univsubst), nf = + let univsubst, make_body = if poly || now then let usubst, uctx = Future.force univs in let ctx, subst = @@ -286,29 +282,43 @@ let close_proof ?feedback_id ~now fpl = let subst = Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst) in - (subst, Univ.ContextSet.to_context ctx), nf + let univsubst = (subst, Univ.ContextSet.to_context ctx) in + let make_body p _c t _octx = + let (c, ctx), eff = Future.force p in + let body = nf c and typ = nf t in + let used_univs = + Univ.LSet.union (Universes.universes_of_constr body) + (Universes.universes_of_constr typ) + in + let ctx = Universes.restrict_universe_context ctx used_univs in + let p = Future.from_val ((body, Univ.ContextSet.empty),eff) in + let univs = Univ.ContextSet.to_context ctx in + univs, p, typ + in univsubst, make_body else let ctx = List.fold_left (fun acc (c, (t, octx)) -> Univ.ContextSet.union octx acc) Univ.ContextSet.empty initial_goals in - (Univ.LMap.empty, Univ.ContextSet.to_context ctx), (fun x -> x) + let univs = Univ.ContextSet.to_context ctx in + let univsubst = (Univ.LMap.empty, univs) in + univsubst, (fun p c t octx -> univs, p, t) in let entries = - Future.map2 (fun p (c, (t, octx)) -> { Entries. - const_entry_body = nf_body nf p; + Future.map2 (fun p (c, (t, octx)) -> + let univs, body, typ = make_body p c t octx in + { Entries. + const_entry_body = body; const_entry_secctx = section_vars; const_entry_feedback = feedback_id; - const_entry_type = Some (nf t); + const_entry_type = Some typ; const_entry_inline_code = false; const_entry_opaque = true; const_entry_universes = univs; const_entry_polymorphic = poly; const_entry_proj = None}) fpl initial_goals in - if now then - List.iter (fun x ->ignore(Future.force x.Entries.const_entry_body)) entries; { id = pid; entries = entries; persistence = strength; universes = univsubst }, Ephemeron.get terminator diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 291da4a98..83a703a3a 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -838,6 +838,8 @@ struct let new_evar (evd, evs) env typ = let src = (Loc.ghost, Evar_kinds.GoalEvar) in let (evd, ev) = Evarutil.new_evar evd env ~src typ in + let evd = Typeclasses.mark_unresolvables + ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in let (evk, _) = Term.destEvar ev in let h = (evd, build_goal evk :: evs) in (h, ev) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f32c06ba4..a4d840cf0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1807,14 +1807,16 @@ and interp_atomic ist tac = extend_gl_hyps) is incorrect. This means that evar instantiated by pf_interp_constr may be lost, there. *) let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in - let (_,c_interp) = + let (sigma',c_interp) = try pf_interp_constr ist (extend_gl_hyps gl sign) c with e when to_catch e (* Hack *) -> errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") in tclTHEN (tclEVARS sigma) - (Tactics.change (Some op) c_interp (interp_clause ist env cl)) + (tclTHEN (* At least recover the declared universes *) + (tclPUSHEVARUNIVCONTEXT (Evd.evar_universe_context sigma')) + (Tactics.change (Some op) c_interp (interp_clause ist env cl))) gl end end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 024165fd0..0fbb511a7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3720,7 +3720,7 @@ let interpretable_as_section_decl d1 d2 = match d2,d1 with | (_,Some b1,t1), (_,Some b2,t2) -> eq_constr b1 b2 && eq_constr t1 t2 | (_,None,t1), (_,_,t2) -> eq_constr t1 t2 -let abstract_subproof id tac = +let abstract_subproof id gk tac = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -3749,8 +3749,8 @@ let abstract_subproof id tac = evd, ctx, nf concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in - let (const, safe, subst) = - try Pfedit.build_constant_by_tactic id secsign (concl, ctx) solve_tac + let (const, safe, (subst, ctx)) = + try Pfedit.build_constant_by_tactic ~goal_kind:gk id secsign (concl, ctx) solve_tac with Proof_errors.TacticFailure e as src -> (* if the tactic [tac] fails, it reports a [TacticFailure e], which is an error irrelevant to the proof system (in fact it @@ -3766,7 +3766,8 @@ let abstract_subproof id tac = let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in - let evd = Evd.merge_context_set Evd.univ_flexible evd (Univ.ContextSet.of_context ctx) in + let evd = Evd.merge_context_set Evd.univ_rigid evd (Univ.ContextSet.of_context ctx) in + let evd = Evd.merge_universe_subst evd subst in let open Declareops in let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in let effs = cons_side_effects eff no_seff in @@ -3780,14 +3781,18 @@ let anon_id = Id.of_string "anonymous" let tclABSTRACT name_op tac = let open Proof_global in - let s = match name_op with - | Some s -> s + let default_gk = (Global, false, Proof Theorem) in + let s, gk = match name_op with + | Some s -> + (try let _, gk, _ = current_proof_statement () in s, gk + with NoCurrentProof -> s, default_gk) | None -> - let name = try get_current_proof_name () with NoCurrentProof -> anon_id in - add_suffix name "_subproof" + let name, gk = + try let name, gk, _ = current_proof_statement () in name, gk + with NoCurrentProof -> anon_id, default_gk in + add_suffix name "_subproof", gk in - abstract_subproof s tac - + abstract_subproof s gk tac let admit_as_an_axiom = Proofview.tclUNIT () >>= fun () -> (* delay for Coqlib.build_coq_proof_admitted *) diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index d45c2af3e..cce5242ec 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -791,8 +791,8 @@ let rec string_of_list sep f = function let solve_by_tac name evi t poly subst ctx = let id = name in let concl = Universes.subst_opt_univs_constr subst evi.evar_concl in - (* spiwack: the status is dropped *) - let (entry,_,subst) = Pfedit.build_constant_by_tactic + (* spiwack: the status is dropped. MS: the ctx is dropped too *) + let (entry,_,(subst,ctx)) = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) evi.evar_hyps (concl, ctx) (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Term_typing.handle_side_effects env entry in |