Commit dd3aac24 authored by Andrei Paskevich's avatar Andrei Paskevich

Reworking tags and transformations, stage 3:

- everything is converted to the new shiny way of doing things.
  Well, everything except Gappa, which seems very unifinished anyway,
  and Encoding_instantiate, which is too complex and would like to 
  update it with François.

Also, I commented a little piece of exception reporting in manager/,
will see it with Claude.

THIS IS STILL A WORK IN PROGRESS!
Please inform me about any bugs, ugly APIs, and proposed corrections.

All the non-implemented things, mentioned in the previous commit
message are still in the TODO list and will be done soon.
parent 5c650119
......@@ -100,7 +100,7 @@ LIB_CORE = ident ty term pattern decl theory task pretty env printer trans
LIB_PARSER = ptree parser lexer denv typing
LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
register prover whyconf
whyconf
LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
split_conjunction encoding_decorate encoding_decorate_mono \
......
......@@ -3,7 +3,8 @@
prelude "# this is a prelude for Gappa"
printer "gappa"
(* printer "gappa" *)
printer "why3"
filename "%f-%t-%g.gappa"
valid 0
......
......@@ -5,7 +5,7 @@ DIR=drivers/
for prover in z3 cvc3; do
for what in "" _goal _mono _def; do
for complete in "" _nbp; do
cat ${DIR}${prover}.drv |sed -e "s/transformation \"encoding_decorate\"/transformation \"encoding_instantiate$what$complete\"/" > ${DIR}${prover}_inst${what}${complete}.drv
cat ${DIR}${prover}.drv |sed -e "s/transformation \"encoding_decorate\"/(* transformation \"encoding_instantiate$what$complete\" *)/" > ${DIR}${prover}_inst${what}${complete}.drv
done
done
done
......@@ -30,10 +30,11 @@ open Task
type prelude = string list
type prelude_map = prelude Mid.t
type syntax_map = string Mid.t
type 'a pp = formatter -> 'a -> unit
type printer = prelude -> prelude_map -> task pp
type printer = prelude -> prelude_map -> syntax_map -> task pp
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
......@@ -118,32 +119,32 @@ let print_th_prelude task fmt pm =
let prel = try Mid.find th.th_name pm with Not_found -> [] in
print_prelude fmt prel) th_used
exception KnownTypeSyntax of tysymbol
exception KnownLogicSyntax of lsymbol
let add_ts_syntax ts s sm =
check_syntax s (List.length ts.ts_args);
if Mid.mem ts.ts_name sm then raise (KnownTypeSyntax ts);
Mid.add ts.ts_name s sm
let add_ls_syntax ls s sm =
check_syntax s (List.length ls.ls_args);
if Mid.mem ls.ls_name sm then raise (KnownLogicSyntax ls);
Mid.add ls.ls_name s sm
let meta_remove_type = "remove_type"
let meta_remove_logic = "remove_logic"
let meta_remove_prop = "remove_prop"
let meta_syntax_type = "syntax_type"
let meta_syntax_logic = "syntax_logic"
let () =
register_meta meta_remove_type [MTtysymbol];
register_meta meta_remove_logic [MTlsymbol];
register_meta meta_remove_prop [MTprsymbol];
register_meta meta_syntax_type [MTtysymbol; MTstring];
register_meta meta_syntax_logic [MTlsymbol; MTstring]
register_meta meta_remove_prop [MTprsymbol]
let remove_type ts = create_meta meta_remove_type [MAts ts]
let remove_logic ls = create_meta meta_remove_logic [MAls ls]
let remove_prop pr = create_meta meta_remove_prop [MApr pr]
let syntax_type ts s =
check_syntax s (List.length ts.ts_args);
create_meta meta_syntax_type [MAts ts; MAstr s]
let syntax_logic ls s =
check_syntax s (List.length ls.ls_args);
create_meta meta_syntax_logic [MAls ls; MAstr s]
let get_remove_set task =
let add td s = match td.td_node with
| Meta (_,[MARid id]) -> Sid.add id s
......@@ -155,16 +156,6 @@ let get_remove_set task =
let s = Stdecl.fold add (find_meta task meta_remove_prop).tds_set s in
s
let get_syntax_map task =
let add td m = match td.td_node with
| Meta (_,[MARid id; MARstr s]) -> Mid.add id s m
| _ -> assert false
in
let m = Mid.empty in
let m = Stdecl.fold add (find_meta task meta_syntax_type).tds_set m in
let m = Stdecl.fold add (find_meta task meta_syntax_logic).tds_set m in
m
(** {2 exceptions to use in transformations and printers} *)
exception UnsupportedType of ty * string
......@@ -203,6 +194,12 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
fprintf fmt "Printer '%s' is already registered" s
| UnknownPrinter s ->
fprintf fmt "Unknown printer '%s'" s
| KnownTypeSyntax ts ->
fprintf fmt "Syntax for type symbol %a is already defined"
Pretty.print_ts ts
| KnownLogicSyntax ls ->
fprintf fmt "Syntax for logical symbol %a is already defined"
Pretty.print_ls ls
| BadSyntaxIndex i ->
fprintf fmt "Bad argument index %d, must start with 1" i
| BadSyntaxArity (i1,i2) ->
......
......@@ -29,9 +29,11 @@ open Task
type prelude = string list
type prelude_map = prelude Mid.t
type syntax_map = string Mid.t
type 'a pp = Format.formatter -> 'a -> unit
type printer = prelude -> prelude_map -> task pp
type printer = prelude -> prelude_map -> syntax_map -> task pp
val register_printer : string -> printer -> unit
......@@ -48,18 +50,14 @@ val meta_remove_type : string
val meta_remove_logic : string
val meta_remove_prop : string
val meta_syntax_type : string
val meta_syntax_logic : string
val remove_type : tysymbol -> tdecl
val remove_logic : lsymbol -> tdecl
val remove_prop : prsymbol -> tdecl
val syntax_type : tysymbol -> string -> tdecl
val syntax_logic : lsymbol -> string -> tdecl
val get_remove_set : task -> Sid.t
val get_syntax_map : task -> string Mid.t
val add_ts_syntax : tysymbol -> string -> syntax_map -> syntax_map
val add_ls_syntax : lsymbol -> string -> syntax_map -> syntax_map
val syntax_arguments : string -> 'a pp -> 'a list pp
(** (syntax_arguments templ print_arg fmt l) prints in the formatter fmt
......@@ -72,12 +70,12 @@ exception UnsupportedExpr of expr * string
exception UnsupportedDecl of decl * string
exception NotImplemented of string
val unsupportedType : ty -> string -> unit
val unsupportedTerm : term -> string -> unit
val unsupportedFmla : fmla -> string -> unit
val unsupportedExpr : expr -> string -> unit
val unsupportedDecl : decl -> string -> unit
val notImplemented : string -> unit
val unsupportedType : ty -> string -> 'a
val unsupportedTerm : term -> string -> 'a
val unsupportedFmla : fmla -> string -> 'a
val unsupportedExpr : expr -> string -> 'a
val unsupportedDecl : decl -> string -> 'a
val notImplemented : string -> 'a
(** {3 functions that catch inner error} *)
......@@ -85,7 +83,7 @@ exception Unsupported of string
(** This exception must be raised only inside a call
of one of the catch_* functions below *)
val unsupported : string -> unit
val unsupported : string -> 'a
val catch_unsupportedType : (ty -> 'a) -> (ty -> 'a)
(** [catch_unsupportedType f] return a function which applied on [arg]:
......
......@@ -47,7 +47,9 @@ type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mstr.t
let cm_find cm th = try Mid.find th.th_name cm with Not_found -> empty_tds
let mm_find mm t = try Mstr.find t mm with Not_found -> empty_tds
let mm_find mm t =
try Mstr.find t mm with Not_found -> ignore (lookup_meta t); empty_tds
let cm_add cm th td = Mid.add th.th_name (tds_add td (cm_find cm th)) cm
let mm_add mm t td = Mstr.add t (tds_add td (mm_find mm t)) mm
......@@ -202,40 +204,27 @@ let task_tdecls = task_fold (fun acc td -> td::acc) []
let task_decls = task_fold (fun acc td ->
match td.td_node with Decl d -> d::acc | _ -> acc) []
(* TO BE REMOVED *)
let old_task_clone task =
Mid.fold (fun _ x -> Stdecl.fold (function
| { td_node = Clone (_,cl) } ->
Mid.fold (fun id id' m ->
let s = try Mid.find id' m with Not_found -> Sid.empty in
Mid.add id' (Sid.add id s) m) cl
| _ -> assert false) x.tds_set) (task_clone task) Mid.empty
let old_task_use task =
Mid.fold (fun _ x -> Stdecl.fold (function
| { td_node = Clone (th,cl) } -> (fun m ->
if Mid.is_empty cl then Mid.add th.th_name th m else m)
| _ -> assert false) x.tds_set) (task_clone task) Mid.empty
(* special selector for metaproperties of a single ident *)
let rec last_use task = match task with
| Some {task_decl={td_node=Clone(_,cl)}} when Mid.is_empty cl -> task
| Some {task_prev=task} -> last_use task
| None -> None
exception NotTaggingMeta of string
let rec last_clone task = match task with
| Some {task_decl={td_node=Clone _}} -> task
| Some {task_prev=task} -> last_clone task
| None -> None
let find_meta_ids t tds acc =
begin match lookup_meta t with
| [MTtysymbol|MTlsymbol|MTprsymbol] -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, [MARid id]) when s = t -> Sid.add id acc
| _ -> assert false) tds.tds_set acc
(* Exception reporting *)
let () = Exn_printer.register
begin fun fmt exn -> match exn with
let () = Exn_printer.register (fun fmt exn -> match exn with
| LemmaFound -> Format.fprintf fmt "Task cannot contain a lemma"
| SkipFound -> Format.fprintf fmt "Task cannot contain a skip"
| GoalFound -> Format.fprintf fmt "The task already ends with a goal"
| GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
| _ -> raise exn
end
| NotTaggingMeta s ->
Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" s
| _ -> raise exn)
......@@ -93,12 +93,11 @@ val task_decls : task -> decl list
val task_goal : task -> prsymbol
(* TO BE REMOVED *)
(* special selector for metaproperties of a single ident *)
val old_task_clone : task -> Sid.t Mid.t
val old_task_use : task -> theory Mid.t
val last_clone : task -> task
val last_use : task -> task
exception NotTaggingMeta of string
val find_meta_ids : string -> tdecl_set -> Sid.t -> Sid.t
(* exceptions *)
......
......@@ -74,6 +74,9 @@ val on_theories_metas : theory list -> string list ->
(** {2 Registration} *)
exception UnknownTrans of string
exception KnownTrans of string
val register_transform : string -> (Env.env -> task trans) -> unit
val register_transform_l : string -> (Env.env -> task tlist) -> unit
......
This diff is collapsed.
......@@ -19,49 +19,20 @@
(** Manage Why drivers *)
open Format
open Util
open Ident
open Task
open Trans
open Env
(** {2 create a driver} *)
type driver
val load_driver : env -> string -> driver
val load_driver : Env.env -> string -> driver
(** loads a driver from a file
@param env TODO
@param string driver file name
*)
(** {2 query a driver} *)
type driver_query
val driver_query : driver -> task -> driver_query
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 -> Sid.t Mid.t
val query_driver : driver_query -> driver
val query_env : driver_query -> env
val query_tag : driver_query -> int
val print_global_prelude : driver_query -> formatter -> unit
val print_theory_prelude : driver_query -> ident -> formatter -> unit
val print_full_prelude : driver_query -> task -> formatter -> unit
(** {2 use a driver} *)
val get_env : driver -> env
val get_printer : driver -> string option
val get_transform : driver -> string list
(** file_of_task input_file theory_name task *)
val file_of_task : driver -> string -> string -> task -> string
val file_of_task : driver -> string -> string -> Task.task -> string
val call_on_buffer :
?debug : bool ->
......@@ -70,18 +41,14 @@ 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 *)
val print_task :
?debug : bool ->
driver -> Format.formatter -> Task.task -> unit
(** {2 error reporting} *)
type error
exception Error of error
val report : formatter -> error -> unit
val prove_task :
?debug : bool ->
command : string ->
?timelimit : int ->
?memlimit : int ->
driver -> Task.task -> unit -> Call_provers.prover_result
(**************************************************************************)
(* *)
(* 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 () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error
| _ -> raise exn)
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 ?(debug=false) 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 t, lookup_transform t with
Not_found -> errorm "unknown transformation %s" t
in
let transl = List.map lookup (get_transform drv) in
let apply task (s, tr) =
try
Register.apply_driver tr drv task
with e when not debug ->
Format.eprintf "failure in transformation %s@." s;
raise e
in
let task = List.fold_left apply task transl in
let printer = printer (driver_query drv task) in
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 ?debug drv fmt task; pp_print_flush fmt ();
call_on_buffer ?debug ~command ?timelimit ?memlimit drv buf
(**************************************************************************)
(* *)
(* 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. *)
(* *)
(**************************************************************************)
(** Apply printers and registered transformations mentionned in drivers *)
val print_task :
?debug : bool ->
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
(**************************************************************************)
(* *)
(* 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 Task
open Trans
open Driver
type query = driver_query
type clone = Ident.Sid.t Ident.Mid.t
type use = Theory.theory Ident.Mid.t
type 'a value = Env.env option -> driver option -> task -> 'a
type 'a trans_reg = {
mutable value : 'a value;
generate : unit -> 'a value;
}
type 'a tlist_reg = 'a list trans_reg
let create gen = {
value = gen ();
generate = gen;
}
module WHenv = Hashweak.Make (struct
type t = Env.env
let tag = Env.env_tag
end)
module WHquery = Hashweak.Make (struct
type t = driver_query
let tag = query_tag
end)
module WHtask = Hashweak.Make (struct
type t = task_hd
let tag t = t.task_tag
end)
exception ArgumentNeeded
let memo_env fn =
let fn = WHenv.memoize 7 fn in function
| None -> raise ArgumentNeeded
| Some env -> fn env
let memo_query fn =
let fn = WHquery.memoize 7 fn in function
| None -> raise ArgumentNeeded
| Some drv -> fun task -> fn (driver_query drv task)
let memo_use fn =
let fn task = fn (old_task_use task) in
let fn = WHtask.memoize_option 63 fn in
fun task -> fn (last_use task)
let memo_clone fn =
let fn task = fn (old_task_clone task) in
let fn = WHtask.memoize_option 63 fn in
fun task -> fn (last_clone task)
let memo_goal fn = WHtask.memoize_option 7 fn
let gen_task f () =
let f0 = Trans.apply (f ()) in
fun _ _ task -> f0 task
let gen_env f () =
let f0 env = Trans.apply (f env) in
let f1 = memo_env f0 in
fun env _ task -> f1 env task
let gen_query f () =
let f0 query = Trans.apply (f query) in
let f1 = memo_query f0 in
fun _ drv task -> f1 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 _ task -> f2 env task task
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 drv task 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 _ task -> f3 env task task task
let store f = create (gen_task 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 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 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 singleton reg = conv_res (fun x -> [x]) reg
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
let compose_l r1 r2 = combine (fun t1 t2 x -> Util.list_apply t2 (t1 x)) r1 r2
(** register printers and transformations *)
type printer = query -> Format.formatter -> task -> unit
let printers : (string, printer) Hashtbl.t = Hashtbl.create 17
let transforms : (string, task trans_reg) Hashtbl.t = Hashtbl.create 17
let transforms_l : (string, task tlist_reg) Hashtbl.t = Hashtbl.create 17
let register_printer = Hashtbl.replace printers
let register_transform = Hashtbl.replace transforms
let register_transform_l = Hashtbl.replace transforms_l
let lookup_printer = Hashtbl.find printers
let lookup_transform = Hashtbl.find transforms
let lookup_transform_l = Hashtbl.find transforms_l
let list_printers () = Hashtbl.fold (fun k _ acc -> k::acc) printers []
let list_transforms () = Hashtbl.fold (fun k _ acc -> k::acc) transforms []
let list_transforms_l () = Hashtbl.fold (fun k _ acc -> k::acc) transforms_l []
(** exception to use in a printer and transformation *)
open Ty
open Term
open Decl
type error =
| UnsupportedType of ty * string
| UnsupportedExpr of expr * string
| UnsupportedDecl of decl * string
| NotImplemented of string
exception Error of error
let error e = raise (Error e)
let unsupportedType e s = error (UnsupportedType (e,s))
let unsupportedTerm e s = error (UnsupportedExpr (Term e,s))
let unsupportedFmla e s = error (UnsupportedExpr (Fmla e,s))
let unsupportedExpr e s = error (UnsupportedExpr (e,s))
let unsupportedDecl e s = error (UnsupportedDecl (e,s))
let notImplemented s = error (NotImplemented s)
let report fmt = function
| UnsupportedType (e,s) ->
let msg = "This type isn't supported" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_ty e s
| UnsupportedExpr (e,s) ->
let msg = "This expression isn't supported" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_expr e s
| UnsupportedDecl (d,s) ->
let msg = "This declaration isn't supported" in
Format.fprintf fmt
"@[<hov 3> %s:@\n%a@\n%s@]@\n" msg Pretty.print_decl d s
| NotImplemented (s) ->
Format.fprintf fmt "@[<hov 3> Unimplemented feature:@\n%s@]@\n" s
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Error error -> report fmt error