From da178a880e3ace820b41d38b191d3785b82991f5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 1 Jul 2010 17:21:14 +0200 Subject: Imported Upstream version 8.2pl2+dfsg --- tactics/decl_interp.ml | 4 ++-- tactics/decl_proof_instr.ml | 34 ++++++++++++++++++++++--------- tactics/decl_proof_instr.mli | 13 ++++++------ tactics/equality.ml | 23 +++++++++++++++++---- tactics/hiddentac.ml | 8 ++++---- tactics/inv.ml | 4 ++-- tactics/leminv.ml | 6 +++++- tactics/refine.ml | 8 +++++++- tactics/tacinterp.ml | 13 ++++++++---- tactics/tactics.ml | 48 +++++++++++++++++++++++++++++++++++++------- tactics/tauto.ml4 | 17 +++++++++++----- 11 files changed, 133 insertions(+), 45 deletions(-) (limited to 'tactics') diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index c99884c0..62824670 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decl_interp.ml 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id: decl_interp.ml 12422 2009-10-27 08:42:49Z corbinea $ i*) open Util open Names @@ -334,7 +334,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = if List.length params <> expected then errorlabstrm "suppose it is" (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ + (if expected = 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 62a8ddfc..67d1d41a 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 12135 2009-05-20 14:49:23Z herbelin $ *) +(* $Id: decl_proof_instr.ml 12422 2009-10-27 08:42:49Z corbinea $ *) open Util open Pp @@ -1161,7 +1161,7 @@ let case_tac params pat_info hyps gls0 = let clause = build_dep_clause params pat_info per_info hyps gls0 in let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let nek = - register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info + register_dep_subcase (id,(List.length params,List.length hyps)) (pf_env gls0) per_info pat_info.pat_pat ek in let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in tclTHENS (assert_postpone id clause) @@ -1227,6 +1227,7 @@ let hrec_for fix_id per_info gls obj_id = let hd2 = applist (mkVar fix_id,args@[obj]) in compose_lam rc (whd_beta gls.sigma hd2) + let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match tree, objs with Close_patt t,_ -> @@ -1235,16 +1236,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | Skip_patt (_,t),skipped::next_objs -> let args0 = push_arg skipped args in execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls - | End_patt (id,nhyps),[] -> + | End_patt (id,(nparams,nhyps)),[] -> begin match List.assoc id args with [None,br_args] -> - let metas = - list_tabulate (fun n -> mkMeta (succ n)) nhyps in + let all_metas = + list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + let param_metas,hyp_metas = list_chop nparams all_metas in tclTHEN (tclDO nhrec introf) (tacnext - (applist (mkVar id,List.rev_append br_args metas))) gls + (applist (mkVar id, + List.append param_metas + (List.rev_append br_args hyp_metas)))) gls | _ -> anomaly "wrong stack size" end | Split_patt (ids,ind,br), casee::next_objs -> @@ -1318,7 +1322,19 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = | End_patt (_,_) , _ :: _ -> anomaly "execute_cases : End of branch with garbage left" - +let understand_my_constr c gls = + let env = pf_env gls in + let nc = names_of_rel_context env in + let rawc = Detyping.detype false [] nc c in + let rec frob = function REvar _ -> RHole (dummy_loc,QuestionMark Expand) | rc -> map_rawconstr frob rc in + Pretyping.Default.understand_tcc (sig_sig gls) env ~expected_type:(pf_concl gls) (frob rawc) + +let set_refine,my_refine = +let refine = ref (fun (_:open_constr) -> (assert false : tactic) ) in +((fun tac -> refine:= tac), +(fun c gls -> + let oc = understand_my_constr c gls in + !refine oc gls)) (* end focus/claim *) @@ -1361,7 +1377,7 @@ let end_tac et2 gls = | ET_Case_analysis,EK_dep tree -> execute_cases Anonymous pi (fun c -> tclTHENLIST - [refine c; + [my_refine c; clear clauses; justification assumption]) (initial_instance_stack clauses) [pi.per_casee] 0 tree @@ -1382,7 +1398,7 @@ let end_tac et2 gls = (fun c -> tclTHENLIST [clear [fix_id]; - refine c; + my_refine c; clear clauses; justification assumption]) (initial_instance_stack clauses) diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index 877c8047..5f4a0485 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.mli 11481 2008-10-20 19:23:51Z herbelin $ *) +(* $Id: decl_proof_instr.mli 12422 2009-10-27 08:42:49Z corbinea $ *) open Refiner open Names @@ -42,20 +42,20 @@ val execute_cases : Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic val tree_of_pats : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree val add_branch : - identifier * int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val append_branch : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier *(int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> (Names.Idset.t * Decl_mode.split_tree) option -> (Names.Idset.t * Decl_mode.split_tree) option val append_tree : - identifier * int -> int -> (Rawterm.cases_pattern*recpath) list list -> + identifier * (int * int) -> int -> (Rawterm.cases_pattern*recpath) list list -> split_tree -> split_tree val build_dep_clause : Term.types Decl_expr.statement list -> @@ -65,7 +65,7 @@ val build_dep_clause : Term.types Decl_expr.statement list -> Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types val register_dep_subcase : - Names.identifier * int -> + Names.identifier * (int * int) -> Environ.env -> Decl_mode.per_info -> Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind @@ -115,3 +115,4 @@ val init_tree: (Names.Idset.t * Decl_mode.split_tree) option) -> Decl_mode.split_tree +val set_refine : (Evd.open_constr -> Proof_type.tactic) -> unit diff --git a/tactics/equality.ml b/tactics/equality.ml index 58a00419..bf199379 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 12053 2009-04-06 16:20:42Z msozeau $ *) +(* $Id: equality.ml 12886 2010-03-27 14:22:00Z herbelin $ *) open Pp open Util @@ -688,6 +688,16 @@ let minimal_free_rels env sigma (c,cty) = else (cty',rels') +(* Like the above, but recurse over all the rels found until there are + no more rels to be found *) +let minimal_free_rels_rec env sigma = + let rec minimalrec_free_rels_rec prev_rels (c,cty) = + let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in + let combined_rels = Intset.union prev_rels direct_rels in + let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i))) + in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels))) + in minimalrec_free_rels_rec Intset.empty + (* [sig_clausal_form siglen ty] Will explode [siglen] [sigS,sigT ]'s on [ty] (depending on the @@ -706,7 +716,7 @@ let minimal_free_rels env sigma (c,cty) = WARNING: No checking is done to make sure that the sigS(or sigT)'s are actually there. - - Only homogenious pairs are built i.e. pairs where all the + - Only homogeneous pairs are built i.e. pairs where all the dependencies are of the same sort [sig_clausal_form] proceed as follows: the default tuple is @@ -747,7 +757,12 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = Evd.existential_opt_value (Evd.evars_of !evdref) (destEvar ev) with - | Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | Some w -> + let w_type = type_of env sigma w in + if Evarconv.e_conv env evdref w_type a then + applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + else + error "Cannot solve a unification problem." | None -> anomaly "Not enough components to build the dependent tuple" in let scf = sigrec_clausal_form siglen ty in @@ -812,7 +827,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = *) let make_iterated_tuple env sigma dflt (z,zty) = - let (zty,rels) = minimal_free_rels env sigma (z,zty) in + let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in let sorted_rels = Sort.list (<) (Intset.elements rels) in let (tuple,tuplety) = diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8e517453..4ab40acb 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hiddentac.ml 12102 2009-04-24 10:48:11Z herbelin $ *) +(* $Id: hiddentac.ml 13124 2010-06-13 11:09:38Z herbelin $ *) open Term open Proof_type @@ -83,10 +83,10 @@ let h_simple_induction_destruct isrec h = let h_simple_induction = h_simple_induction_destruct true let h_simple_destruct = h_simple_induction_destruct false -let h_induction_destruct isrec ev l = +let h_induction_destruct ev isrec l = abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) -> List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l)) - (induction_destruct ev isrec l) + (induction_destruct isrec ev l) let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl] let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl] @@ -105,7 +105,7 @@ let h_revert l = abstract_tactic (TacRevert l) (revert l) (* Constructors *) let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_ebindings ev l) -let h_right ev l = abstract_tactic (TacLeft (ev,l)) (right_with_ebindings ev l) +let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_ebindings ev l) let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_ebindings ev l) (* Moved to tacinterp because of dependencies in Tacinterp.interp let h_any_constructor t = diff --git a/tactics/inv.ml b/tactics/inv.ml index 977b602e..af204e77 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml 11784 2009-01-14 11:36:32Z herbelin $ *) +(* $Id: inv.ml 12410 2009-10-24 17:23:39Z herbelin $ *) open Pp open Util @@ -291,7 +291,7 @@ let generalizeRewriteIntros tac depids id gls = let rec tclMAP_i n tacfun = function | [] -> tclDO n (tacfun None) | a::l -> - if n=0 then error "Too much names." + if n=0 then error "Too many names." else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) let remember_first_eq id x = if !x = no_move then x := MoveAfter id diff --git a/tactics/leminv.ml b/tactics/leminv.ml index e798f59a..4cbfa6c2 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *) +(* $Id: leminv.ml 13126 2010-06-13 11:09:51Z herbelin $ *) open Pp open Util @@ -291,11 +291,15 @@ let add_inversion_lemma_exn na com comsort bool tac = (* ================================= *) let lemInv id c gls = + ignore (pf_get_hyp gls id); (* ensure id exists *) try let clause = mk_clenv_type_of gls c in let clause = clenv_constrain_last_binding (mkVar id) clause in Clenvtac.res_pf clause ~allow_K:true gls with + | NoSuchBinding -> + errorlabstrm "" + (hov 0 (pr_constr c ++ spc () ++ str "does not refer to an inversion lemma.")) | UserError (a,b) -> errorlabstrm "LemInv" (str "Cannot refine current goal with the lemma " ++ diff --git a/tactics/refine.ml b/tactics/refine.ml index 322d25e5..ff3f0887 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refine.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: refine.ml 13129 2010-06-13 14:23:55Z herbelin $ *) (* JCF -- 6 janvier 1998 EXPERIMENTAL *) @@ -108,6 +108,8 @@ let replace_by_meta env sigma = function | _ -> invalid_arg "Tcc.replace_by_meta (TO DO)" *) in + if occur_meta ty then + error "Unable to manage a dependent metavariable of higher-order type."; mkCast (m,DEFAULTcast, ty),[n,ty],[Some th] exception NoMeta @@ -189,6 +191,8 @@ let rec compute_metamap env sigma c = match kind_of_term c with end | Case (ci,p,cc,v) -> + if occur_meta p then + error "Unable to manage a metavariable in the return clause of a match."; (* bof... *) let nbr = Array.length v in let v = Array.append [|p;cc|] v in @@ -380,3 +384,5 @@ let refine (evd,c) gl = complicated to update meta types when passing through a binder *) let th = compute_metamap (pf_env gl) evd c in tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl + +let _ = Decl_proof_instr.set_refine refine (* dirty trick to solve circular dependency *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 71b50b66..5c891c58 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: tacinterp.ml 13130 2010-06-13 18:45:09Z herbelin $ *) open Constrintern open Closure @@ -1096,7 +1096,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps = match_next_pattern find_next') with | PatternMatchingFailure -> apply_one_mhyp_context_rec tl in - match_next_pattern (fun () -> match_pat lmatch hyp pat) () + match_next_pattern (fun () -> + let hyp = if b<>None then refresh_universes_strict hyp else hyp in + match_pat lmatch hyp pat) () | Some patv -> match b with | Some body -> @@ -1112,7 +1114,9 @@ let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) lhyps = | PatternMatchingFailure -> match_next_pattern_in_body next_in_body' () in match_next_pattern_in_typ - (fun () -> match_pat lmeta hyp pat) () + (fun () -> + let hyp = refresh_universes_strict hyp in + match_pat lmeta hyp pat) () with PatternMatchingFailure -> apply_one_mhyp_context_rec tl in match_next_pattern_in_body @@ -2872,7 +2876,8 @@ let add_tacdef isrec tacl = (***************************************************************************) (* Other entry points *) -let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x +let glob_tactic x = + Flags.with_option strict_check (intern_tactic (make_empty_glob_sign ())) x let glob_tactic_env l env x = Flags.with_option strict_check diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0a8b5d01..0a4c0fbe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 12187 2009-06-13 19:36:59Z msozeau $ *) +(* $Id: tactics.ml 12956 2010-04-20 08:49:15Z herbelin $ *) open Pp open Util @@ -249,14 +249,51 @@ let change_option occl t = function Some id -> change_in_hyp occl t id | None -> change_in_concl occl t -let change occl c cls = +let out_arg = function + | ArgVar _ -> anomaly "Unevaluated or_var variable" + | ArgArg x -> x + +let adjust_clause occl cls = + (* warn as much as possible on loss of occurrence information *) (match cls, occl with ({onhyps=(Some(_::_::_)|None)} |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}), Some _ -> error "No occurrences expected when changing several hypotheses." | _ -> ()); - onClauses (change_option occl c) cls + (* get at clause from cls if only goal or one hyp specified *) + let occl,cls = match occl with + | None -> None,cls + | Some (occs,c) -> + if cls.onhyps=Some[] && occs=all_occurrences then + Some (on_snd (List.map out_arg) cls.concl_occs,c), + {cls with concl_occs=all_occurrences_expr} + else + match cls.onhyps with + | Some[(occs',id),l] when + cls.concl_occs=no_occurrences_expr && occs=all_occurrences -> + Some (on_snd (List.map out_arg) occs',c), + {cls with onhyps=Some[(all_occurrences_expr,id),l]} + | _ -> + occl,cls in + (* check if cls has still specified occs *) + if cls.onhyps <> None && + List.exists (fun ((occs,_),_) -> occs <> all_occurrences_expr) + (Option.get cls.onhyps) + || cls.concl_occs <> all_occurrences_expr && + cls.concl_occs <> no_occurrences_expr + then + Flags.if_verbose Pp.msg_warning + (if cls.onhyps=Some[] then + str "Trailing \"at\" modifier not taken into account." + else + str "\"at\" modifier in clause \"in\" not taken into account."); + (* Anticipate on onClauses which removes concl if not at all occs *) + if cls.concl_occs=no_occurrences_expr then cls + else {cls with concl_occs=all_occurrences_expr} + +let change occl c cls = + onClauses (change_option occl c) (adjust_clause occl cls) (* Pour usage interne (le niveau User est pris en compte par reduce) *) let red_in_concl = reduct_in_concl (red_product,DEFAULTcast) @@ -1397,10 +1434,6 @@ let quantify lconstr = the left of each x1, ...). *) -let out_arg = function - | ArgVar _ -> anomaly "Unevaluated or_var variable" - | ArgArg x -> x - let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> None @@ -2546,6 +2579,7 @@ let induction_tac_felim with_evars indvars scheme gl = let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl = let env = pf_env gl in let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in + let deps = List.map (fun (id,c,t)-> (id,c,refresh_universes_strict t)) deps in let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in let names = compute_induction_names (Array.length indsign) names in let dephyps = List.map (fun (id,_,_) -> id) deps in diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 1729695d..d3e7da6a 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4 11739 2009-01-02 19:33:19Z herbelin $ i*) +(*i $Id: tauto.ml4 12955 2010-04-20 08:10:14Z herbelin $ i*) open Term open Hipattern @@ -20,6 +20,7 @@ open Tacticals open Tacinterp open Tactics open Util +open Genarg let assoc_var s ist = match List.assoc (Names.id_of_string s) ist.lfun with @@ -97,18 +98,21 @@ let is_conj ist = let flatten_contravariant_conj ist = let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in + let hyp = assoc_var "id" ist in match match_with_conjunction ~strict:strict_in_contravariant_hyp typ with | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then let newtyp = valueIn (VConstr (List.fold_right mkArrow args c)) in + let hyp = valueIn (VConstr hyp) in let intros = iter_tac (List.map (fun _ -> <:tactic< intro >>) args) <:tactic< idtac >> in <:tactic< let newtyp := $newtyp in - assert newtyp by ($intros; apply id; split; assumption); - clear id + let hyp := $hyp in + assert newtyp by ($intros; apply hyp; split; assumption); + clear hyp >> else <:tactic> @@ -129,16 +133,19 @@ let is_disj ist = let flatten_contravariant_disj ist = let typ = assoc_var "X1" ist in let c = assoc_var "X2" ist in + let hyp = assoc_var "id" ist in match match_with_disjunction ~strict:strict_in_contravariant_hyp typ with | Some (_,args) -> let i = List.length args in if not binary_mode || i = 2 then + let hyp = valueIn (VConstr hyp) in iter_tac (list_map_i (fun i arg -> let typ = valueIn (VConstr (mkArrow arg c)) in <:tactic< let typ := $typ in - assert typ by (intro; apply id; constructor $i; assumption) - >>) 1 args) <:tactic< clear id >> + let hyp := $hyp in + assert typ by (intro; apply hyp; constructor $i; assumption) + >>) 1 args) <:tactic< let hyp := $hyp in clear hyp >> else <:tactic> | _ -> -- cgit v1.2.3