diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 70 |
1 files changed, 32 insertions, 38 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a5d8a480ee..759cbe22ee 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -458,19 +458,11 @@ let labels_of_mib mib = Array.iter visit_mip mib.mind_packets; get () -let globalize_constant_universes env cb = +let globalize_constant_universes cb = match cb.const_universes with | Monomorphic cstrs -> - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _ | Primitive _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> - match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now (false, c)]) + (* Constraints hidden in the opaque body are added by [add_constant_aux] *) + [Now (false, cstrs)] | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] @@ -480,9 +472,9 @@ let globalize_mind_universes mb = [Now (false, ctx)] | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] -let constraints_of_sfb env sfb = +let constraints_of_sfb sfb = match sfb with - | SFBconst cb -> globalize_constant_universes env cb + | SFBconst cb -> globalize_constant_universes cb | SFBmind mib -> globalize_mind_universes mib | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)] | SFBmodule mb -> [Now (false, mb.mod_constraints)] @@ -520,7 +512,8 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = separately. *) senv else - let cst = constraints_of_sfb senv.env sfb in + (* Delayed constraints from opaque body are added by [add_constant_aux] *) + let cst = constraints_of_sfb sfb in add_constraints_list cst senv in let env' = match sfb, gn with @@ -553,6 +546,17 @@ type exported_private_constant = let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in + let delayed_cst = match cb.const_body with + | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) -> + let fc = Opaqueproof.get_direct_constraints o in + begin match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now (false, c)] + end + | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] + in + (* This is the only place where we hashcons the contents of a constant body *) + let cb = if in_section then cb else Declareops.hcons_const_body cb in let cb, otab = match cb.const_body with | OpaqueDef lc when not in_section -> (* In coqc, opaque constants outside sections will be stored @@ -565,6 +569,7 @@ let add_constant_aux ~in_section senv (kn, cb) = in let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in + let senv' = add_constraints_list delayed_cst senv' in let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver @@ -645,18 +650,10 @@ let inline_side_effects env body side_eff = let body = List.fold_right fold_arg args body in (body, ctx, sigs) -let inline_private_constants_in_definition_entry env ce = - let open Entries in - { ce with - const_entry_body = Future.chain - ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx',_ = inline_side_effects env body side_eff in - let ctx' = Univ.ContextSet.union ctx ctx' in - (body, ctx'), ()); - } - -let inline_private_constants_in_constr env body side_eff = - pi1 (inline_side_effects env body side_eff) +let inline_private_constants env ((body, ctx), side_eff) = + let body, ctx',_ = inline_side_effects env body side_eff in + let ctx' = Univ.ContextSet.union ctx ctx' in + (body, ctx') let is_suffix l suf = match l with | [] -> false @@ -709,13 +706,7 @@ let constant_entry_of_side_effect eff = let export_eff eff = (eff.seff_constant, eff.seff_body, eff.seff_role) -let export_side_effects mb env c = - let open Entries in - let body = c.const_entry_body in - let _, eff = Future.force body in - let ce = { c with - Entries.const_entry_body = Future.chain body - (fun (b_ctx, _) -> b_ctx, ()) } in +let export_side_effects mb env (b_ctx, eff) = let not_exists e = try ignore(Environ.lookup_constant e.seff_constant env); false with Not_found -> true in @@ -739,7 +730,7 @@ let export_side_effects mb env c = in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, ce + | [] -> List.rev acc, b_ctx | eff :: rest -> if Int.equal sl 0 then let env, cb = @@ -758,9 +749,13 @@ let export_side_effects mb env c = in translate_seff trusted seff [] env +let n_univs cb = match cb.const_universes with +| Monomorphic _ -> 0 +| Polymorphic auctx -> Univ.AUContext.size auctx + let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create (Future.from_val p)) cb) in + let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val p)) cb) in let bodies = List.map map exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -768,8 +763,7 @@ let export_private_constants ~in_section ce senv = let add_recipe ~in_section l r senv = let kn = Constant.make2 senv.modpath l in - let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in - let cb = if in_section then cb else Declareops.hcons_const_body cb in + let cb = Term_typing.translate_recipe senv.env kn r in let senv = add_constant_aux ~in_section senv (kn, cb) in kn, senv @@ -788,7 +782,7 @@ let add_constant ?role ~in_section l decl senv = Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let cb = map_constant Opaqueproof.create cb in + let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with |