-- This module implements abstract interpretation of numerical
-- operations on Term objects by implementing the number classes for
-- the Term object.

-- Some algebraic manipulation and constant reductions are performed
-- based on the CT datatype.

module Ai () where

    


import Term     -- Syntax data structure
import Cas      -- Algebraic manipulations
import Complex

-- Abstract Interpretation

op name as = Op (Sym name) as

binop code fn a b =
    case [a,b] of
      [(Lit a), (Lit b)] -> lit (fn a b)
      as -> op code as

unop code fn a =
    case [a] of
      [(Lit a)] -> lit (fn a)
      as -> op code as




--- Type class instances to treat Term as number
instance (Eq a, Num a) => Num (Term a)
    where
      (+) = ctAdd -- binop "add" (+)
      (*) = ctMul -- binop "mul" (*)
      abs = unop "abs" (abs)
      signum = unop "signum" (signum)
      negate = unop "negate" (negate)
      fromInteger = lit . fromInteger

instance (Fractional a) => Fractional (Term a)
    where
      (/) = binop "div" (/)
      fromRational = lit . fromRational

instance (Floating a) => Floating (Term a)
    where
      logBase = binop "logBase" (logBase)
      (**) = binop "**" (**) 
      exp = unop "exp" exp 
      log = unop "log" log
      sqrt = unop "sqrt" sqrt
      sin = unop "sin" sin
      cos = unop "cos" cos
      tan = unop "tan" tan
      asin = unop "asin" asin
      acos = unop "acos" acos
      atan = unop "atan" atan
      sinh = unop "sinh" sinh
      cosh = unop "cosh" cosh
      tanh = unop "tanh" tanh
      asinh = unop "asinh" asinh
      acosh = unop "acosh" acosh
      atanh = unop "atanh" atanh
      pi = lit pi

instance (Ord a) => Ord (Term a)

-- Terms can not be converted to numbers in general, so this throws an
-- error for non-literal terms.
forLit f = g where
    g (Lit x) = f x
    g _ =  error "forLit: not a literal"


instance (Real a) => Real (Term a) where
    toRational = forLit toRational

instance (RealFrac a) => RealFrac (Term a) where
    properFraction = error "properFraction" -- forLit properFraction 

instance (RealFloat a) => RealFloat (Term a) where
    floatRadix = forLit floatRadix
    floatDigits = forLit floatDigits
    floatRange = forLit floatRange
    decodeFloat = forLit decodeFloat
    encodeFloat = f where f a b = lit (encodeFloat a b)
    isNaN = forLit isNaN
    isInfinite = forLit isInfinite
    isDenormalized = forLit isDenormalized
    isNegativeZero = forLit isNegativeZero
    isIEEE = forLit isIEEE

-- Algebraic manipulations using CT as an intermediate representation.
type ITerm a = CT a (Term a)
type CTBinop a = ITerm a -> ITerm a -> ITerm a


-- Given a CT domain transform pair (abstracting computation in CT
-- domain), lift a binary operator on a to work on Term a.
type Binop  a = a -> a -> a
type TBinop a = Term a -> Term a -> Term a
type CTtx   a = (Term a -> ITerm a, ITerm a -> Term a)

ctLift :: Num a => CTtx a -> Binop a -> TBinop a
ctLift (ct, ict) binop = f where 
    (<*>) = ctOp binop                -- lift Binop to CTBinop
    f a b = ict ((ct a) <*> (ct b))   -- pullback to yield TBinop

-- Transforms to/from CT domain in terms of opcode, zero and unit.
ct  :: Num a => Sym -> (a -> Bool) -> (a -> Bool) -> Term a -> ITerm a
ict :: Num a => Sym -> Term a -> Term a -> ITerm a -> Term a

ct opcode isz isu = f where
    f (Lit l) | isz l = Z
    f (Lit l) | isu l = U
    f (Lit l) = L l
    f (Op o [Lit a,b]) | (o == opcode) = L a :<*>: T b
    f t = T t

ict opcode z u = f where
    f Z = z
    f U = u
    f (L l) = Lit l
    f (T t) = t
    f (a :<*>: b) = Op opcode [(f a), (f b)]


-- Lifted operations for use in the Num instance.
ctAdd :: Num a => TBinop a
ctAdd = ctLift (ct', ict') (+) where
    opc    = Sym "add"      -- symbol for matching
    ct'    = ct  opc (\_ -> False)       (0 ==)
    ict'   = ict opc (Var (Sym "<inf>")) (Lit 0)

ctMul :: Num a => TBinop a
ctMul = ctLift (ct', ict') (*) where
    opc    = Sym "mul"
    ct'    = ct  opc (0 ==)  (1 ==)
    ict'   = ict opc (Lit 0) (Lit 1)