diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:00 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-15 16:05:00 +0000 |
commit | 07c80f246315ac314c82d580bf356df3fb8201d8 (patch) | |
tree | f911826b7040f89ecb4f092969d22b4477e4449b /checker/validate.ml | |
parent | 56c88d763b0cf636a740f531bd7d734426769d7d (diff) |
Checker: reified encoding of .vo types in values.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/validate.ml')
-rw-r--r-- | checker/validate.ml | 155 |
1 files changed, 40 insertions, 115 deletions
diff --git a/checker/validate.ml b/checker/validate.ml index 649b2cdd6..4c5ca184e 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -39,29 +39,12 @@ let pr_obj o = pr_obj_rec o; Format.print_newline() 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 () @@ -73,30 +56,46 @@ 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 +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. *) -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/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 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 = +and val_sum name cc vv ctx o = let ctx = ctx/name in if Obj.is_block o then (val_block (ctx/name) o; @@ -111,94 +110,20 @@ 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 +and val_array v ctx o = val_block (ctx/"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 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_sum "constant/mutind" 0 [|[|val_kn|];[|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|]) +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" |