{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- | Number space types and functions.
module Language.Drasil.Space (
  -- * Types
  Space(..), Primitive,
  RealInterval(..), Inclusive(..),
  DomainDesc(..), RTopology(..), DiscreteDomainDesc, ContinuousDomainDesc,
  -- * Class
  HasSpace(..),
  -- * Functions
  getActorName, getInnerSpace, mkFunction, isBasicNumSpace,
  assertReal, assertNumeric, assertNonNatNumeric, assertEquivNumeric, assertIndexLike, assertBoolean,
  assertSet,
  assertVector, assertNumericVector, assertNonNatNumVector, assertRealVector,
  assertFunction, assertNonFunction
) where

import qualified Data.List.NonEmpty        as NE

import           Control.Lens              (Getter)
import           Language.Drasil.Symbol    (Symbol)

-- FIXME: These need to be spaces and not just types.

-- | The difference kinds of spaces that may exist. This type holds
-- numerical spaces (such as the set of integers, rationals, etc.),
-- a space for booleans, a space for characters, dimensional spaces (vectors, arrays, etc.),
-- a space for Actors, discrete sets (both for numbers and strings), and a void space.
data Space =
    Integer
  | Rational
  | Real
  | Natural
  | Boolean
  | Char
  | String
  | Vect Space -- TODO: Length for vectors?
  | Set Space
  | Matrix Int Int Space
  | Array Space
  | Actor String 
  | Function (NE.NonEmpty Primitive) Primitive
  | Void
  deriving (Space -> Space -> Bool
(Space -> Space -> Bool) -> (Space -> Space -> Bool) -> Eq Space
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Space -> Space -> Bool
== :: Space -> Space -> Bool
$c/= :: Space -> Space -> Bool
/= :: Space -> Space -> Bool
Eq, Int -> Space -> ShowS
[Space] -> ShowS
Space -> String
(Int -> Space -> ShowS)
-> (Space -> String) -> ([Space] -> ShowS) -> Show Space
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Space -> ShowS
showsPrec :: Int -> Space -> ShowS
$cshow :: Space -> String
show :: Space -> String
$cshowList :: [Space] -> ShowS
showList :: [Space] -> ShowS
Show)

-- | HasSpace is anything which has a 'Space'.
class HasSpace c where
  -- | Provides a 'Getter' to the 'Space'.
  typ      :: Getter c Space

type Primitive = Space

mkFunction :: [Primitive] -> Primitive -> Space
mkFunction :: [Space] -> Space -> Space
mkFunction []  = String -> Space -> Space
forall a. HasCallStack => String -> a
error String
"Function space creation requires at least 1 input Space"
mkFunction [Space]
ins = NonEmpty Space -> Space -> Space
Function ([Space] -> NonEmpty Space
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [Space]
ins)

-- The 'spaces' below are all good.

-- | Topology of a subset of reals.
data RTopology = Continuous | Discrete

-- | Describes the domain of a 'Symbol' given a topology. Can be bounded or encase all of the domain.
data DomainDesc (tplgy :: RTopology) a b where
  BoundedDD :: Symbol -> RTopology -> a -> b -> DomainDesc 'Discrete a b
  AllDD     :: Symbol -> RTopology -> DomainDesc 'Continuous a b

type DiscreteDomainDesc a b = DomainDesc 'Discrete a b
type ContinuousDomainDesc a b = DomainDesc 'Continuous a b

-- | Inclusive or exclusive bounds.
data Inclusive = Inc | Exc

-- | A RealInterval is a subset of 'Real' (as a 'Space').
-- These come in different flavours.
-- For now, we embed 'Expr' for the bounds, but that will change as well.
data RealInterval a b where
  Bounded :: (Inclusive, a) -> (Inclusive, b) -> RealInterval a b -- ^ Interval from (x .. y).
  UpTo    :: (Inclusive, a) -> RealInterval a b                   -- ^ Interval from (-infinity .. x).
  UpFrom  :: (Inclusive, b) -> RealInterval a b                   -- ^ Interval from (x .. infinity).

-- | Gets the name of an 'Actor'.
getActorName :: Space -> String
getActorName :: Space -> String
getActorName (Actor String
n) = String
n
getActorName Space
_         = ShowS
forall a. HasCallStack => String -> a
error String
"getActorName called on non-actor space"

-- | Gets the inner 'Space' of a vector or set.
getInnerSpace :: Space -> Space
getInnerSpace :: Space -> Space
getInnerSpace (Vect Space
s) = Space
s
getInnerSpace (Set Space
s) = Space
s
getInnerSpace Space
_        = String -> Space
forall a. HasCallStack => String -> a
error String
"getInnerSpace called on non-vector space"

-- | Is this Space a basic numeric space?
isBasicNumSpace :: Space -> Bool
isBasicNumSpace :: Space -> Bool
isBasicNumSpace Space
Integer     = Bool
True
isBasicNumSpace Space
Rational    = Bool
True
isBasicNumSpace Space
Real        = Bool
True
isBasicNumSpace Space
Natural     = Bool
True
isBasicNumSpace Space
Boolean     = Bool
False
isBasicNumSpace Space
Char        = Bool
False
isBasicNumSpace Space
String      = Bool
False
isBasicNumSpace Set {}      = Bool
False
isBasicNumSpace Vect {}     = Bool
False
isBasicNumSpace Matrix {}   = Bool
False
isBasicNumSpace Array {}    = Bool
False
isBasicNumSpace Actor {}    = Bool
False
isBasicNumSpace Function {} = Bool
False
isBasicNumSpace Space
Void        = Bool
False

-- | Assert that a 'Space' is 'Real' or return a formatted error message.
assertReal :: Space -> (String -> String) -> Either String ()
assertReal :: Space -> ShowS -> Either String ()
assertReal Space
Real ShowS
_   = () -> Either String ()
forall a b. b -> Either a b
Right ()
assertReal Space
s    ShowS
msg = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that a 'Space' is "numeric" or return a formatted error message.
assertNumeric :: Space -> (String -> String) -> Either String ()
assertNumeric :: Space -> ShowS -> Either String ()
assertNumeric Space
s ShowS
msg
  | Space -> Bool
isBasicNumSpace Space
s = () -> Either String ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise         = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that a numeric 'Space' is not 'Natural' or return a formatted error
-- message.
assertNonNatNumeric :: Space -> (String -> String) -> Either String ()
assertNonNatNumeric :: Space -> ShowS -> Either String ()
assertNonNatNumeric Space
s ShowS
msg
  | Space -> Bool
isBasicNumSpace Space
s Bool -> Bool -> Bool
&& Space
s Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
Natural = () -> Either String ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise                         = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that two numeric 'Space's are equivalent or return a formatted error
-- message.
assertEquivNumeric ::  Space -> Space -> (String -> String -> String) -> Either String ()
assertEquivNumeric :: Space -> Space -> (String -> ShowS) -> Either String ()
assertEquivNumeric Space
l Space
r String -> ShowS
msg 
  | Space -> Bool
isBasicNumSpace Space
l Bool -> Bool -> Bool
&& Space
l Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
r = () -> Either String ()
forall a b. b -> Either a b
Right ()
  | Bool
otherwise                   = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> ShowS
msg (Space -> String
forall a. Show a => a -> String
show Space
l) (Space -> String
forall a. Show a => a -> String
show Space
r)

-- | Assert that a 'Space' is an index-like type (Integer or Natural) or return a
-- formatted error message.
assertIndexLike :: Space -> (String -> String) -> Either String ()
assertIndexLike :: Space -> ShowS -> Either String ()
assertIndexLike Space
Integer ShowS
_   = () -> Either String ()
forall a b. b -> Either a b
Right ()
assertIndexLike Space
Natural ShowS
_   = () -> Either String ()
forall a b. b -> Either a b
Right ()
assertIndexLike Space
t       ShowS
msg = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
t

-- | Assert that a 'Space' is a 'Boolean' or return a formatted error message.
assertBoolean :: Space -> (String -> String) -> Either String ()
assertBoolean :: Space -> ShowS -> Either String ()
assertBoolean Space
Boolean ShowS
_   = () -> Either String ()
forall a b. b -> Either a b
Right ()
assertBoolean Space
sp      ShowS
msg = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
sp

-- | Assert that a 'Space' is a 'Set' and return either the element type or a
-- formatted error message.
assertSet :: Space -> (String -> String) -> Either String Space
assertSet :: Space -> ShowS -> Either String Space
assertSet (Set Space
t) ShowS
_   = Space -> Either String Space
forall a b. b -> Either a b
Right Space
t
assertSet Space
s       ShowS
msg = String -> Either String Space
forall a b. a -> Either a b
Left (String -> Either String Space) -> String -> Either String Space
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that a 'Space' is a 'Vect' and return either the element type or a
-- formatted error message.
assertVector :: Space -> (String -> String) -> Either String Space
assertVector :: Space -> ShowS -> Either String Space
assertVector (Vect Space
t) ShowS
_   = Space -> Either String Space
forall a b. b -> Either a b
Right Space
t
assertVector Space
s        ShowS
msg = String -> Either String Space
forall a b. a -> Either a b
Left (String -> Either String Space) -> String -> Either String Space
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that a 'Space' is a numeric vector (i.e., a vector of a basic
-- numeric type) and return either the numeric type or a formatted error
-- message.
assertNumericVector :: Space -> (String -> String) -> Either String Space
assertNumericVector :: Space -> ShowS -> Either String Space
assertNumericVector (Vect Space
t) ShowS
_ | Space -> Bool
isBasicNumSpace Space
t = Space -> Either String Space
forall a b. b -> Either a b
Right Space
t
assertNumericVector Space
s ShowS
msg                          = String -> Either String Space
forall a b. a -> Either a b
Left (String -> Either String Space) -> String -> Either String Space
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that a 'Space' is a non-'Natural' numeric vector and return either
-- the numeric type or a formatted error message.
assertNonNatNumVector :: (String -> String) -> Space -> Either String Space
assertNonNatNumVector :: ShowS -> Space -> Either String Space
assertNonNatNumVector ShowS
msg vn :: Space
vn@(Vect Space
Natural)              = String -> Either String Space
forall a b. a -> Either a b
Left (String -> Either String Space) -> String -> Either String Space
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
vn
assertNonNatNumVector ShowS
_   (Vect Space
et) | Space -> Bool
isBasicNumSpace Space
et = Space -> Either String Space
forall a b. b -> Either a b
Right Space
et
assertNonNatNumVector ShowS
msg Space
t                              = String -> Either String Space
forall a b. a -> Either a b
Left (String -> Either String Space) -> String -> Either String Space
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
t

-- | Assert that a 'Space' is a 'Vect' of 'Real's or return a formatted error
-- message.
assertRealVector :: Space -> (String -> String) -> Either String ()
assertRealVector :: Space -> ShowS -> Either String ()
assertRealVector (Vect Space
Real) ShowS
_   = () -> Either String ()
forall a b. b -> Either a b
Right ()
assertRealVector Space
t           ShowS
msg = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
t

-- | Assert that a 'Space' is a 'Function', returning either the parameters and
-- output type or a formatted error message.
assertFunction :: Space -> (String -> String) -> Either String (NE.NonEmpty Primitive, Primitive)
assertFunction :: Space -> ShowS -> Either String (NonEmpty Space, Space)
assertFunction (Function NonEmpty Space
params Space
out) ShowS
_   = (NonEmpty Space, Space) -> Either String (NonEmpty Space, Space)
forall a b. b -> Either a b
Right (NonEmpty Space
params, Space
out)
assertFunction Space
s                     ShowS
msg = String -> Either String (NonEmpty Space, Space)
forall a b. a -> Either a b
Left (String -> Either String (NonEmpty Space, Space))
-> String -> Either String (NonEmpty Space, Space)
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
s

-- | Assert that a 'Space' is anything but a 'Function' or return a formatted
-- error message.
assertNonFunction :: Space -> (String -> String) -> Either String ()
assertNonFunction :: Space -> ShowS -> Either String ()
assertNonFunction f :: Space
f@Function{} ShowS
msg = String -> Either String ()
forall a b. a -> Either a b
Left (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ ShowS
msg ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ Space -> String
forall a. Show a => a -> String
show Space
f
assertNonFunction Space
_            ShowS
_   = () -> Either String ()
forall a b. b -> Either a b
Right ()