0 | module Postgres.Data.PostgresType
  1 |
  2 | import Data.List
  3 |
  4 | %default total
  5 |
  6 | -- see src/include/catalog/pg_type.h
  7 |
  8 | --
  9 | -- Oid
 10 | --
 11 |
 12 | ||| Postgres Oids are just integers that have special
 13 | ||| internal semantics within Postgres.
 14 | public export
 15 | data Oid : Type where
 16 |   MkOid : Int -> Oid
 17 |
 18 | Eq Oid where
 19 |   (MkOid x) == (MkOid y) = x == y
 20 |
 21 | Show Oid where
 22 |   show (MkOid oid) = show oid
 23 |
 24 | ||| Get an integer representation of an Oid. Probably only useful
 25 | ||| when actually sending the Oid to Postgres for some reason.
 26 | export
 27 | oidToInt : Oid -> Int
 28 | oidToInt (MkOid x) = x
 29 |
 30 | --
 31 | -- Type
 32 | --
 33 |
 34 | ||| Not an exhaustive list of types, just a short list of
 35 | ||| builtins with explicit support in this library.
 36 | public export
 37 | data PType = PInteger
 38 |            | PDouble
 39 |            | PChar
 40 |            | PBoolean
 41 |            | PDate
 42 |            | PTime
 43 |            | PDatetime
 44 |            | PString
 45 |            | PJson
 46 |            | PUuid
 47 |            | POid
 48 |            | PArray PType
 49 |            | POther String
 50 |            | PUnknown Oid
 51 |
 52 | export
 53 | Show PType where
 54 |   show PInteger   = "Integer"
 55 |   show PDouble    = "Double"
 56 |   show PChar      = "Char"
 57 |   show PBoolean   = "Boolean"
 58 |   show PDate      = "Date"
 59 |   show PTime      = "Time"
 60 |   show PDatetime  = "DateTime"
 61 |   show PString    = "String"
 62 |   show PJson      = "JSON"
 63 |   show PUuid      = "UUID"
 64 |   show POid       = "OID"
 65 |   show (PArray t) = (show t) ++ "[]"
 66 |   show (POther x) = "?" ++ x
 67 |   show (PUnknown (MkOid oid)) = "Oid: " ++ (show oid)
 68 |
 69 | public export
 70 | data Nullability = Nullable | NonNullable
 71 |
 72 | public export
 73 | data PColType : PType -> Type where
 74 |   MkColType : (nullable: Nullability) -> (pt : PType) -> PColType pt
 75 |
 76 | export
 77 | Show (PColType t) where
 78 |   show (MkColType _ x) = show x
 79 |
 80 | public export
 81 | pType : PColType t -> PType
 82 | pType (MkColType _ t) = t
 83 |
 84 | public export
 85 | nullable : PColType t -> Bool
 86 | nullable (MkColType Nullable _) = True
 87 | nullable (MkColType NonNullable _) = False
 88 |
 89 | public export
 90 | makeNullable : PColType t -> PColType t
 91 | makeNullable (MkColType _ t) = MkColType Nullable t
 92 |
 93 | --
 94 | -- Format Code
 95 | --
 96 |
 97 | public export
 98 | data FormatCode = Text | Binary
 99 |
100 | export
101 | Show FormatCode where
102 |   show Text   = "Text"
103 |   show Binary = "Binary"
104 |
105 | --
106 | -- Type Dictionary
107 | --
108 |
109 | export
110 | data TypeDictionary : Type where
111 |   MkTypeDictionary : List (Oid, PType) -> TypeDictionary
112 |
113 | -- The dot accessor makes it like a record type where the
114 | -- following accessor is public but the constructor is not.
115 | ||| A sorted list of type tuples (pairs of Oid and type).
116 | ||| Sorted by Oid.
117 | export
118 | (.types) : TypeDictionary -> List (Oid, PType)
119 | (.types) (MkTypeDictionary xs) = xs
120 |
121 | ||| A sorted list of type tuples (pairs of Oid and type).
122 | ||| Sorted by Oid.
123 | export
124 | types : TypeDictionary -> List (Oid, PType)
125 | types (MkTypeDictionary xs) = xs
126 |
127 | export
128 | empty : TypeDictionary
129 | empty = MkTypeDictionary []
130 |
131 | ||| Create a dictionary of Postgres types. The dictionary is
132 | ||| sorted by Oid for future lookup.
133 | export
134 | typeDictionary : List (Oid, PType) -> TypeDictionary
135 | typeDictionary xs = MkTypeDictionary (sortBy (compare `on` oidToInt . fst) xs)
136 |
137 | ||| Find the Postgres Type the given Oid refers to, or
138 | ||| admit defeat via PUnknown.
139 | export
140 | lookup : Oid -> TypeDictionary -> PType
141 | lookup oid = maybe (PUnknown oid) id . lookup oid . types
142 |
143 | export
144 | Show TypeDictionary where
145 |   show = concat . intersperse "\n" . map showTuple . types
146 |     where
147 |       showTuple : (Oid, PType) -> String
148 |       showTuple (oid, type) = (show oid) ++ ": " ++ (show type)
149 |
150 |