Use references in reduction tactics.

We dynamically check that the provided references are indeed evaluable
ones, instead of ensuring this at internalization time.

3 files changed, 56 insertions, 13 deletions

diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index e3b0d6bf6b..d3430213b4 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -8,6 +8,7 @@
 
 open Names
 open Locus
+open Globnames
 open Misctypes
 open Genredexpr
 open Tac2expr
@@ -70,9 +71,11 @@ let to_clause = function
   { onhyps = hyps; concl_occs = to_occurrences to_int_or_var concl; }
 | _ -> assert false
 
-let to_evaluable_ref = function
-| ValBlk (0, [| id |]) -> EvalVarRef (Value.to_ident id)
-| ValBlk (1, [| cst |]) -> EvalConstRef (Value.to_constant cst)
+let to_reference = function
+| ValBlk (0, [| id |]) -> VarRef (Value.to_ident id)
+| ValBlk (1, [| cst |]) -> ConstRef (Value.to_constant cst)
+| ValBlk (2, [| ind |]) -> IndRef (Value.to_ext Value.val_inductive ind)
+| ValBlk (3, [| cstr |]) -> ConstructRef (Value.to_ext Value.val_constructor cstr)
 | _ -> assert false
 
 let to_red_flag = function
@@ -84,7 +87,7 @@ let to_red_flag = function
     rCofix = Value.to_bool cofix;
     rZeta = Value.to_bool zeta;
     rDelta = Value.to_bool delta;
-    rConst = Value.to_list to_evaluable_ref const;
+    rConst = Value.to_list to_reference const;
   }
 | _ -> assert false
 
@@ -310,29 +313,26 @@ end
 let () = define_prim2 "tac_cbv" begin fun flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
-  Tactics.reduce (Cbv flags) cl
+  Tac2tactics.cbv flags cl
 end
 
 let () = define_prim2 "tac_cbn" begin fun flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
-  Tactics.reduce (Cbn flags) cl
+  Tac2tactics.cbn flags cl
 end
 
 let () = define_prim2 "tac_lazy" begin fun flags cl ->
   let flags = to_red_flag flags in
   let cl = to_clause cl in
-  Tactics.reduce (Lazy flags) cl
+  Tac2tactics.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 map v = to_pair to_reference (fun occ -> to_occurrences to_int_or_var occ) v in
   let refs = Value.to_list map refs in
   let cl = to_clause cl in
-  Tactics.reduce (Unfold refs) cl
+  Tac2tactics.unfold refs cl
 end
 
 let () = define_prim2 "tac_fold" begin fun args cl ->
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml
index 7fdda1f17d..2f4965783f 100644
--- a/src/tac2tactics.ml
+++ b/src/tac2tactics.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
 open Util
 open Names
 open Globnames
@@ -13,6 +14,7 @@ open Misctypes
 open Tactypes
 open Genredexpr
 open Proofview
+open Proofview.Notations
 
 (** FIXME: export a better interface in Tactics *)
 let delayed_of_tactic tac env sigma =
@@ -67,10 +69,42 @@ let map_pattern_with_occs (pat, occ) = match pat with
 | Pattern.PRef (VarRef id) -> (occ, Inl (EvalVarRef id))
 | _ -> (occ, Inr pat)
 
+let get_evaluable_reference = function
+| VarRef id -> Proofview.tclUNIT (EvalVarRef id)
+| ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst)
+| r ->
+  Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++
+    Nametab.pr_global_env Id.Set.empty r ++ spc () ++
+    str "to an evaluable reference.")
+
 let simpl flags where cl =
   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
   Tactics.reduce (Simpl (flags, where)) cl
 
+let cbv flags cl =
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  Tactics.reduce (Cbv flags) cl
+
+let cbn flags cl =
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  Tactics.reduce (Cbn flags) cl
+
+let lazy_ flags cl =
+  Proofview.Monad.List.map get_evaluable_reference flags.rConst >>= fun rConst ->
+  let flags = { flags with rConst } in
+  Tactics.reduce (Lazy flags) cl
+
+let unfold occs cl =
+  let map (gr, occ) =
+    get_evaluable_reference gr >>= fun gr -> Proofview.tclUNIT (occ, gr)
+  in
+  Proofview.Monad.List.map map occs >>= fun occs ->
+  Tactics.reduce (Unfold occs) cl
+
 let vm where cl =
   let where = Option.map map_pattern_with_occs where in
   Tactics.reduce (CbvVm where) cl
diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli
index affbbbbdd7..d835f768a1 100644
--- a/src/tac2tactics.mli
+++ b/src/tac2tactics.mli
@@ -8,6 +8,7 @@
 
 open Names
 open Locus
+open Globnames
 open Genredexpr
 open Misctypes
 open Tactypes
@@ -36,9 +37,17 @@ type rewriting =
 val rewrite :
   evars_flag -> rewriting list -> clause -> unit tactic option -> unit tactic
 
-val simpl : evaluable_global_reference glob_red_flag ->
+val simpl : global_reference glob_red_flag ->
   (Pattern.constr_pattern * occurrences_expr) option -> clause -> unit tactic
 
+val cbv : global_reference glob_red_flag -> clause -> unit tactic
+
+val cbn : global_reference glob_red_flag -> clause -> unit tactic
+
+val lazy_ : global_reference glob_red_flag -> clause -> unit tactic
+
+val unfold : (global_reference * occurrences_expr) list -> 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