{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeApplications #-}
module SortSemanticsSpec(main, spec) where

import Prelude hiding (exp,seq,fail)

import           Syntax hiding (fail)
import qualified Syntax as T
import           SortSemantics -- hiding (sortContext)
import           AbstractInterpreter
import           Abstract.TermEnvironment
import           SortContext(Context,Sort(..))
import qualified SortContext as Ctx

import           Data.Abstract.Stable
import           Data.Abstract.FreeCompletion (fromCompletion)
import           Data.Abstract.Except as E
import           Data.Abstract.Error as F
import qualified Data.Abstract.Maybe as A
import           Data.Abstract.There
import qualified Data.Abstract.Map as S
import           Data.Abstract.Terminating (fromTerminating)
import qualified Data.HashMap.Lazy as M
import qualified Data.HashSet as H

import           Test.Hspec hiding (context)

import           GHC.Exts(IsString(..))

import qualified CaseStudy

main :: IO ()
main = hspec spec

spec :: Spec
spec = do

  describe "Utilities" $ do
    it "convertToList should work with identical sorts" $
      let ?ctx = Ctx.empty in
      convertToList [ lexical, lexical ] ?ctx `shouldBe` term (List Lexical)

    it "convertToList should work with different sorts" $
      let ?ctx = Ctx.empty in
      convertToList [ lexical, lexical, numerical ] ?ctx `shouldBe` term (List Top)

    it "convertToList should work on an empty list" $
      let ?ctx = Ctx.empty in
      convertToList [] ?ctx `shouldBe` term (List Bottom)

  describe "match" $ do
    it "should match an identical builtin string literal" $
      let ?ctx = Ctx.empty in
      seval (match (StringLiteral "x")) lexical `shouldBe` successOrfail () (emptyEnv, lexical)

    it "should match another builtin string literal" $
      let ?ctx = Ctx.empty in
      seval (match (StringLiteral "y")) lexical `shouldBe` successOrfail () (emptyEnv, lexical)

    it "should match an equal builtin number literal" $
      let ?ctx = Ctx.empty in
      seval (match (NumberLiteral 42)) numerical `shouldBe` successOrfail () (emptyEnv, numerical)

    it "should match another builtin number literal" $
      let ?ctx = Ctx.empty in
      seval (match (NumberLiteral 1)) numerical `shouldBe`  successOrfail () (emptyEnv, numerical)

    it "a string literal should not match a number literal" $
      let ?ctx = Ctx.empty in
      seval (match (NumberLiteral 1)) lexical `shouldBe` uncaught ()

    it "a number literal should not match a string literal" $
      let ?ctx = Ctx.empty in
      seval (match (StringLiteral "x")) numerical `shouldBe` uncaught ()

    it "should match a PCF expression" $
      let ?ctx = Ctx.fromList [("Zero",[],"Exp")] in
      let t = term "Exp"
      in seval (match (Cons "Zero" [])) t `shouldBe` success (emptyEnv, t)

    it "should match a nested PCF expression" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp")] in
      let t = term "Exp"
      in seval (match (Cons "Succ" [Cons "Zero" []])) t `shouldBe` successOrfail () (emptyEnv, t)

    it "should match a constructor with more than one argument" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp") ,("Zero",[],"Exp") ,("Ifz",["Exp","Exp","Exp"],"Exp")] in
      let t = term "Exp"
      in seval (match (Cons "Ifz" [Cons "Zero" [], Cons "Succ" [Cons "Zero" []], Cons "Zero" []])) t `shouldBe`
        successOrfail () (emptyEnv, t)

    it "should introduce one variable" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp")] in
      let t = term "Exp"
      in seval (match (Cons "Succ" ["x"])) t `shouldBe` successOrfail () (termEnv [("x", t)], t)

    it "should introduce one variable 2" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp")] in
      let t = term "Exp"
      in seval (match (Cons "Succ" ["x"])) t `shouldBe` successOrfail () (termEnv [("x", t)], t)

    it "should introduce multiple variables and support linear pattern matching" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp")] in
      let t = term "Exp"
      in seval (match (Cons "Succ" ["x"]) `seq` match (Cons "Succ" ["y"])) t `shouldBe`
         successOrfail () (termEnv [("x", t), ("y", t)], t)

    it "should support linear pattern matching" $
      let ?ctx = Ctx.fromList [] in
      let t = term (Tuple [Lexical, Lexical])
      in seval (match (Cons "" ["x", "x"])) t `shouldBe` successOrfail () (termEnv [("x",lexical)],t)

    it "should succeed when exploding literals" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv [("x", term (List Bottom))]
      in seval' (match (Explode "_" "x")) (S.delete "x" emptyEnv) numerical `shouldBe` success (tenv, numerical)

    -- it "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" $ do
    it "should build a builtin string literal" $
      let ?ctx = Ctx.empty in
      seval (build (StringLiteral "foo")) bottom `shouldBe` success (emptyEnv, lexical)

    it "should build a builtin number literal" $
      let ?ctx = Ctx.empty in
      seval (build (NumberLiteral 1)) bottom `shouldBe` success (emptyEnv, numerical)

    it "a string grammar should not be build on a number literal" $
      let ?ctx = Ctx.empty in
      seval (build (NumberLiteral 1)) bottom `shouldNotBe` success (emptyEnv, lexical)

    it "a number grammar should not be build on a string literal" $
      let ?ctx = Ctx.empty in
      seval (match (StringLiteral "x")) bottom `shouldNotBe` success (emptyEnv, numerical)

    it "should build a simple constant PCF expression" $
      let ?ctx = Ctx.fromList [("Zero",[],"Exp")] in
      let t = bottom
          t' = term "Exp"
      in seval (build (Cons "Zero" [])) t `shouldBe` success (emptyEnv, t')

    it "should build a nested PCF expression" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp")] in
      let t = bottom
          t' = term "Exp"
      in seval (build (Cons "Succ" [Cons "Zero" []])) t `shouldBe` success (emptyEnv, t')

    it "should build a constructor with more than one argument" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp") ,("Zero",[],"Exp") ,("Ifz",["Exp","Exp","Exp"],"Exp")] in
      let t = term "Exp"
      in seval (build (Cons "Ifz" [Cons "Zero" [], Cons "Succ" [Cons "Zero" []], Cons "Zero" []])) t `shouldBe`
        success (emptyEnv, t)

    it "build should be inverse to match" $
      let ?ctx = Ctx.empty in
      let pat = NumberLiteral 1
      in seval (match pat `seq` build pat) numerical `shouldBe` successOrfail () (emptyEnv, numerical)

    it "build should be inverse to match with a more complicated term" $
      let ?ctx = Ctx.empty in
      let pat = Cons "Cons" [Var "x", Var "xs"]
          t = convertToList [numerical] ?ctx
          tenv = termEnv [("x", numerical), ("xs", term (List Numerical))]
      in seval' (match pat `seq` build pat) tenv t `shouldBe` successOrfail () (tenv, t)

    it "should throw away the current subject term if needed" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv [("x", numerical)]
      in seval' (build (Var "x")) tenv lexical `shouldBe` success (tenv, numerical)

    it "should lookup variables" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv [("x", numerical)]
      in seval' (build (Var "x")) tenv bottom `shouldBe` success (tenv, numerical)

    it "should merge two variables into one term" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv [("x", numerical), ("y", term (List Lexical))]
          t = bottom
      in seval' (build (Cons "Cons" [Var "x", Var "y"])) tenv t `shouldBe` success (tenv, term (List Top))

    it "should properly construct a list of the same type" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv [("x", numerical), ("y", term (List Numerical))]
          t = bottom
      in seval' (build (Cons "Cons" [Var "x", Var "y"])) tenv t `shouldBe` success (tenv, term (List Numerical))

    it "should merge a variable and the given subject term" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp") ,("Zero",[],"Exp") ,("Ifz",["Exp","Exp","Exp"],"Exp")] in
      let t = bottom
          tenv = termEnv [("x", term "Exp")]
      in seval' (build (Cons "Ifz" [Var "x", Cons "Succ" [Cons "Zero" []], Cons "Zero" []])) tenv t `shouldBe`
        success (tenv, term "Exp")

    -- 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,[])] buildPattern

  describe "scope" $ do
    it "should hide declared variables" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv [("x", numerical)]
      in do
         seval' (scope ["x"] (build "x")) tenv numerical `shouldBe` failure "unbound term variable x in build pattern x"
         seval' (scope ["x"] (match "x")) tenv numerical `shouldBe` success (tenv, numerical)

    it "should make non-declared variables available" $
      let ?ctx = Ctx.empty in
      let tenv = termEnv'' [ ("x",numerical) ] ["y"] in
      do
         seval' (scope ["y"] (build "x")) tenv numerical `shouldBe`
           success (tenv, numerical)
         seval' (scope ["y"] (match "z")) (S.delete' @[] ["z"] tenv) numerical `shouldBe`
           success (S.delete' @[] ["y"] $ termEnv [ ("x",numerical), ("z",numerical)], numerical)

    it "should hide variables bound in a choice's test from the else branch" $
      let ?ctx = Ctx.fromList [("Zero",[],"Exp"), ("One",[],"Exp")] in
      let exp = term "Exp"
          tenv = S.delete "x" emptyEnv
          prog = (build (T.Cons "Zero" []) `seq` match "x" `seq` T.fail)
                `leftChoice`
                (match "x")
      in seval' prog tenv exp `shouldBe` success (termEnv [("x", exp)], exp)

  describe "let" $ do
    it "should apply a single function call" $
      let ?ctx = Ctx.empty in
      let t = term (Tuple ["Exp","Exp"])
          -- tenv = termEnv [("x",t)]
          tenv = termEnv'' [] ["x","y"]
      in seval' (let_ [("swap", swap)] (scope ["x"] (match "x" `seq` call "swap" [] ["x"]))) tenv t
           `shouldBe` success (tenv, t)

    it "should support recursion" $
      let ?ctx = Ctx.empty in
      let t = convertToList [numerical, numerical, numerical] ?ctx
          tenv = termEnv' []
      in seval (let_ [("map", map')] (scope ["x"] (match "x" `seq` call "map" [scope [] $ build (NumberLiteral 1)] ["x"]))) t
        `shouldBe` success (tenv, term (List Numerical))

  describe "call" $ do
    it "should apply a single function call" $
      let ?ctx = Ctx.empty in
      let senv = stratEnv [("swap",swap)]
          t = term (Tuple ["Exp","Exp"])
          tenv = termEnv []
      in seval'' 10 (scope ["x"] (match "x" `seq` call "swap" [] [])) senv emptyEnv t `shouldBe` success (tenv, t)

    it "should support an empty list in recursive applications" $
      let ?ctx = Ctx.empty in
      let senv = stratEnv [("map",map')]
          t = convertToList [] ?ctx
          tenv = termEnv []
      in seval'' 10 (scope ["x"] (match "x" `seq` call "map" [scope [] $ build (NumberLiteral 1)] ["x"])) senv emptyEnv t `shouldBe`
           success (tenv, term (List Numerical))

    it "should support a singleton list in recursive applications" $
      let ?ctx = Ctx.empty in
      let senv = stratEnv [("map",map')]
          t = convertToList [numerical] ?ctx
          tenv = termEnv []
      in seval'' 10 (scope ["x"] (match "x" `seq` call "map" [scope [] $ build (NumberLiteral 1)] ["x"])) senv emptyEnv t `shouldBe`
           success (tenv, term (List Numerical))

    it "should support recursion on a list of numbers" $
      let ?ctx = Ctx.empty in
      let senv = stratEnv [("map",map')]
          c = Ctx.empty
          t = convertToList [numerical, numerical, numerical] c
          tenv = termEnv []
      in seval'' 10 (scope ["x"] (match "x" `seq` call "map" [scope [] $ build (NumberLiteral 1)] ["x"])) senv emptyEnv t `shouldBe`
           success (tenv, term (List Numerical))

    it "should terminate and not produce infinite sorts" $
      let ?ctx = Ctx.empty in
      let senv = -- stratEnv [("map",T.liftStrategyScopes map'),
                 --          ("foo",T.liftStrategyScopes $ Strategy [] [] (scope ["x"] (match "x" `seq` call "map" ["foo"] ["x"])))]
            stratEnv [("map",map'),
                      ("foo",strategy [] [] (scope ["x"] (match "x" `seq` call "map" [call "foo" [] []] ["x"])))]
          c = Ctx.empty
          t = Term Top c
          tenv = termEnv []
      in do
        pendingWith "does not terminate with current stack widening"
        seval'' 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"
          reduce = match (Cons "Add" [Cons "Zero" [], "y"]) `seq` build "y"
      in seval' (reduce) (S.delete "y" emptyEnv) 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"
          reduce = match (Cons "Add" ["x", Cons "Zero" []]) `seq` build "x"
      in seval' reduce (S.delete "x" emptyEnv) 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"
          reduce1 = match (Cons "Add" [Cons "Zero" [], "y"]) `seq` build "y"
          reduce2 = match (Cons "Add" ["x", Cons "Zero" []]) `seq` build "x"
      in seval' (reduce1 `leftChoice` reduce2) (S.delete' @[] ["x", "y"] emptyEnv) exp
           `shouldBe` successOrfail () (termEnv' [may "x" exp, may "y" 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"
          reduce = match (Cons "Add" ["x", "y"]) `seq` build "x" `seq` match (Cons "Zero" []) `seq` build "y"
      in seval' reduce (S.delete' @[] ["x", "y"] emptyEnv) exp `shouldBe` successOrfail () (termEnv [("x", exp),("y", exp)], exp)

    it "reduce Double(x)" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp"),("Double",["Exp"],"Exp")] in
      let exp = term "Exp"
          reduce = match (Cons "Double" ["x"]) `seq` build (Cons "Add" ["x", "x"])
      in seval' reduce (S.delete' @[] ["x"] emptyEnv) exp `shouldBe` successOrfail () (termEnv [("x", exp)], exp)

    it "reduce Add(Zero,y) <+ Add(x,Zero) <+ Double(x)" $
      let ?ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp"),("Add",["Exp","Exp"],"Exp")] in
      let exp = term "Exp"
          reduce1 = match (Cons "Add" [Cons "Zero" [], "y"]) `seq` build "y"
          reduce2 = match (Cons "Add" ["x", Cons "Zero" []]) `seq` build "x"
          reduce3 = match (Cons "Double" ["x"]) `seq` build (Cons "Add" ["x", "x"])
      in seval' (reduce1 `leftChoice` reduce2 `leftChoice` reduce3) (S.delete' @[] ["x","y"] emptyEnv) exp
           `shouldBe` successOrfail () (termEnv' [may "x" exp, may "y" exp], exp)

    -- 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 = C.convertToList l1
    --   let t2 = C.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 "Boolean Algebra" $
    caseStudy CaseStudy.balg $
      it "trans_bottomup: BExp -> Exp" $ \balg -> do
          pendingWith "The sort semantics is too imprecise to check this traversal"
          seval'' 10 (call "trans__bottomup_0_0" [] []) balg emptyEnv (term "BExp") `shouldBe`
            successOrfail () (emptyEnv, term "Exp")

  describe "PCF interpreter in Stratego" $
    caseStudy CaseStudy.pcf $ do
      it "lookup: String * Env -> Val" $ \pcf ->
        let prog = term (Tuple [Lexical, List (Tuple [Lexical, "Val"])])
            val  = term "Val"
        in seval'' 10 (call "lookup_0_0" [] []) pcf emptyEnv prog `shouldBe`
            successOrfail () (emptyEnv, val)

      it "eval: Env * Exp -> Val" $ \pcf ->
        let prog = term (Tuple [List (Tuple [Lexical, "Val"]), "Exp"])
            val  = term "Val"
        in seval'' 10 (call "eval_0_0" [] []) pcf emptyEnv prog `shouldBe`
             successOrfail () (emptyEnv, val)

  describe "Negative Normal Form" $
    caseStudy CaseStudy.nnf $
      it "nnf: Formula -> Formula" $ \pcf -> do
        pendingWith "too imprecise to type check"
        seval'' 10 (call "main_0_0" [] []) pcf emptyEnv (term "Formula") `shouldBe`
          successOrfail () (emptyEnv, term "Formula")

  describe "Arrow" $
    caseStudy CaseStudy.arrows $ do

      it "widening should work" $ \_ -> do
        Ctx.widening ?ctx 10 (List "Var") (List "Var")
          `shouldBe` (Stable,List "Var")

        let tenv = S.fromThereList [ ("l_32"::StratVar,(Must,List "Var")),("k_18",(May,Top)),("n_15",(Must,"ArrCommand"))
                                   , ("r_15",(Must,"ArrCommand")), ("vars-list", (Must,List "Var")), ("j_18",(May,List "Var"))
                                   ]
        S.widening (Ctx.widening ?ctx 10) tenv tenv
          `shouldBe` (Stable,tenv)

  -- Success ([l_32 -> List (Var), k_18? -> Top, n_15 -> ArrCommand, r_15 -> ArrCommand, vars-list -> List (Var), j_18? -> List (Var), o_15 -> Bottom, z_18 -> List (Top), i_18? -> Var, y_18 -> Top, l_18? -> Top, u_18 -> List (Top), f_19 -> List (Top)],List (Var)) ⊔ Fail ())
  -- Success ([l_32 -> List (Var), k_18? -> Top, n_15 -> ArrCommand, r_15 -> ArrCommand, vars-list -> List (Var), j_18? -> List (Var), o_15 -> Bottom, z_18 -> List (Top), i_18? -> Var, y_18 -> Top, l_18? -> Top, u_18 -> List (Top), f_19 -> List (Top)],List (Var)) ⊔ Fail (), Unstable


      it "tuple-pat: List Var -> APat" $ \desugar ->
        let prog = term $ List "Var"
            val  = term "APat"
            env = termEnv []
        in sevalNoNeg'' 10 (call "tuple_pat_0_0" [] []) desugar env prog `shouldBe`
            successOrfail () (env, val)

      it "tuple-exp: List Exp -> Exp" $ \desugar ->
        let prog = term $ List "Exp"
            val  = term "Exp"
            env = termEnv [] -- delete desugar $ termEnv []
        in seval'' 10 (call "tuple_exp_0_0" [] []) desugar env prog `shouldBe`
            successOrfail () (env, val)

      it "tuple: List Var -> Exp" $ \desugar ->
        let prog = term $ List "Var"
            val  = term "Exp"
            env = termEnv []
        in sevalNoNeg'' 10 (call "tuple_0_0" [] []) desugar env prog `shouldBe`
            successOrfail () (env, val)

      it "at-end: (=> List Var) -> List Var -> List Var " $ \desugar ->
        let prog = term $ List "Var"
            val  = term $ List "Var"
            env = termEnv []
            s = build $ Cons "Cons" [Cons "VarVar" [StringLiteral "v"], Cons "Nil" []]
        in sevalNoNeg'' 10 (call "at_end_1_0" [s] []) desugar env prog `shouldBe`
            successOrfail () (env, val)

      it "at-end (scoped strat arg): (=> List Var) -> List Var -> List Var " $ \desugar ->
        let prog = term $ List "Var"
            val  = term $ List "Var"
            env = termEnv [("vars-list", term $ List "Var")]
            s = build $ Var "vars-list"
        in sevalNoNeg'' 10 (call "at_end_1_0" [s] []) desugar env prog `shouldBe`
            successOrfail () (env, val)

      it "conc: (List Var, List Var) -> List Var " $ \desugar ->
        let prog = term $ Tuple [List "Var", List "Var"]
            val  = term $ List "Var"
            env = termEnv []
            senv = filterStratEnv ["conc_0_0", "at_end_1_0", "concat_0_0"] <$> desugar
        in sevalNoNeg'' 10 (call "conc_0_0" [] []) senv env prog `shouldBe`
            successOrfail () (env, val)

      it "free-pat-vars: APat -> List Var " $ \desugar ->
        let prog = term "APat"
            val  = term $ List "Var"
            env = termEnv []
            senv = filterStratEnv ["free_pat_vars_0_0", "collect_all_1_0", "collect_all_2_0",
                                   "crush_3_0", "foldr_3_0", "union_0_0", "HdMember_1_0", "fetch_1_0", "eq_0_0"] <$> desugar
        in sevalNoNeg'' 10 (call "free_pat_vars_0_0" [] []) senv env prog `shouldBe`
            successOrfail () (env, val)

      it "free-decls-vars: Declbinds -> List Var " $ \desugar ->
        let prog = term "Declbinds"
            val  = term $ List "Var"
            env = termEnv []
            senv = filterStratEnv ["free_decls_vars_0_0", "collect_all_3_0",
                                   "union_0_0", "crush_3_0", "foldr_3_0",
                                   "HdMember_1_0", "fetch_1_0", "eq_0_0"] <$> desugar
        in sevalNoNeg'' 10 (call "free_decls_vars_0_0" [] []) senv env prog `shouldBe`
            successOrfail () (env, val)

      it "desugar-arrow': ArrCommand -> Exp" $ \desugar ->
        let prog = term "ArrCommand"
            val  = term "Exp"
            env = termEnv [("vars-list", term $ List "Var")]
        in sevalNoNeg'' 10 (call "desugar_arrow_p__0_1" [] [TermVar "vars-list"]) desugar env prog `shouldBe`
            successOrfail () (env, val)

  where
    -- sound' :: Strat -> [(C.Term,[(TermVar,C.Term)])] -> Property
    -- sound' s xs = sound (M.empty,ctx) (C.fromFoldable $ fmap (second termEnv') xs) (eval' s) (eval' s :: Interp (SW.Categories (Strat,StratEnv) (TermEnv,Term) SW.Stack) Term Term) where
    --   ctx = (alpha::C.Pow C.Term -> Context) (C.fromFoldable (map fst xs))

    -- sound'' :: Strat -> [(C.Term,[(TermVar,C.Term)])] -> TermPattern -> Property
    -- sound'' s xs pat = sound (M.empty,ctx) (C.fromFoldable $ fmap (second termEnv') xs) (eval' s) (eval' s :: Interp (SW.Categories (Strat,StratEnv) (TermEnv,Term) SW.Stack) Term Term) where
    --   ctx = (alpha::C.Pow C.Term -> Context) (C.fromFoldable (map fst xs)) `union` patContext tenv pat
    --   tenv = (termEnv [ (v,(alpha::C.Pow C.Term -> Term) (C.singleton t)) | (_,xs') <- xs, (v,t) <- xs'])

    -- patContext :: TermEnv -> TermPattern -> Context
    -- patContext tenv pat = case pat of
      -- Cons c pats -> SortContext
      --   { signatures = unionsWith (++) (M.singleton c [(map (patToSort tenv) pats, patToSort tenv pat)]:map (signatures . (patContext tenv)) pats)
      --   , lexicals = Set.empty
      --   , injectionClosure = M.empty -- Since we're taking the union, we can just leave this empty.
      --   }
      -- _ -> SortContext { signatures = M.empty, lexicals = Set.empty, injectionClosure = M.empty }

    -- patToSort :: TermEnv -> TermPattern -> Sort
    -- patToSort _ (Cons (Constructor c) _) = Sort (SortId c)
    -- patToSort _ (StringLiteral _) = Lexical
    -- patToSort _ (NumberLiteral _) = Numerical
    -- patToSort _ (As _ _) = error "no such sort: as"
    -- patToSort _ (Explode _ _) = error "no such sort: explode"
    -- patToSort tenv (Var x) = case S.lookup x tenv of
    --   M.Just (Term s _) -> s
    --   M.JustNothing (Term s _) -> s
    --   M.Nothing -> Bottom

    -- termEnv' = C.TermEnv . M.fromList
    termEnv :: [(TermVar, Term)] -> TermEnv Term
    termEnv = S.fromList

    -- termEnv' = S.fromThereList
    termEnv' :: [(TermVar, A.Maybe Term)] -> TermEnv Term
    -- termEnv' ts = termEnv (filter (\(_,)))
    -- termEnv' :: [(TermVar, A.Maybe Term)] -> TermEnv
    termEnv' = S.fromThereList . concatMap (\(v,mt) -> case mt of
      A.Nothing -> []
      A.Just t -> [(v,(Must, t))]
      A.JustNothing t -> [(v,(May, t))]
     )

    termEnv''  :: [(TermVar, Term)] -> [TermVar] -> TermEnv Term
    termEnv'' bound = foldr S.delete (S.fromList bound)

    -- delete :: TermVars s => s -> TermEnv Term -> TermEnv Term
    -- delete s = S.delete' (termVars s :: Set TermVar)

    emptyEnv :: TermEnv Term
    emptyEnv = S.empty

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

    swap = strategy [] [] (scope ["x","y"] (match (Cons "" ["x","y"]) `seq` build (Cons "" ["y","x"])))

    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" [call "f" [] []] ["xs"] `seq`
               match "xs'" `seq`
               build (Cons "Cons" ["x'", "xs'"]))
              (build (Cons "Nil" []))))

    seval :: LStrat -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    seval s = seval'' 10 s (stratEnv []) emptyEnv

    seval' :: LStrat -> TermEnv Term -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    seval' s = seval'' 10 s (stratEnv [])

    seval'' :: Int -> LStrat -> LStratEnv -> TermEnv Term -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    seval'' j s senv tenv t =
      fromCompletion (error "top element")
        (fromTerminating (error "sort semantics does not terminate")
           (eval j s senv (context t) tenv t))

    sevalNoNeg'' :: Int -> LStrat -> LStratEnv -> TermEnv Term -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    sevalNoNeg'' j s senv tenv t = dropNegativeBindings $ seval'' j s senv tenv t

    dropNegativeBindings :: Error TypeError (Except () (TermEnv Term,a)) -> Error TypeError (Except () (TermEnv Term,a))
    -- dropNegativeBindings (F.Success (E.Success (env,a))) = (F.Success (E.Success (S.dropNegativeBindings env,a)))
    -- dropNegativeBindings (F.Success (E.SuccessOrfail e (env,a))) = (F.Success (E.SuccessOrfail e (S.dropNegativeBindings env,a)))
    dropNegativeBindings res = res

    term :: (?ctx :: Context) => Sort -> Term
    term s = Term s ?ctx

    bottom :: (?ctx :: Context) => Term
    bottom = term Bottom

    lexical :: (?ctx :: Context) => Term
    lexical = term Lexical

    numerical :: (?ctx :: Context) => Term
    numerical = term Numerical

    -- top :: (?ctx :: Context) => Term
    -- top = term Top

    -- atop :: (?ctx :: Context) => A.Maybe Term
    -- atop = A.JustNothing top

    may :: k -> v -> (k,A.Maybe v)
    may k v = (k,A.JustNothing v)

    -- must :: k -> v -> (k,A.Maybe v)
    -- must k v = (k,A.Just v)

    -- notThere :: k -> (k, A.Maybe v) 
    -- notThere k = (k,A.Nothing)

    success :: a -> Error e (Except () a)
    success a = F.Success $ E.Success a

    successOrfail :: () -> a -> Error e (Except () a)
    successOrfail () a = F.Success $ E.SuccessOrFail () a

    uncaught :: () -> Error e (Except () a)
    uncaught = F.Success . E.Fail

    failure :: String -> Error TypeError (Except () a)
    failure = F.Fail . fromString

    caseStudy :: IO (Context,LStratEnv) -> ((?ctx :: Context) => SpecWith LStratEnv) -> Spec
    caseStudy loadCaseStudy spc = do
      (cntx,senv) <- runIO loadCaseStudy
      let ?ctx = cntx in beforeAll (return senv) spc
