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