Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg

14 files changed, 407 insertions, 160 deletions

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 96366594..6ea153a3 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -55,7 +55,7 @@ let print_context env =
        env_stratification=
         {env_universes=univ; env_engagement=engt}} = env in
     msgnl(hov 0
-      (str"CONTEXT SUMMARY" ++ fnl() ++
+      (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
       str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
@@ -65,5 +65,3 @@ let print_context env =
 let stats () =
   print_context (Safe_typing.get_env());
   print_memory_stat ()
-
-let _ = at_exit stats
diff --git a/checker/checker.ml b/checker/checker.ml
index 3d928933..70e2eb97 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -256,7 +256,7 @@ let rec explain_exn = function
   | Not_found -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
   | Failure s -> 
-      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report ())
+      hov 0 (str "Failure: " ++ str s ++ report ())
   | Invalid_argument s -> 
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
   | Sys.Break -> 
@@ -385,4 +385,4 @@ let run () =
     flush_all(); 
     exit 1)
 
-let start () = init(); run(); exit 0
+let start () = init(); run(); Check_stat.stats(); exit 0
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2cf3854a..c6a7b4b4 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,6 +1,7 @@
 open Util
 open Names
 open Term
+open Validate
 
 (* Bytecode *)
 type values
@@ -11,17 +12,22 @@ type action
 type retroknowledge
 
 type engagement = ImpredicativeSet
+let val_eng = val_enum "eng" 1
 
 
 type polymorphic_arity = {
   poly_param_levels : Univ.universe option list;
   poly_level : Univ.universe;
 }
+let val_pol_arity =
+  val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
 
 type constant_type =
   | NonPolymorphicType of constr
   | PolymorphicArity of rel_context * polymorphic_arity
 
+let val_cst_type =
+  val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
 
 
 type substitution_domain = 
@@ -29,6 +35,9 @@ type substitution_domain =
   | MBI of mod_bound_id
   | MPI of module_path
 
+let val_subst_dom =
+  val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+
 module Umap = Map.Make(struct 
 			 type t = substitution_domain
 			 let compare = Pervasives.compare
@@ -39,6 +48,13 @@ type resolver
 type substitution = (module_path * resolver option) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
+let val_res = val_opt no_val
+
+let val_subst =
+  val_map ~name:"substitution"
+    val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+
+
 let fold_subst fs fb fp =
   Umap.fold
     (fun k (mp,_) acc ->
@@ -360,6 +376,11 @@ let force_constr = force subst_mps
 
 type constr_substituted = constr substituted
 
+let val_cstr_subst =
+  val_ref
+    (val_sum "constr_substituted" 0
+      [|[|val_constr|];[|val_subst;val_constr|]|])
+
 let subst_constr_subst = subst_substituted
 
 type constant_body = {
@@ -372,6 +393,11 @@ type constant_body = {
     const_opaque : bool; 
     const_inline : bool}
 
+let val_cb = val_tuple "constant_body"
+  [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
+    val_bool; val_bool |]
+
+
 let subst_rel_declaration sub (id,copt,t as x) =
   let copt' = Option.smartmap (subst_mps sub) copt in
   let t' = subst_mps sub t in
@@ -383,6 +409,8 @@ type recarg =
   | Norec 
   | Mrec of int 
   | Imbr of inductive
+let val_recarg = val_sum "recarg" 1 (* Norec *)
+  [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
 
 let subst_recarg sub r = match r with
   | Norec | Mrec _  -> r
@@ -390,6 +418,12 @@ let subst_recarg sub r = match r with
       if kn==kn' then r else Imbr (kn',i)
 
 type wf_paths = recarg Rtree.t
+let val_wfp = val_rec_sum "wf_paths" 0
+  (fun val_wfp -> 
+    [|[|val_int;val_int|]; (* Rtree.Param *)
+      [|val_recarg;val_array val_wfp|]; (* Rtree.Node *)
+      [|val_int;val_array val_wfp|] (* Rtree.Rec *)
+    |])
 
 let mk_norec = Rtree.mk_node Norec [||]
 
@@ -417,10 +451,14 @@ type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
 }
+let val_mono_ind_arity =
+  val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
 
 type inductive_arity = 
 | Monomorphic of monomorphic_inductive_arity
 | Polymorphic of polymorphic_arity
+let val_ind_arity = val_sum "inductive_arity" 0
+  [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
 
 type one_inductive_body = {
 
@@ -471,6 +509,12 @@ type one_inductive_body = {
     mind_reloc_tbl :  reloc_table; 
   }
 
+let val_one_ind = val_tuple "one_inductive_body"
+  [|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|]
+
+
 type mutual_inductive_body = {
 
   (* The component of the mutual inductive block *)
@@ -503,6 +547,10 @@ type mutual_inductive_body = {
   (* Source of the inductive block when aliased in a module *)
     mind_equiv : kernel_name option
   }
+let val_ind_pack = val_tuple "mutual_inductive_body"
+  [|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 subst_arity sub = function
 | NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
@@ -558,6 +606,8 @@ let subst_mind sub mib =
 
 (* Modules *)
 
+(* Whenever you change these types, please do update the validation
+   functions below *)
 type structure_field_body = 
   | SFBconst of constant_body
   | SFBmind of mutual_inductive_body
@@ -592,6 +642,30 @@ and module_type_body =
       typ_strength : module_path option;
       typ_alias : substitution}
 
+(* the validation functions: *)
+let rec val_sfb o = val_sum "struct_field_body" 0
+  [|[|val_cb|];       (* SFBconst *)
+    [|val_ind_pack|]; (* SFBmind *)
+    [|val_module|];   (* SFBmodule *)
+    [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
+    [|val_modtype|]   (* SFBmodtype *)
+  |] o
+and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
+and val_seb o = val_sum "struct_expr_body" 0
+  [|[|val_mp|];                      (* SEBident *)
+    [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
+    [|val_uid;val_sb|];              (* SEBstruct *)
+    [|val_seb;val_seb;val_cstrs|];   (* SEBapply *)
+    [|val_seb;val_with|]             (* SEBwith *)
+  |] o
+and val_with o = val_sum "with_declaration_body" 0
+  [|[|val_list val_id;val_mp;val_cstrs|];
+    [|val_list val_id;val_cb|]|] o
+and val_module o = val_tuple "module_body"
+  [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+and val_modtype o = val_tuple "module_type_body"
+  [|val_seb;val_opt val_mp;val_subst|] o
+
 	
 let rec subst_with_body sub = function
   | With_module_body(id,mp,typ_opt,cst) ->
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 78bf2053..d71e625f 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -212,3 +212,8 @@ val join_alias : substitution -> substitution -> substitution
 val update_subst_alias : substitution -> substitution -> substitution
 val update_subst : substitution -> substitution -> substitution
 val subst_key : substitution -> substitution -> substitution
+
+(* Validation *)
+val val_eng : Obj.t -> unit
+val val_module : Obj.t -> unit
+val val_modtype : Obj.t -> unit
diff --git a/checker/environ.ml b/checker/environ.ml
index 58f08bdd..4bdbeee6 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -201,6 +201,3 @@ let lookup_module mp env =
 
 let lookup_modtype ln env = 
   MPmap.find ln env.env_globals.env_modtypes
-
-let lookup_alias mp env =
-  MPmap.find mp env.env_globals.env_alias
diff --git a/checker/environ.mli b/checker/environ.mli
index a3f531dd..1541bf0d 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -1,6 +1,8 @@
 open Names
 open Term
 
+(* Environments *)
+
 type globals = {
   env_constants : Declarations.constant_body Cmap.t;
   env_inductives : Declarations.mutual_inductive_body KNmap.t;
@@ -20,26 +22,33 @@ type env = {
   env_imports : Digest.t MPmap.t;
 }
 val empty_env : env
+
+(* Engagement *)
 val engagement : env -> Declarations.engagement option
-val universes : env -> Univ.universes
-val named_context : env -> named_context
-val rel_context : env -> rel_context
 val set_engagement : Declarations.engagement -> env -> env
 
+(* Digests *)
 val add_digest : env -> dir_path -> Digest.t -> env
 val lookup_digest : env -> dir_path -> Digest.t
 
+(* de Bruijn variables *)
+val rel_context : env -> rel_context
 val lookup_rel : int -> env -> rel_declaration
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
 val push_rec_types : name array * constr array * 'a -> env -> env
 
+(* Named variables *)
+val named_context : env -> named_context
 val push_named : named_declaration -> env -> env
 val lookup_named : identifier -> env -> named_declaration
 val named_type : identifier -> env -> constr
 
+(* Universes *)
+val universes : env -> Univ.universes
 val add_constraints : Univ.constraints -> env -> env
 
+(* Constants *)
 val lookup_constant : constant -> env -> Declarations.constant_body
 val add_constant : constant -> Declarations.constant_body -> env -> env
 val constant_type : env -> constant -> Declarations.constant_type
@@ -49,6 +58,7 @@ val constant_value : env -> constant -> constr
 val constant_opt_value : env -> constant -> constr option
 val evaluable_constant : constant -> env -> bool
 
+(* Inductives *)
 val lookup_mind :
   mutual_inductive -> env -> Declarations.mutual_inductive_body
 val scrape_mind : env -> mutual_inductive -> mutual_inductive
@@ -56,6 +66,7 @@ val add_mind :
   mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
 val mind_equiv : env -> inductive -> inductive -> bool
 
+(* Modules *)
 val add_modtype :
   module_path -> Declarations.module_type_body -> env -> env
 val shallow_add_module :
@@ -64,4 +75,3 @@ val register_alias : module_path -> module_path -> env -> env
 val scrape_alias : module_path -> env -> module_path
 val lookup_module : module_path -> env -> Declarations.module_body
 val lookup_modtype : module_path -> env -> Declarations.module_type_body
-val lookup_alias : module_path -> env -> module_path
diff --git a/checker/include b/checker/include
new file mode 100644
index 00000000..331eb45c
--- /dev/null
+++ b/checker/include
@@ -0,0 +1,176 @@
+(* -*-tuareg-*- *)
+
+(* Caml script to include for debugging the checker.
+   Usage: from the checker/ directory launch ocaml toplevel and then
+   type #use"include";;
+   This command loads the relevent modules, defines some pretty
+   printers, and provides functions to interactively check modules
+   (mainly run_l and norec).
+ *)
+
+#cd ".."
+#directory "lib";;
+#directory "kernel";;
+#directory "checker";;
+
+#load "unix.cma";;
+#load "str.cma";;
+#load "gramlib.cma";;
+#load "check.cma";;
+
+open Typeops;;
+open Check;;
+
+
+open Pp;;
+open Util;;
+open Names;;
+open Term;;
+open Environ;;
+open Declarations;;
+open Mod_checking;;
+
+let pr_id id = str(string_of_id id)
+let pr_na = function Name id -> pr_id id | _ -> str"_";;
+let prdp dp = pp(str(string_of_dirpath dp));;
+(*
+let prc c = pp(Himsg.pr_lconstr_env (Check.get_env()) c);;
+let prcs cs = prc (Declarations.force cs);;
+let pru u = pp(str(Univ.string_of_universe u));;*)
+let pru u = pp(Univ.pr_uni u);;
+let prlab l = pp(str(string_of_label l));;
+let prid id = pp(pr_id id);;
+let prcon c = pp(Indtypes.prcon c);;
+let prkn kn = pp(Indtypes.prkn kn);;
+
+
+let prus g = pp(Univ.pr_universes g);;
+
+let prcstrs c =
+  let g = Univ.merge_constraints c Univ.initial_universes in
+  pp(Univ.pr_universes g);;
+(*let prcstrs c = pp(Univ.pr_constraints c);; *)
+(*
+let prenvu e =
+  let u = universes e in
+  let pu =
+  str "UNIVERSES:"++fnl()++str"  "++hov 0 (Univ.pr_universes u) ++fnl() in
+  pp pu;;
+
+let prenv e =
+  let ctx1 = named_context e in
+  let ctx2 = rel_context e in
+  let pe =
+    hov 1 (str"[" ++
+           prlist_with_sep spc (fun (na,_,_) -> pr_id na) (List.rev ctx1)++
+           str"]") ++ spc() ++
+    hov 1 (str"[" ++
+           prlist_with_sep spc (fun (na,_,_) -> pr_na na) (List.rev ctx2)++
+           str"]") in
+  pp pe;;
+*)
+
+let prsub s =
+  let string_of_mp mp =
+    let s = string_of_mp mp in
+    (match mp with MPself _ -> "#self."|MPbound _ -> "#bound."|_->"")^s in 
+  pp (hv 0 
+  (fold_subst
+    (fun msid mp strm ->
+      str "S " ++ str (debug_string_of_msid msid) ++ str " |-> " ++
+      str (string_of_mp mp) ++ fnl() ++ strm)
+    (fun mbid mp strm ->
+      str"B " ++ str (debug_string_of_mbid mbid) ++ str " |-> " ++
+      str (string_of_mp mp) ++ fnl() ++ strm)
+    (fun mp1 mp strm ->
+      str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
+      str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
+;;
+
+#install_printer prid;;
+#install_printer prcon;;
+#install_printer prlab;;
+#install_printer prdp;;
+#install_printer prkn;;
+#install_printer pru;;
+(*
+#install_printer prc;;
+#install_printer prcs;;
+*)
+#install_printer prcstrs;;
+(*#install_printer prus;;*)
+(*#install_printer prenv;;*)
+(*#install_printer prenvu;;*)
+#install_printer prsub;;
+
+Checker.init();;
+Flags.make_silent false;;
+Flags.debug := true;;
+Sys.catch_break true;;
+
+let module_of_file f =
+  let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
+  (mb:module_body)
+;;
+let mod_access m fld =
+  match m.mod_expr with
+      Some(SEBstruct(msid,l)) -> List.assoc fld l
+    | _ -> failwith "bad structure type"
+;;
+
+let parse_dp s =
+  make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s)))
+;;
+let parse_sp s =
+  let l = List.rev (Str.split(Str.regexp"\\.") s) in
+  {dirpath=List.tl l; basename=List.hd l};;
+let parse_kn s =
+   let l = List.rev (Str.split(Str.regexp"\\.") s) in
+   let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+   make_kn(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let parse_con s =
+   let l = List.rev (Str.split(Str.regexp"\\.") s) in
+   let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+   make_con(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let get_mod dp = 
+  lookup_module dp (Safe_typing.get_env())
+;;
+let get_mod_type dp = 
+  lookup_modtype dp (Safe_typing.get_env())
+;;
+let get_cst kn = 
+  lookup_constant kn (Safe_typing.get_env())
+;;
+
+let read_mod s f = 
+  let lib = intern_from_file (parse_dp s,f) in
+  ((Obj.magic lib.library_compiled):
+    dir_path *
+    module_body *
+    (dir_path * Digest.t) list *
+    engagement option);;
+
+let deref_mod md s =
+  let (Some (SEBstruct(msid,l))) = md.mod_expr in
+  List.assoc (label_of_id(id_of_string s)) l
+;;
+
+let expln f x =
+  try f x
+  with UserError(_,strm) as e ->
+    msgnl strm; raise e
+
+let admit_l l =
+  let l = List.map parse_sp l in
+  Check.recheck_library ~admit:l ~check:l;;
+let run_l l =
+  Check.recheck_library ~admit:[] ~check:(List.map parse_sp l);;
+let norec q =
+  Check.recheck_library ~norec:[parse_sp q] ~admit:[] ~check:[];;
+
+(*
+admit_l["Bool";"OrderedType";"DecidableType"];;
+run_l["FSetInterface"];;
+*)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index af5e4f46..9e7a2336 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -130,6 +130,12 @@ let check_definition_sub env cb1 cb2 =
 	Reduction.conv env c1 c2
     | _ -> ())
 
+let lookup_modtype mp env =
+  try Environ.lookup_modtype mp env
+  with Not_found ->
+    failwith ("Unknown module type: "^string_of_mp mp)
+
+
 let rec check_with env mtb with_decl = 
   match with_decl with
     | With_definition_body _ -> 
@@ -308,7 +314,8 @@ and check_structure_field (s,env) mp lab = function
 
 and check_modexpr env mse = match mse with
   | SEBident mp ->
-      let mtb = lookup_modtype mp env in 
+      let mp = scrape_alias mp env in
+      let mtb = lookup_modtype mp env in
       mtb.typ_alias
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
diff --git a/checker/modops.ml b/checker/modops.ml
index 27ea4d55..498bd775 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -125,6 +125,7 @@ let strengthen_mind env mp l mib = match mib.mind_equiv with
 let rec eval_struct env = function 
   | SEBident mp -> 
       begin
+        let mp = scrape_alias mp env in
 	let mtb =lookup_modtype mp env in
 	match mtb.typ_expr,mtb.typ_strength with
 	    mtb,None -> eval_struct env mtb
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index d5779923..9e886837 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -106,6 +106,10 @@ type compiled_library =
     (dir_path * Digest.t) list *
     engagement option
  
+open Validate
+let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
+let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_eng|]
+
 (* This function should append a certificate to the .vo file.
    The digest must be part of the certicate to rule out attackers
    that could change the .vo file between the time it was read and
@@ -116,7 +120,7 @@ let stamp_library file digest = ()
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
 let import file (dp,mb,depends,engmt as vo) digest = 
-  Validate.val_vo (Obj.repr vo);
+  Validate.apply !Flags.debug val_vo vo;
   Flags.if_verbose msgnl (str "*** vo structure validated ***");
   let env = !genv in
   check_imports msg_warning dp env depends;
diff --git a/checker/term.ml b/checker/term.ml
index 45568a59..f245d155 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -15,6 +15,7 @@ open Pp
 open Names
 open Univ
 open Esubst
+open Validate
 
 (* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
@@ -35,6 +36,10 @@ type case_info =
     ci_cstr_nargs : int array; (* number of real args of each constructor *)
     ci_pp_info    : case_printing (* not interpreted by the kernel *)
   }
+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|]
 
 (* Sorts. *)
 
@@ -51,6 +56,9 @@ let family_of_sort = function
   | Prop Pos -> InSet
   | Type _ -> InType
 
+let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
+let val_sortfam = val_enum "sorts_family" 3
+
 (********************************************************************)
 (*       Constructions as implemented                               *)
 (********************************************************************)
@@ -65,7 +73,16 @@ type 'constr pfixpoint =
 type 'constr pcofixpoint =
     int * 'constr prec_declaration
 
+let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_prec f =
+  val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+let val_fix f =
+  val_tuple"pfixpoint"
+    [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+
 type cast_kind = VMcast | DEFAULTcast 
+let val_cast = val_enum "cast_kind" 2
 
 (*s*******************************************************************)
 (* The type of constructions *)
@@ -88,11 +105,31 @@ type constr =
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
 
+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 *)
+|])
+
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
 type fixpoint = constr pfixpoint
 type cofixpoint = constr pcofixpoint
 
+
 let rec strip_outer_cast c = match c with
   | Cast (c,_,_) -> strip_outer_cast c
   | _ -> c
@@ -275,6 +312,13 @@ let subst1 lam = substl [lam]
 (*     Type of assumptions and contexts                                    *)
 (***************************************************************************)
 
+let val_ndecl =
+  val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+let val_rdecl =
+  val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+let val_nctxt = val_list val_ndecl
+let val_rctxt = val_list val_rdecl
+
 type named_declaration = identifier * constr option * constr
 type rel_declaration = name * constr option * constr
 
@@ -395,6 +439,7 @@ let decompose_prod_n_assum n =
 (***************************)
 
 type arity = rel_context * sorts
+let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
 
 let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
 
diff --git a/checker/term.mli b/checker/term.mli
index 30a2c03a..1367e581 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -109,3 +109,10 @@ val destArity : constr -> arity
 val isArity : constr -> bool
 val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
 val eq_constr : constr -> constr -> bool
+
+(* Validation *)
+val val_sortfam : Obj.t -> unit
+val val_sort : Obj.t -> unit
+val val_constr : Obj.t -> unit
+val val_rctxt : Obj.t -> unit
+val val_nctxt : Obj.t -> unit
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 1af8b2ce..1832ebec 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -140,7 +140,10 @@ let type_of_constant env cst =
 
 let judge_of_constant_knowing_parameters env cst paramstyp =
   let c = Const cst in
-  let cb = lookup_constant cst env in
+  let cb =
+    try lookup_constant cst env 
+    with Not_found ->
+      failwith ("Cannot find constant: "^string_of_con cst) in
   let _ = check_args env c cb.const_hyps in 
   type_of_constant_knowing_parameters env cb.const_type paramstyp
 
@@ -222,7 +225,10 @@ let judge_of_cast env (c,cj) k tj =
 
 let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
   let c = Ind ind in
-  let (mib,mip) = lookup_mind_specif env ind in
+  let (mib,mip) =
+    try lookup_mind_specif env ind
+    with Not_found ->
+      failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in
   check_args env c mib.mind_hyps;
   type_of_inductive_knowing_parameters env mip paramstyp
 
@@ -235,7 +241,10 @@ let judge_of_constructor env c =
   let constr = Construct c in
   let _ =
     let ((kn,_),_) = c in
-    let mib = lookup_mind kn env in
+    let mib = 
+      try lookup_mind kn env
+      with Not_found ->
+        failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in
     check_args env constr mib.mind_hyps in 
   let specif = lookup_mind_specif env (inductive_of_constructor c) in
   type_of_constructor c specif
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|])