From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 4 Jul 2009 13:28:35 +0200 Subject: Imported Upstream version 8.2.pl1+dfsg --- tactics/auto.ml | 101 ++++++++++++++++++++++++-------------------- tactics/auto.mli | 3 +- tactics/class_tactics.ml4 | 17 +++----- tactics/decl_proof_instr.ml | 4 +- tactics/equality.ml | 4 +- tactics/evar_tactics.ml | 8 ++-- tactics/evar_tactics.mli | 4 +- tactics/extraargs.ml4 | 6 +-- tactics/extraargs.mli | 4 +- tactics/hiddentac.ml | 6 +-- tactics/hiddentac.mli | 4 +- tactics/refine.ml | 27 +++++++----- tactics/tacinterp.ml | 46 +++++++++++++------- tactics/tacinterp.mli | 5 ++- tactics/tacticals.ml | 3 +- tactics/tactics.ml | 72 +++++++++++++++++++------------ 16 files changed, 181 insertions(+), 133 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 1212656b..36136a6c 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 11739 2009-01-02 19:33:19Z herbelin $ *) +(* $Id: auto.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Pp open Util @@ -150,10 +150,13 @@ module Hint_db = struct try Constr_map.find key db.hintdb_map with Not_found -> empty_se + let map_none db = + Sort.merge pri_order db.hintdb_nopat [] + let map_all k db = let (l,l',_) = find k db in Sort.merge pri_order (db.hintdb_nopat @ l) l' - + let map_auto (k,c) db = let st = if db.use_dn then Some db.hintdb_state else None in let l' = lookup_tacs (k,c) st (find k db) in @@ -637,26 +640,24 @@ let print_hint_ref ref = ppnl(pr_hint_ref ref) let pr_hint_term cl = try - let (hdc,args) = head_constr_bound cl in - let hd = head_of_constr_reference hdc in let dbs = Hintdbmap.to_list !searchtable in let valid_dbs = - if occur_existential cl then - map_succeed - (fun (name, db) -> (name, db, Hint_db.map_all hd db)) - dbs - else - map_succeed - (fun (name, db) -> - (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) - dbs - in - if valid_dbs = [] then - (str "No hint applicable for current goal") - else - (str "Applicable Hints :" ++ fnl () ++ - hov 0 (prlist pr_hints_db valid_dbs)) - with Bound | Match_failure _ | Failure _ -> + let fn = try + let (hdc,args) = head_constr_bound cl in + let hd = head_of_constr_reference hdc in + if occur_existential cl then + Hint_db.map_all hd + else Hint_db.map_auto (hd, applist (hdc,args)) + with Bound -> Hint_db.map_none + in + map_succeed (fun (name, db) -> (name, db, fn db)) dbs + in + if valid_dbs = [] then + (str "No hint applicable for current goal") + else + (str "Applicable Hints :" ++ fnl () ++ + hov 0 (prlist pr_hints_db valid_dbs)) + with Match_failure _ | Failure _ -> (str "No hint applicable for current goal") let error_no_such_hint_database x = @@ -795,6 +796,13 @@ let flags_of_state st = {auto_unif_flags with modulo_conv_on_closed_terms = Some st; modulo_delta = st} +let hintmap_of hdc concl = + match hdc with + | None -> Hint_db.map_none + | Some hdc -> + if occur_existential concl then Hint_db.map_all hdc + else Hint_db.map_auto (hdc,concl) + let rec trivial_fail_db mod_delta db_list local_db gl = let intro_tac = tclTHEN intro @@ -808,12 +816,8 @@ let rec trivial_fail_db mod_delta db_list local_db gl = (trivial_resolve mod_delta db_list local_db (pf_concl gl)))) gl and my_find_search_nodelta db_list local_db hdc concl = - if occur_existential concl then - List.map (fun hint -> (None,hint)) - (list_map_append (Hint_db.map_all hdc) (local_db::db_list)) - else - List.map (fun hint -> (None,hint)) - (list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list)) + List.map (fun hint -> (None,hint)) + (list_map_append (hintmap_of hdc concl) (local_db::db_list)) and my_find_search mod_delta = if mod_delta then my_find_search_delta @@ -821,28 +825,31 @@ and my_find_search mod_delta = and my_find_search_delta db_list local_db hdc concl = let flags = {auto_unif_flags with use_metas_eagerly = true} in + let f = hintmap_of hdc concl in if occur_existential concl then list_map_append (fun db -> if Hint_db.use_dn db then let flags = flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db) + List.map (fun x -> (Some flags,x)) (f db) else let flags = {flags with modulo_delta = Hint_db.transparent_state db} in - List.map (fun x -> (Some flags,x)) (Hint_db.map_all hdc db)) + List.map (fun x -> (Some flags,x)) (f db)) (local_db::db_list) else list_map_append (fun db -> if Hint_db.use_dn db then let flags = flags_of_state (Hint_db.transparent_state db) in - List.map (fun x -> (Some flags, x)) (Hint_db.map_auto (hdc,concl) db) + List.map (fun x -> (Some flags, x)) (f db) else let (ids, csts as st) = Hint_db.transparent_state db in let flags, l = let l = - if (Idpred.is_empty ids && Cpred.is_empty csts) - then Hint_db.map_auto (hdc,concl) db - else Hint_db.map_all hdc db + match hdc with None -> Hint_db.map_none db + | Some hdc -> + if (Idpred.is_empty ids && Cpred.is_empty csts) + then Hint_db.map_auto (hdc,concl) db + else Hint_db.map_all hdc db in {flags with modulo_delta = st}, l in List.map (fun x -> (Some flags,x)) l) (local_db::db_list) @@ -861,13 +868,15 @@ and tac_of_hint db_list local_db concl (flags, {pat=p; code=t}) = and trivial_resolve mod_delta db_list local_db cl = try - let hdconstr,_ = head_constr_bound cl in - List.map (tac_of_hint db_list local_db cl) - (priority - (my_find_search mod_delta db_list local_db - (head_of_constr_reference hdconstr) cl)) - with Bound | Not_found -> - [] + let head = + try let hdconstr,_ = head_constr_bound cl in + Some (head_of_constr_reference hdconstr) + with Bound -> None + in + List.map (tac_of_hint db_list local_db cl) + (priority + (my_find_search mod_delta db_list local_db head cl)) + with Not_found -> [] let trivial lems dbnames gl = let db_list = @@ -903,12 +912,14 @@ let h_trivial lems l = let possible_resolve mod_delta db_list local_db cl = try - let hdconstr,_ = head_constr_bound cl in - List.map (tac_of_hint db_list local_db cl) - (my_find_search mod_delta db_list local_db - (head_of_constr_reference hdconstr) cl) - with Bound | Not_found -> - [] + let head = + try let hdconstr,_ = head_constr_bound cl in + Some (head_of_constr_reference hdconstr) + with Bound -> None + in + List.map (tac_of_hint db_list local_db cl) + (my_find_search mod_delta db_list local_db head cl) + with Not_found -> [] let decomp_unary_term_then (id,_,typc) kont1 kont2 gl = try diff --git a/tactics/auto.mli b/tactics/auto.mli index c9065ef3..132b9063 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto.mli 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id: auto.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) (*i*) open Util @@ -53,6 +53,7 @@ module Hint_db : type t val empty : transparent_state -> bool -> t val find : global_reference -> t -> search_entry + val map_none : t -> pri_auto_tactic list val map_all : global_reference -> t -> pri_auto_tactic list val map_auto : global_reference * constr -> t -> pri_auto_tactic list val add_one : hint_entry -> t -> t diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 6a425984..b7eb3620 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: class_tactics.ml4 12189 2009-06-15 05:08:44Z msozeau $ *) open Pp open Util @@ -46,18 +46,18 @@ let typeclasses_db = "typeclass_instances" let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db full_transparent_state true) -let check_imported_library d = +let check_required_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in if not (Library.library_is_loaded dir) then - error ("Library "^(list_last d)^" has to be imported first.") + error ("Library "^(list_last d)^" has to be required first.") let classes_dirpath = make_dirpath (List.map id_of_string ["Classes";"Coq"]) let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () - else check_imported_library ["Coq";"Setoids";"Setoid"] + else check_required_library ["Coq";"Setoids";"Setoid"] (** Typeclasses instance search tactic / eauto *) @@ -245,7 +245,6 @@ module SearchProblem = struct Option.iter (fun r -> (* msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *) r := true) do_cut; - let sigma = Evarutil.nf_evars sigma in let gl = List.map (Evarutil.nf_evar_info sigma) gl in let nbgl = List.length gl in (* let gl' = { it = gl ; sigma = sigma } in *) @@ -338,6 +337,7 @@ let is_transparent_gr (ids, csts) = function | IndRef _ | ConstructRef _ -> false let make_resolve_hyp env sigma st flags pri (id, _, cty) = + let cty = Evarutil.nf_evar sigma cty in let ctx, ar = decompose_prod cty in let keep = match kind_of_term (fst (decompose_app ar)) with @@ -625,9 +625,6 @@ let is_applied_setoid_relation t = let _ = Equality.register_is_applied_setoid_relation is_applied_setoid_relation -exception Found of (constr * constr * (types * types) list * constr * constr array * - (constr * (constr * constr * constr * constr)) option array) - let split_head = function hd :: tl -> hd, tl | [] -> assert(false) @@ -1675,7 +1672,7 @@ let typeclass_app_constrexpr t ?(bindings=NoBindings) gl = let bindings = Tacinterp.interp_bindings my_ist gl bl in typeclass_app (Evd.evars_of !evars) gl ~bindings:bindings j.uj_val j.uj_type -let typeclass_app_raw t gl = +let typeclass_app_raw (_,t) gl = let env = pf_env gl in let evars = ref (create_evar_defs (project gl)) in let j = Pretyping.Default.understand_judgment_tcc evars env t in @@ -1715,7 +1712,7 @@ END let not_declared env ty rel = tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ - str ty ++ str" relation. Maybe you need to import the Setoid library") + str ty ++ str" relation. Maybe you need to require the Setoid library") let relation_of_constr env c = match kind_of_term c with diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 2d0395a3..62a8ddfc 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: decl_proof_instr.ml 12135 2009-05-20 14:49:23Z herbelin $ *) open Util open Pp @@ -174,7 +174,7 @@ let mark_proof_tree_as_done pt = let mark_as_done pts = map_pftreestate (fun _ -> mark_proof_tree_as_done) - (traverse 0 pts) + (up_to_matching_rule is_focussing_command pts) (* post-instruction focus management *) diff --git a/tactics/equality.ml b/tactics/equality.ml index baebee07..58a00419 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *) open Pp open Util @@ -1215,7 +1215,7 @@ let subst_one x gl = tclMAP introtac depdecls]) @ [tclTRY (clear [x;hyp])]) gl -let subst = tclMAP subst_one +let subst ids = tclTHEN tclNORMEVAR (tclMAP subst_one ids) let subst_all gl = let test (_,c) = diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 43c18a8b..67b89888 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evar_tactics.ml 11576 2008-11-10 19:13:15Z msozeau $ *) +(* $Id: evar_tactics.ml 12102 2009-04-24 10:48:11Z herbelin $ *) open Term open Util @@ -29,7 +29,7 @@ let evar_list evc c = in evrec [] c -let instantiate n rawc ido gl = +let instantiate n (ist,rawc) ido gl = let sigma = gl.sigma in let evl = match ido with @@ -52,7 +52,9 @@ let instantiate n rawc ido gl = error "not enough uninstantiated existential variables"; if n <= 0 then error "Incorrect existential variable index."; let ev,_ = destEvar (List.nth evl (n-1)) in - let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in + let env = Evd.evar_env (Evd.find sigma ev) in + let ltac_vars = Tacinterp.extract_ltac_vars ist sigma env in + let evd' = w_refine ev (ltac_vars,rawc) (create_goal_evar_defs sigma) in tclTHEN (tclEVARS (evars_of evd')) tclNORMEVAR diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index cc06d2c6..f577b338 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evar_tactics.mli 11512 2008-10-27 12:28:36Z herbelin $ i*) +(*i $Id: evar_tactics.mli 12102 2009-04-24 10:48:11Z herbelin $ i*) open Tacmach open Names open Tacexpr open Termops -val instantiate : int -> Rawterm.rawconstr -> +val instantiate : int -> Tacinterp.interp_sign * Rawterm.rawconstr -> (identifier * hyp_location_flag, unit) location -> tactic (*i diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 694c3495..5eb333a0 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extraargs.ml4 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: extraargs.ml4 12102 2009-04-24 10:48:11Z herbelin $ *) open Pp open Pcoq @@ -100,9 +100,9 @@ END let pr_gen prc _prlc _prtac c = prc c -let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw +let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw -let interp_raw _ _ (t,_) = t +let interp_raw ist gl (t,_) = (ist,t) let glob_raw = Tacinterp.intern_constr diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index bccb150f..b64adf24 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraargs.mli 11800 2009-01-18 18:34:15Z msozeau $ i*) +(*i $Id: extraargs.mli 12102 2009-04-24 10:48:11Z herbelin $ i*) open Tacexpr open Term @@ -25,7 +25,7 @@ val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type val rawwit_raw : constr_expr raw_abstract_argument_type -val wit_raw : rawconstr typed_abstract_argument_type +val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type val raw : constr_expr Pcoq.Gram.Entry.e type 'id gen_place= ('id * hyp_location_flag,unit) location diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index b270ba2d..8e517453 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hiddentac.ml 11671 2008-12-12 12:43:03Z herbelin $ *) +(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *) open Term open Proof_type @@ -75,10 +75,6 @@ let h_generalize_dep c = let h_let_tac b na c cl = let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl) -let h_instantiate n c ido = -(Evar_tactics.instantiate n c ido) - (* abstract_tactic (TacInstantiate (n,c,cls)) - (Evar_refiner.instantiate n c (simple_clause_of cls)) *) (* Derived basic tactics *) let h_simple_induction_destruct isrec h = diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 0ebb024a..9270411a 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hiddentac.mli 11671 2008-12-12 12:43:03Z herbelin $ i*) +(*i $Id: hiddentac.mli 12102 2009-04-24 10:48:11Z herbelin $ i*) (*i*) open Names @@ -62,8 +62,6 @@ val h_generalize_gen : (constr with_occurrences * name) list -> tactic val h_generalize_dep : constr -> tactic val h_let_tac : letin_flag -> name -> constr -> Tacticals.clause -> tactic -val h_instantiate : int -> Rawterm.rawconstr -> - (identifier * hyp_location_flag, unit) location -> tactic (* Derived basic tactics *) diff --git a/tactics/refine.ml b/tactics/refine.ml index dff3b003..322d25e5 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refine.ml 11671 2008-12-12 12:43:03Z herbelin $ *) +(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *) (* JCF -- 6 janvier 1998 EXPERIMENTAL *) @@ -327,29 +327,31 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = gl (* fix => tactique Fix *) - | Fix ((ni,_),(fi,ai,_)) , _ -> + | Fix ((ni,j),(fi,ai,_)) , _ -> let out_name = function | Name id -> id | _ -> error "Recursive functions must have names." in let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in + let firsts,lasts = list_chop j (Array.to_list fixes) in tclTHENS - (mutual_fix (out_name fi.(0)) (succ ni.(0)) - (List.tl (Array.to_list fixes))) + (mutual_fix_with_index + (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j) (List.map (function | None -> tclIDTAC | Some th -> tcc_aux subst th) sgp) gl (* cofix => tactique CoFix *) - | CoFix (_,(fi,ai,_)) , _ -> + | CoFix (j,(fi,ai,_)) , _ -> let out_name = function | Name id -> id | _ -> error "Recursive functions must have names." in let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in + let firsts,lasts = list_chop j (Array.to_list cofixes) in tclTHENS - (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes))) + (mutual_cofix_with_index (out_name fi.(j)) (firsts@List.tl lasts) j) (List.map (function | None -> tclIDTAC | Some th -> tcc_aux subst th) sgp) @@ -366,10 +368,15 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = (* Et finalement la tactique refine elle-même : *) -let refine oc gl = +let refine (evd,c) gl = let sigma = project gl in - let (sigma,c) = Evarutil.evars_to_metas sigma oc in + let evd = Evd.evars_of (Typeclasses.resolve_typeclasses + ~onlyargs:true ~fail:false (pf_env gl) + (Evd.create_evar_defs evd)) + in + let c = Evarutil.nf_evar evd c in + let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise complicated to update meta types when passing through a binder *) - let th = compute_metamap (pf_env gl) sigma c in - tclTHEN (Refiner.tclEVARS sigma) (tcc_aux [] th) gl + let th = compute_metamap (pf_env gl) evd c in + tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d9026a6d..71b50b66 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 11745 2009-01-04 18:43:08Z herbelin $ *) +(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Constrintern open Closure @@ -539,7 +539,9 @@ let intern_induction_arg ist = function | ElimOnIdent (loc,id) -> if !strict_check then (* If in a defined tactic, no intros-until *) - ElimOnConstr (intern_constr ist (CRef (Ident (dloc,id))),NoBindings) + match intern_constr ist (CRef (Ident (dloc,id))) with + | RVar (loc,id),_ -> ElimOnIdent (loc,id) + | c -> ElimOnConstr (c,NoBindings) else ElimOnIdent (loc,id) @@ -1396,6 +1398,14 @@ let retype_list sigma env lst = try (x,Retyping.get_judgment_of env sigma csr)::a with | Anomaly _ -> a) lst [] +let extract_ltac_vars_data ist sigma env = + let (ltacvars,_ as vars) = constr_list ist env in + vars, retype_list sigma env ltacvars + +let extract_ltac_vars ist sigma env = + let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in + typs,unbndltacvars + let implicit_tactic = ref None let declare_implicit_tactic tac = implicit_tactic := Some tac @@ -1441,8 +1451,8 @@ let solve_remaining_evars env initial_sigma evd c = proc_rec (Evarutil.nf_isevar !evdref c) let interp_gen kind ist sigma env (c,ce) = - let (ltacvars,unbndltacvars as vars) = constr_list ist env in - let typs = retype_list sigma env ltacvars in + let (ltacvars,unbndltacvars as vars),typs = + extract_ltac_vars_data ist sigma env in let c = match ce with | None -> c (* If at toplevel (ce<>None), the error can be due to an incorrect @@ -1717,10 +1727,20 @@ let interp_induction_arg ist gl = function | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c) | ElimOnAnonHyp n as x -> x | ElimOnIdent (loc,id) -> - if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr - (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))), - NoBindings) + try + match List.assoc id ist.lfun with + | VInteger n -> ElimOnAnonHyp n + | VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id) + | VConstr c -> ElimOnConstr (c,NoBindings) + | _ -> user_err_loc (loc,"", + strbrk "Cannot coerce " ++ pr_id id ++ + strbrk " neither to a quantified hypothesis nor to a term.") + with Not_found -> + (* Interactive mode *) + if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) + else ElimOnConstr + (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))), + NoBindings) let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c) let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c)) @@ -2735,6 +2755,7 @@ let bad_tactic_args s = (* Declaration of the TAC-DEFINITION object *) let add (kn,td) = mactab := Gmap.add kn td !mactab +let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab) type tacdef_kind = | NewTac of identifier | UpdateTac of ltac_constant @@ -2749,9 +2770,7 @@ let load_md i ((sp,kn),defs) = let kn = Names.make_kn mp dir (label_of_id id) in Nametab.push_tactic (Until i) sp kn; add (kn,t) - | UpdateTac kn -> - mactab := Gmap.remove kn !mactab; - add (kn,t)) defs + | UpdateTac kn -> replace (kn,t)) defs let open_md i((sp,kn),defs) = let dp,_ = repr_path sp in @@ -2762,10 +2781,7 @@ let open_md i((sp,kn),defs) = let sp = Libnames.make_path dp id in let kn = Names.make_kn mp dir (label_of_id id) in Nametab.push_tactic (Exactly i) sp kn - | UpdateTac kn -> - let (path, id) = decode_kn kn in - let sp = Libnames.make_path path id in - Nametab.push_tactic (Exactly i) sp kn) defs + | UpdateTac kn -> ()) defs let cache_md x = load_md 1 x diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index add57cb5..b66bdb85 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacinterp.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id: tacinterp.mli 12102 2009-04-24 10:48:11Z herbelin $ i*) (*i*) open Dyn @@ -44,6 +44,9 @@ and interp_sign = debug : debug_info; trace : ltac_trace } +val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> + Pretyping.var_map * Pretyping.unbound_ltac_var_map + (* Transforms an id into a constr if possible *) val constr_of_id : Environ.env -> identifier -> constr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 28e987fa..3db6bcef 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacticals.ml 11735 2009-01-02 17:22:31Z herbelin $ *) +(* $Id: tacticals.ml 12102 2009-04-24 10:48:11Z herbelin $ *) open Pp open Util @@ -26,7 +26,6 @@ open Clenvtac open Rawterm open Pattern open Matching -open Evar_refiner open Genarg open Tacexpr diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2c567034..0a8b5d01 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *) open Pp open Util @@ -155,19 +155,37 @@ let order_hyps = Tacmach.order_hyps (* Renaming hypotheses *) let rename_hyp = Tacmach.rename_hyp +(**************************************************************) +(* Fresh names *) +(**************************************************************) + +let fresh_id_avoid avoid id = + next_global_ident_away true id avoid + +let fresh_id avoid id gl = + fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id + +(**************************************************************) +(* Fixpoints and CoFixpoints *) +(**************************************************************) + (* Refine as a fixpoint *) let mutual_fix = Tacmach.mutual_fix -let fix ido n = match ido with - | None -> mutual_fix (Pfedit.get_current_proof_name ()) n [] - | Some id -> mutual_fix id n [] +let fix ido n gl = match ido with + | None -> + mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl + | Some id -> + mutual_fix id n [] gl (* Refine as a cofixpoint *) let mutual_cofix = Tacmach.mutual_cofix -let cofix = function - | None -> mutual_cofix (Pfedit.get_current_proof_name ()) [] - | Some id -> mutual_cofix id [] +let cofix ido gl = match ido with + | None -> + mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl + | Some id -> + mutual_cofix id [] gl (**************************************************************) (* Reduction and conversion tactics *) @@ -286,12 +304,6 @@ let unfold_constr = function (* Introduction tactics *) (*******************************************) -let fresh_id_avoid avoid id = - next_global_ident_away true id avoid - -let fresh_id avoid id gl = - fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id - let id_of_name_with_default id = function | Anonymous -> id | Name id -> id @@ -565,9 +577,14 @@ let error_uninstantiated_metas t clenv = let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") -let clenv_refine_in with_evars id clenv gl = +let clenv_refine_in with_evars ?(with_classes=true) id clenv gl = let clenv = clenv_pose_dependent_evars with_evars clenv in - let new_hyp_typ = clenv_type clenv in + let clenv = + if with_classes then + { clenv with evd = Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd } + else clenv + in + let new_hyp_typ = clenv_type clenv in if not with_evars & occur_meta new_hyp_typ then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in @@ -1098,9 +1115,6 @@ let forward_general_multi_rewrite = let register_general_multi_rewrite f = forward_general_multi_rewrite := f -let clear_last = tclLAST_HYP (fun c -> (clear [destVar c])) -let case_last = tclLAST_HYP simplest_case - let error_unexpected_extra_pattern loc nb pat = let s1,s2,s3 = match pat with | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" @@ -1111,8 +1125,8 @@ let error_unexpected_extra_pattern loc nb pat = str (if nb = 1 then "was" else "were") ++ strbrk " expected in the branch).") -let intro_or_and_pattern loc b ll l' tac = - tclLAST_HYP (fun c gl -> +let intro_or_and_pattern loc b ll l' tac id gl = + let c = mkVar id in let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let nv = mis_constr_nargs ind in let bracketed = b or not (l'=[]) in @@ -1126,10 +1140,10 @@ let intro_or_and_pattern loc b ll l' tac = let ll = fix_empty_or_and_pattern (Array.length nv) ll in check_or_and_pattern_size loc ll (Array.length nv); tclTHENLASTn - (tclTHEN case_last clear_last) + (tclTHEN (simplest_case c) (clear [id])) (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l')) nv (Array.of_list ll)) - gl) + gl let rewrite_hyp l2r id gl = let rew_on l2r = @@ -1194,8 +1208,9 @@ let rec intros_patterns b avoid thin destopt = function | (loc, IntroOrAndPattern ll) :: l' -> tclTHEN introf - (intro_or_and_pattern loc b ll l' - (intros_patterns b avoid thin destopt)) + (onLastHyp + (intro_or_and_pattern loc b ll l' + (intros_patterns b avoid thin destopt))) | (loc, IntroRewrite l2r) :: l -> tclTHEN (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true) @@ -1229,8 +1244,10 @@ let prepare_intros s ipat gl = match ipat with | IntroRewrite l2r -> let id = make_id s gl in id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses - | IntroOrAndPattern ll -> make_id s gl, - intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) + | IntroOrAndPattern ll -> make_id s gl, + onLastHyp + (intro_or_and_pattern loc true ll [] + (intros_patterns true [] [] no_move)) let ipat_of_name = function | Anonymous -> None @@ -1261,6 +1278,7 @@ let as_tac id ipat = match ipat with !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allClauses | Some (loc,IntroOrAndPattern ll) -> intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) + id | Some (loc, (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | IntroWildcard)) -> user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected") @@ -2167,7 +2185,7 @@ let dependent_pattern c gl = let conclvar = subst_term_occ all_occurrences c ty in mkNamedLambda id cty conclvar in - let subst = (c, varname c, cty) :: List.map (fun c -> (c, varname c, pf_type_of gl c)) deps in + let subst = (c, varname c, cty) :: List.rev_map (fun c -> (c, varname c, pf_type_of gl c)) deps in let concllda = List.fold_left mklambda (pf_concl gl) subst in let conclapp = applistc concllda (List.rev_map pi1 subst) in convert_concl_no_check conclapp DEFAULTcast gl -- cgit v1.2.3