Skip to content

GitLab

why3
why3
Commit ebe0622b authored by Francois Bobot's avatar Francois Bobot
Browse files
Options

Mise à jour de Register et Driver pour le nouveau task

parent babd2215
Hide whitespace changes
Inline Side-by-side
Showing with 207 additions and 153 deletions
src/core/register.ml
View file @ ebe0622b
......@@ -21,15 +21,18 @@ open Env
open Task
open Trans
type 'a value = env option -> (*clone option ->*) 'a
type 'a value = env option -> 'a
type 'a registered = {
mutable value : 'a value;
generate : unit -> 'a value;
}
type 'a trans_reg = 'a trans registered
type 'a tlist_reg = 'a tlist registered
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
let create gen = {
value = gen ();
......@@ -38,7 +41,9 @@ let create gen = {
exception ArgumentNeeded
let memo f tag h = function
let memo tag f =
let h = Hashtbl.create 7 in
function
| None -> raise ArgumentNeeded
| Some x ->
let t = tag x in
......@@ -48,33 +53,67 @@ let memo f tag h = function
Hashtbl.add h t r;
r
let memo0 tag f = memo f tag (Hashtbl.create 7)
let memo_env e = memo env_tag e
let memo2 extract f =
let h = Hashtbl.create 7 in
fun x ->
let arg,tag = extract x in
try Hashtbl.find h tag
with Not_found ->
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 unused0 f = fun _ -> f
let store0 memo_env f =
let gen () =
let f0 () env task = Trans.apply (f () env) task in
memo_env (f0 ()) in
create gen
(*
let cl_tag cl = cl.cl_tag
*)
let store0 memo_env (*memo_cl*) f =
let store1 memo_env memo_arg2 f =
let gen () =
(*
let f2 = memo_env (f ()) in
fun env -> memo_cl (f2 env)
*)
memo_env (f ())
in
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 store f = store0 unused0 (*unused0 *) f
let store_env f = store0 (memo0 env_tag) (*unused0 *) f
let store_clone f = store0 (memo0 env_tag) (*(memo0 cl_tag)*) f
let apply0 reg env (*clone*) = Trans.apply (reg.value env (*clone*))
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 apply_clone reg env clone = apply0 reg (Some env) (Some clone)*)
let apply_env reg env = apply0 reg (Some env) (*None*)
let apply reg = apply0 reg None (*None*)
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 apply0 reg = reg.value
let apply_env reg env = apply0 reg (Some env)
let apply reg = apply0 reg None
let clear reg = reg.value <- reg.generate ()
......@@ -82,19 +121,22 @@ let combine comb reg1 reg2 =
let gen () =
let reg1 = reg1.generate () in
let reg2 = reg2.generate () in
fun env (*cl*) -> comb (reg1 env (*cl*)) (reg2 env (*cl*)) in
fun env -> comb (reg1 env) (reg2 env) in
create gen
let compose r1 r2 = combine (fun t1 t2 -> Trans.compose t1 t2) r1 r2
let compose_l r1 r2 = combine (fun t1 t2 -> Trans.compose_l t1 t2) r1 r2
let compose r1 r2 = combine (fun t1 t2 x -> t2 (t1 x)) r1 r2
let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
let compose_l r1 r2 = combine (fun t1 t2 x -> list_apply t2 (t1 x)) r1 r2
let conv_res conv reg1 =
let gen () =
let reg1 = reg1.generate () in
fun env (*cl*) -> conv (reg1 env (*cl*)) in
fun env -> conv (reg1 env) in
create gen
let singleton reg = conv_res Trans.singleton reg
let singleton reg = conv_res (fun f x -> [f x]) reg
let identity = store (fun () -> Trans.identity)
let identity_l = store (fun () -> Trans.identity_l)
......
src/core/register.mli
View file @ ebe0622b
......@@ -24,8 +24,16 @@ open Trans
type 'a trans_reg
type 'a tlist_reg = 'a list trans_reg
val store : (unit -> 'a trans) -> 'a trans_reg
val store_env : (unit -> env -> 'a trans) -> 'a trans_reg
type clone = Theory.clone_map
type use = Theory.use_map
val store : (unit -> 'a trans) -> 'a trans_reg
val store_env : (unit -> env -> 'a trans) -> 'a trans_reg
val store_clone : (unit -> env -> clone -> 'a trans) -> 'a trans_reg
val store_use : (unit -> env -> use -> 'a trans) -> 'a trans_reg
val store_both : (unit -> env -> use -> clone -> 'a trans) -> 'a trans_reg
val store_task : (unit -> env -> task -> 'a trans) -> 'a trans_reg
(*
val store_clone : (unit -> env -> clone -> 'a trans) -> 'a trans_reg
*)
......
src/core/task.ml
View file @ ebe0622b
......@@ -42,6 +42,10 @@ and tdecl =
| Use of theory
| Clone of theory * (ident * ident) list
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)
module Task = struct
type t = task_hd
......
src/core/task.mli
View file @ ebe0622b
......@@ -41,6 +41,10 @@ and tdecl = private
| Use of theory
| Clone of theory * (ident * ident) list
val task_clone : task -> clone_map
val task_used : task -> use_map
val task_tag : task -> int
(* constructors *)
val add_tdecl : task -> tdecl -> task
......
src/driver/driver.ml
View file @ ebe0622b
......@@ -123,17 +123,20 @@ let print_translation fmt = function
| Tag s -> fprintf fmt "tag %a"
(Pp.print_iter1 Sstr.iter Pp.comma Pp.string) s
type printer = driver -> formatter -> task -> unit
and raw_driver = {
drv_printer : printer option;
drv_prover : Call_provers.prover;
drv_prelude : string list;
drv_filename : string option;
drv_transforms : task tlist_reg;
drv_rules : theory_rules list;
type printer = (ident -> translation) -> formatter -> task -> unit
and driver = {
drv_env : env;
drv_printer : printer option;
drv_prover : Call_provers.prover;
drv_prelude : string list;
drv_filename : string option;
drv_transforms : task tlist_reg;
drv_thprelude : string list Mid.t;
drv_translations : (translation * translation) Mid.t
}
(*
and driver = {
drv_raw : raw_driver;
drv_clone : Theory.clone_map;
......@@ -145,7 +148,7 @@ and driver = {
drv_theory : (translation * translation) Hid.t;
drv_with_task : translation Hid.t;
}
*)
(*
let print_driver fmt driver =
......@@ -223,28 +226,28 @@ let check_syntax loc s len =
i len) s
let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
let load_rules env (premap,tmap) {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in
let th = try
find_theory env qfile id
with Env.TheoryNotFound (l,s) ->
errorm ~loc "theory %s.%s not found" (String.concat "." l) s
in
let add_htheory cloned id t =
let add_htheory tmap cloned id t =
try
let t2,t3 = Hid.find driver.drv_theory id in
let t2,t3 = Mid.find id tmap 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
Mid.add id t23 tmap
with Not_found ->
let t23 = if cloned then (Tag Sstr.empty),t else t,(Tag Sstr.empty) in
Hid.add driver.drv_theory id t23 in
let add = function
Mid.add id t23 tmap in
let add (premap,tmap) = function
| Rremove (c,(loc,q)) ->
begin
try
add_htheory c
premap,add_htheory tmap c
(ns_find_pr th.th_export q).pr_name Remove
with Not_found -> errorm ~loc "Unknown axioms %s"
(string_of_qualid qualid q)
......@@ -254,7 +257,7 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
try
let ls = ns_find_ls th.th_export q in
check_syntax loc s (List.length ls.ls_args);
add_htheory false ls.ls_name (Syntax s)
premap,add_htheory tmap false ls.ls_name (Syntax s)
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
end
......@@ -263,14 +266,14 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
try
let ts = ns_find_ts th.th_export q in
check_syntax loc s (List.length ts.ts_args);
add_htheory false ts.ts_name (Syntax s)
premap,add_htheory tmap 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 (ns_find_ls th.th_export q).ls_name
premap,add_htheory tmap c (ns_find_ls th.th_export q).ls_name
(Tag (Sstr.singleton s))
with Not_found -> errorm ~loc "Unknown logic %s"
(string_of_qualid qualid q)
......@@ -278,7 +281,7 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagty (c,(loc,q),s) ->
begin
try
add_htheory c (ns_find_ts th.th_export q).ts_name
premap,add_htheory tmap c (ns_find_ts th.th_export q).ts_name
(Tag (Sstr.singleton s))
with Not_found -> errorm ~loc "Unknown type %s"
(string_of_qualid qualid q)
......@@ -286,19 +289,19 @@ let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
| Rtagpr (c,(loc,q),s) ->
begin
try
add_htheory c (ns_find_pr th.th_export q).pr_name
premap,add_htheory tmap c (ns_find_pr th.th_export q).pr_name
(Tag (Sstr.singleton s))
with Not_found -> errorm ~loc "Unknown proposition %s"
(string_of_qualid qualid q)
end
| Rprelude (loc,s) ->
let l =
try Hid.find driver.drv_thprelude th.th_name
try Mid.find th.th_name premap
with Not_found -> []
in
Hid.replace driver.drv_thprelude th.th_name (s::l)
Mid.add th.th_name (s::l) premap,tmap
in
List.iter add trl
List.fold_left add (premap,tmap) trl
let load_driver file env =
let f = load_file file in
......@@ -344,33 +347,40 @@ let load_driver file env =
)
identity_l transformations in
let transforms = trans ltransforms in
{ drv_printer = !printer;
drv_prover = {Call_provers.pr_call_stdin = !call_stdin;
let (premap,tmap) =
List.fold_left (load_rules env) (Mid.empty,Mid.empty) f.f_rules in
{
drv_env = env;
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;
drv_transforms = transforms;
drv_rules = f.f_rules;
drv_prelude = !prelude;
drv_filename = !filename;
drv_transforms = transforms;
drv_thprelude = premap;
drv_translations = tmap
}
(** querying drivers *)
let query_ident drv id =
try
Hid.find drv.drv_with_task id
with Not_found ->
let r = try
Mid.find id drv.drv_clone
with Not_found -> Sid.empty in
let tr = try fst (Hid.find drv.drv_theory id)
with Not_found -> Tag Sstr.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_task id tr;
tr
let query_ident drv clone =
let h = Hid.create 7 in
fun id ->
try
Hid.find h id
with Not_found ->
let r = try
Mid.find id clone
with Not_found -> Sid.empty in
let tr = try fst (Mid.find id drv.drv_translations)
with Not_found -> Tag Sstr.empty in
let tr = Sid.fold
(fun id acc -> try translation_union acc
(snd (Mid.find id drv.drv_translations))
with Not_found -> acc) r tr in
Hid.add h id tr;
tr
let syntax_arguments s print fmt l =
let args = Array.of_list l in
......@@ -383,48 +393,36 @@ let syntax_arguments s print fmt l =
let apply_transforms drv =
(* apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone *)
apply_env drv.drv_raw.drv_transforms drv.drv_env
let cook_driver env clone used drv =
let drv = { drv_raw = drv;
drv_clone = clone;
drv_used = used;
drv_env = env;
drv_thprelude = Hid.create 17;
drv_theory = Hid.create 17;
drv_with_task = Hid.create 17} in
List.iter (load_rules env drv) drv.drv_raw.drv_rules;
drv
apply_env drv.drv_transforms drv.drv_env
let print_prelude drv fmt =
let print_prelude drv used fmt =
let pr_pr s () = fprintf fmt "%s@\n" s in
List.fold_right pr_pr drv.drv_raw.drv_prelude ();
List.fold_right pr_pr drv.drv_prelude ();
let seen = Hid.create 17 in
let rec print_prel th_name th =
if Hid.mem seen th_name then () else begin
Hid.add seen th_name ();
Mid.iter print_prel th.th_used;
let prel =
try Hid.find drv.drv_thprelude th_name
try Mid.find th_name drv.drv_thprelude
with Not_found -> []
in
List.fold_right pr_pr prel ()
end
in
Mid.iter print_prel drv.drv_used;
Mid.iter print_prel used;
fprintf fmt "@."
let print_task drv fmt task = match drv.drv_raw.drv_printer with
let print_task drv fmt task = match drv.drv_printer with
| None -> errorm "no printer"
| Some f ->
print_prelude drv fmt;
f drv fmt task
print_prelude drv (task_used task) fmt;
f (query_ident drv (task_clone task)) fmt task
let regexp_filename = Str.regexp "%\\([a-z]\\)"
let filename_of_goal drv filename theory_name task =
match drv.drv_raw.drv_filename with
match drv.drv_filename with
| None -> errorm "no filename syntax given"
| Some f ->
let pr_name = (task_goal task).pr_name in
......@@ -442,14 +440,14 @@ let file_printer =
[]
let call_prover_on_file ?debug ?timeout drv filename =
Call_provers.on_file drv.drv_raw.drv_prover filename
Call_provers.on_file drv.drv_prover filename
let call_prover_on_formatter ?debug ?timeout ?filename drv ib =
Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_raw.drv_prover ib
Call_provers.on_formatter ?debug ?timeout ?filename drv.drv_prover ib
let call_prover ?debug ?timeout drv task =
let filename =
match drv.drv_raw.drv_filename with
match drv.drv_filename with
| None -> None
| Some _ -> Some (filename_of_goal drv "why" "call_prover" task) in
let formatter fmt = print_task drv fmt task in
......
src/driver/driver.mli
View file @ ebe0622b
......@@ -25,15 +25,9 @@ open Env
(** creating drivers *)
type raw_driver
val load_driver : string -> env -> raw_driver
(** cooked driver *)
type driver
val cook_driver :
env -> Theory.clone_map -> Theory.use_map -> raw_driver -> driver
val load_driver : string -> env -> driver
(** querying drivers *)
......@@ -42,14 +36,13 @@ type translation =
| Syntax of string
| Tag of Util.Sstr.t
val query_ident : driver -> ident -> translation
val syntax_arguments : string -> (formatter -> 'a -> unit) ->
formatter -> 'a list -> unit
(* syntax_argument templ print_arg fmt l print in the formatter fmt
the list l using the template templ and the printer print_arg *)
(** registering printers *)
type printer = driver -> formatter -> task -> unit
type printer = (ident -> translation) -> formatter -> task -> unit
val register_printer : string -> printer -> unit
......@@ -65,7 +58,7 @@ val list_transforms : unit -> string list
val apply_transforms : driver -> task -> task list
(** print_task *)
val print_task : printer
val print_task : driver -> formatter -> task -> unit
val filename_of_goal : driver -> string -> string -> task -> string
(* filename_of_goal filename theory_name ctxt *)
......
src/main.ml
View file @ ebe0622b
......@@ -170,13 +170,17 @@ let transform env l =
let extract_goals ?filter =
fun env drv acc th ->
fun env acc th ->
let l = split_theory th filter in
let l = List.rev_map (fun task ->
let cl = Util.option_apply Ident.Mid.empty (fun t -> t.task_clone) task in
let us = Util.option_apply Ident.Mid.empty (fun t -> t.task_used) task in
let us = Ident.Mid.add th.th_name th us in
let drv = Driver.cook_driver env cl us drv in (th,task,drv)) l in
let l = List.rev_map
(fun task ->
(* let cl =
Util.option_apply Ident.Mid.empty (fun t -> t.task_clone) task in *)
(* let us =
Util.option_apply Ident.Mid.empty (fun t -> t.task_used) task in *)
(* let us = Ident.Mid.add th.th_name th us in *)
(* let drv = Driver.cook_driver env cl us drv in *)
(th,task)) l in
List.rev_append l acc
let file_sanitizer = None (* We should remove which character? *)
......@@ -191,9 +195,9 @@ let print_theory_namespace fmt th =
let do_goals env drv src_filename_printer dest_filename_printer file goals =
(* Apply transformations *)
let goals = List.fold_left
(fun acc (th,task,drv) ->
(fun acc (th,task) ->
List.rev_append
(List.map (fun e -> (th,e,drv))
(List.map (fun e -> (th,e))
(Driver.apply_transforms drv task)
) acc) [] goals
in
......@@ -210,7 +214,7 @@ let do_goals env drv src_filename_printer dest_filename_printer file goals =
with Invalid_argument _ -> file in
Ident.string_unique src_filename_printer file in
List.iter
(fun (th,task,drv) ->
(fun (th,task) ->
let dest =
Driver.filename_of_goal drv
file th.th_name.Ident.id_short task in
......@@ -235,7 +239,7 @@ let do_goals env drv src_filename_printer dest_filename_printer file goals =
let fmt = if file = "-" then std_formatter
else formatter_of_out_channel (open_out file)
in
let print_task fmt (th,task,drv) =
let print_task fmt (th,task) =
fprintf fmt "@[%a@]" (Driver.print_task drv) task
in
let print_zero fmt () = fprintf fmt "\000@?" in
......@@ -243,7 +247,7 @@ let do_goals env drv src_filename_printer dest_filename_printer file goals =
end;
if !call then
(* we are in the call mode *)
let call (th,task,drv) =
let call (th,task) =
let res =
Driver.call_prover ~debug:!debug ?timeout drv task in
printf "%s %s %s : %a@."
......@@ -262,7 +266,8 @@ let do_no_file env drv src_filename_printer dest_filename_printer =
(* Extract the goal(s) *)
Hashtbl.iter
(fun tname goals ->
let dir,file,th = match List.rev (Str.split (Str.regexp "\\.") tname) with
let dir,file,th =
match List.rev (Str.split (Str.regexp "\\.") tname) with
| t::p -> List.rev p, List.hd p, t
| _ -> assert false
in
......@@ -280,7 +285,7 @@ let do_no_file env drv src_filename_printer dest_filename_printer =
eprintf "--goal : Unknown goal %s@." s ; exit 1 in
Decl.Spr.add pr acc
) s Decl.Spr.empty) in
let goals = extract_goals ?filter env drv [] th in
let goals = extract_goals ?filter env [] th in
do_goals env drv src_filename_printer dest_filename_printer file goals)
which_theories
......@@ -317,7 +322,7 @@ let do_file env drv src_filename_printer dest_filename_printer file =
(* Extract the goal(s) *)
let goals =
if !set_all_goals
then Mnm.fold (fun _ th acc -> extract_goals env drv acc th) m []
then Mnm.fold (fun _ th acc -> extract_goals env acc th) m []
else
Hashtbl.fold
(fun tname goals acc ->
......@@ -335,7 +340,7 @@ let do_file env drv src_filename_printer dest_filename_printer file =
file s ; exit 1 in
Decl.Spr.add pr acc
) s Decl.Spr.empty) in
extract_goals ?filter env drv acc th
extract_goals ?filter env acc th
) which_theories [] in
do_goals env drv src_filename_printer dest_filename_printer file goals
end
......
src/printer/alt_ergo.ml
View file @ ebe0622b
......@@ -44,7 +44,7 @@ let rec print_type drv fmt ty = match ty.ty_node with
| Tyvar id ->
print_tvsymbols fmt id
| Tyapp (ts, tl) ->
match Driver.query_ident drv ts.ts_name with
match drv ts.ts_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_type drv) fmt tl
......@@ -71,7 +71,7 @@ let rec print_term drv fmt t = match t.t_node with
print_ident fmt id
| Tapp (ls, tl) ->
begin
match Driver.query_ident drv ls.ls_name with
match drv ls.ls_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_term drv) fmt tl
......@@ -97,7 +97,7 @@ let rec print_fmla drv fmt f = match f.f_node with
print_ident fmt id
| Fapp (ls, tl) ->
begin
match Driver.query_ident drv ls.ls_name with
match drv ls.ls_name with
| Driver.Remove -> assert false (* Mettre une erreur *)
| Driver.Syntax s ->
Driver.syntax_arguments s (print_term drv) fmt tl
......@@ -149,7 +149,7 @@ let print_logic_binder drv fmt v =
let print_type_decl drv fmt = function
| ts, Tabstract ->
begin
match Driver.query_ident drv ts.ts_name with
match drv ts.ts_name with
| Driver.Remove | Driver.Syntax _ -> false
| Driver.Tag _ ->
match ts.ts_args with
......@@ -164,7 +164,7 @@ let print_type_decl drv fmt = function
let ac_th = ["algebra";"AC"]