diff options
author | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
tree | 591e9e512063e34099782e2518573f15ffeac003 /tactics | |
parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/auto.ml | 7 | ||||
-rw-r--r-- | tactics/autorewrite.ml | 66 | ||||
-rw-r--r-- | tactics/autorewrite.mli | 7 | ||||
-rw-r--r-- | tactics/contradiction.ml | 6 | ||||
-rw-r--r-- | tactics/decl_interp.ml | 429 | ||||
-rw-r--r-- | tactics/decl_interp.mli | 18 | ||||
-rw-r--r-- | tactics/decl_proof_instr.ml | 1476 | ||||
-rw-r--r-- | tactics/decl_proof_instr.mli | 118 | ||||
-rw-r--r-- | tactics/eauto.ml4 | 4 | ||||
-rw-r--r-- | tactics/equality.ml | 503 | ||||
-rw-r--r-- | tactics/equality.mli | 26 | ||||
-rw-r--r-- | tactics/evar_tactics.ml | 4 | ||||
-rw-r--r-- | tactics/extraargs.ml4 | 114 | ||||
-rw-r--r-- | tactics/extraargs.mli | 13 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 168 | ||||
-rw-r--r-- | tactics/extratactics.mli | 20 | ||||
-rw-r--r-- | tactics/leminv.ml | 4 | ||||
-rw-r--r-- | tactics/setoid_replace.ml | 399 | ||||
-rw-r--r-- | tactics/setoid_replace.mli | 7 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 486 | ||||
-rw-r--r-- | tactics/tacinterp.mli | 14 | ||||
-rw-r--r-- | tactics/tacticals.ml | 3 | ||||
-rw-r--r-- | tactics/tacticals.mli | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 241 | ||||
-rw-r--r-- | tactics/tactics.mli | 5 |
25 files changed, 3356 insertions, 786 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 7c1c375b..3cd1591d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 8878 2006-05-30 16:44:25Z herbelin $ *) +(* $Id: auto.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Util @@ -192,7 +192,10 @@ let make_exact_entry (c,cty) = { pri=0; pat=None; code=Give_exact c }) let dummy_goal = - {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty}; + {it={evar_hyps=empty_named_context_val; + evar_concl=mkProp; + evar_body=Evar_empty; + evar_extra=None}; sigma=Evd.empty} let make_apply_entry env sigma (eapply,verbose) (c,cty) = diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index ceeb4763..872b8697 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: autorewrite.ml 8114 2006-03-02 18:09:27Z herbelin $ *) +(* $Id: autorewrite.ml 9157 2006-09-21 15:10:08Z herbelin $ *) open Equality open Hipattern @@ -60,11 +60,11 @@ type raw_rew_rule = constr * bool * raw_tactic_expr (* Applies all the rules of one base *) let one_base general_rewrite_maybe_in tac_main bas = - let lrul = - try + let lrul = + try Stringmap.find bas !rewtab - with Not_found -> - errorlabstrm "AutoRewrite" + with Not_found -> + errorlabstrm "AutoRewrite" (str ("Rewriting base "^(bas)^" does not exist")) in let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in @@ -74,16 +74,19 @@ let one_base general_rewrite_maybe_in tac_main bas = (tclTHENSFIRSTn (general_rewrite_maybe_in dir csr) [|tac_main|] tc))) tclIDTAC lrul)) + + (* The AutoRewrite tactic *) let autorewrite tac_main lbas = tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac bas -> tclTHEN tac (one_base general_rewrite tac_main bas)) tclIDTAC lbas)) -let autorewrite_in id tac_main lbas gl = +let autorewrite_mutlti_in idl tac_main lbas : tactic = + fun gl -> (* let's check at once if id exists (to raise the appropriate error) *) - let _ = Tacmach.pf_get_hyp gl id in - let general_rewrite_in = + let _ = List.map (Tacmach.pf_get_hyp gl) idl in + let general_rewrite_in id = let id = ref id in let to_be_cleared = ref false in fun dir cstr gl -> @@ -117,10 +120,51 @@ let autorewrite_in id tac_main lbas gl = | _ -> assert false) (* there must be at least an hypothesis *) | _ -> assert false (* rewriting cannot complete a proof *) in + tclMAP (fun id -> tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac bas -> - tclTHEN tac (one_base general_rewrite_in tac_main bas)) tclIDTAC lbas)) - gl + tclTHEN tac (one_base (general_rewrite_in id) tac_main bas)) tclIDTAC lbas))) + idl gl + +let autorewrite_in id = autorewrite_mutlti_in [id] + +let gen_auto_multi_rewrite tac_main lbas cl = + let try_do_hyps treat_id l = + autorewrite_mutlti_in (List.map treat_id l) tac_main lbas + in + if cl.concl_occs <> [] then + error "The \"at\" syntax isn't available yet for the autorewrite tactic" + else + let compose_tac t1 t2 = + match cl.onhyps with + | Some [] -> t1 + | _ -> tclTHENFIRST t1 t2 + in + compose_tac + (if cl.onconcl then autorewrite tac_main lbas else tclIDTAC) + (match cl.onhyps with + | Some l -> try_do_hyps (fun ((_,id),_) -> id) l + | None -> + fun gl -> + (* try to rewrite in all hypothesis + (except maybe the rewritten one) *) + let ids = Tacmach.pf_ids_of_hyps gl + in try_do_hyps (fun id -> id) ids gl) + +let auto_multi_rewrite = gen_auto_multi_rewrite Refiner.tclIDTAC + +let auto_multi_rewrite_with tac_main lbas cl gl = + match cl.Tacexpr.onconcl,cl.Tacexpr.onhyps with + | false,Some [_] | true,Some [] | false,Some [] -> + (* autorewrite with .... in clause using tac n'est sur que + si clause reprensente soit le but soit UNE hypothse + *) + gen_auto_multi_rewrite tac_main lbas cl gl + | _ -> + Util.errorlabstrm "autorewrite" + (str "autorewrite .. in .. using can only be used either with a unique hypothesis or" ++ + str " on the conclusion") + (* Functions necessary to the library object declaration *) let cache_hintrewrite (_,(rbase,lrl)) = @@ -165,8 +209,8 @@ let classify_hintrewrite (_,x) = Libobject.Substitute x (* Declaration of the Hint Rewrite library object *) let (in_hintrewrite,out_hintrewrite)= Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with - Libobject.open_function = (fun i o -> if i=1 then cache_hintrewrite o); Libobject.cache_function = cache_hintrewrite; + Libobject.load_function = (fun _ -> cache_hintrewrite); Libobject.subst_function = subst_hintrewrite; Libobject.classify_function = classify_hintrewrite; Libobject.export_function = export_hintrewrite } diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 47d3c86a..f402a35d 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: autorewrite.mli 7034 2005-05-18 19:30:44Z sacerdot $ i*) +(*i $Id: autorewrite.mli 9073 2006-08-22 08:54:29Z jforest $ i*) (*i*) open Tacmach @@ -22,4 +22,9 @@ val add_rew_rules : string -> raw_rew_rule list -> unit val autorewrite : tactic -> string list -> tactic val autorewrite_in : Names.identifier -> tactic -> string list -> tactic + +val auto_multi_rewrite : string list -> Tacticals.clause -> tactic + +val auto_multi_rewrite_with : tactic -> string list -> Tacticals.clause -> tactic + val print_rewrite_hintdb : string -> unit diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 0f274aae..eca16066 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: contradiction.ml 5920 2004-07-16 20:01:26Z herbelin $ *) +(* $Id: contradiction.ml 9269 2006-10-24 13:01:55Z herbelin $ *) open Util open Term @@ -22,6 +22,10 @@ open Rawterm (* Absurd *) let absurd c gls = + let env = pf_env gls and sigma = project gls in + let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env + (Evd.create_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in + let c = j.Environ.utj_val in (tclTHENS (tclTHEN (elim_type (build_coq_False ())) (cut c)) ([(tclTHENS diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml new file mode 100644 index 00000000..8ace0a08 --- /dev/null +++ b/tactics/decl_interp.ml @@ -0,0 +1,429 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Names +open Topconstr +open Tacinterp +open Tacmach +open Decl_expr +open Decl_mode +open Pretyping.Default +open Rawterm +open Term +open Pp + +let raw_app (loc,hd,args) = if args =[] then hd else RApp(loc,hd,args) + +let intern_justification globs = function + Automated l -> Automated (List.map (intern_constr globs) l) + | By_tactic tac -> By_tactic (intern_tactic globs tac) + +let intern_statement intern_it globs st = + {st_label=st.st_label; + st_it=intern_it globs st.st_it} + +let intern_constr_or_thesis globs = function + Thesis n -> Thesis n + | This c -> This (intern_constr globs c) + +let add_var id globs= + let l1,l2=globs.ltacvars in + {globs with ltacvars= (id::l1),(id::l2)} + +let add_name nam globs= + match nam with + Anonymous -> globs + | Name id -> add_var id globs + +let intern_hyp iconstr globs = function + Hvar (loc,(id,topt)) -> add_var id globs, + Hvar (loc,(id,option_map (intern_constr globs) topt)) + | Hprop st -> add_name st.st_label globs, + Hprop (intern_statement iconstr globs st) + +let intern_hyps iconstr globs hyps = + snd (list_fold_map (intern_hyp iconstr) globs hyps) + +let intern_cut intern_it globs cut= + {cut_stat=intern_statement intern_it globs cut.cut_stat; + cut_by=intern_justification globs cut.cut_by} + +let intern_casee globs = function + Real c -> Real (intern_constr globs c) + | Virtual cut -> Virtual (intern_cut intern_constr globs cut) + +let intern_hyp_list args globs = + let intern_one globs (loc,(id,opttyp)) = + (add_var id globs), + (loc,(id,option_map (intern_constr globs) opttyp)) in + list_fold_map intern_one globs args + +let intern_fundecl args body globs= + let nglobs,nargs = intern_hyp_list args globs in + nargs,intern_constr nglobs body + +let rec add_vars_of_simple_pattern globs = function + CPatAlias (loc,p,id) -> + add_vars_of_simple_pattern (add_var id globs) p +(* Stdpp.raise_with_loc loc + (UserError ("simple_pattern",str "\"as\" is not allowed here"))*) + | CPatOr (loc, _)-> + Stdpp.raise_with_loc loc + (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here")) + | CPatDelimiters (_,_,p) -> + add_vars_of_simple_pattern globs p + | CPatCstr (_,_,pl) | CPatNotation(_,_,pl) -> + List.fold_left add_vars_of_simple_pattern globs pl + | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs + | _ -> globs + +let rec intern_bare_proof_instr globs = function + Pthus i -> Pthus (intern_bare_proof_instr globs i) + | Pthen i -> Pthen (intern_bare_proof_instr globs i) + | Phence i -> Phence (intern_bare_proof_instr globs i) + | Pcut c -> Pcut (intern_cut intern_constr_or_thesis globs c) + | Prew (s,c) -> Prew (s,intern_cut intern_constr globs c) + | Psuppose hyps -> Psuppose (intern_hyps intern_constr globs hyps) + | Pcase (params,pat,hyps) -> + let nglobs,nparams = intern_hyp_list params globs in + let nnglobs= add_vars_of_simple_pattern nglobs pat in + let nhyps = intern_hyps intern_constr_or_thesis nnglobs hyps in + Pcase (nparams,pat,nhyps) + | Ptake witl -> Ptake (List.map (intern_constr globs) witl) + | Pconsider (c,hyps) -> Pconsider (intern_constr globs c, + intern_hyps intern_constr globs hyps) + | Pper (et,c) -> Pper (et,intern_casee globs c) + | Pend bt -> Pend bt + | Pescape -> Pescape + | Passume hyps -> Passume (intern_hyps intern_constr globs hyps) + | Pgiven hyps -> Pgiven (intern_hyps intern_constr globs hyps) + | Plet hyps -> Plet (intern_hyps intern_constr globs hyps) + | Pclaim st -> Pclaim (intern_statement intern_constr globs st) + | Pfocus st -> Pfocus (intern_statement intern_constr globs st) + | Pdefine (id,args,body) -> + let nargs,nbody = intern_fundecl args body globs in + Pdefine (id,nargs,nbody) + | Pcast (id,typ) -> + Pcast (id,intern_constr globs typ) + +let rec intern_proof_instr globs instr= + {emph = instr.emph; + instr = intern_bare_proof_instr globs instr.instr} + +let interp_justification env sigma = function + Automated l -> + Automated (List.map (fun c ->understand env sigma (fst c)) l) + | By_tactic tac -> By_tactic tac + +let interp_constr check_sort env sigma c = + if check_sort then + understand_type env sigma (fst c) + else + understand env sigma (fst c) + +let special_whd env = + let infos=Closure.create_clos_infos Closure.betadeltaiota env in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) + +let decompose_eq env id = + let typ = Environ.named_type id env in + let whd = special_whd env typ in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then args.(0) + else error "previous step is not an equality" + | _ -> error "previous step is not an equality" + +let get_eq_typ info env = + let last_id = + match info.pm_last with + Anonymous -> error "no previous equality" + | Name id -> id in + let typ = decompose_eq env last_id in + typ + +let interp_constr_in_type typ env sigma c = + understand env sigma (fst c) ~expected_type:typ + +let interp_statement interp_it env sigma st = + {st_label=st.st_label; + st_it=interp_it env sigma st.st_it} + +let interp_constr_or_thesis check_sort env sigma = function + Thesis n -> Thesis n + | This c -> This (interp_constr check_sort env sigma c) + +let type_tester_var body typ = + raw_app(dummy_loc, + RLambda(dummy_loc,Anonymous,typ, + RSort (dummy_loc,RProp Null)),body) + +let abstract_one_hyp inject h raw = + match h with + Hvar (loc,(id,None)) -> + RProd (dummy_loc,Name id, RHole (loc,Evd.BinderType (Name id)), raw) + | Hvar (loc,(id,Some typ)) -> + RProd (dummy_loc,Name id,fst typ, raw) + | Hprop st -> + RProd (dummy_loc,st.st_label,inject st.st_it, raw) + +let rawconstr_of_hyps inject hyps = + List.fold_right (abstract_one_hyp inject) hyps (RSort (dummy_loc,RProp Null)) + +let rec match_hyps blend names constr = function + [] -> [] + | hyp::q -> + let (name,typ,body)=destProd constr in + let st= {st_label=name;st_it=substl names typ} in + let qnames= + match name with + Anonymous -> mkMeta 0 :: names + | Name id -> mkVar id :: names in + let qhyp = match hyp with + Hprop st' -> Hprop (blend st st') + | Hvar _ -> Hvar st in + qhyp::(match_hyps blend qnames body q) + +let interp_hyps_gen inject blend env sigma hyps = + let constr=understand env sigma (rawconstr_of_hyps inject hyps) in + match_hyps blend [] constr hyps + +let interp_hyps = interp_hyps_gen fst (fun x _ -> x) + +let dummy_prefix= id_of_string "__" + +let rec deanonymize ids = + function + PatVar (loc,Anonymous) -> + let (found,known) = !ids in + let new_id=Nameops.next_ident_away dummy_prefix known in + let _= ids:= (loc,new_id) :: found , new_id :: known in + PatVar (loc,Name new_id) + | PatVar (loc,Name id) as pat -> + let (found,known) = !ids in + let _= ids:= (loc,id) :: found , known in + pat + | PatCstr(loc,cstr,lpat,nam) -> + PatCstr(loc,cstr,List.map (deanonymize ids) lpat,nam) + +let rec raw_of_pat = + function + PatVar (loc,Anonymous) -> anomaly "Anonymous pattern variable" + | PatVar (loc,Name id) -> + RVar (loc,id) + | PatCstr(loc,((ind,_) as cstr),lpat,_) -> + let mind= fst (Global.lookup_inductive ind) in + let rec add_params n q = + if n<=0 then q else + add_params (pred n) (RHole(dummy_loc, + Evd.TomatchTypeParameter(ind,n))::q) in + let args = List.map raw_of_pat lpat in + raw_app(loc,RRef(dummy_loc,Libnames.ConstructRef cstr), + add_params mind.Declarations.mind_nparams args) + +let prod_one_hyp = function + (loc,(id,None)) -> + (fun raw -> + RProd (dummy_loc,Name id, + RHole (loc,Evd.BinderType (Name id)), raw)) + | (loc,(id,Some typ)) -> + (fun raw -> + RProd (dummy_loc,Name id,fst typ, raw)) + +let prod_one_id (loc,id) raw = + RProd (dummy_loc,Name id, + RHole (loc,Evd.BinderType (Name id)), raw) + +let let_in_one_alias (id,pat) raw = + RLetIn (dummy_loc,Name id,raw_of_pat pat, raw) + +let rec bind_primary_aliases map pat = + match pat with + PatVar (_,_) -> map + | PatCstr(loc,_,lpat,nam) -> + let map1 = + match nam with + Anonymous -> map + | Name id -> (id,pat)::map + in + List.fold_left bind_primary_aliases map1 lpat + +let bind_secondary_aliases map subst = + List.fold_left (fun map (ids,idp) -> (ids,List.assoc idp map)::map) map subst + +let bind_aliases patvars subst patt = + let map = bind_primary_aliases [] patt in + let map1 = bind_secondary_aliases map subst in + List.rev map1 + +let interp_pattern env pat_expr = + let patvars,pats = Constrintern.intern_pattern env pat_expr in + match pats with + [] -> anomaly "empty pattern list" + | [subst,patt] -> + (patvars,bind_aliases patvars subst patt,patt) + | _ -> anomaly "undetected disjunctive pattern" + +let rec match_args dest names constr = function + [] -> [],names,substl names constr + | _::q -> + let (name,typ,body)=dest constr in + let st={st_label=name;st_it=substl names typ} in + let qnames= + match name with + Anonymous -> assert false + | Name id -> mkVar id :: names in + let args,bnames,body = match_args dest qnames body q in + st::args,bnames,body + +let rec match_aliases names constr = function + [] -> [],names,substl names constr + | _::q -> + let (name,c,typ,body)=destLetIn constr in + let st={st_label=name;st_it=(substl names c,substl names typ)} in + let qnames= + match name with + Anonymous -> assert false + | Name id -> mkVar id :: names in + let args,bnames,body = match_aliases qnames body q in + st::args,bnames,body + +let detype_ground c = Detyping.detype false [] [] c + +let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = + let et,pinfo = + match info.pm_stack with + Per(et,pi,_,_)::_ -> et,pi + | _ -> error "No proof per cases/induction/inversion in progress." in + let mib,oib=Global.lookup_inductive pinfo.per_ind in + let num_params = pinfo.per_nparams in + let _ = + let expected = mib.Declarations.mind_nparams - num_params in + 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) ++ + str "expected") in + let app_ind = + let rind = RRef (dummy_loc,Libnames.IndRef pinfo.per_ind) in + let rparams = List.map detype_ground pinfo.per_params in + let rparams_rec = + List.map + (fun (loc,(id,_)) -> + RVar (loc,id)) params in + let dum_args= + list_tabulate (fun _ -> RHole (dummy_loc,Evd.QuestionMark)) + oib.Declarations.mind_nrealargs in + raw_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in + let pat_vars,aliases,patt = interp_pattern env pat in + let inject = function + Thesis (Plain) -> Rawterm.RSort(dummy_loc,RProp Null) + | Thesis (Sub n) -> + error "thesis[_] is not allowed here" + | Thesis (For rec_occ) -> + if not (List.mem rec_occ pat_vars) then + errorlabstrm "suppose it is" + (str "Variable " ++ Nameops.pr_id rec_occ ++ + str " does not occur in pattern."); + Rawterm.RSort(dummy_loc,RProp Null) + | This (c,_) -> c in + let term1 = rawconstr_of_hyps inject hyps in + let loc_ids,npatt = + let rids=ref ([],pat_vars) in + let npatt= deanonymize rids patt in + List.rev (fst !rids),npatt in + let term2 = + RLetIn(dummy_loc,Anonymous, + RCast(dummy_loc,raw_of_pat npatt, + CastConv DEFAULTcast,app_ind),term1) in + let term3=List.fold_right let_in_one_alias aliases term2 in + let term4=List.fold_right prod_one_id loc_ids term3 in + let term5=List.fold_right prod_one_hyp params term4 in + let constr = understand sigma env term5 in + let tparams,nam4,rest4 = match_args destProd [] constr params in + let tpatvars,nam3,rest3 = match_args destProd nam4 rest4 loc_ids in + let taliases,nam2,rest2 = match_aliases nam3 rest3 aliases in + let (_,pat_pat,pat_typ,rest1) = destLetIn rest2 in + let blend st st' = + match st'.st_it with + Thesis nam -> {st_it=Thesis nam;st_label=st'.st_label} + | This _ -> {st_it = This st.st_it;st_label=st.st_label} in + let thyps = match_hyps blend nam2 (Termops.pop rest1) hyps in + tparams,{pat_vars=tpatvars; + pat_aliases=taliases; + pat_constr=pat_pat; + pat_typ=pat_typ; + pat_pat=patt; + pat_expr=pat},thyps + +let interp_cut interp_it env sigma cut= + {cut_stat=interp_statement interp_it env sigma cut.cut_stat; + cut_by=interp_justification env sigma cut.cut_by} + +let interp_casee env sigma = function + Real c -> Real (understand env sigma (fst c)) + | Virtual cut -> Virtual (interp_cut (interp_constr true) env sigma cut) + +let abstract_one_arg = function + (loc,(id,None)) -> + (fun raw -> + RLambda (dummy_loc,Name id, + RHole (loc,Evd.BinderType (Name id)), raw)) + | (loc,(id,Some typ)) -> + (fun raw -> + RLambda (dummy_loc,Name id,fst typ, raw)) + +let rawconstr_of_fun args body = + List.fold_right abstract_one_arg args (fst body) + +let interp_fun env sigma args body = + let constr=understand env sigma (rawconstr_of_fun args body) in + match_args destLambda [] constr args + +let rec interp_bare_proof_instr info sigma env = function + Pthus i -> Pthus (interp_bare_proof_instr info sigma env i) + | Pthen i -> Pthen (interp_bare_proof_instr info sigma env i) + | Phence i -> Phence (interp_bare_proof_instr info sigma env i) + | Pcut c -> Pcut (interp_cut (interp_constr_or_thesis true) sigma env c) + | Prew (s,c) -> Prew (s,interp_cut + (interp_constr_in_type (get_eq_typ info env)) + sigma env c) + | Psuppose hyps -> Psuppose (interp_hyps sigma env hyps) + | Pcase (params,pat,hyps) -> + let tparams,tpat,thyps = interp_cases info env sigma params pat hyps in + Pcase (tparams,tpat,thyps) + | Ptake witl -> + Ptake (List.map (fun c -> understand sigma env (fst c)) witl) + | Pconsider (c,hyps) -> Pconsider (interp_constr false sigma env c, + interp_hyps sigma env hyps) + | Pper (et,c) -> Pper (et,interp_casee sigma env c) + | Pend bt -> Pend bt + | Pescape -> Pescape + | Passume hyps -> Passume (interp_hyps sigma env hyps) + | Pgiven hyps -> Pgiven (interp_hyps sigma env hyps) + | Plet hyps -> Plet (interp_hyps sigma env hyps) + | Pclaim st -> Pclaim (interp_statement (interp_constr true) sigma env st) + | Pfocus st -> Pfocus (interp_statement (interp_constr true) sigma env st) + | Pdefine (id,args,body) -> + let nargs,_,nbody = interp_fun sigma env args body in + Pdefine (id,nargs,nbody) + | Pcast (id,typ) -> + Pcast(id,interp_constr true sigma env typ) + +let rec interp_proof_instr info sigma env instr= + {emph = instr.emph; + instr = interp_bare_proof_instr info sigma env instr.instr} + + + diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli new file mode 100644 index 00000000..08d97646 --- /dev/null +++ b/tactics/decl_interp.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Tacinterp +open Decl_expr +open Mod_subst + + +val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr +val interp_proof_instr : Decl_mode.pm_info -> + Evd.evar_map -> Environ.env -> glob_proof_instr -> proof_instr diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml new file mode 100644 index 00000000..e7acd6d6 --- /dev/null +++ b/tactics/decl_proof_instr.ml @@ -0,0 +1,1476 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Util +open Pp +open Evd + +open Refiner +open Proof_type +open Proof_trees +open Tacmach +open Tacinterp +open Decl_expr +open Decl_mode +open Decl_interp +open Rawterm +open Names +open Declarations +open Tactics +open Tacticals +open Term +open Termops +open Reductionops +open Goptions + +(* Strictness option *) + +let get_its_info gls = get_info gls.it + +let get_strictness,set_strictness = + let strictness = ref false in + (fun () -> (!strictness)),(fun b -> strictness:=b) + +let _ = + declare_bool_option + { optsync = true; + optname = "strict mode"; + optkey = (SecondaryTable ("Strict","Proofs")); + optread = get_strictness; + optwrite = set_strictness } + +let tcl_change_info_gen info_gen = + (fun gls -> + let gl =sig_it gls in + {it=[{gl with evar_extra=info_gen}];sigma=sig_sig gls}, + function + [pftree] -> + {pftree with + goal=gl; + ref=Some (Change_evars,[pftree])} + | _ -> anomaly "change_info : Wrong number of subtrees") + +let tcl_change_info info gls = tcl_change_info_gen (Some (pm_in info)) gls + +let tcl_erase_info gls = tcl_change_info_gen None gls + +let special_whd gl= + let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + (fun t -> Closure.whd_val infos (Closure.inject t)) + +let special_nf gl= + let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in + (fun t -> Closure.norm_val infos (Closure.inject t)) + +let is_good_inductive env ind = + let mib,oib = Inductive.lookup_mind_specif env ind in + oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) + +let check_not_per pts = + if not (Proof_trees.is_complete_proof (proof_of_pftreestate pts)) then + match get_stack pts with + Per (_,_,_,_)::_ -> + error "You are inside a proof per cases/induction.\n\ +Please \"suppose\" something or \"end\" it now." + | _ -> () + +let get_thesis gls0 = + let info = get_its_info gls0 in + match info.pm_subgoals with + [m,thesis] -> thesis + | _ -> error "Thesis is split" + +let mk_evd metalist gls = + let evd0= create_evar_defs (sig_sig gls) in + let add_one (meta,typ) evd = + meta_declare meta typ evd in + List.fold_right add_one metalist evd0 + +(* start a proof *) + +let start_proof_tac gls= + let gl=sig_it gls in + let info={pm_last=Anonymous; + pm_partial_goal=mkMeta 1; + pm_hyps= + begin + let hyps = pf_ids_of_hyps gls in + List.fold_right Idset.add hyps Idset.empty + end; + pm_subgoals= [1,gl.evar_concl]; + pm_stack=[]} in + {it=[{gl with evar_extra=Some (pm_in info)}];sigma=sig_sig gls}, + function + [pftree] -> + {pftree with + goal=gl; + ref=Some (Decl_proof true,[pftree])} + | _ -> anomaly "Dem : Wrong number of subtrees" + +let go_to_proof_mode () = + Pfedit.mutate + (fun pts -> nth_unproven 1 (solve_pftreestate start_proof_tac pts)) + +(* closing gaps *) + +let daimon_tac gls = + set_daimon_flag (); + ({it=[];sigma=sig_sig gls}, + function + [] -> + {open_subgoals=0; + goal=sig_it gls; + ref=Some (Daimon,[])} + | _ -> anomaly "Daimon: Wrong number of subtrees") + +let daimon _ pftree = + set_daimon_flag (); + {pftree with + open_subgoals=0; + ref=Some (Daimon,[])} + +let daimon_subtree = map_pftreestate (fun _ -> frontier_mapi daimon ) + +(* marking closed blocks *) + +let rec is_focussing_instr = function + Pthus i | Pthen i | Phence i -> is_focussing_instr i + | Pescape | Pper _ | Pclaim _ | Pfocus _ + | Psuppose _ | Pcase (_,_,_) -> true + | _ -> false + +let mark_rule_as_done = function + Decl_proof true -> Decl_proof false + | Decl_proof false -> + anomaly "already marked as done" + | Nested(Proof_instr (lock_focus,instr),spfl) -> + if lock_focus then + Nested(Proof_instr (false,instr),spfl) + else + anomaly "already marked as done" + | _ -> anomaly "mark_rule_as_done" + +let mark_proof_tree_as_done pt = + match pt.ref with + None -> anomaly "mark_proof_tree_as_done" + | Some (r,spfl) -> + {pt with ref= Some (mark_rule_as_done r,spfl)} + +let mark_as_done pts = + map_pftreestate + (fun _ -> mark_proof_tree_as_done) + (traverse 0 pts) + +(* post-instruction focus management *) + +let goto_current_focus pts = up_until_matching_rule is_focussing_command pts + +let goto_current_focus_or_top pts = + try + up_until_matching_rule is_focussing_command pts + with Not_found -> top_of_tree pts + +(* return *) + +let close_tactic_mode pts = + let pts1= + try goto_current_focus pts + with Not_found -> + error "\"return\" cannot be used outside of Declarative Proof Mode" in + let pts2 = daimon_subtree pts1 in + let pts3 = mark_as_done pts2 in + goto_current_focus pts3 + +let return_from_tactic_mode () = Pfedit.mutate close_tactic_mode + +(* end proof/claim *) + +let close_block bt pts = + let stack = + if Proof_trees.is_complete_proof (proof_of_pftreestate pts) then + get_top_stack pts + else + get_stack pts in + match bt,stack with + B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> + daimon_subtree (goto_current_focus pts) + | _, Claim::_ -> + error "\"end claim\" expected" + | _, Focus_claim::_ -> + error "\"end focus\" expected" + | _, [] -> + error "\"end proof\" expected" + | _, (Per (et,_,_,_)::_|Suppose_case::Per (et,_,_,_)::_) -> + begin + match et with + ET_Case_analysis -> error "\"end cases\" expected" + | ET_Induction -> error "\"end induction\" expected" + end + | _,_ -> anomaly "lonely suppose on stack" + +(* utility for suppose / suppose it is *) + +let close_previous_case pts = + if + Proof_trees.is_complete_proof (proof_of_pftreestate pts) + then + match get_top_stack pts with + Per (et,_,_,_) :: _ -> anomaly "Weird case occured ..." + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (mark_as_done pts) + | _ -> error "Not inside a proof per cases or induction." + else + match get_stack pts with + Per (et,_,_,_) :: _ -> pts + | Suppose_case :: Per (et,_,_,_) :: _ -> + goto_current_focus (mark_as_done (daimon_subtree pts)) + | _ -> error "Not inside a proof per cases or induction." + +(* Proof instructions *) + +(* automation *) + +let filter_hyps f gls = + let filter_aux (id,_,_) = + if f id then + tclIDTAC + else + tclTRY (clear [id]) in + tclMAP filter_aux (Environ.named_context_of_val gls.it.evar_hyps) gls + +let local_hyp_prefix = id_of_string "___" + +let add_justification_hyps keep items gls = + let add_aux c gls= + match kind_of_term c with + Var id -> + keep:=Idset.add id !keep; + tclIDTAC gls + | _ -> + let id=pf_get_new_id local_hyp_prefix gls in + keep:=Idset.add id !keep; + letin_tac false (Names.Name id) c Tacexpr.nowhere gls in + tclMAP add_aux items gls + +let apply_to_prepared_goal items kont gls = + let tokeep = ref Idset.empty in + let auxres = add_justification_hyps tokeep items gls in + tclTHENLIST + [ (fun _ -> auxres); + filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep); + kont ] gls + +let my_automation_tac = ref + (fun gls -> anomaly "No automation registered") + +let register_automation_tac tac = my_automation_tac:= tac + +let automation_tac gls = !my_automation_tac gls + +let justification tac gls= + tclORELSE + (tclSOLVE [tac]) + (fun gls -> + if get_strictness () then + error "insufficient justification" + else + begin + msgnl (str "Warning: insufficient justification"); + daimon_tac gls + end) gls + +let default_justification items gls= + justification (apply_to_prepared_goal items automation_tac) gls + +(* code for have/then/thus/hence *) + +type stackd_elt = +{se_meta:metavariable; + se_type:types; + se_last_meta:metavariable; + se_meta_list:(metavariable*types) list; + se_evd: evar_defs} + +let rec replace_in_list m l = function + [] -> raise Not_found + | c::q -> if m=fst c then l@q else c::replace_in_list m l q + +let enstack_subsubgoals env se stack gls= + let hd,params = decompose_app (special_whd gls se.se_type) in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let process i gentyp = + let constructor = mkConstruct(ind,succ i) + (* constructors numbering*) in + let appterm = applist (constructor,params) in + let apptype = Term.prod_applist gentyp params in + let rc,_ = Reduction.dest_prod env apptype in + let rec meta_aux last lenv = function + [] -> (last,lenv,[]) + | (nam,_,typ)::q -> + let nlast=succ last in + let (llast,holes,metas) = + meta_aux nlast (mkMeta nlast :: lenv) q in + (llast,holes,(nlast,special_nf gls (substl lenv typ))::metas) in + let (nlast,holes,nmetas) = + meta_aux se.se_last_meta [] (List.rev rc) in + let refiner = applist (appterm,List.rev holes) in + let evd = meta_assign se.se_meta refiner se.se_evd in + let ncreated = replace_in_list + se.se_meta nmetas se.se_meta_list in + let evd0 = List.fold_left + (fun evd (m,typ) -> meta_declare m typ evd) evd nmetas in + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_evd=evd0; + se_meta_list=ncreated; + se_last_meta=nlast} stack) (List.rev nmetas) + in + Array.iteri process gentypes + | _ -> () + +let find_subsubgoal env c ctyp skip evd metas gls = + let stack = Stack.create () in + let max_meta = + List.fold_left (fun a (m,_) -> max a m) 0 metas in + let _ = + List.iter (fun (m,typ) -> + Stack.push + {se_meta=m; + se_type=typ; + se_last_meta=max_meta; + se_meta_list=metas; + se_evd=evd} stack) (List.rev metas) in + let rec dfs n = + let se = Stack.pop stack in + try + let unifier = + Unification.w_unify true env Reduction.CUMUL + ctyp se.se_type se.se_evd in + if n <= 0 then + {se with se_evd=meta_assign se.se_meta c unifier} + else + dfs (pred n) + with _ -> + begin + enstack_subsubgoals env se stack gls; + dfs n + end in + let nse= try dfs skip with Stack.Empty -> raise Not_found in + nse.se_meta_list,nse.se_evd + +let rec nf_list evd = + function + [] -> [] + | (m,typ)::others -> + if meta_defined evd m then + nf_list evd others + else + (m,nf_meta evd typ)::nf_list evd others + + +let rec max_linear_context meta_one c = + if !meta_one = None then + if isMeta c then + begin + meta_one:= Some c; + mkMeta 1 + end + else + try + map_constr (max_linear_context meta_one) c + with Not_found -> + begin + meta_one:= Some c; + mkMeta 1 + end + else + if isMeta c then + raise Not_found + else + map_constr (max_linear_context meta_one) c + +let thus_tac c ctyp gls = + let info = get_its_info gls in + let evd0 = mk_evd info.pm_subgoals gls in + let list,evd = + try + find_subsubgoal (pf_env gls) c ctyp 0 evd0 info.pm_subgoals gls + with Not_found -> + error "I could not relate this statement to the thesis" in + let nflist = nf_list evd list in + let nfgoal = nf_meta evd info.pm_partial_goal in +(* let _ = msgnl (str "Partial goal : " ++ + print_constr_env (pf_env gls) nfgoal) in *) + let rgl = ref None in + let refiner = max_linear_context rgl nfgoal in + match !rgl with + None -> exact_check refiner gls + | Some pgl when not (isMeta refiner) -> + let ninfo={info with + pm_partial_goal = pgl; + pm_subgoals = nflist} in + tclTHEN + (Tactics.refine refiner) + (tcl_change_info ninfo) + gls + | _ -> + let ninfo={info with + pm_partial_goal = nfgoal; + pm_subgoals = nflist} in + tcl_change_info ninfo gls + +let anon_id_base = id_of_string "__" + + +let mk_stat_or_thesis info = function + This c -> c + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here" + | Thesis (Sub n) -> + begin + try List.assoc n info.pm_subgoals + with Not_found -> error "No such part in thesis." + end + | Thesis Plain -> + match info.pm_subgoals with + [_,c] -> c + | _ -> error + "\"thesis\" is split, please specify which part you refer to." + +let instr_cut mkstat _thus _then cut gls0 = + let info = get_its_info gls0 in + let just_tac gls = + match cut.cut_by with + Automated l -> + let elems = + if _then then + match info.pm_last with + Anonymous -> l + | Name id -> (mkVar id) ::l + else l in + default_justification elems gls + | By_tactic t -> + justification (Tacinterp.eval_tactic t) gls in + let c_id = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_fact") gls0 + | Name id -> id in + let c_stat = mkstat info cut.cut_stat.st_it in + let thus_tac gls= + if _thus then + thus_tac (mkVar c_id) c_stat gls + else tclIDTAC gls in + let ninfo = {info with pm_last=Name c_id} in + tclTHENS (internal_cut c_id c_stat) + [tclTHEN tcl_erase_info just_tac; + tclTHEN (tcl_change_info ninfo) thus_tac] gls0 + +(* iterated equality *) +let _eq = Libnames.constr_of_reference (Coqlib.glob_eq) + +let decompose_eq id gls = + let typ = pf_get_hyp_typ gls id in + let whd = (special_whd gls typ) in + match kind_of_term whd with + App (f,args)-> + if eq_constr f _eq && (Array.length args)=3 + then (args.(0), + args.(1), + args.(2)) + else error "previous step is not an equality" + | _ -> error "previous step is not an equality" + +let instr_rew _thus rew_side cut gls0 = + let info = get_its_info gls0 in + let last_id = + match info.pm_last with + Anonymous -> error "no previous equality" + | Name id -> id in + let typ,lhs,rhs = decompose_eq last_id gls0 in + let just_tac gls = + match cut.cut_by with + Automated l -> + let elems = (mkVar last_id) :: l in + default_justification elems gls + | By_tactic t -> + justification (Tacinterp.eval_tactic t) gls in + let c_id = match cut.cut_stat.st_label with + Anonymous -> + pf_get_new_id (id_of_string "_eq") gls0 + | Name id -> id in + let ninfo = {info with pm_last=Name c_id} in + let thus_tac new_eq gls= + if _thus then + thus_tac (mkVar c_id) new_eq gls + else tclIDTAC gls in + match rew_side with + Lhs -> + let new_eq = mkApp(_eq,[|typ;cut.cut_stat.st_it;rhs|]) in + tclTHENS (internal_cut c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity lhs) + [just_tac;exact_check (mkVar last_id)]); + tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + | Rhs -> + let new_eq = mkApp(_eq,[|typ;lhs;cut.cut_stat.st_it|]) in + tclTHENS (internal_cut c_id new_eq) + [tclTHEN tcl_erase_info + (tclTHENS (transitivity rhs) + [exact_check (mkVar last_id);just_tac]); + tclTHEN (tcl_change_info ninfo) (thus_tac new_eq)] gls0 + + + +(* tactics for claim/focus *) + +let instr_claim _thus st gls0 = + let info = get_its_info gls0 in + let id = match st.st_label with + Anonymous -> pf_get_new_id (id_of_string "_claim") gls0 + | Name id -> id in + let thus_tac gls= + if _thus then + thus_tac (mkVar id) st.st_it gls + else tclIDTAC gls in + let ninfo1 = {info with + pm_stack= + (if _thus then Focus_claim else Claim)::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,st.st_it]} in + let ninfo2 = {info with pm_last=Name id} in + tclTHENS (internal_cut id st.st_it) + [tcl_change_info ninfo1; + tclTHEN (tcl_change_info ninfo2) thus_tac] gls0 + +(* tactics for assume *) + +let reset_concl gls = + let info = get_its_info gls in + tcl_change_info + {info with + pm_partial_goal=mkMeta 1; + pm_subgoals= [1,gls.it.evar_concl]} gls + +let set_last id gls = + let info = get_its_info gls in + tcl_change_info + {info with + pm_last=Name id} gls + +let intro_pm id gls= + let info = get_its_info gls in + match info.pm_subgoals with + [(_,typ)] -> + tclTHEN (intro_mustbe_force id) reset_concl gls + | _ -> error "Goal is split" + +let push_intro_tac coerce nam gls = + let hid = + match nam with + Anonymous -> pf_get_new_id (id_of_string "_hyp") gls + | Name id -> id in + let mark_id gls0 = + let info = get_its_info gls0 in + let ninfo = {info with + pm_last = Name hid; + pm_hyps = Idset.add hid info.pm_hyps } in + tcl_change_info ninfo gls0 in + tclTHENLIST + [intro_pm hid; + coerce hid; + mark_id] + gls + +let assume_tac hyps gls = + List.fold_right + (fun (Hvar st | Hprop st) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_hyps_or_theses hyps gls = + List.fold_right + (function + (Hvar {st_label=nam;st_it=c} | Hprop {st_label=nam;st_it=This c}) -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,None,c)) nam) + | Hprop {st_label=nam;st_it=Thesis (tk)} -> + tclTHEN + (push_intro_tac + (fun id -> tclIDTAC) nam)) + hyps tclIDTAC gls + +let assume_st hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> convert_hyp (id,None,st.st_it)) st.st_label)) + hyps tclIDTAC gls + +let assume_st_letin hyps gls = + List.fold_right + (fun st -> + tclTHEN + (push_intro_tac + (fun id -> + convert_hyp (id,Some (fst st.st_it),snd st.st_it)) st.st_label)) + hyps tclIDTAC gls + +(* tactics for consider/given *) + +let update_goal_info gls = + let info = get_its_info gls in + match info.pm_subgoals with + [m,_] -> tcl_change_info {info with pm_subgoals =[m,pf_concl gls]} gls + | _ -> error "thesis is split" + +let conjunction_arity id gls = + let typ = pf_get_hyp_typ gls id in + let hd,params = decompose_app (special_whd gls typ) in + let env =pf_env gls in + match kind_of_term hd with + Ind ind when is_good_inductive env ind -> + let mib,oib= + Inductive.lookup_mind_specif env ind in + let gentypes= + Inductive.arities_of_constructors ind (mib,oib) in + let _ = if Array.length gentypes <> 1 then raise Not_found in + let apptype = Term.prod_applist gentypes.(0) params in + let rc,_ = Reduction.dest_prod env apptype in + List.length rc + | _ -> raise Not_found + +let rec intron_then n ids ltac gls = + if n<=0 then + tclTHEN + (fun gls -> + if List.exists (fun id -> occur_id [] id (pf_concl gls)) ids then + update_goal_info gls + else + tclIDTAC gls) + (ltac ids) + gls + else + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (intro_mustbe_force id) + (intron_then (pred n) (id::ids) ltac) gls + +let pm_rename_hyp id hid gls = + if occur_id [] id (pf_concl gls) then + tclTHEN (rename_hyp id hid) update_goal_info gls + else + rename_hyp id hid gls + +let rec consider_match may_intro introduced available expected gls = + match available,expected with + [],[] -> + if not may_intro then + set_last (List.hd introduced) gls + else + let info = get_its_info gls in + let nameset=List.fold_right Idset.add introduced info.pm_hyps in + tcl_change_info {info with + pm_last = Name (List.hd introduced); + pm_hyps = nameset} gls + | _,[] -> error "last statements do not match a complete hypothesis" + (* should tell which ones *) + | [],hyps -> + if may_intro then + begin + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclIFTHENELSE + (intro_pm id) + (consider_match true [] [id] hyps) + (fun _ -> + error "not enough sub-hypotheses to match statements") + gls + end + else + error "not enough sub-hypotheses to match statements" + (* should tell which ones *) + | id::rest_ids,(Hvar st | Hprop st)::rest -> + tclIFTHENELSE (convert_hyp (id,None,st.st_it)) + begin + match st.st_label with + Anonymous -> + consider_match may_intro (id::introduced) rest_ids rest + | Name hid -> + tclTHENLIST + [pm_rename_hyp id hid; + consider_match may_intro (hid::introduced) rest_ids rest] + end + begin + (fun gls -> + let nhyps = + try conjunction_arity id gls with + Not_found -> error "matching hypothesis not found" in + tclTHENLIST + [general_case_analysis (mkVar id,NoBindings); + intron_then nhyps [] + (fun l -> consider_match may_intro introduced + (List.rev_append l rest_ids) expected)] gls) + end + gls + +let consider_tac c hyps gls = + match kind_of_term (strip_outer_cast c) with + Var id -> + consider_match false [] [id] hyps gls + | _ -> + let id = pf_get_new_id (id_of_string "_tmp") gls in + tclTHEN + (forward None (Genarg.IntroIdentifier id) c) + (consider_match false [] [id] hyps) gls + + +let given_tac hyps gls = + consider_match true [] [] hyps gls + +(* tactics for take *) + +let rec take_tac wits gls = + match wits with + [] -> tclIDTAC gls + | wit::rest -> + let typ = pf_type_of gls wit in + tclTHEN (thus_tac wit typ) (take_tac rest) gls + + +(* tactics for define *) + +let rec build_function args body = + match args with + st::rest -> + let pfun= lift 1 (build_function rest body) in + let id = match st.st_label with + Anonymous -> assert false + | Name id -> id in + mkLambda (Name id, st.st_it, subst_term (mkVar id) pfun) + | [] -> body + +let define_tac id args body gls = + let t = build_function args body in + letin_tac true (Name id) t Tacexpr.nowhere gls + +(* tactics for reconsider *) + +let cast_tac id_or_thesis typ gls = + let info = get_its_info gls in + match id_or_thesis with + This id -> + let (_,body,_) = pf_get_hyp gls id in + convert_hyp (id,body,typ) gls + | Thesis (For _ ) -> + error "\"thesis for ...\" is not applicable here" + | Thesis (Sub n) -> + begin + let old_typ = + try List.assoc n info.pm_subgoals + with Not_found -> error "No such part in thesis." in + if is_conv_leq (pf_env gls) (sig_sig gls) typ old_typ then + let new_sg = List.merge + (fun (n,_) (p,_) -> Pervasives.compare n p) + [n,typ] (List.remove_assoc n info.pm_subgoals) in + tcl_change_info {info with pm_subgoals=new_sg} gls + else + error "not convertible" + end + | Thesis Plain -> + match info.pm_subgoals with + [m,c] -> + tclTHEN + (convert_concl typ DEFAULTcast) + (tcl_change_info {info with pm_subgoals= [m,typ]}) gls + | _ -> error + "\"thesis\" is split, please specify which part you refer to." + + +(* per cases *) + +let start_tree env ind = + let constrs = (snd (Inductive.lookup_mind_specif env ind)).mind_consnames in + Split (Idset.empty,ind,Array.map (fun _ -> None) constrs) + +let build_per_info etype casee gls = + let concl=get_thesis gls in + let env=pf_env gls in + let ctyp=pf_type_of gls casee in + let is_dep = dependent casee concl in + let hd,args = decompose_app (special_whd gls ctyp) in + let ind = + try + destInd hd + with _ -> + error "Case analysis must be done on an inductive object" in + let nparams = + let mind = fst (Global.lookup_inductive ind) in + match etype with + ET_Induction -> mind.mind_nparams_rec + | _ -> mind.mind_nparams in + let params,real_args = list_chop nparams args in + let abstract_obj body c = + let typ=pf_type_of gls c in + lambda_create env (typ,subst_term c body) in + let pred= List.fold_left abstract_obj + (lambda_create env (ctyp,subst_term casee concl)) real_args in + is_dep, + {per_casee=casee; + per_ctype=ctyp; + per_ind=ind; + per_pred=pred; + per_args=real_args; + per_params=params; + per_nparams=nparams} + +let per_tac etype casee gls= + let env=pf_env gls in + let info = get_its_info gls in + match casee with + Real c -> + let is_dep,per_info = build_per_info etype c gls in + let ek = + if is_dep then + EK_dep (start_tree env per_info.per_ind) + else EK_unknown in + tcl_change_info + {info with + pm_stack= + Per(etype,per_info,ek,[])::info.pm_stack} gls + | Virtual cut -> + assert (cut.cut_stat.st_label=Anonymous); + let id = pf_get_new_id (id_of_string "_matched") gls in + let c = mkVar id in + let modified_cut = + {cut with cut_stat={cut.cut_stat with st_label=Name id}} in + tclTHEN + (instr_cut (fun _ c -> c) false false modified_cut) + (fun gls0 -> + let is_dep,per_info = build_per_info etype c gls0 in + assert (not is_dep); + tcl_change_info + {info with pm_stack= + Per(etype,per_info,EK_unknown,[])::info.pm_stack} gls0) + gls + +(* suppose *) + +let rec build_product args body = + match args with + (Hprop st| Hvar st )::rest -> + let pprod= lift 1 (build_product rest body) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_term (mkVar id) pprod in + mkProd (st.st_label, st.st_it, lbody) + | [] -> body + +let register_nodep_subcase id= function + Per(et,pi,ek,clauses)::s -> + begin + match ek with + EK_unknown -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_nodep -> clauses,Per(et,pi,EK_nodep,id::clauses)::s + | EK_dep _ -> error "Do not mix \"suppose\" with \"suppose it is\"." + end + | _ -> anomaly "wrong stack state" + +let suppose_tac hyps gls0 = + let info = get_its_info gls0 in + let thesis = get_thesis gls0 in + let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let clause = build_product hyps thesis in + let ninfo1 = {info with + pm_stack=Suppose_case::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,clause]} in + let old_clauses,stack = register_nodep_subcase id info.pm_stack in + let ninfo2 = {info with + pm_stack=stack} in + tclTHENS (internal_cut id clause) + [tclTHENLIST [tcl_change_info ninfo1; + assume_tac hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* suppose it is ... *) + +(* pattern matching compiling *) + +let rec nb_prod_after n c= + match kind_of_term c with + | Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else + 1+(nb_prod_after 0 b) + | _ -> 0 + +let constructor_arities env ind = + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let constr_types = Inductiveops.arities_of_constructors env ind in + let hyp = nb_prod_after nparams in + Array.map hyp constr_types + +let rec n_push rest ids n = + if n<=0 then Pop rest else Push (ids,n_push rest ids (pred n)) + +let explode_branches ids env ind rest= + Array.map (fun n -> Some (Idset.empty,n_push rest ids n)) (constructor_arities env ind) + +let rec tree_of_pats env ((id,_) as cpl) pats = + match pats with + [] -> End_of_branch cpl + | args::stack -> + match args with + [] -> Pop (tree_of_pats env cpl stack) + | patt :: rest_args -> + match patt with + PatVar (_,v) -> + Push (Idset.singleton id, + tree_of_pats env cpl (rest_args::stack)) + | PatCstr (_,(ind,cnum),args,nam) -> + let _,mind = Inductive.lookup_mind_specif env ind in + let br= Array.map (fun _ -> None) mind.mind_consnames in + br.(pred cnum) <- + Some (Idset.singleton id, + tree_of_pats env cpl (args::rest_args::stack)); + Split(Idset.empty,ind,br) + +let rec add_branch env ((id,_) as cpl) pats tree= + match pats with + [] -> + begin + match tree with + End_of_branch cpl0 -> End_of_branch cpl0 + (* this ensures precedence *) + | _ -> anomaly "tree is expected to end here" + end + | args::stack -> + match args with + [] -> + begin + match tree with + Pop t -> Pop (add_branch env cpl stack t) + | _ -> anomaly "we should pop here" + end + | patt :: rest_args -> + match patt with + PatVar (_,v) -> + begin + match tree with + Push (ids,t) -> + Push (Idset.add id ids, + add_branch env cpl (rest_args::stack) t) + | Split (ids,ind,br) -> + Split (Idset.add id ids, + ind,array_map2 + (append_branch env cpl 1 + (rest_args::stack)) + (constructor_arities env ind) br) + | _ -> anomaly "No pop/stop expected here" + end + | PatCstr (_,(ind,cnum),args,nam) -> + match tree with + Push (ids,t) -> + let br = explode_branches ids env ind t in + let _ = + br.(pred cnum)<- + option_map + (fun (ids,tree) -> + Idset.add id ids, + add_branch env cpl + (args::rest_args::stack) tree) + br.(pred cnum) in + Split (ids,ind,br) + | Split (ids,ind0,br0) -> + if (ind <> ind0) then error + (* this can happen with coercions *) + "Case pattern belongs to wrong inductive type"; + let br=Array.copy br0 in + let ca = constructor_arities env ind in + let _= br.(pred cnum)<- + append_branch env cpl 0 (args::rest_args::stack) + ca.(pred cnum) br.(pred cnum) in + Split (ids,ind,br) + | _ -> anomaly "No pop/stop expected here" +and append_branch env ((id,_) as cpl) depth pats nargs = function + Some (ids,tree) -> + Some (Idset.add id ids,append_tree env cpl depth pats tree) + | None -> + Some (* (n_push (tree_of_pats env cpl pats) + (Idset.singleton id) nargs) *) + (Idset.singleton id,tree_of_pats env cpl pats) +and append_tree env ((id,_) as cpl) depth pats tree = + if depth<=0 then add_branch env cpl pats tree + else match tree with + Pop t -> Pop (append_tree env cpl (pred depth) pats t) + | Push (ids,t) -> Push (Idset.add id ids, + append_tree env cpl depth pats t) + | End_of_branch _ -> anomaly "Premature end of branch" + | Split (ids,ind,branches) -> + Split (Idset.add id ids,ind, + array_map2 + (append_branch env cpl (succ depth) pats) + (constructor_arities env ind) + branches) + +(* suppose it is *) + +let rec st_assoc id = function + [] -> raise Not_found + | st::_ when st.st_label = id -> st.st_it + | _ :: rest -> st_assoc id rest + +let thesis_for obj typ per_info env= + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + let ind = destInd cind in + let _ = if ind <> per_info.per_ind then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong inductive type)") in + let params,args = list_chop per_info.per_nparams all_args in + let _ = if not (List.for_all2 eq_constr params per_info.per_params) then + errorlabstrm "thesis_for" + ((Printer.pr_constr_env env obj) ++ spc () ++ + str "cannot give an induction hypothesis (wrong parameters)") in + let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in + compose_prod rc (whd_beta hd2) + +let rec build_product_dep pat_info per_info args body gls = + match args with + (Hprop {st_label=nam;st_it=This c} + | Hvar {st_label=nam;st_it=c})::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match nam with + Anonymous -> body + | Name id -> subst_var id pprod in + mkProd (nam,c,lbody) + | Hprop ({st_it=Thesis tk} as st)::rest -> + let pprod= + lift 1 (build_product_dep pat_info per_info rest body gls) in + let lbody = + match st.st_label with + Anonymous -> body + | Name id -> subst_var id pprod in + let ptyp = + match tk with + For id -> + let obj = mkVar id in + let typ = + try st_assoc (Name id) pat_info.pat_vars + with Not_found -> + snd (st_assoc (Name id) pat_info.pat_aliases) in + thesis_for obj typ per_info (pf_env gls) + | Plain -> get_thesis gls + | Sub n -> anomaly "Subthesis in cases" in + mkProd (st.st_label,ptyp,lbody) + | [] -> body + +let build_dep_clause params pat_info per_info hyps gls = + let concl= + thesis_for pat_info.pat_constr pat_info.pat_typ per_info (pf_env gls) in + let open_clause = + build_product_dep pat_info per_info hyps concl gls in + let prod_one st body = + match st.st_label with + Anonymous -> mkProd(Anonymous,st.st_it,lift 1 body) + | Name id -> mkNamedProd id st.st_it (lift 1 body) in + let let_one_in st body = + match st.st_label with + Anonymous -> mkLetIn(Anonymous,fst st.st_it,snd st.st_it,lift 1 body) + | Name id -> + mkNamedLetIn id (fst st.st_it) (snd st.st_it) (lift 1 body) in + let aliased_clause = + List.fold_right let_one_in pat_info.pat_aliases open_clause in + List.fold_right prod_one (params@pat_info.pat_vars) aliased_clause + +let rec register_dep_subcase id env per_info pat = function + EK_nodep -> error "Only \"suppose it is\" can be used here." + | EK_unknown -> + register_dep_subcase id env per_info pat + (EK_dep (start_tree env per_info.per_ind)) + | EK_dep tree -> EK_dep (add_branch env id [[pat]] tree) + +let case_tac params pat_info hyps gls0 = + let info = get_its_info gls0 in + let id = pf_get_new_id (id_of_string "_subcase") gls0 in + let et,per_info,ek,old_clauses,rest = + match info.pm_stack with + Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest) + | _ -> anomaly "wrong place for cases" in + let clause = build_dep_clause params pat_info per_info hyps gls0 in + let ninfo1 = {info with + pm_stack=Suppose_case::info.pm_stack; + pm_partial_goal=mkMeta 1; + pm_subgoals = [1,clause]} in + let nek = + register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info + pat_info.pat_pat ek in + let ninfo2 = {info with + pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in + tclTHENS (internal_cut id clause) + [tclTHENLIST + [tcl_change_info ninfo1; + assume_st (params@pat_info.pat_vars); + assume_st_letin pat_info.pat_aliases; + assume_hyps_or_theses hyps; + clear old_clauses]; + tcl_change_info ninfo2] gls0 + +(* end cases *) + +type instance_stack = + (constr option*bool*(constr list) list) list + +let initial_instance_stack ids = + List.map (fun id -> id,[None,false,[]]) ids + +let push_one_arg arg = function + [] -> anomaly "impossible" + | (head,is_rec,args) :: ctx -> + ((head,is_rec,(arg::args)) :: ctx) + +let push_arg arg stacks = + List.map (fun (id,stack) -> (id,push_one_arg arg stack)) stacks + + +let push_one_head c is_rec ids (id,stack) = + let head = if Idset.mem id ids then Some c else None in + id,(head,is_rec,[]) :: stack + +let push_head c is_rec ids stacks = + List.map (push_one_head c is_rec ids) stacks + +let pop_one rec_flag (id,stack) = + let nstack= + match stack with + [] -> anomaly "impossible" + | [c] as l -> l + | (Some head,is_rec,args)::(head0,is_rec0,args0)::ctx -> + let arg = applist (head,(List.rev args)) in + rec_flag:= !rec_flag || is_rec; + (head0,is_rec0,(arg::args0))::ctx + | (None,is_rec,args)::(head0,is_rec0,args0)::ctx -> + rec_flag:= !rec_flag || is_rec; + (head0,is_rec0,(args@args0))::ctx + in id,nstack + +let pop_stacks stacks = + let rec_flag= ref false in + let nstacks = List.map (pop_one rec_flag) stacks in + !rec_flag , nstacks + +let patvar_base = id_of_string "__" + +let test_fun (str:string) = () + +let hrec_for obj_id fix_id per_info gls= + let obj=mkVar obj_id in + let typ=pf_get_hyp_typ gls obj_id in + let rc,hd1=decompose_prod typ in + let cind,all_args=decompose_app typ in + match kind_of_term cind with + Ind ind when ind=per_info.per_ind -> + let params,args= list_chop per_info.per_nparams all_args in + if try + (List.for_all2 eq_constr params per_info.per_params) + with Invalid_argument _ -> false then + let hd2 = applist (mkVar fix_id,args@[obj]) in + Some (compose_lam rc (whd_beta hd2)) + else None + | _ -> None + +let rec execute_cases at_top fix_name per_info kont0 stacks tree gls = + match tree with + Pop t -> + let is_rec,nstacks = pop_stacks stacks in + if is_rec then + let _ = test_fun "is_rec=true" in + let c_id = pf_get_new_id (id_of_string "_hrec") gls in + tclTHEN + (intro_mustbe_force c_id) + (execute_cases false fix_name per_info kont0 nstacks t) gls + else + execute_cases false fix_name per_info kont0 nstacks t gls + | Push (_,t) -> + let id = pf_get_new_id patvar_base gls in + let nstacks = push_arg (mkVar id) stacks in + let kont = execute_cases false fix_name per_info kont0 nstacks t in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont + | Name fix_id -> + (fun gls -> + if at_top then + kont gls + else + match hrec_for id fix_id per_info gls with + None -> kont gls + | Some c_obj -> + let c_id = + pf_get_new_id (id_of_string "_hrec") gls in + tclTHENLIST + [generalize [c_obj]; + intro_mustbe_force c_id; + kont] gls) + end gls + | Split(ids,ind,br) -> + let (_,typ,_)=destProd (pf_concl gls) in + let hd,args=decompose_app (special_whd gls typ) in + let _ = assert (ind = destInd hd) in + let nparams = (fst (Global.lookup_inductive ind)).mind_nparams in + let params = list_firstn nparams args in + let constr i =applist (mkConstruct(ind,succ i),params) in + let next_tac is_rec i = function + Some (sub_ids,tree) -> + let br_stacks = + List.filter (fun (id,_) -> Idset.mem id sub_ids) stacks in + let p_stacks = + push_head (constr i) is_rec ids br_stacks in + execute_cases false fix_name per_info kont0 p_stacks tree + | None -> + msgnl (str "Warning : missing case"); + kont0 (mkMeta 1) + in + let id = pf_get_new_id patvar_base gls in + let kont is_rec = + tclTHENSV + (general_case_analysis (mkVar id,NoBindings)) + (Array.mapi (next_tac is_rec) br) in + tclTHEN + (intro_mustbe_force id) + begin + match fix_name with + Anonymous -> kont false + | Name fix_id -> + (fun gls -> + if at_top then + kont false gls + else + match hrec_for id fix_id per_info gls with + None -> kont false gls + | Some c_obj -> + tclTHENLIST + [generalize [c_obj]; + kont true] gls) + end gls + | End_of_branch (id,nhyps) -> + match List.assoc id stacks with + [None,_,args] -> + let metas = list_tabulate (fun n -> mkMeta (succ n)) nhyps in + kont0 (applist (mkVar id,List.rev_append args metas)) gls + | _ -> anomaly "wrong stack size" + +let end_tac et2 gls = + let info = get_its_info gls in + let et1,pi,ek,clauses = + match info.pm_stack with + Suppose_case::_ -> + anomaly "This case should already be trapped" + | Claim::_ -> + error "\"end claim\" expected." + | Focus_claim::_ -> + error "\"end focus\" expected." + | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) + | [] -> + anomaly "This case should already be trapped" in + let et = + if et1 <> et2 then + match et1 with + ET_Case_analysis -> + error "\"end cases\" expected." + | ET_Induction -> + error "\"end induction\" expected." + else et1 in + tclTHEN + tcl_erase_info + begin + match et,ek with + _,EK_unknown -> + tclSOLVE [simplest_elim pi.per_casee] + | ET_Case_analysis,EK_nodep -> + tclTHEN + (general_case_analysis (pi.per_casee,NoBindings)) + (default_justification (List.map mkVar clauses)) + | ET_Induction,EK_nodep -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + simple_induct (AnonHyp (succ (List.length pi.per_args))); + default_justification (List.map mkVar clauses)] + | ET_Case_analysis,EK_dep tree -> + tclTHENLIST + [generalize (pi.per_args@[pi.per_casee]); + execute_cases true Anonymous pi + (fun c -> tclTHENLIST + [refine c; + clear clauses; + justification assumption]) + (initial_instance_stack clauses) tree] + | ET_Induction,EK_dep tree -> + tclTHEN (generalize (pi.per_args@[pi.per_casee])) + begin + fun gls0 -> + let fix_id = pf_get_new_id (id_of_string "_fix") gls0 in + tclTHEN + (fix (Some fix_id) (succ (List.length pi.per_args))) + (execute_cases true (Name fix_id) pi + (fun c -> + tclTHENLIST + [clear [fix_id]; + refine c; + clear clauses; + justification assumption + (* justification automation_tac *)]) + (initial_instance_stack clauses) tree) gls0 + end + end gls + +(* escape *) + +let rec abstract_metas n avoid head = function + [] -> 1,head,[] + | (meta,typ)::rest -> + let id = Nameops.next_ident_away (id_of_string "_sbgl") avoid in + let p,term,args = abstract_metas (succ n) (id::avoid) head rest in + succ p,mkLambda(Name id,typ,subst_meta [meta,mkRel p] term), + (mkMeta n)::args + +let build_refining_context gls = + let info = get_its_info gls in + let avoid=pf_ids_of_hyps gls in + let _,fn,args=abstract_metas 1 avoid info.pm_partial_goal info.pm_subgoals in + applist (fn,args) + +let escape_command pts = + let pts1 = nth_unproven 1 pts in + let gls = top_goal_of_pftreestate pts1 in + let term = build_refining_context gls in + let tac = tclTHEN + (abstract_operation (Proof_instr (true,{emph=0;instr=Pescape})) tcl_erase_info) + (Tactics.refine term) in + traverse 1 (solve_pftreestate tac pts1) + +(* General instruction engine *) + +let rec do_proof_instr_gen _thus _then instr = + match instr with + Pthus i -> + assert (not _thus); + do_proof_instr_gen true _then i + | Pthen i -> + assert (not _then); + do_proof_instr_gen _thus true i + | Phence i -> + assert (not (_then || _thus)); + do_proof_instr_gen true true i + | Pcut c -> + instr_cut mk_stat_or_thesis _thus _then c + | Prew (s,c) -> + assert (not _then); + instr_rew _thus s c + | Pconsider (c,hyps) -> consider_tac c hyps + | Pgiven hyps -> given_tac hyps + | Passume hyps -> assume_tac hyps + | Plet hyps -> assume_tac hyps + | Pclaim st -> instr_claim false st + | Pfocus st -> instr_claim true st + | Ptake witl -> take_tac witl + | Pdefine (id,args,body) -> define_tac id args body + | Pcast (id,typ) -> cast_tac id typ + | Pper (et,cs) -> per_tac et cs + | Psuppose hyps -> suppose_tac hyps + | Pcase (params,pat_info,hyps) -> case_tac params pat_info hyps + | Pend (B_elim et) -> end_tac et + | Pend _ | Pescape -> anomaly "Not applicable" + +let eval_instr {instr=instr} = + do_proof_instr_gen false false instr + +let rec preprocess pts instr = + match instr with + Phence i |Pthus i | Pthen i -> preprocess pts i + | Pcut _ | Passume _ | Plet _ | Pclaim _ | Pfocus _ + | Pconsider (_,_) | Pcast (_,_) | Pgiven _ | Ptake _ + | Pdefine (_,_,_) | Pper _ | Prew _ -> + check_not_per pts; + true,pts + | Pescape -> + check_not_per pts; + false,pts + | Pcase _ | Psuppose _ | Pend (B_elim _) -> + true,close_previous_case pts + | Pend bt -> + false,close_block bt pts + +let rec postprocess pts instr = + match instr with + Phence i | Pthus i | Pthen i -> postprocess pts i + | Pcut _ | Passume _ | Plet _ | Pconsider (_,_) | Pcast (_,_) + | Pgiven _ | Ptake _ | Pdefine (_,_,_) | Prew (_,_) -> pts + | Pclaim _ | Pfocus _ | Psuppose _ | Pcase _ | Pper _ -> nth_unproven 1 pts + | Pescape -> + escape_command pts + | Pend _ -> + goto_current_focus_or_top (mark_as_done pts) + +let do_instr raw_instr pts = + let has_tactic,pts1 = preprocess pts raw_instr.instr in + let pts2 = + if has_tactic then + let gl = nth_goal_of_pftreestate 1 pts1 in + let env= pf_env gl in + let sigma= project gl in + let ist = {ltacvars = ([],[]); ltacrecvars = []; + gsigma = sigma; genv = env} in + let glob_instr = intern_proof_instr ist raw_instr in + let instr = + interp_proof_instr (get_its_info gl) sigma env glob_instr in + let lock_focus = is_focussing_instr instr.instr in + let marker= Proof_instr (lock_focus,instr) in + solve_nth_pftreestate 1 + (abstract_operation marker (eval_instr instr)) pts1 + else pts1 in + postprocess pts2 raw_instr.instr + +let proof_instr raw_instr = + Pfedit.mutate (do_instr raw_instr) + +(* + +(* STUFF FOR ITERATED RELATIONS *) +let decompose_bin_app t= + let hd,args = destApp + +let identify_transitivity_lemma c = + let varx,tx,c1 = destProd c in + let vary,ty,c2 = destProd (pop c1) in + let varz,tz,c3 = destProd (pop c2) in + let _,p1,c4 = destProd (pop c3) in + let _,lp2,lp3 = destProd (pop c4) in + let p2=pop lp2 in + let p3=pop lp3 in +*) + diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli new file mode 100644 index 00000000..ba8dc7b6 --- /dev/null +++ b/tactics/decl_proof_instr.mli @@ -0,0 +1,118 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id:$ *) + +open Refiner +open Names +open Term +open Tacmach + +val go_to_proof_mode: unit -> unit +val return_from_tactic_mode: unit -> unit + +val register_automation_tac: tactic -> unit + +val automation_tac : tactic + +val daimon_subtree: pftreestate -> pftreestate + +val do_instr: Decl_expr.raw_proof_instr -> pftreestate -> pftreestate +val proof_instr: Decl_expr.raw_proof_instr -> unit + +val tcl_change_info : Decl_mode.pm_info -> tactic + +val mark_proof_tree_as_done : Proof_type.proof_tree -> Proof_type.proof_tree + +val mark_as_done : pftreestate -> pftreestate + +val execute_cases : bool -> + Names.name -> + Decl_mode.per_info -> + (Term.constr -> Proof_type.tactic) -> + (Names.Idset.elt * (Term.constr option * bool * Term.constr list) list) + list -> + Decl_mode.split_tree -> Proof_type.tactic + +val tree_of_pats : + Environ.env -> + Names.Idset.elt * int -> + Rawterm.cases_pattern list list -> Decl_mode.split_tree +val add_branch : + Environ.env -> + Names.Idset.elt * int -> + Rawterm.cases_pattern list list -> + Decl_mode.split_tree -> Decl_mode.split_tree +val append_branch : + Environ.env -> + Names.Idset.elt * int -> + int -> + Rawterm.cases_pattern list list -> + int -> + (Names.Idset.t * Decl_mode.split_tree) option -> + (Names.Idset.t * Decl_mode.split_tree) option + +val append_tree : Environ.env -> + Names.Idset.elt * int -> + int -> + Rawterm.cases_pattern list list -> + Decl_mode.split_tree -> Decl_mode.split_tree + +val build_dep_clause : Term.types Decl_expr.statement list -> + Decl_expr.proof_pattern -> + Decl_mode.per_info -> + (Term.types Decl_expr.statement, Term.types Decl_expr.or_thesis) + Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types + +val register_dep_subcase : + Names.identifier * int -> + Environ.env -> + Decl_mode.per_info -> + Rawterm.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind + +val thesis_for : Term.constr -> + Term.constr -> Decl_mode.per_info -> Environ.env -> Term.constr + +val close_previous_case : pftreestate -> pftreestate + +val test_fun : string -> unit + + +val pop_stacks : + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list -> + bool * + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list + + +val push_head : Term.constr -> + bool -> + Names.Idset.t -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list + +val push_arg : Term.constr -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list -> + (Names.identifier * + (Term.constr option * bool * Term.constr list) list) list + +val hrec_for: + Names.identifier -> + Names.identifier -> + Decl_mode.per_info -> Proof_type.goal Tacmach.sigma -> Term.constr option + +val consider_match : + bool -> + Names.Idset.elt list -> + Names.Idset.elt list -> + (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list -> + Proof_type.tactic diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 32abc347..6da0dd49 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: eauto.ml4 8878 2006-05-30 16:44:25Z herbelin $ *) +(* $Id: eauto.ml4 9277 2006-10-25 13:02:22Z herbelin $ *) open Pp open Util @@ -46,7 +46,7 @@ END let e_resolve_with_bindings_tac (c,lbind) gl = let t = pf_hnf_constr gl (pf_type_of gl c) in - let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in + let clause = make_clenv_binding_apply gl None (c,t) lbind in Clenvtac.e_res_pf clause gl let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls diff --git a/tactics/equality.ml b/tactics/equality.ml index f05c3882..2526c84e 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 9010 2006-07-05 07:17:41Z jforest $ *) +(* $Id: equality.ml 9211 2006-10-05 12:38:33Z letouzey $ *) open Pp open Util @@ -82,34 +82,34 @@ let elimination_sort_of_clause = function *) let general_rewrite_bindings_clause cls lft2rgt (c,l) gl = - let ctype = pf_type_of gl c in + let ctype = pf_apply get_type_of gl c in (* A delta-reduction would be here too strong, since it would break search for a defined setoid relation in head position. *) let t = snd (decompose_prod (whd_betaiotazeta ctype)) in let head = if isApp t then fst (destApp t) else t in - if relation_table_mem head && l = NoBindings then - general_s_rewrite_clause cls lft2rgt c [] gl - else - (* Original code. In particular, [splay_prod] performs delta-reduction. *) - let env = pf_env gl in - let sigma = project gl in - let _,t = splay_prod env sigma t in - match match_with_equation t with - | None -> - if l = NoBindings - then general_s_rewrite_clause cls lft2rgt c [] gl - else error "The term provided does not end with an equation" - | Some (hdcncl,_) -> - let hdcncls = string_of_inductive hdcncl in - let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in - let dir = if cls=None then lft2rgt else not lft2rgt in - let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in - let elim = - try pf_global gl (id_of_string rwr_thm) - with Not_found -> - error ("Cannot find rewrite principle "^rwr_thm) - in - general_elim_clause cls (c,l) (elim,NoBindings) gl + if relation_table_mem head && l = NoBindings then + general_s_rewrite_clause cls lft2rgt c [] gl + else + (* Original code. In particular, [splay_prod] performs delta-reduction. *) + let env = pf_env gl in + let sigma = project gl in + let _,t = splay_prod env sigma t in + match match_with_equation t with + | None -> + if l = NoBindings + then general_s_rewrite_clause cls lft2rgt c [] gl + else error "The term provided does not end with an equation" + | Some (hdcncl,_) -> + let hdcncls = string_of_inductive hdcncl in + let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in + let dir = if cls=None then lft2rgt else not lft2rgt in + let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in + let elim = + try pf_global gl (id_of_string rwr_thm) + with Not_found -> + error ("Cannot find rewrite principle "^rwr_thm) + in + general_elim_clause cls (c,l) (elim,NoBindings) gl let general_rewrite_bindings = general_rewrite_bindings_clause None let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings) @@ -119,36 +119,39 @@ let general_rewrite_bindings_in l2r id = let general_rewrite_in l2r id c = general_rewrite_bindings_clause (Some id) l2r (c,NoBindings) - let general_multi_rewrite l2r c cl = - let rec do_hyps = function - | [] -> tclIDTAC - | ((_,id),_) :: l -> - tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l) - in - let rec try_do_hyps = function - | [] -> tclIDTAC - | id :: l -> - tclTHENFIRST - (tclTRY (general_rewrite_bindings_in l2r id c)) - (try_do_hyps l) - in if cl.concl_occs <> [] then - error "The \"at\" syntax isn't available yet for the rewrite tactic" - else - tclTHENFIRST - (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC) - (match cl.onhyps with - | Some l -> do_hyps l - | None -> - fun gl -> - (* try to rewrite in all hypothesis - (except maybe the rewritten one) *) - let ids = match kind_of_term (fst c) with - | Var id -> list_remove id (pf_ids_of_hyps gl) - | _ -> pf_ids_of_hyps gl - in try_do_hyps ids gl) - + error "The \"at\" syntax isn't available yet for the rewrite/replace tactic" + else match cl.onhyps with + | Some l -> + (* If a precise list of locations is given, success is mandatory for + each of these locations. *) + let rec do_hyps = function + | [] -> tclIDTAC + | ((_,id),_) :: l -> + tclTHENFIRST (general_rewrite_bindings_in l2r id c) (do_hyps l) + in + if not cl.onconcl then do_hyps l + else tclTHENFIRST (general_rewrite_bindings l2r c) (do_hyps l) + | None -> + (* Otherwise, if we are told to rewrite in all hypothesis via the + syntax "* |-", we fail iff all the different rewrites fail *) + let rec do_hyps_atleastonce = function + | [] -> (fun gl -> error "Nothing to rewrite.") + | id :: l -> + tclIFTHENTRYELSEMUST + (general_rewrite_bindings_in l2r id c) + (do_hyps_atleastonce l) + in + let do_hyps gl = + (* If the term to rewrite is an hypothesis, don't rewrite in itself *) + let ids = match kind_of_term (fst c) with + | Var id -> list_remove id (pf_ids_of_hyps gl) + | _ -> pf_ids_of_hyps gl + in do_hyps_atleastonce ids gl + in + if not cl.onconcl then do_hyps + else tclIFTHENTRYELSEMUST (general_rewrite_bindings l2r c) do_hyps (* Conditional rewriting, the success of a rewriting is related to the resolution of the conditions by a given tactic *) @@ -182,9 +185,14 @@ let rewriteRL_clause = function tac : Used to prove the equality c1 = c2 gl : goal *) -let abstract_replace clause c2 c1 unsafe tac gl = - let t1 = pf_type_of gl c1 - and t2 = pf_type_of gl c2 in +let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = + let try_prove_eq = + match try_prove_eq_opt with + | None -> tclIDTAC + | Some tac -> tclTRY (tclCOMPLETE tac) + in + let t1 = pf_apply get_type_of gl c1 + and t2 = pf_apply get_type_of gl c2 in if unsafe or (pf_conv_x gl t1 t2) then let e = build_coq_eq () in let sym = build_coq_sym_eq () in @@ -192,34 +200,28 @@ let abstract_replace clause c2 c1 unsafe tac gl = tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (tclTRY (rewriteRL_clause clause (mkVar id,NoBindings))) + (tclTRY (general_multi_rewrite false (mkVar id,NoBindings) clause)) (clear [id])); tclFIRST [assumption; tclTHEN (apply sym) assumption; - tclTRY (tclCOMPLETE tac) + try_prove_eq ] ] gl else error "terms do not have convertible types" + +let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl -let replace c2 c1 gl = abstract_replace None c2 c1 false tclIDTAC gl - -let replace_in id c2 c1 gl = abstract_replace (Some id) c2 c1 false tclIDTAC gl +let replace_in id c2 c1 gl = multi_replace (onHyp id) c2 c1 false None gl -let replace_by c2 c1 tac gl = abstract_replace None c2 c1 false tac gl +let replace_by c2 c1 tac gl = multi_replace onConcl c2 c1 false (Some tac) gl -let replace_in_by id c2 c1 tac gl = abstract_replace (Some id) c2 c1 false tac gl +let replace_in_by id c2 c1 tac gl = multi_replace (onHyp id) c2 c1 false (Some tac) gl - -let new_replace c2 c1 id tac_opt gl = - let tac = - match tac_opt with - | Some tac -> tac - | _ -> tclIDTAC - in - abstract_replace id c2 c1 false tac gl +let replace_in_clause_maybe_by c2 c1 cl tac_opt gl = + multi_replace cl c2 c1 false tac_opt gl (* End of Eduardo's code. The rest of this file could be improved using the functions match_with_equation, etc that I defined @@ -269,24 +271,27 @@ exception DiscrFound of (constructor * int) list * constructor * constructor let find_positions env sigma t1 t2 = - let rec findrec posn t1 t2 = + let rec findrec sorts posn t1 t2 = let hd1,args1 = whd_betadeltaiota_stack env sigma t1 in let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with | Construct sp1, Construct sp2 when List.length args1 = mis_constructor_nargs_env env sp1 - -> - (* both sides are fully applied constructors, so either we descend, - or we can discriminate here. *) + -> + let sorts = list_intersect sorts (allowed_sorts env (fst sp1)) in + (* both sides are fully applied constructors, so either we descend, + or we can discriminate here. *) if sp1 = sp2 then + let nrealargs = constructor_nrealargs env sp1 in + let rargs1 = list_lastn nrealargs args1 in + let rargs2 = list_lastn nrealargs args2 in List.flatten - (list_map2_i - (fun i arg1 arg2 -> - findrec ((sp1,i)::posn) arg1 arg2) - 0 args1 args2) - else - raise (DiscrFound(List.rev posn,sp1,sp2)) + (list_map2_i (fun i -> findrec sorts ((sp1,i)::posn)) + 0 rargs1 rargs2) + else if List.mem InType sorts then (* see build_discriminator *) + raise (DiscrFound (List.rev posn,sp1,sp2)) + else [] | _ -> let t1_0 = applist (hd1,args1) @@ -295,14 +300,13 @@ let find_positions env sigma t1 t2 = [] else let ty1_0 = get_type_of env sigma t1_0 in - match get_sort_family_of env sigma ty1_0 with - | InSet | InType -> [(List.rev posn,t1_0,t2_0)] - | InProp -> [] - in - (try - Inr(findrec [] t1 t2) - with DiscrFound (path,c1,c2) -> - Inl (path,c1,c2)) + let s = get_sort_family_of env sigma ty1_0 in + if List.mem s sorts then [(List.rev posn,t1_0,t2_0)] else [] in + try + (* Rem: to allow injection on proofs objects, just add InProp *) + Inr (findrec [InSet;InType] [] t1 t2) + with DiscrFound (path,c1,c2) -> + Inl (path,c1,c2) let discriminable env sigma t1 t2 = match find_positions env sigma t1 t2 with @@ -371,6 +375,7 @@ let discriminable env sigma t1 t2 = the continuation then constructs the case-split. *) + let descend_then sigma env head dirn = let IndType (indf,_) = try find_rectype env sigma (get_type_of env sigma head) @@ -383,9 +388,7 @@ let descend_then sigma env head dirn = (dirn_nlams, dirn_env, (fun dirnval (dfltval,resty) -> - let arsign,_ = get_arity env indf in - let depind = build_dependent_inductive env indf in - let deparsign = (Anonymous,None,depind)::arsign in + let deparsign = make_arity_signature env true indf in let p = it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in let build_branch i = @@ -416,7 +419,7 @@ let descend_then sigma env head dirn = let construct_discriminator sigma env dirn c sort = let IndType(indf,_) = - try find_rectype env sigma (type_of env sigma c) + try find_rectype env sigma (get_type_of env sigma c) with Not_found -> (* one can find Rel(k) in case of dependent constructors like T := c : (A:Set)A->T and a discrimination @@ -428,10 +431,8 @@ let construct_discriminator sigma env dirn c sort = dependent types") in let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in - let arsign,arsort = get_arity env indf in let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in - let depind = build_dependent_inductive env indf in - let deparsign = (Anonymous,None,depind)::arsign in + let deparsign = make_arity_signature env true indf in let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in let cstrs = get_constructors env indf in let build_branch i = @@ -445,17 +446,22 @@ let construct_discriminator sigma env dirn c sort = let rec build_discriminator sigma env dirn c sort = function | [] -> construct_discriminator sigma env dirn c sort | ((sp,cnum),argnum)::l -> - let cty = type_of env sigma c in - let IndType (indf,_) = - try find_rectype env sigma cty with Not_found -> assert false in - let (ind,_) = dest_ind_family indf in - let (mib,mip) = lookup_mind_specif env ind in - let nparams = mib.mind_nparams in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in - let newc = mkRel(cnum_nlams-(argnum-nparams)) in + let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator sigma cnum_env dirn newc sort l in kont subval (build_coq_False (),mkSort (Prop Null)) +(* Note: discrimination could be more clever: if some elimination is + not allowed because of a large impredicative constructor in the + path (see allowed_sorts in find_positions), the positions could + still be discrimated by projecting first instead of putting the + discrimination combinator inside the projecting combinator. Example + of relevant situation: + + Inductive t:Set := c : forall A:Set, A -> nat -> t. + Goal ~ c _ 0 0 = c _ 0 1. intro. discriminate H. +*) + let gen_absurdity id gl = if is_empty_type (clause_type (onHyp id) gl) then @@ -466,12 +472,12 @@ let gen_absurdity id gl = (* Precondition: eq is leibniz equality - returns ((eq_elim t t1 P i t2), absurd_term) - where P=[e:t]discriminator - absurd_term=False + returns ((eq_elim t t1 P i t2), absurd_term) + where P=[e:t]discriminator + absurd_term=False *) -let discrimination_pf e (t,t1,t2) discriminator lbeq gls = +let discrimination_pf e (t,t1,t2) discriminator lbeq = let i = build_coq_I () in let absurd_term = build_coq_False () in let eq_elim = lbeq.ind in @@ -479,28 +485,28 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls = exception NotDiscriminable -let discrEq (lbeq,(t,t1,t2)) id gls = - let sort = pf_type_of gls (pf_concl gls) in +let eq_baseid = id_of_string "e" + +let discr_positions env sigma (lbeq,(t,t1,t2)) id cpath dirn sort = + let e = next_ident_away eq_baseid (ids_of_context env) in + let e_env = push_named (e,None,t) env in + let discriminator = + build_discriminator sigma e_env dirn (mkVar e) sort cpath in + let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in + tclCOMPLETE + ((tclTHENS (cut_intro absurd_term) + [onLastHyp gen_absurdity; + refine (mkApp (pf,[|mkVar id|]))])) + +let discrEq (lbeq,(t,t1,t2) as u) id gls = let sigma = project gls in let env = pf_env gls in - (match find_positions env sigma t1 t2 with - | Inr _ -> - errorlabstrm "discr" (str" Not a discriminable equality") - | Inl (cpath, (_,dirn), _) -> - let e = pf_get_new_id (id_of_string "ee") gls in - let e_env = push_named (e,None,t) env in - let discriminator = - build_discriminator sigma e_env dirn (mkVar e) sort cpath in - let (pf, absurd_term) = - discrimination_pf e (t,t1,t2) discriminator lbeq gls - in - tclCOMPLETE((tclTHENS (cut_intro absurd_term) - ([onLastHyp gen_absurdity; - refine (mkApp (pf, [| mkVar id |]))]))) gls) - -let not_found_message id = - (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++ - str" was not found in the current environment") + match find_positions env sigma t1 t2 with + | Inr _ -> + errorlabstrm "discr" (str" Not a discriminable equality") + | Inl (cpath, (_,dirn), _) -> + let sort = pf_apply get_type_of gls (pf_concl gls) in + discr_positions env sigma u id cpath dirn sort gls let onEquality tac id gls = let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in @@ -533,7 +539,7 @@ let discrEverywhere = tclORELSE (Tacticals.tryAllClauses discrSimpleClause) (fun gls -> - errorlabstrm "DiscrEverywhere" (str" No discriminable equalities")) + errorlabstrm "DiscrEverywhere" (str"No discriminable equalities")) let discr_tac = function | None -> discrEverywhere @@ -723,15 +729,9 @@ let make_iterated_tuple env sigma dflt (z,zty) = let rec build_injrec sigma env dflt c = function | [] -> make_iterated_tuple env sigma dflt (c,type_of env sigma c) | ((sp,cnum),argnum)::l -> - let cty = type_of env sigma c in - let (ity,_) = find_mrectype env sigma cty in - let (mib,mip) = lookup_mind_specif env ity in - let nparams = mib.mind_nparams in let (cnum_nlams,cnum_env,kont) = descend_then sigma env c cnum in - let newc = mkRel(cnum_nlams-(argnum-nparams)) in - let (subval,tuplety,dfltval) = - build_injrec sigma cnum_env dflt newc l - in + let newc = mkRel(cnum_nlams-argnum) in + let (subval,tuplety,dfltval) = build_injrec sigma cnum_env dflt newc l in (kont subval (dfltval,tuplety), tuplety,dfltval) @@ -739,6 +739,7 @@ let build_injector sigma env dflt c cpath = let (injcode,resty,_) = build_injrec sigma env dflt c cpath in (injcode,resty) +(* let try_delta_expand env sigma t = let whdt = whd_betadeltaiota env sigma t in let rec hd_rec c = @@ -749,12 +750,39 @@ let try_delta_expand env sigma t = | _ -> t in hd_rec whdt +*) (* Given t1=t2 Inj calculates the whd normal forms of t1 and t2 and it expands then only when the whdnf has a constructor of an inductive type in hd position, otherwise delta expansion is not done *) -let injEq (eq,(t,t1,t2)) id gls = +let simplify_args env sigma t = + (* Quick hack to reduce in arguments of eq only *) + match decompose_app t with + | eq, [t;c1;c2] -> applist (eq,[t;nf env sigma c1;nf env sigma c2]) + | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2]) + | _ -> t + +let inject_at_positions env sigma (eq,(t,t1,t2)) id posns = + let e = next_ident_away eq_baseid (ids_of_context env) in + let e_env = push_named (e,None,t) env in + let injectors = + map_succeed + (fun (cpath,t1',t2') -> + (* arbitrarily take t1' as the injector default value *) + let (injbody,resty) = build_injector sigma e_env t1' (mkVar e) cpath in + let injfun = mkNamedLambda e t injbody in + let pf = applist(eq.congr,[t;resty;injfun;t1;t2;mkVar id]) in + let ty = simplify_args env sigma (get_type_of env sigma pf) in + (pf,ty)) + posns in + if injectors = [] then + errorlabstrm "Equality.inj" (str "Failed to decompose the equality"); + tclMAP + (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf]) + injectors + +let injEq ipats (eq,(t,t1,t2)) id gls = let sigma = project gls in let env = pf_env gls in match find_positions env sigma t1 t2 with @@ -766,100 +794,38 @@ let injEq (eq,(t,t1,t2)) id gls = errorlabstrm "Equality.inj" (str"Nothing to do, it is an equality between convertible terms") | Inr posns -> - let e = pf_get_new_id (id_of_string "e") gls in - let e_env = push_named (e,None,t) env in - let injectors = - map_succeed - (fun (cpath,t1_0,t2_0) -> - try - let (injbody,resty) = - (* take arbitrarily t1_0 as the injector default value *) - build_injector sigma e_env t1_0 (mkVar e) cpath in - let injfun = mkNamedLambda e t injbody in - let _ = type_of env sigma injfun in (injfun,resty) - with e when catchable_exception e -> - (* may fail because ill-typed or because of a Prop argument *) - (* error "find_sigma_data" *) - failwith "caught") - posns - in - if injectors = [] then - errorlabstrm "Equality.inj" - (str "Failed to decompose the equality"); - tclMAP - (fun (injfun,resty) -> - let pf = applist(eq.congr, - [t;resty;injfun; - try_delta_expand env sigma t1; - try_delta_expand env sigma t2; - mkVar id]) - in - let ty = - try pf_nf gls (pf_type_of gls pf) - with - | UserError("refiner__fail",_) -> - errorlabstrm "InjClause" - (str (string_of_id id) ++ str" Not a projectable equality") - in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) - injectors +(* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ? + let t1 = try_delta_expand env sigma t1 in + let t2 = try_delta_expand env sigma t2 in +*) + tclTHEN + (inject_at_positions env sigma (eq,(t,t1,t2)) id posns) + (intros_pattern None ipats) gls -let inj = onEquality injEq +let inj ipats = onEquality (injEq ipats) -let injClause = function - | None -> onNegatedEquality injEq - | Some id -> try_intros_until inj id +let injClause ipats = function + | None -> onNegatedEquality (injEq ipats) + | Some id -> try_intros_until (inj ipats) id -let injConcl gls = injClause None gls -let injHyp id gls = injClause (Some id) gls +let injConcl gls = injClause [] None gls +let injHyp id gls = injClause [] (Some id) gls -let decompEqThen ntac (lbeq,(t,t1,t2)) id gls = - let sort = pf_type_of gls (pf_concl gls) in +let decompEqThen ntac (lbeq,(t,t1,t2) as u) id gls = + let sort = pf_apply get_type_of gls (pf_concl gls) in let sigma = project gls in let env = pf_env gls in - (match find_positions env sigma t1 t2 with - | Inl (cpath, (_,dirn), _) -> - let e = pf_get_new_id (id_of_string "e") gls in - let e_env = push_named (e,None,t) env in - let discriminator = - build_discriminator sigma e_env dirn (mkVar e) sort cpath in - let (pf, absurd_term) = - discrimination_pf e (t,t1,t2) discriminator lbeq gls in - tclCOMPLETE - ((tclTHENS (cut_intro absurd_term) - ([onLastHyp gen_absurdity; - refine (mkApp (pf, [| mkVar id |]))]))) gls - | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) - ntac 0 gls - | Inr posns -> - (let e = pf_get_new_id (id_of_string "e") gls in - let e_env = push_named (e,None,t) env in - let injectors = - map_succeed - (fun (cpath,t1_0,t2_0) -> - let (injbody,resty) = - (* take arbitrarily t1_0 as the injector default value *) - build_injector sigma e_env t1_0 (mkVar e) cpath in - let injfun = mkNamedLambda e t injbody in - try - let _ = type_of env sigma injfun in (injfun,resty) - with e when catchable_exception e -> failwith "caught") - posns - in - if injectors = [] then - errorlabstrm "Equality.decompEqThen" - (str "Discriminate failed to decompose the equality"); - (tclTHEN - (tclMAP (fun (injfun,resty) -> - let pf = applist(lbeq.congr, - [t;resty;injfun;t1;t2; - mkVar id]) in - let ty = pf_nf gls (pf_type_of gls pf) in - ((tclTHENS (cut ty) - ([tclIDTAC;refine pf])))) - (List.rev injectors)) - (ntac (List.length injectors))) - gls)) + match find_positions env sigma t1 t2 with + | Inl (cpath, (_,dirn), _) -> + discr_positions env sigma u id cpath dirn sort gls + | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *) + ntac 0 gls + | Inr posns -> + tclTHEN + (inject_at_positions env sigma (lbeq,(t,t1,t2)) id (List.rev posns)) + (ntac (List.length posns)) + gls let dEqThen ntac = function | None -> onNegatedEquality (decompEqThen ntac) @@ -903,7 +869,7 @@ let find_elim sort_of_gl lbeq = let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) - let eq_elim = find_elim (pf_type_of gls (pf_concl gls)) lbeq in + let eq_elim = find_elim (pf_apply get_type_of gls (pf_concl gls)) lbeq in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) @@ -1013,7 +979,7 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id) let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None let substClause l2r c cls gls = - let eq = pf_type_of gls c in + let eq = pf_apply get_type_of gls c in tclTHENS (cutSubstClause l2r eq cls) [tclIDTAC; exact_no_check c] gls let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls) @@ -1147,28 +1113,10 @@ let subst_all gl = let ids = list_uniquize ids in subst ids gl + (* Rewrite the first assumption for which the condition faildir does not fail and gives the direction of the rewrite *) -let rewrite_assumption_cond faildir gl = - let rec arec = function - | [] -> error "No such assumption" - | (id,_,t)::rest -> - (try let dir = faildir t gl in - general_rewrite dir (mkVar id) gl - with Failure _ | UserError _ -> arec rest) - in arec (pf_hyps gl) - - -let rewrite_assumption_cond_in faildir hyp gl = - let rec arec = function - | [] -> error "No such assumption" - | (id,_,t)::rest -> - (try let dir = faildir t gl in - general_rewrite_in dir hyp (mkVar id) gl - with Failure _ | UserError _ -> arec rest) - in arec (pf_hyps gl) - let cond_eq_term_left c t gl = try let (_,x,_) = snd (find_eq_data_decompose t) in @@ -1189,6 +1137,48 @@ let cond_eq_term c t gl = else failwith "not convertible" with PatternMatchingFailure -> failwith "not an equality" +let rewrite_mutli_assumption_cond cond_eq_term cl gl = + let rec arec = function + | [] -> error "No such assumption" + | (id,_,t) ::rest -> + begin + try + let dir = cond_eq_term t gl in + general_multi_rewrite dir (mkVar id,NoBindings) cl gl + with | Failure _ | UserError _ -> arec rest + end + in + arec (pf_hyps gl) + +let replace_multi_term dir_opt c = + let cond_eq_fun = + match dir_opt with + | None -> cond_eq_term c + | Some true -> cond_eq_term_left c + | Some false -> cond_eq_term_right c + in + rewrite_mutli_assumption_cond cond_eq_fun + +(* JF. old version +let rewrite_assumption_cond faildir gl = + let rec arec = function + | [] -> error "No such assumption" + | (id,_,t)::rest -> + (try let dir = faildir t gl in + general_rewrite dir (mkVar id) gl + with Failure _ | UserError _ -> arec rest) + in arec (pf_hyps gl) + + +let rewrite_assumption_cond_in faildir hyp gl = + let rec arec = function + | [] -> error "No such assumption" + | (id,_,t)::rest -> + (try let dir = faildir t gl in + general_rewrite_in dir hyp (mkVar id) gl + with Failure _ | UserError _ -> arec rest) + in arec (pf_hyps gl) + let replace_term_left t = rewrite_assumption_cond (cond_eq_term_left t) let replace_term_right t = rewrite_assumption_cond (cond_eq_term_right t) @@ -1200,6 +1190,27 @@ let replace_term_in_left t = rewrite_assumption_cond_in (cond_eq_term_left t) let replace_term_in_right t = rewrite_assumption_cond_in (cond_eq_term_right t) let replace_term_in t = rewrite_assumption_cond_in (cond_eq_term t) +*) + +let replace_term_left t = replace_multi_term (Some true) t Tacticals.onConcl + +let replace_term_right t = replace_multi_term (Some false) t Tacticals.onConcl + +let replace_term t = replace_multi_term None t Tacticals.onConcl + +let replace_term_in_left t hyp = replace_multi_term (Some true) t (Tacticals.onHyp hyp) + +let replace_term_in_right t hyp = replace_multi_term (Some false) t (Tacticals.onHyp hyp) + +let replace_term_in t hyp = replace_multi_term None t (Tacticals.onHyp hyp) + + + + + + + + -let _ = Setoid_replace.register_replace replace +let _ = Setoid_replace.register_replace (fun tac_opt c2 c1 gl -> replace_in_clause_maybe_by c2 c1 onConcl tac_opt gl) let _ = Setoid_replace.register_general_rewrite general_rewrite diff --git a/tactics/equality.mli b/tactics/equality.mli index 9ee565c5..3d6a08b6 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: equality.mli 8780 2006-05-02 21:58:58Z letouzey $ i*) +(*i $Id: equality.mli 9195 2006-10-01 09:41:57Z herbelin $ i*) (*i*) open Names @@ -22,6 +22,7 @@ open Tacticals open Tactics open Tacexpr open Rawterm +open Genarg (*i*) val general_rewrite_bindings : bool -> constr with_bindings -> tactic @@ -50,19 +51,21 @@ val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic val conditional_rewrite_in : bool -> identifier -> tactic -> constr with_bindings -> tactic +val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic val replace_in : identifier -> constr -> constr -> tactic -val replace_by : constr -> constr -> tactic -> tactic -val replace_in_by : identifier -> constr -> constr -> tactic -> tactic -val new_replace : constr -> constr -> identifier option -> tactic option -> tactic +val replace_by : constr -> constr -> tactic -> tactic +val replace_in_by : identifier -> constr -> constr -> tactic -> tactic + val discr : identifier -> tactic val discrConcl : tactic val discrClause : clause -> tactic val discrHyp : identifier -> tactic val discrEverywhere : tactic val discr_tac : quantified_hypothesis option -> tactic -val inj : identifier -> tactic -val injClause : quantified_hypothesis option -> tactic +val inj : intro_pattern_expr list -> identifier -> tactic +val injClause : intro_pattern_expr list -> quantified_hypothesis option -> + tactic val dEq : quantified_hypothesis option -> tactic val dEqThen : (int -> tactic) -> quantified_hypothesis option -> tactic @@ -111,9 +114,8 @@ val subst : identifier list -> tactic val subst_all : tactic (* Replace term *) -val replace_term_left : constr -> tactic -val replace_term_right : constr -> tactic -val replace_term : constr -> tactic -val replace_term_in_left : constr -> identifier -> tactic -val replace_term_in_right : constr -> identifier -> tactic -val replace_term_in : constr -> identifier -> tactic +(* [replace_multi_term dir_opt c cl] + perfoms replacement of [c] by the first value found in context + (according to [dir] if given to get the rewrite direction) in the clause [cl] +*) +val replace_multi_term : bool option -> constr -> clause -> tactic diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 31c060f1..ed40af1c 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 8759 2006-04-28 12:24:14Z herbelin $ *) +(* $Id: evar_tactics.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Term open Util @@ -51,7 +51,7 @@ 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 (pf_env gl) ev rawc (create_evar_defs sigma) in + let evd' = w_refine ev rawc (create_evar_defs sigma) in Refiner.tclEVARS (evars_of evd') gl (* diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 5a0b4b8c..3c7d76b2 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extraargs.ml4 8739 2006-04-26 22:23:37Z herbelin $ *) +(* $Id: extraargs.ml4 9076 2006-08-23 15:05:54Z jforest $ *) open Pp open Pcoq @@ -124,3 +124,115 @@ ARGUMENT EXTEND hloc END + + + + + + +(* Julien: Mise en commun des differentes version de replace with in by *) + +let pr_by_arg_tac _prc _prlc prtac opt_c = + match opt_c with + | None -> mt () + | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) + +ARGUMENT EXTEND by_arg_tac + TYPED AS tactic_opt + PRINTED BY pr_by_arg_tac +| [ "by" tactic3(c) ] -> [ Some c ] +| [ ] -> [ None ] +END + + +let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = + match lo,concl with + | Some [],true -> mt () + | None,true -> str "in" ++ spc () ++ str "*" + | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" + | Some l,_ -> + str "in" ++ spc () ++ + Util.prlist_with_sep spc pr_id l ++ + match concl with + | true -> spc () ++ str "|-" ++ spc () ++ str "*" + | _ -> mt () + + +let pr_in_arg_hyp _ _ _ = pr_in_hyp (fun (_,id) -> Ppconstr.pr_id id) + +let pr_in_arg_hyp_typed _ _ _ = pr_in_hyp Ppconstr.pr_id + + +let pr_var_list_gen pr_id = Util.prlist_with_sep (fun () -> str ",") pr_id + +let pr_var_list_typed _ _ _ = pr_var_list_gen Ppconstr.pr_id + +let pr_var_list _ _ _ = pr_var_list_gen (fun (_,id) -> Ppconstr.pr_id id) + + +ARGUMENT EXTEND comma_var_lne + TYPED AS var list + PRINTED BY pr_var_list_typed + RAW_TYPED AS var list + RAW_PRINTED BY pr_var_list + GLOB_TYPED AS var list + GLOB_PRINTED BY pr_var_list +| [ var(x) ] -> [ [x] ] +| [ var(x) "," comma_var_lne(l) ] -> [x::l] +END + +ARGUMENT EXTEND comma_var_l + TYPED AS var list + PRINTED BY pr_var_list_typed + RAW_TYPED AS var list + RAW_PRINTED BY pr_var_list + GLOB_TYPED AS var list + GLOB_PRINTED BY pr_var_list +| [ comma_var_lne(l) ] -> [l] +| [] -> [ [] ] +END + +let pr_in_concl _ _ _ = function true -> str "|- " ++ spc () ++ str "*" | _ -> str "|-" + +ARGUMENT EXTEND inconcl + TYPED AS bool + PRINTED BY pr_in_concl +| [ "|-" "*" ] -> [ true ] +| [ "|-" ] -> [ false ] +END + + + +ARGUMENT EXTEND in_arg_hyp + TYPED AS var list option * bool + PRINTED BY pr_in_arg_hyp_typed + RAW_TYPED AS var list option * bool + RAW_PRINTED BY pr_in_arg_hyp + GLOB_TYPED AS var list option * bool + GLOB_PRINTED BY pr_in_arg_hyp +| [ "in" "*" ] -> [(None,true)] +| [ "in" "*" inconcl_opt(b) ] -> [let onconcl = match b with Some b -> b | None -> true in (None,onconcl)] +| [ "in" comma_var_l(l) inconcl_opt(b) ] -> [ let onconcl = match b with Some b -> b | None -> false in + Some l, onconcl + ] +| [ ] -> [ (Some [],true) ] +END + + +let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = + {Tacexpr.onhyps= + Util.option_map + (fun l -> + List.map + (fun id -> ( ([],trad_id id) ,Tacexpr.InHyp)) + l + ) + hyps; + Tacexpr.onconcl=concl; + Tacexpr.concl_occs = []} + + +let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd +let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) + + diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 004fef02..4a9a0c5f 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 6621 2005-01-21 17:24:37Z herbelin $ i*) +(*i $Id: extraargs.mli 9076 2006-08-23 15:05:54Z jforest $ i*) open Tacexpr open Term @@ -39,3 +39,14 @@ val rawwit_hloc : loc_place raw_abstract_argument_type val wit_hloc : place closed_abstract_argument_type val hloc : loc_place Pcoq.Gram.Entry.e + +val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.Entry.e +val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type +val wit_in_arg_hyp : (Names.identifier list option * bool) closed_abstract_argument_type +val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause +val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause + + +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e +val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type +val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index c2820c44..a8204665 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 8979 2006-06-23 10:17:14Z herbelin $ *) +(* $Id: extratactics.ml4 9266 2006-10-24 09:03:15Z herbelin $ *) open Pp open Pcoq @@ -20,116 +20,25 @@ open Names (* Equality *) open Equality -(* Pierre L: for an easy implementation of "rewrite ... in <clause>", rewrite - has moved to g_tactics.ml4 - -TACTIC EXTEND rewrite -| [ "rewrite" orient(b) constr_with_bindings(c) ] -> - [general_rewrite_bindings b c] -END - -TACTIC EXTEND rewrite_in -| [ "rewrite" orient(b) constr_with_bindings(c) "in" hyp(h) ] -> - [general_rewrite_bindings_in b h c] -END - -let h_rewriteLR x = h_rewrite true (x,Rawterm.NoBindings) -*) - -(* Julien: Mise en commun des differentes version de replace with in by - TODO: deplacer dans extraargs - -*) - -let pr_by_arg_tac _prc _prlc prtac opt_c = - match opt_c with - | None -> mt () - | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) - -let pr_in_hyp = function - | None -> mt () - | Some id -> spc () ++ hov 2 (str "in" ++ spc () ++ Nameops.pr_id id) - -let pr_in_arg_hyp _prc _prlc _prtac opt_c = - pr_in_hyp (Util.option_map snd opt_c) - -let pr_in_arg_hyp_typed _prc _prlc _prtac = - pr_in_hyp - -ARGUMENT EXTEND by_arg_tac - TYPED AS tactic_opt - PRINTED BY pr_by_arg_tac -| [ "by" tactic3(c) ] -> [ Some c ] -| [ ] -> [ None ] -END - -ARGUMENT EXTEND in_arg_hyp - TYPED AS var_opt - PRINTED BY pr_in_arg_hyp_typed - RAW_TYPED AS var_opt - RAW_PRINTED BY pr_in_arg_hyp - GLOB_TYPED AS var_opt - GLOB_PRINTED BY pr_in_arg_hyp -| [ "in" hyp(c) ] -> [ Some (c) ] -| [ ] -> [ None ] -END TACTIC EXTEND replace ["replace" constr(c1) "with" constr(c2) in_arg_hyp(in_hyp) by_arg_tac(tac) ] --> [ new_replace c1 c2 in_hyp (Util.option_map Tacinterp.eval_tactic tac) ] -END - -(* Julien: - old version - -TACTIC EXTEND replace -| [ "replace" constr(c1) "with" constr(c2) ] -> - [ replace c1 c2 ] -END - -TACTIC EXTEND replace_by -| [ "replace" constr(c1) "with" constr(c2) "by" tactic(tac) ] -> - [ replace_by c1 c2 (snd tac) ] - -END - -TACTIC EXTEND replace_in -| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) ] -> - [ replace_in h c1 c2 ] -END - -TACTIC EXTEND replace_in_by -| [ "replace" constr(c1) "with" constr(c2) "in" hyp(h) "by" tactic(tac) ] -> - [ replace_in_by h c1 c2 (snd tac) ] +-> [ replace_in_clause_maybe_by c1 c2 (glob_in_arg_hyp_to_clause in_hyp) (Util.option_map Tacinterp.eval_tactic tac) ] END -*) - TACTIC EXTEND replace_term_left - [ "replace" "->" constr(c) ] -> [ replace_term_left c ] + [ "replace" "->" constr(c) in_arg_hyp(in_hyp) ] + -> [ replace_multi_term (Some true) c (glob_in_arg_hyp_to_clause in_hyp)] END TACTIC EXTEND replace_term_right - [ "replace" "<-" constr(c) ] -> [ replace_term_right c ] + [ "replace" "<-" constr(c) in_arg_hyp(in_hyp) ] + -> [replace_multi_term (Some false) c (glob_in_arg_hyp_to_clause in_hyp)] END TACTIC EXTEND replace_term - [ "replace" constr(c) ] -> [ replace_term c ] -END - -TACTIC EXTEND replace_term_in_left - [ "replace" "->" constr(c) "in" hyp(h) ] - -> [ replace_term_in_left c h ] -END - -TACTIC EXTEND replace_term_in_right - [ "replace" "<-" constr(c) "in" hyp(h) ] - -> [ replace_term_in_right c h ] -END - -TACTIC EXTEND replace_term_in - [ "replace" constr(c) "in" hyp(h) ] - -> [ replace_term_in c h ] + [ "replace" constr(c) in_arg_hyp(in_hyp) ] + -> [ replace_multi_term None c (glob_in_arg_hyp_to_clause in_hyp) ] END TACTIC EXTEND simplify_eq @@ -143,7 +52,11 @@ END let h_discrHyp id = h_discriminate (Some id) TACTIC EXTEND injection - [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause h ] + [ "injection" quantified_hypothesis_opt(h) ] -> [ injClause [] h ] +END +TACTIC EXTEND injection_as + [ "injection" quantified_hypothesis_opt(h) + "as" simple_intropattern_list(ipat)] -> [ injClause ipat h ] END let h_injHyp id = h_injection (Some id) @@ -182,7 +95,7 @@ END (* AutoRewrite *) open Autorewrite - +(* J.F : old version TACTIC EXTEND autorewrite [ "autorewrite" "with" ne_preident_list(l) ] -> [ autorewrite Refiner.tclIDTAC l ] @@ -193,6 +106,21 @@ TACTIC EXTEND autorewrite | [ "autorewrite" "with" ne_preident_list(l) "in" hyp(id) "using" tactic(t) ] -> [ autorewrite_in id (snd t) l ] END +*) + +TACTIC EXTEND autorewrite +| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) ] -> + [ auto_multi_rewrite l (glob_in_arg_hyp_to_clause cl) ] +| [ "autorewrite" "with" ne_preident_list(l) in_arg_hyp(cl) "using" tactic(t) ] -> + [ + let cl = glob_in_arg_hyp_to_clause cl in + auto_multi_rewrite_with (snd t) l cl + + ] +END + + + let add_rewrite_hint name ort t lcsr = let env = Global.env() and sigma = Evd.empty in @@ -223,22 +151,22 @@ let refine_tac = h_refine open Setoid_replace TACTIC EXTEND setoid_replace - [ "setoid_replace" constr(c1) "with" constr(c2) ] -> - [ setoid_replace None c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel)] -> - [ setoid_replace (Some rel) c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) ] -> - [ setoid_replace None c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] -> - [ setoid_replace (Some rel) c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) ] -> - [ setoid_replace_in h None c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel)] -> - [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:[] ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) ] -> - [ setoid_replace_in h None c1 c2 ~new_goals:l ] - | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) ] -> - [ setoid_replace_in h (Some rel) c1 c2 ~new_goals:l ] + [ "setoid_replace" constr(c1) "with" constr(c2) by_arg_tac(tac)] -> + [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:[] ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) by_arg_tac(tac)] -> + [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:[] ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> + [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) None c1 c2 ~new_goals:l ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac) ] -> + [ setoid_replace (Util.option_map Tacinterp.eval_tactic tac) (Some rel) c1 c2 ~new_goals:l ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) by_arg_tac(tac) ] -> + [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:[] ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) by_arg_tac(tac)] -> + [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:[] ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> + [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h None c1 c2 ~new_goals:l ] + | [ "setoid_replace" constr(c1) "with" constr(c2) "in" hyp(h) "using" "relation" constr(rel) "generate" "side" "conditions" constr_list(l) by_arg_tac(tac)] -> + [ setoid_replace_in (Util.option_map Tacinterp.eval_tactic tac) h (Some rel) c1 c2 ~new_goals:l ] END TACTIC EXTEND setoid_rewrite @@ -471,3 +399,9 @@ VERNAC COMMAND EXTEND ImplicitTactic | [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ Tacinterp.declare_implicit_tactic (Tacinterp.interp tac) ] END + +TACTIC EXTEND apply_in +| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in id [c] ] +| ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") + "in" hyp(id) ] -> [ apply_in id (c::cl) ] +END diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 91766254..234c0161 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extratactics.mli 8977 2006-06-23 10:09:59Z herbelin $ i*) +(*i $Id: extratactics.mli 9073 2006-08-22 08:54:29Z jforest $ i*) open Util open Names @@ -22,21 +22,3 @@ val h_injHyp : quantified_hypothesis -> tactic val refine_tac : Genarg.open_constr -> tactic - - -(* Julien: Mise en commun des differentes version de replace with in by - TODO: deplacer dans extraargs - -*) - - -val rawwit_in_arg_hyp: identifier located option raw_abstract_argument_type - -val in_arg_hyp: identifier located option Pcoq.Gram.Entry.e - - - -val rawwit_by_arg_tac : - (raw_tactic_expr option, constr_expr, raw_tactic_expr) abstract_argument_type - -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 7974ce56..9507ce5f 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 7837 2006-01-11 09:47:32Z herbelin $ *) +(* $Id: leminv.ml 9154 2006-09-20 17:18:18Z corbinea $ *) open Pp open Util @@ -217,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = (str"Computed inversion goal was not closed in initial signature"); *) let invSign = named_context_val invEnv in - let pfs = mk_pftreestate (mk_goal invSign invGoal) in + let pfs = mk_pftreestate (mk_goal invSign invGoal None) in let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in let (pfterm,meta_types) = extract_open_pftreestate pfs in let global_named_context = Global.named_context () in diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 8c8d4d37..2727e669 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: setoid_replace.ml 8900 2006-06-06 14:40:27Z letouzey $ *) +(* $Id: setoid_replace.ml 9331 2006-11-01 09:36:06Z herbelin $ *) open Tacmach open Proof_type @@ -33,7 +33,7 @@ open Decl_kinds open Constrintern open Mod_subst -let replace = ref (fun _ _ -> assert false) +let replace = ref (fun _ _ _ -> assert false) let register_replace f = replace := f let general_rewrite = ref (fun _ _ -> assert false) @@ -155,7 +155,7 @@ let coq_MSCovariant = lazy(constant ["Setoid"] "MSCovariant") let coq_MSContravariant = lazy(constant ["Setoid"] "MSContravariant") let coq_singl = lazy(constant ["Setoid"] "singl") -let coq_cons = lazy(constant ["Setoid"] "cons") +let coq_cons = lazy(constant ["Setoid"] "necons") let coq_equality_morphism_of_asymmetric_areflexive_transitive_relation = lazy(constant ["Setoid"] @@ -805,135 +805,140 @@ let new_morphism m signature id hook = let typeofm = Typing.type_of env Evd.empty m in let typ = clos_norm_flags Closure.betaiotazeta empty_env Evd.empty typeofm in let argsrev, output = - match signature with - None -> decompose_prod typ - | Some (_,output') -> - (* the carrier of the relation output' can be a Prod ==> - we must uncurry on the fly output. - E.g: A -> B -> C vs A -> (B -> C) - args output args output - *) - let rel = find_relation_class output' in - let rel_a,rel_quantifiers_no = - match rel with - Relation rel -> rel.rel_a, rel.rel_quantifiers_no - | Leibniz (Some t) -> t, 0 - | Leibniz None -> assert false in - let rel_a_n = - clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in - try - let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in - let argsrev,_ = decompose_prod output_rel_a_n in - let n = List.length argsrev in - let argsrev',_ = decompose_prod typ in - let m = List.length argsrev' in - decompose_prod_n (m - n) typ - with UserError(_,_) -> - (* decompose_lam_n failed. This may happen when rel_a is an axiom, - a constructor, an inductive type, etc. *) - decompose_prod typ + match signature with + None -> decompose_prod typ + | Some (_,output') -> + (* the carrier of the relation output' can be a Prod ==> + we must uncurry on the fly output. + E.g: A -> B -> C vs A -> (B -> C) + args output args output + *) + let rel = + try find_relation_class output' + with Not_found -> errorlabstrm "Add Morphism" + (str "Not a valid signature: " ++ pr_lconstr output' ++ + str " is neither a registered relation nor the Leibniz " ++ + str " equality.") in + let rel_a,rel_quantifiers_no = + match rel with + Relation rel -> rel.rel_a, rel.rel_quantifiers_no + | Leibniz (Some t) -> t, 0 + | Leibniz None -> assert false in + let rel_a_n = + clos_norm_flags Closure.betaiotazeta empty_env Evd.empty rel_a in + try + let _,output_rel_a_n = decompose_lam_n rel_quantifiers_no rel_a_n in + let argsrev,_ = decompose_prod output_rel_a_n in + let n = List.length argsrev in + let argsrev',_ = decompose_prod typ in + let m = List.length argsrev' in + decompose_prod_n (m - n) typ + with UserError(_,_) -> + (* decompose_lam_n failed. This may happen when rel_a is an axiom, + a constructor, an inductive type, etc. *) + decompose_prod typ in let args_ty = List.rev argsrev in let args_ty_len = List.length (args_ty) in let args_ty_quantifiers_rev,args,args_instance,output,output_instance = - match signature with - None -> - if args_ty = [] then - errorlabstrm "New Morphism" - (str "The term " ++ pr_lconstr m ++ str " has type " ++ - pr_lconstr typeofm ++ str " that is not a product.") ; - ignore (check_is_dependent 0 args_ty output) ; - let args = - List.map - (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in - let output = default_relation_for_carrier output in - [],args,args,output,output - | Some (args,output') -> - assert (args <> []); - let number_of_arguments = List.length args in - let number_of_quantifiers = args_ty_len - number_of_arguments in - if number_of_quantifiers < 0 then - errorlabstrm "New Morphism" - (str "The morphism " ++ pr_lconstr m ++ str " has type " ++ - pr_lconstr typeofm ++ str " that attends at most " ++ int args_ty_len ++ - str " arguments. The signature that you specified requires " ++ - int number_of_arguments ++ str " arguments.") - else - begin - (* the real_args_ty returned are already delifted *) - let args_ty_quantifiers_rev, real_args_ty, real_output = - check_is_dependent number_of_quantifiers args_ty output in - let quantifiers_rel_context = - List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in - let env = push_rel_context quantifiers_rel_context env in - let find_relation_class t real_t = - try - let rel = find_relation_class t in - rel, unify_relation_class_carrier_with_type env rel real_t - with Not_found -> - errorlabstrm "Add Morphism" - (str "Not a valid signature: " ++ pr_lconstr t ++ - str " is neither a registered relation nor the Leibniz " ++ - str " equality.") - in - let find_relation_class_v (variance,t) real_t = - let relation,relation_instance = find_relation_class t real_t in - match relation, variance with - Leibniz _, None - | Relation {rel_sym = Some _}, None - | Relation {rel_sym = None}, Some _ -> - (variance, relation), (variance, relation_instance) - | Relation {rel_sym = None},None -> - errorlabstrm "Add Morphism" - (str "You must specify the variance in each argument " ++ - str "whose relation is asymmetric.") - | Leibniz _, Some _ - | Relation {rel_sym = Some _}, Some _ -> - errorlabstrm "Add Morphism" - (str "You cannot specify the variance of an argument " ++ - str "whose relation is symmetric.") - in - let args, args_instance = - List.split - (List.map2 find_relation_class_v args real_args_ty) in - let output,output_instance= find_relation_class output' real_output in - args_ty_quantifiers_rev, args, args_instance, output, output_instance - end + match signature with + None -> + if args_ty = [] then + errorlabstrm "New Morphism" + (str "The term " ++ pr_lconstr m ++ str " has type " ++ + pr_lconstr typeofm ++ str " that is not a product.") ; + ignore (check_is_dependent 0 args_ty output) ; + let args = + List.map + (fun (_,ty) -> None,default_relation_for_carrier ty) args_ty in + let output = default_relation_for_carrier output in + [],args,args,output,output + | Some (args,output') -> + assert (args <> []); + let number_of_arguments = List.length args in + let number_of_quantifiers = args_ty_len - number_of_arguments in + if number_of_quantifiers < 0 then + errorlabstrm "New Morphism" + (str "The morphism " ++ pr_lconstr m ++ str " has type " ++ + pr_lconstr typeofm ++ str " that attends at most " ++ int args_ty_len ++ + str " arguments. The signature that you specified requires " ++ + int number_of_arguments ++ str " arguments.") + else + begin + (* the real_args_ty returned are already delifted *) + let args_ty_quantifiers_rev, real_args_ty, real_output = + check_is_dependent number_of_quantifiers args_ty output in + let quantifiers_rel_context = + List.map (fun (n,t) -> n,None,t) args_ty_quantifiers_rev in + let env = push_rel_context quantifiers_rel_context env in + let find_relation_class t real_t = + try + let rel = find_relation_class t in + rel, unify_relation_class_carrier_with_type env rel real_t + with Not_found -> + errorlabstrm "Add Morphism" + (str "Not a valid signature: " ++ pr_lconstr t ++ + str " is neither a registered relation nor the Leibniz " ++ + str " equality.") + in + let find_relation_class_v (variance,t) real_t = + let relation,relation_instance = find_relation_class t real_t in + match relation, variance with + Leibniz _, None + | Relation {rel_sym = Some _}, None + | Relation {rel_sym = None}, Some _ -> + (variance, relation), (variance, relation_instance) + | Relation {rel_sym = None},None -> + errorlabstrm "Add Morphism" + (str "You must specify the variance in each argument " ++ + str "whose relation is asymmetric.") + | Leibniz _, Some _ + | Relation {rel_sym = Some _}, Some _ -> + errorlabstrm "Add Morphism" + (str "You cannot specify the variance of an argument " ++ + str "whose relation is symmetric.") + in + let args, args_instance = + List.split + (List.map2 find_relation_class_v args real_args_ty) in + let output,output_instance= find_relation_class output' real_output in + args_ty_quantifiers_rev, args, args_instance, output, output_instance + end in - let argsconstr,outputconstr,lem = + let argsconstr,outputconstr,lem = gen_compat_lemma_statement args_ty_quantifiers_rev output_instance - args_instance (apply_to_rels m args_ty_quantifiers_rev) in - (* "unfold make_compatibility_goal" *) - let lem = + args_instance (apply_to_rels m args_ty_quantifiers_rev) in + (* "unfold make_compatibility_goal" *) + let lem = Reductionops.clos_norm_flags - (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref)) - env Evd.empty lem in - (* "unfold make_compatibility_goal_aux" *) - let lem = + (Closure.unfold_red (Lazy.force coq_make_compatibility_goal_eval_ref)) + env Evd.empty lem in + (* "unfold make_compatibility_goal_aux" *) + let lem = Reductionops.clos_norm_flags - (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref)) - env Evd.empty lem in - (* "simpl" *) - let lem = Tacred.nf env Evd.empty lem in + (Closure.unfold_red(Lazy.force coq_make_compatibility_goal_aux_eval_ref)) + env Evd.empty lem in + (* "simpl" *) + let lem = Tacred.nf env Evd.empty lem in if Lib.is_modtype () then - begin - ignore - (Declare.declare_internal_constant id - (ParameterEntry lem, IsAssumption Logical)) ; - let mor_name = morphism_theory_id_of_morphism_proof_id id in - let lemma_infos = Some (id,argsconstr,outputconstr) in - add_morphism lemma_infos mor_name - (m,args_ty_quantifiers_rev,args,output) - end + begin + ignore + (Declare.declare_internal_constant id + (ParameterEntry lem, IsAssumption Logical)) ; + let mor_name = morphism_theory_id_of_morphism_proof_id id in + let lemma_infos = Some (id,argsconstr,outputconstr) in + add_morphism lemma_infos mor_name + (m,args_ty_quantifiers_rev,args,output) + end else - begin - new_edited id - (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr); - Pfedit.start_proof id (Global, Proof Lemma) - (Declare.clear_proofs (Global.named_context ())) - lem hook; - Options.if_verbose msg (Printer.pr_open_subgoals ()); - end + begin + new_edited id + (m,args_ty_quantifiers_rev,args,argsconstr,output,outputconstr); + Pfedit.start_proof id (Global, Proof Lemma) + (Declare.clear_proofs (Global.named_context ())) + lem hook; + Options.if_verbose msg (Printer.pr_open_subgoals ()); + end let morphism_hook _ ref = let pf_id = id_of_global ref in @@ -1272,7 +1277,7 @@ let relation_class_that_matches_a_constr caller_name new_goals hypt = forall x1 x2, rel1 x1 x2 -> rel2 x1 x2 The Coq part of the tactic, however, needs rel1 == rel2. Hence the third case commented out. - Note: accepting user-defined subtrelations seems to be the last + Note: accepting user-defined subrelations seems to be the last useful generalization that does not go against the original spirit of the tactic. *) @@ -1351,9 +1356,9 @@ let cartesian_product gl a = (aux (List.map (elim_duplicates gl identity) (Array.to_list a))) let mark_occur gl ~new_goals t in_c input_relation input_direction = - let rec aux output_relation output_direction in_c = + let rec aux output_relation output_directions in_c = if eq_constr t in_c then - if input_direction = output_direction + if List.mem input_direction output_directions && subrelation gl input_relation output_relation then [ToReplace] else [] @@ -1400,33 +1405,32 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = (fun res (mor,c,al) -> let a = let arguments = Array.of_list mor.args in - let apply_variance_to_direction default_dir = + let apply_variance_to_direction = function - None -> default_dir - | Some true -> output_direction - | Some false -> opposite_direction output_direction + None -> [Left2Right;Right2Left] + | Some true -> output_directions + | Some false -> List.map opposite_direction output_directions in Util.array_map2 (fun a (variance,relation) -> - (aux relation - (apply_variance_to_direction Left2Right variance) a) @ - (aux relation - (apply_variance_to_direction Right2Left variance) a) + (aux relation (apply_variance_to_direction variance) a) ) al arguments in let a' = cartesian_product gl a in + List.flatten (List.map (fun output_direction -> (List.map (function a -> if not (get_mark a) then ToKeep (in_c,output_relation,output_direction) else - MApp (c,ACMorphism mor,a,output_direction)) a') @ res + MApp (c,ACMorphism mor,a,output_direction)) a')) + output_directions) @ res ) [] mors_and_cs_and_als in (* Then we look for well typed functions *) let res_functions = (* the tactic works only if the function type is made of non-dependent products only. However, here we - can cheat a bit by partially istantiating c to match + can cheat a bit by partially instantiating c to match the requirement when the arguments to be replaced are bound by non-dependent products only. *) let typeofc = Tacmach.pf_type_of gl c in @@ -1437,7 +1441,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = function [] -> if a_rev = [] then - [ToKeep (in_c,output_relation,output_direction)] + List.map (fun output_direction -> + ToKeep (in_c,output_relation,output_direction)) + output_directions else let a' = cartesian_product gl (Array.of_list (List.rev a_rev)) @@ -1445,7 +1451,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = List.fold_left (fun res a -> if not (get_mark a) then - (ToKeep (in_c,output_relation,output_direction))::res + List.map (fun output_direction -> + (ToKeep (in_c,output_relation,output_direction))) + output_directions @ res else let err = match output_relation with @@ -1461,7 +1469,9 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = let mor = ACFunction{f_args=List.rev f_args_rev;f_output=typ} in let func = beta_expand c c_args_rev in - (MApp (func,mor,a,output_direction))::res + List.map (fun output_direction -> + (MApp (func,mor,a,output_direction))) + output_directions @ res ) [] a' | (he::tl) as a-> let typnf = Reduction.whd_betadeltaiota env typ in @@ -1472,8 +1482,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = | Prod (name,s,t) -> let env' = push_rel (name,None,s) env in let he = - (aux (Leibniz (Some s)) Left2Right he) @ - (aux (Leibniz (Some s)) Right2Left he) in + (aux (Leibniz (Some s)) [Left2Right;Right2Left] he) in if he = [] then [] else let he0 = List.hd he in @@ -1515,41 +1524,48 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = | Prod (_, c1, c2) -> if (dependent (mkRel 1) c2) then - errorlabstrm "Setoid_replace" - (str "Cannot rewrite in the type of a variable bound " ++ - str "in a dependent product.") + if (occur_term t c2) + then errorlabstrm "Setoid_replace" + (str "Cannot rewrite in the type of a variable bound " ++ + str "in a dependent product.") + else + List.map (fun output_direction -> + ToKeep (in_c,output_relation,output_direction)) + output_directions else - let typeofc1 = Tacmach.pf_type_of gl c1 in - if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then - (* to avoid this error we should introduce an impl relation - whose first argument is Type instead of Prop. However, - the type of the new impl would be Type -> Prop -> Prop - that is no longer a Relation_Definitions.relation. Thus - the Coq part of the tactic should be heavily modified. *) - errorlabstrm "Setoid_replace" - (str "Rewriting in a product A -> B is possible only when A " ++ - str "is a proposition (i.e. A is of type Prop). The type " ++ - pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++ - str " that is not convertible to Prop.") - else - aux output_relation output_direction - (mkApp ((Lazy.force coq_impl), - [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |])) + let typeofc1 = Tacmach.pf_type_of gl c1 in + if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then + (* to avoid this error we should introduce an impl relation + whose first argument is Type instead of Prop. However, + the type of the new impl would be Type -> Prop -> Prop + that is no longer a Relation_Definitions.relation. Thus + the Coq part of the tactic should be heavily modified. *) + errorlabstrm "Setoid_replace" + (str "Rewriting in a product A -> B is possible only when A " ++ + str "is a proposition (i.e. A is of type Prop). The type " ++ + pr_lconstr c1 ++ str " has type " ++ pr_lconstr typeofc1 ++ + str " that is not convertible to Prop.") + else + aux output_relation output_directions + (mkApp ((Lazy.force coq_impl), + [| c1 ; subst1 (mkRel 1 (*dummy*)) c2 |])) | _ -> - if occur_term t in_c then - errorlabstrm "Setoid_replace" - (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++ - str " that is not an applicative context.") - else - [ToKeep (in_c,output_relation,output_direction)] + if occur_term t in_c then + errorlabstrm "Setoid_replace" + (str "Trying to replace " ++ pr_lconstr t ++ str " in " ++ pr_lconstr in_c ++ + str " that is not an applicative context.") + else + List.map (fun output_direction -> + ToKeep (in_c,output_relation,output_direction)) + output_directions in let aux2 output_relation output_direction = List.map (fun res -> output_relation,output_direction,res) - (aux output_relation output_direction in_c) in + (aux output_relation [output_direction] in_c) in let res = (aux2 (Lazy.force coq_iff_relation) Right2Left) @ - (* This is the case of a proposition of signature A ++> iff or B --> iff *) + (* [Left2Right] is the case of a prop of signature A ++> iff or B --> iff *) (aux2 (Lazy.force coq_iff_relation) Left2Right) @ (aux2 (Lazy.force coq_impl_relation) Right2Left) in let res = elim_duplicates gl (function (_,_,t) -> t) res in @@ -1849,8 +1865,27 @@ let general_s_rewrite_in id lft2rgt c ~new_goals gl = else relation_rewrite_in id c2 c1 (Right2Left,eqclause) ~new_goals gl -let setoid_replace relation c1 c2 ~new_goals gl = - try + +(* + [general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals ] + common part of [setoid_replace] and [setoid_replace_in] (distinction is done using rewrite_tac). + + Algorith sketch: + 1- find the (setoid) relation [rel] between [c1] and [c2] using [relation] + 2- assert [H:rel c2 c1] + 3- replace [c1] with [c2] using [rewrite_tac] (should be [general_s_rewrite] if we want to replace in the + goal, and [general_s_rewrite_in id] if we want to replace in the hypothesis [id]). Possibly generate + new_goals if asked (cf general_s_rewrite) + 4- if [try_prove_eq_tac_opt] is [Some tac] try to complete [rel c2 c1] using tac and do nothing if + [try_prove_eq_tac_opt] is [None] +*) +let general_setoid_replace rewrite_tac try_prove_eq_tac_opt relation c1 c2 ~new_goals gl = + let try_prove_eq_tac = + match try_prove_eq_tac_opt with + | None -> Tacticals.tclIDTAC + | Some tac -> Tacticals.tclTRY (Tacticals.tclCOMPLETE tac ) + in + try let relation = match relation with Some rel -> @@ -1873,23 +1908,29 @@ let setoid_replace relation c1 c2 ~new_goals gl = tclTHENS (assert_tac false Anonymous eq) [onLastHyp (fun id -> tclTHEN - (general_s_rewrite dir (mkVar id) ~new_goals) + (rewrite_tac dir (mkVar id) ~new_goals) (clear [id])); - Tacticals.tclIDTAC] + try_prove_eq_tac] in tclORELSE (replace true eq_left_to_right) (replace false eq_right_to_left) gl with - Optimize -> (!replace c1 c2) gl + Optimize -> (* (!replace tac_opt c1 c2) gl *) + let eq = mkApp (Lazy.force coq_eq, [| pf_type_of gl c1;c2 ; c1 |]) in + tclTHENS (assert_tac false Anonymous eq) + [onLastHyp (fun id -> + tclTHEN + (rewrite_tac false (mkVar id) ~new_goals) + (clear [id])); + try_prove_eq_tac] gl + + -let setoid_replace_in id relation c1 c2 ~new_goals gl = - let hyp = pf_type_of gl (mkVar id) in - let new_hyp = Termops.replace_term c1 c2 hyp in - cut_replacing id new_hyp - (fun exact -> tclTHENLASTn - (setoid_replace relation c2 c1 ~new_goals) - [| exact; tclIDTAC |]) gl +let setoid_replace = general_setoid_replace general_s_rewrite +let setoid_replace_in tac_opt id relation c1 c2 ~new_goals gl = + general_setoid_replace (general_s_rewrite_in id) tac_opt relation c1 c2 ~new_goals gl + (* [setoid_]{reflexivity,symmetry,transitivity} tactics *) let setoid_reflexivity gl = diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli index 750addcc..eb71f68e 100644 --- a/tactics/setoid_replace.mli +++ b/tactics/setoid_replace.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: setoid_replace.mli 8779 2006-05-02 20:59:21Z letouzey $ i*) +(*i $Id: setoid_replace.mli 9073 2006-08-22 08:54:29Z jforest $ i*) open Term open Proof_type @@ -39,7 +39,7 @@ type morphism_signature = (bool option * constr_expr) list * constr_expr val pr_morphism_signature : morphism_signature -> Pp.std_ppcmds -val register_replace : (constr -> constr -> tactic) -> unit +val register_replace : (tactic option -> constr -> constr -> tactic) -> unit val register_general_rewrite : (bool -> constr -> tactic) -> unit val print_setoids : unit -> unit @@ -52,8 +52,9 @@ val default_morphism : ?filter:(constr morphism -> bool) -> constr -> relation morphism val setoid_replace : - constr option -> constr -> constr -> new_goals:constr list -> tactic + tactic option -> constr option -> constr -> constr -> new_goals:constr list -> tactic val setoid_replace_in : + tactic option -> identifier -> constr option -> constr -> constr -> new_goals:constr list -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 114968c8..1e8c55ef 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 8991 2006-06-27 11:59:50Z herbelin $ *) +(* $Id: tacinterp.ml 9302 2006-10-27 21:21:17Z barras $ *) open Constrintern open Closure @@ -48,6 +48,12 @@ open Pretyping open Pretyping.Default open Pcoq +let safe_msgnl s = + try msgnl s with e -> + msgnl + (str "bug in the debugger : " ++ + str "an exception is raised while printing debug information") + let error_syntactic_metavariables_not_allowed loc = user_err_loc (loc,"out_ident", @@ -75,6 +81,7 @@ type value = (* later, as in "tac" in "Intro H; tac" *) | VConstr of constr (* includes idents known to be bound and references *) | VConstr_context of constr + | VList of value list | VRec of value ref let locate_tactic_call loc = function @@ -112,13 +119,16 @@ let constr_of_VConstr_context = function errorlabstrm "constr_of_VConstr_context" (str "not a context variable") (* Displays a value *) -let pr_value env = function +let rec pr_value env = function | VVoid -> str "()" | VInteger n -> int n | VIntroPattern ipat -> pr_intro_pattern ipat | VConstr c | VConstr_context c -> (match env with Some env -> pr_lconstr_env env c | _ -> str "a term") | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "a tactic" + | VList [] -> str "an empty list" + | VList (a::_) -> + str "a list (first element is " ++ pr_value env a ++ str")" (* Transforms a named_context into a (string * constr) list *) let make_hyps = List.map (fun (id,_,typ) -> (id, typ)) @@ -213,7 +223,7 @@ let _ = (fun (s,t) -> add_primitive_tactic s t) [ "idtac",TacId []; "fail", TacFail(ArgArg 0,[]); - "fresh", TacArg(TacFreshId None) + "fresh", TacArg(TacFreshId []) ] let lookup_atomic id = Idmap.find id !atomic_mactab @@ -238,6 +248,34 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } +(* Tactics table (TacExtend). *) + +let tac_tab = Hashtbl.create 17 + +let add_tactic s t = + if Hashtbl.mem tac_tab s then + errorlabstrm ("Refiner.add_tactic: ") + (str ("Cannot redeclare tactic "^s)); + Hashtbl.add tac_tab s t + +let overwriting_add_tactic s t = + if Hashtbl.mem tac_tab s then begin + Hashtbl.remove tac_tab s; + warning ("Overwriting definition of tactic "^s) + end; + Hashtbl.add tac_tab s t + +let lookup_tactic s = + try + Hashtbl.find tac_tab s + with Not_found -> + errorlabstrm "Refiner.lookup_tactic" + (str"The tactic " ++ str s ++ str" is not installed") +(* +let vernac_tactic (s,args) = + let tacfun = lookup_tactic s args in + abstract_extended_tactic s args tacfun +*) (* Interpretation of extra generic arguments *) type glob_sign = { ltacvars : identifier list * identifier list; @@ -331,9 +369,9 @@ let intern_hyp ist (loc,id as locid) = let intern_hyp_or_metaid ist id = intern_hyp ist (skip_metaid id) -let intern_int_or_var ist = function +let intern_or_var ist = function | ArgVar locid -> ArgVar (intern_hyp ist locid) - | ArgArg n as x -> x + | ArgArg _ as x -> x let intern_inductive ist = function | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) @@ -495,7 +533,7 @@ let intern_inversion_strength lf ist = function (* Interprets an hypothesis name *) let intern_hyp_location ist ((occs,id),hl) = - ((List.map (intern_int_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl) + ((List.map (intern_or_var ist) occs,intern_hyp ist (skip_metaid id)), hl) let interp_constrpattern_gen sigma env ltacvar c = let c = intern_gen false ~allow_soapp:true ~ltacvars:(ltacvar,[]) @@ -527,7 +565,7 @@ let internalise_tacarg ch = G_xml.parse_tactic_arg ch let extern_tacarg ch env sigma = function | VConstr c -> !print_xml_term ch env sigma c | VTactic _ | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ - | VIntroPattern _ | VRec _ -> + | VIntroPattern _ | VRec _ | VList _ -> error "Only externing of terms is implemented" let extern_request ch req gl la = @@ -625,13 +663,13 @@ let rec intern_atomic lf ist x = (* Automation tactics *) | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l) | TacAuto (n,lems,l) -> - TacAuto (option_map (intern_int_or_var ist) n, + TacAuto (option_map (intern_or_var ist) n, List.map (intern_constr ist) lems,l) | TacAutoTDB n -> TacAutoTDB n | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id) | TacDestructConcl -> TacDestructConcl | TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2) - | TacDAuto (n,p) -> TacDAuto (option_map (intern_int_or_var ist) n,p) + | TacDAuto (n,p) -> TacDAuto (option_map (intern_or_var ist) n,p) (* Derived basic tactics *) | TacSimpleInduction h -> @@ -676,7 +714,8 @@ let rec intern_atomic lf ist x = TacReduce (intern_red_expr ist r, clause_app (intern_hyp_location ist) cl) | TacChange (occl,c,cl) -> TacChange (option_map (intern_constr_occurrence ist) occl, - intern_constr ist c, clause_app (intern_hyp_location ist) cl) + (if occl = None then intern_type ist c else intern_constr ist c), + clause_app (intern_hyp_location ist) cl) (* Equivalence relations *) | TacReflexivity -> TacReflexivity @@ -728,7 +767,7 @@ and intern_tactic_seq ist = function ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr) | TacId l -> ist.ltacvars, TacId (intern_message ist l) | TacFail (n,l) -> - ist.ltacvars, TacFail (intern_int_or_var ist n,intern_message ist l) + ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l) | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac) | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s) | TacThen (t1,t2) -> @@ -741,7 +780,7 @@ and intern_tactic_seq ist = function lfun', TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl) | TacDo (n,tac) -> - ist.ltacvars, TacDo (intern_int_or_var ist n,intern_tactic ist tac) + ist.ltacvars, TacDo (intern_or_var ist n,intern_tactic ist tac) | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac) | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac) | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac) @@ -776,7 +815,7 @@ and intern_tacarg strict ist = function List.map (intern_tacarg !strict_check ist) l) | TacExternal (loc,com,req,la) -> TacExternal (loc,com,req,List.map (intern_tacarg !strict_check ist) la) - | TacFreshId _ as x -> x + | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) | Tacexp t -> Tacexp (intern_tactic ist t) | TacDynamic(loc,t) as x -> (match tag t with @@ -803,7 +842,7 @@ and intern_genarg ist x = | IntArgType -> in_gen globwit_int (out_gen rawwit_int x) | IntOrVarArgType -> in_gen globwit_int_or_var - (intern_int_or_var ist (out_gen rawwit_int_or_var x)) + (intern_or_var ist (out_gen rawwit_int_or_var x)) | StringArgType -> in_gen globwit_string (out_gen rawwit_string x) | PreIdentArgType -> @@ -1045,6 +1084,19 @@ let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid | ArgArg n -> n +let int_or_var_list_of_VList = function + | VList l -> List.map (fun n -> ArgArg (coerce_to_int n)) l + | _ -> raise Not_found + +let interp_int_or_var_as_list ist = function + | ArgVar (_,id as locid) -> + (try int_or_var_list_of_VList (List.assoc id ist.lfun) + with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)]) + | ArgArg n as x -> [x] + +let interp_int_or_var_list ist l = + List.flatten (List.map (interp_int_or_var_as_list ist) l) + let constr_of_value env = function | VConstr csr -> csr | VIntroPattern (IntroIdentifier id) -> constr_of_id env id @@ -1065,6 +1117,17 @@ let interp_hyp ist gl (loc,id as locid) = if is_variable env id then id else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found") +let hyp_list_of_VList env = function + | VList l -> List.map (coerce_to_hyp env) l + | _ -> raise Not_found + +let interp_hyp_list_as_list ist gl (loc,id as x) = + try hyp_list_of_VList (pf_env gl) (List.assoc id ist.lfun) + with Not_found | CannotCoerceTo _ -> [interp_hyp ist gl x] + +let interp_hyp_list ist gl l = + List.flatten (List.map (interp_hyp_list_as_list ist gl) l) + let interp_clause_pattern ist gl (l,occl) = let rec check acc = function | (hyp,l) :: rest -> @@ -1126,8 +1189,7 @@ let interp_evaluable ist env = function (* Interprets an hypothesis name *) let interp_hyp_location ist gl ((occs,id),hl) = - ((List.map (fun n -> ArgArg (interp_int_or_var ist n)) occs, - interp_hyp ist gl id),hl) + ((interp_int_or_var_list ist occs,interp_hyp ist gl id),hl) let interp_clause ist gl { onhyps=ol; onconcl=b; concl_occs=occs } = { onhyps=option_map(List.map (interp_hyp_location ist gl)) ol; @@ -1157,11 +1219,25 @@ let rec intropattern_ids = function List.flatten (List.map intropattern_ids (List.flatten ll)) | IntroWildcard | IntroAnonymous -> [] -let rec extract_ids = function - | (id,VIntroPattern ipat)::tl -> intropattern_ids ipat @ extract_ids tl - | _::tl -> extract_ids tl +let rec extract_ids ids = function + | (id,VIntroPattern ipat)::tl when not (List.mem id ids) -> + intropattern_ids ipat @ extract_ids ids tl + | _::tl -> extract_ids ids tl | [] -> [] +let default_fresh_id = id_of_string "H" + +let interp_fresh_id ist gl l = + let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in + let avoid = extract_ids ids ist.lfun in + let id = + if l = [] then default_fresh_id + else + id_of_string (String.concat "" (List.map (function + | ArgArg s -> s + | ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l)) in + Tactics.fresh_id avoid id gl + (* To retype a list of key*constr with undefined key *) let retype_list sigma env lst = List.fold_right (fun (x,csr) a -> @@ -1210,7 +1286,7 @@ let solve_remaining_evars env initial_sigma evars c = Pretype_errors.error_unsolvable_implicit loc env sigma src) | _ -> map_constr proc_rec c in - map_constr proc_rec c + proc_rec c let interp_gen kind ist sigma env (c,ce) = let (ltacvars,unbndltacvars) = constr_list ist env in @@ -1254,20 +1330,33 @@ let pf_interp_open_constr casted ist gl cc = let pf_interp_constr ist gl = interp_constr ist (project gl) (pf_env gl) +let constr_list_of_VList env = function + | VList l -> List.map (constr_of_value env) l + | _ -> raise Not_found + +let pf_interp_constr_list_as_list ist gl (c,_ as x) = + match c with + | RVar (_,id) -> + (try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun) + with Not_found -> [interp_constr ist (project gl) (pf_env gl) x]) + | _ -> [interp_constr ist (project gl) (pf_env gl) x] + +let pf_interp_constr_list ist gl l = + List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l) + (* Interprets a type expression *) let pf_interp_type ist gl = interp_type ist (project gl) (pf_env gl) (* Interprets a reduction expression *) let interp_unfold ist env (l,qid) = - (l,interp_evaluable ist env qid) + (interp_int_or_var_list ist l,interp_evaluable ist env qid) let interp_flag ist env red = { red with rConst = List.map (interp_evaluable ist env) red.rConst } let interp_pattern ist sigma env (l,c) = - (List.map (fun n -> ArgArg (interp_int_or_var ist n)) l, - interp_constr ist sigma env c) + (interp_int_or_var_list ist l, interp_constr ist sigma env c) let pf_interp_pattern ist gl = interp_pattern ist (project gl) (pf_env gl) @@ -1296,11 +1385,39 @@ let interp_may_eval f ist gl = function user_err_loc (loc, "interp_may_eval", str "Unbound context identifier" ++ pr_id s)) | ConstrTypeOf c -> pf_type_of gl (f ist gl c) - | ConstrTerm c -> f ist gl c + | ConstrTerm c -> + try + f ist gl c + with e -> + begin + match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": interpretation of term " ++ + Printer.pr_rawconstr_env (pf_env gl) (fst c) ++ + str " raised an exception" ++ + fnl() ++ + !Tactic_debug.explain_logic_error_no_anomaly e) + | _ -> () + end; + raise e (* Interprets a constr expression possibly to first evaluate *) let interp_constr_may_eval ist gl c = - let csr = interp_may_eval pf_interp_constr ist gl c in + let csr = + try + interp_may_eval pf_interp_constr ist gl c + with e -> + begin match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": evaluation of term raised an exception" ++ + fnl() ++ + !Tactic_debug.explain_logic_error_no_anomaly e) + | _ -> () + end; + raise e + in begin db_constr ist.debug (pf_env gl) csr; csr @@ -1312,6 +1429,7 @@ let message_of_value = function | VIntroPattern ipat -> pr_intro_pattern ipat | VConstr_context c | VConstr c -> pr_constr c | VRec _ | VTactic _ | VRTactic _ | VFun _ -> str "<tactic>" + | VList _ -> str "<list>" let rec interp_message ist = function | [] -> mt() @@ -1380,12 +1498,16 @@ let interp_binding ist gl (loc,b,c) = let interp_bindings ist gl = function | NoBindings -> NoBindings -| ImplicitBindings l -> ImplicitBindings (List.map (pf_interp_constr ist gl) l) +| ImplicitBindings l -> ImplicitBindings (pf_interp_constr_list ist gl l) | ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l) let interp_constr_with_bindings ist gl (c,bl) = (pf_interp_constr ist gl c, interp_bindings ist gl bl) +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)) +let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c) + (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1453,9 +1575,8 @@ and interp_tacarg ist gl = function interp_app ist gl fv largs loc | TacExternal (loc,com,req,la) -> interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la) - | TacFreshId idopt -> - let s = match idopt with None -> "H" | Some s -> s in - let id = Tactics.fresh_id (extract_ids ist.lfun) (id_of_string s) gl in + | TacFreshId l -> + let id = interp_fresh_id ist gl l in VIntroPattern (IntroIdentifier id) | Tacexp t -> val_interp ist gl t | TacDynamic(_,t) -> @@ -1481,7 +1602,31 @@ and interp_app ist gl fv largs loc = | VFun(olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then - let v = val_interp { ist with lfun=newlfun@olfun } gl body in + let v = + let res = + try + val_interp { ist with lfun=newlfun@olfun } gl body + with e -> + begin match ist.debug with + DebugOn lev -> + safe_msgnl + (str "Level " ++ int lev ++ + str ": evaluation raises an exception" ++ + fnl() ++ + !Tactic_debug.explain_logic_error_no_anomaly e) + | _ -> () + end; + raise e + in + (match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": evaluation returns" ++ fnl() ++ + pr_value (Some (pf_env gl)) res) + | _ -> ()); + res + in + if lval=[] then locate_tactic_call loc v else interp_app ist gl v lval loc else @@ -1559,52 +1704,52 @@ and interp_match_context ist g lz lr lmr = let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps = let (lgoal,ctxt) = match_subterm nocc c csr in let lctxt = give_context ctxt id in - try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps - with e when is_match_catchable e -> - apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in + try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps + with e when is_match_catchable e -> + apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in let rec apply_match_context ist env goal nrs lex lpt = begin - if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); - match lpt with - | (All t)::tl -> - begin - db_mc_pattern_success ist.debug; - try eval_with_fail ist lz goal t - with e when is_match_catchable e -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl - end - | (Pat (mhyps,mgoal,mt))::tl -> - let hyps = make_hyps (pf_hyps goal) in - let hyps = if lr then List.rev hyps else hyps in - let mhyps = List.rev mhyps (* Sens naturel *) in - let concl = pf_concl goal in - (match mgoal with - | Term mg -> - (try - let lgoal = matches mg concl in - db_matched_concl ist.debug (pf_env goal) concl; - apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps - with e when is_match_catchable e -> - (match e with - | PatternMatchingFailure -> db_matching_failure ist.debug - | Eval_fail s -> db_eval_failure ist.debug s - | _ -> db_logic_failure ist.debug e); - apply_match_context ist env goal (nrs+1) (List.tl lex) tl) - | Subterm (id,mg) -> - (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps - with - | PatternMatchingFailure -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) - | _ -> - errorlabstrm "Tacinterp.apply_match_context" - (v 0 (str "No matching clauses for match goal" ++ - (if ist.debug=DebugOff then - fnl() ++ str "(use \"Debug On\" for more info)" - else mt()))) + if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); + match lpt with + | (All t)::tl -> + begin + db_mc_pattern_success ist.debug; + try eval_with_fail ist lz goal t + with e when is_match_catchable e -> + apply_match_context ist env goal (nrs+1) (List.tl lex) tl + end + | (Pat (mhyps,mgoal,mt))::tl -> + let hyps = make_hyps (pf_hyps goal) in + let hyps = if lr then List.rev hyps else hyps in + let mhyps = List.rev mhyps (* Sens naturel *) in + let concl = pf_concl goal in + (match mgoal with + | Term mg -> + (try + let lgoal = matches mg concl in + db_matched_concl ist.debug (pf_env goal) concl; + apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps + with e when is_match_catchable e -> + (match e with + | PatternMatchingFailure -> db_matching_failure ist.debug + | Eval_fail s -> db_eval_failure ist.debug s + | _ -> db_logic_failure ist.debug e); + apply_match_context ist env goal (nrs+1) (List.tl lex) tl) + | Subterm (id,mg) -> + (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps + with + | PatternMatchingFailure -> + apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) + | _ -> + errorlabstrm "Tacinterp.apply_match_context" + (v 0 (str "No matching clauses for match goal" ++ + (if ist.debug=DebugOff then + fnl() ++ str "(use \"Debug On\" for more info)" + else mt()))) end in let env = pf_env g in - apply_match_context ist env g 0 lmr - (read_match_rule (fst (constr_list ist env)) lmr) + apply_match_context ist env g 0 lmr + (read_match_rule (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = @@ -1679,6 +1824,8 @@ and interp_genarg ist gl x = | BindingsArgType -> in_gen wit_bindings (interp_bindings ist gl (out_gen globwit_bindings x)) + | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x + | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x | List0ArgType _ -> app_list0 (interp_genarg ist gl) x | List1ArgType _ -> app_list1 (interp_genarg ist gl) x | OptArgType _ -> app_opt (interp_genarg ist gl) x @@ -1691,6 +1838,16 @@ and interp_genarg ist gl x = | None -> lookup_interp_genarg s ist gl x +and interp_genarg_constr_list0 ist gl x = + let lc = out_gen (wit_list0 globwit_constr) x in + let lc = pf_interp_constr_list ist gl lc in + in_gen (wit_list0 wit_constr) lc + +and interp_genarg_constr_list1 ist gl x = + let lc = out_gen (wit_list1 globwit_constr) x in + let lc = pf_interp_constr_list ist gl lc in + in_gen (wit_list1 wit_constr) lc + (* Interprets the Match expressions *) and interp_match ist g lz constr lmr = let rec apply_match_subterm ist nocc (id,c) csr mt = @@ -1706,26 +1863,115 @@ and interp_match ist g lz constr lmr = (try eval_with_fail ist lz g t with e when is_match_catchable e -> apply_match ist csr []) | (Pat ([],Term c,mt))::tl -> - (try - let lm = matches c csr in - let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in - eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt - with e when is_match_catchable e -> apply_match ist csr tl) + (try let lm = + (try matches c csr with + e -> + (match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": matching with pattern" ++ fnl() ++ + Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++ + str "raised the exception" ++ fnl() ++ + !Tactic_debug.explain_logic_error_no_anomaly e) + | _ -> ()); raise e) in + (try let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in + eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt + with e -> + (match ist.debug with + DebugOn lev -> + safe_msgnl (str "rule body for pattern" ++ fnl() ++ + Printer.pr_constr_pattern_env (pf_env g) c ++ fnl() ++ + str "raised the exception" ++ fnl() ++ + !Tactic_debug.explain_logic_error_no_anomaly e) + | _ -> ()); raise e) + with e when is_match_catchable e -> + (match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ":switching to the next rule"); + | DebugOff -> ()); + apply_match ist csr tl) + | (Pat ([],Subterm (id,c),mt))::tl -> (try apply_match_subterm ist 0 (id,c) csr mt with PatternMatchingFailure -> apply_match ist csr tl) | _ -> errorlabstrm "Tacinterp.apply_match" (str "No matching clauses for match") in - let csr = interp_ltac_constr ist g constr in + let csr = + try interp_ltac_constr ist g constr with + e -> (match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": evaluation of the matched expression raised " ++ + str "the exception" ++ fnl() ++ + !Tactic_debug.explain_logic_error e) + | _ -> ()); raise e in let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in - apply_match ist csr ilr + let res = + try apply_match ist csr ilr with + e -> + begin match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": match expression failed with error" ++ fnl() ++ + !Tactic_debug.explain_logic_error e) + | _ -> () + end; + raise e in + (if ist.debug <> DebugOff then + safe_msgnl (str "match expression returns " ++ + pr_value (Some (pf_env g)) res)); + res (* Interprets tactic expressions : returns a "constr" *) and interp_ltac_constr ist gl e = - try constr_of_value (pf_env gl) (val_interp ist gl e) + let result = + try (val_interp ist gl e) with Not_found -> + begin match ist.debug with + DebugOn lev -> + safe_msgnl (str "Level " ++ int lev ++ + str ": evaluation failed for" ++ fnl() ++ + Pptactic.pr_glob_tactic (pf_env gl) e) + | _ -> () + end; + raise Not_found in + try let cresult = constr_of_value (pf_env gl) result in + (if !debug <> DebugOff then + safe_msgnl (Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ + str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult); + cresult) + with Not_found -> - errorlabstrm "" (str "Must evaluate to a term") + errorlabstrm "" + (str "Must evaluate to a term" ++ fnl() ++ + str "offending expression: " ++ fnl() ++ + Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++ str "this is a " ++ + (match result with + VTactic _ -> str "VTactic" + | VRTactic _ -> str "VRTactic" + | VFun (il,ul,b) -> + (str "VFun with body " ++ fnl() ++ + Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++ + str "instantiated arguments " ++ fnl() ++ + List.fold_right + (fun p s -> + let (i,v) = p in str (string_of_id i) ++ str ", " ++ s) + il (str "") ++ + str "uninstantiated arguments " ++ fnl() ++ + List.fold_right + (fun opt_id s -> + (match opt_id with + Some id -> str (string_of_id id) + | None -> str "_") ++ str ", " ++ s) + ul (str "")) + | VVoid -> str "VVoid" + | VInteger _ -> str "VInteger" + | VConstr _ -> str "VConstr" + | VIntroPattern _ -> str "VIntroPattern" + | VConstr_context _ -> str "VConstrr_context" + | VRec _ -> str "VRec" + | VList _ -> str "VList")) (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = @@ -1767,7 +2013,7 @@ and interp_atomic ist gl = function abstract_tactic (TacAssert (t,ipat,c)) (Tactics.forward (option_map (interp_tactic ist) t) (interp_intro_pattern ist gl ipat) c) - | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl) + | TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (na,c,clp) -> let clp = interp_clause ist gl clp in @@ -1781,11 +2027,11 @@ and interp_atomic ist gl = function *) (* Automation tactics *) | TacTrivial (lems,l) -> - Auto.h_trivial (List.map (pf_interp_constr ist gl) lems) + Auto.h_trivial (pf_interp_constr_list ist gl lems) (option_map (List.map (interp_hint_base ist)) l) | TacAuto (n,lems,l) -> Auto.h_auto (option_map (interp_int_or_var ist) n) - (List.map (pf_interp_constr ist gl) lems) + (pf_interp_constr_list ist gl lems) (option_map (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) @@ -1820,8 +2066,8 @@ and interp_atomic ist gl = function | TacLApply c -> h_lapply (pf_interp_constr ist gl c) (* Context management *) - | TacClear (b,l) -> h_clear b (List.map (interp_hyp ist gl) l) - | TacClearBody l -> h_clear_body (List.map (interp_hyp ist gl) l) + | TacClear (b,l) -> h_clear b (interp_hyp_list ist gl l) + | TacClearBody l -> h_clear_body (interp_hyp_list ist gl l) | TacMove (dep,id1,id2) -> h_move dep (interp_hyp ist gl id1) (interp_hyp ist gl id2) | TacRename (id1,id2) -> @@ -1842,7 +2088,9 @@ and interp_atomic ist gl = function h_reduce (pf_interp_red_expr ist gl r) (interp_clause ist gl cl) | TacChange (occl,c,cl) -> h_change (option_map (pf_interp_pattern ist gl) occl) - (pf_interp_constr ist gl c) (interp_clause ist gl cl) + (if occl = None then pf_interp_type ist gl c + else pf_interp_constr ist gl c) + (interp_clause ist gl cl) (* Equivalence relations *) | TacReflexivity -> h_reflexivity @@ -1861,21 +2109,25 @@ and interp_atomic ist gl = function | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Inv.inv_clause k (interp_intro_pattern ist gl ids) - (List.map (interp_hyp ist gl) idl) + (interp_hyp_list ist gl idl) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (InversionUsing (c,idl),hyp) -> Leminv.lemInv_clause (interp_declared_or_quantified_hypothesis ist gl hyp) (pf_interp_constr ist gl c) - (List.map (interp_hyp ist gl) idl) + (interp_hyp_list ist gl idl) (* For extensions *) | TacExtend (loc,opn,l) -> - fun gl -> vernac_tactic (opn,List.map (interp_genarg ist gl) l) gl + let tac = lookup_tactic opn in + fun gl -> + let args = List.map (interp_genarg ist gl) l in + abstract_extended_tactic opn args (tac args) gl | TacAlias (loc,_,l,(_,body)) -> fun gl -> let rec f x = match genarg_tag x with - | IntArgType -> VInteger (out_gen globwit_int x) - | IntOrVarArgType -> - VInteger (interp_int_or_var ist (out_gen globwit_int_or_var x)) + | IntArgType -> + VInteger (out_gen globwit_int x) + | IntOrVarArgType -> + mk_int_or_var_value ist (out_gen globwit_int_or_var x) | PreIdentArgType -> failwith "pre-identifiers cannot be bound" | IntroPatternArgType -> @@ -1885,14 +2137,14 @@ and interp_atomic ist gl = function VIntroPattern (IntroIdentifier (interp_ident ist gl (out_gen globwit_ident x))) | VarArgType -> - VConstr (mkVar (interp_hyp ist gl (out_gen globwit_var x))) + mk_hyp_value ist gl (out_gen globwit_var x) | RefArgType -> VConstr (constr_of_global (pf_interp_reference ist gl (out_gen globwit_ref x))) - | SortArgType -> - VConstr (mkSort (interp_sort (out_gen globwit_sort x))) + | SortArgType -> + VConstr (mkSort (interp_sort (out_gen globwit_sort x))) | ConstrArgType -> - VConstr (pf_interp_constr ist gl (out_gen globwit_constr x)) + mk_constr_value ist gl (out_gen globwit_constr x) | ConstrMayEvalArgType -> VConstr (interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x)) @@ -1900,11 +2152,36 @@ and interp_atomic ist gl = function (* Special treatment of tactic arguments *) val_interp ist gl (out_gen (globwit_tactic (out_some (tactic_genarg_level s))) x) + | List0ArgType ConstrArgType -> + let wit = wit_list0 globwit_constr in + VList (List.map (mk_constr_value ist gl) (out_gen wit x)) + | List0ArgType VarArgType -> + let wit = wit_list0 globwit_var in + VList (List.map (mk_hyp_value ist gl) (out_gen wit x)) + | List0ArgType IntArgType -> + let wit = wit_list0 globwit_int in + VList (List.map (fun x -> VInteger x) (out_gen wit x)) + | List0ArgType IntOrVarArgType -> + let wit = wit_list0 globwit_int_or_var in + VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) + | List1ArgType ConstrArgType -> + let wit = wit_list1 globwit_constr in + VList (List.map (mk_constr_value ist gl) (out_gen wit x)) + | List1ArgType VarArgType -> + let wit = wit_list1 globwit_var in + VList (List.map (mk_hyp_value ist gl) (out_gen wit x)) + | List1ArgType IntArgType -> + let wit = wit_list1 globwit_int in + VList (List.map (fun x -> VInteger x) (out_gen wit x)) + | List1ArgType IntOrVarArgType -> + let wit = wit_list1 globwit_int_or_var in + VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) | StringArgType | BoolArgType | QuantHypArgType | RedExprArgType | OpenConstrArgType _ | ConstrWithBindingsArgType | ExtraArgType _ | BindingsArgType - | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ + | OptArgType _ | PairArgType _ + | List0ArgType _ | List1ArgType _ -> error "This generic type is not supported in alias" in @@ -1925,7 +2202,7 @@ let interp_tac_gen lfun debug t gl = ltacvars = (List.map fst lfun, []); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } t) gl -let eval_tactic t = interp_tactic { lfun=[]; debug=get_debug() } t +let eval_tactic t gls = interp_tactic { lfun=[]; debug=get_debug() } t gls let interp t = interp_tac_gen [] (get_debug()) t @@ -1941,7 +2218,8 @@ let hide_interp t ot gl = let t = eval_tactic te in match ot with | None -> abstract_tactic_expr (TacArg (Tacexp te)) t gl - | Some t' -> abstract_tactic_expr (TacArg (Tacexp te)) (tclTHEN t t') gl + | Some t' -> + abstract_tactic_expr ~dflt:true (TacArg (Tacexp te)) (tclTHEN t t') gl (***************************************************************************) (* Substitution at module closing time *) @@ -1973,7 +2251,7 @@ let subst_induction_arg subst = function | ElimOnIdent id as x -> x let subst_and_short_name f (c,n) = - assert (n=None); (* since tacdef are strictly globalized *) +(* assert (n=None); *)(* since tacdef are strictly globalized *) (f c,None) let subst_or_var f = function @@ -2170,9 +2448,11 @@ and subst_tacarg subst = function TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) - | TacDynamic(_,t) as x -> + | TacDynamic(the_loc,t) as x -> (match tag t with - | "tactic" | "value" | "constr" -> x + | "tactic" | "value" -> x + | "constr" -> + TacDynamic(the_loc, constr_in (subst_mps subst (constr_out t))) | s -> anomaly_loc (dloc, "Tacinterp.val_interp", str "Unknown dynamic: <" ++ str s ++ str ">")) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 7c0180a6..01e7750a 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 8975 2006-06-23 08:52:53Z herbelin $ i*) +(*i $Id: tacinterp.mli 9178 2006-09-26 11:18:22Z barras $ i*) (*i*) open Dyn @@ -34,6 +34,7 @@ type value = | VIntroPattern of intro_pattern_expr | VConstr of constr | VConstr_context of constr + | VList of value list | VRec of value ref (* Signature for interpretation: val\_interp and interpretation functions *) @@ -63,6 +64,14 @@ val add_tacdef : bool -> (identifier Util.located * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit +(* Tactic extensions *) +val add_tactic : + string -> (closed_generic_argument list -> tactic) -> unit +val overwriting_add_tactic : + string -> (closed_generic_argument list -> tactic) -> unit +val lookup_tactic : + string -> (closed_generic_argument list) -> tactic + (* Adds an interpretation function for extra generic arguments *) type glob_sign = { ltacvars : identifier list * identifier list; @@ -84,6 +93,9 @@ val interp_genarg : val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument +val intern_tactic : + glob_sign -> raw_tactic_expr -> glob_tactic_expr + val intern_constr : glob_sign -> constr_expr -> rawconstr_and_expr diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index ff6ac41a..06289169 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacticals.ml 8878 2006-05-30 16:44:25Z herbelin $ *) +(* $Id: tacticals.ml 9211 2006-10-05 12:38:33Z letouzey $ *) open Pp open Util @@ -68,6 +68,7 @@ let tclTHENTRY = tclTHENTRY let tclIFTHENELSE = tclIFTHENELSE let tclIFTHENSELSE = tclIFTHENSELSE let tclIFTHENSVELSE = tclIFTHENSVELSE +let tclIFTHENTRYELSEMUST = tclIFTHENTRYELSEMUST let unTAC = unTAC diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 7ceddc8b..458ab732 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacticals.mli 7909 2006-01-21 11:09:18Z herbelin $ i*) +(*i $Id: tacticals.mli 9211 2006-10-05 12:38:33Z letouzey $ i*) (*i*) open Pp @@ -64,7 +64,7 @@ val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic - +val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic val unTAC : tactic -> goal sigma -> proof_tree sigma diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4eaf0259..f77814de 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 8878 2006-05-30 16:44:25Z herbelin $ *) +(* $Id: tactics.ml 9281 2006-10-26 07:52:31Z herbelin $ *) open Pp open Util @@ -245,20 +245,22 @@ 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 = - next_global_ident_away true id (avoid@(pf_ids_of_hyps gl)) + fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id let id_of_name_with_default s = function | Anonymous -> id_of_string s | Name id -> id -let default_id gl = function +let default_id env sigma = function | (name,None,t) -> - (match kind_of_term (pf_whd_betadeltaiota gl (pf_type_of gl t)) with - | Sort (Prop _) -> (id_of_name_with_default "H" name) - | Sort (Type _) -> (id_of_name_with_default "X" name) - | _ -> anomaly "Wrong sort") - | (name,Some b,_) -> id_of_name_using_hdchar (pf_env gl) b name + (match Typing.sort_of env sigma t with + | Prop _ -> (id_of_name_with_default "H" name) + | Type _ -> (id_of_name_with_default "X" name)) + | (name,Some b,_) -> id_of_name_using_hdchar env b name (* Non primitive introduction tactics are treated by central_intro There is possibly renaming, with possibly names to avoid and @@ -270,14 +272,32 @@ type intro_name_flag = | IntroMustBe of identifier let find_name decl gl = function - | IntroAvoid idl -> - let id = fresh_id idl (default_id gl decl) gl in id + | IntroAvoid idl -> + (* this case must be compatible with [find_intro_names] below. *) + let id = fresh_id idl (default_id (pf_env gl) gl.sigma decl) gl in id | IntroBasedOn (id,idl) -> fresh_id idl id gl | IntroMustBe id -> let id' = fresh_id [] id gl in if id' <> id then error ((string_of_id id)^" is already used"); id' +(* Returns the names that would be created by intros, without doing + intros. This function is supposed to be compatible with an + iteration of [find_name] above. As [default_id] checks the sort of + the type to build hyp names, we maintain an environment to be able + to type dependent hyps. *) +let find_intro_names ctxt gl = + let _, res = List.fold_right + (fun decl acc -> + let wantedname,x,typdecl = decl in + let env,idl = acc in + let name = fresh_id idl (default_id env gl.sigma decl) gl in + let newenv = push_rel (wantedname,x,typdecl) env in + (newenv,(name::idl))) + ctxt (pf_env gl , []) in + List.rev res + + let build_intro_tac id = function | None -> introduction id | Some dest -> tclTHEN (introduction id) (move_hyp true id dest) @@ -427,12 +447,9 @@ let rec intros_rmove = function move_to_rhyp destopt; intros_rmove rest ] -(****************************************************) -(* Resolution tactics *) -(****************************************************) - -(* Refinement tactic: unification with the head of the head normal form - * of the type of a term. *) +(**************************) +(* Refinement tactics *) +(**************************) let apply_type hdcty argl gl = refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl @@ -448,6 +465,48 @@ let bring_hyps hyps = let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in refine_no_check (mkApp (f, instance_from_named_context hyps)) gl) +(**************************) +(* Cut tactics *) +(**************************) + +let cut c gl = + match kind_of_term (hnf_type_of gl c) with + | Sort _ -> + let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in + let t = mkProd (Anonymous, c, pf_concl gl) in + tclTHENFIRST + (internal_cut_rev id c) + (tclTHEN (apply_type t [mkVar id]) (thin [id])) + gl + | _ -> error "Not a proposition or a type" + +let cut_intro t = tclTHENFIRST (cut t) intro + +(* let cut_replacing id t tac = + tclTHENS (cut t) + [tclORELSE + (intro_replacing id) + (tclORELSE (intro_erasing id) (intro_using id)); + tac (refine_no_check (mkVar id)) ] *) + +(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le + but, ou dans une autre hypothèse *) +let cut_replacing id t tac = + tclTHENS (cut t) [ + tclORELSE (intro_replacing id) (intro_erasing id); + tac (refine_no_check (mkVar id)) ] + +let cut_in_parallel l = + let rec prec = function + | [] -> tclIDTAC + | h::t -> tclTHENFIRST (cut h) (prec t) + in + prec (List.rev l) + +(****************************************************) +(* Resolution tactics *) +(****************************************************) + (* Resolution with missing arguments *) let apply_with_bindings (c,lbind) gl = @@ -459,7 +518,7 @@ let apply_with_bindings (c,lbind) gl = try let n = nb_prod thm_ty - nb_prod (pf_concl gl) in if n<0 then error "Apply: theorem has not enough premisses."; - let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in + let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause gl with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn -> let red_thm = @@ -470,7 +529,7 @@ let apply_with_bindings (c,lbind) gl = with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) -> (* Last chance: if the head is a variable, apply may try second order unification *) - let clause = make_clenv_binding_apply gl (-1) (c,thm_ty0) lbind in + let clause = make_clenv_binding_apply gl None (c,thm_ty0) lbind in Clenvtac.res_pf clause gl let apply c = apply_with_bindings (c,NoBindings) @@ -485,6 +544,44 @@ let apply_without_reduce c gl = let clause = mk_clenv_type_of gl c in res_pf clause gl +(* [apply_in hyp c] replaces + + hyp : forall y1, ti -> t hyp : rho(u) + ======================== with ============ and the ======= + goal goal rho(ti) + + assuming that [c] has type [forall x1..xn -> t' -> u] for some [t] + unifiable with [t'] with unifier [rho] +*) + +let find_matching_clause unifier clause = + let rec find clause = + try unifier clause + with exn when catchable_exception exn -> + try find (clenv_push_prod clause) + with NotExtensibleClause -> failwith "Cannot apply" + in find clause + +let apply_in_once gls innerclause (d,lbind) = + let thm = nf_betaiota (pf_type_of gls d) in + let clause = make_clenv_binding gls (d,thm) lbind in + let ordered_metas = List.rev (clenv_independent clause) in + if ordered_metas = [] then error "Statement without assumptions"; + let f mv = find_matching_clause (clenv_fchain mv clause) innerclause in + try list_try_find f ordered_metas + with Failure _ -> error "Unable to unify" + +let apply_in id lemmas gls = + let t' = pf_get_hyp_typ gls id in + let innermostclause = mk_clenv_from_n gls (Some 0) (mkVar id,t') in + let clause = List.fold_left (apply_in_once gls) innermostclause lemmas in + let new_hyp_prf = clenv_value clause in + let new_hyp_typ = clenv_type clause in + tclTHEN + (tclEVARS (evars_of clause.env)) + (cut_replacing id new_hyp_typ + (fun x gls -> refine_no_check new_hyp_prf gls)) gls + (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -502,45 +599,14 @@ let apply_without_reduce c gl = end. *) -(**************************) -(* Cut tactics *) -(**************************) - let cut_and_apply c gl = let goal_constr = pf_concl gl in - match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with - | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> - tclTHENLAST - (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())]) - (apply_term c [mkMeta (new_meta())]) gl - | _ -> error "Imp_elim needs a non-dependent product" - -let cut c gl = - match kind_of_term (hnf_type_of gl c) with - | Sort _ -> - let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in - let t = mkProd (Anonymous, c, pf_concl gl) in - tclTHENFIRST - (internal_cut_rev id c) - (tclTHEN (apply_type t [mkVar id]) (thin [id])) - gl - | _ -> error "Not a proposition or a type" - -let cut_intro t = tclTHENFIRST (cut t) intro - -let cut_replacing id t tac = - tclTHENS (cut t) - [tclORELSE - (intro_replacing id) - (tclORELSE (intro_erasing id) (intro_using id)); - tac (refine_no_check (mkVar id)) ] - -let cut_in_parallel l = - let rec prec = function - | [] -> tclIDTAC - | h::t -> tclTHENFIRST (cut h) (prec t) - in - prec (List.rev l) + match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with + | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) -> + tclTHENLAST + (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())]) + (apply_term c [mkMeta (new_meta())]) gl + | _ -> error "Imp_elim needs a non-dependent product" (********************************************************************) (* Exact tactics *) @@ -717,7 +783,7 @@ let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl = let indclause = make_clenv_binding gl (c,t) lbindc in let elimt = pf_type_of gl elimc in let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in - elimtac elimclause indclause gl + elimtac elimclause indclause gl let general_elim c e ?(allow_K=true) = general_elim_clause (elimination_clause_scheme allow_K) c e @@ -747,6 +813,14 @@ let elim (c,lbindc as cx) elim = let simplest_elim c = default_elim (c,NoBindings) (* Elimination in hypothesis *) +(* Typically, elimclause := (eq_ind ?x ?P ?H ?y ?Heq : ?P ?y) + indclause : forall ..., hyps -> a=b (to take place of ?Heq) + id : phi(a) (to take place of ?H) + and the result is to overwrite id with the proof of phi(b) + + but this generalizes to any elimination scheme with one constructor + (e.g. it could replace id:A->B->C by id:C, knowing A/\B) +*) let elimination_in_clause_scheme id elimclause indclause gl = let (hypmv,indmv) = @@ -757,8 +831,7 @@ let elimination_in_clause_scheme id elimclause indclause gl = let elimclause' = clenv_fchain indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = pf_type_of gl hyp in - let hypclause = - mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in + let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in let elimclause'' = clenv_fchain hypmv elimclause' hypclause in let new_hyp_prf = clenv_value elimclause'' in let new_hyp_typ = clenv_type elimclause'' in @@ -1145,13 +1218,18 @@ let consume_pattern avoid id gl = function (IntroIdentifier (fresh_id avoid id gl), names) | pat::names -> (pat,names) +let re_intro_dependent_hypotheses tophyp (lstatus,rstatus) = + let newlstatus = (* if some IH has taken place at the top of hyps *) + List.map (function (hyp,None) -> (hyp,tophyp) | x -> x) lstatus in + tclTHEN + (intros_rmove rstatus) + (intros_move newlstatus) + type elim_arg_kind = RecArg | IndArg | OtherArg let induct_discharge statuslists destopt avoid' (avoid,ra) names gl = let avoid = avoid @ avoid' in - let (lstatus,rstatus) = statuslists in - let tophyp = ref None in - let rec peel_tac ra names gl = match ra with + let rec peel_tac ra names tophyp gl = match ra with | (RecArg,recvarname) :: (IndArg,hyprecname) :: ra' -> let recpat,names = match names with @@ -1160,36 +1238,35 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl = (pat, [IntroIdentifier id]) | _ -> consume_pattern avoid recvarname gl names in let hyprec,names = consume_pattern avoid hyprecname gl names in - (* This is buggy for intro-or-patterns with different first hypnames *) - if !tophyp=None then tophyp := first_name_buggy hyprec; + (* IH stays at top: we need to update tophyp *) + (* This is buggy for intro-or-patterns with different first hypnames *) + (* Would need to pass peel_tac as a continuation of intros_patterns *) + (* (or to have hypotheses classified by blocks...) *) + let tophyp = if tophyp=None then first_name_buggy hyprec else tophyp in tclTHENLIST [ intros_patterns avoid [] destopt [recpat]; intros_patterns avoid [] None [hyprec]; - peel_tac ra' names ] gl + peel_tac ra' names tophyp] gl | (IndArg,hyprecname) :: ra' -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid hyprecname gl names in - tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl + tclTHEN (intros_patterns avoid [] destopt [pat]) + (peel_tac ra' names tophyp) gl | (RecArg,recvarname) :: ra' -> let pat,names = consume_pattern avoid recvarname gl names in - tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl + tclTHEN (intros_patterns avoid [] destopt [pat]) + (peel_tac ra' names tophyp) gl | (OtherArg,_) :: ra' -> let pat,names = match names with | [] -> IntroAnonymous, [] | pat::names -> pat,names in - tclTHEN (intros_patterns avoid [] destopt [pat]) (peel_tac ra' names) gl + tclTHEN (intros_patterns avoid [] destopt [pat]) + (peel_tac ra' names tophyp) gl | [] -> check_unused_names names; - tclIDTAC gl + re_intro_dependent_hypotheses tophyp statuslists gl in - let intros_move lstatus = - let newlstatus = (* if some IH has taken place at the top of hyps *) - List.map (function (hyp,None) -> (hyp,!tophyp) | x -> x) lstatus in - intros_move newlstatus - in - tclTHENLIST [ peel_tac ra names; - intros_rmove rstatus; - intros_move lstatus ] gl + peel_tac ra names None gl (* - le recalcul de indtyp à chaque itération de atomize_one est pour ne pas s'embêter à regarder si un letin_tac ne fait pas des @@ -1648,8 +1725,13 @@ let compute_elim_sig ?elimc elimt = | hiname,Some _,hi -> error "cannot recognize an induction schema" | hiname,None,hi -> let hi_ind, hi_args = decompose_app hi in - let hi_is_ind = (* hi est d'un type inductif *) - match kind_of_term hi_ind with | Ind (mind,_) -> true | _ -> false in + let hi_is_ind = (* hi est d'un type globalisable *) + match kind_of_term hi_ind with + | Ind (mind,_) -> true + | Var _ -> true + | Const _ -> true + | Construct _ -> true + | _ -> false in let hi_args_enough = (* hi a le bon nbre d'arguments *) List.length hi_args = List.length params + !res.nargs -1 in (* FIXME: Ces deux tests ne sont pas suffisants. *) @@ -1827,6 +1909,7 @@ let recolle_clenv scheme lid elimclause gl = elimclause + (* Unification of the goal and the principle applied to meta variables: (elimc ?i ?j ?k...?l). This solves partly meta variables (and may produce new ones). Then refine with the resulting term with holes. @@ -1858,7 +1941,7 @@ let induction_from_context_l isrec elim_info lid names gl = + (if scheme.indarg <> None then 1 else 0) in (* Number of given induction args must be exact. *) if List.length lid <> nargs_indarg_farg + scheme.nparams then - error "not the right number of arguments given to induction scheme"; + error "not the right number of arguments given to induction scheme"; let env = pf_env gl in (* hyp0 is used for re-introducing hyps at the right place afterward. We chose the first element of the list of variables on which to diff --git a/tactics/tactics.mli b/tactics/tactics.mli index aaacee8f..48b9f432 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli 8878 2006-05-30 16:44:25Z herbelin $ i*) +(*i $Id: tactics.mli 9266 2006-10-24 09:03:15Z herbelin $ i*) (*i*) open Names @@ -58,6 +58,7 @@ val cofix : identifier option -> tactic (*s Introduction tactics. *) val fresh_id : identifier list -> identifier -> goal sigma -> identifier +val find_intro_names : rel_context -> goal sigma -> identifier list val intro : tactic val introf : tactic @@ -168,6 +169,8 @@ val apply_with_bindings : constr with_bindings -> tactic val cut_and_apply : constr -> tactic +val apply_in : identifier -> constr with_bindings list -> tactic + (*s Elimination tactics. *) |