aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-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
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
-rw-r--r--library/declare.ml23
-rw-r--r--library/lib.ml9
-rw-r--r--library/lib.mli5
-rw-r--r--library/library.ml187
-rw-r--r--library/library.mli15
-rw-r--r--plugins/extraction/extraction.ml4
-rw-r--r--printing/prettyp.ml7
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/discharge.mli1
-rw-r--r--toplevel/stm.ml108
-rw-r--r--toplevel/stm.mli5
-rw-r--r--toplevel/toplevel.mllib2
-rw-r--r--toplevel/vernac.ml12
-rw-r--r--toplevel/vi_checking.ml4
28 files changed, 481 insertions, 225 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 0a1d713c4..75642648d 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 2d6e53407..05c7a2040 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 d92b66707..ef56ae512 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 e40441d74..21a961fc3 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 177ae9d45..800b167ab 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 21aba6348..23d6d559d 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 f6188f536..db4d8fb72 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 7794f19be..6e656fad9 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 3e9b646c1..a93415f92 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 55901bce9..f059ea1ae 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 6f71ecd82..b1c336ad9 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
diff --git a/lib/flags.ml b/lib/flags.ml
index 9832ba587..91e28132a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -45,7 +45,7 @@ let boot = ref false
let batch_mode = ref false
-type compilation_mode = BuildVo | BuildVi
+type compilation_mode = BuildVo | BuildVi | Vi2Vo
let compilation_mode = ref BuildVo
type async_proofs = APoff | APonLazy | APonParallel of int
diff --git a/lib/flags.mli b/lib/flags.mli
index ecaa11388..6c6aa5fbe 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,7 +11,7 @@
val boot : bool ref
val batch_mode : bool ref
-type compilation_mode = BuildVo | BuildVi
+type compilation_mode = BuildVo | BuildVi | Vi2Vo
val compilation_mode : compilation_mode ref
type async_proofs = APoff | APonLazy | APonParallel of int
diff --git a/library/declare.ml b/library/declare.ml
index 3bd4cdd3f..477e96bd8 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -117,7 +117,13 @@ let open_constant i ((sp,kn), obj) =
if obj.cst_locl then ()
else
let con = Global.constant_of_delta_kn kn in
- Nametab.push (Nametab.Exactly i) sp (ConstRef con)
+ Nametab.push (Nametab.Exactly i) sp (ConstRef con);
+ match (Global.lookup_constant con).const_body with
+ | (Def _ | Undef _) -> ()
+ | OpaqueDef lc ->
+ match Lazyconstr.get_opaque_future_constraints lc with
+ | Some f when Future.is_val f -> Global.add_constraints (Future.force f)
+ | _ -> ()
let exists_name id =
variable_exists id || Global.exists_objlabel (Label.of_id id)
@@ -144,12 +150,12 @@ let discharged_hyps kn sechyps =
let discharge_constant ((sp, kn), obj) =
let con = constant_of_kn kn in
- let cb = Global.lookup_constant con in
- let repl = replacement_context () in
- let sechyps = section_segment_of_constant con in
- let recipe = { d_from=cb; d_modlist=repl; d_abstract=named_of_variable_context sechyps } in
- let new_hyps = (discharged_hyps kn sechyps) @ obj.cst_hyps in
- let new_decl = GlobalRecipe recipe in
+ let from = Global.lookup_constant con in
+ let modlist = replacement_context () in
+ let hyps = section_segment_of_constant con in
+ let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in
+ let abstract = named_of_variable_context hyps in
+ let new_decl = GlobalRecipe{ from; info = { Lazyconstr.modlist; abstract }} in
Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; }
(* Hack to reduce the size of .vo: we keep only what load/open needs *)
@@ -192,8 +198,7 @@ let declare_sideff se =
let pt_opaque_of cb =
match cb with
| { const_body = Def sc } -> Lazyconstr.force sc, false
- | { const_body = OpaqueDef fc } ->
- Lazyconstr.force_opaque (Future.force fc), true
+ | { const_body = OpaqueDef fc } -> Lazyconstr.force_opaque fc, true
| { const_body = Undef _ } -> anomaly(str"Undefined side effect")
in
let ty_of cb =
diff --git a/library/lib.ml b/library/lib.ml
index eef8171cc..ee89bb997 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -385,7 +385,7 @@ type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap
let sectab =
Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
- Cooking.work_list * abstr_list) list)
+ Lazyconstr.work_list * abstr_list) list)
~name:"section-context"
let add_section () =
@@ -455,6 +455,13 @@ let section_instance = function
let is_in_section ref =
try ignore (section_instance ref); true with Not_found -> false
+let full_replacement_context () = List.map pi2 !sectab
+let full_section_segment_of_constant con =
+ List.map (fun (vars,_,(x,_)) -> fun hyps ->
+ named_of_variable_context
+ (try Names.Cmap.find con x
+ with Not_found -> extract_hyps (vars, hyps))) !sectab
+
(*************)
(* Sections. *)
diff --git a/library/lib.mli b/library/lib.mli
index fa3bd3f48..787dc969e 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -186,4 +186,9 @@ val discharge_con : Names.constant -> Names.constant
val discharge_global : Globnames.global_reference -> Globnames.global_reference
val discharge_inductive : Names.inductive -> Names.inductive
+(* discharging a constant in one go *)
+val full_replacement_context : unit -> Lazyconstr.work_list list
+val full_section_segment_of_constant :
+ Names.constant -> (Context.named_context -> Context.named_context) list
+
diff --git a/library/library.ml b/library/library.ml
index 1088bcb16..c40f9d204 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -299,12 +299,10 @@ exception Faulty
(** Fetching a table of opaque terms at position [pos] in file [f],
expecting to find first a copy of [digest]. *)
-let fetch_opaque_table dp (f,pos,digest) =
- if !Flags.load_proofs == Flags.Dont then
- error "Not accessing an opaque term due to option -dont-load-proofs.";
+let fetch_table what dp (f,pos,digest) =
let dir_path = Names.DirPath.to_string dp in
try
- Pp.msg_info (Pp.str "Fetching opaque terms from disk for " ++ str dir_path);
+ msg_info (str"Fetching " ++ str what++str" from disk for " ++ str dir_path);
let ch = System.with_magic_number_check raw_intern_library f in
let () = seek_in ch pos in
if not (String.equal (System.digest_in f ch) digest) then raise Faulty;
@@ -316,64 +314,129 @@ let fetch_opaque_table dp (f,pos,digest) =
table
with e when Errors.noncritical e ->
error
- ("The file "^f^" (bound to " ^ dir_path ^ ") is inaccessible or corrupted,\n"
- ^ "cannot load some opaque constant bodies in it.\n")
+ ("The file "^f^" (bound to " ^ dir_path ^
+ ") is inaccessible or corrupted,\n" ^
+ "cannot load some "^what^" in it.\n")
(** Delayed / available tables of opaque terms *)
-type opaque_table_status =
+type 'a table_status =
| ToFetch of string * int * Digest.t
- | Fetched of Term.constr array
+ | Fetched of 'a Future.computation array
-let opaque_tables = ref (LibraryMap.empty : opaque_table_status LibraryMap.t)
+let opaque_tables =
+ ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t)
+let univ_tables =
+ ref (LibraryMap.empty : (Univ.constraints table_status) LibraryMap.t)
let add_opaque_table dp st =
opaque_tables := LibraryMap.add dp st !opaque_tables
+let add_univ_table dp st =
+ univ_tables := LibraryMap.add dp st !univ_tables
-let access_opaque_table dp i =
- let t = match LibraryMap.find dp !opaque_tables with
+let access_table fetch_table add_table tables dp i =
+ let t = match LibraryMap.find dp tables with
| Fetched t -> t
| ToFetch (f,pos,digest) ->
- let t = fetch_opaque_table dp (f,pos,digest) in
- add_opaque_table dp (Fetched t);
+ let t = fetch_table dp (f,pos,digest) in
+ add_table dp (Fetched t);
t
in
assert (i < Array.length t); t.(i)
+let access_opaque_table dp i =
+ if !Flags.load_proofs == Flags.Dont then
+ error "Not accessing an opaque term due to option -dont-load-proofs.";
+ access_table
+ (fetch_table "opaque proofs")
+ add_opaque_table !opaque_tables dp i
+let access_univ_table dp i =
+ access_table
+ (fetch_table "universe constraints of opaque proofs")
+ add_univ_table !univ_tables dp i
+
(** Table of opaque terms from the library currently being compiled *)
module OpaqueTables = struct
- let a_constr = Term.mkRel 1
+ let a_constr = Future.from_val (Term.mkRel 1)
+ let a_univ = Future.from_val Univ.empty_constraint
+ let a_discharge : Lazyconstr.cooking_info list = []
- let local_table = ref (Array.make 100 a_constr)
+ let local_opaque_table = ref (Array.make 100 a_constr)
+ let local_univ_table = ref (Array.make 100 a_univ)
+ let local_discharge_table = ref (Array.make 100 a_discharge)
let local_index = ref 0
- let get dp i =
+ module FMap = Map.Make(Future.UUID)
+ let f2t = ref FMap.empty
+
+ let get_opaque_nolib _ i = (!local_opaque_table).(i)
+
+ let get_opaque dp i =
if DirPath.equal dp (Lib.library_dp ())
- then (!local_table).(i)
+ then (!local_opaque_table).(i)
else access_opaque_table dp i
+
+ let join_local_opaque dp i =
+ if DirPath.equal dp (Lib.library_dp ()) then
+ Future.sink (!local_opaque_table).(i)
- let store c =
+ let join_local_univ dp i =
+ if DirPath.equal dp (Lib.library_dp ()) then
+ Future.sink (!local_univ_table).(i)
+
+ let get_univ_nolib _ i = Some (!local_univ_table).(i)
+
+ let get_univ dp i =
+ if DirPath.equal dp (Lib.library_dp ())
+ then Some (!local_univ_table).(i)
+ else try Some (access_univ_table dp i) with Not_found -> None
+
+ let store (d,cu) =
let n = !local_index in
incr local_index;
- if Int.equal n (Array.length !local_table) then begin
+ if Int.equal n (Array.length !local_opaque_table) then begin
let t = Array.make (2*n) a_constr in
- Array.blit !local_table 0 t 0 n;
- local_table := t
+ Array.blit !local_opaque_table 0 t 0 n;
+ local_opaque_table := t;
+ let t = Array.make (2*n) a_univ in
+ Array.blit !local_univ_table 0 t 0 n;
+ local_univ_table := t;
+ let t = Array.make (2*n) a_discharge in
+ Array.blit !local_discharge_table 0 t 0 n;
+ local_discharge_table := t
end;
- (!local_table).(n) <- c;
+ let c, u = Future.split2 ~greedy:true cu in
+ if Future.is_val u then ignore(Future.join u);
+ if Future.is_val c then ignore(Future.join c);
+ (!local_opaque_table).(n) <- c;
+ (!local_univ_table).(n) <- u;
+ (!local_discharge_table).(n) <- d;
+ f2t := FMap.add (Future.uuid cu) n !f2t;
Some (Lib.library_dp (), n)
- let dump () = Array.sub !local_table 0 !local_index
+ let dump () =
+ Array.sub !local_opaque_table 0 !local_index,
+ Array.sub !local_univ_table 0 !local_index,
+ Array.sub !local_discharge_table 0 !local_index,
+ FMap.bindings !f2t
end
-let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get
+let _ = Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque
+let _ = Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ
+let _ = Lazyconstr.set_join_indirect_local_opaque OpaqueTables.join_local_opaque
+let _ = Lazyconstr.set_join_indirect_local_univ OpaqueTables.join_local_univ
(************************************************************************)
(* Internalise libraries *)
+type seg_lib = library_disk
+type seg_univ = Univ.constraints Future.computation array
+type seg_discharge = Lazyconstr.cooking_info list array
+type seg_proofs = Term.constr Future.computation array
+
let mk_library md digest =
{
library_name = md.md_name;
@@ -386,7 +449,10 @@ let mk_library md digest =
let intern_from_file f =
let ch = System.with_magic_number_check raw_intern_library f in
- let lmd, _, digest_lmd = System.marshal_in_segment f ch in
+ let (lmd : seg_lib), pos, digest_lmd = System.marshal_in_segment f ch in
+ let (univs : seg_univ option), _, _ = System.marshal_in_segment f ch in
+ Option.iter (fun univs -> add_univ_table lmd.md_name (Fetched univs)) univs;
+ let _ = System.skip_in_segment f ch in
let pos, digest = System.skip_in_segment f ch in
register_library_filename lmd.md_name f;
add_opaque_table lmd.md_name (ToFetch (f,pos,digest));
@@ -394,18 +460,6 @@ let intern_from_file f =
close_in ch;
library
-let load_library_todo f =
- let paths = Loadpath.get_paths () in
- let _, longf =
- System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
- let f = longf^"i" in
- let ch = System.with_magic_number_check raw_intern_library f in
- let _ = System.skip_in_segment f ch in
- let tasks, _, _ = System.marshal_in_segment f ch in
- match tasks with
- | Some a -> a, longf
- | None -> errorlabstrm "load_library_todo" (str"not a .vi file")
-
let rec intern_library needed (dir, f) =
(* Look if in the current logical environment *)
try find_library dir, needed
@@ -604,10 +658,27 @@ let start_library f =
let id = Id.of_string (Filename.basename f) in
check_coq_overwriting ldir0 id;
let ldir = add_dirpath_suffix ldir0 id in
- Lazyconstr.set_indirect_opaque_creator OpaqueTables.store;
+ Lazyconstr.set_indirect_creator OpaqueTables.store;
Declaremods.start_library ldir;
ldir,longf
+let load_library_todo f =
+ let paths = Loadpath.get_paths () in
+ let _, longf =
+ System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
+ let f = longf^"i" in
+ let ch = System.with_magic_number_check raw_intern_library f in
+ let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in
+ let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in
+ let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in
+ let tasks, _, _ = System.marshal_in_segment f ch in
+ let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in
+ close_in ch;
+ if tasks = None then errorlabstrm "restart" (str"not a .vi file");
+ if s2 = None then errorlabstrm "restart" (str"not a .vi file");
+ if s3 = None then errorlabstrm "restart" (str"not a .vi file");
+ longf, s1, Option.get s2, Option.get s3, Option.get tasks, s5
+
(************************************************************************)
(*s [save_library dir] ends library [dir] and save it to the disk. *)
@@ -635,10 +706,25 @@ let error_recursively_dependent_library dir =
writing the content and computing the checksum... *)
let save_library_to ?todo dir f =
- let f = if todo = None then f ^ "o" else f ^ "i" in
- Lazyconstr.reset_indirect_opaque_creator ();
+ let f, todo, utab, dtab =
+ match todo with
+ | None ->
+ assert(!Flags.compilation_mode = Flags.BuildVo);
+ f ^ "o", (fun _ -> None), (fun _ -> None), (fun _ -> None)
+ | Some d ->
+ assert(!Flags.compilation_mode = Flags.BuildVi);
+ f ^ "i", (fun x -> Some (d x)), (fun x -> Some x), (fun x -> Some x) in
+ Lazyconstr.reset_indirect_creator ();
+ (* HACK: end_library resets Lib and then joins the safe env. To join the
+ * env one needs to access the futures stored in the tables. Standard
+ * accessors use Lib. Hence *)
+ Lazyconstr.set_indirect_opaque_accessor OpaqueTables.get_opaque_nolib;
+ Lazyconstr.set_indirect_univ_accessor OpaqueTables.get_univ_nolib;
let cenv, seg, ast = Declaremods.end_library dir in
- let table = OpaqueTables.dump () in
+ let opaque_table, univ_table, disch_table, f2t_map =
+ OpaqueTables.dump () in
+ assert(!Flags.compilation_mode = Flags.BuildVi ||
+ Array.for_all Future.is_val opaque_table);
let md = {
md_name = dir;
md_compiled = cenv;
@@ -651,9 +737,11 @@ let save_library_to ?todo dir f =
let (f',ch) = raw_extern_library f in
try
(* Writing vo payload *)
- System.marshal_out_segment f' ch md; (* env + objs *)
- System.marshal_out_segment f' ch todo; (* STM tasks *)
- System.marshal_out_segment f' ch table; (* opaques *)
+ System.marshal_out_segment f' ch (md : seg_lib);
+ System.marshal_out_segment f' ch (utab univ_table : seg_univ option);
+ System.marshal_out_segment f' ch (dtab disch_table : seg_discharge option);
+ System.marshal_out_segment f' ch (todo f2t_map : 'tasks option);
+ System.marshal_out_segment f' ch (opaque_table : seg_proofs);
close_out ch;
(* Writing native code files *)
if not !Flags.no_native_compiler then
@@ -662,7 +750,7 @@ let save_library_to ?todo dir f =
let lp = List.map map_path lp in
let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in
if not (Int.equal (Nativelibrary.compile_library dir ast lp fn) 0) then
- msg_error (str "Could not compile the library to native code. Skipping.")
+ msg_error (str"Could not compile the library to native code. Skipping.")
with reraise ->
let reraise = Errors.push reraise in
let () = msg_warning (str ("Removed file "^f')) in
@@ -670,6 +758,15 @@ let save_library_to ?todo dir f =
let () = Sys.remove f' in
raise reraise
+let save_library_raw f lib univs proofs =
+ let (f',ch) = raw_extern_library (f^"o") in
+ System.marshal_out_segment f' ch (lib : seg_lib);
+ System.marshal_out_segment f' ch (Some univs : seg_univ option);
+ System.marshal_out_segment f' ch (None : seg_discharge option);
+ System.marshal_out_segment f' ch (None : 'tasks option);
+ System.marshal_out_segment f' ch (proofs : seg_proofs);
+ close_out ch
+
(************************************************************************)
(*s Display the memory use of a library. *)
diff --git a/library/library.mli b/library/library.mli
index 647138483..ec39059e9 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -29,6 +29,13 @@ val require_library_from_file :
Id.t option -> CUnix.physical_path -> bool option -> unit
(** {6 ... } *)
+
+(** Segments of a library *)
+type seg_lib
+type seg_univ = Univ.constraints Future.computation array
+type seg_discharge = Lazyconstr.cooking_info list array
+type seg_proofs = Term.constr Future.computation array
+
(** Open a module (or a library); if the boolean is true then it's also
an export otherwise just a simple import *)
val import_module : bool -> qualid located -> unit
@@ -37,8 +44,12 @@ val import_module : bool -> qualid located -> unit
val start_library : string -> DirPath.t * string
(** {6 End the compilation of a library and save it to a ".vo" file } *)
-val save_library_to : ?todo:'a -> DirPath.t -> string -> unit
-val load_library_todo : string -> 'a * string
+val save_library_to : ?todo:((Future.UUID.t * int) list -> 'tasks) ->
+ DirPath.t -> string -> unit
+
+val load_library_todo :
+ string -> string * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs
+val save_library_raw : string -> seg_lib -> seg_univ -> seg_proofs -> unit
(** {6 Interrogate the status of libraries } *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c6bb9faa0..6fc1973d0 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -999,7 +999,7 @@ let extract_constant env kn cb =
| OpaqueDef c ->
add_opaque r;
if access_opaque () then
- mk_typ (Lazyconstr.force_opaque (Future.force c))
+ mk_typ (Lazyconstr.force_opaque c)
else mk_typ_ax ())
| (Info,Default) ->
(match cb.const_body with
@@ -1008,7 +1008,7 @@ let extract_constant env kn cb =
| OpaqueDef c ->
add_opaque r;
if access_opaque () then
- mk_def (Lazyconstr.force_opaque (Future.force c))
+ mk_def (Lazyconstr.force_opaque c)
else mk_ax ())
let extract_constant_spec env kn cb =
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index e8b0295cc..da230ee0d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -385,11 +385,11 @@ let print_constant with_values sep sp =
str"*** [ " ++
print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_univ_cstr (Future.force cb.const_constraints)
+ Printer.pr_univ_cstr (Declareops.constraints_of_constant cb)
| _ ->
print_basename sp ++ str sep ++ cut () ++
(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
- Printer.pr_univ_cstr (Future.force cb.const_constraints))
+ Printer.pr_univ_cstr (Declareops.constraints_of_constant cb))
let gallina_print_constant_with_infos sp =
print_constant true " = " sp ++
@@ -531,8 +531,7 @@ let print_full_pure_context () =
| OpaqueDef lc ->
str "Theorem " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
- str "Proof " ++ pr_lconstr
- (Lazyconstr.force_opaque (Future.force lc))
+ str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc)
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype typ ++ cut () ++ str " := " ++
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7d225a470..07c91c8d5 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -136,7 +136,7 @@ let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac
let constr_of_def = function
| Declarations.Undef _ -> assert false
| Declarations.Def cs -> Lazyconstr.force cs
- | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
+ | Declarations.OpaqueDef lc -> Lazyconstr.force_opaque lc
let build_by_tactic env typ tac =
let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 74a94465e..8a133fc48 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -355,6 +355,7 @@ let parse_args arglist =
|"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
|"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
|"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
+ |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo
(* Options with zero arg *)
|"-batch" -> set_batch_mode ()
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index a74f69456..aa64e3f22 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -10,6 +10,7 @@ open Context
open Cooking
open Declarations
open Entries
+open Lazyconstr
val process_inductive :
named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index 9e3d943c0..e73774c97 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -635,9 +635,13 @@ module Slaves : sig
(?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit) -> unit
type tasks
- val dump : unit -> tasks
+ val dump : (Future.UUID.t * int) list -> tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
+ val finish_task :
+ string ->
+ Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+ tasks -> int -> unit
val cancel_worker : int -> unit
@@ -762,11 +766,11 @@ end = struct (* {{{ *)
let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
let set_reach_known_state f = reach_known_state := f
- type request =
+ type 'a request =
ReqBuildProof of
- (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * string
+ (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs * Loc.t * 'a * string
- let name_of_request (ReqBuildProof (_,_,_,_,s)) = s
+ let name_of_request (ReqBuildProof (_,_,_,_,_,s)) = s
type response =
| RespBuiltProof of Entries.proof_output list
@@ -791,19 +795,19 @@ end = struct (* {{{ *)
type task =
| TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
(Entries.proof_output list Future.assignement -> unit) * cancel_switch
- * Loc.t * string
+ * Loc.t * Future.UUID.t * string
let pr_task = function
- | TaskBuildProof(_,bop,eop,_,_,_,s) ->
+ | TaskBuildProof(_,bop,eop,_,_,_,_,s) ->
"TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^
","^s^")"
- let request_of_task task =
+ let request_of_task task : Future.UUID.t request =
match task with
- | TaskBuildProof (exn_info,bop,eop,_,_,loc,s) ->
- ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,s)
+ | TaskBuildProof (exn_info,bop,eop,_,_,loc,uuid,s) ->
+ ReqBuildProof(exn_info,eop,VCS.slice ~start:eop ~stop:bop,loc,uuid,s)
let cancel_switch_of_task = function
- | TaskBuildProof (_,_,_,_,c,_,_) -> c
+ | TaskBuildProof (_,_,_,_,c,_,_,_) -> c
let build_proof_here_core loc eop () =
let wall_clock1 = Unix.gettimeofday () in
@@ -818,25 +822,24 @@ end = struct (* {{{ *)
let slave_respond msg =
match msg with
- | ReqBuildProof(exn_info,eop,vcs,loc,_) ->
+ | ReqBuildProof(exn_info,eop,vcs,loc,_,_) ->
VCS.restore vcs;
VCS.print ();
let r = RespBuiltProof (
let l = Future.force (build_proof_here exn_info loc eop) in
List.iter (fun (_,se) -> Declareops.iter_side_effects (function
| Declarations.SEsubproof(_,
- { Declarations.const_body = Declarations.OpaqueDef f;
- const_constraints = cst} ) ->
- ignore(Future.join f); ignore(Future.join cst)
+ { Declarations.const_body = Declarations.OpaqueDef f } ) ->
+ Lazyconstr.join_lazy_constr f
| _ -> ())
se) l;
l) in
VCS.print ();
r
- let check_task name l i =
+ let check_task_aux name l i =
match List.nth l i with
- | ReqBuildProof ((id,valid),eop,vcs,loc,s) ->
+ | ReqBuildProof ((id,valid),eop,vcs,loc,_,s) as req ->
Pp.msg_info(str(Printf.sprintf "Checking task %d (%s) of %s" i s name));
VCS.restore vcs;
try
@@ -848,7 +851,7 @@ end = struct (* {{{ *)
vernac_interp eop ~proof
{ verbose = false; loc;
expr = (VernacEndProof (Proved (true,None))) };
- true
+ Some (req,proof)
with e -> (try
match Stateid.get e with
| None ->
@@ -872,10 +875,38 @@ end = struct (* {{{ *)
spc () ++ print e)
with e ->
Pp.msg_error (str"unable to print error message: " ++
- str (Printexc.to_string e))); false
+ str (Printexc.to_string e))); None
+
+ let finish_task name u d p l i =
+ match check_task_aux name l i with
+ | None -> exit 1
+ | Some (ReqBuildProof ((id,valid),eop,vcs,loc,bucket,s), (po,pt)) ->
+ let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
+ let con =
+ Nametab.locate_constant
+ (Libnames.qualid_of_ident po.Proof_global.id) in
+ let c = Global.lookup_constant con in
+ match c.Declarations.const_body with
+ | Declarations.OpaqueDef lc ->
+ let pr, uc = Lazyconstr.get_opaque_futures lc in
+ let pr = Future.chain ~greedy:true ~pure:true pr discharge in
+ let pr = Future.chain ~greedy:true ~pure:true pr Constr.hcons in
+ ignore(Future.join pr);
+ ignore(Future.join uc);
+ Pp.msg_info(str(Printf.sprintf
+ "Assigning output of task %d (%s) of %s to bucket %d"
+ i s name bucket));
+ u.(bucket) <- uc;
+ p.(bucket) <- pr
+ | _ -> assert false
+
+ let check_task name l i =
+ match check_task_aux name l i with
+ | Some _ -> true
+ | None -> false
let info_tasks l =
- CList.map_i (fun i (ReqBuildProof(_,_,_,loc,s)) ->
+ CList.map_i (fun i (ReqBuildProof(_,_,_,loc,_,s)) ->
let time1 =
try float_of_string (Aux_file.get !hints loc "proof_build_time")
with Not_found -> 0.0 in
@@ -894,13 +925,13 @@ end = struct (* {{{ *)
let marshal_err s = raise (MarshalError s)
- let marshal_request oc (req : request) =
+ let marshal_request oc (req : Future.UUID.t request) =
try marshal_to_channel oc req
with Failure s | Invalid_argument s | Sys_error s ->
marshal_err ("marshal_request: "^s)
let unmarshal_request ic =
- try (Marshal.from_channel ic : request)
+ try (Marshal.from_channel ic : Future.UUID.t request)
with Failure s | Invalid_argument s | Sys_error s ->
marshal_err ("unmarshal_request: "^s)
@@ -938,16 +969,18 @@ end = struct (* {{{ *)
let force () : Entries.proof_output list Future.assignement =
try `Val (build_proof_here_core loc stop ()) with e -> `Exn e in
let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
+ let uuid = Future.uuid f in
TQueue.push queue
- (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
+ (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
f, cancel_switch
end else
build_proof_here exn_info loc stop, cancel_switch
else
let f, assign = Future.create_delegate (State.exn_on id ~valid) in
+ let uuid = Future.uuid f in
Pp.feedback (Interface.InProgress 1);
TQueue.push queue
- (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,name));
+ (TaskBuildProof(exn_info,start,stop,assign,cancel_switch,loc,uuid,name));
f, cancel_switch
exception RemoteException of std_ppcmds
@@ -991,13 +1024,13 @@ end = struct (* {{{ *)
let rec loop () =
let response = unmarshal_response ic in
match task, response with
- | TaskBuildProof(_,_,_, assign,_,_,_), RespBuiltProof pl ->
+ | TaskBuildProof(_,_,_, assign,_,_,_,_), RespBuiltProof pl ->
assign (`Val pl);
(* We restart the slave, to avoid memory leaks. We could just
Pp.feedback (Interface.InProgress ~-1) *)
last_task := None;
raise KillRespawn
- | TaskBuildProof(_,_,_, assign,_,_,_),RespError(err_id,valid,e,s) ->
+ | TaskBuildProof(_,_,_, assign,_,_,_,_),RespError(err_id,valid,e,s) ->
let e = Stateid.add ~valid (RemoteException e) err_id in
assign (`Exn e);
Option.iter (State.assign valid) s;
@@ -1029,7 +1062,7 @@ end = struct (* {{{ *)
msg_warning(strbrk("Marshalling error: "^s^". "^
"The system state could not be sent to the worker process. "^
"Falling back to local, lazy, evaluation."));
- let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+ let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
assign(`Comp(build_proof_here exn_info loc stop));
Pp.feedback (Interface.InProgress ~-1)
| MarshalError s ->
@@ -1052,7 +1085,7 @@ end = struct (* {{{ *)
| Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled ->
msg_warning(strbrk "The worker was cancelled.");
Option.iter (fun task ->
- let TaskBuildProof (_, start, _, assign, _,_,_) = task in
+ let TaskBuildProof (_, start, _, assign, _,_,_,_) = task in
let s = "Worker cancelled by the user" in
let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in
assign (`Exn e);
@@ -1066,7 +1099,7 @@ end = struct (* {{{ *)
msg_warning(strbrk "The worker process died badly.");
Option.iter (fun task ->
msg_warning(strbrk "Falling back to local, lazy, evaluation.");
- let TaskBuildProof (exn_info, _, stop, assign,_,loc,_) = task in
+ let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in
assign(`Comp(build_proof_here exn_info loc stop));
Pp.feedback (Interface.InProgress ~-1);
) !last_task;
@@ -1158,13 +1191,14 @@ end = struct (* {{{ *)
done
(* For external users this name is nicer than request *)
- type tasks = request list
- let dump () =
+ type tasks = int request list
+ let dump f2t_map =
assert(SlavesPool.is_empty ()); (* ATM, we allow that only if no slaves *)
let tasks = TQueue.dump queue in
prerr_endline (Printf.sprintf "dumping %d\n" (List.length tasks));
let tasks = List.map request_of_task tasks in
- tasks
+ List.map (function ReqBuildProof(a,b,c,d,x,e) ->
+ ReqBuildProof(a,b,c,d,List.assoc x f2t_map,e)) tasks
end (* }}} *)
@@ -1562,7 +1596,7 @@ let join () =
VCS.print ()
type tasks = Slaves.tasks
-let dump () = Slaves.dump ()
+let dump x = Slaves.dump x
let check_task name tasks i =
let vcs = VCS.backup () in
try
@@ -1572,6 +1606,16 @@ let check_task name tasks i =
rc
with e when Errors.noncritical e -> VCS.restore vcs; false
let info_tasks tasks = Slaves.info_tasks tasks
+let finish_tasks name u d p tasks =
+ let finish_task (_,_,i) =
+ let vcs = VCS.backup () in
+ Future.purify (Slaves.finish_task name u d p tasks) i;
+ Pp.pperr_flush ();
+ VCS.restore vcs in
+ try List.iter finish_task (info_tasks tasks)
+ with e ->
+ Pp.pperrnl Pp.(str"File " ++ str name ++ str ":" ++ spc () ++ print e);
+ exit 1
let merge_proof_branch qast keep brname =
let brinfo = VCS.get_branch brname in
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index 0a7473792..c47bacf65 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -44,10 +44,13 @@ val stop_worker : int -> unit
val join : unit -> unit
(* To save to disk an incomplete document *)
type tasks
-val dump : unit -> tasks
+val dump : (Future.UUID.t * int) list -> tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
+val finish_tasks : string ->
+ Library.seg_univ -> Library.seg_discharge -> Library.seg_proofs ->
+ tasks -> unit
(* Id of the tip of the current branch *)
val get_current_state : unit -> Stateid.t
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 6f39725ff..16cc51086 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -18,10 +18,10 @@ Vernacentries
Vernac_classifier
Stm
Whelp
+Vi_checking
Vernac
Ide_slave
Usage
Coqloop
Coqinit
-Vi_checking
Coqtop
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index abf58df45..b35929fef 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -367,6 +367,14 @@ let compile verbosely f =
let _ = load_vernac verbosely long_f_dot_v in
Stm.finish ();
check_pending_proofs ();
- let todo = Stm.dump () in
- Library.save_library_to ~todo ldir long_f_dot_v
+ Library.save_library_to ~todo:Stm.dump ldir long_f_dot_v
+ | Vi2Vo ->
+ let open Filename in
+ let open Library in
+ Dumpglob.noglob ();
+ let f = if check_suffix f ".vi" then chop_extension f else f in
+ let lfdv, lib, univs, disch, tasks, proofs = load_library_todo f in
+ Stm.set_compilation_hints (Aux_file.load_aux_file_for lfdv);
+ Stm.finish_tasks lfdv univs disch proofs tasks;
+ Library.save_library_raw lfdv lib univs proofs
diff --git a/toplevel/vi_checking.ml b/toplevel/vi_checking.ml
index a52a83dfe..5fae1c459 100644
--- a/toplevel/vi_checking.ml
+++ b/toplevel/vi_checking.ml
@@ -10,7 +10,7 @@ open Util
let check_vi (ts,f) =
Dumpglob.noglob ();
- let tasks, long_f_dot_v = Library.load_library_todo f in
+ let long_f_dot_v, _, _, _, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
List.fold_left (fun acc ids -> Stm.check_task f tasks ids && acc) true ts
@@ -38,7 +38,7 @@ let schedule_vi_checking j fs =
let f =
if Filename.check_suffix f ".vi" then Filename.chop_extension f
else f in
- let tasks, long_f_dot_v = Library.load_library_todo f in
+ let long_f_dot_v, _,_,_, tasks, _ = Library.load_library_todo f in
Stm.set_compilation_hints (Aux_file.load_aux_file_for long_f_dot_v);
let infos = Stm.info_tasks tasks in
let eta = List.fold_left (fun a (_,t,_) -> a +. t) 0.0 infos in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 10:09:39 +0000