{-# 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, Types, isMap, isNull, isSet, map_empty_, isEnv, isDefinedVal, isChar, isVec, isType, isList, isNat, isInt, atoms_, integers_, values_, set_, list_, tuple_, atom_, nulltype_, non_null_values_, types_, value_types_, toList, isList, libFromList, listUnites, null)
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.Maybe (isJust)
import Data.Text (Text)
import Data.Ratio
type MetaVar = String
type Name = Text
data Funcons = FName Name
| FApp Name [Funcons]
| FSet [Funcons]
| FMap [Funcons]
| FBinding Funcons [Funcons]
| FValue Values
| FSortSeq Funcons VAL.SeqSortOp
| FSortPower Funcons Funcons
| FSortUnion Funcons Funcons
| FSortInter Funcons Funcons
| FSortComplement Funcons
| FSortComputes Funcons
| FSortComputesFrom Funcons Funcons
deriving (Funcons -> Funcons -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Funcons -> Funcons -> Bool
$c/= :: Funcons -> Funcons -> Bool
== :: Funcons -> Funcons -> Bool
$c== :: Funcons -> Funcons -> Bool
Eq, Eq Funcons
Funcons -> Funcons -> Bool
Funcons -> Funcons -> Ordering
Funcons -> Funcons -> Funcons
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Funcons -> Funcons -> Funcons
$cmin :: Funcons -> Funcons -> Funcons
max :: Funcons -> Funcons -> Funcons
$cmax :: Funcons -> Funcons -> Funcons
>= :: Funcons -> Funcons -> Bool
$c>= :: Funcons -> Funcons -> Bool
> :: Funcons -> Funcons -> Bool
$c> :: Funcons -> Funcons -> Bool
<= :: Funcons -> Funcons -> Bool
$c<= :: Funcons -> Funcons -> Bool
< :: Funcons -> Funcons -> Bool
$c< :: Funcons -> Funcons -> Bool
compare :: Funcons -> Funcons -> Ordering
$ccompare :: Funcons -> Funcons -> Ordering
Ord, Int -> Funcons -> ShowS
[Funcons] -> ShowS
Funcons -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Funcons] -> ShowS
$cshowList :: [Funcons] -> ShowS
show :: Funcons -> String
$cshow :: Funcons -> String
showsPrec :: Int -> Funcons -> ShowS
$cshowsPrec :: Int -> Funcons -> ShowS
Show, ReadPrec [Funcons]
ReadPrec Funcons
Int -> ReadS Funcons
ReadS [Funcons]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Funcons]
$creadListPrec :: ReadPrec [Funcons]
readPrec :: ReadPrec Funcons
$creadPrec :: ReadPrec Funcons
readList :: ReadS [Funcons]
$creadList :: ReadS [Funcons]
readsPrec :: Int -> ReadS Funcons
$creadsPrec :: Int -> ReadS Funcons
Read)
applyFuncon :: Name -> [Funcons] -> Funcons
applyFuncon :: Name -> [Funcons] -> Funcons
applyFuncon Name
str [Funcons]
args | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Funcons]
args = Name -> Funcons
FName Name
str
| Bool
otherwise = Name -> [Funcons] -> Funcons
FApp Name
str [Funcons]
args
tuple_ :: [Funcons] -> Funcons
tuple_ :: [Funcons] -> Funcons
tuple_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"tuple"
list_ :: [Funcons] -> Funcons
list_ :: [Funcons] -> Funcons
list_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"list"
set_ :: [Funcons] -> Funcons
set_ :: [Funcons] -> Funcons
set_ = Name -> [Funcons] -> Funcons
applyFuncon Name
"set"
data FTerm = TVar MetaVar
| TName Name
| TApp Name [FTerm]
| TSeq [FTerm]
| TSet [FTerm]
| TMap [FTerm]
| TBinding FTerm 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 (FTerm -> FTerm -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FTerm -> FTerm -> Bool
$c/= :: FTerm -> FTerm -> Bool
== :: FTerm -> FTerm -> Bool
$c== :: FTerm -> FTerm -> Bool
Eq, Eq FTerm
FTerm -> FTerm -> Bool
FTerm -> FTerm -> Ordering
FTerm -> FTerm -> FTerm
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: FTerm -> FTerm -> FTerm
$cmin :: FTerm -> FTerm -> FTerm
max :: FTerm -> FTerm -> FTerm
$cmax :: FTerm -> FTerm -> FTerm
>= :: FTerm -> FTerm -> Bool
$c>= :: FTerm -> FTerm -> Bool
> :: FTerm -> FTerm -> Bool
$c> :: FTerm -> FTerm -> Bool
<= :: FTerm -> FTerm -> Bool
$c<= :: FTerm -> FTerm -> Bool
< :: FTerm -> FTerm -> Bool
$c< :: FTerm -> FTerm -> Bool
compare :: FTerm -> FTerm -> Ordering
$ccompare :: FTerm -> FTerm -> Ordering
Ord, Int -> FTerm -> ShowS
[FTerm] -> ShowS
FTerm -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [FTerm] -> ShowS
$cshowList :: [FTerm] -> ShowS
show :: FTerm -> String
$cshow :: FTerm -> String
showsPrec :: Int -> FTerm -> ShowS
$cshowsPrec :: Int -> FTerm -> ShowS
Show, ReadPrec [FTerm]
ReadPrec FTerm
Int -> ReadS FTerm
ReadS [FTerm]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [FTerm]
$creadListPrec :: ReadPrec [FTerm]
readPrec :: ReadPrec FTerm
$creadPrec :: ReadPrec FTerm
readList :: ReadS [FTerm]
$creadList :: ReadS [FTerm]
readsPrec :: Int -> ReadS FTerm
$creadsPrec :: Int -> ReadS FTerm
Read)
type Values = VAL.Values Funcons
instance HasValues Funcons where
inject :: Values -> Funcons
inject = Values -> Funcons
FValue
project :: Funcons -> Maybe Values
project Funcons
f = case Funcons
f of
FValue Values
v -> forall a. a -> Maybe a
Just Values
v
Funcons
_ -> forall a. Maybe a
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 :: Values
binary32 = forall t. Name -> [t] -> Values t
ADTVal Name
"binary32" []
binary64 :: Values
binary64 :: Values
binary64 = forall t. Name -> [t] -> Values t
ADTVal Name
"binary64" []
adtval :: Name -> [Values] -> Values
adtval :: Name -> [Values] -> Values
adtval Name
nm = forall t. Name -> [t] -> Values t
ADTVal Name
nm forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue
tuple_val__ :: [Values] -> Values
tuple_val__ :: [Values] -> Values
tuple_val__ = Name -> [Values] -> Values
adtval Name
"tuple"
tuple_val_ :: [Values] -> Funcons
tuple_val_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
tuple_val__
nullaryTypes :: [(Name,Types)]
nullaryTypes :: [(Name, Types)]
nullaryTypes =
[ (Name
"algebraic-datatypes", forall t. Types t
ADTs)
, (Name
"adts" , forall t. Types t
ADTs)
, (Name
"rationals", forall t. Types t
Rationals)
, (Name
"values", forall t. Types t
VAL.Values)
]
unaryTypes :: [(Name,Types->Types)]
unaryTypes :: [(Name, Types -> Types)]
unaryTypes =
[ (Name
"multisets", forall t. HasValues t => Types t -> Types t
multisets)
]
binaryTypes :: [(Name,Types->Types->Types)]
binaryTypes :: [(Name, Types -> Types -> Types)]
binaryTypes =
[]
boundedIntegerTypes :: [(Name, Integer -> Types)]
boundedIntegerTypes :: [(Name, Integer -> Types)]
boundedIntegerTypes = []
floatTypes :: [(Name, IEEEFormats -> Types)]
floatTypes :: [(Name, IEEEFormats -> Types)]
floatTypes = [(Name
"ieee-floats", forall t. IEEEFormats -> Types t
IEEEFloats)]
int_ :: Int -> Funcons
int_ :: Int -> Funcons
int_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Integer -> Values t
mk_integers forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger
nat_ :: Int -> Funcons
nat_ :: Int -> Funcons
nat_ Int
i | Int
i forall a. Ord a => a -> a -> Bool
< Int
0 = Int -> Funcons
int_ Int
i
| Bool
otherwise = Values -> Funcons
FValue forall a b. (a -> b) -> a -> b
$ forall t. Integer -> Values t
mk_naturals forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> Integer
toInteger Int
i
bool_ :: Bool -> Funcons
bool_ :: Bool -> Funcons
bool_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Values
bool__
bool__ :: Bool -> Values
bool__ :: Bool -> Values
bool__ = forall t. Bool -> Values t
VAL.tobool
atom_ :: String -> Funcons
atom_ :: String -> Funcons
atom_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. String -> Values t
Atom
string_ :: String -> Funcons
string_ :: String -> Funcons
string_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Values
string__
string__ :: String -> Values
string__ :: String -> Values
string__ = forall t. Name -> [t] -> Values t
ADTVal Name
"list" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Char -> Funcons
char_
char_ :: Char -> Funcons
char_ :: Char -> Funcons
char_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Values
char__
char__ :: Char -> Values
char__ :: Char -> Values
char__ = forall t. HasValues t => Char -> Values t
mk_unicode_characters
list__ :: [Values] -> Values
list__ :: [Values] -> Values
list__ = forall t. HasValues t => [Values t] -> Values t
VAL.list
set__ :: [Values] -> Values
set__ :: [Values] -> Values
set__ = forall t. (Ord t, HasValues t) => [Values t] -> Values t
VAL.set
vector__ :: [Values] -> Values
vector__ :: [Values] -> Values
vector__ = forall t. HasValues t => [Values t] -> Values t
VAL.vector
tuple__ :: [Values] -> Values
tuple__ :: [Values] -> Values
tuple__ = forall t. HasValues t => [Values t] -> Values t
VAL.tuple
float_ :: Double -> Funcons
float_ :: Double -> Funcons
float_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Double -> Values t
Float
ieee_float_32_ :: Float -> Funcons
ieee_float_32_ :: Float -> Funcons
ieee_float_32_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Float -> Values t
IEEE_Float_32
ieee_float_64_ :: Double -> Funcons
ieee_float_64_ :: Double -> Funcons
ieee_float_64_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Double -> Values t
IEEE_Float_64
empty_map_,map_empty_ :: Funcons
empty_map_ :: Funcons
empty_map_ = Values -> Funcons
FValue (forall t. ValueMaps (Values t) -> Values t
Map forall k a. Map k a
M.empty)
map_empty_ :: Funcons
map_empty_ = Funcons
empty_map_
empty_set_ :: Funcons
empty_set_ :: Funcons
empty_set_ = Values -> Funcons
FValue Values
empty_set__
empty_set__ :: Values
empty_set__ :: Values
empty_set__ = forall t. ValueSets (Values t) -> Values t
Set forall a. Set a
S.empty
type_ :: Types -> Funcons
type_ :: Types -> Funcons
type_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. Types -> Values
typeVal
sort_ :: ComputationTypes -> Funcons
sort_ :: ComputationTypes -> Funcons
sort_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. ComputationTypes t -> Values t
ComputationType
comp_type_ :: ComputationTypes -> Funcons
comp_type_ :: ComputationTypes -> Funcons
comp_type_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. ComputationTypes t -> Values t
ComputationType
vec :: V.Vector (Values) -> Funcons
vec :: Vector Values -> Funcons
vec = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. ValueVectors (Values t) -> Values t
Vector
vec_ :: [Values] -> Funcons
vec_ :: [Values] -> Funcons
vec_ = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. ValueVectors (Values t) -> Values t
Vector forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Vector a
V.fromList
typeVal :: Types -> Values
typeVal :: Types -> Values
typeVal = forall t. ComputationTypes t -> Values t
ComputationType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Types t -> ComputationTypes t
Type
fvalues :: [Values] -> [Funcons]
fvalues :: [Values] -> [Funcons]
fvalues = forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue
listval :: [Values] -> Funcons
listval :: [Values] -> Funcons
listval = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. Name -> [t] -> Values t
ADTVal Name
"list" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue
setval :: [Values] -> Funcons
setval :: [Values] -> Funcons
setval = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
setval_
setval_ :: [Values] -> Values
setval_ :: [Values] -> Values
setval_ = forall t. ValueSets (Values t) -> Values t
Set forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList
mapval :: [Values] -> Funcons
mapval :: [Values] -> Funcons
mapval = Values -> Funcons
FValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
mapval_
mapval_ :: [Values] -> Values
mapval_ :: [Values] -> Values
mapval_ [Values]
mvs = case forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Maybe (Values, [Values])
fromBinding [Values]
mvs of
Just [(Values, [Values])]
vs -> forall t. ValueMaps (Values t) -> Values t
Map forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith forall a b. a -> b -> a
const [(Values, [Values])]
vs
Maybe [(Values, [Values])]
_ -> forall a. HasCallStack => String -> a
error String
"mapval: invalid map-notation"
fromBinding :: Values -> Maybe (Values, [Values])
fromBinding :: Values -> Maybe (Values, [Values])
fromBinding (ADTVal Name
"tuple" (Funcons
k':[Funcons]
vs')) = do
Values
k <- forall t. HasValues t => t -> Maybe (Values t)
project Funcons
k'
[Values]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs'
forall (m :: * -> *) a. Monad m => a -> m a
return (Values
k,[Values]
vs)
fromBinding Values
k = forall a. a -> Maybe a
Just (Values
k,[])
downcastType :: Funcons -> Types
downcastType :: Funcons -> Types
downcastType (FValue Values
v) = forall t. Values t -> Types t
downcastValueType Values
v
downcastType Funcons
_ = forall a. HasCallStack => String -> a
error String
"downcasting to sort failed"
downcastSort :: Funcons -> ComputationTypes
downcastSort :: Funcons -> ComputationTypes
downcastSort (FValue (ComputationType ComputationTypes
s)) = ComputationTypes
s
downcastSort Funcons
_ = forall a. HasCallStack => String -> a
error String
"downcasting to sort failed"
downcastValue :: Funcons -> Values
downcastValue :: Funcons -> Values
downcastValue (FValue Values
v) = Values
v
downcastValue Funcons
_ = forall a. HasCallStack => String -> a
error String
"downcasting to value failed"
recursiveFunconValue :: Funcons -> Maybe Values
recursiveFunconValue :: Funcons -> Maybe Values
recursiveFunconValue (FValue Values
v) = forall a. a -> Maybe a
Just Values
v
recursiveFunconValue (FSet [Funcons]
fs) = forall t. ValueSets (Values t) -> Values t
Set forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
S.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe Values
recursiveFunconValue [Funcons]
fs
recursiveFunconValue (FMap [Funcons]
fs) = do
[Values]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe Values
recursiveFunconValue [Funcons]
fs
[(Values, [Values])]
assocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values -> Maybe (Values, [Values])
fromBinding [Values]
vs
forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. ValueMaps (Values t) -> Values t
Map forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Values, [Values])]
assocs)
recursiveFunconValue Funcons
_ = forall a. Maybe a
Nothing
allEqual :: [Values] -> [Values] -> Bool
allEqual :: [Values] -> [Values] -> Bool
allEqual [Values]
xs [Values]
ys = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
xs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
ys Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall t. (HasValues t, Eq t) => Values t -> Values t -> Bool
(===) [Values]
xs [Values]
ys)
allUnEqual :: [Values] -> [Values] -> Bool
allUnEqual :: [Values] -> [Values] -> Bool
allUnEqual [Values]
xs [Values]
ys = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
xs forall a. Eq a => a -> a -> Bool
/= forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
ys Bool -> Bool -> Bool
|| forall (t :: * -> *). Foldable t => t Bool -> Bool
or (forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall t. (HasValues t, Eq t) => Values t -> Values t -> Bool
(=/=) [Values]
xs [Values]
ys)
isNull :: Funcons -> Bool
isNull :: Funcons -> Bool
isNull (FValue Values
n) = Values
n forall a. Eq a => a -> a -> Bool
== forall t. Values t
null__
isNull Funcons
_ = Bool
False
hasStep :: Funcons -> Bool
hasStep (FValue Values
_) = Bool
False
hasStep Funcons
_ = Bool
True
isVal :: Funcons -> Bool
isVal (FValue Values
_) = Bool
True
isVal Funcons
_ = Bool
False
isDefinedVal :: Funcons -> Bool
isDefinedVal Funcons
f = Funcons -> Bool
isVal Funcons
f Bool -> Bool -> Bool
&& Bool -> Bool
not (Funcons -> Bool
isNull Funcons
f)
isString :: Funcons -> Bool
isString (FValue Values
v) = forall t. HasValues t => Values t -> Bool
isString_ Values
v
isString Funcons
_ = Bool
False
isChar :: Funcons -> Bool
isChar (FValue Values
v) = forall a. Maybe a -> Bool
isJust (forall t. HasValues t => Values t -> Maybe Char
upcastCharacter Values
v)
isChar Funcons
_ = Bool
False
isNat :: Funcons -> Bool
isNat (FValue (Int Integer
_)) = Bool
True
isNat Funcons
_ = Bool
False
isInt :: Funcons -> Bool
isInt (FValue (Int Integer
_)) = Bool
True
isInt Funcons
_ = Bool
False
isList :: Funcons -> Bool
isList (FValue (ADTVal Name
"list" [Funcons]
_)) = Bool
True
isList Funcons
_ = Bool
False
isEnv :: Funcons -> Bool
isEnv Funcons
f = Funcons -> Bool
isMap Funcons
f
isMap :: Funcons -> Bool
isMap (FValue (Map ValueMaps Values
_)) = Bool
True
isMap Funcons
_ = Bool
False
isSet :: Funcons -> Bool
isSet (FValue (Set ValueSets Values
_)) = Bool
True
isSet Funcons
_ = Bool
False
isTup :: p -> Bool
isTup p
_ = Bool
False
isSort :: Funcons -> Bool
isSort (FValue (ComputationType ComputationTypes
_)) = Bool
True
isSort Funcons
_ = Bool
False
isSort_ :: Values t -> Bool
isSort_ (ComputationType ComputationTypes t
_) = Bool
True
isSort_ Values t
_ = Bool
False
isType :: Funcons -> Bool
isType (FValue (ComputationType (Type Types
_))) = Bool
True
isType Funcons
_ = Bool
False
isVec :: Funcons -> Bool
isVec (FValue (Vector Vector Values
_)) = Bool
True
isVec Funcons
_ = Bool
False
isCharacter_ :: Values t -> Bool
isCharacter_ Values t
v = forall a. Maybe a -> Bool
isJust (forall t. HasValues t => Values t -> Maybe Char
upcastCharacter Values t
v)
integers_,values_ :: Funcons
integers_ :: Funcons
integers_ = Types -> Funcons
type_ forall t. Types t
Integers
values_ :: Funcons
values_ = Types -> Funcons
type_ forall t. Types t
VAL.Values
nulltype_ :: Funcons
nulltype_ = Types -> Funcons
type_ forall t. Types t
NullType
vectors_ :: Types -> Funcons
vectors_ :: Types -> Funcons
vectors_ = Types -> Funcons
type_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasValues t => Types t -> Types t
vectors
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 (Int -> TPattern -> ShowS
[TPattern] -> ShowS
TPattern -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TPattern] -> ShowS
$cshowList :: [TPattern] -> ShowS
show :: TPattern -> String
$cshow :: TPattern -> String
showsPrec :: Int -> TPattern -> ShowS
$cshowsPrec :: Int -> TPattern -> ShowS
Show, TPattern -> TPattern -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TPattern -> TPattern -> Bool
$c/= :: TPattern -> TPattern -> Bool
== :: TPattern -> TPattern -> Bool
$c== :: TPattern -> TPattern -> Bool
Eq, Eq TPattern
TPattern -> TPattern -> Bool
TPattern -> TPattern -> Ordering
TPattern -> TPattern -> TPattern
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: TPattern -> TPattern -> TPattern
$cmin :: TPattern -> TPattern -> TPattern
max :: TPattern -> TPattern -> TPattern
$cmax :: TPattern -> TPattern -> TPattern
>= :: TPattern -> TPattern -> Bool
$c>= :: TPattern -> TPattern -> Bool
> :: TPattern -> TPattern -> Bool
$c> :: TPattern -> TPattern -> Bool
<= :: TPattern -> TPattern -> Bool
$c<= :: TPattern -> TPattern -> Bool
< :: TPattern -> TPattern -> Bool
$c< :: TPattern -> TPattern -> Bool
compare :: TPattern -> TPattern -> Ordering
$ccompare :: TPattern -> TPattern -> Ordering
Ord, ReadPrec [TPattern]
ReadPrec TPattern
Int -> ReadS TPattern
ReadS [TPattern]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [TPattern]
$creadListPrec :: ReadPrec [TPattern]
readPrec :: ReadPrec TPattern
$creadPrec :: ReadPrec TPattern
readList :: ReadS [TPattern]
$creadList :: ReadS [TPattern]
readsPrec :: Int -> ReadS TPattern
$creadsPrec :: Int -> ReadS TPattern
Read)
data DataTypeMembers = Name [TPattern] [DataTypeAltt]
deriving (Int -> DataTypeMembers -> ShowS
[DataTypeMembers] -> ShowS
DataTypeMembers -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataTypeMembers] -> ShowS
$cshowList :: [DataTypeMembers] -> ShowS
show :: DataTypeMembers -> String
$cshow :: DataTypeMembers -> String
showsPrec :: Int -> DataTypeMembers -> ShowS
$cshowsPrec :: Int -> DataTypeMembers -> ShowS
Show)
data DataTypeAltt = DataTypeInclusionn FTerm
| DataTypeMemberConstructor Name [FTerm] (Maybe [TPattern])
deriving (Int -> DataTypeAltt -> ShowS
[DataTypeAltt] -> ShowS
DataTypeAltt -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DataTypeAltt] -> ShowS
$cshowList :: [DataTypeAltt] -> ShowS
show :: DataTypeAltt -> String
$cshow :: DataTypeAltt -> String
showsPrec :: Int -> DataTypeAltt -> ShowS
$cshowsPrec :: Int -> DataTypeAltt -> ShowS
Show)
typeLookup :: Name -> TypeRelation -> Maybe DataTypeMembers
typeLookup :: Name -> TypeRelation -> Maybe DataTypeMembers
typeLookup = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup
emptyTypeRelation :: TypeRelation
emptyTypeRelation :: TypeRelation
emptyTypeRelation = forall k a. Map k a
M.empty
typeEnvUnions :: [TypeRelation] -> TypeRelation
typeEnvUnions :: [TypeRelation] -> TypeRelation
typeEnvUnions = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr TypeRelation -> TypeRelation -> TypeRelation
typeEnvUnion TypeRelation
emptyTypeRelation
typeEnvUnion :: TypeRelation -> TypeRelation -> TypeRelation
typeEnvUnion :: TypeRelation -> TypeRelation -> TypeRelation
typeEnvUnion = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (\DataTypeMembers
_ DataTypeMembers
_ -> forall a. HasCallStack => String -> a
error String
"duplicate type-name")
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList