diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 91 |
1 files changed, 69 insertions, 22 deletions
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) + |