Commit 75d67633 authored by Francois Bobot's avatar Francois Bobot

raw_driver and driver

parent f6d5509e
......@@ -125,15 +125,19 @@ let print_translation fmt = function
type printer = driver -> formatter -> task -> unit
and driver = {
and raw_driver = {
drv_printer : printer option;
drv_task : task;
drv_clone : clone option;
drv_prover : Call_provers.prover;
drv_prelude : string option;
drv_filename : string option;
drv_transforms : task tlist_reg;
drv_rules : theory_rules list;
}
and driver = {
drv_raw : raw_driver;
drv_clone : clone;
drv_env : env;
drv_thprelude : string Hid.t;
(* the first is the translation only for this ident, the second is
also for representant *)
......@@ -141,6 +145,7 @@ and driver = {
drv_with_task : translation Hid.t;
}
(*
let print_driver fmt driver =
printf "drv_theory %a@\n"
......@@ -334,8 +339,6 @@ let load_driver file env =
identity_l transformations in
let transforms = trans ltransforms in
{ drv_printer = !printer;
drv_task = None;
drv_clone = None;
drv_prover = {Call_provers.pr_call_stdin = !call_stdin;
pr_call_file = !call_file;
pr_regexps = regexps};
......@@ -343,9 +346,6 @@ let load_driver file env =
drv_filename = !filename;
drv_transforms = transforms;
drv_rules = f.f_rules;
drv_thprelude = Hid.create 1;
drv_theory = Hid.create 1;
drv_with_task = Hid.create 1;
}
(** querying drivers *)
......@@ -355,7 +355,7 @@ let query_ident drv id =
Hid.find drv.drv_with_task id
with Not_found ->
let r = try
Mid.find id (Util.of_option drv.drv_clone).cl_map
Mid.find id drv.drv_clone.cl_map
with Not_found -> Sid.empty in
let tr = try fst (Hid.find drv.drv_theory id)
with Not_found -> Tag Sstr.empty in
......@@ -375,23 +375,28 @@ let syntax_arguments s print fmt l =
(** using drivers *)
let apply_transforms env clone drv =
apply_clone drv.drv_transforms env clone
let apply_transforms drv =
apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone
let cook_driver env clone drv =
let drv = { drv_raw = drv;
drv_clone = clone;
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 clone drv) drv.drv_raw.drv_rules;
drv
let print_task env clone drv fmt task = match drv.drv_printer with
let print_task drv fmt task = match drv.drv_raw.drv_printer with
| None -> errorm "no printer"
| Some f -> let drv = {drv with drv_task = task;
drv_clone = Some clone;
drv_thprelude = Hid.create 17;
drv_theory = Hid.create 17;
drv_with_task = Hid.create 17} in
List.iter (load_rules env clone drv) drv.drv_rules;
f drv fmt task
| Some f -> f drv fmt task
let regexp_filename = Str.regexp "%\\([a-z]\\)"
let filename_of_goal drv ident_printer filename theory_name task =
match drv.drv_filename with
match drv.drv_raw.drv_filename with
| None -> errorm "no filename syntax given"
| Some f ->
let pr_name = (task_goal task).pr_name in
......@@ -409,18 +414,18 @@ let file_printer =
[]
let call_prover_on_file ?debug ?timeout drv filename =
Call_provers.on_file drv.drv_prover filename
Call_provers.on_file drv.drv_raw.drv_prover filename
let call_prover_on_buffer ?debug ?timeout ?filename drv ib =
Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_prover ib
Call_provers.on_buffer ?debug ?timeout ?filename drv.drv_raw.drv_prover ib
let call_prover ?debug ?timeout env clone drv task =
let call_prover ?debug ?timeout drv task =
let filename =
match drv.drv_filename with
match drv.drv_raw.drv_filename with
| None -> None
| Some _ -> Some (filename_of_goal drv file_printer "" "" task) in
let buffer = Buffer.create 128 in
bprintf buffer "%a@?" (print_task env clone drv) task;
bprintf buffer "%a@?" (print_task drv) task;
call_prover_on_buffer ?debug ?timeout ?filename drv buffer
......
......@@ -25,9 +25,14 @@ open Env
(** creating drivers *)
type raw_driver
val load_driver : string -> env -> raw_driver
(** cooked driver *)
type driver
val load_driver : string -> env -> driver
val cook_driver : env -> clone -> raw_driver -> driver
(** querying drivers *)
......@@ -56,10 +61,10 @@ val list_transforms : unit -> string list
(** using drivers *)
(** transform task *)
val apply_transforms : env -> clone -> driver -> task -> task list
val apply_transforms : driver -> task -> task list
(** print_task *)
val print_task : env -> clone -> printer
val print_task : printer
val filename_of_goal : driver -> Ident.ident_printer ->
string -> string -> task -> string
......@@ -79,8 +84,6 @@ val call_prover :
and the output of the prover *)
?timeout:int -> (* specify the time limit given to the prover,
if not set unlimited time *)
env ->
clone ->
driver -> (* the driver to use *)
task -> (* the task to prove with a goal as the last declaration *)
Call_provers.prover_result
......
......@@ -167,7 +167,9 @@ let transform env l =
let extract_goals ?filter =
fun env drv acc th ->
let l = split_theory th filter in
let l = List.rev_map (fun task -> (th,task)) l in
let l = List.rev_map (fun (task,cl) ->
let drv = Driver.cook_driver env cl drv in
(th,task,drv)) l in
List.rev_append l acc
let file_sanitizer =
......@@ -209,18 +211,20 @@ let do_file env drv filename_printer file =
| Some s -> Some
(Hashtbl.fold
(fun s l acc ->
let pr = try ns_find_pr th.th_export l with Not_found ->
eprintf "File %s : --goal : Unknown goal %s@." file s ; exit 1 in
let pr = try ns_find_pr th.th_export l
with Not_found ->
eprintf "File %s : --goal : Unknown goal %s@."
file s ; exit 1 in
Decl.Spr.add pr acc
) s Decl.Spr.empty) in
extract_goals ?filter env drv acc th
) which_theories [] in
(* Apply transformations *)
let goals = List.fold_left
(fun acc (th,(task,cl)) ->
(fun acc (th,task,drv) ->
List.rev_append
(List.map (fun e -> (th,e,cl)) (Driver.apply_transforms env cl drv
task)
(List.map (fun e -> (th,e,drv))
(Driver.apply_transforms drv task)
) acc) [] goals in
(* Pretty-print the goals or call the prover *)
begin
......@@ -238,7 +242,7 @@ let do_file env drv filename_printer file =
let ident_printer = Ident.create_ident_printer
~sanitizer:file_sanitizer [] in
List.iter
(fun (th,task,cl) ->
(fun (th,task,drv) ->
let cout =
if dir = "-"
then stdout
......@@ -249,7 +253,7 @@ let do_file env drv filename_printer file =
let filename = Filename.concat dir filename in
open_out filename in
let fmt = formatter_of_out_channel cout in
fprintf fmt "%a@?" (Driver.print_task env cl drv) task;
fprintf fmt "%a@?" (Driver.print_task drv) task;
close_out cout) goals
end;
begin
......@@ -257,18 +261,18 @@ let do_file env drv filename_printer file =
| None -> ()
| Some file (* we are in the output file mode *) ->
List.iter
(fun (th,task,cl) ->
(fun (th,task,drv) ->
let fmt = if file = "-"
then std_formatter
else formatter_of_out_channel (open_out file) in
fprintf fmt "%a\000@?" (Driver.print_task env cl drv) task)
fprintf fmt "%a\000@?" (Driver.print_task drv) task)
goals
end;
if !call then
(* we are in the call mode *)
let call (th,task,cl) =
let call (th,task,drv) =
let res =
Driver.call_prover ~debug:!debug ?timeout env cl drv task in
Driver.call_prover ~debug:!debug ?timeout drv task in
printf "%s %s %s : %a@."
file th.th_name.Ident.id_short
((task_goal task).Decl.pr_name).Ident.id_long
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment