aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml6
-rw-r--r--pretyping/cases.ml387
-rw-r--r--pretyping/cases.mli26
-rw-r--r--pretyping/classops.ml53
-rw-r--r--pretyping/classops.mli4
-rw-r--r--pretyping/coercion.ml9
-rw-r--r--pretyping/globEnv.ml201
-rw-r--r--pretyping/globEnv.mli83
-rw-r--r--pretyping/glob_ops.ml20
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--pretyping/inferCumulativity.ml2
-rw-r--r--pretyping/ltac_pretype.ml2
-rw-r--r--pretyping/pretyping.ml459
-rw-r--r--pretyping/pretyping.mli8
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--pretyping/recordops.ml14
-rw-r--r--pretyping/reductionops.ml19
-rw-r--r--pretyping/reductionops.mli3
-rw-r--r--pretyping/typeclasses.ml40
19 files changed, 735 insertions, 603 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index 9d4badc60a..b8958ca944 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -21,7 +21,7 @@ module NamedDecl = Context.Named.Declaration
(*i*)
let name_table =
- Summary.ref (Refmap.empty : Name.t list Refmap.t)
+ Summary.ref (GlobRef.Map.empty : Name.t list GlobRef.Map.t)
~name:"rename-arguments"
type req =
@@ -29,7 +29,7 @@ type req =
| ReqGlobal of GlobRef.t * Name.t list
let load_rename_args _ (_, (_, (r, names))) =
- name_table := Refmap.add r names !name_table
+ name_table := GlobRef.Map.add r names !name_table
let cache_rename_args o = load_rename_args 1 o
@@ -68,7 +68,7 @@ let rename_arguments local r names =
let req = if local then ReqLocal else ReqGlobal (r, names) in
Lib.add_anonymous_leaf (inRenameArgs (req, (r, names)))
-let arguments_names r = Refmap.find r !name_table
+let arguments_names r = GlobRef.Map.find r !name_table
let rec rename_prod c = function
| [] -> c
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ad33297f0a..7baa755ab5 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -35,7 +35,7 @@ open Evarsolve
open Evarconv
open Evd
open Context.Rel.Declaration
-open Ltac_pretype
+open GlobEnv
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
@@ -114,8 +114,10 @@ let rec relocate_index sigma n1 n2 k t =
(**********************************************************************)
(* Structures used in compiling pattern-matching *)
+let (!!) env = GlobEnv.env env
+
type 'a rhs =
- { rhs_env : env;
+ { rhs_env : GlobEnv.t;
rhs_vars : Id.Set.t;
avoid_ids : Id.Set.t;
it : 'a option}
@@ -247,8 +249,7 @@ let push_history_pattern n pci cont =
*)
type 'a pattern_matching_problem =
- { env : env;
- lvar : Ltac_pretype.ltac_var_map;
+ { env : GlobEnv.t;
evdref : evar_map ref;
pred : constr;
tomatch : tomatch_stack;
@@ -256,7 +257,7 @@ type 'a pattern_matching_problem =
mat : 'a matrix;
caseloc : Loc.t option;
casestyle : case_style;
- typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
+ typing_function: type_constraint -> GlobEnv.t -> evar_map ref -> 'a option -> unsafe_judgment }
(*--------------------------------------------------------------------------*
* A few functions to infer the inductive type from the patterns instead of *
@@ -331,6 +332,10 @@ let binding_vars_of_inductive sigma = function
| NotInd _ -> []
| IsInd (_,IndType(_,realargs),_) -> List.filter (isRel sigma) realargs
+let set_tomatch_realnames names = function
+ | NotInd _ as t -> t
+ | IsInd (typ,ind,_) -> IsInd (typ,ind,names)
+
let extract_inductive_data env sigma decl =
match decl with
| LocalAssum (_,t) ->
@@ -357,58 +362,58 @@ let find_tomatch_tycon evdref env loc = function
| None ->
empty_tycon,None
-let make_return_predicate_ltac_lvar sigma na tm c lvar =
+let make_return_predicate_ltac_lvar env sigma na tm c =
+ (* If we have an [x as x return ...] clause and [x] expands to [c],
+ we have to update the status of [x] in the substitution:
+ - if [c] is a variable [id'], then [x] should now become [id']
+ - otherwise, [x] should be hidden *)
match na, DAst.get tm with
| Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' ->
- if Id.Map.mem id lvar.ltac_genargs then
- let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in
- let ltac_idents = match kind sigma c with
- | Var id' -> Id.Map.add id id' lvar.ltac_idents
- | _ -> lvar.ltac_idents in
- { lvar with ltac_genargs; ltac_idents }
- else lvar
- | _ -> lvar
-
-let ltac_interp_realnames lvar = function
- | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal)
- | _ as x -> x
+ let expansion = match kind sigma c with
+ | Var id' -> Name id'
+ | _ -> Anonymous in
+ GlobEnv.hide_variable env expansion id
+ | _ -> env
let is_patvar pat =
match DAst.get pat with
| PatVar _ -> true
| _ -> false
-let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
+let coerce_row typing_fun evdref env pats (tomatch,(na,indopt)) =
let loc = loc_of_glob_constr tomatch in
- let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
- let j = typing_fun tycon env evdref !lvar tomatch in
- let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) env) evdref j in
+ let tycon,realnames = find_tomatch_tycon evdref !!env loc indopt in
+ let j = typing_fun tycon env evdref tomatch in
+ let j = evd_comb1 (Coercion.inh_coerce_to_base ?loc:(loc_of_glob_constr tomatch) !!env) evdref j in
let typ = nf_evar !evdref j.uj_type in
- lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
+ let env = make_return_predicate_ltac_lvar env !evdref na tomatch j.uj_val in
let t =
if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else
- try try_find_ind env !evdref typ realnames
+ try try_find_ind !!env !evdref typ realnames
with Not_found ->
- unify_tomatch_with_patterns evdref env loc typ pats realnames in
- (j.uj_val,t)
+ unify_tomatch_with_patterns evdref !!env loc typ pats realnames in
+ (env,(j.uj_val,t))
-let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
+let coerce_to_indtype typing_fun evdref env matx tomatchl =
let pats = List.map (fun r -> r.patterns) matx in
let matx' = match matrix_transpose pats with
| [] -> List.map (fun _ -> []) tomatchl (* no patterns at all *)
| m -> m in
- let lvar = ref lvar in
- let tms = List.map2 (coerce_row typing_fun evdref env lvar) matx' tomatchl in
- let tms = List.map (ltac_interp_realnames !lvar) tms in
- !lvar,tms
+ let env,tms = List.fold_left2_map (fun env -> coerce_row typing_fun evdref env) env matx' tomatchl in
+ env,tms
(************************************************************************)
(* Utils *)
let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
- let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in
+ let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in
e
+let evd_comb2 f evdref x y =
+ let (evd',y) = f !evdref x y in
+ evdref := evd';
+ y
+
let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
(* Ideally, we could find a common inductive type to which both the
term to match and the patterns coerce *)
@@ -418,7 +423,7 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
let typ,names =
match typ with IsInd(t,_,names) -> t,Some names | NotInd(_,t) -> t,None in
let tmtyp =
- try try_find_ind pb.env !(pb.evdref) typ names
+ try try_find_ind !!(pb.env) !(pb.evdref) typ names
with Not_found -> NotInd (None,typ) in
match tmtyp with
| NotInd (None,typ) ->
@@ -426,17 +431,17 @@ let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
(match find_row_ind tm1 with
| None -> (current,tmtyp)
| Some (_,(ind,_)) ->
- let indt = inductive_template pb.evdref pb.env None ind in
+ let indt = inductive_template pb.evdref !!(pb.env) None ind in
let current =
if List.is_empty deps && isEvar !(pb.evdref) typ then
(* Don't insert coercions if dependent; only solve evars *)
- let () = Option.iter ((:=) pb.evdref) (cumul pb.env !(pb.evdref) indt typ) in
+ let () = Option.iter ((:=) pb.evdref) (cumul !!(pb.env) !(pb.evdref) indt typ) in
current
else
- (evd_comb2 (Coercion.inh_conv_coerce_to true pb.env)
+ (evd_comb2 (Coercion.inh_conv_coerce_to true !!(pb.env))
pb.evdref (make_judge current typ) indt).uj_val in
let sigma = !(pb.evdref) in
- (current,try_find_ind pb.env sigma indt names))
+ (current,try_find_ind !!(pb.env) sigma indt names))
| _ -> (current,tmtyp)
let type_of_tomatch = function
@@ -466,10 +471,10 @@ let remove_current_pattern eqn =
alias_stack = alias_of_pat pat :: eqn.alias_stack }
| [] -> anomaly (Pp.str "Empty list of patterns.")
-let push_current_pattern (cur,ty) eqn =
+let push_current_pattern sigma (cur,ty) eqn =
match eqn.patterns with
| pat::pats ->
- let rhs_env = push_rel (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
+ let _,rhs_env = push_rel sigma (LocalDef (alias_of_pat pat,cur,ty)) eqn.rhs.rhs_env in
{ eqn with
rhs = { eqn.rhs with rhs_env = rhs_env };
patterns = pats }
@@ -739,7 +744,7 @@ let merge_name get_name obj = function
let merge_names get_name = List.map2 (merge_name get_name)
-let get_names env sigma sign eqns =
+let get_names avoid env sigma sign eqns =
let names1 = List.make (Context.Rel.length sign) Anonymous in
(* If any, we prefer names used in pats, from top to bottom *)
let names2,aliasname =
@@ -752,7 +757,7 @@ let get_names env sigma sign eqns =
avoiding conflicts with user ids *)
let allvars =
List.fold_left (fun l (_,_,eqn) -> Id.Set.union l eqn.rhs.avoid_ids)
- Id.Set.empty eqns in
+ avoid eqns in
let names3,_ =
List.fold_left2
(fun (l,avoid) d na ->
@@ -774,7 +779,7 @@ let get_names env sigma sign eqns =
let recover_initial_subpattern_names = List.map2 RelDecl.set_name
-let recover_and_adjust_alias_names names sign =
+let recover_and_adjust_alias_names (_,avoid) names sign =
let rec aux = function
| [],[] ->
[]
@@ -786,31 +791,31 @@ let recover_and_adjust_alias_names names sign =
in
List.split (aux (names,sign))
-let push_rels_eqn sign eqn =
+let push_rels_eqn sigma sign eqn =
{eqn with
- rhs = {eqn.rhs with rhs_env = push_rel_context sign eqn.rhs.rhs_env} }
+ rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } }
-let push_rels_eqn_with_names sign eqn =
+let push_rels_eqn_with_names sigma sign eqn =
let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in
let subpatnames = List.map alias_of_pat subpats in
let sign = recover_initial_subpattern_names subpatnames sign in
- push_rels_eqn sign eqn
+ push_rels_eqn sigma sign eqn
-let push_generalized_decl_eqn env n decl eqn =
+let push_generalized_decl_eqn env sigma n decl eqn =
match RelDecl.get_name decl with
| Anonymous ->
- push_rels_eqn [decl] eqn
+ push_rels_eqn sigma [decl] eqn
| Name _ ->
- push_rels_eqn [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn
+ push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn
let drop_alias_eqn eqn =
{ eqn with alias_stack = List.tl eqn.alias_stack }
-let push_alias_eqn alias eqn =
+let push_alias_eqn sigma alias eqn =
let aliasname = List.hd eqn.alias_stack in
let eqn = drop_alias_eqn eqn in
let alias = RelDecl.set_name aliasname alias in
- push_rels_eqn [alias] eqn
+ push_rels_eqn sigma [alias] eqn
(**********************************************************************)
(* Functions to deal with elimination predicate *)
@@ -958,7 +963,7 @@ let rec extract_predicate ccl = function
ccl
let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
- let sign = make_arity_signature env sigma true indf in
+ let sign = make_arity_signature !!env sigma true indf in
(* n is the number of real args + 1 (+ possible let-ins in sign) *)
let n = List.length sign in
(* Before abstracting we generalize over cur and on those realargs *)
@@ -979,7 +984,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
let pred = extract_predicate ccl tms in
(* Build the predicate properly speaking *)
let sign = List.map2 set_name (na::names) sign in
- it_mkLambda_or_LetIn_name env sigma pred sign
+ it_mkLambda_or_LetIn_name !!env sigma pred sign
(* [expand_arg] is used by [specialize_predicate]
if Yk denotes [Xk;xk] or [Xk],
@@ -1208,7 +1213,7 @@ let first_clause_irrefutable env = function
let group_equations pb ind current cstrs mat =
let mat =
- if first_clause_irrefutable pb.env mat then [List.hd mat] else mat in
+ if first_clause_irrefutable !!(pb.env) mat then [List.hd mat] else mat in
let brs = Array.make (Array.length cstrs) [] in
let only_default = ref None in
let _ =
@@ -1216,7 +1221,7 @@ let group_equations pb ind current cstrs mat =
(fun eqn () ->
let rest = remove_current_pattern eqn in
let pat = current_pattern eqn in
- match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with
+ match DAst.get (check_and_adjust_constructor !!(pb.env) ind cstrs pat) with
| PatVar name ->
(* This is a default clause that we expand *)
for i=1 to Array.length cstrs do
@@ -1238,7 +1243,7 @@ let rec generalize_problem names pb = function
| [] -> pb, []
| i::l ->
let pb',deps = generalize_problem names pb l in
- let d = map_constr (lift i) (lookup_rel i pb.env) in
+ let d = map_constr (lift i) (lookup_rel i !!(pb.env)) in
begin match d with
| LocalDef (Anonymous,_,_) -> pb', deps
| _ ->
@@ -1271,7 +1276,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
(* that had matched constructor C *)
let cs_args = const_info.cs_args in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs_args in
- let names,aliasname = get_names pb.env !(pb.evdref) cs_args eqns in
+ let names,aliasname = get_names (GlobEnv.vars_of_env pb.env) !!(pb.env) !(pb.evdref) cs_args eqns in
let typs = List.map2 RelDecl.set_name names cs_args
in
@@ -1279,7 +1284,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
(* This is a bit too strong I think, in the sense that what we would *)
(* really like is to have beta-iota reduction only at the positions where *)
(* parameters are substituted *)
- let typs = List.map (map_type (nf_betaiota pb.env !(pb.evdref))) typs in
+ let typs = List.map (map_type (nf_betaiota !!(pb.env) !(pb.evdref))) typs in
(* We build the matrix obtained by expanding the matching on *)
(* "C x1..xn as x" followed by a residual matching on eqn into *)
@@ -1291,11 +1296,11 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
let typs' =
List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in
- let extenv = push_rel_context typs pb.env in
+ let typs,extenv = push_rel_context !(pb.evdref) typs pb.env in
let typs' =
List.map (fun (c,d) ->
- (c,extract_inductive_data extenv !(pb.evdref) d,d)) typs' in
+ (c,extract_inductive_data !!extenv !(pb.evdref) d,d)) typs' in
(* We compute over which of x(i+1)..xn and x matching on xi will need a *)
(* generalization *)
@@ -1360,7 +1365,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
let submat = adjust_impossible_cases pb pred tomatch submat in
let () = match submat with
| [] ->
- raise_pattern_matching_error (pb.env, Evd.empty, NonExhaustive (complete_history history))
+ raise_pattern_matching_error (!!(pb.env), Evd.empty, NonExhaustive (complete_history history))
| _ -> ()
in
@@ -1370,7 +1375,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
tomatch = tomatch;
pred = pred;
history = history;
- mat = List.map (push_rels_eqn_with_names typs) submat }
+ mat = List.map (push_rels_eqn_with_names !(pb.evdref) typs) submat }
(**********************************************************************
INVARIANT:
@@ -1400,13 +1405,13 @@ and match_current pb (initial,tomatch) =
let ((current,typ),deps,dep) = tomatch in
match typ with
| NotInd (_,typ) ->
- check_all_variables pb.env !(pb.evdref) typ pb.mat;
+ check_all_variables !!(pb.env) !(pb.evdref) typ pb.mat;
compile_all_variables initial tomatch pb
| IsInd (_,(IndType(indf,realargs) as indt),names) ->
let mind,_ = dest_ind_family indf in
- let mind = Tacred.check_privacy pb.env mind in
- let cstrs = get_constructors pb.env indf in
- let arsign, _ = get_arity pb.env indf in
+ let mind = Tacred.check_privacy !!(pb.env) mind in
+ let cstrs = get_constructors !!(pb.env) indf in
+ let arsign, _ = get_arity !!(pb.env) indf in
let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in
let no_cstr = Int.equal (Array.length cstrs) 0 in
if (not no_cstr || not (List.is_empty pb.mat)) && onlydflt then
@@ -1423,18 +1428,17 @@ and match_current pb (initial,tomatch) =
postprocess_dependencies !(pb.evdref) depstocheck
brvals pb.tomatch pb.pred deps cstrs in
let brvals = Array.map (fun (sign,body) ->
- let sign = List.map (map_name (ltac_interp_name pb.lvar)) sign in
it_mkLambda_or_LetIn body sign) brvals in
let (pred,typ) =
- find_predicate pb.caseloc pb.env pb.evdref
+ find_predicate pb.caseloc pb.env pb.evdref
pred current indt (names,dep) tomatch in
- let ci = make_case_info pb.env (fst mind) pb.casestyle in
- let pred = nf_betaiota pb.env !(pb.evdref) pred in
+ let ci = make_case_info !!(pb.env) (fst mind) pb.casestyle in
+ let pred = nf_betaiota !!(pb.env) !(pb.evdref) pred in
let case =
- make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals
+ make_case_or_project !!(pb.env) !(pb.evdref) indf ci pred current brvals
in
- let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in
- Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
+ let _ = Evarutil.evd_comb1 (Typing.type_of !!(pb.env)) pb.evdref pred in
+ Typing.check_allowed_sort !!(pb.env) !(pb.evdref) mind current pred;
{ uj_val = applist (case, inst);
uj_type = prod_applist !(pb.evdref) typ inst }
@@ -1444,14 +1448,15 @@ and match_current pb (initial,tomatch) =
and shift_problem ((current,t),_,na) pb =
let ty = type_of_tomatch t in
let tomatch = lift_tomatch_stack 1 pb.tomatch in
- let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
+ let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
+ let env = Name.fold_left (fun env id -> hide_variable env Anonymous id) pb.env na in
let pb =
{ pb with
- env = push_rel (LocalDef (na,current,ty)) pb.env;
+ env = snd (push_rel !(pb.evdref) (LocalDef (na,current,ty)) env);
tomatch = tomatch;
pred = lift_predicate 1 pred tomatch;
history = pop_history pb.history;
- mat = List.map (push_current_pattern (current,ty)) pb.mat } in
+ mat = List.map (push_current_pattern !(pb.evdref) (current,ty)) pb.mat } in
let j = compile pb in
{ uj_val = subst1 current j.uj_val;
uj_type = subst1 current j.uj_type }
@@ -1461,7 +1466,7 @@ and shift_problem ((current,t),_,na) pb =
are already introduced in the context, we avoid creating aliases to
themselves by treating this case specially. *)
and pop_problem ((current,t),_,na) pb =
- let pred = specialize_predicate_var (current,t,na) pb.env pb.tomatch pb.pred in
+ let pred = specialize_predicate_var (current,t,na) !!(pb.env) pb.tomatch pb.pred in
let pb =
{ pb with
pred = pred;
@@ -1483,9 +1488,9 @@ and compile_branch initial current realargs names deps pb arsign eqns cstr =
and compile_generalization pb i d rest =
let pb =
{ pb with
- env = push_rel d pb.env;
+ env = snd (push_rel !(pb.evdref) d pb.env);
tomatch = rest;
- mat = List.map (push_generalized_decl_eqn pb.env i d) pb.mat } in
+ mat = List.map (push_generalized_decl_eqn pb.env !(pb.evdref) i d) pb.mat } in
let j = compile pb in
{ uj_val = mkLambda_or_LetIn d j.uj_val;
uj_type = mkProd_wo_LetIn d j.uj_type }
@@ -1498,11 +1503,11 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
let alias = LocalDef (na,c,t) in
let pb =
{ pb with
- env = push_rel alias pb.env;
+ env = snd (push_rel !(pb.evdref) alias pb.env);
tomatch = lift_tomatch_stack 1 rest;
pred = lift_predicate 1 pb.pred pb.tomatch;
history = pop_history_pattern pb.history;
- mat = List.map (push_alias_eqn alias) pb.mat } in
+ mat = List.map (push_alias_eqn !(pb.evdref) alias) pb.mat } in
let j = compile pb in
let sigma = !(pb.evdref) in
{ uj_val =
@@ -1534,7 +1539,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
if not (Flags.is_program_mode ()) && (isRel sigma orig || isVar sigma orig) then
(* Try to compile first using non expanded alias *)
try
- if initial then f orig (Retyping.get_type_of pb.env sigma orig)
+ if initial then f orig (Retyping.get_type_of !!(pb.env) sigma orig)
else just_pop ()
with e when precatchable_exception e ->
(* Try then to compile using expanded alias *)
@@ -1549,7 +1554,7 @@ and compile_alias initial pb (na,orig,(expanded,expanded_typ)) rest =
(* Could be needed in case of a recursive call which requires to
be on a variable for size reasons *)
pb.evdref := sigma;
- if initial then f orig (Retyping.get_type_of pb.env !(pb.evdref) orig)
+ if initial then f orig (Retyping.get_type_of !!(pb.env) !(pb.evdref) orig)
else just_pop ()
@@ -1573,7 +1578,7 @@ substituer après par les initiaux *)
* Syntactic correctness has already been done in constrintern *)
let matx_of_eqns env eqns =
let build_eqn {CAst.loc;v=(ids,initial_lpat,initial_rhs)} =
- let avoid = ids_of_named_context_val (named_context_val env) in
+ let avoid = ids_of_named_context_val (named_context_val !!env) in
let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in
let rhs =
{ rhs_env = env;
@@ -1616,8 +1621,8 @@ let matx_of_eqns env eqns =
*)
let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
- let n = Context.Rel.length (rel_context env) in
- let n' = Context.Rel.length (rel_context extenv) in
+ let n = Context.Rel.length (rel_context !!env) in
+ let n' = Context.Rel.length (rel_context !!extenv) in
(* We first remove the bindings that are dependently typed (they are
difficult to manage and it is not sure these are so useful in practice);
Notes:
@@ -1630,22 +1635,22 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t =
(* d1 ... dn dn+1 ... dn'-p+1 ... dn' *)
(* \--env-/ (= x:ty) *)
(* \--------------extenv------------/ *)
- let (p, _, _) = lookup_rel_id x (rel_context extenv) in
+ let (p, _, _) = lookup_rel_id x (rel_context !!extenv) in
let rec traverse_local_defs p =
- match lookup_rel p extenv with
+ match lookup_rel p !!extenv with
| LocalDef (_,c,_) -> assert (isRel sigma c); traverse_local_defs (p + destRel sigma c)
| LocalAssum _ -> p in
let p = traverse_local_defs p in
let u = lift (n' - n) u in
- try Some (p, u, expand_vars_in_term extenv sigma u)
+ try Some (p, u, expand_vars_in_term !!extenv sigma u)
(* pedrot: does this really happen to raise [Failure _]? *)
with Failure _ -> None in
let subst0 = List.map_filter map subst in
let t0 = lift (n' - n) t in
(subst0, t0)
-let push_binder d (k,env,subst) =
- (k+1,push_rel d env,List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
+let push_binder sigma d (k,env,subst) =
+ (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst)
let rec list_assoc_in_triple x = function
[] -> raise Not_found
@@ -1667,7 +1672,7 @@ let rec list_assoc_in_triple x = function
*)
let abstract_tycon ?loc env evdref subst tycon extenv t =
- let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*)
+ let t = nf_betaiota !!env !evdref t in (* it helps in some cases to remove K-redex*)
let src = match EConstr.kind !evdref t with
| Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk))
| _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in
@@ -1679,31 +1684,31 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
convertible subterms of the substitution *)
let rec aux (k,env,subst as x) t =
match EConstr.kind !evdref t with
- | Rel n when is_local_def (lookup_rel n env) -> t
+ | Rel n when is_local_def (lookup_rel n !!env) -> t
| Evar ev ->
- let ty = get_type_of env !evdref t in
- let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in
+ let ty = get_type_of !!env !evdref t in
+ let ty = Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty in
let inst =
List.map_i
(fun i _ ->
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
- 1 (rel_context env) in
- let ev' = evd_comb1 (Evarutil.new_evar env ~src) evdref ty in
- begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
+ 1 (rel_context !!env) in
+ let ev' = evd_comb1 (Evarutil.new_evar !!env ~src) evdref ty in
+ begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env !evdref (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
end;
ev'
| _ ->
- let good = List.filter (fun (_,u,_) -> is_conv_leq env !evdref t u) subst in
+ let good = List.filter (fun (_,u,_) -> is_conv_leq !!env !evdref t u) subst in
match good with
| [] ->
- map_constr_with_full_binders !evdref push_binder aux x t
+ map_constr_with_full_binders !evdref (push_binder !evdref) aux x t
| (_, _, u) :: _ -> (* u is in extenv *)
let vl = List.map pi1 good in
let ty =
- let ty = get_type_of env !evdref t in
- Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty
+ let ty = get_type_of !!env !evdref t in
+ Evarutil.evd_comb1 (refresh_universes (Some false) !!env) evdref ty
in
let dummy_subst = List.init k (fun _ -> mkProp) in
let ty = substl dummy_subst (aux x ty) in
@@ -1711,7 +1716,7 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
let inst =
List.map_i
(fun i _ -> if Int.List.mem i vl then u else mkRel i) 1
- (rel_context extenv) in
+ (rel_context !!extenv) in
let map a = match EConstr.kind !evdref a with
| Rel n -> not (noccurn !evdref n u) || Int.Set.mem n depvl
| _ -> true
@@ -1719,10 +1724,10 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
let rel_filter = List.map map inst in
let named_filter =
List.map (fun d -> local_occur_var !evdref (NamedDecl.get_id d) u)
- (named_context extenv) in
+ (named_context !!extenv) in
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = u :: List.map mkRel vl in
- let ev = evd_comb1 (Evarutil.new_evar extenv ~src ~filter ~candidates) evdref ty in
+ let ev = evd_comb1 (Evarutil.new_evar !!extenv ~src ~filter ~candidates) evdref ty in
lift k ev
in
aux (0,extenv,subst0) t0
@@ -1732,19 +1737,19 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
| None ->
(* This is the situation we are building a return predicate and
we are in an impossible branch *)
- let n = Context.Rel.length (rel_context env) in
- let n' = Context.Rel.length (rel_context tycon_env) in
+ let n = Context.Rel.length (rel_context !!env) in
+ let n' = Context.Rel.length (rel_context !!tycon_env) in
let impossible_case_type, u =
evd_comb1
- (new_type_evar (reset_context env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase))
+ (new_type_evar (reset_context !!env) ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase))
evdref univ_flexible_alg
in
(lift (n'-n) impossible_case_type, mkSort u)
| Some t ->
let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
- let tt = evd_comb1 (Typing.type_of extenv) evdref t in
+ let tt = evd_comb1 (Typing.type_of !!extenv) evdref t in
(t,tt) in
- match cumul env !evdref tt (mkSort s) with
+ match cumul !!env !evdref tt (mkSort s) with
| None -> anomaly (Pp.str "Build_tycon: should be a type.");
| Some sigma -> evdref := sigma;
{ uj_val = t; uj_type = tt }
@@ -1761,14 +1766,14 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
let build_inversion_problem loc env sigma tms t =
let make_patvar t (subst,avoid) =
- let id = next_name_away (named_hd env sigma t Anonymous) avoid in
+ let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in
DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in
let rec reveal_pattern t (subst,avoid as acc) =
- match EConstr.kind sigma (whd_all env sigma t) with
+ match EConstr.kind sigma (whd_all !!env sigma t) with
| Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
| App (f,v) when isConstruct sigma f ->
let cstr,u = destConstruct sigma f in
- let n = constructor_nrealargs_env env cstr in
+ let n = constructor_nrealargs_env !!env cstr in
let l = List.lastn n (Array.to_list v) in
let l,acc = List.fold_right_map reveal_pattern l acc in
DAst.make (PatCstr (cstr,l,Anonymous)), acc
@@ -1780,19 +1785,19 @@ let build_inversion_problem loc env sigma tms t =
let patl,acc = List.fold_right_map reveal_pattern realargs acc in
let pat,acc = make_patvar t acc in
let indf' = lift_inductive_family n indf in
- let sign = make_arity_signature env sigma true indf' in
+ let sign = make_arity_signature !!env sigma true indf' in
let patl = pat :: List.rev patl in
- let patl,sign = recover_and_adjust_alias_names patl sign in
+ let patl,sign = recover_and_adjust_alias_names acc patl sign in
let p = List.length patl in
- let env' = push_rel_context sign env in
+ let _,env' = push_rel_context sigma sign env in
let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in
List.rev_append patl patl',acc_sign,acc
| (t, NotInd (bo,typ)) :: tms ->
let pat,acc = make_patvar t acc in
let d = LocalAssum (alias_of_pat pat,typ) in
- let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
+ let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in
pat::patl,acc_sign,acc in
- let avoid0 = vars_of_env env in
+ let avoid0 = GlobEnv.vars_of_env env in
(* [patl] is a list of patterns revealing the substructure of
constructors present in the constraints on the type of the
multiple terms t1..tn that are matched in the original problem;
@@ -1808,9 +1813,9 @@ let build_inversion_problem loc env sigma tms t =
let decls =
List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in
- let pb_env = push_rel_context sign env in
+ let _,pb_env = push_rel_context sigma sign env in
let decls =
- List.map (fun (c,d) -> (c,extract_inductive_data pb_env sigma d,d)) decls in
+ List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in
let decls = List.rev decls in
let dep_sign = find_dependencies_signature sigma (List.make n true) decls in
@@ -1843,7 +1848,7 @@ let build_inversion_problem loc env sigma tms t =
constraints are incompatible with the constraints on the
inductive types of the multiple terms matched in Xi *)
let catch_all_eqn =
- if List.for_all (irrefutable env) patl then
+ if List.for_all (irrefutable !!env) patl then
(* No need for a catch all clause *)
[]
else
@@ -1857,13 +1862,12 @@ let build_inversion_problem loc env sigma tms t =
it = None } } ] in
(* [pb] is the auxiliary pattern-matching serving as skeleton for the
return type of the original problem Xi *)
- let s' = Retyping.get_sort_of env sigma t in
+ let s' = Retyping.get_sort_of !!env sigma t in
let sigma, s = Evd.new_sort_variable univ_flexible sigma in
- let sigma = Evd.set_leq_sort env sigma s' s in
+ let sigma = Evd.set_leq_sort !!env sigma s' s in
let evdref = ref sigma in
let pb =
{ env = pb_env;
- lvar = empty_lvar;
evdref = evdref;
pred = (*ty *) mkSort s;
tomatch = sub_tms;
@@ -1878,16 +1882,16 @@ let build_inversion_problem loc env sigma tms t =
(* Here, [pred] is assumed to be in the context built from all *)
(* realargs and terms to match *)
let build_initial_predicate arsign pred =
- let rec buildrec n pred tmnames = function
+ let rec buildrec pred tmnames = function
| [] -> List.rev tmnames,pred
| (decl::realdecls)::lnames ->
let na = RelDecl.get_name decl in
- let n' = n + List.length realdecls in
- buildrec (n'+1) pred (force_name na::tmnames) lnames
+ let realnames = List.map RelDecl.get_name realdecls in
+ buildrec pred ((force_name na,realnames)::tmnames) lnames
| _ -> assert false
- in buildrec 0 pred [] (List.rev arsign)
+ in buildrec pred [] (List.rev arsign)
-let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
+let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
let lift = if dolift then lift else fun n t -> t in
let get_one_sign n tm (na,t) =
match tm with
@@ -1895,7 +1899,7 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
(match t with
| None -> let sign = match bo with
| None -> [LocalAssum (na, lift n typ)]
- | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign,sign
+ | Some b -> [LocalDef (na, lift n b, lift n typ)] in sign
| Some {CAst.loc} ->
user_err ?loc
(str"Unexpected type annotation for a term of non inductive type."))
@@ -1905,31 +1909,23 @@ let extract_arity_signature ?(dolift=true) env0 lvar tomatchl tmsign =
let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in
let arsign = fst (get_arity env0 indf') in
let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
- let realnal, realnal' =
+ let realnal =
match t with
| Some {CAst.loc;v=(ind',realnal)} ->
if not (eq_ind ind ind') then
user_err ?loc (str "Wrong inductive type.");
if not (Int.equal nrealargs_ctxt (List.length realnal)) then
anomaly (Pp.str "Ill-formed 'in' clause in cases.");
- let realnal = List.rev realnal in
- let realnal' = List.map (ltac_interp_name lvar) realnal in
- realnal,realnal'
+ List.rev realnal
| None ->
- let realnal = List.make nrealargs_ctxt Anonymous in
- realnal, realnal in
- let na' = ltac_interp_name lvar na in
+ List.make nrealargs_ctxt Anonymous in
let t = EConstr.of_constr (build_dependent_inductive env0 indf') in
- (* Context with names for typing *)
- let arsign1 = LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in
- (* Context with names for building the term *)
- let arsign2 = LocalAssum (na', t) :: List.map2 RelDecl.set_name realnal' arsign in
- arsign1,arsign2 in
+ LocalAssum (na, t) :: List.map2 RelDecl.set_name realnal arsign in
let rec buildrec n = function
| [],[] -> []
| (_,tm)::ltm, (_,x)::tmsign ->
let l = get_one_sign n tm x in
- l :: buildrec (n + List.length (fst l)) (ltm,tmsign)
+ l :: buildrec (n + List.length l) (ltm,tmsign)
| _ -> assert false
in List.rev (buildrec 0 (tomatchl,tmsign))
@@ -1986,9 +1982,9 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
in
assert (len == 0);
let p = predicate 0 c in
- let env' = List.fold_right push_rel_context arsign env in
- try let sigma' = fst (Typing.type_of env' sigma p) in
- Some (sigma', p)
+ let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in
+ try let sigma' = fst (Typing.type_of !!env' sigma p) in
+ Some (sigma', p, arsign)
with e when precatchable_exception e -> None
(* Builds the predicate. If the predicate is dependent, its context is
@@ -2017,15 +2013,14 @@ let noccur_with_meta sigma n m term =
in
try (occur_rec n term; true) with LocalOccur -> false
-let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred =
+let prepare_predicate ?loc typing_fun env sigma tomatchs arsign tycon pred =
let refresh_tycon sigma t =
(** If we put the typing constraint in the term, it has to be
refreshed to preserve the invariant that no algebraic universe
can appear in the term. *)
refresh_universes ~status:Evd.univ_flexible ~onlyalg:true (Some true)
- env sigma t
+ !!env sigma t
in
- let typing_arsign,building_arsign = List.split arsign in
let preds =
match pred, tycon with
(* No return clause *)
@@ -2035,12 +2030,12 @@ let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred
(* First strategy: we abstract the tycon wrt to the dependencies *)
let sigma, t = refresh_tycon sigma t in
let p1 =
- prepare_predicate_from_arsign_tycon env sigma loc tomatchs typing_arsign t in
+ prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
(* Second strategy: we build an "inversion" predicate *)
let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
(match p1 with
- | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
- | None -> [sigma2, pred2])
+ | Some (sigma1,pred1,arsign) -> [sigma1, pred1, arsign; sigma2, pred2, arsign]
+ | None -> [sigma2, pred2, arsign])
| None, _ ->
(* No dependent type constraint, or no constraints at all: *)
(* we use two strategies *)
@@ -2048,28 +2043,28 @@ let prepare_predicate ?loc typing_fun env sigma lvar tomatchs arsign tycon pred
| Some t -> refresh_tycon sigma t
| None ->
let (sigma, (t, _)) =
- new_type_evar env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
+ new_type_evar !!env sigma univ_flexible_alg ~src:(Loc.tag ?loc @@ Evar_kinds.CasesType false) in
sigma, t
in
(* First strategy: we build an "inversion" predicate *)
let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
(* Second strategy: we directly use the evar as a non dependent pred *)
- let pred2 = lift (List.length (List.flatten typing_arsign)) t in
- [sigma1, pred1; sigma, pred2]
+ let pred2 = lift (List.length (List.flatten arsign)) t in
+ [sigma1, pred1, arsign; sigma, pred2, arsign]
(* Some type annotation *)
| Some rtntyp, _ ->
(* We extract the signature of the arity *)
- let envar = List.fold_right push_rel_context typing_arsign env in
+ let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in
let sigma, newt = new_sort_variable univ_flexible_alg sigma in
let evdref = ref sigma in
- let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref lvar rtntyp in
+ let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
let sigma = !evdref in
let predccl = nf_evar sigma predcclj.uj_val in
- [sigma, predccl]
+ [sigma, predccl, building_arsign]
in
List.map
- (fun (sigma,pred) ->
- let (nal,pred) = build_initial_predicate building_arsign pred in
+ (fun (sigma,pred,arsign) ->
+ let (nal,pred) = build_initial_predicate arsign pred in
sigma,nal,pred)
preds
@@ -2152,7 +2147,7 @@ let constr_of_pat env evdref arsign pat avoid =
typ env (substl args liftt, []) ua avoid
in
let args' = arg' :: List.map (lift n') args in
- let env' = push_rel_context sign' env in
+ let env' = EConstr.push_rel_context sign' env in
(pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
in
@@ -2172,8 +2167,8 @@ let constr_of_pat env evdref arsign pat avoid =
let avoid = Id.Set.add id avoid in
let sign, i, avoid =
try
- let env = push_rel_context sign env in
- evdref := the_conv_x_leq (push_rel_context sign env)
+ let env = EConstr.push_rel_context sign env in
+ evdref := the_conv_x_leq (EConstr.push_rel_context sign env)
(lift (succ m) ty) (lift 1 apptype) !evdref;
let eq_t = mk_eq evdref (lift (succ m) ty)
(mkRel 1) (* alias *)
@@ -2240,7 +2235,6 @@ let lift_rel_context n l =
full signature. However prevpatterns are in the original one signature per pattern form.
*)
let build_ineqs evdref prevpatterns pats liftsign =
- let _tomatchs = List.length pats in
let diffs =
List.fold_left
(fun c eqnpats ->
@@ -2288,7 +2282,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
let _, newpatterns, pats =
List.fold_left2
(fun (idents, newpatterns, pats) pat arsign ->
- let pat', cpat, idents = constr_of_pat env evdref arsign pat idents in
+ let pat', cpat, idents = constr_of_pat !!env evdref arsign pat idents in
(idents, pat' :: newpatterns, cpat :: pats))
(Id.Set.empty, [], []) eqn.patterns sign
in
@@ -2315,7 +2309,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
in
let ineqs = build_ineqs evdref prevpatterns pats signlen in
let rhs_rels' = rels_of_patsign !evdref rhs_rels in
- let _signenv = push_rel_context rhs_rels' env in
+ let _signenv,_ = push_rel_context !evdref rhs_rels' env in
let arity =
let args, nargs =
List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
@@ -2335,11 +2329,11 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
let eqs_rels, arity = decompose_prod_n_assum !evdref neqs arity in
eqs_rels @ neqs_rels @ rhs_rels', arity
in
- let rhs_env = push_rel_context rhs_rels' env in
+ let _,rhs_env = push_rel_context !evdref rhs_rels' env in
let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
- let _btype = evd_comb1 (Typing.type_of env) evdref bbody in
+ let _btype = evd_comb1 (Typing.type_of !!env) evdref bbody in
let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
let branch =
@@ -2492,10 +2486,10 @@ let context_of_arsign l =
l ([], 0)
in x
-let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
+let compile_program_cases ?loc style (typing_function, evdref) tycon env
(predopt, tomatchl, eqns) =
let typing_fun tycon env = function
- | Some t -> typing_function tycon env evdref lvar t
+ | Some t -> typing_function tycon env evdref t
| None -> Evarutil.evd_comb0 use_unit_judge evdref in
(* We build the matrix of patterns and right-hand side *)
@@ -2503,29 +2497,28 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
(* We build the vector of terms to match consistently with the *)
(* constructors found in patterns *)
- let predlvar,tomatchs = coerce_to_indtype typing_function evdref env lvar matx tomatchl in
+ let env,tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in
let tycon = valcon_of_tycon tycon in
let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env !evdref tomatchs tycon in
- let env = push_rel_context tomatchs_lets env in
+ let _,env = push_rel_context !evdref tomatchs_lets env in
let len = List.length eqns in
let sign, allnames, signlen, eqs, neqs, args =
(* The arity signature *)
- let arsign = extract_arity_signature ~dolift:false env predlvar tomatchs tomatchl in
- let arsign = List.map fst arsign in (* Because no difference between the arity for typing and the arity for building *)
+ let arsign = extract_arity_signature ~dolift:false !!env tomatchs tomatchl in
(* Build the dependent arity signature, the equalities which makes
the first part of the predicate and their instantiations. *)
let avoid = Id.Set.empty in
- build_dependent_signature env evdref avoid tomatchs arsign
+ build_dependent_signature !!env evdref avoid tomatchs arsign
in
let tycon, arity =
let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
match tycon' with
- | None -> let ev = mkExistential env evdref in ev, lift nar ev
+ | None -> let ev = mkExistential !!env evdref in ev, lift nar ev
| Some t ->
let pred =
match prepare_predicate_from_arsign_tycon env !evdref loc tomatchs sign t with
- | Some (evd, pred) -> evdref := evd; pred
+ | Some (evd, pred, arsign) -> evdref := evd; pred
| None ->
lift nar t
in Option.get tycon, pred
@@ -2541,7 +2534,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
in
let matx = List.rev matx in
let _ = assert (Int.equal len (List.length lets)) in
- let env = push_rel_context lets env in
+ let _,env = push_rel_context !evdref lets env in
let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
let args = List.rev_map (lift len) args in
@@ -2554,10 +2547,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t)
| NotInd (Some b, t) -> LocalDef (na,b,t)
| IsInd (typ,_,_) -> LocalAssum (na,typ) in
- let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
+ let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
let typs =
- List.map (fun (c,d) -> (c,extract_inductive_data env !evdref d,d)) typs in
+ List.map (fun (c,d) -> (c,extract_inductive_data !!env !evdref d,d)) typs in
let dep_sign =
find_dependencies_signature !evdref
@@ -2566,20 +2559,20 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let typs' =
List.map3
- (fun (tm,tmt) deps na ->
+ (fun (tm,tmt) deps (na,realnames) ->
let deps = if not (isRel !evdref tm) then [] else deps in
+ let tmt = set_tomatch_realnames realnames tmt in
((tm,tmt),deps,na))
tomatchs dep_sign nal in
let initial_pushed = List.map (fun x -> Pushed (true,x)) typs' in
let typing_function tycon env evdref = function
- | Some t -> typing_function tycon env evdref lvar t
+ | Some t -> typing_function tycon env evdref t
| None -> evd_comb0 use_unit_judge evdref in
let pb =
{ env = env;
- lvar = lvar;
evdref = evdref;
pred = pred;
tomatch = initial_pushed;
@@ -2591,7 +2584,7 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let j = compile pb in
(* We check for unused patterns *)
- List.iter (check_unused_pattern env) matx;
+ List.iter (check_unused_pattern !!env) matx;
let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
@@ -2602,10 +2595,10 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
(**************************************************************************)
(* Main entry of the matching compilation *)
-let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomatchl, eqns) =
+let compile_cases ?loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
if predopt == None && Flags.is_program_mode () && Program.is_program_cases () then
compile_program_cases ?loc style (typing_fun, evdref)
- tycon env lvar (predopt, tomatchl, eqns)
+ tycon env (predopt, tomatchl, eqns)
else
(* We build the matrix of patterns and right-hand side *)
@@ -2613,15 +2606,13 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
(* We build the vector of terms to match consistently with the *)
(* constructors found in patterns *)
- let predlvar,tomatchs = coerce_to_indtype typing_fun evdref env lvar matx tomatchl in
-
-
+ let predenv,tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
(* If an elimination predicate is provided, we check it is compatible
with the type of arguments to match; if none is provided, we
build alternative possible predicates *)
- let arsign = extract_arity_signature env predlvar tomatchs tomatchl in
- let preds = prepare_predicate ?loc typing_fun env !evdref predlvar tomatchs arsign tycon predopt in
+ let arsign = extract_arity_signature !!env tomatchs tomatchl in
+ let preds = prepare_predicate ?loc typing_fun predenv !evdref tomatchs arsign tycon predopt in
let compile_for_one_predicate (sigma,nal,pred) =
(* We push the initial terms to match and push their alias to rhs' envs *)
@@ -2631,10 +2622,10 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
let out_tmt na = function NotInd (None,t) -> LocalAssum (na,t)
| NotInd (Some b,t) -> LocalDef (na,b,t)
| IsInd (typ,_,_) -> LocalAssum (na,typ) in
- let typs = List.map2 (fun na (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
+ let typs = List.map2 (fun (na,_) (tm,tmt) -> (tm,out_tmt na tmt)) nal tomatchs in
let typs =
- List.map (fun (c,d) -> (c,extract_inductive_data env sigma d,d)) typs in
+ List.map (fun (c,d) -> (c,extract_inductive_data !!env sigma d,d)) typs in
let dep_sign =
find_dependencies_signature !evdref
@@ -2643,8 +2634,9 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
let typs' =
List.map3
- (fun (tm,tmt) deps na ->
+ (fun (tm,tmt) deps (na,realnames) ->
let deps = if not (isRel !evdref tm) then [] else deps in
+ let tmt = set_tomatch_realnames realnames tmt in
((tm,tmt),deps,na))
tomatchs dep_sign nal in
@@ -2652,14 +2644,13 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
(* A typing function that provides with a canonical term for absurd cases*)
let typing_fun tycon env evdref = function
- | Some t -> typing_fun tycon env evdref lvar t
+ | Some t -> typing_fun tycon env evdref t
| None -> evd_comb0 use_unit_judge evdref in
let myevdref = ref sigma in
let pb =
{ env = env;
- lvar = lvar;
evdref = myevdref;
pred = pred;
tomatch = initial_pushed;
@@ -2672,7 +2663,7 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
let j = compile pb in
(* We coerce to the tycon (if an elim predicate was provided) *)
- let j = inh_conv_coerce_to_tycon ?loc env myevdref j tycon in
+ let j = inh_conv_coerce_to_tycon ?loc !!env myevdref j tycon in
evdref := !myevdref;
j in
@@ -2681,6 +2672,6 @@ let compile_cases ?loc style (typing_fun, evdref) tycon env lvar (predopt, tomat
let j = list_try_compile compile_for_one_predicate preds in
(* We check for unused patterns *)
- List.iter (check_unused_pattern env) matx;
+ List.iter (check_unused_pattern !!env) matx;
j
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 04a3464679..76b81a58c1 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -15,7 +15,6 @@ open Environ
open EConstr
open Inductiveops
open Glob_term
-open Ltac_pretype
open Evardefine
(** {5 Compilation of pattern-matching } *)
@@ -42,9 +41,9 @@ val irrefutable : env -> cases_pattern -> bool
val compile_cases :
?loc:Loc.t -> case_style ->
- (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref ->
+ (type_constraint -> GlobEnv.t -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
type_constraint ->
- env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses ->
+ GlobEnv.t -> glob_constr option * tomatch_tuples * cases_clauses ->
unsafe_judgment
val constr_of_pat :
@@ -59,7 +58,7 @@ val constr_of_pat :
Names.Id.Set.t
type 'a rhs =
- { rhs_env : env;
+ { rhs_env : GlobEnv.t;
rhs_vars : Id.Set.t;
avoid_ids : Id.Set.t;
it : 'a option}
@@ -103,8 +102,7 @@ and pattern_continuation =
| Result of cases_pattern list
type 'a pattern_matching_problem =
- { env : env;
- lvar : Ltac_pretype.ltac_var_map;
+ { env : GlobEnv.t;
evdref : evar_map ref;
pred : constr;
tomatch : tomatch_stack;
@@ -112,21 +110,19 @@ type 'a pattern_matching_problem =
mat : 'a matrix;
caseloc : Loc.t option;
casestyle : case_style;
- typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
-
+ typing_function: type_constraint -> GlobEnv.t -> evar_map ref -> 'a option -> unsafe_judgment }
val compile : 'a pattern_matching_problem -> unsafe_judgment
val prepare_predicate : ?loc:Loc.t ->
(type_constraint ->
- Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
- Environ.env ->
+ GlobEnv.t -> Evd.evar_map ref -> glob_constr -> unsafe_judgment) ->
+ GlobEnv.t ->
Evd.evar_map ->
- Ltac_pretype.ltac_var_map ->
(types * tomatch_type) list ->
- (rel_context * rel_context) list ->
+ rel_context list ->
constr option ->
- glob_constr option -> (Evd.evar_map * Name.t list * constr) list
+ glob_constr option -> (Evd.evar_map * (Name.t * Name.t list) list * constr) list
-val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t ->
- Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
+val make_return_predicate_ltac_lvar : GlobEnv.t -> Evd.evar_map -> Name.t ->
+ Glob_term.glob_constr -> constr -> GlobEnv.t
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 542fb5456c..94da51626f 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -16,7 +16,6 @@ open Constr
open Libnames
open Globnames
open Nametab
-open Environ
open Libobject
open Mod_subst
@@ -39,7 +38,7 @@ type cl_info_typ = {
type coe_typ = GlobRef.t
-module CoeTypMap = Refmap_env
+module CoeTypMap = GlobRef.Map_env
type coe_info_typ = {
coe_value : GlobRef.t;
@@ -118,6 +117,9 @@ let class_tab =
let coercion_tab =
ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
+let coercions_in_scope =
+ ref GlobRef.Set_env.empty
+
module ClPairOrd =
struct
type t = cl_index * cl_index
@@ -131,12 +133,13 @@ module ClPairMap = Map.Make(ClPairOrd)
let inheritance_graph =
ref (ClPairMap.empty : inheritance_path ClPairMap.t)
-let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)
+let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope)
-let unfreeze (fcl,fco,fig) =
+let unfreeze (fcl,fco,fig,in_scope) =
class_tab:=fcl;
coercion_tab:=fco;
- inheritance_graph:=fig
+ inheritance_graph:=fig;
+ coercions_in_scope:=in_scope
(* ajout de nouveaux "objets" *)
@@ -316,16 +319,16 @@ let lookup_pattern_path_between env (s,t) =
(* rajouter une coercion dans le graphe *)
-let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
- ref (fun _ _ _ -> str "<a class path>")
+let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
+ ref (fun _ -> str "<a class path>")
let install_path_printer f = path_printer := f
-let print_path env sigma x = !path_printer env sigma x
+let print_path x = !path_printer x
-let message_ambig env sigma l =
+let message_ambig l =
str"Ambiguous paths:" ++ spc () ++
- prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l
+ prlist_with_sep fnl print_path l
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
@@ -339,7 +342,7 @@ let different_class_params i =
| CL_CONST c -> Global.is_polymorphic (ConstRef c)
| _ -> false
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph (ic,source,target) =
let old_inheritance_graph = !inheritance_graph in
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
@@ -381,7 +384,7 @@ let add_coercion_in_graph env sigma (ic,source,target) =
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
if is_ambig && not !Flags.quiet then
- Feedback.msg_info (message_ambig env sigma !ambig_paths)
+ Feedback.msg_info (message_ambig !ambig_paths)
type coercion = {
coercion_type : coe_typ;
@@ -426,7 +429,7 @@ let _ =
optread = (fun () -> !automatically_import_coercions);
optwrite = (:=) automatically_import_coercions }
-let cache_coercion env sigma (_, c) =
+let cache_coercion (_, c) =
let () = add_class c.coercion_source in
let () = add_class c.coercion_target in
let is, _ = class_info c.coercion_source in
@@ -439,15 +442,22 @@ let cache_coercion env sigma (_, c) =
coe_param = c.coercion_params;
} in
let () = add_new_coercion c.coercion_type xf in
- add_coercion_in_graph env sigma (xf,is,it)
+ add_coercion_in_graph (xf,is,it)
let load_coercion _ o =
if !automatically_import_coercions then
- cache_coercion (Global.env ()) Evd.empty o
+ cache_coercion o
+
+let set_coercion_in_scope (_, c) =
+ let r = c.coercion_type in
+ coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope
let open_coercion i o =
- if Int.equal i 1 && not !automatically_import_coercions then
- cache_coercion (Global.env ()) Evd.empty o
+ if Int.equal i 1 then begin
+ set_coercion_in_scope o;
+ if not !automatically_import_coercions then
+ cache_coercion o
+ end
let subst_coercion (subst, c) =
let coe = subst_coe_typ subst c.coercion_type in
@@ -492,8 +502,8 @@ let inCoercion : coercion -> obj =
open_function = open_coercion;
load_function = load_coercion;
cache_function = (fun objn ->
- let env = Global.env () in cache_coercion env Evd.empty objn
- );
+ set_coercion_in_scope objn;
+ cache_coercion objn);
subst_function = subst_coercion;
classify_function = classify_coercion;
discharge_function = discharge_coercion }
@@ -535,7 +545,7 @@ let coercion_of_reference r =
module CoercionPrinting =
struct
type t = coe_typ
- let compare = RefOrdered.compare
+ let compare = GlobRef.Ordered.compare
let encode = coercion_of_reference
let subst = subst_coe_typ
let printer x = pr_global_env Id.Set.empty x
@@ -553,3 +563,6 @@ let hide_coercion coe =
let coe_info = coercion_info coe in
Some coe_info.coe_param
else None
+
+let is_coercion_in_scope r =
+ GlobRef.Set_env.mem r !coercions_in_scope
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index af00c0a8dc..7c4842c8ae 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -99,7 +99,7 @@ val lookup_pattern_path_between :
(**/**)
(* Crade *)
val install_path_printer :
- (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+ ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
(**/**)
(** {6 This is for printing purpose } *)
@@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list
(** [hide_coercion] returns the number of params to skip if the coercion must
be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
val hide_coercion : coe_typ -> int option
+
+val is_coercion_in_scope : GlobRef.t -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5e3821edf1..e15c00f7dc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -363,12 +363,20 @@ let saturate_evd env evd =
Typeclasses.resolve_typeclasses
~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
+let warn_coercion_not_in_scope =
+ CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated"
+ Pp.(fun r -> str "Coercion used but not in scope: " ++
+ Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use "
+ ++ str "this coercion, please Import the module that contains it.")
+
(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
try
let j,t,evd =
List.fold_left
(fun (ja,typ_cl,sigma) i ->
+ if not (is_coercion_in_scope i.coe_value) then
+ warn_coercion_not_in_scope i.coe_value;
let isid = i.coe_is_identity in
let isproj = i.coe_is_projection in
let sigma, c = new_global sigma i.coe_value in
@@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl =
(hj,typ_cl,sigma) p
in evd, j
with NoCoercion as e -> raise e
- | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.")
(* Try to coerce to a funclass; raise NoCoercion if not possible *)
let inh_app_fun_core env evd j =
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
new file mode 100644
index 0000000000..12788e5ec5
--- /dev/null
+++ b/pretyping/globEnv.ml
@@ -0,0 +1,201 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Util
+open Pp
+open CErrors
+open Names
+open Environ
+open EConstr
+open Evarutil
+open Termops
+open Vars
+open Ltac_pretype
+
+(** This files provides a level of abstraction for the kind of
+ environment used for type inference (so-called pretyping); in
+ particular:
+ - it supports that term variables can be interpreted as Ltac
+ variables pointing to the effective expected name
+ - it incrementally and lazily computes the renaming of rel
+ variables used to build purely-named evar contexts
+*)
+
+type t = {
+ static_env : env;
+ (** For locating indices *)
+ renamed_env : env;
+ (** For name management *)
+ extra : ext_named_context Lazy.t;
+ (** Delay the computation of the evar extended environment *)
+ lvar : ltac_var_map;
+}
+
+let make env sigma lvar =
+ let get_extra env sigma =
+ let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
+ Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
+ (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
+ {
+ static_env = env;
+ renamed_env = env;
+ extra = lazy (get_extra env sigma);
+ lvar = lvar;
+ }
+
+let env env = env.static_env
+
+let vars_of_env env =
+ Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env)
+
+let ltac_interp_name { ltac_idents ; ltac_genargs } = function
+ | Anonymous -> Anonymous
+ | Name id as na ->
+ try Name (Id.Map.find id ltac_idents)
+ with Not_found ->
+ if Id.Map.mem id ltac_genargs then
+ user_err (str "Ltac variable" ++ spc () ++ Id.print id ++
+ spc () ++ str "is not bound to an identifier." ++
+ spc () ++str "It cannot be used in a binder.")
+ else na
+
+let push_rel sigma d env =
+ let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
+ let env = {
+ static_env = push_rel d env.static_env;
+ renamed_env = push_rel d' env.renamed_env;
+ extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra));
+ lvar = env.lvar;
+ } in
+ d', env
+
+let push_rel_context ?(force_names=false) sigma ctx env =
+ let open Context.Rel.Declaration in
+ let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in
+ let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in
+ let env = {
+ static_env = push_rel_context ctx env.static_env;
+ renamed_env = push_rel_context ctx' env.renamed_env;
+ extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra));
+ lvar = env.lvar;
+ } in
+ ctx', env
+
+let push_rec_types sigma (lna,typarray) env =
+ let open Context.Rel.Declaration in
+ let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
+ let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in
+ Array.map get_name ctx, env
+
+let e_new_evar env evdref ?src ?naming typ =
+ let open Context.Named.Declaration in
+ let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in
+ let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in
+ let (subst, _, nc) = Lazy.force env.extra in
+ let typ' = csubst_subst subst typ in
+ let instance = inst_rels @ inst_vars in
+ let sign = val_of_named_context nc in
+ let sigma = !evdref in
+ let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in
+ evdref := sigma;
+ e
+
+let e_new_type_evar env evdref ~src =
+ let (evd', s) = Evd.new_sort_variable Evd.univ_flexible_alg !evdref in
+ evdref := evd';
+ e_new_evar env evdref ~src (EConstr.mkSort s)
+
+let hide_variable env expansion id =
+ let lvar = env.lvar in
+ if Id.Map.mem id lvar.ltac_genargs then
+ let lvar = match expansion with
+ | Name id' ->
+ (* We are typically in a situation [match id return P with ... end]
+ which we interpret as [match id' as id' return P with ... end],
+ with [P] interpreted in an environment where [id] is bound to [id'].
+ The variable is already bound to [id'], so nothing to do *)
+ lvar
+ | _ ->
+ (* We are typically in a situation [match id return P with ... end]
+ with [id] bound to a non-variable term [c]. We interpret as
+ [match c as id return P with ... end], and hides [id] while
+ interpreting [P], since it has become a binder and cannot be anymore be
+ substituted by a variable coming from the Ltac substitution. *)
+ { lvar with
+ ltac_uconstrs = Id.Map.remove id lvar.ltac_uconstrs;
+ ltac_constrs = Id.Map.remove id lvar.ltac_constrs;
+ ltac_genargs = Id.Map.remove id lvar.ltac_genargs } in
+ { env with lvar }
+ else
+ env
+
+let protected_get_type_of env sigma c =
+ try Retyping.get_type_of ~lax:true env sigma c
+ with Retyping.RetypeError _ ->
+ user_err
+ (str "Cannot reinterpret " ++ quote (print_constr c) ++
+ str " in the current environment.")
+
+let invert_ltac_bound_name env id0 id =
+ try mkRel (pi1 (lookup_rel_id id (rel_context env.static_env)))
+ with Not_found ->
+ user_err (str "Ltac variable " ++ Id.print id0 ++
+ str " depends on pattern variable name " ++ Id.print id ++
+ str " which is not bound in current context.")
+
+let interp_ltac_variable ?loc typing_fun env sigma id =
+ (* Check if [id] is an ltac variable *)
+ try
+ let (ids,c) = Id.Map.find id env.lvar.ltac_constrs in
+ let subst = List.map (invert_ltac_bound_name env id) ids in
+ let c = substl subst c in
+ { uj_val = c; uj_type = protected_get_type_of env.renamed_env sigma c }
+ with Not_found ->
+ try
+ let {closure;term} = Id.Map.find id env.lvar.ltac_uconstrs in
+ let lvar = {
+ ltac_constrs = closure.typed;
+ ltac_uconstrs = closure.untyped;
+ ltac_idents = closure.idents;
+ ltac_genargs = Id.Map.empty; }
+ in
+ (* spiwack: I'm catching [Not_found] potentially too eagerly
+ here, as the call to the main pretyping function is caught
+ inside the try but I want to avoid refactoring this function
+ too much for now. *)
+ typing_fun {env with lvar} term
+ with Not_found ->
+ (* Check if [id] is a ltac variable not bound to a term *)
+ (* and build a nice error message *)
+ if Id.Map.mem id env.lvar.ltac_genargs then begin
+ let Geninterp.Val.Dyn (typ, _) = Id.Map.find id env.lvar.ltac_genargs in
+ user_err ?loc
+ (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \
+ bound to a " ++ Geninterp.Val.pr typ ++ str ".")
+ end;
+ raise Not_found
+
+module ConstrInterpObj =
+struct
+ type ('r, 'g, 't) obj =
+ unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+ let name = "constr_interp"
+ let default _ = None
+end
+
+module ConstrInterp = Genarg.Register(ConstrInterpObj)
+
+let register_constr_interp0 = ConstrInterp.register0
+
+let interp_glob_genarg env sigma ty arg =
+ let open Genarg in
+ let GenArg (Glbwit tag, arg) = arg in
+ let interp = ConstrInterp.obj tag in
+ interp env.lvar.ltac_genargs env.renamed_env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
new file mode 100644
index 0000000000..4038523211
--- /dev/null
+++ b/pretyping/globEnv.mli
@@ -0,0 +1,83 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Names
+open Environ
+open Evd
+open EConstr
+open Ltac_pretype
+
+(** To embed constr in glob_constr *)
+
+val register_constr_interp0 :
+ ('r, 'g, 't) Genarg.genarg_type ->
+ (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+
+(** {6 Pretyping name management} *)
+
+(** The following provides a level of abstraction for the kind of
+ environment used for type inference (so-called pretyping); in
+ particular:
+ - it supports that term variables can be interpreted as Ltac
+ variables pointing to the effective expected name
+ - it incrementally and lazily computes the renaming of rel
+ variables used to build purely-named evar contexts
+*)
+
+(** Type of environment extended with naming and ltac interpretation data *)
+
+type t
+
+(** Build a pretyping environment from an ltac environment *)
+
+val make : env -> evar_map -> ltac_var_map -> t
+
+(** Export the underlying environement *)
+
+val env : t -> env
+
+val vars_of_env : t -> Id.Set.t
+
+(** Push to the environment, returning the declaration(s) with interpreted names *)
+
+val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t
+val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t
+val push_rec_types : evar_map -> Name.t array * constr array -> t -> Name.t array * t
+
+(** Declare an evar using renaming information *)
+
+val e_new_evar : t -> evar_map ref -> ?src:Evar_kinds.t Loc.located ->
+ ?naming:Namegen.intro_pattern_naming_expr -> constr -> constr
+
+val e_new_type_evar : t -> evar_map ref -> src:Evar_kinds.t Loc.located -> constr
+
+(** [hide_variable env na id] tells to hide the binding of [id] in
+ the ltac environment part of [env] and to additionally rebind
+ it to [id'] in case [na] is some [Name id']. It is useful e.g.
+ for the dual status of [y] as term and binder. This is the case
+ of [match y return p with ... end] which implicitly denotes
+ [match z as z return p with ... end] when [y] is bound to a
+ variable [z] and [match t as y return p with ... end] when [y]
+ is bound to a non-variable term [t]. In the latter case, the
+ binding of [y] to [t] should be hidden in [p]. *)
+
+val hide_variable : t -> Name.t -> Id.t -> t
+
+(** In case a variable is not bound by a term binder, look if it has
+ an interpretation as a term in the ltac_var_map *)
+
+val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) ->
+ t -> evar_map -> Id.t -> unsafe_judgment
+
+(** Interpreting a generic argument, typically a "ltac:(...)", taking
+ into account the possible renaming *)
+
+val interp_glob_genarg : t -> evar_map -> constr ->
+ Genarg.glob_generic_argument -> constr * evar_map
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 24eb666828..bd13f1d00a 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -15,7 +15,6 @@ open Nameops
open Globnames
open Glob_term
open Evar_kinds
-open Ltac_pretype
(* Untyped intermediate terms, after ASTs and before constr. *)
@@ -577,22 +576,9 @@ let glob_constr_of_closed_cases_pattern p = match DAst.get p with
let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
-(**********************************************************************)
-(* Interpreting ltac variables *)
-
-open Pp
-open CErrors
-
-let ltac_interp_name { ltac_idents ; ltac_genargs } = function
- | Anonymous -> Anonymous
- | Name id as n ->
- try Name (Id.Map.find id ltac_idents)
- with Not_found ->
- if Id.Map.mem id ltac_genargs then
- user_err (str"Ltac variable"++spc()++ Id.print id ++
- spc()++str"is not bound to an identifier."++spc()++
- str"It cannot be used in a binder.")
- else n
+(* This has to be in some file... *)
+
+open Ltac_pretype
let empty_lvar : ltac_var_map = {
ltac_constrs = Id.Map.empty;
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c967f4e884..91a2ef9c1e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -101,5 +101,4 @@ val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
-val ltac_interp_name : Ltac_pretype.ltac_var_map -> Name.t -> Name.t
val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index eb283a0220..be79b8b07d 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk =
| FEvar ((_,args),e) ->
let variances = infer_stack infos variances stk in
infer_vect infos variances (Array.map (mk_clos e) args)
- | FRel _ -> variances
+ | FRel _ -> infer_stack infos variances stk
| FFlex fl ->
let variances = infer_table_key infos variances fl in
infer_stack infos variances stk
diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml
index be8579c2e5..ac59b96eef 100644
--- a/pretyping/ltac_pretype.ml
+++ b/pretyping/ltac_pretype.ml
@@ -64,5 +64,5 @@ type ltac_var_map = {
ltac_idents: Id.t Id.Map.t;
(** Ltac variables bound to identifiers *)
ltac_genargs : unbound_ltac_var_map;
- (** Ltac variables bound to other kinds of arguments *)
+ (** All Ltac variables (to pass on ltac subterms, and for error reporting) *)
}
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a315376aca..d10c00fa6e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -38,19 +38,20 @@ open Reductionops
open Type_errors
open Typing
open Globnames
-open Nameops
open Evarutil
open Evardefine
open Pretype_errors
open Glob_term
open Glob_ops
+open GlobEnv
open Evarconv
-open Ltac_pretype
module NamedDecl = Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
+let (!!) env = GlobEnv.env env
+
(************************************************************************)
(* This concerns Cases *)
open Inductive
@@ -58,58 +59,6 @@ open Inductiveops
(************************************************************************)
-module ExtraEnv =
-struct
-
-type t = {
- env : Environ.env;
- extra : Evarutil.ext_named_context Lazy.t;
- (** Delay the computation of the evar extended environment *)
-}
-
-let get_extra env sigma =
- let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
- Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc)
- (rel_context env) ~init:(empty_csubst, avoid, named_context env)
-
-let make_env env sigma = { env = env; extra = lazy (get_extra env sigma) }
-let rel_context env = rel_context env.env
-
-let push_rel sigma d env = {
- env = push_rel d env.env;
- extra = lazy (push_rel_decl_to_named_context sigma d (Lazy.force env.extra));
-}
-
-let pop_rel_context n env sigma = make_env (pop_rel_context n env.env) sigma
-
-let push_rel_context sigma ctx env = {
- env = push_rel_context ctx env.env;
- extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx (Lazy.force env.extra));
-}
-
-let lookup_named id env = lookup_named id env.env
-
-let e_new_evar env evdref ?src ?naming typ =
- let open Context.Named.Declaration in
- let inst_vars = List.map (get_id %> mkVar) (named_context env.env) in
- let inst_rels = List.rev (rel_list 0 (nb_rel env.env)) in
- let (subst, _, nc) = Lazy.force env.extra in
- let typ' = csubst_subst subst typ in
- let instance = inst_rels @ inst_vars in
- let sign = val_of_named_context nc in
- let sigma = !evdref in
- let (sigma, e) = new_evar_instance sign sigma typ' ?src ?naming instance in
- evdref := sigma;
- e
-
-let push_rec_types sigma (lna,typarray,_) env =
- let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in
- Array.fold_left (fun e assum -> push_rel sigma assum e) env ctxt
-
-end
-
-open ExtraEnv
-
(* An auxiliary function for searching for fixpoint guard indexes *)
exception Found of int array
@@ -400,7 +349,7 @@ let adjust_evar_source evdref na c =
let inh_conv_coerce_to_tycon ?loc resolve_tc env evdref j = function
| None -> j
| Some t ->
- evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc env.ExtraEnv.env) evdref j t
+ evd_comb2 (Coercion.inh_conv_coerce_to ?loc resolve_tc !!env) evdref j t
let check_instance loc subst = function
| [] -> ()
@@ -417,76 +366,21 @@ let orelse_name name name' = match name with
| Anonymous -> name'
| _ -> name
-let ltac_interp_name_env k0 lvar env sigma =
- (* envhd is the initial part of the env when pretype was called first *)
- (* (in practice is is probably 0, but we have to grant the
- specification of pretype which accepts to start with a non empty
- rel_context) *)
- (* tail is the part of the env enriched by pretyping *)
- let n = Context.Rel.length (rel_context env) - k0 in
- let ctxt,_ = List.chop n (rel_context env) in
- let open Context.Rel.Declaration in
- let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in
- if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env
- else push_rel_context sigma ctxt' (pop_rel_context n env sigma)
-
-let invert_ltac_bound_name lvar env id0 id =
- let id' = Id.Map.find id lvar.ltac_idents in
- try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
- with Not_found ->
- user_err (str "Ltac variable " ++ Id.print id0 ++
- str " depends on pattern variable name " ++ Id.print id ++
- str " which is not bound in current context.")
-
-let protected_get_type_of env sigma c =
- try Retyping.get_type_of ~lax:true env.ExtraEnv.env sigma c
- with Retyping.RetypeError _ ->
- user_err
- (str "Cannot reinterpret " ++ quote (print_constr c) ++
- str " in the current environment.")
-
-let pretype_id pretype k0 loc env evdref lvar id =
- let sigma = !evdref in
+let pretype_id pretype k0 loc env evdref id =
(* Look for the binder of [id] *)
try
- let (n,_,typ) = lookup_rel_id id (rel_context env) in
+ let (n,_,typ) = lookup_rel_id id (rel_context !!env) in
{ uj_val = mkRel n; uj_type = lift n typ }
with Not_found ->
- let env = ltac_interp_name_env k0 lvar env !evdref in
- (* Check if [id] is an ltac variable *)
- try
- let (ids,c) = Id.Map.find id lvar.ltac_constrs in
- let subst = List.map (invert_ltac_bound_name lvar env id) ids in
- let c = substl subst c in
- { uj_val = c; uj_type = protected_get_type_of env sigma c }
- with Not_found -> try
- let {closure;term} = Id.Map.find id lvar.ltac_uconstrs in
- let lvar = {
- ltac_constrs = closure.typed;
- ltac_uconstrs = closure.untyped;
- ltac_idents = closure.idents;
- ltac_genargs = Id.Map.empty; }
- in
- (* spiwack: I'm catching [Not_found] potentially too eagerly
- here, as the call to the main pretyping function is caught
- inside the try but I want to avoid refactoring this function
- too much for now. *)
- pretype env evdref lvar term
- with Not_found ->
- (* Check if [id] is a ltac variable not bound to a term *)
- (* and build a nice error message *)
- if Id.Map.mem id lvar.ltac_genargs then begin
- let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
- user_err ?loc
- (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \
- bound to a " ++ Geninterp.Val.pr typ ++ str ".")
- end;
- (* Check if [id] is a section or goal variable *)
- try
- { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id env) }
- with Not_found ->
- (* [id] not found, standard error message *)
- error_var_not_found ?loc id
+ try
+ GlobEnv.interp_ltac_variable ?loc (fun env -> pretype env evdref) env !evdref id
+ with Not_found ->
+ (* Check if [id] is a section or goal variable *)
+ try
+ { uj_val = mkVar id; uj_type = NamedDecl.get_type (lookup_named id !!env) }
+ with Not_found ->
+ (* [id] not found, standard error message *)
+ error_var_not_found ?loc id
(*************************************************************************)
(* Main pretyping function *)
@@ -524,18 +418,18 @@ let pretype_global ?loc rigid env evd gr us =
match us with
| None -> evd, None
| Some l ->
- let _, ctx = Global.constr_of_global_in_context env.ExtraEnv.env gr in
+ let _, ctx = Global.constr_of_global_in_context !!env gr in
let len = Univ.AUContext.size ctx in
interp_instance ?loc evd ~len l
in
- let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
+ let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance !!env evd gr in
(sigma, c)
let pretype_ref ?loc evdref env ref us =
match ref with
| VarRef id ->
(* Section variable *)
- (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id env))
+ (try make_judge (mkVar id) (NamedDecl.get_type (lookup_named id !!env))
with Not_found ->
(* This may happen if env is a goal env and section variables have
been cleared - section variables should be different from goal
@@ -544,7 +438,7 @@ let pretype_ref ?loc evdref env ref us =
| ref ->
let evd, c = pretype_global ?loc univ_flexible env !evdref ref us in
let () = evdref := evd in
- let ty = unsafe_type_of env.ExtraEnv.env evd c in
+ let ty = unsafe_type_of !!env evd c in
make_judge c ty
let judge_of_Type ?loc evd s =
@@ -560,31 +454,13 @@ let pretype_sort ?loc evdref = function
| GType s -> evd_comb1 (judge_of_Type ?loc) evdref s
let new_type_evar env evdref loc =
- let sigma = !evdref in
- let (sigma, (e, _)) =
- Evarutil.new_type_evar env.ExtraEnv.env sigma
- univ_flexible_alg ~src:(loc,Evar_kinds.InternalHole)
- in
- evdref := sigma;
- e
-
-module ConstrInterpObj =
-struct
- type ('r, 'g, 't) obj =
- unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map
- let name = "constr_interp"
- let default _ = None
-end
-
-module ConstrInterp = Genarg.Register(ConstrInterpObj)
-
-let register_constr_interp0 = ConstrInterp.register0
+ e_new_type_evar env evdref ~src:(Loc.tag ?loc Evar_kinds.InternalHole)
(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
(* in environment [env], with existential variables [evdref] and *)
(* the type constraint tycon *)
-let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref t =
let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc resolve_tc in
let pretype_type = pretype_type k0 resolve_tc in
let pretype = pretype k0 resolve_tc in
@@ -598,7 +474,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| GVar id ->
inh_conv_coerce_to_tycon ?loc env evdref
- (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
+ (pretype_id (fun e r t -> pretype tycon e r t) k0 loc env evdref id)
tycon
| GEvar (id, inst) ->
@@ -609,13 +485,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
with Not_found ->
user_err ?loc (str "Unknown existential variable.") in
let hyps = evar_filtered_context (Evd.find !evdref evk) in
- let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
+ let args = pretype_instance k0 resolve_tc env evdref loc hyps evk inst in
let c = mkEvar (evk, args) in
- let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in
+ let j = (Retyping.get_judgment_of !!env !evdref c) in
inh_conv_coerce_to_tycon ?loc env evdref j tycon
| GPatVar kind ->
- let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
@@ -624,48 +499,40 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
| GHole (k, naming, None) ->
- let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
- | None ->
- new_type_evar env evdref loc in
+ | None -> new_type_evar env evdref loc in
{ uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
| GHole (k, _naming, Some arg) ->
- let env = ltac_interp_name_env k0 lvar env !evdref in
let ty =
match tycon with
| Some ty -> ty
- | None ->
- new_type_evar env evdref loc in
- let open Genarg in
- let ist = lvar.ltac_genargs in
- let GenArg (Glbwit tag, arg) = arg in
- let interp = ConstrInterp.obj tag in
- let (c, sigma) = interp ist env.ExtraEnv.env !evdref ty arg in
+ | None -> new_type_evar env evdref loc in
+ let (c, sigma) = GlobEnv.interp_glob_genarg env !evdref ty arg in
let () = evdref := sigma in
{ uj_val = c; uj_type = ty }
| GRec (fixkind,names,bl,lar,vdef) ->
let rec type_bl env ctxt = function
- [] -> ctxt
+ | [] -> ctxt
| (na,bk,None,ty)::bl ->
- let ty' = pretype_type empty_valcon env evdref lvar ty in
+ let ty' = pretype_type empty_valcon env evdref ty in
let dcl = LocalAssum (na, ty'.utj_val) in
- let dcl' = LocalAssum (ltac_interp_name lvar na,ty'.utj_val) in
- type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl
+ let dcl', env = push_rel !evdref dcl env in
+ type_bl env (Context.Rel.add dcl' ctxt) bl
| (na,bk,Some bd,ty)::bl ->
- let ty' = pretype_type empty_valcon env evdref lvar ty in
- let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
+ let ty' = pretype_type empty_valcon env evdref ty in
+ let bd' = pretype (mk_tycon ty'.utj_val) env evdref bd in
let dcl = LocalDef (na, bd'.uj_val, ty'.utj_val) in
- let dcl' = LocalDef (ltac_interp_name lvar na, bd'.uj_val, ty'.utj_val) in
- type_bl (push_rel !evdref dcl env) (Context.Rel.add dcl' ctxt) bl in
+ let dcl', env = push_rel !evdref dcl env in
+ type_bl env (Context.Rel.add dcl' ctxt) bl in
let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
let larj =
Array.map2
(fun e ar ->
- pretype_type empty_valcon (push_rel_context !evdref e env) evdref lvar ar)
+ pretype_type empty_valcon (snd (push_rel_context !evdref e env)) evdref ar)
ctxtv lar in
let lara = Array.map (fun a -> a.utj_val) larj in
let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
@@ -678,14 +545,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| GFix (vn,i) -> i
| GCoFix i -> i
in
- begin match conv env.ExtraEnv.env !evdref ftys.(fixi) t with
+ begin match conv !!env !evdref ftys.(fixi) t with
| None -> ()
| Some sigma -> evdref := sigma
end
| None -> ()
in
(* Note: bodies are not used by push_rec_types, so [||] is safe *)
- let newenv = push_rec_types !evdref (names,ftys,[||]) env in
+ let names,newenv = push_rec_types !evdref (names,ftys) env in
let vdefj =
Array.map2_i
(fun i ctxt def ->
@@ -694,12 +561,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let (ctxt,ty) =
decompose_prod_n_assum !evdref (Context.Rel.length ctxt)
(lift nbfix ftys.(i)) in
- let nenv = push_rel_context !evdref ctxt newenv in
- let j = pretype (mk_tycon ty) nenv evdref lvar def in
+ let ctxt,nenv = push_rel_context !evdref ctxt newenv in
+ let j = pretype (mk_tycon ty) nenv evdref def in
{ uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
ctxtv vdef in
- evdref := Typing.check_type_fixpoint ?loc env.ExtraEnv.env !evdref names ftys vdefj;
+ evdref := Typing.check_type_fixpoint ?loc !!env !evdref names ftys vdefj;
let nf c = nf_evar !evdref c in
let ftys = Array.map nf ftys in (** FIXME *)
let fdefs = Array.map (fun x -> nf (j_val x)) vdefj in
@@ -721,13 +588,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let fixdecls = (names,ftys,fdefs) in
let indexes =
search_guard
- ?loc env.ExtraEnv.env possible_indexes (nf_fix !evdref fixdecls)
+ ?loc !!env possible_indexes (nf_fix !evdref fixdecls)
in
make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
| GCoFix i ->
let fixdecls = (names,ftys,fdefs) in
let cofix = (i, fixdecls) in
- (try check_cofix env.ExtraEnv.env (i, nf_fix !evdref fixdecls)
+ (try check_cofix !!env (i, nf_fix !evdref fixdecls)
with reraise ->
let (e, info) = CErrors.push reraise in
let info = Option.cata (Loc.add_loc info) info loc in
@@ -742,11 +609,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| GProj (p, c) ->
(* TODO: once GProj is used as an input syntax, use bidirectional typing here *)
- let cj = pretype empty_tycon env evdref lvar c in
- judge_of_projection env.ExtraEnv.env !evdref p cj
+ let cj = pretype empty_tycon env evdref c in
+ judge_of_projection !!env !evdref p cj
| GApp (f,args) ->
- let fj = pretype empty_tycon env evdref lvar f in
+ let fj = pretype empty_tycon env evdref f in
let floc = loc_of_glob_constr f in
let length = List.length args in
let candargs =
@@ -762,7 +629,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
if Int.equal npars 0 then []
else
try
- let IndType (indf, args) = find_rectype env.ExtraEnv.env !evdref ty in
+ let IndType (indf, args) = find_rectype !!env !evdref ty in
let ((ind',u'),pars) = dest_ind_family indf in
if eq_ind ind ind' then List.map EConstr.of_constr pars
else (* Let the usual code throw an error *) []
@@ -784,17 +651,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| [] -> resj
| c::rest ->
let argloc = loc_of_glob_constr c in
- let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env.ExtraEnv.env) evdref resj in
- let resty = whd_all env.ExtraEnv.env !evdref resj.uj_type in
+ let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc !!env) evdref resj in
+ let resty = whd_all !!env !evdref resj.uj_type in
match EConstr.kind !evdref resty with
| Prod (na,c1,c2) ->
let tycon = Some c1 in
- let hj = pretype tycon env evdref lvar c in
+ let hj = pretype tycon env evdref c in
let candargs, ujval =
match candargs with
| [] -> [], j_val hj
| arg :: args ->
- begin match conv env.ExtraEnv.env !evdref (j_val hj) arg with
+ begin match conv !!env !evdref (j_val hj) arg with
| Some sigma -> evdref := sigma;
args, nf_evar !evdref (j_val hj)
| None ->
@@ -807,104 +674,96 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
apply_rec env (n+1) j candargs rest
| _ ->
- let hj = pretype empty_tycon env evdref lvar c in
+ let hj = pretype empty_tycon env evdref c in
error_cant_apply_not_functional
- ?loc:(Loc.merge_opt floc argloc) env.ExtraEnv.env !evdref
+ ?loc:(Loc.merge_opt floc argloc) !!env !evdref
resj [|hj|]
in
let resj = apply_rec env 1 fj candargs args in
let resj =
match EConstr.kind !evdref resj.uj_val with
| App (f,args) ->
- if is_template_polymorphic env.ExtraEnv.env !evdref f then
+ if is_template_polymorphic !!env !evdref f then
(* Special case for inductive type applications that must be
refreshed right away. *)
let c = mkApp (f, args) in
- let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env.ExtraEnv.env) evdref c in
- let t = Retyping.get_type_of env.ExtraEnv.env !evdref c in
+ let c = evd_comb1 (Evarsolve.refresh_universes (Some true) !!env) evdref c in
+ let t = Retyping.get_type_of !!env !evdref c in
make_judge c (* use this for keeping evars: resj.uj_val *) t
else resj
| _ -> resj
in
inh_conv_coerce_to_tycon ?loc env evdref resj tycon
- | GLambda(name,bk,c1,c2) ->
+ | GLambda(name,bk,c1,c2) ->
let tycon' = evd_comb1
(fun evd tycon ->
match tycon with
| None -> evd, tycon
| Some ty ->
- let evd, ty' = Coercion.inh_coerce_to_prod ?loc env.ExtraEnv.env evd ty in
+ let evd, ty' = Coercion.inh_coerce_to_prod ?loc !!env evd ty in
evd, Some ty')
evdref tycon
in
- let (name',dom,rng) = evd_comb1 (split_tycon ?loc env.ExtraEnv.env) evdref tycon' in
+ let (name',dom,rng) = evd_comb1 (split_tycon ?loc !!env) evdref tycon' in
let dom_valcon = valcon_of_tycon dom in
- let j = pretype_type dom_valcon env evdref lvar c1 in
- (* The name specified by ltac is used also to create bindings. So
- the substitution must also be applied on variables before they are
- looked up in the rel context. *)
+ let j = pretype_type dom_valcon env evdref c1 in
let var = LocalAssum (name, j.utj_val) in
- let j' = pretype rng (push_rel !evdref var env) evdref lvar c2 in
- let name = ltac_interp_name lvar name in
- let resj = judge_of_abstraction env.ExtraEnv.env (orelse_name name name') j j' in
+ let var',env' = push_rel !evdref var env in
+ let j' = pretype rng env' evdref c2 in
+ let name = get_name var' in
+ let resj = judge_of_abstraction !!env (orelse_name name name') j j' in
inh_conv_coerce_to_tycon ?loc env evdref resj tycon
- | GProd(name,bk,c1,c2) ->
- let j = pretype_type empty_valcon env evdref lvar c1 in
- (* The name specified by ltac is used also to create bindings. So
- the substitution must also be applied on variables before they are
- looked up in the rel context. *)
- let j' = match name with
+ | GProd(name,bk,c1,c2) ->
+ let j = pretype_type empty_valcon env evdref c1 in
+ let name, j' = match name with
| Anonymous ->
- let j = pretype_type empty_valcon env evdref lvar c2 in
- { j with utj_val = lift 1 j.utj_val }
+ let j = pretype_type empty_valcon env evdref c2 in
+ name, { j with utj_val = lift 1 j.utj_val }
| Name _ ->
let var = LocalAssum (name, j.utj_val) in
- let env' = push_rel !evdref var env in
- pretype_type empty_valcon env' evdref lvar c2
+ let var, env' = push_rel !evdref var env in
+ get_name var, pretype_type empty_valcon env' evdref c2
in
- let name = ltac_interp_name lvar name in
let resj =
try
- judge_of_product env.ExtraEnv.env name j j'
+ judge_of_product !!env name j j'
with TypeError _ as e ->
let (e, info) = CErrors.push e in
let info = Option.cata (Loc.add_loc info) info loc in
iraise (e, info) in
inh_conv_coerce_to_tycon ?loc env evdref resj tycon
- | GLetIn(name,c1,t,c2) ->
+ | GLetIn(name,c1,t,c2) ->
let tycon1 =
match t with
| Some t ->
- mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val
+ mk_tycon (pretype_type empty_valcon env evdref t).utj_val
| None ->
empty_tycon in
- let j = pretype tycon1 env evdref lvar c1 in
+ let j = pretype tycon1 env evdref c1 in
let t = evd_comb1 (Evarsolve.refresh_universes
- ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
+ ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env)
evdref j.uj_type in
- (* The name specified by ltac is used also to create bindings. So
- the substitution must also be applied on variables before they are
- looked up in the rel context. *)
let var = LocalDef (name, j.uj_val, t) in
let tycon = lift_tycon 1 tycon in
- let j' = pretype tycon (push_rel !evdref var env) evdref lvar c2 in
- let name = ltac_interp_name lvar name in
+ let var, env = push_rel !evdref var env in
+ let j' = pretype tycon env evdref c2 in
+ let name = get_name var in
{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
uj_type = subst1 j.uj_val j'.uj_type }
| GLetTuple (nal,(na,po),c,d) ->
- let cj = pretype empty_tycon env evdref lvar c in
+ let cj = pretype empty_tycon env evdref c in
let (IndType (indf,realargs)) =
- try find_rectype env.ExtraEnv.env !evdref cj.uj_type
+ try find_rectype !!env !evdref cj.uj_type
with Not_found ->
let cloc = loc_of_glob_constr c in
- error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj
+ error_case_not_inductive ?loc:cloc !!env !evdref cj
in
let ind = fst (fst (dest_ind_family indf)) in
- let cstrs = get_constructors env.ExtraEnv.env indf in
+ let cstrs = get_constructors !!env indf in
if not (Int.equal (Array.length cstrs) 1) then
user_err ?loc (str "Destructing let is only for inductive types" ++
str " with one constructor.");
@@ -914,7 +773,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
int cs.cs_nargs ++ str " variables.");
let fsign, record =
let set_name na d = set_name na (map_rel_decl EConstr.of_constr d) in
- match Environ.get_projections env.ExtraEnv.env ind with
+ match Environ.get_projections !!env ind with
| None ->
List.map2 set_name (List.rev nal) cs.cs_args, false
| Some ps ->
@@ -933,108 +792,97 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let fsign = if Flags.version_strictly_greater Flags.V8_6
then Context.Rel.map (whd_betaiota !evdref) fsign
else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+ let fsign,env_f = push_rel_context !evdref fsign env in
let obj ind p v f =
- if not record then
- let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
- let nal = List.rev nal in
- let fsign = List.map2 set_name nal fsign in
+ if not record then
let f = it_mkLambda_or_LetIn f fsign in
- let ci = make_case_info env.ExtraEnv.env (fst ind) LetStyle in
+ let ci = make_case_info !!env (fst ind) LetStyle in
mkCase (ci, p, cj.uj_val,[|f|])
else it_mkLambda_or_LetIn f fsign
in
- let env_f = push_rel_context !evdref fsign env in
- (* Make dependencies from arity signature impossible *)
+ (* Make dependencies from arity signature impossible *)
let arsgn =
- let arsgn,_ = get_arity env.ExtraEnv.env indf in
+ let arsgn,_ = get_arity !!env indf in
List.map (set_name Anonymous) arsgn
in
- let indt = build_dependent_inductive env.ExtraEnv.env indf in
+ let indt = build_dependent_inductive !!env indf in
let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
- let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in
- let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in
- let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in
- let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *)
let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
+ let predenv = Cases.make_return_predicate_ltac_lvar env !evdref na c cj.uj_val in
let nar = List.length arsgn in
+ let psign',env_p = push_rel_context ~force_names:true !evdref psign predenv in
(match po with
| Some p ->
- let env_p = push_rel_context !evdref psign env in
- let pj = pretype_type empty_valcon env_p evdref predlvar p in
+ let pj = pretype_type empty_valcon env_p evdref p in
let ccl = nf_evar !evdref pj.utj_val in
let p = it_mkLambda_or_LetIn ccl psign' in
let inst =
(Array.map_to_list EConstr.of_constr cs.cs_concl_realargs)
@[EConstr.of_constr (build_dependent_constructor cs)] in
let lp = lift cs.cs_nargs p in
- let fty = hnf_lam_applist env.ExtraEnv.env !evdref lp inst in
- let fj = pretype (mk_tycon fty) env_f evdref lvar d in
+ let fty = hnf_lam_applist !!env !evdref lp inst in
+ let fj = pretype (mk_tycon fty) env_f evdref d in
let v =
let ind,_ = dest_ind_family indf in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+ Typing.check_allowed_sort !!env !evdref ind cj.uj_val p;
obj ind p cj.uj_val fj.uj_val
in
{ uj_val = v; uj_type = (substl (realargs@[cj.uj_val]) ccl) }
| None ->
let tycon = lift_tycon cs.cs_nargs tycon in
- let fj = pretype tycon env_f evdref predlvar d in
+ let fj = pretype tycon env_f evdref d in
let ccl = nf_evar !evdref fj.uj_type in
let ccl =
if noccur_between !evdref 1 cs.cs_nargs ccl then
lift (- cs.cs_nargs) ccl
else
- error_cant_find_case_type ?loc env.ExtraEnv.env !evdref
+ error_cant_find_case_type ?loc !!env !evdref
cj.uj_val in
(* let ccl = refresh_universes ccl in *)
let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign' in
let v =
let ind,_ = dest_ind_family indf in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val p;
+ Typing.check_allowed_sort !!env !evdref ind cj.uj_val p;
obj ind p cj.uj_val fj.uj_val
in { uj_val = v; uj_type = ccl })
| GIf (c,(na,po),b1,b2) ->
- let cj = pretype empty_tycon env evdref lvar c in
+ let cj = pretype empty_tycon env evdref c in
let (IndType (indf,realargs)) =
- try find_rectype env.ExtraEnv.env !evdref cj.uj_type
+ try find_rectype !!env !evdref cj.uj_type
with Not_found ->
let cloc = loc_of_glob_constr c in
- error_case_not_inductive ?loc:cloc env.ExtraEnv.env !evdref cj in
- let cstrs = get_constructors env.ExtraEnv.env indf in
+ error_case_not_inductive ?loc:cloc !!env !evdref cj in
+ let cstrs = get_constructors !!env indf in
if not (Int.equal (Array.length cstrs) 2) then
user_err ?loc
(str "If is only for inductive types with two constructors.");
let arsgn =
- let arsgn,_ = get_arity env.ExtraEnv.env indf in
+ let arsgn,_ = get_arity !!env indf in
(* Make dependencies from arity signature impossible *)
List.map (set_name Anonymous) arsgn
in
let nar = List.length arsgn in
- let indt = build_dependent_inductive env.ExtraEnv.env indf in
+ let indt = build_dependent_inductive !!env indf in
let psign = LocalAssum (na, indt) :: arsgn in (* For locating names in [po] *)
- let predlvar = Cases.make_return_predicate_ltac_lvar !evdref na c cj.uj_val lvar in
- let psign' = LocalAssum (ltac_interp_name predlvar na, indt) :: arsgn in
- let psign' = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign' in
- let psign' = Namegen.name_context env.ExtraEnv.env !evdref psign' in (* For naming abstractions in [po] *)
let psign = List.map (fun d -> map_rel_decl EConstr.of_constr d) psign in
+ let predenv = Cases.make_return_predicate_ltac_lvar env !evdref na c cj.uj_val in
+ let psign,env_p = push_rel_context !evdref psign predenv in
let pred,p = match po with
| Some p ->
- let env_p = push_rel_context !evdref psign env in
- let pj = pretype_type empty_valcon env_p evdref predlvar p in
+ let pj = pretype_type empty_valcon env_p evdref p in
let ccl = nf_evar !evdref pj.utj_val in
- let pred = it_mkLambda_or_LetIn ccl psign' in
+ let pred = it_mkLambda_or_LetIn ccl psign in
let typ = lift (- nar) (beta_applist !evdref (pred,[cj.uj_val])) in
pred, typ
| None ->
let p = match tycon with
| Some ty -> ty
- | None ->
- let env = ltac_interp_name_env k0 lvar env !evdref in
- new_type_evar env evdref loc
+ | None -> new_type_evar env evdref loc
in
- it_mkLambda_or_LetIn (lift (nar+1) p) psign', p in
+ it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
let pred = nf_evar !evdref pred in
let p = nf_evar !evdref p in
let f cs b =
@@ -1049,85 +897,83 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let csgn =
List.map (set_name Anonymous) cs_args
in
- let env_c = push_rel_context !evdref csgn env in
- let bj = pretype (mk_tycon pi) env_c evdref lvar b in
+ let _,env_c = push_rel_context !evdref csgn env in
+ let bj = pretype (mk_tycon pi) env_c evdref b in
it_mkLambda_or_LetIn bj.uj_val cs_args in
let b1 = f cstrs.(0) b1 in
let b2 = f cstrs.(1) b2 in
let v =
let ind,_ = dest_ind_family indf in
- let ci = make_case_info env.ExtraEnv.env (fst ind) IfStyle in
+ let ci = make_case_info !!env (fst ind) IfStyle in
let pred = nf_evar !evdref pred in
- Typing.check_allowed_sort env.ExtraEnv.env !evdref ind cj.uj_val pred;
+ Typing.check_allowed_sort !!env !evdref ind cj.uj_val pred;
mkCase (ci, pred, cj.uj_val, [|b1;b2|])
in
let cj = { uj_val = v; uj_type = p } in
inh_conv_coerce_to_tycon ?loc env evdref cj tycon
| GCases (sty,po,tml,eqns) ->
- Cases.compile_cases ?loc sty
- ((fun vtyc env evdref -> pretype vtyc (make_env env !evdref) evdref),evdref)
- tycon env.ExtraEnv.env (* loc *) lvar (po,tml,eqns)
+ Cases.compile_cases ?loc sty (pretype,evdref) tycon env (po,tml,eqns)
| GCast (c,k) ->
let cj =
match k with
| CastCoerce ->
- let cj = pretype empty_tycon env evdref lvar c in
- evd_comb1 (Coercion.inh_coerce_to_base ?loc env.ExtraEnv.env) evdref cj
+ let cj = pretype empty_tycon env evdref c in
+ evd_comb1 (Coercion.inh_coerce_to_base ?loc !!env) evdref cj
| CastConv t | CastVM t | CastNative t ->
let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in
- let tj = pretype_type empty_valcon env evdref lvar t in
+ let tj = pretype_type empty_valcon env evdref t in
let tval = evd_comb1 (Evarsolve.refresh_universes
- ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
+ ~onlyalg:true ~status:Evd.univ_flexible (Some false) !!env)
evdref tj.utj_val in
let tval = nf_evar !evdref tval in
let cj, tval = match k with
| VMcast ->
- let cj = pretype empty_tycon env evdref lvar c in
+ let cj = pretype empty_tycon env evdref c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
if not (occur_existential !evdref cty || occur_existential !evdref tval) then
- match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+ match Reductionops.vm_infer_conv !!env !evdref cty tval with
| Some evd -> (evdref := evd; cj, tval)
| None ->
- error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
- (ConversionFailed (env.ExtraEnv.env,cty,tval))
+ error_actual_type ?loc !!env !evdref cj tval
+ (ConversionFailed (!!env,cty,tval))
else user_err ?loc (str "Cannot check cast with vm: " ++
str "unresolved arguments remain.")
| NATIVEcast ->
- let cj = pretype empty_tycon env evdref lvar c in
+ let cj = pretype empty_tycon env evdref c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
begin
- match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+ match Nativenorm.native_infer_conv !!env !evdref cty tval with
| Some evd -> (evdref := evd; cj, tval)
| None ->
- error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
- (ConversionFailed (env.ExtraEnv.env,cty,tval))
+ error_actual_type ?loc !!env !evdref cj tval
+ (ConversionFailed (!!env,cty,tval))
end
| _ ->
- pretype (mk_tycon tval) env evdref lvar c, tval
+ pretype (mk_tycon tval) env evdref c, tval
in
let v = mkCast (cj.uj_val, k, tval) in
{ uj_val = v; uj_type = tval }
in inh_conv_coerce_to_tycon ?loc env evdref cj tycon
-and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
+and pretype_instance k0 resolve_tc env evdref loc hyps evk update =
let f decl (subst,update) =
let id = NamedDecl.get_id decl in
let t = replace_vars subst (NamedDecl.get_type decl) in
let c, update =
try
let c = List.assoc id update in
- let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
+ let c = pretype k0 resolve_tc (mk_tycon t) env evdref c in
c.uj_val, List.remove_assoc id update
with Not_found ->
try
- let (n,_,t') = lookup_rel_id id (rel_context env) in
- if is_conv env.ExtraEnv.env !evdref t (lift n t') then mkRel n, update else raise Not_found
+ let (n,_,t') = lookup_rel_id id (rel_context !!env) in
+ if is_conv !!env !evdref t (lift n t') then mkRel n, update else raise Not_found
with Not_found ->
try
- let t' = env |> lookup_named id |> NamedDecl.get_type in
- if is_conv env.ExtraEnv.env !evdref t t' then mkVar id, update else raise Not_found
+ let t' = !!env |> lookup_named id |> NamedDecl.get_type in
+ if is_conv !!env !evdref t t' then mkVar id, update else raise Not_found
with Not_found ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !evdref evk ++
@@ -1137,19 +983,19 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
check_instance loc subst inst;
Array.map_of_list snd subst
-(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with
+(* [pretype_type valcon env evdref c] coerces [c] into a type *)
+and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) evdref c = match DAst.get c with
| GHole (knd, naming, None) ->
let loc = loc_of_glob_constr c in
(match valcon with
| Some v ->
let s =
let sigma = !evdref in
- let t = Retyping.get_type_of env.ExtraEnv.env sigma v in
- match EConstr.kind sigma (whd_all env.ExtraEnv.env sigma t) with
+ let t = Retyping.get_type_of !!env sigma v in
+ match EConstr.kind sigma (whd_all !!env sigma t) with
| Sort s -> ESorts.kind sigma s
| Evar ev when is_Type sigma (existential_type sigma ev) ->
- evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev
+ evd_comb1 (define_evar_as_sort !!env) evdref ev
| _ -> anomaly (Pp.str "Found a type constraint which is not a type.")
in
(* Correction of bug #5315 : we need to define an evar for *all* holes *)
@@ -1160,40 +1006,39 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
{ utj_val = v;
utj_type = s }
| None ->
- let env = ltac_interp_name_env k0 lvar env !evdref in
let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
{ utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
utj_type = s})
| _ ->
- let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
+ let j = pretype k0 resolve_tc empty_tycon env evdref c in
let loc = loc_of_glob_constr c in
- let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in
+ let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc !!env) evdref j in
match valcon with
| None -> tj
| Some v ->
- begin match cumul env.ExtraEnv.env !evdref v tj.utj_val with
+ begin match cumul !!env !evdref v tj.utj_val with
| Some sigma -> evdref := sigma; tj
| None ->
error_unexpected_type
- ?loc:(loc_of_glob_constr c) env.ExtraEnv.env !evdref tj.utj_val v
+ ?loc:(loc_of_glob_constr c) !!env !evdref tj.utj_val v
end
let ise_pretype_gen flags env sigma lvar kind c =
- let env = make_env env sigma in
+ let env = GlobEnv.make env sigma lvar in
let evdref = ref sigma in
- let k0 = Context.Rel.length (rel_context env) in
+ let k0 = Context.Rel.length (rel_context !!env) in
let c', c'_ty = match kind with
| WithoutTypeConstraint ->
- let j = pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c in
+ let j = pretype k0 flags.use_typeclasses empty_tycon env evdref c in
j.uj_val, j.uj_type
| OfType exptyp ->
- let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c in
+ let j = pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref c in
j.uj_val, j.uj_type
| IsType ->
- let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c in
+ let tj = pretype_type k0 flags.use_typeclasses empty_valcon env evdref c in
tj.utj_val, mkSort tj.utj_type
in
- process_inference_flags flags env.ExtraEnv.env sigma (!evdref,c',c'_ty)
+ process_inference_flags flags !!env sigma (!evdref,c',c'_ty)
let default_inference_flags fail = {
use_typeclasses = true;
@@ -1236,7 +1081,7 @@ let understand_ltac flags env sigma lvar kind c =
(sigma, c)
let pretype k0 resolve_tc typcon env evdref lvar t =
- pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t
+ pretype k0 resolve_tc typcon (GlobEnv.make env !evdref lvar) evdref t
let pretype_type k0 resolve_tc valcon env evdref lvar t =
- pretype_type k0 resolve_tc valcon (make_env env !evdref) evdref lvar t
+ pretype_type k0 resolve_tc valcon (GlobEnv.make env !evdref lvar) evdref t
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 73f5b77e0e..fcc361b16b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -122,11 +122,3 @@ val pretype_type :
val ise_pretype_gen :
inference_flags -> env -> evar_map ->
ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr * types
-
-(**/**)
-
-(** To embed constr in glob_constr *)
-
-val register_constr_interp0 :
- ('r, 'g, 't) Genarg.genarg_type ->
- (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 5da5aff449..d0359b43f4 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -32,6 +32,7 @@ Program
Coercion
Detyping
Indrec
+GlobEnv
Cases
Pretyping
Unification
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 2f861c117b..bd41e61b34 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -192,11 +192,11 @@ let rec assoc_pat a = function
let object_table =
- Summary.ref (Refmap.empty : ((cs_pattern * constr) * obj_typ) list Refmap.t)
+ Summary.ref (GlobRef.Map.empty : ((cs_pattern * constr) * obj_typ) list GlobRef.Map.t)
~name:"record-canonical-structs"
let canonical_projections () =
- Refmap.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
+ GlobRef.Map.fold (fun x -> List.fold_right (fun ((y,_),c) acc -> ((x,y),c)::acc))
!object_table []
let keep_true_projections projs kinds =
@@ -289,11 +289,11 @@ let warn_redundant_canonical_projection =
let add_canonical_structure warn o =
let lo = compute_canonical_projections warn o in
List.iter (fun ((proj,(cs_pat,_ as pat)),s) ->
- let l = try Refmap.find proj !object_table with Not_found -> [] in
+ let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
let ocs = try Some (assoc_pat cs_pat l)
with Not_found -> None
in match ocs with
- | None -> object_table := Refmap.add proj ((pat,s)::l) !object_table;
+ | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table;
| Some (c, cs) ->
let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF))
and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in
@@ -372,18 +372,18 @@ let declare_canonical_structure ref =
add_canonical_structure (check_and_decompose_canonical_structure ref)
let lookup_canonical_conversion (proj,pat) =
- assoc_pat pat (Refmap.find proj !object_table)
+ assoc_pat pat (GlobRef.Map.find proj !object_table)
let decompose_projection sigma c args =
match EConstr.kind sigma c with
| Const (c, u) ->
let n = find_projection_nparams (ConstRef c) in
(** Check if there is some canonical projection attached to this structure *)
- let _ = Refmap.find (ConstRef c) !object_table in
+ let _ = GlobRef.Map.find (ConstRef c) !object_table in
let arg = Stack.nth args n in
arg
| Proj (p, c) ->
- let _ = Refmap.find (ConstRef (Projection.constant p)) !object_table in
+ let _ = GlobRef.Map.find (ConstRef (Projection.constant p)) !object_table in
c
| _ -> raise Not_found
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ba40262815..f4c8a6cd66 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -88,6 +88,7 @@ let set_reduction_effect x funkey =
(** Machinery to custom the behavior of the reduction *)
module ReductionBehaviour = struct
open Globnames
+ open Names
open Libobject
type t = {
@@ -97,7 +98,7 @@ module ReductionBehaviour = struct
}
let table =
- Summary.ref (Refmap.empty : t Refmap.t) ~name:"reductionbehaviour"
+ Summary.ref (GlobRef.Map.empty : t GlobRef.Map.t) ~name:"reductionbehaviour"
type flag = [ `ReductionDontExposeCase | `ReductionNeverUnfold ]
type req =
@@ -105,7 +106,7 @@ module ReductionBehaviour = struct
| ReqGlobal of GlobRef.t * (int list * int * flag list)
let load _ (_,(_,(r, b))) =
- table := Refmap.add r b !table
+ table := GlobRef.Map.add r b !table
let cache o = load 1 o
@@ -160,7 +161,7 @@ module ReductionBehaviour = struct
let get r =
try
- let b = Refmap.find r !table in
+ let b = GlobRef.Map.find r !table in
let flags =
if Int.equal b.b_nargs max_int then [`ReductionNeverUnfold]
else if b.b_dont_expose_case then [`ReductionDontExposeCase] else [] in
@@ -628,6 +629,18 @@ let safe_meta_value sigma ev =
try Some (Evd.meta_value sigma ev)
with Not_found -> None
+let strong_with_flags whdfun flags env sigma t =
+ let push_rel_check_zeta d env =
+ let open CClosure.RedFlags in
+ let d = match d with
+ | LocalDef (na,c,t) when not (red_set flags fZETA) -> LocalAssum (na,t)
+ | d -> d in
+ push_rel d env in
+ let rec strongrec env t =
+ map_constr_with_full_binders sigma
+ push_rel_check_zeta strongrec env (whdfun flags env sigma t) in
+ strongrec env t
+
let strong whdfun env sigma t =
let rec strongrec env t =
map_constr_with_full_binders sigma push_rel strongrec env (whdfun env sigma t) in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 07eeec9276..dd3cd26f0f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -144,6 +144,9 @@ val pr_state : state -> Pp.t
(** {6 Reduction Function Operators } *)
+val strong_with_flags :
+ (CClosure.RedFlags.reds -> reduction_function) ->
+ (CClosure.RedFlags.reds -> reduction_function)
val strong : reduction_function -> reduction_function
val local_strong : local_reduction_function -> local_reduction_function
val strong_prodspine : local_reduction_function -> local_reduction_function
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index efb3c339ac..55d9838bbb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -88,7 +88,7 @@ type typeclass = {
cl_unique : bool;
}
-type typeclasses = typeclass Refmap.t
+type typeclasses = typeclass GlobRef.Map.t
type instance = {
is_class: GlobRef.t;
@@ -99,7 +99,7 @@ type instance = {
is_impl: GlobRef.t;
}
-type instances = (instance Refmap.t) Refmap.t
+type instances = (instance GlobRef.Map.t) GlobRef.Map.t
let instance_impl is = is.is_impl
@@ -121,8 +121,8 @@ let new_instance cl info glob impl =
* states management
*)
-let classes : typeclasses ref = Summary.ref Refmap.empty ~name:"classes"
-let instances : instances ref = Summary.ref Refmap.empty ~name:"instances"
+let classes : typeclasses ref = Summary.ref GlobRef.Map.empty ~name:"classes"
+let instances : instances ref = Summary.ref GlobRef.Map.empty ~name:"instances"
let typeclass_univ_instance (cl, u) =
assert (Univ.AUContext.size cl.cl_univs == Univ.Instance.length u);
@@ -131,7 +131,7 @@ let typeclass_univ_instance (cl, u) =
cl_props = subst_ctx cl.cl_props}
let class_info c =
- try Refmap.find c !classes
+ try GlobRef.Map.find c !classes
with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c))
let global_class_of_constr env sigma c =
@@ -154,7 +154,7 @@ let class_of_constr sigma c =
let is_class_constr sigma c =
try let gr, u = Termops.global_of_constr sigma c in
- Refmap.mem gr !classes
+ GlobRef.Map.mem gr !classes
with Not_found -> false
let rec is_class_type evd c =
@@ -172,7 +172,7 @@ let is_class_evar evd evi =
*)
let load_class (_, cl) =
- classes := Refmap.add cl.cl_impl cl !classes
+ classes := GlobRef.Map.add cl.cl_impl cl !classes
let cache_class = load_class
@@ -336,17 +336,17 @@ type instance_action =
let load_instance inst =
let insts =
- try Refmap.find inst.is_class !instances
- with Not_found -> Refmap.empty in
- let insts = Refmap.add inst.is_impl inst insts in
- instances := Refmap.add inst.is_class insts !instances
+ try GlobRef.Map.find inst.is_class !instances
+ with Not_found -> GlobRef.Map.empty in
+ let insts = GlobRef.Map.add inst.is_impl inst insts in
+ instances := GlobRef.Map.add inst.is_class insts !instances
let remove_instance inst =
let insts =
- try Refmap.find inst.is_class !instances
+ try GlobRef.Map.find inst.is_class !instances
with Not_found -> assert false in
- let insts = Refmap.remove inst.is_impl insts in
- instances := Refmap.add inst.is_class insts !instances
+ let insts = GlobRef.Map.remove inst.is_impl insts in
+ instances := GlobRef.Map.add inst.is_class insts !instances
let cache_instance (_, (action, i)) =
match action with
@@ -464,23 +464,23 @@ let instance_constructor (cl,u) args =
(term, applist (mkConstU cst, pars))
| _ -> assert false
-let typeclasses () = Refmap.fold (fun _ l c -> l :: c) !classes []
+let typeclasses () = GlobRef.Map.fold (fun _ l c -> l :: c) !classes []
-let cmap_elements c = Refmap.fold (fun k v acc -> v :: acc) c []
+let cmap_elements c = GlobRef.Map.fold (fun k v acc -> v :: acc) c []
let instances_of c =
- try cmap_elements (Refmap.find c.cl_impl !instances) with Not_found -> []
+ try cmap_elements (GlobRef.Map.find c.cl_impl !instances) with Not_found -> []
let all_instances () =
- Refmap.fold (fun k v acc ->
- Refmap.fold (fun k v acc -> v :: acc) v acc)
+ GlobRef.Map.fold (fun k v acc ->
+ GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
!instances []
let instances r =
let cl = class_info r in instances_of cl
let is_class gr =
- Refmap.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
+ GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
let is_instance = function
| ConstRef c ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:28:25 +0000