From 5f5ccf3ebb2bdd69f18dc2df87641a315f260158 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Tue, 4 Aug 2026 16:15:37 +0200
Subject: [PATCH 1/8] Add support for FDIFF _ (FDOM _) to HOL->CakeML
 translator

---
 basis/MapProgLib.sml       | 16 +++++++--
 basis/MapProgScript.sml    | 26 +++++++++++++-
 basis/pure/mlmapScript.sml | 73 ++++++++++++++++++++++++++++----------
 3 files changed, 93 insertions(+), 22 deletions(-)

diff --git a/basis/MapProgLib.sml b/basis/MapProgLib.sml
index ae0d95736b..0d7de418ad 100644
--- a/basis/MapProgLib.sml
+++ b/basis/MapProgLib.sml
@@ -10,6 +10,7 @@ open MapProgTheory;
 (*
   val _  = translation_extends "MapProg";
   val th = miscTheory.TotOrd_num_cmp;
+  val th = mlstringTheory.TotOrd_compare;
 *)
 
 fun add_fmap_for_cmp th = let
@@ -50,7 +51,7 @@ fun add_fmap_for_cmp th = let
   val _ = add_user_proved_v_thm flookup_thm
   (* delete *)
   val th1 = cj 4 ops_thm
-  val th2 = cj 3 mlmap_op_v_thms
+  val th2 = cj 4 mlmap_op_v_thms
   val tm1 = th1 |> concl |> dest_imp |> fst |> rator |> rator
   val tm2 = th2 |> concl |> rator |> rator
   val (i1,i2) = match_term tm2 tm1
@@ -59,7 +60,7 @@ fun add_fmap_for_cmp th = let
   val _ = add_user_proved_v_thm domsub_thm
   (* update *)
   val th1 = cj 3 ops_thm
-  val th2 = cj 4 mlmap_op_v_thms
+  val th2 = cj 5 mlmap_op_v_thms
   val tm1 = th1 |> concl |> dest_imp |> fst |> rator |> rator
   val tm2 = th2 |> concl |> rator |> rator
   val (i1,i2) = match_term tm2 tm1
@@ -68,13 +69,22 @@ fun add_fmap_for_cmp th = let
   val _ = add_user_proved_v_thm fmap_update_thm
   (* union *)
   val th1 = cj 5 ops_thm
-  val th2 = cj 2 mlmap_op_v_thms
+  val th2 = cj 3 mlmap_op_v_thms
   val tm1 = th1 |> concl |> dest_imp |> fst |> rator |> rator
   val tm2 = th2 |> concl |> rator |> rator
   val (i1,i2) = match_term tm2 tm1
   val th2a = INST i1 (INST_TYPE i2 th2)
   val funion_thm = MATCH_MP th1 th2a
   val _ = add_user_proved_v_thm funion_thm
+  (* fdiff_fdom *)
+  val th1 = cj 6 ops_thm
+  val th2 = cj 2 mlmap_op_v_thms
+  val tm1 = th1 |> concl |> dest_imp |> fst |> rator |> rator
+  val tm2 = th2 |> concl |> rator |> rator
+  val (i1,i2) = match_term tm2 tm1
+  val th2a = INST i1 (INST_TYPE i2 th2)
+  val fdiff_fdom_thm = MATCH_MP th1 th2a
+  val _ = add_user_proved_v_thm fdiff_fdom_thm
   in () end;
 
 end
\ No newline at end of file
diff --git a/basis/MapProgScript.sml b/basis/MapProgScript.sml
index 83ce95d3fa..8ada06a3d8 100644
--- a/basis/MapProgScript.sml
+++ b/basis/MapProgScript.sml
@@ -126,6 +126,8 @@ val _ = ml_prog_update (add_dec
   ``Dtabbrev unknown_loc [«'a»;«'b»] «map»
              (Atapp [Atvar «'a»; Atvar «'b»] (Short «map»))`` I);
 
+val _ = next_ml_names := ["diff"];
+val mlmap_diff_v_thm = translate mlmapTheory.diff_def;
 val _ = next_ml_names := ["lookup"];
 val mlmap_lookup_v_thm = translate mlmapTheory.lookup_def;
 val _ = next_ml_names := ["member"];
@@ -262,6 +264,24 @@ Proof
   \\ metis_tac [mlmapTheory.union_thm]
 QED
 
+Theorem IMP_FMAP_TYPE_fdiff_fdom[local]:
+  (MAP_TYPE b a --> MAP_TYPE b c --> MAP_TYPE b a) mlmap$diff v ⇒
+  (FMAP_TYPE cmp b a --> FMAP_TYPE cmp b c --> FMAP_TYPE cmp b a) mlmap$fdiff_fdom v
+Proof
+  fs [ml_translatorTheory.Arrow_def,FMAP_TYPE_def,
+      ml_translatorTheory.AppReturns_def] \\ rw []
+  \\ last_x_assum drule \\ strip_tac
+  \\ first_x_assum $ qspec_then ‘refs’ strip_assume_tac \\ fs []
+  \\ first_x_assum $ irule_at Any \\ rw []
+  \\ last_x_assum drule \\ strip_tac
+  \\ first_x_assum $ qspec_then ‘refs’ strip_assume_tac \\ fs []
+  \\ first_x_assum $ irule_at Any \\ rw []
+  \\ first_x_assum $ irule_at Any \\ rw []
+  >~ [‘mlmap$cmp_of (mlmap$diff c m)’]
+  >- (Cases_on ‘c’ \\ Cases_on ‘m’ \\ gvs [mlmapTheory.diff_def,mlmapTheory.cmp_of_def])
+  \\ metis_tac [mlmapTheory.diff_thm]
+QED
+
 Theorem IMP_FMAP_TYPE_ops:
   MAP_TYPE (key:'k -> v -> bool) (a:'a -> v -> bool) (mlmap$empty cmp) v ∧ TotOrd cmp ⇒
   FMAP_TYPE cmp key a FEMPTY v ∧
@@ -272,7 +292,9 @@ Theorem IMP_FMAP_TYPE_ops:
   ((MAP_TYPE key a --> key --> MAP_TYPE key a) mlmap$delete v1 ⇒
    (FMAP_TYPE cmp key a --> key --> FMAP_TYPE cmp key a) $\\ v1) ∧
   ((MAP_TYPE key a --> MAP_TYPE key a --> MAP_TYPE key a) mlmap$union v1 ⇒
-   (FMAP_TYPE cmp key a --> FMAP_TYPE cmp key a --> FMAP_TYPE cmp key a) FUNION v1)
+   (FMAP_TYPE cmp key a --> FMAP_TYPE cmp key a --> FMAP_TYPE cmp key a) FUNION v1) ∧
+  ((MAP_TYPE key a --> MAP_TYPE key c --> MAP_TYPE key a) mlmap$diff v1 ⇒
+   (FMAP_TYPE cmp key a --> FMAP_TYPE cmp key c --> FMAP_TYPE cmp key a) mlmap$fdiff_fdom v1)
 Proof
   rw []
   >- (irule MAP_TYPE_empty_IMP_FMAP_TYPE \\ simp [])
@@ -280,10 +302,12 @@ Proof
   >- (irule IMP_FMAP_TYPE_FUPDATE \\ simp [])
   >- (irule IMP_FMAP_TYPE_DOMSUB \\ simp [])
   >- (irule IMP_FMAP_TYPE_FUNION \\ simp [])
+  >- (irule IMP_FMAP_TYPE_fdiff_fdom \\ simp [])
 QED
 
 Theorem mlmap_op_v_thms =
   LIST_CONJ [mlmap_lookup_v_thm,
+             mlmap_diff_v_thm,
              mlmap_union_v_thm,
              mlmap_delete_v_thm,
              mlmap_insert_v_thm];
diff --git a/basis/pure/mlmapScript.sml b/basis/pure/mlmapScript.sml
index 9a0bf507d7..37f3f7e300 100644
--- a/basis/pure/mlmapScript.sml
+++ b/basis/pure/mlmapScript.sml
@@ -71,6 +71,14 @@ Definition filterWithKey_def:
   filterWithKey p (Map cmp t) = Map cmp (balanced_map$filterWithKey p t)
 End
 
+Definition diff_def:
+  diff (Map cmp t1 : ('a, 'b) map) (Map _ t2 : ('a, 'c) map) =
+    Map cmp (balanced_map$filterWithKey (λk v.
+      case balanced_map$lookup cmp k t2 of
+      | NONE => T
+      | _    => F) t1)
+End
+
 Definition map_def:
   map f (Map cmp t) = Map cmp (balanced_map$map f t)
 End
@@ -559,23 +567,6 @@ Proof
   \\ first_assum (irule_at Any) \\ rw []
 QED
 
-Theorem filter_lemma:
-  filter f t = filterWithKey (λk. f) t
-Proof
-  Cases_on ‘t’
-  \\ rw [filter_def, filterWithKey_def]
-  \\ rw [balanced_mapTheory.filter_def, SF ETA_ss]
-QED
-
-Theorem filter_thm:
-  map_ok t ⇒
-    map_ok (filter f t) ∧
-    to_fmap (filter f t) =
-    FDIFF (to_fmap t) {k | (k,v) | FLOOKUP (to_fmap t) k = SOME v ∧ ¬f v}
-Proof
-  simp [filter_lemma, filterWithKey_thm]
-QED
-
 Theorem lookup_thm:
    map_ok t ==> lookup t k = FLOOKUP (to_fmap t) k
 Proof
@@ -594,6 +585,53 @@ Proof
   \\ fs [FLOOKUP_DEF]
 QED
 
+Definition fdiff_fdom_def:
+  fdiff_fdom f1 f2 = FDIFF f1 (FDOM f2)
+End
+
+Theorem diff_thm:
+  map_ok f1 ∧ map_ok f2 ∧ cmp_of f1 = cmp_of f2 ⇒
+    map_ok (diff f1 f2) ∧
+    to_fmap (diff f1 f2) =
+    fdiff_fdom (to_fmap f1) (to_fmap f2)
+Proof
+  Cases_on ‘f1’
+  \\ Cases_on ‘f2’
+  \\ fs [fdiff_fdom_def,diff_def]
+  \\ strip_tac
+  \\ last_x_assum assume_tac
+  \\ drule filterWithKey_thm
+  \\ simp [filterWithKey_def]
+  \\ rw []
+  \\ gvs [cmp_of_def]
+  \\ gvs [TO_FLOOKUP, FLOOKUP_SIMP, FUN_EQ_THM]
+  \\ gen_tac
+  \\ Cases_on ‘FLOOKUP (to_fmap (Map f b)) x’ \\ fs []
+  \\ rpt AP_THM_TAC
+  \\ AP_TERM_TAC
+  \\ imp_res_tac (lookup_thm |> INST_TYPE [beta |-> gamma])
+  \\ gvs [lookup_def]
+  \\ simp [EXTENSION, FORALL_PROD, GSPECIFICATION, EXISTS_PROD]
+  \\ CASE_TAC \\ gvs []
+QED
+
+Theorem filter_lemma:
+  filter f t = filterWithKey (λk. f) t
+Proof
+  Cases_on ‘t’
+  \\ rw [filter_def, filterWithKey_def]
+  \\ rw [balanced_mapTheory.filter_def, SF ETA_ss]
+QED
+
+Theorem filter_thm:
+  map_ok t ⇒
+    map_ok (filter f t) ∧
+    to_fmap (filter f t) =
+    FDIFF (to_fmap t) {k | (k,v) | FLOOKUP (to_fmap t) k = SOME v ∧ ¬f v}
+Proof
+  simp [filter_lemma, filterWithKey_thm]
+QED
+
 Theorem filterWithKey_all:
   map_ok t ⇒
     all f (filterWithKey f t)
@@ -638,4 +676,3 @@ Proof
   \\ Cases_on `k ∈ FDOM (to_fmap (Map f b))` \\ fs []
   \\ fs [FLOOKUP_DEF]
 QED
-

From 914eaf694471d7022695f49ca8b72c9f9aa3bcd4 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Wed, 5 Aug 2026 00:12:25 +0200
Subject: [PATCH 2/8] Add mlstring$fast_compare and prove TotOrd_fast_compare

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DN4q4aJByF8Yr4Gk7pccjF
---
 basis/pure/mlstringScript.sml | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/basis/pure/mlstringScript.sml b/basis/pure/mlstringScript.sml
index bbf6eb62ba..6710739196 100644
--- a/basis/pure/mlstringScript.sml
+++ b/basis/pure/mlstringScript.sml
@@ -986,6 +986,12 @@ Definition fast_ge_def:
     if strlen s1 = strlen s2 then mlstring_ge s1 s2 else strlen s1 ≥ strlen s2
 End
 
+Definition fast_compare_def:
+  fast_compare s1 s2 =
+    if fast_lt s1 s2 then LESS else
+    if fast_le s1 s2 then EQUAL else GREATER
+End
+
 (* Properties of string orderings *)
 
 val flip_ord_def = ternaryComparisonsTheory.invert_comparison_def
@@ -1385,6 +1391,21 @@ Proof
      transitive_fast_lt]
 QED
 
+Theorem fast_compare_thm:
+   fast_compare = TO_of_LinearOrder fast_lt
+Proof
+  rw[FUN_EQ_THM, fast_compare_def, TO_of_LinearOrder, fast_le_thm]
+  >> rpt (IF_CASES_TAC >> gvs[fast_lt_nonrefl])
+QED
+
+Theorem TotOrd_fast_compare:
+   TotOrd fast_compare
+Proof
+  rw[fast_compare_thm]
+  >> irule TotOrd_TO_of_Strong
+  >> rw[StrongLinearOrder_fast_lt]
+QED
+
 Definition collate_aux_def:
   (collate_aux f (s1: mlstring) s2 ord n 0 = ord) /\
   (collate_aux f s1 s2 ord n (SUC len) =

From 815cf41e703c149a9c329313cf293f38b5ec58eb Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Wed, 5 Aug 2026 14:20:26 +0200
Subject: [PATCH 3/8] Set up bootstrap translation for better finite map
 translations

---
 basis/StringProgScript.sml                        |  2 ++
 basis/pure/mlintScript.sml                        | 10 +++++++++-
 basis/types.txt                                   |  2 ++
 compiler/bootstrap/translation/decProgScript.sml  | 14 +++++++++++++-
 .../pseudo_bool/cp_encoding/cp_to_ilpScript.sml   | 15 +++------------
 5 files changed, 29 insertions(+), 14 deletions(-)

diff --git a/basis/StringProgScript.sml b/basis/StringProgScript.sml
index 094d89bc4c..1924925947 100644
--- a/basis/StringProgScript.sml
+++ b/basis/StringProgScript.sml
@@ -27,6 +27,8 @@ val _ = trans "<"  “fast_lt”;
 val _ = trans "<=" “fast_le”;
 val _ = trans ">"  “fast_gt”;
 val _ = trans ">=" “fast_ge”;
+val _ = next_ml_names := ["compare"];
+val _ = translate fast_compare_def;
 val _ = ml_prog_update (close_module NONE);
 
 val _ = trans "sub" mlstringSyntax.strsub_tm;
diff --git a/basis/pure/mlintScript.sml b/basis/pure/mlintScript.sml
index 89daf4cf1f..66cccf2e97 100644
--- a/basis/pure/mlintScript.sml
+++ b/basis/pure/mlintScript.sml
@@ -3,7 +3,7 @@
 *)
 Theory mlint
 Ancestors
-  mlstring gcd
+  mlstring toto gcd
 Libs
   preamble
 
@@ -551,6 +551,14 @@ Definition num_gcd_def:
   num_gcd a b = if a = 0n then b else num_gcd (b MOD a) a
 End
 
+Theorem TotOrd_int_cmp:
+  TotOrd int_cmp
+Proof
+  rw [TotOrd, int_cmp_def]
+  \\ every_case_tac \\ gvs []
+  \\ intLib.ARITH_TAC
+QED
+
 Theorem num_gcd_eq_gcd:
   num_gcd = gcd
 Proof
diff --git a/basis/types.txt b/basis/types.txt
index ebef856d81..e665f62066 100644
--- a/basis/types.txt
+++ b/basis/types.txt
@@ -94,6 +94,7 @@ String.Fast.<: string -> string -> bool
 String.Fast.<=: string -> string -> bool
 String.Fast.>: string -> string -> bool
 String.Fast.>=: string -> string -> bool
+String.Fast.compare: string -> string -> ordering
 String.<: string -> string -> bool
 String.<=: string -> string -> bool
 String.>: string -> string -> bool
@@ -270,6 +271,7 @@ Array.all: ('a -> bool) -> 'a Array.array -> bool
 Array.collate: ('a -> 'b -> ordering) -> 'a Array.array -> 'b Array.array -> ordering
 Array.lookup: 'a Array.array -> 'a -> int -> 'a
 Array.updateResize: 'a Array.array -> 'a -> int -> 'a -> 'a Array.array
+Map.diff: ('a, 'b) map -> ('a, 'c) map -> ('a, 'b) map
 Map.lookup: ('a, 'b) map -> 'a -> 'b option
 Map.member: 'a -> ('a, 'b) map -> bool
 Map.insert: ('a, 'b) map -> 'a -> 'b -> ('a, 'b) map
diff --git a/compiler/bootstrap/translation/decProgScript.sml b/compiler/bootstrap/translation/decProgScript.sml
index 625d0230dd..a6ee900fcc 100644
--- a/compiler/bootstrap/translation/decProgScript.sml
+++ b/compiler/bootstrap/translation/decProgScript.sml
@@ -6,7 +6,7 @@ Ancestors
   ast ml_translator ml_pmatch[qualified] semanticPrimitives
   repl_init_envProg ast_extras
 Libs
-  preamble ml_translatorLib ml_progLib
+  preamble ml_translatorLib ml_progLib MapProgLib
 
 open preamble astTheory semanticPrimitivesTheory;
 open ml_translatorLib ml_translatorTheory ml_progLib;
@@ -67,3 +67,15 @@ val r = translate namespaceTheory.id_to_n_def;
 val r = translate repl_decs_allowedTheory.safe_exp_pmatch;
 val r = translate candle_prover_invTheory.safe_dec_def;
 val r = translate repl_decs_allowedTheory.decs_allowed_def;
+
+(* --- *)
+
+(* teach the translator how to translate fmap operations for key types:
+    - mlstring
+    - int
+    - num
+*)
+
+val _ = MapProgLib.add_fmap_for_cmp mlstringTheory.TotOrd_fast_compare;
+val _ = MapProgLib.add_fmap_for_cmp mlintTheory.TotOrd_int_cmp;
+val _ = MapProgLib.add_fmap_for_cmp miscTheory.TotOrd_num_cmp;
diff --git a/examples/pseudo_bool/cp_encoding/cp_to_ilpScript.sml b/examples/pseudo_bool/cp_encoding/cp_to_ilpScript.sml
index 94ce1ded3f..66f0c8a38b 100644
--- a/examples/pseudo_bool/cp_encoding/cp_to_ilpScript.sml
+++ b/examples/pseudo_bool/cp_encoding/cp_to_ilpScript.sml
@@ -1091,15 +1091,6 @@ Proof
     mlstringTheory.StrongLinearOrder_fast_lt]
 QED
 
-(* NOTE: could move upstream to mlintTheory (next to int_cmp_def) *)
-Theorem TotOrd_int_cmp:
-  TotOrd mlint$int_cmp
-Proof
-  rw[totoTheory.TotOrd,mlintTheory.int_cmp_def]>>
-  every_case_tac>>gvs[]>>
-  intLib.ARITH_TAC
-QED
-
 (* Total order on varc: variables (INL, by fast_compare) before
   constants (INR, by int_cmp) *)
 Definition varc_compare_def:
@@ -1118,14 +1109,14 @@ Proof
   >- (
     Cases_on`x`>>Cases_on`y`>>
     gvs[varc_compare_def]>>
-    metis_tac[TotOrd_fast_compare,TotOrd_int_cmp,totoTheory.TotOrd])
+    metis_tac[TotOrd_fast_compare,mlintTheory.TotOrd_int_cmp,totoTheory.TotOrd])
   >- (
     Cases_on`x`>>Cases_on`y`>>
     gvs[varc_compare_def]>>
-    metis_tac[TotOrd_fast_compare,TotOrd_int_cmp,totoTheory.TotOrd])>>
+    metis_tac[TotOrd_fast_compare,mlintTheory.TotOrd_int_cmp,totoTheory.TotOrd])>>
   Cases_on`x`>>Cases_on`y`>>Cases_on`z`>>
   gvs[varc_compare_def]>>
-  metis_tac[TotOrd_fast_compare,TotOrd_int_cmp,totoTheory.TotOrd]
+  metis_tac[TotOrd_fast_compare,mlintTheory.TotOrd_int_cmp,totoTheory.TotOrd]
 QED
 
 Datatype:

From 2eee534c1709771f66d8822551b4b1e328b60621 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Wed, 5 Aug 2026 15:37:59 +0200
Subject: [PATCH 4/8] More work on finite maps and the translator

---
 compiler/inference/tests/.gitignore | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 compiler/inference/tests/.gitignore

diff --git a/compiler/inference/tests/.gitignore b/compiler/inference/tests/.gitignore
new file mode 100644
index 0000000000..6ee69c6136
--- /dev/null
+++ b/compiler/inference/tests/.gitignore
@@ -0,0 +1 @@
+new_types.txt

From 175554b2555385cfece7b4ecd313cee562019eb4 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Wed, 5 Aug 2026 17:50:46 +0200
Subject: [PATCH 5/8] Changes missed in previous commit

---
 compiler/inference/tests/Holmakefile          | 12 ++++++++-
 compiler/inference/tests/README.md            |  3 ++-
 .../inference/tests/basisTypeCheckScript.sml  | 13 +++++++---
 developers/changes-since-release.md           | 26 +++++++++++++++++++
 4 files changed, 49 insertions(+), 5 deletions(-)

diff --git a/compiler/inference/tests/Holmakefile b/compiler/inference/tests/Holmakefile
index c1f16bda19..59ad231169 100644
--- a/compiler/inference/tests/Holmakefile
+++ b/compiler/inference/tests/Holmakefile
@@ -1,5 +1,15 @@
 INCLUDES = $(CAKEMLDIR)/misc $(CAKEMLDIR)/basis ..
 
-all: $(DEFAULT_TARGETS) README.md
+all: $(DEFAULT_TARGETS) README.md check-basis-types
+.PHONY: all check-basis-types
 
 sinclude $(CAKEMLDIR)/developers/readme.mk
+
+# basisTypeCheckScript.sml writes the inferred basis signature to
+# new_types.txt. This must agree with the checked-in basis/types.txt, which is
+# otherwise only checked much later in the regression, by running the compiled
+# cake binary in unverified/sexpr-bootstrap.
+check-basis-types: basisTypeCheckTheory.uo
+	diff --context $(CAKEMLDIR)/basis/types.txt new_types.txt
+
+EXTRA_CLEANS = new_types.txt
diff --git a/compiler/inference/tests/README.md b/compiler/inference/tests/README.md
index 139c447ca1..384559d5e1 100644
--- a/compiler/inference/tests/README.md
+++ b/compiler/inference/tests/README.md
@@ -4,4 +4,5 @@ the logic of HOL.
 [basisTypeCheckScript.sml](basisTypeCheckScript.sml):
 This file checks that the CakeML standard basis library passes the
 type inferencer. This file also acts as a test of cv_compute
-evaluation of the type inferencer.
+evaluation of the type inferencer. It writes the inferred signature to
+new_types.txt, which the Holmakefile diffs against basis/types.txt.
diff --git a/compiler/inference/tests/basisTypeCheckScript.sml b/compiler/inference/tests/basisTypeCheckScript.sml
index 688b541d1d..46dc0e265f 100644
--- a/compiler/inference/tests/basisTypeCheckScript.sml
+++ b/compiler/inference/tests/basisTypeCheckScript.sml
@@ -1,7 +1,8 @@
 (*
   This file checks that the CakeML standard basis library passes the
   type inferencer. This file also acts as a test of cv_compute
-  evaluation of the type inferencer.
+  evaluation of the type inferencer. It writes the inferred signature to
+  new_types.txt, which the Holmakefile diffs against basis/types.txt.
 *)
 Theory basisTypeCheck[no_sig_docs]
 Ancestors
@@ -26,10 +27,16 @@ val print_types = let
                                   "fully evaluate type inferencer error message)")
           end
           else failwith "Failed to fully evaluate type inferencer applied to basis."
-  val _ = print "\nTypes of all basis functions:\n\n"
   val strs = EVAL (mk_comb(“inf_env_to_types_string”,rand x))
                |> concl |> rand |> listSyntax.dest_list |> fst
-               |> map (stringSyntax.fromHOLstring o rand) |> map print
+               |> map (stringSyntax.fromHOLstring o rand)
+  val _ = print "\nTypes of all basis functions:\n\n"
+  val _ = app print strs
   val _ = print "\n"
+  (* the same text that the compiler prints for its --types option, i.e. the
+     content that basis/types.txt ought to have *)
+  val f = TextIO.openOut "new_types.txt"
+  val _ = app (fn s => TextIO.output (f,s)) (["\n"] @ strs @ ["\n"])
+  val _ = TextIO.closeOut f
   in () end
 
diff --git a/developers/changes-since-release.md b/developers/changes-since-release.md
index edd5da5bf1..562de698f7 100644
--- a/developers/changes-since-release.md
+++ b/developers/changes-since-release.md
@@ -19,12 +19,25 @@ has been added to basis.
 `String.concatWith` has been reimplemented using `concat` and `intersperse`,
 avoiding potentially quadratic behavior due to left-associative concatenations (#1425).
 
+`String.Fast.compare` has been added.
+Like the other operations in the `String.Fast` module, it orders strings by
+length first and only compares contents when the lengths are equal, which is faster.
+
+### Map
+
+`Map.diff` has been added to basis. `Map.diff m1 m2` removes from `m1` every
+key that occurs in `m2`. The inputs can have different value types.
+
 ### TextIO
 
 `TextIO.output`'s behavior is now linear in the size of the string
 (previously quadratic -- oops!). This should allow users to output large strings
 (as in: much larger than 2kB) without the program hanging (#1425).
 
+`TextIO.inputAllFrom` has been added to basis. It reads all input from stdin
+(on `None`) or from a named file (on `Some fname`), closing the stream
+afterwards, and returns `None` if the file cannot be opened.
+
 ## Compiler backend and runtime
 
 ### BVI
@@ -54,6 +67,19 @@ results, has been deleted and a new `basis_ffiLib.prove_sem_thm` is to
 be used instead from now on. The old one used to be slow and clunky to
 use; the new one runs within a few seconds at each call site.
 
+### Translation of HOL finite maps
+
+The new `MapProgLib.add_fmap_for_cmp` teaches the translator to represent
+HOL finite maps (`:'a |-> 'b`) by `mlmap` balanced binary trees. Given a
+`TotOrd cmp` theorem for an already translated comparison `cmp`, it
+registers translations of the following:
+ - `FEMPTY`
+ - `FLOOKUP`
+ - `fmap_update` (a wrapper around `_ |+ (_, _)`)
+ - `$\\`
+ - `FUNION`
+ - `fdiff_fdom` (a wrapper around `FDIFF _ (FDOM _)`)
+
 ### simp additions
 
 The following simps have been added:

From 01d157a510d2b9268a31b3ee40bb9be0d4986fd2 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Fri, 7 Aug 2026 09:32:07 +0200
Subject: [PATCH 6/8] Fix inferProg for finite map change

---
 compiler/bootstrap/translation/decProgScript.sml   | 4 ++--
 compiler/bootstrap/translation/inferProgScript.sml | 3 +++
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/compiler/bootstrap/translation/decProgScript.sml b/compiler/bootstrap/translation/decProgScript.sml
index a6ee900fcc..c2706a49e5 100644
--- a/compiler/bootstrap/translation/decProgScript.sml
+++ b/compiler/bootstrap/translation/decProgScript.sml
@@ -73,9 +73,9 @@ val r = translate repl_decs_allowedTheory.decs_allowed_def;
 (* teach the translator how to translate fmap operations for key types:
     - mlstring
     - int
-    - num
+ (* - num *)
 *)
 
 val _ = MapProgLib.add_fmap_for_cmp mlstringTheory.TotOrd_fast_compare;
 val _ = MapProgLib.add_fmap_for_cmp mlintTheory.TotOrd_int_cmp;
-val _ = MapProgLib.add_fmap_for_cmp miscTheory.TotOrd_num_cmp;
+(* val _ = MapProgLib.add_fmap_for_cmp miscTheory.TotOrd_num_cmp; *)
diff --git a/compiler/bootstrap/translation/inferProgScript.sml b/compiler/bootstrap/translation/inferProgScript.sml
index 4b314db01d..3c0f202974 100644
--- a/compiler/bootstrap/translation/inferProgScript.sml
+++ b/compiler/bootstrap/translation/inferProgScript.sml
@@ -468,6 +468,9 @@ Proof
   AP_TERM_TAC \\ fs [FUN_EQ_THM,FORALL_PROD]
 QED
 
+val _ = translate
+  (alist_to_fmap_def |> RW [GSYM fmap_update_def] |> INST_TYPE [alpha|->“:mlstring”]);
+
 val _ = translate (typeSystemTheory.build_ctor_tenv_def
          |> REWRITE_RULE [MAP_type_name_subst]
                     |> SIMP_RULE std_ss [lemma]);

From 2aa89b6f5788f208a78ff2780bc879a795853b98 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Mon, 10 Aug 2026 09:40:23 +0200
Subject: [PATCH 7/8] Remove old fmap support in HOL->CakeML translator

---
 basis/ListProgScript.sml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

diff --git a/basis/ListProgScript.sml b/basis/ListProgScript.sml
index 86db50a175..4259d3a6c9 100644
--- a/basis/ListProgScript.sml
+++ b/basis/ListProgScript.sml
@@ -405,6 +405,8 @@ val _ =  ml_prog_update (close_module NONE);
 
 val _ = ml_prog_update (open_module "Alist");
 
+(*
+
 Definition FMAP_EQ_ALIST_def:
   FMAP_EQ_ALIST f l <=> (ALOOKUP l = FLOOKUP f)
 End
@@ -417,9 +419,13 @@ End
 val _ = add_type_inv ``FMAP_TYPE (a:'a -> v -> bool) (b:'b -> v -> bool)``
                      ``:('a # 'b) list``;
 
+*)
+
 val _ = next_ml_names := ["lookup"];
 val ALOOKUP_eval = translate ALOOKUP_def;
 
+(*
+
 val Eval_FLOOKUP = Q.prove(
   `!v. ((LIST_TYPE (PAIR_TYPE (b:'b -> v -> bool) (a:'a -> v -> bool)) -->
           b --> OPTION_TYPE a) ALOOKUP) v ==>
@@ -429,12 +435,16 @@ val Eval_FLOOKUP = Q.prove(
   |> (fn th => MATCH_MP th ALOOKUP_eval)
   |> add_user_proved_v_thm;
 
+*)
+
 val _ = next_ml_names := ["update"];
 Definition AUPDATE_def:
   AUPDATE l (x:'a,y:'b) = (x,y)::l
 End
 val AUPDATE_eval = translate AUPDATE_def;
 
+(*
+
 Theorem FMAP_EQ_ALIST_UPDATE[local]:
   FMAP_EQ_ALIST f l ==> FMAP_EQ_ALIST (FUPDATE f (x,y)) (AUPDATE l (x,y))
 Proof
@@ -466,6 +476,8 @@ val Eval_FEMPTY = Q.prove(
   |> MATCH_MP (MATCH_MP Eval_WEAKEN NIL_eval)
   |> add_eval_thm;
 
+*)
+
 Definition AEVERY_AUX_def:
   (AEVERY_AUX aux P [] = T) /\
   (AEVERY_AUX aux P ((x:'a,y:'b)::xs) =
@@ -479,6 +491,8 @@ val _ = next_ml_names := ["every","every"];
 val _ = translate AEVERY_AUX_def;
 val AEVERY_eval = translate AEVERY_def;
 
+(*
+
 Theorem AEVERY_AUX_THM[local]:
   !l aux P. AEVERY_AUX aux P l <=>
               !x y. (ALOOKUP l x = SOME y) /\ ~(MEM x aux) ==> P (x,y)
@@ -514,6 +528,8 @@ val Eval_FEVERY = Q.prove(
   |> (fn th => MATCH_MP th AEVERY_eval)
   |> add_user_proved_v_thm;
 
+*)
+
 val _ = next_ml_names := ["map"];
 Definition AMAP_def:
   (AMAP f [] = []) /\
@@ -521,6 +537,8 @@ Definition AMAP_def:
 End
 val AMAP_eval = translate AMAP_def;
 
+(*
+
 Theorem ALOOKUP_AMAP[local]:
   !l. ALOOKUP (AMAP f l) a =
         case ALOOKUP l a of NONE => NONE | SOME x => SOME (f x)
@@ -576,6 +594,8 @@ val Eval_FUNION = Q.prove(
   |> (fn th => MATCH_MP th append_eval)
   |> add_user_proved_v_thm;
 
+*)
+
 val _ = next_ml_names := ["delete"];
 Definition ADEL_def:
   (ADEL [] z = []) /\
@@ -583,6 +603,8 @@ Definition ADEL_def:
 End
 val ADEL_eval = translate ADEL_def;
 
+(*
+
 Theorem ALOOKUP_ADEL[local]:
   !l a x. ALOOKUP (ADEL l a) x = if x = a then NONE else ALOOKUP l x
 Proof
@@ -609,4 +631,6 @@ val Eval_fmap_domsub = Q.prove(
   |> (fn th => MATCH_MP th ADEL_eval)
   |> add_user_proved_v_thm;
 
+*)
+
 val _ =  ml_prog_update (close_module NONE);

From 5ccbdb6dcd04bee3a4105155aafd2ee5ee02f8f3 Mon Sep 17 00:00:00 2001
From: Magnus Myreen <magnus.myreen@cl.cam.ac.uk>
Date: Wed, 12 Aug 2026 22:51:13 +0200
Subject: [PATCH 8/8] Fix PEG translations

---
 .../translation/caml_parserProgScript.sml     | 69 ++++++-------
 .../bootstrap/translation/decProgScript.sml   | 22 ++++-
 .../bootstrap/translation/inferProgScript.sml |  3 -
 .../translation/pancake_parseProgScript.sml   | 68 +++++++------
 .../translation/parserProgScript.sml          | 97 +++++++++++--------
 compiler/parsing/cmlParseScript.sml           |  8 +-
 .../ocaml/camlPtreeConversionScript.sml       |  5 +-
 compiler/parsing/proofs/parserProofScript.sml |  4 +-
 examples/grepProgScript.sml                   | 29 +++---
 9 files changed, 174 insertions(+), 131 deletions(-)

diff --git a/compiler/bootstrap/translation/caml_parserProgScript.sml b/compiler/bootstrap/translation/caml_parserProgScript.sml
index 83016440c1..5e25d196ae 100644
--- a/compiler/bootstrap/translation/caml_parserProgScript.sml
+++ b/compiler/bootstrap/translation/caml_parserProgScript.sml
@@ -218,39 +218,8 @@ val r = translate extract_record_defns_def;
 val r = translate strip_record_fields_def;
 
 val r = preprocess ptree_TypeDefinition_def |> translate;
-
 val r = preprocess ptree_ModuleType_def |> translate;
 val r = preprocess ptree_Definition_def |> translate;
-
-Theorem destresult_side[local]:
-  pegexec_destresult_side v = (?r. v = Result r)
-Proof
-  rw [fetch "-" "pegexec_destresult_side_def"]
-  \\ Cases_on `v` \\ gs []
-QED
-
-Theorem ptree_definition_side:
-  (∀x. camlptreeconversion_ptree_definition_side x) ∧
-  (∀x. camlptreeconversion_ptree_modexpr_side x) ∧
-  (∀x. camlptreeconversion_ptree_moduleitems_side x) ∧
-  (∀x. camlptreeconversion_ptree_moduleitem_side x) ∧
-  (∀x. camlptreeconversion_ptree_exprordefn_side x)
-Proof
-  ho_match_mp_tac ptree_Definition_ind \\ rw []
-  \\ simp [Once (fetch "-" "camlptreeconversion_ptree_definition_side_def")]
-  \\ rw []
-  \\ simp [parserProgTheory.parse_prog_side_def,
-           parserProgTheory.peg_exec_side_def,
-           parserProgTheory.coreloop_side_def]
-  \\ rename [‘lexer_fun inp’]
-  \\ qspec_then ‘lexer_fun$lexer_fun inp’ strip_assume_tac
-                cmlPEGTheory.owhile_TopLevelDecs_total
-  \\ fs [parserProgTheory.INTRO_FLOOKUP, SF ETA_ss]
-  \\ simp [destresult_side, cmlPEGTheory.parse_TopLevelDecs_total]
-QED
-
-val _ = List.map update_precondition (CONJUNCTS ptree_definition_side);
-
 val r = preprocess ptree_Start_def |> translate;
 
 (* -------------------------------------------------------------------------
@@ -269,19 +238,42 @@ Proof
 QED
 
 val r = translate (identMixed_def |> PURE_REWRITE_RULE [and_or_imp_lemma]);
-
 val r = translate run_lexer_def;
-val r = translate run_parser_def;
+
+Definition peg_caml_rules_def:
+  peg_caml_rules n fk k tf3 errs eo r i =
+  case FLOOKUP camlPEG.rules n of
+  | NONE => Looped
+  | SOME x => pegexec$EV x i r eo errs (appf1 tf3 k) fk
+End
+
+val r = peg_caml_rules_def
+  |> RW [camlPEG_def, oneline OPTION_BIND_def]
+  |> SRULE [FUPDATE_LIST, parserProgTheory.option_CASE_FLOOKUP_SIMP, FOLDL]
+  |> translate;
+
+val r = run_parser_def
+  |> SRULE [pegexecTheory.coreloop_def,
+            pegexecTheory.peg_exec_def, GSYM peg_caml_rules_def,
+            parserProgTheory.INTRO_FLOOKUP]
+  |> SRULE [camlPEG_def]
+  |> translate;
 
 Theorem run_parser_side[local]:
   ∀x. caml_parser_run_parser_side x
 Proof
-  rw [fetch "-" "caml_parser_run_parser_side_def",
-      parserProgTheory.peg_exec_side_def,
-      parserProgTheory.coreloop_side_def,
-      camlPEGTheory.owhile_Start_total]
+  rw [fetch "-" "caml_parser_run_parser_side_def"]
   \\ qspec_then ‘x’ strip_assume_tac owhile_Start_total
-  \\ gs [parserProgTheory.INTRO_FLOOKUP, SF ETA_ss]
+  \\ pop_assum mp_tac
+  \\ simp [parserProgTheory.INTRO_FLOOKUP, GSYM peg_caml_rules_def]
+  \\ CONV_TAC (DEPTH_CONV ETA_CONV)
+  \\ qmatch_goalsub_abbrev_tac ‘OWHILE g1 g2’
+  \\ strip_tac \\ gvs []
+  \\ qmatch_goalsub_abbrev_tac ‘OWHILE f1 f2’
+  \\ qsuff_tac ‘g1 = f1 ∧ f2 = g2’ >- (strip_tac \\ gvs [])
+  \\ unabbrev_all_tac
+  \\ rpt $ pop_assum kall_tac
+  \\ fs [FUN_EQ_THM, camlPEG_def]
 QED
 
 val _ = update_precondition run_parser_side;
@@ -297,4 +289,3 @@ QED
 val _ = update_precondition run_side;
 
 val () = ml_translatorLib.clean_on_exit := true;
-
diff --git a/compiler/bootstrap/translation/decProgScript.sml b/compiler/bootstrap/translation/decProgScript.sml
index c2706a49e5..7ec619d59a 100644
--- a/compiler/bootstrap/translation/decProgScript.sml
+++ b/compiler/bootstrap/translation/decProgScript.sml
@@ -78,4 +78,24 @@ val r = translate repl_decs_allowedTheory.decs_allowed_def;
 
 val _ = MapProgLib.add_fmap_for_cmp mlstringTheory.TotOrd_fast_compare;
 val _ = MapProgLib.add_fmap_for_cmp mlintTheory.TotOrd_int_cmp;
-(* val _ = MapProgLib.add_fmap_for_cmp miscTheory.TotOrd_num_cmp; *)
+val _ = MapProgLib.add_fmap_for_cmp miscTheory.TotOrd_num_cmp;
+
+val RW = REWRITE_RULE;
+
+val _ = translate (alist_to_fmap_def |> RW [GSYM fmap_update_def]
+                                     |> INST_TYPE [alpha|->“:mlstring”]);
+
+val _ = translate (alist_to_fmap_def |> RW [GSYM fmap_update_def]
+                                     |> INST_TYPE [alpha|->“:int”]);
+
+val _ = translate (alist_to_fmap_def |> RW [GSYM fmap_update_def]
+                                     |> INST_TYPE [alpha|->“:num”]);
+
+val _ = translate (miscTheory.fmap_update_def |> GSYM |> oneline
+                                              |> INST_TYPE [alpha|->“:mlstring”]);
+
+val _ = translate (miscTheory.fmap_update_def |> GSYM |> oneline
+                                              |> INST_TYPE [alpha|->“:int”]);
+
+val _ = translate (miscTheory.fmap_update_def |> GSYM |> oneline
+                                              |> INST_TYPE [alpha|->“:num”]);
diff --git a/compiler/bootstrap/translation/inferProgScript.sml b/compiler/bootstrap/translation/inferProgScript.sml
index 3c0f202974..4b314db01d 100644
--- a/compiler/bootstrap/translation/inferProgScript.sml
+++ b/compiler/bootstrap/translation/inferProgScript.sml
@@ -468,9 +468,6 @@ Proof
   AP_TERM_TAC \\ fs [FUN_EQ_THM,FORALL_PROD]
 QED
 
-val _ = translate
-  (alist_to_fmap_def |> RW [GSYM fmap_update_def] |> INST_TYPE [alpha|->“:mlstring”]);
-
 val _ = translate (typeSystemTheory.build_ctor_tenv_def
          |> REWRITE_RULE [MAP_type_name_subst]
                     |> SIMP_RULE std_ss [lemma]);
diff --git a/compiler/bootstrap/translation/pancake_parseProgScript.sml b/compiler/bootstrap/translation/pancake_parseProgScript.sml
index e5a2bd287e..ff93b647b5 100644
--- a/compiler/bootstrap/translation/pancake_parseProgScript.sml
+++ b/compiler/bootstrap/translation/pancake_parseProgScript.sml
@@ -102,33 +102,47 @@ val _ = translate keep_nat_def;
 
 val _ = translate keep_int_def;
 
-val _ = translate pancake_peg_def;
-
-val _ = translate parse_def;
-
-Theorem parse_side_lemma = Q.prove(`
-  !x. parse_side x = T`,
-  SIMP_TAC std_ss [fetch "-" "parse_side_def",
-                   parserProgTheory.peg_exec_side_def,
-                   parserProgTheory.coreloop_side_def] \\
-  rpt strip_tac \\
-  assume_tac PEG_wellformed \\
-  drule_then strip_assume_tac pegexecTheory.peg_exec_total \\
-  first_x_assum $ qspec_then `x` strip_assume_tac \\
-  gvs [pegexecTheory.peg_exec_def,
-       pegexecTheory.coreloop_def,
-       AllCaseEqs(),
-       pegexecTheory.evalcase_distinct,
-       SIMP_CONV (srw_ss()) [pancake_peg_def] ``pancake_peg.start``,
-       IS_SOME_EXISTS] \\
-  rename1 ‘_ = SOME (Result rr)’ \\
-  qexists_tac `Result rr`\\
-  pop_assum (REWRITE_TAC o single o GSYM) \\
-  rpt (AP_THM_TAC ORELSE AP_TERM_TAC) \\
-  rw[FUN_EQ_THM] \\
-  rpt(PURE_FULL_CASE_TAC >> gvs[FDOM_FLOOKUP]) \\
-  gvs [flookup_thm])
-  |> update_precondition;
+Definition peg_pancake_rules_def:
+  peg_pancake_rules n fk k tf3 errs eo r i =
+  case FLOOKUP pancake_peg.rules n of
+  | NONE => Looped
+  | SOME x => pegexec$EV x i r eo errs (appf1 tf3 k) fk
+End
+
+val r = peg_pancake_rules_def
+  |> RW [pancake_peg_def, oneline OPTION_BIND_def]
+  |> SRULE [FUPDATE_LIST, parserProgTheory.option_CASE_FLOOKUP_SIMP, FOLDL]
+  |> translate;
+
+val r = parse_def
+  |> RW [pegexecTheory.peg_exec_def, GSYM peg_pancake_rules_def,
+         pegexecTheory.coreloop_def, parserProgTheory.INTRO_FLOOKUP]
+  |> SRULE [pancake_peg_def]
+  |> translate;
+
+Theorem parse_side_lemma:
+  !x. parse_side x = T
+Proof
+  SIMP_TAC std_ss [fetch "-" "parse_side_def"]
+  \\ rpt strip_tac
+  \\ assume_tac PEG_wellformed
+  \\ drule_then strip_assume_tac pegexecTheory.peg_exec_total
+  \\ first_x_assum $ qspec_then `x` strip_assume_tac
+  \\ pop_assum mp_tac
+  \\ rewrite_tac [pegexecTheory.coreloop_def,
+                  pegexecTheory.peg_exec_def, GSYM peg_pancake_rules_def,
+                  parserProgTheory.INTRO_FLOOKUP]
+  \\ simp [pancake_peg_def]
+  \\ qmatch_goalsub_abbrev_tac ‘OWHILE _ f2’ \\ strip_tac
+  \\ qmatch_goalsub_abbrev_tac ‘OWHILE _ g2’
+  \\ gvs [AllCaseEqs()]
+  \\ qsuff_tac ‘f2 = g2’ >- (strip_tac \\ gvs [])
+  \\ unabbrev_all_tac
+  \\ rpt $ pop_assum kall_tac
+  \\ simp [pancake_peg_def, SF ETA_ss]
+QED
+
+val _ = update_precondition parse_side_lemma;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 
diff --git a/compiler/bootstrap/translation/parserProgScript.sml b/compiler/bootstrap/translation/parserProgScript.sml
index 74294ea022..9f3aafef02 100644
--- a/compiler/bootstrap/translation/parserProgScript.sml
+++ b/compiler/bootstrap/translation/parserProgScript.sml
@@ -94,8 +94,6 @@ Proof
 QED
 val _ = update_precondition validaddsym_side_lemma;
 
-val _ = translate (def_of_const ``cmlPEG``);
-
 Theorem not_mlstring_emp[simp]:
   x ≠  «» ⇒
   0 < strlen x
@@ -104,34 +102,6 @@ Proof
   Cases_on`s`>>gvs[]
 QED
 
-Theorem cmlpeg_side[local]:
-  cmlpeg_side ⇔ T
-Proof
-  fs[fetch "-" "cmlpeg_side_def",
-    fetch "-" "peg_v_side_def",
-    fetch "-" "peg_longv_side_def",
-    fetch "-" "peg_uqconstructorname_side_def"
-    ]
-QED
-
-val _ = update_precondition cmlpeg_side;
-
-Theorem INTRO_FLOOKUP:
-   (if n ∈ FDOM G.rules then
-      pegexec$EV (G.rules ' n) i r eo errs (appf1 tf3 k) fk
-    else Looped) =
-   (case FLOOKUP G.rules n of
-      NONE => Looped
-    | SOME x => pegexec$EV x i r eo errs (appf1 tf3 k) fk)
-Proof
-  SRW_TAC [] [finite_mapTheory.FLOOKUP_DEF]
-QED
-
-val _ = translate (def_of_const ``coreloop`` |> RW [INTRO_FLOOKUP]
-                   |> SPEC_ALL |> RW1 [FUN_EQ_THM]);
-
-val _ = translate (def_of_const ``peg_exec``);
-
 (* parsing: cmlvalid *)
 
 Theorem monad_unitbind_assert:
@@ -241,17 +211,62 @@ val _ = translate (def_of_const ``ptree_TopLevelDecs``);
 
 (* parsing: top-level parser *)
 
-val _ = translate (RW [monad_unitbind_assert] parse_prog_def);
-
-Theorem parse_prog_side_lemma = Q.prove(`
-  !x. parse_prog_side x = T`,
-  SIMP_TAC std_ss [fetch "-" "parse_prog_side_def",
-    fetch "-" "peg_exec_side_def", fetch "-" "coreloop_side_def"]
-  THEN REPEAT STRIP_TAC
-  THEN STRIP_ASSUME_TAC (Q.SPEC `v1` owhile_TopLevelDecs_total)
-  THEN FULL_SIMP_TAC std_ss [INTRO_FLOOKUP] THEN POP_ASSUM MP_TAC
-  THEN CONV_TAC (DEPTH_CONV ETA_CONV) THEN FULL_SIMP_TAC std_ss [])
-  |> update_precondition;
+Theorem INTRO_FLOOKUP:
+   (if n ∈ FDOM G.rules then
+      pegexec$EV (G.rules ' n) i r eo errs (appf1 tf3 k) fk
+    else Looped) =
+   (case FLOOKUP G.rules n of
+      NONE => Looped
+    | SOME x => pegexec$EV x i r eo errs (appf1 tf3 k) fk)
+Proof
+  SRW_TAC [] [finite_mapTheory.FLOOKUP_DEF]
+QED
+
+Theorem option_CASE_FLOOKUP_SIMP:
+  option_CASE (FLOOKUP FEMPTY n) f h = f ∧
+  option_CASE (FLOOKUP (m |+ (a,b)) n) f h =
+  if n = a then h b else option_CASE (FLOOKUP m n) f h
+Proof
+  rw [] \\ gvs [FLOOKUP_SIMP]
+QED
+
+Definition peg_cml_rules_def:
+  peg_cml_rules n fk k tf3 errs eo r i =
+  case FLOOKUP cmlPEG.rules n of
+  | NONE => Looped
+  | SOME x => pegexec$EV x i r eo errs (appf1 tf3 k) fk
+End
+
+val def = peg_cml_rules_def
+  |> RW [cmlPEG_def, oneline OPTION_BIND_def]
+  |> SRULE [FUPDATE_LIST, option_CASE_FLOOKUP_SIMP, FOLDL];
+
+val _ = translate def;
+
+val def = cml_parse_nTopLevelDecs_def
+  |> SRULE [monad_unitbind_assert, pegresult_bind_def, FUN_EQ_THM,
+            pegexecTheory.peg_exec_def, pegexecTheory.coreloop_def, INTRO_FLOOKUP,
+            GSYM peg_cml_rules_def]
+  |> SRULE [cmlPEG_def];
+
+val _ = translate def;
+
+Theorem cml_parse_ntopleveldecs_side_lemma[local]:
+  !x. cml_parse_ntopleveldecs_side x = T
+Proof
+  rewrite_tac [fetch "-" "cml_parse_ntopleveldecs_side_def"]
+  \\ rpt strip_tac
+  \\ qspec_then ‘x’ strip_assume_tac owhile_TopLevelDecs_total
+  \\ fs [INTRO_FLOOKUP, GSYM peg_cml_rules_def]
+  \\ gvs [cmlPEG_def]
+  \\ pop_assum mp_tac
+  \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ fs []
+QED
+
+val _ = update_precondition cml_parse_ntopleveldecs_side_lemma;
+
+val r = translate parse_prog_def;
+val _ = null (hyp r) orelse failwith "unproved side conditions";
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
 
diff --git a/compiler/parsing/cmlParseScript.sml b/compiler/parsing/cmlParseScript.sml
index 85b8ee2017..7b6d0542ce 100644
--- a/compiler/parsing/cmlParseScript.sml
+++ b/compiler/parsing/cmlParseScript.sml
@@ -72,12 +72,16 @@ Definition cmlParseExpr_def:
   od
 End
 
+Definition cml_parse_nTopLevelDecs_def:
+  cml_parse_nTopLevelDecs toks =
+  destResult (cmlpegexec nTopLevelDecs toks)
+End
+
 Definition parse_prog_def:
   parse_prog =
     do
-      pts <- destResult o cmlpegexec nTopLevelDecs;
+      pts <- cml_parse_nTopLevelDecs;
       pt <- optlift $ oHD pts;
       optlift $ ptree_TopLevelDecs pt;
     od
 End
-
diff --git a/compiler/parsing/ocaml/camlPtreeConversionScript.sml b/compiler/parsing/ocaml/camlPtreeConversionScript.sml
index 25e6960506..e7738adc98 100644
--- a/compiler/parsing/ocaml/camlPtreeConversionScript.sml
+++ b/compiler/parsing/ocaml/camlPtreeConversionScript.sml
@@ -3190,9 +3190,6 @@ Definition peg_def:
   peg (Success (_: (tokens$token # locs) list) x _) = return x
 End
 
-Overload cmlpegexec[local] =
-  ``λn t. peg_exec cmlPEG$cmlPEG (cmlPEG$pnt n) t [] NONE [] done failed``;
-
 Definition ptree_Definition_def:
   (ptree_Definition (Lf (_, locs)) =
     fail (locs, «Expected a top-level definition non-terminal»)) ∧
@@ -3213,7 +3210,7 @@ Definition ptree_Definition_def:
               fail (locs, «The CakeML lexer failed»)
             else
               do
-                pts <- peg (destResult (cmlpegexec gram$nTopLevelDecs toks));
+                pts <- peg (cml_parse_nTopLevelDecs toks);
                 pt <- option $ oHD pts;
                 option $ cmlPtreeConversion$ptree_TopLevelDecs pt
               od ++ fail (locs, «The CakeML parser failed»)
diff --git a/compiler/parsing/proofs/parserProofScript.sml b/compiler/parsing/proofs/parserProofScript.sml
index cfbb14f7ed..4eea57e4f5 100644
--- a/compiler/parsing/proofs/parserProofScript.sml
+++ b/compiler/parsing/proofs/parserProofScript.sml
@@ -12,7 +12,8 @@ Theorem parse_prog_correct0:
   (parse_prog s = Failure fl fe ⇒ parse s = NONE) ∧
   (parse_prog s = Success s' a eo ⇒ parse s = SOME a ∧ s' = [])
 Proof
-  simp[parse_prog_def, parse_def, pegresult_bind_def, cmlPEGTheory.pnt_def] >>
+  simp[parse_prog_def, parse_def, pegresult_bind_def, cmlPEGTheory.pnt_def,
+       cml_parse_nTopLevelDecs_def] >>
   ‘∃r. peg_eval cmlPEG (s, nt (mkNT nTopLevelDecs) I) r’
     by simp[pegTheory.peg_eval_total] >>
   drule_then assume_tac pegexecTheory.pegexec >>
@@ -76,4 +77,3 @@ Proof
   >- (drule $ cj 2 parse_prog_correct0 >> simp[]) >>
   drule $ cj 1 parse_prog_correct0 >> simp[]
 QED
-
diff --git a/examples/grepProgScript.sml b/examples/grepProgScript.sml
index 636b145dac..bacf137f14 100644
--- a/examples/grepProgScript.sml
+++ b/examples/grepProgScript.sml
@@ -395,13 +395,10 @@ Proof
 QED
 
 val coreloop_def' =
-( pegexecTheory.coreloop_def
+  pegexecTheory.coreloop_def
     |> REWRITE_RULE [INTRO_FLOOKUP]
-    |> SPEC_ALL |> ONCE_REWRITE_RULE [FUN_EQ_THM]);
-
-val r = translate coreloop_def';
-
-val r = translate (pegexecTheory.peg_exec_def);
+    |> SPEC_ALL |> ONCE_REWRITE_RULE [FUN_EQ_THM]
+    |> INST_TYPE [beta |-> “:reNT”];
 
 (* -- *)
 
@@ -445,19 +442,27 @@ val uncharset_char_side = Q.prove(
     \\ `n MOD 256 < 256` by simp[]
     \\ simp[]) |> update_precondition;
 
-val r = translate rePEG_def;
-
-val r = translate parse_regexp_def;
+Theorem option_CASE_FLOOKUP_SIMP:
+  option_CASE (FLOOKUP FEMPTY n) f h = f ∧
+  option_CASE (FLOOKUP (m |+ (a,b)) n) f h =
+  if n = a then h b else option_CASE (FLOOKUP m n) f h
+Proof
+  rw [] \\ gvs [FLOOKUP_SIMP]
+QED
 
 val termination_lemma =
   MATCH_MP pegexecTheory.coreloop_total wfG_rePEG
-  |> SIMP_RULE(srw_ss())[coreloop_def'];
+  |> SIMP_RULE(srw_ss())[coreloop_def', rePEG_def,
+       FUPDATE_LIST, option_CASE_FLOOKUP_SIMP]
+  |> GEN_ALL;
+
+val _ = translate
+  (parse_regexp_def |> SRULE [pegexecTheory.peg_exec_def,coreloop_def', rePEG_def,
+       FUPDATE_LIST, option_CASE_FLOOKUP_SIMP]);
 
 val parse_regexp_side = Q.prove(
   `∀x. parse_regexp_side x = T`,
   rw[definition"parse_regexp_side_def"] \\
-  rw[definition"peg_exec_side_def"] \\
-  rw[definition"coreloop_side_def"] \\
   qspec_then`MAP add_loc x`strip_assume_tac (GEN_ALL termination_lemma) \\
   qmatch_abbrev_tac`IS_SOME (OWHILE f g h)` \\
   qmatch_assum_abbrev_tac`OWHILE f g' h = SOME _` \\