Lean: fix bug removing all fns before an extern fn

src/sail_lean_backend/pretty_print_lean.ml

@@ -867,10 +867,9 @@ let rec doc_defs_rec ctx defs types docdefs =
   | DEF_aux (DEF_fundef fdef, dannot) :: defs' ->
       let env = dannot.env in
       let pp_f =
-        if Env.is_extern (id_of_fundef fdef) env "lean" then empty
+        if Env.is_extern (id_of_fundef fdef) env "lean" then docdefs
         else docdefs ^^ group (doc_fundef ctx fdef) ^/^ hardline
       in
-
       doc_defs_rec ctx defs' types pp_f
   | DEF_aux (DEF_type tdef, _) :: defs' when List.mem (string_of_id (id_of_type_def tdef)) !opt_extern_types ->
       doc_defs_rec ctx defs' types docdefs

test/lean/SailTinyArm.expected.lean

@@ -512,6 +512,10 @@ instance : Arch where
 
 namespace Functions
 
+/-- Type quantifiers: k_ex6347# : Bool, k_ex6346# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/bitfield.expected.lean

@@ -34,6 +34,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex700# : Bool, k_ex699# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/bitvec_operation.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex779# : Bool, k_ex778# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/enum.expected.lean

@@ -26,6 +26,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex717# : Bool, k_ex716# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/errors.expected.lean

@@ -32,6 +32,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex731# : Bool, k_ex730# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/extern.expected.lean

@@ -21,6 +21,75 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex1162# : Bool, k_ex1161# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
+/-- Type quantifiers: x : Int -/
+def __id (x : Int) : Int :=
+  x
+
+/-- Type quantifiers: len : Nat, k_v : Nat, len ≥ 0 ∧ k_v ≥ 0 -/
+def sail_mask (len : Nat) (v : (BitVec k_v)) : (BitVec len) :=
+  if (LE.le len (Sail.BitVec.length v))
+  then (Sail.BitVec.truncate v len)
+  else (Sail.BitVec.zeroExtend v len)
+
+/-- Type quantifiers: n : Nat, n ≥ 0 -/
+def sail_ones (n : Nat) : (BitVec n) :=
+  (Complement.complement (BitVec.zero n))
+
+/-- Type quantifiers: l : Int, i : Int, n : Nat, n ≥ 0 -/
+def slice_mask {n : _} (i : Int) (l : Int) : (BitVec n) :=
+  if (GE.ge l n)
+  then (HShiftLeft.hShiftLeft (sail_ones n) i)
+  else let one : (BitVec n) := (sail_mask n (0b1 : (BitVec 1)))
+       (HShiftLeft.hShiftLeft (HSub.hSub (HShiftLeft.hShiftLeft one l) one) i)
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shl_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftl m n)
+  else (Int.shiftr m (Neg.neg n))
+
+/-- Type quantifiers: n : Int, m : Int -/
+def _shr_int_general (m : Int) (n : Int) : Int :=
+  if (GE.ge n 0)
+  then (Int.shiftr m n)
+  else (Int.shiftl m (Neg.neg n))
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fdiv_int (n : Int) (m : Int) : Int :=
+  if (Bool.and (LT.lt n 0) (GT.gt m 0))
+  then (HSub.hSub (Int.tdiv (HAdd.hAdd n 1) m) 1)
+  else if (Bool.and (GT.gt n 0) (LT.lt m 0))
+       then (HSub.hSub (Int.tdiv (HSub.hSub n 1) m) 1)
+       else (Int.tdiv n m)
+
+/-- Type quantifiers: m : Int, n : Int -/
+def fmod_int (n : Int) (m : Int) : Int :=
+  (HSub.hSub n (HMul.hMul m (fdiv_int n m)))
+
+/-- Type quantifiers: k_a : Type -/
+def is_none (opt : (Option k_a)) : Bool :=
+  match opt with
+  | .some _ => false
+  | none => true
+
+/-- Type quantifiers: k_a : Type -/
+def is_some (opt : (Option k_a)) : Bool :=
+  match opt with
+  | .some _ => true
+  | none => false
+
+/-- Type quantifiers: k_n : Int -/
+def concat_str_bits (str : String) (x : (BitVec k_n)) : String :=
+  (HAppend.hAppend str (BitVec.toHex x))
+
+/-- Type quantifiers: x : Int -/
+def concat_str_dec (str : String) (x : Int) : String :=
+  (HAppend.hAppend str (Int.repr x))
+
 def spc_forwards (_ : Unit) : String :=
   " "
 

test/lean/extern_bitvec.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex699# : Bool, k_ex698# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/implicit.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex789# : Bool, k_ex788# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/ite.expected.lean

@@ -36,6 +36,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex805# : Bool, k_ex804# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/let.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex772# : Bool, k_ex771# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/loop.expected.lean

@@ -32,6 +32,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex1303# : Bool, k_ex1302# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/mapping.expected.lean

@@ -26,6 +26,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex852# : Bool, k_ex851# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/match.expected.lean

@@ -41,6 +41,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex797# : Bool, k_ex796# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/match_bv.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex1669# : Bool, k_ex1668# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/option.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex699# : Bool, k_ex698# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/range.expected.lean

@@ -21,6 +21,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex759# : Bool, k_ex758# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/register_vector.expected.lean

@@ -96,6 +96,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex2434# : Bool, k_ex2433# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/registers.expected.lean

@@ -50,6 +50,10 @@ abbrev SailM := PreSailM RegisterType trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex873# : Bool, k_ex872# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/struct.expected.lean

@@ -38,6 +38,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex760# : Bool, k_ex759# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/struct_of_enum.expected.lean

@@ -30,6 +30,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex705# : Bool, k_ex704# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/typedef.expected.lean

@@ -29,6 +29,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex715# : Bool, k_ex714# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x

test/lean/typquant.expected.lean

@@ -27,6 +27,10 @@ abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource Unit
 
 namespace Functions
 
+/-- Type quantifiers: k_ex737# : Bool, k_ex736# : Bool -/
+def neq_bool (x : Bool) (y : Bool) : Bool :=
+  (Bool.not (BEq.beq x y))
+
 /-- Type quantifiers: x : Int -/
 def __id (x : Int) : Int :=
   x