From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- checker/validate.ml | 188 +++++++++++++++++++--------------------------------- 1 file changed, 67 insertions(+), 121 deletions(-) (limited to 'checker/validate.ml') 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 *) -(* 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" -- cgit v1.2.3