{-# LANGUAGE GADTs, DataKinds #-}
{-# LANGUAGE KindSignatures #-}

-- | Number space types and functions.
module Language.Drasil.Space (
  -- * Types
  Space(..), 
  RealInterval(..), Inclusive(..),
  DomainDesc(..), RTopology(..), DiscreteDomainDesc, ContinuousDomainDesc,
  -- * Class
  HasSpace(..),
  -- * Functions
  getActorName, getInnerSpace, mkFunction
) where

import qualified Data.List.NonEmpty as NE

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

-- 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
  | Radians
  | Vect Space
  | Array Space
  | Actor String
  | DiscreteD [Double]
  | DiscreteS [String] --ex. let Meal = {"breakfast", "lunch", "dinner"}
  | 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
/= :: Space -> Space -> Bool
$c/= :: Space -> Space -> Bool
== :: Space -> Space -> Bool
$c== :: 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
showList :: [Space] -> ShowS
$cshowList :: [Space] -> ShowS
show :: Space -> String
$cshow :: Space -> String
showsPrec :: Int -> Space -> ShowS
$cshowsPrec :: Int -> Space -> ShowS
Show)

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

type Primitive = Space

mkFunction :: [Primitive] -> Primitive -> Space
mkFunction :: [Space] -> Space -> Space
mkFunction []  = String -> Space -> Space
forall a. HasCallStack => String -> a
error "Function space creation requires at least 1 input Space"
mkFunction ins :: [Space]
ins = NonEmpty Space -> Space -> Space
Function ([Space] -> NonEmpty Space
forall a. [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 n :: String
n) = String
n
getActorName _ = ShowS
forall a. HasCallStack => String -> a
error "getActorName called on non-actor space"

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