[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

7 files changed, 69 insertions, 53 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 712566a00..e15c37e67 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -295,7 +295,7 @@ let rec explain_exn = function
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise)++report())
 
-let parse_args() =
+let parse_args argv =
   let rec parse = function
     | [] -> ()
    | "-impredicative-set" :: rem ->
@@ -340,7 +340,7 @@ let parse_args() =
     | s :: rem ->  add_compile s; parse rem
   in
   try
-    parse (List.tl (Array.to_list Sys.argv))
+    parse (List.tl (Array.to_list argv))
   with
     | UserError(_,s) as e -> begin
 	try
@@ -354,12 +354,12 @@ let parse_args() =
 (* To prevent from doing the initialization twice *)
 let initialized = ref false
 
-let init() =
+let init_with_argv argv =
   if not !initialized then begin
     initialized := true;
     Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
     try
-      parse_args();
+      parse_args argv;
       if_verbose print_header ();
       init_load_path ();
       engage ();
@@ -370,6 +370,8 @@ let init() =
       exit 1
   end
 
+let init() = init_with_argv Sys.argv
+
 let run () =
   try
     compile_files ();
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 3211cc28f..95d1f2bd1 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -482,19 +482,16 @@ let subst_mps sub =
 
 type 'a lazy_subst =
   | LSval of 'a
-  | LSlazy of substitution * 'a
+  | LSlazy of substitution list * 'a
 
 type 'a substituted = 'a lazy_subst ref
 
-let from_val a = ref (LSval a)
+let val_substituted val_a =
+  val_ref
+    (val_sum "constr_substituted" 0
+      [|[|val_a|];[|val_list val_subst;val_a|]|])
 
-let force fsubst r =
-  match !r with
-  | LSval a -> a
-  | LSlazy(s,a) ->
-      let a' = fsubst s a in
-      r := LSval a';
-      a'
+let from_val a = ref (LSval a)
 
 let mp_in_key mp key = 
   let rec mp_rec mp1 = 
@@ -606,21 +603,27 @@ let join (subst1 : substitution) (subst2 : substitution) =
   let subst = Umap.mapi (apply_subst subst2) subst1 in
     (Umap.fold Umap.add subst2 subst)   
 
+
+let force fsubst r =
+  match !r with
+  | LSval a -> a
+  | LSlazy(s,a) ->
+      let subst = List.fold_left join empty_subst (List.rev s) in
+      let a' = fsubst subst a in
+      r := LSval a';
+      a'
+
 let subst_substituted s r =
   match !r with
-    | LSval a -> ref (LSlazy(s,a))
+    | LSval a -> ref (LSlazy([s],a))
     | LSlazy(s',a) ->
-	let s'' = join s' s in
-	  ref (LSlazy(s'',a))
+	  ref (LSlazy(s::s',a))
 
 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 val_cstr_subst = val_substituted val_constr
 
 let subst_constr_subst = subst_substituted
 
@@ -635,8 +638,13 @@ type constant_body = {
     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 |]
+  [|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) =
@@ -791,7 +799,7 @@ type mutual_inductive_body = {
   }
 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|]
+    val_int; val_int; val_rctxt;val_cstrs|]
 
 
 let subst_arity sub = function
@@ -821,7 +829,7 @@ let subst_mind_packet sub mbp =
   { mind_consnames = mbp.mind_consnames;
     mind_consnrealdecls = mbp.mind_consnrealdecls;
     mind_typename = mbp.mind_typename;
-    mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
+   mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc;
     mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt;
     mind_arity = subst_arity sub mbp.mind_arity;
     mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc;
@@ -896,16 +904,16 @@ 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_sb|];              (* SEBstruct *)
     [|val_seb;val_seb;val_cstrs|];   (* SEBapply *)
+    [|val_sb|];              (* SEBstruct *)
     [|val_seb;val_with|]             (* SEBwith *)
   |] o
 and val_with o = val_sum "with_declaration_body" 0
   [|[|val_list val_id;val_mp|];
     [|val_list val_id;val_cb|]|] o
 and val_module o = val_tuple "module_body"
-  [|val_mp;val_opt val_seb;val_opt val_seb;
-    val_seb;val_cstrs;val_res;no_val|] o
+  [|val_mp;val_opt val_seb;val_seb;
+    val_opt val_seb;val_cstrs;val_res;no_val|] o
 and val_modtype o = val_tuple "module_type_body"
   [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o
 
diff --git a/checker/include b/checker/include
index 331eb45c1..b7d46d4b3 100644
--- a/checker/include
+++ b/checker/include
@@ -8,20 +8,26 @@
    (mainly run_l and norec).
  *)
 
-#cd ".."
+#cd "..";;
 #directory "lib";;
 #directory "kernel";;
 #directory "checker";;
+#directory "+camlp4";;
+#directory "+camlp5";;
 
 #load "unix.cma";;
 #load "str.cma";;
 #load "gramlib.cma";;
+(*#load "toplevellib.cma";;
+
+#directory "/usr/lib/ocaml/compiler-libs/utils";;
+let _ = Clflags.recursive_types:=true;;
+*)
 #load "check.cma";;
 
 open Typeops;;
 open Check;;
 
-
 open Pp;;
 open Util;;
 open Names;;
@@ -70,10 +76,11 @@ let prenv e =
   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 
+    (match mp with MPbound _ -> "#bound."|_->"")^s in 
   pp (hv 0 
   (fold_subst
     (fun msid mp strm ->
@@ -86,6 +93,7 @@ let prsub s =
       str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
       str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
 ;;
+*)
 
 #install_printer prid;;
 #install_printer prcon;;
@@ -100,10 +108,10 @@ let prsub s =
 #install_printer prcstrs;;
 (*#install_printer prus;;*)
 (*#install_printer prenv;;*)
-(*#install_printer prenvu;;*)
-#install_printer prsub;;
+(*#install_printer prenvu;;
+#install_printer prsub;;*)
 
-Checker.init();;
+Checker.init_with_argv [|""|];;
 Flags.make_silent false;;
 Flags.debug := true;;
 Sys.catch_break true;;
@@ -114,7 +122,7 @@ let module_of_file f =
 ;;
 let mod_access m fld =
   match m.mod_expr with
-      Some(SEBstruct(msid,l)) -> List.assoc fld l
+      Some(SEBstruct l) -> List.assoc fld l
     | _ -> failwith "bad structure type"
 ;;
 
@@ -153,7 +161,7 @@ let read_mod s f =
     engagement option);;
 
 let deref_mod md s =
-  let (Some (SEBstruct(msid,l))) = md.mod_expr in
+  let (Some (SEBstruct l)) = md.mod_expr in
   List.assoc (label_of_id(id_of_string s)) l
 ;;
 
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index e0aa9e7c3..de57c50a7 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -22,7 +22,7 @@ open Environ
 let rec debug_string_of_mp = function
   | MPfile sl -> string_of_dirpath sl
   | MPbound uid -> "bound("^string_of_mbid uid^")"
-  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+  | MPdot (mp,l) -> debug_string_of_mp mp ^ "." ^ string_of_label l
 
 let rec string_of_mp = function
   | MPfile sl -> string_of_dirpath sl
@@ -36,8 +36,9 @@ let prkn kn =
   let (mp,_,l) = repr_kn kn in
   str(string_of_mp mp ^ "." ^ string_of_label l)
 let prcon c =
-  let (mp,_,l) = repr_con c in
-  str(string_of_mp mp ^ "." ^ string_of_label l)
+  let ck = canonical_con c in
+  let uk = user_con c in
+  if ck=uk then prkn uk else (prkn uk ++str"(="++prkn ck++str")")
 
 (* Same as noccur_between but may perform reductions.
    Could be refined more...  *)
diff --git a/checker/modops.ml b/checker/modops.ml
index 3d07135d1..de0d6c7e9 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -127,10 +127,7 @@ let strengthen_const env mp_from l cb resolver =
 	  
 
 let rec strengthen_mod env mp_from mp_to mb = 
-  assert(mp_from = mb.mod_mp);
-(*  if mp_in_delta mb.mod_mp mb.mod_delta then
-    mb 
-  else*)
+    assert(mp_from = mb.mod_mp);
     match mb.mod_type with
      | SEBstruct (sign) -> 
 	 let resolve_out,sign_out = 
@@ -180,10 +177,6 @@ and strengthen_sig env mp_from sign mp_to resolver =
 	  resolve_out,item::rest'
     
 let strengthen env mtb mp = 
-(*  if mp_in_delta mtb.typ_mp mtb.typ_delta then
-    (* in this case mtb has already been strengthened*)
-    mtb 
-  else*)
     match mtb.typ_expr with
       | SEBstruct (sign) -> 
 	  let resolve_out,sign_out =
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index da0e63c23..8f5d45732 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -131,7 +131,8 @@ let import file (dp,mb,depends,engmt as vo) digest =
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import file (dp,mb,depends,engmt) digest =
+let unsafe_import file (dp,mb,depends,engmt as vo) digest =
+(*  if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*)
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;
   check_engagement env engmt;
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|]