Commit e0d6b38d authored by Sylvain Dailler's avatar Sylvain Dailler

Add a name_table in proof_node.

Add a name_table in printer_args.
Put the definition of name_table in task.ml.
Build_name_tables only called once in proof_node creation.
Modified the rest accordingly.
parent 94a565b4
......@@ -35,6 +35,7 @@ type printer_mapping = {
}
type printer_args = {
name_table : name_tables option;
env : Env.env;
prelude : prelude;
th_prelude : prelude_map;
......
......@@ -36,6 +36,7 @@ type printer_mapping = {
}
type printer_args = {
name_table : name_tables option;
env : Env.env;
prelude : prelude;
th_prelude : prelude_map;
......
......@@ -342,6 +342,19 @@ let on_tagged_pr t task =
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set Spr.empty
(* Printing tasks *)
type id_decl = (Decl.decl list) Ident.Mid.t
type name_tables = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
(* Associate an id to a list of declarations in which it is used *)
id_decl : id_decl;
}
exception Bad_name_table of string
(* Exception reporting *)
let () = Exn_printer.register (fun fmt exn -> match exn with
......@@ -353,6 +366,8 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
Format.fprintf fmt "Metaproperty '%s' is not a symbol tag" m.meta_name
| NotExclusiveMeta m ->
Format.fprintf fmt "Metaproperty '%s' is not exclusive" m.meta_name
| Bad_name_table s ->
Format.fprintf fmt "Name table associated to task was not generated in %s" s
| _ -> raise exn)
(* task1 : prefix
......
......@@ -126,8 +126,21 @@ val on_tagged_ts : meta -> task -> Sts.t
val on_tagged_ls : meta -> task -> Sls.t
val on_tagged_pr : meta -> task -> Spr.t
(** Printing tasks *)
type id_decl = (Decl.decl list) Ident.Mid.t
type name_tables = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
(* Associate an id to a list of declarations in which it is used *)
id_decl : id_decl;
}
(** Exceptions *)
exception Bad_name_table of string
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta
......
......@@ -335,8 +335,8 @@ let list_transforms_l () =
(** transformations with arguments *)
type trans_with_args = string list -> Env.env -> task trans
type trans_with_args_l = string list -> Env.env -> task tlist
type trans_with_args = string list -> Env.env -> Task.name_tables -> task trans
type trans_with_args_l = string list -> Env.env -> Task.name_tables -> task tlist
let transforms_with_args = Hstr.create 17
let transforms_with_args_l = Hstr.create 17
......@@ -404,12 +404,12 @@ let apply_transform tr_name env task =
| Trans_with_args _ (* [apply (t []) task] *)
| Trans_with_args_l _ -> assert false (* apply (t []) task *)
let apply_transform_args tr_name env args task =
let apply_transform_args tr_name env args tables task =
match lookup_trans env tr_name with
| Trans_one t -> [apply t task]
| Trans_list t -> apply t task
| Trans_with_args t -> [apply (t args) env task]
| Trans_with_args_l t -> apply (t args) env task
| Trans_with_args t -> [apply (t args) env tables task]
| Trans_with_args_l t -> apply (t args) env tables task
(** Flag-dependent transformations *)
......
......@@ -164,8 +164,8 @@ val named : string -> 'a trans -> 'a trans
*)
type trans_with_args = string list -> Env.env -> task trans
type trans_with_args_l = string list -> Env.env -> task tlist
type trans_with_args = string list -> Env.env -> Task.name_tables -> task trans
type trans_with_args_l = string list -> Env.env -> Task.name_tables -> task tlist
val list_transforms_with_args : unit -> (string * Pp.formatted) list
val list_transforms_with_args_l : unit -> (string * Pp.formatted) list
......@@ -188,5 +188,5 @@ val list_trans : unit -> string list
val apply_transform : string -> Env.env -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n, directly.*)
val apply_transform_args : string -> Env.env -> string list -> task -> task list
val apply_transform_args : string -> Env.env -> string list -> Task.name_tables -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
......@@ -298,12 +298,13 @@ let prepare_task ~cntexample drv task =
let task = update_task drv task in
List.fold_left apply task transl
let print_task_prepared ?old drv fmt task =
let print_task_prepared ?old drv fmt tables task =
let p = match drv.drv_printer with
| None -> raise NoPrinter
| Some p -> p
in
let printer_args = { Printer.env = drv.drv_env;
name_table = tables;
prelude = drv.drv_prelude;
th_prelude = drv.drv_thprelude;
blacklist = drv.drv_blacklist;
......@@ -313,14 +314,14 @@ let print_task_prepared ?old drv fmt task =
fprintf fmt "@[%a@]@?" (printer ?old) task;
printer_args.printer_mapping
let print_task ?old ?(cntexample=false) drv fmt task =
let print_task ?old ?(cntexample=false) drv fmt tables task =
let task = prepare_task ~cntexample drv task in
let _ = print_task_prepared ?old drv fmt task in
let _ = print_task_prepared ?old drv fmt tables task in
()
let print_theory ?old drv fmt th =
let print_theory ?old drv fmt tables th =
let task = Task.use_export None th in
print_task ?old drv fmt task
print_task ?old drv fmt tables task
let file_name_of_task ?old ?inplace drv task =
match old, inplace with
......@@ -333,12 +334,12 @@ let file_name_of_task ?old ?inplace drv task =
let fn = try Filename.chop_extension fn with Invalid_argument _ -> fn in
get_filename drv fn "T" pr.pr_name.id_string
let prove_task_prepared ~command ~limit ?old ?inplace drv task =
let prove_task_prepared ~command ~limit ?old ?inplace drv tables task =
let buf = Buffer.create 1024 in
let fmt = formatter_of_buffer buf in
let old_channel = Opt.map open_in old in
let filename = file_name_of_task ?old ?inplace drv task in
let printer_mapping = print_task_prepared ?old:old_channel drv fmt task in
let printer_mapping = print_task_prepared ?old:old_channel drv fmt tables task in
pp_print_flush fmt ();
Opt.iter close_in old_channel;
let res =
......@@ -348,9 +349,9 @@ let prove_task_prepared ~command ~limit ?old ?inplace drv task =
res
let prove_task ~command ~limit ?(cntexample=false) ?old
?inplace drv task =
?inplace drv tables task =
let task = prepare_task ~cntexample drv task in
prove_task_prepared ~command ~limit ?old ?inplace drv task
prove_task_prepared ~command ~limit ?old ?inplace drv tables task
(* exception report *)
......
......@@ -46,11 +46,11 @@ val call_on_buffer :
val print_task :
?old : in_channel ->
?cntexample : bool ->
driver -> Format.formatter -> Task.task -> unit
driver -> Format.formatter -> Task.name_tables option -> Task.task -> unit
val print_theory :
?old : in_channel ->
driver -> Format.formatter -> Theory.theory -> unit
driver -> Format.formatter -> Task.name_tables option -> Theory.theory -> unit
(** produce a realization of the given theory using the given driver *)
val prove_task :
......@@ -59,21 +59,21 @@ val prove_task :
?cntexample : bool ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.prover_call
driver -> Task.name_tables option -> Task.task -> Call_provers.prover_call
(** Split the previous function in two simpler functions *)
val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
val print_task_prepared :
?old : in_channel ->
driver -> Format.formatter -> Task.task -> Printer.printer_mapping
driver -> Format.formatter -> Task.name_tables option -> Task.task -> Printer.printer_mapping
val prove_task_prepared :
command : string ->
limit : Call_provers.resource_limit ->
?old : string ->
?inplace : bool ->
driver -> Task.task -> Call_provers.prover_call
driver -> Task.name_tables option -> Task.task -> Call_provers.prover_call
(** Traverse all metas from a driver *)
......
......@@ -903,8 +903,9 @@ let on_selected_row r =
match session_element with
| IproofNode id ->
let task = get_task cont.controller_session id in
let tables = get_tables cont.controller_session id in
let s = Pp.string_of
(Driver.print_task ~cntexample:false task_driver)
(fun fmt -> Driver.print_task ~cntexample:false task_driver fmt tables)
task
in task_view#source_buffer#set_text s;
(* scroll to end of text *)
......
......@@ -19,6 +19,7 @@ open Term
open Decl
open Printer
open Theory
open Task
open Args_wrapper
......@@ -408,7 +409,9 @@ let print_tdecls tables =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *)
let tables = build_name_tables task in
let tables = match args.name_table with
| None -> raise (Bad_name_table "why3printer")
| Some tables -> tables in
print_prelude fmt args.prelude;
fprintf fmt "theory Task@\n";
print_th_prelude task fmt args.th_prelude;
......@@ -430,10 +433,13 @@ let print_task args ?old:_ fmt task =
let () = register_printer "why3" print_task
~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ Used@ for@ debugging."
let print_sequent _args ?old:_ fmt task =
let print_sequent args ?old:_ fmt task =
info := {info_syn = Discriminate.get_syntax_map task;
itp = true};
let tables = build_name_tables task in
let tables = match args.name_table with
| None -> raise (Bad_name_table "why3printer")
| Some tables -> tables in
(* let tables = build_name_tables task in *)
let ut = Task.used_symbols (Task.used_theories task) in
let ld = Task.local_decls task ut in
fprintf fmt "@[<v 0>%a@]"
......
val print_decl: Args_wrapper.name_tables -> Format.formatter -> Decl.decl -> unit
val print_decl: Task.name_tables -> Format.formatter -> Decl.decl -> unit
......@@ -340,9 +340,10 @@ let build_prover_call c id pr limit callback =
Whyconf.get_complete_command config_pr
~with_steps:Call_provers.(limit.limit_steps <> empty_limit.limit_steps) in
let task = Session_itp.get_task c.controller_session id in
let tables = Session_itp.get_tables c.controller_session id in
let call =
Driver.prove_task ?old:None ~cntexample:true ~inplace:false ~command
~limit driver task
~limit driver tables task
in
let pa = (c.controller_session,id,pr,callback,false,call) in
Queue.push pa prover_tasks_in_progress
......@@ -426,9 +427,12 @@ let schedule_proof_attempt c id pr ~limit ~callback =
let schedule_transformation_r c id name args ~callback =
let apply_trans () =
let task = get_task c.controller_session id in
let tables = match get_tables c.controller_session id with
| None -> raise (Task.Bad_name_table "schedule_transformation")
| Some tables -> tables in
begin
try
let subtasks = Trans.apply_transform_args name c.controller_env args task in
let subtasks = Trans.apply_transform_args name c.controller_env args tables task in
(* if result is same as input task, consider it as a failure *)
begin
match subtasks with
......
......@@ -1974,7 +1974,8 @@ let copy_external_proof
let old = open_in file in
let ch = open_out dst_file in
let fmt = formatter_of_out_channel ch in
Driver.print_task ~old driver fmt task;
(* Do not need tables because not a case in itp *)
Driver.print_task ~old driver fmt None task;
close_in old;
close_out ch;
let dst_file = Sysutil.relativize_filename dir dst_file in
......@@ -2022,7 +2023,8 @@ let update_edit_external_proof ~cntexample env_session a =
in
let ch = open_out file in
let fmt = formatter_of_out_channel ch in
Driver.print_task ~cntexample ?old driver fmt goal;
(* Name table is only used in ITP printing *)
Driver.print_task ~cntexample ?old driver fmt None goal;
Opt.iter close_in old;
close_out ch;
file
......
......@@ -40,6 +40,7 @@ type proof_attempt_node = {
type proof_node = {
proofn_name : Ident.ident;
proofn_task : Task.task;
proofn_table : Task.name_tables option;
proofn_parent : proof_parent;
proofn_checksum : Termcode.checksum option;
proofn_shape : Termcode.shape;
......@@ -194,6 +195,10 @@ let get_task (s:session) (id:proofNodeID) =
let node = get_proofNode s id in
node.proofn_task
let get_tables (s: session) (id: proofNodeID) =
let node = get_proofNode s id in
node.proofn_table
let get_transfNode (s : session) (id : transID) =
try
Hint.find s.trans_table id
......@@ -367,10 +372,12 @@ let remove_proof_attempt (s : session) (id : proofNodeID)
of proofNodeID [id] of parent [p] of task [t] *)
let mk_proof_node ~version (s : session) (n : Ident.ident) (t : Task.task)
(parent : proof_parent) (node_id : proofNodeID) =
let tables = Args_wrapper.build_name_tables t in
let sum = Some (Termcode.task_checksum ~version t) in
let shape = Termcode.t_shape_task ~version t in
let pn = { proofn_name = n;
proofn_task = t;
proofn_table = Some tables;
proofn_parent = parent;
proofn_checksum = sum;
proofn_shape = shape;
......@@ -382,6 +389,7 @@ let mk_proof_node_no_task (s : session) (n : Ident.ident)
(parent : proof_parent) (node_id : proofNodeID) sum shape =
let pn = { proofn_name = n;
proofn_task = None;
proofn_table = None;
proofn_parent = parent;
proofn_checksum = sum;
proofn_shape = shape;
......@@ -936,7 +944,10 @@ let add_registered_transformation s env old_tr goal_id =
with Not_found ->
Debug.dprintf debug "[merge_theory] trans not found@.";
let task = goal.proofn_task in
let subgoals = Trans.apply_transform_args old_tr.transf_name env old_tr.transf_args task in
let tables = match goal.proofn_table with
| None -> raise (Task.Bad_name_table "add_registered_transformation")
| Some tables -> tables in
let subgoals = Trans.apply_transform_args old_tr.transf_name env old_tr.transf_args tables task in
graft_transf s goal_id old_tr.transf_name old_tr.transf_args subgoals
let rec merge_goal ~use_shapes env new_s old_s obsolete old_goal new_goal_id =
......
......@@ -62,6 +62,7 @@ val session_iter_proof_attempt: (proofNodeID -> proof_attempt_node -> unit) -> s
type proof_parent = Trans of transID | Theory of theory
val get_task : session -> proofNodeID -> Task.task
val get_tables: session -> proofNodeID -> Task.name_tables option
val get_transformations : session -> proofNodeID -> transID list
val get_proof_attempt_ids :
......
......@@ -192,9 +192,10 @@ let idle_handler t =
old,inplace,command,driver,callback,goal) ->
begin
try
(* Name table are not used outside ITP *)
let call =
Driver.prove_task ?old ~cntexample ~inplace ~command
~limit driver goal
~limit driver None goal
in
let pa = Check_prover (callback,false,call) in
Queue.push pa t.proof_attempts_queue;
......
......@@ -278,10 +278,10 @@ exception Undefined_id of string
(* Bad number of arguments *)
exception Number_of_arguments
let print_id s task =
let tables = Args_wrapper.build_name_tables task in
let km = tables.Args_wrapper.known_map in
let id = try find_any_id tables.Args_wrapper.namespace s with
let print_id s tables =
(* let tables = Args_wrapper.build_name_tables task in*)
let km = tables.Task.known_map in
let id = try find_any_id tables.Task.namespace s with
| Not_found -> raise (Undefined_id s) in
let d =
try Ident.Mid.find id km with
......@@ -294,10 +294,10 @@ let print_id _cont task args =
| [s] -> print_id s task
| _ -> raise Number_of_arguments
let search s task =
let tables = Args_wrapper.build_name_tables task in
let id_decl = tables.Args_wrapper.id_decl in
let id = try find_any_id tables.Args_wrapper.namespace s with
let search s tables =
(*let tables = Args_wrapper.build_name_tables task in*)
let id_decl = tables.Task.id_decl in
let id = try find_any_id tables.Task.namespace s with
| Not_found -> raise (Undefined_id s) in
let l =
try Ident.Mid.find id id_decl with
......@@ -312,7 +312,7 @@ let search_id _cont task args =
type query =
| Qnotask of (Controller_itp.controller -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.task -> string list -> string)
| Qtask of (Controller_itp.controller -> Task.name_tables -> string list -> string)
let commands =
[
......@@ -394,8 +394,10 @@ let interp cont id s =
| Qnotask f, _ -> Query (f cont args)
| Qtask _, None -> Query "please select a goal first"
| Qtask f, Some id ->
let task = Session_itp.get_task cont.Controller_itp.controller_session id in
let s = try Query (f cont task args) with
let tables = match Session_itp.get_tables cont.Controller_itp.controller_session id with
| None -> raise (Task.Bad_name_table "interp")
| Some tables -> tables in
let s = try Query (f cont tables args) with
| Undefined_id s -> Query ("No existing id corresponding to " ^ s)
| Number_of_arguments -> Query "Bad number of arguments"
in s
......
......@@ -244,7 +244,8 @@ let output_task drv fname _tname th task dir =
let name = Ident.string_unique !fname_printer (String.sub dest 0 i) in
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
Driver.print_task drv (formatter_of_out_channel cout) task;
(* Name tables not necessary outside of ITP *)
Driver.print_task drv (formatter_of_out_channel cout) None task;
close_out cout
let output_task_prepared drv fname _tname th task dir =
......@@ -259,7 +260,8 @@ let output_task_prepared drv fname _tname th task dir =
let ext = String.sub dest i (String.length dest - i) in
let cout = open_out (Filename.concat dir (name ^ ext)) in
(* TODO print the counterexample *)
let _counterexample = Driver.print_task_prepared drv (formatter_of_out_channel cout) task in
(* Name tables not necessary outside ITP *)
let _counterexample = Driver.print_task_prepared drv (formatter_of_out_channel cout) None task in
close_out cout
let output_theory drv fname _tname th task dir =
......@@ -275,7 +277,8 @@ let output_theory drv fname _tname th task dir =
Some (open_in backup)
end else None in
let cout = open_out file in
Driver.print_task ?old drv (formatter_of_out_channel cout) task;
(* Name table is not necessary outside ITP *)
Driver.print_task ?old drv (formatter_of_out_channel cout) None task;
close_out cout
let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
......@@ -285,14 +288,16 @@ let do_task drv fname tname (th : Theory.theory) (task : Task.task) =
limit_mem = memlimit } in
match !opt_output, !opt_command with
| None, Some command ->
(* Name tables not necessary outside ITP *)
let call =
Driver.prove_task ~command ~limit ~cntexample:!opt_cntexmp drv task in
Driver.prove_task ~command ~limit ~cntexample:!opt_cntexmp drv None task in
let res = Call_provers.wait_on_call call in
printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res
| None, None ->
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter task
(* Name tables not necessary outside ITP *)
Driver.print_task ~cntexample:!opt_cntexmp drv std_formatter None task
| Some dir, _ -> output_task drv fname tname th task dir
let do_tasks env drv fname tname th task =
......
......@@ -100,7 +100,8 @@ let do_global_theory (_tname,p,t) =
Some (open_in backup)
end else None in
let cout = open_out file in
Driver.print_task ?old opt_driver (formatter_of_out_channel cout) task;
(* Name tables not necessary outside of ITP *)
Driver.print_task ?old opt_driver (formatter_of_out_channel cout) None task;
close_out cout
let () =
......
......@@ -42,17 +42,6 @@ let sanitizer x = x (*sanitizer char_to_lalpha char_to_lalpha x*)
let id_unique printer id =
id_unique_label printer ~sanitizer:sanitizer id
type id_decl = (Decl.decl list) Ident.Mid.t
type name_tables = {
namespace : namespace;
known_map : known_map;
printer : ident_printer;
(* Associate an id to a list of declarations in which it is used *)
id_decl : id_decl;
}
(* Use symb to encapsulate ids into correct categories of symbols *)
type symb =
| Ts of tysymbol
......@@ -198,7 +187,6 @@ let add (d: decl) (tables: name_tables): name_tables =
let tables = add_unsafe s (Pr pr) tables in
add_id tables d t
let build_name_tables task : name_tables =
let pr = fresh_printer () in
let km = Task.task_known task in
......@@ -236,12 +224,12 @@ type (_, _) trans_typ =
| Topt : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
| Toptbool : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
let find_pr s task =
let tables = build_name_tables task in
let find_pr s tables =
(*let tables = build_name_tables task in*)
Mstr.find s tables.namespace.ns_pr
let type_ptree ~as_fmla t task =
let tables = build_name_tables task in
let type_ptree ~as_fmla t tables =
(*let tables = build_name_tables task in*)
let km = tables.known_map in
let ns = tables.namespace in
if as_fmla
......@@ -343,73 +331,73 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
| Topt (s,t) -> "opt [" ^ s ^ "] " ^ print_type t
| Toptbool (s,t) -> "opt [" ^ s ^ "] -> " ^ print_type t
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> task -> b =
fun t f l env task ->
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> name_tables -> task -> b =
fun t f l env tables task ->
match t, l with
| Ttrans, _-> apply f task
| Ttrans_l, _ -> apply f task
| Tenvtrans, _ -> apply (f env) task
| Tenvtrans_l, _ -> apply (f env) task
| Tint t', s :: tail ->
let arg = parse_int s in wrap_to_store t' (f arg) tail env task
let arg = parse_int s in wrap_to_store t' (f arg) tail env tables task
| Tformula t', s :: tail ->
let te = parse_and_type ~as_fmla:true s task in
wrap_to_store t' (f te) tail env task
let te = parse_and_type ~as_fmla:true s tables in
wrap_to_store t' (f te) tail env tables task
| Tterm t', s :: tail ->
let te = parse_and_type ~as_fmla:false s task in
wrap_to_store t' (f te) tail env task
let te = parse_and_type ~as_fmla:false s tables in
wrap_to_store t' (f te) tail env tables task
| Tty t', _s :: tail ->
let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
wrap_to_store t' (f ty) tail env task
wrap_to_store t' (f ty) tail env tables task
| Ttysymbol t', _s :: tail ->
let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
wrap_to_store t' (f tys) tail env task
wrap_to_store t' (f tys) tail env tables task
| Tprsymbol t', s :: tail ->
let pr = find_pr s task in
wrap_to_store t' (f pr) tail env task
let pr = find_pr s tables in
wrap_to_store t' (f pr) tail env tables task
| Ttheory t', s :: tail ->
let th = parse_theory env s in
wrap_to_store t' (f th) tail env task
wrap_to_store t' (f th) tail env tables task
| Tstring t', s :: tail ->
wrap_to_store t' (f s) tail env task
wrap_to_store t' (f s) tail env tables task
| Topt (optname, t'), s :: s' :: tail when s = optname ->
begin match t' with
| Tint t' ->
let arg = Some (parse_int s') in
wrap_to_store t' (f arg) tail env task
wrap_to_store t' (f arg) tail env tables task
| Tprsymbol t' ->
let arg = Some (find_pr s' task) in
wrap_to_store t' (f arg) tail env task
let arg = Some (find_pr s' tables) in
wrap_to_store t' (f arg) tail env tables task
| Tformula t' ->
let arg = Some (parse_and_type ~as_fmla:true s' task) in
wrap_to_store t' (f arg) tail env task
let arg = Some (parse_and_type ~as_fmla:true s' tables) in
wrap_to_store t' (f arg) tail env tables task
| Tterm t' ->
let arg = Some (parse_and_type ~as_fmla:false s' task) in
wrap_to_store t' (f arg) tail env task
let arg = Some (parse_and_type ~as_fmla:false s' tables) in
wrap_to_store t' (f arg) tail env tables task
| Ttheory t' ->
let arg = Some (parse_theory env s') in
wrap_to_store t' (f arg) tail env task
wrap_to_store t' (f arg) tail env tables task
| Tstring t' ->
let arg = Some s' in
wrap_to_store t' (f arg) tail env task
wrap_to_store t' (f arg) tail env tables task
| _ -> raise (Arg_expected (string_of_trans_typ t', s'))
end
| Topt (_, t'), _ ->
wrap_to_store (trans_typ_tail t') (f None) l env task
wrap_to_store (trans_typ_tail t') (f None) l env tables task
| Toptbool (optname, t'), s :: tail when s = optname ->
wrap_to_store t' (f true) tail env task
wrap_to_store t' (f true) tail env tables task