Imported Upstream version 8.2~beta4.svn20080907+dfsgupstream/8.2.beta4.svn20080907+dfsg

6 files changed, 110 insertions, 73 deletions

diff --git a/checker/check.ml b/checker/check.ml
index e91516c7..40ac604e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -23,8 +23,7 @@ type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath
-    (id_of_string p.basename :: List.map id_of_string p.dirpath)
+  make_dirpath (List.map id_of_string p.dirpath)
 let path_of_dirpath dir = 
   match repr_dirpath dir with
       [] -> failwith "path_of_dirpath"
@@ -166,6 +165,9 @@ let remove_load_path dir =
   load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
 let add_load_path (phys_path,coq_path) =
+  if !Flags.debug then
+    msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+           str phys_path);
   let phys_path = canonical_path_name phys_path in
     match list_filter2 (fun p d -> p = phys_path) !load_paths with
       | _,[dir] ->
@@ -224,7 +226,7 @@ let locate_qualified_library qid =
       (* Search library in loadpath *)
       if qid.dirpath=[] then get_load_paths ()
       else
-        (* we assume dir is an absolute dirpath *)
+        (* we assume qid is an absolute dirpath *)
         load_paths_of_dir_path (dir_of_path qid)
     in
     if loadpath = [] then raise LibUnmappedDir;
diff --git a/checker/checker.ml b/checker/checker.ml
index 7de25835..1ed094cf 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -191,6 +191,11 @@ let print_usage_channel co command =
 
   -where                 print Coq's standard library location and exit
   -v                     print Coq version and exit
+  -boot                  boot mode
+  -o                     print the list of assumptions
+  -m                     print the maximum heap size
+ 
+  -impredicative-set     set sort Set impredicative
 
   -h, --help             print this list of options
 "
@@ -323,10 +328,9 @@ let parse_args() =
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
     | ("-v"|"--version") :: _ -> version ()
-
+    | "-boot" :: rem -> boot := true; parse rem	
     | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
-
-    | ("-o" | "-output-context") :: rem ->
+    | ("-o" | "--output-context") :: rem ->
         Check_stat.output_context := true; parse rem
 
     | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 8c84fb0f..4c9b3d61 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -19,6 +19,21 @@ open Pp
 open Declarations
 open Environ
 
+let rec debug_string_of_mp = function
+  | MPfile sl -> string_of_dirpath sl
+  | MPbound uid -> "bound("^string_of_mbid uid^")"
+  | MPself uid -> "self("^string_of_msid uid^")"
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+let rec string_of_mp = function
+  | MPfile sl -> string_of_dirpath sl
+  | MPbound uid -> string_of_mbid uid
+  | MPself uid -> string_of_msid uid
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+
+let string_of_mp mp =
+  if !Flags.debug then debug_string_of_mp mp else string_of_mp mp
+
 let prkn kn =
   let (mp,_,l) = repr_kn kn in
   str(string_of_mp mp ^ "." ^ string_of_label l)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ecf8d633..379273af 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -26,7 +26,7 @@ let refresh_arity ar =
 
 let check_constant_declaration env kn cb =
   Flags.if_verbose msgnl (str "  checking cst: " ++ prcon kn);
-  let env = add_constraints cb.const_constraints env in
+(*  let env = add_constraints cb.const_constraints env in*)
   let env' = check_named_ctxt env cb.const_hyps in
   (match cb.const_type with
       NonPolymorphicType ty ->
@@ -47,58 +47,6 @@ let check_constant_declaration env kn cb =
 (* Checking modules *)
 
 
-let rec add_struct_expr_constraints env = function
-  | SEBident _ -> env
-
-  | SEBfunctor (_,mtb,meb) -> 
-      add_struct_expr_constraints 
-	(add_modtype_constraints env mtb) meb
-
-  | SEBstruct (_,structure_body) ->
-      List.fold_left 
-        (fun env (l,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-(*  let g = Univ.merge_constraints cst Univ.initial_universes in
-msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
-      Univ.pr_universes g++str"============="++fnl());      
-*)
-      Environ.add_constraints cst 
-        (add_struct_expr_constraints 
-	  (add_struct_expr_constraints env meb1) 
-	  meb2)
-  | SEBwith(meb,With_definition_body(_,cb))->
-      Environ.add_constraints cb.const_constraints
-	(add_struct_expr_constraints env meb)
-  | SEBwith(meb,With_module_body(_,_,cst))->
-      Environ.add_constraints cst
-	(add_struct_expr_constraints env meb)	
-		
-and add_struct_elem_constraints env = function 
-  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
-  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SFBmodule mb -> add_module_constraints env mb
-  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
-  | SFBalias (mp,None) -> env
-  | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb = 
-  let env = match mb.mod_expr with
-    | None -> env
-    | Some meb -> add_struct_expr_constraints env meb
-  in
-  let env = match mb.mod_type with
-    | None -> env
-    | Some mtb -> 
-	add_struct_expr_constraints env mtb
-  in
-    Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb = 
-  add_struct_expr_constraints env mtb.typ_expr
-
 exception Not_path
 
 let path_of_mexpr = function
@@ -307,19 +255,18 @@ and check_module_type env mty =
   check_alias mty.typ_alias sub
 
 and check_module env mb =
-  let env' = add_module_constraints env mb in
   let sub =
     match mb.mod_expr, mb.mod_type with
       | None, None -> 
 	  anomaly "Mod_typing.translate_module: empty type and expr in module entry"
-      | None, Some mtb -> check_modexpr env' mtb
+      | None, Some mtb -> check_modexpr env mtb
 
       | Some mexpr, _ -> 
-	  let sub1 = check_modexpr env' mexpr in
+	  let sub1 = check_modexpr env mexpr in
 	  (match mb.mod_type with
 	    | None ->  sub1
 	    | Some mte -> 
-		let sub2 = check_modexpr env' mte in
+		let sub2 = check_modexpr env mte in
                 check_subtypes env
 		  {typ_expr = mexpr;
 		   typ_strength = None;
@@ -342,21 +289,22 @@ and check_structure_field (s,env) mp lab = function
       let mp1 = MPdot(mp,lab) in
       let is_fun, sub = Modops.update_subst env msb mp1 in
       ((if is_fun then s else join s sub),
-       Modops.add_module (MPdot(mp,lab)) msb
-         (add_module_constraints env msb))
+       Modops.add_module (MPdot(mp,lab)) msb env)
   | SFBalias(mp2,cst) ->
+      (* cf Safe_typing.add_alias *)
       (try
+        let mp' = MPdot(mp,lab) in
         let mp2' = scrape_alias mp2 env in
-        let msb = lookup_module mp2' env in
-        (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias),
-         Option.fold_right add_constraints cst
-           (register_alias (MPdot(mp,lab)) mp2 env))
+        let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
+        let sub = update_subst sub (map_mp mp' mp2') in
+        let sub = join_alias sub (map_mp mp' mp2') in
+        let sub = add_mp mp' mp2' sub in
+        (join s sub, register_alias mp' mp2 env)
       with Not_found -> failwith "unkown aliased module")
   | SFBmodtype mty ->
       let kn = MPdot(mp, lab) in
       check_module_type env mty;
-      (join s mty.typ_alias,
-       add_modtype kn mty (add_modtype_constraints env mty))
+      (join s mty.typ_alias, add_modtype kn mty env)
 
 and check_modexpr env mse = match mse with
   | SEBident mp ->
@@ -396,3 +344,57 @@ and check_modexpr env mse = match mse with
         List.fold_left (fun env (lab,mb) ->
           check_structure_field env mp lab mb) (empty_subst,env) msb in
       sub
+
+(*
+let rec add_struct_expr_constraints env = function
+  | SEBident _ -> env
+
+  | SEBfunctor (_,mtb,meb) -> 
+      add_struct_expr_constraints 
+	(add_modtype_constraints env mtb) meb
+
+  | SEBstruct (_,structure_body) ->
+      List.fold_left 
+        (fun env (l,item) -> add_struct_elem_constraints env item)
+        env
+        structure_body
+
+  | SEBapply (meb1,meb2,cst) ->
+(*  let g = Univ.merge_constraints cst Univ.initial_universes in
+msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
+      Univ.pr_universes g++str"============="++fnl());      
+*)
+      Environ.add_constraints cst 
+        (add_struct_expr_constraints 
+	  (add_struct_expr_constraints env meb1) 
+	  meb2)
+  | SEBwith(meb,With_definition_body(_,cb))->
+      Environ.add_constraints cb.const_constraints
+	(add_struct_expr_constraints env meb)
+  | SEBwith(meb,With_module_body(_,_,cst))->
+      Environ.add_constraints cst
+	(add_struct_expr_constraints env meb)	
+		
+and add_struct_elem_constraints env = function 
+  | SFBconst cb -> Environ.add_constraints cb.const_constraints env
+  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
+  | SFBmodule mb -> add_module_constraints env mb
+  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
+  | SFBalias (mp,None) -> env
+  | SFBmodtype mtb -> add_modtype_constraints env mtb
+
+and add_module_constraints env mb = 
+  let env = match mb.mod_expr with
+    | None -> env
+    | Some meb -> add_struct_expr_constraints env meb
+  in
+  let env = match mb.mod_type with
+    | None -> env
+    | Some mtb -> 
+	add_struct_expr_constraints env mtb
+  in
+    Environ.add_constraints mb.mod_constraints env
+
+and add_modtype_constraints env mtb = 
+  add_struct_expr_constraints env mtb.typ_expr
+*)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 49f05daf..c398f0a4 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -195,6 +195,12 @@ let in_whnf (t,stk) =
     | (FFlex _ | FProd _ | FEvar _ | FInd _ | FAtom _ | FRel _) -> true
     | FLOCKED -> assert false
 
+let oracle_order fl1 fl2 =
+  match fl1,fl2 with
+      ConstKey c1, ConstKey c2 -> (*height c1 > height c2*)false
+    | _, ConstKey _ -> true
+    | _ -> false
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = 
   eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -247,6 +253,14 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
         with NotConvertible ->
           (* else the oracle tells which constant is to be expanded *)
           let (app1,app2) =
+            if oracle_order fl1 fl2 then
+              match unfold_reference infos fl1 with
+                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+                | None ->
+                    (match unfold_reference infos fl2 with
+                      | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+                     | None -> raise NotConvertible)
+            else
 	      match unfold_reference infos fl2 with
                 | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
                 | None ->
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 4b156e7e..d5779923 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -31,7 +31,7 @@ let set_engagement c =
 let full_add_module dp mb digest =
   let env = !genv in
   let mp = MPfile dp in
-  let env = add_module_constraints env mb in
+  let env = add_constraints mb.mod_constraints env in
   let env = Modops.add_module mp mb env in
   genv := add_digest env dp digest
 
@@ -121,7 +121,7 @@ let import file (dp,mb,depends,engmt as vo) digest =
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
-  check_module env mb;
+  check_module (add_constraints mb.mod_constraints env) mb;
   stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)