1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* This module defines validation functions to ensure an imported
value (using input_value) has the correct structure. *)
let rec pr_obj_rec o =
if Obj.is_int o then
Format.print_int(Obj.magic o)
else if Obj.is_block o then
let t = Obj.tag o in
if t > Obj.no_scan_tag then
if t = Obj.string_tag then
Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
else
Format.print_string "?"
else
(let n = Obj.size o in
Format.print_string ("#"^string_of_int t^"(");
Format.open_hvbox 0;
for i = 0 to n-1 do
pr_obj_rec (Obj.field o i);
if i<>n-1 then (Format.print_string ","; Format.print_cut())
done;
Format.close_box();
Format.print_string ")")
else Format.print_string "?"
let pr_obj o = pr_obj_rec o; Format.print_newline()
(**************************************************************************)
(* Obj low-level validators *)
type error_context = string list
let mt_ec : error_context = []
let (/) (ctx:error_context) s : error_context = s::ctx
exception ValidObjError of string * error_context * Obj.t
let fail ctx o s = raise (ValidObjError(s,ctx,o))
type func = error_context -> Obj.t -> unit
(* Check that object o is a block with tag t *)
let val_tag t ctx o =
if Obj.is_block o && Obj.tag o = t then ()
else fail ctx o ("expected tag "^string_of_int t)
let val_block ctx o =
if Obj.is_block o then
(if Obj.tag o > Obj.no_scan_tag then
fail ctx o "block: found no scan tag")
else fail ctx o "expected block obj"
open Values
let rec val_gen v ctx o = match v with
| Tuple (name,vs) -> val_tuple ~name vs ctx o
| Sum (name,cc,vv) -> val_sum name cc vv ctx o
| Array v -> val_array v ctx o
| List v0 -> val_sum "list" 1 [|[|Annot ("elem",v0);v|]|] ctx o
| Opt v -> val_sum "option" 1 [|[|v|]|] ctx o
| Int -> if not (Obj.is_int o) then fail ctx o "expected an int"
| String ->
(try val_tag Obj.string_tag ctx o
with Failure _ -> fail ctx o "expected a string")
| Any -> ()
| Annot (s,v) -> val_gen v (ctx/s) o
(* Check that an object is a tuple (or a record). vs is an array of
value representation for each field. Its size corresponds to the
expected size of the object. *)
and val_tuple ?name vs ctx o =
let ctx = match name with
| Some n -> ctx/n
| _ -> ctx
in
let n = Array.length vs in
let val_fld i v =
val_gen v (ctx/("fld="^string_of_int i)) (Obj.field o i) in
val_block ctx o;
if Obj.size o = n then Array.iteri val_fld vs
else
fail ctx o
("tuple size: found "^string_of_int (Obj.size o)^
", expected "^string_of_int n)
(* Check that the object is either a constant constructor of tag < cc,
or a constructed variant. each element of vv is an array of
value representations of the constructor arguments.
The size of vv corresponds to the number of non-constant
constructors, and the size of vv.(i) is the expected arity of the
i-th non-constant constructor. *)
and val_sum name cc vv ctx o =
let ctx = ctx/name in
if Obj.is_block o then
(val_block (ctx/name) o;
let n = Array.length vv in
let i = Obj.tag o in
let ctx' = if n=1 then ctx else ctx/("tag="^string_of_int i) in
if i < n then val_tuple vv.(i) ctx' o
else fail ctx' o ("sum: unexpected tag"))
else if Obj.is_int o then
let (n:int) = Obj.magic o in
(if n<0 || n>=cc then
fail ctx o ("bad constant constructor "^string_of_int n))
else fail ctx o "not a sum"
(* Check the o is an array of values satisfying f. *)
and val_array v ctx o =
val_block (ctx/"array") o;
for i = 0 to Obj.size o - 1 do
val_gen v ctx (Obj.field o i)
done
let validate debug v x =
let o = Obj.repr x in
try val_gen v mt_ec o
with ValidObjError(msg,ctx,obj) ->
if debug then begin
print_endline ("Validation failed: "^msg);
print_endline ("Context: "^String.concat"/"(List.rev ctx));
pr_obj obj
end;
failwith "vo structure validation failed"
|
