aboutsummaryrefslogtreecommitdiff
path: root/kernel/term_typing.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/term_typing.ml')
-rw-r--r--kernel/term_typing.ml74
1 files changed, 51 insertions, 23 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f9fdbdd68e..929f1c13a3 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -65,23 +65,15 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
Feedback.feedback ~id:state_id Feedback.Complete)
-let abstract_constant_universes = function
- | Monomorphic_const_entry uctx ->
- Univ.empty_level_subst, Monomorphic_const uctx
- | Polymorphic_const_entry (nas, uctx) ->
- let sbst, auctx = Univ.abstract_universes nas uctx in
- let sbst = Univ.make_instance_subst sbst in
- sbst, Polymorphic_const auctx
-
let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
match dcl with
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
- | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
- | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
+ | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env
+ | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env
in
let j = infer env t in
- let usubst, univs = abstract_constant_universes uctx in
+ let usubst, univs = Declareops.abstract_universes uctx in
let c = Typeops.assumption_of_judgment env j in
let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
{
@@ -93,13 +85,48 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
cook_context = ctx;
}
+ (** Primitives cannot be universe polymorphic *)
+ | PrimitiveEntry ({ prim_entry_type = otyp;
+ prim_entry_univs = uctxt;
+ prim_entry_content = op_t;
+ }) ->
+ let env = push_context_set ~strict:true uctxt env in
+ let ty = match otyp with
+ | Some typ ->
+ let tyj = infer_type env typ in
+ check_primitive_type env op_t tyj.utj_val;
+ Constr.hcons tyj.utj_val
+ | None ->
+ match op_t with
+ | CPrimitives.OT_op op -> type_of_prim env op
+ | CPrimitives.OT_type _ -> mkSet
+ in
+ let cd =
+ match op_t with
+ | CPrimitives.OT_op op -> Declarations.Primitive op
+ | CPrimitives.OT_type _ -> Undef None in
+ { Cooking.cook_body = cd;
+ cook_type = ty;
+ cook_universes = Monomorphic uctxt;
+ cook_private_univs = None;
+ cook_inline = false;
+ cook_context = None
+ }
+
(** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
so we delay the typing and hash consing of its body.
Remark: when the universe quantification is given explicitly, we could
delay even in the polymorphic case. *)
+
+(** Definition is opaque (Qed) and non polymorphic with known type, so we delay
+the typing and hash consing of its body.
+
+TODO: if the universe quantification is given explicitly, we could delay even in
+the polymorphic case
+ *)
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
- const_entry_universes = Monomorphic_const_entry univs; _ } as c) ->
+ const_entry_universes = Monomorphic_entry univs; _ } as c) ->
let env = push_context_set ~strict:true univs env in
let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in
let tyj = infer_type env typ in
@@ -130,7 +157,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{
Cooking.cook_body = def;
cook_type = typ;
- cook_universes = Monomorphic_const univs;
+ cook_universes = Monomorphic univs;
cook_private_univs = None;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -148,11 +175,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
body, Univ.ContextSet.union ctx ctx'
in
let env, usubst, univs, private_univs = match c.const_entry_universes with
- | Monomorphic_const_entry univs ->
+ | Monomorphic_entry univs ->
let ctx = Univ.ContextSet.union univs ctx in
let env = push_context_set ~strict:true ctx env in
- env, Univ.empty_level_subst, Monomorphic_const ctx, None
- | Polymorphic_const_entry (nas, uctx) ->
+ env, Univ.empty_level_subst, Monomorphic ctx, None
+ | Polymorphic_entry (nas, uctx) ->
(** [ctx] must contain local universes, such that it has no impact
on the rest of the graph (up to transitivity). *)
let env = push_context ~strict:false uctx env in
@@ -165,7 +192,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
if Univ.ContextSet.is_empty ctx then env, None
else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
in
- env, sbst, Polymorphic_const auctx, local
+ env, sbst, Polymorphic auctx, local
in
let j = infer env body in
let typ = match typ with
@@ -238,7 +265,7 @@ let build_constant_declaration _kn env result =
we must look at the body NOW, if any *)
let ids_typ = global_vars_set env typ in
let ids_def = match def with
- | Undef _ -> Id.Set.empty
+ | Undef _ | Primitive _ -> Id.Set.empty
| Def cs -> global_vars_set env (Mod_subst.force_constr cs)
| OpaqueDef lc ->
let vars =
@@ -258,7 +285,7 @@ let build_constant_declaration _kn env result =
(* We use the declared set and chain a check of correctness *)
sort declared,
match def with
- | Undef _ as x -> x (* nothing to check *)
+ | Undef _ | Primitive _ as x -> x (* nothing to check *)
| Def cs as x ->
let ids_typ = global_vars_set env typ in
let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
@@ -307,7 +334,7 @@ let translate_local_def env _id centry =
const_entry_secctx = centry.secdef_secctx;
const_entry_feedback = centry.secdef_feedback;
const_entry_type = centry.secdef_type;
- const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty;
+ const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
const_entry_opaque = false;
const_entry_inline_code = false;
} in
@@ -316,6 +343,7 @@ let translate_local_def env _id centry =
if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
match decl.cook_body with
| Undef _ -> ()
+ | Primitive _ -> ()
| Def _ -> ()
| OpaqueDef lc ->
let ids_typ = global_vars_set env typ in
@@ -324,8 +352,8 @@ let translate_local_def env _id centry =
record_aux env ids_typ ids_def
end;
let () = match decl.cook_universes with
- | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx)
- | Polymorphic_const _ -> assert false
+ | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+ | Polymorphic _ -> assert false
in
let c = match decl.cook_body with
| Def c -> Mod_subst.force_constr c
@@ -336,7 +364,7 @@ let translate_local_def env _id centry =
the body by virtue of the typing of [Entries.section_def_entry]. *)
let () = assert (Univ.ContextSet.is_empty cst) in
p
- | Undef _ -> assert false
+ | Undef _ | Primitive _ -> assert false
in
c, typ
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 03:04:37 +0000