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

import PolySeq
import 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}"