aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-15 16:05:27 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-04-15 16:05:27 +0000
commitd3097cd34ffffda5dbe332ee88fd33d54180fad9 (patch)
treeb634215effd11bfa01b25750522c441013a2ced2 /checker
parent4bd2e928e3b8d463bb793ad814ff42abdabf9611 (diff)
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
Diffstat (limited to 'checker')
-rw-r--r--checker/cic.mli6
-rw-r--r--checker/validate.ml1
-rw-r--r--checker/values.ml11
-rw-r--r--checker/votour.ml2
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;