add more annotation, fix omitted fundefs

lib/generic_equality.sail

@@ -53,9 +53,12 @@ val eq_anything = pure {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic
 
 overload operator == = {eq_anything}
 
-val neq_anything = pure {lem: "neq", lean: "Ne", 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))
+function neq_anything(x, y) = not_bool(eq_anything(y, x))
 
 overload operator != = {neq_anything}
 

lib/mapping.sail

@@ -80,7 +80,7 @@ val string_startswith = pure {
   _: "string_startswith"
 }: (string, string) -> bool
 
-val n_leading_spaces = pure { coq: "n_leading_spaces_Z" } : string -> nat
+val n_leading_spaces = pure { coq: "n_leading_spaces_Z", lean: "String.leadingSpaces" } : string -> nat
 function n_leading_spaces s =
   match s {
     "" => 0,

lib/string.sail

@@ -49,19 +49,31 @@ $define _STRING
 
 $include <arith.sail>
 
-val eq_string = pure {lem: "eq", coq: "generic_eq", _: "eq_string"} : (string, string) -> bool
+val eq_string = pure {
+   lem: "eq",
+   coq: "generic_eq",
+   lean: "Eq",
+   _: "eq_string"} : (string, string) -> bool
 
 overload operator == = {eq_string}
 
-val concat_str = pure {coq: "String.append", lem: "stringAppend", _: "concat_str"} : (string, string) -> string
+val concat_str = pure {
+   coq: "String.append",
+   lem: "stringAppend",
+   lean: "HAppend.hAppend",
+   _: "concat_str"} : (string, string) -> string
 
-val dec_str = pure "dec_str" : int -> string
+val dec_str = pure {
+  lean: "Int.repr",
+  _: "dec_str"} : int -> string
 
 val hex_str = pure "hex_str" : int -> string
 
 val hex_str_upper = pure "hex_str_upper" : int -> string
 
-val bits_str = pure "string_of_bits" : forall 'n. bitvector('n, dec) -> string
+val bits_str = pure {
+   lean: "BitVec.toHex",
+   _: "string_of_bits"} : forall 'n. bitvector('n, dec) -> string
 
 val concat_str_bits : forall 'n. (string, bitvector('n, dec)) -> string
 

lib/vector.sail

@@ -342,16 +342,22 @@ $endif
 
 overload vector_update_subrange = {update_subrange_bits}
 
-val sail_shiftleft = pure "shiftl" : forall 'n ('ord : Order).
+val sail_shiftleft = pure {
+  lean: "HShiftLeft.hShiftLeft",
+  _: "shiftl"} : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
-val sail_shiftright = pure "shiftr" : forall 'n ('ord : Order).
+val sail_shiftright = pure {
+  lean: "HShiftRight.hShiftRight",
+  _: "shiftr"} : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
 val sail_arith_shiftright = pure "arith_shiftr" : forall 'n ('ord : Order).
     (bitvector('n, 'ord), int) -> bitvector('n, 'ord)
 
-val sail_zeros = pure "zeros" : forall 'n, 'n >= 0. int('n) -> bits('n)
+val sail_zeros = pure {
+  lean: "BitVec.zero",
+  _: "zeros" }: forall 'n, 'n >= 0. int('n) -> bits('n)
 
 val sail_ones : forall 'n, 'n >= 0. int('n) -> bits('n)
 

src/sail_lean_backend/Sail/Sail.lean

@@ -346,4 +346,18 @@ def shiftr (a : Int) (n : Int) : Int :=
   | Int.negSucc n => Sail.Nat.iterate (fun x => x * 2) (n+1) a
 
 end Int
+
+def String.leadingSpaces (s : String) : Nat :=
+  s.length - (s.dropWhile (· = ' ')).length
+
+
+instance : HShiftLeft (BitVec w) Int (BitVec w) where
+  hShiftLeft b i :=
+    match i with
+    | .ofNat n => BitVec.shiftLeft b n
+    | .negSucc n => BitVec.ushiftRight b n
+
+instance : HShiftRight (BitVec w) Int (BitVec w) where
+  hShiftRight b i := b <<< (-i)
+
 end Sail

src/sail_lean_backend/pretty_print_lean.ml

@@ -236,9 +236,11 @@ and doc_typ ctx (Typ_aux (t, _) as typ) =
       underscore (* TODO check if the type of implicit arguments can really be always inferred *)
   | Typ_app (Id_aux (Id "option", _), [A_aux (A_typ typ, _)]) -> parens (string "Option " ^^ doc_typ ctx typ)
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) (doc_typ ctx) ts)
-  | Typ_id (Id_aux (Id id, _)) -> string id
+  | Typ_id id -> doc_id_ctor id
   | Typ_app (Id_aux (Id "range", _), [A_aux (A_nexp low, _); A_aux (A_nexp high, _)]) ->
       if provably_nneg ctx low then string "Nat" else string "Int"
+  | Typ_app (Id_aux (Id "result", _), [A_aux (A_typ typ1, _); A_aux (A_typ typ2, _)]) ->
+      parens (separate space [string "Result"; doc_typ ctx typ1; doc_typ ctx typ2])
   | Typ_var kid -> doc_kid ctx kid
   | Typ_app (id, args) -> doc_id_ctor id ^^ space ^^ separate_map space (doc_typ_arg ctx `Only_relevant) args
   | Typ_exist (_, _, typ) -> doc_typ ctx typ
@@ -712,7 +714,7 @@ let doc_funcl ctx funcl =
   let comment, signature, ctx, fixup_binders = doc_funcl_init ctx.global funcl in
   comment ^^ nest 2 (signature ^^ hardline ^^ doc_funcl_body fixup_binders ctx funcl)
 
-let doc_fundef ctx (FD_aux (FD_function (r, typa, fcls), fannot)) =
+let doc_fundef ctx (FD_aux (FD_function (r, typa, fcls), fannot) as full_fundef) =
   match fcls with
   | [] -> failwith "FD_function with empty function list"
   | [funcl] -> doc_funcl ctx funcl
@@ -797,8 +799,14 @@ let doc_val ctx pat exp =
 let rec doc_defs_rec ctx defs types docdefs =
   match defs with
   | [] -> (types, docdefs)
-  | DEF_aux (DEF_fundef fdef, _) :: defs' ->
-      doc_defs_rec ctx defs' types (docdefs ^^ group (doc_fundef ctx fdef) ^/^ hardline)
+  | 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
+        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
   | DEF_aux (DEF_type tdef, _) :: defs' ->
@@ -898,7 +906,7 @@ let main_function_stub =
 
 let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
   (* TODO: remove the following line once we can handle the includes *)
-  let defs = remove_imports defs 0 in
+  (* let defs = remove_imports defs 0 in *)
   let regs = State.find_registers defs in
   let global = { effect_info } in
   let ctx = context_init env global in

test/c/hello_world.expected.lean

@@ -3,8 +3,83 @@ import Out.Sail.BitVec
 
 open Sail
 
+abbrev bits k_n := (BitVec k_n)
+
+/-- Type quantifiers: k_a : Type -/
+
+inductive option (k_a : Type) where
+  | Some (_ : k_a)
+  | None (_ : Unit)
+
+open option
+
 abbrev SailM := PreSailM PEmpty.elim trivialChoiceSource
 
+/-- 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 sail_main (_ : Unit) : SailM Unit := do
   (print_endline_effect "Hello, World!")