driver.ml 9.87 KB
Newer Older
1 2 3
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
MARCHE Claude's avatar
MARCHE Claude committed
4 5 6
(*    François Bobot                                                     *)
(*    Jean-Christophe Filliâtre                                          *)
(*    Claude Marché                                                      *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Format
Andrei Paskevich's avatar
Andrei Paskevich committed
21 22
open Util
open Ident
23 24
open Ty
open Term
Andrei Paskevich's avatar
Andrei Paskevich committed
25
open Decl
26
open Theory
Andrei Paskevich's avatar
Andrei Paskevich committed
27
open Task
28 29
open Printer
open Trans
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
open Driver_ast
31
open Call_provers
32

33
(** drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
34

35
type driver = {
36 37 38 39 40 41 42 43 44
  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;
45
  drv_timeregexps : Call_provers.timeregexp list;
46
  drv_exitcodes   : (int * prover_answer) list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
47
}
48

49 50
(** parse a driver file *)

51 52
exception NoPlugins

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
59
let load_file file =
Jean-Christophe Filliâtre's avatar
drivers  
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
  let f = Driver_lexer.parse_file lb in
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
64
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
65
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
66

67 68 69 70
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)
71

72
let load_driver = let driver_tag = ref (-1) in fun env file ->
73 74 75 76 77
  let prelude   = ref [] in
  let regexps   = ref [] in
  let exitcodes = ref [] in
  let filename  = ref None in
  let printer   = ref None in
78
  let transform = ref [] in
79
  let timeregexps = ref [] in
80

81
  let set_or_raise loc r v error = match !r with
82
    | Some _ -> raise (Loc.Located (loc, Duplicate error))
83 84 85
    | None   -> r := Some v
  in
  let add_to_list r v = (r := v :: !r) in
86
  let add_global (loc, g) = match g with
87 88 89 90 91 92
    | 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)
93
    | TimeRegexp r -> add_to_list timeregexps (Call_provers.timeregexp r)
94 95 96 97 98
    | 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)
99
    | Filename s -> set_or_raise loc filename s "filename"
100 101
    | Printer s -> set_or_raise loc printer s "printer"
    | Transform s -> add_to_list transform s
102
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
103
  in
104
  let f = load_file file in
105 106 107
  List.iter add_global f.f_global;

  let thprelude = ref Mid.empty in
108 109
  let meta      = ref Mid.empty in
  let meta_cl   = ref Mid.empty in
110 111
  let qualid    = ref [] in

112 113
  let find_pr th (loc,q) = try ns_find_pr th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
114
  in
115 116
  let find_ls th (loc,q) = try ns_find_ls th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
117
  in
118 119
  let find_ts th (loc,q) = try ns_find_ts th.th_export q
    with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
120
  in
121
  let add_meta th td m =
122 123
    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
124
  in
125
  let add_local th = function
126 127
    | Rprelude s ->
        let l = try Mid.find th.th_name !thprelude with Not_found -> [] in
128
        thprelude := Mid.add th.th_name (l @ [s]) !thprelude
Andrei Paskevich's avatar
Andrei Paskevich committed
129 130 131 132 133 134
    | 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)
    | Rsyntaxls (c,q,s) ->
        let td = syntax_logic (find_ls th q) s in
        add_meta th td (if c then meta_cl else meta)
135
    | Rremovepr (c,q) ->
136 137
        let td = remove_prop (find_pr th q) in
        add_meta th td (if c then meta_cl else meta)
138 139 140 141 142 143 144 145
    | Rmeta (c,s,al) ->
        let convert = function
          | PMAts q  -> MAts (find_ts th q)
          | PMAls q  -> MAls (find_ls th q)
          | PMApr q  -> MApr (find_pr th q)
          | PMAstr s -> MAstr s
          | PMAint i -> MAint i
        in
146 147
        let m = lookup_meta s in
        let td = create_meta m (List.map convert al) in
148
        add_meta th td (if c then meta_cl else meta)
149
  in
150 151
  let add_local th (loc,rule) =
    try add_local th rule with e -> raise (Loc.Located (loc,e))
152 153 154
  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
155 156
    let th =
      try Env.find_theory env f id with e -> raise (Loc.Located (loc,e))
157 158 159 160 161
    in
    qualid := q;
    List.iter (add_local th) trl
  in
  List.iter add_theory f.f_rules;
162 163
  transform := List.rev !transform;
  incr driver_tag;
164
  {
165 166 167 168 169 170 171 172 173
    drv_env         = env;
    drv_printer     = !printer;
    drv_prelude     = !prelude;
    drv_filename    = !filename;
    drv_transform   = !transform;
    drv_thprelude   = !thprelude;
    drv_meta        = !meta;
    drv_meta_cl     = !meta_cl;
    drv_regexps     = List.rev !regexps;
174
    drv_timeregexps = List.rev !timeregexps;
175
    drv_exitcodes   = List.rev !exitcodes;
176
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
177

178
(** apply drivers *)
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
179

180
exception UnknownSpec of string
181

182 183 184 185 186 187 188
let filename_regexp = Str.regexp "%\\(.\\)"

let get_filename drv input_file theory_name goal_name =
  let file = match drv.drv_filename with
    | Some f -> f
    | None -> "%f-%t-%g.dump"
  in
189
  let replace s = match Str.matched_group 1 s with
190 191 192
    | "%" -> "%"
    | "f" -> input_file
    | "t" -> theory_name
193
    | "g" -> goal_name
194
    | s   -> raise (UnknownSpec s)
195
  in
196
  Str.global_substitute filename_regexp replace file
197

198
let file_of_task drv input_file theory_name task =
199
  get_filename drv input_file theory_name (task_goal task).pr_name.id_string
200

201
let call_on_buffer ~command ?timelimit ?memlimit drv buffer =
202
  let regexps = drv.drv_regexps in
203
  let timeregexps = drv.drv_timeregexps in
204 205 206
  let exitcodes = drv.drv_exitcodes in
  let filename = get_filename drv "" "" "" in
  Call_provers.call_on_buffer
207
    ~command ?timelimit ?memlimit ~regexps ~timeregexps
208
    ~exitcodes ~filename buffer
209

210 211 212 213
(** print'n'prove *)

exception NoPrinter

214 215 216 217
let update_task drv task =
  let task, goal = match task with
    | Some { task_decl = g ; task_prev = t } -> t,g
    | None -> raise Task.GoalNotFound
218 219 220
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
221 222 223 224 225
      if Task.on_used_theory th task then
        Stdecl.fold (fun tdm task ->
          add_tdecl task tdm
        ) s task
      else task
226 227 228 229
    ) drv.drv_meta task
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
230
      Task.on_theory th (fun task sm ->
231
        Stdecl.fold (fun tdm task ->
232
          add_tdecl task (clone_meta tdm sm)
233
        ) s task
234
      ) task task
235 236
    ) drv.drv_meta_cl task
  in
237 238
  add_tdecl task goal

239
let print_task ?old drv fmt task =
240 241 242 243
  let p = match drv.drv_printer with
    | None -> raise NoPrinter
    | Some p -> p
  in
244 245
  let printer =
    lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
MARCHE Claude's avatar
MARCHE Claude committed
246
  in
247 248
  let lookup_transform t = t, lookup_transform t drv.drv_env in
  let transl = List.map lookup_transform drv.drv_transform in
249
  let apply task (_t, tr) =
250
(*  Format.printf "@\n@\n[%f] %s@." (Sys.time ()) t; *)
251
    Trans.apply tr task
252
  in
253 254 255
(*Format.printf "@\n@\nTASK";*)
  let task = update_task drv task in
  let task = List.fold_left apply task transl in
256
  fprintf fmt "@[%a@]@?" (printer ?old) task
257

258
let prove_task ~command ?timelimit ?memlimit ?old drv task =
259 260
  let buf = Buffer.create 1024 in
  let fmt = formatter_of_buffer buf in
261
  print_task ?old drv fmt task; pp_print_flush fmt ();
262
  call_on_buffer ~command ?timelimit ?memlimit drv buf
263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285

(* 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"
  | NoPlugins -> Format.fprintf fmt
      "Plugins are not supported, recomplie Why"
  | 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
  | e -> raise e)