aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercionops.ml12
-rw-r--r--pretyping/nativenorm.ml4
-rw-r--r--pretyping/pretyping.ml28
-rw-r--r--pretyping/pretyping.mli11
-rw-r--r--pretyping/reductionops.ml80
-rw-r--r--pretyping/reductionops.mli15
-rw-r--r--pretyping/retyping.ml10
-rw-r--r--pretyping/unification.ml6
-rw-r--r--pretyping/vnorm.ml2
9 files changed, 58 insertions, 110 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/nativenorm.ml b/pretyping/nativenorm.ml
index 7be34d4cf1..f989dae4c9 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -496,8 +496,8 @@ let stop_profiler m_pid =
let native_norm env sigma c ty =
let c = EConstr.Unsafe.to_constr c in
let ty = EConstr.Unsafe.to_constr ty in
- if not Coq_config.native_compiler then
- user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
+ if not (Flags.get_native_compiler ()) then
+ user_err Pp.(str "Native_compute reduction has been disabled.")
else
(*
Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ded159e484..015c26531a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -189,8 +189,10 @@ let interp_sort_info ?loc evd l =
type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
+type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+
type inference_flags = {
- use_typeclasses : bool;
+ use_typeclasses : use_typeclasses;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
@@ -231,7 +233,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
@@ -270,7 +272,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 _ -> ()
@@ -312,9 +314,9 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
let program_mode = flags.program_mode in
let frozen = frozen_and_pending_holes (initial, sigma) in
let sigma =
- if flags.use_typeclasses
- then apply_typeclasses ~program_mode env sigma frozen false
- else sigma
+ match flags.use_typeclasses with
+ | UseTC -> apply_typeclasses ~program_mode ~fail_evar:false env sigma frozen
+ | NoUseTC | UseTCForConv -> sigma
in
let sigma = match hook with
| None -> sigma
@@ -1287,21 +1289,25 @@ let ise_pretype_gen flags env sigma lvar kind c =
if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
in
let env = GlobEnv.make ~hypnaming env sigma lvar in
+ let use_tc = match flags.use_typeclasses with
+ | NoUseTC -> false
+ | UseTC | UseTCForConv -> true
+ in
let sigma', c', c'_ty = match kind with
| WithoutTypeConstraint | UnknownIfTermOrType ->
- let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode ~poly use_tc empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
- let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+ let sigma, j = pretype ~program_mode ~poly use_tc (mk_tycon exptyp) env sigma c in
sigma, j.uj_val, j.uj_type
| IsType ->
- let sigma, tj = pretype_type ~program_mode ~poly flags.use_typeclasses empty_valcon env sigma c in
+ let sigma, tj = pretype_type ~program_mode ~poly use_tc empty_valcon env sigma c in
sigma, tj.utj_val, mkSort tj.utj_type
in
process_inference_flags flags !!env sigma (sigma',c',c'_ty)
let default_inference_flags fail = {
- use_typeclasses = true;
+ use_typeclasses = UseTC;
solve_unification_constraints = true;
fail_evar = fail;
expand_evars = true;
@@ -1310,7 +1316,7 @@ let default_inference_flags fail = {
}
let no_classes_no_fail_inference_flags = {
- use_typeclasses = false;
+ use_typeclasses = NoUseTC;
solve_unification_constraints = true;
fail_evar = false;
expand_evars = true;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index abbb745161..8be7b1477b 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,8 +44,17 @@ type typing_constraint =
| OfType of types (** A term of the expected type *)
| WithoutTypeConstraint (** A term of unknown expected type *)
+type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+(** Typeclasses are used in 2 ways:
+
+- through the "Typeclass Resolution For Conversion" option, if a
+ conversion problem fails we try again after resolving typeclasses
+ (UseTCForConv and UseTC)
+- after pretyping we resolve typeclasses (UseTC) (in [solve_remaining_evars])
+*)
+
type inference_flags = {
- use_typeclasses : bool;
+ use_typeclasses : use_typeclasses;
solve_unification_constraints : bool;
fail_evar : bool;
expand_evars : bool;
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 1e4b537117..8bb268a92e 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) =
@@ -716,7 +715,7 @@ let reducible_mind_case sigma c = match EConstr.kind sigma c with
f x := t. End M. Definition f := u. and say goodbye to any hope
of refolding M.f this way ...
*)
-let magicaly_constant_of_fixbody env sigma reference bd = function
+let magically_constant_of_fixbody env sigma reference bd = function
| Name.Anonymous -> bd
| Name.Name id ->
let open UnivProblem in
@@ -758,7 +757,7 @@ let contract_cofix ?env sigma ?reference (bodynum,(names,types,bodies as typedbo
| Some e ->
match reference with
| None -> bd
- | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+ | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -800,7 +799,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies
| Some e ->
match reference with
| None -> bd
- | Some r -> magicaly_constant_of_fixbody e sigma r bd names.(ind).binder_name in
+ | Some r -> magically_constant_of_fixbody e sigma r bd names.(ind).binder_name in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -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 821c57d033..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
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-03-09 03:24:32 +0000