From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- tactics/auto.ml | 2 +- tactics/auto.mli | 2 +- tactics/autorewrite.ml | 2 +- tactics/autorewrite.mli | 2 +- tactics/btermdn.ml | 5 +- tactics/btermdn.mli | 2 +- tactics/class_tactics.ml4 | 48 ++-- tactics/contradiction.ml | 2 +- tactics/contradiction.mli | 2 +- tactics/decl_interp.ml | 2 +- tactics/decl_interp.mli | 2 +- tactics/decl_proof_instr.ml | 2 +- tactics/decl_proof_instr.mli | 2 +- tactics/dhyp.ml | 2 +- tactics/dhyp.mli | 2 +- tactics/eauto.ml4 | 27 ++- tactics/eauto.mli | 4 +- tactics/elim.ml | 2 +- tactics/elim.mli | 2 +- tactics/elimschemes.ml | 2 +- tactics/elimschemes.mli | 2 +- tactics/eqdecide.ml4 | 2 +- tactics/eqschemes.ml | 2 +- tactics/eqschemes.mli | 2 +- tactics/equality.ml | 2 +- tactics/equality.mli | 2 +- tactics/evar_tactics.ml | 2 +- tactics/evar_tactics.mli | 2 +- tactics/extraargs.ml4 | 2 +- tactics/extraargs.mli | 2 +- tactics/extratactics.ml4 | 2 +- tactics/extratactics.mli | 2 +- tactics/hiddentac.ml | 2 +- tactics/hiddentac.mli | 2 +- tactics/hipattern.ml4 | 2 +- tactics/hipattern.mli | 2 +- tactics/inv.ml | 2 +- tactics/inv.mli | 2 +- tactics/leminv.ml | 2 +- tactics/nbtermdn.ml | 4 +- tactics/nbtermdn.mli | 4 +- tactics/refine.ml | 2 +- tactics/refine.mli | 2 +- tactics/rewrite.ml4 | 543 ++++++++++++++++++++++++++++--------------- tactics/tacinterp.ml | 6 +- tactics/tacinterp.mli | 2 +- tactics/tactic_option.ml | 57 +++++ tactics/tactic_option.mli | 18 ++ tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 2 +- tactics/tactics.ml | 9 +- tactics/tactics.mli | 2 +- tactics/tactics.mllib | 1 + tactics/tauto.ml4 | 2 +- tactics/termdn.ml | 14 +- tactics/termdn.mli | 4 +- 56 files changed, 558 insertions(+), 270 deletions(-) create mode 100644 tactics/tactic_option.ml create mode 100644 tactics/tactic_option.mli (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index e53e05d0..faf0482b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: auto.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/auto.mli b/tactics/auto.mli index 09af7f8c..9a0719fc 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: auto.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c81dcfed..09f80377 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: autorewrite.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Equality open Hipattern diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index d6fa2455..b7300cba 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: autorewrite.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Term diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index cf536bfd..73aac029 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: btermdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Term open Names @@ -79,8 +79,7 @@ struct | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l) | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c]) | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l) - | Sort s when is_small s -> Dn.Label(Term_dn.SortLabel (Some s), []) - | Sort _ -> Dn.Label(Term_dn.SortLabel None, []) + | Sort _ -> Dn.Label(Term_dn.SortLabel, []) | Evar _ -> Dn.Everything | _ -> Dn.Nothing diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 859890a4..14f9fb23 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: btermdn.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Term diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 7105e84d..afd13b4c 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: class_tactics.ml4 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -69,7 +69,7 @@ let evar_filter evi = { evi with evar_hyps = Environ.val_of_named_context hyps'; evar_filter = List.map (fun _ -> true) hyps' } - + let evars_to_goals p evm = let goals, evm' = Evd.fold @@ -85,6 +85,7 @@ let evars_to_goals p evm = if goals = [] then None else let goals = List.rev goals in + let evm' = evars_reset_evd evm' evm in Some (goals, evm') (** Typeclasses instance search tactic / eauto *) @@ -331,7 +332,14 @@ let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls } let solve_tac (x : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> if gls = [] then sk res fk else fk ()) fk gls } + { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> + if gls = [] then sk res fk else fk ()) fk gls } + +let solve_unif_tac : atac = + { skft = fun sk fk {it = gl; sigma = s} -> + try let s' = Evarconv.consider_remaining_unif_problems (Global.env ()) s in + normevars_tac.skft sk fk ({it=gl; sigma=s'}) + with _ -> fk () } let hints_tac hints = { skft = fun sk fk {it = gl,info; sigma = s} -> @@ -456,7 +464,6 @@ let then_tac (first : atac) (second : atac) : atac = let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = t.skft (fun x _ -> Some x) (fun _ -> None) gl - type run_list_res = (auto_result * run_list_res fk) option let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res = @@ -491,7 +498,7 @@ let run_on_evars ?(only_classes=true) ?(st=full_transparent_state) p evm tac = let res = run_list_tac tac p goals (make_autogoals ~only_classes ~st goals evm') in match get_result res with | None -> raise Not_found - | Some (evm', fk) -> Some (Evd.evars_reset_evd evm' evm, fk) + | Some (evm', fk) -> Some (evars_reset_evd evm' evm, fk) let eauto_tac hints = fix (or_tac (then_tac normevars_tac (hints_tac hints)) intro_tac) @@ -551,16 +558,31 @@ let rec merge_deps deps = function else hd :: merge_deps deps tl let evars_of_evi evi = - Intset.union (Evarutil.evars_of_term evi.evar_concl) - (match evi.evar_body with - | Evar_defined b -> Evarutil.evars_of_term b - | Evar_empty -> Intset.empty) + Intset.union (evars_of_term evi.evar_concl) + (Intset.union + (match evi.evar_body with + | Evar_empty -> Intset.empty + | Evar_defined b -> evars_of_term b) + (Evarutil.evars_of_named_context (evar_filtered_context evi))) + +let deps_of_constraints cstrs deps = + List.fold_right (fun (_, _, x, y) deps -> + let evs = Intset.union (evars_of_term x) (evars_of_term y) in + merge_deps evs deps) + cstrs deps + +let evar_dependencies evm = + Evd.fold + (fun ev evi acc -> + merge_deps (Intset.union (Intset.singleton ev) + (evars_of_evi evi)) acc) + evm [] let split_evars evm = - Evd.fold (fun ev evi acc -> - let deps = Intset.union (Intset.singleton ev) (evars_of_evi evi) in - merge_deps deps acc) - evm [] + let _, cstrs = extract_all_conv_pbs evm in + let evmdeps = evar_dependencies evm in + let deps = deps_of_constraints cstrs evmdeps in + List.sort Intset.compare deps let select_evars evs evm = Evd.fold (fun ev evi acc -> diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 44bde497..9ea4892e 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: contradiction.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Term diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 14dcb469..7306f875 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: contradiction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index eebce493..7866d640 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: decl_interp.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) open Util open Names diff --git a/tactics/decl_interp.mli b/tactics/decl_interp.mli index 2d8b2c1d..859db444 100644 --- a/tactics/decl_interp.mli +++ b/tactics/decl_interp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_interp.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Tacinterp open Decl_expr diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 02a0050d..f9a51afe 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_proof_instr.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Pp diff --git a/tactics/decl_proof_instr.mli b/tactics/decl_proof_instr.mli index 170269dc..6f8126ed 100644 --- a/tactics/decl_proof_instr.mli +++ b/tactics/decl_proof_instr.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: decl_proof_instr.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Refiner open Names diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 4a779edb..5b7e7e94 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: dhyp.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* Chet's comments about this tactic : diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 5af4e56b..a4be2e42 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: dhyp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index d101b9d7..2b25ad73 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: eauto.ml4 13344 2010-07-28 15:04:36Z msozeau $ *) open Pp open Util @@ -396,7 +396,7 @@ END let cons a l = a :: l -let autounfold db cl = +let autounfolds db occs = let unfolds = List.concat (List.map (fun dbname -> let db = try searchtable_map dbname with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname) @@ -404,7 +404,15 @@ let autounfold db cl = let (ids, csts) = Hint_db.unfolds db in Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) - in unfold_option unfolds cl + in unfold_option unfolds + +let autounfold db cls gl = + let cls = concrete_clause_of cls gl in + let tac = autounfolds db in + tclMAP (function + | OnHyp (id,occs,where) -> tac occs (Some (id,where)) + | OnConcl occs -> tac occs None) + cls gl let autosimpl db cl = let unfold_of_elts constr (b, elts) = @@ -419,12 +427,13 @@ let autosimpl db cl = unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db) in unfold_option unfolds cl +open Extraargs + TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) "in" hyp(id) ] -> - [ autounfold (match db with None -> ["core"] | Some x -> x) (Some (id, InHyp)) ] -| [ "autounfold" hintbases(db) ] -> - [ autounfold (match db with None -> ["core"] | Some x -> x) None ] - END +| [ "autounfold" hintbases(db) in_arg_hyp(id) ] -> + [ autounfold (match db with None -> Auto.current_db_names () | Some [] -> ["core"] | Some x -> x) + (glob_in_arg_hyp_to_clause id) ] +END let unfold_head env (ids, csts) c = let rec aux c = @@ -498,7 +507,7 @@ TACTIC EXTEND autounfoldify let db = match kind_of_term x with | Const c -> string_of_label (con_label c) | _ -> assert false - in autounfold ["core";db] None ] + in autounfold ["core";db] onConcl ] END TACTIC EXTEND unify diff --git a/tactics/eauto.mli b/tactics/eauto.mli index 331d2b44..eb90b1b6 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -17,6 +17,8 @@ open Environ open Explore (*i*) +val hintbases : hint_db_name list option Pcoq.Gram.Entry.e +val wit_hintbases : hint_db_name list option typed_abstract_argument_type val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type val rawwit_auto_using : constr_expr list raw_abstract_argument_type @@ -36,4 +38,4 @@ val eauto_with_bases : bool * int -> Term.constr list -> Auto.hint_db list -> Proof_type.tactic -val autounfold : hint_db_name list -> Tacticals.goal_location -> tactic +val autounfold : hint_db_name list -> Tacticals.clause -> tactic diff --git a/tactics/elim.ml b/tactics/elim.ml index 7f1d4249..0372a88d 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: elim.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/elim.mli b/tactics/elim.mli index 8ea6695a..fa18ab0b 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: elim.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 77c878fc..c82e8f64 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: elimschemes.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 795add12..ba0389e5 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: elimschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ *) open Ind_tables diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 7ed6bf1e..90e4b44c 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -14,7 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: eqdecide.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Util open Names diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 9972c2a5..22c3b47f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: eqschemes.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* File created by Hugo Herbelin, Nov 2009 *) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index ae3b1578..447fb359 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: eqschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (* This file builds schemes relative to equality inductive types *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 68f0cc7c..6b16adb4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: equality.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/equality.mli b/tactics/equality.mli index 7c09ae09..f14b3867 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: equality.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 78757939..3e2191d1 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: evar_tactics.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Util diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli index ed4a33ae..78412150 100644 --- a/tactics/evar_tactics.mli +++ b/tactics/evar_tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: evar_tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Tacmach open Names diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index bb63f6b9..c9b2a969 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: extraargs.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Pcoq diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index 22a0c2da..e53fc604 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extraargs.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Tacexpr open Term diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 7afd0543..e1ac42c2 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id$ *) +(* $Id: extratactics.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Pcoq diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 50757148..cfbc8f3d 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: extratactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Proof_type diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 12ecbd9a..220c00d3 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: hiddentac.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Term open Proof_type diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 7bd57cdd..1724bf9c 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: hiddentac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Names diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 3dc9403c..dfa596d3 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) -(* $Id$ *) +(* $Id: hipattern.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index f486f348..cf4cdd0d 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: hipattern.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/tactics/inv.ml b/tactics/inv.ml index 7290b66b..430f7d5f 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: inv.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/inv.mli b/tactics/inv.mli index 033082e9..eb899699 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: inv.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c102d8ec..76432dd8 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: leminv.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 26167978..bdea29df 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: nbtermdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Util open Names @@ -117,7 +117,7 @@ let constr_val_discr_st (idpred,cpred) t = | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l) | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c]) | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l) - | Sort s -> Dn.Label(Term_dn.SortLabel (Some s), []) + | Sort _ -> Dn.Label(Term_dn.SortLabel, []) | Evar _ -> Dn.Everything | _ -> Dn.Nothing diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index 3b90b12a..36c54bd3 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: nbtermdn.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Term @@ -24,7 +24,7 @@ sig | GRLabel of global_reference | ProdLabel | LambdaLabel - | SortLabel of sorts option + | SortLabel end type 'na t diff --git a/tactics/refine.ml b/tactics/refine.ml index 87769ccb..06a78011 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: refine.ml 13323 2010-07-24 15:57:30Z herbelin $ *) (* JCF -- 6 janvier 1998 EXPERIMENTAL *) diff --git a/tactics/refine.mli b/tactics/refine.mli index e847a749..55b4033b 100644 --- a/tactics/refine.mli +++ b/tactics/refine.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: refine.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) open Tacmach diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 010fd088..9d99ad96 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -135,8 +135,7 @@ let rewrite_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "rewrit let arrow_morphism a b = if isprop a && isprop b then Lazy.force impl - else - mkApp(Lazy.force arrow, [|a;b|]) + else Lazy.force arrow let setoid_refl pars x = applistc (Lazy.force setoid_refl_proj) (pars @ [x]) @@ -176,17 +175,18 @@ let new_cstr_evar (goal,cstr) env t = let cstr', t = Evarutil.new_evar cstr env t in (goal, cstr'), t -let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option) (f : 'a -> constr) = +let build_signature evars env m (cstrs : (types * types option) option list) + (finalcstr : (types * types option) option) = let new_evar evars env t = new_cstr_evar evars env (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t in let mk_relty evars env ty obj = match obj with - | None -> + | None | Some (_, None) -> let relty = mk_relation ty in new_evar evars env relty - | Some x -> evars, f x + | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = let t = Reductionops.whd_betadeltaiota env (fst evars) ty in @@ -209,12 +209,11 @@ let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a option) | _, obj :: _ -> anomaly "build_signature: not enough products" | _, [] -> (match finalcstr with - | None -> + | None | Some (_, None) -> let t = Reductionops.nf_betaiota (fst evars) ty in let evars, rel = mk_relty evars env t None in evars, t, rel, [t, Some rel] - | Some codom -> let (t, rel) = codom in - evars, t, rel, [t, Some rel]) + | Some (t, Some rel) -> evars, t, rel, [t, Some rel]) in aux env evars m cstrs let proper_proof env evars carrier relation x = @@ -248,7 +247,7 @@ type hypinfo = { l2r : bool; c1 : constr; c2 : constr; - c : constr option; + c : constr with_bindings option; abs : (constr * types) option; } @@ -256,25 +255,35 @@ let evd_convertible env evd x y = try ignore(Evarconv.the_conv_x env x y evd); true with _ -> false -let decompose_applied_relation env sigma c left2right = +let rec decompose_app_rel env evd t = + match kind_of_term t with + | App (f, args) -> + if Array.length args > 1 then + let fargs, args = array_chop (Array.length args - 2) args in + mkApp (f, fargs), args + else + let (f', args) = decompose_app_rel env evd args.(0) in + let ty = Typing.type_of env evd args.(0) in + let f'' = mkLambda (Name (id_of_string "x"), ty, + mkLambda (Name (id_of_string "y"), lift 1 ty, + mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |]))) + in (f'', args) + | _ -> error "The term provided is not an applied relation." + +let decompose_applied_relation env sigma (c,l) left2right = let ctype = Typing.type_of env sigma c in let find_rel ty = - let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ty) in - let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in - let rec split_last_two = function - | [c1;c2] -> [],(c1, c2) - | x::y::z -> - let l,res = split_last_two (y::z) in x::l, res - | _ -> error "The term provided is not an applied relation." in - let others,(c1,c2) = split_last_two args in + let eqclause = Clenv.make_clenv_binding_env_apply env sigma None (c,ty) l in + let (equiv, args) = decompose_app_rel env sigma (Clenv.clenv_type eqclause) in + let c1 = args.(0) and c2 = args.(1) in let ty1, ty2 = Typing.type_of env eqclause.evd c1, Typing.type_of env eqclause.evd c2 in if not (evd_convertible env eqclause.evd ty1 ty2) then None else Some { cl=eqclause; prf=(Clenv.clenv_value eqclause); - car=ty1; rel=mkApp (equiv, Array.of_list others); - l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None } + car=ty1; rel = equiv; + l2r=left2right; c1=c1; c2=c2; c=Some (c,l); abs=None } in match find_rel ctype with | Some c -> c @@ -398,27 +407,53 @@ let rec decomp_pointwise n c = if n = 0 then c else match kind_of_term c with - | App (pointwise, [| a; b; relb |]) -> decomp_pointwise (pred n) relb - | _ -> raise Not_found + | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) -> + decomp_pointwise (pred n) relb + | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) -> + decomp_pointwise (pred n) (Reductionops.beta_applist (arelb, [mkRel 1])) + | _ -> raise (Invalid_argument "decomp_pointwise") + +let rec apply_pointwise rel = function + | arg :: args -> + (match kind_of_term rel with + | App (f, [| a; b; relb |]) when eq_constr f (Lazy.force pointwise_relation) -> + apply_pointwise relb args + | App (f, [| a; b; arelb |]) when eq_constr f (Lazy.force forall_relation) -> + apply_pointwise (Reductionops.beta_applist (arelb, [arg])) args + | _ -> raise (Invalid_argument "apply_pointwise")) + | [] -> rel + +let pointwise_or_dep_relation n t car rel = + if noccurn 1 car then + mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |]) + else + mkApp (Lazy.force forall_relation, + [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |]) -let lift_cstr env sigma evars args cstr = +let lift_cstr env sigma evars (args : constr list) ty cstr = let cstr = - let start = + let start env car = match cstr with - | Some codom -> codom - | None -> - let car = Evarutil.e_new_evar evars env (new_Type ()) in - let rel = Evarutil.e_new_evar evars env (mk_relation car) in - (car, rel) + | None | Some (_, None) -> + Evarutil.e_new_evar evars env (mk_relation car) + | Some (ty, Some rel) -> rel in - Array.fold_right - (fun arg (car, rel) -> - let ty = Typing.type_of env sigma arg in - let car' = mkProd (Anonymous, ty, car) in - let rel' = mkApp (Lazy.force pointwise_relation, [| ty; car; rel |]) in - (car', rel')) - args start - in Some cstr + let rec aux env prod n = + if n = 0 then start env prod + else + match kind_of_term (Reduction.whd_betadeltaiota env prod) with + | Prod (na, ty, b) -> + if noccurn 1 b then + let b' = lift (-1) b in + let rb = aux env b' (pred n) in + mkApp (Lazy.force pointwise_relation, [| ty; b'; rb |]) + else + let rb = aux (Environ.push_rel (na, None, ty) env) b (pred n) in + mkApp (Lazy.force forall_relation, + [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]) + | _ -> assert false + in aux env ty (List.length args) + in Some (ty, cstr) let unlift_cstr env sigma = function | None -> None @@ -430,12 +465,17 @@ let default_flags = { under_lambdas = true; on_morphisms = true; } type evars = evar_map * evar_map (* goal evars, constraint evars *) +type rewrite_proof = + | RewPrf of constr * constr + | RewCast of cast_kind + +let get_rew_rel = function RewPrf (rel, prf) -> Some rel | _ -> None + type rewrite_result_info = { rew_car : constr; - rew_rel : constr; rew_from : constr; rew_to : constr; - rew_prf : constr; + rew_prf : rewrite_proof; rew_evars : evars; } @@ -444,7 +484,13 @@ type rewrite_result = rewrite_result_info option type strategy = Environ.env -> evar_map -> constr -> types -> constr option -> evars -> rewrite_result option -let resolve_subrelation env sigma car rel rel' res = +let get_rew_prf r = match r.rew_prf with + | RewPrf (rel, prf) -> prf + | RewCast c -> + mkCast (mkApp (Coqlib.build_coq_eq_refl (), [| r.rew_car; r.rew_from |]), + c, mkApp (Coqlib.build_coq_eq (), [| r.rew_car; r.rew_from; r.rew_to |])) + +let resolve_subrelation env sigma car rel prf rel' res = if eq_constr rel rel' then res else (* try let evd' = Evarconv.the_conv_x env rel rel' res.rew_evars in *) @@ -452,12 +498,11 @@ let resolve_subrelation env sigma car rel rel' res = (* with NotConvertible -> *) let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in let evars, subrel = new_cstr_evar res.rew_evars env app in + let appsub = mkApp (subrel, [| res.rew_from ; res.rew_to ; prf |]) in { res with - rew_prf = mkApp (subrel, [| res.rew_from ; res.rew_to ; res.rew_prf |]); - rew_rel = rel'; + rew_prf = RewPrf (rel', appsub); rew_evars = evars } - let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars = let evars, morph_instance, proj, sigargs, m', args, args' = let first = try (array_find args' (fun i b -> b <> None)) @@ -466,9 +511,11 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars let morphargs', morphobjs' = array_chop first args' in let appm = mkApp(m, morphargs) in let appmtype = Typing.type_of env sigma appm in - let cstrs = List.map (Option.map (fun r -> r.rew_car, r.rew_rel)) (Array.to_list morphobjs') in + let cstrs = List.map (Option.map (fun r -> r.rew_car, get_rew_rel r.rew_prf)) (Array.to_list morphobjs') in (* Desired signature *) - let evars, appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a,r) -> r) in + let evars, appmtype', signature, sigargs = + build_signature evars env appmtype cstrs cstr + in (* Actual signature found *) let cl_args = [| appmtype' ; signature ; appm |] in let app = mkApp (Lazy.force proper_type, cl_args) in @@ -492,7 +539,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars let evars, proof = proper_proof env evars carrier relation x in [ proof ; x ; x ] @ acc, subst, evars, sigargs, x :: typeargs' | Some r -> - [ r.rew_prf; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') + [ get_rew_prf r; r.rew_to; x ] @ acc, subst, evars, sigargs, r.rew_to :: typeargs') | None -> if y <> None then error "Cannot rewrite the argument of a dependent function"; x :: acc, x :: subst, evars, sigargs, x :: typeargs') @@ -504,10 +551,10 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars [ a, Some r ] -> evars, proof, a, r, oldt, fnewt newt | _ -> assert(false) -let apply_constraint env sigma car rel cstr res = +let apply_constraint env sigma car rel prf cstr res = match cstr with | None -> res - | Some r -> resolve_subrelation env sigma car rel r res + | Some r -> resolve_subrelation env sigma car rel prf r res let eq_env x y = x == y @@ -523,12 +570,14 @@ let apply_rule hypinfo loccs : strategy = match unif with | Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ -> begin - let goalevars = Evd.evar_merge (fst evars) - (Evd.undefined_evars (Evarutil.nf_evar_map env'.evd)) - in - let res = { rew_car = ty; rew_rel = rel; rew_from = c1; - rew_to = c2; rew_prf = prf; rew_evars = goalevars, snd evars } - in Some (Some (apply_constraint env sigma car rel cstr res)) + if eq_constr t c2 then Some None + else + let goalevars = Evd.evar_merge (fst evars) + (Evd.undefined_evars (Evarutil.nf_evar_map env'.evd)) + in + let res = { rew_car = ty; rew_from = c1; + rew_to = c2; rew_prf = RewPrf (rel, prf); rew_evars = goalevars, snd evars } + in Some (Some (apply_constraint env sigma car rel prf cstr res)) end | _ -> None @@ -539,24 +588,79 @@ let apply_lemma (evm,c) left2right loccs : strategy = apply_rule hypinfo loccs env sigma let make_leibniz_proof c ty r = - let prf = mkApp (Lazy.force coq_f_equal, - [| r.rew_car; ty; - mkLambda (Anonymous, r.rew_car, c (mkRel 1)); - r.rew_from; r.rew_to; r.rew_prf |]) + let prf = + match r.rew_prf with + | RewPrf (rel, prf) -> + let rel = mkApp (Lazy.force coq_eq, [| ty |]) in + let prf = + mkApp (Lazy.force coq_f_equal, + [| r.rew_car; ty; + mkLambda (Anonymous, r.rew_car, c (mkRel 1)); + r.rew_from; r.rew_to; prf |]) + in RewPrf (rel, prf) + | RewCast k -> r.rew_prf in - { r with rew_car = ty; rew_rel = mkApp (Lazy.force coq_eq, [| ty |]); + { r with rew_car = ty; rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf } -let pointwise_or_dep_relation n t car rel = - if noccurn 1 car then - mkApp (Lazy.force pointwise_relation, [| t; lift (-1) car; lift (-1) rel |]) - else - mkApp (Lazy.force forall_relation, - [| t; mkLambda (n, t, car); mkLambda (n, t, rel) |]) - +open Elimschemes + +let reset_env env = + let env' = Global.env_of_context (Environ.named_context_val env) in + Environ.push_rel_context (Environ.rel_context env) env' + +let fold_match ?(force=false) env sigma c = + let (ci, p, c, brs) = destCase c in + let cty = Retyping.get_type_of env sigma c in + let dep, pred, exists, sk = + let env', ctx, body = + let ctx, pred = decompose_lam_assum p in + let env' = Environ.push_rel_context ctx env in + env', ctx, pred + in + let sortp = Retyping.get_sort_family_of env' sigma body in + let sortc = Retyping.get_sort_family_of env sigma cty in + let dep = not (noccurn 1 body) in + let pred = if dep then p else + it_mkProd_or_LetIn (subst1 mkProp body) (List.tl ctx) + in + let sk = + if sortp = InProp then + if sortc = InProp then + if dep then case_dep_scheme_kind_from_prop + else case_scheme_kind_from_prop + else ( + if dep + then case_dep_scheme_kind_from_type_in_prop + else case_scheme_kind_from_type) + else ((* sortc <> InProp by typing *) + if dep + then case_dep_scheme_kind_from_type + else case_scheme_kind_from_type) + in + let exists = Ind_tables.check_scheme sk ci.ci_ind in + if exists || force then + dep, pred, exists, Ind_tables.find_scheme sk ci.ci_ind + else raise Not_found + in + let app = + let ind, args = Inductive.find_rectype env cty in + let pars, args = list_chop ci.ci_npar args in + let meths = List.map (fun br -> br) (Array.to_list brs) in + applist (mkConst sk, pars @ [pred] @ meths @ args @ [c]) + in + sk, (if exists then env else reset_env env), app + +let unfold_match env sigma sk app = + match kind_of_term app with + | App (f', args) when f' = mkConst sk -> + let v = Environ.constant_value (Global.env ()) sk in + Reductionops.whd_beta sigma (mkApp (v, args)) + | _ -> app + let subterm all flags (s : strategy) : strategy = let rec aux env sigma t ty cstr evars = - let cstr' = Option.map (fun c -> (ty, c)) cstr in + let cstr' = Option.map (fun c -> (ty, Some c)) cstr in match kind_of_term t with | App (m, args) -> let rewrite_args success = @@ -578,29 +682,39 @@ let subterm all flags (s : strategy) : strategy = | Some true -> let args' = Array.of_list (List.rev args') in let evars', prf, car, rel, c1, c2 = resolve_morphism env sigma t m args args' cstr' evars' in - let res = { rew_car = ty; rew_rel = rel; rew_from = c1; - rew_to = c2; rew_prf = prf; rew_evars = evars' } in + let res = { rew_car = ty; rew_from = c1; + rew_to = c2; rew_prf = RewPrf (rel, prf); + rew_evars = evars' } + in Some (Some res) in if flags.on_morphisms then let evarsref = ref (snd evars) in - let cstr' = lift_cstr env sigma evarsref args cstr' in - let m' = s env sigma m (Typing.type_of env sigma m) - (Option.map snd cstr') (fst evars, !evarsref) - in + let mty = Typing.type_of env sigma m in + let argsl = Array.to_list args in + let cstr' = lift_cstr env sigma evarsref argsl mty None in + let m' = s env sigma m mty (Option.map snd cstr') (fst evars, !evarsref) in match m' with | None -> rewrite_args None (* Standard path, try rewrite on arguments *) | Some None -> rewrite_args (Some false) | Some (Some r) -> (* We rewrote the function and get a proof of pointwise rel for the arguments. We just apply it. *) - let nargs = Array.length args in + let prf = match r.rew_prf with + | RewPrf (rel, prf) -> + RewPrf (apply_pointwise rel argsl, mkApp (prf, args)) + | x -> x + in let res = - { rew_car = decomp_prod env (fst r.rew_evars) nargs r.rew_car; - rew_rel = decomp_pointwise nargs r.rew_rel; + { rew_car = prod_appvect r.rew_car args; rew_from = mkApp(r.rew_from, args); rew_to = mkApp(r.rew_to, args); - rew_prf = mkApp (r.rew_prf, args); rew_evars = r.rew_evars } - in Some (Some res) + rew_prf = prf; + rew_evars = r.rew_evars } + in + match prf with + | RewPrf (rel, prf) -> + Some (Some (apply_constraint env sigma res.rew_car rel prf cstr res)) + | _ -> Some (Some res) else rewrite_args None | Prod (n, x, b) when noccurn 1 b -> @@ -637,18 +751,24 @@ let subterm all flags (s : strategy) : strategy = let b' = s env' sigma b (Typing.type_of env' sigma b) (unlift_cstr env sigma cstr) evars in (match b' with | Some (Some r) -> - Some (Some { r with - rew_prf = mkLambda (n, t, r.rew_prf); - rew_car = mkProd (n, t, r.rew_car); - rew_rel = pointwise_or_dep_relation n t r.rew_car r.rew_rel; - rew_from = mkLambda(n, t, r.rew_from); - rew_to = mkLambda (n, t, r.rew_to) }) + let prf = match r.rew_prf with + | RewPrf (rel, prf) -> + let rel = pointwise_or_dep_relation n t r.rew_car rel in + let prf = mkLambda (n, t, prf) in + RewPrf (rel, prf) + | x -> x + in + Some (Some { r with + rew_prf = prf; + rew_car = mkProd (n, t, r.rew_car); + rew_from = mkLambda(n, t, r.rew_from); + rew_to = mkLambda (n, t, r.rew_to) }) | _ -> b') | Case (ci, p, c, brs) -> let cty = Typing.type_of env sigma c in - let cstr = Some (mkApp (Lazy.force coq_eq, [| cty |])) in - let c' = s env sigma c cty cstr evars in + let cstr' = Some (mkApp (Lazy.force coq_eq, [| cty |])) in + let c' = s env sigma c cty cstr' evars in (match c' with | Some (Some r) -> Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r)) @@ -668,7 +788,14 @@ let subterm all flags (s : strategy) : strategy = let ctxc x = mkCase (ci, p, c, Array.of_list (List.rev (brs' x))) in Some (Some (make_leibniz_proof ctxc ty r)) | None -> x - else x) + else + match try Some (fold_match env sigma t) with Not_found -> None with + | None -> x + | Some (cst, _, t') -> + match aux env sigma t' ty cstr evars with + | Some (Some prf) -> Some (Some { prf with + rew_from = t; rew_to = unfold_match env sigma cst prf.rew_to }) + | x' -> x) | _ -> if all then Some None else None in aux @@ -676,19 +803,27 @@ let subterm all flags (s : strategy) : strategy = let all_subterms = subterm true default_flags let one_subterm = subterm false default_flags -(** Requires transitivity of the rewrite step, not tail-recursive. *) +(** Requires transitivity of the rewrite step, if not a reduction. + Not tail-recursive. *) let transitivity env sigma (res : rewrite_result_info) (next : strategy) : rewrite_result option = - match next env sigma res.rew_to res.rew_car (Some res.rew_rel) res.rew_evars with + match next env sigma res.rew_to res.rew_car (get_rew_rel res.rew_prf) res.rew_evars with | None -> None | Some None -> Some (Some res) | Some (Some res') -> - let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car ; res.rew_rel |]) in - let evars, prf = new_cstr_evar res'.rew_evars env prfty in - let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to; - res.rew_prf; res'.rew_prf |]) - in Some (Some { res' with rew_from = res.rew_from; rew_evars = evars; rew_prf = prf }) - + match res.rew_prf with + | RewCast c -> Some (Some { res' with rew_from = res.rew_from }) + | RewPrf (rew_rel, rew_prf) -> + match res'.rew_prf with + | RewCast _ -> Some (Some ({ res with rew_to = res'.rew_to })) + | RewPrf (res'_rel, res'_prf) -> + let prfty = mkApp (Lazy.force transitive_type, [| res.rew_car; rew_rel |]) in + let evars, prf = new_cstr_evar res'.rew_evars env prfty in + let prf = mkApp (prf, [|res.rew_from; res'.rew_from; res'.rew_to; + rew_prf; res'_prf |]) + in Some (Some { res' with rew_from = res.rew_from; + rew_evars = evars; rew_prf = RewPrf (res'_rel, prf) }) + (** Rewriting strategies. Inspired by ELAN's rewriting strategies: @@ -714,8 +849,8 @@ module Strategies = let mty = mkApp (Lazy.force proper_proxy_type, [| ty ; rel; t |]) in new_cstr_evar evars env mty in - Some (Some { rew_car = ty; rew_rel = rel; rew_from = t; rew_to = t; - rew_prf = proof; rew_evars = evars }) + Some (Some { rew_car = ty; rew_from = t; rew_to = t; + rew_prf = RewPrf (rel, proof); rew_evars = evars }) let progress (s : strategy) : strategy = fun env sigma t ty cstr evars -> @@ -769,13 +904,24 @@ module Strategies = let old_hints (db : string) : strategy = let rules = Autorewrite.find_rewrites db in - lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules) + lemmas (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules) let hints (db : string) : strategy = fun env sigma t ty cstr evars -> - let rules = Autorewrite.find_matches db t in - lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules) - env sigma t ty cstr evars + let rules = Autorewrite.find_matches db t in + lemmas (List.map (fun hint -> (inj_open (hint.Autorewrite.rew_lemma, NoBindings), hint.Autorewrite.rew_l2r)) rules) + env sigma t ty cstr evars + + let reduce (r : Redexpr.red_expr) : strategy = + let rfn, ckind = Redexpr.reduction_of_red_expr r in + fun env sigma t ty cstr evars -> + let t' = rfn env sigma t in + if eq_constr t' t then + Some None + else + Some (Some { rew_car = ty; rew_from = t; rew_to = t'; + rew_prf = RewCast ckind; rew_evars = evars }) + end @@ -787,7 +933,7 @@ let rewrite_strat flags occs hyp = Strategies.choice app (subterm true flags (fun env -> aux () env)) in aux () -let rewrite_with (evm,c) left2right loccs : strategy = +let rewrite_with {it = c; sigma = evm} left2right loccs : strategy = fun env sigma -> let evars = Evd.merge sigma evm in let hypinfo = ref (decompose_applied_relation env evars c left2right) in @@ -803,7 +949,7 @@ let apply_strategy (s : strategy) env sigma concl cstr evars = | Some None -> Some None | Some (Some res) -> evars := res.rew_evars; - Some (Some (res.rew_prf, (res.rew_car, res.rew_rel, res.rew_from, res.rew_to))) + Some (Some (res.rew_prf, (res.rew_car, res.rew_from, res.rew_to))) let split_evars_once sigma evd = Evd.fold (fun ev evi deps -> @@ -834,6 +980,12 @@ let solve_constraints env evars = let nf_zeta = Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA]) +let map_rewprf f = function + | RewPrf (rel, prf) -> RewPrf (f rel, f prf) + | RewCast c -> RewCast c + +exception RewriteFailure + let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let concl, is_hyp = match clause with @@ -852,12 +1004,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let env = pf_env gl in let eq = apply_strategy strat env sigma concl (Some cstr) evars in match eq with - | Some (Some (p, (_, _, oldt, newt))) -> + | Some (Some (p, (car, oldt, newt))) -> (try let cstrevars = !evars in let evars = solve_constraints env cstrevars in - let p = Evarutil.nf_evar evars p in - let p = nf_zeta env evars p in + let p = map_rewprf + (fun p -> nf_zeta env evars (Evarutil.nf_evar evars p)) + p + in let newt = Evarutil.nf_evar evars newt in let abs = Option.map (fun (x, y) -> Evarutil.nf_evar evars x, Evarutil.nf_evar evars y) abs in @@ -865,27 +1019,36 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = let rewtac = match is_hyp with | Some id -> - let term = - match abs with - | None -> p - | Some (t, ty) -> - mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) - in - cut_replacing id newt - (Tacmach.refine_no_check (mkApp (term, [| mkVar id |]))) + (match p with + | RewPrf (rel, p) -> + let term = + match abs with + | None -> p + | Some (t, ty) -> + mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) + in + cut_replacing id newt + (Tacmach.refine_no_check (mkApp (term, [| mkVar id |]))) + | RewCast c -> + change_in_hyp None newt (id, InHypTypeOnly)) + | None -> - (match abs with - | None -> - let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in - tclTHENLAST - (Tacmach.internal_cut_no_check false name newt) - (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p)) - | Some (t, ty) -> - Tacmach.refine_no_check - (mkApp (mkLambda (Name (id_of_string "newt"), newt, - mkLambda (Name (id_of_string "lemma"), ty, - mkApp (p, [| mkRel 2 |]))), - [| mkMeta goal_meta; t |]))) + (match p with + | RewPrf (rel, p) -> + (match abs with + | None -> + let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in + tclTHENLAST + (Tacmach.internal_cut_no_check false name newt) + (tclTHEN (Tactics.revert [name]) (Tacmach.refine_no_check p)) + | Some (t, ty) -> + Tacmach.refine_no_check + (mkApp (mkLambda (Name (id_of_string "newt"), newt, + mkLambda (Name (id_of_string "lemma"), ty, + mkApp (p, [| mkRel 2 |]))), + [| mkMeta goal_meta; t |]))) + | RewCast c -> + change_in_concl None newt) in let evartac = if not (undef = Evd.empty) then @@ -900,14 +1063,14 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = ++ fnl () ++ Himsg.explain_typeclass_error env e)) gl) | Some None -> tclFAIL 0 (str"setoid rewrite failed: no progress made") gl - | None -> raise Not_found + | None -> raise RewriteFailure let cl_rewrite_clause_strat strat clause gl = init_setoid (); let meta = Evarutil.new_meta() in let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in try cl_rewrite_clause_aux strat meta clause gl - with Not_found -> + with RewriteFailure -> tclFAIL 0 (str"setoid rewrite failed: strategy failed") gl let cl_rewrite_clause l left2right occs clause gl = @@ -939,11 +1102,13 @@ let glob_strategy ist l = l let subst_strategy evm l = l let apply_constr_expr c l2r occs = fun env sigma -> - let c = Constrintern.interp_open_constr sigma env c in - apply_lemma c l2r occs env sigma + let evd, c = Constrintern.interp_open_constr sigma env c in + apply_lemma (evd, (c, NoBindings)) l2r occs env sigma -let interp_constr_list env sigma cs = - List.map (fun c -> Constrintern.interp_open_constr sigma env c, true) cs +let interp_constr_list env sigma = + List.map (fun c -> + let evd, c = Constrintern.interp_open_constr sigma env c in + (evd, (c, NoBindings)), true) open Pcoq @@ -980,15 +1145,18 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ Strategies.choice h h' ] | [ "old_hints" preident(h) ] -> [ Strategies.old_hints h ] | [ "hints" preident(h) ] -> [ Strategies.hints h ] - | [ "terms" constr_list(h) ] -> [ fun env sigma -> Strategies.lemmas (interp_constr_list env sigma h) env sigma ] + | [ "terms" constr_list(h) ] -> [ fun env sigma -> + Strategies.lemmas (interp_constr_list env sigma h) env sigma ] + | [ "eval" red_expr(r) ] -> [ fun env sigma -> + Strategies.reduce (Tacinterp.interp_redexp env sigma r) env sigma ] END TACTIC EXTEND class_rewrite -| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] -| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] -| [ "clrewrite" orient(o) open_constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some id) ] -| [ "clrewrite" orient(o) open_constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ] -| [ "clrewrite" orient(o) open_constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ] +| [ "clrewrite" orient(o) constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] +| [ "clrewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] +| [ "clrewrite" orient(o) constr_with_bindings(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some id) ] +| [ "clrewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ] +| [ "clrewrite" orient(o) constr_with_bindings(c) ] -> [ cl_rewrite_clause c o all_occurrences None ] END TACTIC EXTEND class_rewrite_strat @@ -998,7 +1166,7 @@ END let clsubstitute o c = - let is_tac id = match kind_of_term (snd c) with Var id' when id' = id -> true | _ -> false in + let is_tac id = match kind_of_term (fst c.it) with Var id' when id' = id -> true | _ -> false in Tacticals.onAllHypsAndConcl (fun cl -> match cl with @@ -1006,22 +1174,22 @@ let clsubstitute o c = | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl)) TACTIC EXTEND substitute -| [ "substitute" orient(o) open_constr(c) ] -> [ clsubstitute o c ] +| [ "substitute" orient(o) constr_with_bindings(c) ] -> [ clsubstitute o c ] END (* Compatibility with old Setoids *) TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(o) open_constr(c) ] + [ "setoid_rewrite" orient(o) constr_with_bindings(c) ] -> [ cl_rewrite_clause c o all_occurrences None ] - | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) ] -> + | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some id)] - | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) ] -> + | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None] - | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id)] -> + | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id)] - | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ)] -> + | [ "setoid_rewrite" orient(o) constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some id)] END @@ -1104,12 +1272,12 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans = (Ident (dummy_loc,id_of_string "Equivalence_Symmetric"), lemma2); (Ident (dummy_loc,id_of_string "Equivalence_Transitive"), lemma3)]) -type 'a binders_let_argtype = (local_binder list, 'a) Genarg.abstract_argument_type +type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type -let (wit_binders_let : Genarg.tlevel binders_let_argtype), - (globwit_binders_let : Genarg.glevel binders_let_argtype), - (rawwit_binders_let : Genarg.rlevel binders_let_argtype) = - Genarg.create_arg "binders_let" +let (wit_binders : Genarg.tlevel binders_argtype), + (globwit_binders : Genarg.glevel binders_argtype), + (rawwit_binders : Genarg.rlevel binders_argtype) = + Genarg.create_arg "binders" open Pcoq.Constr @@ -1147,35 +1315,35 @@ VERNAC COMMAND EXTEND AddRelation3 END VERNAC COMMAND EXTEND AddParametricRelation - | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ] - | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n (Some lemma1) None None ] - | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n None None None ] END VERNAC COMMAND EXTEND AddParametricRelation2 - [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n None (Some lemma2) None ] - | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ] END VERNAC COMMAND EXTEND AddParametricRelation3 - [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ] - | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] - | [ "Add" "Parametric" "Relation" binders_let(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] END @@ -1242,7 +1410,7 @@ let build_morphism_signature m = | _ -> [] in aux t in - let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None snd in + let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None in let _ = isevars := evars in let _ = List.iter (fun (ty, rel) -> @@ -1264,7 +1432,7 @@ let default_morphism sign m = let env = Global.env () in let t = Typing.type_of env Evd.empty m in let evars, _, sign, cstrs = - build_signature (Evd.empty,Evd.empty) env t (fst sign) (snd sign) (fun (ty, rel) -> rel) + build_signature (Evd.empty,Evd.empty) env t (fst sign) (snd sign) in let morph = mkApp (Lazy.force proper_type, [| t; sign; m |]) @@ -1324,13 +1492,13 @@ let add_morphism glob binders m s n = VERNAC COMMAND EXTEND AddSetoid1 [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> [ add_setoid [] a aeq t n ] - | [ "Add" "Parametric" "Setoid" binders_let(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> [ add_setoid binders a aeq t n ] | [ "Add" "Morphism" constr(m) ":" ident(n) ] -> [ add_morphism_infer (not (Vernacexpr.use_section_locality ())) m n ] | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> [ add_morphism (not (Vernacexpr.use_section_locality ())) [] m s n ] - | [ "Add" "Parametric" "Morphism" binders_let(binders) ":" constr(m) + | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] -> [ add_morphism (not (Vernacexpr.use_section_locality ())) binders m s n ] END @@ -1390,16 +1558,16 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)} -let get_hyp gl evars c clause l2r = - let hi = decompose_applied_relation (pf_env gl) evars c l2r in +let get_hyp gl evars (c,l) clause l2r = + let hi = decompose_applied_relation (pf_env gl) evars (c,l) l2r in let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl -let general_rewrite_flags = { under_lambdas = false; on_morphisms = false } +let general_rewrite_flags = { under_lambdas = false; on_morphisms = true } -let apply_lemma gl c cl l2r occs = +let apply_lemma gl (c,l) cl l2r occs = let sigma = project gl in - let hypinfo = ref (get_hyp gl sigma c cl l2r) in + let hypinfo = ref (get_hyp gl sigma (c,l) cl l2r) in let app = apply_rule hypinfo occs in let rec aux () = Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env)) @@ -1407,12 +1575,12 @@ let apply_lemma gl c cl l2r occs = let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let meta = Evarutil.new_meta() in - let hypinfo, strat = apply_lemma gl c cl l2r occs in + let hypinfo, strat = apply_lemma gl (c,l) cl l2r occs in try tclTHEN (Refiner.tclEVARS hypinfo.cl.evd) (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl) gl - with Not_found -> + with RewriteFailure -> let {l2r=l2r; c1=x; c2=y} = hypinfo in raise (Pretype_errors.PretypeError (pf_env gl, @@ -1441,18 +1609,10 @@ let not_declared env ty rel = tclFAIL 0 (str" The relation " ++ Printer.pr_constr_env env rel ++ str" is not a declared " ++ str ty ++ str" relation. Maybe you need to require the Setoid library") -let relation_of_constr env c = - match kind_of_term c with - | App (f, args) when Array.length args >= 2 -> - let relargs, args = array_chop (Array.length args - 2) args in - mkApp (f, relargs), args - | _ -> errorlabstrm "relation_of_constr" - (str "The term " ++ Printer.pr_constr_env env c ++ str" is not an applied relation.") - let setoid_proof gl ty fn fallback = let env = pf_env gl in try - let rel, args = relation_of_constr env (pf_concl gl) in + let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in let evm, car = project gl, pf_type_of gl args.(0) in fn env evm car rel gl with e -> @@ -1460,7 +1620,7 @@ let setoid_proof gl ty fn fallback = with Hipattern.NoEquationFound -> match e with | Not_found -> - let rel, args = relation_of_constr env (pf_concl gl) in + let rel, args = decompose_app_rel env (project gl) (pf_concl gl) in not_declared env ty rel gl | _ -> raise e @@ -1480,8 +1640,7 @@ let setoid_transitivity c gl = let proof = get_transitive_proof env evm car rel in match c with | None -> eapply proof - | Some c -> - apply_with_bindings (proof,Rawterm.ExplicitBindings [ dummy_loc, Rawterm.NamedHyp (id_of_string "y"), c ])) + | Some c -> apply_with_bindings (proof,Rawterm.ImplicitBindings [ c ])) (transitivity_red true c) let setoid_symmetry_in id gl = @@ -1539,3 +1698,25 @@ let implify id gl = TACTIC EXTEND implify [ "implify" hyp(n) ] -> [ implify n ] END + +let rec fold_matches env sigma c = + map_constr_with_full_binders Environ.push_rel + (fun env c -> + match kind_of_term c with + | Case _ -> + let cst, env, c' = fold_match ~force:true env sigma c in + fold_matches env sigma c' + | _ -> fold_matches env sigma c) + env c + +TACTIC EXTEND fold_match +[ "fold_match" constr(c) ] -> [ fun gl -> + let _, _, c' = fold_match ~force:true (pf_env gl) (project gl) c in + change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ] +END + +TACTIC EXTEND fold_matches +| [ "fold_matches" constr(c) ] -> [ fun gl -> + let c' = fold_matches (pf_env gl) (project gl) c in + change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ] +END diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 291df0fe..95e44c40 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: tacinterp.ml 13360 2010-07-30 08:47:08Z herbelin $ *) open Constrintern open Closure @@ -2415,7 +2415,9 @@ and interp_atomic ist gl tac = | TacChange (Some op,c,cl) -> let sign,op = interp_typed_pattern ist env sigma op in h_change (Some op) - (pf_interp_constr ist (extend_gl_hyps gl sign) c) + (try pf_interp_constr ist (extend_gl_hyps gl sign) c + with Not_found | Anomaly _ (* Hack *) -> + errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")) (interp_clause ist gl cl) (* Equivalence relations *) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 854664e9..82f4d99a 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: tacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml new file mode 100644 index 00000000..df5a3283 --- /dev/null +++ b/tactics/tactic_option.ml @@ -0,0 +1,57 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* load); + open_function = (fun _ -> load); + classify_function = (fun (local, tac) -> + if local then Dispose else Substitute (local, tac)); + subst_function = subst} + in + let put local tac = + set_default_tactic local tac; + Lib.add_anonymous_leaf (input (local, tac)) + in + let get () = !locality, !default_tactic in + let print () = + Pptactic.pr_glob_tactic (Global.env ()) !default_tactic_expr ++ + (if !locality then str" (locally defined)" else str" (globally defined)") + in + let freeze () = !locality, !default_tactic_expr in + let unfreeze (local, t) = set_default_tactic local t in + let init () = () in + Summary.declare_summary name + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init }; + put, get, print + diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli new file mode 100644 index 00000000..890ba98e --- /dev/null +++ b/tactics/tactic_option.mli @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* string -> + (* put *) (locality_flag -> glob_tactic_expr -> unit) * + (* get *) (unit -> locality_flag * tactic) * + (* print *) (unit -> Pp.std_ppcmds) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 59a8b794..171a35c0 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: tacticals.ml 13323 2010-07-24 15:57:30Z herbelin $ *) open Pp open Util diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 90508436..af74e382 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: tacticals.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Pp diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e09707ab..9e4be0af 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: tactics.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -2320,6 +2320,9 @@ let linear vars args = true with Seen -> false +let is_defined_variable env id = + pi2 (lookup_named id env) <> None + let abstract_args gl generalize_vars dep id defined f args = let sigma = project gl in let env = pf_env gl in @@ -2347,7 +2350,7 @@ let abstract_args gl generalize_vars dep id defined f args = let liftargty = lift lenctx argty in let leq = constr_cmp Reduction.CUMUL liftargty ty in match kind_of_term arg with - | Var id when leq && not (Idset.mem id nongenvars) -> + | Var id when not (is_defined_variable env id) && leq && not (Idset.mem id nongenvars) -> (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, Idset.add id nongenvars, Idset.remove id vars, env) | _ -> @@ -2374,7 +2377,7 @@ let abstract_args gl generalize_vars dep id defined f args = let parvars = ids_of_constr ~all:true Idset.empty f' in if not (linear parvars args') then true, f, args else - match array_find_i (fun i x -> not (isVar x)) args' with + match array_find_i (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with | None -> false, f', args' | Some nonvar -> let before, after = array_chop nonvar args' in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 92477e23..bfc32654 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: tactics.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) (*i*) open Util diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 0a634138..b885b152 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -21,3 +21,4 @@ Evar_tactics Autorewrite Decl_interp Decl_proof_instr +Tactic_option diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 6091e3d1..a7e7613d 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id$ i*) +(*i $Id: tauto.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*) open Term open Hipattern diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 828fc065..f9f086d9 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: termdn.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Util open Names @@ -33,7 +33,7 @@ struct | GRLabel of global_reference | ProdLabel | LambdaLabel - | SortLabel of sorts option + | SortLabel module Y = struct type t = term_label @@ -97,12 +97,7 @@ let constr_pat_discr_st (idpred,cpred) t = Some (GRLabel ref, args) | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l) - | PSort s, [] -> - let s' = match s with - | RProp c -> Some (Prop c) - | RType _ -> None - (* Don't try to be clever about type levels here *) - in Some (SortLabel s', []) + | PSort s, [] -> Some (SortLabel, []) | _ -> None open Dn @@ -125,8 +120,7 @@ let constr_val_discr_st (idpred,cpred) t = | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l) | Prod (n, d, c) -> Label(ProdLabel, [d; c]) | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l) - | Sort s when is_small s -> Label(SortLabel (Some s), []) - | Sort _ -> Label (SortLabel None, []) + | Sort _ -> Label (SortLabel, []) | Evar _ -> Everything | _ -> Nothing diff --git a/tactics/termdn.mli b/tactics/termdn.mli index b7c9f273..e778de8d 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: termdn.mli 13332 2010-07-26 22:12:43Z msozeau $ i*) (*i*) open Term @@ -58,7 +58,7 @@ sig | GRLabel of global_reference | ProdLabel | LambdaLabel - | SortLabel of sorts option + | SortLabel val constr_pat_discr_st : transparent_state -> constr_pattern -> (term_label * constr_pattern list) option -- cgit v1.2.3