Commit 51a377d3 authored by Andrei Paskevich's avatar Andrei Paskevich

simplify transformation descriptions

parent 5cc897ae
......@@ -11,6 +11,8 @@
open Format
open Pp
open Stdlib
open Ident
open Ty
open Term
......@@ -29,30 +31,23 @@ type 'a pp = formatter -> 'a -> unit
type printer =
Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
type reg_printer =
{ reg_desc : formatted;
reg_printer : printer;
}
type reg_printer = Pp.formatted * printer
let printers : (string, reg_printer) Hashtbl.t = Hashtbl.create 17
let printers : reg_printer Hstr.t = Hstr.create 17
exception KnownPrinter of string
exception UnknownPrinter of string
let register_printer ~desc s p =
if Hashtbl.mem printers s then raise (KnownPrinter s);
Hashtbl.replace printers s {reg_desc = desc; reg_printer = p}
if Hstr.mem printers s then raise (KnownPrinter s);
Hstr.replace printers s (desc, p)
let lookup_printer s =
try (Hashtbl.find printers s).reg_printer
try snd (Hstr.find printers s)
with Not_found -> raise (UnknownPrinter s)
let list_printers () = Hashtbl.fold (fun k p acc ->
(k,p.reg_desc)::acc) printers []
let print_printer_desc fmt (s,f) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]"
s Pp.formatted f
let list_printers () =
Hstr.fold (fun k (desc,_) acc -> (k,desc)::acc) printers []
let () = register_printer ~desc:"Print nothing" "(null)"
(fun _ _ _ _ ?old:_ _ _ -> ())
......
......@@ -25,14 +25,13 @@ type blacklist = string list
type 'a pp = Format.formatter -> 'a -> unit
type printer =
Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
val register_printer : desc:Pp.formatted -> string -> printer -> unit
val lookup_printer : string -> printer
val list_printers : unit -> (string * Pp.formatted) list
val print_printer_desc : Pp.formatter -> (string * Pp.formatted) -> unit
(** {2 use printers} *)
......
......@@ -249,85 +249,40 @@ let named s f (x : task) =
if Debug.test_flag Debug.stack_trace then f x
else try f x with e -> raise (TransFailure (s,e))
type desc_labels = (label * Pp.formatted) list
type desc_metas = (meta * Pp.formatted) list
type reg_desc =
{
reg_desc_labels : desc_labels;
reg_desc_metas : desc_metas;
reg_desc : Pp.formatted;
}
let print_reg_desc fmt r =
let print_meta fmt (m,f) =
fprintf fmt "@[%s@\n @[%a%a@]@]"
m.meta_name Pp.formatted m.meta_desc Pp.formatted f in
let print_label fmt (l,f) =
fprintf fmt "@[%s@\n @[%a@]@]"
l.lab_string Pp.formatted f in
fprintf fmt "@[@[%a@]%a%a@]"
Pp.formatted r.reg_desc
(Pp.print_list_delim
~start:(Pp.constant_formatted "@\nlabels:@\n @[")
~stop:(Pp.constant_formatted "@]")
~sep:Pp.newline
print_label) r.reg_desc_labels
(Pp.print_list_delim
~start:(Pp.constant_formatted "@\nmetas:@\n @[")
~stop:(Pp.constant_formatted "@]")
~sep:Pp.newline
print_meta) r.reg_desc_metas
let print_trans_desc fmt (x,r) =
fprintf fmt "@[%s@\n @[%a@]@]" x print_reg_desc r
type 'a reg_trans = (env -> 'a trans) * reg_desc
let mk_reg_trans ?(desc_labels=[]) ?(desc_metas=[]) ~desc f =
f, { reg_desc_labels = desc_labels;
reg_desc_metas = desc_metas;
reg_desc = desc}
type 'a reg_trans = Pp.formatted * (env -> 'a trans)
let transforms : (task reg_trans) Hstr.t = Hstr.create 17
let transforms_l : (task list reg_trans) Hstr.t = Hstr.create 17
let register_transform ?desc_labels ?desc_metas ~desc s p =
let register_transform ~desc s p =
if Hstr.mem transforms s then raise (KnownTrans s);
Hstr.replace transforms s
(mk_reg_trans ?desc_labels ?desc_metas ~desc (fun _ -> named s p))
Hstr.replace transforms s (desc, fun _ -> named s p)
let register_transform_l ?desc_labels ?desc_metas ~desc s p =
let register_transform_l ~desc s p =
if Hstr.mem transforms_l s then raise (KnownTrans s);
Hstr.replace transforms_l s
(mk_reg_trans ?desc_labels ?desc_metas ~desc (fun _ -> named s p))
Hstr.replace transforms_l s (desc, fun _ -> named s p)
let register_env_transform ?desc_labels ?desc_metas ~desc s p =
let register_env_transform ~desc s p =
if Hstr.mem transforms s then raise (KnownTrans s);
Hstr.replace transforms s
(mk_reg_trans ?desc_labels ?desc_metas ~desc
(Wenv.memoize 3 (fun e -> named s (p e))))
Hstr.replace transforms s (desc, Wenv.memoize 3 (fun e -> named s (p e)))
let register_env_transform_l ?desc_labels ?desc_metas ~desc s p =
let register_env_transform_l ~desc s p =
if Hstr.mem transforms_l s then raise (KnownTrans s);
Hstr.replace transforms_l s
(mk_reg_trans ?desc_labels ?desc_metas ~desc
(Wenv.memoize 3 (fun e -> named s (p e))))
Hstr.replace transforms_l s (desc, Wenv.memoize 3 (fun e -> named s (p e)))
let lookup_transform s =
try fst (Hstr.find transforms s)
try snd (Hstr.find transforms s)
with Not_found -> raise (UnknownTrans s)
let lookup_transform_l s =
try fst (Hstr.find transforms_l s)
try snd (Hstr.find transforms_l s)
with Not_found -> raise (UnknownTrans s)
let list_transforms () = Hstr.fold (fun k r acc ->
(k,snd r)::acc) transforms []
let list_transforms () =
Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms []
let list_transforms_l () = Hstr.fold
(fun k r acc -> (k,snd r)::acc) transforms_l []
let list_transforms_l () =
Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms_l []
(** fast transform *)
type gentrans =
......@@ -369,7 +324,6 @@ let on_flag m ft def arg =
let tr_name = Printf.sprintf "%s : %s" m.meta_name s in
named tr_name (t arg))
let () = Exn_printer.register (fun fmt exn -> match exn with
| KnownTrans s ->
Format.fprintf fmt "Transformation '%s' is already registered" s
......@@ -385,4 +339,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
Format.fprintf fmt "Failure in transformation %s@\n%a" s
Exn_printer.exn_printer e
| e -> raise e)
......@@ -105,38 +105,20 @@ exception TransFailure of string * exn
exception UnknownTrans of string
exception KnownTrans of string
type desc_labels = (Ident.label * Pp.formatted) list
type desc_metas = (meta * Pp.formatted) list
val register_env_transform :
?desc_labels:desc_labels -> ?desc_metas:desc_metas -> desc:Pp.formatted ->
string -> (Env.env -> task trans) -> unit
desc:Pp.formatted -> string -> (Env.env -> task trans) -> unit
val register_env_transform_l :
?desc_labels:desc_labels -> ?desc_metas:desc_metas -> desc:Pp.formatted ->
string -> (Env.env -> task tlist) -> unit
desc:Pp.formatted -> string -> (Env.env -> task tlist) -> unit
val register_transform :
?desc_labels:desc_labels -> ?desc_metas:desc_metas -> desc:Pp.formatted ->
string -> task trans -> unit
val register_transform_l :
?desc_labels:desc_labels -> ?desc_metas:desc_metas -> desc:Pp.formatted ->
string -> task tlist -> unit
val register_transform : desc:Pp.formatted -> string -> task trans -> unit
val register_transform_l : desc:Pp.formatted -> string -> task tlist -> unit
val lookup_transform : string -> Env.env -> task trans
val lookup_transform_l : string -> Env.env -> task tlist
type reg_desc =
{ reg_desc_labels : desc_labels;
reg_desc_metas : desc_metas;
reg_desc : Pp.formatted;
}
val print_reg_desc : Pp.formatter -> reg_desc -> unit
val print_trans_desc : Pp.formatter -> string * reg_desc -> unit
val list_transforms : unit -> (string * reg_desc) list
val list_transforms_l : unit -> (string * reg_desc) list
val list_transforms : unit -> (string * Pp.formatted) list
val list_transforms_l : unit -> (string * Pp.formatted) list
val named : string -> 'a trans -> 'a trans
(** give transformation a name without registering *)
......
......@@ -1475,8 +1475,10 @@ let () =
let callback () = apply_trans_on_selection name in
let ii = non_splitting#add_image_item
~label:(sanitize_markup name) ~callback () in
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n%a@]" x Pp.formatted r in
ii#misc#set_tooltip_text
(Pp.string_of Trans.print_trans_desc desc) in
(Pp.string_of print_trans_desc desc) in
let trans =
if nonsplitting
then Trans.list_transforms ()
......
......@@ -235,17 +235,21 @@ let () = try
let opt_list = ref false in
if !opt_list_transforms then begin
opt_list := true;
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r in
printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 Trans.print_trans_desc)
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms ()));
printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 Trans.print_trans_desc)
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms_l ()))
end;
if !opt_list_printers then begin
opt_list := true;
let print_printer_desc fmt (s,f) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" s Pp.formatted f in
printf "@[<hov 2>Known printers:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 Printer.print_printer_desc)
(Pp.print_list Pp.newline2 print_printer_desc)
(List.sort sort_pair (Printer.list_printers ()))
end;
if !opt_list_formats then begin
......
......@@ -31,7 +31,6 @@ let syntactic_transform transf =
let () =
Trans.register_transform "abstract_unknown_lsymbols"
(syntactic_transform Abstraction.abstraction)
~desc_metas:[meta_syntax_logic,Pp.empty_formatted]
~desc:"Abstract@ application@ of@ non-built-in@ symbols@ with@ constants.";
Trans.register_transform "simplify_unknown_lsymbols"
(syntactic_transform (fun check_ls -> Trans.goal (fun pr f ->
......@@ -46,7 +45,6 @@ let () =
| Tapp(ls,_) -> not (check_ls ls)
| _ -> true) f)
])))
~desc_metas:[meta_syntax_logic,("" : Pp.formatted)]
~desc:"In the goal substitute equality on application of unknown symbols.";
......
......@@ -319,6 +319,7 @@ let () = register_printer "smtv2"
print_task_old pr thpr blacklist fmt task)
~desc:"Printer for the smtlib version 2 format."
(*
let print_decls =
let add_ls sm acc = function
| [MAls ls; MAls lsdis] ->
......@@ -344,3 +345,4 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task =
let () = register_printer "smtv2new" print_task
~desc:"New (TODO: in which sense?) printer for the smtlib version 2 format."
*)
......@@ -378,6 +378,7 @@ let print_tdecl fmt td = match td.td_node with
fprintf fmt "@[<hov 2>(* meta %s %a *)@]@\n@\n"
m.meta_name (print_list comma print_meta_arg) al
(*
let print_task_old _env pr thpr _blacklist ?old:_ fmt task =
forget_all ();
print_prelude fmt pr;
......@@ -386,6 +387,10 @@ let print_task_old _env pr thpr _blacklist ?old:_ fmt task =
fprintf fmt "theory Task@\n%a@\nend@."
(print_list nothing print_tdecl) (Task.task_tdecls task)
let () = register_printer "why3old" print_task_old
~desc:"TODO"
*)
let print_tdecls =
let print sm fmt td =
info := { info_syn = sm };
......@@ -401,8 +406,6 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task =
(print_list nothing string)
(List.rev (Trans.apply print_tdecls task))
let () = register_printer "why3old" print_task_old
~desc:"TODO"
let () = register_printer "why3" print_task
~desc:"Printer@ for@ the@ logical@ format@ of@ why3.@ There@ is@ currently@ \
a@ lose@ of@ informations@ between@ the@ parser@ and@ the@ printer."
~desc:"Printer@ for@ the@ logical@ format@ of@ Why3,@ \
used@ for@ debugging@ purposes."
......@@ -297,16 +297,7 @@ let discriminate env = Trans.seq [
lsymbol_distinction;
]
let empty_formatted : Pp.formatted = ""
let () = Trans.register_env_transform "discriminate" discriminate
~desc_metas:[meta_select_inst , empty_formatted;
meta_select_lskept, empty_formatted;
meta_select_lsinst, empty_formatted;
meta_inst , empty_formatted;
meta_lskept , empty_formatted;
meta_lsinst , empty_formatted]
~desc:"Discriminate@ polymorphic@ function@ and@ predicate@ symbols.@ \
Allow@ to@ keep@ some@ instantiations@ from@ being@ touched@ by@ \
following@ polymorphism@ encodings."
......@@ -435,7 +435,11 @@ let eliminate_match =
Trans.compose compile_match (Trans.fold_map comp empty_state init_task)
let meta_elim = register_meta "eliminate_algebraic" [MTstring]
~desc:"specify@ how@ the@ algebraic@ must@ be@ eliminated."
~desc:"@[<hov 2>configure the 'eliminate_algebraic' transformation:@\n\
\"keep_types\" : @[keep algebraic type definitions@]@\n\
\"keep_enums\" : @[keep monomorphic enumeration types@]@\n\
\"keep_recs\" : @[keep non-recursive records@]@\n\
\"no_index\" : @[do not generate indexing funcitons@]@]"
let eliminate_algebraic = Trans.compose compile_match
(Trans.on_meta meta_elim (fun ml ->
......@@ -490,17 +494,10 @@ let eliminate_projections = Trans.decl elim None
let () =
Trans.register_transform "compile_match" compile_match
~desc:"Transform@ pattern-matching@ with@ nested@ pattern@ \
into@ nested@ pattern-matching@ with@ simple@ patterns.";
into@ nested@ pattern-matching@ with@ flat@ patterns.";
Trans.register_transform "eliminate_match" eliminate_match
~desc:"TODO";
Trans.register_transform "eliminate_algebraic" eliminate_algebraic
~desc_metas:[meta_elim,
("@\n \
@[- keep_types : @[keep algebraic type definitions@]@\n\
- keep_enums : @[keep monomorphic enumeration types@]@\n\
- keep_recs : @[keep non-recursive records@]@\n\
- no_index : @[do not generate indexing funcitons@]\
@]" : Pp.formatted)]
~desc:"Replaces@ algebraic@ data@ types@ by@ first-order@ definitions.";
~desc:"Replace@ algebraic@ data@ types@ by@ first-order@ definitions.";
Trans.register_transform "eliminate_projections" eliminate_projections
~desc:"TODO"
......@@ -48,13 +48,9 @@ let eliminate_builtin =
Trans.decl (elim_abstract undef_ls rem_pr rem_ls rem_ts) None))))
let () = Trans.register_transform "eliminate_builtin" eliminate_builtin
~desc_metas:[Printer.meta_syntax_logic,
("@ Remove@ their@ definitions@ since@ they@ are@ considered@ \
builtin."
: Pp.formatted);
Printer.meta_remove_prop, Pp.empty_formatted]
~desc:"Eliminate@ facts@ which@ are@ builtin@ in@ the@ prover:@ symbol@ \
definitions@ or@ axiomatics."
~desc:"Eliminate@ symbols@ and@ propositions@ that@ are@ builtin@ \
in@ the@ prover@ (see@ 'syntax'@ and@ 'remove'@ clauses@ in@ \
the@ prover's@ driver)."
(** compute the meta_remove_* given two task one included in the other *)
let compute_diff t1 t2 =
......@@ -160,22 +156,18 @@ let () =
~desc:"Same@ as@ eliminate_definition_func/_pred@ at@ the@ same@ time.";
Trans.register_transform "eliminate_recursion"
eliminate_recursion
~desc:"Same@ as@ eliminate_definition@ ,but@ only@ for@ recursive@ \
~desc:"Same@ as@ eliminate_definition,@ but@ only@ for@ recursive@ \
definition";
Trans.register_transform "eliminate_non_struct_recursion"
eliminate_non_struct_recursion
~desc:"Same@ as@ eliminate_recursion@ ,but@ only@ for@ non@ structural@ \
~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ non@ structural@ \
recursive@ definition";
Trans.register_transform "eliminate_mutual_recursion"
eliminate_mutual_recursion
~desc:"Same@ as@ eliminate_recursion@ ,but@ only@ for@ mutual@ \
~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ mutual@ \
recursive@ definition (at@ least@ two@ functions@ or@ \
predicates@ defined@ at@ the@ same@ time)";
(** Bisect *)
open Task
open Theory
......
......@@ -83,14 +83,7 @@ let encoding_tptp env = Trans.seq [
Protect_finite.protect_finite]
let () = register_env_transform "encoding_smt" encoding_smt
~desc_metas:[meta_select_kept, Pp.empty_formatted;
meta_enco_kept, Pp.empty_formatted;
meta_enco_poly, Pp.empty_formatted]
~desc:"encode@ polymorphism@ with@ default@ configuration@ choosed@ for@ \
smt@ solver"
~desc:"encode@ polymorphism@ for@ provers@ with@ sorts"
let () = register_env_transform "encoding_tptp" encoding_tptp
~desc_metas:[meta_select_kept, Pp.empty_formatted;
meta_enco_kept, Pp.empty_formatted;
meta_enco_poly, Pp.empty_formatted]
~desc:"encode@ polymorphism@ with@ default@ configuration@ choosed@ for@ \
tptp@ solver"
~desc:"encode@ polymorphism@ for@ provers@ without@ sorts"
......@@ -22,10 +22,11 @@ open Task
(** TODO use this label in the following function *)
let label_induction = create_label "induction"
(*
let desc_labels = [label_induction,
("Make the induction on the labeled variables." :
Pp.formatted)]
*)
(*********************************************************)
(******* Data type induction principle *********)
......@@ -361,7 +362,7 @@ let induction_ty_lex = function
let () =
Trans.register_transform_l "induction_ty_lex" (Trans.store induction_ty_lex)
~desc_labels ~desc:"TODO: induction on type with lexicographic order"
~desc:"TODO: induction on type with lexicographic order"
(***************************************************************************)
......@@ -484,7 +485,7 @@ let () =
(fun env ->
let th_int = Env.find_theory env ["int"] "Int" in
Trans.store (induction_int_lex th_int))
~desc_labels ~desc:"TODO: induction on integers"
~desc:"TODO: induction on integers"
......
......@@ -119,18 +119,10 @@ let trivial = t ~use_meta:true ~in_goal:false
~notdeft:notdeft ~notdeff:notdeft ~notls:Util.ffalse
let () =
let register ~desc name t =
Trans.register_transform ~desc name t
~desc_metas:[meta, Pp.empty_formatted]
in
register "inline_all" all
~desc:"Inline@ all@ the@ non-recursive@ defined@ symbols.";
register "inline_goal" goal
~desc:"Same@ as@ inline_all, but@ only@ in@ goals.";
register "inline_trivial" trivial
~desc:"Inline@ only@ the@ non-recursive@ symbols@ that@ have@ a@ trivial@ \
definition:\
@[<hov>\
- just@ a@ constant,@\n\
- all the variables appear at most once.@]"
Trans.register_transform "inline_all" all
~desc:"Inline@ non-recursive@ definitions.";
Trans.register_transform "inline_goal" goal
~desc:"Same@ as@ inline_all, but@ only@ inline in@ goals.";
Trans.register_transform "inline_trivial" trivial
~desc:"Inline@ trivial@ definitions@ like@ @[f(x,y) = g(y,x,0)@]."
......@@ -61,7 +61,8 @@ let trans spr task_hd (((lpr, past), task) as current) =
(current, Task.add_tdecl task task_hd.Task.task_decl)
let meta = Theory.register_meta "instantiate : auto" [Theory.MTprsymbol]
~desc:"Mark proposition that should be automatically instantiated."
~desc:"Mark@ proposition@ that@ should@ be@ automatically@ instantiated@ \
by@ the@ 'instantiate_predicate'@ transformation."
(** all the symbols (unary predicates) that have the "instantiate : auto"
meta are marked for instantiation by the above transformation *)
......@@ -69,6 +70,5 @@ let () =
Trans.register_transform "instantiate_predicate"
(Trans.on_tagged_pr meta (fun spr ->
Trans.fold_map (trans spr) ([], Sterm.empty) None))
~desc_metas:[meta,Pp.empty_formatted]
~desc:"Look@ into@ all@ the@ task@ for@ terms@ that@ can@ instantiate@ \
proposition@ marked@ by@ the@ meta."
proposition@ marked@ by@ the@ 'instantiate : auto'@ meta."
......@@ -176,40 +176,34 @@ let split_premise_full = Trans.decl (split_premise full_split) None
let split_premise_right = Trans.decl (split_premise right_split) None
let split_premise_wp = Trans.decl (split_premise wp_split) None
let desc_labels =
[asym_split,
("Use@ the@ left@ part@ as@ hypothesis@ for@ the@ right@ part@ of@ \
the@ labeled@ term.": Pp.formatted);
stop_split,("Don't@ split@ the@ labeled@ term.": Pp.formatted)]
let () = Trans.register_transform_l "split_goal_full" split_goal_full
~desc_labels ~desc:"Puts@ the@ goal@ in@ a@ conjunctive@ form,@ \
~desc:"Puts@ the@ goal@ in@ a@ conjunctive@ form,@ \
returns@ the@ corresponding@ set@ of@ subgoals.@ The@ number@ of@ subgoals@ \
generated@ may@ be@ exponential@ in@ the@ size@ of@ the@ initial@ goal."
let () = Trans.register_transform_l "split_all_full" split_all_full
~desc_labels ~desc:"Same@ as@ split_goal_full,@ but@ also@ splits@ premises."
~desc:"Same@ as@ split_goal_full,@ but@ also@ splits@ premises."
let () = Trans.register_transform "split_premise_full" split_premise_full
~desc_labels ~desc:"Same@ as@ split_all_full,@ but@ splits@ only@ premises."
~desc:"Same@ as@ split_all_full,@ but@ splits@ only@ premises."
let () = Trans.register_transform_l "split_goal_right" split_goal_right
~desc_labels ~desc:"Same@ as@ split_goal_full,@ but@ don't@ split:@\n \
@[- @[conjunctions under disjunctions@]@\n\
~desc:"@[<hov 2>Same@ as@ split_goal_full,@ but@ don't@ split:@,\
- @[conjunctions under disjunctions@]@\n\
- @[conjunctions on the left of implications.@]@]"
let () = Trans.register_transform_l "split_all_right" split_all_right
~desc_labels ~desc:"Same@ as@ split_goal_right,@ but@ also@ splits@ premises."
~desc:"Same@ as@ split_goal_right,@ but@ also@ splits@ premises."
let () = Trans.register_transform "split_premise_right" split_premise_right
~desc_labels ~desc:"Same@ as@ split_all_right,@ but@ splits@ only@ premises."
~desc:"Same@ as@ split_all_right,@ but@ splits@ only@ premises."
let () = Trans.register_transform_l "split_goal_wp" split_goal_wp
~desc_labels ~desc:"Same@ as@ split_goal_right,@ but@ stops@ at@ \
the `stop_split' label and removes the label."
~desc:"Same@ as@ split_goal_right,@ but@ stops@ at@ \
the@ `stop_split'@ label@ and@ removes@ the@ label."
let () = Trans.register_transform_l "split_all_wp" split_all_wp
~desc_labels ~desc:"Same@ as@ split_goal_wp,@ but@ also@ splits@ premises."
~desc:"Same@ as@ split_goal_wp,@ but@ also@ splits@ premises."
let () = Trans.register_transform "split_premise_wp" split_premise_wp
~desc_labels ~desc:"Same@ as@ split_all_wp,@ but@ splits@ only@ premises."
~desc:"Same@ as@ split_all_wp,@ but@ splits@ only@ premises."
let () = Trans.register_transform_l "split_goal" split_goal_wp
~desc_labels ~desc:"The@ deprecated@ name@ of@ split_goal_wp,@ \
~desc:"The@ deprecated@ name@ of@ split_goal_wp,@ \
kept@ for@ compatibility@ purposes."
let ls_of_var v =
......@@ -250,5 +244,5 @@ let rec split_intro pr dl acc f =
let split_intro = Trans.goal_l (fun pr f -> split_intro pr [] [] f)
let () = Trans.register_transform_l "split_intro" split_intro
~desc_labels ~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
the@ implication@ antecedents@ to@ premises."
......@@ -215,17 +215,21 @@ let () =
let opt_list = ref false in
if !opt_list_transforms then begin
opt_list := true;
let print_trans_desc fmt (x,r) =
fprintf fmt "@[<hov 2>%s@\n%a@]" x Pp.formatted r in
printf "@[<hov 2>Known non-splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline Trans.print_trans_desc)
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms ()));
printf "@[<hov 2>Known splitting transformations:@\n%a@]@\n@."
(Pp.print_list Pp.newline Trans.print_trans_desc)
(Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms_l ()))
end;
if !opt_list_printers then begin
opt_list := true;
let print_printer_desc fmt (s,f) =
fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" s Pp.formatted f in
printf "@[<hov 2>Known printers:@\n%a@]@\n@."
(Pp.print_list Pp.newline Printer.print_printer_desc)
(Pp.print_list Pp.newline2 print_printer_desc)
(List.sort sort_pair (Printer.list_printers ()))
end;
if !opt_list_formats then begin
......
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