Merge pull request #930 from CakeML/print_app_list

Attempt to improve print_app_list

basis/basisProgScript.sml

@@ -22,29 +22,45 @@ val eval_thm = let
  in v_thm end
 val () = ml_prog_update (add_Dlet eval_thm "print");
 
-val print_app_list = process_topdecs
- `fun print_app_list ls =
- (case ls of
- Nil => ()
- | List ls => TextIO.print_list ls
- | Append l1 l2 => (print_app_list l1; print_app_list l2))`;
-val () = append_prog print_app_list;
+val _ = ml_prog_update open_local_block;
 
-Theorem print_app_list_spec:
+val _ = (use_full_type_names := false);
+val r = translate mlstringTheory.sum_sizes_def;
+val r = translate mlstringTheory.make_app_list_ann_def;
+val r = translate mlstringTheory.shrink_def;
+val _ = (next_ml_names := ["str_app_list_opt"]);
+val r = translate mlstringTheory.str_app_list_opt_def;
+val _ = (use_full_type_names := true);
+
+val _ = (append_prog o process_topdecs) `
+ fun print_app_list_aux ls =
+ (case ls of
+ Nil => ()
+ | List ls => TextIO.print_list ls
+ | Append l1 l2 => (print_app_list_aux l1; print_app_list_aux l2))`;
+
+val _ = ml_prog_update open_local_in_block;
+
+val _ = (append_prog o process_topdecs) `
+ fun print_app_list ls = print_app_list_aux (str_app_list_opt ls)`;
+
+val _ = ml_prog_update close_local_blocks;
+
+Theorem print_app_list_aux_spec[local]:
  ∀ls lv out. APP_LIST_TYPE STRING_TYPE ls lv ⇒
- app (p:'ffi ffi_proj) ^(fetch_v "print_app_list" (get_ml_prog_state())) [lv]
+ app (p:'ffi ffi_proj) print_app_list_aux_v [lv]
  (STDIO fs) (POSTv v. &UNIT_TYPE () v * STDIO (add_stdout fs (concat (append ls))))
 Proof
  reverse(Cases_on`STD_streams fs`) >- (rw[STDIO_def] \\ xpull) \\
  pop_assum mp_tac \\ simp[PULL_FORALL] \\ qid_spec_tac`fs` \\
  reverse (Induct_on`ls`) \\ rw[APP_LIST_TYPE_def]
  >- (
- xcf "print_app_list" (get_ml_prog_state())
+ xcf_with_def () (fetch "-" "print_app_list_aux_v_def")
  \\ xmatch \\ xcon
  \\ DEP_REWRITE_TAC[GEN_ALL add_stdo_nil]
  \\ xsimpl \\ metis_tac[STD_streams_stdout])
  >- (
- xcf "print_app_list" (get_ml_prog_state())
+ xcf_with_def () (fetch "-" "print_app_list_aux_v_def")
  \\ xmatch
  \\ xlet_auto >- xsimpl
  \\ xapp
@@ -55,12 +71,24 @@ Proof
  \\ simp[mlstringTheory.concat_thm,mlstringTheory.strcat_thm]
  \\ xsimpl
  \\ metis_tac[STD_streams_stdout])
- \\ xcf "print_app_list" (get_ml_prog_state())
+ \\ xcf_with_def () (fetch "-" "print_app_list_aux_v_def")
  \\ xmatch
  \\ xapp
  \\ simp[]
 QED
 
+Theorem print_app_list_spec:
+ ∀ls lv out. APP_LIST_TYPE STRING_TYPE ls lv ⇒
+ app (p:'ffi ffi_proj) print_app_list_v [lv]
+ (STDIO fs) (POSTv v. &UNIT_TYPE () v * STDIO (add_stdout fs (concat (append ls))))
+Proof
+ rw []
+ \\ xcf_with_def () (fetch "-" "print_app_list_v_def")
+ \\ xlet_auto >- xsimpl
+ \\ once_rewrite_tac [GSYM mlstringTheory.str_app_list_opt_thm]
+ \\ xapp_spec print_app_list_aux_spec \\ fs []
+QED
+
 val _ = (append_prog o process_topdecs)
  `fun print_int i = TextIO.print (Int.toString i)`;
 

basis/pure/mlstringScript.sml

@@ -1094,6 +1094,77 @@ Proof
 QED
 val _ = export_rewrites["ALL_DISTINCT_MAP_explode"]
 
+(* optimising mlstring app_list *)
+
+Datatype:
+ app_list_ann = BigList ('a list)
+ | BigAppend app_list_ann app_list_ann
+ | Small ('a app_list)
+End
+
+Definition sum_sizes_def:
+ sum_sizes [] k = k ∧
+ sum_sizes (l::ls) k = sum_sizes ls (strlen l + k)
+End
+
+Overload size_limit[local] = “2048:num”
+
+Definition make_app_list_ann_def:
+ make_app_list_ann input =
+ case input of
+ | Nil => (Small input, 0)
+ | Append l1 l2 =>
+ (let (x1,n1) = make_app_list_ann l1 in
+ let (x2,n2) = make_app_list_ann l2 in
+ let n = n1+n2 in
+ if n < size_limit then
+ (Small input,n)
+ else
+ (BigAppend x1 x2,n))
+ | List ls =>
+ (let n = sum_sizes ls 0 in
+ if n < size_limit then
+ (Small input,n)
+ else (BigList ls,n))
+End
+
+Definition shrink_def:
+ shrink (Small t) = List [concat (append t)] ∧
+ shrink (BigList ls) = List ls ∧
+ shrink (BigAppend l1 l2) = Append (shrink l1) (shrink l2)
+End
+
+Definition str_app_list_opt_def:
+ str_app_list_opt l =
+ let (t,n) = make_app_list_ann l in
+ shrink t
+End
+
+Triviality str_app_list_opt_test:
+ str_app_list_opt (Append (List [strlit "Hello"; strlit " there"])
+ (List [strlit "!"])) =
+ List [strlit "Hello there!"]
+Proof
+ EVAL_TAC
+QED
+
+Theorem str_app_list_opt_thm:
+ concat (append (str_app_list_opt l)) = concat (append l)
+Proof
+ ‘str_app_list_opt l = shrink $ FST $ make_app_list_ann l’
+ by fs [str_app_list_opt_def,UNCURRY]
+ \\ fs [] \\ pop_assum kall_tac
+ \\ Induct_on ‘l’
+ >~ [‘Nil’] >- EVAL_TAC
+ >~ [‘Append’] >-
+ (simp [Once make_app_list_ann_def]
+ \\ rpt (pairarg_tac \\ gvs [])
+ \\ IF_CASES_TAC
+ \\ gvs [shrink_def,concat_cons,concat_nil,concat_append])
+ \\ simp [Once make_app_list_ann_def] \\ rw []
+ \\ gvs [shrink_def,concat_cons,concat_nil,concat_append]
+QED
+
 (* The translator turns each `empty_ffi s` into a call to the FFI with
  an empty name and passing `s` as the argument. The empty FFI is
  used for logging/timing purposes. *)

basis/types.txt

@@ -338,6 +338,7 @@ pre: int -> int
 while: ('a -> bool) -> ('a -> 'a) -> 'a -> 'a
 owhile: ('a -> bool) -> ('a -> 'a) -> 'a -> 'a option
 least: (int -> bool) -> int
+append: 'a app_list -> 'a list
 repeat: ('a -> 'a) -> 'a -> 'b
 +: int -> int -> int
 -: int -> int -> int

candle/prover/compute/compute_syntaxScript.sml

@@ -52,7 +52,7 @@ Overload "_NUMERAL" = “λtm. Comb _NUMERAL_TM tm”;
 
 (* Compute expressions *)
 
-Overload Cexp = “Tyapp «cexp» []”;
+Overload Cexp = “Tyapp «cval» []”;
 Overload Cexp_list = “Tyapp «list» [Cexp]”;
 Overload "_P1" = “Var «p1» Cexp”;
 Overload "_P2" = “Var «p2» Cexp”;
@@ -222,4 +222,3 @@ End
 val _ = Parse.add_infix ("SAFEMOD", 500, HOLgrammars.LEFT);
 
 val _ = export_theory ();
-

translator/std_preludeScript.sml

@@ -122,6 +122,16 @@ val least_side_thm = Q.prove(
  THEN METIS_TAC [IS_SOME_DEF])
  |> update_precondition;
 
+(* app_list *)
+
+val _ = ml_prog_update open_local_block;
+val r = translate miscTheory.append_aux_def;
+val _ = ml_prog_update open_local_in_block;
+
+val r = translate miscTheory.append_def;
+
+val _ = ml_prog_update close_local_blocks;
+
 val _ = (print_asts := true);
 
 val _ = export_theory();