driver.ml 14 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
21 22
open Ty
open Term
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23 24
open Theory
open Driver_ast
25
open Ident
26

27 28 29 30 31 32 33
(* 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

34
let global_substitute_fmt expr repl_fun text fmt =
35 36 37
  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
38
      pp_print_string fmt (string_after text start)
39 40 41
    else
      match opt_search_forward expr text startpos with
      | None ->
42
          pp_print_string fmt (string_after text start)
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
      | 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
66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
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 *)

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

type theory_driver = {
  thd_prelude : string option;
  thd_tsymbol : unit ;
}

103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120

type translation = 
  | Remove
  | Syntax of string
  | Tag of Snm.t

let translation_union t1 t2 =
  match t1, t2 with
    | Remove, _ | _, Remove -> Remove
    | ((Syntax _ as s), _) | (_,(Syntax _ as s)) -> s
    | Tag s1, Tag s2 -> Tag (Snm.union s1 s2)

let print_translation fmt = function
  | Remove -> fprintf fmt "remove" 
  | Syntax s -> fprintf fmt "syntax %s" s
  | Tag s -> fprintf fmt "tag %a" 
      (Pp.print_iter1 Snm.iter Pp.comma Pp.string) s

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
121
type printer = driver -> formatter -> context -> unit
122

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123
and driver = {
Francois Bobot's avatar
 
Francois Bobot committed
124 125 126 127 128 129 130 131 132
  drv_printer     : printer option;
  drv_context     : context;
  drv_prover      : Call_provers.prover;
  drv_prelude     : string option;
  drv_filename    : string option;
  drv_beforesplit : Transform.ctxt_t list;
  drv_aftersplit  : Transform.ctxt_t list;
  drv_rules       : theory_rules list;
  drv_thprelude   : string Hid.t;
133
  (* the first is the translation only for this ident, the second is also for representant *)
Francois Bobot's avatar
 
Francois Bobot committed
134 135
  drv_theory      : (translation * translation) Hid.t;
  drv_with_ctxt   : translation Hid.t;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
136
}
137

138
(*
139 140 141 142 143
let print_driver fmt driver =
  printf "drv_theory %a@\n" 
    (Pp.print_iter2 Hid.iter Pp.semi Pp.comma print_ident
       (Pp.print_pair print_translation print_translation))
    driver.drv_theory
144
*)
145

146 147 148 149 150
(** registering transformation *)

let (transforms : (string, unit -> Transform.ctxt_t) Hashtbl.t) = Hashtbl.create 17

let register_transform name transform = Hashtbl.replace transforms name transform
151

Francois Bobot's avatar
 
Francois Bobot committed
152 153
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
154 155 156 157 158 159
(** 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
160 161
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []

Francois Bobot's avatar
Francois Bobot committed
162
(*
163 164 165
let () = 
  Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver";
                     "Pervasives";"Format";"List";"Sys";"Unix"]
Francois Bobot's avatar
Francois Bobot committed
166
*)
167

168 169 170 171 172 173 174 175 176 177 178
module Dynlink =
struct
  let is_native = true
  open Dynlink
  let is_native1 = is_native
  let is_native = false
  include Dynlink
  let is_native2 = is_native
  let is_native_not_defined = is_native1 <> is_native2
end

179
let load_plugin dir (byte,nat) =
180 181 182 183
  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.";
184 185 186 187
  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
188
let load_file file =
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
189 190 191
  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
192
  let f = Driver_lexer.parse_file lb in 
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
193
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
194
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
195

196 197 198 199 200 201 202 203 204 205
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

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

208
let check_syntax loc s len = 
209 210 211 212 213 214 215
  iter_group regexp_arg_pos 
    (fun s ->
       let i = int_of_string (matched_group 1 s) in
       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


216
let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
217
  let id,qfile = qualid_to_slist qualid in
218
  let th = try
219
    find_theory driver.drv_context.ctxt_env qfile id 
220 221
  with Not_found -> errorm ~loc "theory %s not found" 
    (String.concat "." qualid) in
222 223 224 225 226 227 228 229 230 231 232 233 234 235
  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 ->
      let t23 = if cloned then (Tag Snm.empty),t else t,(Tag Snm.empty) in
      Hid.add driver.drv_theory id t23 in
  let add = function
    | Rremove (c,(loc,q)) -> 
        begin
          try
236
            add_htheory c (pr_name (Transform.find_pr th.th_export q)) Remove
237 238 239
          with Not_found -> errorm ~loc "Unknown axioms %s" 
            (string_of_qualid qualid q)
        end 
240
    | Rsyntaxls ((loc,q),s) -> 
241 242
        begin
          try
Francois Bobot's avatar
 
Francois Bobot committed
243
            let ls = (Transform.find_l th.th_export q) in
244
            check_syntax loc s (List.length ls.ls_args);
245
            add_htheory false ls.ls_name (Syntax s)
246 247 248
          with Not_found -> errorm ~loc "Unknown logic %s" 
            (string_of_qualid qualid q)
        end 
249
    | Rsyntaxty ((loc,q),s) -> 
250 251
        begin
          try
Francois Bobot's avatar
 
Francois Bobot committed
252
            let ts = Transform.find_ty th.th_export q in
253 254 255 256 257 258 259 260
            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
Francois Bobot's avatar
 
Francois Bobot committed
261
            add_htheory c (Transform.find_l th.th_export q).ls_name 
262
              (Tag (Snm.singleton s))
263 264 265
          with Not_found -> errorm ~loc "Unknown logic %s" 
            (string_of_qualid qualid q)
        end
266 267 268
    | Rtagty (c,(loc,q),s) ->
        begin
          try
Francois Bobot's avatar
 
Francois Bobot committed
269
            add_htheory c (Transform.find_ty th.th_export q).ts_name 
270 271 272 273 274 275 276
              (Tag (Snm.singleton s))
          with Not_found -> errorm ~loc "Unknown type %s" 
            (string_of_qualid qualid q)
        end
    | Rtagpr (c,(loc,q),s) ->
        begin
          try
277
            add_htheory c (pr_name (Transform.find_pr th.th_export q))
278 279 280 281
              (Tag (Snm.singleton s))
          with Not_found -> errorm ~loc "Unknown proposition %s" 
            (string_of_qualid qualid q)
        end
282 283 284 285 286
    | Rprelude (loc,s) -> if Hid.mem driver.drv_thprelude th.th_name
      then errorm ~loc "duplicate prelude"
      else Hid.add driver.drv_thprelude th.th_name s in
  List.iter add trl

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
287 288
let load_driver file env =
  let f = load_file file in
Francois Bobot's avatar
 
Francois Bobot committed
289 290 291 292 293 294 295 296
  let prelude     = ref None in
  let printer     = ref None in
  let call_stdin  = ref None in
  let call_file   = ref None in
  let filename    = ref None in
  let beforesplit = ref None in
  let aftersplit  = ref None in
  let regexps     = ref [] in
297 298 299
  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
300 301 302 303 304 305 306
  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 
307 308 309 310 311 312 313
    | Prelude s -> set_or_raise loc prelude s "prelude"
    | 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
314
    | Filename s -> set_or_raise loc filename s "filename"
Francois Bobot's avatar
 
Francois Bobot committed
315 316
    | Beforesplit s -> set_or_raise loc beforesplit s "beforesplit"
    | Aftersplit s -> set_or_raise loc aftersplit s "aftersplit"
317
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
318 319
  in
  List.iter add f.f_global;
Francois Bobot's avatar
Francois Bobot committed
320
  let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
Francois Bobot's avatar
 
Francois Bobot committed
321 322 323
  let trans r =
    let transformations = match !r with
      | None -> [] | Some l -> l in
324 325 326
    List.map (fun (loc,s) -> try (Hashtbl.find transforms s) () 
              with Not_found -> errorm ~loc "unknown transformation %s" s)
      transformations in
Francois Bobot's avatar
 
Francois Bobot committed
327 328 329 330 331 332 333 334 335 336 337 338 339 340 341
    let beforesplit = trans beforesplit in
    let aftersplit = trans aftersplit in
  { drv_printer     = !printer;
    drv_context     = Context.init_context env;
    drv_prover      = {Call_provers.pr_call_stdin = !call_stdin;
                       pr_call_file               = !call_file;
                       pr_regexps                 = regexps};
    drv_prelude     = !prelude;
    drv_filename    = !filename;
    drv_beforesplit = beforesplit;
    drv_aftersplit  = aftersplit;
    drv_rules       = f.f_rules;
    drv_thprelude   = Hid.create 1;
    drv_theory      = Hid.create 1;
    drv_with_ctxt   = Hid.create 1;
342
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
343 344 345

(** querying drivers *)

346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
let query_ident drv id =
  try
    Hid.find drv.drv_with_ctxt id
  with Not_found ->
    let r = try
      Mid.find id drv.drv_context.ctxt_cloned
    with Not_found -> Sid.empty in
    let tr = try fst (Hid.find drv.drv_theory id) 
    with Not_found -> Tag Snm.empty in 
    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
    Hid.add drv.drv_with_ctxt id tr;
    tr
361 362 363 364 365 366

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
367
  global_substitute_fmt regexp_arg_pos repl_fun s fmt
368
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
369 370
(** using drivers *)

Francois Bobot's avatar
 
Francois Bobot committed
371
let transform_context list ctxt =
372
  List.fold_left (fun ctxt t -> Transform.apply t ctxt) 
Francois Bobot's avatar
 
Francois Bobot committed
373 374 375 376
    ctxt list

let apply_before_split drv = transform_context drv.drv_beforesplit
let apply_after_split drv = transform_context drv.drv_aftersplit
377

378
let print_context drv fmt ctxt = match drv.drv_printer with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
379
  | None -> errorm "no printer"
380 381 382 383 384 385
  | Some f -> let drv = {drv with drv_context = ctxt;
                   drv_thprelude  = Hid.create 17;
                   drv_theory     = Hid.create 17;
                   drv_with_ctxt  = Hid.create 17} in
    List.iter (load_rules drv) drv.drv_rules;
    f drv fmt ctxt 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
386

387 388 389 390 391 392
let regexp_filename = Str.regexp "%\\([a-z]\\)"

let filename_of_goal drv ident_printer filename theory_name ctxt =
  match drv.drv_filename with
    | None -> errorm "no filename syntax given"
    | Some f -> 
393
        let pr_name = pr_name (Transform.goal_of_ctxt ctxt) in
394 395 396 397 398 399 400 401 402
        let repl_fun s = 
          let i = matched_group 1 s in
          match i with
            | "f" -> filename
            | "t" -> theory_name
            | "s" -> id_unique ident_printer pr_name
            | _ -> errorm "substitution variable are only %%f %%t and %%s" in
        global_substitute regexp_filename repl_fun f

403 404 405
let file_printer = 
  create_ident_printer ~sanitizer:(sanitizer char_to_alnumus char_to_alnumus)
    []
406

407 408 409 410 411 412 413 414 415 416 417 418 419 420
let call_prover_on_file ?debug ?timeout drv filename =
  Call_provers.on_file drv.drv_prover filename 
let call_prover_on_buffer ?debug ?timeout ?filename drv ib = 
  Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_prover ib 


let call_prover ?debug ?timeout drv ctx =
  let filename = 
    match drv.drv_filename with
      | None -> None
      | Some _ -> Some (filename_of_goal drv file_printer "" "" ctx) in
  let buffer = Buffer.create 128 in
  bprintf buffer "%a@?" (print_context drv) ctx;
  call_prover_on_buffer ?debug ?timeout ?filename drv buffer
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
421

422 423


424 425 426 427 428
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. test"
End: 
*)