Commit 0cef4834 authored by Sebastian Erdweg's avatar Sebastian Erdweg

add a few tests to SortSemanticsSpec for simplifying arithmetic expressions

parent 627882f3
......@@ -3,7 +3,7 @@
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TupleSections #-}
module Data.Abstract.Map (Map,singleton,empty,lookup,unsafeLookup,insert,insertWith,unsafeInsertWith,delete,union,adjust,toList,fromList,mapMaybe,map,compose,widening) where
module Data.Abstract.Map (Map,singleton,empty,lookup,unsafeLookup,insert,insertWith,unsafeInsertWith,delete,union,adjust,toList,fromList,mapMaybe,map,compose,widening,fromThereList) where
import Prelude hiding (lookup,map,Either(..),(**))
......@@ -110,3 +110,6 @@ instance Identifiable a => IsList (Map a b) where
type Item (Map a b) = (a,b)
toList (Map m) = H.toList (H.map snd m)
fromList l = Map (H.fromList (fmap (second (Must,)) l))
fromThereList :: Identifiable a => [(a,(There,b))] -> Map a b
fromThereList = Map . H.fromList
......@@ -23,3 +23,9 @@ instance Complete There where
instance Hashable There where
hashWithSalt s Must = s `hashWithSalt` (1::Int)
hashWithSalt s May = s `hashWithSalt` (2::Int)
may :: a -> (There,a)
may a = (May,a)
must :: a -> (There,a)
must a = (Must,a)
......@@ -3,6 +3,8 @@
{-# LANGUAGE ImplicitParams #-}
module SortSemanticsSpec(main, spec) where
import Prelude hiding (exp)
-- import qualified ConcreteSemantics as C
-- import Soundness
-- import Sort (SortId(..))
......@@ -18,6 +20,7 @@ import Data.Abstract.Error as E
import Data.Abstract.Failure as F
-- import qualified Data.Abstract.Maybe as M
import qualified Data.Abstract.Map as S
import Data.Abstract.There
-- import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (fromTerminating)
-- import qualified Data.Concrete.Powerset as C
......@@ -299,6 +302,33 @@ spec = do
seval'' 1 3 (Call "foo" [] []) senv emptyEnv t `shouldBe`
success (tenv, Term (List (List (List Top))) c)
describe "simplify arithmetics" $ do
it "reduce Add(Zero,y)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp" in
let reduceAddZero = Match (Cons "Add" [Cons "Zero" [], "y"]) `Seq` Build "y" in
seval 0 (reduceAddZero) exp `shouldBe` successOrFail () (termEnv [("y", exp)], exp)
it "reduce Add(x,Zero)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp" in
let reduceAddZero = Match (Cons "Add" ["x", Cons "Zero" []]) `Seq` Build "x" in
seval 0 (reduceAddZero) exp `shouldBe` successOrFail () (termEnv [("x", exp)], exp)
it "reduce Add(Zero,y) < id + Add(x,Zero)" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp" in
let reduceAddZero1 = Match (Cons "Add" [Cons "Zero" [], "y"]) `Seq` Build "y" in
let reduceAddZero2 = Match (Cons "Add" ["x", Cons "Zero" []]) `Seq` Build "x" in
seval 0 (reduceAddZero1 `leftChoice` reduceAddZero2) exp `shouldBe` successOrFail () (termEnv' [("x", may exp),("y", may exp)], exp)
it "reduce Add(x,y); !x; ?Zero()" $
let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
let exp = term "Exp" in
let reduceAddZero = Match (Cons "Add" ["x", "y"]) `Seq` Build "x" `Seq` Match (Cons "Zero" []) `Seq` Build "y" in
seval 0 (reduceAddZero) exp `shouldBe` successOrFail () (termEnv' [("x", must exp),("y", must exp)], exp)
-- prop "should be sound" $ do
-- i <- choose (0,10)
-- j <- choose (0,10)
......@@ -342,6 +372,10 @@ spec = do
-- termEnv' = C.TermEnv . M.fromList
termEnv :: [(TermVar, Term)] -> TermEnv
termEnv = S.fromList
termEnv' :: [(TermVar, (There,Term))] -> TermEnv
termEnv' = S.fromThereList
emptyEnv :: TermEnv
emptyEnv = 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