From 376e61185dadea415d6b7d2df45dc7236e901e5b Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 6 May 2008 18:31:25 +0000 Subject: checker deals with polymorphic constants and module aliases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10892 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/validate.ml | 163 +++++++++++++++++++++++++++++++++------------------- 1 file changed, 103 insertions(+), 60 deletions(-) (limited to 'checker/validate.ml') diff --git a/checker/validate.ml b/checker/validate.ml index 2eb1ec0cf..86e51b7b9 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,5 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* n-1 then (Format.print_string ","; Format.print_cut()) done; Format.close_box(); Format.print_string ")") else Format.print_string "?" -let pr_obj o = pr_obj o; Format.print_newline() - +let pr_obj o = pr_obj_rec o; Format.print_newline() +(**************************************************************************) +(* Low-level validators *) +(* data not validated *) let no_val (o:Obj.t) = () +(* Check that object o is a block with tag t *) let val_tag t o = if Obj.is_block o && Obj.tag o = t then () else failwith ("tag "^string_of_int t) -let val_tuple s v o = - let n = Array.length v in +let val_obj s o = if Obj.is_block o then - if Obj.size o = n then - Array.iteri (fun i f -> f (Obj.field o i)) v - else - (pr_obj o; - failwith - ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))) - else failwith ("tuple:" ^s) + (if Obj.tag o > Obj.no_scan_tag then + failwith (s^". Not a normal tag")) + else failwith (s^". Not a block") +(* 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 n = Array.length v in + val_obj ("tuple: "^s) o; + if Obj.size o = n then + Array.iteri (fun i f -> f (Obj.field o i)) v + else + (pr_obj o; + failwith + ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))) + +(* 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. + 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 = if Obj.is_block o then + (val_obj ("sum: "^s) o; let n = Array.length vv in let i = Obj.tag o in if i < n then val_tuple (s^"("^string_of_int i^")") vv.(i) o - else failwith ("bad tag in sum: "^string_of_int i) + else failwith ("bad tag in sum ("^s^"): "^string_of_int i)) else if Obj.is_int o then let (n:int) = Obj.magic o in - (if n<0 || n>=cc then failwith "bad constant constructor") - else failwith "not a sum" + (if n<0 || n>=cc then failwith ("bad constant constructor ("^s^")")) + else failwith ("not a sum ("^s^")") +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 + +(**************************************************************************) +(* Builtin types *) + +(* Check the o is an array of values satisfying f. *) let val_array f o = - if Obj.is_block o then - for i = 0 to Obj.size o - 1 do - (f (Obj.field o i):unit) - done - else failwith "not array" -(* -let val_tuple s v o = - prerr_endline ("TUPLE "^s); - val_tuple s v o; - prerr_endline ("END "^s) -let val_sum s cc vv o = - prerr_endline ("SUM "^s); - val_sum s cc vv o; - prerr_endline ("END "^s) -let val_array f o = - prerr_endline "ARRAY"; - val_array f o; - prerr_endline "END ARRAY" -*) -let val_int o = if not (Obj.is_int o) then failwith "not int" -(*; prerr_endline "INT" -*) + val_obj "array" o; + for i = 0 to Obj.size o - 1 do + (f (Obj.field o i):unit) + done + +(* Integer validator *) +let val_int o = + if not (Obj.is_int o) then failwith "expected an int" + +(* String validator *) let val_str s = val_tag Obj.string_tag s -(*; prerr_endline ("STR "^Obj.magic s)*) -let val_bool o = val_sum "bool" 2 [||] o +(* Booleans *) +let val_bool = val_enum "bool" 2 +(* Option type *) let val_opt f = val_sum "option" 1 [|[|f|]|] -let rec val_list f o = - val_sum "list" 1 [|[|f;val_list f|]|] o +(* Lists *) +let val_list f = + val_rec_sum "list" 1 (fun vlist -> [|[|f;vlist|]|]) +(* Reference *) let val_ref f = val_tuple "ref" [|f|] -let rec val_set f o = - val_sum "set" 1 [|[|val_set f;f;val_set f;val_int|]|] o -let rec val_map fk fv o = - val_sum "map" 1 [|[|val_map fk fv;fk;fv;val_map fk fv;val_int|]|] o +(**************************************************************************) +(* Standard library types *) + +(* Sets *) +let val_set f = + val_rec_sum "set" 1 (fun vset -> [|[|vset;f;vset;val_int|]|]) + +(* Maps *) +let rec val_map fk fv = + val_rec_sum "map" 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|]) -(* Coq *) +(**************************************************************************) +(* Coq types *) let val_id = val_str @@ -103,27 +141,31 @@ let val_name = val_sum "name" 1 [|[|val_id|]|] let val_uid = val_tuple "uid" [|val_int;val_str;val_dp|] -let rec val_mp o = - val_sum "mp" 0 [|[|val_dp|];[|val_uid|];[|val_uid|];[|val_mp;val_id|]|] o +let val_mp = + val_rec_sum "mp" 0 + (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|]) let val_kn = val_tuple "kn" [|val_mp;val_dp;val_id|] let val_ind = val_tuple "ind"[|val_kn;val_int|] let val_cstr = val_tuple "cstr"[|val_ind;val_int|] -let val_ci = no_val +let val_ci = + let val_cstyle = val_enum "case_style" 5 in + let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in + val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|] -let val_cast = no_val 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 (val_tuple"univ_cstr"[|val_level;val_sum "order" 3[||];val_level|]) + val_set (val_tuple"univ_cstr"[|val_level;val_enum "order" 3;val_level|]) -let val_sort = val_sum "sort" 0 [|[|val_sum "cnt" 2 [||]|];[|val_univ|]|] -let val_sortfam = val_sum "sort_family" 3 [||] +let val_cast = val_enum "cast_kind" 2 +let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|] +let val_sortfam = val_enum "sort_family" 3 let val_evar f = val_tuple "evar" [|val_int;val_array f|] @@ -134,7 +176,7 @@ let val_fix f = let val_cofix f = val_tuple"cofix"[|val_int;val_prec f|] -let rec val_constr o = val_sum "constr" 0 [| +let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [| [|val_int|]; (* Rel *) [|val_id|]; (* Var *) [|val_int|]; (* Meta *) @@ -151,7 +193,7 @@ let rec val_constr o = val_sum "constr" 0 [| [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *) [|val_fix val_constr|]; (* Fix *) [|val_cofix val_constr|] (* CoFix *) -|] o +|]) let val_ndecl = val_tuple"ndecl"[|val_id;val_opt val_constr;val_constr|] @@ -161,7 +203,7 @@ let val_rctxt = val_list val_rdecl let val_arity = val_tuple"arity"[|val_rctxt;val_constr|] -let val_eng = val_sum "eng" 1 [||] +let val_eng = val_enum "eng" 1 let val_pol_arity = val_tuple"pol_arity"[|val_list(val_opt val_univ);val_univ|] let val_cst_type = @@ -185,9 +227,10 @@ let val_cb = val_tuple "cb" let val_recarg = val_sum "recarg" 1 [|[|val_int|];[|val_ind|]|] -let rec val_wfp o = val_sum "wf_paths" 0 - [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|]; - [|val_int;val_array val_wfp|]|] o +let val_wfp = val_rec_sum "wf_paths" 0 + (fun val_wfp -> + [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|]; + [|val_int;val_array val_wfp|]|]) let val_mono_ind_arity = val_tuple"mono_ind_arity"[|val_constr;val_sort|] let val_ind_arity = val_sum "ind_arity" 0 -- cgit v1.2.3