diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 207 |
1 files changed, 110 insertions, 97 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75..de2a890f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre as part of the rebuilding of @@ -62,6 +64,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -69,7 +73,7 @@ open Context.Named.Declaration - [env] : the underlying environment (cf Environ) - [modpath] : the current module name - [modvariant] : - * NONE before coqtop initialization (or when -notop is used) + * NONE before coqtop initialization * LIBRARY at toplevel of a compilation or a regular coqtop session * STRUCT (params,oldsenv) : inside a local module, with module parameters [params] and earlier environment [oldsenv] @@ -112,7 +116,7 @@ module DPMap = Map.Make(DirPath) type safe_environment = { env : Environ.env; - modpath : module_path; + modpath : ModPath.t; modvariant : modvariant; modresolver : Mod_subst.delta_resolver; paramresolver : Mod_subst.delta_resolver; @@ -123,7 +127,7 @@ type safe_environment = future_cst : Univ.ContextSet.t Future.computation list; engagement : engagement option; required : vodigest DPMap.t; - loads : (module_path * module_body) list; + loads : (ModPath.t * module_body) list; local_retroknowledge : Retroknowledge.action list; native_symbols : Nativecode.symbols DPMap.t } @@ -141,7 +145,7 @@ let rec library_dp_of_senv senv = let empty_environment = { env = Environ.empty_env; - modpath = initial_path; + modpath = ModPath.initial; modvariant = NONE; modresolver = Mod_subst.empty_delta_resolver; paramresolver = Mod_subst.empty_delta_resolver; @@ -158,7 +162,7 @@ let empty_environment = let is_initial senv = match senv.revstruct, senv.modvariant with - | [], NONE -> ModPath.equal senv.modpath initial_path + | [], NONE -> ModPath.equal senv.modpath ModPath.initial | _ -> false let delta_of_senv senv = senv.modresolver,senv.paramresolver @@ -190,7 +194,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - CErrors.error "Needs option -impredicative-set." + CErrors.user_err Pp.(str "Needs option -impredicative-set.") | _ -> () end @@ -206,19 +210,19 @@ let get_opaque_body env cbo = Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) type private_constant = Entries.side_effect -type private_constants = private_constant list +type private_constants = Term_typing.side_effects type private_constant_role = Term_typing.side_effect_role = | Subproof | Schema of inductive * string -let empty_private_constants = [] -let add_private x xs = x :: xs -let concat_private xs ys = xs @ ys +let empty_private_constants = Term_typing.empty_seff +let add_private = Term_typing.add_seff +let concat_private = Term_typing.concat_seff let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects -let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x) +let side_effects_of_private_constants = Term_typing.uniq_seff let private_con_of_con env c = let cbo = Environ.lookup_constant c env.env in @@ -235,20 +239,29 @@ let private_con_of_scheme ~kind env cl = let universes_of_private eff = let open Declarations in - List.fold_left (fun acc { Entries.eff } -> - match eff with - | Entries.SEscheme (l,s) -> - List.fold_left (fun acc (_,_,cb,c) -> - let acc = match c with - | `Nothing -> acc - | `Opaque (_, ctx) -> ctx :: acc in - if cb.const_polymorphic then acc - else (Univ.ContextSet.of_context cb.const_universes) :: acc) - acc l - | Entries.SEsubproof (c, cb, e) -> - if cb.const_polymorphic then acc - else Univ.ContextSet.of_context cb.const_universes :: acc) - [] eff + List.fold_left + (fun acc { Entries.eff } -> + match eff with + | Entries.SEscheme (l,s) -> + List.fold_left + (fun acc (_,_,cb,c) -> + let acc = match c with + | `Nothing -> acc + | `Opaque (_, ctx) -> ctx :: acc + in + match cb.const_universes with + | Monomorphic_const ctx -> + ctx :: acc + | Polymorphic_const _ -> acc + ) + acc l + | Entries.SEsubproof (c, cb, e) -> + match cb.const_universes with + | Monomorphic_const ctx -> + ctx :: acc + | Polymorphic_const _ -> acc + ) + [] (Term_typing.uniq_seff eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -344,10 +357,10 @@ let check_required current_libs needed = try let actual = DPMap.find id current_libs in if not(digest_match ~actual ~required) then - CErrors.error - ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str + ["Inconsistent assumptions over module"; DirPath.to_string id; "."]) with Not_found -> - CErrors.error ("Reference to unknown module "^(DirPath.to_string id)^".") + CErrors.user_err Pp.(pr_sequence str ["Reference to unknown module"; DirPath.to_string id; "."]) in Array.iter check needed @@ -361,29 +374,19 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in - CErrors.error ("Identifier "^Id.to_string id^" already defined.") + CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."]) with Not_found -> () in Environ.push_named d env let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in - let poly = de.Entries.const_entry_polymorphic in - let univs = Univ.ContextSet.of_context univs in - let c, univs = match c with - | Def c -> Mod_subst.force_constr c, univs - | OpaqueDef o -> - Opaqueproof.force_proof (Environ.opaque_tables senv.env) o, - Univ.ContextSet.union univs - (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o) - | _ -> assert false in - let senv' = push_context_set poly univs senv in - let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in - univs, {senv' with env=env''} + let c, typ = Term_typing.translate_local_def senv.env id de in + let env'' = safe_push_named (LocalDef (id, 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 @@ -408,26 +411,27 @@ let labels_of_mib mib = get () let globalize_constant_universes env cb = - if cb.const_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - let cstrs = Univ.ContextSet.of_context cb.const_universes in - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> + match cb.const_universes with + | Monomorphic_const cstrs -> + Now (false, cstrs) :: + (match cb.const_body with + | (Undef _ | Def _) -> [] + | 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)]) + | None -> [Later fc] + | Some c -> [Now (false, c)]) + | Polymorphic_const _ -> + [Now (true, Univ.ContextSet.empty)] let globalize_mind_universes mb = - if mb.mind_polymorphic then - [Now (true, Univ.ContextSet.empty)] - else - [Now (false, Univ.ContextSet.of_context mb.mind_universes)] + match mb.mind_universes with + | Monomorphic_ind ctx -> + [Now (false, ctx)] + | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)] + | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)] let constraints_of_sfb env sfb = match sfb with @@ -440,8 +444,8 @@ let constraints_of_sfb env sfb = It also performs the corresponding [add_constraints]. *) type generic_name = - | C of constant - | I of mutual_inductive + | C of Constant.t + | I of MutInd.t | M (** name already known, cf the mod_mp field *) | MT (** name already known, cf the mod_mp field *) @@ -475,12 +479,16 @@ let add_field ((l,sfb) as field) gn senv = 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 +| PureEntry : unit effect_entry + type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + Constant.t * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -499,35 +507,34 @@ let add_constant_aux no_section senv (kn, cb) = let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver - (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv' + (Mod_subst.add_inline_delta_resolver (Constant.user kn) (lev,None)) senv' | _ -> senv' in senv'' +let export_private_constants ~in_section ce senv = + let exported, ce = Term_typing.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 no_section = not in_section in + let senv = List.fold_left (add_constant_aux no_section) senv bodies in + (ce, exported), senv + let add_constant dir l decl senv = - let kn = make_con senv.modpath dir l in + let kn = Constant.make3 senv.modpath dir l in let no_section = DirPath.is_empty dir in - let seff_to_export, decl = - match decl with - | ConstantEntry (true, ce) -> - let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) - | _ -> [], decl - in - let senv = - List.fold_left (add_constant_aux no_section) senv - (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (EffectEntry, ce) -> + Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) 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 senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in add_constant_aux no_section senv (kn, cb) in - (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv + kn, senv (** Insertion of inductive types *) @@ -541,7 +548,7 @@ let check_mind mie lab = let add_mind dir l mie senv = let () = check_mind mie l in - let kn = make_mind senv.modpath dir l in + let kn = MutInd.make3 senv.modpath dir l in let mib = Term_typing.translate_mind senv.env kn mie in let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib @@ -553,7 +560,7 @@ let add_mind dir l mie senv = let add_modtype l params_mte inl senv = let mp = MPdot(senv.modpath, l) in let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte in - let mtb = Declareops.hcons_module_body mtb in + let mtb = Declareops.hcons_module_type mtb in let senv' = add_field (l,SFBmodtype mtb) MT senv in mp, senv' @@ -656,18 +663,21 @@ let build_module_body params restype senv = (struc,None,senv.modresolver,senv.univ) restype' in let mb' = functorize_module params mb in - { mb' with mod_retroknowledge = senv.local_retroknowledge } + { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge } (** Returning back to the old pre-interactive-module environment, with one extra component and some updated fields (constraints, required, etc) *) +let allow_delayed_constants = ref false + let propagate_senv newdef newenv newresolver senv oldsenv = let now_cst, later_cst = List.partition Future.is_val senv.future_cst in (* This asserts that after Paral-ITP, standard vo compilation is behaving * exctly as before: the same universe constraints are added to modules *) - if !Flags.compilation_mode = Flags.BuildVo && - !Flags.async_proofs_mode = Flags.APoff then assert(later_cst = []); + if not !allow_delayed_constants && later_cst <> [] then + CErrors.anomaly ~label:"safe_typing" + Pp.(str "True Future.t were created for opaque constants even if -async-proofs is off"); { oldsenv with env = newenv; modresolver = newresolver; @@ -711,12 +721,12 @@ let end_module l restype senv = let build_mtb mp sign cst delta = { mod_mp = mp; - mod_expr = Abstract; + mod_expr = (); mod_type = sign; mod_type_alg = None; mod_constraints = cst; mod_delta = delta; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } let end_modtype l senv = let mp = senv.modpath in @@ -794,7 +804,10 @@ type compiled_library = { type native_library = Nativecode.global list let get_library_native_symbols senv dir = - DPMap.find dir senv.native_symbols + 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 @@ -816,7 +829,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = CErrors.push e in - CErrors.errorlabstrm "export" (CErrors.iprint e) + CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -829,11 +842,11 @@ let export ?except senv dir = mod_type_alg = None; mod_constraints = senv.univ; mod_delta = senv.modresolver; - mod_retroknowledge = senv.local_retroknowledge + mod_retroknowledge = ModBodyRK senv.local_retroknowledge } in let ast, symbols = - if !Flags.native_compiler then + if !Flags.output_native_objects then Nativelibrary.dump_library mp dir senv.env str else [], Nativecode.empty_symbols in @@ -852,7 +865,7 @@ let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then - CErrors.errorlabstrm "Safe_typing.import" + CErrors.user_err ~hdr:"Safe_typing.import" (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in @@ -903,7 +916,7 @@ let register_inline kn senv = let open Environ in let open Pre_env in if not (evaluable_constant kn senv.env) then - CErrors.error "Register inline: an evaluable constant is expected"; + CErrors.user_err Pp.(str "Register inline: an evaluable constant is expected"); let env = pre_env senv.env in let (cb,r) = Cmap_env.find kn env.env_globals.env_constants in let cb = {cb with const_inline_code = true} in |