lean: add support for external calls to [Int.add|sub|tdiv|tmod|tmod_p…

…ositive]

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
 

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)
 

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