From 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Thu, 19 Jan 2006 22:34:29 +0000 Subject: Imported Upstream version 8.0pl3 --- kernel/declarations.ml | 6 ++++-- kernel/declarations.mli | 3 ++- kernel/entries.ml | 3 ++- kernel/entries.mli | 3 ++- kernel/indtypes.ml | 34 +++++++++++++++++++++++----------- kernel/safe_typing.ml | 12 +++++++----- kernel/safe_typing.mli | 4 +++- kernel/subtyping.ml | 30 +++++++++++++++++++++++++++++- kernel/univ.ml | 10 +++++----- 9 files changed, 77 insertions(+), 28 deletions(-) (limited to 'kernel') 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) -> -- cgit v1.2.3