more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
authorwenzelm
Mon Sep 06 21:33:19 2010 +0200 (2010-09-06)
changeset 391634d701c0388c3
parent 39162 e6ec5283cd22
child 39164 e7e12555e763
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;
src/Pure/Isar/attrib.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/config.ML
src/Pure/goal_display.ML
src/Pure/meta_simplifier.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Mon Sep 06 19:23:54 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Mon Sep 06 21:33:19 2010 +0200
     1.3 @@ -324,7 +324,7 @@
     1.4  
     1.5  structure Configs = Theory_Data
     1.6  (
     1.7 -  type T = Config.value Config.T Symtab.table;
     1.8 +  type T = Config.raw Symtab.table;
     1.9    val empty = Symtab.empty;
    1.10    val extend = I;
    1.11    fun merge data = Symtab.merge (K true) data;
    1.12 @@ -392,22 +392,22 @@
    1.13  (* theory setup *)
    1.14  
    1.15  val _ = Context.>> (Context.map_theory
    1.16 - (register_config Syntax.show_brackets_value #>
    1.17 -  register_config Syntax.show_sorts_value #>
    1.18 -  register_config Syntax.show_types_value #>
    1.19 -  register_config Syntax.show_structs_value #>
    1.20 -  register_config Syntax.show_question_marks_value #>
    1.21 -  register_config Syntax.ambiguity_level_value #>
    1.22 -  register_config Syntax.eta_contract_value #>
    1.23 -  register_config Goal_Display.goals_limit_value #>
    1.24 -  register_config Goal_Display.show_main_goal_value #>
    1.25 -  register_config Goal_Display.show_consts_value #>
    1.26 -  register_config Unify.trace_bound_value #>
    1.27 -  register_config Unify.search_bound_value #>
    1.28 -  register_config Unify.trace_simp_value #>
    1.29 -  register_config Unify.trace_types_value #>
    1.30 -  register_config MetaSimplifier.simp_depth_limit_value #>
    1.31 -  register_config MetaSimplifier.debug_simp_value #>
    1.32 -  register_config MetaSimplifier.trace_simp_value));
    1.33 + (register_config Syntax.show_brackets_raw #>
    1.34 +  register_config Syntax.show_sorts_raw #>
    1.35 +  register_config Syntax.show_types_raw #>
    1.36 +  register_config Syntax.show_structs_raw #>
    1.37 +  register_config Syntax.show_question_marks_raw #>
    1.38 +  register_config Syntax.ambiguity_level_raw #>
    1.39 +  register_config Syntax.eta_contract_raw #>
    1.40 +  register_config Goal_Display.goals_limit_raw #>
    1.41 +  register_config Goal_Display.show_main_goal_raw #>
    1.42 +  register_config Goal_Display.show_consts_raw #>
    1.43 +  register_config Unify.trace_bound_raw #>
    1.44 +  register_config Unify.search_bound_raw #>
    1.45 +  register_config Unify.trace_simp_raw #>
    1.46 +  register_config Unify.trace_types_raw #>
    1.47 +  register_config MetaSimplifier.simp_depth_limit_raw #>
    1.48 +  register_config MetaSimplifier.debug_simp_raw #>
    1.49 +  register_config MetaSimplifier.trace_simp_raw));
    1.50  
    1.51  end;
     2.1 --- a/src/Pure/Syntax/printer.ML	Mon Sep 06 19:23:54 2010 +0200
     2.2 +++ b/src/Pure/Syntax/printer.ML	Mon Sep 06 21:33:19 2010 +0200
     2.3 @@ -7,20 +7,20 @@
     2.4  signature PRINTER0 =
     2.5  sig
     2.6    val show_brackets_default: bool Unsynchronized.ref
     2.7 -  val show_brackets_value: Config.value Config.T
     2.8 +  val show_brackets_raw: Config.raw
     2.9    val show_brackets: bool Config.T
    2.10    val show_types_default: bool Unsynchronized.ref
    2.11 -  val show_types_value: Config.value Config.T
    2.12 +  val show_types_raw: Config.raw
    2.13    val show_types: bool Config.T
    2.14    val show_sorts_default: bool Unsynchronized.ref
    2.15 -  val show_sorts_value: Config.value Config.T
    2.16 +  val show_sorts_raw: Config.raw
    2.17    val show_sorts: bool Config.T
    2.18    val show_free_types: bool Config.T
    2.19    val show_all_types: bool Config.T
    2.20 -  val show_structs_value: Config.value Config.T
    2.21 +  val show_structs_raw: Config.raw
    2.22    val show_structs: bool Config.T
    2.23    val show_question_marks_default: bool Unsynchronized.ref
    2.24 -  val show_question_marks_value: Config.value Config.T
    2.25 +  val show_question_marks_raw: Config.raw
    2.26    val show_question_marks: bool Config.T
    2.27  end;
    2.28  
    2.29 @@ -55,28 +55,28 @@
    2.30  (** options for printing **)
    2.31  
    2.32  val show_brackets_default = Unsynchronized.ref false;
    2.33 -val show_brackets_value =
    2.34 +val show_brackets_raw =
    2.35    Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
    2.36 -val show_brackets = Config.bool show_brackets_value;
    2.37 +val show_brackets = Config.bool show_brackets_raw;
    2.38  
    2.39  val show_types_default = Unsynchronized.ref false;
    2.40 -val show_types_value = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
    2.41 -val show_types = Config.bool show_types_value;
    2.42 +val show_types_raw = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
    2.43 +val show_types = Config.bool show_types_raw;
    2.44  
    2.45  val show_sorts_default = Unsynchronized.ref false;
    2.46 -val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
    2.47 -val show_sorts = Config.bool show_sorts_value;
    2.48 +val show_sorts_raw = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
    2.49 +val show_sorts = Config.bool show_sorts_raw;
    2.50  
    2.51  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    2.52  val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
    2.53  
    2.54 -val show_structs_value = Config.declare "show_structs" (fn _ => Config.Bool false);
    2.55 -val show_structs = Config.bool show_structs_value;
    2.56 +val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
    2.57 +val show_structs = Config.bool show_structs_raw;
    2.58  
    2.59  val show_question_marks_default = Unsynchronized.ref true;
    2.60 -val show_question_marks_value =
    2.61 +val show_question_marks_raw =
    2.62    Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    2.63 -val show_question_marks = Config.bool show_question_marks_value;
    2.64 +val show_question_marks = Config.bool show_question_marks_raw;
    2.65  
    2.66  
    2.67  
     3.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon Sep 06 19:23:54 2010 +0200
     3.2 +++ b/src/Pure/Syntax/syn_trans.ML	Mon Sep 06 21:33:19 2010 +0200
     3.3 @@ -7,7 +7,7 @@
     3.4  signature SYN_TRANS0 =
     3.5  sig
     3.6    val eta_contract_default: bool Unsynchronized.ref
     3.7 -  val eta_contract_value: Config.value Config.T
     3.8 +  val eta_contract_raw: Config.raw
     3.9    val eta_contract: bool Config.T
    3.10    val atomic_abs_tr': string * typ * term -> term * term
    3.11    val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
    3.12 @@ -283,9 +283,8 @@
    3.13  (*do (partial) eta-contraction before printing*)
    3.14  
    3.15  val eta_contract_default = Unsynchronized.ref true;
    3.16 -val eta_contract_value =
    3.17 -  Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
    3.18 -val eta_contract = Config.bool eta_contract_value;
    3.19 +val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
    3.20 +val eta_contract = Config.bool eta_contract_raw;
    3.21  
    3.22  fun eta_contr ctxt tm =
    3.23    let
     4.1 --- a/src/Pure/Syntax/syntax.ML	Mon Sep 06 19:23:54 2010 +0200
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Sep 06 21:33:19 2010 +0200
     4.3 @@ -111,7 +111,7 @@
     4.4    val print_syntax: syntax -> unit
     4.5    val guess_infix: syntax -> string -> mixfix option
     4.6    val ambiguity_enabled: bool Config.T
     4.7 -  val ambiguity_level_value: Config.value Config.T
     4.8 +  val ambiguity_level_raw: Config.raw
     4.9    val ambiguity_level: int Config.T
    4.10    val ambiguity_limit: int Config.T
    4.11    val standard_parse_term: (term -> string option) ->
    4.12 @@ -694,8 +694,8 @@
    4.13  val ambiguity_enabled =
    4.14    Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
    4.15  
    4.16 -val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
    4.17 -val ambiguity_level = Config.int ambiguity_level_value;
    4.18 +val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
    4.19 +val ambiguity_level = Config.int ambiguity_level_raw;
    4.20  
    4.21  val ambiguity_limit =
    4.22    Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
     5.1 --- a/src/Pure/config.ML	Mon Sep 06 19:23:54 2010 +0200
     5.2 +++ b/src/Pure/config.ML	Mon Sep 06 21:33:19 2010 +0200
     5.3 @@ -10,9 +10,10 @@
     5.4    val print_value: value -> string
     5.5    val print_type: value -> string
     5.6    type 'a T
     5.7 -  val bool: value T -> bool T
     5.8 -  val int: value T -> int T
     5.9 -  val string: value T -> string T
    5.10 +  type raw = value T
    5.11 +  val bool: raw -> bool T
    5.12 +  val int: raw -> int T
    5.13 +  val string: raw -> string T
    5.14    val get: Proof.context -> 'a T -> 'a
    5.15    val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    5.16    val put: 'a T -> 'a -> Proof.context -> Proof.context
    5.17 @@ -22,9 +23,9 @@
    5.18    val get_generic: Context.generic -> 'a T -> 'a
    5.19    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    5.20    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    5.21 -  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
    5.22 -  val declare_global: string -> (Context.generic -> value) -> value T
    5.23 -  val declare: string -> (Context.generic -> value) -> value T
    5.24 +  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
    5.25 +  val declare_global: string -> (Context.generic -> value) -> raw
    5.26 +  val declare: string -> (Context.generic -> value) -> raw
    5.27    val name_of: 'a T -> string
    5.28  end;
    5.29  
    5.30 @@ -68,6 +69,8 @@
    5.31    get_value: Context.generic -> 'a,
    5.32    map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    5.33  
    5.34 +type raw = value T;
    5.35 +
    5.36  fun coerce make dest (Config {name, get_value, map_value}) = Config
    5.37   {name = name,
    5.38    get_value = dest o get_value,
     6.1 --- a/src/Pure/goal_display.ML	Mon Sep 06 19:23:54 2010 +0200
     6.2 +++ b/src/Pure/goal_display.ML	Mon Sep 06 21:33:19 2010 +0200
     6.3 @@ -8,14 +8,14 @@
     6.4  signature GOAL_DISPLAY =
     6.5  sig
     6.6    val goals_limit_default: int Unsynchronized.ref
     6.7 -  val goals_limit_value: Config.value Config.T
     6.8 +  val goals_limit_raw: Config.raw
     6.9    val goals_limit: int Config.T
    6.10    val goals_total: bool Config.T
    6.11    val show_main_goal_default: bool Unsynchronized.ref
    6.12 -  val show_main_goal_value: Config.value Config.T
    6.13 +  val show_main_goal_raw: Config.raw
    6.14    val show_main_goal: bool Config.T
    6.15    val show_consts_default: bool Unsynchronized.ref
    6.16 -  val show_consts_value: Config.value Config.T
    6.17 +  val show_consts_raw: Config.raw
    6.18    val show_consts: bool Config.T
    6.19    val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    6.20    val pretty_goals: Proof.context -> thm -> Pretty.T list
    6.21 @@ -26,19 +26,19 @@
    6.22  struct
    6.23  
    6.24  val goals_limit_default = Unsynchronized.ref 10;
    6.25 -val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    6.26 -val goals_limit = Config.int goals_limit_value;
    6.27 +val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    6.28 +val goals_limit = Config.int goals_limit_raw;
    6.29  
    6.30  val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
    6.31  
    6.32  val show_main_goal_default = Unsynchronized.ref false;
    6.33 -val show_main_goal_value =
    6.34 +val show_main_goal_raw =
    6.35    Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
    6.36 -val show_main_goal = Config.bool show_main_goal_value;
    6.37 +val show_main_goal = Config.bool show_main_goal_raw;
    6.38  
    6.39  val show_consts_default = Unsynchronized.ref false;
    6.40 -val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    6.41 -val show_consts = Config.bool show_consts_value;
    6.42 +val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    6.43 +val show_consts = Config.bool show_consts_raw;
    6.44  
    6.45  fun pretty_flexpair ctxt (t, u) = Pretty.block
    6.46    [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
     7.1 --- a/src/Pure/meta_simplifier.ML	Mon Sep 06 19:23:54 2010 +0200
     7.2 +++ b/src/Pure/meta_simplifier.ML	Mon Sep 06 21:33:19 2010 +0200
     7.3 @@ -12,9 +12,9 @@
     7.4  signature BASIC_META_SIMPLIFIER =
     7.5  sig
     7.6    val debug_simp: bool Config.T
     7.7 -  val debug_simp_value: Config.value Config.T
     7.8 +  val debug_simp_raw: Config.raw
     7.9    val trace_simp: bool Config.T
    7.10 -  val trace_simp_value: Config.value Config.T
    7.11 +  val trace_simp_raw: Config.raw
    7.12    val trace_simp_default: bool Unsynchronized.ref
    7.13    val trace_simp_depth_limit: int Unsynchronized.ref
    7.14    type rrule
    7.15 @@ -104,7 +104,7 @@
    7.16    val add_simp: thm -> simpset -> simpset
    7.17    val del_simp: thm -> simpset -> simpset
    7.18    val solver: simpset -> solver -> int -> tactic
    7.19 -  val simp_depth_limit_value: Config.value Config.T
    7.20 +  val simp_depth_limit_raw: Config.raw
    7.21    val simp_depth_limit: int Config.T
    7.22    val clear_ss: simpset -> simpset
    7.23    val simproc_global_i: theory -> string -> term list
    7.24 @@ -250,8 +250,8 @@
    7.25  
    7.26  (* simp depth *)
    7.27  
    7.28 -val simp_depth_limit_value = Config.declare "simp_depth_limit" (K (Config.Int 100));
    7.29 -val simp_depth_limit = Config.int simp_depth_limit_value;
    7.30 +val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
    7.31 +val simp_depth_limit = Config.int simp_depth_limit_raw;
    7.32  
    7.33  val trace_simp_depth_limit = Unsynchronized.ref 1;
    7.34  
    7.35 @@ -273,12 +273,12 @@
    7.36  
    7.37  exception SIMPLIFIER of string * thm;
    7.38  
    7.39 -val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
    7.40 -val debug_simp = Config.bool debug_simp_value;
    7.41 +val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
    7.42 +val debug_simp = Config.bool debug_simp_raw;
    7.43  
    7.44  val trace_simp_default = Unsynchronized.ref false;
    7.45 -val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
    7.46 -val trace_simp = Config.bool trace_simp_value;
    7.47 +val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
    7.48 +val trace_simp = Config.bool trace_simp_raw;
    7.49  
    7.50  fun if_enabled (Simpset ({context, ...}, _)) flag f =
    7.51    (case context of
     8.1 --- a/src/Pure/unify.ML	Mon Sep 06 19:23:54 2010 +0200
     8.2 +++ b/src/Pure/unify.ML	Mon Sep 06 21:33:19 2010 +0200
     8.3 @@ -11,13 +11,13 @@
     8.4  
     8.5  signature UNIFY =
     8.6  sig
     8.7 -  val trace_bound_value: Config.value Config.T
     8.8 +  val trace_bound_raw: Config.raw
     8.9    val trace_bound: int Config.T
    8.10 -  val search_bound_value: Config.value Config.T
    8.11 +  val search_bound_raw: Config.raw
    8.12    val search_bound: int Config.T
    8.13 -  val trace_simp_value: Config.value Config.T
    8.14 +  val trace_simp_raw: Config.raw
    8.15    val trace_simp: bool Config.T
    8.16 -  val trace_types_value: Config.value Config.T
    8.17 +  val trace_types_raw: Config.raw
    8.18    val trace_types: bool Config.T
    8.19    val unifiers: theory * Envir.env * ((term * term) list) ->
    8.20      (Envir.env * (term * term) list) Seq.seq
    8.21 @@ -32,20 +32,20 @@
    8.22  (*Unification options*)
    8.23  
    8.24  (*tracing starts above this depth, 0 for full*)
    8.25 -val trace_bound_value = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
    8.26 -val trace_bound = Config.int trace_bound_value;
    8.27 +val trace_bound_raw = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
    8.28 +val trace_bound = Config.int trace_bound_raw;
    8.29  
    8.30  (*unification quits above this depth*)
    8.31 -val search_bound_value = Config.declare_global "unify_search_bound" (K (Config.Int 60));
    8.32 -val search_bound = Config.int search_bound_value;
    8.33 +val search_bound_raw = Config.declare_global "unify_search_bound" (K (Config.Int 60));
    8.34 +val search_bound = Config.int search_bound_raw;
    8.35  
    8.36  (*print dpairs before calling SIMPL*)
    8.37 -val trace_simp_value = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
    8.38 -val trace_simp = Config.bool trace_simp_value;
    8.39 +val trace_simp_raw = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
    8.40 +val trace_simp = Config.bool trace_simp_raw;
    8.41  
    8.42  (*announce potential incompleteness of type unification*)
    8.43 -val trace_types_value = Config.declare_global "unify_trace_types" (K (Config.Bool false));
    8.44 -val trace_types = Config.bool trace_types_value;
    8.45 +val trace_types_raw = Config.declare_global "unify_trace_types" (K (Config.Bool false));
    8.46 +val trace_types = Config.bool trace_types_raw;
    8.47  
    8.48  
    8.49  type binderlist = (string*typ) list;