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();