Imported Upstream version 8.0pl3upstream/8.0pl3

9 files changed, 77 insertions, 28 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 8943b0b5..ac2c52cc 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.ml,v 1.31.2.1 2004/07/16 19:30:24 herbelin Exp $ i*)
+(*i $Id: declarations.ml,v 1.31.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
 
 (*i*)
 open Util
@@ -104,6 +104,7 @@ type one_inductive_body = {
  }
 
 type mutual_inductive_body = {
+  mind_record : bool;
   mind_finite : bool;
   mind_ntypes : int;
   mind_hyps : section_context;
@@ -139,7 +140,8 @@ let subst_mind_packet sub mbp =
 }
 
 let subst_mind sub mib = 
-  { mind_finite = mib.mind_finite ;
+  { mind_record = mib.mind_record ; 
+    mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (assert (mib.mind_hyps=[]); []) ;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c670fe9a..6cff3936 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.mli,v 1.33.2.2 2005/01/21 16:41:49 herbelin Exp $ i*)
+(*i $Id: declarations.mli,v 1.33.2.3 2005/11/29 21:40:51 letouzey Exp $ i*)
 
 (*i*)
 open Names
@@ -77,6 +77,7 @@ type one_inductive_body = {
  }
 
 type mutual_inductive_body = {
+  mind_record : bool;
   mind_finite : bool;
   mind_ntypes : int;
   mind_hyps : section_context;
diff --git a/kernel/entries.ml b/kernel/entries.ml
index d833499e..a3d3d336 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: entries.ml,v 1.3.8.1 2004/07/16 19:30:25 herbelin Exp $ i*)
+(*i $Id: entries.ml,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*)
 
 (*i*)
 open Names
@@ -49,6 +49,7 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
+  mind_entry_record : bool;
   mind_entry_finite : bool;
   mind_entry_inds : one_inductive_entry list }
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index edade51a..e9bc420e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: entries.mli,v 1.3.8.1 2004/07/16 19:30:25 herbelin Exp $ i*)
+(*i $Id: entries.mli,v 1.3.8.2 2005/11/29 21:40:51 letouzey Exp $ i*)
 
 (*i*)
 open Names
@@ -49,6 +49,7 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
+  mind_entry_record : bool;
   mind_entry_finite : bool;
   mind_entry_inds : one_inductive_entry list }
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 88f837aa..0b1d49f5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml,v 1.59.2.1 2004/07/16 19:30:25 herbelin Exp $ *)
+(* $Id: indtypes.ml,v 1.59.2.4 2005/12/30 15:58:59 barras Exp $ *)
 
 open Util
 open Names
@@ -20,10 +20,14 @@ open Reduction
 open Typeops
 open Entries
 
-(* [check_constructors_names id s cl] checks that all the constructors names
-   appearing in [l] are not present in the set [s], and returns the new set
-   of names. The name [id] is the name of the current inductive type, used
-   when reporting the error. *)
+(* Same as noccur_between but may perform reductions.
+   Could be refined more...  *)
+let weaker_noccur_between env x nvars t =
+  if noccur_between x nvars t then Some t
+  else
+   let t' = whd_betadeltaiota env t in
+   if noccur_between x nvars t then Some t'
+   else None
 
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
@@ -46,6 +50,11 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
+(* [check_constructors_names id s cl] checks that all the constructors names
+   appearing in [l] are not present in the set [s], and returns the new set
+   of names. The name [id] is the name of the current inductive type, used
+   when reporting the error. *)
+
 let check_constructors_names id =
   let rec check idset = function
     | [] -> idset
@@ -337,9 +346,10 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
     match kind_of_term x with
       | Prod (na,b,d) ->
 	  assert (largs = []);
-          if not (noccur_between n ntypes b) then
-	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (ienv_push_var ienv (na, b, mk_norec)) d
+          (match weaker_noccur_between env n ntypes b with
+              None -> raise (IllFormedInd (LocalNonPos n));
+            | Some b ->
+	        check_pos (ienv_push_var ienv (na, b, mk_norec)) d)
       | Rel k ->
           let (ra,rarg) =
             try List.nth ra_env (k-1)
@@ -481,7 +491,7 @@ let allowed_sorts env issmall isunit = function
         then logical_sorts else impredicative_sorts
       else logical_sorts
 
-let build_inductive env env_ar finite inds recargs cst =
+let build_inductive env env_ar record finite inds recargs cst =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let ids = 
@@ -527,7 +537,8 @@ let build_inductive env env_ar finite inds recargs cst =
     } in
   let packets = array_map2 build_one_packet inds recargs in
   (* Build the mutual inductive *)
-  { mind_ntypes = ntypes;
+  { mind_record = record;
+    mind_ntypes = ntypes;
     mind_finite = finite;
     mind_hyps = hyps;
     mind_packets = packets;
@@ -544,5 +555,6 @@ let check_inductive env mie =
   (* Then check positivity conditions *)
   let recargs = check_positivity env_arities inds in
   (* Build the inductive packets *)
-  build_inductive env env_arities mie.mind_entry_finite inds recargs cst
+  build_inductive env env_arities mie.mind_entry_record mie.mind_entry_finite 
+    inds recargs cst
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 4f180599..0f8c0d54 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml,v 1.76.2.1 2004/07/16 19:30:26 herbelin Exp $ *)
+(* $Id: safe_typing.ml,v 1.76.2.2 2005/11/23 14:46:08 barras Exp $ *)
 
 open Util
 open Names
@@ -427,11 +427,13 @@ type compiled_library =
 (* We check that only initial state Require's were performed before 
    [start_library] was called *)
 
+let is_empty senv =
+  senv.revsign = [] &&
+  senv.modinfo.msid = initial_msid &&
+  senv.modinfo.variant = NONE
+
 let start_library dir senv =
-  if not (senv.revsign = [] &&
-	  senv.modinfo.msid = initial_msid &&
-	  senv.modinfo.variant = NONE)
-  then
+  if not (is_empty senv) then
     anomaly "Safe_typing.start_library: environment should be empty";
   let dir_path,l = 
     match (repr_dirpath dir) with
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 84b98984..b973fcde 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: safe_typing.mli,v 1.33.2.1 2004/07/16 19:30:26 herbelin Exp $ i*)
+(*i $Id: safe_typing.mli,v 1.33.2.2 2005/11/23 14:46:08 barras Exp $ i*)
 
 (*i*)
 open Names
@@ -29,6 +29,8 @@ val env_of_safe_env : safe_environment -> Environ.env
 
 val empty_environment : safe_environment
 
+val is_empty : safe_environment -> bool
+
 (* Adding and removing local declarations (Local or Variables) *)
 val push_named_assum :
   identifier * types -> safe_environment ->
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 825ae8fa..835226fb 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml,v 1.11.2.1 2004/07/16 19:30:26 herbelin Exp $ i*)
+(*i $Id: subtyping.ml,v 1.11.2.2 2005/11/29 21:40:52 letouzey Exp $ i*)
 
 (*i*)
 open Util
@@ -132,6 +132,34 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
 	  in
 	    if kn1 <> kn2 then error ()
   end;
+  (* we check that records and their field names are preserved. *)
+  (* To stay compatible, we don't fail but only issue a warning. *)
+  if mib1.mind_record <> mib2.mind_record then begin
+    let sid = string_of_id mib1.mind_packets.(0).mind_typename in 
+    Pp.warning 
+      (sid^": record is implemented as an inductive type or conversely.\n"^
+	 "Beware that extraction cannot handle this situation.\n")
+  end; 
+  if mib1.mind_record then begin 
+    let rec names_prod_letin t = match kind_of_term t with 
+      | Prod(n,_,t) -> n::(names_prod_letin t)
+      | LetIn(n,_,_,t) -> n::(names_prod_letin t)
+      | Cast(t,_) -> names_prod_letin t
+      | _ -> []
+    in 
+    assert (Array.length mib1.mind_packets = 1);
+    assert (Array.length mib2.mind_packets = 1);
+    assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); 
+    assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); 
+    let fields1 = names_prod_letin mib1.mind_packets.(0).mind_user_lc.(0)
+    and fields2 = names_prod_letin mib2.mind_packets.(0).mind_user_lc.(0) in  
+    if fields1 <> fields2 then 
+      let sid = string_of_id mib1.mind_packets.(0).mind_typename in 
+      Pp.warning 
+	(sid^": record has different field names in its signature and "^
+	   "implemantation.\n"^
+	   "Beware that extraction cannot handle this situation.\n");
+  end;
   (* we first check simple things *)
   let cst = 
     array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
diff --git a/kernel/univ.ml b/kernel/univ.ml
index d46609c8..5e9fbd81 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml,v 1.17.10.1 2004/07/16 19:30:28 herbelin Exp $ *)
+(* $Id: univ.ml,v 1.17.10.3 2005/09/08 12:27:46 herbelin Exp $ *)
 
 (* Universes are stratified by a partial ordering $\ge$.
    Let $\~{}$ be the associated equivalence. We also have a strict ordering
@@ -57,7 +57,7 @@ let pr_uni = function
   | Max (gel,gtl) ->
       str "max(" ++ 
       prlist_with_sep pr_coma pr_uni_level gel ++
-      if gel <> [] & gtl <> [] then pr_coma () else mt () ++
+      (if gel <> [] & gtl <> [] then pr_coma () else mt ()) ++
       prlist_with_sep pr_coma
 	(fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl ++
       str ")"
@@ -69,9 +69,8 @@ let super = function
   | Variable u -> 
       Max ([],[u])
   | Max _ ->
-      anomaly ("Cannot take the successor of a non variable universes:\n"^
-       "you are probably typing a type already known to be the type\n"^
-       "of a user-provided term; if you really need this, please report")
+      anomaly ("Cannot take the successor of a non variable universes\n"^
+               "(maybe a bugged tactic)")
 
 (* returns the least upper bound of universes u and v. If they are not
    constrained, then a new universe is created.
@@ -412,6 +411,7 @@ let pr_arc = function
       pr_uni_level u ++ str " " ++
       v 0
         (prlist_with_sep pr_spc (fun v -> str "> " ++ pr_uni_level v) gt ++
+	(if ge <> [] & gt <> [] then spc () else mt ()) ++
          prlist_with_sep pr_spc (fun v -> str ">= " ++ pr_uni_level v) ge) ++
       fnl ()
   | Equiv (u,v) ->