{-# OPTIONS_GHC -XTypeOperators -XRank2Types #-}
{-# LANGUAGE FlexibleContexts, ScopedTypeVariables, DeriveDataTypeable #-} 
module Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax where

import Data.Generics(Typeable,Data)

import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug


-- *Data type declarations
newtype LabVar = LabVar Int deriving (Show, Eq, Typeable, Data)

data LabVal 
    = Nbr
    | Epsilon
    deriving(Show, Eq, Ord, Typeable, Data)  

data Label  
    = LVar LabVar
    | LVal LabVal
    | Non
    deriving(Show, Eq, Typeable, Data)

newtype TypVar = TypVar String deriving (Show, Eq, Typeable, Data)

data Typ    = TVar      TypVar
            | TArrow    Label  Typ    Typ
            | TAll      Label  TypVar Typ
            | TList     Typ
            | TInt
	    | TBool
            deriving (Show, Eq, Typeable, Data)

newtype TermVar = TermVar String deriving (Show, Eq, Ord, Typeable, Data)

-- |abbreviation for the pair (TermVar,Typ)
type TypedVar = (TermVar,Typ)

-- |Syntax of the terms used in the algorithm.
data Term 
    = Var TermVar   
    | Abs    TermVar Typ     Term
    | App    Term    Term
    | TAbs   TypVar  Term
    | TApp   Term    Typ
    | Nil    Typ
    | Cons   Term    Term 
    | LCase  Term    Term TermVar TermVar Term
    | Fix    Term
    | LSeq   TermVar Term Term
    | Let    TermVar Term Term
    | Seq    Term    Term
    | I      Int
    | Add    Term    Term
    | T
    | F
    | BCase  Term    Term Term     
    deriving (Show, Eq, Typeable, Data)


data Constraint 
    = Conj Constraint Constraint
    | Impl Constraint Constraint
    | Leq  Label      Label
    | Eq   Label      Label
    | Tru
    | Fls
    deriving(Show, Eq, Typeable, Data)