From 35e052f78f3556b32e2e76c3f68a5bec7a9d4220 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Mon, 29 Oct 2012 17:09:34 +0100 Subject: [PATCH] update descriptions --- src/core/printer.ml | 2 +- src/core/trans.ml | 3 +- src/driver/autodetection.ml | 3 +- src/driver/call_provers.ml | 3 +- src/parser/glob.ml | 4 +- src/parser/typing.ml | 4 +- src/printer/alt_ergo.ml | 7 +- src/printer/gappa.ml | 23 +++--- src/printer/smtv1.ml | 2 +- src/printer/smtv2.ml | 4 +- src/printer/why3printer.ml | 7 +- src/session/session.ml | 3 +- src/session/session_scheduler.ml | 4 +- src/session/termcode.ml | 5 +- src/session/xml.mll | 6 +- src/transform/close_epsilon.ml | 2 +- src/transform/discriminate.ml | 70 +++++++++---------- src/transform/eliminate_algebraic.ml | 13 ++-- src/transform/eliminate_definition.ml | 23 +++--- src/transform/eliminate_if.ml | 11 ++- src/transform/eliminate_inductive.ml | 4 +- src/transform/eliminate_let.ml | 7 +- src/transform/encoding.ml | 55 +++++++-------- src/transform/encoding_sort.ml | 3 +- src/transform/filter_trigger.ml | 13 ++-- src/transform/induction.ml | 25 ++----- src/transform/inlining.ml | 4 +- src/transform/instantiate_predicate.ml | 4 +- src/transform/introduction.ml | 1 + src/transform/libencoding.ml | 4 +- src/transform/lift_epsilon.ml | 10 ++- src/transform/simplify_array.ml | 5 +- src/transform/simplify_formula.ml | 8 +-- .../simplify_recursive_definition.ml | 2 +- src/transform/smoke_detector.ml | 14 ++-- src/transform/split_goal.ml | 14 ++-- src/util/debug.ml | 2 +- src/util/plugin.ml | 2 +- src/why3bench/bench.ml | 5 +- src/why3bench/benchdb.ml | 2 +- src/why3bench/why3bench.ml | 2 +- src/whyml/mlw_ocaml.ml | 4 +- src/whyml/mlw_wp.ml | 3 +- 43 files changed, 185 insertions(+), 207 deletions(-) diff --git a/src/core/printer.ml b/src/core/printer.ml index 7923c7beb..bfaeeabc7 100644 --- a/src/core/printer.ml +++ b/src/core/printer.ml @@ -215,7 +215,7 @@ let meta_remove_logic = register_meta "remove_logic" [MTlsymbol] Used@ in@ bisection." let meta_realized_theory = register_meta "realized_theory" [MTstring; MTstring] - ~desc:"Specify@ that@ a@ Why3@ theory@ is@ \"realized\"@ as@ a@ module@ \ + ~desc:"Specify@ that@ a@ Why3@ theory@ is@ realized@ as@ a@ module@ \ in@ an@ ITP." let check_syntax_type ts s = check_syntax s (List.length ts.ts_args) diff --git a/src/core/trans.ml b/src/core/trans.ml index e5fcb0e7a..99ebdc7c4 100644 --- a/src/core/trans.ml +++ b/src/core/trans.ml @@ -17,7 +17,8 @@ open Theory open Task let debug = Debug.register_info_flag "transform" - ~desc:"Be@ verbose@ about@ application@ of@ proof@ task@ transformations." + ~desc:"Print@ debugging@ messages@ about@ application@ \ + of@ proof@ task@ transformations." (** Task transformation *) diff --git a/src/driver/autodetection.ml b/src/driver/autodetection.ml index 3b224454a..91f9160d7 100644 --- a/src/driver/autodetection.ml +++ b/src/driver/autodetection.ml @@ -46,7 +46,8 @@ module Wc = Whyconf open Rc let debug = Debug.register_info_flag "autodetect" - ~desc:"Be@ verbose@ about@ autodetection@ of@ external@ provers." + ~desc:"Print@ debugging@ messages@ about@ auto-detection@ \ + of@ external@ provers." (* auto-detection of provers *) diff --git a/src/driver/call_provers.ml b/src/driver/call_provers.ml index cc464471a..8d0027e06 100644 --- a/src/driver/call_provers.ml +++ b/src/driver/call_provers.ml @@ -113,7 +113,8 @@ let rec grep out l = match l with let debug = Debug.register_info_flag "call_prover" - ~desc:"Be@ verbose@ about@ prover@ calls@ and@ keep@ temporary@ files." + ~desc:"Print@ debugging@ messages@ about@ prover@ calls@ \ + and@ keep@ temporary@ files." type post_prover_call = unit -> prover_result diff --git a/src/parser/glob.ml b/src/parser/glob.ml index 510b4e66a..1e5b6fcfe 100644 --- a/src/parser/glob.ml +++ b/src/parser/glob.ml @@ -11,8 +11,8 @@ open Ident -let flag = Debug.register_flag "track_use" - ~desc:"Track@ use/clone@ instructions.@ Used@ by@ why3doc." +let flag = Debug.register_flag "track_symbol_use" + ~desc:"Track@ symbol@ occurrences@ in@ source@ files.@ Used@ by@ why3doc." let () = Debug.unset_flag flag (* make sure it is unset by default *) diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 0b821e380..227d7f775 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -73,9 +73,9 @@ let () = Exn_printer.register (fun fmt e -> match e with | _ -> raise e) let debug_parse_only = Debug.register_flag "parse_only" - ~desc:"Stop@ after@ the@ parsing." + ~desc:"Stop@ after@ parsing." let debug_type_only = Debug.register_flag "type_only" - ~desc:"Stop@ after@ the@ typing." + ~desc:"Stop@ after@ type-checking." (** Environments *) diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml index 570ec4646..2333f3dad 100644 --- a/src/printer/alt_ergo.ml +++ b/src/printer/alt_ergo.ml @@ -20,10 +20,11 @@ open Decl open Printer let meta_ac = Theory.register_meta "AC" [Theory.MTlsymbol] - ~desc:"Specify that a symbol is associative and commutative." + ~desc:"Specify@ that@ a@ symbol@ is@ associative@ and@ commutative." + let meta_printer_option = Theory.register_meta "printer_option" [Theory.MTstring] - ~desc:"Some paramters given to the printer." + ~desc:"Pass@ additional@ parameters@ to@ the@ pretty-printer." type info = { info_syn : syntax_map; @@ -366,7 +367,7 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task = (List.rev (Trans.apply print_decls task)) let () = register_printer "alt-ergo" print_task - ~desc:"Printer for the alt-ergo theorem provers" + ~desc:"Printer for the Alt-Ergo theorem prover." (* let print_goal info fmt (id, f, task) = print_task info fmt task; diff --git a/src/printer/gappa.ml b/src/printer/gappa.ml index 0c43c8e79..0dedc388f 100644 --- a/src/printer/gappa.ml +++ b/src/printer/gappa.ml @@ -31,7 +31,8 @@ let syntactic_transform transf = let () = Trans.register_transform "abstract_unknown_lsymbols" (syntactic_transform Abstraction.abstraction) - ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ constants."; + ~desc:"Abstract@ applications@ of@ non-built-in@ symbols@ with@ \ + constants.@ Used@ by@ the@ Gappa@ pretty-printer."; Trans.register_transform "simplify_unknown_lsymbols" (syntactic_transform (fun check_ls -> Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (Simplify_formula.fmla_cond_subst @@ -45,8 +46,9 @@ let () = | Tapp(ls,_) -> not (check_ls ls) | _ -> true) f) ]))) - ~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ of@ substituting@ quantified@ variables,@ substitute@ applications@ of@ non-buit-in@ symbols."; - + ~desc:"Same@ as@ simplify_trivial_quantification_in_goal,@ but@ instead@ \ + of@ substituting@ quantified@ variables,@ substitute@ applications@ \ + of@ non-buit-in@ symbols.@ Used@ by@ the@ Gappa@ pretty-printer." (* patterns (TODO: add a parser and generalize it out of Gappa) *) @@ -91,13 +93,14 @@ let real_minus = ref ps_equ (** lsymbol, ""/"not ", op, rev_op *) let arith_meta = register_meta "gappa arith" [MTlsymbol;MTstring;MTstring;MTstring] - ~desc:"Specifies how to pretty-print symbols into gappa format:@\n \ -@[\ - @[- first argument: which symbol@]@\n\ - @[- second argument: which prefix around the term@]@\n\ - @[- third argument: which operator to pretty-print@]@\n\ - @[- fourth argument: which is the inverse operator to pretty-print@]\ -@]" + ~desc:"Specify@ how@ to@ pretty-print@ arithmetic@ \ + operations@ in@ the@ Gappa@ format:@\n \ + @[\ + @[- first@ argument:@ the@ symbol@]@\n\ + @[- second@ argument:@ the@ prefix@ to@ put@ before@ the@ term@]@\n\ + @[- third@ argument:@ the@ operator@ to@ print@]@\n\ + @[- fourth@ argument:@ the@ inverse@ operator@]\ + @]" let find_th env file th = let theory = Env.find_theory env [file] th in diff --git a/src/printer/smtv1.ml b/src/printer/smtv1.ml index c5b61efa7..6496bab1c 100644 --- a/src/printer/smtv1.ml +++ b/src/printer/smtv1.ml @@ -223,4 +223,4 @@ let () = register_printer "smtv1" (fun _env pr thpr blacklist ?old:_ fmt task -> forget_all ident_printer; print_task pr thpr blacklist fmt task) - ~desc:"Printer@ for@ the@ smtlib@ version@ 1@ format." + ~desc:"Printer@ for@ the@ SMTlib@ version@ 1@ format." diff --git a/src/printer/smtv2.ml b/src/printer/smtv2.ml index 49c60bd18..7cf5c2195 100644 --- a/src/printer/smtv2.ml +++ b/src/printer/smtv2.ml @@ -317,7 +317,7 @@ let () = register_printer "smtv2" (fun _env pr thpr blacklist ?old:_ fmt task -> forget_all ident_printer; print_task_old pr thpr blacklist fmt task) - ~desc:"Printer for the smtlib version 2 format." + ~desc:"Printer for the SMTlib version 2 format." (* let print_decls = @@ -344,5 +344,5 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task = (List.rev (Trans.apply print_decls task)) let () = register_printer "smtv2new" print_task - ~desc:"New (TODO: in which sense?) printer for the smtlib version 2 format." + ~desc:"Printer for the SMTlib version 2 format." *) diff --git a/src/printer/why3printer.ml b/src/printer/why3printer.ml index 021f3545a..caefd11e1 100644 --- a/src/printer/why3printer.ml +++ b/src/printer/why3printer.ml @@ -386,8 +386,7 @@ 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 () = register_printer "why3old" print_task_old ~desc:"" *) let print_tdecls = @@ -406,5 +405,5 @@ let print_task _env pr thpr _blacklist ?old:_ fmt task = (List.rev (Trans.apply print_tdecls task)) let () = register_printer "why3" print_task - ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3,@ \ - used@ for@ debugging@ purposes." + ~desc:"Printer@ for@ the@ logical@ format@ of@ Why3.@ \ + Used@ for@ debugging." diff --git a/src/session/session.ml b/src/session/session.ml index f9a744fb1..9fe65b444 100644 --- a/src/session/session.ml +++ b/src/session/session.ml @@ -25,7 +25,8 @@ module C = Whyconf module Tc = Termcode let debug = Debug.register_info_flag "session" - ~desc:"About the why3 session creation, reading and writing." + ~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \ + creation,@ reading@ and@ writing." (** {2 Type definitions} *) diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index b39430a86..709f6d38d 100644 --- a/src/session/session_scheduler.ml +++ b/src/session/session_scheduler.ml @@ -14,8 +14,8 @@ open Session open Debug let debug = register_info_flag "scheduler" - ~desc:"About@ the@ session@ scheduler@ which@ schedules@ the@ application@ \ - of@ transformtions@ or@ the@ call@ of@ provers." + ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls@ \ + and@ transformtion@ applications." (***************************) (* main functor *) diff --git a/src/session/termcode.ml b/src/session/termcode.ml index 533cfc815..cd5843a70 100644 --- a/src/session/termcode.ml +++ b/src/session/termcode.ml @@ -24,9 +24,8 @@ let string_of_shape x = x let shape_of_string x = x let debug = Debug.register_info_flag "session_pairing" - ~desc:"About@ the@ way@ old@ goals@ recorded@ in@ sessions@ are@ paired@ \ - with@ new@ goals@ obtained@ after@ modifications@ of@ the@ source@ \ - file." + ~desc:"Print@ debugging@ messages@ about@ reconstruction@ of@ \ + session@ trees@ after@ modification@ of@ source@ files." let current_shape_version = 2 diff --git a/src/session/xml.mll b/src/session/xml.mll index ea6e4b10e..dfbc8c6b8 100644 --- a/src/session/xml.mll +++ b/src/session/xml.mll @@ -9,10 +9,8 @@ (* *) (********************************************************************) - { - - type element = + type element = { name : string; attributes : (string * string) list; elements : element list; @@ -44,7 +42,7 @@ let parse_error s = raise (Parse_error s) open Debug let debug = register_info_flag "xml" - ~desc:"About the xml parsing." + ~desc:"Print@ the@ XML@ parser@ debugging@ messages." } let space = [' ' '\t' '\r' '\n'] diff --git a/src/transform/close_epsilon.ml b/src/transform/close_epsilon.ml index 7ac123e84..0670ccfa2 100644 --- a/src/transform/close_epsilon.ml +++ b/src/transform/close_epsilon.ml @@ -78,6 +78,6 @@ let close_epsilon = if used then Trans.decl close None else Trans.identity) let () = Trans.register_transform "close_epsilon" close_epsilon - ~desc:"TODO" + ~desc:"Beta-abstract free variables out of lambda-terms." (* TODO variable abstraction *) diff --git a/src/transform/discriminate.ml b/src/transform/discriminate.ml index edc255a43..e33a426dc 100644 --- a/src/transform/discriminate.ml +++ b/src/transform/discriminate.ml @@ -17,48 +17,43 @@ open Decl open Theory open Task -let meta_inst = register_meta "encoding : inst" [MTty] - ~desc:"Specify@ which@ type@ should@ instantiate@ symbol@ marked@ by@ \ +let meta_inst = register_meta "encoding : inst" [MTty] + ~desc:"Specify@ which@ types@ should@ instantiate@ symbols@ marked@ by@ \ 'encoding : lskept'." + let meta_lskept = register_meta "encoding : lskept" [MTlsymbol] - ~desc:"Specify@ which@ function@ symbols@ should@ be@ kept.@ If@ the@ \ - function@ is@ polymorphic,@ the@ monorphisations@ which@ signatures@ \ - contain@ only@ types@ @ marked@ with@ 'encoding : inst'@ are@ kept." + ~desc:"Specify@ which@ function/predicate@ symbols@ should@ be@ kept.@ \ + When@ the@ symbol@ is@ polymorphic,@ generate@ every@ possible@ \ + type@ insntance@ with@ types@ marked@ by@ 'encoding : inst'." + let meta_lsinst = register_meta "encoding : lsinst" [MTlsymbol;MTlsymbol] - ~desc:"Specify@ which@ instantiations@ of@ symbols@ should@ be@ kept.@ \ - The first@ symbol@ specifies@ the@ symbol,@ the@ signature@ of@ the@ \ - second@ specifies@ the@ instantiation@ to@ keep." - -let meta_select_inst = register_meta_excl "select_inst" [MTstring] - ~desc:"@[Specify@ how@ to@ automatically@ mark@ type@ by@ \ -'encoding : inst':@]@\n \ -@[\ - - none:@[ don't@ mark@ automatically@]@\n\ - - goal:@[ mark@ all@ the@ closed@ type@ that@ appear@ has@ argument@ \ - in@ the@ goal@]@\n\ - - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\ -@]" + ~desc:"Specify@ which@ type@ instances@ of@ symbols@ should@ be@ kept.@ \ + The first@ symbol@ specifies@ the@ polymorphic@ symbol,@ \ + the@ second@ provides@ a@ monomorphic@ type@ signature@ to@ keep." + +let meta_select_inst = register_meta_excl "select_inst" [MTstring] + ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : inst':@; \ + @[\ + - none: @[don't@ mark@ any@ type@ automatically@]@\n\ + - goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\ + - all: @[mark@ every@ closed@ type@ in@ the@ task.@]\ + @]" let meta_select_lskept = register_meta_excl "select_lskept" [MTstring] - ~desc:"@[Specify@ how@ to@ automatically@ mark@ symbol@ by@ \ -'encoding : lskept':@]@\n \ -@[\ - - none:@[ don't@ mark@ automatically@]@\n\ - - goal:@[ mark@ all@ the@ symbols@ acceptable@ that@ appear@ in@ the@ \ - goal.@ The signature@ of an@ acceptable@ symbol@ contain@ at@ \ - least@ one@ type@ that@ is@ not@ a@ type@ variable@ neither@]@\n\ - - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\ -@]" + ~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lskept':@; \ + @[\ + - none: @[don't@ mark@ any@ symbol@ automatically@]@\n\ + - goal: @[mark@ every@ polymorphic@ symbol@ in@ the@ goal@]@\n\ + - all: @[mark@ every@ polymorphic@ symbol@ in@ the@ task.@]\ + @]" let meta_select_lsinst = register_meta_excl "select_lsinst" [MTstring] - ~desc:"@[Specify@ how@ to@ automatically@ mark@ symbol@ by@ \ -'encoding : lskept':@]@\n \ -@[\ - - none:@[ don't@ mark@ automatically@]@\n\ - - goal:@[ mark@ all@ the@ instantiation of symbols@ that@ appear@ in@ \ - the@ goal@]@\n\ - - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\ -@]" + ~desc:"Specify@ the@ symbols@ to@ mark@ with@ 'encoding : lsinst':@; \ + @[\ + - none: @[don't@ mark@ any@ symbol@ automatically@]@\n\ + - goal: @[mark@ every@ monomorphic@ instance@ in@ the@ goal@]@\n\ + - all: @[mark@ every@ monomorphic@ instance@ in@ the@ task.@]\ + @]" module OHTy = OrderedHashed(struct type t = ty @@ -298,6 +293,5 @@ let discriminate env = Trans.seq [ ] let () = Trans.register_env_transform "discriminate" discriminate - ~desc:"Discriminate@ polymorphic@ function@ and@ predicate@ symbols.@ \ - Allow@ to@ keep@ some@ instantiations@ from@ being@ touched@ by@ \ - following@ polymorphism@ encodings." + ~desc:"Generate@ monomorphic@ type@ instances@ of@ function@ and@ \ + predicate@ symbols@ and@ monomorphize@ task@ premises." diff --git a/src/transform/eliminate_algebraic.ml b/src/transform/eliminate_algebraic.ml index ab815c26f..6d3f3e2f5 100644 --- a/src/transform/eliminate_algebraic.ml +++ b/src/transform/eliminate_algebraic.ml @@ -22,6 +22,7 @@ open Task let meta_infinite = register_meta "infinite_type" [MTtysymbol] ~desc:"Specify@ that@ the@ given@ type@ has@ always@ an@ infinite@ \ cardinality." + let meta_material = register_meta "material_type_arg" [MTtysymbol;MTint] ~desc:"If@ the@ given@ type@ argument@ is@ instantiated@ by@ an@ infinite@ \ type@ then@ the@ associated@ type@ constructor@ is@ infinite" @@ -267,9 +268,9 @@ let add_indexer acc ts ty = function let meta_proj = (* projection symbol, constructor symbol, position, defining axiom *) register_meta "algtype projection" [MTlsymbol;MTlsymbol;MTint;MTprsymbol] - ~desc:"Specifies@ which@ projection@ symbol@ is@ used@ for@ the@ \ + ~desc:"Specify@ which@ projection@ symbol@ is@ used@ for@ the@ \ given@ constructor@ at@ the@ specified@ position.@ \ - Internally@ used." + For@ internal@ use." let add_projections (state,task) _ts _ty csl = (* declare and define the projection functions *) @@ -434,7 +435,7 @@ let eliminate_match = Trans.compose compile_match (Trans.fold_map comp empty_state init_task) let meta_elim = register_meta "eliminate_algebraic" [MTstring] - ~desc:"@[configure the 'eliminate_algebraic' transformation:@\n\ + ~desc:"@[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\ @@ -492,11 +493,11 @@ let eliminate_projections = Trans.decl elim None let () = Trans.register_transform "compile_match" compile_match - ~desc:"Transform@ pattern-matching@ with@ nested@ pattern@ \ + ~desc:"Transform@ pattern-matching@ with@ nested@ patterns@ \ into@ nested@ pattern-matching@ with@ flat@ patterns."; Trans.register_transform "eliminate_match" eliminate_match - ~desc:"TODO"; + ~desc:"Eliminate@ all@ pattern-matching@ expressions."; Trans.register_transform "eliminate_algebraic" eliminate_algebraic ~desc:"Replace@ algebraic@ data@ types@ by@ first-order@ definitions."; Trans.register_transform "eliminate_projections" eliminate_projections - ~desc:"TODO" + ~desc:"Define@ algebraic@ projection@ symbols@ separately." diff --git a/src/transform/eliminate_definition.ml b/src/transform/eliminate_definition.ml index 8b8ab28c0..b8ef0feac 100644 --- a/src/transform/eliminate_definition.ml +++ b/src/transform/eliminate_definition.ml @@ -48,9 +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:"Eliminate@ symbols@ and@ propositions@ that@ are@ builtin@ \ - in@ the@ prover@ (see@ 'syntax'@ and@ 'remove'@ clauses@ in@ \ - the@ prover's@ driver)." + ~desc:"Eliminate@ propositions@ and@ definitions@ of@ symbols@ \ + 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 = @@ -147,26 +147,25 @@ let eliminate_mutual_recursion = Trans.decl elim_mutual None let () = Trans.register_transform "eliminate_definition_func" eliminate_definition_func - ~desc:"Transform@ function@ definition@ into@ axioms."; + ~desc:"Transform@ function@ definitions@ into@ axioms."; Trans.register_transform "eliminate_definition_pred" eliminate_definition_pred - ~desc:"Transform@ predicate@ definition@ into@ axioms."; + ~desc:"Transform@ predicate@ definitions@ into@ axioms."; Trans.register_transform "eliminate_definition" eliminate_definition - ~desc:"Same@ as@ eliminate_definition_func/_pred@ at@ the@ same@ time."; + ~desc:"Transform@ function@ and@ predicate@ definitions@ into@ axioms."; Trans.register_transform "eliminate_recursion" eliminate_recursion ~desc:"Same@ as@ eliminate_definition,@ but@ only@ for@ recursive@ \ - definition"; + definitions."; Trans.register_transform "eliminate_non_struct_recursion" eliminate_non_struct_recursion - ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ non@ structural@ \ - recursive@ definition"; + ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ non-structural@ \ + recursive@ definitions."; Trans.register_transform "eliminate_mutual_recursion" eliminate_mutual_recursion - ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ mutual@ \ - recursive@ definition (at@ least@ two@ functions@ or@ \ - predicates@ defined@ at@ the@ same@ time)"; + ~desc:"Same@ as@ eliminate_recursion,@ but@ only@ for@ mutually@ \ + recursive@ definitions." (** Bisect *) open Task diff --git a/src/transform/eliminate_if.ml b/src/transform/eliminate_if.ml index d75af6e2d..5b4921878 100644 --- a/src/transform/eliminate_if.ml +++ b/src/transform/eliminate_if.ml @@ -105,12 +105,9 @@ let eliminate_if = Trans.compose eliminate_if_term eliminate_if_fmla let () = Trans.register_transform "eliminate_if_term" eliminate_if_term - ~desc:"Replaces@ terms@ of@ the@ form@ [if formula then t2 else t3]@ by@ \ - lifting@ them@ at@ the@ level@ of@ formulas.@ This@ may@ introduce@ \ - [if then else]@ in@ formulas."; + ~desc:"Replaces@ terms@ of@ the@ form@ [if f1 then t2 else t3]@ by@ \ + lifting@ them@ at@ the@ level@ of@ formulas."; Trans.register_transform "eliminate_if_fmla" eliminate_if_fmla - ~desc:"Replaces@ formulas@ of@ the@ form@ [if f1 then f2\ - else f3]@ by@ an@ equivalent@ formula@ using@ implications@ and@ \ - other@ connectives."; + ~desc:"Eliminate@ formulas@ of@ the@ form@ [if f1 then f2 else f3]."; Trans.register_transform "eliminate_if" eliminate_if - ~desc:"Apply@ both@ eliminate_if_term/fmla." + ~desc:"Eliminate@ all@ if-expressions." diff --git a/src/transform/eliminate_inductive.ml b/src/transform/eliminate_inductive.ml index 190e74a05..887c44850 100644 --- a/src/transform/eliminate_inductive.ml +++ b/src/transform/eliminate_inductive.ml @@ -52,5 +52,5 @@ let elim d = match d.d_node with let eliminate_inductive = Trans.decl elim None let () = Trans.register_transform "eliminate_inductive" eliminate_inductive - ~desc:"replaces@ inductive@ predicates@ by@ (incomplete)@ axiomatic@ \ - definitions,@ ie@ construction@ axioms@ and@ an@ inversion@ axiom." + ~desc:"Replace@ inductive@ predicates@ by@ (incomplete)@ axiomatic@ \ + definitions,@ i.e.@ construction@ axioms@ and@ an@ inversion@ axiom." diff --git a/src/transform/eliminate_let.ml b/src/transform/eliminate_let.ml index ca63a4c06..3eb94b5a8 100644 --- a/src/transform/eliminate_let.ml +++ b/src/transform/eliminate_let.ml @@ -29,9 +29,8 @@ let eliminate_let = Trans.rewrite (elim_t true true Mvs.empty) None let () = Trans.register_transform "eliminate_let_term" eliminate_let_term - ~desc:"Eliminates@ let@ by@ substitution,@ at@ the@ term@ level."; + ~desc:"Eliminate@ let-expressions@ in@ terms."; Trans.register_transform "eliminate_let_fmla" eliminate_let_fmla - ~desc:"Eliminates@ let@ by@ substitution,@ at@ the@ predicate@ level."; + ~desc:"Eliminate@ let-expressions@ in@ formulas."; Trans.register_transform "eliminate_let" eliminate_let - ~desc:"Apply@ both@ eliminate_let_term/fmla" - + ~desc:"Eliminate@ all@ let-expressions."; diff --git a/src/transform/encoding.ml b/src/transform/encoding.ml index 894b7e260..20c284c13 100644 --- a/src/transform/encoding.ml +++ b/src/transform/encoding.ml @@ -16,35 +16,30 @@ open Task open Trans let meta_select_kept = register_meta_excl "select_kept" [MTstring] - ~desc:"@[Specify@ how@ to@ automatically@ choose@ the@ type@ that@ are@ \ - kept@ (mark@ by@ 'encoding : kept')@ by@ the@ polymorphic@ \ - encoding:@]@\n \ -@[\ - - none:@[ don't@ mark@ automatically@]@\n\ - - goal:@[ mark@ all@ the@ closed@ type@ that@ appear@ has@ argument@ \ - in@ the@ goal@]@\n\ - - all:@[ same@ as@ goal@ but@ also@ in@ the@ premises.@]\ -@]" -let meta_enco_kept = register_meta_excl "enco_kept" [MTstring] - ~desc:"@[Specify@ how@ to@ keep@ type:@]@\n \ -@[\ - - @[twin: use@ conversion@ function@ between@ the@ kept@ types@ \ - and@ the@ universal@ type (a complete encoding)@]@\n\ - - @[instantiate: instantiate all the axioms with the kept types@]@\n\ - - @[instantiate_complete: same@ as@ instantiate@ but@ keep@ a@ \ - version@ not@ instantiated(a@ complete@ encoding).@]\ -@]" + ~desc:"Specify@ the@ types@ to@ mark@ with@ 'encoding : kept':@; \ + @[\ + - none: @[don't@ mark@ any@ type@ automatically@]@\n\ + - goal: @[mark@ every@ closed@ type@ in@ the@ goal@]@\n\ + - all: @[mark@ every@ closed@ type@ in@ the@ task.@]\ + @]" + +let meta_enco_kept = register_meta_excl "enco_kept" [MTstring] + ~desc:"Specify@ the@ type@ protection@ transformation:@; \ + @[\ + - @[twin: use@ conversion@ functions@ between@ the@ kept@ types@ \ + and@ the@ universal@ type@]@\n\ + - @[instantiate: instantiate the axioms with the kept types@ \ + and@ throw@ out@ polymorphic@ formulas@ (incomplete).@]@\n\ + - @[instantiate_complete: same@ as@ 'instantiate'@ but@ keep@ \ + polymorphic@ formulas.@]\ + @]" + let meta_enco_poly = register_meta_excl "enco_poly" [MTstring] - ~desc:"@[Specify@ how@ to@ keep@ encode@ polymorphism:@]@\n \ -@[\ - - @[decoexp: TODO @]@\n\ - - @[decorate: add@ around@ all@ the@ terms@ a@ function@ which@ \ - give@ the@ type@ of@ the@ terms@]@\n\ - - @[guard: add@ guards@ (hypothesis)@ in@ all@ the@ axioms@ about@ \ - the@ type@ of@ the@ variables@]@\n\ - - @[explicit: add@ type@ argument@ to@ all@ the@ polymorphic@ \ - functions@]\ -@]" + ~desc:"Specify@ the@ type@ encoding@ transformation:@; \ + @[\ + - @[decorate: put@ type@ annotations@ on@ top@ of@ terms@]@\n\ + - @[guard: add@ type@ conditions@ under@ quantifiers.@]\ + @]" let def_enco_select_smt = "none" let def_enco_kept_smt = "twin" @@ -83,7 +78,7 @@ let encoding_tptp env = Trans.seq [ Protect_finite.protect_finite] let () = register_env_transform "encoding_smt" encoding_smt - ~desc:"encode@ polymorphism@ for@ provers@ with@ sorts" + ~desc:"Encode@ polymorphic@ types@ for@ provers@ with@ sorts." let () = register_env_transform "encoding_tptp" encoding_tptp - ~desc:"encode@ polymorphism@ for@ provers@ without@ sorts" + ~desc:"Encode@ polymorphic@ types@ for@ provers@ without@ sorts." diff --git a/src/transform/encoding_sort.ml b/src/transform/encoding_sort.ml index 0e8c07cff..d7b54eef8 100644 --- a/src/transform/encoding_sort.ml +++ b/src/transform/encoding_sort.ml @@ -172,5 +172,4 @@ let t = Trans.fold (fold tenv) None let () = Trans.register_transform "encoding_sort" t - ~desc:"Remove@ each@ type@ application@ by@ discriminating@ it@ into@ one@ \ - specific@ constant@ type." + ~desc:"Replace@ every@ closed@ type@ by@ a@ separate@ type@ constant." diff --git a/src/transform/filter_trigger.ml b/src/transform/filter_trigger.ml index f64421dc7..06cf0a3ab 100644 --- a/src/transform/filter_trigger.ml +++ b/src/transform/filter_trigger.ml @@ -36,7 +36,7 @@ let remove_triggers = Trans.rewriteTF rt rf None let () = Trans.register_transform "remove_triggers" remove_triggers - ~desc:"Remove@ all@ the@ triggers@ from@ quantifiers." + ~desc:"Remove@ all@ triggers@ from@ quantifiers." let keep_no_predicate e = e.t_ty <> None @@ -46,7 +46,7 @@ let filter_trigger_no_predicate = let () = Trans.register_transform "filter_trigger_no_predicate" filter_trigger_no_predicate - ~desc:"Keep@ only@ triggers@ which@ patterns@ are@ terms." + ~desc:"Remove@ all@ formula@ triggers@ from@ quantifiers." let keep_no_fmla = function | { t_ty = Some _ } -> true @@ -58,9 +58,8 @@ let filter_trigger = Trans.rewriteTF rt rf None let () = Trans.register_transform "filter_trigger" filter_trigger - ~desc:"Same@ as@ filter_trigger_no_predicate@ but@ keep@ also@ pattern@ \ - that@ are@ a@ predicate@ application@ (except@ equality)." - + ~desc:"Remove@ all@ complex@ formula@ triggers@ \ + (anything@ but@ predicate@ applications)." let keep_no_builtin rem_ls = function | { t_ty = Some _ } -> true @@ -75,5 +74,5 @@ let filter_trigger_builtin = let () = Trans.register_transform "filter_trigger_builtin" filter_trigger_builtin - ~desc:"Same@ as@ filter_trigger_no_predicate@ but@ keep@ also@ pattern@ \ - that@ are@ a@ predicate@ application@ not@ builtin." + ~desc:"Remove@ all@ complex@ or@ interpreted@ formula@ triggers@ \ + (anything@ but@ non-built-in@ predicate@ applications)." diff --git a/src/transform/induction.ml b/src/transform/induction.ml index 26c717d13..0b82d451a 100644 --- a/src/transform/induction.ml +++ b/src/transform/induction.ml @@ -82,15 +82,7 @@ module Svsl = Mvsl.Set (* DEBUGGING AND PRINTING *) let debug = Debug.register_info_flag "induction" - ~desc:"About@ the@ transformation@ of@ the@ goal@ using@ induction." - -let debug_verbose = Debug.register_info_flag "induction-verbose" - ~desc:"Same@ as@ induction, but@ print@ also@ the@ variables, the@ \ - heuristics@ and@ the lexicographic@ order@ used." - -let debug_int = Debug.register_info_flag "induction_int_lex" - ~desc:"About@ the@ transformation@ of@ the@ goal@ using@ induction@ on@ \ - the@ tuples@ of@ integers." + ~desc:"Print@ debugging@ messages@ of@ the@ 'induction'@ transformation." let print_ty_skm skm = List.iter @@ -336,7 +328,7 @@ let induction_ty_lex km t0 = let lexl, rightmost_qvl = qsplit km vl qvl in let tcase = make_induction_lex lexl rightmost_qvl t in - if Debug.test_flag debug_verbose then + if Debug.test_flag debug then begin print_vset vset; print_heuristic_lex vl; @@ -344,11 +336,6 @@ let induction_ty_lex km t0 = Format.printf "Old Task: %a \n@." Pretty.print_term t0; Format.printf "New Task: %a \n@." Pretty.print_term tcase end; - if Debug.test_flag debug then - begin - Format.printf "Old Task: %a \n@." Pretty.print_term t0; - Format.printf "New Task: %a \n@." Pretty.print_term tcase - end; [tcase] with No_candidates_found -> Format.printf "No candidates found\n"; [t0] @@ -362,7 +349,7 @@ let induction_ty_lex = function let () = Trans.register_transform_l "induction_ty_lex" (Trans.store induction_ty_lex) - ~desc:"TODO: induction on type with lexicographic order" + ~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ algebraic@ types." (***************************************************************************) @@ -460,7 +447,7 @@ let induction_int_lex _km (le_int,lt_int) t0 = begin let t = int_strong_induction_lex (le_int,lt_int) ivl genl t in let t = t_forall_close lvl [] t in - if Debug.test_flag debug_int then + if Debug.test_flag debug then (Format.printf "Old Task: %a \n@." Pretty.print_term t0; Format.printf "New Task: %a \n@." Pretty.print_term t); [t] @@ -485,9 +472,7 @@ let () = (fun env -> let th_int = Env.find_theory env ["int"] "Int" in Trans.store (induction_int_lex th_int)) - ~desc:"TODO: induction on integers" - - + ~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ integers." (* Local Variables: diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml index addcbbc1d..e35e4d7a3 100644 --- a/src/transform/inlining.ml +++ b/src/transform/inlining.ml @@ -78,7 +78,7 @@ let fold in_goal notdeft notdeff notls task_hd (env, task) = (* transformations *) let meta = Theory.register_meta "inline : no" [Theory.MTlsymbol] - ~desc:"Disallow@ the@ inlining@ of@ the@ given@ logic@ symbols." + ~desc:"Disallow@ the@ inlining@ of@ the@ given@ function/predicate@ symbol." let t ?(use_meta=true) ?(in_goal=false) ~notdeft ~notdeff ~notls = let trans notls = @@ -121,7 +121,7 @@ let () = 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."; + ~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)@]." diff --git a/src/transform/instantiate_predicate.ml b/src/transform/instantiate_predicate.ml index 1705c1342..61bedd2e4 100644 --- a/src/transform/instantiate_predicate.ml +++ b/src/transform/instantiate_predicate.ml @@ -70,5 +70,5 @@ let () = Trans.register_transform "instantiate_predicate" (Trans.on_tagged_pr meta (fun spr -> Trans.fold_map (trans spr) ([], Sterm.empty) None)) - ~desc:"Look@ into@ all@ the@ task@ for@ terms@ that@ can@ instantiate@ \ - proposition@ marked@ by@ the@ 'instantiate : auto'@ meta." + ~desc:"Instantiate@ proposition@ marked@ by@ 'instantiate : auto'.@ \ + Used@ for@ Gappa." diff --git a/src/transform/introduction.ml b/src/transform/introduction.ml index cbaa1439e..affda0d4b 100644 --- a/src/transform/introduction.ml +++ b/src/transform/introduction.ml @@ -60,6 +60,7 @@ let intros pr f = let () = Trans.register_transform "introduce_premises" (Trans.goal intros) ~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \ goal@ into@ constant@ symbol@ and@ axioms." + (* Local Variables: compile-command: "unset LANG; make -C ../.. byte" diff --git a/src/transform/libencoding.ml b/src/transform/libencoding.ml index 2eb120cb0..a8bc9013c 100644 --- a/src/transform/libencoding.ml +++ b/src/transform/libencoding.ml @@ -16,11 +16,11 @@ open Decl open Theory let debug = Debug.register_info_flag "encoding" - ~desc:"About the encoding of polymorphism." + ~desc:"Print@ debugging@ messages@ about@ polymorphism@ encoding." (* meta to tag the protected types *) let meta_kept = register_meta "encoding : kept" [MTty] - ~desc:"Specify a type to keep during the encoding of polymorphism." + ~desc:"Specify@ a@ type@ to@ keep@ during@ polymorphism@ encoding." (* sort symbol of the "universal" type *) let ts_base = create_tysymbol (id_fresh "uni") [] None diff --git a/src/transform/lift_epsilon.ml b/src/transform/lift_epsilon.ml index e99f3c055..1c0ab324e 100644 --- a/src/transform/lift_epsilon.ml +++ b/src/transform/lift_epsilon.ml @@ -57,7 +57,13 @@ let lift kind = let lift_epsilon kind = Trans.fold (lift kind) None let meta_epsilon = Theory.register_meta_excl "lift_epsilon" [MTstring] - ~desc:"TODO" + ~desc:"Specify@ whether@ the@ existence@ of@ a@ witness@ for@ the@ \ + formula@ under@ epsilon@ is@ assumed:@; \ + @[\ + - @[implicit:@ implicitly@ assume@ existence@]@\n\ + - @[implied:@ @ do@ not@ assume@ the@ existence@ \ + of@ a@ witness.@]\ + @]" let lift_epsilon = Trans.on_meta_excl meta_epsilon (fun alo -> @@ -69,4 +75,4 @@ let lift_epsilon = Trans.on_meta_excl meta_epsilon lift_epsilon kind) let () = Trans.register_transform "lift_epsilon" lift_epsilon - ~desc:"TODO" + ~desc:"Move@ epsilon-terms@ into@ separate@ function@ definitions." diff --git a/src/transform/simplify_array.ml b/src/transform/simplify_array.ml index bc8dd7530..29a28c36f 100644 --- a/src/transform/simplify_array.ml +++ b/src/transform/simplify_array.ml @@ -41,6 +41,5 @@ let make_rt_rf env = let t env = let rt,rf = make_rt_rf env in Trans.rewriteTF rt rf None let () = Trans.register_env_transform "simplify_array" t - ~desc:"Rewrite@ using@ the@ axiom@ Select_eq@ of@ theory@ map.Map@ \ - whenever@ possible@ using@ syntaxic@ equality@ modulo@ alpha@ \ - equivalence." + ~desc:"Apply,@ wherever@ possible,@ the@ axiom@ 'Select_eq'@ of@ \ + the@ library@ theory@ map.Map." diff --git a/src/transform/simplify_formula.ml b/src/transform/simplify_formula.ml index 5890c1f0e..f2d453be1 100644 --- a/src/transform/simplify_formula.ml +++ b/src/transform/simplify_formula.ml @@ -37,7 +37,7 @@ let () = Trans.register_transform let () = Trans.register_transform_l "simplify_formula_and_task" simplify_formula_and_task ~desc:"Same as simplify_formula, but also@ \ - removes@ axioms@ and@ goals@ that@ become@ trivial." + remove@ axioms@ and@ goals@ that@ become@ trivial." (** remove_trivial_quantification Original version in the alt-ergo prover by Sylvain Conchon *) @@ -127,9 +127,9 @@ let simplify_trivial_quantification = let () = Trans.register_transform "simplify_trivial_quantification" simplify_trivial_quantification ~desc:"@[Simplify@ trivial@ quantifications:@]@\n \ -@[\ - - @[transform \\exists x. x == y /\\ F@ into F[y/x],@]@\n\ - - @[transform \\forall x. x <> y \\/ F@ into F[y/x].@]@]" + @[\ + - @[transform \\exists x. x == y /\\ F@ into F[y/x],@]@\n\ + - @[transform \\forall x. x <> y \\/ F@ into F[y/x].@]@]" let simplify_trivial_quantification_in_goal = Trans.goal (fun pr f -> [create_prop_decl Pgoal pr (fmla_remove_quant f)]) diff --git a/src/transform/simplify_recursive_definition.ml b/src/transform/simplify_recursive_definition.ml index 6a3dce486..7e7a705f8 100644 --- a/src/transform/simplify_recursive_definition.ml +++ b/src/transform/simplify_recursive_definition.ml @@ -115,4 +115,4 @@ let elt d = let t = Trans.decl elt None let () = Trans.register_transform "simplify_recursive_definition" t - ~desc:"Separate@ the@ definitions@ that@ are@ not@ really@ recursive." + ~desc:"Separate@ the@ definitions@ that@ are@ not@ mutually@ recursive." diff --git a/src/transform/smoke_detector.ml b/src/transform/smoke_detector.ml index 5e9299b15..f9a7fd028 100644 --- a/src/transform/smoke_detector.ml +++ b/src/transform/smoke_detector.ml @@ -39,16 +39,14 @@ let rec neg f = match f.t_node with let deep = create neg let () = Trans.register_transform "smoke_detector_top" top - ~desc:"Transformation@ that@ doesn't@ keep@ satisfiability.@ Add@ a@ \ - negation@ at@ the@ top@ of@ the@ goal@ in@ order@ to@ (try)@ to@ \ - detect@ inconsistencies@ in@ the@ premises." + ~desc:"Put@ the@ goal@ under@ negation.@ Used@ to@ \ + detect@ inconsistency@ in@ premises." let () = Trans.register_transform "smoke_detector_deep" deep - ~desc:"Transformation@ that@ doesn't@ keep@ satisfiability.@ Add@ a@ \ - negation@ under@ all@ the@ universal@ quantifications@ and@ \ - hypothesis@ of@ the@ goal@ in@ order@ to@ (try)@ to@ \ - detect@ inconsistencies@ in@ the@ premises." - + ~desc:"Put@ the@ conclusion@ of@ the@ goal@ (under@ universal@ \ + quantifiers@ and@ implications)@ under@ negation.@ \ + Used@ to@ detect@ inconsistency@ in@ premises@ \ + and@ goal@ hypotheses." (* Local Variables: diff --git a/src/transform/split_goal.ml b/src/transform/split_goal.ml index 04eb7576f..3eaa32c03 100644 --- a/src/transform/split_goal.ml +++ b/src/transform/split_goal.ml @@ -177,30 +177,30 @@ let split_premise_right = Trans.decl (split_premise right_split) None let split_premise_wp = Trans.decl (split_premise wp_split) None let () = Trans.register_transform_l "split_goal_full" split_goal_full - ~desc:"Puts@ the@ goal@ in@ a@ conjunctive@ form,@ \ + ~desc:"Put@ 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:"Same@ as@ split_goal_full,@ but@ also@ splits@ premises." + ~desc:"Same@ as@ split_goal_full,@ but@ also@ split@ premises." let () = Trans.register_transform "split_premise_full" split_premise_full - ~desc:"Same@ as@ split_all_full,@ but@ splits@ only@ premises." + ~desc:"Same@ as@ split_all_full,@ but@ split@ only@ premises." let () = Trans.register_transform_l "split_goal_right" split_goal_right ~desc:"@[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:"Same@ as@ split_goal_right,@ but@ also@ splits@ premises." + ~desc:"Same@ as@ split_goal_right,@ but@ also@ split@ premises." let () = Trans.register_transform "split_premise_right" split_premise_right - ~desc:"Same@ as@ split_all_right,@ but@ splits@ only@ premises." + ~desc:"Same@ as@ split_all_right,@ but@ split@ only@ premises." let () = Trans.register_transform_l "split_goal_wp" split_goal_wp ~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:"Same@ as@ split_goal_wp,@ but@ also@ splits@ premises." + ~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises." let () = Trans.register_transform "split_premise_wp" split_premise_wp - ~desc:"Same@ as@ split_all_wp,@ but@ splits@ only@ premises." + ~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises." let () = Trans.register_transform_l "split_goal" split_goal_wp ~desc:"The@ deprecated@ name@ of@ split_goal_wp,@ \ diff --git a/src/util/debug.ml b/src/util/debug.ml index a3c255a97..f59317f16 100644 --- a/src/util/debug.ml +++ b/src/util/debug.ml @@ -59,7 +59,7 @@ let stack_trace = register_info_flag "stack_trace" ~desc:"Avoid@ catching@ exceptions@ in@ order@ to@ get@ the@ stack@ trace." let timestamp = register_info_flag "timestamp" - ~desc:"Print@ a@ timestamp@ before@ debug@ messages." + ~desc:"Print@ a@ timestamp@ before@ debugging@ messages." let time_start = Unix.gettimeofday () diff --git a/src/util/plugin.ml b/src/util/plugin.ml index 0d5128820..7ac65fc18 100644 --- a/src/util/plugin.ml +++ b/src/util/plugin.ml @@ -12,7 +12,7 @@ type plugin = string let debug = Debug.register_info_flag "load_plugin" - ~desc:"About plugins loading." + ~desc:"Print@ debugging@ messages@ about@ plugin@ loading." exception Plugin_Not_Found of plugin * string list diff --git a/src/why3bench/bench.ml b/src/why3bench/bench.ml index 21f95edbf..7aaaaf38f 100644 --- a/src/why3bench/bench.ml +++ b/src/why3bench/bench.ml @@ -75,9 +75,10 @@ type callback = tool_id -> prob_id -> task -> int -> proof_attempt_status -> unit let debug_call = Debug.register_info_flag "call" - ~desc:"Show when call to provers are done" + ~desc:"Print@ debugging@ messages@ about@ prover@ calls." + let debug = Debug.register_info_flag "bench_core" - ~desc:"About the scheduling" + ~desc:"Print@ debugging@ messages@ about@ scheduling@ of@ prover@ calls." module BenchUtil = diff --git a/src/why3bench/benchdb.ml b/src/why3bench/benchdb.ml index 6a4cc4a91..6a752d53a 100644 --- a/src/why3bench/benchdb.ml +++ b/src/why3bench/benchdb.ml @@ -20,7 +20,7 @@ let load_driver = Env.Wenv.memoize 2 (fun env -> Hstr.memo 10 (Driver.load_driver env)) let debug = Debug.register_info_flag "benchdb" - ~desc:"About the communication from the database" + ~desc:"Print@ debugging@ messages@ about@ the@ why3bench@ database." type path = | Pgoal of string diff --git a/src/why3bench/why3bench.ml b/src/why3bench/why3bench.ml index 696626d6a..79a7aae6d 100644 --- a/src/why3bench/why3bench.ml +++ b/src/why3bench/why3bench.ml @@ -21,7 +21,7 @@ module B = Bench module C = Call_provers let debug = Debug.register_info_flag "main" - ~desc:"About initialization of the bench" + ~desc:"Print@ debugging@ messages@ about@ initialization@ of@ the@ bench." let usage_msg = sprintf "Usage: %s [options] [[file|-] [-T [-G ]...]...]...\ diff --git a/src/whyml/mlw_ocaml.ml b/src/whyml/mlw_ocaml.ml index debf946ab..dab3557fc 100644 --- a/src/whyml/mlw_ocaml.ml +++ b/src/whyml/mlw_ocaml.ml @@ -22,8 +22,8 @@ open Printer open Mlw_ty let debug = - Debug.register_info_flag - ~desc:"Print details on program extraction." "extraction" + Debug.register_info_flag "extraction" + ~desc:"Print@ details@ of@ program@ extraction." let clean_fname fname = let fname = Filename.basename fname in diff --git a/src/whyml/mlw_wp.ml b/src/whyml/mlw_wp.ml index 3a34e513c..4fb874822 100644 --- a/src/whyml/mlw_wp.ml +++ b/src/whyml/mlw_wp.ml @@ -963,7 +963,8 @@ let wp_val _env _km th _lv = th *) let fast_wp = Debug.register_flag "fast_wp" - ~desc:"Efficient Weakest Preconditions." + ~desc:"Efficient@ Weakest@ Preconditions.@ \ + Work@ in@ progress,@ not@ ready@ for@ use." module Subst = struct -- 2.26.2