{-# 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
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
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
data SeqSortOp = StarOp | PlusOp | QuestionMarkOp
deriving (Show, Eq, Ord, Read)
data ComputationTypes t = Type (Types t)
| ComputesType (Types t)
| ComputesFromType (Types t) (Types t)
deriving (Ord,Eq,Show, Read)
data Types t= ADTs
| ADT Name [t]
| AnnotatedType (Types t) SeqSortOp
| AsciiCharacters
| Atoms
| Bits Int
| IntegersFrom Integer
| 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)
| 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)
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"
upcastRationals :: Values t -> Values t
upcastRationals (Nat n) = Rational (toRational n)
upcastRationals (Int i) = Rational (toRational i)
upcastRationals v = v
upcastIntegers :: Values t -> Values t
upcastIntegers (Nat n) = Int n
upcastIntegers v = v
upcastNaturals :: Values t -> Values t
upcastNaturals (Int i) | i >= 0 = Nat i
upcastNaturals v = v
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
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
mk_ascii_characters :: Char -> Values t
mk_ascii_characters = Ascii
(===) :: (HasValues t, Eq t ) => Values t -> Values t -> Bool
v1 === v2 = isGround v1 && isGround v2 && (v1 == v2)
(=/=) :: (HasValues t, Eq t ) => 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
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
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