aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/validate.ml
blob: 2f46695cd26aaf76274c5f62b1e43ca4fdcb9546 (plain)
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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
(************************************************************************)
(*  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
let overr (ctx:error_context) f = (fun (_:error_context) -> f ctx) 
let ext s f (ctx:error_context) = f (ctx/s)


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

let apply debug f x =
  let o = Obj.repr x in
  try f 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"

(* data not validated *)
let no_val (c:error_context) (o:Obj.t) = ()

(* 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"

(* Check that an object is a tuple (or a record). v is an array of
   validation functions for each field. Its size corresponds to the
   expected size of the object. *)
let val_tuple ?name v ctx o =
  let ctx = match name with
      Some n -> ctx/n
    | _ -> ctx in
  let n = Array.length v in
  let val_fld i f =
    f (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 v
  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
   validation functions to be applied to 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. *)
let 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"

let val_enum s n = val_sum s n [||]

(* Recursive types: avoid looping by eta-expansion *)
let rec val_rec_sum name cc f ctx o =
  val_sum name cc (f (overr (ctx/name) (val_rec_sum name cc f))) ctx o

(**************************************************************************)
(* Builtin types *)

(* Check the o is an array of values satisfying f. *)
let val_array ?(pos=false) f ctx o =
  let upd_ctx =
    if pos then (fun i -> ctx/string_of_int i) else (fun _ -> ctx) in
  val_block (ctx/"array") o;
  for i = 0 to Obj.size o - 1 do
    (f (upd_ctx i) (Obj.field o i):unit)
  done

(* Integer validator *)
let val_int ctx o =
  if not (Obj.is_int o) then fail ctx o "expected an int"

(* String validator *)
let val_str ctx o =
  try val_tag Obj.string_tag ctx o
  with Failure _ -> fail ctx o "expected a string"

(* Booleans *)
let val_bool = val_enum "bool" 2

(* Option type *)
let val_opt ?(name="option") f =
  val_sum name 1 [|[|f|]|]

(* Lists *)
let val_list ?(name="list") f ctx =
  val_rec_sum name 1 (fun vlist -> [|[|ext "elem" f;vlist|]|])
    ctx

(* Reference *)
let val_ref ?(name="ref") f ctx =
  val_tuple [|f|] (ctx/name)

(**************************************************************************)
(* Standard library types *)

(* Sets *)
let val_set ?(name="Set.t") f =
  val_rec_sum name 1
    (fun vset -> [|[|vset;ext "elem" f;
		     vset;ext "bal" val_int|]|])

(* Maps *)
let rec val_map ?(name="Map.t") fk fv =
  val_rec_sum name 1
    (fun vmap ->
       [|[|vmap; ext "key" fk; ext "value" fv;
	   vmap; ext "bal" val_int|]|])

(**************************************************************************)
(* Coq types *)

(* names *)
let val_id = val_str

let val_dp = val_list ~name:"dirpath" val_id

let val_name = val_sum "name" 1 [|[|val_id|]|]

let val_uid = val_tuple ~name:"uniq_ident" [|val_int;val_str;val_dp|]

let val_mp =
  val_rec_sum "module_path" 0
    (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|])

let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|]

let val_con =
  val_tuple ~name:"constant/mutind" [|val_kn;val_kn|]

let val_ind = val_tuple ~name:"inductive"[|val_con;val_int|]
let val_cstr = val_tuple ~name:"constructor"[|val_ind;val_int|]

(* univ *)
let val_level = val_sum "level" 1 [|[|val_int;val_dp|]|]
let val_univ = val_sum "univ" 0
  [|[|val_level|];[|val_list val_level;val_list val_level|]|]

let val_cstrs =
  val_set ~name:"Univ.constraints"
   (val_tuple ~name:"univ_constraint"
     [|val_level;val_enum "order_request" 3;val_level|])