1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55

@[extern "myAdd"]
opaque myAdd : UInt32 → UInt32 → UInt32

@[extern "wasd"]
opaque wasd : UInt32 → UInt32

namespace Sqlite

private opaque Nonempty : NonemptyType

private def RawConn : Type := Sqlite.Nonempty.type
private def Cursor : Type := Sqlite.Nonempty.type

structure Connection where
  path : String
  conn : RawConn

instance : ToString Connection where
  toString (conn : Connection) := s!"Connection({conn.path})"

inductive Result where
  | ok : Result
  | rows (c : Cursor) : Result
  | error (e : String) : Result

@[extern "lean_sqlite_initialize"]
private opaque initSqlite : IO Unit
builtin_initialize initSqlite

@[extern "lean_sqlite_open"]
private opaque openSqlite : String → IO RawConn

@[extern "lean_sqlite_exec"]
private opaque execSqlite : @&RawConn → String → IO Result

@[extern "lean_sqlite_step"]
private opaque stepSqlite : @&Cursor → IO (Option (Array String))

@[extern "lean_sqlite_reset_cursor"]
private opaque resetCursorSqlite : @&Cursor → IO Unit

def connect (s : String) : IO Connection := do
  let rawconn ← openSqlite s
  pure { path := s, conn := rawconn }

def exec (c : Connection) (query : String) : IO Result :=
  execSqlite c.conn query

def step (c : Cursor) : IO (Option (Array String)) :=
  stepSqlite c

def reset (c : Cursor) : IO Unit :=
  resetCursorSqlite c

end Sqlite