Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

206 lines (167 sloc) 6.538 kb
(* 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)^"\"")
Format.print_string "?"
(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())
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
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
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)
(* 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|]|])
(* 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|])
Jump to Line
Something went wrong with that request. Please try again.