# HG changeset patch # User wenzelm # Date 1185566117 -7200 # Node ID 8f40e6fdb3765d17e35e693f44353157811df278 # Parent 60ac90b795be9f98b6b5420a330e51e5b713cd5d renamed config.ML to config_option.ML; diff -r 60ac90b795be -r 8f40e6fdb376 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Fri Jul 27 20:11:49 2007 +0200 +++ b/src/Pure/IsaMakefile Fri Jul 27 21:55:17 2007 +0200 @@ -63,13 +63,13 @@ Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML \ Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML \ Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML \ - compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML \ - conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML \ - install_pp.ML library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML \ - name.ML net.ML old_goals.ML pattern.ML proofterm.ML pure_setup.ML pure_thy.ML \ - search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \ - term.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML \ - variable.ML + compress.ML config_option.ML conjunction.ML consts.ML context.ML \ + context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML \ + fact_index.ML goal.ML install_pp.ML library.ML logic.ML meta_simplifier.ML \ + more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML proofterm.ML \ + pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML \ + tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML \ + type_infer.ML unify.ML variable.ML @./mk diff -r 60ac90b795be -r 8f40e6fdb376 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Jul 27 20:11:49 2007 +0200 +++ b/src/Pure/ROOT.ML Fri Jul 27 21:55:17 2007 +0200 @@ -41,7 +41,7 @@ use "Syntax/printer.ML"; use "Syntax/syntax.ML"; -use "config.ML"; +use "config_option.ML"; use "General/ml_syntax.ML"; (*core of tactical proof system*) diff -r 60ac90b795be -r 8f40e6fdb376 src/Pure/config.ML --- a/src/Pure/config.ML Fri Jul 27 20:11:49 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,134 +0,0 @@ -(* Title: Pure/config.ML - ID: $Id$ - Author: Makarius - -Configuration options as values within the local context. Global -environment of named options, with type declaration. -*) - -signature CONFIG = -sig - datatype value = Bool of bool | Int of int | String of string - type 'a T - val get: Proof.context -> 'a T -> 'a - val get_thy: theory -> 'a T -> 'a - val get_generic: Context.generic -> 'a T -> 'a - val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context - val map_thy: 'a T -> ('a -> 'a) -> theory -> theory - val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic - val put: 'a T -> 'a -> Proof.context -> Proof.context - val put_thy: 'a T -> 'a -> theory -> theory - val put_generic: 'a T -> 'a -> Context.generic -> Context.generic - val print_configs: Proof.context -> unit - val the_config: string -> value T * value - val bool: string -> bool -> bool T - val int: string -> int -> int T - val string: string -> string -> string T -end; - -structure Config: CONFIG = -struct - -(* mixed values *) - -datatype value = - Bool of bool | - Int of int | - String of string; - -fun print_value (Bool true) = "true" - | print_value (Bool false) = "false" - | print_value (Int i) = signed_string_of_int i - | print_value (String s) = quote s; - -fun print_type (Bool _) = "boolean" - | print_type (Int _) = "integer" - | print_type (String _) = "string"; - -fun same_type (Bool _) (Bool _) = true - | same_type (Int _) (Int _) = true - | same_type (String _) (String _) = true - | same_type _ _ = false; - -fun type_check f value = - let - val value' = f value; - val _ = same_type value value' orelse - error ("Ill-typed configuration option: " ^ print_type value ^ - " expected,\nbut " ^ print_type value' ^ " was found"); - in value' end; - -structure ConfigData = GenericDataFun -( - type T = value Inttab.table; - val empty = Inttab.empty; - val extend = I; - fun merge _ = Inttab.merge (K true); -); - - -(* abstract configuration options *) - -datatype 'a T = Config of - {get_value: Context.generic -> 'a, - map_value: ('a -> 'a) -> Context.generic -> Context.generic}; - -fun get_generic context (Config {get_value, ...}) = get_value context; -fun get_ctxt ctxt = get_generic (Context.Proof ctxt); -fun get_thy thy = get_generic (Context.Theory thy); - -fun map_generic (Config {map_value, ...}) f context = map_value f context; -fun map_ctxt config f = Context.proof_map (map_generic config f); -fun map_thy config f = Context.theory_map (map_generic config f); - -fun put_generic config value = map_generic config (K value); -fun put_ctxt config value = map_ctxt config (K value); -fun put_thy config value = map_thy config (K value); - - -(* global declarations *) - -local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in - -fun print_configs ctxt = - let - fun prt (name, (config, default)) = - Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1, - Pretty.str (print_value (get_ctxt ctxt config))]; - val configs = sort_wrt #1 (Symtab.dest (! global_configs)); - in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; - -fun the_config name = - (case Symtab.lookup (! global_configs) name of SOME cfg => cfg - | NONE => error ("Unknown configuration option " ^ quote name)); - -fun declare make dest name default = - let - val id = serial (); - - val default_value = make default; - fun get_value context = - the_default default_value (Inttab.lookup (ConfigData.get context) id); - fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) (type_check f)); - val config_value = Config {get_value = get_value, map_value = map_value}; - - val _ = CRITICAL (fn () => - (if Symtab.defined (! global_configs) name - then warning ("Hiding existing configuration option " ^ quote name) else (); - change global_configs (Symtab.update (name, (config_value, default_value))))); - - in Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} end; - -end; - -val bool = declare Bool (fn Bool b => b); -val int = declare Int (fn Int i => i); -val string = declare String (fn String s => s); - - -(*final declarations of this structure!*) -val get = get_ctxt; -val map = map_ctxt; -val put = put_ctxt; - -end; diff -r 60ac90b795be -r 8f40e6fdb376 src/Pure/config_option.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/config_option.ML Fri Jul 27 21:55:17 2007 +0200 @@ -0,0 +1,136 @@ +(* Title: Pure/config_option.ML + ID: $Id$ + Author: Makarius + +Configuration options as values within the local context. Global +environment of named options, with type declaration. +*) + +signature CONFIG_OPTION = +sig + datatype value = Bool of bool | Int of int | String of string + type 'a T + val get: Proof.context -> 'a T -> 'a + val get_thy: theory -> 'a T -> 'a + val get_generic: Context.generic -> 'a T -> 'a + val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context + val map_thy: 'a T -> ('a -> 'a) -> theory -> theory + val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic + val put: 'a T -> 'a -> Proof.context -> Proof.context + val put_thy: 'a T -> 'a -> theory -> theory + val put_generic: 'a T -> 'a -> Context.generic -> Context.generic + val print_options: Proof.context -> unit + val the_option: string -> value T * value + val bool: string -> bool -> bool T + val int: string -> int -> int T + val string: string -> string -> string T +end; + +structure ConfigOption: CONFIG_OPTION = +struct + +(* mixed values *) + +datatype value = + Bool of bool | + Int of int | + String of string; + +fun print_value (Bool true) = "true" + | print_value (Bool false) = "false" + | print_value (Int i) = signed_string_of_int i + | print_value (String s) = quote s; + +fun print_type (Bool _) = "boolean" + | print_type (Int _) = "integer" + | print_type (String _) = "string"; + +fun same_type (Bool _) (Bool _) = true + | same_type (Int _) (Int _) = true + | same_type (String _) (String _) = true + | same_type _ _ = false; + +fun type_check f value = + let + val value' = f value; + val _ = same_type value value' orelse + error ("Ill-typed configuration option: " ^ print_type value ^ + " expected,\nbut " ^ print_type value' ^ " was found"); + in value' end; + +structure ConfigOptionData = GenericDataFun +( + type T = value Inttab.table; + val empty = Inttab.empty; + val extend = I; + fun merge _ = Inttab.merge (K true); +); + + +(* abstract configuration options *) + +datatype 'a T = ConfigOption of + {get_value: Context.generic -> 'a, + map_value: ('a -> 'a) -> Context.generic -> Context.generic}; + +fun get_generic context (ConfigOption {get_value, ...}) = get_value context; +fun get_ctxt ctxt = get_generic (Context.Proof ctxt); +fun get_thy thy = get_generic (Context.Theory thy); + +fun map_generic (ConfigOption {map_value, ...}) f context = map_value f context; +fun map_ctxt config f = Context.proof_map (map_generic config f); +fun map_thy config f = Context.theory_map (map_generic config f); + +fun put_generic config value = map_generic config (K value); +fun put_ctxt config value = map_ctxt config (K value); +fun put_thy config value = map_thy config (K value); + + +(* global declarations *) + +local val global_configs = ref (Symtab.empty: (value T * value) Symtab.table) in + +fun print_options ctxt = + let + fun prt (name, (config, default)) = + Pretty.block [Pretty.str (name ^ ": " ^ print_type default ^ " ="), Pretty.brk 1, + Pretty.str (print_value (get_ctxt ctxt config))]; + val configs = sort_wrt #1 (Symtab.dest (! global_configs)); + in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end; + +fun the_option name = + (case Symtab.lookup (! global_configs) name of SOME cfg => cfg + | NONE => error ("Unknown configuration option " ^ quote name)); + +fun declare make dest name default = + let + val id = serial (); + + val default_value = make default; + fun get_value context = + the_default default_value (Inttab.lookup (ConfigOptionData.get context) id); + fun map_value f = ConfigOptionData.map (Inttab.map_default (id, default_value) (type_check f)); + val config_value = ConfigOption {get_value = get_value, map_value = map_value}; + + val _ = CRITICAL (fn () => + (if Symtab.defined (! global_configs) name + then warning ("Hiding existing configuration option " ^ quote name) else (); + change global_configs (Symtab.update (name, (config_value, default_value))))); + + in + ConfigOption {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)} + end; + +end; + +val bool = declare Bool (fn Bool b => b); +val int = declare Int (fn Int i => i); +val string = declare String (fn String s => s); + + +(*final declarations of this structure!*) +val get = get_ctxt; +val map = map_ctxt; +val put = put_ctxt; + +end;