From 9f8d0b7e903c66a334c1a24f685b5b9320cd14f3 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 30 Oct 2024 13:51:10 -0500
Subject: [PATCH] lean: add support for external calls to
 [Int.add|sub|tdiv|tmod|tmod_positive]

---
 lib/arith.sail                 |  9 ++++++---
 test/lean/extern.expected.lean | 15 +++++++++++++++
 test/lean/extern.sail          | 20 ++++++++++++++++++++
 3 files changed, 41 insertions(+), 3 deletions(-)

diff --git a/lib/arith.sail b/lib/arith.sail
index 8657ed88d..cb3f09a2c 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -54,7 +54,7 @@ $include <flow.sail>
 val add_atom = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", _: "add_int"} : forall 'n 'm.
   (int('n), int('m)) -> int('n + 'm)
 
-val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add", _: "add_int"} : (int, int) -> int
+val add_int = pure {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", coq: "Z.add",lean: "Int.add",  _: "add_int"} : (int, int) -> int
 
 overload operator + = {add_atom, add_int}
 
@@ -63,7 +63,7 @@ overload operator + = {add_atom, add_int}
 val sub_atom = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", _: "sub_int"} : forall 'n 'm.
   (int('n), int('m)) -> int('n - 'm)
 
-val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", _: "sub_int"} : (int, int) -> int
+val sub_int = pure {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", coq: "Z.sub", lean: "Int.sub", _: "sub_int"} : (int, int) -> int
 
 overload operator - = {sub_atom, sub_int}
 
@@ -144,7 +144,8 @@ val tdiv_int = pure {
   interpreter: "tdiv_int",
   lem: "tdiv_int",
   c: "tdiv_int",
-  coq: "Z.quot"
+  coq: "Z.quot",
+  lean: "Int.tdiv"
 } : (int, int) -> int
 
 /*! Remainder for truncating division (has sign of dividend) */
@@ -153,6 +154,7 @@ val _tmod_int = pure {
   interpreter: "tmod_int",
   lem: "tmod_int",
   coq: "Z.rem",
+  lean: "Int.tmod",
   c: "tmod_int"
 } : (int, int) -> int
 
@@ -162,6 +164,7 @@ val _tmod_int_positive = pure {
   interpreter: "tmod_int",
   lem: "tmod_int",
   coq: "Z.rem",
+  lean: "Int.tmod",
   _: "tmod_int"
 } : forall 'n, 'n >= 1. (int, int('n)) -> nat
 
diff --git a/test/lean/extern.expected.lean b/test/lean/extern.expected.lean
index 0ad2a5b0f..2e6cf9d44 100644
--- a/test/lean/extern.expected.lean
+++ b/test/lean/extern.expected.lean
@@ -1,3 +1,18 @@
+def extern_add : Int :=
+  (Int.add 5 4)
+
+def extern_sub : Int :=
+  (Int.sub 5 4)
+
+def extern_tdiv : Int :=
+  (Int.tdiv 5 4)
+
+def extern_tmod : Int :=
+  (Int.tmod 5 4)
+
+def extern_tmod_positive : Int :=
+  (Int.tmod 5 4)
+
 def extern_negate : Int :=
   (Int.neg 5)
 
diff --git a/test/lean/extern.sail b/test/lean/extern.sail
index fe98b2a7e..7c652b388 100644
--- a/test/lean/extern.sail
+++ b/test/lean/extern.sail
@@ -2,6 +2,26 @@ default Order dec
 
 $include <prelude.sail>
 
+function extern_add() -> int = {
+  return add_int(5, 4)
+}
+
+function extern_sub() -> int = {
+  return sub_int(5, 4)
+}
+
+function extern_tdiv() -> int = {
+  return tdiv_int(5, 4)
+}
+
+function extern_tmod() -> int = {
+  return tmod_int(5, 4)
+}
+
+function extern_tmod_positive() -> int = {
+  return _tmod_int_positive(5, 4)
+}
+
 function extern_negate() -> int = {
   return negate_int(5)
 }