Hiding tactic value representations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16570 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 53 insertions, 28 deletions

diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 5556912ebb..03d7c645e4 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -193,9 +193,9 @@ let exec_tactic env n f args =
     Tacinterp.eval_tactic(ltac_call f (args@[getter])) (dummy_goal env) in
   !res
 
-let constr_of = function
-  | VConstr ([],c) -> c
-  | _ -> failwith "Ring.exec_tactic: anomaly"
+let constr_of v = match Value.to_constr v with
+  | Some c -> c
+  | None -> failwith "Ring.exec_tactic: anomaly"
 
 let stdlib_modules =
   [["Coq";"Setoids";"Setoid"];
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 21e120a7e7..2c0ca8fd1d 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -50,13 +50,13 @@ let occurrences_of = function
         Errors.error "Illegal negative occurrence number.";
       OnlyOccurrences nl
 
-let coerce_to_int = function
-  | VInteger n -> n
-  | v -> raise (CannotCoerceTo "an integer")
+let coerce_to_int v = match Value.to_int v with
+  | None -> raise (CannotCoerceTo "an integer")
+  | Some n -> n
 
-let int_list_of_VList = function
-  | VList l -> List.map (fun n -> coerce_to_int n) l
-  | _ -> raise Not_found
+let int_list_of_VList v = match Value.to_list v with
+| Some l -> List.map (fun n -> coerce_to_int n) l
+| _ -> raise (CannotCoerceTo "an integer")
 
 let interp_occs ist gl l =
   match l with
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1458cd73bd..e142b93498 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -66,6 +66,30 @@ type value =
   | VList of value list
   | VRec of (Id.t*value) list ref * glob_tactic_expr
 
+module Value =
+struct
+
+type t = value
+
+let of_constr c = VConstr ([], c)
+
+let to_constr = function
+| VConstr (vars, c) ->
+  let () = assert (List.is_empty vars) in Some c
+| _ -> None
+
+let of_int i = VInteger i
+
+let to_int = function
+| VInteger i -> Some i
+| _ -> None
+
+let to_list = function
+| VList l -> Some l
+| _ -> None
+
+end
+
 let dloc = Loc.ghost
 
 let catch_error call_trace tac g =
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 48ba28e11d..7c04899f30 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -19,21 +19,21 @@ open Mod_subst
 open Redexpr
 open Misctypes
 
+module Value :
+sig
+  type t
+  val of_constr : constr -> t
+  val to_constr : t -> constr option
+  val of_int : int -> t
+  val to_int : t -> int option
+  val to_list : t -> t list option
+end
+
 (** Values for interpretation *)
-type value =
-  | VRTactic of (goal list sigma)
-  | VFun of ltac_trace * (Id.t*value) list *
-      Id.t option list * glob_tactic_expr
-  | VVoid
-  | VInteger of int
-  | VIntroPattern of intro_pattern_expr
-  | VConstr of Pattern.constr_under_binders
-  | VConstr_context of constr
-  | VList of value list
-  | VRec of (Id.t*value) list ref * glob_tactic_expr
+type value = Value.t
 
 (** Signature for interpretation: val\_interp and interpretation functions *)
-and interp_sign =
+type interp_sign =
   { lfun : (Id.t * value) list;
     avoid_ids : Id.t list;
     debug : debug_info;
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index b9a9d4d839..0d160e7255 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -20,9 +20,10 @@ open Errors
 open Util
 
 let assoc_var s ist =
-  match List.assoc (Names.Id.of_string s) ist.lfun with
-    | VConstr ([],c) -> c
-    | _ -> failwith "tauto: anomaly"
+  let v = List.assoc (Names.Id.of_string s) ist.lfun in
+  match Value.to_constr v with
+    | Some c -> c
+    | None -> failwith "tauto: anomaly"
 
 (** Parametrization of tauto *)
 
@@ -134,8 +135,8 @@ let flatten_contravariant_conj flags ist =
           ~onlybinary:flags.binary_mode typ
   with
   | Some (_,args) ->
-      let newtyp = valueIn (VConstr ([],List.fold_right mkArrow args c)) in
-      let hyp = valueIn (VConstr ([],hyp)) in
+      let newtyp = valueIn (Value.of_constr (List.fold_right mkArrow args c)) in
+      let hyp = valueIn (Value.of_constr hyp) in
       let intros =
 	iter_tac (List.map (fun _ -> <:tactic< intro >>) args)
 	<:tactic< idtac >> in
@@ -170,9 +171,9 @@ let flatten_contravariant_disj flags ist =
           ~onlybinary:flags.binary_mode
           typ with
   | Some (_,args) ->
-      let hyp = valueIn (VConstr ([],hyp)) in
+      let hyp = valueIn (Value.of_constr hyp) in
       iter_tac (List.map_i (fun i arg ->
-	let typ = valueIn (VConstr ([],mkArrow arg c)) in
+	let typ = valueIn (Value.of_constr (mkArrow arg c)) in
 	let i = Tacexpr.Integer i in
 	<:tactic<
           let typ := $typ in