Open LuKuangChen opened 5 months ago
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" ]
We should finish our LiquidHaskell version at some point.