T1424A.hs

{-# LANGUAGE GADTs #-}

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}

module Gadt where


-- Placeholder for Data.Persistent's Filter type
data Filter a = Filter

{-@ data RefinedFilter record <r :: record -> Bool, q :: record -> User -> Bool> = RefinedFilter (Filter record) @-}
data RefinedFilter record = RefinedFilter (Filter record)

{-@
data User = User
     { userId   :: Int,
       userName :: String
     , userFriend :: Int
     , userSSN    :: Int
     }
@-}
data User = User { userId::Int, userName :: String, userFriend :: Int, userSSN :: Int }
    deriving (Eq, Show)

{-@
data EntityField record typ where
   UserName :: EntityField User String
   UserFriend :: EntityField User Int
   UserSSN :: EntityField  User Int
@-}
data EntityField a b where
  UserName :: EntityField User String
  UserFriend :: EntityField User Int
  UserSSN :: EntityField User Int

{-@ reflect policy @-}
policy :: EntityField a b -> a -> User -> Bool
policy UserName row v = userId v == userFriend row
policy UserFriend row v = userId v == userFriend row
policy UserSSN row v = userId v == userId row

{-@ reflect project @-}
project :: EntityField a b -> a -> b
project UserName user = userName user
project UserFriend user = userFriend user
project UserSSN user = userSSN user

{-@
(==.) :: field:EntityField a b -> val:b -> RefinedFilter<{\row -> project field row == val}, {\row v -> policy field row v}> a
@-}
(==.) :: EntityField a b -> b -> RefinedFilter a
field ==. val = RefinedFilter Filter