driver.ml 12 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  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.                  *)
(*                                                                        *)
(**************************************************************************)

21
open Format
Andrei Paskevich's avatar
Andrei Paskevich committed
22 23
open Util
open Ident
24 25
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
26
open Decl
27
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
28
open Task
29 30
open Printer
open Trans
31
open Driver_ast
32
open Call_provers
33

34
(** drivers *)
35

36
type driver = {
37 38 39 40 41 42 43 44 45
  drv_env         : Env.env;
  drv_printer     : string option;
  drv_filename    : string option;
  drv_transform   : string list;
  drv_prelude     : prelude;
  drv_thprelude   : prelude_map;
  drv_meta        : (theory * Stdecl.t) Mid.t;
  drv_meta_cl     : (theory * Stdecl.t) Mid.t;
  drv_regexps     : (Str.regexp * prover_answer) list;
46
  drv_timeregexps : Call_provers.timeregexp list;
47
  drv_exitcodes   : (int * prover_answer) list;
48
  drv_tag         : int
49
}
50

51 52
(** parse a driver file *)

53
let load_plugin dir (byte,nat) =
Andrei Paskevich's avatar
Andrei Paskevich committed
54
  let file = if Dynlink.is_native then nat else byte in
55
  let file = Filename.concat dir file in
Andrei Paskevich's avatar
Andrei Paskevich committed
56
  Dynlink.loadfile_private file
57

58
let load_file file =
59
  let basename = Filename.dirname file in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
60 61 62
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
63 64 65 66 67 68 69 70 71 72 73 74
  let to_close = Stack.create () in
  Stack.push c to_close;
  let input_lexer s =
    let filename = Sysutil.absolutize_filename basename s in
    let c = open_in filename in
    Stack.push c to_close;
    let lb = Lexing.from_channel c in
    Loc.set_file filename lb;
    lb
  in
  let f = Driver_lexer.parse_file input_lexer lb in
  Stack.iter close_in to_close;
75
  f
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76

77 78 79 80
exception Duplicate    of string
exception UnknownType  of (string list * string list)
exception UnknownLogic of (string list * string list)
exception UnknownProp  of (string list * string list)
81 82
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
83

84
let load_driver = let driver_tag = ref (-1) in fun env file extra_files ->
85 86 87 88 89
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
90
  let transform = ref [] in
91
  let timeregexps = ref [] in
92

93
  let set_or_raise loc r v error = match !r with
94
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
95 96 97
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
98
  let add_global (loc, g) = match g with
99 100 101 102 103 104
    | Prelude s -> add_to_list prelude s
    | RegexpValid s -> add_to_list regexps (Str.regexp s, Valid)
    | RegexpInvalid s -> add_to_list regexps (Str.regexp s, Invalid)
    | RegexpTimeout s -> add_to_list regexps (Str.regexp s, Timeout)
    | RegexpUnknown (s,t) -> add_to_list regexps (Str.regexp s, Unknown t)
    | RegexpFailure (s,t) -> add_to_list regexps (Str.regexp s, Failure t)
105
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
106 107 108 109 110
    | ExitCodeValid s -> add_to_list exitcodes (s, Valid)
    | ExitCodeInvalid s -> add_to_list exitcodes (s, Invalid)
    | ExitCodeTimeout s -> add_to_list exitcodes (s, Timeout)
    | ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
    | ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
111
    | Filename s -> set_or_raise loc filename s "filename"
112 113
    | Printer s -> set_or_raise loc printer s "printer"
    | Transform s -> add_to_list transform s
114
    | Plugin files -> load_plugin (Filename.dirname file) files
115
  in
116
  let f = load_file file in
117 118 119
  List.iter add_global f.f_global;

  let thprelude = ref Mid.empty in
120 121
  let meta      = ref Mid.empty in
  let meta_cl   = ref Mid.empty in
122 123
  let qualid    = ref [] in

124 125
  let find_pr th (loc,q) = try ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
126
  in
127 128
  let find_ls th (loc,q) = try ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
129
  in
130 131
  let find_ts th (loc,q) = try ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
132
  in
133 134 135 136 137 138
  let find_fs th q =
    let ls = find_ls th q in
    if ls.ls_value = None then raise (FSymExpected ls) else ls in
  let find_ps th q =
    let ls = find_ls th q in
    if ls.ls_value <> None then raise (PSymExpected ls) else ls in
139
  let add_meta th td m =
140 141
    let s = try snd (Mid.find th.th_name !m) with Not_found -> Stdecl.empty in
    m := Mid.add th.th_name (th, Stdecl.add td s) !m
142
  in
143
  let add_local th = function
144
    | Rprelude s ->
145
        let l = Mid.find_def [] th.th_name !thprelude in
146
        thprelude := Mid.add th.th_name (s::l) !thprelude
147 148 149
    | Rsyntaxts (c,q,s) ->
        let td = syntax_type (find_ts th q) s in
        add_meta th td (if c then meta_cl else meta)
150 151 152 153 154
    | Rsyntaxfs (c,q,s) ->
        let td = syntax_logic (find_fs th q) s in
        add_meta th td (if c then meta_cl else meta)
    | Rsyntaxps (c,q,s) ->
        let td = syntax_logic (find_ps th q) s in
155
        add_meta th td (if c then meta_cl else meta)
156
    | Rremovepr (c,q) ->
157 158
        let td = remove_prop (find_pr th q) in
        add_meta th td (if c then meta_cl else meta)
159 160 161
    | Rmeta (c,s,al) ->
        let convert = function
          | PMAts q  -> MAts (find_ts th q)
162 163
          | PMAfs q  -> MAls (find_fs th q)
          | PMAps q  -> MAls (find_ps th q)
164 165 166 167
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
168 169
        let m = lookup_meta s in
        let td = create_meta m (List.map convert al) in
170
        add_meta th td (if c then meta_cl else meta)
171
  in
172 173
  let add_local th (loc,rule) =
    try add_local th rule with e -> raise (Loc.Located (loc,e))
174 175 176
  in
  let add_theory { thr_name = (loc,q); thr_rules = trl } =
    let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
177
    let th =
178 179
      try Env.read_theory ~format:"why" env f id
      with e -> raise (Loc.Located (loc,e))
180 181 182 183 184
    in
    qualid := q;
    List.iter (add_local th) trl
  in
  List.iter add_theory f.f_rules;
185
  List.iter (fun f -> List.iter add_theory (load_file f).f_rules) extra_files;
186
  incr driver_tag;
187
  {
188 189
    drv_env         = env;
    drv_printer     = !printer;
190
    drv_prelude     = List.rev !prelude;
191
    drv_filename    = !filename;
192 193
    drv_transform   = List.rev !transform;
    drv_thprelude   = Mid.map List.rev !thprelude;
194 195 196
    drv_meta        = !meta;
    drv_meta_cl     = !meta_cl;
    drv_regexps     = List.rev !regexps;
197
    drv_timeregexps = List.rev !timeregexps;
198
    drv_exitcodes   = List.rev !exitcodes;
199
    drv_tag         = !driver_tag
200
  }
201

202
(** apply drivers *)
203

204
exception UnknownSpec of string
205

206 207 208
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
209 210
  let sanitize = Ident.sanitizer
    Ident.char_to_alnumus Ident.char_to_alnumus in
211 212 213 214
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
215
  let replace s = match Str.matched_group 1 s with
216
    | "%" -> "%"
217 218 219
    | "f" -> sanitize input_file
    | "t" -> sanitize theory_name
    | "g" -> sanitize goal_name
220
    | s   -> raise (UnknownSpec s)
221
  in
222
  Str.global_substitute filename_regexp replace file
223

224
let file_of_task drv input_file theory_name task =
225
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
226

227 228 229
let file_of_theory drv input_file th =
  get_filename drv input_file th.th_name.Ident.id_string "null"

230
let call_on_buffer ~command ?timelimit ?memlimit ~filename drv buffer =
231
  let regexps = drv.drv_regexps in
232
  let timeregexps = drv.drv_timeregexps in
233 234
  let exitcodes = drv.drv_exitcodes in
  Call_provers.call_on_buffer
235
    ~command ?timelimit ?memlimit ~regexps ~timeregexps
236
    ~exitcodes ~filename buffer
237

238 239 240 241
(** print'n'prove *)

exception NoPrinter

242 243 244 245
let update_task drv task =
  let task, goal = match task with
    | Some { task_decl = g ; task_prev = t } -> t,g
    | None -> raise Task.GoalNotFound
246 247 248
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
249 250 251 252 253
      if Task.on_used_theory th task then
        Stdecl.fold (fun tdm task ->
          add_tdecl task tdm
        ) s task
      else task
254 255 256 257
    ) drv.drv_meta task
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
258
      Task.on_theory th (fun task sm ->
259
        Stdecl.fold (fun tdm task ->
260
          add_tdecl task (clone_meta tdm sm)
261
        ) s task
262
      ) task task
263 264
    ) drv.drv_meta_cl task
  in
265 266
  add_tdecl task goal

267 268 269 270 271 272 273 274 275 276 277
let update_task =
  let h = Hashtbl.create 5 in
  fun drv ->
    let update = try Hashtbl.find h drv.drv_tag with
      | Not_found ->
          let upd = Trans.store (update_task drv) in
          Hashtbl.add h drv.drv_tag upd;
          upd
    in
    Trans.apply update

278
let prepare_task drv task =
279
  let lookup_transform t = lookup_transform t drv.drv_env in
280
  let transl = List.map lookup_transform drv.drv_transform in
281
  let apply task tr = Trans.apply tr task in
282
  let task = update_task drv task in
283
  List.fold_left apply task transl
284

285
let print_task_prepared ?old drv fmt task =
286 287 288 289 290 291 292
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
  let printer =
    lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
  in
293
  fprintf fmt "@[%a@]@?" (printer ?old) task
294

295
let print_task ?old drv fmt task =
296
  let task = prepare_task drv task in
297
  print_task_prepared ?old drv fmt task
298

299 300
let print_theory ?old drv fmt th =
  let task = Task.use_export None th in
301
  print_task ?old drv fmt task
302

303
let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
304 305
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
306
  print_task_prepared ?old drv fmt task; pp_print_flush fmt ();
307 308 309 310 311 312 313 314 315
  let filename =
    let pr = Task.task_goal task in
    let fn = match pr.pr_name.id_loc with
      | Some loc -> let fn,_,_,_ = Loc.get loc in Filename.basename fn
      | None -> "" in
    let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
    get_filename drv fn "T" pr.pr_name.id_string
  in
  let res = call_on_buffer ~command ?timelimit ?memlimit ~filename drv buf in
316 317
  Buffer.reset buf;
  res
318

319 320 321 322
let prove_task ~command ?timelimit ?memlimit ?old drv task =
  let task = prepare_task drv task in
  prove_task_prepared ~command ?timelimit ?memlimit ?old drv task

323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340
(* exception report *)

let string_of_qualid thl idl =
  String.concat "." thl ^ "." ^ String.concat "." idl

let () = Exn_printer.register (fun fmt exn -> match exn with
  | NoPrinter -> Format.fprintf fmt
      "No printer specified in the driver file"
  | Duplicate s -> Format.fprintf fmt
      "Duplicate %s specification" s
  | UnknownType (thl,idl) -> Format.fprintf fmt
      "Unknown type symbol %s" (string_of_qualid thl idl)
  | UnknownLogic (thl,idl) -> Format.fprintf fmt
      "Unknown logical symbol %s" (string_of_qualid thl idl)
  | UnknownProp (thl,idl) -> Format.fprintf fmt
      "Unknown proposition %s" (string_of_qualid thl idl)
  | UnknownSpec s -> Format.fprintf fmt
      "Unknown format specifier '%%%s', use %%f, %%t or %%g" s
341 342 343 344
  | FSymExpected ls -> Format.fprintf fmt
      "%a is not a function symbol" Pretty.print_ls ls
  | PSymExpected ls -> Format.fprintf fmt
      "%a is not a predicate symbol" Pretty.print_ls ls
345 346
  | e -> raise e)