diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 565 |
1 files changed, 345 insertions, 220 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 673f025c75..4268f0a602 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -113,10 +113,16 @@ type library_info = DirPath.t * vodigest (** Functor and funsig parameters, most recent first *) type module_parameters = (MBId.t * module_type_body) list -module DPMap = Map.Make(DirPath) +(** Part of the safe_env at a section opening time to be backtracked *) +type section_data = { + rev_env : Environ.env; + rev_univ : Univ.ContextSet.t; + rev_objlabels : Label.Set.t; +} type safe_environment = { env : Environ.env; + sections : section_data Section.t; modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; @@ -127,10 +133,10 @@ type safe_environment = univ : Univ.ContextSet.t; future_cst : Univ.ContextSet.t Future.computation list; engagement : engagement option; - required : vodigest DPMap.t; + required : vodigest DPmap.t; loads : (ModPath.t * module_body) list; local_retroknowledge : Retroknowledge.action list; - native_symbols : Nativecode.symbols DPMap.t } +} and modvariant = | NONE @@ -153,13 +159,14 @@ let empty_environment = revstruct = []; modlabels = Label.Set.empty; objlabels = Label.Set.empty; + sections = Section.empty; future_cst = []; univ = Univ.ContextSet.empty; engagement = None; - required = DPMap.empty; + required = DPmap.empty; loads = []; local_retroknowledge = []; - native_symbols = DPMap.empty } +} let is_initial senv = match senv.revstruct, senv.modvariant with @@ -196,6 +203,18 @@ let set_typing_flags c senv = if env == senv.env then senv else { senv with env } +let set_check_guarded b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_guarded = b } senv + +let set_check_positive b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_positive = b } senv + +let set_check_universes b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with check_universes = b } senv + let set_indices_matter indices_matter senv = set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv @@ -228,19 +247,10 @@ let check_engagement env expected_impredicative_set = (** {6 Stm machinery } *) -let get_opaque_body env cbo = - match cbo.const_body with - | Undef _ -> assert false - | Primitive _ -> assert false - | Def _ -> `Nothing - | OpaqueDef opaque -> - `Opaque - (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, - Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) - type side_effect = { from_env : Declarations.structure_body CEphemeron.key; - eff : Entries.side_eff list; + seff_constant : Constant.t; + seff_body : Constr.t Declarations.constant_body; } module SideEffects : @@ -254,11 +264,9 @@ end = struct module SeffOrd = struct -open Entries type t = side_effect let compare e1 e2 = - let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in - List.compare cmp e1.eff e2.eff + Constant.CanOrd.compare e1.seff_constant e2.seff_constant end module SeffSet = Set.Make(SeffOrd) @@ -279,42 +287,36 @@ end type private_constants = SideEffects.t let side_effects_of_private_constants l = - let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff; _ } -> eff) ans + List.rev (SideEffects.repr l) -let empty_private_constants = SideEffects.empty -let add_private mb eff effs = - let from_env = CEphemeron.create mb in - SideEffects.add { eff; from_env } effs -let concat_private = SideEffects.concat +(* Only used to push in an Environ.env. *) +let lift_constant c = + let body = match c.const_body with + | OpaqueDef _ -> Undef None + | Def _ | Undef _ | Primitive _ as body -> body + in + { c with const_body = body } -let make_eff env cst r = - let open Entries in - let cbo = Environ.lookup_constant cst env.env in - { - seff_constant = cst; - seff_body = cbo; - seff_env = get_opaque_body env.env cbo; - seff_role = r; - } +let map_constant f c = + let body = match c.const_body with + | OpaqueDef o -> OpaqueDef (f o) + | Def _ | Undef _ | Primitive _ as body -> body + in + { c with const_body = body } -let private_con_of_con env c = - let open Entries in - let eff = [make_eff env c Subproof] in - add_private env.revstruct eff empty_private_constants +let push_private_constants env eff = + let eff = side_effects_of_private_constants eff in + let add_if_undefined env eff = + try ignore(Environ.lookup_constant eff.seff_constant env); env + with Not_found -> Environ.add_constant eff.seff_constant (lift_constant eff.seff_body) env + in + List.fold_left add_if_undefined env eff -let private_con_of_scheme ~kind env cl = - let open Entries in - let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in - add_private env.revstruct eff empty_private_constants +let empty_private_constants = SideEffects.empty +let concat_private = SideEffects.concat let universes_of_private eff = - let open Entries in let fold acc eff = - let acc = match eff.seff_env with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc - in match eff.seff_body.const_universes with | Monomorphic ctx -> ctx :: acc | Polymorphic _ -> acc @@ -324,24 +326,34 @@ let universes_of_private eff = let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env +let sections_of_safe_env senv = senv.sections + type constraints_addition = - | Now of bool * Univ.ContextSet.t + | Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation +let push_context_set poly cst senv = + if Univ.ContextSet.is_empty cst then senv + else + let sections = + if Section.is_empty senv.sections then senv.sections + else Section.push_constraints cst senv.sections + in + { senv with + env = Environ.push_context_set ~strict:(not poly) cst senv.env; + univ = Univ.ContextSet.union cst senv.univ; + sections } + let add_constraints cst senv = match cst with | Later fc -> {senv with future_cst = fc :: senv.future_cst} - | Now (poly,cst) -> - { senv with - env = Environ.push_context_set ~strict:(not poly) cst senv.env; - univ = Univ.ContextSet.union cst senv.univ } + | Now cst -> + push_context_set false cst senv let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst -let push_context_set poly ctx = add_constraints (Now (poly,ctx)) - let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false @@ -350,7 +362,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e = List.fold_left (fun e fc -> if Future.UUIDSet.mem (Future.uuid fc) except then e - else add_constraints (Now (false, Future.join fc)) e) + else add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst let is_joined_environment e = List.is_empty e.future_cst @@ -392,7 +404,7 @@ let check_current_library dir senv = match senv.modvariant with (** When operating on modules, we're normally outside sections *) let check_empty_context senv = - assert (Environ.empty_context senv.env) + assert (Environ.empty_context senv.env && Section.is_empty senv.sections) (** When adding a parameter to the current module/modtype, it must have been freshly started *) @@ -412,7 +424,7 @@ let check_initial senv = assert (is_initial senv) let check_required current_libs needed = let check (id,required) = try - let actual = DPMap.find id current_libs in + let actual = DPmap.find id current_libs in if not(digest_match ~actual ~required) then CErrors.user_err Pp.(pr_sequence str ["Inconsistent assumptions over module"; DirPath.to_string id; "."]) @@ -439,20 +451,30 @@ let safe_push_named d env = with Not_found -> () in Environ.push_named d env - let push_named_def (id,de) senv = + let sections = Section.push_local senv.sections in let c, r, typ = Term_typing.translate_local_def senv.env id de in let x = Context.make_annot id r in let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in - { senv with env = env'' } - -let push_named_assum ((id,t,poly),ctx) senv = - let senv' = push_context_set poly ctx senv in - let t, r = Term_typing.translate_local_assum senv'.env t in - let x = Context.make_annot id r in - let env'' = safe_push_named (LocalAssum (x,t)) senv'.env in - {senv' with env=env''} - + { senv with sections; env = env'' } + +let push_named_assum (x,t) senv = + let sections = Section.push_local senv.sections in + let t, r = Term_typing.translate_local_assum senv.env t in + let x = Context.make_annot x r in + let env'' = safe_push_named (LocalAssum (x,t)) senv.env in + { senv with sections; env = env'' } + +let push_section_context (nas, ctx) senv = + let sections = Section.push_context (nas, ctx) senv.sections in + let senv = { senv with sections } in + let ctx = Univ.ContextSet.of_context ctx in + (* We check that the universes are fresh. FIXME: This should be done + implicitly, but we have to work around the API. *) + let () = assert (Univ.LSet.for_all (fun u -> not (Univ.LSet.mem u (fst senv.univ))) (fst ctx)) in + { senv with + env = Environ.push_context_set ~strict:false ctx senv.env; + univ = Univ.ContextSet.union ctx senv.univ } (** {6 Insertion of new declarations to current environment } *) @@ -469,34 +491,26 @@ 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] *) + [cstrs] | Polymorphic _ -> - [Now (true, Univ.ContextSet.empty)] + [] let globalize_mind_universes mb = match mb.mind_universes with | Monomorphic ctx -> - [Now (false, ctx)] - | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] + [ctx] + | Polymorphic _ -> [] -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)] + | SFBmodtype mtb -> [mtb.mod_constraints] + | SFBmodule mb -> [mb.mod_constraints] let add_retroknowledge pttc senv = { senv with @@ -531,8 +545,9 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = separately. *) senv else - let cst = constraints_of_sfb senv.env sfb in - add_constraints_list cst senv + (* Delayed constraints from opaque body are added by [add_constant_aux] *) + let cst = constraints_of_sfb sfb in + List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env @@ -541,8 +556,19 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = | SFBmodule mb, M -> Modops.add_module mb senv.env | _ -> assert false in + let sections = match sfb, gn with + | SFBconst cb, C con -> + let poly = Declareops.constant_is_polymorphic cb in + Section.push_constant ~poly con senv.sections + | SFBmind mib, I mind -> + let poly = Declareops.inductive_is_polymorphic mib in + Section.push_inductive ~poly mind senv.sections + | _, (M | MT) -> senv.sections + | _ -> assert false + in { senv with env = env'; + sections; revstruct = field :: senv.revstruct; modlabels = Label.Set.union mlabs senv.modlabels; objlabels = Label.Set.union olabs senv.objlabels } @@ -553,18 +579,18 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type 'a effect_entry = -| EffectEntry : private_constants effect_entry +| EffectEntry : private_constants Entries.seff_wrap effect_entry | PureEntry : unit effect_entry type global_declaration = | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration - | GlobalRecipe of Cooking.recipe -type exported_private_constant = - Constant.t * Entries.side_effect_role +type exported_private_constant = Constant.t let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn 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 @@ -588,32 +614,27 @@ let add_constant_aux ~in_section senv (kn, cb) = let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty let inline_side_effects env body side_eff = - let open Entries in let open Constr in (** First step: remove the constants that are still in the environment *) - let filter { eff = se; from_env = mb } = - let map e = (e.seff_constant, e.seff_body, e.seff_env) in - let cbl = List.map map se in - let not_exists (c,_,_) = - try ignore(Environ.lookup_constant c env); false - with Not_found -> true in - let cbl = List.filter not_exists cbl in - (cbl, mb) + let filter e = + let cb = (e.seff_constant, e.seff_body) in + try ignore (Environ.lookup_constant e.seff_constant env); None + with Not_found -> Some (cb, e.from_env) in (* CAVEAT: we assure that most recent effects come first *) - let side_eff = List.map filter (SideEffects.repr side_eff) in - let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in - let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in + let side_eff = List.map_filter filter (SideEffects.repr side_eff) in + let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in + let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in let side_eff = List.rev side_eff in (** Most recent side-effects first in side_eff *) if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) else (** Second step: compute the lifts and substitutions to apply *) let cname c r = Context.make_annot (Name (Label.to_id (Constant.label c))) r in - let fold (subst, var, ctx, args) (c, cb, b) = - let (b, opaque) = match cb.const_body, b with - | Def b, _ -> (Mod_subst.force_constr b, false) - | OpaqueDef _, `Opaque (b,_) -> (b, true) + let fold (subst, var, ctx, args) (c, cb) = + let (b, opaque) = match cb.const_body with + | Def b -> (Mod_subst.force_constr b, false) + | OpaqueDef b -> (b, true) | _ -> assert false in match cb.const_universes with @@ -662,37 +683,27 @@ 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 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 inline_private_constants_in_constr env body side_eff = - pi1 (inline_side_effects env body side_eff) - -let rec is_nth_suffix n l suf = - if Int.equal n 0 then l == suf - else match l with - | [] -> false - | _ :: l -> is_nth_suffix (pred n) l suf +let is_suffix l suf = match l with +| [] -> false +| _ :: l -> l == suf (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct. Returns the number of effects that can be trusted. *) let check_signatures curmb sl = - let is_direct_ancestor accu (mb, how_many) = + let is_direct_ancestor accu mb = match accu with | None -> None | Some (n, curmb) -> try let mb = CEphemeron.get mb in - if is_nth_suffix how_many mb curmb - then Some (n + how_many, mb) + if is_suffix mb curmb + then Some (n + 1, mb) else None with CEphemeron.InvalidKey -> None in let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in @@ -700,8 +711,12 @@ let check_signatures curmb sl = | None -> 0 | Some (n, _) -> n +type side_effect_declaration = +| DefinitionEff : Entries.definition_entry -> side_effect_declaration +| OpaqueEff : unit Entries.const_entry_body Entries.opaque_entry -> side_effect_declaration -let constant_entry_of_side_effect cb u = +let constant_entry_of_side_effect eff = + let cb = eff.seff_body in let open Entries in let univs = match cb.const_universes with @@ -710,101 +725,104 @@ let constant_entry_of_side_effect cb u = | Polymorphic auctx -> Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in - let pt = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b, c) -> b, c - | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + let p = + match cb.const_body with + | OpaqueDef b -> b + | Def b -> Mod_subst.force_constr b | _ -> assert false in - DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); - const_entry_secctx = None; + if Declareops.is_opaque cb then + OpaqueEff { + opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); + opaque_entry_secctx = cb.const_hyps; + opaque_entry_feedback = None; + opaque_entry_type = cb.const_type; + opaque_entry_universes = univs; + } + else + DefinitionEff { + const_entry_body = p; + const_entry_secctx = Some cb.const_hyps; const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } -let turn_direct orig = - let open Entries in - let cb = orig.seff_body in - if Declareops.is_opaque cb then - let p = match orig.seff_env with - | `Opaque (b, c) -> (b, c) - | _ -> assert false - in - let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in - let cb = { cb with const_body } in - { orig with seff_body = cb } - else orig - let export_eff eff = - let open Entries in - (eff.seff_constant, eff.seff_body, eff.seff_role) + (eff.seff_constant, eff.seff_body) -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 - let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = List.filter not_exists se in - if List.is_empty cbl then acc, sl - else cbl :: acc, (mb,List.length cbl) :: sl in + let aux (acc,sl) e = + if not (not_exists e) then acc, sl + else e :: acc, e.from_env :: sl in let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in let trusted = check_signatures mb signatures in let push_seff env eff = let { seff_constant = kn; seff_body = cb ; _ } = eff in - let env = Environ.add_constant kn cb env in + let env = Environ.add_constant kn (lift_constant cb) env in match cb.const_universes with | Polymorphic _ -> env | Monomorphic ctx -> - let ctx = match eff.seff_env with - | `Nothing -> ctx - | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx - in Environ.push_context_set ~strict:true ctx env in let rec translate_seff sl seff acc env = match seff with - | [] -> List.rev acc, ce - | cbs :: rest -> + | [] -> List.rev acc, b_ctx + | eff :: rest -> if Int.equal sl 0 then - let env, cbs = - List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in - let ce = constant_entry_of_side_effect ocb u in - let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let eff = { eff with - seff_body = cb; - seff_env = `Nothing; - } in - (push_seff env eff, export_eff eff :: cbs)) - (env,[]) cbs in - translate_seff 0 rest (cbs @ acc) env + let env, cb = + let kn = eff.seff_constant in + let ce = constant_entry_of_side_effect eff in + let open Entries in + let open Term_typing in + let cb = match ce with + | DefinitionEff ce -> + Term_typing.translate_constant Pure env kn (DefinitionEntry ce) + | OpaqueEff ce -> + let handle _env c () = (c, Univ.ContextSet.empty, 0) in + Term_typing.translate_constant (SideEffects handle) env kn (OpaqueEntry ce) + in + let map cu = + let (c, u) = Future.force cu in + let () = match u with + | Opaqueproof.PrivateMonomorphic ctx + | Opaqueproof.PrivatePolymorphic (_, ctx) -> + assert (Univ.ContextSet.is_empty ctx) + in + c + in + let cb = map_constant map cb in + let eff = { eff with seff_body = cb } in + (push_seff env eff, export_eff eff) + in + translate_seff 0 rest (cb :: acc) env else - let cbs_len = List.length cbs in - let cbs = List.map turn_direct cbs in - let env = List.fold_left push_seff env cbs in - let ecbs = List.map export_eff cbs in - translate_seff (sl - cbs_len) rest (ecbs @ acc) env + let env = push_seff env eff in + let ecb = export_eff eff in + translate_seff (sl - 1) rest (ecb :: acc) env in translate_seff trusted seff [] env let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in - let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in + let map univs p = + let local = match univs with + | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty + | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + in + Opaqueproof.create (Future.from_val (p, local)) + in + let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in + let bodies = List.map map exported in + let exported = List.map (fun (kn, _) -> kn) exported in + (* No delayed constants to declare *) let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in (ce, exported), senv -let add_constant ~in_section l decl senv = +let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl senv : (Constant.t * a) * safe_environment = let kn = Constant.make2 senv.modpath l in - let senv = let cb = match decl with | ConstantEntry (EffectEntry, ce) -> @@ -816,10 +834,26 @@ let add_constant ~in_section l decl senv = Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce | ConstantEntry (PureEntry, ce) -> Term_typing.translate_constant Term_typing.Pure senv.env kn ce - | GlobalRecipe r -> - let cb = Term_typing.translate_recipe ~hcons:(not in_section) senv.env kn r in - if in_section then cb else Declareops.hcons_const_body cb in - add_constant_aux ~in_section senv (kn, cb) in + in + let senv = + let delayed_cst = match cb.const_body with + | OpaqueDef fc when not (Declareops.constant_is_polymorphic cb) -> + let map (_, u) = match u with + | Opaqueproof.PrivateMonomorphic ctx -> ctx + | Opaqueproof.PrivatePolymorphic _ -> assert false + in + let fc = Future.chain fc map in + begin match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now c] + end + | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] + in + let cb = map_constant (fun c -> Opaqueproof.create c) cb in + let senv = add_constant_aux ~in_section senv (kn, cb) in + add_constraints_list delayed_cst senv + in + let senv = match decl with | ConstantEntry (_,(Entries.PrimitiveEntry { Entries.prim_entry_content = CPrimitives.OT_type t; _ })) -> @@ -827,7 +861,34 @@ let add_constant ~in_section l decl senv = add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv | _ -> senv in - kn, senv + let eff : a = match side_effect with + | PureEntry -> () + | EffectEntry -> + let body, univs = match cb.const_body with + | (Primitive _ | Undef _) -> assert false + | Def c -> (Def c, cb.const_universes) + | OpaqueDef o -> + let (b, delayed) = Future.force o in + match cb.const_universes, delayed with + | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> + OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') + | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> + (* Upper layers enforce that there are no internal constraints *) + let () = assert (Univ.ContextSet.is_empty ctx) in + OpaqueDef b, Polymorphic auctx + | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) -> + assert false + in + let cb = { cb with const_body = body; const_universes = univs } in + let from_env = CEphemeron.create senv.revstruct in + let eff = { + from_env = from_env; + seff_constant = kn; + seff_body = cb; + } in + { Entries.seff_wrap = SideEffects.add eff empty_private_constants } + in + (kn, eff), senv (** Insertion of inductive types *) @@ -860,13 +921,13 @@ let add_modtype l params_mte inl senv = (** full_add_module adds module with universes and constraints *) let full_add_module mb senv = - let senv = add_constraints (Now (false, mb.mod_constraints)) senv in + let senv = add_constraints (Now mb.mod_constraints) senv in let dp = ModPath.dp mb.mod_mp in let linkinfo = Nativecode.link_info_of_dirpath dp in { senv with env = Modops.add_linked_module mb linkinfo senv.env } let full_add_module_type mp mt senv = - let senv = add_constraints (Now (false, mt.mod_constraints)) senv in + let senv = add_constraints (Now mt.mod_constraints) senv in { senv with env = Modops.add_module_type mp mt senv.env } (** Insertion of modules *) @@ -882,6 +943,73 @@ let add_module l me inl senv = in (mp,mb.mod_delta),senv'' +(** {6 Interactive sections *) + +let open_section senv = + let custom = { + rev_env = senv.env; + rev_univ = senv.univ; + rev_objlabels = senv.objlabels; + } in + let sections = Section.open_section ~custom senv.sections in + { senv with sections } + +let close_section senv = + let open Section in + let sections0 = senv.sections in + let env0 = senv.env in + (* First phase: revert the declarations added in the section *) + let sections, entries, cstrs, revert = Section.close_section sections0 in + let rec pop_revstruct accu entries revstruct = match entries, revstruct with + | [], revstruct -> accu, revstruct + | _ :: _, [] -> + CErrors.anomaly (Pp.str "Unmatched section data") + | entry :: entries, (lbl, leaf) :: revstruct -> + let data = match entry, leaf with + | SecDefinition kn, SFBconst cb -> + let () = assert (Label.equal lbl (Constant.label kn)) in + `Definition (kn, cb) + | SecInductive ind, SFBmind mib -> + let () = assert (Label.equal lbl (MutInd.label ind)) in + `Inductive (ind, mib) + | (SecDefinition _ | SecInductive _), (SFBconst _ | SFBmind _) -> + CErrors.anomaly (Pp.str "Section content mismatch") + | (SecDefinition _ | SecInductive _), (SFBmodule _ | SFBmodtype _) -> + CErrors.anomaly (Pp.str "Module inside a section") + in + pop_revstruct (data :: accu) entries revstruct + in + let redo, revstruct = pop_revstruct [] entries senv.revstruct in + (* Don't revert the delayed constraints. If some delayed constraints were + forced inside the section, they have been turned into global monomorphic + that are going to be replayed. Those that are not forced are not readded + by {!add_constant_aux}. *) + let { rev_env = env; rev_univ = univ; rev_objlabels = objlabels } = revert in + let senv = { senv with env; revstruct; sections; univ; objlabels; } in + (* Second phase: replay the discharged section contents *) + let senv = add_constraints (Now cstrs) senv in + let modlist = Section.replacement_context env0 sections0 in + let cooking_info seg = + let { abstr_ctx; abstr_subst; abstr_uctx } = seg in + let abstract = (abstr_ctx, abstr_subst, abstr_uctx) in + { Opaqueproof.modlist; abstract } + in + let fold senv = function + | `Definition (kn, cb) -> + let in_section = not (Section.is_empty senv.sections) in + let info = cooking_info (Section.segment_of_constant env0 kn sections0) in + let r = { Cooking.from = cb; info } in + let cb = Term_typing.translate_recipe senv.env kn r in + (* Delayed constants are already in the global environment *) + add_constant_aux ~in_section senv (kn, cb) + | `Inductive (ind, mib) -> + let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in + let mie = Cooking.cook_inductive info mib in + let mie = InferCumulativity.infer_inductive senv.env mie in + let _, senv = add_mind (MutInd.label ind) mie senv in + senv + in + List.fold_left fold senv redo (** {6 Starting / ending interactive modules and module types } *) @@ -987,8 +1115,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv = required = senv.required; loads = senv.loads@oldsenv.loads; local_retroknowledge = - senv.local_retroknowledge@oldsenv.local_retroknowledge; - native_symbols = senv.native_symbols} + senv.local_retroknowledge@oldsenv.local_retroknowledge; + } let end_module l restype senv = let mp = senv.modpath in @@ -998,6 +1126,7 @@ let end_module l restype senv = let mbids = List.rev_map fst params in let mb = build_module_body params restype senv in let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in + let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in let newenv = set_engagement_opt newenv senv.engagement in let senv'= propagate_loads { senv with @@ -1028,6 +1157,7 @@ let end_modtype l senv = let () = check_empty_context senv in let mbids = List.rev_map fst params in let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in + let newenv = Environ.set_native_symbols newenv senv.env.Environ.native_symbols in let newenv = Environ.push_context_set ~strict:true senv.univ newenv in let newenv = set_engagement_opt newenv senv.engagement in let senv' = propagate_loads {senv with env=newenv} in @@ -1046,7 +1176,7 @@ let add_include me is_module inl senv = let sign,(),resolver,cst = translate_mse_incl is_module senv.env mp_sup inl me in - let senv = add_constraints (Now (false, cst)) senv in + let senv = add_constraints (Now cst) senv in (* Include Self support *) let rec compute_sign sign mb resolver senv = match sign with @@ -1054,7 +1184,7 @@ let add_include me is_module inl senv = let cst_sub = Subtyping.check_subtypes senv.env mb mtb in let senv = add_constraints - (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) + (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) senv in let mpsup_delta = Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta @@ -1091,19 +1221,13 @@ type compiled_library = { comp_mod : module_body; comp_deps : library_info array; comp_enga : engagement; - comp_natsymbs : Nativecode.symbols + comp_natsymbs : Nativevalues.symbols } let module_of_library lib = lib.comp_mod type native_library = Nativecode.global list -let get_library_native_symbols senv dir = - try DPMap.find dir senv.native_symbols - with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols" - Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ - (str "This use case is not supported, but disabling the native compiler may help.")) - (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath let current_dirpath senv = Names.ModPath.dp (current_modpath senv) @@ -1143,12 +1267,12 @@ let export ?except ~output_native_objects senv dir = let ast, symbols = if output_native_objects then Nativelibrary.dump_library mp dir senv.env str - else [], Nativecode.empty_symbols + else [], Nativevalues.empty_symbols in let lib = { comp_name = dir; comp_mod = mb; - comp_deps = Array.of_list (DPMap.bindings senv.required); + comp_deps = Array.of_list (DPmap.bindings senv.required); comp_enga = Environ.engagement senv.env; comp_natsymbs = symbols } in @@ -1168,17 +1292,18 @@ let import lib cst vodigest senv = (Univ.ContextSet.union mb.mod_constraints cst) senv.env in + let env = + let linkinfo = Nativecode.link_info_of_dirpath lib.comp_name in + Modops.add_linked_module mb linkinfo env + in + let env = Environ.add_native_symbols lib.comp_name lib.comp_natsymbs env in mp, { senv with - env = - (let linkinfo = - Nativecode.link_info_of_dirpath lib.comp_name - in - Modops.add_linked_module mb linkinfo env); + env; modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver; - required = DPMap.add lib.comp_name vodigest senv.required; + required = DPmap.add lib.comp_name vodigest senv.required; loads = (mp,mb)::senv.loads; - native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols } + } (** {6 Safe typing } *) @@ -1284,7 +1409,7 @@ let register_inductive ind prim senv = let add_constraints c = add_constraints - (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) + (Now (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) (* NB: The next old comment probably refers to [propagate_loads] above. |