From 2bdcd093b357adb2185518dabbafd1a0b9279044 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 27 Mar 2012 07:41:19 +0200 Subject: Imported Upstream version 8.3.pl4 --- pretyping/cases.ml | 4 ++-- pretyping/clenv.ml | 9 +++----- pretyping/detyping.ml | 10 +++++---- pretyping/inductiveops.ml | 21 ++++-------------- pretyping/namegen.ml | 47 ++++++++++++++++++++++++----------------- pretyping/namegen.mli | 7 +++--- pretyping/pretype_errors.ml | 4 ++-- pretyping/typeclasses_errors.ml | 6 +++--- pretyping/vnorm.ml | 11 ++++------ 9 files changed, 56 insertions(+), 63 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 749101f7..4205f517 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 14675 2011-11-17 22:19:34Z herbelin $ *) +(* $Id: cases.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Util open Names @@ -100,7 +100,7 @@ let rec list_try_compile f = function | h::t -> try f h with UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> + | Compat.Exc_located (_,(UserError _ | TypeError _ | PretypeError _)) -> list_try_compile f t let force_name = diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index abfef8d4..c2dd9f03 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: clenv.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: clenv.ml 15069 2012-03-20 14:06:07Z herbelin $ *) open Pp open Util @@ -146,9 +146,6 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_rename_from_n gls n (c,t) = - mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t) - let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) (******************************************************************) @@ -460,8 +457,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let clause = mk_clenv_from_env env sigma n (c,t) in clenv_constrain_dep_args hyps_only largs clause | ExplicitBindings lbind -> - let clause = mk_clenv_from_env env sigma n - (c,rename_bound_vars_as_displayed [] t) + let clause = mk_clenv_from_env env sigma n + (c,rename_bound_vars_as_displayed [] [] t) in clenv_match_args lbind clause | NoBindings -> mk_clenv_from_env env sigma n (c,t) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 14e72807..fe4354b6 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: detyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: detyping.ml 15069 2012-03-20 14:06:07Z herbelin $ *) open Pp open Util @@ -533,7 +533,7 @@ and detype_eqn isgoal avoid env constr construct_nargs branch = buildrec [] [] avoid env construct_nargs branch and detype_binder isgoal bk avoid env na ty c = - let flag = if isgoal then RenamingForGoal else (RenamingElsewhereFor c) in + let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (env,c) in let na',avoid' = if bk = BLetIn then compute_displayed_let_name_in flag avoid na c else compute_displayed_name_in flag avoid na c in @@ -553,9 +553,11 @@ let rec detype_rel_context where avoid env sign = | None -> na,avoid | Some c -> if b<>None then - compute_displayed_let_name_in (RenamingElsewhereFor c) avoid na c + compute_displayed_let_name_in + (RenamingElsewhereFor (env,c)) avoid na c else - compute_displayed_name_in (RenamingElsewhereFor c) avoid na c in + compute_displayed_name_in + (RenamingElsewhereFor (env,c)) avoid na c in let b = Option.map (detype false avoid env) b in let t = detype false avoid env t in (na',Explicit,b,t) :: aux avoid' (add_name na' env) rest diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 6e54c170..fe90941d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: inductiveops.ml 15019 2012-03-02 17:27:18Z letouzey $ *) open Util open Names @@ -403,21 +403,6 @@ let arity_of_case_predicate env (ind,params) dep k = (* Inferring the sort of parameters of a polymorphic inductive type knowing the sort of the conclusion *) -(* Check if u (sort of a parameter) appears in the sort of the - inductive (is). This is done by trying to enforce u > u' >= is - in the empty univ graph. If an inconsistency appears, then - is depends on u. *) -let is_constrained is u = - try - let u' = fresh_local_univ() in - let _ = - merge_constraints - (enforce_geq u (super u') - (enforce_geq u' is Constraint.empty)) - initial_universes in - false - with UniverseInconsistency _ -> true - (* Compute the inductive argument types: replace the sorts that appear in the type of the inductive by the sort of the conclusion, and the other ones by fresh universes. *) @@ -429,7 +414,9 @@ let rec instantiate_universes env scl is = function | (na,None,ty)::sign, Some u::exp -> let ctx,_ = Reduction.dest_arity env ty in let s = - if is_constrained is u then + (* Does the sort of parameter [u] appear in (or equal) + the sort of inductive [is] ? *) + if univ_depends u is then scl (* constrained sort: replace by scl *) else (* unconstriained sort: replace by fresh universe *) diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 45060511..f133d842 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: namegen.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: namegen.ml 15069 2012-03-20 14:06:07Z herbelin $ *) (* Created from contents that was formerly in termops.ml and nameops.ml, Nov 2009 *) @@ -223,22 +223,27 @@ let make_all_name_different env = looks for name of same base with lower available subscript beyond current subscript *) -let visibly_occur_id id c = - let rec occur c = match kind_of_term c with +let occur_rel p env id = + try lookup_name_of_rel p env = Name id + with Not_found -> false (* Unbound indice : may happen in debug *) + +let visibly_occur_id id (nenv,c) = + let rec occur n c = match kind_of_term c with | Const _ | Ind _ | Construct _ | Var _ when shortest_qualid_of_global Idset.empty (global_of_constr c) = qualid_of_ident id -> raise Occur - | _ -> iter_constr occur c + | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur + | _ -> iter_constr_with_binders succ occur n c in - try occur c; false + try occur 1 c; false with Occur -> true | Not_found -> false (* Happens when a global is not in the env *) -let next_ident_away_for_default_printing t id avoid = - let bad id = List.mem id avoid or visibly_occur_id id t in +let next_ident_away_for_default_printing env_t id avoid = + let bad id = List.mem id avoid or visibly_occur_id id env_t in next_ident_away_from id bad -let next_name_away_for_default_printing t na avoid = +let next_name_away_for_default_printing env_t na avoid = let id = match na with | Name id -> id | Anonymous -> @@ -246,7 +251,7 @@ let next_name_away_for_default_printing t na avoid = (* taken into account by the function compute_displayed_name_in; *) (* just in case, invent a valid name *) id_of_string "H" in - next_ident_away_for_default_printing t id avoid + next_ident_away_for_default_printing env_t id avoid (**********************************************************************) (* Displaying terms avoiding bound variables clashes *) @@ -269,13 +274,13 @@ let next_name_away_for_default_printing t na avoid = type renaming_flags = | RenamingForCasesPattern | RenamingForGoal - | RenamingElsewhereFor of constr + | RenamingElsewhereFor of (name list * constr) let next_name_for_display flags = match flags with | RenamingForCasesPattern -> next_name_away_in_cases_pattern | RenamingForGoal -> next_name_away_in_goal - | RenamingElsewhereFor t -> next_name_away_for_default_printing t + | RenamingElsewhereFor env_t -> next_name_away_for_default_printing env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) let compute_displayed_name_in flags avoid na c = @@ -297,16 +302,20 @@ let compute_displayed_let_name_in flags avoid na c = let fresh_id = next_name_for_display flags na avoid in (Name fresh_id, fresh_id::avoid) -let rec rename_bound_vars_as_displayed avoid c = - let rec rename avoid c = +let rec rename_bound_vars_as_displayed avoid env c = + let rec rename avoid env c = match kind_of_term c with | Prod (na,c1,c2) -> - let na',avoid' = compute_displayed_name_in (RenamingElsewhereFor c2) avoid na c2 in - mkProd (na', c1, rename avoid' c2) + let na',avoid' = + compute_displayed_name_in + (RenamingElsewhereFor (env,c2)) avoid na c2 in + mkProd (na', c1, rename avoid' (add_name na' env) c2) | LetIn (na,c1,t,c2) -> - let na',avoid' = compute_displayed_let_name_in (RenamingElsewhereFor c2) avoid na c2 in - mkLetIn (na',c1,t, rename avoid' c2) - | Cast (c,k,t) -> mkCast (rename avoid c, k,t) + let na',avoid' = + compute_displayed_let_name_in + (RenamingElsewhereFor (env,c2)) avoid na c2 in + mkLetIn (na',c1,t, rename avoid' (add_name na' env) c2) + | Cast (c,k,t) -> mkCast (rename avoid env c, k,t) | _ -> c in - rename avoid c + rename avoid env c diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index f99ee3f6..464efcf8 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: namegen.mli 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: namegen.mli 15069 2012-03-20 14:06:07Z herbelin $ *) open Names open Term @@ -64,7 +64,7 @@ val next_name_away_with_default : string -> name -> identifier list -> type renaming_flags = | RenamingForCasesPattern (* avoid only global constructors *) | RenamingForGoal (* avoid all globals (as in intro) *) - | RenamingElsewhereFor of constr + | RenamingElsewhereFor of (name list * constr) val make_all_name_different : env -> env @@ -74,4 +74,5 @@ val compute_and_force_displayed_name_in : renaming_flags -> identifier list -> name -> constr -> name * identifier list val compute_displayed_let_name_in : renaming_flags -> identifier list -> name -> constr -> name * identifier list -val rename_bound_vars_as_displayed : identifier list -> types -> types +val rename_bound_vars_as_displayed : + identifier list -> name list -> types -> types diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 688a25b9..a9b2a18b 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pretype_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) +(* $Id: pretype_errors.ml 15025 2012-03-09 14:27:07Z glondu $ *) open Util open Stdpp @@ -45,7 +45,7 @@ exception PretypeError of env * pretype_error let precatchable_exception = function | Util.UserError _ | TypeError _ | PretypeError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | + | Compat.Exc_located(_,(Util.UserError _ | TypeError _ | Nametab.GlobalizationError _ | PretypeError _)) -> true | _ -> false diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 62941a76..7b09f957 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeclasses_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) +(*i $Id: typeclasses_errors.ml 15025 2012-03-09 14:27:07Z glondu $ i*) (*i*) open Names @@ -47,7 +47,7 @@ let unsatisfiable_constraints env evd ev = raise (TypeClassError (env, UnsatisfiableConstraints (evd, None))) | Some ev -> let loc, kind = Evd.evar_source ev evd in - raise (Stdpp.Exc_located (loc, TypeClassError + raise (Compat.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints (evd, Some (ev, kind))))) let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m)) @@ -55,5 +55,5 @@ let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstan let rec unsatisfiable_exception exn = match exn with | TypeClassError (_, UnsatisfiableConstraints _) -> true - | Stdpp.Exc_located(_, e) -> unsatisfiable_exception e + | Compat.Exc_located(_, e) -> unsatisfiable_exception e | _ -> false diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 395f5c8d..57b183d5 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vnorm.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) +(*i $Id: vnorm.ml 15029 2012-03-13 14:47:00Z herbelin $ i*) open Names open Declarations @@ -111,7 +111,7 @@ let build_branches_type env (mind,_ as _ind) mib mip params dep p = a 0) et les lambda correspondant aux realargs *) let build_one_branch i cty = let typi = type_constructor mind mib cty params in - let decl,indapp = Term.decompose_prod typi in + let decl,indapp = decompose_prod_assum typi in let ind,cargs = find_rectype_a env indapp in let nparams = Array.length params in let carity = snd (rtbl.(i)) in @@ -195,11 +195,8 @@ and nf_stk env c t stk = let bsw = branch_of_switch (nb_rel env) sw in let mkbranch i (n,v) = let decl,codom = btypes.(i) in - let env = - List.fold_right - (fun (name,t) env -> push_rel (name,None,t) env) decl env in - let b = nf_val env v codom in - compose_lam decl b + let b = nf_val (push_rel_context decl env) v codom in + it_mkLambda_or_LetIn b decl in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type dep p realargs c in -- cgit v1.2.3