Commit 80ee1151 authored by Sebastian Erdweg's avatar Sebastian Erdweg

migrated stratego tests

parent 5d57e761
......@@ -4,7 +4,7 @@ module ConcreteSpec where
import Prelude hiding (succ,pred)
import SharedSpecs
import ConcreteInterpreter
import Data.Concrete.Error
import Data.Concrete.Failure
import Syntax
import Test.Hspec
......
......@@ -54,7 +54,7 @@ spec = do
num i j = NumVal $ I.Interval i j
toEither :: Terminating (Error String a) -> Either String a
toEither :: Terminating (Failure String a) -> Either String a
toEither (Terminating (Fail e)) = Left e
toEither (Terminating (Success x)) = Right x
toEither NonTerminating = Left "NonTerminating"
......@@ -15,7 +15,8 @@ import Paths_sturdy_stratego
import Control.Monad
import Data.ATerm
import Data.Concrete.Error
import Data.Concrete.Error as E
import Data.Concrete.Failure as F
import Data.Term (TermUtils(..))
import qualified Data.HashMap.Lazy as M
......@@ -28,6 +29,12 @@ import qualified Data.Text.IO as TIO
main :: IO ()
main = hspec spec
success :: a -> Failure String (Error () a)
success a = F.Success $ E.Success a
uncaught :: () -> Failure String (Error () a)
uncaught = F.Success . E.Fail
spec :: Spec
spec = do
......@@ -35,16 +42,16 @@ spec = do
it "should hide declare variables" $ do
let tenv = termEnv [("x", term1)]
eval (Scope ["x"] (Build "x")) M.empty tenv term2
`shouldBe` Fail ()
`shouldBe` uncaught ()
eval (Scope ["x"] (Match "x")) M.empty tenv term2
`shouldBe` Success (tenv,term2)
`shouldBe` success (tenv,term2)
it "should make non-declared variables available" $ do
let tenv = termEnv [("x", term1)]
eval (Scope ["y"] (Build "x")) M.empty tenv term2 `shouldBe`
Success (tenv,term1)
success (tenv,term1)
eval (Scope ["y"] (Match "z")) M.empty tenv term2 `shouldBe`
Success (termEnv [("x", term1), ("z", term2)],term2)
success (termEnv [("x", term1), ("z", term2)],term2)
describe "let" $
it "should support recursion" $ do
......@@ -52,7 +59,7 @@ spec = do
tenv = termEnv []; tenv' = termEnv [("x",t)]
eval (Let [("map", map)] (Match "x" `Seq` Call "map" [Build 1] ["x"])) M.empty tenv t
`shouldBe`
Success (tenv', convertToList [1, 1, 1])
success (tenv', convertToList [1, 1, 1])
describe "call" $
it "should support recursion" $ do
......@@ -61,42 +68,42 @@ spec = do
tenv = termEnv []; tenv' = termEnv [("x",t)]
eval (Match "x" `Seq` Call "map" [Build (T.NumberLiteral 1)] ["x"]) senv tenv t
`shouldBe`
Success (tenv', convertToList [1, 1, 1])
success (tenv', convertToList [1, 1, 1])
describe "match" $ do
prop "should introduce variables" $ \t ->
let tenv = termEnv []
in eval (Match "x" `Seq` Match "y") M.empty tenv t `shouldBe`
Success (termEnv [("x", t), ("y", t)], t)
success (termEnv [("x", t), ("y", t)], t)
prop "should support linear pattern matching" $ \t1 t2 ->
let t' = Cons "f" [t1,t2]
tenv = termEnv []; tenv' = termEnv [("x",t1)]
in eval (Match (T.Cons "f" ["x","x"])) M.empty tenv t' `shouldBe`
if t1 == t2 then Success (tenv', t') else Fail ()
if t1 == t2 then success (tenv', t') else uncaught ()
prop "should match deep" $ \t -> do
p <- similarTermPattern t 3
return $ counterexample (show p) $ when (linear p) $
fmap snd (eval (Match p) M.empty (termEnv []) t) `shouldBe`
Success t
fmap (fmap snd) (eval (Match p) M.empty (termEnv []) t) `shouldBe`
success t
it "should succeed when exploding literals" $
let tenv = termEnv []; tenv' = termEnv [("x", Cons "Nil" [])]
in eval (Match (T.Explode "_" "x")) M.empty tenv 1 `shouldBe`
Success (tenv', 1)
success (tenv', 1)
describe "build" $ do
prop "build should be inverse to match" $ \t -> do
p <- similarTermPattern t 3
return $ counterexample (show p) $ when (linear p) $
fmap snd (eval (Match p `Seq` Build p) M.empty (termEnv []) t) `shouldBe`
Success t
fmap (fmap snd) (eval (Match p `Seq` Build p) M.empty (termEnv []) t) `shouldBe`
success t
prop "build should lookup variables" $ \t -> do
let tenv = termEnv [("x", t)]
eval (Build (T.Var "x")) M.empty tenv t `shouldBe`
Success (tenv,t)
success (tenv,t)
describe "Case Studies" $ describe "Haskell Arrows" $ beforeAll parseArrowCaseStudy $ do
......@@ -107,14 +114,14 @@ spec = do
tenv = termEnv []
eval (Call "union_0_0" [] []) (stratEnv module_) tenv t
`shouldBe`
Success (tenv, convertToList [1,3,2,4])
success (tenv, convertToList [1,3,2,4])
it "concat should work" $ \module_ ->
let l = convertToList (fmap convertToList [[1,2,3],[4,5],[],[6]])
tenv = termEnv []
in eval (Call "concat_0_0" [] []) (stratEnv module_) tenv l
`shouldBe`
Success (tenv, convertToList [1,2,3,4,5,6])
success (tenv, convertToList [1,2,3,4,5,6])
it "free-pat-vars should work" $ \module_ ->
let var x = Cons "Var" [x]
......@@ -124,7 +131,7 @@ spec = do
tenv = termEnv []
in eval (Call "free_pat_vars_0_0" [] []) (stratEnv module_) tenv t
`shouldBe`
Success (tenv, convertToList [var "b", var "c", var "a"])
success (tenv, convertToList [var "b", var "c", var "a"])
where
......
This diff is collapsed.
......@@ -2,7 +2,7 @@
module OrderSpec(main, spec) where
import qualified Data.Abstract.Powerset as A
import qualified Data.Abstract.PreciseStore as S
import qualified Data.Abstract.Map as S
import qualified Data.Concrete.Powerset as P
import Data.Order
import qualified WildcardSemantics as W
......
This diff is collapsed.
......@@ -13,9 +13,10 @@ import qualified WildcardSemantics as W
import Control.Arrow
import Data.Abstract.HandleError
import Data.Abstract.Error as E
import Data.Abstract.Failure as F
import qualified Data.Abstract.Powerset as A
import qualified Data.Abstract.PreciseStore as S
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (fromTerminating)
import qualified Data.Concrete.Powerset as C
......@@ -33,6 +34,15 @@ import Test.QuickCheck hiding (Success)
main :: IO ()
main = hspec spec
success :: a -> Failure String (Error () a)
success a = F.Success $ E.Success a
successOrFail :: () -> a -> Failure String (Error () a)
successOrFail () a = F.Success $ E.SuccessOrFail () a
uncaught :: () -> Failure String (Error () a)
uncaught = F.Success . E.Fail
spec :: Spec
spec = do
......@@ -40,17 +50,17 @@ spec = do
it "should work for the abstract case" $ do
let cons x xs = W.Cons "Cons" [x,xs]
let t = cons 2 W.Wildcard
fmap snd <$> weval 2 (Let [("map", map)]
fmap (fmap snd) <$> weval 2 (Let [("map", map)]
(Match "x" `Seq`
Call "map" [Build 1] ["x"])) t
`shouldBe'`
C.fromFoldable
[ Success $ convertToList [1]
, Success $ convertToList [1,1]
, Success $ convertToList [1,1,1]
, Fail ()
, Fail ()
, Success (cons 1 (cons 1 (cons 1 (cons W.Wildcard W.Wildcard))))]
[ success $ convertToList [1]
, success $ convertToList [1,1]
, success $ convertToList [1,1,1]
, uncaught ()
, uncaught ()
, success (cons 1 (cons 1 (cons 1 (cons W.Wildcard W.Wildcard))))]
describe "call" $
prop "should be sound" $ do
......@@ -109,7 +119,7 @@ spec = do
showLub :: C.Term -> C.Term -> String
showLub t1 t2 = show (alpha (C.fromFoldable [t1,t2] :: C.Pow C.Term) :: W.Term)
shouldBe' :: A.Pow (Error () W.Term) -> A.Pow (Error () W.Term) -> Property
shouldBe' :: A.Pow (Failure String (Error () W.Term)) -> A.Pow (Failure String (Error () W.Term)) -> Property
shouldBe' s1 s2 = counterexample (printf "%s < %s\n" (show s1) (show s2)) (s2 s1 `shouldBe` True)
infix 1 `shouldBe'`
......@@ -125,5 +135,5 @@ spec = do
Build (Cons "Cons" ["x'", "xs'"]))
(Build (Cons "Nil" []))))
weval :: Int -> Strat -> W.Term -> A.Pow (Error () (W.TermEnv,W.Term))
weval :: Int -> Strat -> W.Term -> A.Pow (Failure String (Error () (W.TermEnv,W.Term)))
weval i s = fromTerminating (error "non-terminating wildcard semantics") . W.eval i s M.empty S.empty
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment