Checker: vo validation checks the absence of Var/Evar/Meta

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

4 files changed, 12 insertions, 8 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 8682254e9..d55a9d5c0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -81,9 +81,9 @@ type 'constr pcofixpoint =
 
 type constr =
   | Rel       of int
-  | Var       of Id.t
-  | Meta      of metavariable
-  | Evar      of constr pexistential
+  | Var       of Id.t (** Shouldn't occur in a .vo *)
+  | Meta      of metavariable (** Shouldn't occur in a .vo *)
+  | Evar      of constr pexistential (** Shouldn't occur in a .vo *)
   | Sort      of sorts
   | Cast      of constr * cast_kind * constr
   | Prod      of Name.t * constr * constr
diff --git a/checker/validate.ml b/checker/validate.ml
index 4c5ca184e..b0c1704ee 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -69,6 +69,7 @@ let rec val_gen v ctx o = match v with
     (try val_tag Obj.string_tag ctx o
      with Failure _ -> fail ctx o "expected a string")
   | Any -> ()
+  | Fail -> fail ctx o "unexpected object"
   | Annot (s,v) -> val_gen v (ctx/s) o
 
 (* Check that an object is a tuple (or a record). vs is an array of
diff --git a/checker/values.ml b/checker/values.ml
index 5b3343991..b05085ae4 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 9a9abd32a97761c8de8902f314cb0649  checker/cic.mli
+MD5 1e607e046b15faeee5912eda83dbb1ba  checker/cic.mli
 
 *)
 
@@ -22,6 +22,7 @@ MD5 9a9abd32a97761c8de8902f314cb0649  checker/cic.mli
     could become automatically generated someday ?
 
     - [Any] stands for a value that we won't check,
+    - [Fail] means a value that shouldn't be there at all,
     - [Tuple] provides a name and sub-values in this block
     - [Sum] provides a name, a number of constant constructors,
       and sub-values at each position of each possible constructed
@@ -32,6 +33,7 @@ MD5 9a9abd32a97761c8de8902f314cb0649  checker/cic.mli
 
 type value =
   | Any
+  | Fail
   | Tuple of string * value array
   | Sum of string * int * value array array
   | Array of value
@@ -111,9 +113,9 @@ let v_cast = v_enum "cast_kind" 3
 let rec v_constr =
   Sum ("constr",0,[|
     [|Int|]; (* Rel *)
-    [|v_id|]; (* Var *)
-    [|Int|]; (* Meta *)
-    [|v_evar|]; (* Evar *)
+    [|Fail|]; (* Var *)
+    [|Fail|]; (* Meta *)
+    [|Fail|]; (* Evar *)
     [|v_sort|]; (* Sort *)
     [|v_constr;v_cast;v_constr|]; (* Cast *)
     [|v_name;v_constr;v_constr|]; (* Prod *)
@@ -128,7 +130,6 @@ let rec v_constr =
     [|v_cofix|] (* CoFix *)
   |])
 
-and v_evar = Tuple ("pexistential",[|Int;Array v_constr|])
 and v_prec = Tuple ("prec_declaration",
                     [|Array v_name; Array v_constr; Array v_constr|])
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
diff --git a/checker/votour.ml b/checker/votour.ml
index 19c188310..4e8729033 100644
--- a/checker/votour.ml
+++ b/checker/votour.ml
@@ -14,6 +14,7 @@ open Values
 
 let rec get_name ?(extra=false) = function
   |Any -> "?"
+  |Fail -> assert false
   |Tuple (name,_) -> name
   |Sum (name,_,_) -> name
   |Array v -> "array"^(if extra then "/"^get_name ~extra v else "")
@@ -79,6 +80,7 @@ let rec get_children v o pos = match v with
     if Obj.is_block o && Obj.tag o < Obj.no_scan_tag then
       Array.init (Obj.size o) (fun i -> (Any,Obj.field o i,i::pos))
     else [||]
+  |Fail -> assert false
 
 type info = {
   nam : string;