{-# LANGUAGE UndecidableInstances, OverloadedStrings, TupleSections, RankNTypes, FlexibleInstances, LambdaCase #-}

module Funcons.Operations.Values where

import qualified Data.Map as M
import qualified Data.Vector as V
import qualified Data.Set as S
import qualified Data.BitVector as BV
import qualified Data.MultiSet as MS

import qualified Data.Char as C
import Data.Text (Text, pack, unpack)
import Data.List (intercalate)
import Data.Maybe (fromJust)
import Data.String

import Control.Monad (liftM2)
import Control.Arrow ((***))

type Name = Text
type MVar = String

-- | 
-- This datatype provides a number of builtin value types.
-- The type `t` is expected to be a super-type of `Values t`,
-- such that there is a projection and injection between `t` and `Values t`,
-- (see 'HasValues')
-- Values forms a functor over the type `t` and provides a generic way of
-- comparing values (see `zipWithT`) for example to realise pattern matching 
data Values t   = ADTVal Name [t]
                | Ascii Char 
                | Atom String
                | Bit BV.BitVector
                | Char Char
                | ComputationType (ComputationTypes t)
                | Float Double 
                | IEEE_Float_32 Float
                | IEEE_Float_64 Double
                | Int Integer
                | Map (ValueMaps (Values t))
                | Multiset (MS.MultiSet (Values t))
                | Nat Integer
                | Rational Rational
                | Set (ValueSets (Values t))
                | Vector (ValueVectors (Values t))
                | VMeta (TaggedSyntax t)
                | VAny -- used whenever funcon terms may have holes in them
                       -- currently only the case in "downwards" flowing signals
        deriving (Eq,Ord,Show,Read)

tuple :: HasValues t => [Values t] -> Values t
tuple = ADTVal "tuple" . map inject

list :: HasValues t => [Values t] -> Values t
list = ADTVal "list" . map inject

instance HasValues t => IsString (Values t) where
  fromString = ADTVal "list" . map (inject . Ascii)

data TaggedSyntax t = TagName Name [Values t]
                    | TagType (Types t) (Values t)
                  deriving (Eq, Ord, Show, Read)

type ValueMaps t      = M.Map t t 
type ValueSets t      = S.Set t
type ValueVectors t   = V.Vector t

-- | Postfix operators for specifying sequences.
data SeqSortOp = StarOp | PlusOp | QuestionMarkOp
                deriving (Show, Eq, Ord, Read)


-- | Computation type /S=>T/ reflects a type of term
-- whose given value is of type /S/ and result is of type /T/.
data ComputationTypes t = Type (Types t) -- | /=>T/
                        | ComputesType (Types t) -- | /S=>T/
                        | ComputesFromType (Types t) (Types t)
                        deriving (Ord,Eq,Show, Read)

-- | Representation of builtin types.
data Types t= ADTs
            | ADT Name [t]
            | AnnotatedType (Types t) SeqSortOp
            | AsciiCharacters
            | Atoms
            | Bits Int
            | IntegersFrom Integer -- value-dependent type
            | IntegersUpTo Integer
            | Characters
            | Complement (Types t)
            | ComputationTypes
            | EmptyType
            | GroundValues
            | IEEEFloats IEEEFormats
            | Integers
            | Intersection (Types t) (Types t)
            | Maps (Types t) (Types t)
            | Multisets (Types t)
            | Naturals
            | Nothings
            | Rationals
            | Sets (Types t)
            | Strings
            | Types
            | UnicodeCharacters
            | Union (Types t) (Types t)
            | DefinedValues 
            | Values
            | Vectors (Types t)
            -- extension for meta-programming (see Funcons.MetaProgramming)
            | ASTs
              deriving (Ord,Eq,Show,Read)


class HasValues t where
  project :: t -> Maybe (Values t)
  inject  :: Values t -> t
class HasComputationTypes t where
  projectCT :: t -> Maybe (ComputationTypes t)
  injectCT  :: ComputationTypes t -> t
class HasTypes t where
  projectT  :: t -> Maybe (Types t)
  injectT   :: Types t -> t
instance HasValues t => HasComputationTypes t where
  projectCT v = project v >>= \case
                ComputationType t -> Just t
                _      -> Nothing
                
  injectCT  = inject . ComputationType
instance HasComputationTypes t => HasTypes t where
  projectT ct = projectCT ct >>= \case 
                  Type t -> Just t 
                  _      -> Nothing
  injectT = injectCT . Type

data IEEEFormats = Binary32 | Binary64
        deriving (Enum,Show,Eq,Ord,Read)

-- Specialised version of 'fmap'
vmap :: (Ord b) => (a -> b) -> Values a -> Values b
vmap f v = case v of
    ADTVal nm ts      -> ADTVal nm (map f ts)
    Ascii a           -> Ascii a
    Atom a            -> Atom a
    Bit b             -> Bit b
    Char c            -> Char c
    ComputationType t -> ComputationType (fmap f t)
    Float f           -> Float f
    IEEE_Float_32 f   -> IEEE_Float_32 f
    IEEE_Float_64 f   -> IEEE_Float_64 f
    Int i             -> Int i
    Map m             -> Map $ M.fromList $ map (vmap f *** vmap f) $ M.assocs m
    Set s             -> Set $ S.map (vmap f) s
    Multiset ms       -> Multiset $ MS.map (vmap f) ms
    Nat n             -> Nat n
    Rational r        -> Rational r
    Vector v          -> Vector $ V.map (vmap f) v
    VMeta ts          -> VMeta $ vmapTS f ts
    VAny              -> VAny

vmapTS :: (Ord b) => (a -> b) -> TaggedSyntax a -> TaggedSyntax b
vmapTS f ts = case ts of
    TagName nm vs -> TagName nm (map (vmap f) vs)
    TagType t v   -> TagType (fmap f t) (vmap f v) 
  
traverseV :: (Ord b, Monad m, HasValues a, HasValues b) => 
  (a -> m b) -> Values a -> m (Values b)
traverseV f = traverseVM f (mapM f)

traverseVM :: (Ord b, Monad m, HasValues a, HasValues b) => 
  (a -> m b) -> ([a] -> m [b]) -> Values a -> m (Values b)
traverseVM f fs v = case v of
    ADTVal nm vs      -> return . ADTVal nm =<< fs vs
    Ascii a           -> return $ Ascii a
    Atom a            -> return $ Atom a
    Bit b             -> return $ Bit b
    Char c            -> return $ Char c
    ComputationType t -> return . ComputationType   =<< traverseCTM f fs t
    Float f           -> return $ Float f
    IEEE_Float_32 f   -> return $ IEEE_Float_32 f
    IEEE_Float_64 f   -> return $ IEEE_Float_64 f
    Int i             -> return $ Int i
    Map m             -> do 
        let (keys, vals) = unzip (M.assocs m)
        keys' <- map (fromJust . project) <$> fs (map inject keys)
        vals' <- map (fromJust . project) <$> fs (map inject vals)
        return (Map $ M.fromList $ zip keys' vals')
    Set s             -> return . Set . S.fromList . map (fromJust . project) =<< fs (map inject $ S.toList s)
    Multiset ms       -> return . Multiset . MS.fromList . map (fromJust . project) =<< fs (map inject $ MS.toList ms)
    Nat n             -> return $ Nat n
    Rational r        -> return $ Rational r
    Vector v          -> return . Vector . V.fromList . map (fromJust . project) =<< fs (map inject $ V.toList v)
    VMeta ts -> VMeta <$> traverseTSM f fs ts
    VAny -> return VAny

traverseT :: (Ord b, Monad m, HasValues a, HasValues b) => 
  (a -> m b) -> Types a -> m (Types b)
traverseT f = traverseTM f (mapM f)
traverseTM :: (Ord b, Monad m, HasValues a, HasValues b) => 
  (a -> m b) -> ([a] -> m [b]) -> Types a -> m (Types b)
traverseTM f fs t = case t of
  ADTs -> return ADTs
  ADT nm ts -> return . ADT nm =<< fs ts
  AsciiCharacters -> return AsciiCharacters
  Atoms ->  return Atoms
  AnnotatedType ty op -> AnnotatedType <$> traverseTM f fs ty <*> return op
  ASTs -> return ASTs
  Bits i -> return (Bits i)
  Characters -> return Characters
  ComputationTypes -> return ComputationTypes
  Complement t -> Complement <$> traverseTM f fs t  
  DefinedValues -> return DefinedValues
  GroundValues -> return GroundValues
  IntegersFrom f -> return (IntegersFrom f)
  IntegersUpTo f -> return (IntegersUpTo f)
  Intersection t1 t2 -> Intersection <$> traverseTM f fs t1 <*> traverseTM f fs t2
  Nothings -> return Nothings
  EmptyType -> return EmptyType
  IEEEFloats i -> return (IEEEFloats i)
  Integers -> return Integers
  Maps t1 t2 -> Maps <$> traverseTM f fs t1 <*> traverseTM f fs t2
  Multisets t -> Multisets <$> traverseTM f fs t
  Naturals -> return Naturals
  Rationals -> return Rationals
  Sets t -> Sets <$> traverseTM f fs t
  Strings -> return Strings
  Types -> return Types 
  UnicodeCharacters -> return UnicodeCharacters
  Union t1 t2 -> Union <$> traverseTM f fs t1 <*> traverseTM f fs t2
  Values -> return Values
  Vectors t -> Vectors <$> traverseTM f fs t 

traverseTSM f fs t = case t of
  TagName nm vs -> TagName nm <$> traverse (traverseVM f fs) vs
  TagType ty v  -> TagType <$> traverseTM f fs ty <*> traverseVM f fs v

traverseCTM f fs t = case t of
  Type t -> Type <$> traverseTM f fs t
  ComputesType t -> ComputesType <$> traverseTM f fs t
  ComputesFromType ty ty2 -> ComputesFromType <$> traverseTM f fs ty
                                              <*> traverseTM f fs ty2

structVcompare :: (Monoid m, HasValues a, HasValues b) => 
  (a -> b -> Maybe m) -> Values a -> Values b -> Maybe (Maybe m)
structVcompare comp = structVMcompare comp comps
  where comps xs ys | length xs == length ys = fmap mconcat $ sequence $ zipWith comp xs ys
                    | otherwise = Nothing

structCTMcompare :: (Monoid m, HasValues a, HasValues b) => 
  (a -> b -> Maybe m) -> ([a] -> [b] -> Maybe m) ->
    ComputationTypes a -> ComputationTypes b -> (Maybe (Maybe m))
structCTMcompare comp comps va vb = case (va,vb) of
  (Type x, Type y)  -> structTMcompare comp comps x y 
  (Type _,_)        -> Nothing
  (_, Type _)       -> Nothing
  (ComputesType x, ComputesType y)  -> structTMcompare comp comps x y 
  (ComputesType _, _)               -> Nothing 
  (_, ComputesType _)               -> Nothing
  (ComputesFromType x y, ComputesFromType x' y') -> 
    liftM2 mappend (structTMcompare comp comps x x') (structTMcompare comp comps y y')

structVMcompare :: (Monoid m, HasValues b, HasValues a) => 
  (a -> b -> Maybe m) -> ([a] -> [b] -> Maybe m) -> 
    Values a -> Values b -> Maybe (Maybe m)
structVMcompare comp comps va vb = case (va, vb) of
  (ADTVal nm1 vs1, ADTVal nm2 vs2) 
    | nm1 == nm2 -> Just $ comps vs1 vs2
  (ADTVal _ _, _) -> Nothing
  (_, ADTVal _ _) -> Nothing
  (Ascii x, Ascii u) | x == u -> Just (Just mempty)
  (Ascii _, _)                -> Nothing
  (_, Ascii _)                -> Nothing
  (Atom x, Atom y) | x == y   -> Just (Just mempty)
  (Atom _, _)                 -> Nothing
  (_, Atom _)                 -> Nothing
  (Bit x, Bit y)  | x == y    -> Just (Just mempty)
  (_, Bit _)                  -> Nothing
  (Bit _, _)                  -> Nothing
  (Char x, Char y) | x == y   -> Just (Just mempty)
  (Char _, _)                 -> Nothing
  (_, Char _)                 -> Nothing
  (ComputationType x
    ,ComputationType y)       -> structCTMcompare comp comps x y 
  (_, ComputationType x)      -> Nothing
  (ComputationType _, _)      -> Nothing
  (Float x, Float y) | x == y -> Just (Just mempty)
  (Float _, _)                -> Nothing
  (_, Float _)                -> Nothing
  (IEEE_Float_32 x, IEEE_Float_32 y) | x == y -> Nothing
  (IEEE_Float_32 _, _)                        -> Nothing
  (_, IEEE_Float_32 _)                        -> Nothing
  (IEEE_Float_64 x, IEEE_Float_64 y) | x == y -> Nothing
  (IEEE_Float_64 _, _)                        -> Nothing
  (_, IEEE_Float_64 _)                        -> Nothing
  (Int x, Int y) | x == y                     -> Just (Just mempty)
  (Int _, _)                                  -> Nothing
  (_, Int _)                                  -> Nothing
  (Map m1, Map m2) -> Just $ liftM2 mappend (comps (map inject (M.keys m1)) 
                                                   (map inject (M.keys m2)))
                                            (comps (map inject (M.elems m1)) 
                                                   (map inject (M.elems m2)))
  (Map _, _)      -> Nothing
  (_, Map _)      -> Nothing
  (Set x, Set y) -> Just $ comps (map inject $ S.toList x) (map inject $ S.toList y)  
  (Set _, _)      -> Nothing
  (_, Set _)      -> Nothing
  (Multiset x, Multiset y) -> Just $ comps (map inject $ MS.toList x) 
                                           (map inject $ MS.toList y)
  (Multiset _, _)           -> Nothing
  (_, Multiset _)           -> Nothing
  (Nat x, Nat y)  | x == y  -> Just (Just mempty)
  (Nat _, _)                -> Nothing
  (_, Nat _)                -> Nothing
  (Rational x, Rational y) | x == y -> Just (Just mempty)
  (Rational _, _)                   -> Nothing
  (_, Rational _)                   -> Nothing
  (Vector x, Vector y) -> Just $ comps (map inject $ V.toList x) (map inject $ V.toList y)
  (VAny, VAny)  -> Just (Just mempty)
  (_, VAny)     -> Nothing
  (VAny, _)     -> Nothing
  (VMeta ts, VMeta ts') -> structTSMcompare comp comps ts ts' 
  (VMeta _, _)  -> Nothing
  (_, VMeta _)  -> Nothing

structTSMcompare comp comps ts ts' = case (ts,ts') of
  (TagName nm vs, TagName nm' vs') | nm == nm' -> 
    Just $ comps (map inject vs) (map inject vs')  
  (TagName _ _, _) -> Nothing
  (_, TagName _ _) -> Nothing
  (TagType ty v, TagType ty' v') -> 
    liftM2 (liftM2 mappend) (structTMcompare comp comps ty ty')
                            (structVMcompare comp comps v v')

structTMcompare :: (Monoid m, HasValues a, HasValues b) => 
  (a -> b -> Maybe m) -> ([a] -> [b] -> Maybe m) -> 
    Types a -> Types b -> Maybe (Maybe m)
structTMcompare comp comps ta tb = case (ta, tb) of
  (ADTs, ADTs)                        -> Just (Just mempty)
  (ADTs, _)                           -> Nothing
  (_, ADTs)                           -> Nothing
  (ADT nm1 ts, ADT nm2 ts') | nm1 == nm2 -> Just $ comps ts ts'
  (ADT _ _, _)                        -> Nothing
  (_, ADT _ _)                        -> Nothing
  (Atoms, Atoms)                      -> Just (Just mempty)
  (Atoms, _)                          -> Nothing
  (_, Atoms)                          -> Nothing
  (AsciiCharacters, AsciiCharacters)  -> Just (Just mempty) 
  (AsciiCharacters, _)                -> Nothing
  (_, AsciiCharacters)                -> Nothing
  (ASTs, ASTs)                        -> Just (Just mempty)
  (_, ASTs)                           -> Nothing
  (ASTs, _)                           -> Nothing
  (AnnotatedType t1 op1, AnnotatedType t2 op2) | op1 == op2 -> structTMcompare comp comps t1 t2
  (AnnotatedType _ _, _)              -> Nothing
  (_, AnnotatedType _ _)              -> Nothing
  (Bits x, Bits y)  | x == y          -> Just (Just mempty)
  (Bits _, _)                         -> Nothing
  (_, Bits _)                         -> Nothing
  (Characters, Characters)            -> Just (Just mempty)
  (Characters, _)                     -> Nothing
  (_, Characters)                     -> Nothing
  (Complement x, Complement y)        -> structTMcompare comp comps x y
  (_, Complement _)                   -> Nothing
  (Complement _, _)                   -> Nothing
  (ComputationTypes, ComputationTypes)-> Just (Just mempty)
  (_, ComputationTypes)               -> Nothing
  (ComputationTypes, _)               -> Nothing
  (DefinedValues, DefinedValues)      -> Just (Just mempty)
  (_, DefinedValues)                  -> Nothing
  (DefinedValues, _)                  -> Nothing
  (GroundValues, GroundValues)        -> Just (Just mempty)
  (GroundValues, _)                   -> Nothing
  (_, GroundValues)                   -> Nothing
  (IntegersFrom mx, IntegersFrom mx') | mx == mx' -> Just (Just mempty)
  (IntegersFrom _, _)                 -> Nothing
  (_, IntegersFrom _)                 -> Nothing
  (IntegersUpTo mx, IntegersUpTo mx') | mx == mx' -> Just (Just mempty)
  (IntegersUpTo _, _)                   -> Nothing
  (_, IntegersUpTo _)                   -> Nothing
  (EmptyType, EmptyType)              -> Just (Just mempty)
  (_, EmptyType)                      -> Nothing
  (EmptyType, _)                      -> Nothing
  (IEEEFloats x, IEEEFloats y) | x ==y-> Just (Just mempty)
  (IEEEFloats _, _)                   -> Nothing
  (_, IEEEFloats _)                   -> Nothing
  (Maps k v, Maps k' v')              -> liftM2 mappend (structTMcompare comp comps k k') (structTMcompare comp comps v v')
  (Maps _ _, _)                       -> Nothing
  (_, Maps _ _)                       -> Nothing
  (Integers, Integers)                -> Just (Just mempty)
  (Integers, _)                       -> Nothing
  (_, Integers)                       -> Nothing
  (Intersection x y, Intersection x' y') -> liftM2 mappend (structTMcompare comp comps x x') (structTMcompare comp comps y y')
  (Intersection _ _, _)               -> Nothing
  (_, Intersection _ _)               -> Nothing
  (Multisets x, Multisets y)          -> structTMcompare comp comps x y
  (Multisets _, _)                    -> Nothing
  (_, Multisets _)                    -> Nothing
  (Naturals, Naturals)                -> Just (Just mempty)
  (_, Naturals)                       -> Nothing
  (Naturals, _)                       -> Nothing
  (Nothings, Nothings)                -> Just (Just mempty)
  (_, Nothings)                       -> Nothing
  (Nothings,_)                        -> Nothing
  (Rationals, Rationals)              -> Just (Just mempty)
  (Rationals, _)                      -> Nothing
  (_, Rationals)                      -> Nothing
  (Strings, Strings)                  -> Just (Just mempty) 
  (_, Strings)                        -> Nothing
  (Strings, _)                        -> Nothing
  (Sets x, Sets y)                    -> structTMcompare comp comps x y
  (Sets _, _)                         -> Nothing
  (_, Sets _)                         -> Nothing
  (Types, Types)                      -> Just (Just mempty)
  (_, Types)                          -> Nothing
  (Types, _)                          -> Nothing
  (UnicodeCharacters, UnicodeCharacters)  -> Just (Just mempty)
  (UnicodeCharacters, _)                  -> Nothing
  (_, UnicodeCharacters)                  -> Nothing
  (Union u v, Union x y)                  -> liftM2 mappend (structTMcompare comp comps u x) (structTMcompare comp comps v y)
  (Union _ _, _)                          -> Nothing
  (_, Union _ _)                          -> Nothing
  (Values, Values)                        -> Just (Just mempty)
  (_, Values)                             -> Nothing
  (Values, _)                             -> Nothing
  (Vectors x, Vectors y)                  -> structTMcompare comp comps x y

instance Functor Types where
  fmap f t = case t of 
    ADT nm ts           -> ADT nm (map f ts) 
    ADTs                -> ADTs
    AsciiCharacters     -> AsciiCharacters
    Atoms               -> Atoms
    AnnotatedType ty op -> AnnotatedType (fmap f ty) op
    ASTs                -> ASTs
    Bits n              -> Bits n
    Complement t1       -> Complement (fmap f t1)
    ComputationTypes    -> ComputationTypes
    DefinedValues       -> DefinedValues  
    GroundValues        -> GroundValues
    IntegersFrom p      -> IntegersFrom p
    IntegersUpTo p      -> IntegersUpTo p
    Characters          -> Characters   
    EmptyType           -> EmptyType
    IEEEFloats b        -> IEEEFloats b
    Integers            -> Integers
    Intersection t1 t2  -> Intersection (fmap f t1) (fmap f t2)
    Maps k v            -> Maps (fmap f k) (fmap f v) 
    Multisets t         -> Multisets (fmap f t)
    Naturals            -> Naturals
    Nothings            -> Nothings
    Rationals           -> Rationals
    Sets t              -> Sets (fmap f t)
    Strings             -> Strings
    Types               -> Types
    UnicodeCharacters   -> UnicodeCharacters
    Union t1 t2         -> Union (fmap f t1) (fmap f t2)
    Values              -> Values 
    Vectors t           -> Vectors (fmap f t)

instance Functor ComputationTypes where
  fmap f t = case t of
    Type t -> Type $ fmap f t
    ComputesType t -> ComputesType $ fmap f t
    ComputesFromType t1 t2 -> ComputesFromType (fmap f t1) (fmap f t2)

instance Foldable Types where
  foldMap f fa = case fa of 
    ADT _ ts            -> foldMap f ts
    ADTs                -> mempty
    AsciiCharacters     -> mempty
    Atoms               -> mempty
    ASTs                -> mempty
    AnnotatedType ty op -> foldMap f ty
    Bits _              -> mempty
    Characters          -> mempty
    Complement t1       -> foldMap f t1
    ComputationTypes    -> mempty
    DefinedValues       -> mempty
    GroundValues        -> mempty
    IntegersUpTo q      -> mempty
    IntegersFrom q      -> mempty
    Intersection t1 t2  -> foldMap f t1 `mappend` foldMap f t2
    EmptyType           -> mempty
    IEEEFloats b        -> mempty 
    Integers            -> mempty
    Maps k v            -> foldMap f k `mappend` foldMap f v
    Multisets t         -> foldMap f t
    Naturals            -> mempty 
    Nothings            -> mempty
    Rationals           -> mempty
    Sets t              -> foldMap f t
    Strings             -> mempty
    Types               -> mempty 
    UnicodeCharacters   -> mempty 
    Union t1 t2         -> foldMap f t1 `mappend` foldMap f t2
    Values              -> mempty 
    Vectors t           -> foldMap f t

instance Traversable Types where
  traverse f ta = case ta of 
    ADTs                -> pure ADTs
    ADT nm ts           -> ADT nm <$> traverse f ts
    AsciiCharacters     -> pure AsciiCharacters
    AnnotatedType ty op -> AnnotatedType <$> traverse f ty <*> pure op
    Atoms               -> pure Atoms
    ASTs                -> pure ASTs
    Bits n              -> pure $ Bits n
    Characters          -> pure Characters
    Complement t        -> Complement <$> traverse f t
    ComputationTypes    -> pure ComputationTypes
    DefinedValues       -> pure DefinedValues
    GroundValues        -> pure GroundValues 
    IntegersFrom n      -> pure $ IntegersFrom n
    IntegersUpTo n        -> pure $ IntegersUpTo n
    EmptyType           -> pure EmptyType
    IEEEFloats b        -> pure $ IEEEFloats b
    Integers            -> pure Integers
    Intersection t1 t2  -> Intersection <$> traverse f t1 <*> traverse f t2
    Maps k v            -> Maps <$> traverse f k <*> traverse f v
    Multisets t         -> Multisets <$> traverse f t
    Naturals            -> pure Naturals
    Nothings            -> pure Nothings
    Rationals           -> pure Rationals
    Sets t              -> Sets <$> traverse f t
    Strings             -> pure Strings
    Types               -> pure Types
    UnicodeCharacters   -> pure UnicodeCharacters
    Union t1 t2         -> Union <$> traverse f t1 <*> traverse f t2
    Values              -> pure Values 
    Vectors t           -> Vectors <$> traverse f t

downcastValueType :: Values t -> Types t
downcastValueType (ComputationType (Type t)) = t
downcastValueType (ComputationType (ComputesType t)) = t
downcastValueType (ComputationType (ComputesFromType _ t)) = t
downcastValueType _ = error "valueType: not a type"

-- | Returns the /rational/ representation of a value if it is a subtype.
-- Otherwise it returns the original value.
upcastRationals :: Values t -> Values t
upcastRationals (Nat n) = Rational (toRational n)
upcastRationals (Int i) = Rational (toRational i)
upcastRationals v       = v

-- | Returns the /integer/ representation of a value if it is a subtype.
-- Otherwise it returns the original value.
upcastIntegers :: Values t -> Values t
upcastIntegers (Nat n)  = Int n
upcastIntegers v        = v

-- | Returns the /natural/ representation of a value if it is a subtype.
-- Otherwise it returns the original value.
upcastNaturals :: Values t -> Values t
upcastNaturals (Int i) | i >= 0 = Nat i
upcastNaturals v = v

-- | Returns the /unicode/ representation of an assci value.
-- Otherwise it returns the original value.
upcastUnicode :: Values t -> Values t
upcastUnicode (Ascii c) = Char c
upcastUnicode v = v

castType :: HasValues t => Values t -> Maybe (Types t)
castType (ComputationType (Type ty)) = Just ty
castType (ComputationType (ComputesType ty)) = Just ty
castType (ComputationType (ComputesFromType _ ty)) = Just ty
castType _            = Nothing

-- numbers
mk_integers :: Integer -> Values t
mk_integers i   | i >= 0    = mk_naturals i
                | otherwise = Int i

mk_naturals :: Integer -> Values t
mk_naturals = Nat

mk_unicode_characters :: Char -> Values t
mk_unicode_characters c  | C.isAscii c = mk_ascii_characters c
                         | otherwise   = Char c

-- TODO: haven't included `basic-characters` in the subtyping heirarchy yet.

mk_ascii_characters :: Char -> Values t
mk_ascii_characters = Ascii

--- Value specific

(===) :: (HasValues t, Eq t {- UNNECESSARY CONSTRAINT -}) => Values t -> Values t -> Bool
v1 === v2 = isGround v1 && isGround v2 && (v1 == v2)

(=/=) :: (HasValues t, Eq t {- UNNECESSARY CONSTRAINT -}) => Values t -> Values t -> Bool
v1 =/= v2 = isGround v1 && isGround v2 && (v1 /= v2)

isGround :: HasValues t => Values t -> Bool
isGround (ADTVal _ mv)            = all (maybe False isGround . project) mv
isGround (Ascii _)                = True
isGround (Atom _)                 = True
isGround (Bit _)                  = True
isGround (Char _)                 = True
isGround (Float _)                = True
isGround (IEEE_Float_32 _)        = True
isGround (IEEE_Float_64 _)        = True
isGround (Int _)                  = True
isGround (Map m)                  = all isGround (M.elems m)
isGround (Multiset ms)            = all isGround (MS.elems ms)
isGround (Nat _)                  = True
isGround (ComputationType _)      = True
isGround (Rational _)             = True
isGround (Set s)                  = all isGround (S.toList s)
isGround (Vector v)               = all isGround (V.toList v)
isGround (VMeta _)                = True
isGround VAny                     = False

-- functions that check simple properties of funcons
-- TODO: Some of these are used, and all are exported by Funcons.EDSL
--       But are all of them still needed.  E.g isId doesn't seem very useful now that ids are just strings.
isAscii ((Ascii _))                 = True
isAscii _                           = False
isChar ((Char _))                   = True
isChar _                            = False
isNat ((Int _))                     = True
isNat _                             = False
isInt ((Int _))                     = True
isInt _                             = False
isEnv f                             = isMap f
isMap ((Map _))                     = True
isMap _                             = False
isSet ((Set _))                     = True
isSet _                             = False
isString_ :: HasValues t => Values t -> Bool
isString_ (ADTVal "list" vs)        = not (null vs) && all (maybe False isAscii) (map project vs)
isString_ _                         = False
isType (ComputationType _)          = True
isType _                            = False
isVec ((Vector _))                  = True
isVec _                             = False

unString :: HasValues t => Values t -> String
unString (ADTVal "list" vs) 
  | Just vs' <- sequence (map project vs), all isAscii vs' = map (\(Ascii c) -> c) vs'
unString _ = error "unString"

none__ :: Values t
none__ = ADTVal "none" []

isNoValue :: Values t -> Bool
isNoValue (ADTVal "none" _) = True
isNoValue _ = False

isDefinedVal :: Values t -> Bool
isDefinedVal f = not (isNoValue f)

set_ :: Ord t => [Values t] -> Values t
set_ = Set . S.fromList 

ppValues :: HasValues t => (t -> String) -> Values t -> String
ppValues showT v@(ADTVal "list" vs)
  | isString_ v = show (unString v)
  | otherwise   = "[" ++ showArgs_ (map showT vs) ++ "]"
ppValues showT (ADTVal c []) = unpack c
ppValues showT (ADTVal c vs) = unpack c ++ showArgs (map showT vs)
ppValues showT (Atom c)       = "atom("++ c ++")"
ppValues showT (Ascii c)      = "`" ++ [c] ++ "`"
ppValues showT (Bit i)        = "bits(" ++ show (BV.size i)
                                            ++ ", " ++ show (BV.int i) ++ ")"
ppValues showT (Char c)       = show c
ppValues showT (Float f)      = show f
-- rationals
ppValues showT (IEEE_Float_32 f) = show f
ppValues showT (IEEE_Float_64 d) = show d
ppValues showT (Rational r)   = show r
ppValues showT (Int f)        = show f
ppValues showT (Nat f)        = show f
ppValues showT (Map m)        = if M.null m then "map-empty"
                               else "{" ++ key_values ++ "}"
 where key_values = intercalate ", " (map (\(k,v) -> ppValues showT k++" |-> "++ 
                                                     ppValues showT v)$ M.toList m)
ppValues showT (Multiset s) = "{" ++ showArgs (map (ppValues showT) (MS.toList s)) ++ "}"
ppValues showT (Set s) =  "{" ++ showArgs (map (ppValues showT) (S.toList s)) ++ "}"
ppValues showT (Vector v) =  "vector" ++ showArgs (map (ppValues showT) (V.toList v))
ppValues showT (ComputationType ty) = ppComputationTypes showT ty
ppValues showT VAny = "_"
ppValues showT (VMeta ts) = ppTaggedSyntax showT ts

ppTaggedSyntax :: HasValues t => (t -> String) -> TaggedSyntax t -> String
ppTaggedSyntax showT (TagName nm vs) = "astv" ++ showArgs (unpack nm : map (ppValues showT) vs)
ppTaggedSyntax showT (TagType ty val) = "astv" ++ showArgs [ppTypes showT ty, ppValues showT val]

ppComputationTypes :: HasValues t => (t -> String) -> ComputationTypes t -> String
ppComputationTypes showT (Type t) = ppTypes showT t
ppComputationTypes showT (ComputesType ty) = "=>" ++ ppTypes showT ty
ppComputationTypes showT (ComputesFromType s t) = ppTypes showT s ++ "=>" ++ ppTypes showT t

ppTypes :: HasValues t => (t -> String) -> Types t -> String
ppTypes showT (AnnotatedType ty op)  = ppTypes showT ty ++ ppOp op
ppTypes showT (Complement ty)        = "~(" ++ ppTypes showT ty ++ ")"
ppTypes showT ComputationTypes       = "computation-types"
ppTypes showT GroundValues           = "ground-values"
ppTypes showT Nothings               = "nothing"
ppTypes showT DefinedValues          = "defined-values"
ppTypes showT ASTs                   = "asts"
ppTypes showT Atoms                  = "atoms"
ppTypes showT AsciiCharacters        = "ascii-characters"
ppTypes showT Characters             = "characters"
ppTypes showT (Intersection t1 t2)   = "(" ++ ppTypes showT t1 ++ "^" ++ ppTypes showT t2 ++")"
ppTypes showT (IntegersFrom n)       = "integers-from(" ++ show n ++ ")"
ppTypes showT (IntegersUpTo n)       = "integers-to(" ++ show n ++ ")"
ppTypes showT EmptyType              = "empty-type"
ppTypes showT (UnicodeCharacters)    = "unicode-characters"
ppTypes showT (Integers)             = "integers"
ppTypes showT (Strings)              = "strings"
ppTypes showT (Values)               = "values"
ppTypes showT (Maps x y)             = "maps" ++ showArgs [ppTypes showT x, ppTypes showT y]
ppTypes showT Types                  = "types"
ppTypes showT ADTs                   = "algebraic-datatypes"
ppTypes showT (ADT nm ts)            = unpack nm ++ showArgs (map showT ts)
ppTypes showT (Bits n)               = "bits(" ++ show n ++ ")"
ppTypes showT (IEEEFloats format)    = "ieee-floats(" ++ show format ++ ")"
ppTypes showT (Multisets ty)         = "multisets" ++ showArgs [ppTypes showT ty]
ppTypes showT Naturals               = "naturals"
ppTypes showT Rationals              = "rationals"
ppTypes showT (Sets ty)              = "sets(" ++ ppTypes showT ty ++ ")"
ppTypes showT (Vectors ty)           = "vectors(" ++ ppTypes showT ty ++ ")"
ppTypes showT (Union ty1 ty2)        = "(" ++ ppTypes showT ty1 ++ "|" ++ ppTypes showT ty2 ++")"

ppOp :: SeqSortOp -> String
ppOp StarOp = "*"
ppOp PlusOp = "+"
ppOp QuestionMarkOp = "?"

showArgs :: [String] -> String
showArgs args = "(" ++ showArgs_ args ++ ")"
showArgs_ :: [String] -> String
showArgs_ args = intercalate "," args