Merge pull request #829 from CakeML/help

Add --help command-line option and update how-to document

basis/ListProgScript.sml

@@ -113,7 +113,7 @@ val _ = ml_prog_update open_local_in_block;
 val result = next_ml_names := ["partition"];
 val result = translate mllistTheory.partition_def;
 
-val result = translate FOLDL;
+val result = translate foldl_def;
 
 val _ = ml_prog_update open_local_block;
 val result = translate foldli_aux_def;

basis/PrettyPrinterProgScript.sml

@@ -24,6 +24,9 @@ fun tr name def = (
   translate def
 )
 
+Triviality fromList_thm =
+  fromList_def |> SIMP_RULE std_ss [mllistTheory.foldl_intro];
+
 val _ = tr "fromString" fromString_def
 val _ = tr "fromChar" fromChar_def
 val _ = tr "fromBool" fromBool_def
@@ -34,9 +37,7 @@ val _ = tr "fromWord64" fromWord64_def
 val _ = tr "fromRat" fromRat_def
 val _ = tr "fromOption" fromOption_def
 val _ = tr "fromPair" fromPair_def
-val _ = tr "fromList" fromList_def
-val _ = tr "fromArray" fromArray_def
-val _ = tr "fromVector" fromVector_def
+val _ = tr "fromList" fromList_thm
 
 val sigs = module_signatures [
   "fromString",

basis/pure/mllistScript.sml

@@ -102,12 +102,9 @@ Proof
   rw [partition_def, FILTER, partition_aux_thm]
 QED
 
-val foldl_aux_def = Define`
-  (foldl_aux f e n [] = e) /\
-  (foldl_aux f e n (h::t) = foldl_aux f (f h e) (SUC n) t)`;
-
 val foldl_def = Define`
-  foldl f e l = foldl_aux f e 0 l`;
+  (foldl f e [] = e) /\
+  (foldl f e (h::t) = foldl f (f h e) t)`;
 
 val foldli_aux_def = Define`
   (foldli_aux f e n [] = e) /\
@@ -124,6 +121,12 @@ val foldli_aux_thm = Q.prove (
   rw [ADD1]
 );
 
+Theorem foldl_intro:
+  ∀xs x f. FOLDL f x xs = foldl (λx acc. f acc x) x xs
+Proof
+  Induct \\ fs [foldl_def]
+QED
+
 Theorem foldli_thm:
    !f e l. foldli f e l = FOLDRi (\n. f (LENGTH l - (SUC n))) e (REVERSE l)
 Proof

compiler/bootstrap/compilation/ag32/32/proofs/ag32BootstrapProofScript.sml

@@ -29,15 +29,15 @@ val with_clos_conf_simp = prove(
 
 val ffi_names =
   ``config.lab_conf.ffi_names``
-  |> (REWRITE_CONV[ag32BootstrapTheory.config_def] THENC EVAL)
+  |> (REWRITE_CONV[ag32BootstrapTheory.config_def] THENC EVAL);
 
 val LENGTH_code =
   ``LENGTH code``
-  |> (REWRITE_CONV[ag32BootstrapTheory.code_def] THENC listLib.LENGTH_CONV)
+  |> (REWRITE_CONV[ag32BootstrapTheory.code_def] THENC listLib.LENGTH_CONV);
 
 val LENGTH_data =
   ``LENGTH data``
-  |> (REWRITE_CONV[ag32BootstrapTheory.data_def] THENC listLib.LENGTH_CONV)
+  |> (REWRITE_CONV[ag32BootstrapTheory.data_def] THENC listLib.LENGTH_CONV);
 
 Overload cake_machine_config =
   ``ag32_machine_config (THE config.lab_conf.ffi_names) (LENGTH code) (LENGTH data)``
@@ -281,7 +281,9 @@ Theorem cake_extract_writes:
    let events = MAP get_output_io_event (cake_io_events cl (stdin_fs inp)) in
    let out = extract_writes 1 events in
    let err = extract_writes 2 events in
-   if has_version_flag (TL cl) then
+   if has_help_flag (TL cl) then
+     (out = explode help_string) ∧ (err = "")
+   else if has_version_flag (TL cl) then
      (out = explode current_build_info_str) ∧ (err = "")
    else
      let (cout, cerr) = compile_32 (TL cl) inp in
@@ -294,7 +296,7 @@ Proof
   \\ simp[wfFS_stdin_fs, STD_streams_stdin_fs]
   \\ simp[compilerTheory.full_compile_32_def]
   \\ pairarg_tac \\ simp[]
-  \\ IF_CASES_TAC \\ fs[]
+  \\ ntac 2 (IF_CASES_TAC \\ fs[]
   >- (
     simp[TextIOProofTheory.add_stdo_def]
     \\ SELECT_ELIM_TAC
@@ -324,7 +326,7 @@ Proof
         pop_assum mp_tac
         \\ rw[] \\ fs[] \\ rw[]
         \\ pop_assum mp_tac \\ rw[])
-      >- ( rw[] \\ rw[OPTREL_def])))
+      >- ( rw[] \\ rw[OPTREL_def]))))
   \\ simp[TextIOProofTheory.add_stdout_fastForwardFD, STD_streams_stdin_fs]
   \\ DEP_REWRITE_TAC[TextIOProofTheory.add_stderr_fastForwardFD]
   \\ simp[TextIOProofTheory.STD_streams_add_stdout, STD_streams_stdin_fs]

compiler/bootstrap/translation/compiler32ProgScript.sml

@@ -224,8 +224,10 @@ val res = format_compiler_result_def
 val res = translate compile_32_def;
 
 val res = translate (has_version_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
+val res = translate (has_help_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
 val res = translate print_option_def
 val res = translate current_build_info_str_def
+val res = translate compilerTheory.help_string_def;
 
 val nonzero_exit_code_for_error_msg_def = Define `
   nonzero_exit_code_for_error_msg e =
@@ -240,7 +242,9 @@ val main = process_topdecs`
     let
       val cl = CommandLine.arguments ()
     in
-      if compiler_has_version_flag cl then
+      if compiler_has_help_flag cl then
+        print compiler_help_string
+      else if compiler_has_version_flag cl then
         print compiler_current_build_info_str
       else
         case compiler_compile_32 cl (TextIO.inputAll TextIO.stdIn)  of
@@ -287,6 +291,20 @@ Proof
   \\ imp_res_tac stdin_get_file_content
   \\ xlet_auto >- xsimpl
   \\ xif
+  >-
+   (simp[full_compile_32_def]
+    \\ xapp
+    \\ CONV_TAC SWAP_EXISTS_CONV
+    \\ qexists_tac `help_string`
+    \\ fs [compilerTheory.help_string_def,
+           fetch "-" "compiler_help_string_v_thm"]
+    \\ xsimpl
+    \\ rename1 `add_stdout _ (strlit string)`
+    \\ CONV_TAC SWAP_EXISTS_CONV
+    \\ qexists_tac`fs`
+    \\ xsimpl)
+  \\ xlet_auto >- xsimpl
+  \\ xif
   >- (
     simp[full_compile_32_def]
     \\ xapp

compiler/bootstrap/translation/compiler64ProgScript.sml

@@ -243,8 +243,10 @@ val res = format_compiler_result_def
 val res = translate compile_64_def;
 
 val res = translate (has_version_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
+val res = translate (has_help_flag_def |> SIMP_RULE (srw_ss()) [MEMBER_INTRO])
 val res = translate print_option_def
 val res = translate current_build_info_str_def
+val res = translate compilerTheory.help_string_def;
 
 val nonzero_exit_code_for_error_msg_def = Define `
   nonzero_exit_code_for_error_msg e =
@@ -259,7 +261,9 @@ val main = process_topdecs`
     let
       val cl = CommandLine.arguments ()
     in
-      if compiler_has_version_flag cl then
+      if compiler_has_help_flag cl then
+        print compiler_help_string
+      else if compiler_has_version_flag cl then
         print compiler_current_build_info_str
       else
         case compiler_compile_64 cl (TextIO.inputAll TextIO.stdIn)  of
@@ -306,6 +310,20 @@ Proof
   \\ imp_res_tac stdin_get_file_content
   \\ xlet_auto >- xsimpl
   \\ xif
+  >-
+   (simp[full_compile_64_def]
+    \\ xapp
+    \\ CONV_TAC SWAP_EXISTS_CONV
+    \\ qexists_tac `help_string`
+    \\ fs [compilerTheory.help_string_def,
+           fetch "-" "compiler_help_string_v_thm"]
+    \\ xsimpl
+    \\ rename1 `add_stdout _ (strlit string)`
+    \\ CONV_TAC SWAP_EXISTS_CONV
+    \\ qexists_tac`fs`
+    \\ xsimpl)
+  \\ xlet_auto >- xsimpl
+  \\ xif
   >- (
     simp[full_compile_64_def]
     \\ xapp

compiler/compilerScript.sml

@@ -21,6 +21,90 @@ open ag32_configTheory export_ag32Theory
 
 val _ = new_theory"compiler";
 
+val help_string = (* beginning of --help string *) ‘
+
+Usage:  cake [OPTIONS] < input_file > output_file
+
+The cake executable is usually invoked as shown above. The different
+OPTIONS are described in the OPTIONS listing below.
+
+One can also run the cake execuable as follows to print a listing of
+the type of each top-level binding (including the bindings made in
+the standard basis library).
+
+Usage:  cake --types < input_file
+
+One can invoke the cake executable to print this help message (--help)
+or version information (--version) without an input_file:
+
+Usage:  cake --version
+Usage:  cake --help
+
+OPTIONS:
+
+  --reg_alg=N   N is a natural number that specifies the register
+                allocation algorithm to use:
+                   0   - simple allocator, no spill heuristics
+                   1   - simple allocator, spill heuristics
+                   2   - IRC allocator, no spill heuristics (default)
+                   3   - IRC allocator, spill heuristics
+                   >=4 - linear scan allocator
+
+  --gc=G        specifies garbage collector type; here G is one of:
+                   none   - no garbage collector is used
+                   simple - a non-generational Cheney (default)
+                   genN   - a generational Cheney garbage collector is
+                            used; the size of the nursery generation is
+                            N machine words (example: --gc=gen5000)
+
+  --target=T    specifies that compilation should produce code for target
+                T, where T can be one of x64, arm8, mips, riscv for
+                the 64-bit compiler; for the 32-bit compiler T can be
+                one of arm7 and ag32.
+
+  --sexp=B      B can be either true or false; here false means that the
+                input will be parsed as normal CakeML concrete syntax;
+                true means that the input is parsed as an s-expression.
+
+  --print_sexp  causes the cake to print the given program in
+                s-expression format; with this option, the compiler
+                does not generate machine code.
+
+  --exclude_prelude=B   here B can be either true or false; the default
+                is false; setting this to true causes the compiler not
+                to include the standard basis library.
+
+  --skip_type_inference=B   here B can be either true or false; the
+                default is false; true will make the compiler skip
+                type inference. There are no gurantees of safety if
+                the type inferencer is skipped.
+
+  --explore     outputs several intermediate forms of the compiled
+                program in JSON format
+
+ADDITIONAL OPTIONS:
+
+Optimisations can be configured using the following advanced options.
+
+  --jump=B   true means conditional jumps to be used for out-of-stack checks
+  --multi=B  true means clos_to_bvl phase is to use multi optimisation
+  --known=B  true means clos_to_bvl phase is to use known optimisation
+  --call=B   true means clos_to_bvl phase is to use call optimisation
+  --inline_factor=N  threshold used by for ClosLang inliner in known pass
+  --max_body_size=N  threshold used by for ClosLang inliner in known pass
+  --max_app=N   max number of optimised curried applications in multi pass
+  --inline_size=N  threshold used by for BVL inliner pass
+  --exp_cut=N  threshold for when to cut large expression into subfunctions
+  --split=B  true means main expression will be split at sequencing (;)
+  --tag_bits=N  number of tag bits in every pointer
+  --len_bits=N  number of length bits in every pointer
+  --pad_bits=N  number of zero padding in every pointer
+  --len_size=N  size of length field in heap object header cells
+  --emit_empty_ffi=B  true emits debugging FFI calls for use with DEBUG_FFI
+  --hash_size=N  size of the memoization table used by instruction encoder
+
+’ (* end of --help string *)
+
 (* == Build info =========================================================== *)
 
 val current_version_tm = mlstring_from_proc "git" ["rev-parse", "HEAD"]
@@ -53,7 +137,7 @@ val current_build_info_str_def = Define `
 
 (* ========================================================================= *)
 
-val _ = Datatype`
+Datatype:
   config =
     <| inferencer_config : inf_env
      ; backend_config : α backend$config
@@ -62,9 +146,24 @@ val _ = Datatype`
      ; skip_type_inference : bool
      ; only_print_types    : bool
      ; only_print_sexp     : bool
-     |>`;
+     |>
+End
+
+Datatype:
+  compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring
+End
+
+fun drop_until p [] = []
+  | drop_until p (x::xs) = if p x then x::xs else drop_until p xs;
 
-val _ = Datatype`compile_error = ParseError | TypeError mlstring | AssembleError | ConfigError mlstring`;
+val help_string_tm =
+  help_string |> hd |> (fn QUOTE s => s) |> explode
+  |> drop_until (fn c => c = #"\n") |> tl |> implode
+  |> stringSyntax.fromMLstring;
+
+Definition help_string_def:
+  help_string = strlit ^help_string_tm
+End
 
 val locs_to_string_def = Define `
   (locs_to_string NONE = implode "unknown location") ∧
@@ -437,12 +536,14 @@ val parse_top_config_def = Define`
                get_err_str prelude;
                get_err_str typeinference])`
 
-(* Check for version flag
-   TODO: fix this
-*)
+(* Check for version flag *)
 val has_version_flag_def = Define `
   has_version_flag ls = MEM (strlit"--version") ls`
 
+(* Check for version help *)
+val has_help_flag_def = Define `
+  has_help_flag ls = MEM (strlit"--help") ls`
+
 val format_compiler_result_def = Define`
   format_compiler_result bytes_export (Failure err) =
     (List[]:mlstring app_list, error_to_str err) ∧
@@ -498,7 +599,9 @@ val compile_64_def = Define`
 
 val full_compile_64_def = Define `
   full_compile_64 cl inp fs =
-    if has_version_flag cl then
+    if has_help_flag cl then
+      add_stdout fs help_string
+    else if has_version_flag cl then
       add_stdout fs current_build_info_str
     else
       let (out, err) = compile_64 cl inp in
@@ -535,7 +638,9 @@ val compile_32_def = Define`
 
 val full_compile_32_def = Define `
   full_compile_32 cl inp fs =
-    if has_version_flag cl then
+    if has_help_flag cl then
+      add_stdout fs help_string
+    else if has_version_flag cl then
       add_stdout fs current_build_info_str
     else
       let (out, err) = compile_32 cl inp in

examples/lpr_checker/lpr_commonProgScript.sml

@@ -35,7 +35,7 @@ val _ = translate check_RAT_def;
 val _ = translate check_PR_def;
 val _ = translate is_PR_def;
 
-val _ = translate check_lpr_step_def;
+val _ = translate (check_lpr_step_def |> SIMP_RULE std_ss [mllistTheory.foldl_intro]);
 val _ = translate (is_unsat_def |> SIMP_RULE (srw_ss()) [LET_DEF,MEMBER_INTRO]);
 
 open mlintTheory;

examples/opentheory/reader_commonProgScript.sml

@@ -102,6 +102,7 @@ val r = holSyntaxExtraTheory.tymatch_def
         |> translate;
 val _ = (use_mem_intro := false);
 val r = translate OPTION_MAP_DEF;
+val r = translate FOLDL;
 val r = translate holSyntaxExtraTheory.match_type_def;
 
 val r = m_translate find_axiom_def;
@@ -313,4 +314,3 @@ Theorem context_spec =
   mk_app_of_ArrowP (fetch "ml_hol_kernelProg" "context_v_thm");
 
 val _ = export_theory ();
-