driver.ml 13.5 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 124 125
and driver = {
  drv_printer    : printer option;
  drv_context    : context;
126
  drv_prover     : Call_provers.prover;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
127
  drv_prelude    : string option;
128
  drv_filename   : string option;
129
  drv_transformations : Transform.ctxt_t list;
130
  drv_rules      : theory_rules list;
131 132 133 134
  drv_thprelude  : string Hid.t;
  (* the first is the translation only for this ident, the second is also for representant *)
  drv_theory     : (translation * translation) Hid.t;
  drv_with_ctxt  : translation Hid.t;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
135
}
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
(** registering transformation *)

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

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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
150 151 152 153 154 155
(** registering printers *)

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

let register_printer name printer = Hashtbl.replace printers name printer

156 157 158 159 160 161 162 163 164 165 166

let () = 
  Dynlink.allow_only ["Theory";"Term";"Ident";"Transform";"Driver";
                     "Pervasives";"Format";"List";"Sys";"Unix"]


let load_plugin dir (byte,nat) =
  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
167
let load_file file =
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
168 169 170
  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
171
  let f = Driver_lexer.parse_file lb in 
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
172
  close_in c;
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
173
  f
Jean-Christophe Filliâtre's avatar
drivers  
Jean-Christophe Filliâtre committed
174

175 176 177 178 179 180 181 182 183 184
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

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

187
let check_syntax loc s len = 
188 189 190 191 192 193 194
  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


195
let load_rules driver {thr_name = loc,qualid; thr_rules = trl} =
196
  let id,qfile = qualid_to_slist qualid in
197
  let th = try
198
    find_theory driver.drv_context.ctxt_env qfile id 
199 200
  with Not_found -> errorm ~loc "theory %s not found" 
    (String.concat "." qualid) in
201 202 203 204 205 206 207 208 209 210
  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
211
  let rec find_l ns = function
212
    | [] -> assert false
213
    | [a] -> Mnm.find a ns.ns_ls
214 215
    | a::l -> find_l (Mnm.find a ns.ns_ns) l in
  let rec find_ty ns = function
216
    | [] -> assert false
217 218 219
    | [a] -> Mnm.find a ns.ns_ts
    | a::l -> find_ty (Mnm.find a ns.ns_ns) l in
  let rec find_pr ns = function
220
    | [] -> assert false
221 222
    | [a] -> Mnm.find a ns.ns_pr
    | a::l -> find_pr (Mnm.find a ns.ns_ns) l in
223 224 225 226
  let add = function
    | Rremove (c,(loc,q)) -> 
        begin
          try
227
            add_htheory c (find_pr th.th_export q).pr_name Remove
228 229 230
          with Not_found -> errorm ~loc "Unknown axioms %s" 
            (string_of_qualid qualid q)
        end 
231
    | Rsyntaxls ((loc,q),s) -> 
232 233
        begin
          try
234 235
            let ls = (find_l th.th_export q) in
            check_syntax loc s (List.length ls.ls_args);
236
            add_htheory false ls.ls_name (Syntax s)
237 238 239
          with Not_found -> errorm ~loc "Unknown logic %s" 
            (string_of_qualid qualid q)
        end 
240
    | Rsyntaxty ((loc,q),s) -> 
241 242
        begin
          try
243 244 245 246 247 248 249 250 251 252
            let ts = find_ty th.th_export q in
            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
            add_htheory c (find_l th.th_export q).ls_name 
253
              (Tag (Snm.singleton s))
254 255 256
          with Not_found -> errorm ~loc "Unknown logic %s" 
            (string_of_qualid qualid q)
        end
257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272
    | Rtagty (c,(loc,q),s) ->
        begin
          try
            add_htheory c (find_ty th.th_export q).ts_name 
              (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
            add_htheory c (find_pr th.th_export q).pr_name 
              (Tag (Snm.singleton s))
          with Not_found -> errorm ~loc "Unknown proposition %s" 
            (string_of_qualid qualid q)
        end
273 274 275 276 277
    | 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
278 279
let load_driver file env =
  let f = load_file file in
280 281 282 283
  let prelude = ref None in
  let printer = ref None in
  let call_stdin = ref None in
  let call_file = ref None in
284
  let filename = ref None in
285
  let transformations = ref None in
286 287 288 289
  let regexps = ref [] in
  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
290 291 292 293 294 295 296
  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 
297 298 299 300 301 302 303
    | 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
304
    | Filename s -> set_or_raise loc filename s "filename"
305 306
    | Transformations s -> set_or_raise loc transformations  s "transformations"
    | Plugin files -> load_plugin (Filename.dirname file) files
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
307 308
  in
  List.iter add f.f_global;
Francois Bobot's avatar
Francois Bobot committed
309
  let regexps = List.map (fun (s,a) -> (Str.regexp s,a)) !regexps in
310 311 312 313 314 315
  let transformations = match !transformations with
    | None -> [] | Some l -> l in
  let transformations = 
    List.map (fun (loc,s) -> try (Hashtbl.find transforms s) () 
              with Not_found -> errorm ~loc "unknown transformation %s" s)
      transformations in
316 317
  { drv_printer    = !printer;
    drv_context    = Context.init_context env;
318 319 320
    drv_prover     = {Call_provers.pr_call_stdin = !call_stdin;
                      pr_call_file               = !call_file;
                      pr_regexps                 = regexps};
321
    drv_prelude    = !prelude;
322
    drv_filename   = !filename;
323
    drv_transformations = transformations;
324 325 326 327 328
    drv_rules      = f.f_rules;
    drv_thprelude  = Hid.create 1;
    drv_theory     = Hid.create 1;
    drv_with_ctxt  = Hid.create 1;
  }
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
329 330 331

(** querying drivers *)

332 333 334 335 336 337 338 339 340 341 342 343 344 345 346
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
347 348 349 350 351 352

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
353
  global_substitute_fmt regexp_arg_pos repl_fun s fmt
354
 
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
355 356
(** using drivers *)

357 358 359 360
let transform_context drv ctxt =
  List.fold_left (fun ctxt t -> Transform.apply t ctxt) 
    ctxt drv.drv_transformations

361
let print_context drv fmt ctxt = match drv.drv_printer with
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
362
  | None -> errorm "no printer"
363 364 365 366 367 368
  | 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
369

370 371 372 373 374 375
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 -> 
376
        let pr_name = (goal_of_ctxt ctxt).pr_name in
377 378 379 380 381 382 383 384 385
        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

386 387 388
let file_printer = 
  create_ident_printer ~sanitizer:(sanitizer char_to_alnumus char_to_alnumus)
    []
389

390 391 392 393 394 395 396 397 398 399 400 401 402 403
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
404

405 406


407 408 409 410 411
(*
Local Variables: 
compile-command: "unset LANG; make -C ../.. test"
End: 
*)