diff options
| -rw-r--r-- | ltac/g_class.ml4 | 17 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 64 | ||||
| -rw-r--r-- | tactics/class_tactics.mli | 7 |
3 files changed, 49 insertions, 39 deletions
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index 1adf197d6..7e26b5d18 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -45,13 +45,14 @@ ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug END let pr_search_strategy _prc _prlc _prt = function - | Dfs -> Pp.str "dfs" - | Bfs -> Pp.str "bfs" + | Some Dfs -> Pp.str "dfs" + | Some Bfs -> Pp.str "bfs" + | None -> Pp.mt () ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy -| [ "bfs" ] -> [ Bfs ] -| [ "dfs" ] -> [ Dfs ] -| [ ] -> [ Dfs ] +| [ "(bfs)" ] -> [ Some Bfs ] +| [ "(dfs)" ] -> [ Some Dfs ] +| [ ] -> [ None ] END (* true = All transparent, false = Opaque if possible *) @@ -59,15 +60,17 @@ END VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ set_typeclasses_debug d; - set_typeclasses_strategy s; + Option.iter set_typeclasses_strategy s; set_typeclasses_depth depth ] END (** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) TACTIC EXTEND typeclasses_eauto + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + [ typeclasses_eauto ~strategy:Bfs ~depth:d l ] | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto d l ] + [ typeclasses_eauto ~depth:d l ] | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [ typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ] END diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 5d5511d78..63994bafe 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -914,19 +914,20 @@ module V85 = struct let eauto_tac hints = then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) - let eauto_tac depth hints = - if get_typeclasses_iterative_deepening () then - match depth with - | None -> fix_iterative (eauto_tac hints) - | Some depth -> fix_iterative_limit depth (eauto_tac hints) - else - match depth with - | None -> fix (eauto_tac hints) - | Some depth -> fix_limit depth (eauto_tac hints) - - let real_eauto ?depth unique st hints p evd = + let eauto_tac strategy depth hints = + match strategy with + | Bfs -> + begin match depth with + | None -> fix_iterative (eauto_tac hints) + | Some depth -> fix_iterative_limit depth (eauto_tac hints) end + | Dfs -> + match depth with + | None -> fix (eauto_tac hints) + | Some depth -> fix_limit depth (eauto_tac hints) + + let real_eauto ?depth strategy unique st hints p evd = let res = - run_on_evars ~st ~unique p evd hints (eauto_tac depth hints) + run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints) in match res with | None -> evd @@ -939,12 +940,18 @@ module V85 = struct let resolve_all_evars_once debug depth unique p evd = let db = searchtable_map typeclasses_db in - real_eauto ?depth unique (Hint_db.transparent_state db) [db] p evd - - let eauto85 ?(only_classes=true) ?st depth hints g = + let strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in + real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd + + let eauto85 ?(only_classes=true) ?st ?strategy depth hints g = + let strategy = + match strategy with + | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs + | Some s -> s + in let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in - match run_tac (eauto_tac depth hints) gl with + match run_tac (eauto_tac strategy depth hints) gl with | None -> raise Not_found | Some {it = goals; sigma = s; } -> {it = List.map fst goals; sigma = s;} @@ -1288,22 +1295,23 @@ module Search = struct tclCASE (with_shelf tac) >>= casefn let eauto_tac ?(st=full_transparent_state) ?(unique=false) - ~only_classes ?dfs ~depth ~dep hints = + ~only_classes ?strategy ~depth ~dep hints = let open Proofview in let tac = let search = search_tac ~st only_classes dep hints in - let bfs = - match dfs with - | None -> get_typeclasses_iterative_deepening () - | Some v -> v + let dfs = + match strategy with + | None -> not (get_typeclasses_iterative_deepening ()) + | Some Dfs -> true + | Some Bfs -> false in - if bfs then + if dfs then + let depth = match depth with None -> -1 | Some d -> d in + search depth + else match depth with | None -> fix_iterative search | Some l -> fix_iterative_limit l search - else - let depth = match depth with None -> -1 | Some d -> d in - search depth in let error (e, ie) = match e with @@ -1389,7 +1397,7 @@ end (** Binding to either V85 or Search implementations. *) let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) - ~depth dbs = + ?strategy ~depth dbs = let dbs = List.map_filter (fun db -> try Some (searchtable_map db) with e when CErrors.noncritical e -> None) @@ -1400,10 +1408,10 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) if get_typeclasses_legacy_resolution () then Proofview.V82.tactic (fun gl -> - try V85.eauto85 depth ~only_classes ~st dbs gl + try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl with Not_found -> Refiner.tclFAIL 0 (str"Proof search failed") gl) - else Search.eauto_tac ~st ~only_classes ~depth ~dep:true dbs + else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 1b2fa035b..76760db02 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -24,7 +24,7 @@ type search_strategy = Dfs | Bfs val set_typeclasses_strategy : search_strategy -> unit -val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> +val typeclasses_eauto : ?only_classes:bool -> ?st:transparent_state -> ?strategy:search_strategy -> depth:(Int.t option) -> Hints.hint_db_name list -> unit Proofview.tactic @@ -44,9 +44,8 @@ module Search : sig (** Should we force a unique solution *) only_classes:bool -> (** Should non-class goals be shelved and resolved at the end *) - ?dfs:bool -> - (** Is a traversing-strategy specified? - If yes, true means dfs, false means bfs, i.e iterative deepening *) + ?strategy:search_strategy -> + (** Is a traversing-strategy specified? *) depth:Int.t option -> (** Bounded or unbounded search *) dep:bool -> |