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

import Prelude hiding (exp,seq,fail)

import           Syntax hiding (Fail)
import           Syntax as T
import           IllSortedSemantics
import           AbstractInterpreter
import           SortContext(Context,Sort(..))
import qualified SortContext as Ctx
import           Abstract.TermEnvironment

import           Control.Arrow

import           Data.Abstract.Stable(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 qualified Data.Abstract.Map as S
import           Data.Abstract.Terminating (fromTerminating)
import qualified Data.HashMap.Lazy as M
import           Data.Set (Set)
import           Data.Order

import           Test.Hspec hiding (context)

import           GHC.Exts(IsString(..),IsList(..))
import           Text.Printf(printf)

import qualified CaseStudy

main :: IO ()
main = hspec spec

spec :: Spec
spec = do

  it "Widening" $ do
    let ctx = Ctx.fromList [("Succ",["Exp"],"Exp"),("Zero",[],"Exp")]
    let expr = Sorted "Exp" ctx
    let top = Sorted Top ctx
    termWidening ctx 0 10 expr top `shouldBe` (Unstable,top)
    termWidening ctx 0 10 top expr `shouldBe` (Stable,top)
    termWidening ctx 0 10 (IllSorted [("Succ", [expr])]) (IllSorted [("Zero", [])]) `shouldBe` (Unstable, expr)
    termWidening ctx 1 10 (IllSorted [("Succ", [expr])]) (IllSorted [("Zero", [])]) `shouldBe` (Unstable, IllSorted [("Succ", [expr]), ("Zero", [])])
    termWidening ctx 0 10 (IllSorted [("Zero", [])]) (IllSorted [("Succ", [expr])]) `shouldBe` (Unstable, expr)
    termWidening ctx 0 10 expr (IllSorted [("Succ", [expr])]) `shouldBe` (Stable, expr)
    termWidening ctx 0 10 (IllSorted [("Succ", [expr])]) expr `shouldBe` (Unstable, expr)
    termWidening ctx 0 10 top (IllSorted [("Succ", [expr])]) `shouldBe` (Stable, top)
    termWidening ctx 0 10 (IllSorted [("Succ", [expr])]) top `shouldBe` (Unstable, top)


  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) ]
      in do
         seval' (scope ["y"] (build "x")) tenv numerical `shouldBe`
           success (termEnv [("x", numerical) ], numerical)
         seval' (scope ["y"] (match "z")) tenv numerical `shouldBe`
           success (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 = emptyEnv
          prog = (build (T.Cons "Zero" []) `seq` match "x" `seq` 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)]
      in seval' (let_ [("swap", swap)] (scope ["x"] (match "x" `seq` call "swap" [] ["x"]))) emptyEnv t
           `shouldBe` success (emptyEnv, t)

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

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

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

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

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

    it "should terminate and not produce infinite sorts" $
      let ?ctx = Ctx.empty in
      let t = term Top
      in do
        pendingWith "does not terminate"
        seval'' 0 0 (let_ [("map",map'), ("foo",strategy [] [] (scope ["x"] (match "x" `seq` call "map" [call "foo" [] []] ["x"])))] (call "foo" [] [])) (return M.empty) emptyEnv t `shouldBe`
           success (emptyEnv, term (List (List (List Top))))

  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 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 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) emptyEnv exp `shouldOverapproximate`
           successOrFail () (termEnv [("x",exp), ("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 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 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) emptyEnv exp `shouldOverapproximate`
           successOrFail () (termEnv [("x",exp),("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 $ do
      it "trans_bottomup: BExp -> NExp" $ \balg -> do
          seval'' 0 10 (call "trans__bottomup_0_0" [] []) balg emptyEnv (term "BExp") `shouldBe`
            successOrFail () (emptyEnv, term "NExp")

      it "trans_topdown: BExp -> NExp" $ \balg -> do
          seval'' 1 10 (call "trans__topdown_0_0" [] []) balg emptyEnv (term "BExp") `shouldBe`
            successOrFail () (emptyEnv, term "NExp")

  describe "PCF" $
    caseStudy CaseStudy.pcf $ do
      it "lookup: String * Env -> Val" $ \pcf ->
        let prog = term (Tuple [Lexical, List (Tuple [Lexical, "Val"])])
            val  = term "Val"
        in do
          seval'' 0 1 (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 do
          seval'' 2 10 (call "eval_0_0" [] []) pcf emptyEnv prog `shouldBe`
             successOrFail () (emptyEnv, val)

  describe "Negative Normal Form" $
    caseStudy CaseStudy.nnf $
      it "nnf: Formula -> Formula" $ \nnf -> do
        seval'' 0 10 (call "main_0_0" [] []) nnf emptyEnv (term "Formula") `shouldBe`
            success (emptyEnv, term "Formula")

  describe "Causal Commutative Arrows Normalization" $
    caseStudy CaseStudy.cca $
      it "norm: Exp -> Exp" $ \cca ->
        seval'' 0 10 (call "norm_0_0" [] []) cca emptyEnv (term "Exp") `shouldBe`
            successOrFail () (emptyEnv, term "Exp")

  describe "Arrow Desugaring" $
    caseStudy CaseStudy.arrows $ do
      it "tuple-pat: List Var -> APat" $ \desugar ->
        let prog = term $ List "Var"
            val  = term "APat"
        in do
          seval'' 0 10 (call "tuple_pat_0_0" [] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, val)

      it "tuple: List Var -> Exp" $ \desugar ->
        let prog = term $ List "Var"
            val  = term "Exp"
        in do
          seval'' 0 10 (call "tuple_0_0" [] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, val)

      it "tuple-exp: List Exp -> Exp" $ \desugar ->
        let prog = term $ List "Exp"
            val  = term "Exp"
        in do
          seval'' 0 10 (call "tuple_exp_0_0" [] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, val)

      it "at-end: (=> List Var) -> List Var -> List Var " $ \desugar ->
        let prog = term $ List "Var"
            val  = term $ List "Var"
            s = build $ Cons "Cons" [Cons "VarVar" [StringLiteral "v"], Cons "Nil" []]
        in do
          seval'' 0 10 (call "at_end_1_0" [s] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, 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 do
          seval'' 0 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"
        in do
          seval'' 0 10 (call "conc_0_0" [] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, val)

      it "free-pat-vars: APat -> List Var " $ \desugar ->
        let prog = term "APat"
            val  = term $ List "Var"
        in do
          seval'' 1 10 (call "free_pat_vars_0_0" [] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, val)

      it "free-decls-vars: Declbinds -> List Var " $ \desugar ->
        let prog = term "Declbinds"
            val  = term $ List "Var"
        in do
          seval'' 1 10 (call "free_decls_vars_0_0" [] []) desugar emptyEnv prog `shouldBe`
            successOrFail () (emptyEnv, val)

      it "tuple-pat: List(Var) -> APat" $ \desugar -> do
        seval'' 1 10 (call "tuple_pat_0_0" [] []) desugar emptyEnv (term (List "Var"))`shouldBe`
          successOrFail () (emptyEnv, term "APat")

      it "tuple: List(Var) -> Exp" $ \desugar -> do
        seval'' 1 10 (call "tuple_0_0" [] []) desugar emptyEnv (term (List "Var"))`shouldBe`
          successOrFail () (emptyEnv, term "Exp")
        seval'' 1 10 (call "tuple_0_0" [] []) desugar emptyEnv (IllSorted [("Cons",[term "Var", term (List "Var")]), ("Nil",[])])`shouldBe`
          successOrFail () (emptyEnv, term "Exp")

      it "apply-all(|k:Exp): Exp * List(Exp) -> Expr" $ \desugar -> do
        let tenv = termEnv [("v_14", term "Exp")]
        seval'' 1 10 (call "apply_all_0_1" [] ["v_14"]) desugar tenv (term (Tuple ["Exp", List "Exp"]))`shouldBe`
          successOrFail () (tenv, term "Exp")

      it "well-sorted" $ \desugar -> do
        let t = IllSorted [("OpApp",[term "Exp",term "Qop",term "Exp"])
                          ,("Product",[term "Exps2"])
                          ,("Let",[term "Declbinds",term "Exp"])
                          ,("Negation",[term "Exp"])
                          ,("Labeled",[term "Exp",term "LabelBinds"])
                          ,("AppBin",[term "Exp",term "Exp"])
                          ,("Typed",[term "Exp", term (Option "Context"), term "Type"])
                          ,("Case",[term "AnyExp", term "AltList"])
                          ,("ArrProcedure",[term "APat",term "ArrCommand"])
                          ,("If",[term "AnyExp", term "AnyExp", term "Exp"])
                          ,("LSection",[term "Exp",term "Qop"])
                          ,("ListFromTo",[term "Exp",term "Exp"])
                          ,("List",[term (List "Exp")])
                          ,("ListCompr",[term "Exp", term (List "Qual")])
                          ,("ListFrom",[term "Exp"])
                          ,("Abs",[term "Fargs",term "Exp"])
                          ,("ListFirstFromTo",[term "Exp",term "Exp",term "Exp"])
                          ,("RSection",[term "QopNoNeg",term "Exp"])
                          ,("Constr",[term "Gcon"])
                          ,("Named",[term "Qvar",term "Exp"])
                          ,("Lit",[term "Literal"])
                          ,("ListFirstFrom",[term "Exp",term "Exp"])
                          ,("Var",[term "Qvar"])
                          ,("Do",[term "StmtList"])
                          ]
          in termWidening ?ctx 0 10 t bottom `shouldBe` (Stable,term "Exp")

        let t = IllSorted [("VarVar",[term "Varid"])
                          ,("BinOp",[term "Varsym"])
                          ,("TuplePat",[term "Var", term (List "Var")])
                          ,("ConstrPat",[term "Gcon"])]
          in termWidening ?ctx 0 10 t bottom `shouldBe` (Unstable,term "APat")

        let t = IllSorted [("BinCon",[term "Qop"])]
          in termWidening ?ctx 0 10 t bottom `shouldBe` (Unstable,term "Qcon")

      it "builds" $ \desugar -> do
        let pat = build (Cons "OpApp"
                        [Cons "AppBin"
                          [ Cons "Var" [ StringLiteral "arr" ]
                          , Cons "Abs"
                            [ Cons "Cons"
                              [ "g_17",
                                Cons "Nil" []
                              ],
                              "e_17"
                            ]
                          ],
                          StringLiteral ">>>",
                          "f_17"])

            tenv = termEnv [("g_17", term "APat")
                           ,("e_17", term "Exp")
                           ,("f_17", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")

        let pat = build (Cons "OpApp"
                        [Cons "AppBin"
                          [ Cons "Var" [ StringLiteral "arr" ]
                          , Cons "Abs"
                            [ Cons "Cons"
                              [ "b_17",
                                Cons "Nil" []
                              ],
                              Cons "Product"
                              [ Cons "ECons"
                                [ "z_16"
                                , Cons "Cons"
                                  [ "a_17"
                                  , Cons "Nil" []
                                  ]
                                ]
                              ]
                            ]
                          ],
                          StringLiteral ">>>",
                          Cons "Var" [StringLiteral "app"]])

            tenv = termEnv [("b_17", term "APat")
                           ,("z_16", term "Exp")
                           ,("a_17", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")

        let pat = build (Cons "OpApp"
                        [Cons "AppBin"
                          [ Cons "Var" [ StringLiteral "arr" ]
                          , Cons "Abs"
                            [ Cons "Cons"
                              [ "o_16",
                                Cons "Nil" []
                              ],
                              Cons "If"
                              [ "l_16"
                              , Cons "AppBin"
                                [ Cons "Constr" [StringLiteral "Left"]
                                , "p_16"
                                ]
                              , Cons "AppBin"
                                [ Cons "Constr" [StringLiteral "Right"]
                                , "q_16"
                                ]
                              ]
                            ]
                          ],
                          StringLiteral ">>>",
                          Cons "OpApp"
                          [ "r_16"
                          , StringLiteral "|||"
                          , "s_16"
                          ]])

            tenv = termEnv [("o_16", term "APat")
                           ,("l_16", term "Exp")
                           ,("p_16", term "Exp")
                           ,("q_16", term "Exp")
                           ,("r_16", term "Exp")
                           ,("s_16", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")


        let pat = build (Cons "OpApp"
                        [Cons "AppBin"
                          [ Cons "Var" [ StringLiteral "arr" ]
                          , Cons "Abs"
                            [ Cons "Cons"
                              [ "e_16",
                                Cons "Nil" []
                              ],
                              Cons "Let"
                              [ "a_16"
                              , "f_16"
                              ]
                            ]
                          ],
                          StringLiteral ">>>",
                          "g_16"
                        ])

            tenv = termEnv [("e_16", term "APat")
                           ,("a_16", term "Declbinds")
                           ,("f_16", term "Exp")
                           ,("g_16", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")


        let pat = build (Cons "OpApp"
                        [Cons "AppBin"
                          [ Cons "Var" [ StringLiteral "arr" ]
                          , Cons "Abs"
                            [ Cons "Cons"
                              [ Cons "TuplePat"
                                [ "s_15"
                                , Cons "Cons"
                                  [ "o_15"
                                  , Cons "Nil" []
                                  ]
                                ]
                              , Cons "Nil" []
                              ],
                              "t_15"
                            ]
                          ],
                          StringLiteral ">>>",
                          "u_15"
                        ])

            tenv = termEnv [("s_15", term "APat")
                           ,("o_15", term "APat")
                           ,("t_15", term "Exp")
                           ,("u_15", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")


        let pat = build (Cons "OpApp"
                        [Cons "AppBin"
                          [ Cons "Var" [ StringLiteral "arr" ]
                          , Cons "Abs"
                            [ Cons "Cons"
                              [ "g_15"
                              , Cons "Nil" []
                              ]
                            , Cons "Product"
                              [ Cons "ECons"
                                [ "h_15"
                                , Cons "Cons" [ "e_15", Cons "Nil" []]
                                ]
                              ]
                            ]
                          ],
                          StringLiteral ">>>",
                          "i_15"
                        ])

            tenv = termEnv [("g_15", term "APat")
                           ,("h_15", term "Exp")
                           ,("e_15", term "Exp")
                           ,("i_15", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")

        let pat = build (Cons "ArrForm"
                        [ Cons "Constr" [Cons "BinCon" ["p_14"]]
                        , Cons "Cons"
                          [ "q_14"
                          , Cons "Cons"
                            [ "r_14"
                            , Cons "Nil" []
                            ]
                          ]
                        ])
            tenv = termEnv [("p_14", term "Qop")
                           ,("q_14", term "ArrCommand")
                           ,("r_14", term "ArrCommand")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "ArrCommand")

        let pat = build (Cons "BinCon" ["p_14"])
            tenv = termEnv [("p_14", term "Qop")]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Qcon")

        let pat = build (Cons "OpApp"
                         [Cons "AppBin"
                           [ Cons "Var" [ StringLiteral "arr" ]
                           , Cons "Abs"
                             [ Cons "Cons"
                               [ "g_14"
                               , Cons "Nil" []
                               ]
                             , Cons "Let"
                               [ "c_14"
                               , "h_14"
                               ]
                             ]
                           ],
                           StringLiteral ">>>",
                           "i_14"
                         ])
            tenv = termEnv [("g_14", term "APat")
                           ,("c_14", term "Declbinds")
                           ,("h_14", term "Exp")
                           ,("i_14", term "Exp")
                           ]
          in seval'' 1 10 pat desugar tenv bottom `shouldBe`
              success (tenv, term "Exp")


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

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

    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 :: (?ctx :: Context) => LStrat -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    seval s = seval'' 0 10 s (return M.empty) emptyEnv

    seval' :: (?ctx :: Context) => LStrat -> TermEnv Term -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    seval' s = seval'' 0 10 s (return M.empty)

    seval'' :: (?ctx :: Context) => Int -> Int -> LStrat -> LStratEnv -> TermEnv Term -> Term -> Error TypeError (Except () (TermEnv Term,Term))
    seval'' j k s senv tenv t =
      fmap (fmap (fmap (typecheck' ?ctx) *** typecheck' ?ctx)) $
      fromCompletion (error "top element")
        (fromTerminating (error "sort semantics does not terminate")
           (eval j k s senv ?ctx tenv t))

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

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

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

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

    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

    shouldOverapproximate :: (Show a, PreOrd a) => a -> a -> Expectation
    shouldOverapproximate a b
      | b ⊑ a     = return ()
      | otherwise = expectationFailure (printf "%s does not overapproximate %s" (show a) (show b))
