Merge commit 'upstream/8.2-1+dfsg'

1 files changed, 57 insertions, 143 deletions

diff --git a/checker/validate.ml b/checker/validate.ml
index 86e51b7b..804bf7df 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -6,19 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
+(* $Id$ *)
 
 (* This module defines validation functions to ensure an imported
    value (using input_value) has the correct structure. *)
 
 let rec pr_obj_rec o =
   if Obj.is_int o then
-    Format.print_string ("INT:"^string_of_int(Obj.magic o))
+    Format.print_int(Obj.magic o)
   else if Obj.is_block o then
     let t = Obj.tag o in
     if t > Obj.no_scan_tag then
       if t = Obj.string_tag then
-        Format.print_string ("STR:"^Obj.magic o)
+        Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
       else
         Format.print_string "?"
     else
@@ -36,7 +36,20 @@ let rec pr_obj_rec o =
 let pr_obj o = pr_obj_rec o; Format.print_newline()
 
 (**************************************************************************)
-(* Low-level validators *)
+(* Obj low-level validators *)
+
+exception ValidObjError of string * Obj.t
+let fail o s = raise (ValidObjError(s,o))
+
+let apply debug f x =
+  let o = Obj.repr x in
+  try f o
+  with ValidObjError(msg,obj) ->
+    if debug then begin
+      print_endline ("Validation failed: "^msg);
+      pr_obj obj
+    end;
+    failwith "validation failed"
 
 (* data not validated *)
 let no_val (o:Obj.t) = ()
@@ -44,26 +57,24 @@ 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)
+  else fail o ("expected tag "^string_of_int t)
 
-let val_obj s o =
+let val_block s o =
   if Obj.is_block o then
     (if Obj.tag o > Obj.no_scan_tag then
-      failwith (s^". Not a normal tag"))
-  else failwith (s^". Not a block")
+      fail o (s^": found no scan tag"))
+  else fail o (s^": 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 n = Array.length v in
-  val_obj ("tuple: "^s) o;
+  val_block ("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)))
+    fail o ("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
@@ -73,15 +84,16 @@ let val_tuple s v o =
    i-th non-constant constructor. *)
 let val_sum s cc vv o =
   if Obj.is_block o then
-    (val_obj ("sum: "^s) o;
+    (val_block 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 ("^s^"): "^string_of_int i))
+    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 if Obj.is_int o then
     let (n:int) = Obj.magic o in
-    (if n<0 || n>=cc then failwith ("bad constant constructor ("^s^")"))
-  else failwith ("not a sum ("^s^")")
+    (if n<0 || n>=cc then
+      fail o (s^": bad constant constructor "^string_of_int n))
+  else fail o ("not a sum ("^s^")")
 
 let val_enum s n = val_sum s n [||]
 
@@ -89,177 +101,79 @@ let val_enum s n = val_sum s n [||]
 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
+
 (**************************************************************************)
 (* Builtin types *)
 
 (* Check the o is an array of values satisfying f. *)
-let val_array f o =
-  val_obj "array" o;
+let val_array ?(name="array") f o =
+  val_block name 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"
+  if not (Obj.is_int o) then fail o "expected an int"
 
 (* String validator *)
-let val_str s = val_tag Obj.string_tag s
+let val_str o =
+  try val_tag Obj.string_tag o
+  with Failure _ -> fail o "expected a string"
 
 (* Booleans *)
 let val_bool = val_enum "bool" 2
 
 (* Option type *)
-let val_opt f = val_sum "option" 1 [|[|f|]|]
+let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
 
 (* Lists *)
-let val_list f =
-  val_rec_sum "list" 1 (fun vlist -> [|[|f;vlist|]|])
+let val_list ?(name="list") f =
+  val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
 
 (* Reference *)
-let val_ref f = val_tuple "ref" [|f|]
+let val_ref ?(name="ref") f = val_tuple name [|f|]
 
 (**************************************************************************)
 (* Standard library types *)
 
 (* Sets *)
-let val_set f =
-  val_rec_sum "set" 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+let val_set ?(name="Set.t") f =
+  val_rec_sum name 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|]|])
+let rec val_map ?(name="Map.t") fk fv =
+  val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
 
 (**************************************************************************)
 (* Coq types *)
 
+(* names *)
 let val_id = val_str
 
-let val_dp = val_list val_id
+let val_dp = val_list ~name:"dirpath" val_id
 
 let val_name = val_sum "name" 1 [|[|val_id|]|]
 
-let val_uid = val_tuple "uid" [|val_int;val_str;val_dp|]
+let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
 
 let val_mp =
-  val_rec_sum "mp" 0
+  val_rec_sum "module_path" 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 =
-  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_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
 
+let val_ind = val_tuple "inductive"[|val_kn;val_int|]
+let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
 
+(* univ *)
 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_enum "order" 3;val_level|])
-
-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|]
-
-let val_prec f =
-  val_tuple "prec"[|val_array val_name; val_array f; val_array f|]
-let val_fix f =
-  val_tuple"fix1"[|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"cofix"[|val_int;val_prec f|]
-
-
-let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
-  [|val_int|]; (* Rel *)
-  [|val_id|]; (* Var *)
-  [|val_int|]; (* Meta *)
-  [|val_evar val_constr|]; (* Evar *)
-  [|val_sort|]; (* Sort *)
-  [|val_constr;val_cast;val_constr|]; (* Cast *)
-  [|val_name;val_constr;val_constr|]; (* Prod *)
-  [|val_name;val_constr;val_constr|]; (* Lambda *)
-  [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
-  [|val_constr;val_array val_constr|]; (* App *)
-  [|val_kn|]; (* Const *)
-  [|val_ind|]; (* Ind *)
-  [|val_cstr|]; (* Construct *)
-  [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
-  [|val_fix val_constr|]; (* Fix *)
-  [|val_cofix val_constr|] (* CoFix *)
-|])
-
-
-let val_ndecl = val_tuple"ndecl"[|val_id;val_opt val_constr;val_constr|]
-let val_rdecl = val_tuple"rdecl"[|val_name;val_opt val_constr;val_constr|]
-let val_nctxt = val_list val_ndecl
-let val_rctxt = val_list val_rdecl
-
-let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
-
-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 =
-  val_sum "cst_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
-
-let val_subst_dom =
-  val_sum "subst_dom" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
-
-
-let val_res = val_opt no_val
-
-let val_subst =
-  val_map val_subst_dom (val_tuple "subst range" [|val_mp;val_res|])
-
-let val_cstr_subst =
-  val_ref (val_sum "cstr_subst" 0 [|[|val_constr|];[|val_subst;val_constr|]|])
-
-let val_cb = val_tuple "cb"
-  [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
-    val_bool; val_bool |]
-
-let val_recarg = val_sum "recarg" 1 [|[|val_int|];[|val_ind|]|]
-
-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
-  [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
-
-let val_one_ind = val_tuple "one_ind"
-  [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
-    val_int; val_list val_sortfam;val_array val_constr;val_array val_int;
-    val_wfp; val_int; val_int; no_val|]
-
-let val_ind_pack = val_tuple "ind_pack"
-  [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
-    val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
-
-let rec val_sfb o = val_sum "sfb" 0
-  [|[|val_cb|];[|val_ind_pack|];[|val_mod|];
-    [|val_mp;val_opt val_cstrs|];[|val_modty|]|] o
-and val_sb o = val_list (val_tuple"sb"[|val_id;val_sfb|]) o
-and val_seb o = val_sum "seb" 0
-  [|[|val_mp|];[|val_uid;val_modty;val_seb|];[|val_uid;val_sb|];
-    [|val_seb;val_seb;val_cstrs|];[|val_seb;val_with|]|] o
-and val_with o = val_sum "with" 0
-  [|[|val_list val_id;val_mp;val_cstrs|];
-    [|val_list val_id;val_cb|]|] o
-and val_mod o = val_tuple "module_body"
-  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
-and val_modty o = val_tuple "module_type_body"
-  [|val_seb;val_opt val_mp;val_subst|] o
-
-let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-
-let val_vo = val_tuple "vo" [|val_dp;val_mod;val_deps;val_eng|]
+  val_set ~name:"Univ.constraints"
+   (val_tuple "univ_constraint"
+     [|val_level;val_enum "order_request" 3;val_level|])