mirror of
https://github.com/ilyakooo0/IdrisSqlite.git
synced 2024-11-20 18:39:11 +03:00
72 lines
2.3 KiB
Idris
72 lines
2.3 KiB
Idris
module SQLiteTypes
|
|
|
|
import Decidable.Equality
|
|
|
|
%default total
|
|
|
|
|
|
public export data SQLiteType = TEXT | INTEGER | REAL
|
|
| NULLABLE SQLiteType
|
|
|
|
public export interpSql : SQLiteType -> Type
|
|
interpSql TEXT = String
|
|
interpSql INTEGER = Integer
|
|
interpSql REAL = Double
|
|
interpSql (NULLABLE x) = Maybe (interpSql x)
|
|
|
|
equalSql : (t : SQLiteType) -> (x, y : interpSql t) -> Bool
|
|
equalSql TEXT x y = x == y
|
|
equalSql INTEGER x y = x == y
|
|
equalSql REAL x y = x == y
|
|
equalSql (NULLABLE ty) (Just x) (Just y) = equalSql ty x y
|
|
equalSql (NULLABLE ty) Nothing Nothing = True
|
|
equalSql (NULLABLE ty) _ _ = False
|
|
|
|
export showSql : (t : SQLiteType) -> (x : interpSql t) -> String
|
|
showSql TEXT x = show x
|
|
showSql INTEGER x = show x
|
|
showSql REAL x = show x
|
|
showSql (NULLABLE ty) (Just x) = showSql ty x
|
|
showSql (NULLABLE ty) Nothing = "null"
|
|
|
|
|
|
integerNotText : INTEGER = TEXT -> Void
|
|
integerNotText Refl impossible
|
|
|
|
realNotText : REAL = TEXT -> Void
|
|
realNotText Refl impossible
|
|
|
|
nullableNotText : NULLABLE t = TEXT -> Void
|
|
nullableNotText Refl impossible
|
|
|
|
realNotInteger : REAL = INTEGER -> Void
|
|
realNotInteger Refl impossible
|
|
|
|
nullableNotInteger : NULLABLE t = INTEGER -> Void
|
|
nullableNotInteger Refl impossible
|
|
|
|
nullableNotReal : NULLABLE t = REAL -> Void
|
|
nullableNotReal Refl impossible
|
|
|
|
export implementation DecEq SQLiteType where
|
|
decEq TEXT TEXT = Yes Refl
|
|
decEq INTEGER TEXT = No integerNotText
|
|
decEq REAL TEXT = No realNotText
|
|
decEq (NULLABLE x) TEXT = No nullableNotText
|
|
decEq TEXT INTEGER = No $ integerNotText . sym
|
|
decEq INTEGER INTEGER = Yes Refl
|
|
decEq REAL INTEGER = No realNotInteger
|
|
decEq (NULLABLE x) INTEGER = No nullableNotInteger
|
|
decEq TEXT REAL = No $ realNotText . sym
|
|
decEq INTEGER REAL = No $ realNotInteger . sym
|
|
decEq REAL REAL = Yes Refl
|
|
decEq (NULLABLE x) REAL = No nullableNotReal
|
|
decEq TEXT (NULLABLE x) = No $ nullableNotText . sym
|
|
decEq INTEGER (NULLABLE x) = No $ nullableNotInteger . sym
|
|
decEq REAL (NULLABLE x) = No $ nullableNotReal . sym
|
|
decEq (NULLABLE y) (NULLABLE x) with (decEq y x)
|
|
decEq (NULLABLE x) (NULLABLE x) | (Yes Refl) = Yes Refl
|
|
decEq (NULLABLE y) (NULLABLE x) | (No prf) = No $ prf . inside
|
|
where inside : NULLABLE a = NULLABLE b -> a = b
|
|
inside Refl = Refl
|