{-# 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

-- |
-- 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]
                | FBinding Funcons [Funcons] -- required for map-notation
                | FValue Values
                | FSortSeq Funcons VAL.SeqSortOp
                | FSortPower Funcons Funcons {- evals to natural number -}
                | 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)

-- |
-- 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 :: 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" 

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

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

-- | Funcon term representation identical to 'Funcons',
-- but with meta-variables.
data FTerm  = TVar MetaVar
            | TName Name
            | TApp Name [FTerm]
            | TSeq [FTerm] -- a sequence of terms, consumed during substitution
--            | TList [FTerm]
            | TSet  [FTerm]
            | TMap  [FTerm]
            | TBinding FTerm FTerm -- latter can be a sequence
            | TFuncon Funcons
            | TSortSeq FTerm VAL.SeqSortOp
            | TSortPower FTerm FTerm {- should eval to a natural number -}
            | TSortUnion FTerm FTerm
            | TSortInter FTerm FTerm  
            | TSortComplement FTerm
            | TSortComputes FTerm
            | TSortComputesFrom FTerm FTerm
            | TAny -- used whenever funcon terms may have holes in them
                   -- currently only the case in "downwards" flowing signals
            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

-- | Representation of builtin types.
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)
--  , ("naturals",            Naturals)
--  , ("nats",                Naturals)
  , (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)
--  , ("lists",     Lists)
--  , ("vectors",   Vectors)
  ]

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)]

--- smart constructors for values

-- | Creates an integer 'literal'.
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

-- | Creates a natural 'literal'.
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

-- | Creates an atom from a 'String'.
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

-- | Creates a string literal.
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

-- | The empty map as a 'Funcons'.
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_

-- | The empty set as a 'Funcons'.
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

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

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
-- idval :: Values -> Values
-- idval = ID . ID'

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,[])
 
-- 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 /unicode/ representation of an assci value.
-- Otherwise it returns the original value.
--- Value specific

-- | Attempt to downcast a funcon term to a value.
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 (FList fs) = List <$> mapM recursiveFunconValue fs
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)

-- 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.
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 environment

-- | The typing environment maps datatype names to their definitions.
type TypeRelation = 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.
-- Variable /X/ be a sequence variable.
type TypeParam  = (Maybe MetaVar, Maybe VAL.SeqSortOp, FTerm)
data TPattern   = TPWildCard
                | TPVar MetaVar 
                | TPSeqVar MetaVar VAL.SeqSortOp
                | TPLit FTerm {- should rewrite to a type -}
                | 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)

-- | A datatype has `zero or more' type parameters and
-- `zero or more' alternatives.
data DataTypeMembers = DataTypeMemberss 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)

-- | 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 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)

-- | Lookup the definition of a datatype in the typing environment.
typeLookup :: Name -> TypeRelation -> Maybe DataTypeMembers
typeLookup :: Name -> TypeRelation -> Maybe DataTypeMembers
typeLookup = forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup

-- | The empty 'TypeRelation'.
emptyTypeRelation :: TypeRelation
emptyTypeRelation :: TypeRelation
emptyTypeRelation = forall k a. Map k a
M.empty

-- | Unites a list of 'TypeRelation's.
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

-- | Unites two 'TypeRelation's.
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")

-- | Creates a `TypeRelation' from a list.
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList :: [(Name, DataTypeMembers)] -> TypeRelation
typeEnvFromList = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList