{-# 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
(Funcons -> Funcons -> Bool)
-> (Funcons -> Funcons -> Bool) -> Eq Funcons
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
Eq Funcons
-> (Funcons -> Funcons -> Ordering)
-> (Funcons -> Funcons -> Bool)
-> (Funcons -> Funcons -> Bool)
-> (Funcons -> Funcons -> Bool)
-> (Funcons -> Funcons -> Bool)
-> (Funcons -> Funcons -> Funcons)
-> (Funcons -> Funcons -> Funcons)
-> Ord 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
$cp1Ord :: Eq Funcons
Ord, Int -> Funcons -> ShowS
[Funcons] -> ShowS
Funcons -> String
(Int -> Funcons -> ShowS)
-> (Funcons -> String) -> ([Funcons] -> ShowS) -> Show Funcons
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]
(Int -> ReadS Funcons)
-> ReadS [Funcons]
-> ReadPrec Funcons
-> ReadPrec [Funcons]
-> Read 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 | [Funcons] -> Bool
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
(FTerm -> FTerm -> Bool) -> (FTerm -> FTerm -> Bool) -> Eq FTerm
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
Eq FTerm
-> (FTerm -> FTerm -> Ordering)
-> (FTerm -> FTerm -> Bool)
-> (FTerm -> FTerm -> Bool)
-> (FTerm -> FTerm -> Bool)
-> (FTerm -> FTerm -> Bool)
-> (FTerm -> FTerm -> FTerm)
-> (FTerm -> FTerm -> FTerm)
-> Ord 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
$cp1Ord :: Eq FTerm
Ord, Int -> FTerm -> ShowS
[FTerm] -> ShowS
FTerm -> String
(Int -> FTerm -> ShowS)
-> (FTerm -> String) -> ([FTerm] -> ShowS) -> Show FTerm
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]
(Int -> ReadS FTerm)
-> ReadS [FTerm]
-> ReadPrec FTerm
-> ReadPrec [FTerm]
-> Read 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 -> Funcons
inject = Values Funcons -> Funcons
FValue
  project :: Funcons -> Maybe (Values Funcons)
project Funcons
f = case Funcons
f of
    FValue Values Funcons
v  -> Values Funcons -> Maybe (Values Funcons)
forall a. a -> Maybe a
Just Values Funcons
v
    Funcons
_         -> Maybe (Values 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 Funcons
binary32 = Name -> [Funcons] -> Values Funcons
forall t. Name -> [t] -> Values t
ADTVal Name
"binary32" []

binary64 :: Values
binary64 :: Values Funcons
binary64 = Name -> [Funcons] -> Values Funcons
forall t. Name -> [t] -> Values t
ADTVal Name
"binary64" []

adtval :: Name -> [Values] -> Values
adtval :: Name -> [Values Funcons] -> Values Funcons
adtval Name
nm = Name -> [Funcons] -> Values Funcons
forall t. Name -> [t] -> Values t
ADTVal Name
nm ([Funcons] -> Values Funcons)
-> ([Values Funcons] -> [Funcons])
-> [Values Funcons]
-> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue

tuple_val__ :: [Values] -> Values
tuple_val__ :: [Values Funcons] -> Values Funcons
tuple_val__ = Name -> [Values Funcons] -> Values Funcons
adtval Name
"tuple"
tuple_val_ :: [Values Funcons] -> Funcons
tuple_val_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> ([Values Funcons] -> Values Funcons)
-> [Values Funcons]
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
tuple_val__

nullaryTypes :: [(Name,Types)]
nullaryTypes :: [(Name, Types)]
nullaryTypes =
  [ (Name
"algebraic-datatypes", Types
forall t. Types t
ADTs)
  , (Name
"adts"               , Types
forall t. Types t
ADTs)
--  , ("naturals",            Naturals)
--  , ("nats",                Naturals)
  , (Name
"rationals",           Types
forall t. Types t
Rationals)
  , (Name
"values",              Types
forall t. Types t
VAL.Values)
  ]

unaryTypes :: [(Name,Types->Types)]
unaryTypes :: [(Name, Types -> Types)]
unaryTypes =
  [ (Name
"multisets", Types -> Types
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", IEEEFormats -> Types
forall t. IEEEFormats -> Types t
IEEEFloats)]

--- smart constructors for values

-- | Creates an integer 'literal'.
int_ :: Int -> Funcons
int_ :: Int -> Funcons
int_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Int -> Values Funcons) -> Int -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Values Funcons
forall t. Integer -> Values t
mk_integers (Integer -> Values Funcons)
-> (Int -> Integer) -> Int -> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger

-- | Creates a natural 'literal'.
nat_ :: Int -> Funcons
nat_ :: Int -> Funcons
nat_ Int
i | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0      = Int -> Funcons
int_ Int
i
       | Bool
otherwise  = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons) -> Values Funcons -> Funcons
forall a b. (a -> b) -> a -> b
$ Integer -> Values Funcons
forall t. Integer -> Values t
mk_naturals (Integer -> Values Funcons) -> Integer -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger Int
i

bool_ :: Bool -> Funcons
bool_ :: Bool -> Funcons
bool_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Bool -> Values Funcons) -> Bool -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Values Funcons
bool__

bool__ :: Bool -> Values 
bool__ :: Bool -> Values Funcons
bool__ = Bool -> Values Funcons
forall t. Bool -> Values t
VAL.tobool

-- | Creates an atom from a 'String'.
atom_ :: String -> Funcons
atom_ :: String -> Funcons
atom_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (String -> Values Funcons) -> String -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Values Funcons
forall t. String -> Values t
Atom

-- | Creates a string literal.
string_ :: String -> Funcons
string_ :: String -> Funcons
string_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (String -> Values Funcons) -> String -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Values Funcons
string__
string__ :: String -> Values
string__ :: String -> Values Funcons
string__ = Name -> [Funcons] -> Values Funcons
forall t. Name -> [t] -> Values t
ADTVal Name
"list" ([Funcons] -> Values Funcons)
-> (String -> [Funcons]) -> String -> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Funcons) -> String -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Char -> Funcons
char_ 

char_ :: Char -> Funcons
char_ :: Char -> Funcons
char_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Char -> Values Funcons) -> Char -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Values Funcons
char__

char__ :: Char -> Values
char__ :: Char -> Values Funcons
char__ = Char -> Values Funcons
forall t. HasValues t => Char -> Values t
mk_unicode_characters 

list__ :: [Values] -> Values
list__ :: [Values Funcons] -> Values Funcons
list__ = [Values Funcons] -> Values Funcons
forall t. HasValues t => [Values t] -> Values t
VAL.list

vector__ :: [Values] -> Values
vector__ :: [Values Funcons] -> Values Funcons
vector__ = [Values Funcons] -> Values Funcons
forall t. HasValues t => [Values t] -> Values t
VAL.vector

tuple__ :: [Values] -> Values
tuple__ :: [Values Funcons] -> Values Funcons
tuple__ = [Values Funcons] -> Values Funcons
forall t. HasValues t => [Values t] -> Values t
VAL.tuple


float_ :: Double -> Funcons
float_ :: Double -> Funcons
float_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Double -> Values Funcons) -> Double -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Values Funcons
forall t. Double -> Values t
Float

ieee_float_32_ :: Float -> Funcons
ieee_float_32_ :: Float -> Funcons
ieee_float_32_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Float -> Values Funcons) -> Float -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> Values Funcons
forall t. Float -> Values t
IEEE_Float_32
ieee_float_64_ :: Double -> Funcons
ieee_float_64_ :: Double -> Funcons
ieee_float_64_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Double -> Values Funcons) -> Double -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Values Funcons
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 -> Funcons
FValue (ValueMaps (Values Funcons) -> Values Funcons
forall t. ValueMaps (Values t) -> Values t
Map ValueMaps (Values Funcons)
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 -> Funcons
FValue (ValueSets (Values Funcons) -> Values Funcons
forall t. ValueSets (Values t) -> Values t
Set ValueSets (Values Funcons)
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 -> Funcons
FValue (Values Funcons -> Funcons)
-> (Types -> Values Funcons) -> Types -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Types -> Values Funcons
typeVal

sort_ :: ComputationTypes -> Funcons
sort_ :: ComputationTypes -> Funcons
sort_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (ComputationTypes -> Values Funcons)
-> ComputationTypes
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputationTypes -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType

comp_type_ :: ComputationTypes -> Funcons
comp_type_ :: ComputationTypes -> Funcons
comp_type_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (ComputationTypes -> Values Funcons)
-> ComputationTypes
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ComputationTypes -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType 

vec :: V.Vector (Values) -> Funcons
vec :: Vector (Values Funcons) -> Funcons
vec = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> (Vector (Values Funcons) -> Values Funcons)
-> Vector (Values Funcons)
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (Values Funcons) -> Values Funcons
forall t. ValueVectors (Values t) -> Values t
Vector

vec_ :: [Values] -> Funcons
vec_ :: [Values Funcons] -> Funcons
vec_ = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> ([Values Funcons] -> Values Funcons)
-> [Values Funcons]
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Vector (Values Funcons) -> Values Funcons
forall t. ValueVectors (Values t) -> Values t
Vector (Vector (Values Funcons) -> Values Funcons)
-> ([Values Funcons] -> Vector (Values Funcons))
-> [Values Funcons]
-> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Vector (Values Funcons)
forall a. [a] -> Vector a
V.fromList
-- idval :: Values -> Values
-- idval = ID . ID'

typeVal :: Types -> Values
typeVal :: Types -> Values Funcons
typeVal = ComputationTypes -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes -> Values Funcons)
-> (Types -> ComputationTypes) -> Types -> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Types -> ComputationTypes
forall t. Types t -> ComputationTypes t
Type

fvalues :: [Values] -> [Funcons]
fvalues :: [Values Funcons] -> [Funcons]
fvalues = (Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue

listval :: [Values] -> Funcons
listval :: [Values Funcons] -> Funcons
listval = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> ([Values Funcons] -> Values Funcons)
-> [Values Funcons]
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Funcons] -> Values Funcons
forall t. Name -> [t] -> Values t
ADTVal Name
"list" ([Funcons] -> Values Funcons)
-> ([Values Funcons] -> [Funcons])
-> [Values Funcons]
-> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue

setval :: [Values] -> Funcons
setval :: [Values Funcons] -> Funcons
setval = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> ([Values Funcons] -> Values Funcons)
-> [Values Funcons]
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
setval_

setval_ :: [Values] -> Values
setval_ :: [Values Funcons] -> Values Funcons
setval_ = ValueSets (Values Funcons) -> Values Funcons
forall t. ValueSets (Values t) -> Values t
Set (ValueSets (Values Funcons) -> Values Funcons)
-> ([Values Funcons] -> ValueSets (Values Funcons))
-> [Values Funcons]
-> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> ValueSets (Values Funcons)
forall a. Ord a => [a] -> Set a
S.fromList

mapval :: [Values] -> Funcons
mapval :: [Values Funcons] -> Funcons
mapval = Values Funcons -> Funcons
FValue (Values Funcons -> Funcons)
-> ([Values Funcons] -> Values Funcons)
-> [Values Funcons]
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
mapval_

mapval_ :: [Values] -> Values
mapval_ :: [Values Funcons] -> Values Funcons
mapval_ [Values Funcons]
mvs = case (Values Funcons -> Maybe (Values Funcons, [Values Funcons]))
-> [Values Funcons] -> Maybe [(Values Funcons, [Values Funcons])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values Funcons -> Maybe (Values Funcons, [Values Funcons])
fromBinding [Values Funcons]
mvs of 
  Just [(Values Funcons, [Values Funcons])]
vs -> ValueMaps (Values Funcons) -> Values Funcons
forall t. ValueMaps (Values t) -> Values t
Map (ValueMaps (Values Funcons) -> Values Funcons)
-> ValueMaps (Values Funcons) -> Values Funcons
forall a b. (a -> b) -> a -> b
$ ([Values Funcons] -> [Values Funcons] -> [Values Funcons])
-> [(Values Funcons, [Values Funcons])]
-> ValueMaps (Values Funcons)
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
M.fromListWith [Values Funcons] -> [Values Funcons] -> [Values Funcons]
forall a b. a -> b -> a
const [(Values Funcons, [Values Funcons])]
vs
  Maybe [(Values Funcons, [Values Funcons])]
_       -> String -> Values Funcons
forall a. HasCallStack => String -> a
error String
"mapval: invalid map-notation"

fromBinding :: Values -> Maybe (Values, [Values])
fromBinding :: Values Funcons -> Maybe (Values Funcons, [Values Funcons])
fromBinding (ADTVal Name
"tuple" (Funcons
k':[Funcons]
vs')) = do
  Values Funcons
k   <- Funcons -> Maybe (Values Funcons)
forall t. HasValues t => t -> Maybe (Values t)
project Funcons
k'
  [Values Funcons]
vs  <- (Funcons -> Maybe (Values Funcons))
-> [Funcons] -> Maybe [Values Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe (Values Funcons)
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
vs' 
  (Values Funcons, [Values Funcons])
-> Maybe (Values Funcons, [Values Funcons])
forall (m :: * -> *) a. Monad m => a -> m a
return (Values Funcons
k,[Values Funcons]
vs)
fromBinding Values Funcons
k = (Values Funcons, [Values Funcons])
-> Maybe (Values Funcons, [Values Funcons])
forall a. a -> Maybe a
Just (Values Funcons
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 Funcons
v) = Values Funcons -> Types
forall t. Values t -> Types t
downcastValueType Values Funcons
v
downcastType Funcons
_ = String -> Types
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
_ = String -> ComputationTypes
forall a. HasCallStack => String -> a
error String
"downcasting to sort failed"

downcastValue :: Funcons -> Values
downcastValue :: Funcons -> Values Funcons
downcastValue (FValue Values Funcons
v) = Values Funcons
v
downcastValue Funcons
_ = String -> Values Funcons
forall a. HasCallStack => String -> a
error String
"downcasting to value failed"

recursiveFunconValue :: Funcons -> Maybe Values
recursiveFunconValue :: Funcons -> Maybe (Values Funcons)
recursiveFunconValue (FValue Values Funcons
v) = Values Funcons -> Maybe (Values Funcons)
forall a. a -> Maybe a
Just Values Funcons
v
--recursiveFunconValue (FList fs) = List <$> mapM recursiveFunconValue fs
recursiveFunconValue (FSet [Funcons]
fs)  = ValueSets (Values Funcons) -> Values Funcons
forall t. ValueSets (Values t) -> Values t
Set (ValueSets (Values Funcons) -> Values Funcons)
-> ([Values Funcons] -> ValueSets (Values Funcons))
-> [Values Funcons]
-> Values Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> ValueSets (Values Funcons)
forall a. Ord a => [a] -> Set a
S.fromList ([Values Funcons] -> Values Funcons)
-> Maybe [Values Funcons] -> Maybe (Values Funcons)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Funcons -> Maybe (Values Funcons))
-> [Funcons] -> Maybe [Values Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe (Values Funcons)
recursiveFunconValue [Funcons]
fs
recursiveFunconValue (FMap [Funcons]
fs)  = do
  [Values Funcons]
vs      <- (Funcons -> Maybe (Values Funcons))
-> [Funcons] -> Maybe [Values Funcons]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Funcons -> Maybe (Values Funcons)
recursiveFunconValue [Funcons]
fs
  [(Values Funcons, [Values Funcons])]
assocs  <- (Values Funcons -> Maybe (Values Funcons, [Values Funcons]))
-> [Values Funcons] -> Maybe [(Values Funcons, [Values Funcons])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Values Funcons -> Maybe (Values Funcons, [Values Funcons])
fromBinding [Values Funcons]
vs
  Values Funcons -> Maybe (Values Funcons)
forall (m :: * -> *) a. Monad m => a -> m a
return (ValueMaps (Values Funcons) -> Values Funcons
forall t. ValueMaps (Values t) -> Values t
Map (ValueMaps (Values Funcons) -> Values Funcons)
-> ValueMaps (Values Funcons) -> Values Funcons
forall a b. (a -> b) -> a -> b
$ [(Values Funcons, [Values Funcons])] -> ValueMaps (Values Funcons)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Values Funcons, [Values Funcons])]
assocs)
recursiveFunconValue Funcons
_ = Maybe (Values Funcons)
forall a. Maybe a
Nothing

allEqual :: [Values] -> [Values] -> Bool
allEqual :: [Values Funcons] -> [Values Funcons] -> Bool
allEqual [Values Funcons]
xs [Values Funcons]
ys = [Values Funcons] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values Funcons]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Values Funcons] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values Funcons]
ys Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ((Values Funcons -> Values Funcons -> Bool)
-> [Values Funcons] -> [Values Funcons] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Values Funcons -> Values Funcons -> Bool
forall t. (HasValues t, Eq t) => Values t -> Values t -> Bool
(===) [Values Funcons]
xs [Values Funcons]
ys)

allUnEqual :: [Values] -> [Values] -> Bool
allUnEqual :: [Values Funcons] -> [Values Funcons] -> Bool
allUnEqual [Values Funcons]
xs [Values Funcons]
ys = [Values Funcons] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values Funcons]
xs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [Values Funcons] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values Funcons]
ys Bool -> Bool -> Bool
|| [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or ((Values Funcons -> Values Funcons -> Bool)
-> [Values Funcons] -> [Values Funcons] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Values Funcons -> Values Funcons -> Bool
forall t. (HasValues t, Eq t) => Values t -> Values t -> Bool
(=/=) [Values Funcons]
xs [Values Funcons]
ys)

isNull :: Funcons -> Bool
isNull :: Funcons -> Bool
isNull (FValue Values Funcons
n) = Values Funcons
n Values Funcons -> Values Funcons -> Bool
forall a. Eq a => a -> a -> Bool
== Values Funcons
forall t. Values t
null__
isNull Funcons
_ = Bool
False

hasStep :: Funcons -> Bool
hasStep (FValue Values Funcons
_) = Bool
False 
hasStep Funcons
_ = Bool
True
isVal :: Funcons -> Bool
isVal (FValue Values Funcons
_) = 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 Funcons
v)             = Values Funcons -> Bool
forall t. HasValues t => Values t -> Bool
isString_ Values Funcons
v
isString Funcons
_                      = Bool
False
isChar :: Funcons -> Bool
isChar (FValue Values Funcons
v)               = Maybe Char -> Bool
forall a. Maybe a -> Bool
isJust (Values Funcons -> Maybe Char
forall t. HasValues t => Values t -> Maybe Char
upcastCharacter Values Funcons
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 Funcons)
_))           = Bool
True
isMap Funcons
_                          = Bool
False
isSet :: Funcons -> Bool
isSet (FValue (Set ValueSets (Values Funcons)
_))           = 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 Funcons)
_))        = Bool
True
isVec Funcons
_                         = Bool
False
isCharacter_ :: Values t -> Bool
isCharacter_ Values t
v           = Maybe Char -> Bool
forall a. Maybe a -> Bool
isJust (Values t -> Maybe Char
forall t. HasValues t => Values t -> Maybe Char
upcastCharacter Values t
v)

integers_,values_ :: Funcons
integers_ :: Funcons
integers_ = Types -> Funcons
type_ Types
forall t. Types t
Integers
values_ :: Funcons
values_ = Types -> Funcons
type_ Types
forall t. Types t
VAL.Values
nulltype_ :: Funcons
nulltype_ = Types -> Funcons
type_ Types
forall t. Types t
NullType
vectors_ :: Types -> Funcons
vectors_ :: Types -> Funcons
vectors_ = Types -> Funcons
type_ (Types -> Funcons) -> (Types -> Types) -> Types -> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Types -> Types
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
(Int -> TPattern -> ShowS)
-> (TPattern -> String) -> ([TPattern] -> ShowS) -> Show TPattern
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
(TPattern -> TPattern -> Bool)
-> (TPattern -> TPattern -> Bool) -> Eq TPattern
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
Eq TPattern
-> (TPattern -> TPattern -> Ordering)
-> (TPattern -> TPattern -> Bool)
-> (TPattern -> TPattern -> Bool)
-> (TPattern -> TPattern -> Bool)
-> (TPattern -> TPattern -> Bool)
-> (TPattern -> TPattern -> TPattern)
-> (TPattern -> TPattern -> TPattern)
-> Ord 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
$cp1Ord :: Eq TPattern
Ord, ReadPrec [TPattern]
ReadPrec TPattern
Int -> ReadS TPattern
ReadS [TPattern]
(Int -> ReadS TPattern)
-> ReadS [TPattern]
-> ReadPrec TPattern
-> ReadPrec [TPattern]
-> Read 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
(Int -> DataTypeMembers -> ShowS)
-> (DataTypeMembers -> String)
-> ([DataTypeMembers] -> ShowS)
-> Show DataTypeMembers
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
(Int -> DataTypeAltt -> ShowS)
-> (DataTypeAltt -> String)
-> ([DataTypeAltt] -> ShowS)
-> Show DataTypeAltt
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 = Name -> TypeRelation -> Maybe DataTypeMembers
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup

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

-- | Unites a list of 'TypeRelation's.
typeEnvUnions :: [TypeRelation] -> TypeRelation
typeEnvUnions :: [TypeRelation] -> TypeRelation
typeEnvUnions = (TypeRelation -> TypeRelation -> TypeRelation)
-> TypeRelation -> [TypeRelation] -> TypeRelation
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 = (DataTypeMembers -> DataTypeMembers -> DataTypeMembers)
-> TypeRelation -> TypeRelation -> TypeRelation
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith (\DataTypeMembers
_ DataTypeMembers
_ -> String -> 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 = [(Name, DataTypeMembers)] -> TypeRelation
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList