1(* Title: Pure/config.ML 2 Author: Makarius 3 4Configuration options as values within the local context. 5*) 6 7signature CONFIG = 8sig 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 val name_of: 'a T -> string 14 val pos_of: 'a T -> Position.T 15 val apply: 'a T -> Proof.context -> 'a 16 val get: Proof.context -> 'a T -> 'a 17 val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context 18 val put: 'a T -> 'a -> Proof.context -> Proof.context 19 val restore: 'a T -> Proof.context -> Proof.context -> Proof.context 20 val apply_global: 'a T -> theory -> 'a 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 restore_global: 'a T -> theory -> theory -> theory 25 val apply_generic: 'a T -> Context.generic -> 'a 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 bool: value T -> bool T 31 val bool_value: bool T -> value T 32 val int: value T -> int T 33 val int_value: int T -> value T 34 val real: value T -> real T 35 val real_value: real T -> value T 36 val string: value T -> string T 37 val string_value: string T -> value T 38 val declare: string * Position.T -> (Context.generic -> value) -> value T 39 val declare_bool: string * Position.T -> (Context.generic -> bool) -> bool T 40 val declare_int: string * Position.T -> (Context.generic -> int) -> int T 41 val declare_real: string * Position.T -> (Context.generic -> real) -> real T 42 val declare_string: string * Position.T -> (Context.generic -> string) -> string T 43 val declare_option: string * Position.T -> value T 44 val declare_option_bool: string * Position.T -> bool T 45 val declare_option_int: string * Position.T -> int T 46 val declare_option_real: string * Position.T -> real T 47 val declare_option_string: string * Position.T -> string T 48end; 49 50structure Config: CONFIG = 51struct 52 53(* simple values *) 54 55datatype value = 56 Bool of bool | 57 Int of int | 58 Real of real | 59 String of string; 60 61fun print_value (Bool true) = "true" 62 | print_value (Bool false) = "false" 63 | print_value (Int i) = Value.print_int i 64 | print_value (Real x) = Value.print_real x 65 | print_value (String s) = quote s; 66 67fun print_type (Bool _) = "bool" 68 | print_type (Int _) = "int" 69 | print_type (Real _) = "real" 70 | print_type (String _) = "string"; 71 72fun same_type (Bool _) (Bool _) = true 73 | same_type (Int _) (Int _) = true 74 | same_type (Real _) (Real _) = true 75 | same_type (String _) (String _) = true 76 | same_type _ _ = false; 77 78fun type_check (name, pos) f value = 79 let 80 val value' = f value; 81 val _ = same_type value value' orelse 82 error ("Ill-typed configuration option " ^ quote name ^ Position.here pos ^ ": " ^ 83 print_type value ^ " expected,\nbut " ^ print_type value' ^ " was found"); 84 in value' end; 85 86 87(* abstract configuration options *) 88 89datatype 'a T = Config of 90 {name: string, 91 pos: Position.T, 92 get_value: Context.generic -> 'a, 93 map_value: ('a -> 'a) -> Context.generic -> Context.generic}; 94 95fun name_of (Config {name, ...}) = name; 96fun pos_of (Config {pos, ...}) = pos; 97 98fun apply_generic (Config {get_value, ...}) = get_value; 99fun get_generic context config = apply_generic config context; 100fun map_generic (Config {map_value, ...}) f context = map_value f context; 101fun put_generic config value = map_generic config (K value); 102fun restore_generic config = put_generic config o apply_generic config; 103 104fun apply_ctxt config = apply_generic config o Context.Proof; 105fun get_ctxt ctxt = get_generic (Context.Proof ctxt); 106fun map_ctxt config f = Context.proof_map (map_generic config f); 107fun put_ctxt config value = map_ctxt config (K value); 108fun restore_ctxt config = put_ctxt config o apply_ctxt config; 109 110fun apply_global config = apply_generic config o Context.Theory; 111fun get_global thy = get_generic (Context.Theory thy); 112fun map_global config f = Context.theory_map (map_generic config f); 113fun put_global config value = map_global config (K value); 114fun restore_global config = put_global config o apply_global config; 115 116 117(* coerce type *) 118 119fun coerce make dest (Config {name, pos, get_value, map_value}) = Config 120 {name = name, 121 pos = pos, 122 get_value = dest o get_value, 123 map_value = fn f => map_value (make o f o dest)}; 124 125fun coerce_pair make dest = (coerce make dest, coerce dest make); 126 127val (bool, bool_value) = coerce_pair Bool (fn Bool b => b); 128val (int, int_value) = coerce_pair Int (fn Int i => i); 129val (real, real_value) = coerce_pair Real (fn Real x => x); 130val (string, string_value) = coerce_pair String (fn String s => s); 131 132 133(* context data *) 134 135structure Data = Generic_Data 136( 137 type T = value Inttab.table; 138 val empty = Inttab.empty; 139 val extend = I; 140 fun merge data = Inttab.merge (K true) data; 141); 142 143fun declare (name, pos) default = 144 let 145 val id = serial (); 146 147 fun get_value context = 148 (case Inttab.lookup (Data.get context) id of 149 SOME value => value 150 | NONE => default context); 151 152 fun map_value f context = 153 Data.map (Inttab.update (id, type_check (name, pos) f (get_value context))) context; 154 in 155 Config {name = name, pos = pos, get_value = get_value, map_value = map_value} 156 end; 157 158fun declare_bool name default = bool (declare name (Bool o default)); 159fun declare_int name default = int (declare name (Int o default)); 160fun declare_real name default = real (declare name (Real o default)); 161fun declare_string name default = string (declare name (String o default)); 162 163 164(* system options *) 165 166fun declare_option (name, pos) = 167 let 168 val typ = Options.default_typ name; 169 val default = 170 if typ = Options.boolT then fn _ => Bool (Options.default_bool name) 171 else if typ = Options.intT then fn _ => Int (Options.default_int name) 172 else if typ = Options.realT then fn _ => Real (Options.default_real name) 173 else if typ = Options.stringT then fn _ => String (Options.default_string name) 174 else error ("Unknown type for option " ^ quote name ^ Position.here pos ^ " : " ^ quote typ); 175 in declare (name, pos) default end; 176 177val declare_option_bool = bool o declare_option; 178val declare_option_int = int o declare_option; 179val declare_option_real = real o declare_option; 180val declare_option_string = string o declare_option; 181 182(*final declarations of this structure!*) 183val apply = apply_ctxt; 184val get = get_ctxt; 185val map = map_ctxt; 186val put = put_ctxt; 187val restore = restore_ctxt; 188 189end; 190