From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- tactics/auto.ml | 204 +++++++----- tactics/auto.mli | 18 +- tactics/autorewrite.ml | 13 +- tactics/btermdn.ml | 62 +++- tactics/btermdn.mli | 11 +- tactics/class_tactics.ml4 | 389 +++++++++++++---------- tactics/contradiction.ml | 4 +- tactics/decl_interp.ml | 12 +- tactics/decl_proof_instr.ml | 67 ++-- tactics/dhyp.ml | 12 +- tactics/dn.ml | 54 +++- tactics/dn.mli | 10 +- tactics/eauto.ml4 | 37 ++- tactics/elim.ml | 10 +- tactics/elim.mli | 4 +- tactics/eqdecide.ml4 | 6 +- tactics/equality.ml | 143 +++++---- tactics/equality.mli | 8 +- tactics/evar_tactics.ml | 8 +- tactics/extratactics.ml4 | 24 +- tactics/hiddentac.ml | 37 ++- tactics/hiddentac.mli | 33 +- tactics/hipattern.ml4 | 4 +- tactics/inv.ml | 50 +-- tactics/inv.mli | 15 +- tactics/leminv.ml | 6 +- tactics/nbtermdn.ml | 14 +- tactics/refine.ml | 8 +- tactics/tacinterp.ml | 474 +++++++++++++++------------- tactics/tacinterp.mli | 12 +- tactics/tacticals.ml | 37 ++- tactics/tacticals.mli | 24 +- tactics/tactics.ml | 747 ++++++++++++++++++++++++-------------------- tactics/tactics.mli | 46 ++- tactics/tauto.ml4 | 44 ++- tactics/termdn.ml | 71 +++-- tactics/termdn.mli | 23 +- 37 files changed, 1553 insertions(+), 1188 deletions(-) (limited to 'tactics') diff --git a/tactics/auto.ml b/tactics/auto.ml index 2a5bb95c..066ed786 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: auto.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: auto.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -91,18 +91,20 @@ type search_entry = stored_data list * stored_data list * stored_data Btermdn.t let empty_se = ([],[],Btermdn.create ()) -let add_tac t (l,l',dn) = - match t.pat with - None -> if not (List.mem t l) then (insert t l, l', dn) else (l, l', dn) - | Some pat -> if not (List.mem t l') then (l, insert t l', Btermdn.add dn (pat,t)) else (l, l', dn) +let add_tac pat t st (l,l',dn) = + match pat with + | None -> if not (List.mem t l) then (insert t l, l', dn) else (l, l', dn) + | Some pat -> if not (List.mem t l') then (l, insert t l', Btermdn.add st dn (pat,t)) else (l, l', dn) - -let lookup_tacs (hdc,c) (l,l',dn) = - let l' = List.map snd (Btermdn.lookup dn c) in +let rebuild_dn st (l,l',dn) = + (l, l', List.fold_left (fun dn t -> Btermdn.add (Some st) dn (Option.get t.pat, t)) + (Btermdn.create ()) l') + +let lookup_tacs (hdc,c) st (l,l',dn) = + let l' = List.map snd (Btermdn.lookup st dn c) in let sl' = Sort.list pri_order l' in Sort.merge pri_order l sl' - module Constr_map = Map.Make(struct type t = global_reference let compare = Pervasives.compare @@ -110,12 +112,18 @@ module Constr_map = Map.Make(struct module Hint_db = struct - type t = search_entry Constr_map.t - - let empty = Constr_map.empty + type t = { + hintdb_state : Names.transparent_state; + use_dn : bool; + hintdb_map : search_entry Constr_map.t + } + let empty use_dn = { hintdb_state = empty_transparent_state; + use_dn = use_dn; + hintdb_map = Constr_map.empty } + let find key db = - try Constr_map.find key db + try Constr_map.find key db.hintdb_map with Not_found -> empty_se let map_all k db = @@ -123,21 +131,49 @@ module Hint_db = struct Sort.merge pri_order l l' let map_auto (k,c) db = - lookup_tacs (k,c) (find k db) + let st = if db.use_dn then Some db.hintdb_state else None in + lookup_tacs (k,c) st (find k db) - let add_one (k,v) db = - let oval = find k db in - Constr_map.add k (add_tac v oval) db + let is_exact = function + | Give_exact _ -> true + | _ -> false + let add_one (k,v) db = + let st',rebuild = + match v.code with + | Unfold_nth egr -> + let (ids,csts) = db.hintdb_state in + (match egr with + | EvalVarRef id -> (Idpred.add id ids, csts) + | EvalConstRef cst -> (ids, Cpred.add cst csts)), true + | _ -> db.hintdb_state, false + in + let dnst, db = + if db.use_dn then + Some st', { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map } + else None, db + in + let oval = find k db in + let pat = if not db.use_dn && is_exact v.code then None else v.pat in + { db with hintdb_map = Constr_map.add k (add_tac pat v dnst oval) db.hintdb_map; + hintdb_state = st' } + let add_list l db = List.fold_right add_one l db + + let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db.hintdb_map + + let transparent_state db = db.hintdb_state - let iter f db = Constr_map.iter (fun k (l,l',_) -> f k (l@l')) db + let set_transparent_state db st = { db with hintdb_state = st } + let set_rigid db cst = + let (ids,csts) = db.hintdb_state in + { db with hintdb_state = (ids, Cpred.remove cst csts) } end module Hintdbmap = Gmap -type hint_db = Names.transparent_state * Hint_db.t +type hint_db = Hint_db.t type frozen_hint_db_table = (string,hint_db) Hintdbmap.t @@ -158,7 +194,9 @@ let current_db_names () = (* Definition of the summary *) (**************************************************************************) -let init () = searchtable := Hintdbmap.empty +let auto_init : (unit -> unit) ref = ref (fun () -> ()) + +let init () = searchtable := Hintdbmap.empty; !auto_init () let freeze () = !searchtable let unfreeze fs = searchtable := fs @@ -182,7 +220,11 @@ let rec nb_hyp c = match kind_of_term c with let try_head_pattern c = try head_pattern_bound c - with BoundPattern -> error "Bound head variable" + with BoundPattern -> error "Bound head variable." + +let dummy_goal = + {it = make_evar empty_named_context_val mkProp; + sigma = empty} let make_exact_entry pri (c,cty) = let cty = strip_outer_cast cty in @@ -190,12 +232,11 @@ let make_exact_entry pri (c,cty) = | Prod (_,_,_) -> failwith "make_exact_entry" | _ -> + let ce = mk_clenv_from dummy_goal (c,cty) in + let c' = clenv_type ce in + let pat = Pattern.pattern_of_constr c' in (head_of_constr_reference (List.hd (head_constr cty)), - { pri=(match pri with Some pri -> pri | None -> 0); pat=None; code=Give_exact c }) - -let dummy_goal = - {it = make_evar empty_named_context_val mkProp; - sigma = empty} + { pri=(match pri with Some pri -> pri | None -> 0); pat=Some pat; code=Give_exact c }) let make_apply_entry env sigma (eapply,verbose) pri (c,cty) = let cty = hnf_constr env sigma cty in @@ -238,8 +279,8 @@ let make_resolves env sigma flags pri c = if ents = [] then errorlabstrm "Hint" (pr_lconstr c ++ spc() ++ - (if fst flags then str"cannot be used as a hint" - else str "can be used as a hint only for eauto")); + (if fst flags then str"cannot be used as a hint." + else str "can be used as a hint only for eauto.")); ents (* used to add an hypothesis to the local hint database *) @@ -279,32 +320,23 @@ open Vernacexpr (* declaration of the AUTOHINT library object *) (**************************************************************************) -let add_hint_list hintlist (st,db) = - let db' = Hint_db.add_list hintlist db in - let st' = - List.fold_left - (fun (ids, csts as st) (_, hint) -> - match hint.code with - | Unfold_nth egr -> - (match egr with - | EvalVarRef id -> (Idpred.add id ids, csts) - | EvalConstRef cst -> (ids, Cpred.add cst csts)) - | _ -> st) - st hintlist - in (st', db') - (* If the database does not exist, it is created *) (* TODO: should a warning be printed in this case ?? *) let add_hint dbname hintlist = try let db = searchtable_map dbname in - let db' = add_hint_list hintlist db in + let db' = Hint_db.add_list hintlist db in searchtable_add (dbname,db') with Not_found -> - let db = add_hint_list hintlist (empty_transparent_state, Hint_db.empty) in + let db = Hint_db.add_list hintlist (Hint_db.empty false) in searchtable_add (dbname,db) -let cache_autohint (_,(local,name,hints)) = add_hint name hints +type hint_action = CreateDB of bool | UpdateDB of (global_reference * pri_auto_tactic) list + +let cache_autohint (_,(local,name,hints)) = + match hints with + | CreateDB b -> searchtable_add (name, Hint_db.empty b) + | UpdateDB hints -> add_hint name hints let forward_subst_tactic = ref (fun _ -> failwith "subst_tactic is not installed for auto") @@ -354,12 +386,15 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) = if lab' == lab && data' == data then hint else (lab',data') in - let hintlist' = list_smartmap subst_hint hintlist in - if hintlist' == hintlist then obj else - (local,name,hintlist') - + match hintlist with + | CreateDB _ -> obj + | UpdateDB hintlist -> + let hintlist' = list_smartmap subst_hint hintlist in + if hintlist' == hintlist then obj else + (local,name,UpdateDB hintlist') + let classify_autohint (_,((local,name,hintlist) as obj)) = - if local or hintlist = [] then Dispose else Substitute obj + if local or hintlist = (UpdateDB []) then Dispose else Substitute obj let export_autohint ((local,name,hintlist) as obj) = if local then None else Some obj @@ -373,6 +408,9 @@ let (inAutoHint,outAutoHint) = export_function = export_autohint } +let create_hint_db l n b = + Lib.add_anonymous_leaf (inAutoHint (l,n,CreateDB b)) + (**************************************************************************) (* The "Hint" vernacular command *) (**************************************************************************) @@ -381,19 +419,18 @@ let add_resolves env sigma clist local dbnames = (fun dbname -> Lib.add_anonymous_leaf (inAutoHint - (local,dbname, - List.flatten (List.map (fun (x, y) -> - make_resolves env sigma (true,Flags.is_verbose()) x y) clist)))) + (local,dbname, UpdateDB + (List.flatten (List.map (fun (x, y) -> + make_resolves env sigma (true,Flags.is_verbose()) x y) clist))))) dbnames let add_unfolds l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf - (inAutoHint (local,dbname, List.map make_unfold l))) + (inAutoHint (local,dbname, UpdateDB (List.map make_unfold l)))) dbnames - let add_extern pri (patmetas,pat) tacast local dbname = (* We check that all metas that appear in tacast have at least one occurence in the left pattern pat *) @@ -401,10 +438,10 @@ let add_extern pri (patmetas,pat) tacast local dbname = match (list_subtract tacmetas patmetas) with | i::_ -> errorlabstrm "add_extern" - (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound") + (str "The meta-variable ?" ++ pr_patvar i ++ str" is not bound.") | [] -> Lib.add_anonymous_leaf - (inAutoHint(local,dbname, [make_extern pri pat tacast])) + (inAutoHint(local,dbname, UpdateDB [make_extern pri pat tacast])) let add_externs pri pat tacast local dbnames = List.iter (add_extern pri pat tacast local) dbnames @@ -413,7 +450,7 @@ let add_trivials env sigma l local dbnames = List.iter (fun dbname -> Lib.add_anonymous_leaf ( - inAutoHint(local,dbname, List.map (make_trivial env sigma) l))) + inAutoHint(local,dbname, UpdateDB (List.map (make_trivial env sigma) l)))) dbnames let forward_intern_tac = @@ -439,7 +476,7 @@ let add_hints local dbnames0 h = | _ -> errorlabstrm "evalref_of_ref" (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ - str "to an evaluable reference") + str "to an evaluable reference.") in if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; (gr,r') in @@ -493,7 +530,7 @@ let fmt_hint_list_for_head c = let dbs = Hintdbmap.to_list !searchtable in let valid_dbs = map_succeed - (fun (name,(_,db)) -> (name,db,Hint_db.map_all c db)) + (fun (name,db) -> (name,db,Hint_db.map_all c db)) dbs in if valid_dbs = [] then @@ -519,11 +556,11 @@ let fmt_hint_term cl = let valid_dbs = if occur_existential cl then map_succeed - (fun (name, (_, db)) -> (name, db, Hint_db.map_all hd db)) + (fun (name, db) -> (name, db, Hint_db.map_all hd db)) dbs else map_succeed - (fun (name, (_, db)) -> + (fun (name, db) -> (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) dbs in @@ -534,6 +571,9 @@ let fmt_hint_term cl = hov 0 (prlist fmt_hints_db valid_dbs)) with Bound | Match_failure _ | Failure _ -> (str "No hint applicable for current goal") + +let error_no_such_hint_database x = + error ("No such Hint database: "^x^".") let print_hint_term cl = ppnl (fmt_hint_term cl) @@ -544,7 +584,8 @@ let print_applicable_hint () = print_hint_term (pf_concl gl) (* displays the whole hint database db *) -let print_hint_db ((ids, csts),db) = +let print_hint_db db = + let (ids, csts) = Hint_db.transparent_state db in msg (hov 0 (str"Unfoldable variable definitions: " ++ pr_idpred ids ++ fnl () ++ str"Unfoldable constant definitions: " ++ pr_cpred csts ++ fnl ())); @@ -559,13 +600,13 @@ let print_hint_db_by_name dbname = try let db = searchtable_map dbname in print_hint_db db with Not_found -> - error (dbname^" : No such Hint database") + error_no_such_hint_database dbname (* displays all the hints of all databases *) let print_searchtable () = Hintdbmap.iter (fun name db -> - msg (str "In the database " ++ str name ++ fnl ()); + msg (str "In the database " ++ str name ++ str ":" ++ fnl ()); print_hint_db db) !searchtable @@ -600,7 +641,7 @@ let unify_resolve_nodelta (c,clenv) gls = let unify_resolve flags (c,clenv) gls = let clenv' = connect_clenv gls clenv in let _ = clenv_unique_resolver false ~flags clenv' gls in - h_apply true false (c,NoBindings) gls + h_apply true false [c,NoBindings] gls (* builds a hint database from a constr signature *) @@ -610,7 +651,7 @@ let make_local_hint_db eapply lems g = let sign = pf_hyps g in let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in let hintlist' = list_map_append (pf_apply make_resolves g (eapply,false) None) lems in - (empty_transparent_state, Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty)) + Hint_db.add_list hintlist' (Hint_db.add_list hintlist (Hint_db.empty false)) (* Serait-ce possible de compiler d'abord la tactique puis de faire la substitution sans passer par bdize dont l'objectif est de préparer un @@ -648,7 +689,7 @@ let rec trivial_fail_db mod_delta db_list local_db gl = tclTHEN intro (fun g'-> let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') - in trivial_fail_db mod_delta db_list (add_hint_list hintl local_db) g') + in trivial_fail_db mod_delta db_list (Hint_db.add_list hintl local_db) g') in tclFIRST (assumption::intro_tac:: @@ -658,12 +699,10 @@ let rec trivial_fail_db mod_delta db_list local_db gl = and my_find_search_nodelta db_list local_db hdc concl = let tacl = if occur_existential concl then - list_map_append - (fun (st, db) -> (Hint_db.map_all hdc db)) + list_map_append (Hint_db.map_all hdc) (local_db::db_list) else - list_map_append (fun (_, db) -> - Hint_db.map_auto (hdc,concl) db) + list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) in List.map @@ -691,12 +730,13 @@ and my_find_search_delta db_list local_db hdc concl = let tacl = if occur_existential concl then list_map_append - (fun (st, db) -> - let st = {flags with modulo_delta = st} in + (fun db -> + let st = {flags with modulo_delta = Hint_db.transparent_state db} in List.map (fun x -> (st,x)) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun ((ids, csts as st), db) -> + list_map_append (fun db -> + let (ids, csts as st) = Hint_db.transparent_state db in let st, l = let l = if (Idpred.is_empty ids && Cpred.is_empty csts) @@ -737,7 +777,7 @@ let trivial lems dbnames gl = try searchtable_map x with Not_found -> - error ("trivial: "^x^": No such Hint database")) + error_no_such_hint_database x) ("core"::dbnames) in tclTRY (trivial_fail_db false db_list (make_local_hint_db false lems gl)) gl @@ -776,7 +816,7 @@ let decomp_unary_term c gls = if Hipattern.is_conjunction hd then simplest_case c gls else - errorlabstrm "Auto.decomp_unary_term" (str "not a unary type") + errorlabstrm "Auto.decomp_unary_term" (str "Not a unary type.") let decomp_empty_term c gls = let typc = pf_type_of gls c in @@ -784,7 +824,7 @@ let decomp_empty_term c gls = if Hipattern.is_empty_type hd then simplest_case c gls else - errorlabstrm "Auto.decomp_empty_term" (str "not an empty type") + errorlabstrm "Auto.decomp_empty_term" (str "Not an empty type.") (* decomp is an natural number giving an indication on decomposition @@ -817,7 +857,7 @@ let rec search_gen decomp n mod_delta db_list local_db extra_sign goal = (mkVar hid, htyp)] with Failure _ -> [] in - search_gen decomp n mod_delta db_list (add_hint_list hintl local_db) [d] g') + search_gen decomp n mod_delta db_list (Hint_db.add_list hintl local_db) [d] g') in let rec_tacs = List.map @@ -840,7 +880,7 @@ let delta_auto mod_delta n lems dbnames gl = try searchtable_map x with Not_found -> - error ("auto: "^x^": No such Hint database")) + error_no_such_hint_database x) ("core"::dbnames) in let hyps = pf_hyps gl in @@ -956,7 +996,7 @@ let rec super_search n db_list local_db argl goal = (tclTHEN intro (fun g -> let hintl = pf_apply make_resolve_any_hyp g (pf_last_hyp g) in - super_search n db_list (add_hint_list hintl local_db) + super_search n db_list (Hint_db.add_list hintl local_db) argl g)) :: ((List.map @@ -974,7 +1014,7 @@ let search_superauto n to_add argl g = (fun (id,c) -> add_named_decl (id, None, pf_type_of g c)) to_add empty_named_context in let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in - let db = add_hint_list db0 (make_local_hint_db false [] g) in + let db = Hint_db.add_list db0 (make_local_hint_db false [] g) in super_search n [Hintdbmap.find "core" !searchtable] db argl g let superauto n to_add argl = diff --git a/tactics/auto.mli b/tactics/auto.mli index 37406a30..edaaa1c1 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: auto.mli 10868 2008-04-29 12:30:25Z msozeau $ i*) +(*i $Id: auto.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Util @@ -47,24 +47,30 @@ type search_entry = stored_data list * stored_data list * stored_data Btermdn.t module Hint_db : sig type t - val empty : t + val empty : bool -> t val find : global_reference -> t -> search_entry val map_all : global_reference -> t -> pri_auto_tactic list val map_auto : global_reference * constr -> t -> pri_auto_tactic list val add_one : global_reference * pri_auto_tactic -> t -> t val add_list : (global_reference * pri_auto_tactic) list -> t -> t val iter : (global_reference -> stored_data list -> unit) -> t -> unit + + val transparent_state : t -> transparent_state + val set_transparent_state : t -> transparent_state -> t + val set_rigid : t -> constant -> t end type hint_db_name = string -type hint_db = transparent_state * Hint_db.t +type hint_db = Hint_db.t val searchtable_map : hint_db_name -> hint_db -val current_db_names : unit -> hint_db_name list +val searchtable_add : (hint_db_name * hint_db) -> unit -val add_hint_list : (global_reference * pri_auto_tactic) list -> hint_db -> hint_db +val create_hint_db : bool -> hint_db_name -> bool -> unit + +val current_db_names : unit -> hint_db_name list val add_hints : locality_flag -> hint_db_name list -> hints -> unit @@ -207,3 +213,5 @@ val superauto : int -> (identifier * constr) list -> autoArguments list -> tacti *) val h_superauto : int option -> reference list -> bool -> bool -> tactic + +val auto_init : (unit -> unit) ref diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 1d096ec7..4759b6da 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: autorewrite.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: autorewrite.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Equality open Hipattern @@ -56,7 +56,7 @@ let print_rewrite_hintdb bas = with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist")) + (str ("Rewriting base "^(bas)^" does not exist.")) type raw_rew_rule = constr * bool * raw_tactic_expr @@ -67,7 +67,7 @@ let one_base general_rewrite_maybe_in tac_main bas = Stringmap.find bas !rewtab with Not_found -> errorlabstrm "AutoRewrite" - (str ("Rewriting base "^(bas)^" does not exist")) + (str ("Rewriting base "^(bas)^" does not exist.")) in let lrul = List.map (fun (c,_,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) -> @@ -99,7 +99,7 @@ let autorewrite_multi_in idl tac_main lbas : tactic = match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with (last_hyp_id,_,_)::_ -> last_hyp_id | _ -> (* even the hypothesis id is missing *) - error ("No such hypothesis : " ^ (string_of_id !id)) + error ("No such hypothesis: " ^ (string_of_id !id) ^".") in let gl' = general_rewrite_in dir all_occurrences !id cstr false gl in let gls = (fst gl').Evd.it in @@ -140,7 +140,7 @@ let gen_auto_multi_rewrite tac_main lbas cl = if cl.concl_occs <> all_occurrences_expr & cl.concl_occs <> no_occurrences_expr then - error "The \"at\" syntax isn't available yet for the autorewrite tactic" + error "The \"at\" syntax isn't available yet for the autorewrite tactic." else let compose_tac t1 t2 = match cl.onhyps with @@ -170,8 +170,7 @@ let auto_multi_rewrite_with tac_main lbas cl gl = 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") + (strbrk "autorewrite .. in .. using can only be used either with a unique hypothesis or on the conclusion.") (* Functions necessary to the library object declaration *) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index f0b23b8d..a0aecbbc 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: btermdn.ml 6427 2004-12-07 17:41:10Z sacerdot $ *) +(* $Id: btermdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Term +open Names open Termdn open Pattern open Libnames @@ -19,6 +20,23 @@ open Libnames let dnet_depth = ref 8 +let bounded_constr_pat_discr_st st (t,depth) = + if depth = 0 then + None + else + match constr_pat_discr_st st t with + | None -> None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + +let bounded_constr_val_discr_st st (t,depth) = + if depth = 0 then + Dn.Nothing + else + match constr_val_discr_st st t with + | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) + | Dn.Nothing -> Dn.Nothing + | Dn.Everything -> Dn.Everything + let bounded_constr_pat_discr (t,depth) = if depth = 0 then None @@ -29,24 +47,44 @@ let bounded_constr_pat_discr (t,depth) = let bounded_constr_val_discr (t,depth) = if depth = 0 then - None + Dn.Nothing else match constr_val_discr t with - | None -> None - | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) + | Dn.Nothing -> Dn.Nothing + | Dn.Everything -> Dn.Everything type 'a t = (global_reference,constr_pattern * int,'a) Dn.t - + let create = Dn.create + +let add = function + | None -> + (fun dn (c,v) -> + Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v)) + | Some st -> + (fun dn (c,v) -> + Dn.add dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) -let add dn (c,v) = Dn.add dn bounded_constr_pat_discr ((c,!dnet_depth),v) - -let rmv dn (c,v) = Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v) +let rmv = function + | None -> + (fun dn (c,v) -> + Dn.rmv dn bounded_constr_pat_discr ((c,!dnet_depth),v)) + | Some st -> + (fun dn (c,v) -> + Dn.rmv dn (bounded_constr_pat_discr_st st) ((c,!dnet_depth),v)) -let lookup dn t = - List.map - (fun ((c,_),v) -> (c,v)) - (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth)) +let lookup = function + | None -> + (fun dn t -> + List.map + (fun ((c,_),v) -> (c,v)) + (Dn.lookup dn bounded_constr_val_discr (t,!dnet_depth))) + | Some st -> + (fun dn t -> + List.map + (fun ((c,_),v) -> (c,v)) + (Dn.lookup dn (bounded_constr_val_discr_st st) (t,!dnet_depth))) let app f dn = Dn.app (fun ((c,_),v) -> f(c,v)) dn diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 1ac33557..959f7d10 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,11 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: btermdn.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: btermdn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Term open Pattern +open Names (*i*) (* Discrimination nets with bounded depth. *) @@ -19,10 +20,10 @@ type 'a t val create : unit -> 'a t -val add : 'a t -> (constr_pattern * 'a) -> 'a t -val rmv : 'a t -> (constr_pattern * 'a) -> 'a t - -val lookup : 'a t -> constr -> (constr_pattern * 'a) list +val add : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t +val rmv : transparent_state option -> 'a t -> (constr_pattern * 'a) -> 'a t + +val lookup : transparent_state option -> 'a t -> constr -> (constr_pattern * 'a) list val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit val dnet_depth : int ref diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 9a1a3042..6eb5e359 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: class_tactics.ml4 11150 2008-06-19 11:38:27Z msozeau $ *) +(* $Id: class_tactics.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -43,11 +43,13 @@ open Evd let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" +let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db false) + let check_imported_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in if not (Library.library_is_loaded dir) then - error ("Library "^(list_last d)^" has to be imported first") + error ("Library "^(list_last d)^" has to be imported first.") let classes_dirpath = make_dirpath (List.map id_of_string ["Classes";"Coq"]) @@ -58,6 +60,17 @@ let init_setoid () = (** Typeclasses instance search tactic / eauto *) +let evars_of_term init c = + let rec evrec acc c = + match kind_of_term c with + | Evar (n, _) -> Intset.add n acc + | _ -> fold_constr evrec acc c + in + evrec init c + +let intersects s t = + Intset.exists (fun el -> Intset.mem el t) s + open Auto let e_give_exact c gl = @@ -98,7 +111,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (add_hint_list hintl local_db) g'))) :: + (Hint_db.add_list hintl local_db) g'))) :: (List.map pi1 (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal @@ -108,11 +121,15 @@ and e_my_find_search db_list local_db hdc concl = let hintl = if occur_existential concl then list_map_append - (fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_all hdc db)) + (fun db -> + let st = Hint_db.transparent_state db in + List.map (fun x -> (st, x)) (Hint_db.map_all hdc db)) (local_db::db_list) else list_map_append - (fun (st, db) -> List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db)) + (fun db -> + let st = Hint_db.transparent_state db in + List.map (fun x -> (st, x)) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = @@ -147,15 +164,14 @@ let e_possible_resolve db_list local_db gl = let find_first_goal gls = try first_goal gls with UserError _ -> assert false - - + type search_state = { depth : int; (*r depth of search before failing *) tacres : goal list sigma * validation; pri : int; last_tactic : std_ppcmds; dblist : Auto.hint_db list; - localdb : Auto.hint_db list } + localdb : (bool ref * bool ref option * Auto.hint_db) list } let filter_hyp t = match kind_of_term t with @@ -167,13 +183,25 @@ let rec catchable = function | Stdpp.Exc_located (_, e) -> catchable e | e -> Logic.catchable_exception e +let is_dep gl gls = + let evs = evars_of_term Intset.empty gl.evar_concl in + if evs = Intset.empty then false + else + List.fold_left + (fun b gl -> + if b then b + else + let evs' = evars_of_term Intset.empty gl.evar_concl in + intersects evs evs') + false gls + module SearchProblem = struct type state = search_state let debug = ref false - let success s = (sig_it (fst s.tacres)) = [] + let success s = sig_it (fst s.tacres) = [] let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl) @@ -182,23 +210,14 @@ module SearchProblem = struct prlist (pr_ev evars) (sig_it gls) let filter_tactics (glls,v) l = -(* if !debug then *) -(* (let _ = Proof_trees.db_pr_goal (List.hd (sig_it glls)) in *) -(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) -(* msg (str"Goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n")); *) + let glls,nv = apply_tac_list tclNORMEVAR glls in + let v p = v (nv p) in let rec aux = function | [] -> [] | (tac,pri,pptac) :: tacl -> try -(* if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *) let (lgls,ptl) = apply_tac_list tac glls in let v' p = v (ptl p) in -(* if !debug then *) -(* begin *) -(* let evars = Evarutil.nf_evars (Refiner.project glls) in *) -(* msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *) -(* msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *) -(* end; *) ((lgls,v'),pri,pptac) :: aux tacl with e when catchable e -> aux tacl in aux l @@ -214,65 +233,83 @@ module SearchProblem = struct List.length (sig_it (fst s.tacres)) + nb_empty_evars (sig_sig (fst s.tacres)) in - if d <> 0 && d <> 1 then d else + if d <> 0 then d else let pri = s.pri - s'.pri in if pri <> 0 then pri else nbgoals s - nbgoals s' - + let branching s = if s.depth = 0 then [] else - let lg = fst s.tacres in - let nbgl = List.length (sig_it lg) in - assert (nbgl > 0); - let g = find_first_goal lg in - let assumption_tacs = - let l = - filter_tactics s.tacres - (List.map - (fun id -> (Eauto.e_give_exact_constr (mkVar id), 0, - (str "exact" ++ spc () ++ pr_id id))) - (List.filter (fun id -> filter_hyp (pf_get_hyp_typ g id)) - (pf_ids_of_hyps g))) - in - List.map (fun (res,pri,pp) -> { s with tacres = res; pri = 0; - last_tactic = pp; localdb = List.tl s.localdb }) l - in -(* let intro_tac = *) -(* List.map *) -(* (fun ((lgls,_) as res,pri,pp) -> *) -(* let g' = first_goal lgls in *) -(* let hintl = *) -(* make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') *) -(* in *) -(* let ldb = Hint_db.add_list hintl (match s.localdb with [] -> assert false | hd :: _ -> hd) in *) -(* { s with tacres = res; *) -(* last_tactic = pp; *) -(* pri = pri; *) -(* localdb = ldb :: List.tl s.localdb }) *) -(* (filter_tactics s.tacres [Tactics.intro,1,(str "intro")]) *) -(* in *) - let possible_resolve ((lgls,_) as res, pri, pp) = - let nbgl' = List.length (sig_it lgls) in - if nbgl' < nbgl then - { s with tacres = res; last_tactic = pp; pri = pri; - localdb = List.tl s.localdb } - else - { s with - depth = pred s.depth; tacres = res; - last_tactic = pp; pri = pri; - localdb = - list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb } - in - let rec_tacs = - let l = - filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) (pf_concl g)) - in - List.map possible_resolve l - in - List.sort compare (assumption_tacs (* @intro_tac @ custom_tac *) @ rec_tacs) - + let (cut, do_cut, ldb as hdldb) = List.hd s.localdb in + if !cut then [] + else begin + Option.iter (fun r -> r := true) do_cut; + let {it=gl; sigma=sigma} = fst s.tacres in + let nbgl = List.length gl in + let g = { it = List.hd gl ; sigma = sigma } in + let new_db, localdb = + let tl = List.tl s.localdb in + match tl with + | [] -> hdldb, tl + | (cut', do', ldb') :: rest -> + if not (is_dep (Evarutil.nf_evar_info sigma (List.hd gl)) (List.tl gl)) then + let fresh = ref false in + if do' = None then + (fresh, None, ldb), (cut', Some fresh, ldb') :: rest + else + (cut', None, ldb), tl + else hdldb, tl + in let localdb = new_db :: localdb in + let assumption_tacs = + let l = + filter_tactics s.tacres + (List.map + (fun id -> (Eauto.e_give_exact_constr (mkVar id), 0, + (str "exact" ++ spc () ++ pr_id id))) + (List.filter (fun id -> filter_hyp (pf_get_hyp_typ g id)) + (pf_ids_of_hyps g))) + in + List.map (fun (res,pri,pp) -> { s with tacres = res; pri = 0; + last_tactic = pp; localdb = List.tl s.localdb }) l + in + let intro_tac = + List.map + (fun ((lgls,_) as res,pri,pp) -> + let g' = first_goal lgls in + let hintl = + make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') + in + let ldb = Hint_db.add_list hintl ldb in + { s with tacres = res; + last_tactic = pp; + pri = pri; + localdb = (cut, None, ldb) :: List.tl s.localdb }) + (filter_tactics s.tacres [Tactics.intro,1,(str "intro")]) + in + let possible_resolve ((lgls,_) as res, pri, pp) = + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { s with + depth = pred s.depth; + tacres = res; last_tactic = pp; pri = pri; + localdb = List.tl localdb } + else + { s with depth = pred s.depth; tacres = res; + last_tactic = pp; pri = pri; + localdb = list_tabulate (fun _ -> new_db) (nbgl'-nbgl) @ localdb } + in + let concl = Evarutil.nf_evar (project g) (pf_concl g) in + let rec_tacs = + let l = + filter_tactics s.tacres (e_possible_resolve s.dblist ldb concl) + in + List.map possible_resolve l + in + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) + end + let pp s = msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ s.last_tactic ++ str "\n")) @@ -340,11 +377,13 @@ let e_breadth_search debug s = let tac = if debug then Search.debug_breadth_first else Search.breadth_first in let s = tac s in s.tacres - with Not_found -> error "EAuto: breadth first search failed" + with Not_found -> error "eauto: breadth first search failed." -let e_search_auto debug (in_depth,p) lems db_list gls = +let e_search_auto debug (in_depth,p) lems st db_list gls = let sigma = Evd.sig_sig (fst gls) and gls' = Evd.sig_it (fst gls) in - let local_dbs = List.map (fun gl -> make_local_hint_db true lems ({it = gl; sigma = sigma})) gls' in + let local_dbs = List.map (fun gl -> + let db = make_local_hint_db true lems ({it = gl; sigma = sigma}) in + (ref false, None, Hint_db.set_transparent_state db st)) gls' in let state = make_initial_state p gls db_list local_dbs in if in_depth then e_depth_search debug state @@ -355,20 +394,14 @@ let full_eauto debug n lems gls = let dbnames = current_db_names () in let dbnames = list_subtract dbnames ["v62"] in let db_list = List.map searchtable_map dbnames in - e_search_auto debug n lems db_list gls + e_search_auto debug n lems empty_transparent_state db_list gls let nf_goal (gl, valid) = { gl with sigma = Evarutil.nf_evars gl.sigma }, valid let typeclasses_eauto debug n lems gls = - let dbnames = [typeclasses_db] in - let db_list = List.map - (fun x -> - try searchtable_map x - with Not_found -> (empty_transparent_state, Hint_db.empty)) - dbnames - in - e_search_auto debug n lems db_list gls + let db = searchtable_map typeclasses_db in + e_search_auto debug n lems (Hint_db.transparent_state db) [db] gls exception Found of evar_map @@ -404,31 +437,23 @@ let resolve_all_evars_once debug (mode, depth) env p evd = exception FoundTerm of constr -let resolve_one_typeclass env gl = - let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = Evd.empty } in - let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof Evd.empty (List.hd x)))) in +let resolve_one_typeclass env ?(sigma=Evd.empty) gl = + let gls = { it = [ Evd.make_evar (Environ.named_context_val env) gl ] ; sigma = sigma } in + let valid x = raise (FoundTerm (fst (Refiner.extract_open_proof sigma (List.hd x)))) in let gls', valid' = typeclasses_eauto false (true, default_eauto_depth) [] (gls, valid) in try ignore(valid' []); assert false with FoundTerm t -> let term = Evarutil.nf_evar (sig_sig gls') t in if occur_existential term then raise Not_found else term +let _ = + Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z) + let has_undefined p oevd evd = Evd.fold (fun ev evi has -> has || (evi.evar_body = Evar_empty && p ev evi && (try Typeclasses.is_resolvable (Evd.find oevd ev) with _ -> true))) (Evd.evars_of evd) false -let evars_of_term init c = - let rec evrec acc c = - match kind_of_term c with - | Evar (n, _) -> Intset.add n acc - | _ -> fold_constr evrec acc c - in - evrec init c - -let intersects s t = - Intset.exists (fun el -> Intset.mem el t) s - let rec merge_deps deps = function | [] -> [deps] | hd :: tl -> @@ -486,18 +511,21 @@ let resolve_all_evars debug m env p oevd do_split fail = | Some evd' -> docomp evd' comps in docomp oevd split -(* let resolve_all_evars debug m env p oevd = *) -(* let oevm = Evd.evars_of oevd in *) -(* try *) -(* let rec aux n evd = *) -(* if has_undefined p oevm evd then *) -(* if n > 0 then *) -(* let evd' = resolve_all_evars_once debug m env p evd in *) -(* aux (pred n) evd' *) -(* else None *) -(* else Some evd *) -(* in aux 3 oevd *) -(* with Not_found -> None *) +let resolve_typeclass_evars d p env evd onlyargs split fail = + let pred = + if onlyargs then + (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && + Typeclasses.is_class_evar evi) + else (fun ev evi -> Typeclasses.is_class_evar evi) + in resolve_all_evars d p env pred evd split fail + +let solve_inst debug mode depth env evd onlyargs split fail = + resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail + +let _ = + Typeclasses.solve_instanciations_problem := + solve_inst false true default_eauto_depth + VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings | [ "Typeclasses" "unfold" reference_list(cl) ] -> [ @@ -505,6 +533,20 @@ VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings ] END +VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings +| [ "Typeclasses" "rigid" reference_list(cl) ] -> [ + let db = searchtable_map typeclasses_db in + let db' = + List.fold_left (fun acc r -> + let gr = Syntax_def.global_with_alias r in + match gr with + | ConstRef c -> Hint_db.set_rigid acc c + | _ -> acc) db cl + in + searchtable_add (typeclasses_db,db') + ] +END + (** Typeclass-based rewriting. *) let respect_proj = lazy (mkConst (snd (List.hd (Lazy.force morphism_class).cl_projs))) @@ -518,6 +560,7 @@ let try_find_reference dir s = let gen_constant dir s = Coqlib.gen_constant "Class_setoid" dir s let coq_proj1 = lazy(gen_constant ["Init"; "Logic"] "proj1") let coq_proj2 = lazy(gen_constant ["Init"; "Logic"] "proj2") +let coq_eq = lazy(gen_constant ["Init"; "Logic"] "eq") let iff = lazy (gen_constant ["Init"; "Logic"] "iff") let coq_all = lazy (gen_constant ["Init"; "Logic"] "all") let impl = lazy (gen_constant ["Program"; "Basics"] "impl") @@ -539,7 +582,7 @@ let coq_inverse = lazy (gen_constant (* ["Classes"; "RelationClasses"] "inverse" let inverse car rel = mkApp (Lazy.force coq_inverse, [| car ; car; mkProp; rel |]) let complement = lazy (gen_constant ["Classes"; "RelationClasses"] "complement") -let pointwise_relation = lazy (gen_constant ["Classes"; "RelationClasses"] "pointwise_relation") +let pointwise_relation = lazy (gen_constant ["Classes"; "Morphisms"] "pointwise_relation") let respectful_dep = lazy (gen_constant ["Classes"; "Morphisms"] "respectful_dep") let respectful = lazy (gen_constant ["Classes"; "Morphisms"] "respectful") @@ -556,6 +599,8 @@ let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalenc let setoid_equiv = lazy (gen_constant ["Classes"; "SetoidClass"] "equiv") let setoid_morphism = lazy (gen_constant ["Classes"; "SetoidClass"] "setoid_morphism") let setoid_refl_proj = lazy (gen_constant ["Classes"; "SetoidClass"] "Equivalence_Reflexive") + +let setoid_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "SetoidRelation") let arrow_morphism a b = if isprop a && isprop b then @@ -570,12 +615,25 @@ let morphism_type = lazy (constr_of_global (Lazy.force morphism_class).cl_impl) let morphism_proxy_type = lazy (constr_of_global (Lazy.force morphism_proxy_class).cl_impl) +let is_applied_setoid_relation t = + match kind_of_term t with + | App (c, args) when Array.length args >= 2 -> + let head = if isApp c then fst (destApp c) else c in + if eq_constr (Lazy.force coq_eq) head then false + else (try + let evd, evar = Evarutil.new_evar (Evd.create_evar_defs Evd.empty) (Global.env()) (new_Type ()) in + let inst = mkApp (Lazy.force setoid_relation, [| evar; c |]) in + ignore(Typeclasses.resolve_one_typeclass (Global.env()) (Evd.evars_of evd) inst); + true + with _ -> false) + | _ -> false + +let _ = + Equality.register_is_applied_setoid_relation is_applied_setoid_relation + exception Found of (constr * constr * (types * types) list * constr * constr array * (constr * (constr * constr * constr * constr)) option array) -let is_equiv env sigma t = - isConst t && Reductionops.is_conv env sigma (Lazy.force setoid_equiv) t - let split_head = function hd :: tl -> hd, tl | [] -> assert(false) @@ -703,13 +761,13 @@ let decompose_setoid_eqhyp env sigma c left2right = | [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 + | _ -> error "The term provided is not an applied relation." in let others,(c1,c2) = split_last_two args in let ty1, ty2 = Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2 in if not (evd_convertible env eqclause.evd ty1 ty2) then - error "The term does not end with an applied homogeneous relation" + error "The term does not end with an applied homogeneous relation." else { cl=eqclause; prf=(Clenv.clenv_value eqclause); car=ty1; rel=mkApp (equiv, Array.of_list others); @@ -736,11 +794,11 @@ let allowK = true let refresh_hypinfo env sigma hypinfo = if !hypinfo.abs = None then - let {l2r=l2r; c = c} = !hypinfo in + let {l2r=l2r; c = c;cl=cl} = !hypinfo in match c with | Some c -> (* Refresh the clausenv to not get the same meta twice in the goal. *) - hypinfo := decompose_setoid_eqhyp env sigma c l2r; + hypinfo := decompose_setoid_eqhyp cl.env (Evd.evars_of cl.evd) c l2r; | _ -> () else () @@ -780,11 +838,12 @@ let unify_eqn env sigma hypinfo t = let mvs = clenv_dependent false env' in clenv_pose_metas_as_evars env' mvs in - let c1 = Clenv.clenv_nf_meta env' c1 - and c2 = Clenv.clenv_nf_meta env' c2 - and car = Clenv.clenv_nf_meta env' car - and rel = Clenv.clenv_nf_meta env' rel in - let prf = Clenv.clenv_value env' in + let evd' = Typeclasses.resolve_typeclasses env'.env env'.evd in + let env' = { env' with evd = evd' } in + let nf c = Evarutil.nf_evar (Evd.evars_of evd') (Clenv.clenv_nf_meta env' c) in + let c1 = nf c1 and c2 = nf c2 + and car = nf car and rel = nf rel + and prf = nf (Clenv.clenv_value env') in let ty1 = Typing.mtype_of env'.env env'.evd c1 and ty2 = Typing.mtype_of env'.env env'.evd c2 in @@ -974,16 +1033,7 @@ let build_new gl env sigma flags loccs hypinfo concl cstr evars = let rest = List.filter (fun o -> o > nbocc_min_1) occs in if rest <> [] then error_invalid_occurrence rest; eq - -let resolve_typeclass_evars d p env evd onlyargs split fail = - let pred = - if onlyargs then - (fun ev evi -> Typeclasses.is_implicit_arg (snd (Evd.evar_source ev evd)) && - class_of_constr evi.Evd.evar_concl <> None) - else - (fun ev evi -> class_of_constr evi.Evd.evar_concl <> None) - in resolve_all_evars d p env pred evd split fail - + let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause gl = let concl, is_hyp = match clause with @@ -1025,7 +1075,7 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g | None -> let name = next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in tclTHENLAST - (Tacmach.internal_cut_no_check name newt) + (Tacmach.internal_cut_no_check false name newt) (tclTHEN (Tactics.revert [name]) (Tactics.refine p)) | Some (t, ty) -> Tactics.refine @@ -1057,11 +1107,17 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g try cl_rewrite_clause_aux ~flags hypinfo goal_meta occs clause gl with DependentMorphism -> tclFAIL 0 (str " setoid rewrite failed: cannot handle dependent morphisms") gl -let cl_rewrite_clause c left2right occs clause gl = +let cl_rewrite_clause (evm,c) left2right occs clause gl = init_setoid (); let meta = Evarutil.new_meta() in let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in - let hypinfo = ref (decompose_setoid_eqhyp (pf_env gl) (project gl) c left2right) in + let env = pf_env gl in + let evars = Evd.merge (project gl) evm in +(* let c = *) +(* let j = Pretyping.Default.understand_judgment_tcc evars env c in *) +(* j.Environ.uj_val *) +(* in *) + let hypinfo = ref (decompose_setoid_eqhyp env evars c left2right) in cl_rewrite_clause_aux hypinfo meta occs clause gl open Genarg @@ -1071,20 +1127,20 @@ let occurrences_of = function | n::_ as nl when n < 0 -> (false,List.map abs nl) | nl -> if List.exists (fun n -> n < 0) nl then - error "Illegal negative occurrence number"; + error "Illegal negative occurrence number."; (true,nl) TACTIC EXTEND class_rewrite -| [ "clrewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id) ] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), [])) ] -| [ "clrewrite" orient(o) constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None ] -| [ "clrewrite" orient(o) constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ] +| [ "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 ] END let clsubstitute o c = - let is_tac id = match kind_of_term c with Var id' when id' = id -> true | _ -> false in + let is_tac id = match kind_of_term (snd c) with Var id' when id' = id -> true | _ -> false in Tacticals.onAllClauses (fun cl -> match cl with @@ -1092,7 +1148,7 @@ let clsubstitute o c = | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl)) TACTIC EXTEND substitute -| [ "substitute" orient(o) constr(c) ] -> [ clsubstitute o c ] +| [ "substitute" orient(o) open_constr(c) ] -> [ clsubstitute o c ] END let pr_debug _prc _prlc _prt b = @@ -1122,13 +1178,6 @@ let pr_depth _prc _prlc _prt = function ARGUMENT EXTEND depth TYPED AS int option PRINTED BY pr_depth | [ int_or_var_opt(v) ] -> [ match v with Some (ArgArg i) -> Some i | _ -> None ] END - -let solve_inst debug mode depth env evd onlyargs split fail = - resolve_typeclass_evars debug (mode, depth) env evd onlyargs split fail - -let _ = - Typeclasses.solve_instanciations_problem := - solve_inst false true default_eauto_depth VERNAC COMMAND EXTEND Typeclasses_Settings | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ @@ -1146,7 +1195,8 @@ TACTIC EXTEND typeclasses_eauto fun gl -> let gls = {it = [sig_it gl]; sigma = project gl} in let vals v = List.hd v in - typeclasses_eauto d (mode, depth) [] (gls, vals) ] + try typeclasses_eauto d (mode, depth) [] (gls, vals) + with Not_found -> tclFAIL 0 (str" typeclasses eauto failed") gl ] END @@ -1172,15 +1222,15 @@ let _ = (* Compatibility with old Setoids *) TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(o) constr(c) ] + [ "setoid_rewrite" orient(o) open_constr(c) ] -> [ cl_rewrite_clause c o all_occurrences None ] - | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) ] -> + | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) ] -> [ cl_rewrite_clause c o all_occurrences (Some (([],id), []))] - | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) ] -> + | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) ] -> [ cl_rewrite_clause c o (occurrences_of occ) None] - | [ "setoid_rewrite" orient(o) constr(c) "at" occurrences(occ) "in" hyp(id)] -> + | [ "setoid_rewrite" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id)] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))] - | [ "setoid_rewrite" orient(o) constr(c) "in" hyp(id) "at" occurrences(occ)] -> + | [ "setoid_rewrite" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ)] -> [ cl_rewrite_clause c o (occurrences_of occ) (Some (([],id), []))] END @@ -1225,10 +1275,10 @@ let constr_tac = Tacinterp.interp (Tacexpr.TacAtom (dummy_loc, Tacexpr.TacAnyCon let declare_relation ?(binders=[]) a aeq n refl symm trans = init_setoid (); + let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.SetoidTactics.SetoidRelation" + in ignore(anew_instance binders instance []); match (refl,symm,trans) with - (None, None, None) -> - let instance = declare_instance a aeq n "Coq.Classes.SetoidTactics.DefaultRelation" - in ignore(anew_instance binders instance []) + (None, None, None) -> () | (Some lemma1, None, None) -> ignore (declare_instance_refl binders a aeq n lemma1) | (None, Some lemma2, None) -> @@ -1577,7 +1627,7 @@ let relation_of_constr c = | App (f, args) when Array.length args >= 2 -> let relargs, args = array_chop (Array.length args - 2) args in mkApp (f, relargs), args - | _ -> error "Not an applied relation" + | _ -> error "Not an applied relation." let is_loaded d = let d' = List.map id_of_string d in @@ -1624,7 +1674,7 @@ let setoid_symmetry_in id gl = 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 equivalence" + | _ -> error "The term provided is not an equivalence." in let others,(c1,c2) = split_last_two args in let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in @@ -1690,3 +1740,18 @@ TACTIC EXTEND apply_typeclasses Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl ] END + +let rec head_of_constr t = + let t = strip_outer_cast(collapse_appl t) in + match kind_of_term t with + | Prod (_,_,c2) -> head_of_constr c2 + | LetIn (_,_,_,c2) -> head_of_constr c2 + | App (f,args) -> head_of_constr f + | _ -> t + +TACTIC EXTEND head_of_constr + [ "head_of_constr" ident(h) constr(c) ] -> [ + let c = head_of_constr c in + letin_tac None (Name h) c allHyps + ] +END diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index a2c840a1..313d74a1 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: contradiction.ml 10169 2007-10-03 12:31:45Z herbelin $ *) +(* $Id: contradiction.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Term @@ -85,7 +85,7 @@ let contradiction_term (c,lbind as cl) gl = (fun id -> simplest_elim (mkApp (mkVar id,[|c|]))) gl else raise Not_found - with Not_found -> error "Not a contradiction" + with Not_found -> error "Not a contradiction." let contradiction = function | None -> tclTHEN intros contradiction_context diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml index d96fa720..97225617 100644 --- a/tactics/decl_interp.ml +++ b/tactics/decl_interp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: decl_interp.ml 10739 2008-04-01 14:45:20Z herbelin $ i*) +(*i $Id: decl_interp.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) open Util open Names @@ -162,8 +162,8 @@ let decompose_eq env id = 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" + else error "Previous step is not an equality." + | _ -> error "Previous step is not an equality." let get_eq_typ info env = let typ = decompose_eq env (get_last env) in @@ -331,9 +331,9 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = 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 : " ++ + (str "Wrong number of extra arguments: " ++ (if expected = 0 then str "none" else int expected) ++ - str "expected") in + 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 @@ -400,7 +400,7 @@ let interp_suffices_clause sigma env (hyps,cot)= let nhyps,nc = interp_hyps_gen fst (fun x _ -> x) sigma env hyps c in nhyps,This nc | Thesis Plain as th -> interp_hyps sigma env hyps,th - | Thesis (For n) -> error "\"thesis for\" is not applicable here" in + | Thesis (For n) -> error "\"thesis for\" is not applicable here." in let push_one hyp env0 = match hyp with (Hprop st | Hvar st) -> diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 895b97fe..5356868a 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: decl_proof_instr.ml 11072 2008-06-08 16:13:37Z herbelin $ *) +(* $Id: decl_proof_instr.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Pp @@ -106,6 +106,9 @@ let clean_tmp gls = in clean_all (tmp_ids gls) gls +let assert_postpone id t = + assert_as true (dummy_loc, Genarg.IntroIdentifier id) t + (* start a proof *) let start_proof_tac gls= @@ -188,7 +191,7 @@ 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 + 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 @@ -207,18 +210,18 @@ let close_block bt pts = B_claim, Claim::_ | B_focus, Focus_claim::_ | B_proof, [] -> daimon_subtree (goto_current_focus pts) | _, Claim::_ -> - error "\"end claim\" expected" + error "\"end claim\" expected." | _, Focus_claim::_ -> - error "\"end focus\" expected" + error "\"end focus\" expected." | _, [] -> - error "\"end proof\" 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" + ET_Case_analysis -> error "\"end cases\" expected." + | ET_Induction -> error "\"end induction\" expected." end - | _,_ -> anomaly "lonely suppose on stack" + | _,_ -> anomaly "Lonely suppose on stack." (* utility for suppose / suppose it is *) @@ -284,10 +287,10 @@ let justification tac gls= (tclSOLVE [tclTHEN tac assumption]) (fun gls -> if get_strictness () then - error "insufficient justification" + error "Insufficient justification." else begin - msg_warning (str "insufficient justification"); + msg_warning (str "Insufficient justification."); daimon_tac gls end) gls @@ -475,7 +478,7 @@ let thus_tac c ctyp submetas gls = try find_subsubgoal c ctyp 0 submetas gls with Not_found -> - error "I could not relate this statement to the thesis" in + error "I could not relate this statement to the thesis." in if list = [] then exact_check proof gls else @@ -490,7 +493,7 @@ let anon_id_base = id_of_string "__" let mk_stat_or_thesis info gls = function This c -> c | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here" + error "\"thesis for ...\" is not applicable here." | Thesis Plain -> pf_concl gls let just_tac _then cut info gls0 = @@ -524,7 +527,7 @@ let instr_cut mkstat _thus _then cut gls0 = if _thus then thus_tac (mkVar c_id) c_stat [] gls else tclIDTAC gls in - tclTHENS (internal_cut c_id c_stat) + tclTHENS (assert_postpone c_id c_stat) [tclTHEN tcl_erase_info (just_tac _then cut info); thus_tac] gls0 @@ -542,12 +545,12 @@ let decompose_eq id gls = then (args.(0), args.(1), args.(2)) - else error "previous step is not an equality" - | _ -> error "previous step is not an equality" + else error "Previous step is not an equality." + | _ -> error "Previous step is not an equality." let instr_rew _thus rew_side cut gls0 = let last_id = - try get_last (pf_env gls0) with _ -> error "no previous equality" in + try get_last (pf_env gls0) with _ -> error "No previous equality." in let typ,lhs,rhs = decompose_eq last_id gls0 in let items_tac gls = match cut.cut_by with @@ -572,14 +575,14 @@ let instr_rew _thus rew_side cut gls0 = 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) + tclTHENS (assert_postpone c_id new_eq) [tclTHEN tcl_erase_info (tclTHENS (transitivity lhs) [just_tac;exact_check (mkVar last_id)]); 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) + tclTHENS (assert_postpone c_id new_eq) [tclTHEN tcl_erase_info (tclTHENS (transitivity rhs) [exact_check (mkVar last_id);just_tac]); @@ -600,7 +603,7 @@ let instr_claim _thus st gls0 = else tclIDTAC gls in let ninfo1 = {pm_stack= (if _thus then Focus_claim else Claim)::info.pm_stack} in - tclTHENS (internal_cut id st.st_it) + tclTHENS (assert_postpone id st.st_it) [tcl_change_info ninfo1; thus_tac] gls0 @@ -691,7 +694,7 @@ let instr_suffices _then cut gls0 = let c_term = applist (mkVar c_id,List.map mkMeta metas) in let thus_tac gls= thus_tac c_term c_head c_ctx gls in - tclTHENS (internal_cut c_id c_stat) + tclTHENS (assert_postpone c_id c_stat) [tclTHENLIST [ assume_tac ctx; tcl_erase_info; @@ -730,7 +733,7 @@ let rec consider_match may_intro introduced available expected gls = match available,expected with [],[] -> tclIDTAC gls - | _,[] -> error "last statements do not match a complete hypothesis" + | _,[] -> error "Last statements do not match a complete hypothesis." (* should tell which ones *) | [],hyps -> if may_intro then @@ -740,11 +743,11 @@ let rec consider_match may_intro introduced available expected gls = (intro_mustbe_force id) (consider_match true [] [id] hyps) (fun _ -> - error "not enough sub-hypotheses to match statements") + error "Not enough sub-hypotheses to match statements.") gls end else - error "not enough sub-hypotheses to match statements" + 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)) @@ -761,7 +764,7 @@ let rec consider_match may_intro introduced available expected gls = (fun gls -> let nhyps = try conjunction_arity id gls with - Not_found -> error "matching hypothesis not found" in + Not_found -> error "Matching hypothesis not found." in tclTHENLIST [general_case_analysis false (mkVar id,NoBindings); intron_then nhyps [] @@ -777,7 +780,7 @@ let consider_tac c hyps gls = | _ -> let id = pf_get_new_id (id_of_string "_tmp") gls in tclTHEN - (forward None (Genarg.IntroIdentifier id) c) + (forward None (dummy_loc, Genarg.IntroIdentifier id) c) (consider_match false [] [id] hyps) gls @@ -818,7 +821,7 @@ let cast_tac id_or_thesis typ gls = let (_,body,_) = pf_get_hyp gls id in convert_hyp (id,body,typ) gls | Thesis (For _ ) -> - error "\"thesis for ...\" is not applicable here" + error "\"thesis for ...\" is not applicable here." | Thesis Plain -> convert_concl typ DEFAULTcast gls @@ -884,7 +887,7 @@ let build_per_info etype casee gls = try destInd hd with _ -> - error "Case analysis must be done on an inductive object" in + error "Case analysis must be done on an inductive object." in let mind,oind = Global.lookup_inductive ind in let nparams,index = match etype with @@ -955,7 +958,7 @@ let suppose_tac hyps gls0 = let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in let old_clauses,stack = register_nodep_subcase id info.pm_stack in let ninfo2 = {pm_stack=stack} in - tclTHENS (internal_cut id clause) + tclTHENS (assert_postpone id clause) [tclTHENLIST [tcl_change_info ninfo1; assume_tac hyps; clear old_clauses]; @@ -1042,7 +1045,7 @@ let rec add_branch ((id,_) as cpl) pats tree= | Split_patt (_,ind0,_) -> if (ind <> ind0) then error (* this can happen with coercions *) - "Case pattern belongs to wrong inductive type"; + "Case pattern belongs to wrong inductive type."; let mapi i ati bri = if i = pred cnum then let nargs = @@ -1083,12 +1086,12 @@ let thesis_for obj typ per_info env= 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 + 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 + 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) @@ -1161,7 +1164,7 @@ let case_tac params pat_info hyps gls0 = register_dep_subcase (id,List.length hyps) (pf_env gls0) per_info pat_info.pat_pat ek in let ninfo2 = {pm_stack=Per(et,per_info,nek,id::old_clauses)::rest} in - tclTHENS (internal_cut id clause) + tclTHENS (assert_postpone id clause) [tclTHENLIST [tcl_change_info ninfo1; assume_st (params@pat_info.pat_vars); diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 5dd7f5fd..14731b26 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dhyp.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: dhyp.ml 11309 2008-08-06 10:30:35Z herbelin $ *) (* Chet's comments about this tactic : @@ -246,7 +246,7 @@ let add_destructor_hint local na loc pat pri code = | ConclLocation _, _ -> (None, code) | _ -> errorlabstrm "add_destructor_hint" - (str "The tactic should be a function of the hypothesis name") end + (str "The tactic should be a function of the hypothesis name.") end in let (_,pat) = Constrintern.interp_constrpattern Evd.empty (Global.env()) pat in @@ -279,13 +279,13 @@ let match_dpat dp cls gls = (is_matching concld.d_typ cl) & (is_matching concld.d_sort (pf_type_of gls cl))) hl) - then error "No match" + then error "No match." | ({onhyps=Some[]},ConclLocation concld) when onconcl -> let cl = pf_concl gls in if not ((is_matching concld.d_typ cl) & (is_matching concld.d_sort (pf_type_of gls cl))) - then error "No match" + then error "No match." | _ -> error "ApplyDestructor" let forward_interp_tactic = @@ -304,8 +304,8 @@ let applyDestructor cls discard dd gls = ConstrMayEval(ConstrTerm (RRef(dummy_loc,VarRef id),None)) in TacLetIn (false, [(dummy_loc, x), arg], tac) | None, (None, tac) -> tac - | _, (Some _,_) -> error "Destructor expects an hypothesis" - | _, (None,_) -> error "Destructor is for conclusion") + | _, (Some _,_) -> error "Destructor expects an hypothesis." + | _, (None,_) -> error "Destructor is for conclusion.") cll in let discard_0 = List.map (fun cl -> diff --git a/tactics/dn.ml b/tactics/dn.ml index ab908ff9..2a8166dc 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -1,3 +1,4 @@ +(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* - None :: (path_of_deferred deferred) - | Some (lbl,[]) -> - (Some (lbl,0))::(path_of_deferred deferred) - | Some (lbl,(h::def_subl as v)) -> - (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) + | None -> + None :: (path_of_deferred deferred) + | Some (lbl,[]) -> + (Some (lbl,0))::(path_of_deferred deferred) + | Some (lbl,(h::def_subl as v)) -> + (Some (lbl,List.length v))::(pathrec (def_subl@deferred) h) in pathrec [] let tm_of tm lbl = - try [Tlm.map tm lbl] with Not_found -> [] - + try [Tlm.map tm lbl, true] with Not_found -> [] + +let rec skip_arg n tm = + if n = 0 then [tm,true] + else + List.flatten + (List.map + (fun a -> match a with + | None -> skip_arg (pred n) (Tlm.map tm a) + | Some (lbl,m) -> + skip_arg (pred n + m) (Tlm.map tm a)) + (Tlm.dom tm)) + let lookup tm dna t = let rec lookrec t tm = - (tm_of tm None)@ - (match dna t with - | None -> [] - | Some(lbl,v) -> - List.fold_left - (fun l c -> List.flatten(List.map (lookrec c) l)) - (tm_of tm (Some(lbl,List.length v))) v) + match dna t with + | Nothing -> tm_of tm None + | Label(lbl,v) -> + tm_of tm None@ + (List.fold_left + (fun l c -> + List.flatten(List.map (fun (tm, b) -> + if b then lookrec c tm + else [tm,b]) l)) + (tm_of tm (Some(lbl,List.length v))) v) + | Everything -> skip_arg 1 tm in - List.flatten(List.map Tlm.xtract (lookrec t tm)) + List.flatten (List.map (fun (tm,b) -> Tlm.xtract tm) (lookrec t tm)) let add tm dna (pat,inf) = let p = path_of dna pat in Tlm.add tm (p,(pat,inf)) diff --git a/tactics/dn.mli b/tactics/dn.mli index f8efd053..62e37a73 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: dn.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: dn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (* Discrimination nets. *) @@ -28,13 +28,19 @@ val add : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf val rmv : ('lbl,'pat,'inf) t -> ('lbl,'pat) decompose_fun -> 'pat * 'inf -> ('lbl,'pat,'inf) t +type 'res lookup_res = Label of 'res | Nothing | Everything + +type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res + (* [lookup t f tree] looks for trees (and their associated information) in table [t] such that the structured object [tree] matches against them; [f] is used to translated [tree] into its prefix decomposition: [f] must decompose any tree into a label characterizing its root node and the list of its subtree *) -val lookup : ('lbl,'pat,'inf) t -> ('lbl,'term) decompose_fun -> 'term +val lookup : ('lbl,'pat,'inf) t -> ('lbl,'term) lookup_fun -> 'term -> ('pat * 'inf) list val app : (('pat * 'inf) -> unit) -> ('lbl,'pat,'inf) t -> unit + +val skip_arg : int -> ('lbl,'pat,'inf) t -> (('lbl,'pat,'inf) t * bool) list diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 2effe103..1503ca9a 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: eauto.ml4 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: eauto.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -74,11 +74,11 @@ let prolog_tac l n gl = let n = match n with | ArgArg n -> n - | _ -> error "Prolog called with a non closed argument" + | _ -> error "Prolog called with a non closed argument." in try (prolog l n gl) with UserError ("Refiner.tclFIRST",_) -> - errorlabstrm "Prolog.prolog" (str "Prolog failed") + errorlabstrm "Prolog.prolog" (str "Prolog failed.") TACTIC EXTEND prolog | [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] @@ -111,7 +111,7 @@ let rec e_trivial_fail_db mod_delta db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db mod_delta db_list - (add_hint_list hintl local_db) g'))) :: + (Hint_db.add_list hintl local_db) g'))) :: (List.map fst (e_trivial_resolve mod_delta db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal @@ -124,10 +124,9 @@ and e_my_find_search_nodelta db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> Hint_db.map_all hdc db) (local_db::db_list) + list_map_append (Hint_db.map_all hdc) (local_db::db_list) else - list_map_append (fun (st, db) -> - Hint_db.map_auto (hdc,concl) db) (local_db::db_list) + list_map_append (Hint_db.map_auto (hdc,concl)) (local_db::db_list) in let tac_of_hint = fun {pri=b; pat = p; code=t} -> @@ -160,12 +159,12 @@ and e_my_find_search_delta db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> - let flags = {auto_unif_flags with modulo_delta = st} in + list_map_append (fun db -> + let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun (st, db) -> - let flags = {auto_unif_flags with modulo_delta = st} in + list_map_append (fun db -> + let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in let tac_of_hint = @@ -285,8 +284,7 @@ module SearchProblem = struct let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in - - let ldb = add_hint_list hintl (List.hd s.localdb) in + let ldb = Hint_db.add_list hintl (List.hd s.localdb) in { depth = s.depth; tacres = res; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb }) @@ -333,7 +331,7 @@ let e_depth_search debug p db_list local_db gl = let tac = if debug then Search.debug_depth_first else Search.depth_first in let s = tac (make_initial_state p gl db_list local_db) in s.tacres - with Not_found -> error "EAuto: depth first search failed" + with Not_found -> error "eauto: depth first search failed." let e_breadth_search debug n db_list local_db gl = try @@ -342,7 +340,7 @@ let e_breadth_search debug n db_list local_db gl = in let s = tac (make_initial_state n gl db_list local_db) in s.tacres - with Not_found -> error "EAuto: breadth first search failed" + with Not_found -> error "eauto: breadth first search failed." let e_search_auto debug (in_depth,p) lems db_list gl = let local_db = make_local_hint_db true lems gl in @@ -361,7 +359,7 @@ let eauto debug np lems dbnames = List.map (fun x -> try searchtable_map x - with Not_found -> error ("EAuto: "^x^": No such Hint database")) + with Not_found -> error ("No such Hint database: "^x^".")) ("core"::dbnames) in tclTRY (e_search_auto debug np lems db_list) @@ -379,12 +377,12 @@ let gen_eauto d np lems = function let make_depth = function | None -> !default_search_depth | Some (ArgArg d) -> d - | _ -> error "EAuto called with a non closed argument" + | _ -> error "eauto called with a non closed argument." let make_dimension n = function | None -> (true,make_depth n) | Some (ArgArg d) -> (false,d) - | _ -> error "EAuto called with a non closed argument" + | _ -> error "eauto called with a non closed argument." open Genarg @@ -452,7 +450,8 @@ let autosimpl db cl = else [] in let unfolds = List.concat (List.map (fun dbname -> - let ((ids, csts), _) = searchtable_map dbname in + let db = searchtable_map dbname in + let (ids, csts) = Hint_db.transparent_state db in unfold_of_elts (fun x -> EvalConstRef x) (Cpred.elements csts) @ unfold_of_elts (fun x -> EvalVarRef x) (Idpred.elements ids)) db) in unfold_option unfolds cl diff --git a/tactics/elim.ml b/tactics/elim.ml index 889ead5e..55df0f0a 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: elim.ml 9842 2007-05-20 17:44:23Z herbelin $ *) +(* $Id: elim.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -49,8 +49,8 @@ let introCaseAssumsThen tac ba = else (ba.branchnames, []), if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in - let introCaseAssums = tclTHEN (intros_pattern None l1) (intros_clearing l3) - in + let introCaseAssums = + tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the @@ -115,7 +115,7 @@ let inductive_of = function | IndRef ity -> ity | r -> errorlabstrm "Decompose" - (Printer.pr_global r ++ str " is not an inductive type") + (Printer.pr_global r ++ str " is not an inductive type.") let decompose_these c l gls = let indl = (*List.map inductive_of*) l in @@ -182,7 +182,7 @@ let double_ind h1 h2 gls = let (abs_i,abs_j) = if abs_i < abs_j then (abs_i,abs_j) else if abs_i > abs_j then (abs_j,abs_i) else - error "Both hypotheses are the same" in + error "Both hypotheses are the same." in (tclTHEN (tclDO abs_i intro) (onLastHyp (fun id -> diff --git a/tactics/elim.mli b/tactics/elim.mli index d01d3027..cbbf2f83 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: elim.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: elim.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Names @@ -23,7 +23,7 @@ val introElimAssumsThen : (branch_assumptions -> tactic) -> branch_args -> tactic val introCaseAssumsThen : - (intro_pattern_expr list -> branch_assumptions -> tactic) -> + (intro_pattern_expr Util.located list -> branch_assumptions -> tactic) -> branch_args -> tactic val general_decompose : (identifier * constr -> bool) -> constr -> tactic diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4 index 8e0b2ca3..41f85fa3 100644 --- a/tactics/eqdecide.ml4 +++ b/tactics/eqdecide.ml4 @@ -14,7 +14,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: eqdecide.ml4 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: eqdecide.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -152,14 +152,14 @@ let decideGralEquality g = let rectype = match kind_of_term headtyp with | Ind mi -> mi - | _ -> error "This decision procedure only works for inductive objects" + | _ -> error"This decision procedure only works for inductive objects." in (tclTHEN (mkBranches c1 c2) (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype))) g with PatternMatchingFailure -> - error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}" + error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}." let decideEqualityGoal = tclTHEN intros decideGralEquality diff --git a/tactics/equality.ml b/tactics/equality.ml index a475b392..7fb19423 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: equality.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -76,14 +76,9 @@ let elimination_sort_of_clause = function (* The next function decides in particular whether to try a regular rewrite or a setoid rewrite. - - Old approach was: - break everything, if [eq] appears in head position - then regular rewrite else try setoid rewrite - - New approach is: - if head position is a known setoid relation then setoid rewrite - else back to the old approach + Approach is to break everything, if [eq] appears in head position + then regular rewrite else try setoid rewrite. + If occurrences are set, use setoid_rewrite. *) let general_s_rewrite_clause = function @@ -93,45 +88,55 @@ let general_s_rewrite_clause = function let general_setoid_rewrite_clause = ref general_s_rewrite_clause let register_general_setoid_rewrite_clause = (:=) general_setoid_rewrite_clause +let is_applied_setoid_relation = ref (fun _ -> false) +let register_is_applied_setoid_relation = (:=) is_applied_setoid_relation + +let is_applied_relation t = + match kind_of_term t with + | App (c, args) when Array.length args >= 2 -> true + | _ -> false + +let leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl 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 with_evars cls (c,l) (elim,NoBindings) gl + +let leibniz_eq = Lazy.lazy_from_fun build_coq_eq + let general_rewrite_ebindings_clause cls lft2rgt occs (c,l) with_evars gl = - 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_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] 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 ctype in - match match_with_equation t with - | None -> - if l = NoBindings - then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl - else error "The term provided does not end with an equation" - | Some (hdcncl,_) -> - if occs <> all_occurrences then ( - !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl) - else - 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 - try general_elim_clause with_evars cls (c,l) (elim,NoBindings) gl - with e -> - let eq = build_coq_eq () in - if not (eq_constr eq head) then - try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl - with _ -> raise e - else raise e - + if occs <> all_occurrences then ( + !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl) + else + let ctype = pf_apply get_type_of gl c in + let env = pf_env gl in + let sigma = project gl in + let rels, t = decompose_prod (whd_betaiotazeta ctype) in + match match_with_equation t with + | Some (hdcncl,_) -> (* Fast path: direct leibniz rewrite *) + leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl + | None -> + let env' = List.fold_left (fun env (n,t) -> push_rel (n, None, t) env) env rels in + let _,t' = splay_prod env' sigma t in (* Search for underlying eq *) + match match_with_equation t' with + | Some (hdcncl,_) -> (* Maybe a setoid relation with eq inside *) + if l = NoBindings && !is_applied_setoid_relation t then + !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + else + (try leibniz_rewrite_ebindings_clause cls lft2rgt (c,l) with_evars gl hdcncl + with e -> + try !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + with _ -> raise e) + | None -> (* Can't be leibniz, try setoid *) + if l = NoBindings + then !general_setoid_rewrite_clause cls lft2rgt occs c ~new_goals:[] gl + else error "The term provided does not end with an equation." + let general_rewrite_ebindings = general_rewrite_ebindings_clause None let general_rewrite_bindings l2r occs (c,bl) = @@ -269,7 +274,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = ] ] gl else - error "terms do not have convertible types" + error "Terms do not have convertible types." let replace c2 c1 gl = multi_replace onConcl c2 c1 false None gl @@ -494,7 +499,7 @@ let construct_discriminator sigma env dirn c sort = *) errorlabstrm "Equality.construct_discriminator" (str "Cannot discriminate on inductive constructors with - dependent types") in + dependent types.") in let (ind,_) = dest_ind_family indf in let (mib,mip) = lookup_mind_specif env ind in let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in @@ -534,7 +539,7 @@ let gen_absurdity id gl = simplest_elim (mkVar id) gl else errorlabstrm "Equality.gen_absurdity" - (str "Not the negation of an equality") + (str "Not the negation of an equality.") (* Precondition: eq is leibniz equality @@ -559,7 +564,7 @@ let apply_on_clause (f,t) clause = let argmv = (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> errorlabstrm "" (str "Ill-formed clause applicator")) in + | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in clenv_fchain argmv f_clause clause let discr_positions env sigma (lbeq,(t,t1,t2)) eq_clause cpath dirn sort = @@ -580,7 +585,7 @@ let discrEq (lbeq,(t,t1,t2) as u) eq_clause gls = let env = pf_env gls in match find_positions env sigma t1 t2 with | Inr _ -> - errorlabstrm "discr" (str"Not a discriminable equality") + 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 eq_clause cpath dirn sort gls @@ -594,7 +599,7 @@ let onEquality with_evars tac (c,lbindc) gls = let eq = try find_eq_data_decompose eqn with PatternMatchingFailure -> - errorlabstrm "" (str"No primitive equality found") in + errorlabstrm "" (str"No primitive equality found.") in tclTHEN (Refiner.tclEVARS (Evd.evars_of eq_clause'.evd)) (tac eq eq_clause') gls @@ -607,7 +612,7 @@ let onNegatedEquality with_evars tac gls = (onLastHyp (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) gls | _ -> - errorlabstrm "" (str "Not a negated primitive equality") + errorlabstrm "" (str "Not a negated primitive equality.") let discrSimpleClause with_evars = function | None -> onNegatedEquality with_evars discrEq @@ -622,7 +627,7 @@ let discrEverywhere with_evars = (Tacticals.tryAllClauses (fun cl -> tclCOMPLETE (discrSimpleClause with_evars cl))) (fun gls -> - errorlabstrm "DiscrEverywhere" (str"No discriminable equalities")) + errorlabstrm "DiscrEverywhere" (str"No discriminable equalities.")) let discr_tac with_evars = function | None -> discrEverywhere with_evars @@ -723,7 +728,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (* the_conv_x had a side-effect on evdref *) dflt else - error "Cannot solve an unification problem" + error "Cannot solve an unification problem." else let (a,p_i_minus_1) = match whd_beta_stack p_i with | (_sigS,[a;p]) -> (a,p) @@ -865,7 +870,7 @@ let inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns = (pf,ty)) posns in if injectors = [] then - errorlabstrm "Equality.inj" (str "Failed to decompose the equality"); + errorlabstrm "Equality.inj" (str "Failed to decompose the equality."); tclMAP (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf]) injectors @@ -879,10 +884,10 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause = match find_positions env sigma t1 t2 with | Inl _ -> errorlabstrm "Inj" - (str"Not a projectable equality but a discriminable one") + (str"Not a projectable equality but a discriminable one.") | Inr [] -> errorlabstrm "Equality.inj" - (str"Nothing to do, it is an equality between convertible terms") + (str"Nothing to do, it is an equality between convertible terms.") | Inr posns -> (* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ? let t1 = try_delta_expand env sigma t1 in @@ -923,7 +928,7 @@ let injEq ipats (eq,(t,t1,t2)) eq_clause = ) with _ -> tclTHEN (inject_at_positions env sigma (eq,(t,t1,t2)) eq_clause posns) - (intros_pattern None ipats) + (intros_pattern no_move ipats) let inj ipats with_evars = onEquality with_evars (injEq ipats) @@ -986,7 +991,7 @@ let find_elim sort_of_gl lbeq = (match lbeq.rect with | Some eq_rect -> eq_rect | None -> errorlabstrm "find_elim" - (str "this type of substitution is not allowed")) + (str "This type of substitution is not allowed.")) (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *) @@ -1086,11 +1091,10 @@ let try_rewrite tac gls = tac gls with | PatternMatchingFailure -> - errorlabstrm "try_rewrite" (str "Not a primitive equality here") + errorlabstrm "try_rewrite" (str "Not a primitive equality here.") | e when catchable_exception e -> errorlabstrm "try_rewrite" - (str "Cannot find a well-typed generalization of the goal that" ++ - str " makes the proof progress") + (strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.") let cutSubstClause l2r eqn cls gls = match cls with @@ -1145,7 +1149,7 @@ let unfold_body x gl = match Sign.lookup_named x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis") in + (pr_id x ++ str" is not a defined hypothesis.") in let aft = afterHyp x gl in let hl = List.fold_right (fun (y,yval,_) cl -> ((all_occurrences_expr,y),InHyp) :: cl) aft [] in @@ -1182,7 +1186,8 @@ let subst_one x gl = let test hyp _ = is_eq_x varx hyp in Sign.fold_named_context test ~init:() hyps; errorlabstrm "Subst" - (str "cannot find any non-recursive equality over " ++ pr_id x) + (str "Cannot find any non-recursive equality over " ++ pr_id x ++ + str".") with FoundHyp res -> res in (* The set of hypotheses using x *) @@ -1263,7 +1268,7 @@ let cond_eq_term c t gl = let rewrite_multi_assumption_cond cond_eq_term cl gl = let rec arec = function - | [] -> error "No such assumption" + | [] -> error "No such assumption." | (id,_,t) ::rest -> begin try @@ -1286,7 +1291,7 @@ let replace_multi_term dir_opt c = (* JF. old version let rewrite_assumption_cond faildir gl = let rec arec = function - | [] -> error "No such assumption" + | [] -> error "No such assumption." | (id,_,t)::rest -> (try let dir = faildir t gl in general_rewrite dir (mkVar id) gl @@ -1296,7 +1301,7 @@ let rewrite_assumption_cond faildir gl = let rewrite_assumption_cond_in faildir hyp gl = let rec arec = function - | [] -> error "No such assumption" + | [] -> error "No such assumption." | (id,_,t)::rest -> (try let dir = faildir t gl in general_rewrite_in dir hyp (mkVar id) gl diff --git a/tactics/equality.mli b/tactics/equality.mli index 42c502be..f05ebc6c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: equality.mli 11166 2008-06-22 13:23:35Z herbelin $ i*) +(*i $Id: equality.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) +open Util open Names open Term open Sign @@ -45,6 +46,7 @@ val rewriteRL : constr -> tactic val register_general_setoid_rewrite_clause : (identifier option -> bool -> occurrences -> constr -> new_goals:constr list -> tactic) -> unit +val register_is_applied_setoid_relation : (constr -> bool) -> unit val general_rewrite_bindings_in : bool -> occurrences -> identifier -> constr with_bindings -> evars_flag -> tactic @@ -74,9 +76,9 @@ val discrHyp : identifier -> tactic val discrEverywhere : evars_flag -> tactic val discr_tac : evars_flag -> constr with_ebindings induction_arg option -> tactic -val inj : intro_pattern_expr list -> evars_flag -> +val inj : intro_pattern_expr located list -> evars_flag -> constr with_ebindings -> tactic -val injClause : intro_pattern_expr list -> evars_flag -> +val injClause : intro_pattern_expr located list -> evars_flag -> constr with_ebindings induction_arg option -> tactic val injHyp : identifier -> tactic val injConcl : tactic diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index b4a39a24..3c266c51 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 11072 2008-06-08 16:13:37Z herbelin $ *) +(* $Id: evar_tactics.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Term open Util @@ -41,16 +41,16 @@ let instantiate n rawc ido gl = (match decl with (_,None,typ) -> evar_list sigma typ | _ -> error - "please be more specific : in type or value ?") + "Please be more specific: in type or value?") | InHypTypeOnly -> let (_, _, typ) = decl in evar_list sigma typ | InHypValueOnly -> (match decl with (_,Some body,_) -> evar_list sigma body - | _ -> error "not a let .. in hypothesis") in + | _ -> error "Not a defined hypothesis.") in if List.length evl < n then error "not enough uninstantiated existential variables"; - if n <= 0 then error "incorrect existential variable index"; + if n <= 0 then error "Incorrect existential variable index."; let ev,_ = destEvar (List.nth evl (n-1)) in let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in tclTHEN diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 885138e4..66716acd 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: extratactics.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Pcoq @@ -486,21 +486,29 @@ END TACTIC EXTEND apply_in -| ["apply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in false id [c] ] -| ["apply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") - "in" hyp(id) ] -> [ apply_in false id (c::cl) ] +| ["apply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> + [ apply_in false id cl ] END TACTIC EXTEND eapply_in -| ["eapply" constr_with_bindings(c) "in" hyp(id) ] -> [ apply_in true id [c] ] -| ["epply" constr_with_bindings(c) "," constr_with_bindings_list_sep(cl,",") - "in" hyp(id) ] -> [ apply_in true id (c::cl) ] +| ["eapply" ne_constr_with_bindings_list_sep(cl,",") "in" hyp(id) ] -> + [ apply_in true id cl ] END (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as defined by Conor McBride *) TACTIC EXTEND generalize_eqs -| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ] +| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:false ] +END +TACTIC EXTEND generalize_eqs_vars +| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize id ~generalize_vars:true ] +END + +TACTIC EXTEND conv +| ["conv" constr(x) constr(y) ] -> [ conv x y ] END +TACTIC EXTEND resolve_classes +| ["resolve_classes" ] -> [ resolve_classes ] +END diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 190a7ba2..31c1b02f 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: hiddentac.ml 11094 2008-06-10 19:35:23Z herbelin $ *) +(* $Id: hiddentac.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Term open Proof_type @@ -30,8 +30,8 @@ let inj_occ (occ,c) = (occ,inj_open c) (* Basic tactics *) let h_intro_move x y = - abstract_tactic (TacIntroMove (x, Option.map inj_id y)) (intro_move x y) -let h_intro x = h_intro_move (Some x) None + abstract_tactic (TacIntroMove (x, y)) (intro_move x y) +let h_intro x = h_intro_move (Some x) no_move let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption let h_exact c = abstract_tactic (TacExact (inj_open c)) (exact_check c) @@ -40,7 +40,7 @@ let h_exact_no_check c = let h_vm_cast_no_check c = abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) let h_apply simple ev cb = - abstract_tactic (TacApply (simple,ev,inj_open_wb cb)) + abstract_tactic (TacApply (simple,ev,List.map inj_open_wb cb)) (apply_with_ebindings_gen simple ev cb) let h_elim ev cb cbo = abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) @@ -70,7 +70,7 @@ let h_generalize cl = let h_generalize_dep c = abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) let h_let_tac b na c cl = - let with_eq = if b then None else Some true in + let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c cl) let h_instantiate n c ido = (Evar_tactics.instantiate n c ido) @@ -78,16 +78,19 @@ let h_instantiate n c ido = (Evar_refiner.instantiate n c (simple_clause_of cls)) *) (* Derived basic tactics *) -let h_simple_induction h = - abstract_tactic (TacSimpleInduction h) (simple_induct h) -let h_simple_destruct h = - abstract_tactic (TacSimpleDestruct h) (simple_destruct h) -let h_new_induction ev c e idl cl = - abstract_tactic (TacNewInduction (ev,List.map inj_ia c,Option.map inj_open_wb e,idl,cl)) - (new_induct ev c e idl cl) -let h_new_destruct ev c e idl cl = - abstract_tactic (TacNewDestruct (ev,List.map inj_ia c,Option.map inj_open_wb e,idl,cl)) - (new_destruct ev c e idl cl) +let h_simple_induction_destruct isrec h = + abstract_tactic (TacSimpleInductionDestruct (isrec,h)) + (if isrec then (simple_induct h) else (simple_destruct h)) +let h_simple_induction = h_simple_induction_destruct true +let h_simple_destruct = h_simple_induction_destruct false + +let h_induction_destruct isrec ev l = + abstract_tactic (TacInductionDestruct (isrec,ev,List.map (fun (c,e,idl,cl) -> + List.map inj_ia c,Option.map inj_open_wb e,idl,cl) l)) + (induction_destruct ev isrec l) +let h_new_induction ev c e idl cl = h_induction_destruct ev true [c,e,idl,cl] +let h_new_destruct ev c e idl cl = h_induction_destruct ev false [c,e,idl,cl] + let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) @@ -128,8 +131,8 @@ let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) let h_transitivity c = abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c) -let h_simplest_apply c = h_apply false false (c,NoBindings) -let h_simplest_eapply c = h_apply false true (c,NoBindings) +let h_simplest_apply c = h_apply false false [c,NoBindings] +let h_simplest_eapply c = h_apply false true [c,NoBindings] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index eed3b1da..3e636668 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: hiddentac.mli 11072 2008-06-08 16:13:37Z herbelin $ i*) +(*i $Id: hiddentac.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Names +open Util open Term open Proof_type open Tacmach @@ -25,7 +26,7 @@ open Clenv (* Basic tactics *) -val h_intro_move : identifier option -> identifier option -> tactic +val h_intro_move : identifier option -> identifier move_location -> tactic val h_intro : identifier -> tactic val h_intros_until : quantified_hypothesis -> tactic @@ -35,7 +36,7 @@ val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> - constr with_ebindings -> tactic + constr with_ebindings list -> tactic val h_elim : evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic @@ -63,14 +64,20 @@ val h_instantiate : int -> Rawterm.rawconstr -> val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic -val h_new_induction : - evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> - Tacticals.clause option -> tactic -val h_new_destruct : - evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> - Tacticals.clause option -> tactic +val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic +val h_new_induction : evars_flag -> + constr with_ebindings induction_arg list -> constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + Tacticals.clause option -> tactic +val h_new_destruct : evars_flag -> + constr with_ebindings induction_arg list -> constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + Tacticals.clause option -> tactic +val h_induction_destruct : rec_flag -> evars_flag -> + (constr with_ebindings induction_arg list * constr with_ebindings option * + (intro_pattern_expr located option * intro_pattern_expr located option) * + Tacticals.clause option) list -> tactic + val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic @@ -80,7 +87,7 @@ val h_lapply : constr -> tactic (* Context management *) val h_clear : bool -> identifier list -> tactic val h_clear_body : identifier list -> tactic -val h_move : bool -> identifier -> identifier -> tactic +val h_move : bool -> identifier -> identifier move_location -> tactic val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic @@ -110,4 +117,4 @@ val h_simplest_eapply : constr -> tactic val h_simplest_elim : constr -> tactic val h_simplest_case : constr -> tactic -val h_intro_patterns : intro_pattern_expr list -> tactic +val h_intro_patterns : intro_pattern_expr located list -> tactic diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index fca84fd2..de500f89 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) -(* $Id: hipattern.ml4 8866 2006-05-28 16:21:04Z herbelin $ *) +(* $Id: hipattern.ml4 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -273,7 +273,7 @@ let dest_nf_eq gls eqn = try snd (first_match (match_eq_nf gls eqn) equalities) with PatternMatchingFailure -> - error "Not an equality" + error "Not an equality." (*** Sigma-types *) diff --git a/tactics/inv.ml b/tactics/inv.ml index 8bd10a4d..68ebfd3c 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inv.ml 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: inv.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -101,7 +101,7 @@ let make_inv_predicate env sigma indf realargs id status concl = | Dep dflt_concl -> if not (occur_var env id concl) then errorlabstrm "make_inv_predicate" - (str "Current goal does not depend on " ++ pr_id id); + (str "Current goal does not depend on " ++ pr_id id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have c also rewritten when the case * will be done *) @@ -291,10 +291,10 @@ let generalizeRewriteIntros tac depids id gls = let rec tclMAP_i n tacfun = function | [] -> tclDO n (tacfun None) | a::l -> - if n=0 then error "Too much names" + if n=0 then error "Too much names." else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) -let remember_first_eq id x = if !x = None then x := Some id +let remember_first_eq id x = if !x = no_move then x := MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -321,7 +321,7 @@ let projectAndApply thin id eqname names depids gls = [(if names <> [] then clear [id] else tclIDTAC); (tclMAP_i neqns (fun idopt -> tclTHEN - (intro_move idopt None) + (intro_move idopt no_move) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHyp (substHypIfVariable (subst_hyp false))))) @@ -350,7 +350,7 @@ let rewrite_equations_gene othin neqns ba gl = (onLastHyp (fun id -> tclTRY - (projectAndApply thin id (ref None) + (projectAndApply thin id (ref no_move) [] depids)))); onHyps (compose List.rev (afterHyp last)) bring_hyps; onHyps (afterHyp last) @@ -375,24 +375,24 @@ let rewrite_equations_gene othin neqns ba gl = None: the equations are introduced, but not rewritten Some thin: the equations are rewritten, and cleared if thin is true *) -let rec get_names allow_conj = function +let rec get_names allow_conj (loc,pat) = match pat with | IntroWildcard -> - error "Discarding pattern not allowed for inversion equations" + error "Discarding pattern not allowed for inversion equations." | IntroAnonymous -> - error "Anonymous pattern not allowed for inversion equations" - | IntroFresh _-> - error "Fresh pattern not allowed for inversion equations" + error "Anonymous pattern not allowed for inversion equations." + | IntroFresh _ -> + error "Fresh pattern not allowed for inversion equations." | IntroRewrite _-> - error "Rewriting pattern not allowed for inversion equations" + error "Rewriting pattern not allowed for inversion equations." | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else let l = List.map (fun id -> Option.get (fst (get_names false id))) l in (Some (List.hd l), l) else - error "Nested conjunctive patterns not allowed for inversion equations" + error"Nested conjunctive patterns not allowed for inversion equations." | IntroOrAndPattern l -> - error "Disjunctive patterns not allowed for inversion equations" + error "Disjunctive patterns not allowed for inversion equations." | IntroIdentifier id -> (Some id,[id]) @@ -404,7 +404,7 @@ let rewrite_equations othin neqns names ba gl = let names = List.map (get_names true) names in let (depids,nodepids) = split_dep_and_nodep ba.assums gl in let rewrite_eqns = - let first_eq = ref None in + let first_eq = ref no_move in match othin with | Some thin -> tclTHENSEQ @@ -413,12 +413,12 @@ let rewrite_equations othin neqns names ba gl = tclMAP_i neqns (fun o -> let idopt,names = extract_eqn_names o in (tclTHEN - (intro_move idopt None) + (intro_move idopt no_move) (onLastHyp (fun id -> tclTRY (projectAndApply thin id first_eq names depids))))) names; tclMAP (fun (id,_,_) gl -> - intro_move None (if thin then None else !first_eq) gl) + intro_move None (if thin then no_move else !first_eq) gl) nodepids; tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] | None -> tclIDTAC @@ -453,7 +453,7 @@ let raw_inversion inv_kind id status names gl = try pf_reduce_to_atomic_ind gl (pf_type_of gl c) with UserError _ -> errorlabstrm "raw_inversion" - (str ("The type of "^(string_of_id id)^" is not inductive")) in + (str ("The type of "^(string_of_id id)^" is not inductive.")) in let indclause = mk_clenv_from gl (c,t) in let ccl = clenv_type indclause in check_no_metas indclause ccl; @@ -494,7 +494,7 @@ let not_found_message ids = let dep_prop_prop_message id = errorlabstrm "Inv" (str "Inversion on " ++ pr_id id ++ - str " would needs dependent elimination Prop-Prop") + str " would need dependent elimination from Prop to Prop.") let not_inductive_here id = errorlabstrm "mind_specif_of_mind" @@ -524,15 +524,15 @@ open Tacexpr let inv k = inv_gen false k NoDep -let half_inv_tac id = inv SimpleInversion IntroAnonymous (NamedHyp id) -let inv_tac id = inv FullInversion IntroAnonymous (NamedHyp id) -let inv_clear_tac id = inv FullInversionClear IntroAnonymous (NamedHyp id) +let half_inv_tac id = inv SimpleInversion None (NamedHyp id) +let inv_tac id = inv FullInversion None (NamedHyp id) +let inv_clear_tac id = inv FullInversionClear None (NamedHyp id) let dinv k c = inv_gen false k (Dep c) -let half_dinv_tac id = dinv SimpleInversion None IntroAnonymous (NamedHyp id) -let dinv_tac id = dinv FullInversion None IntroAnonymous (NamedHyp id) -let dinv_clear_tac id = dinv FullInversionClear None IntroAnonymous (NamedHyp id) +let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id) +let dinv_tac id = dinv FullInversion None None (NamedHyp id) +let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) (* InvIn will bring the specified clauses into the conclusion, and then * perform inversion on the named hypothesis. After, it will intro them diff --git a/tactics/inv.mli b/tactics/inv.mli index bd38d08f..bbb2a322 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inv.mli 7880 2006-01-16 13:59:08Z herbelin $ i*) +(*i $Id: inv.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) +open Util open Names open Term open Tacmach @@ -21,20 +22,20 @@ type inversion_status = Dep of constr option | NoDep val inv_gen : bool -> inversion_kind -> inversion_status -> - intro_pattern_expr -> quantified_hypothesis -> tactic + intro_pattern_expr located option -> quantified_hypothesis -> tactic val invIn_gen : - inversion_kind -> intro_pattern_expr -> identifier list -> + inversion_kind -> intro_pattern_expr located option -> identifier list -> quantified_hypothesis -> tactic val inv_clause : - inversion_kind -> intro_pattern_expr -> identifier list -> + inversion_kind -> intro_pattern_expr located option -> identifier list -> quantified_hypothesis -> tactic -val inv : inversion_kind -> intro_pattern_expr -> +val inv : inversion_kind -> intro_pattern_expr located option -> quantified_hypothesis -> tactic -val dinv : inversion_kind -> constr option -> intro_pattern_expr -> - quantified_hypothesis -> tactic +val dinv : inversion_kind -> constr option -> + intro_pattern_expr located option -> quantified_hypothesis -> tactic val half_inv_tac : identifier -> tactic val inv_tac : identifier -> tactic diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 70e8c375..5acc5197 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: leminv.ml 10348 2007-12-06 17:36:14Z aspiwack $ *) +(* $Id: leminv.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -214,7 +214,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = (ids_of_named_context (named_context invEnv))); (* errorlabstrm "lemma_inversion" - (str"Computed inversion goal was not closed in initial signature"); + (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 None) in @@ -272,7 +272,7 @@ let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op = errorlabstrm "lemma_inversion" (str"Cannot compute lemma inversion when there are" ++ spc () ++ str"free variables in the types of an inductive" ++ spc () ++ - str"which are not free in its instance"); *) + str"which are not free in its instance."); *) add_inversion_lemma na env sigma t sort dep_option inv_op let add_inversion_lemma_exn na com comsort bool tac = diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index d9d0a799..b94ae2dd 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: nbtermdn.ml 10346 2007-12-05 21:11:19Z aspiwack $ *) +(* $Id: nbtermdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -46,14 +46,14 @@ let add dn (na,(pat,valu)) = let hkey = Option.map fst (Termdn.constr_pat_discr pat) in dn.table <- Gmap.add na (pat,valu) dn.table; let dnm = dn.patterns in - dn.patterns <- Gmap.add hkey (Btermdn.add (get_dn dnm hkey) (pat,valu)) dnm + dn.patterns <- Gmap.add hkey (Btermdn.add None (get_dn dnm hkey) (pat,valu)) dnm let rmv dn na = let (pat,valu) = Gmap.find na dn.table in let hkey = Option.map fst (Termdn.constr_pat_discr pat) in dn.table <- Gmap.remove na dn.table; let dnm = dn.patterns in - dn.patterns <- Gmap.add hkey (Btermdn.rmv (get_dn dnm hkey) (pat,valu)) dnm + dn.patterns <- Gmap.add hkey (Btermdn.rmv None (get_dn dnm hkey) (pat,valu)) dnm let in_dn dn na = Gmap.mem na dn.table @@ -62,8 +62,12 @@ let remap ndn na (pat,valu) = add ndn (na,(pat,valu)) let lookup dn valu = - let hkey = Option.map fst (Termdn.constr_val_discr valu) in - try Btermdn.lookup (Gmap.find hkey dn.patterns) valu with Not_found -> [] + let hkey = + match (Termdn.constr_val_discr valu) with + | Dn.Label(l,_) -> Some l + | _ -> None + in + try Btermdn.lookup None (Gmap.find hkey dn.patterns) valu with Not_found -> [] let app f dn = Gmap.iter f dn.table diff --git a/tactics/refine.ml b/tactics/refine.ml index 84e9dccc..7ed58f6f 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refine.ml 9841 2007-05-19 21:13:42Z herbelin $ *) +(* $Id: refine.ml 11309 2008-08-06 10:30:35Z herbelin $ *) (* JCF -- 6 janvier 1998 EXPERIMENTAL *) @@ -229,7 +229,7 @@ let rec compute_metamap env sigma c = match kind_of_term c with (* Produit. Est-ce bien exact ? *) | Prod (_,_,_) -> if occur_meta c then - error "Refine: proof term contains metas in a product" + error "refine: proof term contains metas in a product." else TH (c,[],[]) @@ -330,7 +330,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | Fix ((ni,_),(fi,ai,_)) , _ -> let out_name = function | Name id -> id - | _ -> error "recursive functions must have names !" + | _ -> error "Recursive functions must have names." in let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in tclTHENS @@ -345,7 +345,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | CoFix (_,(fi,ai,_)) , _ -> let out_name = function | Name id -> id - | _ -> error "recursive functions must have names !" + | _ -> error "Recursive functions must have names." in let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in tclTHENS diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f4547930..3f8eb0ca 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacinterp.ml 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: tacinterp.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Constrintern open Closure @@ -51,13 +51,13 @@ open Pcoq let safe_msgnl s = try msgnl s with e -> msgnl - (str "bug in the debugger : " ++ + (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", - str "Syntactic metavariables allowed only in quotations") + str "Syntactic metavariables allowed only in quotations.") let error_global_not_found_loc (loc,qid) = error_global_not_found_loc loc qid @@ -72,10 +72,10 @@ type ltac_type = (* Values for interpretation *) type value = - | VTactic of loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *) | VRTactic of (goal list sigma * validation) (* For Match results *) (* Not a true value *) - | VFun of (identifier*value) list * identifier option list * glob_tactic_expr + | VFun of ltac_trace * (identifier*value) list * + identifier option list * glob_tactic_expr | VVoid | VInteger of int | VIntroPattern of intro_pattern_expr (* includes idents which are not *) @@ -86,20 +86,20 @@ type value = | VList of value list | VRec of (identifier*value) list ref * glob_tactic_expr -let locate_tactic_call loc = function - | VTactic (_,t) -> VTactic (loc,t) - | v -> v - -let locate_error_in_file dir = function - | Stdpp.Exc_located (loc,e) -> Error_in_file ("",(true,dir,loc),e) - | e -> Error_in_file ("",(true,dir,dummy_loc),e) +let dloc = dummy_loc -let catch_error loc tac g = - try tac g - with e when loc <> dummy_loc -> - match e with - | Stdpp.Exc_located (_,e) -> raise (Stdpp.Exc_located (loc,e)) - | e -> raise (Stdpp.Exc_located (loc,e)) +let catch_error call_trace tac g = + if call_trace = [] then tac g else try tac g with + | LtacLocated _ as e -> raise e + | Stdpp.Exc_located (_,LtacLocated _) as e -> raise e + | e -> + let (loc',c),tail = list_sep_last call_trace in + let loc,e' = match e with Stdpp.Exc_located(loc,e) -> loc,e | _ ->dloc,e in + if tail = [] then + let loc = if loc' = dloc then loc else loc' in + raise (Stdpp.Exc_located(loc,e')) + else + raise (Stdpp.Exc_located(loc',LtacLocated((c,tail,loc),e'))) (* Signature for interpretation: val_interp and interpretation functions *) type interp_sign = @@ -107,11 +107,11 @@ type interp_sign = avoid_ids : identifier list; (* ids inherited from the call context (needed to get fresh ids) *) debug : debug_info; - last_loc : loc } + trace : ltac_trace } let check_is_value = function | VRTactic _ -> (* These are goals produced by Match *) - error "Immediate match producing tactics not allowed in local definitions" + error "Immediate match producing tactics not allowed in local definitions." | _ -> () (* For tactic_of_value *) @@ -121,16 +121,16 @@ exception NotTactic let constr_of_VConstr_context = function | VConstr_context c -> c | _ -> - errorlabstrm "constr_of_VConstr_context" (str "not a context variable") + errorlabstrm "constr_of_VConstr_context" (str "Not a context variable.") (* Displays a value *) let rec pr_value env = function | VVoid -> str "()" | VInteger n -> int n - | VIntroPattern ipat -> pr_intro_pattern ipat + | VIntroPattern ipat -> pr_intro_pattern (dloc,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" + | (VRTactic _ | VFun _ | VRec _) -> str "a tactic" | VList [] -> str "an empty list" | VList (a::_) -> str "a list (first element is " ++ pr_value env a ++ str")" @@ -143,24 +143,13 @@ let constr_of_id env id = construct_reference (Environ.named_context env) id (* To embed tactics *) -let ((tactic_in : (interp_sign -> raw_tactic_expr) -> Dyn.t), - (tactic_out : Dyn.t -> (interp_sign -> raw_tactic_expr))) = +let ((tactic_in : (interp_sign -> glob_tactic_expr) -> Dyn.t), + (tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr))) = create "tactic" let ((value_in : value -> Dyn.t), (value_out : Dyn.t -> value)) = create "value" -let tacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) -let tacticOut = function - | TacArg (TacDynamic (_,d)) -> - if (tag d) = "tactic" then - tactic_out d - else - anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") - | ast -> - anomalylabstrm "tacticOut" - (str "Not a Dynamic ast: " (* ++ print_ast ast*) ) - let valueIn t = TacDynamic (dummy_loc,value_in t) let valueOut = function | TacDynamic (_,d) -> @@ -182,8 +171,6 @@ let constrOut = function | ast -> anomalylabstrm "constrOut" (str "Not a Dynamic ast") -let dloc = dummy_loc - (* Globalizes the identifier *) let find_reference env qid = (* We first look for a variable of the current proof *) @@ -195,7 +182,7 @@ let find_reference env qid = let error_not_evaluable s = errorlabstrm "evalref_of_ref" (str "Cannot coerce" ++ spc () ++ s ++ spc () ++ - str "to an evaluable reference") + str "to an evaluable reference.") (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) let atomic_mactab = ref Idmap.empty @@ -211,7 +198,7 @@ let _ = "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); "compute", TacReduce(Cbv all_flags,nocl); - "intro", TacIntroMove(None,None); + "intro", TacIntroMove(None,no_move); "intros", TacIntroPattern []; "assumption", TacAssumption; "cofix", TacCofix None; @@ -263,7 +250,7 @@ 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)); + (str ("Cannot redeclare tactic "^s^".")); Hashtbl.add tac_tab s t let overwriting_add_tactic s t = @@ -278,7 +265,7 @@ let lookup_tactic s = Hashtbl.find tac_tab s with Not_found -> errorlabstrm "Refiner.lookup_tactic" - (str"The tactic " ++ str s ++ str" is not installed") + (str"The tactic " ++ str s ++ str" is not installed.") (* let vernac_tactic (s,args) = let tacfun = lookup_tactic s args in @@ -311,11 +298,17 @@ let lookup_genarg_glob id = let (f,_,_) = lookup_genarg id in f let lookup_interp_genarg id = let (_,f,_) = lookup_genarg id in f let lookup_genarg_subst id = let (_,_,f) = lookup_genarg id in f -(* Dynamically check that an argument is a tactic, possibly unboxing VRec *) +let propagate_trace ist loc id = function + | VFun (_,lfun,it,b) -> + let t = if it=[] then b else TacFun (it,b) in + VFun ((loc,LtacVarCall (id,t))::ist.trace,lfun,it,b) + | x -> x + +(* Dynamically check that an argument is a tactic *) let coerce_to_tactic loc id = function - | VTactic _ | VFun _ | VRTactic _ as a -> a + | VFun _ | VRTactic _ as a -> a | _ -> user_err_loc - (loc, "", str "variable " ++ pr_id id ++ str " should be bound to a tactic") + (loc, "", str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") (*****************) (* Globalization *) @@ -422,6 +415,11 @@ let intern_constr_reference strict ist = function let loc,_ as lqid = qualid_of_reference r in RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r) +let intern_move_location ist = function + | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id) + | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id) + | MoveToEnd toleft as x -> x + (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = @@ -432,7 +430,7 @@ let intern_isolated_global_tactic_reference r = | Ident (_,id) -> Tacexp (lookup_atomic id) | _ -> raise Not_found -let intern_isolated_tactic_reference ist r = +let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) try Reference (intern_ltac_variable ist r) with Not_found -> @@ -440,7 +438,7 @@ let intern_isolated_tactic_reference ist r = try intern_isolated_global_tactic_reference r with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference true ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) with Not_found -> (* Reference not found *) error_global_not_found_loc (qualid_of_reference r) @@ -475,7 +473,7 @@ let intern_non_tactic_reference strict ist r = with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) match r with - | Ident (_,id) when not strict -> IntroPattern (IntroIdentifier id) + | Ident (loc,id) when not strict -> IntroPattern (loc,IntroIdentifier id) | _ -> (* Reference not found *) error_global_not_found_loc (qualid_of_reference r) @@ -487,13 +485,14 @@ let intern_message_token ist = function let intern_message ist = List.map (intern_message_token ist) let rec intern_intro_pattern lf ist = function - | IntroOrAndPattern l -> - IntroOrAndPattern (intern_case_intro_pattern lf ist l) - | IntroIdentifier id -> - IntroIdentifier (intern_ident lf ist id) - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x - -and intern_case_intro_pattern lf ist = + | loc, IntroOrAndPattern l -> + loc, IntroOrAndPattern (intern_or_and_intro_pattern lf ist l) + | loc, IntroIdentifier id -> + loc, IntroIdentifier (intern_ident lf ist id) + | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) + as x -> x + +and intern_or_and_intro_pattern lf ist = List.map (List.map (intern_intro_pattern lf ist)) let intern_quantified_hypothesis ist = function @@ -602,10 +601,10 @@ let intern_red_expr ist = function let intern_inversion_strength lf ist = function | NonDepInversion (k,idl,ids) -> NonDepInversion (k,List.map (intern_hyp_or_metaid ist) idl, - intern_intro_pattern lf ist ids) + Option.map (intern_intro_pattern lf ist) ids) | DepInversion (k,copt,ids) -> DepInversion (k, Option.map (intern_constr ist) copt, - intern_intro_pattern lf ist ids) + Option.map (intern_intro_pattern lf ist) ids) | InversionUsing (c,idl) -> InversionUsing (intern_constr ist c, List.map (intern_hyp_or_metaid ist) idl) @@ -642,9 +641,9 @@ 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 _ + | VRTactic _ | VFun _ | VVoid | VInteger _ | VConstr_context _ | VIntroPattern _ | VRec _ | VList _ -> - error "Only externing of terms is implemented" + error "Only externing of terms is implemented." let extern_request ch req gl la = output_string ch "\n" -(* Reads the hypotheses of a Match Context rule *) -let rec intern_match_context_hyps sigma env lfun = function +(* Reads the hypotheses of a "match goal" rule *) +let rec intern_match_goal_hyps sigma env lfun = function | (Hyp ((_,na) as locna,mp))::tl -> let ido, metas1, pat = intern_pattern sigma env ~as_type:true lfun mp in - let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in + let lfun, metas2, hyps = intern_match_goal_hyps sigma env lfun tl in let lfun' = name_cons na (Option.List.cons ido lfun) in lfun', metas1@metas2, Hyp (locna,pat)::hyps | [] -> lfun, [], [] @@ -667,7 +666,7 @@ let extract_let_names lrc = (fun ((loc,name),_) l -> if List.mem name l then user_err_loc - (loc, "glob_tactic", str "This variable is bound several times"); + (loc, "glob_tactic", str "This variable is bound several times."); name::l) lrc [] @@ -684,14 +683,15 @@ let rec intern_atomic lf ist x = | TacIntroPattern l -> TacIntroPattern (List.map (intern_intro_pattern lf ist) l) | TacIntrosUntil hyp -> TacIntrosUntil (intern_quantified_hypothesis ist hyp) - | TacIntroMove (ido,ido') -> + | TacIntroMove (ido,hto) -> TacIntroMove (Option.map (intern_ident lf ist) ido, - Option.map (intern_hyp ist) ido') + intern_move_location ist hto) | TacAssumption -> TacAssumption | TacExact c -> TacExact (intern_constr ist c) | TacExactNoCheck c -> TacExactNoCheck (intern_constr ist c) | TacVmCastNoCheck c -> TacVmCastNoCheck (intern_constr ist c) - | TacApply (a,ev,cb) -> TacApply (a,ev,intern_constr_with_bindings ist cb) + | TacApply (a,ev,cb) -> + TacApply (a,ev,List.map (intern_constr_with_bindings ist) cb) | TacElim (ev,cb,cbo) -> TacElim (ev,intern_constr_with_bindings ist cb, Option.map (intern_constr_with_bindings ist) cbo) @@ -735,20 +735,15 @@ let rec intern_atomic lf ist x = List.map (intern_constr ist) lems) (* Derived basic tactics *) - | TacSimpleInduction h -> - TacSimpleInduction (intern_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids,cls) -> - TacNewInduction (ev,List.map (intern_induction_arg ist) lc, - Option.map (intern_constr_with_bindings ist) cbo, - intern_intro_pattern lf ist ids, - Option.map (clause_app (intern_hyp_location ist)) cls) - | TacSimpleDestruct h -> - TacSimpleDestruct (intern_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids,cls) -> - TacNewDestruct (ev,List.map (intern_induction_arg ist) c, + | TacSimpleInductionDestruct (isrec,h) -> + TacSimpleInductionDestruct (isrec,intern_quantified_hypothesis ist h) + | TacInductionDestruct (ev,isrec,l) -> + TacInductionDestruct (ev,isrec,List.map (fun (lc,cbo,(ipato,ipats),cls) -> + (List.map (intern_induction_arg ist) lc, Option.map (intern_constr_with_bindings ist) cbo, - intern_intro_pattern lf ist ids, - Option.map (clause_app (intern_hyp_location ist)) cls) + (Option.map (intern_intro_pattern lf ist) ipato, + Option.map (intern_intro_pattern lf ist) ipats), + Option.map (clause_app (intern_hyp_location ist)) cls)) l) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in @@ -764,7 +759,7 @@ let rec intern_atomic lf ist x = | TacClear (b,l) -> TacClear (b,List.map (intern_hyp_or_metaid ist) l) | TacClearBody l -> TacClearBody (List.map (intern_hyp_or_metaid ist) l) | TacMove (dep,id1,id2) -> - TacMove (dep,intern_hyp_or_metaid ist id1,intern_hyp_or_metaid ist id2) + TacMove (dep,intern_hyp_or_metaid ist id1,intern_move_location ist id2) | TacRename l -> TacRename (List.map (fun (id1,id2) -> intern_hyp_or_metaid ist id1, @@ -812,8 +807,7 @@ let rec intern_atomic lf ist x = TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l) | TacAlias (loc,s,l,(dir,body)) -> let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in - try TacAlias (loc,s,l,(dir,body)) - with e -> raise (locate_error_in_file (string_of_dirpath dir) e) + TacAlias (loc,s,l,(dir,body)) and intern_tactic ist tac = (snd (intern_tactic_seq ist tac) : glob_tactic_expr) @@ -829,8 +823,8 @@ and intern_tactic_seq ist = function let l = List.map (fun (n,b) -> (n,intern_tacarg !strict_check (if isrec then ist' else ist) b)) l in ist.ltacvars, TacLetIn (isrec,l,intern_tactic ist' u) - | TacMatchContext (lz,lr,lmr) -> - ist.ltacvars, TacMatchContext(lz,lr, intern_match_rule ist lmr) + | TacMatchGoal (lz,lr,lmr) -> + ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule ist lmr) | TacMatch (lz,c,lmr) -> ist.ltacvars, TacMatch (lz,intern_tactic ist c,intern_match_rule ist lmr) | TacId l -> ist.ltacvars, TacId (intern_message ist l) @@ -885,7 +879,7 @@ and intern_tacarg strict ist = function if istac then Reference (ArgVar (adjust_loc loc,id)) else ConstrMayEval (ConstrTerm (RVar (adjust_loc loc,id), None)) else error_syntactic_metavariables_not_allowed loc - | TacCall (loc,f,[]) -> intern_isolated_tactic_reference ist f + | TacCall (loc,f,[]) -> intern_isolated_tactic_reference strict ist f | TacCall (loc,f,l) -> TacCall (loc, intern_applied_tactic_reference ist f, @@ -906,7 +900,7 @@ and intern_match_rule ist = function All (intern_tactic ist tc) :: (intern_match_rule ist tl) | (Pat (rl,mp,tc))::tl -> let {ltacvars=(lfun,l2); gsigma=sigma; genv=env} = ist in - let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in + let lfun',metas1,hyps = intern_match_goal_hyps sigma env lfun rl in let ido,metas2,pat = intern_pattern sigma env lfun mp in let metas = list_uniquize (metas1@metas2) in let ist' = { ist with ltacvars = (metas@(Option.List.cons ido lfun'),l2) } in @@ -1006,23 +1000,23 @@ let read_pattern lfun = function (* Reads the hypotheses of a Match Context rule *) let cons_and_check_name id l = if List.mem id l then - user_err_loc (dloc,"read_match_context_hyps", - str ("Hypothesis pattern-matching variable "^(string_of_id id)^ - " used twice in the same pattern")) + user_err_loc (dloc,"read_match_goal_hyps", + strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^ + " used twice in the same pattern.")) else id::l -let rec read_match_context_hyps lfun lidh = function +let rec read_match_goal_hyps lfun lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> let lidh' = name_fold cons_and_check_name na lidh in Hyp (locna,read_pattern lfun mp):: - (read_match_context_hyps lfun lidh' tl) + (read_match_goal_hyps lfun lidh' tl) | [] -> [] (* Reads the rules of a Match Context or a Match *) let rec read_match_rule lfun = function | (All tc)::tl -> (All tc)::(read_match_rule lfun tl) | (Pat (rl,mp,tc))::tl -> - Pat (read_match_context_hyps lfun [] rl, read_pattern lfun mp,tc) + Pat (read_match_goal_hyps lfun [] rl, read_pattern lfun mp,tc) :: read_match_rule lfun tl | [] -> [] @@ -1110,8 +1104,8 @@ let debugging_exception_step ist signal_anomaly e pp = let error_ltac_variable loc id env v s = user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ - str " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ - strbrk "which cannot be coerced to " ++ str s) + strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ + strbrk "which cannot be coerced to " ++ str s ++ str".") exception CannotCoerceTo of string @@ -1153,8 +1147,8 @@ let coerce_to_intro_pattern env = function IntroIdentifier (destVar c) | v -> raise (CannotCoerceTo "an introduction pattern") -let interp_intro_pattern_var ist env id = - try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env)(dloc,id) +let interp_intro_pattern_var loc ist env id = + try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some env) (loc,id) with Not_found -> IntroIdentifier id let coerce_to_hint_base = function @@ -1171,8 +1165,9 @@ let coerce_to_int = function let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid - with Not_found -> user_err_loc(fst locid,"interp_int", - str "Unbound variable" ++ pr_id (snd locid)) + with Not_found -> + user_err_loc(fst locid,"interp_int", + str "Unbound variable " ++ pr_id (snd locid) ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid @@ -1209,7 +1204,7 @@ let interp_hyp ist gl (loc,id as locid) = with Not_found -> (* Then look if bound in the proof context at calling time *) if is_variable env id then id - else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found") + 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 @@ -1227,11 +1222,16 @@ let interp_clause_pattern ist gl (l,occl) = | (hyp,l) :: rest -> let hyp = interp_hyp ist gl hyp in if List.mem hyp acc then - error ("Hypothesis "^(string_of_id hyp)^" occurs twice"); + error ("Hypothesis "^(string_of_id hyp)^" occurs twice."); (hyp,l)::(check (hyp::acc) rest) | [] -> [] in (l,check [] occl) +let interp_move_location ist gl = function + | MoveAfter id -> MoveAfter (interp_hyp ist gl id) + | MoveBefore id -> MoveBefore (interp_hyp ist gl id) + | MoveToEnd toleft as x -> x + (* Interprets a qualified name *) let coerce_to_reference env v = try match v with @@ -1309,7 +1309,7 @@ let rec constr_list_aux env = function let constr_list ist env = constr_list_aux env ist.lfun (* Extract the identifier list from lfun: join all branches (what to do else?)*) -let rec intropattern_ids = function +let rec intropattern_ids (loc,pat) = match pat with | IntroIdentifier id -> [id] | IntroOrAndPattern ll -> List.flatten (List.map intropattern_ids (List.flatten ll)) @@ -1317,7 +1317,7 @@ let rec intropattern_ids = function let rec extract_ids ids = function | (id,VIntroPattern ipat)::tl when not (List.mem id ids) -> - intropattern_ids ipat @ extract_ids ids tl + intropattern_ids (dloc,ipat) @ extract_ids ids tl | _::tl -> extract_ids ids tl | [] -> [] @@ -1388,7 +1388,7 @@ let solve_remaining_evars env initial_sigma evd c = proc_rec c let interp_gen kind ist sigma env (c,ce) = - let (ltacvars,unbndltacvars) = constr_list ist env in + let (ltacvars,unbndltacvars as vars) = constr_list ist env in let typs = retype_list sigma env ltacvars in let c = match ce with | None -> c @@ -1398,7 +1398,8 @@ let interp_gen kind ist sigma env (c,ce) = | Some c -> let ltacdata = (List.map fst ltacvars,unbndltacvars) in intern_gen (kind = IsType) ~ltacvars:ltacdata sigma env c in - understand_ltac sigma env (typs,unbndltacvars) kind c + let trace = (dloc,LtacConstrInterp (c,vars))::ist.trace in + catch_error trace (understand_ltac sigma env (typs,unbndltacvars) kind) c (* Interprets a constr and solve remaining evars with default tactic *) let interp_econstr kind ist sigma env cc = @@ -1532,7 +1533,7 @@ let interp_may_eval f ist gl = function with | Not_found -> user_err_loc (loc, "interp_may_eval", - str "Unbound context identifier" ++ pr_id s)) + str "Unbound context identifier" ++ pr_id s ++ str".")) | ConstrTypeOf c -> pf_type_of gl (f ist gl c) | ConstrTerm c -> try @@ -1565,31 +1566,38 @@ let inj_may_eval = function let message_of_value = function | VVoid -> str "()" | VInteger n -> int n - | VIntroPattern ipat -> pr_intro_pattern ipat + | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat) | VConstr_context c | VConstr c -> pr_constr c - | VRec _ | VTactic _ | VRTactic _ | VFun _ -> str "" + | VRec _ | VRTactic _ | VFun _ -> str "" | VList _ -> str "" -let rec interp_message ist = function - | [] -> mt() - | MsgString s :: l -> pr_arg str s ++ interp_message ist l - | MsgInt n :: l -> pr_arg int n ++ interp_message ist l - | MsgIdent (loc,id) :: l -> +let rec interp_message_token ist = function + | MsgString s -> str s + | MsgInt n -> int n + | MsgIdent (loc,id) -> let v = try List.assoc id ist.lfun - with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found") in - pr_arg message_of_value v ++ interp_message ist l + with Not_found -> user_err_loc (loc,"",pr_id id ++ str" not found.") in + message_of_value v let rec interp_message_nl ist = function | [] -> mt() - | l -> interp_message ist l ++ fnl() + | l -> prlist_with_sep spc (interp_message_token ist) l ++ fnl() -let rec interp_intro_pattern ist gl = function - | IntroOrAndPattern l -> IntroOrAndPattern (interp_case_intro_pattern ist gl l) - | IntroIdentifier id -> interp_intro_pattern_var ist (pf_env gl) id - | IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _ as x -> x +let interp_message ist l = + (* Force evaluation of interp_message_token so that potential errors + are raised now and not at printing time *) + prlist (fun x -> spc () ++ x) (List.map (interp_message_token ist) l) -and interp_case_intro_pattern ist gl = +let rec interp_intro_pattern ist gl = function + | loc, IntroOrAndPattern l -> + loc, IntroOrAndPattern (interp_or_and_intro_pattern ist gl l) + | loc, IntroIdentifier id -> + loc, interp_intro_pattern_var loc ist (pf_env gl) id + | loc, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) + as x -> x + +and interp_or_and_intro_pattern ist gl = List.map (List.map (interp_intro_pattern ist gl)) (* Quantified named or numbered hypothesis or hypothesis in context *) @@ -1663,14 +1671,14 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = let value_interp ist = match tac with (* Immediate evaluation *) - | TacFun (it,body) -> VFun (ist.lfun,it,body) + | TacFun (it,body) -> VFun (ist.trace,ist.lfun,it,body) | TacLetIn (true,l,u) -> interp_letrec ist gl l u | TacLetIn (false,l,u) -> interp_letin ist gl l u - | TacMatchContext (lz,lr,lmr) -> interp_match_context ist gl lz lr lmr + | TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist gl lz lr lmr | TacMatch (lz,c,lmr) -> interp_match ist gl lz c lmr | TacArg a -> interp_tacarg ist gl a (* Delayed evaluation *) - | t -> VTactic (ist.last_loc,eval_tactic ist t) + | t -> VFun (ist.trace,ist.lfun,[],t) in check_for_interrupt (); match ist.debug with @@ -1679,9 +1687,16 @@ let rec val_interp ist gl (tac:glob_tactic_expr) = | _ -> value_interp ist and eval_tactic ist = function - | TacAtom (loc,t) -> fun gl -> catch_error loc (interp_atomic ist gl t) gl + | TacAtom (loc,t) -> + fun gl -> + let box = ref None in abstract_tactic_box := box; + let call = LtacAtomCall (t,box) in + let tac = (* catch error in the interpretation *) + catch_error ((dloc,call)::ist.trace) (interp_atomic ist gl) t in + (* catch error in the evaluation *) + catch_error ((loc,call)::ist.trace) tac gl | TacFun _ | TacLetIn _ -> assert false - | TacMatchContext _ | TacMatch _ -> assert false + | TacMatchGoal _ | TacMatch _ -> assert false | TacId s -> tclIDTAC_MESSAGE (interp_message_nl ist s) | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) (interp_message ist s) | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) @@ -1714,31 +1729,33 @@ and force_vrec ist gl = function | VRec (lfun,body) -> val_interp {ist with lfun = !lfun} gl body | v -> v -and interp_ltac_reference isapplied mustbetac ist gl = function +and interp_ltac_reference loc' mustbetac ist gl = function | ArgVar (loc,id) -> let v = List.assoc id ist.lfun in let v = force_vrec ist gl v in + let v = propagate_trace ist loc id v in if mustbetac then coerce_to_tactic loc id v else v | ArgArg (loc,r) -> let ids = extract_ids [] ist.lfun in + let loc_info = ((if loc' = dloc then loc else loc'),LtacNameCall r) in let ist = { lfun=[]; debug=ist.debug; avoid_ids=ids; - last_loc = if isapplied then ist.last_loc else loc } in + trace = loc_info::ist.trace } in val_interp ist gl (lookup r) and interp_tacarg ist gl = function | TacVoid -> VVoid - | Reference r -> interp_ltac_reference false false ist gl r + | Reference r -> interp_ltac_reference dloc false ist gl r | Integer n -> VInteger n - | IntroPattern ipat -> VIntroPattern (interp_intro_pattern ist gl ipat) + | IntroPattern ipat -> VIntroPattern (snd (interp_intro_pattern ist gl ipat)) | ConstrMayEval c -> VConstr (interp_constr_may_eval ist gl c) | MetaIdArg (loc,_,id) -> assert false - | TacCall (loc,r,[]) -> interp_ltac_reference false true ist gl r + | TacCall (loc,r,[]) -> interp_ltac_reference loc true ist gl r | TacCall (loc,f,l) -> - let fv = interp_ltac_reference true true ist gl f + let fv = interp_ltac_reference loc true ist gl f and largs = List.map (interp_tacarg ist gl) l in List.iter check_is_value largs; - interp_app ist gl fv largs loc + interp_app loc ist gl fv largs | TacExternal (loc,com,req,la) -> interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la) | TacFreshId l -> @@ -1748,12 +1765,7 @@ and interp_tacarg ist gl = function | TacDynamic(_,t) -> let tg = (tag t) in if tg = "tactic" then - let f = (tactic_out t) in - val_interp ist gl - (intern_tactic { - ltacvars = (List.map fst ist.lfun,[]); ltacrecvars = []; - gsigma = project gl; genv = pf_env gl } - (f ist)) + val_interp ist gl (tactic_out t ist) else if tg = "value" then value_out t else if tg = "constr" then @@ -1763,48 +1775,54 @@ and interp_tacarg ist gl = function (str "Unknown dynamic: <" ++ str (Dyn.tag t) ++ str ">")) (* Interprets an application node *) -and interp_app ist gl fv largs loc = +and interp_app loc ist gl fv largs = match fv with - | VFun(olfun,var,body) -> + | VFun(trace,olfun,var,body) -> let (newlfun,lvar,lval)=head_with_value (var,largs) in if lvar=[] then let v = try - let lloc = if lval=[] then loc else ist.last_loc in - val_interp { ist with lfun=newlfun@olfun; last_loc=lloc } gl body + catch_error trace + (val_interp { ist with lfun=newlfun@olfun; trace=trace } gl) body with e -> debugging_exception_step ist false e (fun () -> str "evaluation"); raise e in debugging_step ist (fun () -> str "evaluation returns" ++ fnl() ++ pr_value (Some (pf_env gl)) v); - if lval=[] then v else interp_app ist gl v lval loc + if lval=[] then v else interp_app loc ist gl v lval else - VFun(newlfun@olfun,lvar,body) + VFun(trace,newlfun@olfun,lvar,body) | _ -> user_err_loc (loc, "Tacinterp.interp_app", - (str"Illegal tactic application")) + (str"Illegal tactic application.")) (* Gives the tactic corresponding to the tactic value *) -and tactic_of_value vle g = +and tactic_of_value ist vle g = match vle with | VRTactic res -> res - | VTactic (loc,tac) -> catch_error loc tac g - | VFun _ -> error "A fully applied tactic is expected" + | VFun (trace,lfun,[],t) -> + let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in + catch_error trace tac g + | VFun _ -> error "A fully applied tactic is expected." | _ -> raise NotTactic (* Evaluation with FailError catching *) and eval_with_fail ist is_lazy goal tac = try (match val_interp ist goal tac with - | VTactic (loc,tac) when not is_lazy -> VRTactic (catch_error loc tac goal) + | VFun (trace,lfun,[],t) when not is_lazy -> + let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in + VRTactic (catch_error trace tac goal) | a -> a) with - | Stdpp.Exc_located (_,FailError (0,s)) | FailError (0,s) -> + | FailError (0,s) | Stdpp.Exc_located(_, FailError (0,s)) + | Stdpp.Exc_located(_,LtacLocated (_,FailError (0,s))) -> raise (Eval_fail s) - | Stdpp.Exc_located (s',FailError (lvl,s)) -> - raise (Stdpp.Exc_located (s',FailError (lvl - 1, s))) - | FailError (lvl,s) -> - raise (FailError (lvl - 1, s)) + | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) + | Stdpp.Exc_located(s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) + | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1, s')))) (* Interprets the clauses of a recursive LetIn *) and interp_letrec ist gl llc u = @@ -1822,14 +1840,14 @@ and interp_letin ist gl llc u = val_interp ist gl u (* Interprets the Match Context expressions *) -and interp_match_context ist g lz lr lmr = +and interp_match_goal 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 - let rec apply_match_context ist env goal nrs lex lpt = + let rec apply_match_goal ist env goal nrs lex lpt = begin if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); match lpt with @@ -1838,7 +1856,7 @@ and interp_match_context ist g lz lr lmr = 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 + apply_match_goal ist env goal (nrs+1) (List.tl lex) tl end | (Pat (mhyps,mgoal,mt))::tl -> let hyps = make_hyps (pf_hyps goal) in @@ -1856,21 +1874,21 @@ and interp_match_context ist g lz lr lmr = | 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) + apply_match_goal 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)) + apply_match_goal ist env goal (nrs+1) (List.tl lex) tl)) | _ -> - errorlabstrm "Tacinterp.apply_match_context" + errorlabstrm "Tacinterp.apply_match_goal" (v 0 (str "No matching clauses for match goal" ++ (if ist.debug=DebugOff then fnl() ++ str "(use \"Set Ltac Debug\" for more info)" - else mt()))) + else mt()) ++ str".")) end in let env = pf_env g in - apply_match_context ist env g 0 lmr + apply_match_goal ist env g 0 lmr (read_match_rule (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) @@ -2023,7 +2041,7 @@ and interp_match ist g lz constr lmr = with PatternMatchingFailure -> apply_match ist csr tl) | _ -> errorlabstrm "Tacinterp.apply_match" (str - "No matching clauses for match") in + "No matching clauses for match.") in let csr = try interp_ltac_constr ist g constr with e -> debugging_exception_step ist true e @@ -2058,9 +2076,8 @@ and interp_ltac_constr ist gl e = 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) -> + | VFun (_,il,ul,b) -> (str "VFun with body " ++ fnl() ++ Pptactic.pr_glob_tactic (pf_env gl) b ++ fnl() ++ str "instantiated arguments " ++ fnl() ++ @@ -2074,20 +2091,19 @@ and interp_ltac_constr ist gl e = (match opt_id with Some id -> str (string_of_id id) | None -> str "_") ++ str ", " ++ s) - ul (str "")) + ul (mt())) | VVoid -> str "VVoid" | VInteger _ -> str "VInteger" | VConstr _ -> str "VConstr" | VIntroPattern _ -> str "VIntroPattern" | VConstr_context _ -> str "VConstrr_context" | VRec _ -> str "VRec" - | VList _ -> str "VList")) + | VList _ -> str "VList") ++ str".") (* Interprets tactic expressions : returns a "tactic" *) and interp_tactic ist tac gl = - try tactic_of_value (val_interp ist gl tac) gl - with NotTactic -> - errorlabstrm "" (str "Must be a command or must give a tactic value") + try tactic_of_value ist (val_interp ist gl tac) gl + with NotTactic -> errorlabstrm "" (str "Not a tactic.") (* Interprets a primitive tactic *) and interp_atomic ist gl = function @@ -2096,14 +2112,15 @@ and interp_atomic ist gl = function h_intro_patterns (List.map (interp_intro_pattern ist gl) l) | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) - | TacIntroMove (ido,ido') -> + | TacIntroMove (ido,hto) -> h_intro_move (Option.map (interp_fresh_ident ist gl) ido) - (Option.map (interp_hyp ist gl) ido') + (interp_move_location ist gl hto) | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) - | TacApply (a,ev,cb) -> h_apply a ev (interp_constr_with_bindings ist gl cb) + | TacApply (a,ev,cb) -> + h_apply a ev (List.map (interp_constr_with_bindings ist gl) cb) | TacElim (ev,cb,cbo) -> h_elim ev (interp_constr_with_bindings ist gl cb) (Option.map (interp_constr_with_bindings ist gl) cbo) @@ -2149,20 +2166,16 @@ and interp_atomic ist gl = function (pf_interp_constr_list ist gl lems) (* Derived basic tactics *) - | TacSimpleInduction h -> - h_simple_induction (interp_quantified_hypothesis ist h) - | TacNewInduction (ev,lc,cbo,ids,cls) -> - h_new_induction ev (List.map (interp_induction_arg ist gl) lc) - (Option.map (interp_constr_with_bindings ist gl) cbo) - (interp_intro_pattern ist gl ids) - (Option.map (interp_clause ist gl) cls) - | TacSimpleDestruct h -> - h_simple_destruct (interp_quantified_hypothesis ist h) - | TacNewDestruct (ev,c,cbo,ids,cls) -> - h_new_destruct ev (List.map (interp_induction_arg ist gl) c) - (Option.map (interp_constr_with_bindings ist gl) cbo) - (interp_intro_pattern ist gl ids) - (Option.map (interp_clause ist gl) cls) + | TacSimpleInductionDestruct (isrec,h) -> + h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) + | TacInductionDestruct (isrec,ev,l) -> + h_induction_destruct ev isrec + (List.map (fun (lc,cbo,(ipato,ipats),cls) -> + (List.map (interp_induction_arg ist gl) lc, + Option.map (interp_constr_with_bindings ist gl) cbo, + (Option.map (interp_intro_pattern ist gl) ipato, + Option.map (interp_intro_pattern ist gl) ipats), + Option.map (interp_clause ist gl) cls)) l) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2180,7 +2193,7 @@ and interp_atomic ist gl = function | 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) + h_move dep (interp_hyp ist gl id1) (interp_move_location ist gl id2) | TacRename l -> h_rename (List.map (fun (id1,id2) -> interp_hyp ist gl id1, @@ -2222,11 +2235,11 @@ and interp_atomic ist gl = function (Option.map (interp_tactic ist) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) - (interp_intro_pattern ist gl ids) + (Option.map (interp_intro_pattern ist gl) ids) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (NonDepInversion (k,idl,ids),hyp) -> Inv.inv_clause k - (interp_intro_pattern ist gl ids) + (Option.map (interp_intro_pattern ist gl) ids) (interp_hyp_list ist gl idl) (interp_declared_or_quantified_hypothesis ist gl hyp) | TacInversion (InversionUsing (c,idl),hyp) -> @@ -2237,10 +2250,9 @@ and interp_atomic ist gl = function (* For extensions *) | TacExtend (loc,opn,l) -> 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 args = List.map (interp_genarg ist gl) l in + abstract_extended_tactic opn args (tac args) + | TacAlias (loc,s,l,(_,body)) -> fun gl -> let rec f x = match genarg_tag x with | IntArgType -> VInteger (out_gen globwit_int x) @@ -2250,7 +2262,7 @@ and interp_atomic ist gl = function failwith "pre-identifiers cannot be bound" | IntroPatternArgType -> VIntroPattern - (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)) + (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) | IdentArgType -> VIntroPattern (IntroIdentifier @@ -2301,14 +2313,12 @@ and interp_atomic ist gl = function | ExtraArgType _ | BindingsArgType | OptArgType _ | PairArgType _ | List0ArgType _ | List1ArgType _ - -> error "This generic type is not supported in alias" + -> error "This generic type is not supported in alias." in let lfun = (List.map (fun (x,c) -> (x,f c)) l)@ist.lfun in - let v = locate_tactic_call loc (val_interp { ist with lfun=lfun } gl body) - in - try tactic_of_value v gl - with NotTactic -> user_err_loc (loc,"",str "not a tactic") + let trace = (loc,LtacNotationCall s)::ist.trace in + interp_tactic { ist with lfun=lfun; trace=trace } body gl let make_empty_glob_sign () = { ltacvars = ([],[]); ltacrecvars = []; @@ -2316,20 +2326,20 @@ let make_empty_glob_sign () = (* Initial call for interpretation *) let interp_tac_gen lfun avoid_ids debug t gl = - interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; last_loc=dloc } + interp_tactic { lfun=lfun; avoid_ids=avoid_ids; debug=debug; trace=[] } (intern_tactic { ltacvars = (List.map fst lfun, []); ltacrecvars = []; gsigma = project gl; genv = pf_env gl } t) gl let eval_tactic t gls = - interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); last_loc=dloc } + interp_tactic { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } t gls let interp t = interp_tac_gen [] [] (get_debug()) t let eval_ltac_constr gl t = interp_ltac_constr - { lfun=[]; avoid_ids=[]; debug=get_debug(); last_loc=dloc } gl + { lfun=[]; avoid_ids=[]; debug=get_debug(); trace=[] } gl (intern_tactic (make_empty_glob_sign ()) t ) (* Hides interpretation for pretty-print *) @@ -2392,7 +2402,7 @@ let subst_global_reference subst = let subst_global ref = let ref',t' = subst_global subst ref in if not (eq_constr (constr_of_global ref') t') then - ppnl (str "Warning: the reference " ++ pr_global ref ++ str " is not " ++ + ppnl (str "Warning: The reference " ++ pr_global ref ++ str " is not " ++ str " expanded to \"" ++ pr_lconstr t' ++ str "\", but to " ++ pr_global ref') ; ref' @@ -2430,10 +2440,10 @@ let subst_match_pattern subst = function | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc) | Term pc -> Term (subst_pattern subst pc) -let rec subst_match_context_hyps subst = function +let rec subst_match_goal_hyps subst = function | Hyp (locs,mp) :: tl -> Hyp (locs,subst_match_pattern subst mp) - :: subst_match_context_hyps subst tl + :: subst_match_goal_hyps subst tl | [] -> [] let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with @@ -2443,7 +2453,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacExact c -> TacExact (subst_rawconstr subst c) | TacExactNoCheck c -> TacExactNoCheck (subst_rawconstr subst c) | TacVmCastNoCheck c -> TacVmCastNoCheck (subst_rawconstr subst c) - | TacApply (a,ev,cb) -> TacApply (a,ev,subst_raw_with_bindings subst cb) + | TacApply (a,ev,cb) -> + TacApply (a,ev,List.map (subst_raw_with_bindings subst) cb) | TacElim (ev,cb,cbo) -> TacElim (ev,subst_raw_with_bindings subst cb, Option.map (subst_raw_with_bindings subst) cbo) @@ -2474,14 +2485,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDAuto (n,p,lems) -> TacDAuto (n,p,List.map (subst_rawconstr subst) lems) (* Derived basic tactics *) - | TacSimpleInduction h as x -> x - | TacNewInduction (ev,lc,cbo,ids,cls) -> - TacNewInduction (ev,List.map (subst_induction_arg subst) lc, - Option.map (subst_raw_with_bindings subst) cbo, ids, cls) - | TacSimpleDestruct h as x -> x - | TacNewDestruct (ev,c,cbo,ids,cls) -> - TacNewDestruct (ev,List.map (subst_induction_arg subst) c, - Option.map (subst_raw_with_bindings subst) cbo, ids, cls) + | TacSimpleInductionDestruct (isrec,h) as x -> x + | TacInductionDestruct (isrec,ev,l) -> + TacInductionDestruct (isrec,ev,List.map (fun (lc,cbo,ids,cls) -> + List.map (subst_induction_arg subst) lc, + Option.map (subst_raw_with_bindings subst) cbo, ids, cls) l) | TacDoubleInduction (h1,h2) as x -> x | TacDecomposeAnd c -> TacDecomposeAnd (subst_rawconstr subst c) | TacDecomposeOr c -> TacDecomposeOr (subst_rawconstr subst c) @@ -2540,8 +2548,8 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with | TacLetIn (r,l,u) -> let l = List.map (fun (n,b) -> (n,subst_tacarg subst b)) l in TacLetIn (r,l,subst_tactic subst u) - | TacMatchContext (lz,lr,lmr) -> - TacMatchContext(lz,lr, subst_match_rule subst lmr) + | TacMatchGoal (lz,lr,lmr) -> + TacMatchGoal(lz,lr, subst_match_rule subst lmr) | TacMatch (lz,c,lmr) -> TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr) | TacId _ | TacFail _ as x -> x @@ -2588,7 +2596,7 @@ and subst_match_rule subst = function | (All tc)::tl -> (All (subst_tactic subst tc))::(subst_match_rule subst tl) | (Pat (rl,mp,tc))::tl -> - let hyps = subst_match_context_hyps subst rl in + let hyps = subst_match_goal_hyps subst rl in let pat = subst_match_pattern subst mp in Pat (hyps,pat,subst_tactic subst tc) ::(subst_match_rule subst tl) @@ -2707,12 +2715,12 @@ let print_ltac id = try let kn = Nametab.locate_tactic id in let t = lookup kn in - str "Ltac" ++ spc() ++ pr_qualid id ++ str ":=" ++ spc() ++ + str "Ltac" ++ spc() ++ pr_qualid id ++ str " :=" ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t with Not_found -> errorlabstrm "print_ltac" - (pr_qualid id ++ spc() ++ str "is not a user defined tactic") + (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") open Libnames @@ -2729,14 +2737,14 @@ let make_absolute_name ident repl = if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is already an Ltac named " ++ pr_reference ident) + str "There is already an Ltac named " ++ pr_reference ident ++ str".") else if is_atomic_kn kn then user_err_loc (loc,"Tacinterp.add_tacdef", - str "Reserved Ltac name " ++ pr_reference ident) + str "Reserved Ltac name " ++ pr_reference ident ++ str".") else id, kn with Not_found -> user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is no Ltac named " ++ pr_reference ident) + str "There is no Ltac named " ++ pr_reference ident ++ str".") let rec filter_map f l = let rec aux acc = function @@ -2782,17 +2790,33 @@ let glob_tactic_env l env x = x let interp_redexp env sigma r = - let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); last_loc=dloc } in + let ist = { lfun=[]; avoid_ids=[]; debug=get_debug (); trace=[] } in let gist = {(make_empty_glob_sign ()) with genv = env; gsigma = sigma } in interp_red_expr ist sigma env (intern_red_expr gist r) +(***************************************************************************) +(* Embed tactics in raw or glob tactic expr *) + +let globTacticIn t = TacArg (TacDynamic (dummy_loc,tactic_in t)) +let tacticIn t = globTacticIn (fun ist -> glob_tactic (t ist)) + +let tacticOut = function + | TacArg (TacDynamic (_,d)) -> + if (tag d) = "tactic" then + tactic_out d + else + anomalylabstrm "tacticOut" (str "Dynamic tag should be tactic") + | ast -> + anomalylabstrm "tacticOut" + (str "Not a Dynamic ast: " (* ++ print_ast ast*) ) + (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = Auto.set_extern_interp (fun l -> let l = List.map (fun (id,c) -> (id,VConstr c)) l in - interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); last_loc=dloc}) + interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]}) let _ = Auto.set_extern_intern_tac (fun l -> Flags.with_option strict_check diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 87aa85dc..928e5914 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 10919 2008-05-11 22:04:26Z msozeau $ i*) +(*i $Id: tacinterp.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Dyn @@ -26,9 +26,9 @@ open Redexpr (* Values for interpretation *) type value = - | VTactic of Util.loc * tactic (* For mixed ML/Ltac tactics (e.g. Tauto) *) | VRTactic of (goal list sigma * validation) - | VFun of (identifier * value) list * identifier option list * glob_tactic_expr + | VFun of ltac_trace * (identifier*value) list * + identifier option list * glob_tactic_expr | VVoid | VInteger of int | VIntroPattern of intro_pattern_expr @@ -42,18 +42,16 @@ and interp_sign = { lfun : (identifier * value) list; avoid_ids : identifier list; debug : debug_info; - last_loc : loc } + trace : ltac_trace } (* Transforms an id into a constr if possible *) val constr_of_id : Environ.env -> identifier -> constr (* To embed several objects in Coqast.t *) val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr -val tacticOut : raw_tactic_expr -> (interp_sign -> raw_tactic_expr) +val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr val valueIn : value -> raw_tactic_arg -val valueOut: raw_tactic_arg -> value val constrIn : constr -> constr_expr -val constrOut : constr_expr -> constr (* Sets the debugger mode *) val set_debug : debug_info -> unit diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index eeca6301..3b13d1a0 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tacticals.ml 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: tacticals.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -86,7 +86,7 @@ let tclMAP tacfun l = let tclNTH_HYP m (tac : constr->tactic) gl = tac (try mkVar(let (id,_,_) = List.nth (pf_hyps gl) (m-1) in id) - with Failure _ -> error "No such assumption") gl + with Failure _ -> error "No such assumption.") gl (* apply a tactic to the last element of the signature *) @@ -94,11 +94,11 @@ let tclLAST_HYP = tclNTH_HYP 1 let tclLAST_NHYPS n tac gl = tac (try list_firstn n (pf_ids_of_hyps gl) - with Failure _ -> error "No such assumptions") gl + with Failure _ -> error "No such assumptions.") gl let tclTRY_sign (tac : constr->tactic) sign gl = let rec arec = function - | [] -> tclFAIL 0 (str "no applicable hypothesis") + | [] -> tclFAIL 0 (str "No applicable hypothesis.") | [s] -> tac (mkVar s) (*added in order to get useful error messages *) | (s::sl) -> tclORELSE (tac (mkVar s)) (arec sl) in @@ -218,7 +218,7 @@ let lastHyp gl = List.hd (pf_ids_of_hyps gl) let nLastHyps n gl = try list_firstn n (pf_hyps gl) - with Failure "firstn" -> error "Not enough hypotheses in the goal" + with Failure "firstn" -> error "Not enough hypotheses in the goal." let onClause t cls gl = t cls gl @@ -270,19 +270,28 @@ type branch_args = { nassums : int; (* the number of assumptions to be introduced *) branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) - branchnames : intro_pattern_expr list} + branchnames : intro_pattern_expr located list} type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) +let check_or_and_pattern_size loc names n = + if List.length names <> n then + if n = 1 then + user_err_loc (loc,"",str "Expects a conjunctive pattern.") + else + user_err_loc (loc,"",str "Expects a disjunctive pattern with " ++ int n + ++ str " branches.") + let compute_induction_names n = function - | IntroAnonymous -> + | None -> Array.make n [] - | IntroOrAndPattern names when List.length names = n -> + | Some (loc,IntroOrAndPattern names) -> + check_or_and_pattern_size loc names n; Array.of_list names | _ -> - errorlabstrm "" (str "Expects " ++ int n ++ str " lists of names") + error "Unexpected introduction pattern." let compute_construtor_signatures isrec (_,k as ity) = let rec analrec c recargs = @@ -335,7 +344,7 @@ let general_elim_then_using mk_elim let indmv = match kind_of_term (last_arg elimclause.templval.Evd.rebus) with | Meta mv -> mv - | _ -> error "elimination" + | _ -> anomaly "elimination" in let pmv = let p, _ = decompose_app elimclause.templtyp.Evd.rebus in @@ -348,7 +357,7 @@ let general_elim_then_using mk_elim | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is not known") + error ("The elimination combinator " ^ name_elim ^ " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause' in let elimclause' = clenv_match_args elimbindings elimclause' in @@ -393,7 +402,7 @@ let elimination_then_using tac predicate bindings c gl = let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let indclause = mk_clenv_from gl (c,t) in general_elim_then_using gl_make_elim - true IntroAnonymous tac predicate bindings ind indclause gl + true None tac predicate bindings ind indclause gl let case_then_using = general_elim_then_using gl_make_case_dep false @@ -423,7 +432,7 @@ let make_elim_branch_assumptions ba gl = id::constargs, recargs, indargs) tl idtl - | (_, _) -> error "make_elim_branch_assumptions" + | (_, _) -> anomaly "make_elim_branch_assumptions" in makerec ([],[],[],[],[]) ba.branchsign (try list_firstn ba.nassums (pf_hyps gl) @@ -447,7 +456,7 @@ let make_case_branch_assumptions ba gl = id::cargs, recargs, id::constargs) tl idtl - | (_, _) -> error "make_case_branch_assumptions" + | (_, _) -> anomaly "make_case_branch_assumptions" in makerec ([],[],[],[]) ba.branchsign (try list_firstn ba.nassums (pf_hyps gl) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e97abe9f..6826977b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tacticals.mli 10785 2008-04-13 21:41:54Z herbelin $ i*) +(*i $Id: tacticals.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Pp +open Util open Names open Term open Sign @@ -124,23 +125,30 @@ type branch_args = { nassums : int; (* the number of assumptions to be introduced *) branchsign : bool list; (* the signature of the branch. true=recursive argument, false=constant *) - branchnames : intro_pattern_expr list} + branchnames : intro_pattern_expr located list} type branch_assumptions = { ba : branch_args; (* the branch args *) assums : named_context} (* the list of assumptions introduced *) +(* [check_disjunctive_pattern_size loc pats n] returns an appropriate *) +(* error message if |pats| <> n *) +val check_or_and_pattern_size : + Util.loc -> or_and_intro_pattern_expr -> int -> unit + (* Useful for [as intro_pattern] modifier *) val compute_induction_names : - int -> intro_pattern_expr -> intro_pattern_expr list array + int -> intro_pattern_expr located option -> + intro_pattern_expr located list array val elimination_sort_of_goal : goal sigma -> sorts_family val elimination_sort_of_hyp : identifier -> goal sigma -> sorts_family val general_elim_then_using : - (inductive -> goal sigma -> constr) -> rec_flag -> intro_pattern_expr -> - (branch_args -> tactic) -> constr option -> - (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic + (inductive -> goal sigma -> constr) -> rec_flag -> + intro_pattern_expr located option -> (branch_args -> tactic) -> + constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> + tactic val elimination_then_using : (branch_args -> tactic) -> constr option -> @@ -151,12 +159,12 @@ val elimination_then : (arg_bindings * arg_bindings) -> constr -> tactic val case_then_using : - intro_pattern_expr -> (branch_args -> tactic) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic val case_nodep_then_using : - intro_pattern_expr -> (branch_args -> tactic) -> + intro_pattern_expr located option -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> inductive -> clausenv -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 88274ef6..b02e84e7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 11166 2008-06-22 13:23:35Z herbelin $ *) +(* $Id: tactics.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Pp open Util @@ -75,6 +75,8 @@ let inj_ebindings = function | ExplicitBindings l -> ExplicitBindings (List.map (fun (l,id,c) -> (l,id,inj_open c)) l) +let dloc = dummy_loc + (*********************************************) (* Tactics *) (*********************************************) @@ -98,7 +100,7 @@ let string_of_inductive c = let (mib,mip) = Global.lookup_inductive ind_sp in string_of_id mip.mind_typename | _ -> raise Bound - with Bound -> error "Bound head variable" + with Bound -> error "Bound head variable." let rec head_constr_bound t l = let t = strip_outer_cast(collapse_appl t) in @@ -114,7 +116,7 @@ let rec head_constr_bound t l = | _ -> raise Bound let head_constr c = - try head_constr_bound c [] with Bound -> error "Bound head variable" + try head_constr_bound c [] with Bound -> error "Bound head variable." (* let bad_tactic_args s l = @@ -126,15 +128,44 @@ let bad_tactic_args s l = (******************************************) let introduction = Tacmach.introduction -let intro_replacing = Tacmach.intro_replacing -let internal_cut = Tacmach.internal_cut -let internal_cut_rev = Tacmach.internal_cut_rev let refine = Tacmach.refine let convert_concl = Tacmach.convert_concl let convert_hyp = Tacmach.convert_hyp -let thin = Tacmach.thin let thin_body = Tacmach.thin_body +let error_clear_dependency env id = function + | Evarutil.OccurHypInSimpleClause None -> + errorlabstrm "" (pr_id id ++ str " is used in conclusion.") + | Evarutil.OccurHypInSimpleClause (Some id') -> + errorlabstrm "" + (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str".") + | Evarutil.EvarTypingBreak ev -> + errorlabstrm "" + (str "Cannot remove " ++ pr_id id ++ + strbrk " without breaking the typing of " ++ + Printer.pr_existential env ev ++ str".") + +let thin l gl = + try thin l gl + with Evarutil.ClearDependencyError (id,err) -> + error_clear_dependency (pf_env gl) id err + +let internal_cut_gen b d t gl = + try internal_cut b d t gl + with Evarutil.ClearDependencyError (id,err) -> + error_clear_dependency (pf_env gl) id err + +let internal_cut = internal_cut_gen false +let internal_cut_replace = internal_cut_gen true + +let internal_cut_rev_gen b d t gl = + try internal_cut_rev b d t gl + with Evarutil.ClearDependencyError (id,err) -> + error_clear_dependency (pf_env gl) id err + +let internal_cut_rev = internal_cut_rev_gen false +let internal_cut_rev_replace = internal_cut_rev_gen true + (* Moving hypotheses *) let move_hyp = Tacmach.move_hyp @@ -174,7 +205,7 @@ let reduct_in_hyp redfun ((_,id),where) gl = match c with | None -> if where = InHypValueOnly then - errorlabstrm "" (pr_id id ++ str "has no value"); + errorlabstrm "" (pr_id id ++ str "has no value."); convert_hyp_no_check (id,None,redfun' ty) gl | Some b -> let b' = if where <> InHypTypeOnly then redfun' b else b in @@ -197,7 +228,7 @@ let change_and_check cv_pb t env sigma c = if is_fconv cv_pb env sigma t c then t else - errorlabstrm "convert-check-hyp" (str "Not convertible") + errorlabstrm "convert-check-hyp" (str "Not convertible.") (* Use cumulutavity only if changing the conclusion not a subterm *) let change_on_subterm cv_pb t = function @@ -219,7 +250,7 @@ let change occl c cls = ({onhyps=(Some(_::_::_)|None)} |{onhyps=Some(_::_);concl_occs=((false,_)|(true,_::_))}), Some _ -> - error "No occurrences expected when changing several hypotheses" + error "No occurrences expected when changing several hypotheses." | _ -> ()); onClauses (change_option occl c) cls @@ -273,15 +304,19 @@ let fresh_id_avoid avoid id = let fresh_id avoid id gl = fresh_id_avoid (avoid@(pf_ids_of_hyps gl)) id -let id_of_name_with_default s = function - | Anonymous -> id_of_string s +let id_of_name_with_default id = function + | Anonymous -> id | Name id -> id +let hid = id_of_string "H" +let xid = id_of_string "X" + +let default_id_of_sort = function Prop _ -> hid | Type _ -> xid + let default_id env sigma = function | (name,None,t) -> - (match Typing.sort_of env sigma t with - | Prop _ -> (id_of_name_with_default "H" name) - | Type _ -> (id_of_name_with_default "X" name)) + let dft = default_id_of_sort (Typing.sort_of env sigma t) in + id_of_name_with_default dft name | (name,Some b,_) -> id_of_name_using_hdchar env b name (* Non primitive introduction tactics are treated by central_intro @@ -293,14 +328,14 @@ type intro_name_flag = | IntroBasedOn of identifier * identifier list | IntroMustBe of identifier -let find_name decl gl = function +let find_name loc decl gl = function | 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 -> + | IntroMustBe id -> let id' = fresh_id [] id gl in - if id' <> id then error ((string_of_id id)^" is already used"); + if id'<>id then user_err_loc (loc,"",pr_id id ++ str" is already used."); id' (* Returns the names that would be created by intros, without doing @@ -319,65 +354,72 @@ let find_intro_names ctxt gl = 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) + | MoveToEnd true -> introduction id + | dest -> tclTHEN (introduction id) (move_hyp true id dest) -let rec intro_gen name_flag move_flag force_flag gl = +let rec intro_gen loc name_flag move_flag force_flag gl = match kind_of_term (pf_concl gl) with | Prod (name,t,_) -> - build_intro_tac (find_name (name,None,t) gl name_flag) move_flag gl + build_intro_tac (find_name loc (name,None,t) gl name_flag) move_flag gl | LetIn (name,b,t,_) -> - build_intro_tac (find_name (name,Some b,t) gl name_flag) move_flag gl + build_intro_tac (find_name loc (name,Some b,t) gl name_flag) move_flag + gl | _ -> if not force_flag then raise (RefinerError IntroNeedsProduct); try tclTHEN (reduce (Red true) onConcl) - (intro_gen name_flag move_flag force_flag) gl + (intro_gen loc name_flag move_flag force_flag) gl with Redelimination -> - errorlabstrm "Intro" (str "No product even after head-reduction") + user_err_loc(loc,"Intro",str "No product even after head-reduction.") -let intro_mustbe_force id = intro_gen (IntroMustBe id) None true -let intro_using id = intro_gen (IntroBasedOn (id,[])) None false -let intro_force force_flag = intro_gen (IntroAvoid []) None force_flag +let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true +let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false +let intro_force force_flag = intro_gen dloc (IntroAvoid []) no_move force_flag let intro = intro_force false let introf = intro_force true -let intro_avoiding l = intro_gen (IntroAvoid l) None false - -let introf_move_name destopt = intro_gen (IntroAvoid []) destopt true +let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false -(* For backwards compatibility *) -let central_intro = intro_gen +let introf_move_name destopt = intro_gen dloc (IntroAvoid []) destopt true (**** Multiple introduction tactics ****) let rec intros_using = function - [] -> tclIDTAC - | str::l -> tclTHEN (intro_using str) (intros_using l) + | [] -> tclIDTAC + | str::l -> tclTHEN (intro_using str) (intros_using l) let intros = tclREPEAT (intro_force false) let intro_erasing id = tclTHEN (thin [id]) (introduction id) +let rec get_next_hyp_position id = function + | [] -> error ("No such hypothesis: " ^ string_of_id id) + | (hyp,_,_) :: right -> + if hyp = id then + match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd true + else + get_next_hyp_position id right + +let intro_replacing id gl = + let next_hyp = get_next_hyp_position id (pf_hyps gl) in + tclTHENLIST [thin [id]; introduction id; move_hyp true id next_hyp] gl + let intros_replacing ids gl = let rec introrec = function | [] -> tclIDTAC | id::tl -> - (tclTHEN (tclORELSE (intro_replacing id) - (tclORELSE (intro_erasing id) (* ?? *) - (intro_using id))) - (introrec tl)) + tclTHEN (tclORELSE (intro_replacing id) (intro_using id)) + (introrec tl) in introrec ids gl (* User-level introduction tactics *) -let intro_move idopt idopt' = match idopt with - | None -> intro_gen (IntroAvoid []) idopt' true - | Some id -> intro_gen (IntroMustBe id) idopt' true +let intro_move idopt hto = match idopt with + | None -> intro_gen dloc (IntroAvoid []) hto true + | Some id -> intro_gen dloc (IntroMustBe id) hto true let pf_lookup_hypothesis_as_renamed env ccl = function | AnonHyp n -> pf_lookup_index_as_renamed env ccl n @@ -415,7 +457,8 @@ let depth_of_quantified_hypothesis red h gl = errorlabstrm "lookup_quantified_hypothesis" (str "No " ++ msg_quantified_hypothesis h ++ strbrk " in current goal" ++ - if red then strbrk " even after head-reduction" else mt ()) + (if red then strbrk " even after head-reduction" else mt ()) ++ + str".") let intros_until_gen red h g = tclDO (depth_of_quantified_hypothesis red h g) intro g @@ -434,7 +477,7 @@ let try_intros_until tac = function let rec intros_move = function | [] -> tclIDTAC | (hyp,destopt) :: rest -> - tclTHEN (intro_gen (IntroMustBe hyp) destopt false) + tclTHEN (intro_gen dloc (IntroMustBe hyp) destopt false) (intros_move rest) let dependent_in_decl a (_,c,t) = @@ -442,33 +485,6 @@ let dependent_in_decl a (_,c,t) = | None -> dependent a t | Some body -> dependent a body || dependent a t -let move_to_rhyp rhyp gl = - let rec get_lhyp lastfixed depdecls = function - | [] -> - (match rhyp with - | None -> lastfixed - | Some h -> anomaly ("Hypothesis should occur: "^ (string_of_id h))) - | (hyp,c,typ) as ht :: rest -> - if Some hyp = rhyp then - lastfixed - else if List.exists (occur_var_in_decl (pf_env gl) hyp) depdecls then - get_lhyp lastfixed (ht::depdecls) rest - else - get_lhyp (Some hyp) depdecls rest - in - let sign = pf_hyps gl in - let (hyp,c,typ as decl) = List.hd sign in - match get_lhyp None [decl] (List.tl sign) with - | None -> tclIDTAC gl - | Some hypto -> move_hyp true hyp hypto gl - -let rec intros_rmove = function - | [] -> tclIDTAC - | (hyp,destopt) :: rest -> - tclTHENLIST [ introduction hyp; - move_to_rhyp destopt; - intros_rmove rest ] - (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) @@ -515,7 +531,7 @@ let cut c gl = (internal_cut_rev id c) (tclTHEN (apply_type t [mkVar id]) (thin [id])) gl - | _ -> error "Not a proposition or a type" + | _ -> error "Not a proposition or a type." let cut_intro t = tclTHENFIRST (cut t) intro @@ -529,9 +545,7 @@ let cut_intro t = tclTHENFIRST (cut t) intro (* 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)) ] + tclTHENS (cut t) [ intro_replacing id; tac (refine_no_check (mkVar id)) ] let cut_in_parallel l = let rec prec = function @@ -543,7 +557,7 @@ let cut_in_parallel l = let error_uninstantiated_metas t clenv = let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" - in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id) + in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") let clenv_refine_in with_evars id clenv gl = let clenv = clenv_pose_dependent_evars with_evars clenv in @@ -577,7 +591,7 @@ let elimination_clause_scheme with_evars allow_K elimclause indclause gl = (match kind_of_term (last_arg elimclause.templval.rebus) with | Meta mv -> mv | _ -> errorlabstrm "elimination_clause" - (str "The type of elimination clause is not well-formed")) + (str "The type of elimination clause is not well-formed.")) in let elimclause' = clenv_fchain indmv elimclause indclause in res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags @@ -643,22 +657,28 @@ let simplest_elim c = default_elim false (c,NoBindings) (e.g. it could replace id:A->B->C by id:C, knowing A/\B) *) +let clenv_fchain_in id elim_flags mv elimclause hypclause = + try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause + with PretypeError (env,NoOccurrenceFound (op,_)) -> + (* Set the hypothesis name in the message *) + raise (PretypeError (env,NoOccurrenceFound (op,Some id))) + let elimination_in_clause_scheme with_evars id elimclause indclause gl = let (hypmv,indmv) = match clenv_independent elimclause with [k1;k2] -> (k1,k2) | _ -> errorlabstrm "elimination_clause" - (str "The type of elimination clause is not well-formed") in + (str "The type of elimination clause is not well-formed.") in 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 elimclause'' = - clenv_fchain ~allow_K:false ~flags:elim_flags hypmv elimclause' hypclause in + let elimclause'' = + clenv_fchain_in id elim_flags hypmv elimclause' hypclause in let new_hyp_typ = clenv_type elimclause'' in if eq_constr hyp_typ new_hyp_typ then errorlabstrm "general_rewrite_in" - (str "Nothing to rewrite in " ++ pr_id id); + (str "Nothing to rewrite in " ++ pr_id id ++ str"."); clenv_refine_in with_evars id elimclause'' gl let general_elim_in with_evars id = @@ -688,6 +708,13 @@ let simplest_case c = general_case_analysis false (c,NoBindings) (* Resolution tactics *) (****************************************************) +let resolve_classes gl = + let env = pf_env gl and evd = project gl in + if evd = Evd.empty then tclIDTAC gl + else + let evd' = Typeclasses.resolve_typeclasses env (Evd.create_evar_defs evd) in + (tclTHEN (tclEVARS (Evd.evars_of evd')) tclNORMEVAR) gl + (* Resolution with missing arguments *) let general_apply with_delta with_destruct with_evars (c,lbind) gl = @@ -701,7 +728,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = let thm_ty0 = nf_betaiota (pf_type_of gl c) in let try_apply thm_ty nprod = let n = nb_prod thm_ty - nprod in - if n<0 then error "Apply: theorem has not enough premisses."; + if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in try try_apply thm_ty0 concl_nprod @@ -744,16 +771,22 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl = try_red_apply thm_ty0 in try_main_apply c gl -let apply_with_ebindings_gen b = general_apply b b +let rec apply_with_ebindings_gen b e = function + | [] -> + tclIDTAC + | [cb] -> + general_apply b b e cb + | cb::cbl -> + tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl) -let apply_with_ebindings = apply_with_ebindings_gen false false -let eapply_with_ebindings = apply_with_ebindings_gen false true +let apply_with_ebindings cb = apply_with_ebindings_gen false false [cb] +let eapply_with_ebindings cb = apply_with_ebindings_gen false true [cb] let apply_with_bindings (c,bl) = apply_with_ebindings (c,inj_ebindings bl) let eapply_with_bindings (c,bl) = - apply_with_ebindings_gen false true (c,inj_ebindings bl) + apply_with_ebindings_gen false true [c,inj_ebindings bl] let apply c = apply_with_ebindings (c,NoBindings) @@ -788,10 +821,10 @@ let find_matching_clause unifier clause = let progress_with_clause innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in - if ordered_metas = [] then error "Statement without assumptions"; + 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" + with Failure _ -> error "Unable to unify." let apply_in_once gl innerclause (d,lbind) = let thm = nf_betaiota (pf_type_of gl d) in @@ -832,7 +865,7 @@ let cut_and_apply c gl = 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" + | _ -> error "lapply needs a non-dependent product." (********************************************************************) (* Exact tactics *) @@ -844,7 +877,7 @@ let exact_check c gl = if pf_conv_x_leq gl ct concl then refine_no_check c gl else - error "Not an exact proof" + error "Not an exact proof." let exact_no_check = refine_no_check @@ -863,7 +896,7 @@ let (assumption : tactic) = fun gl -> let hyps = pf_hyps gl in let rec arec only_eq = function | [] -> - if only_eq then arec false hyps else error "No such assumption" + if only_eq then arec false hyps else error "No such assumption." | (id,c,t)::rest -> if (only_eq & eq_constr t concl) or (not only_eq & pf_conv_x_leq gl t concl) @@ -881,11 +914,20 @@ let (assumption : tactic) = fun gl -> * subsequently used in other hypotheses or in the conclusion of the * goal. *) -let clear ids gl = (* avant seul dyn_clear n'echouait pas en [] *) - if ids=[] then tclIDTAC gl else with_check (thin ids) gl +let clear ids = (* avant seul dyn_clear n'echouait pas en [] *) + if ids=[] then tclIDTAC else thin ids let clear_body = thin_body +let clear_wildcards ids = + tclMAP (fun (loc,id) gl -> + try with_check (Tacmach.thin_no_check [id]) gl + with ClearDependencyError (id,err) -> + (* Intercept standard [thin] error message *) + Stdpp.raise_with_loc loc + (error_clear_dependency (pf_env gl) (id_of_string "_") err)) + ids + (* Takes a list of booleans, and introduces all the variables * quantified in the goal which are associated with a value * true in the boolean list. *) @@ -919,17 +961,17 @@ let specialize mopt (c,lbind) g = let term = applist(thd,tstack) in if occur_meta term then errorlabstrm "" (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas term)))); + pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ + str "."); Some (evars_of clause.evd), term in tclTHEN (match evars with Some e -> tclEVARS e | _ -> tclIDTAC) - (match kind_of_term (fst (decompose_app c)) with - | Var id when List.exists (fun (i,_,_)-> i=id) (pf_hyps g) -> - let id' = fresh_id [] id g in - tclTHENS (fun g -> internal_cut id' (pf_type_of g term) g) - [ exact_no_check term; - tclTHEN (clear [id]) (rename_hyp [id',id]) ] + (match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with + | Var id when List.mem id (pf_ids_of_hyps g) -> + tclTHENFIRST + (fun g -> internal_cut_replace id (pf_type_of g term) g) + (exact_no_check term) | _ -> tclTHENLAST (fun g -> cut (pf_type_of g term) g) (exact_no_check term)) @@ -955,14 +997,14 @@ let keep hyps gl = (************************) let check_number_of_constructors expctdnumopt i nconstr = - if i=0 then error "The constructors are numbered starting from 1"; + if i=0 then error "The constructors are numbered starting from 1."; begin match expctdnumopt with | Some n when n <> nconstr -> error ("Not an inductive goal with "^ - string_of_int n^plural n " constructor") + string_of_int n^plural n " constructor"^".") | _ -> () end; - if i > nconstr then error "Not enough constructors" + if i > nconstr then error "Not enough constructors." let constructor_tac with_evars expctdnumopt i lbind gl = let cl = pf_concl gl in @@ -987,7 +1029,7 @@ let any_constructor with_evars tacopt gl = let mind = fst (pf_reduce_to_quantified_ind gl (pf_concl gl)) in let nconstr = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in - if nconstr = 0 then error "The type has no constructors"; + if nconstr = 0 then error "The type has no constructors."; tclFIRST (List.map (fun i -> tclTHEN (constructor_tac with_evars None i NoBindings) t) @@ -1025,22 +1067,33 @@ let fix_empty_case nv l = and "[ ]" for no clause at all; so we are a bit liberal here *) if Array.length nv = 0 & l = [[]] then [] else l -let intro_or_and_pattern ll l' tac = +let error_unexpected_extra_pattern loc nb pat = + let s1,s2,s3 = match pat with + | IntroIdentifier _ -> "name", (plural nb " introduction pattern"), "no" + | _ -> "introduction pattern", "", "none" in + user_err_loc (loc,"",str "Unexpected " ++ str s1 ++ str " (" ++ + (if nb = 0 then (str s3 ++ str s2) else + (str "at most " ++ int nb ++ str s2)) ++ spc () ++ + str (if nb = 1 then "was" else "were") ++ + strbrk " expected in the branch).") + +let intro_or_and_pattern loc b ll l' tac = tclLAST_HYP (fun c gl -> let ind,_ = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in let nv = mis_constr_nargs ind in - let rec adjust_names_length tail n = function - | [] when n = 0 or tail -> [] - | [] -> IntroAnonymous :: adjust_names_length tail (n-1) [] - | _ :: _ as l when n = 0 -> - if tail then l else error "Too many names in some branch" - | ip :: l -> ip :: adjust_names_length tail (n-1) l in + let bracketed = b or not (l'=[]) in + let rec adjust_names_length nb n = function + | [] when n = 0 or not bracketed -> [] + | [] -> (dloc,IntroAnonymous) :: adjust_names_length nb (n-1) [] + | (loc',pat) :: _ as l when n = 0 -> + if bracketed then error_unexpected_extra_pattern loc' nb pat; + l + | ip :: l -> ip :: adjust_names_length nb (n-1) l in let ll = fix_empty_case nv ll in - if List.length ll <> Array.length nv then - error "Not the right number of patterns"; + check_or_and_pattern_size loc ll (Array.length nv); tclTHENLASTn (tclTHEN case_last clear_last) - (array_map2 (fun n l -> tac ((adjust_names_length (l'=[]) n l)@l')) + (array_map2 (fun n l -> tac ((adjust_names_length n n l)@l')) nv (Array.of_list ll)) gl) @@ -1052,11 +1105,11 @@ let clear_if_atomic l2r id gl = else tclIDTAC gl let rec explicit_intro_names = function -| IntroIdentifier id :: l -> +| (_, IntroIdentifier id) :: l -> id :: explicit_intro_names l -| (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _) :: l -> +| (_, (IntroWildcard | IntroAnonymous | IntroFresh _ | IntroRewrite _)) :: l -> explicit_intro_names l -| IntroOrAndPattern ll :: l' -> +| (_, IntroOrAndPattern ll) :: l' -> List.flatten (List.map (fun l -> explicit_intro_names (l@l')) ll) | [] -> [] @@ -1065,84 +1118,90 @@ let rec explicit_intro_names = function to ensure that dependent hypotheses are cleared in the right dependency order (see bug #1000); we use fresh names, not used in the tactic, for the hyps to clear *) -let rec intros_patterns avoid thin destopt = function - | IntroWildcard :: l -> +let rec intros_patterns b avoid thin destopt = function + | (loc, IntroWildcard) :: l -> tclTHEN - (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true) + (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true) (onLastHyp (fun id -> tclORELSE - (tclTHEN (clear [id]) (intros_patterns avoid thin destopt l)) - (intros_patterns avoid (id::thin) destopt l))) - | IntroIdentifier id :: l -> + (tclTHEN (clear [id]) (intros_patterns b avoid thin destopt l)) + (intros_patterns b avoid ((loc,id)::thin) destopt l))) + | (loc, IntroIdentifier id) :: l -> tclTHEN - (intro_gen (IntroMustBe id) destopt true) - (intros_patterns avoid thin destopt l) - | IntroAnonymous :: l -> + (intro_gen loc (IntroMustBe id) destopt true) + (intros_patterns b avoid thin destopt l) + | (loc, IntroAnonymous) :: l -> tclTHEN - (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) destopt true) - (intros_patterns avoid thin destopt l) - | IntroFresh id :: l -> + (intro_gen loc (IntroAvoid (avoid@explicit_intro_names l)) + destopt true) + (intros_patterns b avoid thin destopt l) + | (loc, IntroFresh id) :: l -> tclTHEN - (intro_gen (IntroBasedOn (id, avoid@explicit_intro_names l)) destopt true) - (intros_patterns avoid thin destopt l) - | IntroOrAndPattern ll :: l' -> + (intro_gen loc (IntroBasedOn (id, avoid@explicit_intro_names l)) + destopt true) + (intros_patterns b avoid thin destopt l) + | (loc, IntroOrAndPattern ll) :: l' -> tclTHEN introf - (intro_or_and_pattern ll l' (intros_patterns avoid thin destopt)) - | IntroRewrite l2r :: l -> + (intro_or_and_pattern loc b ll l' + (intros_patterns b avoid thin destopt)) + | (loc, IntroRewrite l2r) :: l -> tclTHEN - (intro_gen (IntroAvoid (avoid@explicit_intro_names l)) None true) + (intro_gen loc (IntroAvoid(avoid@explicit_intro_names l)) no_move true) (onLastHyp (fun id -> tclTHENLIST [ !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses; clear_if_atomic l2r id; - intros_patterns avoid thin destopt l ])) - | [] -> clear thin + intros_patterns b avoid thin destopt l ])) + | [] -> clear_wildcards thin -let intros_pattern = intros_patterns [] [] +let intros_pattern = intros_patterns false [] [] -let intro_pattern destopt pat = intros_patterns [] [] destopt [pat] +let intro_pattern destopt pat = intros_patterns false [] [] destopt [dloc,pat] let intro_patterns = function | [] -> tclREPEAT intro - | l -> intros_pattern None l + | l -> intros_pattern no_move l (**************************) (* Other cut tactics *) (**************************) -let hid = id_of_string "H" -let xid = id_of_string "X" +let make_id s = fresh_id [] (default_id_of_sort s) -let make_id s = fresh_id [] (match s with Prop _ -> hid | Type _ -> xid) - -let prepare_intros s ipat gl = match ipat with +let prepare_intros s (loc,ipat) gl = match ipat with + | IntroIdentifier id -> id, tclIDTAC | IntroAnonymous -> make_id s gl, tclIDTAC | IntroFresh id -> fresh_id [] id gl, tclIDTAC - | IntroWildcard -> let id = make_id s gl in id, thin [id] - | IntroIdentifier id -> id, tclIDTAC + | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id] | IntroRewrite l2r -> let id = make_id s gl in id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allClauses | IntroOrAndPattern ll -> make_id s gl, - (tclTHENS - (tclTHEN case_last clear_last) - (List.map (intros_pattern None) ll)) + intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) let ipat_of_name = function | Anonymous -> IntroAnonymous | Name id -> IntroIdentifier id +let allow_replace c gl = function (* A rather arbitrary condition... *) + | _, IntroIdentifier id -> + fst (decompose_app (snd (decompose_lam_assum c))) = mkVar id + | _ -> + false + let assert_as first ipat c gl = match kind_of_term (hnf_type_of gl c) with | Sort s -> let id,tac = prepare_intros s ipat gl in - tclTHENS ((if first then internal_cut else internal_cut_rev) id c) + let repl = allow_replace c gl ipat in + tclTHENS + ((if first then internal_cut_gen else internal_cut_rev_gen) repl id c) (if first then [tclIDTAC; tac] else [tac; tclIDTAC]) gl - | _ -> error "Not a proposition or a type" + | _ -> error "Not a proposition or a type." -let assert_tac first na = assert_as first (ipat_of_name na) +let assert_tac first na = assert_as first (dloc,ipat_of_name na) let true_cut = assert_tac true (**************************) @@ -1341,7 +1400,8 @@ let letin_abstract id c occs gl = let ccl = match occurrences_of_goal occs with | None -> pf_concl gl | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in - let lastlhyp = if depdecls = [] then None else Some(pi1(list_last depdecls)) in + let lastlhyp = + if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in (depdecls,lastlhyp,ccl) let letin_tac with_eq name c occs gl = @@ -1349,23 +1409,29 @@ let letin_tac with_eq name c occs gl = let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in if name = Anonymous then fresh_id [] x gl else if not (mem_named_context x (pf_hyps gl)) then x else - error ("The variable "^(string_of_id x)^" is already declared") in + error ("The variable "^(string_of_id x)^" is already declared.") in let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in let t = pf_type_of gl c in let newcl,eq_tac = match with_eq with - | Some lr -> - let heq = fresh_id [] (add_prefix "Heq" id) gl in + | Some (lr,(loc,ido)) -> + let heq = match ido with + | IntroAnonymous -> fresh_id [id] (add_prefix "Heq" id) gl + | IntroFresh heq_base -> fresh_id [id] heq_base gl + | IntroIdentifier id -> id + | _ -> error"Expect an introduction pattern naming one hypothesis." in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in let eq = applist (eqdata.eq,args) in let refl = applist (eqdata.refl, [t;mkVar id]) in mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)), - tclTHEN (intro_gen (IntroMustBe heq) lastlhyp true) (thin_body [heq;id]) + tclTHEN + (intro_gen loc (IntroMustBe heq) lastlhyp true) + (thin_body [heq;id]) | None -> mkNamedLetIn id c t ccl, tclIDTAC in tclTHENLIST [ convert_concl_no_check newcl DEFAULTcast; - intro_gen (IntroMustBe id) lastlhyp true; + intro_gen dloc (IntroMustBe id) lastlhyp true; eq_tac; tclMAP convert_hyp_no_check depdecls ] gl @@ -1390,7 +1456,7 @@ let unfold_body x gl = match Sign.lookup_named x hyps with (_,Some xval,_) -> xval | _ -> errorlabstrm "unfold_body" - (pr_id x ++ str" is not a defined hypothesis") in + (pr_id x ++ str" is not a defined hypothesis.") in let aft = afterHyp x gl in let hl = List.fold_right (fun (y,yval,_) cl -> (([],y),InHyp) :: cl) aft [] in let xvar = mkVar x in @@ -1445,76 +1511,85 @@ let unfold_all x gl = let check_unused_names names = if names <> [] & Flags.is_verbose () then - let s = if List.tl names = [] then " " else "s " in msg_warning - (str"Unused introduction pattern" ++ str s ++ - str": " ++ prlist_with_sep spc pr_intro_pattern names) - -let rec first_name_buggy = function - | IntroOrAndPattern [] -> None - | IntroOrAndPattern ([]::l) -> first_name_buggy (IntroOrAndPattern l) - | IntroOrAndPattern ((p::_)::_) -> first_name_buggy p - | IntroWildcard -> None - | IntroRewrite _ -> None - | IntroIdentifier id -> Some id + (str"Unused introduction " ++ str (plural (List.length names) "pattern") + ++ str": " ++ prlist_with_sep spc pr_intro_pattern names) + +let rec first_name_buggy avoid gl (loc,pat) = match pat with + | IntroOrAndPattern [] -> no_move + | IntroOrAndPattern ([]::l) -> + first_name_buggy avoid gl (loc,IntroOrAndPattern l) + | IntroOrAndPattern ((p::_)::_) -> first_name_buggy avoid gl p + | IntroWildcard -> no_move + | IntroRewrite _ -> no_move + | IntroIdentifier id -> MoveAfter id | IntroAnonymous | IntroFresh _ -> assert false let consume_pattern avoid id gl = function - | [] -> (IntroIdentifier (fresh_id avoid id gl), []) - | IntroAnonymous::names -> + | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), []) + | (loc,IntroAnonymous)::names -> + let avoid = avoid@explicit_intro_names names in + ((loc,IntroIdentifier (fresh_id avoid id gl)), names) + | (loc,IntroFresh id')::names -> let avoid = avoid@explicit_intro_names names in - (IntroIdentifier (fresh_id avoid id gl), names) + ((loc,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 + List.map (function (hyp,MoveToEnd true) -> (hyp,tophyp) | x -> x) lstatus + in tclTHEN - (intros_rmove rstatus) + (intros_move rstatus) (intros_move newlstatus) +let update destopt tophyp = if destopt = no_move then tophyp else destopt + type elim_arg_kind = RecArg | IndArg | OtherArg let induct_discharge statuslists destopt avoid' (avoid,ra) names gl = let avoid = avoid @ avoid' in - let rec peel_tac ra names tophyp 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 - | [IntroIdentifier id as pat] -> - let id = next_ident_away (add_prefix "IH" id) avoid in - (pat, [IntroIdentifier id]) + | [loc,IntroIdentifier id as pat] -> + let id' = next_ident_away (add_prefix "IH" id) avoid in + (pat, [dloc, IntroIdentifier id']) | _ -> consume_pattern avoid recvarname gl names in let hyprec,names = consume_pattern avoid hyprecname gl names in (* 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 + let newtophyp = + if tophyp=no_move then first_name_buggy avoid gl hyprec else tophyp + in tclTHENLIST - [ intros_patterns avoid [] destopt [recpat]; - intros_patterns avoid [] None [hyprec]; - peel_tac ra' names tophyp] gl + [ intros_patterns true avoid [] (update destopt tophyp) [recpat]; + intros_patterns true avoid [] no_move [hyprec]; + peel_tac ra' names newtophyp] 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]) + tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [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]) + tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat]) (peel_tac ra' names tophyp) gl | (OtherArg,_) :: ra' -> let pat,names = match names with - | [] -> IntroAnonymous, [] + | [] -> (dloc, IntroAnonymous), [] | pat::names -> pat,names in - tclTHEN (intros_patterns avoid [] destopt [pat]) + tclTHEN (intros_patterns true avoid [] (update destopt tophyp) [pat]) (peel_tac ra' names tophyp) gl | [] -> check_unused_names names; re_intro_dependent_hypotheses tophyp statuslists gl in - peel_tac ra names None gl + peel_tac ra names no_move 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 @@ -1572,7 +1647,7 @@ let find_atomic_param_of_ind nparams indtyp = Idset.elements !indvars; - (* [cook_sign] builds the lists [indhyps] of hyps that must be +(* [cook_sign] builds the lists [indhyps] of hyps that must be erased, the lists of hyps to be generalize [(hdeps,tdeps)] on the goal together with the places [(lstatus,rstatus)] where to re-intro them after induction. To know where to re-intro the dep hyp, we @@ -1583,7 +1658,7 @@ let find_atomic_param_of_ind nparams indtyp = more ancient (on the right) to more recent hyp (on the left) but the computation of [lhyp] progresses from the other way, [cook_hyp] is in two passes (an alternative would have been to write an - higher-order algorithm). We strongly use references to reduce + higher-order algorithm). We use references to reduce the accumulation of arguments. To summarize, the situation looks like this @@ -1635,7 +1710,7 @@ let find_atomic_param_of_ind nparams indtyp = *) -exception Shunt of identifier option +exception Shunt of identifier move_location let cook_sign hyp0_opt indvars_init env = let hyp0,indvars = @@ -1657,7 +1732,7 @@ let cook_sign hyp0_opt indvars_init env = (* If there was no main induction hypotheses, then hyp is one of indvars too, so add it to indhyps. *) (if hyp0_opt=None then indhyps := hyp::!indhyps); - None (* fake value *) + MoveToEnd false (* fake value *) end else if List.mem hyp indvars then begin (* warning: hyp can still occur after induction *) (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *) @@ -1673,11 +1748,11 @@ let cook_sign hyp0_opt indvars_init env = rstatus := (hyp,rhyp)::!rstatus else ldeps := hyp::!ldeps; (* status computed in 2nd phase *) - Some hyp end + MoveBefore hyp end else - Some hyp + MoveBefore hyp in - let _ = fold_named_context seek_deps env ~init:None in + let _ = fold_named_context seek_deps env ~init:(MoveToEnd false) in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp (hyp,_,_) = if hyp = hyp0 then raise (Shunt lhyp); @@ -1685,15 +1760,16 @@ let cook_sign hyp0_opt indvars_init env = lstatus := (hyp,lhyp)::!lstatus; lhyp end else - if List.mem hyp !indhyps then lhyp else (Some hyp) + if List.mem hyp !indhyps then lhyp else MoveAfter hyp in try - let _ = fold_named_context_reverse compute_lstatus ~init:None env in -(* anomaly "hyp0 not found" *) - raise (Shunt (None)) (* ?? FIXME *) + let _ = + fold_named_context_reverse compute_lstatus ~init:(MoveToEnd true) env in + raise (Shunt (MoveToEnd true)) (* ?? FIXME *) with Shunt lhyp0 -> let statuslists = (!lstatus,List.rev !rstatus) in - (statuslists, (if hyp0_opt=None then None else lhyp0) , !indhyps, !decldeps) + (statuslists, (if hyp0_opt=None then MoveToEnd true else lhyp0), + !indhyps, !decldeps) (* @@ -1764,7 +1840,7 @@ let empty_scheme = hypothesis on which the induction is made *) let induction_tac with_evars (varname,lbind) typ scheme gl = let elimc,lbindelimc = - match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in + match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in let elimt = scheme.elimt in let indclause = make_clenv_binding gl (mkVar varname,typ) lbind in let elimclause = @@ -1779,9 +1855,9 @@ let make_base n id = (* digits *) id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0))) -(* Builds tw different names from an optional inductive type and a +(* Builds two different names from an optional inductive type and a number, also deals with a list of names to avoid. If the inductive - type is None, then hyprecname is HIi where i is a number. *) + type is None, then hyprecname is IHi where i is a number. *) let make_up_names n ind_opt cname = let is_hyp = atompart_of_id cname = "H" in let base = string_of_id (make_base n cname) in @@ -1825,7 +1901,7 @@ let chop_context n l = let error_ind_scheme s = let s = if s <> "" then s^" " else s in - error ("Cannot recognise "^s^"an induction schema") + error ("Cannot recognize "^s^"an induction scheme.") let mkEq t x y = mkApp (build_coq_eq (), [| t; x; y |]) @@ -1950,29 +2026,23 @@ let abstract_args gl id = dep, succ (List.length ctx), vars) | _ -> None -let abstract_generalize id gl = +let abstract_generalize id ?(generalize_vars=true) gl = Coqlib.check_required_library ["Coq";"Logic";"JMeq"]; -(* let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string "Coq.Logic.JMeq")) in *) -(* Library.require_library [qualid] None; *) let oldid = pf_get_new_id id gl in let newc = abstract_args gl id in match newc with | None -> tclIDTAC gl | Some (newc, dep, n, vars) -> - if dep then - tclTHENLIST [refine newc; - rename_hyp [(id, oldid)]; - tclDO n intro; - generalize_dep (mkVar oldid); - tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars] - gl - else - tclTHENLIST [refine newc; - clear [id]; - tclDO n intro; - tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars] - gl - + let tac = + if dep then + tclTHENLIST [refine newc; rename_hyp [(id, oldid)]; tclDO n intro; + generalize_dep (mkVar oldid)] + else + tclTHENLIST [refine newc; clear [id]; tclDO n intro] + in + if generalize_vars then + tclTHEN tac (tclMAP (fun id -> tclTRY (generalize_dep (mkVar id))) vars) gl + else tac gl let occur_rel n c = let res = not (noccurn n c) in @@ -2016,11 +2086,11 @@ let cut_list n l = res -(* This functions splits the products of the induction scheme [elimt] in three +(* This function splits the products of the induction scheme [elimt] into four parts: - - branches, easily detectable (they are not referred by rels in the subterm) - - what was found before branches (acc1) that is: parameters and predicates - - what was found after branches (acc3) that is: args and indarg if any + - branches, easily detectable (they are not referred by rels in the subterm) + - what was found before branches (acc1) that is: parameters and predicates + - what was found after branches (acc3) that is: args and indarg if any if there is no branch, we try to fill in acc3 with args/indargs. We also return the conclusion. *) @@ -2033,13 +2103,13 @@ let decompose_paramspred_branch_args elimt = then cut_noccur elimt' ((nme,None,tpe)::acc2) else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl | App(_, _) | Rel _ -> acc2 , [] , elimt - | _ -> error "cannot recognise an induction schema" in + | _ -> error_ind_scheme "" in let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types = match kind_of_term elimt with | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1) | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl | App(_, _) | Rel _ -> acc1,[],[],elimt - | _ -> error "cannot recognise an induction schema" in + | _ -> error_ind_scheme "" in let acc1, acc2 , acc3, ccl = cut_occur elimt [] in (* Particular treatment when dealing with a dependent empty type elim scheme: if there is no branch, then acc1 contains all hyps which is wrong (acc1 @@ -2053,8 +2123,7 @@ let decompose_paramspred_branch_args elimt = let hd_ccl_pred,_ = decompose_app ccl in match kind_of_term hd_ccl_pred with | Rel i -> let acc3,acc1 = cut_list (i-1) hyps in acc1 , [] , acc3 , ccl - | _ -> error "cannot recognize an induction schema" - + | _ -> error_ind_scheme "" let exchange_hd_app subst_hd t = @@ -2064,7 +2133,7 @@ let exchange_hd_app subst_hd t = (* [rebuild_elimtype_from_scheme scheme] rebuilds the type of an eliminator from its [scheme_info]. The idea is to build variants of - eliminator by modifying there scheme_info, then rebuild the + eliminator by modifying their scheme_info, then rebuild the eliminator type, then prove it (with tactics). *) let rebuild_elimtype_from_scheme (scheme:elim_scheme): types = let hiconcl = @@ -2081,7 +2150,7 @@ let rebuild_elimtype_from_scheme (scheme:elim_scheme): types = exception NoLastArg exception NoLastArgCcl -(* Builds an elim_scheme frome its type and calling form (const+binding) We +(* Builds an elim_scheme from its type and calling form (const+binding). We first separate branches. We obtain branches, hyps before (params + preds), hyps after (args <+ indarg if present>) and conclusion. Then we proceed as follows: @@ -2131,7 +2200,7 @@ let compute_elim_sig ?elimc elimt = (* 3- Look at last arg: is it the indarg? *) ignore ( match List.hd args_indargs with - | hiname,Some _,hi -> error "cannot recognize an induction schema" + | hiname,Some _,hi -> error_ind_scheme "" | hiname,None,hi -> let hi_ind, hi_args = decompose_app hi in let hi_is_ind = (* hi est d'un type globalisable *) @@ -2156,11 +2225,11 @@ let compute_elim_sig ?elimc elimt = with Exit -> (* Ending by computing indrev: *) match !res.indarg with | None -> !res (* No indref *) - | Some ( _,Some _,_) -> error "Cannot recognise an induction scheme" + | Some ( _,Some _,_) -> error_ind_scheme "" | Some ( _,None,ind) -> let indhd,indargs = decompose_app ind in try {!res with indref = Some (global_of_constr indhd) } - with _ -> error "Cannot find the inductive type of the inductive schema";; + with _ -> error "Cannot find the inductive type of the inductive scheme.";; (* Check that the elimination scheme has a form similar to the elimination schemes built by Coq. Schemes may have the standard @@ -2169,17 +2238,17 @@ let compute_elim_sig ?elimc elimt = extra final argument of the form (f x y ...) in the conclusion. In the non standard case, naming of generated hypos is slightly different. *) -let compute_elim_signature elimc elimt names_info = +let compute_elim_signature elimc elimt names_info ind_type_guess = let scheme = compute_elim_sig ~elimc:elimc elimt in let f,l = decompose_app scheme.concl in (* Vérifier que les arguments de Qi sont bien les xi. *) match scheme.indarg with - | Some (_,Some _,_) -> error "strange letin, cannot recognize an induction schema" + | Some (_,Some _,_) -> error "Strange letin, cannot recognize an induction scheme." | None -> (* Non standard scheme *) - let npred = List.length scheme.predicates in let is_pred n c = let hd = fst (decompose_app c) in match kind_of_term hd with - | Rel q when n < q & q <= n+npred -> IndArg + | Rel q when n < q & q <= n+scheme.npredicates -> IndArg + | _ when hd = ind_type_guess & not scheme.farg_in_concl -> RecArg | _ -> OtherArg in let rec check_branch p c = match kind_of_term c with @@ -2208,10 +2277,9 @@ let compute_elim_signature elimc elimt names_info = | Some ( _,None,ind) -> (* Standard scheme from an inductive type *) let indhd,indargs = decompose_app ind in - let npred = List.length scheme.predicates in let is_pred n c = let hd = fst (decompose_app c) in match kind_of_term hd with - | Rel q when n < q & q <= n+npred -> IndArg + | Rel q when n < q & q <= n+scheme.npredicates -> IndArg | _ when hd = indhd -> RecArg | _ -> OtherArg in let rec check_branch p c = match kind_of_term c with @@ -2242,7 +2310,7 @@ let compute_elim_signature elimc elimt names_info = list_lastn scheme.nargs indargs = extended_rel_list 0 scheme.args in if not (ccl_arg_ok & ind_is_ok) then - error "Cannot recognize the conclusion of an induction schema"; + error_ind_scheme "the conclusion of"; [] in let indsign = Array.of_list (find_branches 0 (List.rev scheme.branches)) in @@ -2251,7 +2319,7 @@ let compute_elim_signature elimc elimt names_info = let find_elim_signature isrec elim hyp0 gl = let tmptyp0 = pf_get_hyp_typ gl hyp0 in - let (elimc,elimt) = match elim with + let (elimc,elimt),ind = match elim with | None -> let mind,_ = pf_reduce_to_quantified_ind gl tmptyp0 in let s = elimination_sort_of_goal gl in @@ -2259,21 +2327,15 @@ let find_elim_signature isrec elim hyp0 gl = if isrec then lookup_eliminator mind s else pf_apply make_case_gen gl mind s in let elimt = pf_type_of gl elimc in - ((elimc, NoBindings), elimt) - | Some (elimc,lbind as e) -> - (e, pf_type_of gl elimc) in - let indsign,elim_scheme = compute_elim_signature elimc elimt hyp0 in + ((elimc, NoBindings), elimt), mkInd mind + | Some (elimc,lbind as e) -> + let ind_type_guess,_ = decompose_app (snd (decompose_prod tmptyp0)) in + (e, pf_type_of gl elimc), ind_type_guess in + let indsign,elim_scheme = + compute_elim_signature elimc elimt hyp0 ind in (indsign,elim_scheme) -let mapi f l = - let rec mapi_aux f i l = - match l with - | [] -> [] - | e::l' -> f e i :: mapi_aux f (i+1) l' in - mapi_aux f 0 l - - (* Instantiate all meta variables of elimclause using lid, some elts of lid are parameters (first ones), the other are arguments. Returns the clause obtained. *) @@ -2285,19 +2347,20 @@ let recolle_clenv scheme lid elimclause gl = match kind_of_term x with | Meta mv -> mv | _ -> errorlabstrm "elimination_clause" - (str "The type of elimination clause is not well-formed")) + (str "The type of the elimination clause is not well-formed.")) arr in let nmv = Array.length lindmv in let lidparams,lidargs = cut_list (scheme.nparams) lid in let nidargs = List.length lidargs in (* parameters correspond to first elts of lid. *) let clauses_params = - mapi (fun id i -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i)) lidparams in + list_map_i (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(i)) + 0 lidparams in (* arguments correspond to last elts of lid. *) let clauses_args = - mapi - (fun id i -> mkVar id , pf_get_hyp_typ gl id , lindmv.(nmv-nidargs+i)) - lidargs in + list_map_i + (fun i id -> mkVar id , pf_get_hyp_typ gl id , lindmv.(nmv-nidargs+i)) + 0 lidargs in let clause_indarg = match scheme.indarg with | None -> [] @@ -2321,10 +2384,10 @@ let recolle_clenv scheme lid elimclause gl = (elimc ?i ?j ?k...?l). This solves partly meta variables (and may produce new ones). Then refine with the resulting term with holes. *) -let induction_tac_felim with_evars indvars (* (elimc,lbindelimc) elimt *) scheme gl = +let induction_tac_felim with_evars indvars scheme gl = let elimt = scheme.elimt in let elimc,lbindelimc = - match scheme.elimc with | Some x -> x | None -> error "No definition of the principle" in + match scheme.elimc with | Some x -> x | None -> error "No definition of the principle." in (* elimclause contains this: (elimc ?i ?j ?k...?l) *) let elimclause = make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in @@ -2334,6 +2397,29 @@ let induction_tac_felim with_evars indvars (* (elimc,lbindelimc) elimt *) scheme let resolved = clenv_unique_resolver true elimclause' gl in clenv_refine with_evars resolved gl +let apply_induction_in_context isrec hyp0 indsign indvars names induct_tac gl = + let env = pf_env gl in + let statlists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in + let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in + let names = compute_induction_names (Array.length indsign) names in + let dephyps = List.map (fun (id,_,_) -> id) deps in + let deps_cstr = + List.fold_left + (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in + tclTHENLIST + [ + (* Generalize dependent hyps (but not args) *) + if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr; + (* clear dependent hyps *) + thin dephyps; + (* side-conditions in elim (resp case) schemes come last (resp first) *) + (if isrec then tclTHENFIRSTn else tclTHENLASTn) + (tclTHEN induct_tac (tclTRY (thin (List.rev indhyps)))) + (array_map2 + (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) + ] + gl + (* Induction with several induction arguments, main differences with induction_from_context is that there is no main induction argument, so we chose one to be the positioning reference. On the other hand, @@ -2348,8 +2434,7 @@ let induction_from_context_l isrec with_evars 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"; - let env = pf_env gl in + error "Not the right number of arguments given to induction scheme."; (* 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 induct. It is probably the first of them appearing in the @@ -2361,12 +2446,6 @@ let induction_from_context_l isrec with_evars elim_info lid names gl = let nargs_without_first = nargs_indarg_farg - 1 in let ivs,lp = cut_list nargs_without_first l in e, ivs, lp in - let statlists,lhyp0,indhyps,deps = cook_sign None (hyp0::indvars) env in - let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in - let names = compute_induction_names (Array.length indsign) names in - let dephyps = List.map (fun (id,_,_) -> id) deps in - let deps_cstr = - List.fold_left (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in (* terms to patternify we must patternify indarg or farg if present in concl *) let lid_in_pattern = if scheme.indarg <> None & not scheme.indarg_in_concl then List.rev indvars @@ -2375,68 +2454,32 @@ let induction_from_context_l isrec with_evars elim_info lid names gl = let realindvars = (* hyp0 is a real induction arg if it is not the farg in the conclusion of the induction scheme *) List.rev ((if scheme.farg_in_concl then indvars else hyp0::indvars) @ lid_params) in - (* Magistral effet de bord: comme dans induction_from_context. *) - tclTHENLIST - [ - (* Generalize dependent hyps (but not args) *) - if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr; - thin dephyps; (* clear dependent hyps *) - (* pattern to make the predicate appear. *) - reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; - (* FIXME: Tester ca avec un principe dependant et non-dependant *) - (if isrec then tclTHENFIRSTn else tclTHENLASTn) - (tclTHENLIST [ - (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all - possible holes using arguments given by the user (but the - functional one). *) - induction_tac_felim with_evars realindvars scheme; - tclTRY (thin (List.rev (indhyps))); - ]) - (array_map2 - (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) - ] - gl - - + let induct_tac = tclTHENLIST [ + (* pattern to make the predicate appear. *) + reduce (Pattern (List.map inj_with_occurrences lidcstr)) onConcl; + (* Induction by "refine (indscheme ?i ?j ?k...)" + resolution of all + possible holes using arguments given by the user (but the + functional one). *) + (* FIXME: Tester ca avec un principe dependant et non-dependant *) + induction_tac_felim with_evars realindvars scheme + ] in + apply_induction_in_context isrec + None indsign (hyp0::indvars) names induct_tac gl let induction_from_context isrec with_evars elim_info (hyp0,lbind) names gl = let indsign,scheme = elim_info in let indref = match scheme.indref with | None -> assert false | Some x -> x in let tmptyp0 = pf_get_hyp_typ gl hyp0 in let typ0 = pf_apply reduce_to_quantified_ref gl indref tmptyp0 in - - let env = pf_env gl in - let indvars = find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in - (* induction_from_context_l isrec elim_info (hyp0::List.rev indvars) names gl *) - let statlists,lhyp0,indhyps,deps = cook_sign (Some hyp0) indvars env in - let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in - let names = compute_induction_names (Array.length indsign) names in - let dephyps = List.map (fun (id,_,_) -> id) deps in - let deps_cstr = - List.fold_left - (fun a (id,b,_) -> if b = None then (mkVar id)::a else a) [] deps in - - (* Magistral effet de bord: si hyp0 a des arguments, ceux d'entre - eux qui ouvrent de nouveaux buts arrivent en premier dans la - liste des sous-buts du fait qu'ils sont le plus à gauche dans le - combinateur engendré par make_case_gen (un "Cases (hyp0 ?) of - ...") et il faut alors appliquer tclTHENLASTn; en revanche, - comme lookup_eliminator renvoie un combinateur de la forme - "ind_rec ... (hyp0 ?)", les buts correspondant à des arguments de - hyp0 sont maintenant à la fin et c'est tclTHENFIRSTn qui marche !!! *) - tclTHENLIST - [ if deps = [] then tclIDTAC else apply_type tmpcl deps_cstr; - thin dephyps; - (if isrec then tclTHENFIRSTn else tclTHENLASTn) - (tclTHENLIST - [ induction_tac with_evars (hyp0,lbind) typ0 scheme; - tclTHEN (tclTRY (unfold_body hyp0)) (thin [hyp0]); - tclTRY (thin indhyps) ]) - (array_map2 - (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) - ] - gl - + let indvars = + find_atomic_param_of_ind scheme.nparams (snd (decompose_prod typ0)) in + let induct_tac = tclTHENLIST [ + induction_tac with_evars (hyp0,lbind) typ0 scheme; + tclTRY (unfold_body hyp0); + thin [hyp0] + ] in + apply_induction_in_context isrec + (Some hyp0) indsign indvars names induct_tac gl exception TryNewInduct of exn @@ -2466,20 +2509,25 @@ let induction_without_atomization isrec with_evars elim names lid gl = in let nlid = List.length lid in if nlid <> awaited_nargs - then error "Not the right number of induction arguments" + then error "Not the right number of induction arguments." else induction_from_context_l isrec with_evars elim_info lid names gl -let new_induct_gen isrec with_evars elim names (c,lbind) cls gl = +let new_induct_gen isrec with_evars elim (eqname,names) (c,lbind) cls gl = match kind_of_term c with | Var id when not (mem_named_context id (Global.named_context())) - & lbind = NoBindings & not with_evars & cls = None -> + & lbind = NoBindings & not with_evars & cls = None + & eqname = None -> induction_with_atomization_of_ind_arg isrec with_evars elim names (id,lbind) gl | _ -> let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) Anonymous in let id = fresh_id [] x gl in - let with_eq = if cls <> None then Some (not (isVar c)) else None in + let with_eq = + match eqname with + | Some eq -> Some (false,eq) + | _ -> + if cls <> None then Some (false,(dloc,IntroAnonymous)) else None in tclTHEN (letin_tac with_eq (Name id) c (Option.default allClauses cls)) (induction_with_atomization_of_ind_arg @@ -2490,7 +2538,10 @@ let new_induct_gen isrec with_evars elim names (c,lbind) cls gl = that all arguments and parameters of the scheme are given (mandatory for the moment), so we don't need to deal with parameters of the inductive type as in new_induct_gen. *) -let new_induct_gen_l isrec with_evars elim names lc gl = +let new_induct_gen_l isrec with_evars elim (eqname,names) lc gl = + if eqname <> None then + errorlabstrm "" (str "Do not know what to do with " ++ + pr_intro_pattern (Option.get eqname)); let newlc = ref [] in let letids = ref [] in let rec atomize_list l gl = @@ -2532,18 +2583,18 @@ let induct_destruct_l isrec with_evars lc elim names cls = let _ = if elim = None then - error ("Induction scheme must be given when several induction hypothesis.\n" - ^ "Example: induction x1 x2 x3 using my_scheme.") in + errorlabstrm "" (strbrk "Induction scheme must be given when several induction hypothesis are given.\n" ++ + str "Example: induction x1 x2 x3 using my_scheme.") in let newlc = List.map (fun x -> match x with (* FIXME: should we deal with ElimOnIdent? *) | ElimOnConstr (x,NoBindings) -> x - | _ -> error "don't know where to find some argument") + | _ -> error "Don't know where to find some argument.") lc in if cls <> None then error - "'in' clause not supported when several induction hypothesis are given"; + "'in' clause not supported when several induction hypothesis are given."; new_induct_gen_l isrec with_evars elim names newlc (* Induction either over a term, over a quantified premisse, or over @@ -2551,7 +2602,7 @@ let induct_destruct_l isrec with_evars lc elim names cls = principles). TODO: really unify induction with one and induction with several args *) -let induct_destruct isrec with_evars lc elim names cls = +let induct_destruct isrec with_evars (lc,elim,names,cls) = assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) if List.length lc = 1 then (* induction on one arg: use old mechanism *) try @@ -2565,11 +2616,16 @@ let induct_destruct isrec with_evars lc elim names cls = with _ -> raise x) else induct_destruct_l isrec with_evars lc elim names cls +let induction_destruct isrec with_evars = function + | [] -> tclIDTAC + | [a] -> induct_destruct isrec with_evars a + | a::l -> + tclTHEN + (induct_destruct isrec with_evars a) + (tclMAP (induct_destruct false with_evars) l) - - -let new_induct = induct_destruct true -let new_destruct = induct_destruct false +let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls) +let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls) (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) @@ -2858,7 +2914,7 @@ let abstract_subproof name tac gl = let na = next_global_ident_away false name (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in if occur_existential concl then - error "\"abstract\" cannot handle existentials"; + error "\"abstract\" cannot handle existentials."; let lemme = start_proof na (Global, Proof Lemma) secsign concl (fun _ _ -> ()); let _,(const,kind,_) = @@ -2901,7 +2957,7 @@ let admit_as_an_axiom gl = let name = add_suffix (get_current_proof_name ()) "_admitted" in let na = next_global_ident_away false name (pf_ids_of_hyps gl) in let concl = it_mkNamedProd_or_LetIn (pf_concl gl) sign in - if occur_existential concl then error "\"admit\" cannot handle existentials"; + if occur_existential concl then error"\"admit\" cannot handle existentials."; let axiom = let cd = Entries.ParameterEntry (concl,false) in let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in @@ -2911,3 +2967,8 @@ let admit_as_an_axiom gl = (applist (axiom, List.rev (Array.to_list (instance_from_named_context sign)))) gl + +let conv x y gl = + try let evd = Evarconv.the_conv_x_leq (pf_env gl) x y (Evd.create_evar_defs (project gl)) in + tclEVARS (Evd.evars_of evd) gl + with _ -> tclFAIL 0 (str"Not convertible") gl diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b7ab31c4..d39433d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -6,9 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: tactics.mli 11166 2008-06-22 13:23:35Z herbelin $ i*) +(*i $Id: tactics.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) +open Util open Names open Term open Environ @@ -68,7 +69,8 @@ val find_intro_names : rel_context -> goal sigma -> identifier list val intro : tactic val introf : tactic val intro_force : bool -> tactic -val intro_move : identifier option -> identifier option -> tactic +val intro_move : identifier option -> identifier move_location -> tactic + (* [intro_avoiding idl] acts as intro but prevents the new identifier to belong to [idl] *) val intro_avoiding : identifier list -> tactic @@ -110,9 +112,10 @@ val onInductionArg : (*s Introduction tactics with eliminations. *) -val intro_pattern : identifier option -> intro_pattern_expr -> tactic -val intro_patterns : intro_pattern_expr list -> tactic -val intros_pattern : identifier option -> intro_pattern_expr list -> tactic +val intro_pattern : identifier move_location -> intro_pattern_expr -> tactic +val intro_patterns : intro_pattern_expr located list -> tactic +val intros_pattern : + identifier move_location -> intro_pattern_expr located list -> tactic (*s Exact tactics. *) @@ -167,7 +170,7 @@ val keep : identifier list -> tactic val specialize : int option -> constr with_ebindings -> tactic -val move_hyp : bool -> identifier -> identifier -> tactic +val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier * identifier) list -> tactic val revert : identifier list -> tactic @@ -183,7 +186,7 @@ val apply_without_reduce : constr -> tactic val apply_list : constr list -> tactic val apply_with_ebindings_gen : - advanced_flag -> evars_flag -> constr with_ebindings -> tactic + advanced_flag -> evars_flag -> constr with_ebindings list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic @@ -260,7 +263,9 @@ val elim : val simple_induct : quantified_hypothesis -> tactic val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic + constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic (*s Case analysis tactics. *) @@ -269,7 +274,18 @@ val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> clause option -> tactic + constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + clause option -> tactic + +(*s Generic case analysis / induction tactics. *) + +val induction_destruct : evars_flag -> rec_flag -> + (constr with_ebindings induction_arg list * + constr with_ebindings option * + (intro_pattern_expr located option * intro_pattern_expr located option) * + clause option) list -> + tactic (*s Eliminations giving the type instead of the proof. *) @@ -330,20 +346,24 @@ val cut_replacing : identifier -> constr -> (tactic -> tactic) -> tactic val cut_in_parallel : constr list -> tactic -val assert_as : bool -> intro_pattern_expr -> constr -> tactic -val forward : tactic option -> intro_pattern_expr -> constr -> tactic -val letin_tac : bool option -> name -> constr -> clause -> tactic +val assert_as : bool -> intro_pattern_expr located -> constr -> tactic +val forward : tactic option -> intro_pattern_expr located -> constr -> tactic +val letin_tac : (bool * intro_pattern_expr located) option -> name -> + constr -> clause -> tactic val true_cut : name -> constr -> tactic val assert_tac : bool -> name -> constr -> tactic val generalize : constr list -> tactic val generalize_gen : ((occurrences * constr) * name) list -> tactic val generalize_dep : constr -> tactic +val conv : constr -> constr -> tactic +val resolve_classes : tactic + val tclABSTRACT : identifier option -> tactic -> tactic val admit_as_an_axiom : tactic -val abstract_generalize : identifier -> tactic +val abstract_generalize : identifier -> ?generalize_vars:bool -> tactic val register_general_multi_rewrite : (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 54094d99..17ea121f 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -8,8 +8,9 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(*i $Id: tauto.ml4 10731 2008-03-30 22:30:44Z herbelin $ i*) +(*i $Id: tauto.ml4 11309 2008-08-06 10:30:35Z herbelin $ i*) +open Term open Hipattern open Names open Libnames @@ -36,16 +37,35 @@ let is_unit ist = <:tactic> else <:tactic> - + +let is_record t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + mib.Declarations.mind_record + | _ -> false + +let is_binary t = + let (hdapp,args) = decompose_app t in + match (kind_of_term hdapp) with + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + mib.Declarations.mind_nparams = 2 + | _ -> false + let is_conj ist = let ind = assoc_last ist in - if (is_conjunction ind) && (is_nodep_ind ind) then + if (is_conjunction ind) && (is_nodep_ind ind) (* && not (is_record ind) *) + && is_binary ind (* for compatibility, as (?X _ _) matches + applications with 2 or more arguments. *) + then <:tactic> else <:tactic> let is_disj ist = - if is_disjunction (assoc_last ist) then + if is_disjunction (assoc_last ist) && is_binary (assoc_last ist) then <:tactic> else <:tactic> @@ -122,7 +142,7 @@ let rec tauto_intuit t_reduce solver ist = and t_simplif = tacticIn simplif and t_is_disj = tacticIn is_disj and t_tauto_intuit = tacticIn (tauto_intuit t_reduce solver) in - let t_solver = Tacexpr.TacArg (valueIn (VTactic (dummy_loc,solver))) in + let t_solver = globTacticIn (fun _ist -> solver) in <:tactic< ($t_simplif;$t_axioms || match reverse goal with @@ -145,16 +165,14 @@ let rec tauto_intuit t_reduce solver ist = $t_solver ) >> -let reduction_not_iff=interp +let reduction_not_iff _ist = <:tactic progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff | H:_ |- _ => progress unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in H end >> - -let t_reduction_not_iff = - Tacexpr.TacArg (valueIn (VTactic (dummy_loc,reduction_not_iff))) +let t_reduction_not_iff = tacticIn reduction_not_iff let intuition_gen tac = interp (tacticIn (tauto_intuit t_reduction_not_iff tac)) @@ -162,12 +180,12 @@ let intuition_gen tac = let simplif_gen = interp (tacticIn simplif) let tauto g = - try intuition_gen (interp <:tactic>) g + try intuition_gen <:tactic> g with Refiner.FailError _ | UserError _ -> - errorlabstrm "tauto" [< str "tauto failed" >] + errorlabstrm "tauto" (str "tauto failed.") -let default_intuition_tac = interp <:tactic< auto with * >> +let default_intuition_tac = <:tactic< auto with * >> TACTIC EXTEND tauto | [ "tauto" ] -> [ tauto ] @@ -175,5 +193,5 @@ END TACTIC EXTEND intuition | [ "intuition" ] -> [ intuition_gen default_intuition_tac ] -| [ "intuition" tactic(t) ] -> [ intuition_gen (snd t) ] +| [ "intuition" tactic(t) ] -> [ intuition_gen (fst t) ] END diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 65ad1dee..bd439fb4 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: termdn.ml 7639 2005-12-02 10:01:15Z gregoire $ *) +(* $Id: termdn.ml 11282 2008-07-28 11:51:53Z msozeau $ *) open Util open Names @@ -41,43 +41,54 @@ let decomp_pat = decrec [] let constr_pat_discr t = - if not (occur_meta_pattern t) then + if not (occur_meta_pattern t) then None else match decomp_pat t with - | PRef ((IndRef _) as ref), args - | PRef ((ConstructRef _ ) as ref), args - | PRef ((VarRef _) as ref), args -> Some(ref,args) - | _ -> None - -let constr_val_discr t = - let c, l = decomp t in - match kind_of_term c with - (* Const _,_) -> Some(TERM c,l) *) - | Ind ind_sp -> Some(IndRef ind_sp,l) - | Construct cstr_sp -> Some(ConstructRef cstr_sp,l) - | Var id -> Some(VarRef id,l) + | PRef ((IndRef _) as ref), args + | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args) + | PRef ((VarRef v) as ref), args -> Some(ref,args) | _ -> None -(* Les deux fonctions suivantes ecrasaient les precedentes, - ajout d'un suffixe _nil CP 16/08 *) - -let constr_pat_discr_nil t = - match constr_pat_discr t with - | None -> None - | Some (c,_) -> Some(c,[]) - -let constr_val_discr_nil t = - match constr_val_discr t with - | None -> None - | Some (c,_) -> Some(c,[]) +let constr_pat_discr_st (idpred,cpred) t = + match decomp_pat t with + | PRef ((IndRef _) as ref), args + | PRef ((ConstructRef _ ) as ref), args -> Some (ref,args) + | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) -> + Some(ref,args) + | PVar v, args when not (Idpred.mem v idpred) -> + Some(VarRef v,args) + | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> + Some (ref, args) + | _ -> None + +open Dn + +let constr_val_discr t = + let c, l = decomp t in + match kind_of_term c with + | Ind ind_sp -> Label(IndRef ind_sp,l) + | Construct cstr_sp -> Label((ConstructRef cstr_sp),l) + | Var id -> Label(VarRef id,l) + | Const _ -> Everything + | _ -> Nothing + +let constr_val_discr_st (idpred,cpred) t = + let c, l = decomp t in + match kind_of_term c with + | Const c -> if Cpred.mem c cpred then Everything else Label(ConstRef c,l) + | Ind ind_sp -> Label(IndRef ind_sp,l) + | Construct cstr_sp -> Label((ConstructRef cstr_sp),l) + | Var id when not (Idpred.mem id idpred) -> Label(VarRef id,l) + | Evar _ -> Everything + | _ -> Nothing let create = Dn.create -let add dn = Dn.add dn constr_pat_discr - -let rmv dn = Dn.rmv dn constr_pat_discr +let add dn st = Dn.add dn (constr_pat_discr_st st) -let lookup dn t = Dn.lookup dn constr_val_discr t +let rmv dn st = Dn.rmv dn (constr_pat_discr_st st) +let lookup dn st t = Dn.lookup dn (constr_val_discr_st st) t + let app f dn = Dn.app f dn diff --git a/tactics/termdn.mli b/tactics/termdn.mli index b65c0eeb..79efd8eb 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: termdn.mli 6427 2004-12-07 17:41:10Z sacerdot $ i*) +(*i $Id: termdn.mli 11282 2008-07-28 11:51:53Z msozeau $ i*) (*i*) open Term open Pattern open Libnames +open Names (*i*) (* Discrimination nets of terms. *) @@ -22,7 +23,10 @@ open Libnames order in such a way patterns having the same prefix have this common prefix shared and the seek for the action associated to the patterns that a term matches are found in time proportional to the maximal -number of nodes of the patterns matching the term *) +number of nodes of the patterns matching the term. The [transparent_state] +indicates which constants and variables can be considered as rigid. +These dnets are able to cope with existential variables as well, which match +[Everything]. *) type 'a t @@ -30,13 +34,13 @@ val create : unit -> 'a t (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) -val add : 'a t -> (constr_pattern * 'a) -> 'a t +val add : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t -val rmv : 'a t -> (constr_pattern * 'a) -> 'a t +val rmv : 'a t -> transparent_state -> (constr_pattern * 'a) -> 'a t (* [lookup t c] looks for patterns (with their action) matching term [c] *) -val lookup : 'a t -> constr -> (constr_pattern * 'a) list +val lookup : 'a t -> transparent_state -> constr -> (constr_pattern * 'a) list val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit @@ -44,9 +48,12 @@ val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit (*i*) (* These are for Nbtermdn *) -val constr_pat_discr : +val constr_pat_discr_st : transparent_state -> constr_pattern -> (global_reference * constr_pattern list) option -val constr_val_discr : - constr -> (global_reference * constr list) option +val constr_val_discr_st : transparent_state -> + constr -> (global_reference * constr list) Dn.lookup_res + +val constr_pat_discr : constr_pattern -> (global_reference * constr_pattern list) option +val constr_val_discr : constr -> (global_reference * constr list) Dn.lookup_res (*i*) -- cgit v1.2.3