liquidhaskell-0.4.0.0: tests/pos/DataBase.hs

module DataBase where

data Rec s v = R (s -> v)
type DBRec = Rec String Value

get :: String -> DBRec -> Value 
get i (R a) = a i

set :: String -> Value -> DBRec -> DBRec
set i x (R a) = R $ \k -> if k == i then x else a k

{-@ empty :: Rec {v:String|0=1} {v : DataBase.Value | v = DataBase.BOT} @-}
empty :: Rec String Value
empty = R $ const BOT

data Value = BOT
           | INT Int 
           | BOOL Bool 
           | STRING String
--            | VEC Value Int


append a1 a2 = \k -> case a1 k of 
                     BOT -> a2 k
                     v   -> v