Types.hs

{-# LANGUAGE OverloadedStrings, TupleSections #-}

module Funcons.Types where

import qualified Data.Map as M
import qualified Data.Set as S
import qualified Data.MultiSet as MS
import qualified Data.Vector as V
import qualified Data.BitVector as BV
import Data.Text (Text)
import Data.Maybe (isJust)
import Data.Ratio

type MetaVar = String
type Name = Text

-- | 
-- Internal representation of funcon terms.
-- The generic constructors 'FName' and 'FApp' use names to represent
-- nullary funcons and applications of funcons to other terms. 
-- Funcon terms are easily created using 'applyFuncon' or via
-- the smart constructors exported by "Funcons.Core".
data Funcons    = FName Name
                | FApp Name Funcons
                | FTuple [Funcons]
                | FList [Funcons]
                | FSet [Funcons]
                | FMap [Funcons]
                | FValue Values
                | FSortSeq Funcons SeqSortOp
                | FSortUnion Funcons Funcons
                | FSortComputes Funcons
                | FSortComputesFrom Funcons Funcons
                deriving (Eq, Ord, Show)

-- |
-- Build funcon terms by applying a funcon name to `zero or more' funcon terms.
-- This function is useful for defining smart constructors, e,g,
--
-- > handle_thrown_ :: [Funcons] -> Funcons
-- > handle_thrown_ = applyFuncon "handle-thrown"
--
-- or alternatively,
--
-- > handle_thrown_ :: Funcons -> Funcons -> Funcons
-- > handle_thrown_ x y = applyFuncon "handle-thrown" [x,y]
applyFuncon :: Name -> [Funcons] -> Funcons
applyFuncon str args    | null args = FName str
                        | otherwise = FApp str (FTuple args)

-- | Creates a list of funcon terms.
list_ :: [Funcons] -> Funcons
list_ = FList

-- | Creates a set of funcon terms.
set_ :: [Funcons] -> Funcons
set_ = FSet


-- | Funcon term representation identical to 'Funcons', 
-- but with meta-variables. 
data FTerm  = TVar MetaVar
            | TName Name
            | TApp Name FTerm
            | TTuple [FTerm]
            | TList [FTerm]
            | TSet  [FTerm]
            | TMap  [FTerm]
            | TFuncon Funcons
            | TSortSeq FTerm SeqSortOp
            | TSortUnion FTerm FTerm
            | TSortComputes FTerm
            | TSortComputesFrom FTerm FTerm
            deriving (Eq, Ord, Show)

-- | 
-- This datatype provides a number of builtin value types. 
-- Composite values are only built up out of other values.
-- The only exception is 'Thunk' which stores a thunked computation
-- (funcon term).
data Values     = ADTVal Name [Values]
                | Ascii Int
                | Atom String
                | Bit BV.BitVector
                | Char Char
                | ComputationType ComputationTypes
                | Float Float
                | IEEE_Float_32 Float
                | IEEE_Float_64 Double
                | Int Integer
                | List [Values]
                | Map Map
                | Multiset (MS.MultiSet Values)
                | Nat Integer
                | Rational Rational
                | Set Set
                | String String
                | Thunk Funcons
                | EmptyTuple -- | Tuples are split in 'EmptyTuple' and 'NonEmptyTuple' to avoid singleton tuples. Tuples should be constructed by applications of 'tuple_'. 
                | NonEmptyTuple Values Values [Values]
                | Vector Vectors
        deriving (Eq,Ord,Show)

type Map        = M.Map Values Values
type Set        = S.Set Values
type Vectors    = V.Vector Values

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

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

-- | Representation of builtin types.
data Types  = ADTs
            | ADT Name [Types]
            | AsciiCharacters
            | Atoms
            | Bits Int
            | BoundedIntegers Integer Integer
            | ComputationTypes
            | EmptyType
            | IEEEFloats IEEEFormats
            | Integers
            | Lists Types
            | Maps Types Types
            | Multisets Types
            | Naturals
            | Rationals
            | Sets Types
            | Strings
            | Thunks ComputationTypes -- | Types optionally attached to 'SeqSortOp'.
            | Tuples [TTParam]
            | Types
            | UnicodeCharacters
            | Union Types Types
            | Values
            | Vectors Types
              deriving (Ord,Eq,Show)

type TTParam = (Types,Maybe SeqSortOp)

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

binary32 :: Values
binary32 = ADTVal "binary32" []

binary64 :: Values
binary64 = ADTVal "binary64" []

adtval :: Name -> Values -> Values
adtval nm = ADTVal nm . tuple_unval

nullaryTypes :: [(Name,Types)]
nullaryTypes =
  [ ("algebraic-datatypes", ADTs)
  , ("atoms",               Atoms)
  , ("computation-types",   ComputationTypes)
  , ("empty-type",          EmptyType)
  , ("integers",            Integers)
  , ("naturals",            Naturals)
  , ("rationals",           Rationals)
  , ("strings",             Strings)
  , ("types",               Types)
  , ("unicode-characters",  UnicodeCharacters)
  , ("values",              Values)
  ]

unaryTypes :: [(Name,Types->Types)]
unaryTypes =
  [ ("lists",     Lists)
  , ("multisets", Multisets)
  , ("sets",      Sets)
  , ("vectors",   Vectors)
  ]

binaryTypes :: [(Name,Types->Types->Types)]
binaryTypes =
  [ ("maps", Maps)
  ]

boundedIntegerTypes :: [(Name, Integer -> Integer -> Types)]
boundedIntegerTypes = [("bounded-integers", BoundedIntegers)]

floatTypes :: [(Name, IEEEFormats -> Types)]
floatTypes = [("ieee-floats", IEEEFloats)]

bitsTypes :: [(Name, Int -> Types)]
bitsTypes = [("bits", Bits)]

-- type environment

-- | The typing environment maps datatype names to their definitions.
type TypeEnv = M.Map Name DataTypeMembers

-- | A type parameter is of the form X:T where the name of the parameter,/X/, is optional.
-- When present, /X/ can be used to specify the type of constructors.
type TypeParam = (Maybe MetaVar,FTerm)
-- | A datatype has `zero or more' type parameters and
-- `zero or more' alternatives.
data DataTypeMembers = DataTypeMembers [TypeParam] [DataTypeAlt]

-- | An alternative is either a datatype constructor or the inclusion
-- of some other type. The types are arbitrary funcon terms (with possible
-- variables) that may require evaluation to be resolved to a 'Types'.
data DataTypeAlt = DataTypeInclusion FTerm
                 | DataTypeConstructor Name FTerm

-- | Lookup the definition of a datatype in the typing environment.
typeLookup :: Name -> TypeEnv -> Maybe DataTypeMembers
typeLookup = M.lookup

-- | The empty 'TypeEnv'.
emptyTypeEnv :: TypeEnv
emptyTypeEnv = M.empty

-- | Unites a list of 'TypeEnv's.
typeEnvUnions :: [TypeEnv] -> TypeEnv
typeEnvUnions = foldr typeEnvUnion emptyTypeEnv

-- | Unites two 'TypeEnv's.
typeEnvUnion :: TypeEnv -> TypeEnv -> TypeEnv
typeEnvUnion = M.unionWith (\_ _ -> error "duplicate type-name")

-- | Creates a `TypeEnv' from a list.
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeEnv
typeEnvFromList = M.fromList

{-
-- I think this is no longer needed.
-- Ids
newtype ID = ID' Values
    deriving (Eq)

instance Ord ID where
    (ID' v1) `compare` (ID' v2) = idCompare v1 v2

idCompare :: Values -> Values -> Ordering
(Int i1)    `idCompare` (Int i2)     = compare i1 i2
(Int _)     `idCompare` _            = LT
_           `idCompare` (Int _)     = GT
(String s)  `idCompare` (String s2) = compare s s2
_           `idCompare` _           = error "comparing non-atomic ids"
-}

-- Values should be atoms: Ints,Booleans,Strings,Tuples? etc

-- Ids are just `strings` now.
{-
id_ :: Funcons -> Funcons
id_ (FValue v@(Int _))    = FValue (ID (ID' v))
id_ (FValue v@(String _)) = FValue (ID (ID' v))
id_ v = error $ "id supplied with non-atomic value"
-}

--- smart constructors for values

-- | Creates an integer 'literal'.
int_ :: Int -> Funcons
int_ = FValue . mk_integers . toInteger

-- | Creates a natural 'literal'.
nat_ :: Int -> Funcons 
nat_ i | i < 0      = int_ i
       | otherwise  = FValue $ mk_naturals $ toInteger i

-- | Creates an atom from a 'String'. 
atom_ :: String -> Funcons
atom_ = FValue . Atom

-- | Creates a rational literal.
rational_ :: Rational -> Funcons
rational_ = FValue . mk_rationals

-- | Creates a string literal.
string_ :: String -> Funcons
string_ = FValue . String

-- | Creates an empty tuple as a 'Values'.
empty_tuple_ :: Funcons 
empty_tuple_ = FValue EmptyTuple

-- | The empty map as a 'Funcons'.
empty_map_,map_empty_ :: Funcons
empty_map_ = FValue (Map M.empty)
map_empty_ = empty_map_

-- | The empty set as a 'Funcons'.
empty_set_ :: Funcons
empty_set_ = FValue (Set S.empty)

-- | Creates a tuple of funcon terms.
tuple_ :: [Funcons] -> Funcons
tuple_ = FTuple

tuple_val_ :: [Values] -> Funcons
tuple_val_ = FValue . safe_tuple_val

type_ :: Types -> Funcons
type_ = FValue . typeVal

vec :: V.Vector (Values) -> Funcons
vec = FValue . Vector

-- idval :: Values -> Values
-- idval = ID . ID'

typeVal :: Types -> Values
typeVal = ComputationType . Type

safe_tuple_val :: [Values] -> Values
safe_tuple_val []         = EmptyTuple
safe_tuple_val [v]        = v
safe_tuple_val (v1:v2:vs) = NonEmptyTuple v1 v2 vs

tuple_unval :: Values -> [Values]
tuple_unval EmptyTuple               = []
tuple_unval (NonEmptyTuple v1 v2 vs) = v1:v2:vs
tuple_unval v                        = [v]

types_unval :: Types -> [Types]
types_unval (Tuples ts)
    | any (isJust . snd) ts = [Tuples ts]
    | otherwise             = map fst ts
types_unval t = [t]


fvalues :: [Values] -> [Funcons]
fvalues = map FValue

listval :: [Values] -> Funcons
listval = FValue . List

setval :: [Values] -> Funcons
setval = FValue . setval_

setval_ = Set . S.fromList

mapval :: [Values] -> Funcons
mapval = FValue . mapval_

mapval_ = Map . M.fromList . map toKeyValue
 where  toKeyValue (NonEmptyTuple k v []) = (k,v)
        toKeyValue _ = error "mapval"

-- subtyping rationals
mk_rationals :: Rational -> Values
mk_rationals r  | denominator r == 1 = mk_integers (numerator r)
                | otherwise             = Rational r

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

mk_naturals :: Integer -> Values
mk_naturals = Nat

-- | Returns the /rational/ representation of a value if it is a subtype.
-- Otherwise it returns the original value.
upcastRationals :: Values -> Values
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 -> Values
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 -> Values
upcastNaturals v = v

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

castType :: Values -> Maybe Types
castType (ComputationType (Type ty)) = Just ty
castType EmptyTuple                  = Just (Tuples [])
castType (NonEmptyTuple t1 t2 ts)    = Tuples <$> mapM (fmap (,Nothing) . castType) (t1:t2:ts)
castType _                           = Nothing

--- Value specific

-- | Attempt to downcast a funcon term to a value.
downcastValue :: Funcons -> Values
downcastValue (FValue v) = v
downcastValue _ = error "downcasting to value failed"

-- | Attempt to downcast a funcon term to a type.
downcastType :: Funcons -> Types
downcastType (FValue (ComputationType (Type ty))) = ty
downcastType _ = error "downcasting to type failed"

-- | Attempt to downcast a value to a type.
downcastValueType :: Values -> Types
downcastValueType (ComputationType (Type t)) = t
downcastValueType _ = error "valueType: not a type"

recursiveFunconValue :: Funcons -> Maybe Values
recursiveFunconValue (FValue v) = Just v
recursiveFunconValue (FList fs) = List <$> mapM recursiveFunconValue fs
recursiveFunconValue (FSet fs)  = Set . S.fromList <$> mapM recursiveFunconValue fs
recursiveFunconValue (FMap fs)  = Map . M.fromList <$> mapM unFTuple fs
 where  unFTuple (FTuple [k,v]) = (,) <$> recursiveFunconValue k <*> recursiveFunconValue v
        unFTuple _ = Nothing
recursiveFunconValue _ = Nothing

(===) :: Values -> Values -> Bool
v1 === v2 = isGround v1 && isGround v2 && (v1 == v2)

(=/=) :: Values -> Values -> Bool
v1 =/= v2 = isGround v1 && isGround v2 && (v1 /= v2)

isGround :: Values -> Bool
isGround (ADTVal _ mv)            = all isGround mv
isGround (Ascii _)                = True
isGround (Atom _)                 = True
isGround (Bit _)                  = True
isGround (Char _)                 = True
isGround (ComputationType _)      = True
isGround (EmptyTuple)             = True
isGround (Float _)                = True
isGround (IEEE_Float_32 _)        = True
isGround (IEEE_Float_64 _)        = True
isGround (Int _)                  = True
isGround (List vs)                = all isGround vs
isGround (Map m)                  = all isGround (M.elems m)
isGround (Multiset ms)            = all isGround ms
isGround (Nat _)                  = True
isGround (NonEmptyTuple v1 v2 vs) = all isGround (v1:v2:vs)
isGround (Rational _)             = True
isGround (Set s)                  = all isGround (S.toList s)
isGround (String _)               = True
isGround (Thunk _)                = False
isGround (Vector v)               = all isGround (V.toList v)

-- functions that check simple properties of funcons
-- TODO: these may not be needed any longer
isAscii (FValue (Ascii _))      = True
isAscii _                       = False
isChar (FValue (Char _))         = True
isChar _                        = False
isId = isString -- TODO: is this needed any more?
isNat (FValue (Int _))          = True
isNat _                         = False
isInt (FValue (Int _))           = True
isInt _                         = False
isList (FValue (List _))         = True
isList _                        = False
isEnv f                         = isMap f
isMap (FValue (Map _))           = True
isMap _                         = False
isSet (FValue (Set _))           = True
isSet _                         = False
isString (FValue v)              = isString_ v
isString _                      = False
isString_ (String _)            = True
isString_ _                     = False
isThunk (FValue (Thunk _))       = True
isThunk _                       = False
isTup (FValue EmptyTuple)       = True
isTup (FValue (NonEmptyTuple _ _ _)) = True
isTup _                         = False
isType (FValue (ComputationType (Type _))) = True
isType _                        = False
isVal (FValue _)                 = True
isVal _                         = False
isVec (FValue (Vector _))        = True
isVec _                         = False
isType_ (ComputationType (Type _)) = True
isType_ _                       = False

integers_,strings_,values_,unicode_characters_ :: Funcons
integers_ = type_ Integers
unicode_characters_  = type_ UnicodeCharacters
strings_ = type_ Strings
values_ = type_ Values