driver.ml 9.88 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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
30
open Driver_ast
31
open Call_provers
32

33
(** drivers *)
34

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

49 50
(** parse a driver file *)

51 52
exception NoPlugins

53
let load_plugin dir (byte,nat) =
54
  if not Config.why_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

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

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

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

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

179
(** apply drivers *)
180

181
exception UnknownSpec of string
182

183 184 185 186 187 188 189
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
190
  let replace s = match Str.matched_group 1 s with
191 192 193
    | "%" -> "%"
    | "f" -> input_file
    | "t" -> theory_name
194
    | "g" -> goal_name
195
    | s   -> raise (UnknownSpec s)
196
  in
197
  Str.global_substitute filename_regexp replace file
198

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

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

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

exception NoPrinter

213 214 215 216
let update_task drv task =
  let task, goal = match task with
    | Some { task_decl = g ; task_prev = t } -> t,g
    | None -> raise Task.GoalNotFound
217 218 219 220 221
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
      let cs = (find_clone task th).tds_set in
      Stdecl.fold (fun td task -> match td.td_node with
222 223
        | Clone (_,tm,lm,pm)
          when Mts.is_empty tm && Mls.is_empty lm && Mpr.is_empty pm ->
224
            Stdecl.fold (fun td task -> add_tdecl task td) s task
225
        | _ -> task
226 227 228 229 230 231 232 233 234 235 236 237 238
      ) cs task
    ) drv.drv_meta task
  in
  let task =
    Mid.fold (fun _ (th,s) task ->
      let cs = (find_clone task th).tds_set in
      Stdecl.fold (fun tdc task ->
        Stdecl.fold (fun tdm task ->
          add_tdecl task (clone_meta tdm th tdc)
        ) s task
      ) cs task
    ) drv.drv_meta_cl task
  in
239 240
  add_tdecl task goal

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

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

(* 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)