src/Pure/config.ML
author wenzelm
Tue Aug 28 11:22:04 2018 +0200 (10 months ago)
changeset 68827 1286ca9dfd26
parent 63806 c54a53ef1873
child 69574 b4ea943ce0b7
permissions -rw-r--r--
tuned signature;
     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 restore: 'a T -> Proof.context -> Proof.context -> Proof.context
    22   val get_global: theory -> 'a T -> 'a
    23   val map_global: 'a T -> ('a -> 'a) -> theory -> theory
    24   val put_global: 'a T -> 'a -> theory -> theory
    25   val restore_global: 'a T -> theory -> theory -> theory
    26   val get_generic: Context.generic -> 'a T -> 'a
    27   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    28   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    29   val restore_generic: 'a T -> Context.generic -> Context.generic -> Context.generic
    30   val declare: string * Position.T -> (Context.generic -> value) -> raw
    31   val declare_option: string * Position.T -> raw
    32   val name_of: 'a T -> string
    33   val pos_of: 'a T -> Position.T
    34 end;
    35 
    36 structure Config: CONFIG =
    37 struct
    38 
    39 (* simple values *)
    40 
    41 datatype value =
    42   Bool of bool |
    43   Int of int |
    44   Real of real |
    45   String of string;
    46 
    47 fun print_value (Bool true) = "true"
    48   | print_value (Bool false) = "false"
    49   | print_value (Int i) = signed_string_of_int i
    50   | print_value (Real x) = Value.print_real x
    51   | print_value (String s) = quote s;
    52 
    53 fun print_type (Bool _) = "bool"
    54   | print_type (Int _) = "int"
    55   | print_type (Real _) = "real"
    56   | print_type (String _) = "string";
    57 
    58 fun same_type (Bool _) (Bool _) = true
    59   | same_type (Int _) (Int _) = true
    60   | same_type (Real _) (Real _) = true
    61   | same_type (String _) (String _) = true
    62   | same_type _ _ = false;
    63 
    64 fun type_check (name, pos) f value =
    65   let
    66     val value' = f value;
    67     val _ = same_type value value' orelse
    68       error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^
    69         print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found");
    70   in value' end;
    71 
    72 
    73 (* abstract configuration options *)
    74 
    75 datatype 'a T = Config of
    76  {name: string,
    77   pos: Position.T,
    78   get_value: Context.generic -> 'a,
    79   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    80 
    81 type raw = value T;
    82 
    83 fun coerce make dest (Config {name, pos, get_value, map_value}) = Config
    84  {name = name,
    85   pos = pos,
    86   get_value = dest o get_value,
    87   map_value = fn f => map_value (make o f o dest)};
    88 
    89 val bool = coerce Bool (fn Bool b => b);
    90 val int = coerce Int (fn Int i => i);
    91 val real = coerce Real (fn Real x => x);
    92 val string = coerce String (fn String s => s);
    93 
    94 fun get_generic context (Config {get_value, ...}) = get_value context;
    95 fun map_generic (Config {map_value, ...}) f context = map_value f context;
    96 fun put_generic config value = map_generic config (K value);
    97 fun restore_generic config context = put_generic config (get_generic context config);
    98 
    99 fun get_ctxt ctxt = get_generic (Context.Proof ctxt);
   100 fun map_ctxt config f = Context.proof_map (map_generic config f);
   101 fun put_ctxt config value = map_ctxt config (K value);
   102 fun restore_ctxt config ctxt = put_ctxt config (get_ctxt ctxt config);
   103 
   104 fun get_global thy = get_generic (Context.Theory thy);
   105 fun map_global config f = Context.theory_map (map_generic config f);
   106 fun put_global config value = map_global config (K value);
   107 fun restore_global config thy = put_global config (get_global thy config);
   108 
   109 
   110 (* context information *)
   111 
   112 structure Data = Generic_Data
   113 (
   114   type T = value Inttab.table;
   115   val empty = Inttab.empty;
   116   val extend = I;
   117   fun merge data = Inttab.merge (K true) data;
   118 );
   119 
   120 fun declare (name, pos) default =
   121   let
   122     val id = serial ();
   123 
   124     fun get_value context =
   125       (case Inttab.lookup (Data.get context) id of
   126         SOME value => value
   127       | NONE => default context);
   128 
   129     fun map_value f context =
   130       Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context;
   131   in
   132     Config {name = name, pos = pos, get_value = get_value, map_value = map_value}
   133   end;
   134 
   135 fun declare_option (name, pos) =
   136   let
   137     val typ = Options.default_typ name;
   138     val default =
   139       if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
   140       else if typ = Options.intT then fn _ => Int (Options.default_int name)
   141       else if typ = Options.realT then fn _ => Real (Options.default_real name)
   142       else if typ = Options.stringT then fn _ => String (Options.default_string name)
   143       else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ);
   144   in declare (name, pos) default end;
   145 
   146 fun name_of (Config {name, ...}) = name;
   147 fun pos_of (Config {pos, ...}) = pos;
   148 
   149 
   150 (*final declarations of this structure!*)
   151 val get = get_ctxt;
   152 val map = map_ctxt;
   153 val put = put_ctxt;
   154 val restore = restore_ctxt;
   155 
   156 end;