From 62c6c0ccc1930a556eeeab9b7a2050929cd790f1 Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 19 Feb 2010 10:43:17 +0000 Subject: [checker] fixed vo validation problems, module incompatibilities remain git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12799 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/validate.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'checker/validate.ml') diff --git a/checker/validate.ml b/checker/validate.ml index 804bf7dfe..704468169 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,9 +162,11 @@ 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_kn = + let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|] in + val_tuple "kn*kn" [|val_kn;val_kn|] let val_ind = val_tuple "inductive"[|val_kn;val_int|] let val_cstr = val_tuple "constructor"[|val_ind;val_int|] -- cgit v1.2.3