From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- checker/validate.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) (limited to 'checker/validate.ml') diff --git a/checker/validate.ml b/checker/validate.ml index 804bf7df..ab17aa7f 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -41,6 +41,8 @@ let pr_obj o = pr_obj_rec o; Format.print_newline() exception ValidObjError of string * Obj.t let fail o s = raise (ValidObjError(s,o)) +let ep s1 f s2 = f (s1^"/"^s2) + let apply debug f x = let o = Obj.repr x in try f o @@ -49,7 +51,7 @@ let apply debug f x = print_endline ("Validation failed: "^msg); pr_obj obj end; - failwith "validation failed" + failwith "vo structure validation failed" (* data not validated *) let no_val (o:Obj.t) = () @@ -71,8 +73,7 @@ let val_block s o = let val_tuple s v o = 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 + if Obj.size o = n then Array.iteri (fun i f -> f (Obj.field o i)) v else fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)) @@ -88,7 +89,7 @@ let val_sum s cc vv 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^": max is "^string_of_int i)) + else fail o ("bad tag in (sum type) "^s^": found "^string_of_int i)) else if Obj.is_int o then let (n:int) = Obj.magic o in (if n<0 || n>=cc then @@ -161,11 +162,14 @@ let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|] let val_mp = val_rec_sum "module_path" 0 - (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|]) + (fun vmp -> [|[|val_dp|];[|val_uid|];[|vmp;val_id|]|]) let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] -let val_ind = val_tuple "inductive"[|val_kn;val_int|] +let val_con = + val_tuple "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|] (* univ *) -- cgit v1.2.3