summaryrefslogtreecommitdiff
path: root/checker/validate.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/validate.ml')
-rw-r--r--checker/validate.ml188
1 files changed, 67 insertions, 121 deletions
diff --git a/checker/validate.ml b/checker/validate.ml
index 67baff73..63180f05 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -36,32 +36,21 @@ let pr_obj o = pr_obj_rec o; Format.print_newline()
(**************************************************************************)
(* Obj low-level validators *)
-type error_context = string list
+type error_frame =
+| CtxAnnot of string
+| CtxType of string
+| CtxField of int
+| CtxTag of int
+
+type error_context = error_frame 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 ()
@@ -73,36 +62,61 @@ let val_block ctx o =
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
+let val_dyn ctx o =
+ let fail () = fail ctx o "expected a Dyn.t" in
+ if not (Obj.is_block o) then fail ()
+ else if not (Obj.size o = 2) then fail ()
+ else if not (Obj.tag (Obj.field o 0) = Obj.int_tag) then fail ()
+ else ()
+
+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 -> ()
+ | Fail s -> fail ctx o ("unexpected object " ^ s)
+ | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o
+ | Dyn -> val_dyn ctx 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. *)
-let val_tuple ?name v ctx o =
+and val_tuple ?name vs 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
+ | Some n -> ctx/CtxType n
+ | _ -> ctx
+ in
+ let n = Array.length vs in
+ let val_fld i v =
+ val_gen v (ctx/(CtxField i)) (Obj.field o i) in
val_block ctx o;
- if Obj.size o = n then Array.iteri val_fld v
+ 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)
+ ", 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.
+ 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. *)
-let val_sum name cc vv ctx o =
- let ctx = ctx/name in
+and val_sum name cc vv ctx o =
+ let ctx = ctx/CtxType name in
if Obj.is_block o then
- (val_block (ctx/name) o;
+ (val_block ctx 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
+ let ctx' = if n=1 then ctx else ctx/CtxTag 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
@@ -111,95 +125,27 @@ let val_sum name cc vv ctx o =
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;
+and val_array v ctx o =
+ val_block (ctx/CtxType "array") o;
for i = 0 to Obj.size o - 1 do
- (f (upd_ctx i) (Obj.field o i):unit)
+ val_gen v ctx (Obj.field o i)
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 print_frame = function
+| CtxType t -> t
+| CtxAnnot t -> t
+| CtxField i -> Printf.sprintf "fld=%i" i
+| CtxTag i -> Printf.sprintf "tag=%i" i
-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_dp;val_int|]|]
-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|])
+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
+ let ctx = List.rev_map print_frame ctx in
+ print_endline ("Validation failed: "^msg);
+ print_endline ("Context: "^String.concat"/"ctx);
+ pr_obj obj
+ end;
+ failwith "vo structure validation failed"
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 02:35:45 +0000