diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/declareops.ml | 16 | ||||
| -rw-r--r-- | kernel/declareops.mli | 1 | ||||
| -rw-r--r-- | kernel/modops.ml | 28 | ||||
| -rw-r--r-- | kernel/modops.mli | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 22 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 9 |
8 files changed, 9 insertions, 75 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4c2f221990..dbe83a8565 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,7 +126,7 @@ let on_body f = function | Undef _ as x -> x | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) | OpaqueDef lc -> - OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc -> + OpaqueDef (Future.chain lc (fun lc -> (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc))))) let constr_of_def = function diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 973859ede6..3083c17389 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -52,8 +52,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 (Future.chain lc (subst_lazy_constr sub)) (* TODO : the native compiler seems to rely on a fresh (ref NotLinked) being created at each substitution. Quite ugly... For the moment, @@ -100,7 +99,7 @@ let hcons_const_def = function Def (from_val (Term.hcons_constr constr)) | OpaqueDef lc -> OpaqueDef - (Future.chain ~pure:true lc + (Future.chain lc (fun lc -> opaque_from_val (Term.hcons_constr (force_opaque lc)))) let hcons_const_body cb = @@ -242,17 +241,6 @@ let join_constant_body cb = | OpaqueDef d -> ignore(Future.join d) | _ -> () -let prune_constant_body cb = - let cst, cbo = cb.const_constraints, cb.const_body in - let cst' = Future.drop cst in - let cbo' = match cbo with - | OpaqueDef d -> - let d' = Future.drop d in - if d' == d then cbo else OpaqueDef d' - | _ -> cbo in - if cst' == cst && cbo' == cbo then cb - else {cb with const_constraints = cst'; const_body = cbo'} - let string_of_side_effect = function | SEsubproof (c,_) -> Names.string_of_con c | SEscheme (cl,_) -> diff --git a/kernel/declareops.mli b/kernel/declareops.mli index f593b45472..177ae9d45e 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -59,7 +59,6 @@ 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 -val prune_constant_body : constant_body -> constant_body (** {6 Hash-consing} *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 76feb8498d..6a0a952f7d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -592,7 +592,7 @@ let rec collect_mbid l sign = match sign with let clean_bounded_mod_expr sign = if is_functor sign then collect_mbid MBIset.empty sign else sign -(** {6 Stm machinery : join and prune } *) +(** {6 Stm machinery } *) let rec join_module mb = implem_iter join_signature join_expression mb.mod_expr; @@ -610,29 +610,3 @@ and join_structure struc = List.iter join_field struc and join_signature sign = functor_iter join_modtype join_structure sign and join_expression me = functor_iter join_modtype (fun _ -> ()) me -let rec prune_module mb = - let me, mta, mt = mb.mod_expr, mb.mod_type_alg, mb.mod_type in - let mt' = prune_signature mt in - let me' = implem_smartmap prune_signature prune_expression me in - let mta' = Option.smartmap prune_expression mta in - if me' == me && mta' == mta && mt' == mt then mb - else {mb with mod_expr = me'; mod_type_alg = mta'; mod_type = mt'} -and prune_modtype mt = - let te, ta = mt.typ_expr, mt.typ_expr_alg in - let te' = prune_signature te in - let ta' = Option.smartmap prune_expression ta in - if te==te' && ta==ta' then mt else { mt with typ_expr=te'; typ_expr_alg=ta' } -and prune_field (l,body as orig) = match body with - |SFBconst sb -> - let sb' = prune_constant_body sb in - if sb == sb' then orig else (l, SFBconst sb') - |SFBmind _ -> orig - |SFBmodule m -> - let m' = prune_module m in - if m == m' then orig else (l, SFBmodule m') - |SFBmodtype m -> - let m' = prune_modtype m in - if m == m' then orig else (l, SFBmodtype m') -and prune_structure struc = List.smartmap prune_field struc -and prune_signature sign = functor_smartmap prune_modtype prune_structure sign -and prune_expression me = functor_smartmap prune_modtype (fun me -> me) me diff --git a/kernel/modops.mli b/kernel/modops.mli index 6aed95988c..11eb876ad0 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -76,13 +76,11 @@ val subst_modtype_and_resolver : module_type_body -> module_path -> val clean_bounded_mod_expr : module_signature -> module_signature -(** {6 Stm machinery : join and prune } *) +(** {6 Stm machinery } *) val join_module : module_body -> unit val join_structure : structure_body -> unit -val prune_structure : structure_body -> structure_body - (** {6 Errors } *) type signature_mismatch_error = diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 57e44a3226..90d52572a7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -197,28 +197,6 @@ let join_safe_environment e = (fun e fc -> add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst -(* TODO : out of place and maybe incomplete w.r.t. modules *) -(* this is there to explore the opaque pre-env structure but is - * not part of the trusted code base *) -let prune_env env = - let open Pre_env in - let prune_ckey (cb,k) = Declareops.prune_constant_body cb, k in - let prune_globals glob = - { glob with env_constants = Cmap_env.map prune_ckey glob.env_constants } - in - let env = Environ.pre_env env in - Environ.env_of_pre_env {env with - env_globals = prune_globals env.env_globals; - env_named_vals = []; - env_rel_val = []} -let prune_safe_environment e = - { e with - modvariant = (match e.modvariant with LIBRARY -> LIBRARY | _ -> NONE); - revstruct = Modops.prune_structure e.revstruct; - future_cst = []; - env = prune_env e.env } - - (** {6 Various checks } *) let exists_modlabel l senv = Label.Set.mem l senv.modlabels diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index a56bb8578e..b16d5b63d4 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -43,8 +43,6 @@ 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 -(* future computations are just dropped by this function *) -val prune_safe_environment : safe_environment -> safe_environment (** {6 Enriching a safe environment } *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 567511c93f..987621619a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -84,9 +84,8 @@ let infer_declaration ?(what="UNKNOWN") env dcl = | DefinitionEntry c -> let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in if c.const_entry_opaque && not (Option.is_empty c.const_entry_type) then - let id = "infer_declaration " ^ what in let body_cst = - Future.chain ~id entry_body (fun (body, side_eff) -> + Future.chain entry_body (fun (body, side_eff) -> let body = handle_side_effects env body side_eff in let j, cst = infer env body in let j = @@ -163,7 +162,7 @@ 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 ~id:(string_of_con kn) lc (fun lc -> + OpaqueDef (Future.chain 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 @@ -198,7 +197,7 @@ let translate_local_def env id centry = 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" + const_entry_body = Future.chain ce.const_entry_body (fun (body, side_eff) -> - handle_side_effects env body side_eff, Declareops.no_seff); + handle_side_effects env body side_eff, Declareops.no_seff); } |