diff options
27 files changed, 491 insertions, 318 deletions
diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml index e540058f14..fd5972fb74 100644 --- a/contrib/firstorder/sequent.ml +++ b/contrib/firstorder/sequent.ml @@ -281,7 +281,7 @@ let create_with_auto_hints l depth gl= searchtable_map dbname with Not_found-> error ("Firstorder: "^dbname^" : No such Hint database") in - Hint_db.iter g (snd hdb) in + Hint_db.iter g hdb in List.iter h l; !seqref diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 3d80bd0040..d7bcde69cb 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = false (true,5) [Lazy.force refl_equal] - [empty_transparent_state, Auto.Hint_db.empty] + [Auto.Hint_db.empty false] ) ) ) diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 6ec0fac42d..767a7dd667 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -161,21 +161,22 @@ 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 fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in - let flags = Auto.auto_unif_flags in let hintl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) - (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.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) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) - (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.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 = fun (st, ({pri=b; pat = p; code=t} as _patac)) -> @@ -279,7 +280,7 @@ module MySearchProblem = 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 }) @@ -375,7 +376,7 @@ let rec trivial_fail_db 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 db_list (add_hint_list hintl local_db) g') + in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g') in tclFIRST (assumption::intro_tac:: @@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl = (trivial_resolve db_list local_db (pf_concl gl)))) gl and my_find_search db_list local_db hdc concl = - let flags = Auto.auto_unif_flags in let tacl = if occur_existential concl then - list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) - (Hint_db.map_all hdc db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.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) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) - (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) + list_map_append (fun db -> + let flags = {Auto.auto_unif_flags with Unification.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 List.map (fun (st, {pri=b; pat=p; code=t} as _patac) -> @@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = with Failure _ -> [] in (free_try - (search_gen decomp n db_list (add_hint_list hintl local_db) [d]) + (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d]) g')) in let rec_tacs = diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index 474b3616a8..70087b2d44 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) = let setoid_of_relation env a r = - lapp coq_mk_Setoid - [|a ; r ; - Class_tactics.reflexive_proof env a r ; - Class_tactics.symmetric_proof env a r ; - Class_tactics.transitive_proof env a r |] + try + lapp coq_mk_Setoid + [|a ; r ; + Class_tactics.reflexive_proof env a r ; + Class_tactics.symmetric_proof env a r ; + Class_tactics.transitive_proof env a r |] + with Not_found -> + error "cannot find setoid relation" let op_morph r add mul opp req m1 m2 m3 = lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |] diff --git a/tactics/auto.ml b/tactics/auto.ml index 0d5d275384..69fe51efa8 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -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 lookup_tacs (hdc,c) (l,l',dn) = - let l' = List.map snd (Btermdn.lookup dn c) in +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 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,45 @@ 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 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 && v.pri = 0 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 +190,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 @@ -184,18 +218,21 @@ let try_head_pattern c = try head_pattern_bound c 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 match kind_of_term cty with | 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 @@ -279,32 +316,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 +382,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 +404,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 +415,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 *) @@ -404,7 +437,7 @@ let add_extern pri (patmetas,pat) tacast local dbname = (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 +446,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 = @@ -493,7 +526,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 +552,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 @@ -544,7 +577,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 ())); @@ -610,7 +644,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 prparer un @@ -648,7 +682,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 +692,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 +723,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) @@ -817,7 +850,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 @@ -956,7 +989,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 +1007,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 5b151162c4..c5df28d427 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -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/btermdn.ml b/tactics/btermdn.ml index 7d41ebf9df..2412968a1e 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -9,6 +9,7 @@ (* $Id$ *) 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.Nothing 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 e0ba8ddcaf..86107641d0 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -11,6 +11,7 @@ (*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 a353a4222f..68cf37b49e 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -43,6 +43,8 @@ open Evd let default_eauto_depth = 100 let typeclasses_db = "typeclass_instances" +let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db true) + let check_imported_library d = let d' = List.map id_of_string d in let dir = make_dirpath (List.rev d') in @@ -98,7 +100,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 @@ -106,13 +108,17 @@ let rec e_trivial_fail_db db_list local_db goal = and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = - if occur_existential concl then +(* if occur_existential concl then *) +(* list_map_append *) +(* (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_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 = @@ -186,6 +192,8 @@ module SearchProblem = struct (* (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 -> @@ -214,7 +222,7 @@ 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' @@ -239,24 +247,26 @@ module SearchProblem = struct 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 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 (List.hd s.localdb) 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; + { s with + depth = pred s.depth; + tacres = res; last_tactic = pp; pri = pri; localdb = List.tl s.localdb } else { s with @@ -265,13 +275,14 @@ module SearchProblem = struct localdb = list_addn (nbgl'-nbgl) (List.hd s.localdb) s.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 (List.hd s.localdb) (pf_concl g)) + filter_tactics s.tacres (e_possible_resolve s.dblist (List.hd s.localdb) concl) in List.map possible_resolve l in - List.sort compare (assumption_tacs (* @intro_tac @ custom_tac *) @ rec_tacs) + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) let pp s = msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ @@ -342,9 +353,11 @@ let e_breadth_search debug s = in let s = tac s in s.tacres 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 + 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 +368,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 @@ -505,6 +512,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))) @@ -539,7 +560,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") @@ -780,11 +801,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 @@ -1057,11 +1079,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 @@ -1075,16 +1103,16 @@ let occurrences_of = function (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 +1120,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 = @@ -1146,7 +1174,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 +1201,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 @@ -1690,3 +1719,16 @@ TACTIC EXTEND apply_typeclasses Clenvtac.clenv_refine true {cl' with evd = evd'} gl) gl ] END + +(* TACTIC EXTEND solve_evar *) +(* [ "solve_evar" int_or_var(n) ] -> [ fun gl -> *) +(* let n = match n with ArgArg i -> pred i | _ -> assert false in *) +(* let ev, evi = try List.nth (Evd.to_list (project gl)) n with Not_found -> assert false in *) +(* let id = pf_get_new_id (add_suffix (id_of_string "evar") (string_of_int n)) gl in *) +(* tclTHEN (true_cut (Name id) evi.evar_concl gl) *) + +(* ] *) +(* END *) + + +(* let nprod = nb_prod (pf_concl gl) in *) diff --git a/tactics/dn.ml b/tactics/dn.ml index dbfafcd61c..0809c80ebb 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 *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -32,6 +33,10 @@ type ('lbl,'pat) decompose_fun = 'pat -> ('lbl * 'pat list) option +type 'res lookup_res = Label of 'res | Nothing | Everything + +type ('lbl,'tree) lookup_fun = 'tree -> ('lbl * 'tree list) lookup_res + type ('lbl,'pat,'inf) t = (('lbl * int) option,'pat * 'inf) Tlm.t let create () = Tlm.empty @@ -46,29 +51,44 @@ let path_of dna = and pathrec deferred t = match dna t with - | 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) + | 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 e07742e0fd..e37ed9af3f 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -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 3b982b4c08..70bc9a5924 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -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 }) @@ -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/nbtermdn.ml b/tactics/nbtermdn.ml index c53a5088a9..431748868c 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -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/termdn.ml b/tactics/termdn.ml index 1c95f7fdc6..995183dc90 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -41,43 +41,53 @@ 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) + | _ -> 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 6e1bdd87ca..a9f11b3afa 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -12,6 +12,7 @@ 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*) diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 42961baea2..d77704c12a 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -134,8 +134,8 @@ End Respecting. (** The default equivalence on function spaces, with higher-priority than [eq]. *) -Program Instance pointwise_equivalence [ Equivalence A eqA ] : - Equivalence (B -> A) (pointwise_relation eqA) | 9. +Program Instance pointwise_equivalence [ Equivalence B eqB ] : + Equivalence (A -> B) (pointwise_relation eqB) | 9. Next Obligation. Proof. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 05167bdc58..7240217990 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -39,10 +39,6 @@ Class Morphism A (R : relation A) (m : A) : Prop := Implicit Arguments Morphism [A]. -(** We allow to unfold the [relation] definition while doing morphism search. *) - -Typeclasses unfold relation. - (** Respectful morphisms. *) (** The fully dependent version, not used yet. *) @@ -79,6 +75,15 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop Open Local Scope signature_scope. +(** Pointwise lifting is just respect with leibnize equality on the left. *) + +Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := + fun f g => forall x : A, R (f x) (g x). + +Lemma pointwise_pointwise A B (R : relation B) : + relation_equivalence (pointwise_relation R) (@eq A ==> R). +Proof. intros. split. simpl_relation. firstorder. Qed. + (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) @@ -99,17 +104,18 @@ Proof. firstorder. Qed. (** The subrelation property goes through products as usual. *) -Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] : - ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). -Proof. firstorder. Qed. +Instance morphisms_subrelation_respectful [ subl : subrelation A R₂ R₁, subr : subrelation B S₁ S₂ ] : + subrelation (R₁ ==> S₁) (R₂ ==> S₂). +Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. -Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] : - ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. -Proof. firstorder. Qed. +(** And of course it is reflexive. *) + +Instance morphisms_subrelation_refl : ! subrelation A R R | 10. +Proof. simpl_relation. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) -Lemma subrelation_morphism [ sub : subrelation A R₁ R₂, mor : Morphism A R₁ m ] : Morphism R₂ m. +Lemma subrelation_morphism [ mor : Morphism A R₁ m, sub : subrelation A R₁ R₂ ] : Morphism R₂ m. Proof. intros. apply sub. apply mor. Qed. @@ -121,8 +127,9 @@ Proof. reduce. subst. firstorder. Qed. (** We use an external tactic to manage the application of subrelation, which is otherwise always applicable. We allow its use only once per branch. *) -Inductive subrelation_done : Prop := - did_subrelation : subrelation_done. +Inductive subrelation_done : Prop := did_subrelation : subrelation_done. + +Inductive normalization_done : Prop := did_normalization. Ltac subrelation_tac := match goal with @@ -131,7 +138,7 @@ Ltac subrelation_tac := set(H:=did_subrelation) ; eapply @subrelation_morphism end. -Hint Extern 4 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. +Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) @@ -181,20 +188,10 @@ Program Instance trans_contra_co_morphism transitivity x0... Qed. -(* (** Dually... *) *) - -(* Program Instance [ Transitive A R ] => *) -(* trans_co_contra_inv_impl_morphism : Morphism (R ++> R --> inverse impl) R. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* apply* trans_contra_co_morphism ; eauto. eauto. *) -(* Qed. *) - (** Morphism declarations for partial applications. *) Program Instance trans_contra_inv_impl_morphism - [ Transitive A R ] : Morphism (R --> inverse impl) (R x). + [ Transitive A R ] : Morphism (R --> inverse impl) (R x) | 3. Next Obligation. Proof with auto. @@ -202,7 +199,7 @@ Program Instance trans_contra_inv_impl_morphism Qed. Program Instance trans_co_impl_morphism - [ Transitive A R ] : Morphism (R ==> impl) (R x). + [ Transitive A R ] : Morphism (R ==> impl) (R x) | 3. Next Obligation. Proof with auto. @@ -210,23 +207,23 @@ Program Instance trans_co_impl_morphism Qed. Program Instance trans_sym_co_inv_impl_morphism - [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x). + [ PER A R ] : Morphism (R ==> inverse impl) (R x) | 2. Next Obligation. Proof with auto. - transitivity y... + transitivity y... symmetry... Qed. Program Instance trans_sym_contra_impl_morphism - [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x). + [ PER A R ] : Morphism (R --> impl) (R x) | 2. Next Obligation. Proof with auto. - transitivity x0... + transitivity x0... symmetry... Qed. Program Instance equivalence_partial_app_morphism - [ Equivalence A R ] : Morphism (R ==> iff) (R x). + [ Equivalence A R ] : Morphism (R ==> iff) (R x) | 1. Next Obligation. Proof with auto. @@ -240,36 +237,16 @@ Program Instance equivalence_partial_app_morphism to get an [R y z] goal. *) Program Instance trans_co_eq_inv_impl_morphism - [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R. + [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R | 2. Next Obligation. Proof with auto. transitivity y... Qed. -(* Program Instance [ Transitive A R ] => *) -(* trans_contra_eq_impl_morphism : Morphism (R --> (@eq A) ==> impl) R. *) - -(* Next Obligation. *) -(* Proof with auto. *) -(* transitivity x... *) -(* Qed. *) - (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance trans_sym_morphism - [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R. - - Next Obligation. - Proof with auto. - split ; intros. - transitivity x0... transitivity x... - - transitivity y... transitivity y0... - Qed. - -Program Instance equiv_morphism [ Equivalence A R ] : - Morphism (R ==> R ==> iff) R. +Program Instance PER_morphism [ PER A R ] : Morphism (R ==> R ==> iff) R | 1. Next Obligation. Proof with auto. @@ -293,6 +270,15 @@ Program Instance iff_impl_id : Program Instance inverse_iff_impl_id : Morphism (iff --> impl) id. +Program Instance compose_morphism A B C R₀ R₁ R₂ : + Morphism ((R₁ ==> R₂) ==> (R₀ ==> R₁) ==> (R₀ ==> R₂)) (@compose A B C). + + Next Obligation. + Proof. + simpl_relation. + unfold compose. apply H. apply H0. apply H1. + Qed. + (** Coq functions are morphisms for leibniz equality, applied only if really needed. *) @@ -342,10 +328,6 @@ Instance morphism_morphism_proxy [ Morphism A R x ] : MorphismProxy A R x | 2. Proof. firstorder. Qed. -(* Instance (A : Type) [ Reflexive B R ] => *) -(* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) -(* Proof. simpl_relation. Qed. *) - (** [R] is Reflexive, hence we can build the needed proof. *) Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] : @@ -373,12 +355,11 @@ Ltac partial_application_tactic := end in match goal with + | [ _ : subrelation_done |- _ ] => fail 1 + | [ _ : normalization_done |- _ ] => fail 1 | [ |- @Morphism _ _ ?m ] => on_morphism m end. -(* Program Instance [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) => *) -(* reflexive_partial_app_morphism : Morphism R' (m x). *) - Hint Extern 4 (@Morphism _ _ _) => partial_application_tactic : typeclass_instances. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), @@ -406,8 +387,8 @@ Proof. firstorder. Qed. Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] : Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). -Proof. red ; intros. - pose normalizes as r. +Proof. red ; intros. + assert(r:=normalizes). setoid_rewrite r. setoid_rewrite inverse_respectful. reflexivity. @@ -415,8 +396,14 @@ Qed. (** Once we have normalized, we will apply this instance to simplify the problem. *) -Program Instance morphism_inverse_morphism - [ Morphism A R m ] : Morphism (inverse R) m | 2. +Definition morphism_inverse_morphism [ mor : Morphism A R m ] : Morphism (inverse R) m := mor. + +Ltac morphism_inverse := + match goal with + [ |- @Morphism _ (flip _) _ ] => eapply @morphism_inverse_morphism + end. + +Hint Extern 2 (@Morphism _ _ _) => morphism_inverse : typeclass_instances. (** Bootstrap !!! *) @@ -441,10 +428,9 @@ Proof. assumption. Qed. -Inductive normalization_done : Prop := did_normalization. - Ltac morphism_normalization := match goal with + | [ _ : subrelation_done |- _ ] => fail 1 | [ _ : normalization_done |- _ ] => fail 1 | [ |- @Morphism _ _ _ ] => let H := fresh "H" in set(H:=did_normalization) ; eapply @morphism_releq_morphism @@ -465,4 +451,4 @@ Ltac morphism_reflexive := | [ |- @Morphism _ _ _ ] => eapply @reflexive_morphism end. -Hint Extern 4 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. +Hint Extern 7 (@Morphism _ _ _) => morphism_reflexive : typeclass_instances. diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 7dc1f95ef5..ec62e12ecd 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -29,7 +29,7 @@ Program Instance not_iff_morphism : (** Logical conjunction. *) -Program Instance and_impl_iff_morphism : +Program Instance and_impl_morphism : Morphism (impl ==> impl ==> impl) and. (* Program Instance and_impl_iff_morphism : *) @@ -49,7 +49,7 @@ Program Instance and_iff_morphism : (** Logical disjunction. *) -Program Instance or_impl_iff_morphism : +Program Instance or_impl_morphism : Morphism (impl ==> impl ==> impl) or. (* Program Instance or_impl_iff_morphism : *) diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v index 5018fa01ec..1b3896678a 100644 --- a/theories/Classes/Morphisms_Relations.v +++ b/theories/Classes/Morphisms_Relations.v @@ -48,3 +48,11 @@ Proof. intro. apply (predicate_equivalence_pointwise (cons A (cons A nil))). Qed Instance subrelation_pointwise : Morphism (subrelation ==> pointwise_relation (A:=A) (pointwise_relation (A:=A) impl)) id. Proof. intro. apply (predicate_implication_pointwise (cons A (cons A nil))). Qed. + + +Lemma inverse_pointwise_relation A (R : relation A) : + relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). +Proof. intros. split; firstorder. Qed. + + + diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 31398aa3b9..c4e98c24ab 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -21,13 +21,14 @@ Require Import Coq.Program.Basics. Require Import Coq.Program.Tactics. Require Export Coq.Relations.Relation_Definitions. +(** We allow to unfold the [relation] definition while doing morphism search. *) + +Typeclasses unfold relation. + Notation inverse R := (flip (R:relation _) : relation _). Definition complement {A} (R : relation A) : relation A := fun x y => R x y -> False. -Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := - fun f g => forall x : A, R (f x) (g x). - (** These are convertible. *) Lemma complement_inverse : forall A (R : relation A), complement (inverse R) = inverse (complement R). @@ -394,7 +395,3 @@ Program Instance subrelation_partial_order : Proof. unfold relation_equivalence in *. firstorder. Qed. - -Lemma inverse_pointwise_relation A (R : relation A) : - relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)). -Proof. reflexivity. Qed. diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index 227a932071..adeb38d490 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -41,13 +41,13 @@ Typeclasses unfold equiv. (** Shortcuts to make proof search easier. *) Definition setoid_refl [ sa : Setoid A ] : Reflexive equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Definition setoid_sym [ sa : Setoid A ] : Symmetric equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Definition setoid_trans [ sa : Setoid A ] : Transitive equiv. -Proof. eauto with typeclass_instances. Qed. +Proof. typeclasses eauto. Qed. Existing Instance setoid_refl. Existing Instance setoid_sym. @@ -123,7 +123,7 @@ Ltac setoidify := repeat setoidify_tac. (** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *) Program Definition setoid_morphism [ sa : Setoid A ] : Morphism (equiv ++> equiv ++> iff) equiv := - trans_sym_morphism. + PER_morphism. (** Add this very useful instance in the database. *) diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index e033343d1d..20f4623f9f 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -660,6 +660,8 @@ Add Relation key E.eq transitivity proved by E.eq_trans as KeySetoid. +Typeclasses unfold key. + Implicit Arguments Equal [[elt]]. Add Parametric Relation (elt : Type) : (t elt) Equal diff --git a/theories/FSets/FSetFacts.v b/theories/FSets/FSetFacts.v index 6afb8fcb7b..4d24f54f45 100644 --- a/theories/FSets/FSetFacts.v +++ b/theories/FSets/FSetFacts.v @@ -309,6 +309,8 @@ Add Relation elt E.eq transitivity proved by E.eq_trans as EltSetoid. +Typeclasses unfold elt. + Add Relation t Equal reflexivity proved by eq_refl symmetry proved by eq_sym diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index 947dc818e1..bb2c01437d 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -102,6 +102,8 @@ exact sub_opp. exact add_opp. Qed. +Typeclasses unfold NZadd NZmul NZsub NZeq. + Add Ring BigZr : BigZring. (** Todo: tactic translating from [BigZ] to [Z] + omega *) diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index cbf6f701f2..5376027ddb 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -30,6 +30,7 @@ Module Make (N:NType) <: ZType. | Neg : N.t -> t_. Definition t := t_. + Typeclasses unfold t. Definition zero := Pos N.zero. Definition one := Pos N.one. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 485480fa04..1e0b45cd2c 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -76,6 +76,8 @@ exact mul_assoc. exact mul_add_distr_r. Qed. +Typeclasses unfold NZadd NZsub NZmul. + Add Ring BigNr : BigNring. (** Todo: tactic translating from [BigN] to [Z] + omega *) diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 0baba94c6d..c360f53dc8 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -139,7 +139,7 @@ let _ = pr ""; pr " Definition %s := %s_." t t; pr ""; - + pr " Typeclasses unfold %s." t; pr " Definition w_0 := w0_op.(znz_0)."; pr ""; |