sail-to-lean: Add lean backends for mapping.sail (#969)

Add lean backends for mapping.sail. The following functions now have lean counterparts:

    string_take
    string_drop
    string_length
    string_append
    string_startswith

lib/generic_equality.sail

@@ -49,11 +49,11 @@ $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: "Eq", _: "eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
 
 overload operator == = {eq_anything}
 
-val neq_anything = pure {lem: "neq", lean: "bneq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
+val neq_anything = pure {lem: "neq", lean: "Ne", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool
 
 function neq_anything(x, y) = not_bool(eq_anything(x, y))
 

lib/mapping.sail

@@ -51,17 +51,34 @@ $include <arith.sail>
 $include <option.sail>
 
 $[sv_function { types = "int #1" }]
-val string_take = pure "string_take" : (string, nat) -> string
+val string_take = pure {
+  lean: "String.take",
+  _: "string_take"
+}: (string, nat) -> string
 
 $[sv_function { types = "int #1" }]
-val string_drop = pure "string_drop" : (string, nat) -> string
+val string_drop = pure {
+  lean: "String.drop",
+  _: "string_drop"
+}: (string, nat) -> string
 
 $[sv_function { return_type = "int" }]
-val string_length = pure "string_length" : string -> nat
-
-val string_append = pure {coq: "String.append", c: "concat_str", _: "string_append"} : (string, string) -> string
-
-val string_startswith = pure "string_startswith" : (string, string) -> bool
+val string_length = pure {
+  lean: "String.length",
+  _: "string_length"
+}: string -> nat
+
+val string_append = pure {
+  coq: "String.append",
+  lean: "String.append",
+  c: "concat_str",
+  _: "string_append"
+} : (string, string) -> string
+
+val string_startswith = pure {
+  lean: "String.startsWith",
+  _: "string_startswith"
+}: (string, string) -> bool
 
 val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat
 function n_leading_spaces s =

src/sail_lean_backend/pretty_print_lean.ml

@@ -214,6 +214,7 @@ and doc_typ ctx (Typ_aux (t, _) as typ) =
       nest 2 (parens (flow space [string "Vector"; doc_typ ctx elem_typ; doc_nexp ctx m]))
   | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
   | Typ_id (Id_aux (Id "int", _)) -> string "Int"
+  | Typ_id (Id_aux (Id "string", _)) -> string "String"
   | Typ_app (Id_aux (Id "atom_bool", _), _) | Typ_id (Id_aux (Id "bool", _)) -> string "Bool"
   | Typ_id (Id_aux (Id "bit", _)) -> parens (string "BitVec 1")
   | Typ_id (Id_aux (Id "nat", _)) -> string "Nat"

test/lean/extern.expected.lean

@@ -94,11 +94,26 @@ def extern_gt_int (_ : Unit) : Bool :=
   (GT.gt 5 4)
 
 def extern_eq_anything (_ : Unit) : Bool :=
-  (BEq.beq true true)
+  (Eq true true)
 
 def extern_vector_update (_ : Unit) : (Vector Int 5) :=
   (vectorUpdate #v[23, 23, 23, 23, 23] 2 42)
 
+def extern_string_take (_ : Unit) : String :=
+  (String.take "Hello, world" 5)
+
+def extern_string_drop (_ : Unit) : String :=
+  (String.drop "Hello, world" 5)
+
+def extern_string_length (_ : Unit) : Int :=
+  (String.length "Hello, world")
+
+def extern_string_append (_ : Unit) : String :=
+  (String.append "Hello, " "world")
+
+def extern_string_startswith (_ : Unit) : Bool :=
+  (String.startsWith "Hello, world" "Hello")
+
 def initialize_registers (_ : Unit) : Unit :=
   ()
 

test/lean/extern.sail

@@ -2,6 +2,7 @@ default Order dec
 
 $include <prelude.sail>
 $include <generic_equality.sail>
+$include <mapping.sail>
 
 /* Testing arith.sail */
 
@@ -134,3 +135,24 @@ function extern_vector_update() -> vector(5, dec, int) = {
   vector_update([23, 23, 23, 23, 23], 2, 42)
 }
 
+/* Testing mapping.sail */
+
+function extern_string_take() -> string = {
+  return string_take("Hello, world", 5)
+}
+
+function extern_string_drop() -> string = {
+  return string_drop("Hello, world", 5)
+}
+
+function extern_string_length() -> int = {
+  return string_length("Hello, world")
+}
+
+function extern_string_append() -> string = {
+  return string_append("Hello, ", "world")
+}
+
+function extern_string_startswith() -> bool = {
+  return string_startswith("Hello, world", "Hello")
+}