Commit 3a8e66bf authored by Andrei Paskevich's avatar Andrei Paskevich

(re)write some descriptions

parent b12068d1
......@@ -128,12 +128,12 @@ let read_channel env path filename cin =
(** Read all the file *)
let th_uc = Sysutil.fold_channel fold th_uc cin in
(** Return the map with the theory *)
(), Mstr.singleton "EqLin" (close_theory th_uc)
(), Mstr.singleton "EquLin" (close_theory th_uc)
let library_of_env = Env.register_format "EquLin" ["equlin"] read_channel
~desc:"@[Generate rendomly linear arithmetic problems:@\n \
@[The first line give the seed to use. Each other lines corresond to one goal@\n \
@[- @[the first number give the number of variables@]@\n\
- @[the second the number of equation@]@\n\
- @[the third the absolute maximun of the constants used@]\
@]"
~desc:"@[<hov>Generate@ random@ linear@ arithmetic@ problems.@ \
The@ first@ line@ gives@ the@ seed.@ Each@ other@ line@ \
describes@ a@ goal@ and@ contains@ three@ numbers:@]@\n \
@[- @[the@ number@ of@ variables@]@\n\
- @[the@ number@ of@ equations@]@\n\
- @[the@ maximum@ absolute@ value@ of@ coefficients.@]@]"
......@@ -256,7 +256,7 @@ and comment_line = parse
(), Tptp_typing.typecheck env path ast
let library_of_env = Env.register_format "tptp" ["p";"ax"] read_channel
~desc:"TFF1 TPTP format."
~desc:"TPTP format (CNF FOF FOFX TFF)"
}
(*
......
......@@ -234,7 +234,5 @@ let print_task fof _env pr thpr ?old:_ fmt task =
fprintf fmt "@[%a@]@."
(print_list nothing (print_decl info)) (Task.task_decls task)
let () = register_printer "tptp-tff" (print_task false)
~desc:"Printer for the TPTP-TFF format."
let () = register_printer "tptp-fof" (print_task true)
~desc:"Printer for the TPTP-FOF format."
let () = register_printer "tptp-tff" (print_task false) ~desc:"TPTP TFF format"
let () = register_printer "tptp-fof" (print_task true) ~desc:"TPTP FOF format"
......@@ -28,12 +28,10 @@ open Decl
open Theory
open Task
(* TODO: Is it not an example of register_stop_flag? *)
let debug_print_labels = Debug.register_flag "print_labels"
~desc:"Control if ident labels are printed."
~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
let debug_print_locs = Debug.register_flag "print_locs"
~desc:"Control if ident location are printed."
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let iprinter,aprinter,tprinter,pprinter =
let bl = ["theory"; "type"; "constant"; "function"; "predicate"; "inductive";
......
......@@ -343,7 +343,7 @@ and string = parse
(), parse_logic_file env path lb
let library_of_env = Env.register_format "why" ["why"] read_channel
~desc:"Purely@ logical@ Why3@ native@ format."
~desc:"Why@ logical@ language"
let parse_logic_file env = parse_logic_file (library_of_env env)
}
......
......@@ -29,10 +29,8 @@ open Typing
open Ptree
open Pgm_module
(** TODO: Why is it defined here, it seems to modify the comportement:
it calls Pgm_ocaml.extract_module. A stop flag? *)
let debug_extraction = Debug.register_flag "extraction"
~desc:"TODO"
let debug_extraction = Debug.register_stop_flag "extraction"
~desc:"for internal use"
exception ClashModule of string
......@@ -161,14 +159,14 @@ let read_channel =
one_time_hack := false;
let genv = Env.env_of_library env in
Env.register_format "whyml-old-library" ["mlw"] read_channel genv
~desc:"TODO: old version?"
~desc:"for internal use"
end
else env
in
read_channel env path file c
let library_of_env = Env.register_format "whyml-old" [] read_channel
~desc:"TODO: older version? not really used?"
~desc:"WhyML@ programming@ language@ (obsolete@ implementation)"
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
......
......@@ -28,9 +28,9 @@ open Pgm_types.T
open Pgm_ttree
let debug_print_labels = Debug.register_flag "print_labels"
~desc:"Specify to pretty-print the labels in why3ml format."
~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
let debug_print_locs = Debug.register_flag "print_locs"
~desc:"Specify to pretty-print the localization in why3ml format."
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
(* pretty-printing (for debugging) *)
......
......@@ -34,8 +34,8 @@ open Pgm_types
open Pgm_types.T
open Pgm_module
let debug = Debug.register_flag "program_typing"
~desc:"About the way program are typed."
let debug = Debug.register_flag "whyml_typing"
~desc:"Print@ details@ of@ program@ typechecking."
let is_debug () = Debug.test_flag debug
let error = Loc.error
......
......@@ -33,8 +33,8 @@ open Pgm_types
open Pgm_types.T
open Pgm_module
let debug = Debug.register_flag "program_wp"
~desc:"About the way weakest precondition is computed."
let debug = Debug.register_flag "whyml_wp"
~desc:"Print@ details@ of@ verification@ condition@ generation."
(* mutable fields *)
......
......@@ -24,7 +24,7 @@ open Mlw_module
open Mlw_typing
let debug = Debug.register_flag "print_modules"
~desc:"Print modules after typing."
~desc:"Print@ program@ modules@ after@ typechecking."
let read_channel env path file c =
let lb = Lexing.from_channel c in
......@@ -43,4 +43,4 @@ let read_channel env path file c =
mm, tm
let library_of_env = Env.register_format "whyml" ["mlw"] read_channel
~desc:"Why3 programs format"
~desc:"WhyML programming language"
......@@ -33,11 +33,11 @@ open Mlw_expr
open Mlw_decl
let debug_print_labels = Debug.register_flag "print_labels"
~desc:"print labels during pretty-printing"
~desc:"Print@ labels@ of@ identifiers@ and@ expressions."
let debug_print_locs = Debug.register_flag "print_locs"
~desc:"print locations during pretty-printing"
~desc:"Print@ locations@ of@ identifiers@ and@ expressions."
let debug_print_reg_types = Debug.register_flag "print_reg_types"
~desc:"TODO"
~desc:"Print@ types@ of@ regions@ (mutable@ fields)."
let iprinter =
let isanitize = sanitizer char_to_alpha char_to_alnumus in
......
......@@ -30,13 +30,13 @@ open Mlw_ty.T
open Mlw_expr
let debug = Debug.register_flag "whyml_wp"
~desc:"TODO:What is the difference with program_wp?"
~desc:"Print@ details@ of@ verification@ conditions@ generation."
(** Seems to modify the behavior, should use register_stop_flag *)
let no_track = Debug.register_flag "wp_no_track"
~desc:"TODO"
let no_eval = Debug.register_flag "wp_no_eval"
~desc:"TODO"
let no_track = Debug.register_stop_flag "wp_no_track"
~desc:"Do@ not@ remove@ redundant@ type@ invariant@ conditions@ from@ VCs."
let no_eval = Debug.register_stop_flag "wp_no_eval"
~desc:"Do@ not@ simplify@ pattern@ matching@ on@ record@ datatypes@ in@ VCs."
(** Marks *)
......
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