{-# LANGUAGE OverloadedStrings, TupleSections, FlexibleInstances #-}
module Funcons.Types (
module Funcons.Types,
module VAL,) where
import qualified Funcons.Operations as VAL hiding (SortErr, ValueOp)
import Funcons.Operations hiding (Name, Values, ComputationTypes, TaggedSyntax, Types, isMap, isAscii, isNoValue, isSet, map_empty_, isEnv, isDefinedVal, isString_, isChar, isVec, isType, isList, isNat, isInt, atoms_, integers_, values_, set_, list_, tuple_, atom_, nothing_, defined_values_, types_, value_types_, toList, isList)
import qualified Data.Char as C
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 Data.Text (Text)
import Data.Ratio
type MetaVar = String
type Name = Text
data Funcons = FName Name
| FApp Name [Funcons]
| FSet [Funcons]
| FMap [Funcons]
| FValue Values
| FSortSeq Funcons VAL.SeqSortOp
| FSortPower Funcons Funcons
| FSortUnion Funcons Funcons
| FSortInter Funcons Funcons
| FSortComplement Funcons
| FSortComputes Funcons
| FSortComputesFrom Funcons Funcons
deriving (Eq, Ord, Show, Read)
applyFuncon :: Name -> [Funcons] -> Funcons
applyFuncon str args | null args = FName str
| otherwise = FApp str args
tuple_ :: [Funcons] -> Funcons
tuple_ = FValue . ADTVal "list"
list_ :: [Funcons] -> Funcons
list_ = applyFuncon "list"
set_ :: [Funcons] -> Funcons
set_ = applyFuncon "set"
data FTerm = TVar MetaVar
| TName Name
| TApp Name [FTerm]
| TSeq [FTerm]
| TSet [FTerm]
| TMap [FTerm]
| TFuncon Funcons
| TSortSeq FTerm VAL.SeqSortOp
| TSortPower FTerm FTerm
| TSortUnion FTerm FTerm
| TSortInter FTerm FTerm
| TSortComplement FTerm
| TSortComputes FTerm
| TSortComputesFrom FTerm FTerm
| TAny
deriving (Eq, Ord, Show, Read)
type Values = VAL.Values Funcons
type TaggedSyntax = VAL.TaggedSyntax Funcons
instance HasValues Funcons where
inject = FValue
project f = case f of
FValue v -> Just v
_ -> Nothing
type Map = M.Map Values Values
type Set = S.Set Values
type Vectors = V.Vector Values
type ComputationTypes = VAL.ComputationTypes Funcons
type Types = VAL.Types Funcons
type TTParam = (Types,Maybe VAL.SeqSortOp)
binary32 :: Values
binary32 = ADTVal "binary32" []
binary64 :: Values
binary64 = ADTVal "binary64" []
adtval :: Name -> [Values] -> Values
adtval nm = ADTVal nm . map FValue
tuple_val__ :: [Values] -> Values
tuple_val__ = adtval "tuple"
tuple_val_ = FValue . tuple_val__
nullaryTypes :: [(Name,Types)]
nullaryTypes =
[ ("algebraic-datatypes", ADTs)
, ("adts" , ADTs)
, ("non-grounded-values", Complement GroundValues)
, ("atoms", Atoms)
, ("empty-type", EmptyType)
, ("rationals", Rationals)
, ("unicode-characters", UnicodeCharacters)
, ("values", VAL.Values)
]
unaryTypes :: [(Name,Types->Types)]
unaryTypes =
[ ("multisets", Multisets)
]
binaryTypes :: [(Name,Types->Types->Types)]
binaryTypes =
[]
boundedIntegerTypes :: [(Name, Integer -> Types)]
boundedIntegerTypes = [("integers-from", IntegersFrom)
,("from", IntegersFrom)
,("integers-up-to", IntegersUpTo)
,("up-to", IntegersUpTo)
]
floatTypes :: [(Name, IEEEFormats -> Types)]
floatTypes = [("ieee-floats", IEEEFloats)]
int_ :: Int -> Funcons
int_ = FValue . mk_integers . toInteger
nat_ :: Int -> Funcons
nat_ i | i < 0 = int_ i
| otherwise = FValue $ mk_naturals $ toInteger i
atom_ :: String -> Funcons
atom_ = FValue . Atom
string_ :: String -> Funcons
string_ = FValue . string__
string__ :: String -> Values
string__ = ADTVal "list" . map (FValue . Ascii)
float_ :: Double -> Funcons
float_ = FValue . Float
ieee_float_32_ :: Float -> Funcons
ieee_float_32_ = FValue . IEEE_Float_32
ieee_float_64_ :: Double -> Funcons
ieee_float_64_ = FValue . IEEE_Float_64
empty_map_,map_empty_ :: Funcons
empty_map_ = FValue (Map M.empty)
map_empty_ = empty_map_
empty_set_ :: Funcons
empty_set_ = FValue (Set S.empty)
type_ :: Types -> Funcons
type_ = FValue . typeVal
sort_ :: ComputationTypes -> Funcons
sort_ = FValue . ComputationType
comp_type_ :: ComputationTypes -> Funcons
comp_type_ = FValue . ComputationType
vec :: V.Vector (Values) -> Funcons
vec = FValue . Vector
vec_ :: [Values] -> Funcons
vec_ = FValue . Vector . V.fromList
typeVal :: Types -> Values
typeVal = ComputationType . Type
fvalues :: [Values] -> [Funcons]
fvalues = map FValue
listval :: [Values] -> Funcons
listval = FValue . ADTVal "list" . map FValue
setval :: [Values] -> Funcons
setval = FValue . setval_
setval_ :: [Values] -> Values
setval_ = Set . S.fromList
mapval :: [Values] -> Funcons
mapval = FValue . mapval_
mapval_ :: [Values] -> Values
mapval_ = Map . M.fromList . mkPairs
downcastType :: Funcons -> Types
downcastType (FValue v) = downcastValueType v
downcastType _ = error "downcasting to sort failed"
downcastSort :: Funcons -> ComputationTypes
downcastSort (FValue (ComputationType s)) = s
downcastSort _ = error "downcasting to sort failed"
downcastValue :: Funcons -> Values
downcastValue (FValue v) = v
downcastValue _ = error "downcasting to value failed"
recursiveFunconValue :: Funcons -> Maybe Values
recursiveFunconValue (FValue v) = Just v
recursiveFunconValue (FSet fs) = Set . S.fromList <$> mapM recursiveFunconValue fs
recursiveFunconValue (FMap fs) = Map . M.fromList . mkPairs <$> mapM recursiveFunconValue fs
recursiveFunconValue _ = Nothing
allEqual :: [Values] -> [Values] -> Bool
allEqual xs ys = length xs == length ys && and (zipWith (===) xs ys)
allUnEqual :: [Values] -> [Values] -> Bool
allUnEqual xs ys = length xs /= length ys || or (zipWith (=/=) xs ys)
isNoValue :: Funcons -> Bool
isNoValue (FValue n) = n == none__
isNoValue _ = False
hasStep (FValue _) = False
hasStep _ = True
isVal (FValue _) = True
isVal _ = False
isDefinedVal f = isVal f && not (isNoValue f)
isAscii (FValue (Ascii _)) = True
isAscii _ = False
isAscii_ (Ascii _) = True
isAscii_ _ = False
isString (FValue (ADTVal "list" s)) = all isAscii s
isString _ = False
isString_ (ADTVal "list" s) = all isAscii s
isString_ _ = False
isChar (FValue (Char _)) = True
isChar _ = False
isNat (FValue (Int _)) = True
isNat _ = False
isInt (FValue (Int _)) = True
isInt _ = False
isList (FValue (ADTVal "list" _)) = True
isList _ = False
isEnv f = isMap f
isMap (FValue (Map _)) = True
isMap _ = False
isSet (FValue (Set _)) = True
isSet _ = False
isTup _ = False
isSort (FValue (ComputationType _)) = True
isSort _ = False
isSort_ (ComputationType _) = True
isSort_ _ = False
isType (FValue (ComputationType (Type _))) = True
isType _ = False
isVec (FValue (Vector _)) = True
isVec _ = False
isCharacter_ (Char _) = True
isCharacter_ (Ascii _) = True
isCharacter_ _ = False
integers_,atoms_,values_,unicode_characters_ :: Funcons
integers_ = type_ Integers
unicode_characters_ = type_ UnicodeCharacters
values_ = type_ VAL.Values
defined_values_ = type_ DefinedValues
nothing_ = type_ Nothings
vectors_ :: Types -> Funcons
vectors_ = type_ . Vectors
atoms_ = type_ Atoms
type TypeRelation = M.Map Name DataTypeMembers
type TypeParam = (Maybe MetaVar, Maybe VAL.SeqSortOp, FTerm)
data TPattern = TPWildCard
| TPVar MetaVar
| TPSeqVar MetaVar VAL.SeqSortOp
| TPLit FTerm
| TPComputes TPattern
| TPComputesFrom TPattern TPattern
| TPADT Name [TPattern]
deriving (Show, Eq, Ord, Read)
data DataTypeMembers = DataTypeMemberss Name [TPattern] [DataTypeAltt]
deriving (Show)
data DataTypeAltt = DataTypeInclusionn FTerm
| DataTypeMemberConstructor Name [FTerm] (Maybe [TPattern])
deriving (Show)
typeLookup :: Name -> TypeRelation -> Maybe DataTypeMembers
typeLookup = M.lookup
emptyTypeRelation :: TypeRelation
emptyTypeRelation = M.empty
typeEnvUnions :: [TypeRelation] -> TypeRelation
typeEnvUnions = foldr typeEnvUnion emptyTypeRelation
typeEnvUnion :: TypeRelation -> TypeRelation -> TypeRelation
typeEnvUnion = M.unionWith (\_ _ -> error "duplicate type-name")
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList = M.fromList