From f199d006bdd316a811691e8fe11b72d83ceff80d Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 22 Feb 2023 14:20:19 +0100 Subject: [PATCH 1/5] Attempt to improve print_app_list --- basis/basisProgScript.sml | 52 +++++++++++++++++++------ basis/pure/mlstringScript.sml | 71 +++++++++++++++++++++++++++++++++++ 2 files changed, 111 insertions(+), 12 deletions(-) diff --git a/basis/basisProgScript.sml b/basis/basisProgScript.sml index f74c4491a2..4c17657d41 100644 --- a/basis/basisProgScript.sml +++ b/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 r = translate mlstringTheory.sum_sizes_def; +val r = translate mlstringTheory.make_app_list_ann_def; +val r = translate miscTheory.append_aux_def; +val r = translate miscTheory.append_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 _ = (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)`; diff --git a/basis/pure/mlstringScript.sml b/basis/pure/mlstringScript.sml index e956313d2d..5aa3ac5206 100644 --- a/basis/pure/mlstringScript.sml +++ b/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. *) From ed0b09dbe0ff7d797342c937eaefa34eb6095c31 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Wed, 22 Feb 2023 23:57:46 +0100 Subject: [PATCH 2/5] Switch use_full_type_names to false --- basis/basisProgScript.sml | 4 ++-- translator/std_preludeScript.sml | 10 ++++++++++ 2 files changed, 12 insertions(+), 2 deletions(-) diff --git a/basis/basisProgScript.sml b/basis/basisProgScript.sml index 4c17657d41..b29075780d 100644 --- a/basis/basisProgScript.sml +++ b/basis/basisProgScript.sml @@ -24,13 +24,13 @@ val () = ml_prog_update (add_Dlet eval_thm "print"); val _ = ml_prog_update open_local_block; +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 miscTheory.append_aux_def; -val r = translate miscTheory.append_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 = diff --git a/translator/std_preludeScript.sml b/translator/std_preludeScript.sml index ee3c7e51a0..2587f684ba 100644 --- a/translator/std_preludeScript.sml +++ b/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(); From df61ce52fe8e382a902a787aef334dc89e6b09c5 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 23 Feb 2023 12:59:05 +0100 Subject: [PATCH 3/5] Change name of Candle type cexp to cval --- candle/prover/compute/compute_syntaxScript.sml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/candle/prover/compute/compute_syntaxScript.sml b/candle/prover/compute/compute_syntaxScript.sml index 261e689308..f3bddd296c 100644 --- a/candle/prover/compute/compute_syntaxScript.sml +++ b/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 (); - From e331367434fa1a68c4e01838618bc519410f11a7 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Thu, 23 Feb 2023 23:36:52 +0100 Subject: [PATCH 4/5] Insert missing line --- basis/types.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/basis/types.txt b/basis/types.txt index 784ac593ac..1d73c1505f 100644 --- a/basis/types.txt +++ b/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 @@ -378,4 +379,3 @@ print: string -> unit print_app_list: string app_list -> unit print_int: int -> unit print_pp: PrettyPrinter.pp_data -> unit - From 0b5b02742b5e8502d34c76d487374b7791b71f37 Mon Sep 17 00:00:00 2001 From: Magnus Myreen Date: Tue, 28 Feb 2023 22:34:27 +0100 Subject: [PATCH 5/5] Fix end of file --- basis/types.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/basis/types.txt b/basis/types.txt index 1d73c1505f..588c79d723 100644 --- a/basis/types.txt +++ b/basis/types.txt @@ -379,3 +379,4 @@ print: string -> unit print_app_list: string app_list -> unit print_int: int -> unit print_pp: PrettyPrinter.pp_data -> unit +