diff options
Diffstat (limited to 'tactics/class_tactics.ml4')
-rw-r--r-- | tactics/class_tactics.ml4 | 389 |
1 files changed, 227 insertions, 162 deletions
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 |