0 | module Sqlite3.Parameter

  2 | import public Control.Monad.State

  4 | import Data.Buffer.Indexed

  5 | import Data.ByteString

  6 | import Data.List.Quantifiers

  7 | import Data.Maybe

  8 | import Data.SortedMap

  9 | import Data.String

 11 | import Sqlite3.Cmd

 12 | import Sqlite3.Expr

 13 | import Sqlite3.Marshall

 14 | import Sqlite3.Table

 15 | import Sqlite3.Types

 17 | %default total

 20 | public export

 21 | record Parameter where

 22 |   constructor P

 23 |   name  : String

 24 |   type  : SqliteType

 25 |   value : IdrisType type

 29 | public export

 30 | record ParamST where

 31 |   constructor PS

 32 |   ix   : Nat

 33 |   args : List Parameter

 37 | init : ParamST

 38 | init = PS 0 []

 41 | public export

 42 | 0 ParamStmt : Type

 43 | ParamStmt = State ParamST String

 49 | encOp : String -> Expr s t -> Expr s t -> ParamStmt

 51 | encPrefix : String -> Expr s t -> ParamStmt

 53 | encExprs : SnocList String -> List (Expr s t) -> ParamStmt

 55 | encFun1 : String -> Expr s t -> ParamStmt

 57 | encFun : String -> List (Expr s t) -> ParamStmt

 62 | encodeExprP : Expr s t -> ParamStmt

 63 | encodeExprP (Lit t v)    =

 64 |   state $ \(PS x as) =>

 65 |     let s := ":\{show x}"

 66 |      in (PS (S x) (P s t v :: as), s)

 68 | encodeExprP (Add x y)    = encOp "+" x y

 69 | encodeExprP (Mult x y)   = encOp "*" x y

 70 | encodeExprP (Sub x y)    = encOp "-" x y

 71 | encodeExprP (Div x y)    = encOp "/" x y

 72 | encodeExprP (Mod x y)    = encOp "%" x y

 73 | encodeExprP (Abs y)       = encFun1 "abs" y

 74 | encodeExprP (x < y)      = encOp "<" x y

 75 | encodeExprP (x > y)      = encOp ">" x y

 76 | encodeExprP (x <= y)     = encOp "<=" x y

 77 | encodeExprP (x >= y)     = encOp ">=" x y

 78 | encodeExprP (x == y)     = encOp "==" x y

 79 | encodeExprP (x /= y)     = encOp "!=" x y

 80 | encodeExprP (IS x y)     = encOp "IS" x y

 81 | encodeExprP (IS_NOT x y) = encOp "IS NOT" x y

 82 | encodeExprP (x && y)     = encOp "AND" x y

 83 | encodeExprP (x || y)     = encOp "OR" x y

 84 | encodeExprP (x ++ y)     = encOp "||" x y

 85 | encodeExprP (x .&. y)    = encOp "&" x y

 86 | encodeExprP (x .|. y)    = encOp "|" x y

 87 | encodeExprP (ShiftR x y) = encOp ">>" x y

 88 | encodeExprP (ShiftL x y) = encOp "<<" x y

 89 | encodeExprP (Neg x)      = encPrefix "-" x

 90 | encodeExprP (NOT x)      = encPrefix "NOT" x

 91 | encodeExprP (Raw s)      = pure s

 92 | encodeExprP NULL         = pure "NULL"

 93 | encodeExprP TRUE         = pure "1"

 94 | encodeExprP FALSE        = pure "0"

 95 | encodeExprP (Col c)      = pure c

 96 | encodeExprP (COALESCE xs)     = encFun "coalesce" xs

 97 | encodeExprP (COUNT x)         = encFun1 "count" x

 98 | encodeExprP (AVG x)           = encFun1 "avg" x

 99 | encodeExprP (SUM x)           = encFun1 "sum" x

100 | encodeExprP (MIN x)           = encFun1 "min" x

101 | encodeExprP (MAX x)           = encFun1 "max" x

102 | encodeExprP (GROUP_CONCAT x s) = do

103 |   ex <- encodeExprP x

104 |   pure "group_concat(\{ex}, \{s})"

106 | encodeExprP CURRENT_TIME      = pure "CURRENT_TIME"

107 | encodeExprP CURRENT_DATE      = pure "CURRENT_DATE"

108 | encodeExprP CURRENT_TIMESTAMP = pure "CURRENT_TIMESTAMP"

109 | encodeExprP (LIKE x y)        = encOp "LIKE" x y

110 | encodeExprP (GLOB x y)        = encOp "GLOB" x y

112 | encodeExprP (IN x xs) = do

113 |   s  <- encodeExprP x

114 |   ss <- encExprs [<] xs

115 |   pure "(\{s}) IN (\{ss})"

117 | encOp s x y = do

118 |   sx <- encodeExprP x

119 |   sy <- encodeExprP y

120 |   pure $ "(\{sx} \{s} \{sy})"

122 | encPrefix s x = do

123 |   sx <- encodeExprP x

124 |   pure $ "\{s}(\{sx})"

126 | encExprs sc []      = pure . commaSep id $ sc <>> []

127 | encExprs sc (x::xs) = do

128 |   v <- encodeExprP x

129 |   encExprs (sc :< v) xs

131 | encFun f xs      = do

132 |   exs <- encExprs [<] xs

133 |   pure "\{f}(\{exs})"

135 | encFun1 f x      = do

136 |   ex <- encodeExprP x

137 |   pure "\{f}(\{ex})"

143 | record Constraints where

144 |   constructor CS

145 |   colConstraints : SortedMap String String

146 |   tblConstraints : List String

148 | addCol : Constraints -> (col, constraint : String) -> Constraints

149 | addCol (CS cs ts) n v =

150 |   case lookup n cs of

151 |     Just s  => CS (insert n (s ++ " " ++ v) cs) ts

152 |     Nothing => CS (insert n v cs) ts

154 | addTbl : Constraints -> String -> Constraints

155 | addTbl (CS cs ss) s = CS cs (s::ss)

157 | names : SnocList String -> LAll (TColumn t) ts -> String

158 | names sc []           = commaSep id (sc <>> [])

159 | names sc (TC c :: cs) = names (sc :< c) cs

161 | encodeDflt : Expr s t -> String

162 | encodeDflt x         = "DEFAULT (\{encodeExpr x})"

164 | references : (t : SQLTable) -> LAll (TColumn t) xs -> String

165 | references t cs = "REFERENCES \{t.name} (\{names [<] cs})"

167 | encAction : Action -> String

168 | encAction SET_NULL    = "SET NULL"

169 | encAction SET_DEFAULT = "SET DEFAULT"

170 | encAction CASCADE     = "CASCADE"

171 | encAction RESTRICT    = "RESTRICT"

172 | encAction NO_ACTION   = "NO ACTION"

174 | encEvent : Event -> String

175 | encEvent (ON_UPDATE a) = "ON UPDATE \{encAction a}"

176 | encEvent (ON_DELETE a) = "ON DELETE \{encAction a}"

178 | encEvents : List Event -> String

179 | encEvents [] = ""

180 | encEvents xs = " \{unwords $ map encEvent xs}"

182 | encConstraint : Constraints -> Constraint t -> Constraints

183 | encConstraint y (NOT_NULL $ TC n)      = addCol y n"NOT NULL"

184 | encConstraint y (AUTOINCREMENT $ TC n) = addCol y n "AUTOINCREMENT"

185 | encConstraint y (UNIQUE [TC n])        = addCol y n "UNIQUE"

186 | encConstraint y (PRIMARY_KEY [TC n])   = addCol y n "PRIMARY KEY"

187 | encConstraint y (DEFAULT s expr)       = addCol y s (encodeDflt expr)

188 | encConstraint y (UNIQUE xs)            = addTbl y "UNIQUE (\{names [<] xs})"

189 | encConstraint y (PRIMARY_KEY xs)       = addTbl y "PRIMARY KEY (\{names [<] xs})"

190 | encConstraint y (CHECK x)              = addTbl y "CHECK (\{encodeExpr x})"

191 | encConstraint y (ForeignKey s [p] ys as) = addCol y p.name "\{references s ys}\{encEvents as}"

192 | encConstraint y (ForeignKey s xs  ys as) = addTbl y

193 |   "FOREIGN KEY (\{names [<] xs}) \{references s ys} \{encEvents as}"

195 | ine : Bool -> String

196 | ine True  = "IF NOT EXISTS"

197 | ine False = ""

199 | ie : Bool -> String

200 | ie True  = "IF EXISTS"

201 | ie False = ""

203 | encodeCols : SortedMap String String -> List Column -> List String

204 | encodeCols m = map encodeCol

205 |   where

206 |     encodeCol : Column -> String

207 |     encodeCol (C n t) =

208 |       let constraints := fromMaybe "" (lookup n m)

209 |        in "\{n} \{show t} \{constraints}"

211 | insertCols : SnocList String -> LAll (TColumn t) ts -> String

212 | insertCols sc []         = commaSep id (sc <>> [])

213 | insertCols sc (TC c::cs) = insertCols (sc :< c) cs

215 | exprs : SnocList String -> LAll (Expr s) ts -> ParamStmt

216 | exprs sc []      = pure $ commaSep id (sc <>> [])

217 | exprs sc (c::cs) = do

218 |   s <- encodeExprP c

219 |   exprs (sc :< s) cs

221 | namedExprs : SnocList String -> LAll (NamedExpr s) ts -> ParamStmt

222 | namedExprs sc []      = pure $ commaSep id (sc <>> [])

223 | namedExprs sc (AS c n::cs) = do

224 |   s <- encodeExprP c

225 |   let s2 := if n == "" then s else "\{s} AS \{n}"

226 |   namedExprs (sc :< s2) cs

228 | updateVals : SnocList String -> List (Val t) -> ParamStmt

229 | updateVals sc []        = pure $ commaSep id (sc <>> [])

230 | updateVals sc (x :: xs) = do

231 |   v <- encodeExprP x.val

232 |   updateVals (sc :< "\{x.name} = \{v}") xs

241 | encodeCmd : Cmd t -> ParamStmt

242 | encodeCmd (CreateTable t cs ifNotExists) =

243 |   let CS m ts := foldl encConstraint (CS empty []) cs

244 |       cols    := encodeCols m t.cols

245 |       add     := commaSep id (cols ++ ts)

246 |    in pure "CREATE TABLE \{ine ifNotExists} \{t.name} (\{add});"

247 | encodeCmd (DropTable t ifExists) =

248 |    pure "DROP TABLE \{ie ifExists} \{t.name};"

249 | encodeCmd (INSERT t cs vs) = do

250 |   vstr <- exprs [<] vs

251 |   pure "INSERT INTO \{t.name} (\{insertCols [<] cs}) VALUES (\{vstr});"

252 | encodeCmd (REPLACE t cs vs) = do

253 |   vstr <- exprs [<] vs

254 |   pure "REPLACE INTO \{t.name} (\{insertCols [<] cs}) VALUES (\{vstr});"

255 | encodeCmd (UPDATE t vs wh) = do

256 |   vstr <- updateVals [<] vs

257 |   xstr <- encodeExprP wh

258 |   pure "UPDATE \{t.name} SET \{vstr} WHERE \{xstr};"

259 | encodeCmd (DELETE t wh) = do

260 |   xstr <- encodeExprP wh

261 |   pure "DELETE FROM \{t.name} WHERE \{xstr};"

263 | joinPred : JoinPred s t -> ParamStmt

264 | joinPred (Left u)  = pure "USING (\{commaSep name u})"

265 | joinPred (Right x) = do

266 |   ez <- encodeExprP x

267 |   pure "ON \{ez}"

269 | tbl : SQLTable -> String

270 | tbl (ST n a _) = if n == a then n else "\{n} AS \{a}"

272 | join : Join s t -> ParamStmt

273 | join (JOIN t p) = do

274 |   ep <- joinPred p

275 |   pure "JOIN \{tbl t} \{ep}"

277 | join (OUTER_JOIN t p) = do

278 |   ep <- joinPred p

279 |   pure "LEFT OUTER JOIN \{tbl t} \{ep}"

281 | join (CROSS_JOIN t) = pure "CROSS JOIN \{tbl t}"

282 | join (FROM t)       = pure "FROM \{tbl t}"

284 | encodeFrom : From s -> ParamStmt

285 | encodeFrom [<]      = pure ""

286 | encodeFrom [<x]     = join x

287 | encodeFrom (x :< y) = do

288 |   ef <- encodeFrom x

289 |   ej <- join y

290 |   pure "\{ef} \{ej}"

292 | asc : AscDesc -> String

293 | asc NoAsc = ""

294 | asc Asc   = "Asc"

295 | asc Desc  = "Desc"

297 | collate : Collation t -> String

298 | collate None   = ""

299 | collate NOCASE = "COLLATE NOCASE"

301 | encodeOrderingTerm : OrderingTerm t -> ParamStmt

302 | encodeOrderingTerm (O expr coll a) = do

303 |   ex <- encodeExprP expr

304 |   pure "\{ex} \{collate coll} \{asc a}"

306 | ots : SnocList String -> List (OrderingTerm t) -> ParamStmt

307 | ots ss []      = pure $ commaSep id (ss <>> [])

308 | ots ss (x::xs) = do

309 |   s <- encodeOrderingTerm x

310 |   ots (ss :< s) xs

312 | encodeOrd : String -> List (OrderingTerm t) -> ParamStmt

313 | encodeOrd s [] = pure ""

314 | encodeOrd s xs = do

315 |   str <- ots [<] xs

316 |   pure "\{s} \{str}"

318 | limit : Maybe Nat -> Nat -> String

319 | limit Nothing  0 = ""

320 | limit (Just n) 0 = "LIMIT \{show n}"

321 | limit x n = let lim := maybe "-1" show x in "LIMIT \{lim} OFFSET \{show n}"

323 | encodeHaving : Expr s t -> ParamStmt

324 | encodeHaving TRUE = pure ""

325 | encodeHaving x    = do

326 |   s <- encodeExprP x

327 |   pure "HAVING \{s}"

334 | encodeQuery : Query ts -> ParamStmt

335 | encodeQuery (Q distinct _ from vs where_ having group_by order_by lim off) = do

336 |   vstr <- namedExprs [<] vs

337 |   fstr <- encodeFrom from

338 |   wh   <- encodeExprP where_

339 |   hav  <- encodeHaving having

340 |   grp  <- encodeOrd "GROUP BY" (map ord group_by)

341 |   ord  <- encodeOrd "ORDER BY" order_by

342 |   let rest = "\{vstr} \{fstr} WHERE \{wh} \{grp} \{hav} \{ord} \{limit lim off}"

343 |   pure $ case distinct of

344 |     True  => "SELECT DISTINCT \{rest}"

345 |     False => "SELECT \{rest}"