rc.mll 10.2 KB
Newer Older
MARCHE Claude's avatar
manager  
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
3 4 5 6 7
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
MARCHE Claude's avatar
manager  
MARCHE Claude committed
8 9 10
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
11
(*  License version 2.1, with the special exception on linking            *)
MARCHE Claude's avatar
manager  
MARCHE Claude committed
12 13 14 15 16 17 18 19 20 21 22
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

{

  open Lexing
23
  open Format
24
  open Util
MARCHE Claude's avatar
manager  
MARCHE Claude committed
25 26 27 28 29 30 31 32

  let get_home_dir () =
    try Sys.getenv "HOME"
    with Not_found -> 
      (* try windows env var *)
      try Sys.getenv "USERPROFILE"
      with Not_found -> ""

33

34

MARCHE Claude's avatar
manager  
MARCHE Claude committed
35 36 37 38 39 40 41
type rc_value =
  | RCint of int
  | RCbool of bool
  | RCfloat of float
  | RCstring of string
  | RCident of string

42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105

(* Error handling *)

(* exception SyntaxError *)
exception ExtraParameters of string
exception MissingParameters of string
(* exception UnknownSection of string *)
exception UnknownField of string
(* exception MissingSection of string *)
exception MissingField of string
exception DuplicateSection of string
exception DuplicateField of string * rc_value * rc_value
exception StringExpected of string * rc_value
exception IdentExpected of string * rc_value
exception IntExpected of string * rc_value
exception BoolExpected of string * rc_value
exception DuplicateProver of string

let error ?loc e = match loc with
  | None -> raise e
  | Some loc -> raise (Loc.Located (loc, e))

(* conf files *)

let print_rc_value fmt = function
  | RCint i -> fprintf fmt "%d" i
  | RCbool b -> fprintf fmt "%B" b
  | RCfloat f -> fprintf fmt "%f" f
  | RCstring s -> fprintf fmt "%S" s (* "%s"  %S ? *)
  | RCident s -> fprintf fmt "%s" s

let () = Exn_printer.register (fun fmt e -> match e with
  (* | SyntaxError -> *)
  (*     fprintf fmt "syntax error" *)
  | ExtraParameters s ->
      fprintf fmt "section '%s': header too long" s
  | MissingParameters s ->
      fprintf fmt "section '%s': header too short" s
  (* | UnknownSection s -> *)
  (*     fprintf fmt "unknown section '%s'" s *)
  | UnknownField s ->
      fprintf fmt "unknown field '%s'" s
  (* | MissingSection s -> *)
  (*     fprintf fmt "section '%s' is missing" s *)
  | MissingField s ->
      fprintf fmt "field '%s' is missing" s
  | DuplicateSection s ->
      fprintf fmt "section '%s' is already given" s
  | DuplicateField (s,u,v) ->
      fprintf fmt "cannot set field '%s' to %a, as it is already set to %a"
        s print_rc_value v print_rc_value u
  | StringExpected (s,v) ->
      fprintf fmt "cannot set field '%s' to %a: a string is expected"
        s print_rc_value v
  | IdentExpected (s,v) ->
      fprintf fmt "cannot set field '%s' to %a: an identifier is expected"
        s print_rc_value v
  | IntExpected (s,v) ->
      fprintf fmt "cannot set field '%s' to %a: an integer is expected"
        s print_rc_value v
  | DuplicateProver s ->
      fprintf fmt "prover %s is already listed" s
  | e -> raise e)

106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122
type section = rc_value list Mstr.t
type family  = (string * section) list
type ofamily  = (string option * section) list
type t = ofamily Mstr.t

let empty = Mstr.empty
let empty_section = Mstr.empty

let make_t tl =
  let add_key acc (key,value) =
    let l = try Mstr.find key acc with Not_found -> [] in
    Mstr.add key (value::l) acc in
  let add_section t (args,sectionl) =
    let sname,arg = match args with
      | []    -> assert false
      | [sname]    -> sname,None
      | [sname;arg] -> sname,Some arg
123
      | sname::_     -> raise (ExtraParameters sname) in
124 125 126 127 128 129 130 131 132 133 134
    let m = List.fold_left add_key empty_section sectionl in
    let m = Mstr.map List.rev m in
    let l = try Mstr.find sname t with Not_found -> [] in
    Mstr.add sname ((arg,m)::l) t in
  List.fold_left add_section empty tl

let get_section t sname =
  try
    let l = Mstr.find sname t in
    match l with
      | [None,v] -> Some v
135 136
      | [Some _,_] -> raise (ExtraParameters sname)
      | _ -> raise (DuplicateSection sname)
137 138 139 140 141 142
  with Not_found -> None

let get_family t sname =
  try
    let l = Mstr.find sname t in
    let get (arg,section) =
143
      (match arg with None -> raise (MissingParameters sname) | Some v -> v,
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160
        section) in
    List.map get l
  with Not_found -> []


let set_section t sname section =
  Mstr.add sname [None,section] t

let set_family t sname sections =
  if sections = [] then Mstr.remove sname t else
    let set (arg,section) = (Some arg,section) in
    Mstr.add sname (List.map set sections) t

let get_value read ?default section key =
  try
    let l = Mstr.find key section in
    match l with
161 162 163
      | []  -> assert false
      | [v] -> read key v
      | v1::v2::_ -> raise (DuplicateField (key,v1,v2))
164 165
  with Not_found ->
    match default with
166
      | None -> raise (MissingField key)
167 168 169 170 171
      | Some v -> v

let get_valuel read ?default section key =
  try
    let l = Mstr.find key section in
172
    List.map (read key) l
173 174
  with Not_found ->
    match default with
175
      | None -> raise (MissingField key)
176
      | Some v -> v
177

178 179 180 181 182 183 184
let set_value write section key value =
  Mstr.add key [write value] section

let set_valuel write section key valuel =
  if valuel = [] then Mstr.remove key section else
    Mstr.add key (List.map write valuel) section

185
let rint k = function
MARCHE Claude's avatar
manager  
MARCHE Claude committed
186
  | RCint n -> n
187
  | v -> raise (IntExpected (k,v))
MARCHE Claude's avatar
manager  
MARCHE Claude committed
188

189 190
let wint i = RCint i

191
let rbool k = function
MARCHE Claude's avatar
manager  
MARCHE Claude committed
192
  | RCbool b -> b
193
  | v -> raise (BoolExpected (k,v))
MARCHE Claude's avatar
manager  
MARCHE Claude committed
194

195 196
let wbool b = RCbool b

197
let rstring k = function
MARCHE Claude's avatar
manager  
MARCHE Claude committed
198
  | RCident s | RCstring s -> s
199
  | v -> raise (StringExpected (k,v))
MARCHE Claude's avatar
manager  
MARCHE Claude committed
200

201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
let wstring s = RCstring s

let get_int = get_value rint
let get_intl = get_valuel rint
let set_int = set_value wint
let set_intl = set_valuel wint

let get_bool = get_value rbool
let get_booll = get_valuel rbool
let set_bool = set_value wbool
let set_booll = set_valuel wbool

let get_string = get_value rstring
let get_stringl = get_valuel rstring
let set_string = set_value wstring
let set_stringl = set_valuel wstring

let check_exhaustive section keyl =
  let test k _ = if Sstr.mem k keyl then ()
220
    else raise (UnknownField k) in
221 222
  Mstr.iter test section

MARCHE Claude's avatar
manager  
MARCHE Claude committed
223 224
let buf = Buffer.create 17

225
let current_rec = ref []
MARCHE Claude's avatar
manager  
MARCHE Claude committed
226 227 228 229 230 231 232 233 234
let current_list = ref []
let current = ref []

let push_field key value =
  current_list := (key,value) :: !current_list

let push_record () =
  if !current_list <> [] then
    current := (!current_rec,List.rev !current_list) :: !current;
235
  current_rec := [];
MARCHE Claude's avatar
manager  
MARCHE Claude committed
236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252
  current_list := []

}

let space = [' ' '\t' '\r' '\n']+
let digit = ['0'-'9']
let letter = ['a'-'z' 'A'-'Z']
let ident = (letter | '_') (letter | digit | '_' | '-' | '(' | ')') * 
let sign = '-' | '+' 
let integer = sign? digit+
let mantissa = ['e''E'] sign? digit+
let real = sign? digit* '.' digit* mantissa?
let escape = ['\\''"''n''t''r']

rule record = parse
  | space 
      { record lexbuf }
253 254
  | '[' (ident as key) space*
      { header [key] lexbuf }
MARCHE Claude's avatar
manager  
MARCHE Claude committed
255 256 257 258 259 260 261
  | eof 
      { push_record () }
  | (ident as key) space* '=' space* 
      { value key lexbuf }
  | _ as c
      { failwith ("Rc: invalid keyval pair starting with " ^ String.make 1 c) }

262 263 264 265 266 267 268 269 270 271 272 273
and header keylist = parse
  | (ident as key) space*
      { header (key::keylist) lexbuf }
  | ']'
      { push_record ();
        current_rec := List.rev keylist;
        record lexbuf }
  | eof
      { failwith "Rc: unterminated header" }
  | _ as c
      { failwith ("Rc: invalid header starting with " ^ String.make 1 c) }

MARCHE Claude's avatar
manager  
MARCHE Claude committed
274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294
and value key = parse
  | integer as i
      { push_field key (RCint (int_of_string i));
        record lexbuf }
  | real as r
      { push_field key (RCfloat (float_of_string r));
        record lexbuf }
  | '"' 
      { Buffer.clear buf;
	string_val key lexbuf } 
  | "true"
      { push_field key (RCbool true);
        record lexbuf }
  | "false"
      { push_field key (RCbool false);
        record lexbuf }
  | ident as id
      { push_field key (RCident (*kind_of_ident*) id);
        record lexbuf }
  | eof
      { failwith "Rc: unterminated keyval pair" }
295 296
  | _ as c
      { failwith ("Rc: invalid value starting with " ^ String.make 1 c) }
MARCHE Claude's avatar
manager  
MARCHE Claude committed
297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322

and string_val key = parse 
  | '"' 
      { push_field key (RCstring (Buffer.contents buf));
	record lexbuf
      }
  | [^ '\\' '"'] as c
      { Buffer.add_char buf c;
        string_val key lexbuf }
  | '\\' (['\\''\"'] as c)   
      { Buffer.add_char buf c;
        string_val key lexbuf }
  | '\\' 'n'
      { Buffer.add_char buf '\n';
        string_val key lexbuf }
  | '\\' (_ as c)
      { Buffer.add_char buf '\\';
        Buffer.add_char buf c;
        string_val key lexbuf }
  | eof
      { failwith "Rc: unterminated string" }


{

  let from_file f =
323 324 325 326
      let c = 
	try open_in f 
	with Sys_error _ -> raise Not_found
(*
MARCHE Claude's avatar
manager  
MARCHE Claude committed
327 328
	  Format.eprintf "Cannot open file %s@." f;
	  exit 1
329 330 331 332 333 334
*)
      in
      current := [];
      let lb = from_channel c in
      record lb;
      close_in c;
335
      make_t !current
336

337
let to_file s t =
338
  let print_kv k fmt v = fprintf fmt "%s = %a" k print_rc_value v in
339 340 341 342
  let print_kvl fmt k vl = Pp.print_list Pp.newline (print_kv k) fmt vl in
  let print_section sname fmt (h,l) =
    fprintf fmt "[%s %a]@\n%a"
      sname (Pp.print_option Pp.string) h
343
      (Pp.print_iter22 Mstr.iter Pp.newline print_kvl) l in
344
  let print_sectionl fmt sname l =
345
    Pp.print_list Pp.newline2 (print_section sname) fmt l in
346 347
  let print_t fmt t =
    Pp.print_iter22 Mstr.iter Pp.newline2 print_sectionl fmt t in
348 349
  let out = open_out s in
  let fmt = formatter_of_out_channel out in
350
  print_t fmt t;
351 352 353 354 355
  pp_print_flush fmt ();
  close_out out



MARCHE Claude's avatar
manager  
MARCHE Claude committed
356
}