diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:01:48 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 18:21:25 +0100 |
commit | 3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch) | |
tree | 45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /proofs | |
parent | cca57bcd89770e76e1bcc21eb41756dca2c51425 (diff) | |
parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) |
Merge branch 'master'.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
-rw-r--r-- | proofs/pfedit.ml | 16 | ||||
-rw-r--r-- | proofs/proof.ml | 16 | ||||
-rw-r--r-- | proofs/proof.mli | 2 | ||||
-rw-r--r-- | proofs/proof_global.ml | 2 | ||||
-rw-r--r-- | proofs/refine.ml | 11 | ||||
-rw-r--r-- | proofs/refine.mli | 5 | ||||
-rw-r--r-- | proofs/tacmach.ml | 3 | ||||
-rw-r--r-- | proofs/tacmach.mli | 9 |
9 files changed, 64 insertions, 2 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 59a41792a..8367c09b8 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -48,7 +48,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let sigma',typed_c = let flags = { Pretyping.use_typeclasses = true; - Pretyping.use_unif_heuristics = true; + Pretyping.solve_unification_constraints = true; Pretyping.use_hook = None; Pretyping.fail_evar = false; Pretyping.expand_evars = true } in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 09b924c7e..d9a68acb8 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -13,6 +13,17 @@ open Entries open Environ open Evd +let use_unification_heuristics_ref = ref true +let _ = Goptions.declare_bool_option { + Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optname = "Solve unification constraints at every \".\""; + Goptions.optkey = ["Solve";"Unification";"Constraints"]; + Goptions.optread = (fun () -> !use_unification_heuristics_ref); + Goptions.optwrite = (fun a -> use_unification_heuristics_ref:=a); +} + +let use_unification_heuristics () = !use_unification_heuristics_ref + let refining = Proof_global.there_are_pending_proofs let check_no_pending_proofs = Proof_global.check_no_pending_proof @@ -119,6 +130,11 @@ let solve ?with_end_tac gi info_lvl tac pr = | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac | Vernacexpr.SelectAll -> tac in + let tac = + if use_unification_heuristics () then + Proofview.tclTHEN tac Refine.solve_constraints + else tac + in let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac pr in let () = match info_lvl with diff --git a/proofs/proof.ml b/proofs/proof.ml index 0a3b08c04..b2103489a 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -372,6 +372,22 @@ let in_proof p k = k (Proofview.return p.proofview) let unshelve p = { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } +let pr_proof p = + let p = map_structured_proof p (fun _sigma g -> g) in + Pp.( + let pr_goal_list = prlist_with_sep spc Goal.pr_goal in + let rec aux acc = function + | [] -> acc + | (before,after)::stack -> + aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ + pr_goal_list after) stack in + str "[" ++ str "focus structure: " ++ + aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++ + str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++ + str "given up: " ++ pr_goal_list p.given_up_goals ++ + str "]" + ) + (*** Compatibility layer with <=v8.2 ***) module V82 = struct let subgoals p = diff --git a/proofs/proof.mli b/proofs/proof.mli index 8dcc5b76e..9d38e16ad 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -182,6 +182,8 @@ val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a focused goals. *) val unshelve : proof -> proof +val pr_proof : proof -> Pp.std_ppcmds + (*** Compatibility layer with <=v8.2 ***) module V82 : sig val subgoals : proof -> Goal.goal list Evd.sigma diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index eb1bea897..0eff0e6b4 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -623,7 +623,7 @@ module Bullet = struct let _ = register_behavior strict end - (* Current bullet behavior, controled by the option *) + (* Current bullet behavior, controlled by the option *) let current_behavior = ref Strict.strict let _ = diff --git a/proofs/refine.ml b/proofs/refine.ml index c36bb143e..1ee6e0ca5 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -152,3 +152,14 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl -> } in refine ?unsafe f end } + +(** {7 solve_constraints} + + Ensure no remaining unification problems are left. Run at every "." by default. *) + +let solve_constraints = + let open Proofview in + tclENV >>= fun env -> tclEVARMAP >>= fun sigma -> + try let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + Unsafe.tclEVARSADVANCE sigma + with e -> tclZERO e diff --git a/proofs/refine.mli b/proofs/refine.mli index 205b97974..1a254d578 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -43,3 +43,8 @@ val with_type : Environ.env -> Evd.evar_map -> val refine_casted : ?unsafe:bool -> EConstr.t Sigma.run -> unit tactic (** Like {!refine} except the refined term is coerced to the conclusion of the current goal. *) + +(** {7 Unification constraint handling} *) + +val solve_constraints : unit tactic +(** Solve any remaining unification problems, applying heuristics. *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 97c5cda77..b55f8ef11 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -179,6 +179,9 @@ module New = struct let pf_unsafe_type_of gl t = pf_apply unsafe_type_of gl t + let pf_get_type_of gl t = + pf_apply (Retyping.get_type_of ~lax:true) gl t + let pf_type_of gl t = pf_apply type_of gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 1992cec65..1b05bc7d6 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -109,7 +109,16 @@ module New : sig val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env val pf_concl : ('a, 'r) Proofview.Goal.t -> types + (** WRONG: To be avoided at all costs, it typechecks the term entirely but + forgets the universe constraints necessary to retypecheck it *) val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types + + (** This function does no type inference and expects an already well-typed term. + It recomputes its type in the fastest way possible (no conversion is ever involved) *) + val pf_get_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types + + (** This function entirely type-checks the term and computes its type + and the implied universe constraints. *) val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool |