aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml37
-rw-r--r--kernel/cooking.mli7
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/declareops.ml39
-rw-r--r--kernel/declareops.mli14
-rw-r--r--kernel/entries.mli3
-rw-r--r--kernel/mod_typing.ml18
-rw-r--r--kernel/modops.ml29
-rw-r--r--kernel/modops.mli4
-rw-r--r--kernel/safe_typing.ml91
-rw-r--r--kernel/safe_typing.mli11
-rw-r--r--kernel/term_typing.ml199
-rw-r--r--kernel/term_typing.mli19
13 files changed, 355 insertions, 124 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index bb29b9645..4c2f22199 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -42,11 +42,7 @@ type my_global_reference =
| IndRef of inductive
| ConstructRef of constructor
-let cache = (Hashtbl.create 13 : (my_global_reference, constr) Hashtbl.t)
-
-let clear_cooking_sharing () = Hashtbl.clear cache
-
-let share r (cstl,knl) =
+let share cache r (cstl,knl) =
try Hashtbl.find cache r
with Not_found ->
let f,l =
@@ -59,13 +55,12 @@ let share r (cstl,knl) =
mkConst (pop_con cst), Cmap.find cst cstl in
let c = mkApp (f, Array.map mkVar l) in
Hashtbl.add cache r c;
- (* has raised Not_found if not in work_list *)
c
-let update_case_info ci modlist =
+let update_case_info cache ci modlist =
try
let ind, n =
- match kind_of_term (share (IndRef ci.ci_ind) modlist) with
+ match kind_of_term (share cache (IndRef ci.ci_ind) modlist) with
| App (f,l) -> (destInd f, Array.length l)
| Ind ind -> ind, 0
| _ -> assert false in
@@ -78,7 +73,9 @@ let empty_modlist = (Cmap.empty, Mindmap.empty)
let is_empty_modlist (cm, mm) =
Cmap.is_empty cm && Mindmap.is_empty mm
-let expmod_constr modlist c =
+let expmod_constr cache modlist c =
+ let share = share cache in
+ let update_case_info = update_case_info cache in
let rec substrec c =
match kind_of_term c with
| Case (ci,p,t,br) ->
@@ -122,25 +119,27 @@ type recipe = {
type inline = bool
type result =
- constant_def * constant_type * Univ.constraints * inline
+ constant_def * constant_type * constant_constraints * inline
* Context.section_context option
let on_body f = function
- | Undef inl -> Undef inl
+ | Undef _ as x -> x
| Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
| OpaqueDef lc ->
- OpaqueDef (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))
+ OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc ->
+ (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc)))))
let constr_of_def = function
| Undef _ -> assert false
| Def cs -> Lazyconstr.force cs
- | OpaqueDef lc -> Lazyconstr.force_opaque lc
+ | OpaqueDef lc -> Lazyconstr.force_opaque (Future.force lc)
let cook_constant env r =
+ let cache = Hashtbl.create 13 in
let cb = r.d_from in
- let hyps = Context.map_named_context (expmod_constr r.d_modlist) r.d_abstract 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 r.d_modlist c) hyps)
+ (fun c -> abstract_constant_body (expmod_constr cache r.d_modlist c) hyps)
cb.const_body
in
let const_hyps =
@@ -149,12 +148,16 @@ let cook_constant env r =
hyps ~init:cb.const_hyps in
let typ = match cb.const_type with
| NonPolymorphicType t ->
- let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+ let typ =
+ abstract_constant_type (expmod_constr cache r.d_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 r.d_modlist t) hyps in
+ let typ =
+ abstract_constant_type (expmod_constr cache r.d_modlist t) hyps in
let j = make_judge (constr_of_def body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
(body, typ, cb.const_constraints, cb.const_inline_code, Some const_hyps)
+
+let expmod_constr modlist c = expmod_constr (Hashtbl.create 13) modlist c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 8d046a12e..2d6e53407 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -24,17 +24,12 @@ type recipe = {
type inline = bool
type result =
- constant_def * constant_type * constraints * inline
+ constant_def * constant_type * constant_constraints * inline
* Context.section_context option
val cook_constant : env -> recipe -> result
-
(** {6 Utility functions used in module [Discharge]. } *)
val expmod_constr : work_list -> constr -> constr
-val clear_cooking_sharing : unit -> unit
-
-
-
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 43b908e1f..5cb406ffa 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -38,7 +38,7 @@ type inline = int option
type constant_def =
| Undef of inline
| Def of Lazyconstr.constr_substituted
- | OpaqueDef of Lazyconstr.lazy_constr
+ | OpaqueDef of Lazyconstr.lazy_constr Future.computation
(** Linking information for the native compiler. The boolean flag indicates if
the term is protected by a lazy tag *)
@@ -48,15 +48,19 @@ type native_name =
| LinkedInteractive of string * bool
| NotLinked
+type constant_constraints = Univ.constraints Future.computation
+
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 : Univ.constraints;
+ const_constraints : constant_constraints;
const_native_name : native_name ref;
const_inline_code : bool }
+type side_effect = NewConstant of constant * constant_body
+
(** {6 Representation of mutual inductive types in the kernel } *)
type recarg =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 64496033a..e597ea9a9 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,7 +19,7 @@ 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 lc)
+ | OpaqueDef lc -> Some (Lazyconstr.force_opaque (Future.force lc))
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
@@ -50,7 +50,8 @@ let subst_const_type sub arity =
let subst_const_def sub = function
| Undef inl -> Undef inl
| Def c -> Def (subst_constr_subst sub c)
- | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+ | OpaqueDef lc ->
+ OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
let subst_const_body sub cb = {
const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
@@ -84,14 +85,24 @@ let hcons_const_type = function
let hcons_const_def = function
| Undef inl -> Undef inl
- | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs)))
- | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc)
+ | Def l_constr ->
+ let constr = force l_constr in
+ Def (from_val (Term.hcons_constr constr))
+ | OpaqueDef lc ->
+ if Future.is_val lc then
+ let constr = force_opaque (Future.force lc) in
+ OpaqueDef (Future.from_val (opaque_from_val (Term.hcons_constr constr)))
+ else OpaqueDef lc
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 = Univ.hcons_constraints cb.const_constraints }
+ 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 }
(** Inductive types *)
@@ -193,3 +204,21 @@ let hcons_mind mib =
mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
mind_constraints = Univ.hcons_constraints mib.mind_constraints }
+
+let join_constant_body cb =
+ ignore(Future.join cb.const_constraints);
+ match cb.const_body with
+ | OpaqueDef d -> ignore(Future.join d)
+ | _ -> ()
+
+let string_of_side_effect = function
+ | NewConstant (c,_) -> Names.string_of_con c
+type side_effects = side_effect list
+let no_seff = ([] : side_effects)
+let iter_side_effects f l = List.iter f l
+let fold_side_effects f a l = List.fold_left f a l
+let uniquize_side_effects l = List.uniquize l
+let union_side_effects l1 l2 = l1 @ l2
+let flatten_side_effects l = List.flatten l
+let side_effects_of_list l = l
+let cons_side_effects x l = x :: l
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index c4d67ba52..635b8c47a 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -28,6 +28,19 @@ val body_of_constant : constant_body -> Term.constr option
val is_opaque : constant_body -> bool
+(** Side effects *)
+
+val string_of_side_effect : side_effect -> string
+
+type side_effects
+val no_seff : side_effects
+val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
+val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
+val uniquize_side_effects : side_effects -> side_effects
+val union_side_effects : side_effects -> side_effects -> side_effects
+val flatten_side_effects : side_effects list -> side_effects
+val side_effects_of_list : side_effect list -> side_effects
+val cons_side_effects : side_effect -> side_effects -> side_effects
(** {6 Inductive types} *)
@@ -45,6 +58,7 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
+val join_constant_body : constant_body -> unit
(** {6 Hash-consing} *)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 392a2cd84..3b7a2fd19 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -47,7 +47,8 @@ type mutual_inductive_entry = {
mind_entry_inds : one_inductive_entry list }
(** {6 Constants (Definition/Axiom) } *)
-type const_entry_body = constr
+type proof_output = constr * Declareops.side_effects
+type const_entry_body = proof_output Future.computation
type definition_entry = {
const_entry_body : const_entry_body;
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f7f3c2b77..67db4e806 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -97,16 +97,17 @@ and check_with_def env sign (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 =
- union_constraints
- (union_constraints cb.const_constraints cst1)
+ let cst = union_constraints
+ (union_constraints
+ (Future.force cb.const_constraints) cst1)
cst2
in
let def = Def (Lazyconstr.from_val j.uj_val) in
def,cst
| Def cs ->
let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
- let cst = union_constraints cb.const_constraints cst1 in
+ let cst = union_constraints
+ (Future.force cb.const_constraints) cst1 in
let def = Def (Lazyconstr.from_val c) in
def,cst
in
@@ -115,7 +116,7 @@ and check_with_def env sign (idl,c) mp equiv =
const_body = def;
const_body_code =
Cemitcodes.from_val (compile_constant_body env' def);
- const_constraints = cst }
+ const_constraints = Future.from_val cst }
in
SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
| _ ->
@@ -373,13 +374,14 @@ let rec add_struct_expr_constraints env = function
(add_struct_expr_constraints env meb1)
meb2)
| SEBwith(meb,With_definition_body(_,cb))->
- Environ.add_constraints cb.const_constraints
+ Environ.add_constraints (Future.force cb.const_constraints)
(add_struct_expr_constraints env meb)
| SEBwith(meb,With_module_body(_,_))->
add_struct_expr_constraints env meb
and add_struct_elem_constraints env = function
- | SFBconst cb -> Environ.add_constraints cb.const_constraints env
+ | SFBconst cb ->
+ Environ.add_constraints (Future.force cb.const_constraints) env
| SFBmind mib -> Environ.add_constraints mib.mind_constraints env
| SFBmodule mb -> add_module_constraints env mb
| SFBmodtype mtb -> add_modtype_constraints env mtb
@@ -418,7 +420,7 @@ let rec struct_expr_constraints cst = function
meb2
| SEBwith(meb,With_definition_body(_,cb))->
struct_expr_constraints
- (Univ.union_constraints cb.const_constraints cst) meb
+ (Univ.union_constraints (Future.force cb.const_constraints) cst) meb
| SEBwith(meb,With_module_body(_,_))->
struct_expr_constraints cst meb
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 3b789016b..39e5514c9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -588,3 +588,32 @@ let clean_bounded_mod_expr = function
let str_clean = collect_mbid [] str in
if str_clean == str then str else str_clean
| str -> str
+
+let rec join_module_body mb =
+ Option.iter join_struct_expr_body mb.mod_expr;
+ Option.iter join_struct_expr_body mb.mod_type_alg;
+ join_struct_expr_body mb.mod_type
+and join_structure_body struc =
+ let join_body (l,body) = match body with
+ | SFBconst sb -> join_constant_body sb
+ | SFBmind _ -> ()
+ | SFBmodule m -> join_module_body m
+ | SFBmodtype m ->
+ join_struct_expr_body m.typ_expr;
+ Option.iter join_struct_expr_body m.typ_expr_alg in
+ List.iter join_body struc;
+and join_struct_expr_body = function
+ | SEBfunctor (_,t,e) ->
+ join_struct_expr_body t.typ_expr;
+ Option.iter join_struct_expr_body t.typ_expr_alg;
+ join_struct_expr_body e
+ | SEBident mp -> ()
+ | SEBstruct s -> join_structure_body s
+ | SEBapply (mexpr,marg,u) ->
+ join_struct_expr_body mexpr;
+ join_struct_expr_body marg
+ | SEBwith (seb,wdcl) ->
+ join_struct_expr_body seb;
+ match wdcl with
+ | With_module_body _ -> ()
+ | With_definition_body (_, sb) -> join_constant_body sb
diff --git a/kernel/modops.mli b/kernel/modops.mli
index c4d8ab349..30f9274d2 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -50,6 +50,10 @@ val subst_modtype_and_resolver : module_type_body -> module_path ->
val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
+val join_module_body : module_body -> unit
+val join_structure_body : structure_body -> unit
+val join_struct_expr_body : struct_expr_body -> unit
+
(** Errors *)
type signature_mismatch_error =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 753b97a0c..13368aab9 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -99,6 +99,7 @@ type safe_environment =
objlabels : Label.Set.t;
revstruct : structure_body;
univ : Univ.constraints;
+ future_cst : Univ.constraints Future.computation list;
engagement : engagement option;
imports : library_info list;
loads : (module_path * module_body) list;
@@ -107,6 +108,36 @@ type safe_environment =
let exists_modlabel l senv = Label.Set.mem l senv.modlabels
let exists_objlabel l senv = Label.Set.mem l senv.objlabels
+(* type to be maintained isomorphic to Entries.side_effects *)
+(* XXX ideally this function obtains a valid side effect that
+ * can be pushed into another (safe) environment without re-typechecking *)
+type side_effect = NewConstant of constant * constant_body
+let sideff_of_con env c =
+ Obj.magic (NewConstant (c, Environ.lookup_constant c env.env))
+
+let env_of_safe_env senv = senv.env
+let env_of_senv = env_of_safe_env
+
+type constraints_addition =
+ Now of Univ.constraints | Later of Univ.constraints Future.computation
+
+let add_constraints cst senv =
+ match cst with
+ | Later fc -> {senv with future_cst = fc :: senv.future_cst}
+ | Now cst ->
+ { senv with
+ env = Environ.add_constraints cst senv.env;
+ univ = Univ.union_constraints cst senv.univ }
+
+let is_curmod_library senv =
+ match senv.modinfo.variant with LIBRARY _ -> true | _ -> false
+
+let rec join_safe_environment e =
+ join_structure_body e.revstruct;
+ List.fold_left
+ (fun e fc -> add_constraints (Now (Future.join fc)) e)
+ {e with future_cst = []} e.future_cst
+
let check_modlabel l senv =
if exists_modlabel l senv then error_existing_label l
let check_objlabel l senv =
@@ -141,25 +172,21 @@ let rec empty_environment =
modlabels = Label.Set.empty;
objlabels = Label.Set.empty;
revstruct = [];
+ future_cst = [];
univ = Univ.empty_constraint;
engagement = None;
imports = [];
loads = [];
local_retroknowledge = [] }
-let env_of_safe_env senv = senv.env
-let env_of_senv = env_of_safe_env
-
-let add_constraints cst senv =
- { senv with
- env = Environ.add_constraints cst senv.env;
- univ = Univ.union_constraints cst senv.univ }
-
let constraints_of_sfb = function
- | SFBconst cb -> cb.const_constraints
- | SFBmind mib -> mib.mind_constraints
- | SFBmodtype mtb -> mtb.typ_constraints
- | SFBmodule mb -> mb.mod_constraints
+ | 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
(* A generic function for adding a new field in a same environment.
It also performs the corresponding [add_constraints]. *)
@@ -246,14 +273,20 @@ let safe_push_named (id,_,_ as d) env =
Environ.push_named d env
let push_named_def (id,de) senv =
- let (c,typ,cst) = Term_typing.translate_local_def senv.env de in
- let senv' = add_constraints cst senv in
+ let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
+ (* XXX for now we force *)
+ let c = match c with
+ | Def c -> Lazyconstr.force c
+ | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
+ | _ -> assert false in
+ let cst = Future.join cst 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''})
let push_named_assum (id,t) senv =
let (t,cst) = Term_typing.translate_local_assum senv.env t in
- let senv' = add_constraints cst senv in
+ let senv' = add_constraints (Now cst) senv in
let env'' = safe_push_named (id,None,t) senv'.env in
(cst, {senv' with env=env''})
@@ -267,16 +300,17 @@ type global_declaration =
let add_constant dir l decl senv =
let kn = make_con senv.modinfo.modpath dir l in
let cb = match decl with
- | ConstantEntry ce -> Term_typing.translate_constant senv.env ce
+ | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
| GlobalRecipe r ->
- let cb = Term_typing.translate_recipe senv.env r in
+ let cb = Term_typing.translate_recipe senv.env kn r in
if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
in
let cb = match cb.const_body with
| 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 (Lazyconstr.turn_indirect lc) }
+ { cb with const_body =
+ OpaqueDef (Future.chain lc Lazyconstr.turn_indirect) }
| _ -> cb
in
let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -317,7 +351,7 @@ let add_modtype l mte inl senv =
(* full_add_module adds module with universes and constraints *)
let full_add_module mb senv =
- let senv = add_constraints mb.mod_constraints senv in
+ let senv = add_constraints (Now mb.mod_constraints) senv in
{ senv with env = Modops.add_module mb senv.env }
(* Insertion of modules *)
@@ -350,6 +384,7 @@ let start_module l senv =
objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
+ future_cst = [];
engagement = None;
imports = senv.imports;
loads = [];
@@ -435,6 +470,7 @@ let end_module l restype senv =
objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
univ = Univ.union_constraints senv'.univ oldsenv.univ;
+ future_cst = senv'.future_cst @ oldsenv.future_cst;
(* engagement is propagated to the upper level *)
engagement = senv'.engagement;
imports = senv'.imports;
@@ -457,14 +493,14 @@ let end_module l restype senv =
senv.modinfo.modpath inl me in
mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
in
- let senv = add_constraints cst senv in
+ let senv = add_constraints (Now cst) senv in
let mp_sup = senv.modinfo.modpath in
(* Include Self support *)
let rec compute_sign sign mb resolver senv =
match sign with
| SEBfunctor(mbid,mtb,str) ->
let cst_sub = check_subtypes senv.env mb mtb in
- let senv = add_constraints cst_sub senv in
+ let senv = add_constraints (Now cst_sub) senv in
let mpsup_delta =
inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
in
@@ -533,6 +569,7 @@ let add_module_parameter mbid mte inl senv =
objlabels = senv.objlabels;
revstruct = [];
univ = senv.univ;
+ future_cst = senv.future_cst;
engagement = senv.engagement;
imports = senv.imports;
loads = [];
@@ -557,6 +594,7 @@ let start_modtype l senv =
objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
+ future_cst = [];
engagement = None;
imports = senv.imports;
loads = [] ;
@@ -609,6 +647,7 @@ let end_modtype l senv =
objlabels = oldsenv.objlabels;
revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
univ = Univ.union_constraints senv.univ oldsenv.univ;
+ future_cst = senv.future_cst @ oldsenv.future_cst;
engagement = senv.engagement;
imports = senv.imports;
loads = senv.loads@oldsenv.loads;
@@ -644,6 +683,8 @@ type compiled_library = {
type native_library = Nativecode.global list
+let join_compiled_library l = join_module_body l.comp_mod
+
(* We check that only initial state Require's were performed before
[start_library] was called *)
@@ -674,12 +715,16 @@ let start_library dir senv =
objlabels = Label.Set.empty;
revstruct = [];
univ = Univ.empty_constraint;
+ future_cst = [];
engagement = None;
imports = senv.imports;
loads = [];
local_retroknowledge = [] }
let export senv dir =
+ let senv =
+ try join_safe_environment senv
+ with e -> Errors.errorlabstrm "future" (Errors.print e) in
let modinfo = senv.modinfo in
begin
match modinfo.variant with
@@ -763,7 +808,6 @@ let import lib digest senv =
in
mp, senv, lib.comp_natsymbs
-
type judgment = unsafe_judgment
let j_val j = j.uj_val
@@ -787,3 +831,6 @@ let register_inline kn senv =
let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in
let env = { env with Pre_env.env_globals = new_globals } in
{ senv with env = env_of_pre_env env }
+
+let add_constraints c = add_constraints (Now c)
+
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7ca033383..210d601fb 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -26,6 +26,15 @@ type safe_environment
val env_of_safe_env : safe_environment -> Environ.env
+val sideff_of_con : safe_environment -> constant -> side_effect
+
+val is_curmod_library : safe_environment -> bool
+
+
+(* safe_environment has functional data affected by lazy computations,
+ * thus this function returns a new safe_environment *)
+val join_safe_environment : safe_environment -> safe_environment
+
val empty_environment : safe_environment
val is_empty : safe_environment -> bool
@@ -109,6 +118,8 @@ val export : safe_environment -> DirPath.t
val import : compiled_library -> Digest.t -> safe_environment
-> module_path * safe_environment * Nativecode.symbol array
+val join_compiled_library : compiled_library -> unit
+
(** {6 Typing judgments } *)
type judgment
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 33a4b55e8..fd31d782a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,6 +23,10 @@ open Environ
open Entries
open Typeops
+let debug = false
+let prerr_endline =
+ if debug then prerr_endline else fun _ -> ()
+
let constrain_type env j cst1 = function
| None ->
make_polymorphic_if_constant_for_ind env j, cst1
@@ -33,19 +37,6 @@ let constrain_type env j cst1 = function
let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
NonPolymorphicType t, cstrs
-let local_constrain_type env j cst1 = function
- | None ->
- j.uj_type, cst1
- | 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);
- t, union_constraints (union_constraints cst1 cst2) cst3
-
-let translate_local_def env de =
- let (j,cst) = infer env de.const_entry_body in
- let (typ,cst) = local_constrain_type env j cst de.const_entry_type in
- (j.uj_val,typ,cst)
let translate_local_assum env t =
let (j,cst) = infer env t in
@@ -55,23 +46,89 @@ let translate_local_assum env t =
(* Insertion of constants and parameters in environment. *)
-let infer_declaration env = function
+let handle_side_effects env body side_eff =
+ let handle_sideff t (NewConstant (c,cb)) =
+ let cname =
+ let name = string_of_con c in
+ for i = 0 to String.length name - 1 do
+ if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
+ Name (id_of_string name) in
+ let rec sub i x = match kind_of_term x with
+ | Const c' when eq_constant c c' -> mkRel i
+ | _ -> map_constr_with_binders ((+) 1) sub i x in
+ match cb.const_body with
+ | Undef _ -> assert false
+ | Def b ->
+ let b = Lazyconstr.force b in
+ let b_ty = Typeops.type_of_constant_type env cb.const_type in
+ let t = sub 1 (Vars.lift 1 t) in
+ mkLetIn (cname, b, b_ty, t)
+ | OpaqueDef b ->
+ let b = Lazyconstr.force_opaque (Future.force b) in
+ let b_ty = Typeops.type_of_constant_type env cb.const_type in
+ let t = sub 1 (Vars.lift 1 t) in
+ mkApp (mkLambda (cname, b_ty, t), [|b|])
+ in
+ (* CAVEAT: we assure a proper order *)
+ Declareops.fold_side_effects handle_sideff body
+ (Declareops.uniquize_side_effects side_eff)
+
+(* what is used for debugging only *)
+let infer_declaration ?(what="UNKNOWN") env dcl =
+ match dcl with
| DefinitionEntry c ->
- let (j,cst) = infer env c.const_entry_body in
- let j =
- {uj_val = hcons_constr j.uj_val;
- uj_type = hcons_constr j.uj_type} in
- let (typ,cst) = constrain_type env j cst c.const_entry_type in
- let def =
- if c.const_entry_opaque
- then OpaqueDef (Lazyconstr.opaque_from_val j.uj_val)
- else Def (Lazyconstr.from_val j.uj_val)
- in
- def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+ let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
+ if c.const_entry_opaque && c.const_entry_type <> None then
+ let _ = prerr_endline ("deferring typing of "^what) in
+ let body_cst = Future.chain ~id:("infer_declaration " ^ what)
+ entry_body (fun entry_body ->
+ let _ = prerr_endline ("forcing deferred typing of "^what) in
+ let body, side_eff = entry_body in
+ let _ = prerr_endline ("... got proof of "^what) in
+ let body = if side_eff = Declareops.no_seff then body else
+ let _ = prerr_endline (" Handling the following side eff:") in
+ Declareops.iter_side_effects (fun e ->
+ prerr_endline(" " ^ Declareops.string_of_side_effect e))
+ side_eff;
+ handle_side_effects env body side_eff in
+ let (j,cst) = infer env body in
+ let _ = prerr_endline ("... typed proof of "^what) in
+ let j =
+ {uj_val = hcons_constr j.uj_val;
+ uj_type = hcons_constr j.uj_type} in
+ let (_typ,cst) = constrain_type env j cst c.const_entry_type in
+ Lazyconstr.opaque_from_val j.uj_val, cst) in
+ let body, cst = Future.split2 body_cst in
+ let def = OpaqueDef body in
+ let typ = match c.const_entry_type with
+ | None -> assert false
+ | Some typ -> NonPolymorphicType typ in
+ (def, typ, cst, c.const_entry_inline_code, ctx)
+ else
+ let _ = prerr_endline ("typing now "^what) in
+ let body, side_eff = Future.force entry_body in
+ let body = if side_eff = Declareops.no_seff then body else
+ let _ = prerr_endline (" Handling the following side eff:") in
+ Declareops.iter_side_effects (fun e ->
+ prerr_endline(" " ^ Declareops.string_of_side_effect e))
+ side_eff;
+ handle_side_effects env body side_eff in
+ let (j,cst) =
+ try infer env body
+ with Not_found as e ->
+ prerr_endline ("infer not found " ^ what);
+ raise e in
+ let j =
+ {uj_val = hcons_constr j.uj_val;
+ uj_type = hcons_constr j.uj_type} in
+ let (typ,cst) = constrain_type env j cst c.const_entry_type in
+ let _ = prerr_endline ("...typed "^what) in
+ let def = Def (Lazyconstr.from_val j.uj_val) in
+ (def, typ, Future.from_val cst, c.const_entry_inline_code, ctx)
| 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, cst, false, ctx
+ Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
let global_vars_set_constant_type env = function
| NonPolymorphicType t -> global_vars_set env t
@@ -81,48 +138,78 @@ 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 check_declared_variables declared inferred =
- let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
- let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in
- if not (Id.Set.is_empty undeclared_set) then
- error ("The following section variables are used but not declared:\n"^
- (String.concat ", "
- (List.map Id.to_string (Id.Set.elements undeclared_set))))
-
-let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
- let hyps =
- let inferred =
- let ids_typ = global_vars_set_constant_type env typ in
- let ids_def = match def with
- | Undef _ -> Id.Set.empty
- | Def cs -> global_vars_set env (Lazyconstr.force cs)
- | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc)
- in
- keep_hyps env (Id.Set.union ids_typ ids_def)
- in
+let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
+ let check declared inferred =
+ let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+ let inferred_set, declared_set = mk_set inferred, mk_set declared in
+ if not (Id.Set.subset inferred_set declared_set) then
+ error ("The following section variable are used but not declared:\n"^
+ (String.concat ", " (List.map Id.to_string
+ (Id.Set.elements (Idset.diff inferred_set declared_set))))) in
+ (* We try to postpone the computation of used section variables *)
+ let hyps, def =
match ctx with
- | None -> inferred
- | Some declared ->
- check_declared_variables declared inferred;
- declared
- in
- let tps = Cemitcodes.from_val (compile_constant_body env def) in
+ | None when named_context env <> [] ->
+ (* No declared section vars, and non-empty section context:
+ we must look at the body NOW, if any *)
+ let ids_typ = global_vars_set_constant_type env typ in
+ 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);
+ global_vars_set env (Lazyconstr.force_opaque (Future.force lc)) in
+ keep_hyps env (Idset.union ids_typ ids_def), def
+ | None -> [], def (* Empty section context: no need to check *)
+ | Some declared ->
+ (* We use the declared set and chain a check of correctness *)
+ declared,
+ match def with
+ | Undef _ as x -> x (* nothing to check *)
+ | Def cs as x ->
+ let ids_typ = global_vars_set_constant_type env typ in
+ let ids_def = global_vars_set env (Lazyconstr.force cs) in
+ let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+ check declared inferred;
+ x
+ | OpaqueDef lc -> (* In this case we can postpone the check *)
+ OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc ->
+ let ids_typ = global_vars_set_constant_type env typ in
+ let ids_def =
+ global_vars_set env (Lazyconstr.force_opaque lc) in
+ let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+ check declared inferred; lc)) in
{ const_hyps = hyps;
const_body = def;
const_type = typ;
- const_body_code = tps;
+ const_body_code = Cemitcodes.from_val (compile_constant_body env def);
const_constraints = cst;
const_native_name = ref NotLinked;
const_inline_code = inline_code }
(*s Global and local constant declaration. *)
-let translate_constant env ce =
- build_constant_declaration env (infer_declaration env ce)
+let translate_constant env kn ce =
+ build_constant_declaration kn env
+ (infer_declaration ~what:(string_of_con kn) env ce)
+
+let translate_recipe env kn r =
+ let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
+ build_constant_declaration kn env (def,typ,cst,inline_code,hyps)
-let translate_recipe env r =
- build_constant_declaration env (Cooking.cook_constant env 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
+ let typ = type_of_constant_type env typ in
+ def, typ, cst
(* Insertion of inductive types. *)
let translate_mind env kn mie = Indtypes.check_inductive env kn mie
+
+let handle_side_effects env ce = { ce with
+ const_entry_body = Future.chain ~id:"handle_side_effects"
+ ce.const_entry_body (fun (body, side_eff) ->
+ handle_side_effects env body side_eff, Declareops.no_seff);
+}
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c9bff84fc..59706bb83 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -13,20 +13,25 @@ open Environ
open Declarations
open Entries
-val translate_local_def : env -> definition_entry ->
- constr * types * constraints
+val translate_local_def : env -> Id.t -> definition_entry ->
+ constant_def * types * constant_constraints
val translate_local_assum : env -> types -> types * constraints
-val translate_constant : env -> constant_entry -> constant_body
+(* returns the same definition_entry but with side effects turned into
+ * let-ins or beta redexes. it is meant to get a term out of a not yet
+ * type checked proof *)
+val handle_side_effects : env -> definition_entry -> definition_entry
+
+val translate_constant : env -> constant -> constant_entry -> constant_body
val translate_mind :
env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
-val translate_recipe : env -> Cooking.recipe -> constant_body
-
+val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : env -> constant_entry -> Cooking.result
-val build_constant_declaration : env -> Cooking.result -> constant_body
+val infer_declaration : ?what:string -> env -> constant_entry -> Cooking.result
+val build_constant_declaration :
+ constant -> env -> Cooking.result -> constant_body
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 23:58:34 +0000