aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/arguments_renaming.ml4
-rw-r--r--pretyping/cases.ml62
-rw-r--r--pretyping/coercion.ml1
-rw-r--r--pretyping/evarconv.ml34
-rw-r--r--pretyping/evardefine.ml8
-rw-r--r--pretyping/evarsolve.ml10
-rw-r--r--pretyping/find_subterm.ml4
-rw-r--r--pretyping/nativenorm.ml6
-rw-r--r--pretyping/pretyping.ml26
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/tacred.ml24
-rw-r--r--pretyping/typeclasses.ml18
-rw-r--r--pretyping/unification.ml20
-rw-r--r--pretyping/vnorm.ml8
15 files changed, 127 insertions, 112 deletions
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ca1d0b7fba..077ee4e150 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -13,6 +13,8 @@ open Term
open Environ
open Util
open Libobject
+
+module NamedDecl = Context.Named.Declaration
(*i*)
let name_table =
@@ -48,7 +50,7 @@ let discharge_rename_args = function
(try
let vars,_,_ = section_segment_of_reference c in
let c' = pop_global_reference c in
- let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+ let var_names = List.map (fst %> NamedDecl.get_id %> Name.mk_name) vars in
let names' = List.map (fun l -> var_names @ l) names in
Some (ReqGlobal (c', names), (c', names'))
with Not_found -> Some req)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0e659aec93..4cda689e9c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -32,6 +32,9 @@ open Evd
open Sigma.Notations
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* Pattern-matching errors *)
type pattern_matching_error =
@@ -604,7 +607,7 @@ let relocate_index_tomatch n1 n2 =
NonDepAlias :: genrec depth rest
| Abstract (i,d) :: rest ->
let i = relocate_rel n1 n2 depth i in
- Abstract (i, map_constr (relocate_index n1 n2 depth) d)
+ Abstract (i, RelDecl.map_constr (relocate_index n1 n2 depth) d)
:: genrec (depth+1) rest in
genrec 0
@@ -637,7 +640,7 @@ let replace_tomatch n c =
| NonDepAlias :: rest ->
NonDepAlias :: replrec depth rest
| Abstract (i,d) :: rest ->
- Abstract (i, map_constr (replace_term n c depth) d)
+ Abstract (i, RelDecl.map_constr (replace_term n c depth) d)
:: replrec (depth+1) rest in
replrec 0
@@ -662,7 +665,7 @@ let rec liftn_tomatch_stack n depth = function
NonDepAlias :: liftn_tomatch_stack n depth rest
| Abstract (i,d)::rest ->
let i = if i<depth then i else i+n in
- Abstract (i, map_constr (liftn n depth) d)
+ Abstract (i, RelDecl.map_constr (liftn n depth) d)
::(liftn_tomatch_stack n (depth+1) rest)
let lift_tomatch_stack n = liftn_tomatch_stack n 1
@@ -730,7 +733,7 @@ let get_names env sign eqns =
(* We now replace the names y1 .. yn y by the actual names *)
(* xi1 .. xin xi to be found in the i-th clause of the matrix *)
-let recover_initial_subpattern_names = List.map2 set_name
+let recover_initial_subpattern_names = List.map2 RelDecl.set_name
let recover_and_adjust_alias_names names sign =
let rec aux = function
@@ -755,11 +758,11 @@ let push_rels_eqn_with_names sign eqn =
push_rels_eqn sign eqn
let push_generalized_decl_eqn env n decl eqn =
- match get_name decl with
+ match RelDecl.get_name decl with
| Anonymous ->
push_rels_eqn [decl] eqn
| Name _ ->
- push_rels_eqn [set_name (get_name (Environ.lookup_rel n eqn.rhs.rhs_env)) decl] eqn
+ push_rels_eqn [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 }
@@ -767,7 +770,7 @@ let drop_alias_eqn eqn =
let push_alias_eqn alias eqn =
let aliasname = List.hd eqn.alias_stack in
let eqn = drop_alias_eqn eqn in
- let alias = set_name aliasname alias in
+ let alias = RelDecl.set_name aliasname alias in
push_rels_eqn [alias] eqn
(**********************************************************************)
@@ -1194,7 +1197,7 @@ let rec generalize_problem names pb = function
| LocalDef (Anonymous,_,_) -> pb', deps
| _ ->
(* for better rendering *)
- let d = map_type (whd_betaiota !(pb.evdref)) d in
+ let d = RelDecl.map_type (whd_betaiota !(pb.evdref)) d in
let tomatch = lift_tomatch_stack 1 pb'.tomatch in
let tomatch = relocate_index_tomatch (i+1) 1 tomatch in
{ pb' with
@@ -1222,7 +1225,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 names,aliasname = get_names pb.env cs_args eqns in
- let typs = List.map2 set_name names cs_args
+ let typs = List.map2 RelDecl.set_name names cs_args
in
(* We build the matrix obtained by expanding the matching on *)
@@ -1272,7 +1275,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
let typs' =
List.map2
(fun (tm, (tmtyp,_), decl) deps ->
- let na = get_name decl in
+ let na = RelDecl.get_name decl in
let na = match curname, na with
| Name _, Anonymous -> curname
| Name _, Name _ -> na
@@ -1656,8 +1659,7 @@ let abstract_tycon loc env evdref subst tycon extenv t =
List.map (fun a -> not (isRel a) || dependent a u
|| Int.Set.mem (destRel a) depvl) inst in
let named_filter =
- let open Context.Named.Declaration in
- List.map (fun d -> dependent (mkVar (get_id d)) u)
+ List.map (fun d -> dependent (mkVar (NamedDecl.get_id d)) u)
(named_context extenv) in
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = u :: List.map mkRel vl in
@@ -1753,7 +1755,7 @@ let build_inversion_problem loc env sigma tms t =
let sub_tms =
List.map2 (fun deps (tm, (tmtyp,_), decl) ->
- let na = if List.is_empty deps then Anonymous else force_name (get_name decl) in
+ let na = if List.is_empty deps then Anonymous else force_name (RelDecl.get_name decl) in
Pushed (true,((tm,tmtyp),deps,na)))
dep_sign decls in
let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
@@ -1816,7 +1818,7 @@ let build_initial_predicate arsign pred =
let rec buildrec n pred tmnames = function
| [] -> List.rev tmnames,pred
| (decl::realdecls)::lnames ->
- let na = get_name decl in
+ let na = RelDecl.get_name decl in
let n' = n + List.length realdecls in
buildrec (n'+1) pred (force_name na::tmnames) lnames
| _ -> assert false
@@ -1849,7 +1851,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
List.rev realnal
| None -> List.make nrealargs_ctxt Anonymous in
LocalAssum (na, build_dependent_inductive env0 indf')
- ::(List.map2 set_name realnal arsign) in
+ ::(List.map2 RelDecl.set_name realnal arsign) in
let rec buildrec n = function
| [],[] -> []
| (_,tm)::ltm, (_,x)::tmsign ->
@@ -1869,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
- let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in
+ let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
let subst, len =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
@@ -2046,7 +2048,7 @@ let constr_of_pat env evdref arsign pat avoid =
let patargs, args, sign, env, n, m, avoid =
List.fold_right2
(fun decl ua (patargs, args, sign, env, n, m, avoid) ->
- let t = get_type decl in
+ let t = RelDecl.get_type decl in
let pat', sign', arg', typ', argtypargs, n', avoid =
let liftt = liftn (List.length sign) (succ (List.length args)) t in
typ env (substl args liftt, []) ua avoid
@@ -2086,8 +2088,8 @@ let constr_of_pat env evdref arsign pat avoid =
(* Mark the equality as a hole *)
pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
in
- let pat', sign, patc, patty, args, z, avoid = typ env (get_type (List.hd arsign), List.tl arsign) pat avoid in
- pat', (sign, patc, (get_type (List.hd arsign), args), pat'), avoid
+ let pat', sign, patc, patty, args, z, avoid = typ env (RelDecl.get_type (List.hd arsign), List.tl arsign) pat avoid in
+ pat', (sign, patc, (RelDecl.get_type (List.hd arsign), args), pat'), avoid
(* shadows functional version *)
@@ -2118,7 +2120,7 @@ let vars_of_ctx ctx =
(GRef (Loc.ghost, delayed_force coq_eq_refl_ref, None)),
[hole; GVar (Loc.ghost, prev)])) :: vars
| _ ->
- match get_name decl with
+ match RelDecl.get_name decl with
Anonymous -> invalid_arg "vars_of_ctx"
| Name n -> n, GVar (Loc.ghost, n) :: vars)
ctx (Id.of_string "vars_of_ctx_error", [])
@@ -2295,7 +2297,7 @@ let abstract_tomatch env tomatchs tycon =
let build_dependent_signature env evdref avoid tomatchs arsign =
let avoid = ref avoid in
let arsign = List.rev arsign in
- let allnames = List.rev_map (List.map get_name) arsign in
+ let allnames = List.rev_map (List.map RelDecl.get_name) arsign in
let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
let eqs, neqs, refls, slift, arsign' =
List.fold_left2
@@ -2312,14 +2314,14 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
as much as possible *)
let argsign = List.tl arsign in (* arguments in inverse application order *)
let app_decl = List.hd arsign in (* The matched argument *)
- let appn = get_name app_decl in
- let appt = get_type app_decl in
+ let appn = RelDecl.get_name app_decl in
+ let appt = RelDecl.get_type app_decl in
let argsign = List.rev argsign in (* arguments in application order *)
let env', nargeqs, argeqs, refl_args, slift, argsign' =
List.fold_left2
(fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg decl ->
- let name = get_name decl in
- let t = get_type decl in
+ let name = RelDecl.get_name decl in
+ let t = RelDecl.get_type decl in
let argt = Retyping.get_type_of env !evdref arg in
let eq, refl_arg =
if Reductionops.is_conv env !evdref argt t then
@@ -2337,7 +2339,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
let previd, id =
let name =
match kind_of_term arg with
- Rel n -> get_name (lookup_rel n env)
+ Rel n -> RelDecl.get_name (lookup_rel n env)
| _ -> name
in
make_prime avoid name
@@ -2346,7 +2348,7 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
(LocalAssum (Name (eq_id avoid previd), eq)) :: argeqs,
refl_arg :: refl_args,
pred slift,
- set_name (Name id) decl :: argsign'))
+ RelDecl.set_name (Name id) decl :: argsign'))
(env, neqs, [], [], slift, []) args argsign
in
let eq = mk_JMeq evdref
@@ -2361,13 +2363,13 @@ let build_dependent_signature env evdref avoid tomatchs arsign =
succ nargeqs,
refl_eq :: refl_args,
pred slift,
- ((set_name (Name id) app_decl :: argsign') :: arsigns))
+ ((RelDecl.set_name (Name id) app_decl :: argsign') :: arsigns))
| _ -> (* Non dependent inductive or not inductive, just use a regular equality *)
let decl = match arsign with [x] -> x | _ -> assert(false) in
- let name = get_name decl in
+ let name = RelDecl.get_name decl in
let previd, id = make_prime avoid name in
- let arsign' = set_name (Name id) decl in
+ let arsign' = RelDecl.set_name (Name id) decl in
let tomatch_ty = type_of_tomatch ty in
let eq =
mk_eq evdref (lift nar tomatch_ty)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 98dea9fc9a..2b860ae9c5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -153,7 +153,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env evdref x y in
let dest_prod c =
- let open Context.Rel.Declaration in
match Reductionops.splay_prod_n env ( !evdref) 1 c with
| [LocalAssum (na,t) | LocalDef (na,_,t)], c -> (na,t), c
| _ -> raise NoSubtacCoercion
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 26af90958b..cd7ce89e0f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -24,7 +24,10 @@ open Globnames
open Evd
open Pretype_errors
open Sigma.Notations
-open Context.Rel.Declaration
+open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
type unify_fun = transparent_state ->
env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
@@ -58,14 +61,13 @@ let eval_flexible_term ts env evd c =
else None
| Rel n ->
(try match lookup_rel n env with
- | LocalAssum _ -> None
- | LocalDef (_,v,_) -> Some (lift n v)
+ | RelDecl.LocalAssum _ -> None
+ | RelDecl.LocalDef (_,v,_) -> Some (lift n v)
with Not_found -> None)
| Var id ->
(try
if is_transparent_variable ts id then
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ env |> lookup_named id |> NamedDecl.get_value
else None
with Not_found -> None)
| LetIn (_,b,_,c) -> Some (subst1 b c)
@@ -394,7 +396,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
assert (match sk with [] -> true | _ -> false);
let (na,c1,c'1) = destLambda term in
let c = nf_evar evd c1 in
- let env' = push_rel (LocalAssum (na,c)) env in
+ let env' = push_rel (RelDecl.LocalAssum (na,c)) env in
let out1 = whd_betaiota_deltazeta_for_iota_state
(fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
let out2 = whd_nored_state evd
@@ -600,7 +602,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let b = nf_evar i b1 in
let t = nf_evar i t1 in
let na = Nameops.name_max na1 na2 in
- evar_conv_x ts (push_rel (LocalDef (na,b,t)) env) i pbty c'1 c'2);
+ evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
and f2 i =
let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1)
@@ -715,7 +717,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(fun i ->
let c = nf_evar i c1 in
let na = Nameops.name_max na1 na2 in
- evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i CONV c'1 c'2)]
+ evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
| Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
| Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1
@@ -774,7 +776,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
(fun i ->
let c = nf_evar i c1 in
let na = Nameops.name_max n1 n2 in
- evar_conv_x ts (push_rel (LocalAssum (na,c)) env) i pbty c'1 c'2)]
+ evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
| Rel x1, Rel x2 ->
if Int.equal x1 x2 then
@@ -951,7 +953,6 @@ let choose_less_dependent_instance evk evd term args =
| [] -> None
| (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
-open Context.Named.Declaration
let apply_on_subterm env evdref f c t =
let rec applyrec (env,(k,c) as acc) t =
(* By using eq_constr, we make an approximation, for instance, we *)
@@ -982,14 +983,16 @@ let filter_possible_projections c ty ctxt args =
List.map_i (fun i decl ->
let () = assert (i < len) in
let a = Array.unsafe_get args i in
- (match decl with LocalAssum _ -> false | LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
+ (match decl with
+ | NamedDecl.LocalAssum _ -> false
+ | NamedDecl.LocalDef (_,c,_) -> not (isRel c || isVar c)) ||
a == c ||
(* Here we make an approximation, for instance, we could also be *)
(* interested in finding a term u convertible to c such that a occurs *)
(* in u *)
isRel a && Int.Set.mem (destRel a) fv1 ||
isVar a && Id.Set.mem (destVar a) fv2 ||
- Id.Set.mem (get_id decl) tyvars)
+ Id.Set.mem (NamedDecl.get_id decl) tyvars)
0 ctxt
let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
@@ -1020,10 +1023,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let env_evar = evar_filtered_env evi in
let sign = named_context_val env_evar in
let ctxt = evar_filtered_context evi in
- let instance = List.map mkVar (List.map get_id ctxt) in
+ let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in
let rec make_subst = function
- | decl'::ctxt', c::l, occs::occsl when isVarId (get_id decl') c ->
+ | decl'::ctxt', c::l, occs::occsl when isVarId (NamedDecl.get_id decl') c ->
begin match occs with
| Some _ ->
error "Cannot force abstraction on identity instance."
@@ -1031,7 +1034,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
make_subst (ctxt',l,occsl)
end
| decl'::ctxt', c::l, occs::occsl ->
- let (id,_,t) = to_tuple decl' in
+ let id = NamedDecl.get_id decl' in
+ let t = NamedDecl.get_type decl' in
let evs = ref [] in
let ty = Retyping.get_type_of env_rhs evd c in
let filter' = filter_possible_projections c ty ctxt args in
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index b91ae6c724..06f619410c 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -19,21 +19,21 @@ open Evarutil
open Pretype_errors
open Sigma.Notations
+module RelDecl = Context.Rel.Declaration
+
let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
let evd = Sigma.Unsafe.of_evar_map evd in
let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
(Sigma.to_evar_map evd, evk)
let env_nf_evar sigma env =
- let open Context.Rel.Declaration in
process_rel_context
- (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env
+ (fun d e -> push_rel (RelDecl.map_constr (nf_evar sigma) d) e) env
let env_nf_betaiotaevar sigma env =
- let open Context.Rel.Declaration in
process_rel_context
(fun d e ->
- push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env
+ push_rel (RelDecl.map_constr (Reductionops.nf_betaiota sigma) d) e) env
(****************************************)
(* Operations on value/type constraints *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6c8677855a..a744f5ec61 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -169,7 +169,7 @@ type 'a update =
| NoUpdate
open Context.Named.Declaration
-let inst_of_vars sign = Array.map_of_list (mkVar % get_id) sign
+let inst_of_vars sign = Array.map_of_list (get_id %> mkVar) sign
let restrict_evar_key evd evk filter candidates =
match filter, candidates with
@@ -632,13 +632,13 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
~status:univ_flexible (Some false) env evd (mkSort s) in
define_evar_from_virtual_equation define_fun env evd src t_in_env
ty_t_in_sign sign filter inst_in_env in
- let evd,b_in_sign = match d with
- | LocalAssum _ -> evd,None
+ let evd,d' = match d with
+ | LocalAssum _ -> evd, Context.Named.Declaration.LocalAssum (id,t_in_sign)
| LocalDef (_,b,_) ->
let evd,b = define_evar_from_virtual_equation define_fun env evd src b
t_in_sign sign filter inst_in_env in
- evd,Some b in
- (push_named_context_val (Context.Named.Declaration.of_tuple (id,b_in_sign,t_in_sign)) sign, Filter.extend 1 filter,
+ evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in
+ (push_named_context_val d' sign, Filter.extend 1 filter,
(mkRel 1)::(List.map (lift 1) inst_in_env),
(mkRel 1)::(List.map (lift 1) inst_in_sign),
push_rel d env,evd,id::avoid))
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 38b6075e5a..4b9cf415f0 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -16,6 +16,8 @@ open Nameops
open Termops
open Pretype_errors
+module NamedDecl = Context.Named.Declaration
+
(** Processing occurrences *)
type occurrence_error =
@@ -61,7 +63,7 @@ let proceed_with_occurrences f occs x =
let map_named_declaration_with_hyploc f hyploc acc decl =
let open Context.Named.Declaration in
- let f = f (Some (get_id decl, hyploc)) in
+ let f = f (Some (NamedDecl.get_id decl, hyploc)) in
match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->
error_occurrences_error (IncorrectInValueOccurrence id)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0dd64697c6..1e5f12b209 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -20,6 +20,8 @@ open Nativecode
open Nativevalues
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+
(** This module implements normalization by evaluation to OCaml code *)
exception Find_at of int
@@ -122,7 +124,7 @@ let build_case_type dep p realargs c =
(* TODO move this function *)
let type_of_rel env n =
- lookup_rel n env |> get_type |> lift n
+ env |> lookup_rel n |> RelDecl.get_type |> lift n
let type_of_prop = mkSort type1_sort
@@ -133,7 +135,7 @@ let type_of_sort s =
let type_of_var env id =
let open Context.Named.Declaration in
- try lookup_named id env |> get_type
+ try env |> lookup_named id |> get_type
with Not_found ->
anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound")
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 3e65363d68..385e100e2d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,7 +44,8 @@ open Evarconv
open Pattern
open Misctypes
open Sigma.Notations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
type var_map = constr_under_binders Id.Map.t
@@ -104,7 +105,7 @@ let lookup_named id env = lookup_named id env.env
let e_new_evar env evdref ?src ?naming typ =
let subst2 subst vsubst c = csubst_subst subst (replace_vars vsubst c) in
let open Context.Named.Declaration in
- let inst_vars = List.map (fun d -> mkVar (get_id d)) (named_context env.env) 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, vsubst, _, nc) = Lazy.force env.extra in
let typ' = subst2 subst vsubst typ in
@@ -403,9 +404,10 @@ let ltac_interp_name_env k0 lvar env =
(* tail is the part of the env enriched by pretyping *)
let n = Context.Rel.length (rel_context env) - k0 in
let ctxt,_ = List.chop n (rel_context env) in
- let env = pop_rel_context n env in
- let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in
- push_rel_context ctxt env
+ let open Context.Rel.Declaration in
+ let ctxt' = List.smartmap (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 ctxt' (pop_rel_context n env)
let invert_ltac_bound_name lvar env id0 id =
let id' = Id.Map.find id lvar.ltac_idents in
@@ -460,7 +462,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
end;
(* Check if [id] is a section or goal variable *)
try
- { uj_val = mkVar id; uj_type = (get_type (lookup_named id env)) }
+ { 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
@@ -505,7 +507,7 @@ let pretype_ref loc evdref env ref us =
match ref with
| VarRef id ->
(* Section variable *)
- (try make_judge (mkVar id) (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
@@ -803,8 +805,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let j = pretype_type empty_valcon env evdref lvar c2 in
{ j with utj_val = lift 1 j.utj_val }
| Name _ ->
- let var = (name,j.utj_val) in
- let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in
+ let var = LocalAssum (name, j.utj_val) in
+ let env' = push_rel var env in
pretype_type empty_valcon env' evdref lvar c2
in
let name = ltac_interp_name lvar name in
@@ -1043,8 +1045,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
let f decl (subst,update) =
- let id = get_id decl in
- let t = replace_vars subst (get_type decl) in
+ 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
@@ -1056,7 +1058,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
if is_conv env.ExtraEnv.env !evdref t t' then mkRel n, update else raise Not_found
with Not_found ->
try
- let t' = lookup_named id env |> get_type in
+ 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
with Not_found ->
user_err ~loc (str "Cannot interpret " ++
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ba1b4a10a7..7ee70d9e0d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -790,11 +790,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma =
(h 0 (str "<<" ++ Termops.print_constr x ++
str "|" ++ cut () ++ Cst_stack.pr cst_l ++
str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++
- str ">>") ++ fnl ())
+ str ">>"))
in
let fold () =
let () = if !debug_RAKAM then
- let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in
+ let open Pp in Feedback.msg_notice (str "<><><><><>") in
(s,cst_l)
in
match kind_of_term x with
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 98b36fb92f..5b67af3e73 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -20,6 +20,9 @@ open Termops
open Arguments_renaming
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
type retype_error =
| NotASort
| NotAnArity
@@ -78,8 +81,7 @@ let sort_of_atomic_type env sigma ft args =
in concl_of_arity env 0 ft (Array.to_list args)
let type_of_var env id =
- let open Context.Named.Declaration in
- try get_type (lookup_named id env)
+ try NamedDecl.get_type (lookup_named id env)
with Not_found -> retype_error (BadVariable id)
let decomp_sort env sigma t =
@@ -94,7 +96,7 @@ let retype ?(polyprop=true) sigma =
(try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
with Not_found -> retype_error (BadMeta n))
| Rel n ->
- let ty = get_type (lookup_rel n env) in
+ let ty = RelDecl.get_type (lookup_rel n env) in
lift n ty
| Var id -> type_of_var env id
| Const cst -> rename_type_of_constant env cst
@@ -239,7 +241,7 @@ let sorts_of_context env evc ctxt =
| [] -> env,[]
| d :: ctxt ->
let env,sorts = aux ctxt in
- let s = get_sort_of env evc (get_type d) in
+ let s = get_sort_of env evc (RelDecl.get_type d) in
(push_rel d env,s::sorts) in
snd (aux ctxt)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index bb883b29f1..7da7385089 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -25,6 +25,9 @@ open Patternops
open Locus
open Sigma.Notations
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(* Errors *)
type reduction_tactic_error =
@@ -54,13 +57,12 @@ let is_evaluable env = function
| EvalVarRef id -> is_evaluable_var env id
let value_of_evaluable_ref env evref u =
- let open Context.Named.Declaration in
match evref with
| EvalConstRef con ->
(try constant_value_in env (con,u)
with NotEvaluableConst IsProj ->
raise (Invalid_argument "value_of_evaluable_ref"))
- | EvalVarRef id -> lookup_named id env |> get_value |> Option.get
+ | EvalVarRef id -> env |> lookup_named id |> NamedDecl.get_value |> Option.get
let evaluable_of_global_reference env = function
| ConstRef cst when is_evaluable_const env cst -> EvalConstRef cst
@@ -112,22 +114,18 @@ let unsafe_reference_opt_value env sigma eval =
| Declarations.Def c -> Some (Mod_subst.force_constr c)
| _ -> None)
| EvalVar id ->
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ env |> lookup_named id |> NamedDecl.get_value
| EvalRel n ->
- let open Context.Rel.Declaration in
- lookup_rel n env |> map_value (lift n) |> get_value
+ env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value
| EvalEvar ev -> Evd.existential_opt_value sigma ev
let reference_opt_value env sigma eval u =
match eval with
| EvalConst cst -> constant_opt_value_in env (cst,u)
| EvalVar id ->
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ env |> lookup_named id |> NamedDecl.get_value
| EvalRel n ->
- let open Context.Rel.Declaration in
- lookup_rel n env |> map_value (lift n) |> get_value
+ env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value
| EvalEvar ev -> Evd.existential_opt_value sigma ev
exception NotEvaluable
@@ -541,11 +539,9 @@ let match_eval_ref_value env sigma constr =
| Const (sp, u) when is_evaluable env (EvalConstRef sp) ->
Some (constant_value_in env (sp, u))
| Var id when is_evaluable env (EvalVarRef id) ->
- let open Context.Named.Declaration in
- lookup_named id env |> get_value
+ env |> lookup_named id |> NamedDecl.get_value
| Rel n ->
- let open Context.Rel.Declaration in
- lookup_rel n env |> map_value (lift n) |> get_value
+ env |> lookup_rel n |> RelDecl.map_value (lift n) |> RelDecl.get_value
| Evar ev -> Evd.existential_opt_value sigma ev
| _ -> None
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2c675b9eae..4c33a9c789 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -17,6 +17,9 @@ open Util
open Typeclasses_errors
open Libobject
open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
(*i*)
let typeclasses_unique_solutions = ref false
@@ -181,7 +184,7 @@ let subst_class (subst,cl) =
let do_subst_con c = Mod_subst.subst_constant subst c
and do_subst c = Mod_subst.subst_mps subst c
and do_subst_gr gr = fst (subst_global subst gr) in
- let do_subst_ctx = List.smartmap (map_constr do_subst) in
+ let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
let do_subst_context (grs,ctx) =
List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
do_subst_ctx ctx in
@@ -197,19 +200,16 @@ let subst_class (subst,cl) =
let discharge_class (_,cl) =
let repl = Lib.replacement_context () in
let rel_of_variable_context ctx = List.fold_right
- ( fun (n,_,b,t) (ctx', subst) ->
- let decl = match b with
- | None -> LocalAssum (Name n, substn_vars 1 subst t)
- | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t)
- in
- (decl :: ctx', n :: subst)
+ ( fun (decl,_) (ctx', subst) ->
+ let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
+ (decl' :: ctx', NamedDecl.get_id decl :: subst)
) ctx ([], []) in
let discharge_rel_context subst n rel =
let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
let ctx, _ =
List.fold_right
(fun decl (ctx, k) ->
- map_constr (substn_vars k subst) decl :: ctx, succ k
+ RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
)
rel ([], n)
in ctx
@@ -222,7 +222,7 @@ let discharge_class (_,cl) =
let discharge_context ctx' subst (grs, ctx) =
let grs' =
let newgrs = List.map (fun decl ->
- match decl |> get_type |> class_of_constr with
+ match decl |> RelDecl.get_type |> class_of_constr with
| None -> None
| Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
ctx'
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bc009e50a2..8feb34e3e8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -29,7 +29,9 @@ open Locus
open Locusops
open Find_subterm
open Sigma.Notations
-open Context.Named.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
let keyed_unification = ref (false)
let _ = Goptions.declare_bool_option {
@@ -78,9 +80,8 @@ let occur_meta_evd sigma mv c =
let abstract_scheme env evd c l lname_typ =
List.fold_left2
(fun (t,evd) (locc,a) decl ->
- let open Context.Rel.Declaration in
- let na = get_name decl in
- let ta = get_type decl in
+ let na = RelDecl.get_name decl in
+ let ta = RelDecl.get_type decl in
let na = match kind_of_term a with Var id -> Name id | _ -> na in
(* [occur_meta ta] test removed for support of eelim/ecase but consequences
are unclear...
@@ -1080,8 +1081,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
if !debug_unification then Feedback.msg_debug (str "Leaving unification with success");
a
with e ->
+ let e = CErrors.push e in
if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure");
- raise e
+ iraise e
let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env
@@ -1472,10 +1474,10 @@ let indirectly_dependent c d decls =
it is needed otherwise, as e.g. when abstracting over "2" in
"forall H:0=2, H=H:>(0=1+1) -> 0=2." where there is now obvious
way to see that the second hypothesis depends indirectly over 2 *)
- List.exists (fun d' -> dependent_in_decl (mkVar (get_id d')) d) decls
+ List.exists (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) decls
let indirect_dependency d decls =
- decls |> List.filter (fun d' -> dependent_in_decl (mkVar (get_id d')) d) |> List.hd |> get_id
+ decls |> List.filter (fun d' -> dependent_in_decl (mkVar (NamedDecl.get_id d')) d) |> List.hd |> NamedDecl.get_id
let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) =
let current_sigma = Sigma.to_evar_map current_sigma in
@@ -1594,7 +1596,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let likefirst = clause_with_generic_occurrences occs in
let mkvarid () = mkVar id in
let compute_dependency _ d (sign,depdecls) =
- let hyp = get_id d in
+ let hyp = NamedDecl.get_id d in
match occurrences_of_hyp hyp occs with
| NoOccurrences, InHyp ->
if indirectly_dependent c d depdecls then
@@ -1631,7 +1633,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
replace_term_occ_modulo occ test mkvarid concl
in
let lastlhyp =
- if List.is_empty depdecls then None else Some (get_id (List.last depdecls)) in
+ if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in
let res = match out test with
| None -> None
| Some (sigma, c) -> Some (Sigma.Unsafe.of_pair (c, sigma))
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c396f593bb..331ad0912f 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -17,6 +17,9 @@ open Reduction
open Vm
open Context.Rel.Declaration
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
(*******************************************)
(* Calcul de la forme normal d'un terme *)
(*******************************************)
@@ -203,12 +206,11 @@ and constr_type_of_idkey env (idkey : Vars.id_key) stk =
in
nf_univ_args ~nb_univs mk env stk
| VarKey id ->
- let open Context.Named.Declaration in
- let ty = get_type (lookup_named id env) in
+ let ty = NamedDecl.get_type (lookup_named id env) in
nf_stk env (mkVar id) ty stk
| RelKey i ->
let n = (nb_rel env - i) in
- let ty = get_type (lookup_rel n env) in
+ let ty = RelDecl.get_type (lookup_rel n env) in
nf_stk env (mkRel n) (lift n ty) stk
and nf_stk ?from:(from=0) env c t stk =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:29:58 +0000