aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--pretyping/cases.ml372
-rw-r--r--pretyping/cases.mli26
-rw-r--r--pretyping/globEnv.ml193
-rw-r--r--pretyping/globEnv.mli79
-rw-r--r--pretyping/glob_ops.ml20
-rw-r--r--pretyping/glob_ops.mli5
-rw-r--r--pretyping/pretyping.ml442
-rw-r--r--pretyping/pretyping.mli8
-rw-r--r--pretyping/pretyping.mllib1
-rw-r--r--test-suite/success/ltac.v10
11 files changed, 624 insertions, 534 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a0446bd6a0..f4313a8fa3 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2029,7 +2029,7 @@ let _ =
let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
(EConstr.of_constr c, sigma)
in
- Pretyping.register_constr_interp0 wit_tactic eval
+ GlobEnv.register_constr_interp0 wit_tactic eval
let vernac_debug b =
set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ad33297f0a..120dc61436 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,50 +362,45 @@ 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 *)
@@ -418,7 +418,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 +426,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 +466,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 }
@@ -786,31 +786,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 +958,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 +979,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 +1208,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 +1216,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 +1238,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 +1271,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 !!(pb.env) !(pb.evdref) cs_args eqns in
let typs = List.map2 RelDecl.set_name names cs_args
in
@@ -1279,7 +1279,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 +1291,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 +1360,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 +1370,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 +1400,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 +1423,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 +1443,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 +1461,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 +1483,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 +1498,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 +1534,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 +1549,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 +1573,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 +1616,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 +1630,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 +1667,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 +1679,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 +1711,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 +1719,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 +1732,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 +1761,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 +1780,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 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 = 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 +1808,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 +1843,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 +1857,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 +1877,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 +1894,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 +1904,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 +1977,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 +2008,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 +2025,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 +2038,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 +2142,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 +2162,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 +2230,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 +2277,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 +2304,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 +2324,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 +2481,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 +2492,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 +2529,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 +2542,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 +2554,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 +2579,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 +2590,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 +2601,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 +2617,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 +2629,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 +2639,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 +2658,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 +2667,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/globEnv.ml b/pretyping/globEnv.ml
new file mode 100644
index 0000000000..1bb4551f7c
--- /dev/null
+++ b/pretyping/globEnv.ml
@@ -0,0 +1,193 @@
+(************************************************************************)
+(* * 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 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 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..2445618749
--- /dev/null
+++ b/pretyping/globEnv.mli
@@ -0,0 +1,79 @@
+(************************************************************************)
+(* * 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
+
+(** 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
+
+(** [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 7bc0140931..91a2ef9c1e 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -101,9 +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
-(* [ltac_interp_name subst na] interprets a name according to a name
- substitution (subst.ltac_idents) and a list of names
- (subst.ltac_genargs) on which to fail; returns [na] otherwise *)
-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/pretyping.ml b/pretyping/pretyping.ml
index 4c3a001186..2d200ad27e 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,77 +366,21 @@ let orelse_name name name' = match name with
| Anonymous -> name'
| _ -> name
-(* Rename identifiers of the (initial part of) typing "rel" env *)
-(* according to a name substitution *)
-let ltac_interp_name_env k0 lvar env sigma =
- (* ctxt is the initial part of the env when pretype was called first *)
- (* (in practice k0 is probably 0, but we have to grant the
- specification of pretype which accepts to start with a non empty
- rel_context) *)
- 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 *)
@@ -525,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
@@ -545,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 =
@@ -563,29 +456,17 @@ let pretype_sort ?loc evdref = function
let new_type_evar env evdref loc =
let sigma = !evdref in
let (sigma, (e, _)) =
- Evarutil.new_type_evar env.ExtraEnv.env sigma
+ Evarutil.new_type_evar !!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
-
(* [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
@@ -599,7 +480,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) ->
@@ -610,13 +491,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
@@ -625,7 +505,6 @@ 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
@@ -634,39 +513,34 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
{ 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
+ 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
@@ -679,14 +553,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 _,newenv = push_rec_types !evdref (names,ftys) env in
let vdefj =
Array.map2_i
(fun i ctxt def ->
@@ -695,12 +569,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
@@ -722,13 +596,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
@@ -743,11 +617,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 =
@@ -763,7 +637,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 *) []
@@ -785,17 +659,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 ->
@@ -808,21 +682,21 @@ 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
@@ -835,40 +709,34 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
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
+ 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
@@ -879,33 +747,31 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
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.");
@@ -915,7 +781,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 ->
@@ -934,108 +800,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 =
@@ -1050,85 +905,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 ++
@@ -1138,19 +991,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 *)
@@ -1161,40 +1014,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;
@@ -1237,7 +1089,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/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0f22a1f0a0..3e19cfc8a6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -348,3 +348,13 @@ symmetry in H.
match goal with h:_ |- _ => assert (h=h) end. (* h should be H0 *)
exact (eq_refl H0).
Abort.
+
+(* Check that internal names used in "match" compilation to push "term
+ to match" on the environment are not interpreted as ltac variables *)
+
+Module ToMatchNames.
+Ltac g c := let r := constr:(match c return _ with a => 1 end) in idtac.
+Goal True.
+g 1.
+Abort.
+End ToMatchNames.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 01:09:41 +0000