src/Pure/config.ML
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 56438 7f6b2634d853
child 57858 39d9c7f175e0
permissions -rw-r--r--
use E 1.8's auto scheduler option
     1 (*  Title:      Pure/config.ML
     2     Author:     Makarius
     3 
     4 Configuration options as values within the local context.
     5 *)
     6 
     7 signature CONFIG =
     8 sig
     9   datatype value = Bool of bool | Int of int | Real of real | String of string
    10   val print_value: value -> string
    11   val print_type: value -> string
    12   type 'a T
    13   type raw = value T
    14   val bool: raw -> bool T
    15   val int: raw -> int T
    16   val real: raw -> real T
    17   val string: raw -> string T
    18   val get: Proof.context -> 'a T -> 'a
    19   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    20   val put: 'a T -> 'a -> Proof.context -> Proof.context
    21   val get_global: theory -> 'a T -> 'a
    22   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
    23   val put_global: 'a T -> 'a -> theory -> theory
    24   val get_generic: Context.generic -> 'a T -> 'a
    25   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    26   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    27   val declare: string * Position.T -> (Context.generic -> value) -> raw
    28   val declare_global: string * Position.T -> (Context.generic -> value) -> raw
    29   val declare_option: string * Position.T -> raw
    30   val declare_option_global: string * Position.T -> raw
    31   val name_of: 'a T -> string
    32   val pos_of: 'a T -> Position.T
    33 end;
    34 
    35 structure Config: CONFIG =
    36 struct
    37 
    38 (* simple values *)
    39 
    40 datatype value =
    41   Bool of bool |
    42   Int of int |
    43   Real of real |
    44   String of string;
    45 
    46 fun print_value (Bool true) = "true"
    47   | print_value (Bool false) = "false"
    48   | print_value (Int i) = signed_string_of_int i
    49   | print_value (Real x) = Markup.print_real x
    50   | print_value (String s) = quote s;
    51 
    52 fun print_type (Bool _) = "bool"
    53   | print_type (Int _) = "int"
    54   | print_type (Real _) = "real"
    55   | print_type (String _) = "string";
    56 
    57 fun same_type (Bool _) (Bool _) = true
    58   | same_type (Int _) (Int _) = true
    59   | same_type (Real _) (Real _) = true
    60   | same_type (String _) (String _) = true
    61   | same_type _ _ = false;
    62 
    63 fun type_check (name, pos) f value =
    64   let
    65     val value' = f value;
    66     val _ = same_type value value' orelse
    67       error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
    68         print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
    69   in value' end;
    70 
    71 
    72 (* abstract configuration options *)
    73 
    74 datatype 'a T = Config of
    75  {name: string,
    76   pos: Position.T,
    77   get_value: Context.generic -> 'a,
    78   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    79 
    80 type raw = value T;
    81 
    82 fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
    83  {name = name,
    84   pos = pos,
    85   get_value = dest o get_value,
    86   map_value = fn f => map_value (make o f o dest)};
    87 
    88 val bool = coerce Bool (fn Bool b => b);
    89 val int = coerce Int (fn Int i => i);
    90 val real = coerce Real (fn Real x => x);
    91 val string = coerce String (fn String s => s);
    92 
    93 fun get_generic context (Config {get_value, ...}) = get_value context;
    94 fun map_generic (Config {map_value, ...}) f context = map_value f context;
    95 fun put_generic config value = map_generic config (K value);
    96 
    97 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
    98 fun map_ctxt config f = Context.proof_map (map_generic config f);
    99 fun put_ctxt config value = map_ctxt config (K value);
   100 
   101 fun get_global thy = get_generic (Context.Theory thy);
   102 fun map_global config f = Context.theory_map (map_generic config f);
   103 fun put_global config value = map_global config (K value);
   104 
   105 
   106 (* context information *)
   107 
   108 structure Value = Generic_Data
   109 (
   110   type T = value Inttab.table;
   111   val empty = Inttab.empty;
   112   val extend = I;
   113   fun merge data = Inttab.merge (K true) data;
   114 );
   115 
   116 local
   117 
   118 fun declare_generic global (name, pos) default =
   119   let
   120     val id = serial ();
   121 
   122     fun get_value context =
   123       (case Inttab.lookup (Value.get context) id of
   124         SOME value => value
   125       | NONE => default context);
   126 
   127     fun update_value f context =
   128       Value.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
   129 
   130     fun map_value f (context as Context.Proof ctxt) =
   131           let val context' = update_value f context in
   132             if global andalso
   133               Context_Position.is_visible ctxt andalso
   134               print_value (get_value (Context.Theory (Context.theory_of context'))) <>
   135                 print_value (get_value context')
   136             then
   137              (if Context_Position.is_visible ctxt then
   138                 warning ("Ignoring local change of global option " ^ quote name)
   139               else (); context)
   140             else context'
   141           end
   142       | map_value f context = update_value f context;
   143   in Config {name = name, pos = pos, get_value = get_value, map_value = map_value} end;
   144 
   145 fun declare_option_generic global (name, pos) =
   146   let
   147     val typ = Options.default_typ name;
   148     val default =
   149       if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
   150       else if typ = Options.intT then fn _ => Int (Options.default_int name)
   151       else if typ = Options.realT then fn _ => Real (Options.default_real name)
   152       else if typ = Options.stringT then fn _ => String (Options.default_string name)
   153       else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
   154   in declare_generic global (name, pos) default end;
   155 
   156 in
   157 
   158 val declare = declare_generic false;
   159 val declare_global = declare_generic true;
   160 val declare_option = declare_option_generic false;
   161 val declare_option_global = declare_option_generic true;
   162 
   163 end;
   164 
   165 fun name_of (Config {name, ...}) = name;
   166 fun pos_of (Config {pos, ...}) = pos;
   167 
   168 
   169 (*final declarations of this structure!*)
   170 val get = get_ctxt;
   171 val map = map_ctxt;
   172 val put = put_ctxt;
   173 
   174 end;