aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml35
-rw-r--r--kernel/cooking.mli12
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/declareops.ml25
-rw-r--r--kernel/declareops.mli1
-rw-r--r--kernel/lazyconstr.ml100
-rw-r--r--kernel/lazyconstr.mli32
-rw-r--r--kernel/mod_typing.ml8
-rw-r--r--kernel/safe_typing.ml38
-rw-r--r--kernel/term_typing.ml54
-rw-r--r--kernel/term_typing.mli4
11 files changed, 196 insertions, 121 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0a1d713c4d..75642648dd 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -23,8 +23,6 @@ open Environ
(*s Cooking the constants. *)
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-
let pop_dirpath p = match DirPath.repr p with
| [] -> anomaly ~label:"dirpath_prefix" (Pp.str "empty dirpath")
| _::l -> DirPath.make l
@@ -111,35 +109,34 @@ let abstract_constant_type =
let abstract_constant_body =
List.fold_left (fun c d -> mkNamedLambda_or_LetIn d c)
-type recipe = {
- d_from : constant_body;
- d_abstract : named_context;
- d_modlist : work_list }
-
+type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
type inline = bool
type result =
- constant_def * constant_type * constant_constraints * inline
+ constant_def * constant_type * Univ.constraints * inline
* Context.section_context option
-let on_body f = function
+let on_body ml hy f = function
| Undef _ as x -> x
| Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
| OpaqueDef lc ->
- OpaqueDef (Future.chain ~pure:true lc (fun lc ->
- (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
+ OpaqueDef (Lazyconstr.discharge_direct_lazy_constr ml hy f lc)
let constr_of_def = function
| Undef _ -> assert false
| Def cs -> Lazyconstr.force cs
- | OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
+ | OpaqueDef lc -> Lazyconstr.force_opaque lc
+
+let cook_constr { Lazyconstr.modlist ; abstract } c =
+ let cache = Hashtbl.create 13 in
+ let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
+ abstract_constant_body (expmod_constr cache modlist c) hyps
-let cook_constant env r =
+let cook_constant env { from = cb; info = { Lazyconstr.modlist; abstract } } =
let cache = Hashtbl.create 13 in
- let cb = r.d_from in
- let hyps = Context.map_named_context (expmod_constr cache r.d_modlist) r.d_abstract in
- let body = on_body
- (fun c -> abstract_constant_body (expmod_constr cache r.d_modlist c) hyps)
+ let hyps = Context.map_named_context (expmod_constr cache modlist) abstract in
+ let body = on_body modlist hyps
+ (fun c -> abstract_constant_body (expmod_constr cache modlist c) hyps)
cb.const_body
in
let const_hyps =
@@ -149,12 +146,12 @@ let cook_constant env r =
let typ = match cb.const_type with
| NonPolymorphicType t ->
let typ =
- abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
+ abstract_constant_type (expmod_constr cache modlist t) hyps in
NonPolymorphicType typ
| PolymorphicArity (ctx,s) ->
let t = mkArity (ctx,Type s.poly_level) in
let typ =
- abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
+ abstract_constant_type (expmod_constr cache modlist t) hyps in
let j = make_judge (constr_of_def body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 2d6e534070..05c7a20400 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -14,22 +14,18 @@ open Univ
(** {6 Cooking the constants. } *)
-type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
-
-type recipe = {
- d_from : constant_body;
- d_abstract : Context.named_context;
- d_modlist : work_list }
+type recipe = { from : constant_body; info : Lazyconstr.cooking_info }
type inline = bool
type result =
- constant_def * constant_type * constant_constraints * inline
+ constant_def * constant_type * Univ.constraints * inline
* Context.section_context option
val cook_constant : env -> recipe -> result
+val cook_constr : Lazyconstr.cooking_info -> Term.constr -> Term.constr
(** {6 Utility functions used in module [Discharge]. } *)
-val expmod_constr : work_list -> constr -> constr
+val expmod_constr : Lazyconstr.work_list -> constr -> constr
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index d92b667073..ef56ae5123 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -38,16 +38,16 @@ type inline = int option
type constant_def =
| Undef of inline
| Def of Lazyconstr.constr_substituted
- | OpaqueDef of Lazyconstr.lazy_constr Future.computation
-
-type constant_constraints = Univ.constraints Future.computation
+ | OpaqueDef of Lazyconstr.lazy_constr
+(* some contraints are in constant_constraints, some other may be in
+ * the OpaueDef *)
type constant_body = {
const_hyps : Context.section_context; (** New: younger hyp at top *)
const_body : constant_def;
const_type : constant_type;
const_body_code : Cemitcodes.to_patch_substituted;
- const_constraints : constant_constraints;
+ const_constraints : Univ.constraints;
const_inline_code : bool }
type side_effect =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index e40441d74c..21a961fc3e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,7 +19,13 @@ open Util
let body_of_constant cb = match cb.const_body with
| Undef _ -> None
| Def c -> Some (Lazyconstr.force c)
- | OpaqueDef lc -> Some (Lazyconstr.force_opaque (Future.force lc))
+ | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
+
+let constraints_of_constant cb = Univ.union_constraints cb.const_constraints
+ (match cb.const_body with
+ | Undef _ -> Univ.empty_constraint
+ | Def c -> Univ.empty_constraint
+ | OpaqueDef lc -> snd (Lazyconstr.force_opaque_w_constraints lc))
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
@@ -52,8 +58,7 @@ let subst_const_type sub arity = match arity with
let subst_const_def sub def = match def with
| Undef _ -> def
| Def c -> Def (subst_constr_subst sub c)
- | OpaqueDef lc ->
- OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
+ | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
let subst_const_body sub cb =
assert (List.is_empty cb.const_hyps); (* we're outside sections *)
@@ -101,20 +106,13 @@ let hcons_const_def = function
| Def l_constr ->
let constr = force l_constr in
Def (from_val (Term.hcons_constr constr))
- | OpaqueDef lc ->
- OpaqueDef
- (Future.chain ~greedy:true ~pure:true lc
- (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc))))
+ | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
let hcons_const_body cb =
{ cb with
const_body = hcons_const_def cb.const_body;
const_type = hcons_const_type cb.const_type;
- const_constraints =
- if Future.is_val cb.const_constraints then
- Future.from_val
- (Univ.hcons_constraints (Future.force cb.const_constraints))
- else cb.const_constraints }
+ const_constraints = Univ.hcons_constraints cb.const_constraints; }
(** {6 Inductive types } *)
@@ -239,9 +237,8 @@ let hcons_mind mib =
(** {6 Stm machinery } *)
let join_constant_body cb =
- ignore(Future.join cb.const_constraints);
match cb.const_body with
- | OpaqueDef d -> ignore(Future.join d)
+ | OpaqueDef d -> Lazyconstr.join_lazy_constr d
| _ -> ()
let string_of_side_effect = function
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 177ae9d45e..800b167abd 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -24,6 +24,7 @@ val constant_has_body : constant_body -> bool
Only use this function if you know what you're doing. *)
val body_of_constant : constant_body -> Term.constr option
+val constraints_of_constant : constant_body -> Univ.constraints
val is_opaque : constant_body -> bool
diff --git a/kernel/lazyconstr.ml b/kernel/lazyconstr.ml
index 21aba6348a..23d6d559d9 100644
--- a/kernel/lazyconstr.ml
+++ b/kernel/lazyconstr.ml
@@ -10,6 +10,9 @@ open Names
open Term
open Mod_subst
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context }
+
(** [constr_substituted] are [constr] with possibly pending
substitutions of kernel names. *)
@@ -29,48 +32,103 @@ let subst_constr_subst = subst_substituted
should end in a .vo, this is checked by coqchk.
*)
+type proofterm = (constr * Univ.constraints) Future.computation
type lazy_constr =
- | Indirect of substitution list * DirPath.t * int (* lib,index *)
- | Direct of constr_substituted (* opaque in section or interactive session *)
+ (* subst, lib, index *)
+ | Indirect of substitution list * DirPath.t * int
+ (* opaque in section or interactive session *)
+ | Direct of cooking_info list * (constr_substituted * Univ.constraints) Future.computation
(* TODO : this hcons function could probably be improved (for instance
hash the dir_path in the Indirect case) *)
-let hcons_lazy_constr = function
- | Direct c -> Direct (from_val (hcons_constr (force c)))
- | Indirect _ as lc -> lc
-
let subst_lazy_constr sub = function
- | Direct cs -> Direct (subst_constr_subst sub cs)
+ | Direct ([],cu) ->
+ Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
+ subst_constr_subst sub c, u))
+ | Direct _ -> Errors.anomaly (Pp.str"still direct but not discharged")
| Indirect (l,dp,i) -> Indirect (sub::l,dp,i)
+let iter_direct_lazy_constr f = function
+ | Indirect _ -> Errors.anomaly (Pp.str "iter_direct_lazy_constr")
+ | Direct (d,cu) ->
+ Direct (d, Future.chain ~greedy:true ~pure:true cu (fun (c, u) -> f (force c); c, u))
+
+let discharge_direct_lazy_constr modlist abstract f = function
+ | Indirect _ -> Errors.anomaly (Pp.str "discharge_direct_lazy_constr")
+ | Direct (d,cu) ->
+ Direct ({ modlist; abstract }::d,
+ Future.chain ~greedy:true ~pure:true cu (fun (c, u) ->
+ from_val (f (force c)), u))
+
let default_get_opaque dp _ =
Errors.error
- ("Cannot access an opaque term in library " ^ DirPath.to_string dp)
+ ("Cannot access opaque proofs in library " ^ DirPath.to_string dp)
+let default_get_univ dp _ =
+ Errors.error
+ ("Cannot access universe constraints of opaque proofs in library " ^
+ DirPath.to_string dp)
-let default_mk_opaque _ = None
+let default_mk_indirect _ = None
+
+let default_join_indirect_local_opaque _ _ = ()
+let default_join_indirect_local_univ _ _ = ()
let get_opaque = ref default_get_opaque
-let mk_opaque = ref default_mk_opaque
+let get_univ = ref default_get_univ
+let join_indirect_local_opaque = ref default_join_indirect_local_opaque
+let join_indirect_local_univ = ref default_join_indirect_local_univ
+
+let mk_indirect = ref default_mk_indirect
let set_indirect_opaque_accessor f = (get_opaque := f)
-let set_indirect_opaque_creator f = (mk_opaque := f)
-let reset_indirect_opaque_creator () = (mk_opaque := default_mk_opaque)
+let set_indirect_univ_accessor f = (get_univ := f)
+let set_indirect_creator f = (mk_indirect := f)
+let set_join_indirect_local_opaque f = join_indirect_local_opaque := f
+let set_join_indirect_local_univ f = join_indirect_local_univ := f
+
+let reset_indirect_creator () = mk_indirect := default_mk_indirect
let force_lazy_constr = function
- | Direct c -> c
+ | Direct (_,c) -> Future.force c
| Indirect (l,dp,i) ->
- List.fold_right subst_constr_subst l (from_val (!get_opaque dp i))
+ let c = Future.force (!get_opaque dp i) in
+ List.fold_right subst_constr_subst l (from_val c),
+ Future.force
+ (Option.default
+ (Future.from_val Univ.empty_constraint)
+ (!get_univ dp i))
+
+let join_lazy_constr = function
+ | Direct (_,c) -> ignore(Future.force c)
+ | Indirect (_,dp,i) ->
+ !join_indirect_local_opaque dp i;
+ !join_indirect_local_univ dp i
let turn_indirect lc = match lc with
| Indirect _ ->
Errors.anomaly (Pp.str "Indirecting an already indirect opaque")
- | Direct c ->
- (* this constr_substituted shouldn't have been substituted yet *)
- assert (fst (Mod_subst.repr_substituted c) == None);
- match !mk_opaque (force c) with
+ | Direct (d,cu) ->
+ let cu = Future.chain ~greedy:true ~pure:true cu (fun (c,u) ->
+ (* this constr_substituted shouldn't have been substituted yet *)
+ assert (fst (Mod_subst.repr_substituted c) == None);
+ hcons_constr (force c),u) in
+ match !mk_indirect (d,cu) with
| None -> lc
| Some (dp,i) -> Indirect ([],dp,i)
-let force_opaque lc = force (force_lazy_constr lc)
-
-let opaque_from_val c = Direct (from_val c)
+let force_opaque lc =
+ let c, _u = force_lazy_constr lc in force c
+let force_opaque_w_constraints lc =
+ let c, u = force_lazy_constr lc in force c, u
+let get_opaque_future_constraints lc = match lc with
+ | Indirect (_,dp,i) -> !get_univ dp i
+ | Direct (_,cu) -> Some(snd (Future.split2 ~greedy:true cu))
+let get_opaque_futures lc = match lc with
+ | Indirect _ -> assert false
+ | Direct (_,cu) ->
+ let cu =
+ Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> force c, u) in
+ Future.split2 ~greedy:true cu
+
+let opaque_from_val cu =
+ Direct ([],Future.chain ~greedy:true ~pure:true cu (fun (c,u) -> from_val c, u))
diff --git a/kernel/lazyconstr.mli b/kernel/lazyconstr.mli
index f6188f5364..db4d8fb726 100644
--- a/kernel/lazyconstr.mli
+++ b/kernel/lazyconstr.mli
@@ -10,6 +10,9 @@ open Names
open Term
open Mod_subst
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
+type cooking_info = { modlist : work_list; abstract : Context.named_context }
+
(** [constr_substituted] are [constr] with possibly pending
substitutions of kernel names. *)
@@ -25,9 +28,10 @@ val subst_constr_subst :
this might trigger the read of some extra parts of .vo files *)
type lazy_constr
+type proofterm = (constr * Univ.constraints) Future.computation
(** From a [constr] to some (immediate) [lazy_constr]. *)
-val opaque_from_val : constr -> lazy_constr
+val opaque_from_val : proofterm -> lazy_constr
(** Turn an immediate [lazy_constr] into an indirect one, thanks
to the indirect opaque creator configured below. *)
@@ -36,10 +40,22 @@ val turn_indirect : lazy_constr -> lazy_constr
(** From a [lazy_constr] back to a [constr]. This might use the
indirect opaque accessor configured below. *)
val force_opaque : lazy_constr -> constr
+val force_opaque_w_constraints : lazy_constr -> constr * Univ.constraints
+val get_opaque_future_constraints :
+ lazy_constr -> Univ.constraints Future.computation option
+val get_opaque_futures :
+ lazy_constr ->
+ Term.constr Future.computation * Univ.constraints Future.computation
val subst_lazy_constr : substitution -> lazy_constr -> lazy_constr
-val hcons_lazy_constr : lazy_constr -> lazy_constr
+(* val hcons_lazy_constr : lazy_constr -> lazy_constr *)
+
+(* Used to discharge the proof term. *)
+val iter_direct_lazy_constr : (constr -> unit) -> lazy_constr -> lazy_constr
+val discharge_direct_lazy_constr : work_list -> Context.named_context -> (constr -> constr) -> lazy_constr -> lazy_constr
+
+val join_lazy_constr : lazy_constr -> unit
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The following two functions activate
@@ -48,6 +64,12 @@ val hcons_lazy_constr : lazy_constr -> lazy_constr
any indirect link, and default accessor always raises an error.
*)
-val set_indirect_opaque_creator : (constr -> (DirPath.t * int) option) -> unit
-val set_indirect_opaque_accessor : (DirPath.t -> int -> constr) -> unit
-val reset_indirect_opaque_creator : unit -> unit
+val set_indirect_creator :
+ (cooking_info list * proofterm -> (DirPath.t * int) option) -> unit
+val set_indirect_opaque_accessor :
+ (DirPath.t -> int -> Term.constr Future.computation) -> unit
+val set_indirect_univ_accessor :
+ (DirPath.t -> int -> Univ.constraints Future.computation option) -> unit
+val set_join_indirect_local_opaque : (DirPath.t -> int -> unit) -> unit
+val set_join_indirect_local_univ : (DirPath.t -> int -> unit) -> unit
+val reset_indirect_creator : unit -> unit
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 7794f19be0..6e656fad9c 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -77,11 +77,11 @@ let rec check_with_def env struc (idl,c) mp equiv =
let j,cst1 = Typeops.infer env' c in
let typ = Typeops.type_of_constant_type env' cb.const_type in
let cst2 = Reduction.conv_leq env' j.uj_type typ in
- let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in
- j.uj_val,cst
+ let cst = cb.const_constraints +++ cst1 +++ cst2 in
+ j.uj_val, cst
| Def cs ->
let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
- let cst = Future.force cb.const_constraints +++ cst1 in
+ let cst = cb.const_constraints +++ cst1 in
c, cst
in
let def = Def (Lazyconstr.from_val c') in
@@ -89,7 +89,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
{ cb with
const_body = def;
const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
- const_constraints = Future.from_val cst }
+ const_constraints = cst }
in
before@(lab,SFBconst(cb'))::after, c', cst
else
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3e9b646c17..a93415f928 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -282,11 +282,11 @@ let safe_push_named (id,_,_ as d) env =
let push_named_def (id,de) senv =
let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
- let c = match c with
- | Def c -> Lazyconstr.force c
- | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
+ let c,cst' = match c with
+ | Def c -> Lazyconstr.force c, Univ.empty_constraint
+ | OpaqueDef c -> Lazyconstr.force_opaque_w_constraints c
| _ -> assert false in
- let cst = Future.join cst in
+ let senv = add_constraints (Now cst') senv in
let senv' = add_constraints (Now cst) senv in
let env'' = safe_push_named (id,Some c,typ) senv'.env in
(cst, {senv' with env=env''})
@@ -314,13 +314,19 @@ let labels_of_mib mib =
get ()
let constraints_of_sfb = function
- | SFBmind mib -> Now mib.mind_constraints
- | SFBmodtype mtb -> Now mtb.typ_constraints
- | SFBmodule mb -> Now mb.mod_constraints
- | SFBconst cb ->
- match Future.peek_val cb.const_constraints with
- | Some c -> Now c
- | None -> Later cb.const_constraints
+ | SFBmind mib -> [Now mib.mind_constraints]
+ | SFBmodtype mtb -> [Now mtb.typ_constraints]
+ | SFBmodule mb -> [Now mb.mod_constraints]
+ | SFBconst cb -> [Now cb.const_constraints] @
+ match cb.const_body with
+ | (Undef _ | Def _) -> []
+ | OpaqueDef lc ->
+ match Lazyconstr.get_opaque_future_constraints lc with
+ | None -> []
+ | Some fc ->
+ match Future.peek_val fc with
+ | None -> [Later fc]
+ | Some c -> [Now c]
(** A generic function for adding a new field in a same environment.
It also performs the corresponding [add_constraints]. *)
@@ -341,7 +347,7 @@ let add_field ((l,sfb) as field) gn senv =
| SFBmodule _ | SFBmodtype _ ->
check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
in
- let senv = add_constraints (constraints_of_sfb sfb) senv in
+ let senv = List.fold_right add_constraints (constraints_of_sfb sfb) senv in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
| SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -377,8 +383,7 @@ let add_constant dir l decl senv =
| OpaqueDef lc when DirPath.is_empty dir ->
(* In coqc, opaque constants outside sections will be stored
indirectly in a specific table *)
- { cb with const_body =
- OpaqueDef (Future.chain ~greedy:true ~pure:true lc Lazyconstr.turn_indirect) }
+ { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
| _ -> cb
in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -660,10 +665,11 @@ let start_library dir senv =
let export compilation_mode senv dir =
let senv =
try
- if compilation_mode = Flags.BuildVi then senv (* FIXME: cleanup future*)
+ if compilation_mode = Flags.BuildVi then { senv with future_cst = [] }
else join_safe_environment senv
- with e -> Errors.errorlabstrm "future" (Errors.print e)
+ with e -> Errors.errorlabstrm "export" (Errors.print e)
in
+ assert(senv.future_cst = []);
let () = check_current_library dir senv in
let mp = senv.modpath in
let str = NoFunctor (List.rev senv.revstruct) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 55901bce93..f059ea1ae4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -28,15 +28,21 @@ let prerr_endline =
if debug then prerr_endline else fun _ -> ()
let constrain_type env j cst1 = function
- | None ->
+ | `None ->
make_polymorphic_if_constant_for_ind env j, cst1
- | Some t ->
+ | `Some t ->
let (tj,cst2) = infer_type env t in
let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
assert (eq_constr t tj.utj_val);
let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
NonPolymorphicType t, cstrs
+ | `SomeWJ (t, tj, cst2) ->
+ let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
+ assert (eq_constr t tj.utj_val);
+ let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
+ NonPolymorphicType t, cstrs
+let map_option_typ = function None -> `None | Some x -> `Some x
let translate_local_assum env t =
let (j,cst) = infer env t in
@@ -68,7 +74,7 @@ let handle_side_effects env body side_eff =
let t = sub c 1 (Vars.lift 1 t) in
mkLetIn (cname c, b, b_ty, t)
| OpaqueDef b ->
- let b = Lazyconstr.force_opaque (Future.join b) in
+ let b = Lazyconstr.force_opaque b in
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
@@ -84,28 +90,27 @@ let hcons_j j =
let feedback_completion_typecheck =
Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete)
-(* what is used for debugging only *)
-let infer_declaration ?(what="UNKNOWN") env dcl =
+let infer_declaration env dcl =
match dcl with
| ParameterEntry (ctx,t,nl) ->
let j, cst = infer env t in
let t = hcons_constr (Typeops.assumption_of_judgment env j) in
- Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
+ Undef nl, NonPolymorphicType t, cst, false, ctx
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true } as c) ->
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
- let body_cst =
+ let tyj, tycst = infer_type env typ in
+ let proofterm =
Future.chain ~greedy:true ~pure:true body (fun (body, side_eff) ->
let body = handle_side_effects env body side_eff in
let j, cst = infer env body in
let j = hcons_j j in
- let _typ, cst = constrain_type env j cst (Some typ) in
+ let _typ, cst = constrain_type env j cst (`SomeWJ (typ,tyj,tycst)) in
feedback_completion_typecheck feedback_id;
- Lazyconstr.opaque_from_val j.uj_val, cst) in
- let body, cst = Future.split2 ~greedy:true body_cst in
- let def = OpaqueDef body in
+ j.uj_val, cst) in
+ let def = OpaqueDef (Lazyconstr.opaque_from_val proofterm) in
let typ = NonPolymorphicType typ in
- def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+ def, typ, tycst, c.const_entry_inline_code, c.const_entry_secctx
| DefinitionEntry c ->
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
@@ -113,10 +118,9 @@ let infer_declaration ?(what="UNKNOWN") env dcl =
let body = handle_side_effects env body side_eff in
let j, cst = infer env body in
let j = hcons_j j in
- let typ, cst = constrain_type env j cst typ in
+ let typ, cst = constrain_type env j cst (map_option_typ typ) in
feedback_completion_typecheck feedback_id;
let def = Def (Lazyconstr.from_val j.uj_val) in
- let cst = Future.from_val cst in
def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
let global_vars_set_constant_type env = function
@@ -127,7 +131,6 @@ let global_vars_set_constant_type env = function
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
-
let record_aux env s1 s2 =
let v =
String.concat " "
@@ -157,16 +160,13 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
let ids_def = match def with
| Undef _ -> Idset.empty
| Def cs -> global_vars_set env (Lazyconstr.force cs)
- | OpaqueDef lc ->
- (* we force so that cst are added to the env immediately after *)
- ignore(Future.join cst);
- let vars =
- global_vars_set env (Lazyconstr.force_opaque (Future.join lc)) in
+ | OpaqueDef lc ->
+ let vars = global_vars_set env (Lazyconstr.force_opaque lc) in
!suggest_proof_using kn env vars ids_typ context_ids;
if !Flags.compilation_mode = Flags.BuildVo then
record_aux env ids_typ vars;
vars
- in
+ in
keep_hyps env (Idset.union ids_typ ids_def), def
| None ->
if !Flags.compilation_mode = Flags.BuildVo then
@@ -184,12 +184,11 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
check declared inferred;
x
| OpaqueDef lc -> (* In this case we can postpone the check *)
- OpaqueDef (Future.chain ~greedy:true ~pure:true lc (fun lc ->
+ OpaqueDef (Lazyconstr.iter_direct_lazy_constr (fun c ->
let ids_typ = global_vars_set_constant_type env typ in
- let ids_def =
- global_vars_set env (Lazyconstr.force_opaque lc) in
+ let ids_def = global_vars_set env c in
let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
- check declared inferred; lc)) in
+ check declared inferred) lc) in
{ const_hyps = hyps;
const_body = def;
const_type = typ;
@@ -200,8 +199,7 @@ let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
(*s Global and local constant declaration. *)
let translate_constant env kn ce =
- build_constant_declaration kn env
- (infer_declaration ~what:(string_of_con kn) env ce)
+ build_constant_declaration kn env (infer_declaration env ce)
let translate_recipe env kn r =
let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
@@ -209,7 +207,7 @@ let translate_recipe env kn r =
let translate_local_def env id centry =
let def,typ,cst,inline_code,ctx =
- infer_declaration ~what:(string_of_id id) env (DefinitionEntry centry) in
+ infer_declaration env (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
def, typ, cst
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 6f71ecd82f..b1c336ad9a 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -14,7 +14,7 @@ open Declarations
open Entries
val translate_local_def : env -> Id.t -> definition_entry ->
- constant_def * types * constant_constraints
+ constant_def * types * Univ.constraints
val translate_local_assum : env -> types -> types * constraints
@@ -32,7 +32,7 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result
+val infer_declaration : env -> constant_entry -> Cooking.result
val build_constant_declaration :
constant -> env -> Cooking.result -> constant_body
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:16:31 +0000