g2 0.1.0.0 → 0.1.0.1
raw patch · 22 files changed
+1628/−2 lines, 22 files
Files
- g2.cabal +22/−2
- quasiquote/Arithmetics/Interpreter.hs +87/−0
- quasiquote/Arithmetics/Test.hs +83/−0
- quasiquote/DeBruijn/Interpreter.hs +48/−0
- quasiquote/DeBruijn/Test.hs +62/−0
- quasiquote/Evaluations.hs +194/−0
- quasiquote/Lambda/Interpreter.hs +38/−0
- quasiquote/Lambda/Test.hs +19/−0
- quasiquote/NQueens/Encoding.hs +62/−0
- quasiquote/NQueens/Test.hs +19/−0
- quasiquote/RegEx/RegEx.hs +36/−0
- quasiquote/RegEx/Test.hs +25/−0
- tests/CaseTest.hs +24/−0
- tests/DefuncTest.hs +83/−0
- tests/Expr.hs +100/−0
- tests/GetNthTest.hs +101/−0
- tests/HigherOrderMathTest.hs +89/−0
- tests/InputOutputTest.hs +117/−0
- tests/PeanoTest.hs +60/−0
- tests/Reqs.hs +68/−0
- tests/TestUtils.hs +137/−0
- tests/Typing.hs +154/−0
g2.cabal view
@@ -2,7 +2,7 @@ -- see http://haskell.org/cabal/users-guide/ name: g2-version: 0.1.0.0+version: 0.1.0.1 synopsis: Haskell symbolic execution engine. description: A Haskell symbolic execution engine. @@ -193,7 +193,6 @@ main-is: Main.hs executable QuasiQuote- -- other-modules: -- other-extensions: build-depends: g2 , base >= 4.8 && < 5@@ -204,6 +203,17 @@ -- -fprof-auto "-with-rtsopts=-p" hs-source-dirs: quasiquote main-is: Main.hs+ other-modules: Arithmetics.Interpreter+ , Arithmetics.Test+ , DeBruijn.Interpreter+ , DeBruijn.Test+ , Evaluations+ , Lambda.Interpreter+ , Lambda.Test+ , NQueens.Encoding+ , NQueens.Test+ , RegEx.RegEx+ , RegEx.Test test-suite test build-depends: g2@@ -223,6 +233,16 @@ default-language: Haskell2010 hs-source-dirs: tests main-is: Test.hs+ other-modules: CaseTest+ , DefuncTest+ , Expr+ , GetNthTest+ , HigherOrderMathTest+ , InputOutputTest+ , PeanoTest+ , Reqs+ , TestUtils+ , Typing ghc-options: -Wall -- -fprof-auto "-with-rtsopts=-p" -threaded
+ quasiquote/Arithmetics/Interpreter.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module Arithmetics.Interpreter where++import Control.Monad+import Data.Data+import G2.QuasiQuotes.G2Rep++type Ident = String+type Env = [(Ident, Int)]++data AExpr = I Int | Var Ident+ | Add AExpr AExpr | Mul AExpr AExpr+ deriving (Eq, Show, Data)++$(derivingG2Rep ''AExpr)++data BExpr = Not BExpr | And BExpr BExpr | Or BExpr BExpr+ | Lt AExpr AExpr | Eq AExpr AExpr+ deriving (Eq, Show, Data)++$(derivingG2Rep ''BExpr)++type Stmts = [Stmt]+data Stmt = Assign Ident AExpr+ | If BExpr Stmts Stmts+ | While BExpr Stmts+ | Assert BExpr+ deriving (Eq, Show, Data)+ +$(derivingG2Rep ''Stmt)++type Bound = [Ident]+type Return = Ident+data Func = Func Bound Stmts Return++$(derivingG2Rep ''Func)++evalFunc :: [Int] -> Func -> Maybe Int+evalFunc is (Func b s r) =+ lookup r =<< evalStmts (zip b is) s++evalStmts :: Env -> Stmts -> Maybe Env+evalStmts = foldM evalStmt ++evalStmt :: Env -> Stmt -> Maybe Env+evalStmt env (Assign ident aexpr) =+ Just $ (ident, evalA env aexpr):env+evalStmt env (If bexpr lhs rhs) =+ if evalB env bexpr+ then evalStmts env lhs+ else evalStmts env rhs+evalStmt env (While bexpr loop) =+ if evalB env bexpr+ then evalStmts env (loop ++ [While bexpr loop])+ else Just env+evalStmt env (Assert bexpr) =+ if evalB env bexpr+ then Just env+ else Nothing++evalA :: Env -> AExpr -> Int+evalA _ (I int) = int+evalA env (Add lhs rhs) =+ evalA env lhs + evalA env rhs+evalA env (Mul lhs rhs) =+ evalA env lhs * evalA env rhs+evalA env (Var ident) =+ case lookup ident env of+ Just int -> int+ _ -> error $+ "lookup with " ++ show (ident, env)++evalB :: Env -> BExpr -> Bool+evalB env (Not bexpr) = not $ evalB env bexpr+evalB env (And lhs rhs) =+ evalB env lhs && evalB env rhs+evalB env (Or lhs rhs) =+ evalB env lhs || evalB env rhs+evalB env (Lt lhs rhs) =+ evalA env lhs < evalA env rhs+evalB env (Eq lhs rhs) =+ evalA env lhs == evalA env rhs+
+ quasiquote/Arithmetics/Test.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE QuasiQuotes #-}++module Arithmetics.Test where++import Arithmetics.Interpreter+import G2.QuasiQuotes.QuasiQuotes++productTest :: IO (Maybe (AExpr, AExpr))+productTest =+ [g2| \(a :: Int) -> ?(s1 :: AExpr)+ ?(s2 :: AExpr) |+ let env = [("x", 23), ("y", 59)] in+ let lhs = Mul (Var "x") (Var "y") in+ let rhs = Mul s1 s2 in+ evalB env (Eq lhs rhs) |] 0++envTest :: BExpr -> IO (Maybe Env)+envTest = [g2|\(b :: BExpr) -> ?(env :: Env) |+ evalB env b |]++assertViolation :: Stmts -> IO (Maybe Env)+assertViolation = [g2|\(stmts :: Stmts) -> ?(env :: Env) |+ evalStmts env stmts == Nothing|]++productSumTest :: IO (Maybe Env)+productSumTest =+ envTest $ And+ ((Eq + (Mul (Var "x") (Var "y"))+ (Add (Var "x") (Var "y"))))+ (Lt (I 0) (Var "x"))+++assertViolationTest1 :: IO (Maybe Env)+assertViolationTest1 = assertViolation+ [ Assert (Lt (I 5) (I 3)) ]++-- x^2 + y^2 + z^2 < (x + y + z)^2+assertViolationTest2 :: IO (Maybe Env)+assertViolationTest2 = assertViolation+ [ Assign "v1" (Add (Var "x") (Add (Var "y") (Var "z")))+ , Assign "v1" (Mul (Var "v1") (Var "v1"))+ , Assign "v2" (Add (Mul (Var "x") (Var "x"))+ (Add (Mul (Var "y") (Var "y"))+ (Mul (Var "z") (Var "z"))))+ , Assert (Lt (Var "v2") (Var "v1"))+ ]+++assertViolationTest3 :: IO (Maybe Env)+assertViolationTest3 = assertViolation+ [+ Assign "k" (I 1),+ Assign "i" (I 0),+ Assign "j" (I 0),+ Assign "n" (I 5),+ While (Or (Lt (Var "i") (Var "n"))+ (Eq (Var "i") (Var "n")))+ [ Assign "i" (Add (Var "i") (I 1))+ , Assign "j" (Add (Var "j") (Var "i"))+ ],+ Assign "z" (Add (Var "k") (Add (Var "i") (Var "j"))),+ Assert (Lt (Mul (Var "n") (I 2)) (Var "z"))+ ]+ ++assertViolationTest4 :: IO (Maybe Env)+assertViolationTest4 = assertViolation+ [+ Assign "k" (I 1),+ Assign "i" (I 0),+ -- Assign "j" (I 0),+ Assign "n" (I 5),+ While (Or (Lt (Var "i") (Var "n"))+ (Eq (Var "i") (Var "n")))+ [ Assign "i" (Add (Var "i") (I 1))+ , Assign "j" (Add (Var "j") (Var "i"))+ ],+ Assign "z" (Add (Var "k") (Add (Var "i") (Var "j"))),+ Assert (Lt (Mul (Var "n") (I 2)) (Var "z"))+ ]+ +
+ quasiquote/DeBruijn/Interpreter.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module DeBruijn.Interpreter ( Expr (..)+ , Ident+ , eval+ , app+ , lams+ , num) where++import Data.Data+import G2.QuasiQuotes.G2Rep++type Ident = Int++data Expr = Var Ident+ | Lam Expr+ | App Expr Expr+ deriving (Show, Read, Eq, Data)++$(derivingG2Rep ''Expr)++type Stack = [Expr]++eval :: Expr -> Expr+eval = eval' []++eval' :: Stack -> Expr -> Expr+eval' (e:stck) (Lam e') = eval' stck (rep 1 e e')+eval' stck (App e1 e2) = eval' (e2:stck) e1+eval' stck e = app $ e:stck++rep :: Int -> Expr -> Expr -> Expr+rep i e v@(Var j)+ | i == j = e+ | otherwise = v+rep i e (Lam e') = Lam (rep (i + 1) e e')+rep i e (App e1 e2) = App (rep i e e1) (rep i e e2)++app :: [Expr] -> Expr+app = foldl1 App++lams :: Int -> Expr -> Expr+lams n e = iterate Lam e !! n++num :: Int -> Expr+num n = Lam $ Lam $ foldr1 App (replicate n (Var 2) ++ [Var 1])
+ quasiquote/DeBruijn/Test.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE QuasiQuotes #-}++module DeBruijn.Test where++import DeBruijn.Interpreter+import G2.QuasiQuotes.QuasiQuotes++solveDeBruijn1 :: IO (Maybe Expr)+solveDeBruijn1 =+ [g2| \(x :: Int) -> ?(syExpr :: Expr) |+ let expr = App syExpr in+ eval (expr (Lam (Var 1))) == (Lam (Var 1))+ && eval (expr (Lam (Var 2))) == (Lam (Var 2)) |] 6++solveDeBruijn :: [([Expr], Expr)] -> IO (Maybe Expr)+solveDeBruijn =+ [g2| \(es :: [([Expr], Expr)]) -> ?(func :: Expr) |+ all (\e -> (eval (app (func:fst e))) == snd e) es |]++solveDeBruijnI :: IO (Maybe Expr)+solveDeBruijnI = solveDeBruijn [ ([num 1], num 1)+ , ([num 2], num 2) ]++solveDeBruijnK :: IO (Maybe Expr)+solveDeBruijnK = solveDeBruijn [ ([num 1, num 2], num 2)+ , ([num 2, num 3], num 3)]++trueLam :: Expr+trueLam = Lam (Lam (Var 2))++falseLam :: Expr+falseLam = Lam (Lam (Var 1))++solveDeBruijnAnd :: IO (Maybe Expr)+solveDeBruijnAnd = solveDeBruijn [ ([trueLam, trueLam], trueLam)+ , ([falseLam, falseLam], falseLam)+ , ([falseLam, trueLam], falseLam) + , ([trueLam, falseLam], falseLam) ]++solveDeBruijnOr :: IO (Maybe Expr)+solveDeBruijnOr = solveDeBruijn [ ([trueLam, trueLam], trueLam)+ , ([falseLam, falseLam], falseLam)+ , ([falseLam, trueLam], trueLam) + , ([trueLam, falseLam], trueLam) ]++solveDeBruijnIte :: IO (Maybe Expr)+solveDeBruijnIte = solveDeBruijn [ ([trueLam, Var 2, Var 4], Var 2)+ , ([falseLam, Var 2, Var 4], Var 4) ]++solveDeBruijnS :: IO (Maybe Expr)+solveDeBruijnS =+ solveDeBruijn+ [ ([Lam (Lam (Var 1)), Lam (Var 1), num 2], num 2)+ , ([Lam (Lam (Var 1)), Lam (Lam (Var 2)), num 3], num 3) ]+ -- [g2| \(_ :: ()) -> ?(func :: Expr) |+ -- let+ -- k = Lam (Lam (Var 2))+ -- in+ -- eval (App func (App k (App (num 1) (num 2)))) == num 2+ -- |] ()+ -- , ([Lam (Lam (Var 1)), Lam (num 3), num 1], num 3)]+ -- , ([Lam (Lam (Lam (Var 2))), Lam (Lam (Var 1)), num 1], Lam (Lam (num 1)))]
+ quasiquote/Evaluations.hs view
@@ -0,0 +1,194 @@+{-# LANGUAGE QuasiQuotes #-}++module Evaluations where++import Data.Time.Clock+import G2.QuasiQuotes.QuasiQuotes++import Arithmetics.Interpreter as A+import DeBruijn.Interpreter as D+import RegEx.RegEx as R+++timeIOAction :: IO a -> IO (a, NominalDiffTime)+timeIOAction action = do+ start <- getCurrentTime+ res <- action+ end <- getCurrentTime+ let diff = diffUTCTime end start+ return (res, diff)++timeIOActionPrint :: Show a => IO a -> IO ()+timeIOActionPrint action = do+ (res, time) <- timeIOAction action+ putStrLn $ show res+ putStrLn $ "time: " ++ show time+++-------------------------------------------+-------------------------------------------+-- Section 2 (Arithmetics)+searchBadEnv :: Stmts -> IO (Maybe Env)+searchBadEnv =+ [g2| \(stmts :: Stmts) -> ?(env :: Env) |+ evalStmts env stmts == Nothing|]++envTest :: BExpr -> IO (Maybe Env)+envTest = [g2|\(b :: BExpr) -> ?(env :: Env) |+ evalB env b |]++badProg :: Stmts+badProg =+ [+ Assign "k" (I 1),+ Assign "i" (I 0),+ -- Assign "j" (I 0),+ Assign "n" (I 5),+ While (A.Or (Lt (A.Var "i") (A.Var "n"))+ (Eq (A.Var "i") (A.Var "n")))+ [ Assign "i" (Add (A.Var "i") (I 1))+ , Assign "j" (Add (A.Var "j") (A.Var "i"))+ ],+ Assign "z" (Add (A.Var "k") (Add (A.Var "i") (A.Var "j"))),+ Assert (Lt (Mul (A.Var "n") (I 2)) (A.Var "z"))+ ]++productSumTest :: BExpr+productSumTest =+ And+ ((Eq + (Mul (A.Var "x") (A.Var "y"))+ (Add (A.Var "x") (A.Var "y"))))+ (Lt (I 0) (A.Var "x"))++runArithmeticsEval :: IO ()+runArithmeticsEval = do+ putStrLn "------------------------"+ putStrLn "-- Arithmetics Eval -------"+ timeIOActionPrint $ searchBadEnv badProg+ timeIOActionPrint $ envTest productSumTest+ putStrLn ""++++-------------------------------------------+-------------------------------------------+-- Section 5.1 (n Queens)+++-------------------------------------------+-------------------------------------------+-- Section 5.2 (Lambda Calculus)++solveDeBruijn :: [([Expr], Expr)] -> IO (Maybe Expr)+solveDeBruijn =+ [g2| \(es :: [([Expr], Expr)]) -> ?(func :: Expr) |+ all (\e -> (eval (app (func:fst e))) == snd e) es |]++idDeBruijn :: [([D.Expr], D.Expr)]+idDeBruijn = [ ([num 1], num 1)+ , ([num 2], num 2) ]++const2Example :: [([D.Expr], D.Expr)]+const2Example =+ [ ([num 1, num 2], num 1)+ , ([num 2, num 3], num 2) ] ++trueLam :: D.Expr+trueLam = Lam (Lam (D.Var 2))++falseLam :: D.Expr+falseLam = Lam (Lam (D.Var 1))++notExample :: [([D.Expr], D.Expr)]+notExample =+ [ ([trueLam], falseLam)+ , ([falseLam], trueLam) ]++orExample :: [([D.Expr], D.Expr)]+orExample =+ [ ([trueLam, trueLam], trueLam)+ , ([falseLam, falseLam], falseLam)+ , ([falseLam, trueLam], trueLam)+ , ([trueLam, falseLam], trueLam )]++andExample :: [([D.Expr], D.Expr)]+andExample =+ [ ([trueLam, trueLam], trueLam)+ , ([falseLam, falseLam], falseLam)+ , ([falseLam, trueLam], falseLam)+ , ([trueLam, falseLam], falseLam )]+++runDeBruijnEval :: IO ()+runDeBruijnEval = do+ putStrLn "------------------------"+ putStrLn "-- DeBruijn Eval -------"+ timeIOActionPrint $ solveDeBruijn idDeBruijn+ timeIOActionPrint $ solveDeBruijn const2Example+ -- timeIOActionPrint $ solveDeBruijn notExample+ timeIOActionPrint $ solveDeBruijn orExample+ -- timeIOActionPrint $ solveDeBruijn andExample+ putStrLn ""+++-------------------------------------------+-------------------------------------------+-- Section 5.3 (Regular Expressions)++stringSearch :: RegEx -> IO (Maybe String)+stringSearch =+ [g2| \(r :: RegEx) -> ?(str :: String) |+ match r str |]++-- (a + b)* c (d + (e f)*)+regex1 :: RegEx+regex1 =+ Concat (Star (R.Or (Atom 'a') (Atom 'b')))+ (Concat (Atom 'c')+ (R.Or (Atom 'd')+ (Concat (Atom 'e')+ (Atom 'f'))))++regex2 :: RegEx+regex2 = Concat (Atom 'a')+ (Concat (Atom 'b')+ (Concat (Atom 'c')+ (Concat (Atom 'd')+ (Concat (Atom 'e')+ ((Atom 'f'))))))++regex3 :: RegEx+regex3 = R.Or (Atom 'a')+ (R.Or (Atom 'b')+ (R.Or (Atom 'c')+ (R.Or (Atom 'd')+ (R.Or (Atom 'e')+ ((Atom 'f'))))))++regex4 :: RegEx+regex4 = Concat (Star (Atom 'a'))+ (Concat (Star (Atom 'b'))+ (Concat (Star (Atom 'c'))+ (Concat (Star (Atom 'd'))+ (Concat (Star (Atom 'e'))+ ((Star (Atom 'f')))))))++++runRegExEval :: IO ()+runRegExEval = do+ putStrLn "------------------------"+ putStrLn "-- RegEx Eval ----------"+ timeIOActionPrint $ stringSearch regex1+ timeIOActionPrint $ stringSearch regex2+ timeIOActionPrint $ stringSearch regex3+ timeIOActionPrint $ stringSearch regex4+ putStrLn ""++++-------------------------------------------+-------------------------------------------++
+ quasiquote/Lambda/Interpreter.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module Lambda.Interpreter where++import Data.Data+import Data.List+import G2.QuasiQuotes.QuasiQuotes+import G2.QuasiQuotes.G2Rep++type Id = String++data Prim = I Int | B Bool | Fun Id+ deriving (Show, Eq, Data)++$(derivingG2Rep ''Prim)++data Expr+ = Var Id+ | Lam Id Expr+ | App Expr Expr+ | Const Prim+ deriving (Show, Eq, Data)++$(derivingG2Rep ''Expr)++type Env = [(Id, Expr)]++eval :: Env -> Expr -> Expr+eval env (Var id) =+ case lookup id env of+ Just expr -> eval env expr+ Nothing -> Const (Fun id)+eval env (App (Lam i body) arg) =+ eval ((i, arg) : env) body+eval env expr = expr+
+ quasiquote/Lambda/Test.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE QuasiQuotes #-}++module Lambda.Test where++import Lambda.Interpreter+import G2.QuasiQuotes.QuasiQuotes++lambdaTest1 :: IO (Maybe Expr)+lambdaTest1 = [g2| \(x :: Int ) -> ?(symExpr :: Expr) |+ let env = [] in+ let expr = App (Lam "b" (Var "b")) symExpr in+ eval env expr == (Const (I 40)) |] 0+++lambdaTest2 :: IO (Maybe Expr)+lambdaTest2 = [g2| \(x :: Int ) -> ?(symExpr :: Expr) |+ let env = [] in+ let expr = symExpr in+ eval env expr == (Const (I 43)) |] 0
+ quasiquote/NQueens/Encoding.hs view
@@ -0,0 +1,62 @@+module NQueens.Encoding where++import Data.List++type Queen = Int++indexPairs :: Int -> [(Int,Int)]+indexPairs n = [(i, j) | i <- [0..n-1], j <- [i+1..n-1]]++legal :: Int -> Queen -> Bool+legal n qs = 1 <= qs && qs <= n++queenPairSafe :: Int -> [Queen] -> (Int, Int) -> Bool+queenPairSafe n qs (i, j) =+ let qs_i = qs !! i+ qs_j = qs !! j+ in (qs_i /= qs_j)+ -- && (abs (qs_j - qs_i) /= (j - i))+ && qs_j - qs_i /= j - i+ && qs_j - qs_i /= i - j++allQueensSafe :: Int -> [Queen] -> Bool+allQueensSafe n qs =+ (n == length qs)+ && all (legal n) qs+ && (all (queenPairSafe n qs) (indexPairs n))++solveListCompN :: Int -> [Int]+solveListCompN n =+ head . filter (allQueensSafe n) $ [x | x <- mapM (const [1..n]) [1..n]]++{-+-- Gets all pairs of unique positions+pairs :: Ord a => [a] -> [(a, a)]+pairs xs = [(a, b) | a <- xs, b <- xs, a < b]++-- Checks if all elements of list are unique+allUnique :: Ord a => [a] -> Bool+allUnique xs = length xs == length (nub xs)++-- Check if two positions are safe+pairSafe :: (Queen, Queen) -> Bool+pairSafe ((x1, y1), (x2, y2)) =+ -- No same x and y value+ (x1 /= x2) && (y1 /= y2)+ -- Not on the same diagonal+ && (abs (x1 - x2) /= abs (y1 - y2))++-- Check that all queens in a list are safe+allSafe :: [Queen] -> Bool+allSafe queens = all pairSafe $ pairs queens++-- Valid Queens on an n x n board+legalQueens :: Int -> [Queen] -> Bool+legalQueens n queens =+ (length queens == n)+ && (n == length (nub queens))+ && all (\(x, y) -> 1 <= x && x <= n && 1 <= y && y <= n) queens+ -- && all (\p -> (1, 1) <= p && p <= (n, n)) queens++-}+
+ quasiquote/NQueens/Test.hs view
@@ -0,0 +1,19 @@+{-# LANGUAGE QuasiQuotes #-}++module NQueens.Test where++import NQueens.Encoding+import G2.QuasiQuotes.QuasiQuotes++{-+queensTestN :: Int -> IO (Maybe [Queen])+queensTestN n = [g2| \(n :: Int) -> ?(queens :: [Queen]) |+ legalQueens n queens+ && allSafe queens |] n+-}++queensTestN :: Int -> IO (Maybe [Queen])+queensTestN num = [g2| \(n :: Int) -> ?(qs :: [Queen]) |+ allQueensSafe n qs |] num++
+ quasiquote/RegEx/RegEx.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module RegEx.RegEx where++import Data.Data+import G2.QuasiQuotes.G2Rep+++data RegEx = Empty | Epsilon | Atom Char+ | Star RegEx | Concat RegEx RegEx | Or RegEx RegEx+ deriving (Show, Eq, Data)++$(derivingG2Rep ''RegEx)++match :: RegEx -> String -> Bool+match Empty _ = False+match Epsilon s = null s+match (Atom x) s = s == [x]+match (Star _) [] = True+match r@(Star x) s = any (match2 x r)+ (splits [1..length s] s)+match (Concat a b) s = any (match2 a b)+ (splits [0..length s] s)+match (Or a b) s = match a s || match b s++match2 :: RegEx -> RegEx -> (String, String) -> Bool+match2 a b (sa, sb) = match a sa && match b sb++splits :: [Int] -> [a] -> [([a], [a])]+splits ns x = map (\n -> splitAt n x) ns++++
+ quasiquote/RegEx/Test.hs view
@@ -0,0 +1,25 @@+{-# LANGUAGE QuasiQuotes #-}++module RegEx.Test where++import RegEx.RegEx+import G2.QuasiQuotes.QuasiQuotes++regexTest1 :: IO (Maybe String)+regexTest1 = stringSearch (Concat (Atom 'a') (Atom 'b'))++regexTest2 :: IO (Maybe String)+regexTest2 = stringSearch r+ where+ r = Concat+ (Star (Or (Atom 'a') (Atom 'b')))+ (Concat (Atom 'c')+ (Or (Atom 'd')+ (Concat (Atom 'e')+ (Atom 'f'))))+ ++stringSearch :: RegEx -> IO (Maybe String)+stringSearch = [g2| \(r :: RegEx) -> ?(str :: String) |+ match r str |]+
+ tests/CaseTest.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE OverloadedStrings #-}++module CaseTest where++import G2.Language+import TestUtils++exists1 :: [Expr] -> Bool+exists1 [(App x y), (App z w)] =+ dcHasName "A" x && dcHasName "B" y && dcHasName "A" z && dcHasName "C" w+exists1 _ = False++exists2 :: [Expr] -> Bool+exists2 [x, y] = dcHasName "B" x && dcHasName "C" y+exists2 _ = False++exists3 :: [Expr] -> Bool+exists3 [x, (App y (App z w))] =+ dcHasName "C" x && dcHasName "A" y && dcHasName "A" z && dcHasName "B" w+exists3 _ = False++exists4 :: [Expr] -> Bool+exists4 [_, (App y z)] = dcHasName "A" y && dcHasName "B" z+exists4 _ = False
+ tests/DefuncTest.hs view
@@ -0,0 +1,83 @@+{-# LANGUAGE OverloadedStrings #-}++module DefuncTest where++import G2.Language+import TestUtils++-- Defunc1++a :: Expr -> Expr+a = App (Data $ DataCon (Name "A" (Just "Defunc1") 0 Nothing) (TyCon (Name "A" (Just "Defunc1") 0 Nothing) TYPE))++dataB :: Expr+dataB = Data $ DataCon (Name "B" (Just "Defunc1") 0 Nothing) (TyCon (Name "A" (Just "Defunc1") 0 Nothing) TYPE)++add1 :: Expr+add1 = Var (Id (Name "add1" (Just "Defunc1") 0 Nothing) tyIntS) ++multiply2 :: Expr+multiply2 = Var (Id (Name "multiply2" (Just "Defunc1") 0 Nothing) tyIntS) ++defunc1Add1 :: [Expr] -> Bool+defunc1Add1 [x, (App b (App _ y))] = x `eqIgT` a (add1) && b `eqIgT` dataB && y `eqIgT` (Lit $ LitInt 3)+defunc1Add1 _ = False++defunc1Multiply2 :: [Expr] -> Bool+defunc1Multiply2 [x, (App b (App _ y))] = x `eqIgT` a (multiply2) && b `eqIgT` dataB && y `eqIgT` (Lit $ LitInt 4)+defunc1Multiply2 _ = False++defuncB :: [Expr] -> Bool+defuncB [App x _, App y _] = x `eqIgT` dataB && y `eqIgT` dataB+defuncB _ = False++-- Defunc2++add1D2 :: Expr+add1D2 = Var (Id (Name "add1" (Just "Defunc2") 0 Nothing) tyIntS)++sub1D2 :: Expr+sub1D2 = Var (Id (Name "sub1" (Just "Defunc2") 0 Nothing) tyIntS)++squareD2 :: Expr+squareD2 = Var (Id (Name "square" (Just "Defunc2") 0 Nothing) tyIntS) ++iListI :: Expr+iListI = Data $ DataCon (Name "I" (Just "Defunc2") 0 Nothing) (TyCon (Name "IList" (Just "Defunc2") 0 Nothing) TYPE)++iListNil :: Expr+iListNil = Data $ DataCon (Name "INil" (Just "Defunc2") 0 Nothing) (TyCon (Name "IList" (Just "Defunc2") 0 Nothing) TYPE)++fListF :: Expr+fListF = Data $ DataCon (Name "F" (Just "Defunc2") 0 Nothing) (TyCon (Name "FList" (Just "Defunc2") 0 Nothing) TYPE)++fListNil :: Expr+fListNil = Data $ DataCon (Name "FNil" (Just "Defunc2") 0 Nothing) (TyCon (Name "FList" (Just "Defunc2") 0 Nothing) TYPE)++add1Def :: Integer -> Integer+add1Def x = x + 1++sub1Def :: Integer -> Integer+sub1Def x = x - 1++squareDef :: Integer -> Integer+squareDef x = x * x++defunc2Check :: [Expr] -> Bool+defunc2Check [flist, llist, llist'] = defunc2Check' flist llist llist'+defunc2Check _ = False++defunc2Check' :: Expr -> Expr -> Expr -> Bool+defunc2Check' (App (App _ f) fs) + (App (App _ (Lit (LitInt i))) is)+ (App (App _ (Lit (LitInt i'))) is') = defunc2Check'' f i i' && defunc2Check' fs is is'+defunc2Check' _ _ _ = True++defunc2Check'' :: Expr -> Integer -> Integer -> Bool+defunc2Check'' (Var (Id (Name "add1" _ _ _) _)) i i' = add1Def i == i'+defunc2Check'' (Var (Id (Name "sub1" _ _ _) _)) i i' = sub1Def i == i'+defunc2Check'' (Var (Id (Name "square" _ _ _) _)) i i' = squareDef i == i'+defunc2Check'' _ _ _ = False++tyIntS :: Type+tyIntS = TyCon (Name "Int" Nothing 0 Nothing) TYPE
+ tests/Expr.hs view
@@ -0,0 +1,100 @@+{-# LANGUAGE OverloadedStrings #-}++module Expr (exprTests) where++import G2.Language+import qualified G2.Language.ExprEnv as E++import Test.Tasty+import Test.Tasty.HUnit++exprTests :: IO TestTree+exprTests = return exprTests'++exprTests' :: TestTree+exprTests' =+ testGroup "Expr"+ [ testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo1+ , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo2+ , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo3+ , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandTo4+ , testCase "Eta Expand To" $ assertBool "Eta Expand To failed" etaExpandToOverSat1 ]++etaExpandTo1 :: Bool+etaExpandTo1 =+ let+ (e, _) = etaExpandTo eenv (mkNameGen ()) 1 idF+ in+ case e of+ (Lam TermL i (App _ (Var i'))) -> i == i'+ _ -> False++etaExpandTo2 :: Bool+etaExpandTo2 =+ let+ (e, _) = etaExpandTo eenv (mkNameGen ()) 1 (Var (Id undefinedN (TyFun int int)))+ in+ case e of+ Var (Id n (TyFun _ _)) -> n == undefinedN+ _ -> False++etaExpandTo3 :: Bool+etaExpandTo3 =+ let+ (e, _) = etaExpandTo eenv (mkNameGen ()) 1+ (Let [(fId, (Var (Id idN (TyFun int int))))] (Var fId))+ in+ case e of+ (Lam TermL i (App (Let _ _) (Var i'))) -> i == i'+ _ -> False++etaExpandTo4 :: Bool+etaExpandTo4 =+ let+ (e, _) = etaExpandTo eenv (mkNameGen ()) 1+ (Let [(fId, (Var (Id undefinedN (TyFun int int))))] (Var fId))+ in+ case e of+ Let [(i, _)] (Var i') -> i == fId && i' == fId+ _ -> False++etaExpandToOverSat1 :: Bool+etaExpandToOverSat1 =+ let+ (e, _) = etaExpandTo eenv (mkNameGen ()) 3 idF+ in+ case e of+ (Lam TermL i (App _ (Var i'))) -> i == i'+ _ -> False++-- DataCons+intD :: DataCon+intD = DataCon (Name "Int" Nothing 0 Nothing) int++-- Types+int :: Type+int = TyCon (Name "Int" Nothing 0 Nothing) TYPE++-- Typed Expr's+x1N :: Name+x1N = Name "x1" Nothing 0 Nothing++fId :: Id+fId = Id (Name "f" Nothing 0 Nothing) (TyFun int int)++idN :: Name+idN = Name "id" Nothing 0 Nothing++idF :: Expr+idF = Var $ Id idN (TyFun int int)++bN :: Name+bN = Name "b" Nothing 0 Nothing++undefinedN :: Name+undefinedN = Name "undefined" Nothing 0 Nothing++eenv :: ExprEnv+eenv = E.fromList [ (x1N, App (Data intD) (Lit (LitInt 1))) + , (idN, Lam TermL (Id bN int) (Var (Id bN int)))+ , (undefinedN, Prim Undefined TyBottom) ]
+ tests/GetNthTest.hs view
@@ -0,0 +1,101 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE OverloadedStrings #-}++module GetNthTest where++import G2.Language+import TestUtils++data CList a = Cons a (CList a) | Nil++data Peano = Succ Peano | Zero++getNth :: CList Integer -> Integer -> Integer+getNth (Cons x _) 0 = x +getNth (Cons _ xs) n = getNth xs (n - 1)+getNth _ _ = -1++getNthErr :: CList a -> Integer -> Maybe a +getNthErr (Cons x _) 0 = Just x +getNthErr (Cons _ xs) n = getNthErr xs (n - 1)+getNthErr _ _ = Nothing++toCList :: Expr -> CList Integer+toCList (App (App (Data (DataCon (Name "Cons" _ _ _) _)) x) y) =+ getInt x Nil $ \x' -> Cons x' (toCList y)+toCList _ = Nil++toCListGen :: Expr -> CList Expr+toCListGen (App (App (Data (DataCon (Name "Cons" _ _ _) _)) e) y) =+ Cons e (toCListGen y)+toCListGen _ = Nil++toCListType :: Expr -> CList Integer+toCListType (App (App (App (Data (DataCon (Name "Cons" _ _ _) _)) (Type _)) x) y) =+ getInt x Nil $ \x' -> Cons x' (toCListType y)+toCListType _ = Nil++toCListGenType :: Expr -> CList Expr+toCListGenType (App (App (App (Data (DataCon (Name "Cons" _ _ _) _)) (Type _)) e) y) =+ Cons e (toCListGenType y)+toCListGenType _ = Nil++cListLength :: CList a -> Integer+cListLength (Cons _ xs) = 1 + cListLength xs+cListLength Nil = 0++getNthTest :: [Expr] -> Bool+getNthTest [cl, i, a] = getIntB i $ \i' -> getIntB a $ \a' -> getNth (toCList cl) i' == a'+getNthTest _ = False++getNthErrTest :: [Expr] -> Bool+getNthErrTest [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListType cl) i' == Nothing+getNthErrTest [cl, i, a] = getIntB i $ \i' -> getIntB a $ \a' -> getNthErr (toCListType cl) i' == Just a'+getNthErrTest _ = False++getNthErrGenTest :: [Expr] -> Bool+getNthErrGenTest [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing+getNthErrGenTest [cl, i, e] =+ case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of+ Just e' -> e' `eqIgT` e+ Nothing -> False+getNthErrGenTest _ = False++getNthErrGenTest' :: [Expr] -> Bool+getNthErrGenTest' [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing+getNthErrGenTest' [cl, i, e] =+ case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of+ Just e' -> e' `eqIgT` e+ Nothing -> False+getNthErrGenTest' _ = False++getNthErrGenTest2 :: [Expr] -> Bool+getNthErrGenTest2 [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing+getNthErrGenTest2 [cl, i, e] =+ case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of+ Just e' -> e' `eqIgT` e+ Nothing -> False+getNthErrGenTest2 _ = False++getNthErrGenTest2' :: [Expr] -> Bool+getNthErrGenTest2' [cl, i, Prim Error _] = getIntB i $ \i' -> getNthErr (toCListGenType cl) i' == Nothing+getNthErrGenTest2' [cl, i, e] =+ case getInt i Nothing $ \i' -> getNthErr (toCListGenType cl) i' of+ Just e' -> e' `eqIgT` e+ Nothing -> False+getNthErrGenTest2' _ = False++elimType :: (ASTContainer m Expr) => m -> m+elimType = modifyASTs elimType'++elimType' :: Expr -> Expr+elimType' (App e (Type _)) = e+elimType' e = e++getNthErrors :: [Expr] -> Bool+getNthErrors [cl, App _ (Lit (LitInt i)), Prim Error _] = getNthErr (toCListGen cl) i == Nothing+getNthErrors _ = False++cfmapTest :: [Expr] -> Bool+cfmapTest [_, e, e'] = cListLength (toCListGenType e) == cListLength (toCListGenType e') || isError e'+cfmapTest _ = False
+ tests/HigherOrderMathTest.hs view
@@ -0,0 +1,89 @@+{-# LANGUAGE OverloadedStrings #-}++module HigherOrderMathTest where++import G2.Language++import TestUtils++abs2 :: Expr+abs2 = Var (Id (Name "abs2" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++abs3 :: Expr+abs3 = Var (Id (Name "abs3" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++square :: Expr+square = Var (Id (Name "square" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++negativeSquare :: Expr+negativeSquare = Var (Id (Name "negativeSquare" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++fourthPower :: Expr+fourthPower = Var (Id (Name "fourthPower" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++add1 :: Expr+add1 = Var (Id (Name "add1" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++sub1 :: Expr+sub1 = Var (Id (Name "sub1" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++add :: Expr+add = Var (Id (Name "add" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++sub :: Expr+sub = Var (Id (Name "sub" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++approxSqrt :: Expr+approxSqrt = Var (Id (Name "approxSqrt" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++pythagorean :: Expr+pythagorean = Var (Id (Name "pythagorean" (Just "HigherOrderMath") 0 Nothing) tyBoolS)++notNegativeAt0 :: Expr+notNegativeAt0 = Var (Id (Name "notNegativeAt0" (Just "HigherOrderMath") 0 Nothing) TyBottom)++notNegativeAt0NegativeAt1 :: Expr+notNegativeAt0NegativeAt1 = Var (Id (Name "notNegativeAt0NegativeAt1" (Just "HigherOrderMath") 0 Nothing) TyBottom)++abs2NonNeg :: [Expr] -> Bool+abs2NonNeg [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` abs2 && x >= 0+abs2NonNeg _ = False++allabs2NonNeg :: [Expr] -> Bool+allabs2NonNeg [f, App _ (Lit (LitFloat x)), _] = not (f `eqIgT` abs3) || x >= 0+allabs2NonNeg _ = True++squareRes :: [Expr] -> Bool+squareRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` square && (x == 0 || x == 1)+squareRes _ = False++negativeSquareRes :: [Expr] -> Bool+negativeSquareRes [f, _] = f `eqIgT` negativeSquare+negativeSquareRes _ = False++fourthPowerRes :: [Expr] -> Bool+fourthPowerRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` square && (x == 0 || x == 1)+fourthPowerRes _ = False++addRes :: [Expr] -> Bool+addRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` add && x > 0+addRes _ = False++subRes :: [Expr] -> Bool+subRes [f, App _ (Lit (LitFloat x)), _] = f `eqIgT` sub && x < 0+subRes _ = False++approxSqrtRes :: [Expr] -> Bool+approxSqrtRes [f, App _ (Lit (LitFloat x))] = f `eqIgT` approxSqrt && x > 0+approxSqrtRes _ = False++pythagoreanRes :: [Expr] -> Bool+pythagoreanRes [f, App _ (Lit (LitFloat x))] = f `eqIgT` pythagorean && x /= 0+pythagoreanRes _ = False++functionSatisfiesRes :: [Expr] -> Bool+functionSatisfiesRes (Var (Id (Name "notNegativeAt0" _ _ _) _):Var (Id (Name"add1" _ _ _) _):_) = True+functionSatisfiesRes _ = False++tyBoolS :: Type+tyBoolS = TyCon (Name "Bool" Nothing 0 Nothing) TYPE
+ tests/InputOutputTest.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE OverloadedStrings #-}+module InputOutputTest ( checkInputOutput+ , checkInputOutputLH ) where++import Test.Tasty+import Test.Tasty.HUnit++import Control.Exception+import qualified Data.Text as T+import System.FilePath++import G2.Config+import G2.Initialization.MkCurrExpr+import G2.Interface+import G2.Language+import G2.Liquid.Interface+import G2.Translation++import Reqs+import TestUtils++checkInputOutput :: FilePath -> String -> String -> Int -> Int -> [Reqs String] -> IO TestTree+checkInputOutput src md entry stps i req = checkInputOutputWithConfig [src] md entry i req (mkConfigTest {steps = stps})++checkInputOutputWithConfig :: [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO TestTree+checkInputOutputWithConfig src md entry i req config = do+ r <- doTimeout (timeLimit config) $ checkInputOutput' src md entry i req config++ let (b, e) = case r of+ Nothing -> (False, "\nTimeout")+ Just (Left e') -> (False, "\n" ++ show e')+ Just (Right (b', _)) -> (b', "")++ return . testCase (show src) $ assertBool ("Input/Output for file " ++ show src ++ " failed on function " ++ entry ++ "." ++ e) b ++checkInputOutput' :: [FilePath] + -> String + -> String + -> Int + -> [Reqs String] + -> Config + -> IO (Either SomeException (Bool, [ExecRes ()]))+checkInputOutput' src md entry i req config = try (checkInputOutput'' src md entry i req config)++checkInputOutput'' :: [FilePath] + -> String + -> String + -> Int + -> [Reqs String] + -> Config + -> IO (Bool, [ExecRes ()])+checkInputOutput'' src md entry i req config = do+ let proj = map takeDirectory src+ (mb_modname, exg2) <- translateLoaded proj src [] simplTranslationConfig config++ let (init_state, _, bindings) = initState exg2 False (T.pack entry) mb_modname (mkCurrExpr Nothing Nothing) config+ putStrLn "test"+ + (r, _) <- runG2WithConfig init_state config bindings++ let chAll = checkExprAll req+ mr <- validateStates proj src md entry chAll [] r+ let io = map (\(ExecRes { conc_args = i', conc_out = o}) -> i' ++ [o]) r++ let chEx = checkExprInOutCount io i req+ + return $ (mr && chEx, r)++------------++checkInputOutputLH :: [FilePath] -> [FilePath] -> String -> String -> Int -> Int -> [Reqs String] -> IO TestTree+checkInputOutputLH proj src md entry stps i req = checkInputOutputLHWithConfig proj src md entry i req (mkConfigTest {steps = stps})++checkInputOutputLHWithConfig :: [FilePath] -> [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO TestTree+checkInputOutputLHWithConfig proj src md entry i req config = do+ r <- doTimeout (timeLimit config) $ checkInputOutputLH' proj src md entry i req config++ let b = case r of+ Just (Right b') -> b'+ _ -> False++ return . testCase (show src) $ assertBool ("Input/Output for file " ++ show src ++ " failed on function " ++ entry ++ ".") b++checkInputOutputLH' :: [FilePath] -> [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO (Either SomeException Bool)+checkInputOutputLH' proj src md entry i req config = try (checkInputOutputLH'' proj src md entry i req config)++checkInputOutputLH'' :: [FilePath] -> [FilePath] -> String -> String -> Int -> [Reqs String] -> Config -> IO Bool+checkInputOutputLH'' proj src md entry i req config = do+ ((r, _), _) <- findCounterExamples proj src (T.pack entry) [] [] config++ let chAll = checkExprAll req++ mr <- validateStates proj src md entry chAll [] r+ let io = map (\(ExecRes { conc_args = i', conc_out = o}) -> i' ++ [o]) r++ let chEx = checkExprInOutCount io i req+ return $ mr && chEx++------------++-- | Checks conditions on given expressions+checkExprAll :: [Reqs String] -> [String]+checkExprAll reqList = [f | RForAll f <- reqList]++checkExprExists :: [Reqs String] -> [String]+checkExprExists reqList = [f | RExists f <- reqList]++checkExprInOutCount :: [[Expr]] -> Int -> [Reqs c] -> Bool+checkExprInOutCount exprs i reqList =+ let+ checkAtLeast = and . map ((>=) (length exprs)) $ [x | AtLeast x <- reqList]+ checkAtMost = and . map ((<=) (length exprs)) $ [x | AtMost x <- reqList]+ checkExactly = and . map ((==) (length exprs)) $ [x | Exactly x <- reqList]++ checkArgCount = and . map ((==) i . length) $ exprs+ in+ checkAtLeast && checkAtMost && checkExactly && checkArgCount
+ tests/PeanoTest.hs view
@@ -0,0 +1,60 @@+{-# LANGUAGE OverloadedStrings #-}++module PeanoTest where++import G2.Language++import TestUtils++zeroPeano :: Expr+zeroPeano =+ Data $ DataCon (Name "Zero" (Just "Peano") 0 Nothing) (TyCon (Name "Peano" (Just "Peano") 0 Nothing) TYPE)++succPeano :: Expr -> Expr+succPeano x =+ App (Data $ DataCon (Name "Succ" (Just "Peano") 0 Nothing) (TyCon (Name "Peano" (Just "Peano") 0 Nothing) TYPE)) x++peano_0_4 :: [Expr] -> Bool+peano_0_4 [a, b, c] = a `eqIgT` zeroPeano && b `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+ && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+peano_0_4 _ = False++peano_1_3 :: [Expr] -> Bool+peano_1_3 [a, b, c] = a `eqIgT` (succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano . succPeano $ zeroPeano)+ && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+peano_1_3 _ = False++peano_1_4 :: [Expr] -> Bool+peano_1_4 [a, b, c] = a `eqIgT` (succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+ && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+peano_1_4 _ = False++peano_2_2 :: [Expr] -> Bool+peano_2_2 [a, b, c] = a `eqIgT` (succPeano . succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano $ zeroPeano)+ && c `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+peano_2_2 _ = False++peano_3_1 :: [Expr] -> Bool+peano_3_1 [a, b, c] = peano_1_3 [b, a, c]+peano_3_1 _ = False++peano_4_0 :: [Expr] -> Bool+peano_4_0 [a, b, c] = peano_0_4 [b, a, c]+peano_4_0 _ = False++peano_4_1 :: [Expr] -> Bool+peano_4_1 [a, b, c] = peano_1_4 [b, a, c]+peano_4_1 _ = False++peano_4_out :: [Expr] -> Bool+peano_4_out [_, _, a] = a `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+peano_4_out _ = False++peano_1_4_5 :: [Expr] -> Bool+peano_1_4_5 [a, b, c] = a `eqIgT` (succPeano $ zeroPeano) && b `eqIgT` (succPeano . succPeano . succPeano . succPeano $ zeroPeano)+ && c `eqIgT` (succPeano . succPeano . succPeano . succPeano . succPeano $ zeroPeano)+peano_1_4_5 _ = False++peano_4_1_5 :: [Expr] -> Bool+peano_4_1_5 [a, b, c] = peano_1_4_5 [b, a, c]+peano_4_1_5 _ = False
+ tests/Reqs.hs view
@@ -0,0 +1,68 @@+module Reqs ( Reqs (..)+ , checkExprGen+ , checkAbsLHExprGen ) where++import G2.Language++-- | Requirements+-- We use these to define checks on tests returning function inputs+-- RForall f -- All the returned inputs satisfy the function f+-- RExists f -- At least one of the returned inputs satisfies the function f+-- AtLeast x -- At least x inputs are returned+-- AtMost x -- At most x inputs are returned+-- Exactly x -- Exactly x inputs are returned+data Reqs c = RForAll c+ | RExists c+ | AtLeast Int+ | AtMost Int+ | Exactly Int++data TestErrors = BadArgCount+ | TooMany+ | TooFew+ | NotExactly+ | ArgsForAllFailed+ | ArgsExistFailed deriving (Show)++-- | Checks conditions on given expressions+checkExprGen :: [[Expr]] -> Int -> [Reqs ([Expr] -> Bool)] -> Bool+checkExprGen exprs i reqList =+ let+ argChecksAll = and . map (\f -> all (givenLengthCheck i f) exprs) $ [f | RForAll f <- reqList]+ argChecksEx = and . map (\f -> any (givenLengthCheck i f) exprs) $ [f | RExists f <- reqList]+ checkL = null $ checkLengths exprs i reqList+ in+ argChecksAll && argChecksEx && checkL++givenLengthCheck :: Int -> ([Expr] -> Bool) -> [Expr] -> Bool+givenLengthCheck i f e = if length e == i then f e else False++checkAbsLHExprGen :: [(State [FuncCall], [Expr], Expr)] -> Int -> [Reqs ([Expr] -> Expr -> [FuncCall] -> Bool)] -> [TestErrors] +checkAbsLHExprGen exprs i reqList =+ let+ argChecksAll =+ if and . map (\f -> all (\(s, es, e) -> lhGivenLengthCheck i f es e (track s)) exprs) $ [f | RForAll f <- reqList]+ then []+ else [ArgsForAllFailed]+ argChecksEx =+ if and . map (\f -> any (\(s, es, e) -> lhGivenLengthCheck i f es e (track s)) exprs) $ [f | RExists f <- reqList]+ then []+ else [ArgsExistFailed]+ checkL = checkLengths (map (\(_, e, _) -> e) exprs) i reqList+ in+ argChecksAll ++ argChecksEx ++ checkL++lhGivenLengthCheck :: Int -> ([Expr] -> Expr -> [FuncCall] -> Bool) -> [Expr] -> Expr -> [FuncCall] -> Bool+lhGivenLengthCheck i f es e fc = if length es == i then f es e fc else False++checkLengths :: [[Expr]] -> Int -> [Reqs c] -> [TestErrors]+checkLengths exprs i reqList =+ let+ checkAtLeast = if and . map ((>=) (length exprs)) $ [x | AtLeast x <- reqList] then [] else [TooFew]+ checkAtMost = if and . map ((<=) (length exprs)) $ [x | AtMost x <- reqList] then [] else [TooMany]+ checkExactly = if and . map ((==) (length exprs)) $ [x | Exactly x <- reqList] then [] else [NotExactly]++ checkArgCount = if and . map ((==) i . length) $ exprs then [] else [BadArgCount]+ in+ checkAtLeast ++ checkAtMost ++ checkExactly ++ checkArgCount+
+ tests/TestUtils.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE OverloadedStrings #-}++module TestUtils where++import qualified Data.Map as M+import Data.Monoid+import qualified Data.Text as T++import G2.Config+import G2.Language++mkConfigTest :: Config+mkConfigTest = (mkConfig "/whatever/" [] M.empty)+ { higherOrderSolver = AllFuncs+ , timeLimit = 50+ , baseInclude = [ "./base-4.9.1.0/Control/Exception/"+ , "./base-4.9.1.0/" ]+ , base = [ "./base-4.9.1.0/Control/Exception/Base.hs"+ , "./base-4.9.1.0/Prelude.hs" ]+ , extraDefaultMods = [] }++mkConfigTestWithMap :: Config+mkConfigTestWithMap =+ mkConfigTest { baseInclude = baseInclude mkConfigTest ++ ["./base-4.9.1.0/Data/Internal/"]+ , base = base mkConfigTest ++ ["./base-4.9.1.0/Data/Internal/Map.hs"] }+++eqIgT :: Expr -> Expr -> Bool+eqIgT (Var n) (Var n') = eqIgIds n n'+eqIgT (Lit c) (Lit c') = c == c'+eqIgT (Prim p _) (Prim p' _) = p == p'+eqIgT (Lam _ n e) (Lam _ n' e') = eqIgIds n n' && e `eqIgT` e'+eqIgT (App e1 e2) (App e1' e2') = e1 `eqIgT` e1' && e2 `eqIgT` e2'+eqIgT (Data (DataCon n _)) (Data (DataCon n' _)) = eqIgNames n n'+eqIgT (Type _) (Type _)= True+eqIgT _ _ = False+++eqIgIds :: Id -> Id -> Bool+eqIgIds (Id n _) (Id n' _) = eqIgNames n n'++eqIgNames :: Name -> Name -> Bool+eqIgNames (Name n m _ _) (Name n' m' _ _) = n == n' && m == m'++typeNameIs :: Type -> T.Text -> Bool+typeNameIs (TyCon n _) s = s == nameOcc n+typeNameIs (TyApp t _) s = typeNameIs t s+typeNameIs _ _ = False++dcHasName :: T.Text -> Expr -> Bool+dcHasName s (Data (DataCon n _)) = s == nameOcc n+dcHasName _ _ = False++isBool :: Expr -> Bool+isBool (Data (DataCon _ (TyCon (Name "Bool" _ _ _) _))) = True+isBool _ = False++dcInAppHasName :: T.Text -> Expr -> Int -> Bool+dcInAppHasName s (Data (DataCon n _)) 0 = s == nameOcc n+dcInAppHasName s (App a _) n = dcInAppHasName s a (n - 1)+dcInAppHasName _ _ _ = False++buriedDCName :: T.Text -> Expr -> Bool+buriedDCName s (App a _) = buriedDCName s a+buriedDCName s (Data (DataCon n _)) = s == nameOcc n+buriedDCName _ _ = False++appNthArgIs :: Expr -> (Expr -> Bool) -> Int -> Bool+appNthArgIs a f i = + let+ u = unApp a+ in+ case length u > i of+ True -> f (u !! i)+ False -> False++isInt :: Expr -> (Integer -> Bool) -> Bool+isInt (Lit (LitInt x)) f = f x+isInt (App _ (Lit (LitInt x))) f = f x+isInt _ _ = False++appNth :: Expr -> Int -> (Expr -> Bool) -> Bool+appNth e 0 p = p e+appNth (App _ e) i p = appNth e (i - 1) p+appNth _ _ _ = False++isIntT :: Type -> Bool+isIntT (TyCon (Name "Int" _ _ _) _) = True+isIntT _ = False++isDouble :: Expr -> (Rational -> Bool) -> Bool+isDouble (App _ (Lit (LitDouble x))) f = f x+isDouble _ _ = False++isFloat :: Expr -> (Rational -> Bool) -> Bool+isFloat (Lit (LitFloat x)) f = f x+isFloat (App _ (Lit (LitFloat x))) f = f x+isFloat _ _ = False++inCast :: Expr -> (Expr -> Bool) -> (Coercion -> Bool) -> Bool+inCast (Cast e c) p q = p e && q c+inCast _ _ _ = False++notCast :: Expr -> Bool+notCast (Cast _ _) = False+notCast _ = True++getInt :: Expr -> a -> (Integer -> a) -> a+getInt (Lit (LitInt x)) _ f = f x+getInt (App _ (Lit (LitInt x))) _ f = f x+getInt _ x _ = x++getIntB :: Expr -> (Integer -> Bool) -> Bool+getIntB e = getInt e False++getBoolB :: Expr -> (Bool -> Bool) -> Bool+getBoolB (Data (DataCon n _)) f = f (nameOcc n == "True")+getBoolB _ _ = False++isApp :: Expr -> Bool+isApp (App _ _) = True+isApp _ = False++isError :: Expr -> Bool+isError (Prim Error _) = True+isError _ = False++isTyFun :: Type -> Bool+isTyFun (TyFun _ _) = True+isTyFun _ = False++noUndefined :: Expr -> Bool+noUndefined = getAll . evalASTs noUndefined'++noUndefined' :: Expr -> All+noUndefined' (Prim Undefined _) = All False+noUndefined' _ = All True
+ tests/Typing.hs view
@@ -0,0 +1,154 @@+{-# LANGUAGE OverloadedStrings #-}++module Typing (typingTests) where++import Prelude hiding (either, maybe)++import G2.Language++import Test.Tasty+import Test.Tasty.HUnit++typingTests :: IO TestTree+typingTests = return typingTests'++typingTests' :: TestTree+typingTests' =+ testGroup "Typing"+ [+ testCase "Function application" $ assertBool "Function application failed" test1+ , testCase "Polymorphic DataCon application" $ assertBool "Polymorphic DataCon application failed" test2+ , testCase "Polymorphic Function application" $ assertBool "Polymorphic Function application failed" test3+ , testCase "Polymorphic Function application 2" $ assertBool "Polymorphic Function application 2 failed" test4+ , testCase "Polymorphic Function application 3" $ assertBool "Polymorphic Function application 3 failed" funcAppTest+ , testCase "Polymorphic Function" $ assertBool "Polymorphic Function failed" funcTest+ , testCase "Kind application" $ assertBool "Kind application failed" tyAppKindTest++ , testCase "Specializes test 1" $ assertBool ".:: failed" specTest1+ , testCase "Specializes test 2" $ assertBool ".:: failed" specTest2+ , testCase "Specializes test 3" $ assertBool ".:: failed" specTest3++ , testCase "Specializes false test 1" $ assertBool ".:: failed" specFalseTest1+ , testCase "Specializes false test 2" $ assertBool ".:: failed" specFalseTest2+ ]++test1 :: Bool+test1 = typeOf (App f1 x1) == int++test2 :: Bool+test2 = typeOf (App (App just (Type int)) x1) == TyApp maybe int++test3 :: Bool+test3 = typeOf + (App + (App+ f2 + (Type int)+ )+ x1+ )+ ==+ int++test4 :: Bool+test4 = typeOf+ (App + (App+ (App+ f3+ (Type int)+ )+ (Type float)+ )+ x1+ )+ ==+ float++funcAppTest :: Bool+funcAppTest = typeOf (App (App idDef (Type int)) x1) == int++funcTest :: Bool+funcTest = idDef .:: (TyForAll (NamedTyBndr aid) (TyFun a a))++tyAppKindTest :: Bool+tyAppKindTest = typeOf (TyApp either a) == TyFun TYPE TYPE++specTest1 :: Bool+specTest1 = x1 .:: int++specTest2 :: Bool+specTest2 = x1 .:: a++specTest3 :: Bool+specTest3 = f2 .:: typeOf f3++specFalseTest1 :: Bool+specFalseTest1 = not $ Var (Id (Name "x1" Nothing 0 Nothing) a) .:: int++specFalseTest2 :: Bool+specFalseTest2 = not $ f3 .:: typeOf f2++-- Typed Expr's+x1 :: Expr+x1 = Var $ Id (Name "x1" Nothing 0 Nothing) int++f1 :: Expr+f1 = Var $ Id (Name "f1" Nothing 0 Nothing) (TyFun int int)++f2 :: Expr+f2 = Var $ Id (Name "f2" Nothing 0 Nothing)+ (TyForAll+ (NamedTyBndr bid)+ (TyFun b b)+ )++f3 :: Expr+f3 = Var $ Id (Name "f3" Nothing 0 Nothing)+ (TyForAll+ (NamedTyBndr bid)+ (TyForAll+ (NamedTyBndr aid)+ (TyFun b a)+ )+ )++just :: Expr+just = Data $ DataCon + (Name "Just" Nothing 0 Nothing) + (TyForAll + (NamedTyBndr aid) + (TyFun a (TyApp maybe a))+ )++idDef :: Expr+idDef = Lam TypeL aid + (Lam TermL+ (Id (Name "x" Nothing 0 Nothing) a)+ (Var (Id (Name "x" Nothing 0 Nothing) a))+ )++-- Types+int :: Type+int = TyCon (Name "Int" Nothing 0 Nothing) TYPE++float :: Type+float = TyCon (Name "Float" Nothing 0 Nothing) TYPE++maybe :: Type+maybe = TyCon (Name "Maybe" Nothing 0 Nothing) (TyFun TYPE TYPE)++either :: Type+either = TyCon (Name "Either" Nothing 0 Nothing) (TyFun TYPE (TyFun TYPE TYPE))++a :: Type+a = TyVar aid++aid :: Id+aid = Id (Name "a" Nothing 0 Nothing) TYPE++b :: Type+b = TyVar bid++bid :: Id+bid = Id (Name "b" Nothing 0 Nothing) TYPE