Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
module SQL
%default total
%access public export
data SqlType = BOOLEAN | INTEGER
mutual
data ColumnExpression : SqlType -> Type where
BooleanLiteral : Bool -> ColumnExpression BOOLEAN
IntegerLiteral : Int -> ColumnExpression INTEGER
SubQueryExpression :
(query : SqlQuery a)
-> { auto prf : QueryHasExactlyOneColumn query }
-> ColumnExpression (getSqlTypeFromQueryWithOneColumn query {prf=prf})
(+) : ColumnExpression INTEGER -> ColumnExpression INTEGER -> ColumnExpression INTEGER
(-) : ColumnExpression INTEGER -> ColumnExpression INTEGER -> ColumnExpression INTEGER
AnyColumnExpression' : Type
AnyColumnExpression' = (sqlType ** ColumnExpression sqlType)
data SqlQuery : (result : Type) -> Type where
SelectColumn : AnyColumnExpression' -> SqlQuery ()
Where : ColumnExpression BOOLEAN -> SqlQuery ()
(>>=) : SqlQuery a -> (a -> SqlQuery b) -> SqlQuery b
namespace QueryHasExactlyOneColumn
data QueryHasNoColumns : (query : SqlQuery a) -> Type where
OkToStartWithWhere : QueryHasNoColumns (Where boolExpression)
OkToAppendWhereNoCols :
{a : Type}
-> {query : SqlQuery a}
-> QueryHasNoColumns query
-> QueryHasNoColumns (do query; Where boolExpression)
data QueryHasExactlyOneColumn : (query : SqlQuery a) -> Type where
Start : QueryHasExactlyOneColumn (SelectColumn (sqlType ** columnExpression))
OkToAppendWhere :
{a : Type}
-> {query : SqlQuery a}
-> QueryHasExactlyOneColumn query
-> QueryHasExactlyOneColumn (do query; Where boolExpression)
OkToAppendSelectToQueryWOColumns :
{sqlType : SqlType}
-> {a : Type}
-> {query : SqlQuery a}
-> QueryHasNoColumns query
-> QueryHasExactlyOneColumn (do query; SelectColumn (sqlType ** columnExpression))
getSqlTypeFromQueryWithOneColumn : (query : SqlQuery a) -> { auto prf : QueryHasExactlyOneColumn query } -> SqlType
getSqlTypeFromQueryWithOneColumn query {prf} = (
case prf of
Start {sqlType} => sqlType
(OkToAppendWhere {query} prf') => getSqlTypeFromQueryWithOneColumn query {prf=prf'}
(OkToAppendSelectToQueryWOColumns {sqlType} prfNoColumns) => sqlType
)
query : SqlQuery ()
query = do
SelectColumn (_ ** IntegerLiteral 11)
Where $ BooleanLiteral True
onlyOne : QueryHasExactlyOneColumn SQL.query
onlyOne = assert_total $ OkToAppendWhere Start
queryType : SqlType
queryType = assert_total $ getSqlTypeFromQueryWithOneColumn query
subQuery : SqlQuery ()
subQuery = assert_total $ do
SelectColumn (_ ** SubQueryExpression (do SelectColumn (_ ** IntegerLiteral 11);))
onlyOne' : QueryHasExactlyOneColumn SQL.subQuery
onlyOne' = Start
{-
Errors (2)
/home/nickolay/workspace/Idris/horn/src/SQL.idr:89:12
Type mismatch between
ColumnExpression (getSqlTypeFromQueryWithOneColumn (SelectColumn (INTEGER **
IntegerLiteral 11)))
and
ColumnExpression INTEGER
/home/nickolay/workspace/Idris/horn/src/SQL.idr:63:5
SQL.getSqlTypeFromQueryWithOneColumn is possibly not total due to: SQL.case block in getSqlTypeFromQueryWithOneColumn at /home/nickolay/workspace/Idris/horn/src/SQL.idr:64:14-16
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment