B2T2 × LiquidHaskell

[LuKuangChen]

We should finish our LiquidHaskell version at some point.

{-@ LIQUID "--exact-data-con" @-}
{-@ LIQUID "--higherorder"    @-}
{-@ LIQUID "--ple"            @-}

module Blank where

import Prelude hiding (map)
import qualified Data.List as Lists
import qualified Data.Set as Sets

data CellType
    = TString
    | TBool
    | TInt

data CellValue
    = CString String
    | CBool Bool
    | CInt Int

{-@ measure typeOf @-}
typeOf (CString _) = TString
typeOf (CBool _)   = TBool
typeOf (CInt _)    = TInt


{-@
type Cell = (t::CellType, {v:CellValue | typeOf v == t})
@-}

{-@
type Column N = (t::CellType, {xs:[{v:CellValue | typeOf v == t}] | len xs == N})
@-}
type Column = (CellType, [CellValue])


{-@
c1 :: Cell
@-}
c1 = (TString, CString "Hello")


{-@ reflect map @-}
map :: (a -> b) -> [a] -> [b]
map f []       = []
map f (x : xs) = f x : map f xs

{-@ measure elts @-}
elts        :: (Ord a) => [a] -> Sets.Set a
elts []     = Sets.empty
elts (x:xs) = Sets.singleton x `Sets.union` elts xs

{-@ measure unique @-}
unique        :: (Ord a) => [a] -> Bool
unique []     = True
unique (x:xs) = unique xs && not (Sets.member x (elts xs))


{-@
type Row = {xs:[(String, Cell)] | unique (map fst xs)}
@-}

{-@
data Table
    = Table
        { nrows :: Int
        , ncols :: Int
        , namedColumns :: {xs:[(String, Column nrows)] | unique (map fst xs) && len xs == ncols}}
@-}
data Table
    = Table
        { nrows :: Int
        , ncols :: Int
        , namedColumns :: [(String, Column)]}

{-@ r1 :: Row @-}
r1 = [ ("foo", (TString, CString "hello"))
     , ("bar", (TInt, CInt 42)) ]


{-@ t1 :: Table @-}
t1 :: Table
t1 = Table 0 2
        [ ("name", (TString, []))
        , ("age" , (TInt,    [])) ]
t2 :: Table
t2 = Table 3 2
        [ ("name", (TString, [CString "Alice", CString "Bob", CString "Charlotte"]))
        , ("age" , (TInt,    [CInt 1, CInt 1, CInt 2])) ]


{-@ LIQUID "--no-termination" @-}
module Blank where

import Prelude   hiding (head, abs, length, drop)
import Data.List hiding (drop, union)
import Data.Set hiding (elems, fromList, map, drop)

{-@ predicate Set_inter X Y Z  = X = Set_cap Y Z         @-}
{-@ predicate Set_disjoint X Y = Set_inter (Set_empty 0) X Y @-}

{-@ die :: {v:_ | false} -> a @-}
die x   = error x

-- I cannot assign types to table columns correctly
-- The difficult part is in ascribing each row (a list of cell) with
-- the column types (a list of base types).

-- data Type = TBool | TInt | TString deriving (Eq)
-- data Cell = CBool Bool | CInt Int | CString String

-- {-@ measure typeof @-}
-- typeof :: Cell -> Type
-- typeof (CBool _)   = TBool
-- typeof (CInt _)    = TInt
-- typeof (CString _) = TString

-- {-@ measure typesof @-}
-- typesof :: [Cell] -> [Type]
-- typesof [] = []
-- typesof (c : cs) = typeof c : typesof cs

-- {-@ getBool :: {c:Cell | HasType c TBool} -> Bool @-}
-- getBool :: Cell -> Bool
-- getBool (CBool b) = b
-- getBool _         = die "impossible"

{-@ predicate HasType C T = (typeof C == T) @-}

-- don't know how to ascribe a list of cells with a list of types yet
{-@ predicate HasTypes Cs Ts = (typesof Cs == Ts) @-}

{-@ measure elts @-}
elts        :: (Ord a) => [a] -> Set a
elts []     = empty
elts (x:xs) = singleton x `union` elts xs

{-@ measure unique @-}
unique        :: (Ord a) => [a] -> Bool
unique []     = True
unique (x:xs) = unique xs && not (member x (elts xs))

{-@
type ListN a N = {xs:[a] | len xs = N}
@-}

data Table = Table { tableNRows :: Int
                   , tableNCols :: Int
                   , tableColnames :: [String]
                   , tableContent  :: [[String]]}

data Row = Row { rowNCols :: Int
               , rowColnames :: [String]
               , rowContent  :: [String]}


{-@
data Table = Table { tableNRows :: {i:_ | i >= 0}
                   , tableNCols :: {i:_ | i > 0}
                   , tableColnames :: {ss:_ | len ss = tableNCols && unique ss}
                   , tableContent  :: ListN (ListN String tableNCols) tableNRows}
@-}

{-@
data Row = Row { rowNCols :: {i:_ | i > 0}
               , rowColnames :: {ss:_ | len ss = rowNCols && unique ss}
               , rowContent  :: ListN String rowNCols}
@-}


{-@ measure colsOf @-}
colsOf (Table nrows ncols colnames content) = colnames

{-@ measure colsOfRow @-}
colsOfRow (Row ncols colnames content) = colnames


{-@ predicate RowHasExactCols   R C       = colsOfRow R   == C @-}
{-@ predicate HasExactCols T C            = colsOf T == C @-}
{-@ predicate HasExactUnorderedCols T C   = elts (colsOf T) == C @-}
{-@ predicate HasCols  T C  = Set_sub C (elts (colsOf T)) @-}
{-@ predicate HasCol   T S  = Set_mem S (elts (colsOf T)) @-}
{-@ predicate HasNoCol T S  = not (HasCol T S) @-}
{-@ predicate List_mem X Xs = Set_mem X (elts Xs) @-}

-- some good tables
-- It'd be great if I can specify the order of columns, but I cann't find a way
-- to use lists in spec.
{-@
person :: {self:_ | 
    HasExactUnorderedCols self (union (singleton "name") (singleton "age"))
    && length self = 1
    }
@-}
person = Table 1 2 
    ["name", "age"]
    [["Alice", "21"]]

{-@
religIncome :: {self:_ | 
    HasExactUnorderedCols self (union (singleton "religion")
                               (union (singleton "<$10k")
                               (union (singleton "$10-20k")
                               (union (singleton ">$20k") empty))))
    && length self = 0}
@-}
religIncome = Table 0 4
    ["religion", "<$10k", "$10-20k", ">$20k"]
    []
-- some bad tables
duplicatedColnames = Table 2 2 ["name", "name"] [["Alice", "21"]]
wrongNRows = Table 2 2 ["name", "age"] [["Alice", "21"]]
wrongNCols = Table 1 3 ["name", "age"] [["Alice", "21"]]
tooFewColnames = Table 1 2 ["name"] [["Alice", "21"]]
tooFewCells = Table 1 2 ["name", "age"] [["21"]]
tooFewRows = Table 1 2 ["name", "age"] []

{-@ type True  = {v:Bool |     v} @-}
{-@ type False = {v:Bool | not v} @-}

{-@ prop_person_has_name :: True @-}
prop_person_has_name = member "name" (elts $ colsOf person)

{-@ prop_person_has_no_NAME :: False @-}
prop_person_has_no_NAME = member "NAME" (elts $ colsOf person)

{-@ getColumn :: self:Table -> {colname:_ | HasCol self colname} -> [String] @-}
getColumn :: Table -> String -> [String]
getColumn = undefined

test_getColumn = 
    [ getColumn person "name"
    -- tests that should fail
    , getColumn person "NAME"
    ]

{-@
buildColumn :: self:_
            -> {colname:_ | not (HasCol self colname)}
            -> ({row:_    | RowHasExactCols row (colsOf self)}
                -> String)
            -> {output:_ | HasExactCols output (colsOf self)}
@-}
buildColumn :: Table -> String -> (Row -> String) -> Table
buildColumn = undefined

test_buildColumn = 
    [ buildColumn person "home"
    -- tests that should fail
    , buildColumn person "name"
    ]


{-@
selectColumns :: self:Table
              -> {ns:[String]  | unique ns && HasCols self (elts ns)}
              -> {output:Table | colsOf output = ns}
@-}
selectColumns :: Table -> [String] -> Table
selectColumns = undefined

test_selectColumns =
    [ selectColumns person ["age", "name"]
    -- tests that should fail
    , selectColumns person ["name", "name"]
    , selectColumns person ["NAME"]
    ]

{-@
assume (!!) :: x:[a] -> {v:Nat | v < len x} -> a
@-}

-- make sure !! is checking indexes
test_indexing = 
    [ ["foo"] !! 0
    -- tests that should fail
    , [] !! 0 ]
    
    
{-@ measure length @-}
length (Table nrows ncols colnames content) = nrows
    

{-@
rowN :: self:Table -> {i:Int | 0 <= i && i < length self} -> [String]
@-}
rowN :: Table -> Int -> [String]
rowN (Table nrows ncols colnames content) i = content !! i

test_rowN = 
    [ rowN person 0
    -- tests that should fail
    , rowN person 1 ]
    

-- Cannot get it working. Don't know why. The error is obscure.
-- {-@ reflect remv @-}
-- remv :: String -> [String] -> [String]
-- remv x [] = []
-- remv x (y : ys)
--     | x == y    = ys
--     | otherwise = x : (remv x ys)



-- 
{-@
drop :: self:Table
     -> {colname:_ | HasCol self colname}
     -> {output:_  | HasExactUnorderedCols output (Set_dif (elts (colsOf self))
                                                  (Set_sng colname))}
@-}
drop :: Table -> String -> Table
drop = undefined

test_drop =
    [ drop person "name"
    , drop person "age"
    -- tests that should fail
    , drop person "NAME" ]


-- {-@
-- pivotLonger :: self:_
--             -> {cols:[{c:_ | HasCol self c}] | unique cols}
--             -> {namesTo:_  | HasNoCol self namesTo}
--             -> {valuesTo:_ | HasNoCol self valuesTo && namesTo == valuesTo}
--             -> {output:_   | HasExactUnorderedCols output 
--                                 (union (Set_dif (elts (colsOf self))
--                                                 (elts cols))
--                                 (union (Set_sng namesTo)
--                                        (Set_sng valuesTo)))}
-- @-}
{-@
pivotLonger 
    :: self:_
    -> {cols:[{c:_ | HasCol self c}] | unique cols}
    -> {namesTo:_  | HasNoCol self namesTo}
    -> {valuesTo:_ | HasNoCol self valuesTo && namesTo != valuesTo}
    -> {output:_   | HasExactUnorderedCols output (union (Set_dif (elts (colsOf self))
                                                                  (elts cols))
                                                         (union (Set_sng namesTo)
                                                                (Set_sng valuesTo)))}
@-}
pivotLonger :: Table -> [String] -> String -> String -> Table
pivotLonger = undefined


test_pivotTable =
    [ pivotLonger religIncome ["<$10k", "$10-20k", ">$20k"] "income" "count"
    -- tests that should fail
    , pivotLonger religIncome ["<$10k", "$10-20k", ">$20k"] "income" "income"
    , pivotLonger religIncome ["<$10k", "$10-20k", ">$20ok"] "income" "count" ]