-- | contains terms and other useful things, imports PolySeq
module Tests where

import Language.Haskell.FreeTheorems.Variations.PolySeq.PolySeq
import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax

term1 = TAbs (TypVar "a")
	 (Abs (TermVar "x") (TArrow Non (TArrow Non (TVar (TypVar "a")) TInt) TInt)
           (Abs (TermVar "y") (TArrow Non (TVar (TypVar "a")) TInt)
	      (App (Var (TermVar "x")) (Var (TermVar "y")))))

testInput1 = "/\\a.\\p::a->Bool.let! p' = p in (fix (\\f::[a]->[a]. \\ys::[a]. case ys of {[] -> []_{a}; x:xs-> let! x' = x in if p x then (let! xs' = xs in x):(f xs) else f xs}))"

testInput2 = "\\f::((Int->Int)->Int)->Int.\\g::(Int->Int)->Int.\\c::Int->Int. f g + g c + (f (\\h::Int->Int.let! h' = h in 3))"
testTyp1 = TAll (LVal Epsilon) (TypVar "a") (TArrow (LVal Epsilon) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))

testTyp2 = TAll (LVal Nbr) (TypVar "a") (TArrow (LVal Epsilon) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))

testTyp3 = TAll (LVal Epsilon) (TypVar "a") (TArrow (LVal Nbr) (TArrow (LVal Epsilon) (TVar (TypVar "a")) TBool) (TArrow (LVal Epsilon) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))

testTyp4 = TAll (LVal Nbr) (TypVar "a") (TArrow (LVal Nbr) (TArrow (LVal Nbr) (TVar (TypVar "a")) TBool) (TArrow (LVal Nbr) (TList (TVar (TypVar "a"))) (TList (TVar (TypVar "a")))))


testTerm = "/\\a.\\p::a->Bool.p:[]_{a->Bool}"