Add support for FDIFF _ (FDOM _) to translator

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,13 +528,17 @@ 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 [] = []) /\
   (AMAP f ((x:'a,y:'b)::xs) = (x,(f y):'c) :: AMAP f xs)
 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,13 +594,17 @@ 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 = []) /\
   (ADEL ((x:'a,y:'b)::xs) z = if x = z then ADEL xs z else (x,y)::ADEL xs z)
 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);

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

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,18 +292,22 @@ 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 [])
   >- (irule IMP_FMAP_TYPE_FLOOKUP \\ simp [])
   >- (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];

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;

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

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
-

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) =

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