terms.hs

Cores are generated from Confluence a modern logic design language. Confluence is a simple, yet high

module Language.Atom.Terms
  (
  -- * Types
    Term  (..)
  , Var   (..)
  , UTerm (..)
  , UVar  (..)
  , TermT (..)
  , NumT
  , IntegralT
  , FloatingT
  , TermType  (..)
  , TermConst (..)
  , utermType
  , uvarType
  -- * Constants
  , boolC
  , true
  , false
  , intC
  , floatC
  , doubleC
  -- * Type Casting
  , toInt
  , toFloat
  , toDouble
  -- * Variable Reference
  , value
  -- * Logical Operations
  , inv
  , (&&.)
  , (||.)
  , and_
  , or_
  , any_
  , all_
  -- * Equality and Comparison
  , (==.)
  , (/=.)
  , (<.)
  , (<=.)
  , (>.)
  , (>=.)
  , min_
  , max_
  , limit
  -- * Arithmetic Operations
  , div_
  , mod_
  , atan2_
  -- * Conditional Operator
  , mux
  -- * Misc
  , termVars
  ) where

import qualified Data.Set as Set
import Data.List
import Data.Ratio

import Language.Atom.Utils

--infixl 7 /., %.
--infixl 6 +., -.
--infixr 5 ++.
infix  4 ==., /=., <., <=., >., >=.
infixl 3 &&. --, ^. -- , &&&, $&, $&&
infixl 2 ||. -- , |||, $$, $:, $|
--infixr 1 -- <==, <-- -- , |->, |=>, -->

-- | The type of a 'Term'.
data TermType
  = TermBool
  | TermInt
  | TermFloat
  | TermDouble
  deriving (Eq, Ord)

-- | The type of a constant.
data TermConst
  = TermConstBool   Bool
  | TermConstInt    Int
  | TermConstFloat  Float
  | TermConstDouble Double
  deriving (Show, Eq, Ord)

-- | A typed term is an combinational expression of inputs and variables ('Var').
data Term :: * -> * where
  Cast  :: (NumT a, NumT b) => Term a -> Term b
  Ref   :: TermT a => Var a -> Term a
  Const :: TermT a => a -> Term a
  Input :: TermT a => [String] -> Term a
  Add   :: NumT a => Term a -> Term a -> Term a
  Sub   :: NumT a => Term a -> Term a -> Term a
  Mul   :: NumT a => Term a -> Term a -> Term a
  Div   :: NumT a => Term a -> Term a -> Term a
  Mod   :: IntegralT a => Term a -> Term a -> Term a
  Inv   :: Term Bool -> Term Bool
  And   :: Term Bool -> Term Bool -> Term Bool
  Eq    :: EqT a  => Term a -> Term a -> Term Bool
  Lt    :: OrdT a => Term a -> Term a -> Term Bool
  Mux   :: TermT a => Term Bool -> Term a -> Term a -> Term a
  Exp   :: FloatingT a => Term a -> Term a
  Log   :: FloatingT a => Term a -> Term a
  Sqrt  :: FloatingT a => Term a -> Term a
  Pow   :: FloatingT a => Term a -> Term a -> Term a
  Sin   :: FloatingT a => Term a -> Term a
  Cos   :: FloatingT a => Term a -> Term a
  Sinh  :: FloatingT a => Term a -> Term a
  Cosh  :: FloatingT a => Term a -> Term a
  Asin  :: FloatingT a => Term a -> Term a
  Acos  :: FloatingT a => Term a -> Term a
  Atan  :: FloatingT a => Term a -> Term a
  Atan2 :: FloatingT a => Term a -> Term a -> Term a
  Asinh :: FloatingT a => Term a -> Term a
  Acosh :: FloatingT a => Term a -> Term a
  Atanh :: FloatingT a => Term a -> Term a

instance TermT a => Ord (Term a) where
  compare a b = case (a,b) of
    (a,b) | termId a /= termId b -> compare (termId a) (termId b)
    (Cast a,  Cast b)   -> compareTerms' a b
    (Ref a,   Ref b)    -> compare a b
    (Const a, Const b)  -> compare a b
    (Input a, Input b)  -> compare a b
    (Add a b, Add c d)  -> compareBinCummTerms (a,b) (c,d)
    (Sub a b, Sub c d)  -> compareBinTerms     (a,b) (c,d)
    (Mul a b, Mul c d)  -> compareBinCummTerms (a,b) (c,d)
    (Div a b, Div c d)  -> compareBinTerms     (a,b) (c,d)
    (Mod a b, Mod c d)  -> compareBinTerms     (a,b) (c,d)
    (Inv a,   Inv b)    -> compare a b
    (And a b, And c d)  -> compareBinCummTerms (a,b) (c,d)
    (Eq  a b, Eq  c d)  -> compareBinCummTerms' (a,b) (c,d)
    (Lt  a b, Lt  c d)  -> compareBinTerms'    (a,b) (c,d)
    (Mux a b c, Mux d e f) -> case (compare a d, compare b e, compare c f) of
      (EQ,EQ,o) -> o
      (EQ,o,_)  -> o
      (o,_,_)   -> o
    (Exp   a,   Exp   b) -> compare a b
    (Log   a,   Log   b) -> compare a b
    (Sqrt  a,   Sqrt  b) -> compare a b
    (Pow   a b, Pow   c d) -> compareBinTerms (a,b) (c,d)
    (Sin   a,   Sin   b) -> compare a b
    (Cos   a,   Cos   b) -> compare a b
    (Sinh  a,   Sinh  b) -> compare a b
    (Cosh  a,   Cosh  b) -> compare a b
    (Asin  a,   Asin  b) -> compare a b
    (Acos  a,   Acos  b) -> compare a b
    (Atan  a,   Atan  b) -> compare a b
    (Atan2 a b, Atan2 c d) -> compareBinTerms (a,b) (c,d)
    (Asinh a,   Asinh b) -> compare a b
    (Acosh a,   Acosh b) -> compare a b
    (Atanh a,   Atanh b) -> compare a b
    (_,_) -> error "Terms.Ord (Term a)"

compareBinTerms :: TermT a => (Term a, Term a) -> (Term a, Term a) -> Ordering
compareBinTerms (a0,a1) (b0,b1) = case compare a0 b0 of
  EQ -> compare a1 b1
  o  -> o

compareBinCummTerms :: TermT a => (Term a, Term a) -> (Term a, Term a) -> Ordering
compareBinCummTerms (a0,a1) (b0,b1) = case (compare a0 b0, compare a0 b1) of
  (EQ,_) -> compare a1 b1
  (_,EQ) -> compare a1 b0
  (o,_)  -> o

compareTerms' :: (TermT a, TermT b) => Term a -> Term b -> Ordering
compareTerms' a b = case (uterm a, uterm b) of
  (UTermBool   a, UTermBool   b) -> compare a b
  (UTermInt    a, UTermInt    b) -> compare a b
  (UTermFloat  a, UTermFloat  b) -> compare a b
  (UTermDouble a, UTermDouble b) -> compare a b
  (a,b) -> compare (utermId a) (utermId b)

compareBinTerms' :: (TermT a, TermT b) => (Term a, Term a) -> (Term b, Term b) -> Ordering
compareBinTerms' (a0,a1) (b0,b1) = case compareTerms' a0 b0 of
  EQ -> compareTerms' a1 b1
  o  -> o

compareBinCummTerms' :: (TermT a, TermT b) => (Term a, Term a) -> (Term b, Term b) -> Ordering
compareBinCummTerms' (a0,a1) (b0,b1) = case (compareTerms' a0 b0, compareTerms' a0 b1) of
  (EQ,_) -> compareTerms' a1 b1
  (_,EQ) -> compareTerms' a1 b0
  (o,_)  -> o

utermId :: UTerm -> Int
utermId t = case t of
  UTermBool   _ -> 0
  UTermInt    _ -> 1
  UTermFloat  _ -> 2
  UTermDouble _ -> 3

termId :: Term a -> Int
termId t = case t of
  Cast _    -> 0
  Ref _     -> 1
  Const _   -> 2
  Input _   -> 3
  Add _ _   -> 4
  Sub _ _   -> 5
  Mul _ _   -> 6
  Div _ _   -> 7
  Mod _ _   -> 8
  Inv _     -> 9
  And _ _   -> 10
  Eq  _ _   -> 11
  Lt  _ _   -> 12
  Mux _ _ _ -> 13
  Exp _     -> 14
  Log _     -> 15
  Sqrt _    -> 16
  Pow _ _   -> 17
  Sin _     -> 18
  Cos _     -> 19
  Sinh _    -> 20
  Cosh _    -> 21
  Asin _    -> 22
  Acos _    -> 23
  Atan _    -> 24
  Atan2 _ _ -> 25
  Asinh _   -> 26
  Acosh _   -> 27
  Atanh _   -> 28


instance TermT a => Eq (Term a) where
  a == b = case compare a b of {EQ -> True; _ -> False}

-- | Untyped term.
data UTerm
  = UTermBool   (Term Bool)
  | UTermInt    (Term Int)
  | UTermFloat  (Term Float)
  | UTermDouble (Term Double)
  deriving (Eq, Ord)

-- | Returns the type of an untyped term.
utermType :: UTerm -> TermType
utermType ut = case ut of
  UTermBool   _ -> TermBool
  UTermInt    _ -> TermInt
  UTermFloat  _ -> TermFloat
  UTermDouble _ -> TermDouble

-- | Returns the type of an untyped variable.
uvarType :: UVar -> TermType
uvarType u = case u of
  UVarBool   _ -> TermBool
  UVarInt    _ -> TermInt
  UVarFloat  _ -> TermFloat
  UVarDouble _ -> TermDouble

instance Show UTerm where
  show (UTermBool   v) = show v
  show (UTermInt    v) = show v
  show (UTermFloat  v) = show v
  show (UTermDouble v) = show v

-- | The class of types that are valid terms.
class (Show a, Eq a, Ord a) => TermT a where
  -- | Returns an untyped variable of a typed variable.
  uvar      :: Var  a -> UVar
  -- | Returns an untyped term of a typed variable.
  uterm     :: Term a -> UTerm
  -- | Returns the term type of a term.
  termType  :: Term a -> TermType
  -- | Returns the term type of a variable.
  varType   :: Var  a -> TermType
  -- | Returns a zero constant.
  zeroConst :: a
instance TermT Bool where
  uvar  v = UVarBool v
  uterm t = UTermBool t
  termType _ = TermBool
  varType  _ = TermBool
  zeroConst = False
instance TermT Int where
  uvar  v = UVarInt v
  uterm t = UTermInt t
  termType _ = TermInt
  varType  _ = TermInt
  zeroConst = 0
instance TermT Float where
  uvar  v = UVarFloat v
  uterm t = UTermFloat t
  termType _ = TermFloat
  varType  _ = TermFloat
  zeroConst = 0
instance TermT Double where
  uvar  v = UVarDouble v
  uterm t = UTermDouble t
  termType _ = TermDouble
  varType  _ = TermDouble
  zeroConst = 0

-- | The class of types that are valid numeric terms.
class TermT a => NumT a
instance NumT Int
instance NumT Float
instance NumT Double

-- | The class of types that are valid integral terms.
class NumT a => IntegralT a
instance IntegralT Int

-- | The class of types that are valid floating point terms.
class (NumT a, RealFloat a) => FloatingT a
instance FloatingT Float
instance FloatingT Double

-- | The class of types the can be compared for equality (==., \==.).
class TermT a => EqT a where
  (==.) :: Term a -> Term a -> Term Bool
  (==.) a b | a == b = true
  (==.) (Const a) (Const b) = Const $ a == b
  (==.) a b = Eq a b
instance EqT Bool where
  (==.) a b | a == b = true
  (==.) a b = a &&. b ||. inv a &&. inv b
instance EqT Int
instance EqT Float
instance EqT Double

-- | The class of types that can be compared for relation (<., >=., etc).
class TermT a => OrdT a
instance OrdT Int
instance OrdT Float
instance OrdT Double

-- | Typed variable.
data Var a
  = Var    [String] a
  deriving (Eq, Ord)

-- | Untyped variable.
data UVar
  = UVarBool   (Var Bool)
  | UVarInt    (Var Int)
  | UVarFloat  (Var Float)
  | UVarDouble (Var Double)
  deriving (Eq, Ord)

instance Show UVar where