aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml5
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/cbv.mli2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/constr_matching.ml49
-rw-r--r--pretyping/detyping.ml163
-rw-r--r--pretyping/detyping.mli7
-rw-r--r--pretyping/evarconv.ml36
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evardefine.ml12
-rw-r--r--pretyping/evarsolve.ml59
-rw-r--r--pretyping/evarsolve.mli2
-rw-r--r--pretyping/glob_ops.ml2
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--pretyping/nativenorm.ml6
-rw-r--r--pretyping/patternops.ml134
-rw-r--r--pretyping/pretyping.ml10
-rw-r--r--pretyping/reductionops.ml23
-rw-r--r--pretyping/reductionops.mli4
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/typing.ml9
-rw-r--r--pretyping/typing.mli2
-rw-r--r--pretyping/unification.ml32
-rw-r--r--pretyping/vnorm.ml6
27 files changed, 340 insertions, 253 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 73be9d6b78..4c87b4e7ed 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1015,7 +1015,7 @@ let adjust_impossible_cases pb pred tomatch submat =
| Evar (evk,_) when snd (evar_source evk !(pb.evdref)) == Evar_kinds.ImpossibleCase ->
if not (Evd.is_defined !(pb.evdref) evk) then begin
let evd, default = use_unit_judge !(pb.evdref) in
- pb.evdref := Evd.define evk (EConstr.Unsafe.to_constr default.uj_type) evd
+ pb.evdref := Evd.define evk default.uj_type evd
end;
add_assert_false_case pb tomatch
| _ ->
@@ -2581,7 +2581,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
- uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); }
+ (* XXX: is this normalization needed? *)
+ uj_type = Evarutil.nf_evar !evdref tycon; }
in j
(**************************************************************************)
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index a2155697ec..cb0fc32575 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -71,7 +71,7 @@ and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
| CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
- | PROJ of projection * Declarations.projection_body * cbv_stack
+ | PROJ of Projection.t * Declarations.projection_body * cbv_stack
(* les vars pourraient etre des constr,
cela permet de retarder les lift: utile ?? *)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 2ac59911c7..cdaa39c53c 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -41,7 +41,7 @@ and cbv_stack =
| TOP
| APP of cbv_value array * cbv_stack
| CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
- | PROJ of projection * Declarations.projection_body * cbv_stack
+ | PROJ of Projection.t * Declarations.projection_body * cbv_stack
val shift_value : int -> cbv_value -> cbv_value
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 04cb6a59fb..6dc3687a0a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -251,7 +251,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
let (n, dom, rng) = destLambda !evdref t in
if isEvar !evdref dom then
let (domk, args) = destEvar !evdref dom in
- evdref := define domk (EConstr.Unsafe.to_constr a) !evdref;
+ evdref := define domk a !evdref;
else ();
t, rng
| _ -> raise NoSubtacCoercion
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 888c76e3d9..89d490a410 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -183,9 +183,36 @@ let push_binder na1 na2 t ctx =
Namegen.next_ident_away Namegen.default_non_dependent_ident avoid in
(na1, id2, t) :: ctx
-let to_fix (idx, (nas, cs, ts)) =
- let inj = EConstr.of_constr in
- (idx, (nas, Array.map inj cs, Array.map inj ts))
+(* This is an optimization of the main pattern-matching which shares
+ the longest common prefix of the body and type of a fixpoint. The
+ only practical effect at the time of writing is in binding variable
+ names: these variable names must be bound only once since the user
+ view at a fix displays only a (maximal) shared common prefix *)
+
+let rec match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env' subst t1 t2 b1 b2 =
+ match t1, EConstr.kind sigma t2, b1, EConstr.kind sigma b2 with
+ | PProd(na1,c1,t1'), Prod(na2,c2,t2'), PLambda (_,c1',b1'), Lambda (na2',c2',b2') ->
+ let ctx = push_binder na1 na2 c2 ctx in
+ let ctx' = push_binder na1 na2' c2' ctx' in
+ let env = EConstr.push_rel (LocalAssum (na2,c2)) env in
+ let subst = sorec ctx env subst c1 c2 in
+ let subst = sorec ctx env subst c1' c2' in
+ let subst = add_binders na1 na2 binding_vars subst in
+ match_under_common_fix_binders sorec sigma binding_vars
+ ctx ctx' env env' subst t1' t2' b1' b2'
+ | PLetIn(na1,c1,u1,t1), LetIn(na2,c2,u2,t2), PLetIn(_,c1',u1',b1), LetIn(na2',c2',u2',b2) ->
+ let ctx = push_binder na1 na2 u2 ctx in
+ let ctx' = push_binder na1 na2' u2' ctx' in
+ let env = EConstr.push_rel (LocalDef (na2,c2,t2)) env in
+ let subst = sorec ctx env subst c1 c2 in
+ let subst = sorec ctx env subst c1' c2' in
+ let subst = Option.fold_left (fun subst u1 -> sorec ctx env subst u1 u2) subst u1 in
+ let subst = Option.fold_left (fun subst u1' -> sorec ctx env subst u1' u2') subst u1' in
+ let subst = add_binders na1 na2 binding_vars subst in
+ match_under_common_fix_binders sorec sigma binding_vars
+ ctx ctx' env env' subst t1 t2 b1 b2
+ | _ ->
+ sorec ctx' env' (sorec ctx env subst t1 t2) b1 b2
let merge_binding sigma allow_bound_rels ctx n cT subst =
let c = match ctx with
@@ -364,8 +391,20 @@ let matches_core env sigma allow_bound_rels
let chk_head = sorec ctx env (sorec ctx env subst a1 a2) p1 p2 in
List.fold_left chk_branch chk_head br1
- | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst
- | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst
+ | PFix ((ln1,i1),(lna1,tl1,bl1)), Fix ((ln2,i2),(lna2,tl2,bl2))
+ when Array.equal Int.equal ln1 ln2 && i1 = i2 ->
+ let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
+ let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
+ let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
+ Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
+
+ | PCoFix (i1,(lna1,tl1,bl1)), CoFix (i2,(lna2,tl2,bl2))
+ when i1 = i2 ->
+ let ctx' = Array.fold_left3 (fun ctx na1 na2 t2 -> push_binder na1 na2 t2 ctx) ctx lna1 lna2 tl2 in
+ let env' = Array.fold_left2 (fun env na2 c2 -> EConstr.push_rel (LocalAssum (na2,c2)) env) env lna2 tl2 in
+ let subst = Array.fold_left4 (match_under_common_fix_binders sorec sigma binding_vars ctx ctx' env env') subst tl1 tl2 bl1 bl2 in
+ Array.fold_left2 (fun subst na1 na2 -> add_binders na1 na2 binding_vars subst) subst lna1 lna2
+
| PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 ->
Array.fold_left2 (sorec ctx env) subst args1 args2
| (PRef _ | PVar _ | PRel _ | PApp _ | PProj _ | PLambda _
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 587892141c..bb563220b6 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -501,6 +501,97 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
let eqnl = detype_eqns constructs constagsl bl in
GCases (tag,pred,[tomatch,(alias,aliastyp)],eqnl)
+let rec share_names detype n l avoid env sigma c t =
+ match EConstr.kind sigma c, EConstr.kind sigma t with
+ (* factorize even when not necessary to have better presentation *)
+ | Lambda (na,t,c), Prod (na',t',c') ->
+ let na = match (na,na') with
+ Name _, _ -> na
+ | _, Name _ -> na'
+ | _ -> na in
+ let t' = detype avoid env sigma t in
+ let id = next_name_away na avoid in
+ let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
+ share_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+ (* May occur for fix built interactively *)
+ | LetIn (na,b,t',c), _ when n > 0 ->
+ let t'' = detype avoid env sigma t' in
+ let b' = detype avoid env sigma b in
+ let id = next_name_away na avoid in
+ let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
+ share_names detype n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+ (* Only if built with the f/n notation or w/o let-expansion in types *)
+ | _, LetIn (_,b,_,t) when n > 0 ->
+ share_names detype n l avoid env sigma c (subst1 b t)
+ (* If it is an open proof: we cheat and eta-expand *)
+ | _, Prod (na',t',c') when n > 0 ->
+ let t'' = detype avoid env sigma t' in
+ let id = next_name_away na' avoid in
+ let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
+ let appc = mkApp (lift 1 c,[|mkRel 1|]) in
+ share_names detype (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+ (* If built with the f/n notation: we renounce to share names *)
+ | _ ->
+ if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+ let c = detype avoid env sigma c in
+ let t = detype avoid env sigma t in
+ (List.rev l,c,t)
+
+let rec share_pattern_names detype n l avoid env sigma c t =
+ let open Pattern in
+ if n = 0 then
+ let c = detype avoid env sigma c in
+ let t = detype avoid env sigma t in
+ (List.rev l,c,t)
+ else match c, t with
+ | PLambda (na,t,c), PProd (na',t',c') ->
+ let na = match (na,na') with
+ Name _, _ -> na
+ | _, Name _ -> na'
+ | _ -> na in
+ let t' = detype avoid env sigma t in
+ let id = next_name_away na avoid in
+ let avoid = Id.Set.add id avoid in
+ let env = Name id :: env in
+ share_pattern_names detype (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+ | _ ->
+ if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
+ let c = detype avoid env sigma c in
+ let t = detype avoid env sigma t in
+ (List.rev l,c,t)
+
+let detype_fix detype avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+ let def_avoid, def_env, lfi =
+ Array.fold_left2
+ (fun (avoid, env, l) na ty ->
+ let id = next_name_away na avoid in
+ (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+ (avoid, env, []) names tys in
+ let n = Array.length tys in
+ let v = Array.map3
+ (fun c t i -> share_names detype (i+1) [] def_avoid def_env sigma c (lift n t))
+ bodies tys vn in
+ GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+
+let detype_cofix detype avoid env sigma n (names,tys,bodies) =
+ let def_avoid, def_env, lfi =
+ Array.fold_left2
+ (fun (avoid, env, l) na ty ->
+ let id = next_name_away na avoid in
+ (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
+ (avoid, env, []) names tys in
+ let ntys = Array.length tys in
+ let v = Array.map2
+ (fun c t -> share_names detype 0 [] def_avoid def_env sigma c (lift ntys t))
+ bodies tys in
+ GRec(GCoFix n,Array.of_list (List.rev lfi),
+ Array.map (fun (bl,_,_) -> bl) v,
+ Array.map (fun (_,_,ty) -> ty) v,
+ Array.map (fun (_,bd,_) -> bd) v)
+
let detype_universe sigma u =
let fn (l, n) = Some (Termops.reference_of_level sigma l, n) in
Univ.Universe.map fn u
@@ -655,76 +746,8 @@ and detype_r d flags avoid env sigma t =
(ci.ci_ind,ci.ci_pp_info.style,
ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
p c bl
- | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
- | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef
-
-and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
- let def_avoid, def_env, lfi =
- Array.fold_left2
- (fun (avoid, env, l) na ty ->
- let id = next_name_away na avoid in
- (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
- (avoid, env, []) names tys in
- let n = Array.length tys in
- let v = Array.map3
- (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t))
- bodies tys vn in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
- Array.map (fun (bl,_,_) -> bl) v,
- Array.map (fun (_,_,ty) -> ty) v,
- Array.map (fun (_,bd,_) -> bd) v)
-
-and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
- let def_avoid, def_env, lfi =
- Array.fold_left2
- (fun (avoid, env, l) na ty ->
- let id = next_name_away na avoid in
- (Id.Set.add id avoid, add_name (Name id) None ty env, id::l))
- (avoid, env, []) names tys in
- let ntys = Array.length tys in
- let v = Array.map2
- (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t))
- bodies tys in
- GRec(GCoFix n,Array.of_list (List.rev lfi),
- Array.map (fun (bl,_,_) -> bl) v,
- Array.map (fun (_,_,ty) -> ty) v,
- Array.map (fun (_,bd,_) -> bd) v)
-
-and share_names d flags n l avoid env sigma c t =
- match EConstr.kind sigma c, EConstr.kind sigma t with
- (* factorize even when not necessary to have better presentation *)
- | Lambda (na,t,c), Prod (na',t',c') ->
- let na = match (na,na') with
- Name _, _ -> na
- | _, Name _ -> na'
- | _ -> na in
- let t' = detype d flags avoid env sigma t in
- let id = next_name_away na avoid in
- let avoid = Id.Set.add id avoid and env = add_name (Name id) None t env in
- share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
- (* May occur for fix built interactively *)
- | LetIn (na,b,t',c), _ when n > 0 ->
- let t'' = detype d flags avoid env sigma t' in
- let b' = detype d flags avoid env sigma b in
- let id = next_name_away na avoid in
- let avoid = Id.Set. add id avoid and env = add_name (Name id) (Some b) t' env in
- share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
- (* Only if built with the f/n notation or w/o let-expansion in types *)
- | _, LetIn (_,b,_,t) when n > 0 ->
- share_names d flags n l avoid env sigma c (subst1 b t)
- (* If it is an open proof: we cheat and eta-expand *)
- | _, Prod (na',t',c') when n > 0 ->
- let t'' = detype d flags avoid env sigma t' in
- let id = next_name_away na' avoid in
- let avoid = Id.Set.add id avoid and env = add_name (Name id) None t' env in
- let appc = mkApp (lift 1 c,[|mkRel 1|]) in
- share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
- (* If built with the f/n notation: we renounce to share names *)
- | _ ->
- if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
- let c = detype d flags avoid env sigma c in
- let t = detype d flags avoid env sigma t in
- (List.rev l,c,t)
+ | Fix (nvn,recdef) -> detype_fix (detype d flags) avoid env sigma nvn recdef
+ | CoFix (n,recdef) -> detype_cofix (detype d flags) avoid env sigma n recdef
and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
try
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 32b94e1b03..817b8ba6e8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -56,6 +56,13 @@ val detype_sort : evar_map -> Sorts.t -> glob_sort
val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> (names_context * env) ->
evar_map -> rel_context -> 'a glob_decl_g list
+val share_pattern_names :
+ (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int ->
+ (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list ->
+ Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern ->
+ Pattern.constr_pattern ->
+ (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a
+
val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr
(** look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d37090a653..144166a343 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -114,9 +114,6 @@ let flex_kind_of_term ts env evd c sk =
| Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
| Cast _ | App _ | Case _ -> assert false
-let add_conv_pb (pb, env, x, y) sigma =
- Evd.add_conv_pb (pb, env, EConstr.Unsafe.to_constr x, EConstr.Unsafe.to_constr y) sigma
-
let apprec_nohdbeta ts env evd c =
let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in
if Stack.not_purely_applicative sk
@@ -1045,7 +1042,7 @@ let choose_less_dependent_instance evk evd term args =
let subst' = List.filter (fun (id,c) -> EConstr.eq_constr evd c term) subst in
match subst' with
| [] -> None
- | (id, _) :: _ -> Some (Evd.define evk (Constr.mkVar id) evd)
+ | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
let apply_on_subterm env evdref f c t =
let rec applyrec (env,(k,c) as acc) t =
@@ -1085,7 +1082,7 @@ let filter_possible_projections evd c ty ctxt args =
let a = Array.unsafe_get args i in
(match decl with
| NamedDecl.LocalAssum _ -> false
- | NamedDecl.LocalDef (_,c,_) -> not (isRel evd (EConstr.of_constr c) || isVar evd (EConstr.of_constr c))) ||
+ | NamedDecl.LocalDef (_,c,_) -> not (isRel evd c || isVar evd 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 *)
@@ -1135,7 +1132,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
end
| decl'::ctxt', c::l, occs::occsl ->
let id = NamedDecl.get_id decl' in
- let t = EConstr.of_constr (NamedDecl.get_type 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 evd c ty ctxt args in
@@ -1183,7 +1180,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(* We force abstraction over this unconstrained occurrence *)
(* and we use typing to propagate this instantiation *)
(* This is an arbitrary choice *)
- let evd = Evd.define evk (Constr.mkVar id) evd in
+ let evd = Evd.define evk (mkVar id) evd in
match evar_conv_x ts env_evar evd CUMUL idty evty with
| UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
| Success evd ->
@@ -1205,14 +1202,11 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(evar_conv_x full_transparent_state)
with IllTypedInstance _ -> raise (TypingFailed evd)
in
- Evd.define evk (EConstr.Unsafe.to_constr rhs) evd
+ Evd.define evk rhs evd
in
abstract_free_holes evd subst, true
with TypingFailed evd -> evd, false
-let to_pb (pb, env, t1, t2) =
- (pb, env, EConstr.Unsafe.to_constr t1, EConstr.Unsafe.to_constr t2)
-
let second_order_matching_with_args ts env evd pbty ev l t =
(*
let evd,ev = evar_absorb_arguments env evd ev l in
@@ -1222,7 +1216,7 @@ let second_order_matching_with_args ts env evd pbty ev l t =
else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t))
if b then Success evd else
*)
- let pb = to_pb (pbty,env,mkApp(mkEvar ev,l),t) in
+ let pb = (pbty,env,mkApp(mkEvar ev,l),t) in
UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities))
let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
@@ -1245,7 +1239,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None ->
let reason = ProblemBeyondCapabilities in
- UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
+ UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
&& List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
(remove_instance_local_defs evd evk2 args2) ->
@@ -1255,7 +1249,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
| Some evd -> Success evd
| None ->
let reason = ProblemBeyondCapabilities in
- UnifFailure (evd, CannotSolveConstraint (to_pb (pbty,env,t1,t2),reason)))
+ UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
| Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 ->
let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
Success (solve_refl ~can_drop:true f env evd
@@ -1295,10 +1289,10 @@ let error_cannot_unify env evd pb ?reason t1 t2 =
let check_problems_are_solved env evd =
match snd (extract_all_conv_pbs evd) with
- | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb (EConstr.of_constr t1) (EConstr.of_constr t2)
+ | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
| _ -> ()
-exception MaxUndefined of (Evar.t * evar_info * Constr.t list)
+exception MaxUndefined of (Evar.t * evar_info * EConstr.t list)
let max_undefined_with_candidates evd =
let fold evk evi () = match evi.evar_candidates with
@@ -1326,7 +1320,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
| a::l ->
try
let conv_algo = evar_conv_x ts in
- let evd = check_evar_instance evd evk (EConstr.of_constr a) conv_algo in
+ let evd = check_evar_instance evd evk a conv_algo in
let evd = Evd.define evk a evd in
match reconsider_unif_constraints conv_algo evd with
| Success evd -> solve_unconstrained_evars_with_candidates ts evd
@@ -1348,7 +1342,7 @@ let solve_unconstrained_impossible_cases env evd =
let ty = j_type j in
let conv_algo = evar_conv_x full_transparent_state in
let evd' = check_evar_instance evd' evk ty conv_algo in
- Evd.define evk (EConstr.Unsafe.to_constr ty) evd'
+ Evd.define evk ty evd'
| _ -> evd') evd evd
let solve_unif_constraints_with_heuristics env
@@ -1357,8 +1351,6 @@ let solve_unif_constraints_with_heuristics env
let rec aux evd pbs progress stuck =
match pbs with
| (pbty,env,t1,t2 as pb) :: pbs ->
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
(match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
| Success evd' ->
let (evd', rest) = extract_all_conv_pbs evd' in
@@ -1375,9 +1367,7 @@ let solve_unif_constraints_with_heuristics env
match stuck with
| [] -> (* We're finished *) evd
| (pbty,env,t1,t2 as pb) :: _ ->
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
- (* There remains stuck problems *)
+ (* There remains stuck problems *)
error_cannot_unify env evd pb t1 t2
in
let (evd,pbs) = extract_all_conv_pbs evd in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 627430708a..9270d6e3aa 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -38,7 +38,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
-(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
+[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"]
(** Check all pending unification problems are solved and raise an
error otherwise *)
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 4cffbbb837..b452755b10 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -77,7 +77,7 @@ let define_pure_evar_as_product evd evk =
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in
- let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
+ let concl = Reductionops.whd_all evenv evd evi.evar_concl in
let s = destSort evd concl in
let evksrc = evar_source evk evd in
let src = subterm_source evk ~where:Domain evksrc in
@@ -101,7 +101,7 @@ let define_pure_evar_as_product evd evk =
evd3, rng
in
let prod = mkProd (Name id, dom, subst_var id rng) in
- let evd3 = Evd.define evk (EConstr.Unsafe.to_constr prod) evd2 in
+ let evd3 = Evd.define evk prod evd2 in
evd3,prod
(* Refine an applied evar to a product and returns its instantiation *)
@@ -128,7 +128,7 @@ let define_pure_evar_as_lambda env evd evk =
let open Context.Named.Declaration in
let evi = Evd.find_undefined evd evk in
let evenv = evar_env evi in
- let typ = Reductionops.whd_all evenv evd (EConstr.of_constr (evar_concl evi)) in
+ let typ = Reductionops.whd_all evenv evd (evar_concl evi) in
let evd1,(na,dom,rng) = match EConstr.kind evd typ with
| Prod (na,dom,rng) -> (evd,(na,dom,rng))
| Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd evd typ
@@ -141,7 +141,7 @@ let define_pure_evar_as_lambda env evd evk =
let src = subterm_source evk ~where:Body (evar_source evk evd1) in
let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
let lam = mkLambda (Name id, dom, subst_var id body) in
- Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
+ Evd.define evk lam evd2, lam
let define_evar_as_lambda env evd (evk,args) =
let evd,lam = define_pure_evar_as_lambda env evd evk in
@@ -166,9 +166,9 @@ let define_evar_as_sort env evd (ev,args) =
let evd, u = new_univ_variable univ_rigid evd in
let evi = Evd.find_undefined evd ev in
let s = Type u in
- let concl = Reductionops.whd_all (evar_env evi) evd (EConstr.of_constr evi.evar_concl) in
+ let concl = Reductionops.whd_all (evar_env evi) evd evi.evar_concl in
let sort = destSort evd concl in
- let evd' = Evd.define ev (Constr.mkSort s) evd in
+ let evd' = Evd.define ev (mkSort s) evd in
Evd.set_leq_sort env evd' (Type (Univ.super u)) (ESorts.kind evd' sort), s
(* Propagation of constraints through application and abstraction:
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 96d80741aa..b7eaff0786 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -89,9 +89,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
Array.iter (refresh_term_evars onevars false) args
| Evar (ev, a) when onevars ->
let evi = Evd.find !evdref ev in
- let ty' = refresh ~onlyalg univ_flexible ~direction:true (EConstr.of_constr evi.evar_concl) in
+ let ty' = refresh ~onlyalg univ_flexible ~direction:true evi.evar_concl in
if !modified then
- evdref := Evd.add !evdref ev {evi with evar_concl = EConstr.Unsafe.to_constr ty'}
+ evdref := Evd.add !evdref ev {evi with evar_concl = ty'}
else ()
| _ -> EConstr.iter !evdref (refresh_term_evars onevars false) t
and refresh_polymorphic_positions args pos =
@@ -137,8 +137,6 @@ let test_success conv_algo env evd c c' rhs =
is_success (conv_algo env evd c c' rhs)
let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd =
- let t1 = EConstr.Unsafe.to_constr t1 in
- let t2 = EConstr.Unsafe.to_constr t2 in
match pbty with
| Some true -> add_conv_pb ~tail (Reduction.CUMUL,env,t1,t2) evd
| Some false -> add_conv_pb ~tail (Reduction.CUMUL,env,t2,t1) evd
@@ -197,7 +195,7 @@ let restrict_evar_key evd evk filter candidates =
| None -> evar_filter evi
| Some filter -> filter in
let candidates = match candidates with
- | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
+ | NoUpdate -> evi.evar_candidates
| UpdateWith c -> Some c in
restrict_evar evd evk filter candidates
end
@@ -600,7 +598,6 @@ let solve_pattern_eqn env sigma l c =
let make_projectable_subst aliases sigma evi args =
let sign = evar_filtered_context evi in
- let sign = List.map (fun d -> map_named_decl EConstr.of_constr d) sign in
let evar_aliases = compute_var_aliases sign sigma in
let (_,full_subst,cstr_subst) =
List.fold_right
@@ -877,7 +874,7 @@ let choose_projection evi sols =
let rec do_projection_effects define_fun env ty evd = function
| ProjectVar -> evd
| ProjectEvar ((evk,argsv),evi,id,p) ->
- let evd = Evd.define evk (Constr.mkVar id) evd in
+ let evd = Evd.define evk (mkVar id) evd in
(* TODO: simplify constraints involving evk *)
let evd = do_projection_effects define_fun env ty evd p in
let ty = whd_all env evd (Lazy.force ty) in
@@ -887,7 +884,7 @@ let rec do_projection_effects define_fun env ty evd = function
one (however, regarding coercions, because t is obtained by
unif, we know that no coercion can be inserted) *)
let subst = make_pure_subst evi argsv in
- let ty' = replace_vars subst (EConstr.of_constr evi.evar_concl) in
+ let ty' = replace_vars subst evi.evar_concl in
if isEvar evd ty' then define_fun env evd (Some false) (destEvar evd ty') ty else evd
else
evd
@@ -1004,7 +1001,7 @@ let filter_effective_candidates evd evi filter candidates =
let filter_candidates evd evk filter candidates_update =
let evi = Evd.find_undefined evd evk in
let candidates = match candidates_update with
- | NoUpdate -> Option.map (fun l -> List.map EConstr.of_constr l) evi.evar_candidates
+ | NoUpdate -> evi.evar_candidates
| UpdateWith c -> Some c
in
match candidates with
@@ -1023,13 +1020,12 @@ let closure_of_filter evd evk = function
| None -> None
| Some filter ->
let evi = Evd.find_undefined evd evk in
- let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in
+ let vars = collect_vars evd (evar_concl evi) in
let test b decl = b || Id.Set.mem (get_id decl) vars ||
match decl with
| LocalAssum _ ->
false
| LocalDef (_,c,_) ->
- let c = EConstr.of_constr c in
not (isRel evd c || isVar evd c)
in
let newfilter = Filter.map_along test filter (evar_context evi) in
@@ -1062,7 +1058,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
match candidates,filter with
| UpdateWith [], _ -> user_err Pp.(str "Not solvable.")
| UpdateWith [nc],_ ->
- let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in
+ let evd = Evd.define evk nc evd in
raise (EvarSolvedWhileRestricting (evd,mkEvar ev))
| NoUpdate, None -> evd,ev
| _ -> restrict_applied_evar evd ev filter candidates
@@ -1113,9 +1109,6 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs =
* Note: argument f is the function used to instantiate evars.
*)
-let instantiate_evar_array evi c args =
- EConstr.of_constr (instantiate_evar_array evi (EConstr.Unsafe.to_constr c) (Array.map EConstr.Unsafe.to_constr args))
-
let filter_compatible_candidates conv_algo env evd evi args rhs c =
let c' = instantiate_evar_array evi c args in
match conv_algo env evd Reduction.CONV rhs c' with
@@ -1135,8 +1128,6 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
| _, None -> filter_candidates evd evk1 filter1 NoUpdate
| None, Some _ -> raise DoesNotPreserveCandidateRestriction
| Some l1, Some l2 ->
- let l1 = List.map EConstr.of_constr l1 in
- let l2 = List.map EConstr.of_constr l2 in
let l1 = filter_effective_candidates evd evi1 filter1 l1 in
let l1' = List.filter (fun c1 ->
let c1' = instantiate_evar_array evi1 c1 argsv1 in
@@ -1242,9 +1233,9 @@ let check_evar_instance evd evk1 body conv_algo =
try Retyping.get_type_of ~lax:true evenv evd body
with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance")
in
- match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
+ match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
| Success evd -> evd
- | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,EConstr.of_constr evi.evar_concl))
+ | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
let update_evar_source ev1 ev2 evd =
let loc, evs2 = evar_source ev2 evd in
@@ -1257,7 +1248,7 @@ let update_evar_source ev1 ev2 evd =
let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
try
let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
- let evd' = Evd.define evk2 (EConstr.Unsafe.to_constr body) evd in
+ let evd' = Evd.define evk2 body evd in
let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
check_evar_instance evd' evk2 body g
with EvarSolvedOnTheFly (evd,c) ->
@@ -1292,17 +1283,19 @@ let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 a
let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
let pbty = if force then None else pbty in
let evi = Evd.find evd evk1 in
- let downcast evk t evd = downcast evk (EConstr.Unsafe.to_constr t) evd in
+ let downcast evk t evd = downcast evk t evd in
let evd =
try
(* ?X : Π Δ. Type i = ?Y : Π Δ'. Type j.
The body of ?X and ?Y just has to be of type Π Δ. Type k for some k <= i, j. *)
let evienv = Evd.evar_env evi in
- let ctx1, i = Reduction.dest_arity evienv evi.evar_concl in
+ let concl1 = EConstr.Unsafe.to_constr evi.evar_concl in
+ let ctx1, i = Reduction.dest_arity evienv concl1 in
let ctx1 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx1 in
let evi2 = Evd.find evd evk2 in
let evi2env = Evd.evar_env evi2 in
- let ctx2, j = Reduction.dest_arity evi2env evi2.evar_concl in
+ let concl2 = EConstr.Unsafe.to_constr evi2.evar_concl in
+ let ctx2, j = Reduction.dest_arity evi2env concl2 in
let ctx2 = List.map (fun c -> map_rel_decl EConstr.of_constr c) ctx2 in
let ui, uj = univ_of_sort i, univ_of_sort j in
if i == j || Evd.check_eq evd ui uj
@@ -1375,14 +1368,14 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs =
| Some l ->
let l' =
List.map_filter
- (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs (EConstr.of_constr c)) l in
+ (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in
match l' with
| [] -> raise IncompatibleCandidates
| [c,evd] ->
(* solve_candidates might have been called recursively in the mean *)
(* time and the evar been solved by the filtering process *)
if Evd.is_undefined evd evk then
- let evd' = Evd.define evk (EConstr.Unsafe.to_constr c) evd in
+ let evd' = Evd.define evk c evd in
check_evar_instance evd' evk c conv_algo
else evd
| l when List.length l < List.length l' ->
@@ -1401,8 +1394,8 @@ let occur_evar_upto_types sigma n c =
Array.iter occur_rec args
else (
seen := Evar.Set.add sp !seen;
- Option.iter occur_rec (existential_opt_value sigma e);
- occur_rec (Evd.existential_type sigma e))
+ Option.iter occur_rec (existential_opt_value0 sigma e);
+ occur_rec (Evd.existential_type0 sigma e))
| _ -> Constr.iter occur_rec c
in
try occur_rec c; false with Occur -> true
@@ -1529,7 +1522,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
(* Try to project (a restriction of) the left evar ... *)
try
let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in
- let evd = Evd.define evk' (EConstr.Unsafe.to_constr body) evd in
+ let evd = Evd.define evk' body evd in
check_evar_instance evd evk' body conv_algo
with
| EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
@@ -1592,14 +1585,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
Id.Set.subset (collect_vars evd rhs) !names
in
let body =
- if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
+ if fast rhs then nf_evar evd rhs (** FIXME? *)
else
let t' = imitate (env,0) rhs in
if !progress then
(recheck_applications conv_algo (evar_env evi) evdref t'; t')
else t'
in (!evdref,body)
-
+
(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
* an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
* [define] tries to find an instance lhs such that
@@ -1644,7 +1637,7 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
print_constr body);
raise e in*)
let evd' = check_evar_instance evd' evk body conv_algo in
- Evd.define evk (EConstr.Unsafe.to_constr body) evd'
+ Evd.define evk body evd'
with
| NotEnoughInformationToProgress sols ->
postpone_non_unique_projection env evd pbty ev sols rhs
@@ -1691,8 +1684,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
*)
let status_changed evd lev (pbty,_,t1,t2) =
- let t1 = EConstr.of_constr t1 in
- let t2 = EConstr.of_constr t2 in
(try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) ||
(try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false)
@@ -1702,7 +1693,7 @@ let reconsider_unif_constraints conv_algo evd =
(fun p (pbty,env,t1,t2 as x) ->
match p with
| Success evd ->
- (match conv_algo env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) with
+ (match conv_algo env evd pbty t1 t2 with
| Success _ as x -> x
| UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e)))
| UnifFailure _ as x -> x)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 9b21599b63..3f05c58c41 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -63,7 +63,7 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
-(** @deprecated Alias for [reconsider_unif_constraints] *)
+[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"]
val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
constr -> alias list option
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 74f2cefab6..e89bbf7c34 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -136,7 +136,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
| GIf (m1, (pat1, p1), c1, t1), GIf (m2, (pat2, p2), c2, t2) ->
f m1 m2 && Name.equal pat1 pat2 &&
Option.equal f p1 p2 && f c1 c2 && f t1 t2
- | GRec (kn1, id1, decl1, c1, t1), GRec (kn2, id2, decl2, c2, t2) ->
+ | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) ->
fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 &&
Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 &&
Array.equal f c1 c2 && Array.equal f t1 t2
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 296f25d3f7..b0d714b03d 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -129,8 +129,8 @@ val allowed_sorts : env -> inductive -> Sorts.family list
val has_dependent_elim : mutual_inductive_body -> bool
(** Primitive projections *)
-val projection_nparams : projection -> int
-val projection_nparams_env : env -> projection -> int
+val projection_nparams : Projection.t -> int
+val projection_nparams_env : env -> Projection.t -> int
val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
EConstr.t -> EConstr.types -> types
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index fcbf50feaf..85911394fa 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -401,9 +401,9 @@ and nf_evar env sigma evk ty args =
mkEvar (evk, Array.of_list args), ty
let evars_of_evar_map sigma =
- { Nativelambda.evars_val = Evd.existential_opt_value sigma;
- Nativelambda.evars_typ = Evd.existential_type sigma;
- Nativelambda.evars_metas = Evd.meta_type sigma }
+ { Nativelambda.evars_val = Evd.existential_opt_value0 sigma;
+ Nativelambda.evars_typ = Evd.existential_type0 sigma;
+ Nativelambda.evars_metas = Evd.meta_type0 sigma }
(* fork perf process, return profiler's process id *)
let start_profiler_linux profile_fn =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index dcb93bfb62..27e457e3b3 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -15,7 +15,6 @@ open Globnames
open Nameops
open Term
open Constr
-open Vars
open Glob_term
open Pp
open Mod_subst
@@ -57,10 +56,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
constr_pattern_eq p1 p2 &&
constr_pattern_eq r1 r2 &&
List.equal pattern_eq l1 l2
-| PFix f1, PFix f2 ->
- fixpoint_eq f1 f2
-| PCoFix f1, PCoFix f2 ->
- cofixpoint_eq f1 f2
+| PFix ((ln1,i1),f1), PFix ((ln2,i2),f2) ->
+ Array.equal Int.equal ln1 ln2 && Int.equal i1 i2 && rec_declaration_eq f1 f2
+| PCoFix (i1,f1), PCoFix (i2,f2) ->
+ Int.equal i1 i2 && rec_declaration_eq f1 f2
| PProj (p1, t1), PProj (p2, t2) ->
Projection.equal p1 p2 && constr_pattern_eq t1 t2
| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _
@@ -71,19 +70,10 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
and pattern_eq (i1, j1, p1) (i2, j2, p2) =
Int.equal i1 i2 && List.equal (==) j1 j2 && constr_pattern_eq p1 p2
-and fixpoint_eq ((arg1, i1), r1) ((arg2, i2), r2) =
- Int.equal i1 i2 &&
- Array.equal Int.equal arg1 arg2 &&
- rec_declaration_eq r1 r2
-
-and cofixpoint_eq (i1, r1) (i2, r2) =
- Int.equal i1 i2 &&
- rec_declaration_eq r1 r2
-
and rec_declaration_eq (n1, c1, r1) (n2, c2, r2) =
Array.equal Name.equal n1 n2 &&
- Array.equal Constr.equal c1 c2 &&
- Array.equal Constr.equal r1 r2
+ Array.equal constr_pattern_eq c1 c2 &&
+ Array.equal constr_pattern_eq r1 r2
let rec occur_meta_pattern = function
| PApp (f,args) ->
@@ -123,8 +113,10 @@ let rec occurn_pattern n = function
| PMeta _ | PSoApp _ -> true
| PEvar (_,args) -> Array.exists (occurn_pattern n) args
| PVar _ | PRef _ | PSort _ -> false
- | PFix fix -> not (noccurn n (mkFix fix))
- | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+ | PFix (_,(_,tl,bl)) ->
+ Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
+ | PCoFix (_,(_,tl,bl)) ->
+ Array.exists (occurn_pattern n) tl || Array.exists (occurn_pattern (n+Array.length tl)) bl
let noccurn_pattern n c = not (occurn_pattern n c)
@@ -192,7 +184,7 @@ let pattern_of_constr env sigma t =
| Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ ->
(* These are the two evar kinds used for existing goals *)
(* see Proofview.mark_in_evm *)
- if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev)
+ if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev)
else PEvar (evk,Array.map (pattern_of_constr env) ctxt)
| Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false
| _ ->
@@ -209,8 +201,16 @@ let pattern_of_constr env sigma t =
in
PCase (cip, pattern_of_constr env p, pattern_of_constr env a,
Array.to_list (Array.mapi branch_of_constr br))
- | Fix f -> PFix f
- | CoFix f -> PCoFix f in
+ | Fix (lni,(lna,tl,bl)) ->
+ let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+ let env' = Array.fold_left2 push env lna tl in
+ PFix (lni,(lna,Array.map (pattern_of_constr env) tl,
+ Array.map (pattern_of_constr env') bl))
+ | CoFix (ln,(lna,tl,bl)) ->
+ let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in
+ let env' = Array.fold_left2 push env lna tl in
+ PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl,
+ Array.map (pattern_of_constr env') bl)) in
pattern_of_constr env t
(* To process patterns, we need a translation without typing at all. *)
@@ -225,10 +225,14 @@ let map_pattern_with_binders g f l = function
| PCase (ci,po,p,pl) ->
PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
| PProj (p,pc) -> PProj (p, f l pc)
+ | PFix (lni,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ PFix (lni,(lna,Array.map (f l) tl,Array.map (f l') bl))
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let l' = Array.fold_left (fun l na -> g na l) l lna in
+ PCoFix (ln,(lna,Array.map (f l) tl,Array.map (f l') bl))
(* Non recursive *)
- | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _
- (* Bound to terms *)
- | PFix _ | PCoFix _ as x) -> x
+ | (PVar _ | PEvar _ | PRel _ | PRef _ | PSort _ | PMeta _ as x) -> x
let error_instantiate_pattern id l =
let is = match l with
@@ -262,15 +266,12 @@ let instantiate_pattern env sigma lvar c =
error_instantiate_pattern id (List.subtract Id.equal ctx vars)
with Not_found (* Map.find failed *) ->
x)
- | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
| c ->
map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
aux [] c
let rec liftn_pattern k n = function
| PRel i as x -> if i >= n then PRel (i+k) else x
- | PFix x -> PFix (destFix (liftn k n (mkFix x)))
- | PCoFix x -> PCoFix (destCoFix (liftn k n (mkCoFix x)))
| c -> map_pattern_with_binders (fun _ -> succ) (liftn_pattern k) n c
let lift_pattern k = liftn_pattern k 1
@@ -337,19 +338,35 @@ let rec subst_pattern subst pat =
if cip' == cip && typ' == typ && c' == c && branches' == branches
then pat
else PCase(cip', typ', c', branches')
- | PFix fixpoint ->
- let cstr = mkFix fixpoint in
- let fixpoint' = destFix (subst_mps subst cstr) in
- if fixpoint' == fixpoint then pat else
- PFix fixpoint'
- | PCoFix cofixpoint ->
- let cstr = mkCoFix cofixpoint in
- let cofixpoint' = destCoFix (subst_mps subst cstr) in
- if cofixpoint' == cofixpoint then pat else
- PCoFix cofixpoint'
-
-let mkPLambda na b = PLambda(na,PMeta None,b)
-let rev_it_mkPLambda = List.fold_right mkPLambda
+ | PFix (lni,(lna,tl,bl)) ->
+ let tl' = Array.smartmap (subst_pattern subst) tl in
+ let bl' = Array.smartmap (subst_pattern subst) bl in
+ if bl' == bl && tl' == tl then pat
+ else PFix (lni,(lna,tl',bl'))
+ | PCoFix (ln,(lna,tl,bl)) ->
+ let tl' = Array.smartmap (subst_pattern subst) tl in
+ let bl' = Array.smartmap (subst_pattern subst) bl in
+ if bl' == bl && tl' == tl then pat
+ else PCoFix (ln,(lna,tl',bl'))
+
+let mkPLetIn na b t c = PLetIn(na,b,t,c)
+let mkPProd na t u = PProd(na,t,u)
+let mkPLambda na t b = PLambda(na,t,b)
+let mkPLambdaUntyped na b = PLambda(na,PMeta None,b)
+let rev_it_mkPLambdaUntyped = List.fold_right mkPLambdaUntyped
+
+let mkPProd_or_LetIn (na,_,bo,t) c =
+ match bo with
+ | None -> mkPProd na t c
+ | Some b -> mkPLetIn na b (Some t) c
+
+let mkPLambda_or_LetIn (na,_,bo,t) c =
+ match bo with
+ | None -> mkPLambda na t c
+ | Some b -> mkPLetIn na b (Some t) c
+
+let it_mkPProd_or_LetIn = List.fold_left (fun c d -> mkPProd_or_LetIn d c)
+let it_mkPLambda_or_LetIn = List.fold_left (fun c d -> mkPLambda_or_LetIn d c)
let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp
@@ -428,7 +445,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
let pred = match p,indnames with
| Some p, Some {CAst.v=(_,nal)} ->
let nvars = na :: List.rev nal @ vars in
- rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
+ rev_it_mkPLambdaUntyped nal (mkPLambdaUntyped na (pat_of_raw metas nvars p))
| None, _ -> PMeta None
| Some p, None ->
match DAst.get p with
@@ -450,9 +467,40 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
| GProj(p,c) ->
PProj(p, pat_of_raw metas vars c)
- | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ ->
+ | GRec (GFix (ln,n), ids, decls, tl, cl) ->
+ if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then
+ err ?loc (Pp.str "\"struct\" annotation is expected.")
+ else
+ let ln = Array.map (fst %> Option.get) ln in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+ let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+ let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+ let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+ let names = Array.map (fun id -> Name id) ids in
+ PFix ((ln,n), (names, tl, cl))
+
+ | GRec (GCoFix n, ids, decls, tl, cl) ->
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in
+ let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in
+ let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in
+ let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in
+ let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in
+ let names = Array.map (fun id -> Name id) ids in
+ PCoFix (n, (names, tl, cl))
+
+ | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ ->
err ?loc (Pp.str "Non supported pattern."))
+and pat_of_glob_in_context metas vars decls c =
+ let rec aux acc vars = function
+ | (na,bk,b,t) :: decls ->
+ let decl = (na,bk,Option.map (pat_of_raw metas vars) b,pat_of_raw metas vars t) in
+ aux (decl::acc) (na::vars) decls
+ | [] ->
+ acc, pat_of_raw metas vars c
+ in aux [] vars decls
+
and pats_of_glob_branches loc metas vars ind brs =
let get_arg p = match DAst.get p with
| PatVar na ->
@@ -477,7 +525,7 @@ and pats_of_glob_branches loc metas vars ind brs =
(str "No unique branch for " ++ int j ++ str"-th constructor.");
let lna = List.map get_arg lv in
let vars' = List.rev lna @ vars in
- let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
+ let pat = rev_it_mkPLambdaUntyped lna (pat_of_raw metas vars' br) in
let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
ext, ((j-1, tags, pat) :: pats)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4962b89a09..947469ca0e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -117,7 +117,7 @@ open ExtraEnv
exception Found of int array
let nf_fix sigma (nas, cs, ts) =
- let inj c = EConstr.to_constr sigma c in
+ let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
(nas, Array.map inj cs, Array.map inj ts)
let search_guard ?loc env possible_indexes fixdefs =
@@ -315,7 +315,7 @@ let apply_inference_hook hook evdref frozen = match frozen with
then
try
let sigma, c = hook sigma evk in
- Evd.define evk (EConstr.Unsafe.to_constr c) sigma
+ Evd.define evk c sigma
with Exit ->
sigma
else
@@ -532,7 +532,7 @@ let pretype_global ?loc rigid env evd gr us =
interp_instance ?loc evd ~len l
in
let (sigma, c) = Evd.fresh_global ?loc ~rigid ?names:instance env.ExtraEnv.env evd gr in
- (sigma, EConstr.of_constr c)
+ (sigma, c)
let pretype_ref ?loc evdref env ref us =
match ref with
@@ -1109,7 +1109,7 @@ 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 = NamedDecl.get_id decl in
- let t = replace_vars subst (EConstr.of_constr (NamedDecl.get_type decl)) in
+ let t = replace_vars subst (NamedDecl.get_type decl) in
let c, update =
try
let c = List.assoc id update in
@@ -1150,7 +1150,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
(* Correction of bug #5315 : we need to define an evar for *all* holes *)
let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
let ev,_ = destEvar !evdref evkt in
- evdref := Evd.define ev (to_constr !evdref v) !evdref;
+ evdref := Evd.define ev (nf_evar !evdref v) !evdref;
(* End of correction of bug #5315 *)
{ utj_val = v;
utj_type = s }
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9e3e68f059..244b8e60b1 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -275,12 +275,12 @@ sig
type cst_member =
| Cst_const of pconstant
- | Cst_proj of projection
+ | Cst_proj of Projection.t
type 'a member =
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
- | Proj of int * int * projection * Cst_stack.t
+ | Proj of int * int * Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Cst of cst_member * int * int list * 'a t * Cst_stack.t
and 'a t = 'a member list
@@ -332,12 +332,12 @@ struct
type cst_member =
| Cst_const of pconstant
- | Cst_proj of projection
+ | Cst_proj of Projection.t
type 'a member =
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
- | Proj of int * int * projection * Cst_stack.t
+ | Proj of int * int * Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Cst of cst_member * int * int list * 'a t * Cst_stack.t
and 'a t = 'a member list
@@ -871,7 +871,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
| Evar ev -> fold ()
| Meta ev ->
(match safe_meta_value sigma ev with
- | Some body -> whrec cst_l (EConstr.of_constr body, stack)
+ | Some body -> whrec cst_l (body, stack)
| None -> fold ())
| Const (c,u as const) ->
reduction_effect_hook env sigma (EConstr.to_constr sigma x)
@@ -1106,7 +1106,7 @@ let local_whd_state_gen flags sigma =
| Evar ev -> s
| Meta ev ->
(match safe_meta_value sigma ev with
- Some c -> whrec (EConstr.of_constr c,stack)
+ Some c -> whrec (c,stack)
| None -> s)
| Construct ((ind,c),u) ->
@@ -1392,7 +1392,7 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
(********************************************************************)
let whd_meta sigma c = match EConstr.kind sigma c with
- | Meta p -> (try EConstr.of_constr (meta_value sigma p) with Not_found -> c)
+ | Meta p -> (try meta_value sigma p with Not_found -> c)
| _ -> c
let default_plain_instance_ident = Id.of_string "H"
@@ -1612,7 +1612,7 @@ let meta_value evd mv =
match meta_opt_fvalue evd mv with
| Some (b,_) ->
let metas = Metamap.bind valrec b.freemetas in
- instance evd metas (EConstr.of_constr b.rebus)
+ instance evd metas b.rebus
| None -> mkMeta mv
in
valrec mv
@@ -1625,9 +1625,8 @@ let meta_instance sigma b =
instance sigma c_sigma b.rebus
let nf_meta sigma c =
- let c = EConstr.Unsafe.to_constr c in
let cl = mk_freelisted c in
- meta_instance sigma { cl with rebus = EConstr.of_constr cl.rebus }
+ meta_instance sigma { cl with rebus = cl.rebus }
(* Instantiate metas that create beta/iota redexes *)
@@ -1648,7 +1647,6 @@ let meta_reducible_instance evd b =
(match
try
let g, s = Metamap.find m metas in
- let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if isConstruct evd g || not is_coerce then Some g else None
with Not_found -> None
@@ -1660,7 +1658,6 @@ let meta_reducible_instance evd b =
(match
try
let g, s = Metamap.find m metas in
- let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if isLambda evd g || not is_coerce then Some g else None
with Not_found -> None
@@ -1669,7 +1666,6 @@ let meta_reducible_instance evd b =
| None -> mkApp (f,Array.map irec l))
| Meta m ->
(try let g, s = Metamap.find m metas in
- let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if not is_coerce then irec g else u
with Not_found -> u)
@@ -1678,7 +1674,6 @@ let meta_reducible_instance evd b =
(match
try
let g, s = Metamap.find m metas in
- let g = EConstr.of_constr g in
let is_coerce = match s with CoerceToType -> true | _ -> false in
if isConstruct evd g || not is_coerce then Some g else None
with Not_found -> None
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 29dc3ed0f2..b8ac085a7a 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -70,12 +70,12 @@ module Stack : sig
type cst_member =
| Cst_const of pconstant
- | Cst_proj of projection
+ | Cst_proj of Projection.t
type 'a member =
| App of 'a app_node
| Case of case_info * 'a * 'a array * Cst_stack.t
- | Proj of int * int * projection * Cst_stack.t
+ | Proj of int * int * Projection.t * Cst_stack.t
| Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
| Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
* 'a t * Cst_stack.t
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 3582b6447a..746a68b217 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -57,8 +57,8 @@ let get_type_from_constraints env sigma t =
if isEvar sigma (fst (decompose_app_vect sigma t)) then
match
List.map_filter (fun (pbty,env,t1,t2) ->
- if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2
- else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1
+ if is_fconv Reduction.CONV env sigma t t1 then Some t2
+ else if is_fconv Reduction.CONV env sigma t t2 then Some t1
else None)
(snd (Evd.extract_all_conv_pbs sigma))
with
@@ -99,7 +99,7 @@ let retype ?(polyprop=true) sigma =
let rec type_of env cstr =
match EConstr.kind sigma cstr with
| Meta n ->
- (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus)
+ (try strip_outer_cast sigma (Evd.meta_ftype sigma n).Evd.rebus
with Not_found -> retype_error (BadMeta n))
| Rel n ->
let ty = RelDecl.get_type (lookup_rel n env) in
@@ -115,7 +115,7 @@ let retype ?(polyprop=true) sigma =
try Inductiveops.find_rectype env sigma t
with Not_found ->
try
- let t = EConstr.of_constr (get_type_from_constraints env sigma t) in
+ let t = get_type_from_constraints env sigma t in
Inductiveops.find_rectype env sigma t
with Not_found -> retype_error BadRecursiveType
in
@@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma =
and type_of_global_reference_knowing_parameters env c args =
let argtyps =
- Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
+ Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
match EConstr.kind sigma c with
| Ind (ind, u) ->
let u = EInstance.kind sigma u in
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 40424ead4a..2aff0c7775 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -50,6 +50,6 @@ val type_of_global_reference_knowing_conclusion :
val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list
-val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
+val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr
val print_retype_error : retype_error -> Pp.t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 518d2f6045..696001ab77 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -416,7 +416,7 @@ exception Partial
reduction is solved by the expanded fix term. *)
let solve_arity_problem env sigma fxminargs c =
let evm = ref sigma in
- let set_fix i = evm := Evd.define i (Constr.mkVar vfx) !evm in
+ let set_fix i = evm := Evd.define i (mkVar vfx) !evm in
let rec check strict c =
let c' = whd_betaiotazeta sigma c in
let (h,rcargs) = decompose_app_vect sigma c' in
@@ -558,7 +558,7 @@ let match_eval_ref_value env sigma constr stack =
else
None
| Proj (p, c) when not (Projection.unfolded p) ->
- reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
+ reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr)
(lazy (EConstr.to_constr sigma (applist (constr,stack))));
if is_evaluable env (EvalConstRef (Projection.constant p)) then
Some (mkProj (Projection.unfold p, c))
@@ -641,7 +641,7 @@ let whd_nothing_for_iota env sigma s =
| _ -> s)
| Evar ev -> s
| Meta ev ->
- (try whrec (EConstr.of_constr (Evd.meta_value sigma ev), stack)
+ (try whrec (Evd.meta_value sigma ev, stack)
with Not_found -> s)
| Const (const, u) when is_transparent_constant full_transparent_state const ->
let u = EInstance.kind sigma u in
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 08051fd3a1..30ddeffa69 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -158,7 +158,7 @@ let rec is_class_type evd c =
| _ -> is_class_constr evd c
let is_class_evar evd evi =
- is_class_type evd (EConstr.of_constr evi.Evd.evar_concl)
+ is_class_type evd evi.Evd.evar_concl
(*
* classes persistent object
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 4c834f2f8f..aaec73f045 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -29,13 +29,12 @@ let meta_type evd mv =
let ty =
try Evd.meta_ftype evd mv
with Not_found -> anomaly (str "unknown meta ?" ++ str (Nameops.string_of_meta mv) ++ str ".") in
- let ty = Evd.map_fl EConstr.of_constr ty in
meta_instance evd ty
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
- let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
+ let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp
let e_type_judgment env evdref j =
@@ -129,7 +128,7 @@ let e_is_correct_arity env evdref c pj ind specif params =
then error ()
| Evar (ev,_), [] ->
let evd, s = Evd.fresh_sort_in_family env !evdref (max_sort allowed_sorts) in
- evdref := Evd.define ev (Constr.mkSort s) evd
+ evdref := Evd.define ev (mkSort s) evd
| _, (LocalDef _ as d)::ar' ->
srec (push_rel d env) (lift 1 pt') ar'
| _ ->
@@ -155,7 +154,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
let p = pj.uj_val in
let params = List.map EConstr.Unsafe.to_constr params in
let () = e_is_correct_arity env evdref c pj ind specif params in
- let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
+ let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in
let lc = Array.map EConstr.of_constr lc in
let n = (snd specif).Declarations.mind_nrealdecls in
let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
@@ -207,7 +206,7 @@ let enrich_env env evdref =
Environ.env_of_pre_env penv'
let check_fix env sigma pfix =
- let inj c = EConstr.to_constr sigma c in
+ let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let (idx, (ids, cs, ts)) = pfix in
check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index fe83a2cc84..4905adf1f3 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -55,4 +55,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
val judge_of_product : Environ.env -> Name.t ->
unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
-val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f2f922fd51..d98ce9abab 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -84,7 +84,7 @@ let occur_meta_or_undefined_evar evd c =
| Evar (ev,args) ->
(match evar_body (Evd.find evd ev) with
| Evar_defined c ->
- occrec c; Array.iter occrec args
+ occrec (EConstr.Unsafe.to_constr c); Array.iter occrec args
| Evar_empty -> raise Occur)
| _ -> Constr.iter occrec c
in try occrec c; false with Occur | Not_found -> true
@@ -189,10 +189,9 @@ let pose_all_metas_as_evars env evd t =
let rec aux t = match EConstr.kind !evdref t with
| Meta mv ->
(match Evd.meta_opt_fvalue !evdref mv with
- | Some ({rebus=c},_) -> EConstr.of_constr c
+ | Some ({rebus=c},_) -> c
| None ->
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
- let ty = EConstr.of_constr ty in
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
let ty =
if Flags.version_strictly_greater Flags.V8_6
@@ -200,7 +199,7 @@ let pose_all_metas_as_evars env evd t =
else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
let src = Evd.evar_source_of_meta mv !evdref in
let ev = Evarutil.e_new_evar env evdref ~src ty in
- evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
+ evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
ev)
| _ ->
EConstr.map !evdref aux t in
@@ -466,7 +465,7 @@ let use_metas_pattern_unification sigma flags nb l =
type key =
| IsKey of CClosure.table_key
- | IsProj of projection * EConstr.constr
+ | IsProj of Projection.t * EConstr.constr
let expand_table_key env = function
| ConstKey cst -> constant_opt_value_in env cst
@@ -1060,7 +1059,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
(evd,t2::ks, m-1)
else
let mv = new_meta () in
- let evd' = meta_declare mv (EConstr.Unsafe.to_constr (substl ks b)) evd in
+ let evd' = meta_declare mv (substl ks b) evd in
(evd', mkMeta mv :: ks, m - 1))
(sigma,[],List.length bs) bs
in
@@ -1247,7 +1246,7 @@ let try_to_coerce env evd c cty tycon =
let j = make_judge c cty in
let (evd',j') = inh_conv_coerce_rigid_to true env evd j tycon in
let evd' = Evarconv.solve_unif_constraints_with_heuristics env evd' in
- let evd' = Evd.map_metas_fvalue (fun c -> EConstr.Unsafe.to_constr (nf_evar evd' (EConstr.of_constr c))) evd' in
+ let evd' = Evd.map_metas_fvalue (fun c -> nf_evar evd' c) evd' in
(evd',j'.uj_val)
let w_coerce_to_type env evd c cty mvty =
@@ -1359,11 +1358,11 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
if meta_defined evd mv then
let {rebus=c'},(status',_) = meta_fvalue evd mv in
let (take_left,st,(evd,metas',evars')) =
- merge_instances env evd flags status' status (EConstr.of_constr c') c
+ merge_instances env evd flags status' status c' c
in
let evd' =
if take_left then evd
- else meta_reassign mv (EConstr.Unsafe.to_constr c,(st,TypeProcessed)) evd
+ else meta_reassign mv (c,(st,TypeProcessed)) evd
in
w_merge_rec evd' (metas'@metas@metas'') (evars'@evars'') eqns
else
@@ -1372,7 +1371,7 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
if isMetaOf evd mv (whd_all env evd c) then evd
else error_cannot_unify env evd (mkMeta mv,c)
else
- meta_assign mv (EConstr.Unsafe.to_constr c,(status,TypeProcessed)) evd in
+ meta_assign mv (c,(status,TypeProcessed)) evd in
w_merge_rec evd' (metas''@metas) evars'' eqns
| [] ->
(* Process type eqns *)
@@ -1396,17 +1395,17 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
unify_0 sp_env evd' CUMUL flags
- (get_type_of sp_env evd' c) (EConstr.of_constr ev.evar_concl) in
+ (get_type_of sp_env evd' c) ev.evar_concl in
let evd''' = w_merge_rec evd'' mc ec [] in
if evd' == evd'''
- then Evd.define sp (EConstr.Unsafe.to_constr c) evd'''
- else Evd.define sp (EConstr.Unsafe.to_constr (Evarutil.nf_evar evd''' c)) evd''' in
+ then Evd.define sp c evd'''
+ else Evd.define sp (Evarutil.nf_evar evd''' c) evd''' in
let check_types evd =
let metas = Evd.meta_list evd in
let eqns = List.fold_left (fun acc (mv, b) ->
match b with
- | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, EConstr.of_constr t.rebus) :: acc
+ | Clval (n, (t, (c, TypeNotProcessed)), v) -> (mv, c, t.rebus) :: acc
| _ -> acc) [] metas
in w_merge_rec evd [] [] eqns
in
@@ -1417,11 +1416,6 @@ let w_merge env with_types flags (evd,metas,evars : subst0) =
in
if with_types then check_types res else res
-let retract_coercible_metas evd =
- let (metas, evd) = retract_coercible_metas evd in
- let map (mv, c, st) = (mv, EConstr.of_constr c, st) in
- (List.map map metas, evd)
-
let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
let metas,evd = retract_coercible_metas evd in
w_merge env true flags.merge_unify_flags (evd,metas,[])
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 3c9b8bc338..049c3aff5a 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -205,7 +205,7 @@ and nf_univ_args ~nb_univs mk env sigma stk =
and nf_evar env sigma evk stk =
let evi = try Evd.find sigma evk with Not_found -> assert false in
let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
- let concl = Evd.evar_concl evi in
+ let concl = EConstr.Unsafe.to_constr @@ Evd.evar_concl evi in
if List.is_empty hyps then
nf_stk env sigma (mkEvar (evk, [||])) concl stk
else match stk with
@@ -381,8 +381,8 @@ let cbv_vm env sigma c t =
if Termops.occur_meta sigma c then
CErrors.user_err Pp.(str "vm_compute does not support metas.");
(** This evar-normalizes terms beforehand *)
- let c = EConstr.to_constr sigma c in
- let t = EConstr.to_constr sigma t in
+ let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
+ let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
let v = Vconv.val_of_constr env c in
EConstr.of_constr (nf_val env sigma v t)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 00:47:26 +0000