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