Commit d6510fb9 authored by Sven Keidel's avatar Sven Keidel

fix stack tests

parent e46df256
{ pkgs ? import <nixpkgs> {} }:
let
hsEnv = pkgs.haskell.packages.ghc863.ghcWithPackages(p: with p; [
hsEnv = pkgs.haskell.packages.ghc844.ghcWithPackages(p: with p; [
stack
]);
......
......@@ -81,3 +81,8 @@ instance Num a => Num (Terminating a) where
instance Fractional a => Fractional (Terminating a) where
(/) = liftA2 (/)
fromRational = pure . fromRational
distributeEither :: Either (Terminating a) (Terminating b) -> Terminating (Either a b)
distributeEither (Left (Terminating a)) = Terminating (Left a)
distributeEither (Right (Terminating a)) = Terminating (Right a)
distributeEither _ = NonTerminating
flags: {}
extra-package-dbs: []
resolver: lts-12.10
resolver: lts-12.26
packages:
- 'lib'
- 'rtg'
......
......@@ -105,11 +105,11 @@ runInterp (Interp f) k l senv ctx tenv a =
sortWidening :: Widening Term
sortWidening (Term s _) (Term s' _)= Term (Sort.widening l s s') ctx
from' :: (TermEnv, (StratEnv, (Strat, Term))) -> ((Strat, StratEnv), (TermEnv, Term))
from' (tenv,(senv,(s,t))) = ((s,senv),(tenv,t))
to' :: ((Strat, StratEnv), (TermEnv, Term)) -> (TermEnv, (StratEnv, (Strat, Term)))
to' ((s,senv),(tenv,t)) = (tenv,(senv,(s,t)))
from' :: (TermEnv, (StratEnv, (Strat, Term))) -> ((Strat, StratEnv), (TermEnv, Term))
from' (tenv',(senv',(s,t))) = ((s,senv'),(tenv',t))
to' :: ((Strat, StratEnv), (TermEnv, Term)) -> (TermEnv, (StratEnv, (Strat, Term)))
to' ((s,senv'),(tenv',t)) = (tenv',(senv',(s,t)))
eval :: Int -> Int -> Strat -> StratEnv -> Context -> TermEnv -> Term -> Terminating (FreeCompletion (Failure String (Error () (TermEnv,Term))))
eval i j s = runInterp (eval' s) i j
......
......@@ -3,50 +3,40 @@
{-# LANGUAGE ImplicitParams #-}
module SortSemanticsSpec(main, spec) where
import qualified ConcreteSemantics as C
import SharedSemantics hiding (cons)
import Soundness
import Sort (SortId(..))
-- import qualified ConcreteSemantics as C
-- import Soundness
-- import Sort (SortId(..))
import Syntax hiding (Fail)
import SortSemantics hiding (sortContext)
import SortSemantics -- hiding (sortContext)
import SortContext(Context,Sort(..))
import qualified SortContext as Ctx
import Control.Arrow
-- import Control.Arrow
import Data.Abstract.FreeCompletion (fromCompletion)
import Data.Abstract.Error as E
import Data.Abstract.Failure as F
import qualified Data.Abstract.Maybe as M
-- import qualified Data.Abstract.Maybe as M
import qualified Data.Abstract.Map as S
import qualified Data.Abstract.StackWidening as SW
-- import qualified Data.Abstract.StackWidening as SW
import Data.Abstract.Terminating (fromTerminating)
import qualified Data.Concrete.Powerset as C
import Data.Constructor
import Data.HashMap.Lazy (HashMap)
-- import qualified Data.Concrete.Powerset as C
-- import Data.Constructor
-- import Data.HashMap.Lazy (HashMap)
import qualified Data.HashMap.Lazy as M
import Data.GaloisConnection
import qualified Data.Set as Set
import qualified Data.Term as C
-- import Data.GaloisConnection
-- import qualified Data.Set as Set
-- import qualified Data.Term as C
import Text.Printf
-- import Text.Printf
import Test.Hspec hiding (context)
import Test.Hspec.QuickCheck
import Test.QuickCheck hiding (Success)
-- import Test.Hspec.QuickCheck
-- 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
......@@ -242,7 +232,7 @@ spec = do
let ?ctx = Ctx.empty in
let tenv = termEnv [("x", numerical)]
in do
seval' 0 (Scope ["x"] (Build "x")) tenv numerical `shouldBe` uncaught ()
seval' 0 (Scope ["x"] (Build "x")) tenv numerical `shouldBe` failure "unbound term variable x in build statement !x"
seval' 0 (Scope ["x"] (Match "x")) tenv numerical `shouldBe` success (tenv, numerical)
it "should make non-declared variables available" $
......@@ -258,7 +248,7 @@ spec = do
let ?ctx = Ctx.empty in
let t = term "Exp"
tenv = termEnv [("x",t)]
in seval 1 (Let [("swap", swap)] (Match "x" `Seq` Call "swap" [] [])) t `shouldBe` success (tenv, t)
in seval 2 (Let [("swap", swap)] (Match "x" `Seq` Call "swap" [] [])) t `shouldBe` success (tenv, t)
it "should support recursion" $
let ?ctx = Ctx.empty in
......@@ -349,7 +339,7 @@ spec = do
-- M.JustNothing (Term s _) -> s
-- M.Nothing -> Bottom
termEnv' = C.TermEnv . M.fromList
-- termEnv' = C.TermEnv . M.fromList
termEnv :: [(TermVar, Term)] -> TermEnv
termEnv = S.fromList
emptyEnv :: TermEnv
......@@ -373,14 +363,14 @@ spec = do
(Build (Cons "Nil" []))))
seval :: Int -> Strat -> Term -> Failure String (Error () (TermEnv,Term))
seval i s t = seval'' i 10 s M.empty emptyEnv t
seval i s = seval'' i 10 s M.empty emptyEnv
seval' :: Int -> Strat -> TermEnv -> Term -> Failure String (Error () (TermEnv,Term))
seval' i s tenv t = seval'' i 10 s M.empty tenv t
seval' i s = seval'' i 10 s M.empty
seval'' :: Int -> Int -> Strat -> StratEnv -> TermEnv -> Term -> Failure String (Error () (TermEnv,Term))
seval'' i j s senv tenv t = fromCompletion (error "top element")
(fromTerminating (error "non-terminating sort semantics")
(fromTerminating (error "sort semantics does not terminate")
(eval i j s senv (context t) tenv t))
term :: (?ctx :: Context) => Sort -> Term
......@@ -398,3 +388,15 @@ spec = do
top :: (?ctx :: Context) => Term
top = term Top
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
failure :: String -> Failure String (Error () a)
failure = F.Fail
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