diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 7 | ||||
| -rw-r--r-- | library/global.mli | 3 | ||||
| -rw-r--r-- | library/goptions.ml | 19 | ||||
| -rw-r--r-- | library/lib.ml | 17 | ||||
| -rw-r--r-- | library/lib.mli | 4 |
5 files changed, 28 insertions, 22 deletions
diff --git a/library/global.ml b/library/global.ml index dcb20a280e..e833f71142 100644 --- a/library/global.ml +++ b/library/global.ml @@ -90,6 +90,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let typing_flags () = Environ.typing_flags (env ()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) @@ -278,3 +279,9 @@ let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) +let set_reduction_sharing b = + let env = safe_env () in + let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in + let flags = { flags with Declarations.share_reduction = b } in + let env = Safe_typing.set_typing_flags flags env in + GlobalSafeEnv.set_safe_env env diff --git a/library/global.mli b/library/global.mli index b2a191ceeb..2819c187ed 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,6 +30,7 @@ val named_context : unit -> Constr.named_context (** Changing the (im)predicativity of the system *) val set_engagement : Declarations.engagement -> unit val set_typing_flags : Declarations.typing_flags -> unit +val typing_flags : unit -> Declarations.typing_flags (** Variables, Local definitions, constants, inductive types *) @@ -155,6 +156,8 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit +val set_reduction_sharing : bool -> unit + (* Modifies the global state, registering new universes *) val current_modpath : unit -> ModPath.t diff --git a/library/goptions.ml b/library/goptions.ml index f14ad333e9..eafcb8fea6 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -318,26 +318,35 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = | Some (name, depr, (read,write,append)) -> write locality (check_and_cast v (read ())) -let bad_type_error () = user_err Pp.(str "Bad type of value for this option.") +let show_value_type = function + | BoolValue _ -> "bool" + | IntValue _ -> "int" + | StringValue _ -> "string" + | StringOptValue _ -> "string" + +let bad_type_error opt_value actual_type = + user_err Pp.(str "Bad type of value for this option:" ++ spc() ++ + str "expected " ++ str (show_value_type opt_value) ++ + str ", got " ++ str actual_type ++ str ".") let check_int_value v = function | IntValue _ -> IntValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "int" let check_bool_value v = function | BoolValue _ -> BoolValue v - | _ -> bad_type_error () + | optv -> bad_type_error optv "bool" let check_string_value v = function | StringValue _ -> StringValue v | StringOptValue _ -> StringOptValue (Some v) - | _ -> bad_type_error () + | optv -> bad_type_error optv "string" let check_unset_value v = function | BoolValue _ -> BoolValue false | IntValue _ -> IntValue None | StringOptValue _ -> StringOptValue None - | _ -> bad_type_error () + | optv -> bad_type_error optv "nothing" (* Nota: For compatibility reasons, some errors are treated as warning. This allows a script to refer to an option that doesn't diff --git a/library/lib.ml b/library/lib.ml index 8b83261e48..8ebe44890c 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -26,13 +26,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of is_type * export * object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_entry = object_name * node +type library_entry = object_name * node -and library_segment = library_entry list +type library_segment = library_entry list type lib_objects = (Names.Id.t * obj) list @@ -73,10 +71,6 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (_,ClosedSection _) :: stk -> clean acc stk - (* LEM; TODO: Understand what this does and see if what I do is the - correct thing for ClosedMod(ule|type) *) - | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> user_err Pp.(str "there are still opened sections") | (_,OpenedModule (ty,_,_,_)) :: _ -> user_err ~hdr:"Lib.classify_segment" @@ -307,7 +301,6 @@ let end_mod is_type = in let (after,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; - add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !lib_state.path_prefix in recalc_path_prefix (); (oname, prefix, fs, after) @@ -555,7 +548,6 @@ let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) - | ClosedSection _ | ClosedModule _ -> None | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly (Pp.str "discharge_item.") @@ -570,7 +562,6 @@ let close_section () = let (secdecls,mark,before) = split_lib_at_opening oname in lib_state := { !lib_state with lib_stk = before }; pop_path_prefix (); - add_entry oname (ClosedSection (List.rev (mark::secdecls))); let newdecls = List.map discharge_item secdecls in Summary.unfreeze_summaries fs; List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls @@ -589,10 +580,8 @@ let freeze ~marshallable = | n, (CompilingLibrary _ as x) -> Some (n,x) | n, OpenedModule (it,e,op,_) -> Some(n,OpenedModule(it,e,op,Summary.empty_frozen)) - | n, ClosedModule _ -> Some (n,ClosedModule []) | n, OpenedSection (op, _) -> - Some(n,OpenedSection(op,Summary.empty_frozen)) - | n, ClosedSection _ -> Some (n,ClosedSection [])) + Some(n,OpenedSection(op,Summary.empty_frozen))) !lib_state.lib_stk in { !lib_state with lib_stk } | _ -> diff --git a/library/lib.mli b/library/lib.mli index c6856a55b4..9933b762ba 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -23,11 +23,9 @@ type node = | Leaf of Libobject.obj | CompilingLibrary of Libnames.object_prefix | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen - | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen - | ClosedSection of library_segment -and library_segment = (Libnames.object_name * node) list +type library_segment = (Libnames.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list |