Binding reduction functions acting on terms.

4 files changed, 172 insertions, 0 deletions

diff --git a/src/tac2core.mli b/src/tac2core.mli
index 566b7efbb7..9fae65bb3e 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -26,3 +26,5 @@ val c_true : ltac_constructor
 val c_false : ltac_constructor
 
 end
+
+val pf_apply : (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index d88402cbf2..2a57fdc705 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -352,6 +352,95 @@ let () = define_prim2 "tac_native" begin fun where cl ->
   Tac2tactics.native where cl
 end
 
+(** Reduction functions *)
+
+let define_red1 name tac =
+  let tac = function
+  | [x] -> tac x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+  | _ -> assert false
+  in
+  Tac2env.define_primitive (pname name) tac
+
+let define_red2 name tac =
+  let tac = function
+  | [x; y] -> tac x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+  | _ -> assert false
+  in
+  Tac2env.define_primitive (pname name) tac
+
+let define_red3 name tac =
+  let tac = function
+  | [x; y; z] -> tac x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+  | _ -> assert false
+  in
+  Tac2env.define_primitive (pname name) tac
+
+let () = define_red1 "eval_red" begin fun c ->
+  let c = Value.to_constr c in
+  Tac2tactics.eval_red c
+end
+
+let () = define_red1 "eval_hnf" begin fun c ->
+  let c = Value.to_constr c in
+  Tac2tactics.eval_hnf c
+end
+
+let () = define_red3 "eval_simpl" begin fun flags where c ->
+  let flags = to_red_flag flags in
+  let where = Value.to_option to_pattern_with_occs where in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_simpl flags where c
+end
+
+let () = define_red2 "eval_cbv" begin fun flags c ->
+  let flags = to_red_flag flags in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_cbv flags c
+end
+
+let () = define_red2 "eval_cbn" begin fun flags c ->
+  let flags = to_red_flag flags in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_cbn flags c
+end
+
+let () = define_red2 "eval_lazy" begin fun flags c ->
+  let flags = to_red_flag flags in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_lazy flags c
+end
+
+let () = define_red2 "eval_unfold" begin fun refs c ->
+  let map v = to_pair Value.to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
+  let refs = Value.to_list map refs in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_unfold refs c
+end
+
+let () = define_red2 "eval_fold" begin fun args c ->
+  let args = Value.to_list Value.to_constr args in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_fold args c
+end
+
+let () = define_red2 "eval_pattern" begin fun where c ->
+  let where = Value.to_list (fun p -> to_pair Value.to_constr (fun occ -> to_occurrences to_int_or_var occ) p) where in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_pattern where c
+end
+
+let () = define_red2 "eval_vm" begin fun where c ->
+  let where = Value.to_option to_pattern_with_occs where in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_vm where c
+end
+
+let () = define_red2 "eval_native" begin fun where c ->
+  let where = Value.to_option to_pattern_with_occs where in
+  let c = Value.to_constr c in
+  Tac2tactics.eval_native where c
+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 25a00fdc2e..a95e60bc97 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -122,6 +122,63 @@ let native where cl =
   let where = Option.map map_pattern_with_occs where in
   Tactics.reduce (CbvNative where) cl
 
+let eval_fun red c =
+  Tac2core.pf_apply begin fun env sigma ->
+  let (redfun, _) = Redexpr.reduction_of_red_expr env red in
+  let (sigma, ans) = redfun env sigma c in
+  Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+  Proofview.tclUNIT ans
+  end
+
+let eval_red c =
+  eval_fun (Red false) c
+
+let eval_hnf c =
+  eval_fun Hnf c
+
+let eval_simpl flags where c =
+  let where = Option.map map_pattern_with_occs where in
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  eval_fun (Simpl (flags, where)) c
+
+let eval_cbv flags c =
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  eval_fun (Cbv flags) c
+
+let eval_cbn flags c =
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  eval_fun (Cbn flags) c
+
+let eval_lazy flags c =
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  eval_fun (Lazy flags) c
+
+let eval_unfold occs c =
+  let map (gr, occ) =
+    get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
+  in
+  Proofview.Monad.List.map map occs >>= fun occs ->
+  eval_fun (Unfold occs) c
+
+let eval_fold cl c =
+  eval_fun (Fold cl) c
+
+let eval_pattern where c =
+  let where = List.map (fun (pat, occ) -> (occ, pat)) where in
+  eval_fun (Pattern where) c
+
+let eval_vm where c =
+  let where = Option.map map_pattern_with_occs where in
+  eval_fun (CbvVm where) c
+
+let eval_native where c =
+  let where = Option.map map_pattern_with_occs where in
+  eval_fun (CbvNative where) c
+
 let on_destruction_arg tac ev arg =
   Proofview.Goal.enter begin fun gl ->
   match arg with
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index 8939d2a9dd..87489bb248 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -9,6 +9,7 @@
 open Names
 open Locus
 open Globnames
+open EConstr
 open Genredexpr
 open Misctypes
 open Tactypes
@@ -54,6 +55,29 @@ val vm : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit ta
 
 val native : (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
 
+val eval_red : constr -> constr tactic
+
+val eval_hnf : constr -> constr tactic
+
+val eval_simpl : global_reference glob_red_flag ->
+  (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+
+val eval_cbv : global_reference glob_red_flag -> constr -> constr tactic
+
+val eval_cbn : global_reference glob_red_flag -> constr -> constr tactic
+
+val eval_lazy : global_reference glob_red_flag -> constr -> constr tactic
+
+val eval_unfold : (global_reference * occurrences_expr) list -> constr -> constr tactic
+
+val eval_fold : constr list -> constr -> constr tactic
+
+val eval_pattern : (EConstr.t * occurrences_expr) list -> constr -> constr tactic
+
+val eval_vm : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+
+val eval_native : (Pattern.constr_pattern * occurrences_expr) option -> constr -> constr tactic
+
 val discriminate : evars_flag -> destruction_arg option -> unit tactic
 
 val injection : evars_flag -> intro_pattern list option -> destruction_arg option -> unit tactic