aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/pretyping.ml48
-rw-r--r--pretyping/pretyping.mli7
-rw-r--r--proofs/pfedit.ml23
-rw-r--r--proofs/pfedit.mli9
-rw-r--r--tactics/evar_tactics.ml1
-rw-r--r--tactics/evar_tactics.mli4
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/tacinterp.ml63
-rw-r--r--tactics/tacinterp.mli3
-rw-r--r--toplevel/auto_ind_decl.ml6
10 files changed, 83 insertions, 83 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index afbfae3ba..69ee8d029 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -49,6 +49,7 @@ type var_map = (identifier * constr_under_binders) list
type unbound_ltac_var_map = (identifier * identifier option) list
type ltac_var_map = var_map * unbound_ltac_var_map
type glob_constr_ltac_closure = ltac_var_map * glob_constr
+type pure_open_constr = evar_map * constr
(************************************************************************)
(* This concerns Cases *)
@@ -101,6 +102,42 @@ let interp_elimination_sort = function
| GProp Pos -> InSet
| GType _ -> InType
+let resolve_evars env evdref fail_evar resolve_classes =
+ if resolve_classes then
+ evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
+ ~split:true ~fail:fail_evar env !evdref);
+ (* Resolve eagerly, potentially making wrong choices *)
+ evdref := (try consider_remaining_unif_problems
+ ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
+ with e -> if fail_evar then raise e else !evdref)
+
+let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
+ let evdref =
+ if use_classes then
+ ref (Typeclasses.resolve_typeclasses ~split:true ~fail:fail_evar env evd)
+ else
+ ref evd in
+ let rec proc_rec c =
+ let c = Reductionops.whd_evar !evdref c in
+ match kind_of_term c with
+ | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
+ let sigma = !evdref in
+ (try
+ let c = hook env sigma ev in
+ evdref := Evd.define evk c !evdref;
+ c
+ with Exit ->
+ if fail_evar then
+ let evi = Evd.find_undefined sigma evk in
+ let (loc,src) = evar_source evk !evdref in
+ Pretype_errors.error_unsolvable_implicit loc env sigma evi src None
+ else
+ c)
+ | _ -> map_constr proc_rec c in
+ let c = proc_rec c in
+ (* Side-effect *)
+ !evdref,c
+
module type S =
sig
@@ -134,7 +171,7 @@ sig
val understand_ltac :
bool -> evar_map -> env -> ltac_var_map ->
- typing_constraint -> glob_constr -> evar_map * constr
+ typing_constraint -> glob_constr -> pure_open_constr
(* Standard call to get a constr from a glob_constr, resolving implicit args *)
@@ -685,15 +722,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
error_unexpected_type_loc
(loc_of_glob_constr c) env !evdref tj.utj_val v
- let resolve_evars env evdref fail_evar resolve_classes =
- if resolve_classes then
- evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
- ~split:true ~fail:fail_evar env !evdref);
- (* Resolve eagerly, potentially making wrong choices *)
- evdref := (try consider_remaining_unif_problems
- ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
- with e -> if fail_evar then raise e else !evdref)
-
let pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c =
let c' = match kind with
| OfType exptyp ->
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e1f79f36c..47b3ec875 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -31,6 +31,7 @@ type var_map = (identifier * Pattern.constr_under_binders) list
type unbound_ltac_var_map = (identifier * identifier option) list
type ltac_var_map = var_map * unbound_ltac_var_map
type glob_constr_ltac_closure = ltac_var_map * glob_constr
+type pure_open_constr = evar_map * constr
module type S =
sig
@@ -65,7 +66,7 @@ sig
val understand_ltac :
bool -> evar_map -> env -> ltac_var_map ->
- typing_constraint -> glob_constr -> evar_map * constr
+ typing_constraint -> glob_constr -> pure_open_constr
(** Standard call to get a constr from a glob_constr, resolving implicit args *)
@@ -117,3 +118,7 @@ val constr_out : Dyn.t -> constr
val interp_sort : glob_sort -> sorts
val interp_elimination_sort : glob_sort -> sorts_family
+(** Last chance for solving evars, possibly using external solver *)
+val solve_remaining_evars : bool -> bool ->
+ (env -> evar_map -> existential -> constr) ->
+ env -> evar_map -> pure_open_constr -> pure_open_constr
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ad15ff903..2c85a26fe 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -165,7 +165,26 @@ let build_constant_by_tactic id sign typ tac =
delete_current_proof ();
raise e
-let build_by_tactic typ tac =
+let build_by_tactic env typ tac =
let id = id_of_string ("temporary_proof"^string_of_int (next())) in
- let sign = Decls.clear_proofs (Global.named_context ()) in
+ let sign = Decls.clear_proofs (named_context env) in
(build_constant_by_tactic id sign typ tac).const_entry_body
+
+(**********************************************************************)
+(* Support for resolution of evars in tactic interpretation, including
+ resolution by application of tactics *)
+
+let implicit_tactic = ref None
+
+let declare_implicit_tactic tac = implicit_tactic := Some tac
+
+let solve_by_implicit_tactic env sigma (evk,args) =
+ let evi = Evd.find_undefined sigma evk in
+ match (!implicit_tactic, snd (evar_source evk sigma)) with
+ | Some tac, (ImplicitArg _ | QuestionMark _)
+ when
+ Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
+ (Environ.named_context env) ->
+ (try build_by_tactic env evi.evar_concl (tclCOMPLETE tac)
+ with e when Logic.catchable_exception e -> raise Exit)
+ | _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2453cb39b..289e8c13c 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -177,4 +177,11 @@ val instantiate_nth_evar_com : int -> Topconstr.constr_expr -> unit
val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
Entries.definition_entry
-val build_by_tactic : types -> tactic -> constr
+val build_by_tactic : env -> types -> tactic -> constr
+
+(** Declare the default tactic to fill implicit arguments *)
+
+val declare_implicit_tactic : tactic -> unit
+
+(* Raise Exit if cannot solve *)
+val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 97177ba34..992fdc915 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -55,4 +55,3 @@ let let_evar name typ gls =
let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in
Refiner.tclTHEN (Refiner.tclEVARS sigma')
(Tactics.letin_tac None name evar None nowhere) gls
-
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 044ec3d3b..882cf3ce6 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -14,8 +14,4 @@ open Termops
val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
(identifier * hyp_location_flag, unit) location -> tactic
-(*i
-val instantiate_tac : tactic_arg list -> tactic
-i*)
-
val let_evar : name -> Term.types -> tactic
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 34cb5f771..e25e55135 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -497,7 +497,7 @@ END
VERNAC COMMAND EXTEND ImplicitTactic
| [ "Declare" "Implicit" "Tactic" tactic(tac) ] ->
- [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ]
+ [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ]
END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 07915be59..98a44c613 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -47,6 +47,7 @@ open Pretyping.Default
open Extrawit
open Pcoq
open Compat
+open Evd
let safe_msgnl s =
try msgnl s with e ->
@@ -1225,59 +1226,6 @@ let interp_fresh_id ist env l =
let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
-let implicit_tactic = ref None
-
-let declare_implicit_tactic tac = implicit_tactic := Some tac
-
-open Evd
-
-let solvable_by_tactic env evi (ev,args) src =
- match (!implicit_tactic, src) with
- | Some tac, (ImplicitArg _ | QuestionMark _)
- when
- Sign.named_context_equal (Environ.named_context_of_val evi.evar_hyps)
- (Environ.named_context env) ->
- let id = id_of_string "H" in
- start_proof id (Local,Proof Lemma) evi.evar_hyps evi.evar_concl
- (fun _ _ -> ());
- begin
- try
- by (tclCOMPLETE tac);
- let _,(const,_,_,_) = cook_proof ignore in
- delete_current_proof (); const.const_entry_body
- with e when Logic.catchable_exception e ->
- delete_current_proof();
- raise Exit
- end
- | _ -> raise Exit
-
-let solve_remaining_evars fail_evar use_classes env initial_sigma evd c =
- let evdref =
- if use_classes then
- ref (Typeclasses.resolve_typeclasses ~split:true ~fail:fail_evar env evd)
- else ref evd in
- let rec proc_rec c =
- let c = Reductionops.whd_evar !evdref c in
- match kind_of_term c with
- | Evar (evk,args as ev) when not (Evd.mem initial_sigma evk) ->
- let (loc,src) = evar_source evk !evdref in
- let sigma = !evdref in
- let evi = Evd.find_undefined sigma evk in
- (try
- let c = solvable_by_tactic env evi ev src in
- evdref := Evd.define evk c !evdref;
- c
- with Exit ->
- if fail_evar then
- Pretype_errors.error_unsolvable_implicit loc env sigma evi src None
- else
- c)
- | _ -> map_constr proc_rec c
- in
- let c = proc_rec c in
- (* Side-effect *)
- !evdref,c
-
let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma (c,ce) =
let (ltacvars,unbndltacvars as vars) = extract_ltac_constr_values ist env in
let c = match ce with
@@ -1290,13 +1238,14 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
intern_gen (kind = IsType) ~allow_patvar ~ltacvars:ltacdata sigma env c
in
let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
- let evd,c =
+ let evdc =
catch_error trace (understand_ltac expand_evar sigma env vars kind) c in
- let evd,c =
+ let (evd,c) =
if expand_evar then
- solve_remaining_evars fail_evar use_classes env sigma evd c
+ solve_remaining_evars fail_evar use_classes
+ solve_by_implicit_tactic env sigma evdc
else
- evd,c in
+ evdc in
db_constr ist.debug env c;
(evd,c)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index a9fc8fa14..96c6da91f 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -152,9 +152,6 @@ val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
val hide_interp : raw_tactic_expr -> tactic option -> tactic
-(** Declare the default tactic to fill implicit arguments *)
-val declare_implicit_tactic : tactic -> unit
-
(** Declare the xml printer *)
val declare_xml_printer :
(out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index ddf5abf03..0a866d3b7 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -581,7 +581,7 @@ let make_bl_scheme mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic
+ [|Pfedit.build_by_tactic (Global.env())
(compute_bl_goal ind lnamesparrec nparrec)
(compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|]
@@ -701,7 +701,7 @@ let make_lb_scheme mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic
+ [|Pfedit.build_by_tactic (Global.env())
(compute_lb_goal ind lnamesparrec nparrec)
(compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|]
@@ -868,7 +868,7 @@ let make_eq_decidability mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic
+ [|Pfedit.build_by_tactic (Global.env())
(compute_dec_goal ind lnamesparrec nparrec)
(compute_dec_tact ind lnamesparrec nparrec)|]
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 18:31:53 +0000