Exporting more reduction functions.

3 files changed, 81 insertions, 0 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index e8e63f520c..3cfd0b5626 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -90,6 +90,13 @@ let to_red_flag = function
   }
 | _ -> assert false
 
+let to_pattern_with_occs pat =
+  to_pair Value.to_pattern (fun occ -> to_occurrences to_int_or_var occ) pat
+
+let to_constr_with_occs c =
+  let (c, occ) = to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) c in
+  (occ, c)
+
 let rec to_intro_pattern = function
 | ValBlk (0, [| b |]) -> IntroForthcoming (Value.to_bool b)
 | ValBlk (1, [| pat |]) -> IntroNaming (to_intro_pattern_naming pat)
@@ -301,6 +308,13 @@ let () = define_prim1 "tac_hnf" begin fun cl ->
   Tactics.reduce Hnf cl
 end
 
+let () = define_prim3 "tac_simpl" begin fun flags where cl ->
+  let flags = to_red_flag flags in
+  let where = Value.to_option to_pattern_with_occs where in
+  let cl = to_clause cl in
+  Tac2tactics.simpl flags where cl
+end
+
 let () = define_prim2 "tac_cbv" begin fun flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
@@ -319,6 +333,40 @@ let () = define_prim2 "tac_lazy" begin fun flags cl ->
   Tactics.reduce (Lazy flags) cl
 end
 
+let () = define_prim2 "tac_unfold" begin fun refs cl ->
+  let map v =
+    let (ref, occ) = to_pair to_evaluable_ref (fun occ -> to_occurrences to_int_or_var occ) v in
+    (occ, ref)
+  in
+  let refs = Value.to_list map refs in
+  let cl = to_clause cl in
+  Tactics.reduce (Unfold refs) cl
+end
+
+let () = define_prim2 "tac_fold" begin fun args cl ->
+  let args = Value.to_list Value.to_constr args in
+  let cl = to_clause cl in
+  Tactics.reduce (Fold args) cl
+end
+
+let () = define_prim2 "tac_pattern" begin fun where cl ->
+  let where = Value.to_list to_constr_with_occs where in
+  let cl = to_clause cl in
+  Tactics.reduce (Pattern where) cl
+end
+
+let () = define_prim2 "tac_vm" begin fun where cl ->
+  let where = Value.to_option to_pattern_with_occs where in
+  let cl = to_clause cl in
+  Tac2tactics.vm where cl
+end
+
+let () = define_prim2 "tac_native" begin fun where cl ->
+  let where = Value.to_option to_pattern_with_occs where in
+  let cl = to_clause cl in
+  Tac2tactics.native where cl
+end
+
 let () = define_prim4 "tac_rewrite" begin fun ev rw cl by ->
   let ev = Value.to_bool ev in
   let rw = Value.to_list to_rewriting rw in
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index e7e15544af..50c1df922e 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -6,8 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Util
+open Names
+open Globnames
 open Misctypes
 open Tactypes
+open Genredexpr
 open Tactics
 open Proofview
 open Tacmach.New
@@ -57,3 +61,24 @@ let rewrite ev rw cl by =
   let rw = List.map map_rw rw in
   let by = Option.map (fun tac -> Tacticals.New.tclCOMPLETE tac, Equality.Naive) by in
   Equality.general_multi_rewrite ev rw cl by
+
+(** Ltac interface treats differently global references than other term
+    arguments in reduction expressions. In Ltac1, this is done at parsing time.
+    Instead, we parse indifferently any pattern and dispatch when the tactic is
+    called. *)
+let map_pattern_with_occs (pat, occ) = match pat with
+| Pattern.PRef (ConstRef cst) -> (occ, Inl (EvalConstRef cst))
+| Pattern.PRef (VarRef id) -> (occ, Inl (EvalVarRef id))
+| _ -> (occ, Inr pat)
+
+let simpl flags where cl =
+  let where = Option.map map_pattern_with_occs where in
+  Tactics.reduce (Simpl (flags, where)) cl
+
+let vm where cl =
+  let where = Option.map map_pattern_with_occs where in
+  Tactics.reduce (CbvVm where) cl
+
+let native where cl =
+  let where = Option.map map_pattern_with_occs where in
+  Tactics.reduce (CbvNative where) cl
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 93cc6ecd68..affbbbbdd7 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Locus
+open Genredexpr
 open Misctypes
 open Tactypes
 open Proofview
@@ -34,3 +35,10 @@ type rewriting =
 
 val rewrite :
   evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
+
+val simpl : evaluable_global_reference glob_red_flag ->
+  (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+
+val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
+
+val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic