aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercionops.ml12
-rw-r--r--pretyping/indrec.ml15
-rw-r--r--pretyping/pretyping.ml17
-rw-r--r--pretyping/pretyping.mli8
-rw-r--r--pretyping/reductionops.ml74
-rw-r--r--pretyping/reductionops.mli15
-rw-r--r--pretyping/retyping.ml20
-rw-r--r--pretyping/unification.ml6
-rw-r--r--pretyping/vnorm.ml2
9 files changed, 53 insertions, 116 deletions
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index d6458e1409..49401a9937 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -67,8 +67,6 @@ end
module ClTypMap = Map.Make(ClTyp)
-module IntMap = Map.Make(Int)
-
let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
type inheritance_path = coe_info_typ list
@@ -97,13 +95,13 @@ struct
module Index = struct include Int let print = Pp.int end
- type 'a t = { v : (cl_typ * 'a) IntMap.t; s : int; inv : int ClTypMap.t }
- let empty = { v = IntMap.empty; s = 0; inv = ClTypMap.empty }
+ type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
+ let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
let mem y b = ClTypMap.mem y b.inv
- let map x b = IntMap.find x b.v
- let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (IntMap.find n b.v))
+ let map x b = Int.Map.find x b.v
+ let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
let add x y b =
- { v = IntMap.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
+ { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
end
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index c92c9a75a0..b5d81f762a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -530,22 +530,25 @@ let change_sort_arity sort =
corresponding eta-expanded term *)
let weaken_sort_scheme env evd set sort npars term ty =
let evdref = ref evd in
- let rec drec np elim =
+ let rec drec ctx np elim =
match kind elim with
| Prod (n,t,c) ->
+ let ctx = LocalAssum (n, t) :: ctx in
if Int.equal np 0 then
let osort, t' = change_sort_arity sort t in
evdref := (if set then Evd.set_eq_sort else Evd.set_leq_sort) env !evdref sort osort;
mkProd (n, t', c),
- mkLambda (n, t', mkApp(term,Termops.rel_vect 0 (npars+1)))
+ mkLambda (n, t', mkApp(term, Context.Rel.to_extended_vect mkRel 0 ctx))
else
- let c',term' = drec (np-1) c in
+ let c',term' = drec ctx (np-1) c in
mkProd (n, t, c'), mkLambda (n, t, term')
- | LetIn (n,b,t,c) -> let c',term' = drec np c in
- mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
+ | LetIn (n,b,t,c) ->
+ let ctx = LocalDef (n, b, t) :: ctx in
+ let c',term' = drec ctx np c in
+ mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
| _ -> anomaly ~label:"weaken_sort_scheme" (Pp.str "wrong elimination type.")
in
- let ty, term = drec npars ty in
+ let ty, term = drec [] npars ty in
!evdref, ty, term
(**********************************************************************)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4bab3bd6ea..52122c09df 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -187,7 +187,7 @@ let interp_sort_info ?loc evd l =
in (evd', Univ.sup u u'))
(evd, Univ.Universe.type0m) l
-type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
+type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
type inference_flags = {
use_typeclasses : bool;
@@ -231,7 +231,7 @@ let frozen_and_pending_holes (sigma, sigma') =
end in
FrozenProgress data
-let apply_typeclasses ~program_mode env sigma frozen fail_evar =
+let apply_typeclasses ~program_mode ~fail_evar env sigma frozen =
let filter_frozen = match frozen with
| FrozenId map -> fun evk -> Evar.Map.mem evk map
| FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
@@ -247,17 +247,16 @@ let apply_typeclasses ~program_mode env sigma frozen fail_evar =
else sigma in
sigma
-let apply_inference_hook hook env sigma frozen = match frozen with
+let apply_inference_hook (hook : inference_hook) env sigma frozen = match frozen with
| FrozenId _ -> sigma
| FrozenProgress (lazy (_, pending)) ->
Evar.Set.fold (fun evk sigma ->
if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
then
- try
- let sigma, c = hook env sigma evk in
+ match hook env sigma evk with
+ | Some (sigma, c) ->
Evd.define evk c sigma
- with Exit ->
- sigma
+ | None -> sigma
else
sigma) pending sigma
@@ -271,7 +270,7 @@ let apply_heuristics env sigma fail_evar =
let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
(* Naive way, call resolution again with failure flag *)
- apply_typeclasses ~program_mode env current_sigma frozen true
+ apply_typeclasses ~program_mode ~fail_evar:true env current_sigma frozen
let check_extra_evars_are_solved env current_sigma frozen = match frozen with
| FrozenId _ -> ()
@@ -314,7 +313,7 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
let frozen = frozen_and_pending_holes (initial, sigma) in
let sigma =
if flags.use_typeclasses
- then apply_typeclasses ~program_mode env sigma frozen false
+ then apply_typeclasses ~fail_evar:false ~program_mode env sigma frozen
else sigma
in
let sigma = match hook with
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 700ca93c33..abbb745161 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,8 +44,6 @@ type typing_constraint =
| OfType of types (** A term of the expected type *)
| WithoutTypeConstraint (** A term of unknown expected type *)
-type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
-
type inference_flags = {
use_typeclasses : bool;
solve_unification_constraints : bool;
@@ -103,13 +101,17 @@ val understand_ltac : inference_flags ->
val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context
+(** [hook env sigma ev] returns [Some (sigma', term)] if [ev] can be
+ instantiated with a solution, [None] otherwise. Used to extend
+ [solve_remaining_evars] below. *)
+type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
+
(** Trying to solve remaining evars and remaining conversion problems
possibly using type classes, heuristics, external tactic solver
hook depending on given flags. *)
(* For simplicity, it is assumed that current map has no other evars
with candidate and no other conversion problems that the one in
[pending], however, it can contain more evars than the pending ones. *)
-
val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
env -> ?initial:evar_map -> (* current map *) evar_map -> evar_map
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1e4b537117..8822cc2338 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -622,9 +622,8 @@ type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
evar_map -> constr -> constr * constr list
-type contextual_state_reduction_function =
+type state_reduction_function =
env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
let pr_state env sigma (tm,sk) =
@@ -1571,10 +1570,6 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta sigma c = match EConstr.kind sigma c with
- | Meta p -> (try meta_value sigma p with Not_found -> c)
- | _ -> c
-
let default_plain_instance_ident = Id.of_string "H"
(* Try to replace all metas. Does not replace metas in the metas' values
@@ -1810,70 +1805,3 @@ let meta_instance sigma b =
let nf_meta sigma c =
let cl = mk_freelisted c in
meta_instance sigma { cl with rebus = cl.rebus }
-
-(* Instantiate metas that create beta/iota redexes *)
-
-let meta_reducible_instance evd b =
- let fm = b.freemetas in
- let fold mv accu =
- let fvalue = try meta_opt_fvalue evd mv with Not_found -> None in
- match fvalue with
- | None -> accu
- | Some (g, (_, s)) -> Metamap.add mv (g.rebus, s) accu
- in
- let metas = Metaset.fold fold fm Metamap.empty in
- let rec irec u =
- let u = whd_betaiota Evd.empty u (* FIXME *) in
- match EConstr.kind evd u with
- | Case (ci,p,c,bl) when EConstr.isMeta evd (strip_outer_cast evd c) ->
- let m = destMeta evd (strip_outer_cast evd c) in
- (match
- try
- let g, s = Metamap.find m metas 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
- with
- | Some g -> irec (mkCase (ci,p,g,bl))
- | None -> mkCase (ci,irec p,c,Array.map irec bl))
- | App (f,l) when EConstr.isMeta evd (strip_outer_cast evd f) ->
- let m = destMeta evd (strip_outer_cast evd f) in
- (match
- try
- let g, s = Metamap.find m metas 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
- with
- | Some g -> irec (mkApp (g,l))
- | None -> mkApp (f,Array.map irec l))
- | Meta m ->
- (try let g, s = Metamap.find m metas in
- let is_coerce = match s with CoerceToType -> true | _ -> false in
- if not is_coerce then irec g else u
- with Not_found -> u)
- | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) ->
- let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in
- (match
- try
- let g, s = Metamap.find m metas 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
- with
- | Some g -> irec (mkProj (p,g))
- | None -> mkProj (p,c))
- | _ -> EConstr.map evd irec u
- in
- if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
- else irec b.rebus
-
-let betazetaevar_applist sigma n c l =
- let rec stacklam n env t stack =
- if Int.equal n 0 then applist (substl env t, stack) else
- match EConstr.kind sigma t, stack with
- | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
- | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
- | Evar _, _ -> applist (substl env t, stack)
- | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
- stacklam n [] c l
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5202380a13..243a2745f0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -139,9 +139,8 @@ type stack_reduction_function = contextual_stack_reduction_function
type local_stack_reduction_function =
evar_map -> constr -> constr * constr list
-type contextual_state_reduction_function =
+type state_reduction_function =
env -> evar_map -> state -> state
-type state_reduction_function = contextual_state_reduction_function
type local_state_reduction_function = evar_map -> state -> state
val pr_state : env -> evar_map -> state -> Pp.t
@@ -203,8 +202,8 @@ val whd_nored_state : local_state_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
val whd_betaiotazeta_state : local_state_reduction_function
-val whd_all_state : contextual_state_reduction_function
-val whd_allnolet_state : contextual_state_reduction_function
+val whd_all_state : state_reduction_function
+val whd_allnolet_state : state_reduction_function
val whd_betalet_state : local_state_reduction_function
(** {6 Head normal forms } *)
@@ -309,13 +308,6 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
evar_map -> constr -> constr -> evar_map option
-(** {6 Special-Purpose Reduction Functions } *)
-
-val whd_meta : local_reduction_function
-val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
-val instance : evar_map -> constr Metamap.t -> constr -> constr
-val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
-
(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state :
@@ -324,4 +316,3 @@ val whd_betaiota_deltazeta_for_iota_state :
(** {6 Meta-related reduction functions } *)
val meta_instance : evar_map -> constr freelisted -> constr
val nf_meta : evar_map -> constr -> constr
-val meta_reducible_instance : evar_map -> constr freelisted -> constr
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d4fa2461b4..1f091c3df8 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -97,6 +97,16 @@ let decomp_sort env sigma t =
let destSort sigma s = ESorts.kind sigma (destSort sigma s)
+let betazetaevar_applist sigma n c l =
+ let rec stacklam n env t stack =
+ if Int.equal n 0 then applist (substl env t, stack) else
+ match EConstr.kind sigma t, stack with
+ | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl
+ | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack
+ | Evar _, _ -> applist (substl env t, stack)
+ | _ -> anomaly (Pp.str "Not enough lambda/let's.") in
+ stacklam n [] c l
+
let retype ?(polyprop=true) sigma =
let rec type_of env cstr =
match EConstr.kind sigma cstr with
@@ -273,8 +283,8 @@ let relevance_of_term env sigma c =
| Rel n ->
let len = Range.length rels in
if n <= len then Range.get rels (n - 1)
- else Retypeops.relevance_of_rel env (n - len)
- | Var x -> Retypeops.relevance_of_var env x
+ else Relevanceops.relevance_of_rel env (n - len)
+ | Var x -> Relevanceops.relevance_of_var env x
| Sort _ -> Sorts.Relevant
| Cast (c, _, _) -> aux rels c
| Prod ({binder_relevance=r}, _, codom) ->
@@ -284,13 +294,13 @@ let relevance_of_term env sigma c =
| LetIn ({binder_relevance=r}, _, _, bdy) ->
aux (Range.cons r rels) bdy
| App (c, _) -> aux rels c
- | Const (c,_) -> Retypeops.relevance_of_constant env c
+ | Const (c,_) -> Relevanceops.relevance_of_constant env c
| Ind _ -> Sorts.Relevant
- | Construct (c,_) -> Retypeops.relevance_of_constructor env c
+ | Construct (c,_) -> Relevanceops.relevance_of_constructor env c
| Case (ci, _, _, _) -> ci.ci_relevance
| Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
| CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
- | Proj (p, _) -> Retypeops.relevance_of_projection env p
+ | Proj (p, _) -> Relevanceops.relevance_of_projection env p
| Int _ | Float _ -> Sorts.Relevant
| Meta _ | Evar _ -> Sorts.Relevant
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ec3fb0758e..90dde01915 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -87,6 +87,12 @@ let occur_meta_or_undefined_evar evd c =
| _ -> Constr.iter occrec c
in try occrec c; false with Occur | Not_found -> true
+let whd_meta sigma c = match EConstr.kind sigma c with
+ | Meta p ->
+ (try Evd.meta_value sigma p with Not_found -> c)
+ (* Not recursive, for some reason *)
+ | _ -> c
+
let occur_meta_evd sigma mv c =
let rec occrec c =
(* Note: evars are not instantiated by terms with metas *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 64068724af..d4da93cc5b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -73,7 +73,7 @@ let type_constructor mind mib u (ctx, typ) params =
if Int.equal ndecls 0 then ctyp
else
let _,ctyp = decompose_prod_n_assum ndecls ctyp in
- substl (List.rev (adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params)))
+ substl (subst_of_rel_context_instance mib.mind_params_ctxt (Array.to_list params))
ctyp
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 22:38:19 +0000