ML bindings of auto-related tactics.

4 files changed, 125 insertions, 0 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 6dcb3f15fb..ed0e6aafd3 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -159,6 +159,17 @@ let to_rewriting = function
   (orient, repeat, c)
 | _ -> assert false
 
+let to_debug = function
+| ValInt 0 -> Hints.Off
+| ValInt 1 -> Hints.Info
+| ValInt 2 -> Hints.Debug
+| _ -> assert false
+
+let to_strategy = function
+| ValInt 0 -> Class_tactics.Bfs
+| ValInt 1 -> Class_tactics.Dfs
+| _ -> assert false
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
@@ -200,6 +211,13 @@ let define_prim4 name tac =
   in
   Tac2env.define_primitive (pname name) tac
 
+let define_prim5 name tac =
+  let tac bt arg = match arg with
+  | [x; y; z; u; v] -> lift (tac bt x y z u v)
+  | _ -> assert false
+  in
+  Tac2env.define_primitive (pname name) tac
+
 (** Tactics from Tacexpr *)
 
 let () = define_prim2 "tac_intros" begin fun _ ev ipat ->
@@ -608,3 +626,49 @@ let () = define_prim1 "tac_subst" begin fun _ ids ->
 end
 
 let () = define_prim0 "tac_substall" (return () >>= fun () -> Equality.subst_all ())
+
+(** Auto *)
+
+let () = define_prim3 "tac_trivial" begin fun bt dbg lems dbs ->
+  let dbg = to_debug dbg in
+  let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+  let lems = Value.to_list map lems in
+  let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
+  Tac2tactics.trivial dbg lems dbs
+end
+
+let () = define_prim5 "tac_eauto" begin fun bt dbg n p lems dbs ->
+  let dbg = to_debug dbg in
+  let n = Value.to_option Value.to_int n in
+  let p = Value.to_option Value.to_int p in
+  let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+  let lems = Value.to_list map lems in
+  let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
+  Tac2tactics.eauto dbg n p lems dbs
+end
+
+let () = define_prim4 "tac_auto" begin fun bt dbg n lems dbs ->
+  let dbg = to_debug dbg in
+  let n = Value.to_option Value.to_int n in
+  let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+  let lems = Value.to_list map lems in
+  let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
+  Tac2tactics.auto dbg n lems dbs
+end
+
+let () = define_prim4 "tac_newauto" begin fun bt dbg n lems dbs ->
+  let dbg = to_debug dbg in
+  let n = Value.to_option Value.to_int n in
+  let map c = thaw bt c >>= fun c -> return (Value.to_constr c) in
+  let lems = Value.to_list map lems in
+  let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in
+  Tac2tactics.new_auto dbg n lems dbs
+end
+
+let () = define_prim4 "tac_typeclasses_eauto" begin fun bt b str n dbs ->
+  let b = Value.to_bool b in
+  let str = to_strategy str in
+  let n = Value.to_option Value.to_int n in
+  let dbs = Value.to_list Value.to_ident dbs in
+  Tac2tactics.typeclasses_eauto b str n dbs
+end
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 5b35d53be4..b35e26c89e 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -216,3 +216,33 @@ let autorewrite ~all by ids cl =
   match by with
   | None -> Autorewrite.auto_multi_rewrite ?conds ids cl
   | Some by -> Autorewrite.auto_multi_rewrite_with ?conds by ids cl
+
+(** Auto *)
+
+let trivial debug lems dbs =
+  let lems = List.map delayed_of_tactic lems in
+  let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
+  Auto.h_trivial ~debug lems dbs
+
+let auto debug n lems dbs =
+  let lems = List.map delayed_of_tactic lems in
+  let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
+  Auto.h_auto ~debug n lems dbs
+
+let new_auto debug n lems dbs =
+  let make_depth n = snd (Eauto.make_dimension n None) in
+  let lems = List.map delayed_of_tactic lems in
+  match dbs with
+  | None -> Auto.new_full_auto ~debug (make_depth n) lems
+  | Some dbs ->
+    let dbs = List.map Id.to_string dbs in
+    Auto.new_auto ~debug (make_depth n) lems dbs
+
+let eauto debug n p lems dbs =
+  let lems = List.map delayed_of_tactic lems in
+  let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in
+  Eauto.gen_eauto (Eauto.make_dimension n p) lems dbs
+
+let typeclasses_eauto only_classes strategy depth dbs =
+  let dbs = List.map Id.to_string dbs in
+  Class_tactics.typeclasses_eauto ~only_classes ~strategy ~depth dbs
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 1c76bd9648..4369919d31 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -84,3 +84,18 @@ val discriminate : evars_flag -> destruction_arg option -> unit tactic
 val injection : evars_flag -> intro_pattern list option -> destruction_arg option -> unit tactic
 
 val autorewrite : all:bool -> unit tactic option -> Id.t list -> clause -> unit tactic
+
+val trivial : Hints.debug -> constr tactic list -> Id.t list option ->
+  unit Proofview.tactic
+
+val auto : Hints.debug -> int option -> constr tactic list ->
+  Id.t list option -> unit Proofview.tactic
+
+val new_auto : Hints.debug -> int option -> constr tactic list ->
+  Id.t list option -> unit Proofview.tactic
+
+val eauto : Hints.debug -> int option -> int option -> constr tactic list ->
+  Id.t list option -> unit Proofview.tactic
+
+val typeclasses_eauto : bool -> Class_tactics.search_strategy -> int option ->
+  Id.t list -> unit Proofview.tactic
diff --git a/theories/Std.v b/theories/Std.v
index 2fa2c34da6..b667258aa2 100644
--- a/theories/Std.v
+++ b/theories/Std.v
@@ -211,3 +211,19 @@ Ltac2 @ external autorewrite : bool -> (unit -> unit) option -> ident list -> cl
 
 Ltac2 @ external subst : ident list -> unit := "ltac2" "tac_subst".
 Ltac2 @ external subst_all : unit -> unit := "ltac2" "tac_substall".
+
+(** auto *)
+
+Ltac2 Type debug := [ Off | Info | Debug ].
+
+Ltac2 Type strategy := [ BFS | DFS ].
+
+Ltac2 @ external trivial : debug -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_trivial".
+
+Ltac2 @ external auto : debug -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_auto".
+
+Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_newauto".
+
+Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto".
+
+Ltac2 @ external typeclasses_eauto : bool -> strategy -> int option -> ident list -> unit := "ltac2" "tac_typeclasses_eauto".