From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 8 Aug 2008 13:18:42 +0200 Subject: Imported Upstream version 8.2~beta4+dfsg --- kernel/environ.ml | 13 +++++-------- kernel/environ.mli | 4 ++-- kernel/indtypes.ml | 12 +++++++----- kernel/inductive.ml | 8 +++++--- kernel/inductive.mli | 5 ++++- kernel/modops.ml | 36 ++++++++++++++++++------------------ kernel/names.ml | 4 ++-- kernel/safe_typing.ml | 13 +++++++------ kernel/term.ml | 23 +++++++++++++++-------- kernel/term.mli | 6 +++++- kernel/term_typing.ml | 4 ++-- kernel/univ.ml | 7 ++++++- kernel/univ.mli | 4 +++- 13 files changed, 81 insertions(+), 58 deletions(-) (limited to 'kernel') diff --git a/kernel/environ.ml b/kernel/environ.ml index ad435eb5..86e02623 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml 11001 2008-05-27 16:56:07Z aspiwack $ *) +(* $Id: environ.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -379,17 +379,14 @@ let insert_after_hyp (ctxt,vals) id d check = (* To be used in Logic.clear_hyps *) let remove_hyps ids check_context check_value (ctxt, vals) = - let ctxt,vals,rmv = - List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals,rmv) -> + List.fold_right2 (fun (id,_,_ as d) (id',v) (ctxt,vals) -> if List.mem id ids then - (ctxt,vals,id::rmv) + (ctxt,vals) else let nd = check_context d in let nv = check_value v in - (nd::ctxt,(id',nv)::vals,rmv)) - ctxt vals ([],[],[]) - in ((ctxt,vals),rmv) - + (nd::ctxt,(id',nv)::vals)) + ctxt vals ([],[]) diff --git a/kernel/environ.mli b/kernel/environ.mli index 30f555a4..97e19782 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: environ.mli 11001 2008-05-27 16:56:07Z aspiwack $ i*) +(*i $Id: environ.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Names @@ -222,7 +222,7 @@ val insert_after_hyp : named_context_val -> variable -> named_declaration -> (named_context -> unit) -> named_context_val -val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val * identifier list +val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val (* spiwack: functions manipulating the retroknowledge *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7cedebbd..01b8aca1 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 10920 2008-05-12 10:19:32Z herbelin $ *) +(* $Id: indtypes.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -254,16 +254,19 @@ let typecheck_inductive env mie = array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> let sign, s = dest_arity env full_arity in let status,cst = match s with - | Type _ when ar_level <> None (* Explicitly polymorphic *) -> + | Type u when ar_level <> None (* Explicitly polymorphic *) + && no_upper_constraints u cst -> (* The polymorphic level is a function of the level of the *) (* conclusions of the parameters *) - Inr (param_ccls, lev), cst + (* We enforce [u >= lev] in case [lev] has a strict upper *) + (* constraints over [u] *) + Inr (param_ccls, lev), enforce_geq u lev cst | Type u (* Not an explicit occurrence of Type *) -> Inl (info,full_arity,s), enforce_geq u lev cst | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) if not (is_type0m_univ lev) & not (is_type0_univ lev) then - error "Large non-propositional inductive types must be in Type"; + error "Large non-propositional inductive types must be in Type."; Inl (info,full_arity,s), cst | Prop _ -> Inl (info,full_arity,s), cst in @@ -598,7 +601,6 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = poly_level = lev; }, all_sorts | Inl ((issmall,isunit),ar,s) -> - let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in let kelim = allowed_sorts issmall isunit s in Monomorphic { mind_user_arity = ar; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 9415941d..4bb8e9d6 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 10920 2008-05-12 10:19:32Z herbelin $ *) +(* $Id: inductive.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -218,7 +218,7 @@ let type_of_constructor cstr (mib,mip) = let specif = mip.mind_user_lc in let i = index_of_constructor cstr in let nconstr = Array.length mip.mind_consnames in - if i > nconstr then error "Not enough constructors in the type"; + if i > nconstr then error "Not enough constructors in the type."; constructor_instantiate (fst ind) mib specif.(i-1) let arities_of_specif kn (mib,mip) = @@ -228,7 +228,9 @@ let arities_of_specif kn (mib,mip) = let arities_of_constructors ind specif = arities_of_specif (fst ind) specif - +let type_of_constructors ind (mib,mip) = + let specif = mip.mind_user_lc in + Array.map (constructor_instantiate (fst ind) mib) specif (************************************************************************) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c2c38d8d..8059051b 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductive.mli 9420 2006-12-08 15:34:09Z barras $ i*) +(*i $Id: inductive.mli 11301 2008-08-04 19:41:18Z herbelin $ i*) (*i*) open Names @@ -47,6 +47,9 @@ val type_of_constructor : constructor -> mind_specif -> types (* Return constructor types in normal form *) val arities_of_constructors : inductive -> mind_specif -> types array +(* Return constructor types in user form *) +val type_of_constructors : inductive -> mind_specif -> types array + (* Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array diff --git a/kernel/modops.ml b/kernel/modops.ml index 9242a757..7bed3254 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 11142 2008-06-18 15:37:31Z soubiran $ i*) +(*i $Id: modops.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Util @@ -22,51 +22,51 @@ open Mod_subst let error_existing_label l = - error ("The label "^string_of_label l^" is already declared") + error ("The label "^string_of_label l^" is already declared.") -let error_declaration_not_path _ = error "Declaration is not a path" +let error_declaration_not_path _ = error "Declaration is not a path." -let error_application_to_not_path _ = error "Application to not path" +let error_application_to_not_path _ = error "Application to not path." -let error_not_a_functor _ = error "Application of not a functor" +let error_not_a_functor _ = error "Application of not a functor." -let error_incompatible_modtypes _ _ = error "Incompatible module types" +let error_incompatible_modtypes _ _ = error "Incompatible module types." -let error_not_equal _ _ = error "Not equal modules" +let error_not_equal _ _ = error "Non equal modules." -let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match") +let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.") -let error_no_such_label l = error ("No such label "^string_of_label l) +let error_no_such_label l = error ("No such label "^string_of_label l^".") let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") let error_result_must_be_signature () = - error "The result module type must be a signature" + error "The result module type must be a signature." let error_signature_expected mtb = - error "Signature expected" + error "Signature expected." let error_no_module_to_end _ = - error "No open module to end" + error "No open module to end." let error_no_modtype_to_end _ = - error "No open module type to end" + error "No open module type to end." let error_not_a_modtype_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module type")) + user_err_loc (loc,"",str ("\""^s^"\" is not a module type.")) let error_not_a_module_loc loc s = - user_err_loc (loc,"",str ("\""^s^"\" is not a module")) + user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) let error_not_a_module s = error_not_a_module_loc dummy_loc s let error_not_a_constant l = - error ("\""^(string_of_label l)^"\" is not a constant") + error ("\""^(string_of_label l)^"\" is not a constant.") let error_with_incorrect l = - error ("Incorrect constraint for label \""^(string_of_label l)^"\"") + error ("Incorrect constraint for label \""^(string_of_label l)^"\".") let error_a_generative_module_expected l = error ("The module " ^ string_of_label l ^ " is not generative. Only " ^ @@ -79,7 +79,7 @@ let error_local_context lo = error ("The local context is not empty.") | (Some l) -> error ("The local context of the component "^ - (string_of_label l)^" is not empty") + (string_of_label l)^" is not empty.") let error_no_such_label_sub l l1 l2 = diff --git a/kernel/names.ml b/kernel/names.ml index 26bcc2eb..25f03495 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 10919 2008-05-11 22:04:26Z msozeau $ *) +(* $Id: names.ml 11238 2008-07-19 09:34:03Z herbelin $ *) open Pp open Util @@ -101,7 +101,7 @@ let label_of_mbid (_,s,_) = s let mk_label l = l -let string_of_label l = l +let string_of_label = string_of_id let id_of_label l = l let label_of_id id = id diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 6906fb29..3c7461b2 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 11170 2008-06-25 08:31:04Z soubiran $ *) +(* $Id: safe_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -163,7 +163,7 @@ let safe_push_named (id,_,_ as d) env = let _ = try let _ = lookup_named id env in - error ("identifier "^string_of_id id^" already defined") + error ("Identifier "^string_of_id id^" already defined.") with Not_found -> () in Environ.push_named d env @@ -446,7 +446,7 @@ let end_module l restype senv = let senv = add_constraints (struct_expr_constraints struct_expr) senv in let msid,str = match (eval_struct senv.env struct_expr) with | SEBstruct(msid,str_l) -> msid,str_l - | _ -> error ("You cannot Include a higher-order Module or Module Type" ) + | _ -> error ("You cannot Include a higher-order Module or Module Type.") in let mp_sup = senv.modinfo.modpath in let str1 = subst_signature_msid msid mp_sup str in @@ -660,7 +660,7 @@ let check_engagement env c = | Some ImpredicativeSet, Some ImpredicativeSet -> () | _, None -> () | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set" + error "Needs option -impredicative-set." let set_engagement c senv = {senv with @@ -739,9 +739,10 @@ let check_imports senv needed = try let actual_stamp = List.assoc id imports in if stamp <> actual_stamp then - error ("Inconsistent assumptions over module " ^(string_of_dirpath id)) + error + ("Inconsistent assumptions over module "^(string_of_dirpath id)^".") with Not_found -> - error ("Reference to unknown module " ^ (string_of_dirpath id)) + error ("Reference to unknown module "^(string_of_dirpath id)^".") in List.iter check needed diff --git a/kernel/term.ml b/kernel/term.ml index c920c80b..1f3d2635 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term.ml 10859 2008-04-27 16:46:15Z herbelin $ *) +(* $Id: term.ml 11309 2008-08-06 10:30:35Z herbelin $ *) (* This module instantiates the structure of generic deBruijn terms to Coq *) @@ -370,16 +370,22 @@ let destProd c = match kind_of_term c with | Prod (x,t1,t2) -> (x,t1,t2) | _ -> invalid_arg "destProd" +let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false + (* Destructs the abstraction [x:t1]t2 *) let destLambda c = match kind_of_term c with | Lambda (x,t1,t2) -> (x,t1,t2) | _ -> invalid_arg "destLambda" +let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false + (* Destructs the let [x:=b:t1]t2 *) let destLetIn c = match kind_of_term c with | LetIn (x,b,t1,t2) -> (x,b,t1,t2) | _ -> invalid_arg "destProd" +let isLetIn c = match kind_of_term c with LetIn _ -> true | _ -> false + (* Destructs an application *) let destApp c = match kind_of_term c with | App (f,a) -> (f, a) @@ -389,10 +395,6 @@ let destApplication = destApp let isApp c = match kind_of_term c with App _ -> true | _ -> false -let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false - -let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false - (* Destructs a constant *) let destConst c = match kind_of_term c with | Const kn -> kn @@ -419,22 +421,27 @@ let destConstruct c = match kind_of_term c with | Construct (kn, a as r) -> r | _ -> invalid_arg "dest" -let isConstruct c = match kind_of_term c with - Construct _ -> true | _ -> false +let isConstruct c = match kind_of_term c with Construct _ -> true | _ -> false (* Destructs a term

Case c of lc1 | lc2 .. | lcn end *) let destCase c = match kind_of_term c with | Case (ci,p,c,v) -> (ci,p,c,v) | _ -> anomaly "destCase" +let isCase c = match kind_of_term c with Case _ -> true | _ -> false + let destFix c = match kind_of_term c with | Fix fix -> fix | _ -> invalid_arg "destFix" - + +let isFix c = match kind_of_term c with Fix _ -> true | _ -> false + let destCoFix c = match kind_of_term c with | CoFix cofix -> cofix | _ -> invalid_arg "destCoFix" +let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false + (******************************************************************) (* Cast management *) (******************************************************************) diff --git a/kernel/term.mli b/kernel/term.mli index 6236dc39..3b5a2bc1 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term.mli 10859 2008-04-27 16:46:15Z herbelin $ i*) +(*i $Id: term.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) (*i*) open Names @@ -230,9 +230,13 @@ val isSort : constr -> bool val isCast : constr -> bool val isApp : constr -> bool val isLambda : constr -> bool +val isLetIn : constr -> bool val isProd : constr -> bool val isConst : constr -> bool val isConstruct : constr -> bool +val isFix : constr -> bool +val isCoFix : constr -> bool +val isCase : constr -> bool val is_Prop : constr -> bool val is_Set : constr -> bool diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 0f649057..f50a0b83 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term_typing.ml 10877 2008-04-30 21:58:41Z herbelin $ *) +(* $Id: term_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Names @@ -60,7 +60,7 @@ let safe_push_named (id,_,_ as d) env = let _ = try let _ = lookup_named id env in - error ("identifier "^string_of_id id^" already defined") + error ("Identifier "^string_of_id id^" already defined.") with Not_found -> () in push_named d env diff --git a/kernel/univ.ml b/kernel/univ.ml index 3791c3e1..11a5452c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 11063 2008-06-06 16:03:45Z soubiran $ *) +(* $Id: univ.ml 11301 2008-08-04 19:41:18Z herbelin $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -550,6 +550,11 @@ let subst_large_constraint u u' v = let subst_large_constraints = List.fold_right (fun (u,u') -> subst_large_constraint u u') +let no_upper_constraints u cst = + match u with + | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst + | Max _ -> anomaly "no_upper_constraints" + (* Pretty-printing *) let num_universes g = diff --git a/kernel/univ.mli b/kernel/univ.mli index 0a1a8328..668e99a0 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: univ.mli 11063 2008-06-06 16:03:45Z soubiran $ i*) +(*i $Id: univ.mli 11301 2008-08-04 19:41:18Z herbelin $ i*) (* Universes. *) @@ -76,6 +76,8 @@ val subst_large_constraint : universe -> universe -> universe -> universe val subst_large_constraints : (universe * universe) list -> universe -> universe +val no_upper_constraints : universe -> constraints -> bool + (*s Pretty-printing of universes. *) val pr_uni : universe -> Pp.std_ppcmds -- cgit v1.2.3