Skip to content

why3
why3
Commit 22e13e75 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

registered transformations may now depend on driver_query

parent 5d5a8047
Hide whitespace changes
Inline Side-by-side
Showing with 491 additions and 205 deletions
Makefile.in
View file @ 22e13e75
......@@ -94,11 +94,12 @@ LIBGENERATED = src/util/rc.ml \
LIB_UTIL = pp loc prtree util hashcons sysutil hashweak rc
LIB_CORE = ident ty term pattern decl theory task pretty trans env register
LIB_CORE = ident ty term pattern decl theory task pretty trans env
LIB_PARSER = ptree parser lexer denv typing
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver whyconf
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
register prover whyconf
LIB_TRANSFORM = simplify_recursive_definition inlining \
split_conjunction encoding_decorate \
......
src/core/task.ml
View file @ 22e13e75
......@@ -42,9 +42,10 @@ and tdecl =
| Use of theory
| Clone of theory * (ident * ident) list
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_used = option_apply Mid.empty (fun t -> t.task_used)
let task_tag = option_apply (-1) (fun t -> t.task_tag)
let task_used = option_apply Mid.empty (fun t -> t.task_used)
let task_tag = option_apply (-1) (fun t -> t.task_tag)
module Task = struct
type t = task_hd
......@@ -188,10 +189,6 @@ let rec last_clone task = match task with
| Some { task_prev = task } -> last_clone task
| None -> None
let get_known = option_apply Mid.empty (fun t -> t.task_known)
let get_clone = option_apply Mid.empty (fun t -> t.task_clone)
let get_used = option_apply Mid.empty (fun t -> t.task_used)
exception GoalNotFound
let task_goal = function
......
src/core/task.mli
View file @ 22e13e75
......@@ -41,9 +41,10 @@ and tdecl = private
| Use of theory
| Clone of theory * (ident * ident) list
val task_known : task -> known_map
val task_clone : task -> clone_map
val task_used : task -> use_map
val task_tag : task -> int
val task_used : task -> use_map
val task_tag : task -> int
(* constructors *)
......@@ -80,10 +81,6 @@ val task_goal : task -> prsymbol
val last_clone : task -> task
val last_use : task -> task
val get_known : task -> known_map
val get_clone : task -> clone_map
val get_used : task -> use_map
(* exceptions *)
exception GoalNotFound
......
src/core/trans.ml
View file @ 22e13e75
......@@ -39,8 +39,6 @@ let singleton f x = [f x]
let compose f g x = g (f x)
let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
let compose_l f g x = list_apply g (f x)
let apply f x = f x
......
src/driver/driver.ml
View file @ 22e13e75
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Format
open Util
open Ident
open Ty
......@@ -24,7 +25,6 @@ open Term
open Decl
open Theory
open Task
open Register
open Driver_ast
open Call_provers
......@@ -32,9 +32,9 @@ open Call_provers
type error = string
exception Error of string
exception Error of error
let report = Format.pp_print_string
let report = pp_print_string
let error ?loc e = match loc with
| None -> raise (Error e)
......@@ -42,10 +42,10 @@ let error ?loc e = match loc with
let errorm ?loc f =
let buf = Buffer.create 512 in
let fmt = Format.formatter_of_buffer buf in
Format.kfprintf
let fmt = formatter_of_buffer buf in
kfprintf
(fun _ ->
Format.pp_print_flush fmt ();
pp_print_flush fmt ();
let s = Buffer.contents buf in
Buffer.clear buf;
error ?loc s)
......@@ -60,14 +60,14 @@ let global_substitute_fmt expr repl_fun text fmt =
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
Format.pp_print_string fmt (Str.string_after text start)
pp_print_string fmt (Str.string_after text start)
else
match opt_search_forward expr text startpos with
| None ->
Format.pp_print_string fmt (Str.string_after text start)
pp_print_string fmt (Str.string_after text start)
| Some pos ->
let end_pos = Str.match_end () in
Format.pp_print_string fmt (String.sub text start (pos - start));
pp_print_string fmt (String.sub text start (pos - start));
repl_fun text fmt;
replace end_pos (end_pos = pos)
in
......@@ -106,20 +106,12 @@ let syntax_arguments s print fmt l =
(** drivers *)
type driver_query = {
query_syntax : ident -> string option;
query_remove : ident -> bool;
query_tags : ident -> Sstr.t;
}
type printer = driver_query -> Format.formatter -> task -> unit
type driver = {
drv_env : Env.env;
drv_printer : printer option;
drv_printer : string option;
drv_prelude : string list;
drv_filename : string option;
drv_transform : task trans_reg;
drv_transform : string list;
drv_thprelude : string list Mid.t;
drv_tags : Sstr.t Mid.t;
drv_tags_cl : Sstr.t Mid.t;
......@@ -128,22 +120,9 @@ type driver = {
drv_remove_cl : Sid.t;
drv_regexps : (Str.regexp * Call_provers.prover_answer) list;
drv_exitcodes : (int * Call_provers.prover_answer) list;
drv_tag : int
}
(** register printers and transformations *)
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
let register_printer name printer = Hashtbl.replace printers name printer
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let transforms : (string, task trans_reg) Hashtbl.t = Hashtbl.create 17
let register_transform name trans = Hashtbl.replace transforms name trans
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let transforms_l : (string, task tlist_reg) Hashtbl.t = Hashtbl.create 17
let register_transform_l name trans = Hashtbl.replace transforms_l name trans
let list_transforms_l () = Hashtbl.fold (fun k _ ac -> k::ac) transforms_l []
(** parse a driver file *)
let load_plugin dir (byte,nat) =
......@@ -163,13 +142,13 @@ let load_file file =
let string_of_qualid thl idl =
String.concat "." thl ^ "." ^ String.concat "." idl
let load_driver env file =
let load_driver = let driver_tag = ref (-1) in fun env file ->
let prelude = ref [] in
let regexps = ref [] in
let exitcodes = ref [] in
let filename = ref None in
let printer = ref None in
let transform = ref identity in
let transform = ref [] in
let set_or_raise loc r v error = match !r with
| Some _ -> errorm ~loc "duplicate %s" error
......@@ -189,12 +168,8 @@ let load_driver env file =
| ExitCodeUnknown (s,t) -> add_to_list exitcodes (s, Unknown t)
| ExitCodeFailure (s,t) -> add_to_list exitcodes (s, Failure t)
| Filename s -> set_or_raise loc filename s "filename"
| Printer s -> begin
try set_or_raise loc printer (Hashtbl.find printers s) "printer"
with Not_found -> errorm ~loc "unknown printer %s" s end
| Transform s -> begin
try transform := compose !transform (Hashtbl.find transforms s)
with Not_found -> errorm ~loc "unknown transformation %s" s end
| Printer s -> set_or_raise loc printer s "printer"
| Transform s -> add_to_list transform s
| Plugin files -> load_plugin (Filename.dirname file) files
in
let f = load_file file in
......@@ -222,7 +197,8 @@ let load_driver env file =
if Mid.mem id !syntax then
errorm ~loc "duplicate syntax rule for %s symbol %s"
k (string_of_qualid !qualid q);
syntax := Mid.add id s !syntax
syntax := Mid.add id s !syntax;
remove := Sid.add id !remove
in
let add_tag c id s =
let mr = if c then tags_cl else tags in
......@@ -255,6 +231,8 @@ let load_driver env file =
List.iter (add_local th) trl
in
List.iter add_theory f.f_rules;
transform := List.rev !transform;
incr driver_tag;
{
drv_env = env;
drv_printer = !printer;
......@@ -269,15 +247,46 @@ let load_driver env file =
drv_remove_cl = !remove_cl;
drv_regexps = !regexps;
drv_exitcodes = !exitcodes;
drv_tag = !driver_tag;
}
(** query drivers *)
type driver_query = {
query_syntax : ident -> string option;
query_remove : ident -> bool;
query_tags : ident -> Sstr.t;
query_driver : driver;
query_lclone : task;
query_tag : int;
}
module Hsdq = Hashcons.Make (struct
type t = driver_query
let equal q1 q2 = q1.query_driver == q2.query_driver &&
q1.query_lclone == q2.query_lclone
let hash q = Hashcons.combine q.query_driver.drv_tag (task_tag q.query_lclone)
let tag n q = { q with query_tag = n }
end)
module Dq = StructMake (struct
type t = driver_query
let tag q = q.query_tag
end)
module Sdq = Dq.S
module Mdq = Dq.M
module Hdq = Dq.H
let get_tags map id = try Mid.find id map with Not_found -> Sstr.empty
let add_tags drv id acc = Sstr.union (get_tags drv.drv_tags_cl id) acc
let add_remove drv id acc = acc || Sid.mem id drv.drv_remove_cl
let query_driver drv clone =
let driver_query drv task =
let clone = task_clone task in
let htags = Hid.create 7 in
let query_tags id = try Hid.find htags id with Not_found ->
let r = try Mid.find id clone with Not_found -> Sid.empty in
......@@ -293,14 +302,30 @@ let query_driver drv clone =
let query_syntax id =
try Some (Mid.find id drv.drv_syntax) with Not_found -> None
in
{ query_syntax = query_syntax;
Hsdq.hashcons {
query_syntax = query_syntax;
query_remove = query_remove;
query_tags = query_tags }
query_tags = query_tags;
query_driver = drv;
query_lclone = last_clone task;
query_tag = -1 }
let query_syntax dq = dq.query_syntax
let query_remove dq = dq.query_remove
let query_tags dq = dq.query_tags
let query_driver dq = dq.query_driver
let query_env dq = dq.query_driver.drv_env
let query_clone dq = task_clone (dq.query_lclone)
let query_tag dq = dq.query_tag
(** apply drivers *)
let print_prelude drv used fmt =
let pr_pr s () = Format.fprintf fmt "%s@\n" s in
let get_transform drv = drv.drv_transform
let get_printer drv = drv.drv_printer
let get_env drv = drv.drv_env
let print_prelude drv task fmt =
let pr_pr s () = fprintf fmt "%s@\n" s in
List.fold_right pr_pr drv.drv_prelude ();
let seen = Hid.create 17 in
let rec print_prel th_name th =
......@@ -314,17 +339,8 @@ let print_prelude drv used fmt =
List.fold_right pr_pr prel ()
end
in
Mid.iter print_prel used;
Format.fprintf fmt "@."
let print_task drv fmt task =
let task = apply_env drv.drv_transform drv.drv_env task in
let printer = match drv.drv_printer with
| None -> errorm "no printer specified in the driver file"
| Some p -> p (query_driver drv (task_clone task))
in
print_prelude drv (task_used task) fmt;
Format.fprintf fmt "@[%a@]@?" printer task
Mid.iter print_prel (task_used task);
fprintf fmt "@."
let filename_regexp = Str.regexp "%\\(.\\)"
......@@ -352,12 +368,6 @@ let call_on_buffer ?debug ~command ~timelimit ~memlimit drv buffer =
Call_provers.call_on_buffer
?debug ~command ~timelimit ~memlimit ~regexps ~exitcodes ~filename buffer
let prove_task ?debug ~command ~timelimit ~memlimit drv task =
let buf = Buffer.create 1024 in
let fmt = Format.formatter_of_buffer buf in
print_task drv fmt task; Format.pp_print_flush fmt ();
call_on_buffer ?debug ~command ~timelimit ~memlimit drv buf
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
......
src/driver/driver.mli
View file @ 22e13e75
......@@ -38,44 +38,28 @@ val load_driver : env -> string -> driver
(** {2 query a driver} *)
val syntax_arguments : string -> (formatter -> 'a -> unit) ->
formatter -> 'a list -> unit
(** (syntax_argument templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** {2 register printers and transformations} *)
type driver_query = {
query_syntax : ident -> string option;
query_remove : ident -> bool;
query_tags : ident -> Sstr.t;
}
type driver_query
type printer = driver_query -> formatter -> task -> unit
val driver_query : driver -> task -> driver_query
val register_printer : string -> printer -> unit
val register_transform : string -> task Register.trans_reg -> unit
val register_transform_l : string -> task Register.tlist_reg -> unit
val list_printers : unit -> string list
val list_transforms : unit -> string list
val list_transforms_l : unit -> string list
val query_syntax : driver_query -> ident -> string option
val query_remove : driver_query -> ident -> bool
val query_tags : driver_query -> ident -> Sstr.t
val query_clone : driver_query -> Theory.clone_map
val query_driver : driver_query -> driver
val query_env : driver_query -> env
val query_tag : driver_query -> int
(** {2 use a driver} *)
val file_of_task : driver -> string -> string -> task -> string
(** file_of_task input_file theory_name task *)
val get_env : driver -> env
val get_printer : driver -> string option
val get_transform : driver -> string list
val print_task : driver -> formatter -> task -> unit
(** print a task *)
(** file_of_task input_file theory_name task *)
val file_of_task : driver -> string -> string -> task -> string
val prove_task :
?debug : bool ->
command : string ->
timelimit : int ->
memlimit : int ->
driver -> task -> unit -> Call_provers.prover_result
val print_prelude : driver -> task -> formatter -> unit
val call_on_buffer :
?debug : bool ->
......@@ -84,6 +68,13 @@ val call_on_buffer :
memlimit : int ->
driver -> Buffer.t -> unit -> Call_provers.prover_result
(** {2 syntax arguments} *)
val syntax_arguments : string -> (formatter -> 'a -> unit) ->
formatter -> 'a list -> unit
(** (syntax_argument templ print_arg fmt l) prints in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** {2 error reporting} *)
type error
......
src/driver/prover.ml 0 → 100644
View file @ 22e13e75
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
open Format
open Driver
open Register
(** error handling *)
type error = string
exception Error of error
let report = pp_print_string
let error e = raise (Error e)
let errorm f =
let buf = Buffer.create 512 in
let fmt = formatter_of_buffer buf in
kfprintf
(fun _ ->
pp_print_flush fmt ();
let s = Buffer.contents buf in
Buffer.clear buf;
error s)
fmt f
(** print'n'prove *)
exception NoPrinter
exception UnknownPrinter of string
exception UnknownTransform of string
let print_task drv fmt task =
let p = match get_printer drv with
| None -> errorm "no printer specified in the driver file"
| Some p -> p
in
let printer = try lookup_printer p with
Not_found -> errorm "unknown printer %s" p
in
let lookup t = try lookup_transform t with
Not_found -> errorm "unknown transformation %s" t
in
let transl = List.map lookup (get_transform drv) in
let apply task tr = Register.apply_driver tr drv task in
let task = List.fold_left apply task transl in
let printer = printer (driver_query drv task) in
print_prelude drv task fmt;
fprintf fmt "@[%a@]@?" printer task
let prove_task ?debug ~command ~timelimit ~memlimit drv task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
print_task drv fmt task; pp_print_flush fmt ();
call_on_buffer ?debug ~command ~timelimit ~memlimit drv buf
src/driver/prover.mli 0 → 100644
View file @ 22e13e75
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
val print_task : Driver.driver -> Format.formatter -> Task.task -> unit
val prove_task :
?debug : bool ->
command : string ->
timelimit : int ->
memlimit : int ->
Driver.driver -> Task.task -> unit -> Call_provers.prover_result
(** {2 error reporting} *)
type error
exception Error of error
val report : Format.formatter -> error -> unit
src/core/register.ml → src/driver/register.ml
View file @ 22e13e75
......@@ -17,22 +17,22 @@
(* *)
(**************************************************************************)
open Env
open Task
open Trans
open Driver
type 'a value = env option -> 'a
type use = Theory.use_map
type clone = Theory.clone_map
type query = driver_query
type 'a value = Env.env option -> driver option -> task -> 'a
type 'a registered = {
type 'a trans_reg = {
mutable value : 'a value;
generate : unit -> 'a value;
}
type 'a trans_reg = (task -> 'a) registered
type 'a tlist_reg = (task -> 'a list) registered
type use = Theory.use_map
type clone = Theory.clone_map
type 'a tlist_reg = 'a list trans_reg
let create gen = {
value = gen ();
......@@ -41,7 +41,7 @@ let create gen = {
exception ArgumentNeeded
let memo tag f =
let memo tag f =
let h = Hashtbl.create 7 in
function
| None -> raise ArgumentNeeded
......@@ -53,7 +53,8 @@ let memo tag f =
Hashtbl.add h t r;
r
let memo_env e = memo env_tag e
let memo_env e = memo Env.env_tag e
let memo_query q = memo query_tag q
let memo2 extract f =
let h = Hashtbl.create 7 in
......@@ -64,80 +65,95 @@ let memo2 extract f =
let r = f arg x in
Hashtbl.add h tag r; r
let memo_clone x = memo2 (fun t ->
let t = last_clone t in
task_clone t,task_tag t) x
let memo_use x = memo2 (fun t ->
let t = last_use t in
task_used t,task_tag t) x
let memo_task x = memo2 (fun t -> t,task_tag t) x
let store f =
let gen () =
let f0 _ task = Trans.apply (f ()) task in
f0 in
create gen
let store0 memo_env f =
let gen () =
let f0 () env task = Trans.apply (f () env) task in
memo_env (f0 ()) in
create gen
let store1 memo_env memo_arg2 f =
let gen () =
let f0 () env arg2 task = Trans.apply (f () env arg2) task in
let f1 () env = memo_arg2 (f0 () env) in
memo_env (f1 ()) in
create gen
let store2 memo_env memo_arg2 memo_arg3 f =
let gen () =
let f0 () env arg2 arg3 task = Trans.apply (f () env arg2 arg3) task in
let f1 () env arg2 = memo_arg3 (f0 () env arg2) in
let f2 () env = memo_arg2 (f1 () env) in
memo_env (f2 ()) in
create gen
let store_env f = store0 memo_env f
let store_clone f = store1 memo_env memo_clone f
let store_use f = store1 memo_env memo_use f
let store_task f = store1 memo_env memo_task f
let store_both f = store2 memo_env memo_use memo_clone f
let memo_use x = memo2 (fun t -> task_used t, task_tag (last_use t)) x
let memo_clone x = memo2 (fun t -> task_clone t, task_tag (last_clone t)) x
let memo_goal x = memo2 (fun t -> t, task_tag t) x
let query drv task = Util.option_map (fun d -> driver_query d task) drv
let gen_gen f () =
let f0 = Trans.apply (f ()) in
fun _ _ -> f0
let gen_env f () =
let f0 env = Trans.apply (f env) in
let f1 = memo_env f0 in
fun env _ -> f1 env
let gen_query f () =
let f0 query = Trans.apply (f query) in
let f1 = memo_query f0 in
fun _ drv task -> f1 (query drv task) task
let gen_arg memo_arg f () =
let f0 env arg = Trans.apply (f env arg) in
let f1 env = memo_arg (f0 env) in
let f2 = memo_env f1 in
fun env _ -> f2 env
let gen_full f () =
let f0 query goal = Trans.apply (f query goal) in
let f1 query = memo_goal (f0 query) in
let f2 = memo_query f1 in
fun _ drv task -> f2 (query drv task) task
let gen_both f () =
let f0 env use clone = Trans.apply (f env use clone) in
let f1 env use = memo_clone (f0 env use) in
let f2 env = memo_use (f1 env) in
let f3 = memo_env f2 in
fun env _ -> f3 env
let store f = create (gen_gen f)
let store_env f = create (gen_env f)
let store_goal f = create (gen_arg memo_goal f)
let store_clone f = create (gen_arg memo_clone f)
let store_use f = create (gen_arg memo_use f)
let store_both f = create (gen_both f)
let store_query f = create (gen_query f)
let store_full f = create (gen_full f)
let apply reg = reg.value None None
let apply_env reg env = reg.value (Some env) None
let apply_driver reg drv = reg.value (Some (get_env drv)) (Some drv)
let clear reg = reg.value <- reg.generate ()
let apply0 reg = reg.value
let conv_res conv reg1 =
let app f env drv task = conv (f env drv task) in
let gen () = app (reg1.generate ()) in
{ value = app reg1.value; generate = gen }
let apply_env reg env = apply0 reg (Some env)
let apply reg = apply0 reg None
let combine comb reg1 reg2 =
let app f1 f2 env drv = comb (f1 env drv) (f2 env drv) in
let gen () = app (reg1.generate ()) (reg2.generate ()) in
{ value = app reg1.value reg2.value; generate = gen }
let clear reg = reg.value <- reg.generate ()
let singleton reg = conv_res (fun x -> [x]) reg
let combine comb reg1 reg2 =
let gen () =
let reg1 = reg1.generate () in
let reg2 = reg2.generate () in
fun env -> comb (reg1 env) (reg2 env) in
create gen
let identity = store (fun () -> Trans.identity)
let identity_l = store (fun () -> Trans.identity_l)
let compose r1 r2 = combine (fun t1 t2 x -> t2 (t1 x)) r1 r2
<