aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/detyping.ml7
-rw-r--r--pretyping/evarconv.ml8
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/inductiveops.ml38
-rw-r--r--pretyping/nativenorm.ml9
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/retyping.ml13
-rw-r--r--pretyping/typing.ml11
-rw-r--r--pretyping/unification.ml10
-rw-r--r--pretyping/vnorm.ml2
12 files changed, 55 insertions, 57 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index bf9e37aa7..5c4cbefad 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -209,8 +209,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
match (EConstr.kind !evdref x, EConstr.kind !evdref y) with
| Sort s, Sort s' ->
(match ESorts.kind !evdref s, ESorts.kind !evdref s' with
- | Prop x, Prop y when x == y -> None
- | Prop _, Type _ -> None
+ | Prop, Prop | Set, Set -> None
+ | (Prop | Set), Type _ -> None
| Type x, Type y when Univ.Universe.equal x y -> None (* false *)
| _ -> subco ())
| Prod (name, a, b), Prod (name', a', b') ->
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 2bc603a90..d7118efd7 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -281,8 +281,8 @@ let matches_core env sigma allow_bound_rels
let open Glob_term in
begin match ps, ESorts.kind sigma s with
- | GProp, Prop Null -> subst
- | GSet, Prop Pos -> subst
+ | GProp, Prop -> subst
+ | GSet, Set -> subst
| GType _, Type _ -> subst
| _ -> raise PatternMatchingFailure
end
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fe49d64c7..d0de2f8c0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -597,8 +597,8 @@ let detype_universe sigma u =
Univ.Universe.map fn u
let detype_sort sigma = function
- | Prop Null -> GProp
- | Prop Pos -> GSet
+ | Prop -> GProp
+ | Set -> GSet
| Type u ->
GType
(if !print_universes
@@ -690,8 +690,7 @@ and detype_r d flags avoid env sigma t =
let c' =
try
let pb = Environ.lookup_projection p (snd env) in
- (** FIXME: handle mutual records *)
- let ind = (pb.Declarations.proj_ind, 0) in
+ let ind = pb.Declarations.proj_ind in
let bodies = Inductiveops.legacy_match_projection (snd env) ind in
let body = bodies.(pb.Declarations.proj_arg) in
let ty = Retyping.get_type_of (snd env) sigma c in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d08f66c1..a71ef6508 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -510,7 +510,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
let tM = Stack.zip evd apprM in
miller_pfenning on_left
(fun () -> if not_only_app then (* Postpone the use of an heuristic *)
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
+ switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM
else quick_fail i)
ev lF tM i
and consume (termF,skF as apprF) (termM,skM as apprM) i =
@@ -578,7 +578,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
i,mkEvar ev
else
i,Stack.zip evd apprF in
- switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+ switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i))
tF tR
else
UnifFailure (evd,OccurCheck (fst ev,tR)))])
@@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
else UnifFailure(evd,(*dummy*)NotSameHead)
and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
match mib.Declarations.mind_record with
- | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
+ | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
+ let (_, projs, _) = info.(snd ind) in
let pars = mib.Declarations.mind_nparams in
(try
let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 8afb9b942..3f5d186d4 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -69,7 +69,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
if onlyalg && alg then
(evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
else t))
- | Prop Pos when refreshset && not direction ->
+ | Set when refreshset && not direction ->
(* Cannot make a universe "lower" than "Set",
only refreshing when we want higher universes. *)
refresh_sort status ~direction s
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1003f86c5..efb205182 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
let has_dependent_elim mib =
match mib.mind_record with
- | Some (Some _) -> mib.mind_finite == BiFinite
- | _ -> true
+ | PrimRecord _ -> mib.mind_finite == BiFinite
+ | NotRecord | FakeRecord -> true
(* Annotation for cases *)
let make_case_info env ind style =
@@ -346,8 +346,10 @@ let get_constructors env (ind,params) =
let get_projections env (ind,params) =
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
match mib.mind_record with
- | Some (Some (id, projs, pbs)) -> Some projs
- | _ -> None
+ | PrimRecord infos ->
+ let (_, projs, _) = infos.(snd (fst ind)) in
+ Some projs
+ | NotRecord | FakeRecord -> None
let make_case_or_project env sigma indf ci pred c branches =
let open EConstr in
@@ -460,25 +462,24 @@ let build_branch_type env sigma dep p cs =
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
-let compute_projections env (kn, _ as ind) =
+let compute_projections env (kn, i as ind) =
let open Term in
let mib = Environ.lookup_mind kn env in
- let indu = match mib.mind_universes with
- | Monomorphic_ind _ -> mkInd ind
- | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
- | Cumulative_ind ctx ->
- mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+ let u = match mib.mind_universes with
+ | Monomorphic_ind _ -> Instance.empty
+ | Polymorphic_ind auctx -> make_abstract_instance auctx
+ | Cumulative_ind acumi ->
+ make_abstract_instance (ACumulativityInfo.univ_context acumi)
in
let x = match mib.mind_record with
- | None | Some None ->
+ | NotRecord | FakeRecord ->
anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
- | Some (Some (id, _, _)) -> Name id
+ | PrimRecord info-> Name (pi1 (info.(i)))
in
- (** FIXME: handle mutual records *)
- let pkt = mib.mind_packets.(0) in
- let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+ let pkt = mib.mind_packets.(i) in
let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
- let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+ let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
+ let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
let mp, dp, l = MutInd.repr3 kn in
(** We build a substitution smashing the lets in the record parameters so
@@ -487,6 +488,7 @@ let compute_projections env (kn, _ as ind) =
let indty =
(* [ty] = [Ind inst] is typed in context [params] *)
let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+ let indu = mkIndU (ind, u) in
let ty = mkApp (indu, inst) in
(* [Ind inst] is typed in context [params-wo-let] *)
ty
@@ -496,8 +498,8 @@ let compute_projections env (kn, _ as ind) =
{ ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
{ ci_ind = ind;
ci_npar = nparamargs;
- ci_cstr_ndecls = mind_consnrealdecls;
- ci_cstr_nargs = mind_consnrealargs;
+ ci_cstr_ndecls = pkt.mind_consnrealdecls;
+ ci_cstr_nargs = pkt.mind_consnrealargs;
ci_pp_info = print_info }
in
let len = List.length ctx in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 4b8e0e096..16d003f67 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
try
if const then
let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
- retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp
+ Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
else
raise Not_found
with Not_found ->
@@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs =
bs ci in
Array.init (Array.length tbl) branch
-let get_proj env ((mind, _n), i) =
+let get_proj env ((mind, n), i) =
let mib = Environ.lookup_mind mind env in
match mib.mind_record with
- | None | Some None ->
+ | NotRecord | FakeRecord ->
CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
- | Some (Some (_, projs, _)) ->
+ | PrimRecord info ->
+ let _, projs, _ = info.(n) in
Projection.make projs.(i) true
let rec nf_val env sigma v typ =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 622a8e982..685aa400b 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -150,8 +150,8 @@ let pattern_of_constr env sigma t =
| Rel n -> PRel n
| Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
| Var id -> PVar id
- | Sort (Prop Null) -> PSort GProp
- | Sort (Prop Pos) -> PSort GSet
+ | Sort Prop -> PSort GProp
+ | Sort Set -> PSort GSet
| Sort (Type _) -> PSort (GType [])
| Cast (c,_,_) -> pattern_of_constr env c
| LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 746a68b21..7e43c5e41 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma =
| Cast (c,_, s) when isSort sigma s -> destSort sigma s
| Sort s ->
begin match ESorts.kind sigma s with
- | Prop _ -> Sorts.type1
+ | Prop | Set -> Sorts.type1
| Type u -> Type (Univ.super u)
end
| Prod (name,t,c2) ->
- (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with
- | _, (Prop Null as s) -> s
- | Prop _, (Prop Pos as s) -> s
- | Type _, (Prop Pos as s) when is_impredicative_set env -> s
- | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ)
- | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2)
- | Prop Null, (Type _ as s) -> s
- | Type u1, Type u2 -> Type (Univ.sup u1 u2))
+ let dom = sort_of env t in
+ let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in
+ Typeops.sort_of_product env dom rang
| App(f,args) when is_template_polymorphic env sigma f ->
let t = type_of_global_reference_knowing_parameters env f args in
sort_of_atomic_type env sigma t args
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index cf34ac016..a66ecaaac 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -241,10 +241,6 @@ let judge_of_set =
{ uj_val = EConstr.mkSet;
uj_type = EConstr.mkSort Sorts.type1 }
-let judge_of_prop_contents = function
- | Null -> judge_of_prop
- | Pos -> judge_of_set
-
let judge_of_type u =
let uu = Univ.Universe.super u in
{ uj_val = EConstr.mkType u;
@@ -333,10 +329,9 @@ let rec execute env sigma cstr =
| Sort s ->
begin match ESorts.kind sigma s with
- | Prop c ->
- sigma, judge_of_prop_contents c
- | Type u ->
- sigma, judge_of_type u
+ | Prop -> sigma, judge_of_prop
+ | Set -> sigma, judge_of_set
+ | Type u -> sigma, judge_of_type u
end
| Proj (p, c) ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5cf6e4b26..4ba5d2794 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t =
let is_eta_constructor_app env sigma ts f l1 term =
match EConstr.kind sigma f with
- | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+ | Construct (((_, i as ind), j), u) when j == 1 ->
+ let open Declarations in
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
+ | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
+ let (_, projs, _) = info.(i) in
Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
(** Check that the other term is neutral *)
is_neutral env sigma ts term
@@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term =
| _ -> false
let eta_constructor_app env sigma f l1 term =
+ let open Declarations in
match EConstr.kind sigma f with
| Construct (((_, i as ind), j), u) ->
let mib = lookup_mind (fst ind) env in
(match mib.Declarations.mind_record with
- | Some (Some (_, projs, _)) ->
+ | PrimRecord info ->
+ let (_, projs, _) = info.(i) in
let npars = mib.Declarations.mind_nparams in
let pars, l1' = Array.chop npars l1 in
let arg = Array.append pars [|term|] in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 14c9f49b1..bd6062824 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -79,7 +79,7 @@ let construct_of_constr const env tag typ =
(* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
try
if const then
- ((retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkIndU indu) tag),
+ ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag),
typ) (*spiwack: this may need to be changed in case there are parameters in the
type which may cause a constant value to have an arity.
(type_constructor seems to be all about parameters actually)
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-24 14:22:58 +0000