module ORM where
{-@ LIQUID "--exactdc" @-}
{-@ LIQUID "--totality" @-}
{-@ LIQUID "--higherorder" @-}
import Prelude hiding (length, filter)
import Language.Haskell.Liquid.ProofCombinators
-- here is a "user" query
{-@ prop :: L Row -> L {v:Row | rowLeft v == 5} @-}
prop :: L Row -> L Row
prop xs = mapCast evalQProp $ filter (evalQ (Qry Eq Fst (Const 5))) xs
{-@ prop0 :: L Row -> L {v:Row | evalQ (Qry Eq Fst (Const 5)) v} @-}
prop0 :: L Row -> L Row
prop0 xs = filter (evalQ (Qry Eq Fst (Const 5))) xs
{-@ mapCast :: (x:Row -> {evalQ (Qry Eq Fst (Const 5)) x <=> rowLeft x == 5})
-> L {v:Row | evalQ (Qry Eq Fst (Const 5)) v}
-> L {v:Row | rowLeft v == 5} @-}
mapCast :: (Row -> Proof) -> L Row -> L Row
mapCast _ N = N
mapCast p (C x xs) = cast (p x) x `C` mapCast p xs
evalQProp :: Row -> Proof
{-@ evalQProp :: x:Row -> {evalQ (Qry Eq Fst (Const 5)) x <=> rowLeft x == 5} @-}
evalQProp (Row l r)
= evalQ (Qry Eq Fst (Const 5)) (Row l r)
==. evalC Eq (evalV Fst (Row l r)) (evalV (Const 5) (Row l r))
==. evalC Eq l 5
==. l == 5
*** QED
-- here is the DB API (will add more detail later but its pretty self contained)
data Cmp = Eq | Ne
{-@ data Cmp = Eq | Ne @-}
data Val = Const {valConst :: Int} | Fst | Snd
{-@ data Val = Const {valConst :: Int} | Fst | Snd @-}
data Qry = Qry {qryCmp :: Cmp, qryLHS :: Val, qryRHS :: Val }
{-@ data Qry = Qry {qryCmp :: Cmp, qryLHS :: Val, qryRHS :: Val } @-}
data Row = Row {rowLeft :: Int, rowRigth :: Int}
{-@ data Row = Row {rowLeft :: Int, rowRigth :: Int} @-}
data L a = N | C {hd :: a, tl :: L a}
{-@ data L [length] a = N | C {hd :: a, tl :: L a} @-}
length :: L a -> Int
{-@ length :: L a -> Nat @-}
{-@ measure length @-}
length N = 0
length (C _ xs) = 1 + length xs
------------------------------------------------------------------------
{-@ reflect evalQ @-}
evalQ :: Qry -> Row -> Bool
evalQ (Qry o v1 v2) r = evalC o (evalV v1 r) (evalV v2 r)
{-@ reflect evalV @-}
evalV :: Val -> Row -> Int
evalV (Const n) _ = n
evalV Fst (Row l _) = l
evalV Snd (Row _ r) = r
{-@ reflect evalC @-}
evalC :: Cmp -> Int -> Int -> Bool
evalC Eq x y = x == y
evalC Ne x y = x /= y
{-@ reflect filterQ @-}
filterQ :: Qry -> L Row -> L Row
filterQ qry xs = filter (evalQ qry) xs
{-@ reflect filter @-}
{-@ filter :: forall <p :: a -> Bool, w :: a -> Bool -> Bool>.
{x::a , b::{v:Bool<w x> | v} |- {v:a | v == x} <: a<p> }
(x:a -> Bool<w x>) -> L a -> L (a<p>)
@-}
filter :: (a -> Bool) -> L a -> L a
filter _ N = N
filter p (C x xs)
| p x = x `C` filter p xs
| otherwise = filter p xs