Update tests

Author: ineol

lib/flow.sail

@@ -55,26 +55,26 @@ therefore be included in just about every Sail specification.
 
 */
 
-val eq_unit = pure { lean : "BEq.beq", _ : "eq_unit" } : (unit, unit) -> bool(true)
+val eq_unit = pure { lean : "_lean_beq", _ : "eq_unit" } : (unit, unit) -> bool(true)
 function eq_unit(_, _) = true
 
-val eq_bit = pure { lem : "eq", lean : "BEq.beq", _ : "eq_bit" } : (bit, bit) -> bool
+val eq_bit = pure { lem : "eq", lean : "_lean_beq", _ : "eq_bit" } : (bit, bit) -> bool
 
-val not_bool = pure {coq: "negb", lean: "Bool.not", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
+val not_bool = pure {coq: "negb", lean: "_lean_not", _: "not"} : forall ('p : Bool). bool('p) -> bool(not('p))
 /* NB: There are special cases in Sail for effectful uses of and_bool and
    or_bool that are not shown here. */
 
-val and_bool = pure {coq: "andb", lean: "Bool.and", _: "and_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p & 'q)
+val and_bool = pure {coq: "andb", lean: "_lean_and", _: "and_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p & 'q)
 
-val and_bool_no_flow = pure {coq: "andb", lean: "Bool.and", _: "and_bool"} : (bool, bool) -> bool
+val and_bool_no_flow = pure {coq: "andb", lean: "_lean_and", _: "and_bool"} : (bool, bool) -> bool
 
-val or_bool = pure {coq: "orb", lean: "Bool.or", _: "or_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p | 'q)
+val or_bool = pure {coq: "orb", lean: "_lean_or", _: "or_bool"} : forall ('p : Bool) ('q : Bool). (bool('p), bool('q)) -> bool('p | 'q)
 
-val eq_int = pure {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", coq: "Z.eqb", lean: "BEq.beq", _: "eq_int"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm)
+val eq_int = pure {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", coq: "Z.eqb", lean: "_lean_beq", _: "eq_int"} : forall 'n 'm. (int('n), int('m)) -> bool('n == 'm)
 
-val eq_bool = pure {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", coq: "Bool.eqb", lean: "BEq.beq", _: "eq_bool"} : (bool, bool) -> bool
+val eq_bool = pure {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", coq: "Bool.eqb", lean: "_lean_beq", _: "eq_bool"} : (bool, bool) -> bool
 
-val neq_int = pure {lem: "neq", lean: "bne"} : forall 'n 'm. (int('n), int('m)) -> bool('n != 'm)
+val neq_int = pure {lem: "neq", lean: "_lean_bne"} : forall 'n 'm. (int('n), int('m)) -> bool('n != 'm)
 function neq_int (x, y) = not_bool(eq_int(x, y))
 
 val neq_bool : (bool, bool) -> bool

lib/generic_equality.sail

@@ -49,7 +49,7 @@ $define _GENERIC_EQUALITY
 
 $include <flow.sail>
 
-val eq_anything = pure {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", lean: "BEq.beq", _: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
+val eq_anything = pure {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", lean: "_lean_beq", _: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
 
 overload operator == = {eq_anything}
 

lib/string.sail

@@ -52,7 +52,7 @@ $include <arith.sail>
 val eq_string = pure {
    lem: "eq",
    coq: "generic_eq",
-   lean: "BEq.beq",
+   lean: "_lean_beq",
    _: "eq_string"} : (string, string) -> bool
 
 overload operator == = {eq_string}

lib/vector.sail

@@ -60,7 +60,7 @@ val eq_bits = pure {
   interpreter: "eq_list",
   lem: "eq_vec",
   coq: "eq_vec",
-  lean: "BEq.beq",
+  lean: "_lean_beq",
   _: "eq_bits"
 } : forall 'n. (bits('n), bits('n)) -> bool
 
@@ -70,7 +70,7 @@ val neq_bits = pure {
   lem: "neq_vec",
   coq: "neq_vec",
   c: "neq_bits",
-  lean: "bne"
+  lean: "_lean_bne"
 } : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_bits(x, y) = not_bool(eq_bits(x, y))

src/sail_lean_backend/Sail/Sail.lean

@@ -507,6 +507,7 @@ def sail_tlbi [Arch] (_ : Arch.tlb_op) : PreSailM RegisterType c ue Unit := pure
 def sail_translation_start [Arch] (_ : Arch.trans_start) : PreSailM RegisterType c ue Unit := pure ()
 def sail_translation_end [Arch] (_ : Arch.trans_end) : PreSailM RegisterType c ue Unit := pure ()
 def sail_take_exception [Arch] (_ : Arch.fault) : PreSailM RegisterType c ue Unit := pure ()
+def sail_return_exception [Arch] (_ : Arch.pa) : PreSailM RegisterType c ue Unit := pure ()
 
 def cycle_count (_ : Unit) : PreSailM RegisterType c ue Unit :=
   modify fun s => { s with cycleCount := s.cycleCount + 1 }

src/sail_lean_backend/Sail/Specialization.lean

@@ -59,6 +59,7 @@ abbrev sail_tlbi [Arch] (op : Arch.tlb_op) : SailM Unit := PreSail.sail_tlbi op
 abbrev sail_translation_start [Arch] (ts : Arch.trans_start) : SailM Unit := PreSail.sail_translation_start ts
 abbrev sail_translation_end [Arch] (te : Arch.trans_end) : SailM Unit := PreSail.sail_translation_end te
 abbrev sail_take_exception [Arch] (f : Arch.fault) : SailM Unit := PreSail.sail_take_exception f
+abbrev sail_return_exception [Arch] (a : Arch.pa) : SailM Unit := PreSail.sail_return_exception a
 
 abbrev cycle_count (a : Unit) : SailM Unit := PreSail.cycle_count a
 

src/sail_lean_backend/pretty_print_lean.ml

@@ -12,6 +12,8 @@ open Pretty_print_common
 (* Command line options *)
 let opt_extern_types : string list ref = ref []
 
+let opt_line_width : int ref = ref 100
+
 type global_context = {
   effect_info : Effects.side_effect_info;
   fun_args : string list Bindings.t;
@@ -86,7 +88,7 @@ let rec fix_id name =
   match name with
   (* Lean keywords to avoid, to expand as needed *)
   | "_lean_wildcard" -> "_"
-  | "rec" | "def" | "at" -> name ^ "'"
+  | "rec" | "def" | "at" | "alias" | "break" -> name ^ "'"
   | "main" ->
       the_main_function_has_been_seen := true;
       "sail_main"
@@ -592,6 +594,11 @@ let rec doc_implicit_args ?(docs = []) ns ims d_args =
 
 let op_of_id id =
   match id with
+  | Some "_lean_and" -> `Binop "&&"
+  | Some "_lean_or" -> `Binop "||"
+  | Some "_lean_beq" -> `Binop "=="
+  | Some "_lean_bne" -> `Binop "!="
+  | Some "_lean_not" -> `Unop "!"
   | Some "_lean_add" -> `Binop "+"
   | Some "_lean_addi" -> `Binop "+i"
   | Some "_lean_sub" -> `Binop "-"
@@ -609,8 +616,8 @@ let op_of_id id =
   | Some "_lean_ge" -> `Binop "≥b"
   | Some "_lean_le" -> `Binop "≤b"
   | Some "_lean_gt" -> `Binop ">b"
-  | Some "_lean_pow2" -> `Unnop "2 ^"
-  | Some "_lean_pow2i" -> `Unnop "2 ^i"
+  | Some "_lean_pow2" -> `Unop "2 ^"
+  | Some "_lean_pow2i" -> `Unop "2 ^i"
   | _ -> `NotOp
 
 let unnop_of_id id = match id with Some "_lean_pow2" -> Some "2 ^ " | _ -> None
@@ -863,7 +870,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
           let e2 = List.nth d_args 1 in
           let res = e1 ^^ space ^^ string op ^^ space ^^ e2 in
           wrap_with_pure as_monadic (parens res) |> nest 2
-      | `Unnop op ->
+      | `Unop op ->
           let e = List.nth d_args 0 in
           let res = string op ^^ space ^^ e in
           wrap_with_pure as_monadic (parens res) |> nest 2
@@ -1472,5 +1479,5 @@ let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail
       (fun file defs -> print file (separate hardline (remove_empties [opens; defs])))
       imp_funcs_files imp_fundefss
   in
-  print funcs_file (separate hardline (remove_empties ([opens; main_fundefs] @ main_function)));
+  print ~len:!opt_line_width funcs_file (separate hardline (remove_empties ([opens; main_fundefs] @ main_function)));
   !the_main_function_has_been_seen

src/sail_lean_backend/sail_plugin_lean.ml

@@ -110,6 +110,10 @@ let lean_options =
         ),
       "use matchbv in the Lean output"
     );
+    ( Flag.create ~prefix:["lean"] "line_width",
+      Arg.Int (fun n -> Pretty_print_lean.opt_line_width := n),
+      "maximum line length of the generated Lean code"
+    );
     ( Flag.create ~prefix:["lean"] "noncomputable",
       Arg.Unit (fun () -> opt_lean_noncomputable := true),
       "add a 'noncomputable section' at the beginning of the output"

test/lean/SailTinyArm.expected.lean

@@ -510,7 +510,7 @@ open AccessType
 
 /-- Type quantifiers: k_ex5891# : Bool, k_ex5890# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
-  (Bool.not (BEq.beq x y))
+  (! (x == y))
 
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
@@ -548,10 +548,10 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
 
 /-- Type quantifiers: m : Int, n : Int -/
 def fdiv_int (n : Int) (m : Int) : Int :=
-  bif (Bool.and (n <b 0) (m >b 0))
+  bif ((n <b 0) && (m >b 0))
   then ((Int.tdiv (n +i 1) m) -i 1)
   else
-    (bif (Bool.and (n >b 0) (m <b 0))
+    (bif ((n >b 0) && (m <b 0))
     then ((Int.tdiv (n -i 1) m) -i 1)
     else (Int.tdiv n m))
 
@@ -1792,13 +1792,13 @@ def GPRs : (Vector (RegisterRef (BitVec 64)) 31) :=
 
 /-- Type quantifiers: n : Nat, 0 ≤ n ∧ n ≤ 31 -/
 def wX (n : Nat) (value : (BitVec 64)) : SailM Unit := do
-  bif (bne n 31)
+  bif (n != 31)
   then writeRegRef (GetElem?.getElem! GPRs n) value
   else (pure ())
 
 /-- Type quantifiers: n : Nat, 0 ≤ n ∧ n ≤ 31 -/
 def rX (n : Nat) : SailM (BitVec 64) := do
-  bif (bne n 31)
+  bif (n != 31)
   then (reg_deref (GetElem?.getElem! GPRs n))
   else (pure (0x0000000000000000 : (BitVec 64)))
 
@@ -1812,29 +1812,29 @@ def decodeLoadStoreRegister (opc : (BitVec 2)) (Rm : (BitVec 5)) (option_v : (Bi
   let t : reg_index := (BitVec.toNat Rt)
   let n : reg_index := (BitVec.toNat Rn)
   let m : reg_index := (BitVec.toNat Rm)
-  bif (Bool.or (bne option_v (0b011 : (BitVec 3))) (BEq.beq S 1#1))
+  bif ((option_v != (0b011 : (BitVec 3))) || (S == 1#1))
   then none
   else
-    (bif (BEq.beq opc (0b00 : (BitVec 2)))
+    (bif (opc == (0b00 : (BitVec 2)))
     then (some (LoadRegister (t, n, m)))
     else
-      (bif (BEq.beq opc (0b01 : (BitVec 2)))
+      (bif (opc == (0b01 : (BitVec 2)))
       then (some (StoreRegister (t, n, m)))
       else none))
 
 def decodeExclusiveOr (sf : (BitVec 1)) (shift : (BitVec 2)) (N : (BitVec 1)) (Rm : (BitVec 5)) (imm6 : (BitVec 6)) (Rn : (BitVec 5)) (Rd : (BitVec 5)) : (Option ast) :=
   let d : reg_index := (BitVec.toNat Rd)
   let n : reg_index := (BitVec.toNat Rn)
   let m : reg_index := (BitVec.toNat Rm)
-  bif (Bool.and (BEq.beq sf 0#1) (BEq.beq (BitVec.access imm6 5) 1#1))
+  bif ((sf == 0#1) && ((BitVec.access imm6 5) == 1#1))
   then none
   else
-    (bif (bne imm6 (0b000000 : (BitVec 6)))
+    (bif (imm6 != (0b000000 : (BitVec 6)))
     then none
     else (some (ExclusiveOr (d, n, m))))
 
 def decodeDataMemoryBarrier (CRm : (BitVec 4)) : (Option ast) :=
-  bif (bne CRm (0xF : (BitVec 4)))
+  bif (CRm != (0xF : (BitVec 4)))
   then none
   else (some (DataMemoryBarrier ()))
 
@@ -1920,7 +1920,7 @@ def execute_DataMemoryBarrier (_ : Unit) : SailM Unit := do
 /-- Type quantifiers: t : Nat, 0 ≤ t ∧ t ≤ 31 -/
 def execute_CompareAndBranch (t : Nat) (offset : (BitVec 64)) : SailM Unit := do
   let operand ← do (rX t)
-  bif (BEq.beq operand (0x0000000000000000 : (BitVec 64)))
+  bif (operand == (0x0000000000000000 : (BitVec 64)))
   then
     (do
       let base ← do (rPC ())

test/lean/append.expected.lean

@@ -47,7 +47,7 @@ open option
 
 /-- Type quantifiers: k_ex688# : Bool, k_ex687# : Bool -/
 def neq_bool (x : Bool) (y : Bool) : Bool :=
-  (Bool.not (BEq.beq x y))
+  (! (x == y))
 
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
@@ -85,10 +85,10 @@ def _shr_int_general (m : Int) (n : Int) : Int :=
 
 /-- Type quantifiers: m : Int, n : Int -/
 def fdiv_int (n : Int) (m : Int) : Int :=
-  bif (Bool.and (n <b 0) (m >b 0))
+  bif ((n <b 0) && (m >b 0))
   then ((Int.tdiv (n +i 1) m) -i 1)
   else
-    (bif (Bool.and (n >b 0) (m <b 0))
+    (bif ((n >b 0) && (m <b 0))
     then ((Int.tdiv (n -i 1) m) -i 1)
     else (Int.tdiv n m))