driver.ml 14.3 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.                  *)
(*                                                                        *)
(**************************************************************************)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
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
Francois Bobot's avatar
Francois Bobot committed
28
open Register
Andrei Paskevich's avatar
Andrei Paskevich committed
29
open Env
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
open Driver_ast
31

32
33
34
35
36
37
38
(* Utils from Str *)

(* From global_substitute of str *)
open Str
let opt_search_forward re s pos =
  try Some(search_forward re s pos) with Not_found -> None

39
let global_substitute_fmt expr repl_fun text fmt =
40
41
42
  let rec replace start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos > String.length text then
43
      pp_print_string fmt (string_after text start)
44
45
46
    else
      match opt_search_forward expr text startpos with
      | None ->
47
          pp_print_string fmt (string_after text start)
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
      | Some pos ->
          let end_pos = match_end() in
          pp_print_string fmt (String.sub text start (pos-start));
          repl_fun text fmt;
          replace end_pos (end_pos = pos)
  in
    (replace 0 false)

let iter_group expr iter_fun text =
  let rec iter start last_was_empty =
    let startpos = if last_was_empty then start + 1 else start in
    if startpos < String.length text then
      match opt_search_forward expr text startpos with
        | None -> ()
        | Some pos ->
            let end_pos = match_end() in
            iter_fun text;
            iter end_pos (end_pos = pos)
  in
  iter 0 false
 
(* *)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
type error = string

exception Error of string

let report = pp_print_string

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

let errorm ?loc f =
  let buf = Buffer.create 512 in
  let fmt = Format.formatter_of_buffer buf in
  Format.kfprintf 
    (fun _ -> 
       Format.pp_print_flush fmt ();
       let s = Buffer.contents buf in
       Buffer.clear buf;
       error ?loc s)
    fmt f

(** creating drivers *)

94
95
type prover_answer = 
    Call_provers.prover_answer =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
96
97
98
99
100
  | Valid
  | Invalid
  | Unknown of string
  | Failure of string
  | Timeout
101
  | HighFailure
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
102
103

type theory_driver = {
MARCHE Claude's avatar
MARCHE Claude committed
104
  thd_prelude : string list;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
105
106
107
  thd_tsymbol : unit ;
}

108
109
110
111

type translation = 
  | Remove
  | Syntax of string
Andrei Paskevich's avatar
Andrei Paskevich committed
112
  | Tag of Sstr.t
113
114
115
116
117

let translation_union t1 t2 =
  match t1, t2 with
    | Remove, _ | _, Remove -> Remove
    | ((Syntax _ as s), _) | (_,(Syntax _ as s)) -> s
Andrei Paskevich's avatar
Andrei Paskevich committed
118
    | Tag s1, Tag s2 -> Tag (Sstr.union s1 s2)
119
120
121
122
123

let print_translation fmt = function
  | Remove -> fprintf fmt "remove" 
  | Syntax s -> fprintf fmt "syntax %s" s
  | Tag s -> fprintf fmt "tag %a" 
Andrei Paskevich's avatar
Andrei Paskevich committed
124
      (Pp.print_iter1 Sstr.iter Pp.comma Pp.string) s
125

Andrei Paskevich's avatar
Andrei Paskevich committed
126
type printer = driver -> formatter -> task -> unit
127

Francois Bobot's avatar
Francois Bobot committed
128
and raw_driver = {
Francois Bobot's avatar
   
Francois Bobot committed
129
130
  drv_printer     : printer option;
  drv_prover      : Call_provers.prover;
MARCHE Claude's avatar
MARCHE Claude committed
131
  drv_prelude     : string list;
Francois Bobot's avatar
   
Francois Bobot committed
132
  drv_filename    : string option;
Francois Bobot's avatar
   
Francois Bobot committed
133
  drv_transforms  : task tlist_reg;
Francois Bobot's avatar
   
Francois Bobot committed
134
  drv_rules       : theory_rules list;
Francois Bobot's avatar
Francois Bobot committed
135
136
137
}

and driver = {
138
139
140
141
  drv_raw         : raw_driver;
  drv_clone       : clone;
  drv_used        : theory Mid.t;
  drv_env         : env;
MARCHE Claude's avatar
MARCHE Claude committed
142
  drv_thprelude   : string list Hid.t;
Francois Bobot's avatar
   
Francois Bobot committed
143
144
  (* the first is the translation only for this ident, the second is
     also for representant *)
Francois Bobot's avatar
   
Francois Bobot committed
145
  drv_theory      : (translation * translation) Hid.t;
Andrei Paskevich's avatar
Andrei Paskevich committed
146
  drv_with_task   : translation Hid.t;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
147
}
148

Francois Bobot's avatar
Francois Bobot committed
149

150
(*
Francois Bobot's avatar
   
Francois Bobot committed
151
  let print_driver fmt driver =
152
  printf "drv_theory %a@\n" 
Francois Bobot's avatar
   
Francois Bobot committed
153
154
155
  (Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
  (Pp.print_pair print_translation print_translation))
  driver.drv_theory
156
*)
157

158
159
(** registering transformation *)

Francois Bobot's avatar
   
Francois Bobot committed
160
let (transforms : (string, task tlist_reg) Hashtbl.t) 
161
    = Hashtbl.create 17
162

Francois Bobot's avatar
   
Francois Bobot committed
163
164
165
let register_transform_l name transform = 
  Hashtbl.replace transforms name transform
let register_transform name t = register_transform_l name (singleton t)
Francois Bobot's avatar
   
Francois Bobot committed
166
167
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
168
169
170
171
172
173
(** registering printers *)

let (printers : (string, printer) Hashtbl.t) = Hashtbl.create 17

let register_printer name printer = Hashtbl.replace printers name printer

Francois Bobot's avatar
   
Francois Bobot committed
174
175
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []

Francois Bobot's avatar
Francois Bobot committed
176
(*
177
178
179
let () = 
  Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver";
                     "Pervasives";"Format";"List";"Sys";"Unix"]
Francois Bobot's avatar
Francois Bobot committed
180
*)
181

182
open Dynlink_compat
183

184
let load_plugin dir (byte,nat) =
185
186
187
188
  if Dynlink.is_native_not_defined then 
    errorm 
"Why has been compiled with a version of caml which doesn't allow\
 native dynlink. So Why chooses to refuse plugin.";
189
190
191
192
  let file = if Dynlink.is_native then nat else byte in
  let file = Filename.concat dir file in
  Dynlink.loadfile_private file

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
193
let load_file file =
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
194
195
196
  let c = open_in file in
  let lb = Lexing.from_channel c in
  Loc.set_file file lb;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
197
  let f = Driver_lexer.parse_file lb in 
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
198
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
199
  f
Jean-Christophe Filliâtre's avatar
drivers    
Jean-Christophe Filliâtre committed
200

201
202
203
204
205
206
207
208
209
210
let rec qualid_to_slist = function
  | [] -> assert false
  | [a] -> a,[]
  | a::l -> let id,l = qualid_to_slist l in (id,a::l)

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

211
212
let regexp_arg_pos = Str.regexp "%\\([0-9]+\\)"

213
let check_syntax loc s len = 
214
215
216
  iter_group regexp_arg_pos 
    (fun s ->
       let i = int_of_string (matched_group 1 s) in
Francois Bobot's avatar
   
Francois Bobot committed
217
218
219
220
221
222
223
       if i=0 
       then errorm ~loc 
         "invalid indice of argument : the first one is %%1 and not %%0";
       if i>len 
       then errorm ~loc 
         "invalid indice of argument \"%%%i\" this logic has only %i argument" 
         i len) s
224
225


226
let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
227
  let id,qfile = qualid_to_slist qualid in
228
  let th = try
Andrei Paskevich's avatar
Andrei Paskevich committed
229
    find_theory env qfile id 
230
231
232
  with Env.TheoryNotFound (l,s) -> 
    errorm ~loc "theory %s.%s not found" (String.concat "." l) s
  in
233
234
235
236
237
238
239
240
  let add_htheory cloned id t =
    try
      let t2,t3 = Hid.find driver.drv_theory id in
      let t23 = 
        if cloned then (translation_union t t2),t3
        else t2,(translation_union t t3) in
      Hid.replace driver.drv_theory id t23 
    with Not_found ->
Andrei Paskevich's avatar
Andrei Paskevich committed
241
      let t23 = if cloned then (Tag Sstr.empty),t else t,(Tag Sstr.empty) in
242
243
244
245
246
      Hid.add driver.drv_theory id t23 in
  let add = function
    | Rremove (c,(loc,q)) -> 
        begin
          try
247
            add_htheory c 
248
              (ns_find_pr th.th_export q).pr_name Remove
249
250
251
          with Not_found -> errorm ~loc "Unknown axioms %s" 
            (string_of_qualid qualid q)
        end 
252
    | Rsyntaxls ((loc,q),s) -> 
253
254
        begin
          try
255
            let ls = ns_find_ls th.th_export q in
256
            check_syntax loc s (List.length ls.ls_args);
257
            add_htheory false ls.ls_name (Syntax s)
258
259
260
          with Not_found -> errorm ~loc "Unknown logic %s" 
            (string_of_qualid qualid q)
        end 
261
    | Rsyntaxty ((loc,q),s) -> 
262
263
        begin
          try
264
            let ts = ns_find_ts th.th_export q in
265
266
267
268
269
270
271
272
            check_syntax loc s (List.length ts.ts_args);
            add_htheory false ts.ts_name (Syntax s)
          with Not_found -> errorm ~loc "Unknown type %s" 
            (string_of_qualid qualid q)
        end
    | Rtagls (c,(loc,q),s) ->
        begin
          try
273
            add_htheory c (ns_find_ls th.th_export q).ls_name 
Andrei Paskevich's avatar
Andrei Paskevich committed
274
              (Tag (Sstr.singleton s))
275
276
277
          with Not_found -> errorm ~loc "Unknown logic %s" 
            (string_of_qualid qualid q)
        end
278
279
280
    | Rtagty (c,(loc,q),s) ->
        begin
          try
281
            add_htheory c (ns_find_ts th.th_export q).ts_name 
Andrei Paskevich's avatar
Andrei Paskevich committed
282
              (Tag (Sstr.singleton s))
283
284
285
286
287
288
          with Not_found -> errorm ~loc "Unknown type %s" 
            (string_of_qualid qualid q)
        end
    | Rtagpr (c,(loc,q),s) ->
        begin
          try
289
            add_htheory c (ns_find_pr th.th_export q).pr_name
Andrei Paskevich's avatar
Andrei Paskevich committed
290
              (Tag (Sstr.singleton s))
291
292
293
          with Not_found -> errorm ~loc "Unknown proposition %s" 
            (string_of_qualid qualid q)
        end
MARCHE Claude's avatar
MARCHE Claude committed
294
295
296
297
298
299
300
    | Rprelude (loc,s) -> 
        let l = 
          try Hid.find driver.drv_thprelude th.th_name 
          with Not_found -> []
        in
        Hid.replace driver.drv_thprelude th.th_name (s::l) 
  in
301
302
  List.iter add trl

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
303
304
let load_driver file env =
  let f = load_file file in
MARCHE Claude's avatar
MARCHE Claude committed
305
  let prelude     = ref [] in
Francois Bobot's avatar
   
Francois Bobot committed
306
307
308
309
  let printer     = ref None in
  let call_stdin  = ref None in
  let call_file   = ref None in
  let filename    = ref None in
310
  let ltransforms = ref None in
Francois Bobot's avatar
   
Francois Bobot committed
311
  let regexps     = ref [] in
312
313
314
  let set_or_raise loc r v error =
    if !r <> None then errorm ~loc "duplicate %s" error
    else r := Some v in 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
315
316
317
318
319
320
321
  let add (loc, g) = match g with
    | Printer _ when !printer <> None -> 
	errorm ~loc "duplicate printer"
    | Printer s when Hashtbl.mem printers s ->
	printer := Some (Hashtbl.find printers s)
    | Printer s -> 
	errorm ~loc "unknown printer %s" s 
MARCHE Claude's avatar
MARCHE Claude committed
322
    | Prelude s -> prelude := s :: !prelude
323
324
325
326
327
328
    | CallStdin s -> set_or_raise loc call_stdin s "callstdin"
    | CallFile s -> set_or_raise loc call_file s "callfile"
    | RegexpValid s -> regexps:=(s,Valid)::!regexps
    | RegexpInvalid s -> regexps:=(s,Invalid)::!regexps
    | RegexpUnknown (s1,s2) -> regexps:=(s1,Unknown s2)::!regexps
    | RegexpFailure (s1,s2) -> regexps:=(s1,Failure s2)::!regexps
329
    | Filename s -> set_or_raise loc filename s "filename"
330
    | Transforms s -> set_or_raise loc ltransforms s "transform"
331
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
332
333
  in
  List.iter add f.f_global;
Francois Bobot's avatar
Francois Bobot committed
334
  let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
Francois Bobot's avatar
   
Francois Bobot committed
335
336
337
  let trans r =
    let transformations = match !r with
      | None -> [] | Some l -> l in
338
339
340
    List.fold_left 
      (fun acc (loc,s) -> 
         let t = 
Francois Bobot's avatar
Francois Bobot committed
341
           try Hashtbl.find transforms s
342
           with Not_found -> errorm ~loc "unknown transformation %s" s in
Francois Bobot's avatar
   
Francois Bobot committed
343
         compose_l acc t
344
      )
Andrei Paskevich's avatar
Andrei Paskevich committed
345
      identity_l transformations in
346
    let transforms = trans ltransforms in
Francois Bobot's avatar
   
Francois Bobot committed
347
348
349
350
351
352
  { drv_printer     = !printer;
    drv_prover      = {Call_provers.pr_call_stdin = !call_stdin;
                       pr_call_file               = !call_file;
                       pr_regexps                 = regexps};
    drv_prelude     = !prelude;
    drv_filename    = !filename;
353
    drv_transforms  = transforms;
Francois Bobot's avatar
   
Francois Bobot committed
354
    drv_rules       = f.f_rules;
355
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
356
357
358

(** querying drivers *)

359
360
let query_ident drv id =
  try
Andrei Paskevich's avatar
Andrei Paskevich committed
361
    Hid.find drv.drv_with_task id
362
363
  with Not_found ->
    let r = try
Francois Bobot's avatar
Francois Bobot committed
364
      Mid.find id drv.drv_clone.cl_map
365
366
    with Not_found -> Sid.empty in
    let tr = try fst (Hid.find drv.drv_theory id) 
Andrei Paskevich's avatar
Andrei Paskevich committed
367
    with Not_found -> Tag Sstr.empty in 
368
369
370
371
    let tr = Sid.fold 
      (fun id acc -> try translation_union acc 
         (snd (Hid.find drv.drv_theory id)) 
       with Not_found -> acc) r tr in
Andrei Paskevich's avatar
Andrei Paskevich committed
372
    Hid.add drv.drv_with_task id tr;
373
    tr
374
375
376
377
378
379

let syntax_arguments s print fmt l =
  let args = Array.of_list l in
  let repl_fun s fmt = 
    let i = int_of_string (matched_group 1 s) in
    print fmt args.(i-1) in
380
  global_substitute_fmt regexp_arg_pos repl_fun s fmt
381
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
382
383
(** using drivers *)

Francois Bobot's avatar
Francois Bobot committed
384
385
386
let apply_transforms drv = 
  apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone

387
388
let cook_driver env clone used drv = 
  let drv = { drv_raw        = drv;
Francois Bobot's avatar
Francois Bobot committed
389
              drv_clone      = clone;
390
391
              drv_used       = used;
              drv_env        = env;
Francois Bobot's avatar
Francois Bobot committed
392
393
394
              drv_thprelude  = Hid.create 17;
              drv_theory     = Hid.create 17;
              drv_with_task  = Hid.create 17} in
395
  List.iter (load_rules env drv) drv.drv_raw.drv_rules;
Francois Bobot's avatar
Francois Bobot committed
396
397
  drv

398

399
400
401
402
403
let print_prelude drv fmt =
  let pr_pr s () = fprintf fmt "%s@\n" s in
  List.fold_right pr_pr drv.drv_raw.drv_prelude ();
  let seen = Hid.create 17 in
  let rec print_prel th_name th =
Andrei Paskevich's avatar
Andrei Paskevich committed
404
    if Hid.mem seen th_name then () else begin
405
406
407
408
409
410
411
      Hid.add seen th_name ();
      Mid.iter print_prel th.th_used;
      let prel = 
        try Hid.find drv.drv_thprelude th_name 
        with Not_found -> []
      in
      List.fold_right pr_pr prel ()
Andrei Paskevich's avatar
Andrei Paskevich committed
412
    end
413
414
415
416
  in
  Mid.iter print_prel drv.drv_used;
  fprintf fmt "@."

Francois Bobot's avatar
Francois Bobot committed
417
let print_task drv fmt task = match drv.drv_raw.drv_printer with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
418
  | None -> errorm "no printer"
419
420
421
  | Some f -> 
      print_prelude drv fmt;
      f drv fmt task 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
422

423
424
let regexp_filename = Str.regexp "%\\([a-z]\\)"

425
let filename_of_goal drv filename theory_name task =
Francois Bobot's avatar
Francois Bobot committed
426
  match drv.drv_raw.drv_filename with
427
428
    | None -> errorm "no filename syntax given"
    | Some f -> 
429
        let pr_name = (task_goal task).pr_name in
430
431
432
433
434
        let repl_fun s = 
          let i = matched_group 1 s in
          match i with
            | "f" -> filename
            | "t" -> theory_name
435
            | "s" -> pr_name.id_short
436
437
438
            | _ -> errorm "substitution variable are only %%f %%t and %%s" in
        global_substitute regexp_filename repl_fun f

439
440
441
let file_printer = 
  create_ident_printer ~sanitizer:(sanitizer char_to_alnumus char_to_alnumus)
    []
442

443
let call_prover_on_file ?debug ?timeout drv filename =
Francois Bobot's avatar
Francois Bobot committed
444
  Call_provers.on_file drv.drv_raw.drv_prover filename 
445
446
let call_prover_on_formatter ?debug ?timeout ?filename drv ib = 
  Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_raw.drv_prover ib
447
448


Francois Bobot's avatar
Francois Bobot committed
449
let call_prover ?debug ?timeout drv task =
450
  let filename = 
Francois Bobot's avatar
Francois Bobot committed
451
    match drv.drv_raw.drv_filename with
452
      | None -> None
453
      | Some _ -> Some (filename_of_goal drv "why" "call_prover" task) in
454
455
  let formatter fmt = print_task drv fmt task in
  call_prover_on_formatter ?debug ?timeout ?filename drv formatter
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
456

457
458


459
460
461
462
463
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. test"
End: 
*)