From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- checker/validate.ml | 120 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 71 insertions(+), 49 deletions(-) (limited to 'checker/validate.ml') diff --git a/checker/validate.ml b/checker/validate.ml index 7d368f05..c5e0bd34 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* f ctx) +let ext s f (ctx:error_context) = f (ctx/s) + -let ep s1 f s2 = f (s1^"/"^s2) +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 o - with ValidObjError(msg,obj) -> + 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 (o:Obj.t) = () +let no_val (c:error_context) (o:Obj.t) = () (* Check that object o is a block with tag t *) -let val_tag t o = +let val_tag t ctx o = if Obj.is_block o && Obj.tag o = t then () - else fail o ("expected tag "^string_of_int t) + else fail ctx o ("expected tag "^string_of_int t) -let val_block s o = +let val_block ctx o = if Obj.is_block o then (if Obj.tag o > Obj.no_scan_tag then - fail o (s^": found no scan tag")) - else fail o (s^": expected block obj") + 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 s v o = +let val_tuple ?name v ctx o = + let ctx = match name with + Some n -> ctx/n + | _ -> ctx in let n = Array.length v in - val_block ("tuple: "^s) o; - if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v + 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 o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)) + 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 @@ -83,70 +96,79 @@ let val_tuple s v o = 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 s cc vv o = +let val_sum name cc vv ctx o = + let ctx = ctx/name in if Obj.is_block o then - (val_block s o; + (val_block (ctx/name) o; let n = Array.length vv in let i = Obj.tag o in - if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o - else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i)) + 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 o (s^": bad constant constructor "^string_of_int n)) - else fail o ("not a sum ("^s^")") + 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 s cc f o = - val_sum s cc (f (val_rec_sum s cc f)) o - -let rec val_rectype f o = - f (val_rectype f) o +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 ?(name="array") f o = - val_block name o; +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 (Obj.field o i):unit) + (f (upd_ctx i) (Obj.field o i):unit) done (* Integer validator *) -let val_int o = - if not (Obj.is_int o) then fail o "expected an int" +let val_int ctx o = + if not (Obj.is_int o) then fail ctx o "expected an int" (* String validator *) -let val_str o = - try val_tag Obj.string_tag o - with Failure _ -> fail o "expected a string" +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|]|] +let val_opt ?(name="option") f = + val_sum name 1 [|[|f|]|] (* Lists *) -let val_list ?(name="list") f = - val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|]) +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 = val_tuple name [|f|] +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;f;vset;val_int|]|]) + 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;fk;fv;vmap;val_int|]|]) + val_rec_sum name 1 + (fun vmap -> + [|[|vmap; ext "key" fk; ext "value" fv; + vmap; ext "bal" val_int|]|]) (**************************************************************************) (* Coq types *) @@ -158,19 +180,19 @@ let val_dp = val_list ~name:"dirpath" val_id let val_name = val_sum "name" 1 [|[|val_id|]|] -let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|] +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 "kernel_name" [|val_mp;val_dp;val_id|] +let val_kn = val_tuple ~name:"kernel_name" [|val_mp;val_dp;val_id|] let val_con = - val_tuple "constant/mutind" [|val_kn;val_kn|] + val_tuple ~name:"constant/mutind" [|val_kn;val_kn|] -let val_ind = val_tuple "inductive"[|val_con;val_int|] -let val_cstr = val_tuple "constructor"[|val_ind;val_int|] +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|]|] @@ -179,5 +201,5 @@ let val_univ = val_sum "univ" 0 let val_cstrs = val_set ~name:"Univ.constraints" - (val_tuple "univ_constraint" + (val_tuple ~name:"univ_constraint" [|val_level;val_enum "order_request" 3;val_level|]) -- cgit v1.2.3