WildcardSemanticsSpec.hs 4.37 KB
Newer Older
Sven Keidel's avatar
Sven Keidel committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module WildcardSemanticsSpec(main, spec) where

import           Prelude hiding (map)
    
import qualified ConcreteSemantics as C
import           SharedSemantics
import           Soundness
import           Syntax hiding (Fail)
import qualified WildcardSemantics as W

import           Control.Arrow

import qualified Data.HashMap.Lazy as M
import           Data.Result hiding (map)
import           Data.Order
import           Data.GaloisConnection
import           Data.Term(TermUtils(..))
import qualified Data.Powerset as C
import qualified Data.AbstractPowerset as A
-- import           Data.PowersetResult (PowersetResult(..))
    
import           Text.Printf

import           Test.Hspec
import           Test.Hspec.QuickCheck
import           Test.QuickCheck hiding (Result(..))

main :: IO ()
main = hspec spec

spec :: Spec
spec = do

  describe "let" $
    it "should work for the abstract case" $ do
      let cons x xs = W.Cons "Cons" [x,xs]
      let t = cons 2 W.Wildcard
      fmap fst <$> 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))))]

  describe "call" $
    prop "should be sound" $ do
      i <- choose (0,10)
      j <- choose (0,10)
      l <- C.similarTerms i 7 2 10
      let (l1,l2) = splitAt j l
      let t1 = convertToList l1
      let t2 = convertToList l2
      return $ counterexample (printf "t: %s\n"
                                      (showLub t1 t2))
             $ sound' (Let [("map", map)]
                  (Match "x" `Seq`
                   Call "map" [Build 1] ["x"]))
                  [(t1,[]),(t2,[])]

  describe "match" $ do

    prop "should handle inconsistent environments" $ do
      let t1 = C.Cons "f" []
          t2 = C.Cons "g" []
      sound' (Match "x") [(t1, [("x", t1)]), (t2, [("y", t2)])]

    prop "should be sound" $ do
      [t1,t2,t3] <- C.similarTerms 3 7 2 10
      matchPattern <- C.similarTermPattern t1 3
      return $ counterexample
                 (printf "pattern: %s\n %s ⊔ %s = %s"
                    (show matchPattern) (show t2) (show t3)
                    (showLub t2 t3))
             $ sound' (Match matchPattern) [(t2,[]),(t3,[])]

  describe "build" $
    prop "should be sound" $ do
      [t1,t2,t3] <- C.similarTerms 3 7 2 10
      matchPattern <- C.similarTermPattern t1 3
      let vars = patternVars' matchPattern
      buildPattern <- arbitraryTermPattern 5 2 $
        if not (null vars) then elements vars else arbitrary
      return $ counterexample
                 (printf "match pattern: %s\nbuild pattern: %s\nt2: %s\nt3: %s\nlub t2 t3 = %s"
                    (show matchPattern) (show buildPattern) (show t2) (show t3)
                    (showLub t2 t3))
             $ sound' (Match matchPattern `Seq` Build buildPattern) [(t2,[]),(t3,[])]

  -- describe "lookupTermVar" $
  --   prop "should be sound" $ do
  --     sound M.empty lookupTermVar lookupTermVar 

  where
    sound' :: Strat -> [(C.Term,[(TermVar,C.Term)])] -> Property
    sound' s xs = sound M.empty (C.fromFoldable $ fmap (second termEnv) xs) (eval' s) (eval' s :: W.Interp W.Term W.Term)

    termEnv = C.TermEnv . M.fromList

    showLub :: C.Term -> C.Term -> String
    showLub t1 t2 = show (alpha (C.fromFoldable [t1,t2] :: C.Pow C.Term) :: W.Term) 

    shouldBe' :: A.Pow (Result W.Term) -> A.Pow (Result W.Term) -> Property
    shouldBe' s1 s2 = counterexample (printf "%s < %s\n" (show s1) (show s2)) (s2  s1 `shouldBe` True)
    infix 1 `shouldBe'`

    map = Strategy ["f"] ["l"] (Scope ["x","xs","x'","xs'"] (
            Build "l" `Seq`
            GuardedChoice
              (Match (Cons "Cons" ["x","xs"]))
              (Build "x" `Seq`
               Call "f" [] [] `Seq`
               Match "x'" `Seq`
               Call "map" ["f"] ["xs"] `Seq`
               Match "xs'" `Seq`
               Build (Cons "Cons" ["x'", "xs'"]))
              (Build (Cons "Nil" []))))

    weval :: Int -> Strat -> W.Term -> A.Pow (Result (W.Term,W.TermEnv))
Jente Hidskes's avatar
Jente Hidskes committed
127
    weval i s = W.eval i s M.empty (W.TermEnv M.empty)