Make progress on extracting the HOL4 files

5 files changed, 319 insertions, 18 deletions

diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index e10ce7e5..4a1f5fdd 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -504,6 +504,33 @@ val all_mk_int_defs = [
   mk_u128_def
 ]
 
+(* Unfolding theorems for “mk_usize” and “mk_isize”: we need specific unfolding
+   theorems because the isize/usize bounds are opaque, and may make the evaluation
+   get stuck in the unit tests *)
+Theorem mk_usize_unfold:
+  ∀ n. mk_usize n =
+    if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then Return (int_to_usize n)
+    else Fail Failure
+Proof
+  rw [mk_usize_def] >> fs [] >>
+  assume_tac usize_bounds >>
+  int_tac
+QED
+val _ = evalLib.add_unfold_thm "mk_usize_unfold"
+
+Theorem mk_isize_unfold:
+  ∀ n. mk_isize n =
+    if (i16_min ≤ n ∨ isize_min ≤ n) ∧
+       (n ≤ i16_max ∨ n ≤ isize_max)
+    then Return (int_to_isize n)
+    else Fail Failure
+Proof
+  rw [mk_isize_def] >> fs [] >>
+  assume_tac isize_bounds >>
+  int_tac
+QED
+val _ = evalLib.add_unfold_thm "mk_isize_unfold"
+
 val isize_neg_def = Define ‘isize_neg x = mk_isize (- (isize_to_int x))’
 val i8_neg_def    = Define ‘i8_neg x    = mk_i8 (- (i8_to_int x))’
 val i16_neg_def   = Define ‘i16_neg x   = mk_i16 (- (i16_to_int x))’
@@ -1521,6 +1548,98 @@ Definition isize_ge_def:
 End
 
 
+(* Equality theorems for the comparisons between integers - used by evalLib *)
+
+val prove_scalar_eq_equiv_tac = metis_tac all_scalar_to_int_to_scalar_lemmas
+
+Theorem isize_eq_equiv:
+  ∀x y. (x = y) = (isize_to_int x = isize_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem i8_eq_equiv:
+  ∀x y. (x = y) = (i8_to_int x = i8_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem i16_eq_equiv:
+  ∀x y. (x = y) = (i16_to_int x = i16_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem i32_eq_equiv:
+  ∀x y. (x = y) = (i32_to_int x = i32_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem i64_eq_equiv:
+  ∀x y. (x = y) = (i64_to_int x = i64_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem i128_eq_equiv:
+  ∀x y. (x = y) = (i128_to_int x = i128_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem usize_eq_equiv:
+  ∀x y. (x = y) = (usize_to_int x = usize_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem u8_eq_equiv:
+  ∀x y. (x = y) = (u8_to_int x = u8_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem u16_eq_equiv:
+  ∀x y. (x = y) = (u16_to_int x = u16_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem u32_eq_equiv:
+  ∀x y. (x = y) = (u32_to_int x = u32_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem u64_eq_equiv:
+  ∀x y. (x = y) = (u64_to_int x = u64_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+Theorem u128_eq_equiv:
+  ∀x y. (x = y) = (u128_to_int x = u128_to_int y)
+Proof
+  prove_scalar_eq_equiv_tac
+QED
+
+(* Remark.: don't move this up, it will break some proofs *)
+val _ = BasicProvers.export_rewrites [
+  "isize_eq_equiv",
+  "i8_eq_equiv",
+  "i16_eq_equiv",
+  "i32_eq_equiv",
+  "i64_eq_equiv",
+  "i128_eq_equiv",
+  "usize_eq_equiv",
+  "u8_eq_equiv",
+  "u16_eq_equiv",
+  "u32_eq_equiv",
+  "u64_eq_equiv",
+  "u128_eq_equiv"
+]
+
 (***
  * Vectors
  *)
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index 1908cbcb..45caf234 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -221,6 +221,7 @@ sig
     val error_nchotomy : thm
     val i128_add_eq : thm
     val i128_div_eq : thm
+    val i128_eq_equiv : thm
     val i128_mul_eq : thm
     val i128_neg_eq : thm
     val i128_rem_eq : thm
@@ -228,6 +229,7 @@ sig
     val i128_to_int_int_to_i128_unfold : thm
     val i16_add_eq : thm
     val i16_div_eq : thm
+    val i16_eq_equiv : thm
     val i16_mul_eq : thm
     val i16_neg_eq : thm
     val i16_rem_eq : thm
@@ -235,6 +237,7 @@ sig
     val i16_to_int_int_to_i16_unfold : thm
     val i32_add_eq : thm
     val i32_div_eq : thm
+    val i32_eq_equiv : thm
     val i32_mul_eq : thm
     val i32_neg_eq : thm
     val i32_rem_eq : thm
@@ -242,6 +245,7 @@ sig
     val i32_to_int_int_to_i32_unfold : thm
     val i64_add_eq : thm
     val i64_div_eq : thm
+    val i64_eq_equiv : thm
     val i64_mul_eq : thm
     val i64_neg_eq : thm
     val i64_rem_eq : thm
@@ -249,6 +253,7 @@ sig
     val i64_to_int_int_to_i64_unfold : thm
     val i8_add_eq : thm
     val i8_div_eq : thm
+    val i8_eq_equiv : thm
     val i8_mul_eq : thm
     val i8_neg_eq : thm
     val i8_rem_eq : thm
@@ -258,11 +263,14 @@ sig
     val index_update_same : thm
     val isize_add_eq : thm
     val isize_div_eq : thm
+    val isize_eq_equiv : thm
     val isize_mul_eq : thm
     val isize_neg_eq : thm
     val isize_rem_eq : thm
     val isize_sub_eq : thm
     val isize_to_int_int_to_isize_unfold : thm
+    val mk_isize_unfold : thm
+    val mk_usize_unfold : thm
     val mk_vec_unfold : thm
     val num2error_11 : thm
     val num2error_ONTO : thm
@@ -277,30 +285,35 @@ sig
     val result_nchotomy : thm
     val u128_add_eq : thm
     val u128_div_eq : thm
+    val u128_eq_equiv : thm
     val u128_mul_eq : thm
     val u128_rem_eq : thm
     val u128_sub_eq : thm
     val u128_to_int_int_to_u128_unfold : thm
     val u16_add_eq : thm
     val u16_div_eq : thm
+    val u16_eq_equiv : thm
     val u16_mul_eq : thm
     val u16_rem_eq : thm
     val u16_sub_eq : thm
     val u16_to_int_int_to_u16_unfold : thm
     val u32_add_eq : thm
     val u32_div_eq : thm
+    val u32_eq_equiv : thm
     val u32_mul_eq : thm
     val u32_rem_eq : thm
     val u32_sub_eq : thm
     val u32_to_int_int_to_u32_unfold : thm
     val u64_add_eq : thm
     val u64_div_eq : thm
+    val u64_eq_equiv : thm
     val u64_mul_eq : thm
     val u64_rem_eq : thm
     val u64_sub_eq : thm
     val u64_to_int_int_to_u64_unfold : thm
     val u8_add_eq : thm
     val u8_div_eq : thm
+    val u8_eq_equiv : thm
     val u8_mul_eq : thm
     val u8_rem_eq : thm
     val u8_sub_eq : thm
@@ -309,6 +322,7 @@ sig
     val update_spec : thm
     val usize_add_eq : thm
     val usize_div_eq : thm
+    val usize_eq_equiv : thm
     val usize_mul_eq : thm
     val usize_rem_eq : thm
     val usize_sub_eq : thm
@@ -1366,6 +1380,11 @@ sig
           ∃z. i128_div x y = Return z ∧
               i128_to_int z = i128_to_int x / i128_to_int y
    
+   [i128_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_i128_i128_to_int] []
+      ⊢ ∀x y. x = y ⇔ i128_to_int x = i128_to_int y
+   
    [i128_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1436,6 +1455,11 @@ sig
           ∃z. i16_div x y = Return z ∧
               i16_to_int z = i16_to_int x / i16_to_int y
    
+   [i16_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_i16_i16_to_int] []
+      ⊢ ∀x y. x = y ⇔ i16_to_int x = i16_to_int y
+   
    [i16_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1505,6 +1529,11 @@ sig
           ∃z. i32_div x y = Return z ∧
               i32_to_int z = i32_to_int x / i32_to_int y
    
+   [i32_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_i32_i32_to_int] []
+      ⊢ ∀x y. x = y ⇔ i32_to_int x = i32_to_int y
+   
    [i32_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1574,6 +1603,11 @@ sig
           ∃z. i64_div x y = Return z ∧
               i64_to_int z = i64_to_int x / i64_to_int y
    
+   [i64_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_i64_i64_to_int] []
+      ⊢ ∀x y. x = y ⇔ i64_to_int x = i64_to_int y
+   
    [i64_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1643,6 +1677,11 @@ sig
           ∃z. i8_div x y = Return z ∧
               i8_to_int z = i8_to_int x / i8_to_int y
    
+   [i8_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_i8_i8_to_int] []
+      ⊢ ∀x y. x = y ⇔ i8_to_int x = i8_to_int y
+   
    [i8_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1730,6 +1769,11 @@ sig
           ∃z. isize_div x y = Return z ∧
               isize_to_int z = isize_to_int x / isize_to_int y
    
+   [isize_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_isize_isize_to_int] []
+      ⊢ ∀x y. x = y ⇔ isize_to_int x = isize_to_int y
+   
    [isize_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1787,6 +1831,24 @@ sig
             if i16_min ≤ n ∧ n ≤ i16_max then n
             else isize_to_int (int_to_isize n)
    
+   [mk_isize_unfold]  Theorem
+      
+      [oracles: DISK_THM] [axioms: isize_bounds] []
+      ⊢ ∀n. mk_isize n =
+            if
+              (i16_min ≤ n ∨ isize_min ≤ n) ∧ (n ≤ i16_max ∨ n ≤ isize_max)
+            then
+              Return (int_to_isize n)
+            else Fail Failure
+   
+   [mk_usize_unfold]  Theorem
+      
+      [oracles: DISK_THM] [axioms: usize_bounds] []
+      ⊢ ∀n. mk_usize n =
+            if 0 ≤ n ∧ (n ≤ u16_max ∨ n ≤ usize_max) then
+              Return (int_to_usize n)
+            else Fail Failure
+   
    [mk_vec_unfold]  Theorem
       
       [oracles: DISK_THM] [axioms: mk_vec_axiom] []
@@ -1866,6 +1928,11 @@ sig
           ∃z. u128_div x y = Return z ∧
               u128_to_int z = u128_to_int x / u128_to_int y
    
+   [u128_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u128_u128_to_int] []
+      ⊢ ∀x y. x = y ⇔ u128_to_int x = u128_to_int y
+   
    [u128_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1923,6 +1990,11 @@ sig
           ∃z. u16_div x y = Return z ∧
               u16_to_int z = u16_to_int x / u16_to_int y
    
+   [u16_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u16_u16_to_int] []
+      ⊢ ∀x y. x = y ⇔ u16_to_int x = u16_to_int y
+   
    [u16_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -1980,6 +2052,11 @@ sig
           ∃z. u32_div x y = Return z ∧
               u32_to_int z = u32_to_int x / u32_to_int y
    
+   [u32_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u32_u32_to_int] []
+      ⊢ ∀x y. x = y ⇔ u32_to_int x = u32_to_int y
+   
    [u32_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -2037,6 +2114,11 @@ sig
           ∃z. u64_div x y = Return z ∧
               u64_to_int z = u64_to_int x / u64_to_int y
    
+   [u64_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u64_u64_to_int] []
+      ⊢ ∀x y. x = y ⇔ u64_to_int x = u64_to_int y
+   
    [u64_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -2094,6 +2176,11 @@ sig
           ∃z. u8_div x y = Return z ∧
               u8_to_int z = u8_to_int x / u8_to_int y
    
+   [u8_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_u8_u8_to_int] []
+      ⊢ ∀x y. x = y ⇔ u8_to_int x = u8_to_int y
+   
    [u8_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -2164,6 +2251,11 @@ sig
           ∃z. usize_div x y = Return z ∧
               usize_to_int z = usize_to_int x / usize_to_int y
    
+   [usize_eq_equiv]  Theorem
+      
+      [oracles: DISK_THM] [axioms: int_to_usize_usize_to_int] []
+      ⊢ ∀x y. x = y ⇔ usize_to_int x = usize_to_int y
+   
    [usize_mul_eq]  Theorem
       
       [oracles: DISK_THM]
@@ -2207,7 +2299,8 @@ sig
       
       [oracles: DISK_THM]
       [axioms: vec_to_list_num_bounds, usize_bounds,
-       usize_to_int_int_to_usize, usize_to_int_bounds, mk_vec_axiom] []
+       int_to_usize_usize_to_int, usize_to_int_bounds,
+       usize_to_int_int_to_usize, mk_vec_axiom] []
       ⊢ ∀v i x.
           usize_to_int i < usize_to_int (vec_len v) ⇒
           ∃nv.
@@ -2219,7 +2312,9 @@ sig
    
    [vec_len_spec]  Theorem
       
-      [oracles: DISK_THM] [axioms: usize_bounds, vec_to_list_num_bounds] []
+      [oracles: DISK_THM]
+      [axioms: int_to_usize_usize_to_int, usize_bounds,
+       vec_to_list_num_bounds] []
       ⊢ ∀v. vec_len v = int_to_usize (len (vec_to_list v)) ∧
             0 ≤ len (vec_to_list v) ∧ len (vec_to_list v) ≤ usize_max
    
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 2f1898b3..7e4aeab4 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -2241,7 +2241,33 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
 
 and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (e : texpression) : unit =
-  let lets, next_e = destruct_lets e in
+  (* Destruct the lets.
+
+     Note that in the case of HOL4, we stop destructing the lets if at some point
+     the "kind" (monadic or non-monadic) of the lets changes.
+
+     We do this because in HOL4 the parsing is not very powerful:
+     if we mix monadic let-bindings and non monadic let-bindings, we have to
+     wrap the let-bindings inside a [do ... od] whenever we need to extract
+     a monadic let-binding non immediately inside a monadic let-binding.
+
+     Ex.:
+     {[
+       do
+         x <- ...;
+         let y = f x in
+         do
+           z <- g y;
+           ...
+         od
+       od
+     ]}
+  *)
+  let lets, next_e =
+    match !backend with
+    | HOL4 -> destruct_lets_no_interleave e
+    | FStar | Coq | Lean -> destruct_lets e
+  in
   (* Open a box for the whole expression.
 
      In the case of Lean, we use a vbox so that line breaks are inserted
@@ -2325,10 +2351,21 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (* Return *)
     ctx
   in
-  let exists_monadic = List.exists (fun (m, _, _) -> m) lets in
   (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box
      immediately *)
-  if (!backend = Lean || !backend = HOL4) && exists_monadic then (
+  let wrap_in_do_od =
+    match !backend with
+    | Lean ->
+        (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *)
+        List.exists (fun (m, _, _) -> m) lets
+    | HOL4 ->
+        (* HOL4 is similar to HOL4, but we add a sanity check *)
+        let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in
+        if wrap_in_do then assert (List.for_all (fun (m, _, _) -> m) lets);
+        wrap_in_do
+    | FStar | Coq -> false
+  in
+  if wrap_in_do_od then (
     F.pp_open_vbox fmt (if !backend = Lean then ctx.indent_incr else 0);
     F.pp_print_string fmt "do";
     F.pp_print_space fmt ());
@@ -2345,7 +2382,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   F.pp_close_box fmt ();
 
   (* do-box (Lean and HOL4 only) *)
-  if (!backend = Lean || !backend = HOL4) && exists_monadic then (
+  if wrap_in_do_od then (
     if !backend = HOL4 then (
       F.pp_print_space fmt ();
       F.pp_print_string fmt "od");
@@ -2512,17 +2549,45 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
   else (
     F.pp_open_hvbox fmt 0;
     F.pp_open_hvbox fmt ctx.indent_incr;
-    let lb, rb =
+    (* Inner/outer brackets: there are several syntaxes for the field updates.
+
+       For instance, in F*:
+       {[
+         { x with f = ..., ... }
+       ]}
+
+       In HOL4:
+       {[
+         x with <| f = ..., ... |>
+       ]}
+
+       In the above examples:
+       - in F*, the { } brackets are "outer" brackets
+       - in HOL4, the <| |> brackets are "inner" brackets
+    *)
+    (* Outer brackets *)
+    let olb, orb =
       match !backend with
       | Lean | FStar -> (Some "{", Some "}")
       | Coq -> (Some "{|", Some "|}")
       | HOL4 -> (None, None)
     in
-    (match lb with
-    | Some lb ->
-        F.pp_print_string fmt lb;
-        F.pp_print_space fmt ()
-    | None -> ());
+    (* Inner brackets *)
+    let ilb, irb =
+      match !backend with
+      | Lean | FStar | Coq -> (None, None)
+      | HOL4 -> (Some "<|", Some "|>")
+    in
+    (* Helper *)
+    let print_bracket (is_left : bool) b =
+      match b with
+      | Some b ->
+          if not is_left then F.pp_print_space fmt ();
+          F.pp_print_string fmt b;
+          if is_left then F.pp_print_space fmt ()
+      | None -> ()
+    in
+    print_bracket true olb;
     let need_paren = inside && !backend = HOL4 in
     if need_paren then F.pp_print_string fmt "(";
     F.pp_open_hvbox fmt ctx.indent_incr;
@@ -2532,6 +2597,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
       F.pp_print_space fmt ();
       F.pp_print_string fmt "with";
       F.pp_print_space fmt ());
+    print_bracket true ilb;
     F.pp_open_hvbox fmt 0;
     let delimiter =
       match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";"
@@ -2555,14 +2621,11 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter)
         F.pp_close_box fmt ())
       supd.updates;
     F.pp_close_box fmt ();
+    print_bracket false irb;
     F.pp_close_box fmt ();
     F.pp_close_box fmt ();
     if need_paren then F.pp_print_string fmt ")";
-    (match rb with
-    | Some rb ->
-        F.pp_print_space fmt ();
-        F.pp_print_string fmt rb
-    | None -> ());
+    print_bracket false orb;
     F.pp_close_box fmt ())
 
 (** Insert a space, if necessary *)
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index 9b768f3b..647678c1 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -220,6 +220,30 @@ let rec destruct_lets (e : texpression) :
       ((monadic, lv, re) :: lets, last_e)
   | _ -> ([], e)
 
+(** Destruct an expression into a list of nested lets, where there
+    is no interleaving between monadic and non-monadic lets.
+ *)
+let destruct_lets_no_interleave (e : texpression) :
+    (bool * typed_pattern * texpression) list * texpression =
+  (* Find the "kind" of the first let (monadic or non-monadic) *)
+  let m =
+    match e.e with
+    | Let (monadic, _, _, _) -> monadic
+    | _ -> raise (Failure "Unreachable")
+  in
+  (* Destruct the rest *)
+  let rec destruct_lets (e : texpression) :
+      (bool * typed_pattern * texpression) list * texpression =
+    match e.e with
+    | Let (monadic, lv, re, next_e) ->
+        if monadic = m then
+          let lets, last_e = destruct_lets next_e in
+          ((monadic, lv, re) :: lets, last_e)
+        else ([], e)
+    | _ -> ([], e)
+  in
+  destruct_lets e
+
 (** Destruct an [App] expression into an expression and a list of arguments.
 
     We simply destruct the expression as long as it is of the form [App (f, x)].
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 709b54a4..1107a123 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -851,7 +851,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
   (* Close the module *)
   (match !Config.backend with
   | FStar | Lean -> ()
-  | HOL4 -> Printf.fprintf out "val _ = export_theory \"%s\"\n" module_name
+  | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n"
   | Coq -> Printf.fprintf out "End %s .\n" module_name);
 
   (* Some logging *)