terms.hs

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

  show (UVarBool   v) = show v
  show (UVarInt    v) = show v
  show (UVarFloat  v) = show v
  show (UVarDouble v) = show v
--instance Show a => Eq (Term a) where
--  a == b = show a == show b

--instance Show a => Ord (Term a) where
--  compare a b = compare (show a) (show b)

parens :: String -> String
parens s = "(" ++ s ++ ")"

instance Show a => Show (Term a) where
  show a = case a of
    Cast a  -> case termType a of
      TermBool   -> parens $ parens "bool"   ++ show a
      TermInt    -> parens $ parens "int"    ++ show a
      TermFloat  -> parens $ parens "float"  ++ show a
      TermDouble -> parens $ parens "double" ++ show a
    Ref a     -> show a
    Const a   -> show a
    Input a   -> join a "."
    Add a b   -> parens $ show a ++ " + " ++ show b
    Sub a b   -> parens $ show a ++ " - " ++ show b
    Mul a b   -> parens $ show a ++ " * " ++ show b
    Div a b   -> parens $ show a ++ " / " ++ show b
    Mod a b   -> parens $ show a ++ " % " ++ show b
    Inv a     -> parens $ "! " ++ show a
    And a b   -> parens $ show a ++ " && " ++ show b
    Eq  a b   -> parens $ show a ++ " == " ++ show b
    Lt  a b   -> parens $ show a ++ " < " ++ show b
    Mux a b c -> parens $ show a ++ " ? " ++ show b ++ " : " ++ show c
    Exp a     -> parens $ "exp(" ++ show a ++ ")"
    Log a     -> parens $ "log(" ++ show a ++ ")"
    Sqrt a    -> parens $ "sqrt(" ++ show a ++ ")"
    Pow a b   -> parens $ "pow(" ++ show a ++ ", " ++ show b ++ ")"
    Sin a     -> parens $ "sin(" ++ show a ++ ")"
    Cos a     -> parens $ "cos(" ++ show a ++ ")"
    Sinh a    -> parens $ "sinh(" ++ show a ++ ")"
    Cosh a    -> parens $ "cosh(" ++ show a ++ ")"
    Asin a    -> parens $ "asin(" ++ show a ++ ")"
    Acos a    -> parens $ "acos(" ++ show a ++ ")"
    Atan a    -> parens $ "atan(" ++ show a ++ ")"
    Atan2 a b -> parens $ "atan2(" ++ show a ++ ", " ++ show b ++ ")"
    Asinh a   -> parens $ "asinh(" ++ show a ++ ")"
    Acosh a   -> parens $ "acosh(" ++ show a ++ ")"
    Atanh a   -> parens $ "atanh(" ++ show a ++ ")"

instance Show (Var a) where
  show (Var n _) = join n "."

instance Num (Term Int) where
  (Const a) + (Const b) = Const $ a + b
  a + b = Add a b

  (Const a) - (Const b) = Const $ a - b
  a - b = Sub a b

  (Const a) * (Const b) = Const $ a * b
  a * b = Mul a b

  negate a = 0 - a
  abs a = mux (a <. 0) (negate a) a
  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1
  fromInteger i = Const $ fromInteger i

instance Num (Term Float) where
  (Const a) + (Const b) = Const $ a + b
  a + b = Add a b

  (Const a) - (Const b) = Const $ a - b
  a - b = Sub a b

  (Const a) * (Const b) = Const $ a * b
  a * b = Mul a b

  negate a = 0 - a
  abs a = mux (a <. 0) (negate a) a
  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1
  fromInteger i = Const $ fromInteger i

instance Num (Term Double) where
  (Const a) + (Const b) = Const $ a + b
  a + b = Add a b

  (Const a) - (Const b) = Const $ a - b
  a - b = Sub a b

  (Const a) * (Const b) = Const $ a * b
  a * b = Mul a b

  negate a = 0 - a
  abs a = mux (a <. 0) (negate a) a
  signum a = mux (a ==. 0) 0 $ mux (a <. 0) (-1) 1
  fromInteger i = Const $ fromInteger i

instance Fractional (Term Float) where
  (Const a) / (Const b) = Const $ a / b
  a / b = Div a b
  recip a = 1 / a
  fromRational r = Const $ (fromInteger (numerator r)) / (fromInteger (denominator r))

instance Fractional (Term Double) where
  (Const a) / (Const b) = Const $ a / b
  a / b = Div a b
  recip a = 1 / a
  fromRational r = Const $ (fromInteger (numerator r)) / (fromInteger (denominator r))

instance Floating (Term Float) where
  pi       = floatC pi
  exp      (Const a) = Const $ exp a
  exp      a         = Exp a
  log      (Const a) = Const $ log a
  log      a         = Log a
  sqrt     (Const a) = Const $ sqrt a
  sqrt     a         = Sqrt a
  (**)     (Const a) (Const b) = Const $ a ** b
  (**)     a b       = Pow a b
  sin      (Const a) = Const $ sin a
  sin      a         = Sin a
  cos      (Const a) = Const $ cos a
  cos      a         = Cos a
  sinh     (Const a) = Const $ sinh a
  sinh     a         = Sinh a
  cosh     (Const a) = Const $ cosh a
  cosh     a         = Cosh a
  asin     (Const a) = Const $ asin a
  asin     a         = Asin a
  acos     (Const a) = Const $ acos a
  acos     a         = Acos a
  atan     (Const a) = Const $ atan a
  atan     a         = Atan a
  asinh    (Const a) = Const $ asinh a
  asinh    a         = Asinh a
  acosh    (Const a) = Const $ acosh a
  acosh    a         = Acosh a
  atanh    (Const a) = Const $ atanh a
  atanh    a         = Atanh a

instance Floating (Term Double) where
  pi       = doubleC pi
  exp      (Const a) = Const $ exp a
  exp      a         = Exp a
  log      (Const a) = Const $ log a
  log      a         = Log a
  sqrt     (Const a) = Const $ sqrt a
  sqrt     a         = Sqrt a
  (**)     (Const a) (Const b) = Const $ a ** b
  (**)     a b       = Pow a b
  sin      (Const a) = Const $ sin a
  sin      a         = Sin a
  cos      (Const a) = Const $ cos a
  cos      a         = Cos a
  sinh     (Const a) = Const $ sinh a
  sinh     a         = Sinh a
  cosh     (Const a) = Const $ cosh a
  cosh     a         = Cosh a
  asin     (Const a) = Const $ asin a
  asin     a         = Asin a
  acos     (Const a) = Const $ acos a
  acos     a         = Acos a
  atan     (Const a) = Const $ atan a
  atan     a         = Atan a
  asinh    (Const a) = Const $ asinh a
  asinh    a         = Asinh a
  acosh    (Const a) = Const $ acosh a
  acosh    a         = Acosh a
  atanh    (Const a) = Const $ atanh a
  atanh    a         = Atanh a

-- | Constant bool.
boolC :: Bool -> Term Bool
boolC = Const

-- | True term.
true :: Term Bool
true = boolC True

-- | False term.
false :: Term Bool
false = boolC False

-- | Constant int.
intC :: Int -> Term Int
intC = Const

-- | Constant float.
floatC :: Float -> Term Float
floatC = Const

-- | Constant double.
doubleC :: Double -> Term Double
doubleC = Const

-- | Int type casting.
toInt :: NumT a => Term a -> Term Int
toInt = Cast

-- | Double type casting.
toFloat :: NumT a => Term a -> Term Float
toFloat = Cast

-- | Double type casting.
toDouble :: NumT a => Term a -> Term Double
toDouble = Cast


-- | Logical negation.
inv :: Term Bool -> Term Bool
inv a = case a of
  Const False -> true
  Const True  -> false
  Inv a -> a
  a -> Inv a

-- | Logical AND.
(&&.) :: Term Bool -> Term Bool -> Term Bool
(&&.) a b | a == b = a
(&&.) a b = case (a,b) of
  (Const False, _) -> false
  (_, Const False) -> false
  (Const True, b) -> b
  (a, Const True) -> a
  (a,b) -> And a b

-- | Logical OR.
(||.) :: Term Bool -> Term Bool -> Term Bool
(||.) a b = inv $ inv a &&. inv b

-- | The conjunction of a Term Bool list.
and_ :: [Term Bool] -> Term Bool
and_ = foldl (&&.) true

-- | The disjunction of a Term Bool list.
or_ :: [Term Bool] -> Term Bool
or_ = foldl (&&.) false

-- | True iff the predicate is true for all elements.
all_ :: (a -> Term Bool) -> [a] -> Term Bool
all_ f a = and_ $ map f a

-- | True iff the predicate is true for any element.
any_ :: (a -> Term Bool) -> [a] -> Term Bool
any_ f a = or_ $ map f a

-- | Not equal.
(/=.) :: EqT a => Term a -> Term a -> Term Bool
a /=. b = inv (a ==. b)

-- | Less than.
(<.) :: OrdT a => Term a -> Term a -> Term Bool
(Const a) <. (Const b) = Const $ a < b
a <. b | a == b = false
a <. b = Lt a b

-- | Greater than.
(>.) :: OrdT a => Term a -> Term a -> Term Bool
a >. b = b <. a

-- | Less than or equal.
(<=.) :: OrdT a => Term a -> Term a -> Term Bool
a <=. b =  inv (a >. b)

-- | Greater than or equal.
(>=.) :: OrdT a => Term a -> Term a -> Term Bool
a >=. b = inv (a <. b)

-- | Returns the minimum of two numbers.
min_ :: OrdT a => Term a -> Term a -> Term a
min_ a b = mux (a <=. b) a b

-- | Returns the maximum of two numbers.
max_ :: OrdT a => Term a -> Term a -> Term a
max_ a b = mux (a >=. b) a b

-- | Limits between min and max.
limit :: OrdT a => Term a -> Term a -> Term a -> Term a
limit min max a = max_ min $ min_ max a

-- | atan2
atan2_ :: FloatingT a => Term a -> Term a -> Term a
atan2_ (Const a) (Const b) = Const $ atan2 a b
atan2_ a b = Atan2 a b

-- | Division.
div_ :: Term Int -> Term Int -> Term Int
div_ (Const a) (Const b) = Const $ a `div` b
div_ a b = Div a b

-- | Modulo.
mod_ :: Term Int -> Term Int -> Term Int
mod_ (Const a) (Const b) = Const $ a `mod` b
mod_ a b = Mod a b

-- | Returns the value of a 'Var'.
value :: TermT a => Var a -> Term a
value a = Ref a

-- | Conditional expression.
--
-- > mux test onTrue ofFalse
mux :: TermT a => Term Bool -> Term a -> Term a -> Term a
mux _ t f | t == f = f
mux (Const True)  t _ = t
mux (Const False) _ f = f
mux (Inv test) t f = Mux test f t
mux test t f = Mux test t f

-- | A set of all variables referenced in a term.
termVars :: TermT a => Term a -> Set.Set UVar
termVars t = case t of
  Cast a    -> termVars a
  Ref v     -> Set.singleton $ uvar v
  Const _   -> Set.empty
  Input _   -> Set.empty
  Add a b   -> Set.union (termVars a) (termVars b)
  Sub a b   -> Set.union (termVars a) (termVars b)
  Mul a b   -> Set.union (termVars a) (termVars b)
  Div a b   -> Set.union (termVars a) (termVars b)
  Mod a b   -> Set.union (termVars a) (termVars b)
  Inv a     -> termVars a
  And a b   -> Set.union (termVars a) (termVars b)
  Eq  a b   -> Set.union (termVars a) (termVars b)
  Lt  a b   -> Set.union (termVars a) (termVars b)
  Mux a b c -> Set.unions [(termVars a), (termVars b), (termVars c)]
  Exp a     -> termVars a
  Log a     -> termVars a
  Sqrt a    -> termVars a
  Pow a b   -> Set.union (termVars a) (termVars b)
  Sin a     -> termVars a
  Cos a     -> termVars a
  Sinh a    -> termVars a
  Cosh a    -> termVars a
  Asin a    -> termVars a
  Acos a    -> termVars a
  Atan a    -> termVars a
  Atan2 a b -> Set.union (termVars a) (termVars b)
  Asinh a   -> termVars a
  Acosh a   -> termVars a
  Atanh a   -> termVars a