From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tactics/eauto.ml4 | 448 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 448 insertions(+) create mode 100644 tactics/eauto.ml4 (limited to 'tactics/eauto.ml4') diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 new file mode 100644 index 00000000..31d79948 --- /dev/null +++ b/tactics/eauto.ml4 @@ -0,0 +1,448 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ e_give_exact c ] +END*) +TACTIC EXTEND Eexact +| [ "EExact" constr(c) ] -> [ e_give_exact c ] +END + +let e_give_exact_constr = h_eexact + +let registered_e_assumption gl = + tclFIRST (List.map (fun id gl -> e_give_exact_constr (mkVar id) gl) + (pf_ids_of_hyps gl)) gl + +(* This automatically define h_eApply (among other things) *) +(*V8 TACTIC EXTEND eapply + [ "eapply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ] +END*) +TACTIC EXTEND eapply + [ "EApply" constr_with_bindings(c) ] -> [ e_resolve_with_bindings_tac c ] +END + +let vernac_e_resolve_constr c = h_eapply (c,NoBindings) + +let e_constructor_tac boundopt i lbind gl = + let cl = pf_concl gl in + let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in + let nconstr = + Array.length (snd (Global.lookup_inductive mind)).mind_consnames + and sigma = project gl in + if i=0 then error "The constructors are numbered starting from 1"; + if i > nconstr then error "Not enough constructors"; + begin match boundopt with + | Some expctdnum -> + if expctdnum <> nconstr then + error "Not the expected number of constructors" + | None -> () + end; + let cons = mkConstruct (ith_constructor_of_inductive mind i) in + let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in + (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl + +let e_one_constructor i = e_constructor_tac None i + +let e_any_constructor tacopt gl = + let t = match tacopt with None -> tclIDTAC | Some t -> t in + 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"; + tclFIRST (List.map (fun i -> tclTHEN (e_one_constructor i NoBindings) t) + (interval 1 nconstr)) gl + +let e_left = e_constructor_tac (Some 2) 1 + +let e_right = e_constructor_tac (Some 2) 2 + +let e_split = e_constructor_tac (Some 1) 1 + +(* This automatically define h_econstructor (among other things) *) +(*V8 TACTIC EXTEND eapply + [ "econstructor" integer(n) with_bindings(c) ] -> [ e_constructor_tac None n c ] +END*) +TACTIC EXTEND econstructor + [ "EConstructor" integer(n) "with" bindings(c) ] -> [ e_constructor_tac None n c ] + | [ "EConstructor" integer(n) ] -> [ e_constructor_tac None n NoBindings ] + | [ "EConstructor" tactic_opt(t) ] -> [ e_any_constructor (option_app Tacinterp.eval_tactic t) ] + END + +TACTIC EXTEND eleft + [ "ELeft" "with" bindings(l) ] -> [e_left l] + | [ "ELeft"] -> [e_left NoBindings] +END + +TACTIC EXTEND eright + [ "ERight" "with" bindings(l) ] -> [e_right l] + | [ "ERight" ] -> [e_right NoBindings] +END + +TACTIC EXTEND esplit + [ "ESplit" "with" bindings(l) ] -> [e_split l] + | [ "ESplit"] -> [e_split NoBindings] +END + + +TACTIC EXTEND eexists + [ "EExists" bindings(l) ] -> [e_split l] +END + + +(************************************************************************) +(* PROLOG tactic *) +(************************************************************************) + +let one_step l gl = + [Tactics.intro] + @ (List.map e_resolve_constr (List.map mkVar (pf_ids_of_hyps gl))) + @ (List.map e_resolve_constr l) + @ (List.map assumption (pf_ids_of_hyps gl)) + +let rec prolog l n gl = + if n <= 0 then error "prolog - failure"; + let prol = (prolog l (n-1)) in + (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl + +let prolog_tac l n gl = + let n = + match n with + | Genarg.ArgArg n -> n + | _ -> error "Prolog called with a non closed argument" + in + try (prolog l n gl) + with UserError ("Refiner.tclFIRST",_) -> + errorlabstrm "Prolog.prolog" (str "Prolog failed") + +(* V8 TACTIC EXTEND prolog +| [ "prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] +END*) +TACTIC EXTEND Prolog +| [ "Prolog" "[" constr_list(l) "]" int_or_var(n) ] -> [ prolog_tac l n ] +END + +(* +let vernac_prolog = + let uncom = function + | Constr c -> c + | _ -> assert false + in + let gentac = + hide_tactic "Prolog" + (function + | (Integer n) :: al -> prolog_tac (List.map uncom al) n + | _ -> assert false) + in + fun coms n -> + gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms)) +*) + +open Auto + +(***************************************************************************) +(* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *) +(***************************************************************************) + +let unify_e_resolve (c,clenv) gls = + let (wc,kONT) = startWalk gls in + let clenv' = connect_clenv wc clenv in + let _ = clenv_unique_resolver false clenv' gls in + vernac_e_resolve_constr c gls + +let rec e_trivial_fail_db db_list local_db goal = + let tacl = + registered_e_assumption :: + (tclTHEN Tactics.intro + (function g'-> + 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 + (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 hintl = + if occur_existential concl then + list_map_append (Hint_db.map_all hdc) (local_db::db_list) + else + 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} as patac) -> + (b, + let tac = + match t with + | Res_pf (term,cl) -> unify_resolve (term,cl) + | ERes_pf (term,cl) -> unify_e_resolve (term,cl) + | Give_exact (c) -> e_give_exact_constr c + | Res_pf_THEN_trivial_fail (term,cl) -> + tclTHEN (unify_e_resolve (term,cl)) + (e_trivial_fail_db db_list local_db) + | Unfold_nth c -> unfold_constr c + | Extern tacast -> conclPattern concl + (out_some p) tacast + in + (tac,fmt_autotactic t)) + (*i + fun gls -> pPNL (fmt_autotactic t); Format.print_flush (); + try tac gls + with e when Logic.catchable_exception(e) -> + (Format.print_string "Fail\n"; + Format.print_flush (); + raise e) + i*) + in + List.map tac_of_hint hintl + +and e_trivial_resolve db_list local_db gl = + try + Auto.priority + (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) + with Bound | Not_found -> [] + +let e_possible_resolve db_list local_db gl = + try List.map snd (e_my_find_search db_list local_db + (List.hd (head_constr_bound gl [])) gl) + with Bound | Not_found -> [] + +let assumption_tac_list id = apply_tac_list (e_give_exact_constr (mkVar id)) + +let find_first_goal gls = + try first_goal gls with UserError _ -> assert false + +(*s The following module [SearchProblem] is used to instantiate the generic + exploration functor [Explore.Make]. *) + +module SearchProblem = struct + + type state = { + depth : int; (*r depth of search before failing *) + tacres : goal list sigma * validation; + last_tactic : std_ppcmds; + dblist : Auto.Hint_db.t list; + localdb : Auto.Hint_db.t list } + + let success s = (sig_it (fst s.tacres)) = [] + + let rec filter_tactics (glls,v) = function + | [] -> [] + | (tac,pptac) :: tacl -> + try + let (lgls,ptl) = apply_tac_list tac glls in + let v' p = v (ptl p) in + ((lgls,v'),pptac) :: filter_tactics (glls,v) tacl + with e when Logic.catchable_exception e -> + filter_tactics (glls,v) tacl + + let rec list_addn n x l = + if n = 0 then l else x :: (list_addn (pred n) x l) + + (* Ordering of states is lexicographic on depth (greatest first) then + number of remaining goals. *) + let compare s s' = + let d = s'.depth - s.depth in + let nbgoals s = List.length (sig_it (fst s.tacres)) in + if d <> 0 then d 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 -> (e_give_exact_constr (mkVar id), + (str "Exact" ++ spc () ++ pr_id id))) + (pf_ids_of_hyps g)) + in + List.map (fun (res,pp) -> { depth = s.depth; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = List.tl s.localdb }) l + in + let intro_tac = + List.map + (fun ((lgls,_) as res,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 + { depth = s.depth; tacres = res; + last_tactic = pp; dblist = s.dblist; + localdb = ldb :: List.tl s.localdb }) + (filter_tactics s.tacres [Tactics.intro,(str "Intro")]) + 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 + (fun ((lgls,_) as res, pp) -> + let nbgl' = List.length (sig_it lgls) in + if nbgl' < nbgl then + { depth = s.depth; tacres = res; last_tactic = pp; + dblist = s.dblist; localdb = List.tl s.localdb } + else + { depth = pred s.depth; tacres = res; + dblist = s.dblist; last_tactic = pp; + localdb = + list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + l + in + List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) + + let pp s = + msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ + s.last_tactic ++ str "\n")) + +end + +module Search = Explore.Make(SearchProblem) + +let make_initial_state n gl dblist localdb = + { SearchProblem.depth = n; + SearchProblem.tacres = tclIDTAC gl; + SearchProblem.last_tactic = (mt ()); + SearchProblem.dblist = dblist; + SearchProblem.localdb = [localdb] } + +let e_depth_search debug p db_list local_db gl = + try + 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.SearchProblem.tacres + with Not_found -> error "EAuto: depth first search failed" + +let e_breadth_search debug n db_list local_db gl = + try + let tac = + if debug then Search.debug_breadth_first else Search.breadth_first + in + let s = tac (make_initial_state n gl db_list local_db) in + s.SearchProblem.tacres + with Not_found -> error "EAuto: breadth first search failed" + +let e_search_auto debug (in_depth,p) db_list gl = + let local_db = make_local_hint_db gl in + if in_depth then + e_depth_search debug p db_list local_db gl + else + e_breadth_search debug p db_list local_db gl + +let eauto debug np dbnames = + let db_list = + List.map + (fun x -> + try Stringmap.find x !searchtable + with Not_found -> error ("EAuto: "^x^": No such Hint database")) + ("core"::dbnames) + in + tclTRY (e_search_auto debug np db_list) + +let full_eauto debug n gl = + let dbnames = stringmap_dom !searchtable in + let dbnames = list_subtract dbnames ["v62"] in + let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in + let local_db = make_local_hint_db gl in + tclTRY (e_search_auto debug n db_list) gl + +let gen_eauto d np = function + | None -> full_eauto d np + | Some l -> eauto d np l + +let make_depth = function + | None -> !default_search_depth + | Some (Genarg.ArgArg d) -> d + | _ -> error "EAuto called with a non closed argument" + +let make_dimension n = function + | None -> (true,make_depth n) + | Some (Genarg.ArgArg d) -> (false,d) + | _ -> error "EAuto called with a non closed argument" + +open Genarg + +(* Hint bases *) + +let pr_hintbases _prc _prt = function + | None -> str " with *" + | Some [] -> mt () + | Some l -> str " with " ++ Util.prlist_with_sep spc str l + +ARGUMENT EXTEND hintbases + TYPED AS preident_list_opt + PRINTED BY pr_hintbases +| [ "with" "*" ] -> [ None ] +| [ "with" ne_preident_list(l) ] -> [ Some l ] +| [ ] -> [ Some [] ] +END + +TACTIC EXTEND EAuto +| [ "EAuto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] -> + [ gen_eauto false (make_dimension n p) db ] +END + +V7 TACTIC EXTEND EAutodebug +| [ "EAutod" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] -> + [ gen_eauto true (make_dimension n p) db ] +END + + -- cgit v1.2.3