-- | The Drasil Expression language
module Language.Drasil.Expr.Lang (
  Relation, ArithBinOp(..), EqBinOp(..), LABinOp(..), OrdBinOp(..),
  VVVBinOp(..), VVNBinOp(..), NVVBinOp(..), ESSBinOp(..), ESBBinOp(..),
  AssocConcatOper(..), AssocArithOper(..), AssocBoolOper(..), UFunc(..),
  UFuncB(..), UFuncVV(..), UFuncVN(..), Completeness(..), Expr(..)
) where

import Data.Either (fromRight, rights)
import qualified Data.Foldable as NE
import Data.List (nub)

import Drasil.Database (UID)

import Language.Drasil.Literal.Class (LiteralC (..))
import Language.Drasil.Literal.Lang (Literal (..))
import Language.Drasil.Space (DiscreteDomainDesc, RealInterval, Space,
  assertVector, assertNumericVector, assertNumeric, assertFunction,
  assertNonNatNumVector, assertRealVector, assertEquivNumeric, assertNonNatNumeric,
  assertIndexLike, assertSet, assertReal, assertBoolean)
import qualified Language.Drasil.Space as S
import Language.Drasil.WellTyped

-- * Expression Types

-- | A relation is just an expression ('Expr').
type Relation = Expr

-- Binary functions

-- | Arithmetic operators (fractional, power, and subtraction).
data ArithBinOp = Frac | Pow | Subt
  deriving ArithBinOp -> ArithBinOp -> Bool
(ArithBinOp -> ArithBinOp -> Bool)
-> (ArithBinOp -> ArithBinOp -> Bool) -> Eq ArithBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ArithBinOp -> ArithBinOp -> Bool
== :: ArithBinOp -> ArithBinOp -> Bool
$c/= :: ArithBinOp -> ArithBinOp -> Bool
/= :: ArithBinOp -> ArithBinOp -> Bool
Eq

-- | Equality operators (equal or not equal).
data EqBinOp = Eq | NEq
  deriving EqBinOp -> EqBinOp -> Bool
(EqBinOp -> EqBinOp -> Bool)
-> (EqBinOp -> EqBinOp -> Bool) -> Eq EqBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: EqBinOp -> EqBinOp -> Bool
== :: EqBinOp -> EqBinOp -> Bool
$c/= :: EqBinOp -> EqBinOp -> Bool
/= :: EqBinOp -> EqBinOp -> Bool
Eq

-- | Index operator. `Index` represents accessing an element at a specific
-- index, while `IndexOf` represents finding the index of a specific element.
data LABinOp = Index | IndexOf
  deriving LABinOp -> LABinOp -> Bool
(LABinOp -> LABinOp -> Bool)
-> (LABinOp -> LABinOp -> Bool) -> Eq LABinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LABinOp -> LABinOp -> Bool
== :: LABinOp -> LABinOp -> Bool
$c/= :: LABinOp -> LABinOp -> Bool
/= :: LABinOp -> LABinOp -> Bool
Eq

-- | Ordered binary operators (less than, greater than, less than or equal to, greater than or equal to).
data OrdBinOp = Lt | Gt | LEq | GEq
  deriving OrdBinOp -> OrdBinOp -> Bool
(OrdBinOp -> OrdBinOp -> Bool)
-> (OrdBinOp -> OrdBinOp -> Bool) -> Eq OrdBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: OrdBinOp -> OrdBinOp -> Bool
== :: OrdBinOp -> OrdBinOp -> Bool
$c/= :: OrdBinOp -> OrdBinOp -> Bool
/= :: OrdBinOp -> OrdBinOp -> Bool
Eq

-- | @Vector x Vector -> Vector@ binary operations (cross product, addition, subtraction).
data VVVBinOp = Cross | VAdd | VSub
  deriving VVVBinOp -> VVVBinOp -> Bool
(VVVBinOp -> VVVBinOp -> Bool)
-> (VVVBinOp -> VVVBinOp -> Bool) -> Eq VVVBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VVVBinOp -> VVVBinOp -> Bool
== :: VVVBinOp -> VVVBinOp -> Bool
$c/= :: VVVBinOp -> VVVBinOp -> Bool
/= :: VVVBinOp -> VVVBinOp -> Bool
Eq

-- | @Vector x Vector -> Number@ binary operations (dot product).
data VVNBinOp = Dot
  deriving VVNBinOp -> VVNBinOp -> Bool
(VVNBinOp -> VVNBinOp -> Bool)
-> (VVNBinOp -> VVNBinOp -> Bool) -> Eq VVNBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: VVNBinOp -> VVNBinOp -> Bool
== :: VVNBinOp -> VVNBinOp -> Bool
$c/= :: VVNBinOp -> VVNBinOp -> Bool
/= :: VVNBinOp -> VVNBinOp -> Bool
Eq

-- | @Number x Vector -> Vector@ binary operations (scaling).
data NVVBinOp = Scale
  deriving NVVBinOp -> NVVBinOp -> Bool
(NVVBinOp -> NVVBinOp -> Bool)
-> (NVVBinOp -> NVVBinOp -> Bool) -> Eq NVVBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NVVBinOp -> NVVBinOp -> Bool
== :: NVVBinOp -> NVVBinOp -> Bool
$c/= :: NVVBinOp -> NVVBinOp -> Bool
/= :: NVVBinOp -> NVVBinOp -> Bool
Eq

-- | Element + Set -> Set
data ESSBinOp = SAdd | SRemove
  deriving ESSBinOp -> ESSBinOp -> Bool
(ESSBinOp -> ESSBinOp -> Bool)
-> (ESSBinOp -> ESSBinOp -> Bool) -> Eq ESSBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ESSBinOp -> ESSBinOp -> Bool
== :: ESSBinOp -> ESSBinOp -> Bool
$c/= :: ESSBinOp -> ESSBinOp -> Bool
/= :: ESSBinOp -> ESSBinOp -> Bool
Eq

-- | Element + Set -> Bool
data ESBBinOp = SContains
  deriving ESBBinOp -> ESBBinOp -> Bool
(ESBBinOp -> ESBBinOp -> Bool)
-> (ESBBinOp -> ESBBinOp -> Bool) -> Eq ESBBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ESBBinOp -> ESBBinOp -> Bool
== :: ESBBinOp -> ESBBinOp -> Bool
$c/= :: ESBBinOp -> ESBBinOp -> Bool
/= :: ESBBinOp -> ESBBinOp -> Bool
Eq

data AssocConcatOper = SUnion
  deriving AssocConcatOper -> AssocConcatOper -> Bool
(AssocConcatOper -> AssocConcatOper -> Bool)
-> (AssocConcatOper -> AssocConcatOper -> Bool)
-> Eq AssocConcatOper
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssocConcatOper -> AssocConcatOper -> Bool
== :: AssocConcatOper -> AssocConcatOper -> Bool
$c/= :: AssocConcatOper -> AssocConcatOper -> Bool
/= :: AssocConcatOper -> AssocConcatOper -> Bool
Eq

-- | Associative operators (adding and multiplication). Also specifies whether it is for integers or for real numbers.
data AssocArithOper = Add | Mul
  deriving AssocArithOper -> AssocArithOper -> Bool
(AssocArithOper -> AssocArithOper -> Bool)
-> (AssocArithOper -> AssocArithOper -> Bool) -> Eq AssocArithOper
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssocArithOper -> AssocArithOper -> Bool
== :: AssocArithOper -> AssocArithOper -> Bool
$c/= :: AssocArithOper -> AssocArithOper -> Bool
/= :: AssocArithOper -> AssocArithOper -> Bool
Eq

-- | Associative boolean operators (and, or).
data AssocBoolOper = And | Or
  deriving AssocBoolOper -> AssocBoolOper -> Bool
(AssocBoolOper -> AssocBoolOper -> Bool)
-> (AssocBoolOper -> AssocBoolOper -> Bool) -> Eq AssocBoolOper
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AssocBoolOper -> AssocBoolOper -> Bool
== :: AssocBoolOper -> AssocBoolOper -> Bool
$c/= :: AssocBoolOper -> AssocBoolOper -> Bool
/= :: AssocBoolOper -> AssocBoolOper -> Bool
Eq

-- | Unary functions (abs, log, ln, sin, etc.).
data UFunc = Abs | Log | Ln | Sin | Cos | Tan | Sec | Csc | Cot | Arcsin
  | Arccos | Arctan | Exp | Sqrt | Neg | MakeRef
  deriving (UFunc -> UFunc -> Bool
(UFunc -> UFunc -> Bool) -> (UFunc -> UFunc -> Bool) -> Eq UFunc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UFunc -> UFunc -> Bool
== :: UFunc -> UFunc -> Bool
$c/= :: UFunc -> UFunc -> Bool
/= :: UFunc -> UFunc -> Bool
Eq, Int -> UFunc -> ShowS
[UFunc] -> ShowS
UFunc -> TypeError
(Int -> UFunc -> ShowS)
-> (UFunc -> TypeError) -> ([UFunc] -> ShowS) -> Show UFunc
forall a.
(Int -> a -> ShowS) -> (a -> TypeError) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UFunc -> ShowS
showsPrec :: Int -> UFunc -> ShowS
$cshow :: UFunc -> TypeError
show :: UFunc -> TypeError
$cshowList :: [UFunc] -> ShowS
showList :: [UFunc] -> ShowS
Show)

-- | @Bool -> Bool@ operators.
data UFuncB = Not
  deriving UFuncB -> UFuncB -> Bool
(UFuncB -> UFuncB -> Bool)
-> (UFuncB -> UFuncB -> Bool) -> Eq UFuncB
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UFuncB -> UFuncB -> Bool
== :: UFuncB -> UFuncB -> Bool
$c/= :: UFuncB -> UFuncB -> Bool
/= :: UFuncB -> UFuncB -> Bool
Eq

-- | @Vector -> Vector@ operators.
data UFuncVV = NegV
  deriving UFuncVV -> UFuncVV -> Bool
(UFuncVV -> UFuncVV -> Bool)
-> (UFuncVV -> UFuncVV -> Bool) -> Eq UFuncVV
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UFuncVV -> UFuncVV -> Bool
== :: UFuncVV -> UFuncVV -> Bool
$c/= :: UFuncVV -> UFuncVV -> Bool
/= :: UFuncVV -> UFuncVV -> Bool
Eq

-- | @Vector -> Number@ operators.
data UFuncVN = Norm | Dim
  deriving UFuncVN -> UFuncVN -> Bool
(UFuncVN -> UFuncVN -> Bool)
-> (UFuncVN -> UFuncVN -> Bool) -> Eq UFuncVN
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UFuncVN -> UFuncVN -> Bool
== :: UFuncVN -> UFuncVN -> Bool
$c/= :: UFuncVN -> UFuncVN -> Bool
/= :: UFuncVN -> UFuncVN -> Bool
Eq

-- | For case expressions (either complete or incomplete).
data Completeness = Complete | Incomplete
  deriving Completeness -> Completeness -> Bool
(Completeness -> Completeness -> Bool)
-> (Completeness -> Completeness -> Bool) -> Eq Completeness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Completeness -> Completeness -> Bool
== :: Completeness -> Completeness -> Bool
$c/= :: Completeness -> Completeness -> Bool
/= :: Completeness -> Completeness -> Bool
Eq

-- ** Expr

-- | Expression language where all terms are supposed to be 'well understood'
--   (i.e., have a definite meaning). Right now, this coincides with
--   "having a definite value", but should not be restricted to that.
data Expr where
  -- | Brings a literal into the expression language.
  Lit :: Literal -> Expr
  -- | Takes an associative arithmetic operator with a list of expressions.
  AssocA   :: AssocArithOper -> [Expr] -> Expr
  -- | Takes an associative boolean operator with a list of expressions.
  AssocB   :: AssocBoolOper  -> [Expr] -> Expr

  AssocC   :: AssocConcatOper -> [Expr] -> Expr
  -- | C stands for "Chunk", for referring to a chunk in an expression.
  --   Implicitly assumes that the chunk has a symbol.
  C        :: UID -> Expr
  -- | Function applications.
  FCall    :: UID -> [Expr] -> Expr
  -- | For multi-case expressions, each pair represents one case.
  Case     :: Completeness -> [(Expr, Relation)] -> Expr
  -- | Represents a matrix of expressions.
  Matrix   :: [[Expr]] -> Expr
  -- | Represents a set of expressions
  Set      :: Space -> [Expr] -> Expr
  -- | used to refernce the (name + type = variable )
  Variable :: String -> Expr -> Expr
  -- | Unary operation for most functions (eg. sin, cos, log, etc.).
  UnaryOp       :: UFunc -> Expr -> Expr
  -- | Unary operation for @Bool -> Bool@ operations.
  UnaryOpB      :: UFuncB -> Expr -> Expr
  -- | Unary operation for @Vector -> Vector@ operations.
  UnaryOpVV     :: UFuncVV -> Expr -> Expr
  -- | Unary operation for @Vector -> Number@ operations.
  UnaryOpVN     :: UFuncVN -> Expr -> Expr

  -- | Binary operator for arithmetic between expressions (fractional, power, and subtraction).
  ArithBinaryOp :: ArithBinOp -> Expr -> Expr -> Expr
  -- | Binary operator for equality between expressions.
  EqBinaryOp    :: EqBinOp -> Expr -> Expr -> Expr
  -- | Binary operator for indexing two expressions.
  LABinaryOp    :: LABinOp -> Expr -> Expr -> Expr
  -- | Binary operator for ordering expressions (less than, greater than, etc.).
  OrdBinaryOp   :: OrdBinOp -> Expr -> Expr -> Expr
  -- | Binary operator for @Vector x Vector -> Vector@ operations (cross product).
  VVVBinaryOp   :: VVVBinOp -> Expr -> Expr -> Expr
  -- | Binary operator for @Vector x Vector -> Number@ operations (dot product).
  VVNBinaryOp   :: VVNBinOp -> Expr -> Expr -> Expr
  -- | Binary operator for @Expr x Vector -> Vector@ operations (scaling).
  NVVBinaryOp   :: NVVBinOp -> Expr -> Expr -> Expr
  -- | Set operator for Element + Set -> Set
  ESSBinaryOp :: ESSBinOp -> Expr -> Expr -> Expr
  -- | Set operator for Element + Set -> Bool
  ESBBinaryOp :: ESBBinOp -> Expr -> Expr -> Expr
  -- | Operators are generalized arithmetic operators over a 'DomainDesc'
  --   of an 'Expr'.  Could be called BigOp.
  --   ex: Summation is represented via 'Add' over a discrete domain.
  Operator :: AssocArithOper -> DiscreteDomainDesc Expr Expr -> Expr -> Expr
  -- | A different kind of 'IsIn'. A 'UID' is an element of an interval.
  RealI    :: UID -> RealInterval Expr Expr -> Expr

-- | Expressions are equal if their constructors and contents are equal.
instance Eq Expr where
  Lit Literal
a               == :: Expr -> Expr -> Bool
== Lit Literal
b               =   Literal
a Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
b
  AssocA AssocArithOper
o1 [Expr]
l1        == AssocA AssocArithOper
o2 [Expr]
l2        =  AssocArithOper
o1 AssocArithOper -> AssocArithOper -> Bool
forall a. Eq a => a -> a -> Bool
== AssocArithOper
o2 Bool -> Bool -> Bool
&& [Expr]
l1 [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr]
l2
  AssocB AssocBoolOper
o1 [Expr]
l1        == AssocB AssocBoolOper
o2 [Expr]
l2        =  AssocBoolOper
o1 AssocBoolOper -> AssocBoolOper -> Bool
forall a. Eq a => a -> a -> Bool
== AssocBoolOper
o2 Bool -> Bool -> Bool
&& [Expr]
l1 [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr]
l2
  C UID
a                 == C UID
b                 =   UID
a UID -> UID -> Bool
forall a. Eq a => a -> a -> Bool
== UID
b
  FCall UID
a [Expr]
b           == FCall UID
c [Expr]
d           =   UID
a UID -> UID -> Bool
forall a. Eq a => a -> a -> Bool
== UID
c Bool -> Bool -> Bool
&& [Expr]
b [Expr] -> [Expr] -> Bool
forall a. Eq a => a -> a -> Bool
== [Expr]
d
  Case Completeness
a [(Expr, Expr)]
b            == Case Completeness
c [(Expr, Expr)]
d            =   Completeness
a Completeness -> Completeness -> Bool
forall a. Eq a => a -> a -> Bool
== Completeness
c Bool -> Bool -> Bool
&& [(Expr, Expr)]
b [(Expr, Expr)] -> [(Expr, Expr)] -> Bool
forall a. Eq a => a -> a -> Bool
== [(Expr, Expr)]
d
  UnaryOp UFunc
a Expr
b         == UnaryOp UFunc
c Expr
d         =   UFunc
a UFunc -> UFunc -> Bool
forall a. Eq a => a -> a -> Bool
== UFunc
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  UnaryOpB UFuncB
a Expr
b        == UnaryOpB UFuncB
c Expr
d        =   UFuncB
a UFuncB -> UFuncB -> Bool
forall a. Eq a => a -> a -> Bool
== UFuncB
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  UnaryOpVV UFuncVV
a Expr
b       == UnaryOpVV UFuncVV
c Expr
d       =   UFuncVV
a UFuncVV -> UFuncVV -> Bool
forall a. Eq a => a -> a -> Bool
== UFuncVV
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  UnaryOpVN UFuncVN
a Expr
b       == UnaryOpVN UFuncVN
c Expr
d       =   UFuncVN
a UFuncVN -> UFuncVN -> Bool
forall a. Eq a => a -> a -> Bool
== UFuncVN
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  ArithBinaryOp ArithBinOp
o Expr
a Expr
b == ArithBinaryOp ArithBinOp
p Expr
c Expr
d =   ArithBinOp
o ArithBinOp -> ArithBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== ArithBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  EqBinaryOp EqBinOp
o Expr
a Expr
b    == EqBinaryOp EqBinOp
p Expr
c Expr
d    =   EqBinOp
o EqBinOp -> EqBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== EqBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  OrdBinaryOp OrdBinOp
o Expr
a Expr
b   == OrdBinaryOp OrdBinOp
p Expr
c Expr
d   =   OrdBinOp
o OrdBinOp -> OrdBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== OrdBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  LABinaryOp LABinOp
o Expr
a Expr
b    == LABinaryOp LABinOp
p Expr
c Expr
d    =   LABinOp
o LABinOp -> LABinOp -> Bool
forall a. Eq a => a -> a -> Bool
== LABinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  VVVBinaryOp VVVBinOp
o Expr
a Expr
b   == VVVBinaryOp VVVBinOp
p Expr
c Expr
d   =   VVVBinOp
o VVVBinOp -> VVVBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== VVVBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  VVNBinaryOp VVNBinOp
o Expr
a Expr
b   == VVNBinaryOp VVNBinOp
p Expr
c Expr
d   =   VVNBinOp
o VVNBinOp -> VVNBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== VVNBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  NVVBinaryOp NVVBinOp
o Expr
a Expr
b   == NVVBinaryOp NVVBinOp
p Expr
c Expr
d   =   NVVBinOp
o NVVBinOp -> NVVBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== NVVBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  ESSBinaryOp ESSBinOp
o Expr
a Expr
b   == ESSBinaryOp ESSBinOp
p Expr
c Expr
d   =   ESSBinOp
o ESSBinOp -> ESSBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== ESSBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  ESBBinaryOp ESBBinOp
o Expr
a Expr
b   == ESBBinaryOp ESBBinOp
p Expr
c Expr
d   =   ESBBinOp
o ESBBinOp -> ESBBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== ESBBinOp
p Bool -> Bool -> Bool
&& Expr
a Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
== Expr
d
  Expr
_                   == Expr
_                   =   Bool
False
-- ^ TODO: This needs to add more equality checks

-- instance Num Expr where
--   (Int 0)        + b              = b
--   a              + (Int 0)        = a
--   (AssocA Add l) + (AssocA Add m) = AssocA Add (l ++ m)
--   (AssocA Add l) + b              = AssocA Add (l ++ [b])
--   a              + (AssocA Add l) = AssocA Add (a : l)
--   a              + b              = AssocA Add [a, b]

--   (AssocA Mul l) * (AssocA Mul m) = AssocA Mul (l ++ m)
--   (AssocA Mul l) * b              = AssocA Mul (l ++ [b])
--   a              * (AssocA Mul l) = AssocA Mul (a : l)
--   a              * b              = AssocA Mul [a, b]

--   a - b = ArithBinaryOp Subt a b

--   fromInteger = Int
--   abs         = UnaryOp Abs
--   negate      = UnaryOp Neg

--   -- this is a Num wart
--   signum _ = error "should not use signum in expressions"

-- instance Fractional Expr where
--   a / b = ArithBinaryOp Frac a b
--   fromRational r = ArithBinaryOp Frac (fromInteger $ numerator   r)
--                                       (fromInteger $ denominator r)

-- Helper class for pretty-printing errors (should move from here)
-- We don't want to (ab)use Show for this
class Pretty p where
  pretty :: p -> String

instance Pretty VVVBinOp where
  pretty :: VVVBinOp -> TypeError
pretty VVVBinOp
Cross = TypeError
"cross product"
  pretty VVVBinOp
VAdd  = TypeError
"vector addition"
  pretty VVVBinOp
VSub  = TypeError
"vector subtraction"

instance LiteralC Expr where
  int :: Integer -> Expr
int = Literal -> Expr
Lit (Literal -> Expr) -> (Integer -> Literal) -> Integer -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
forall r. LiteralC r => Integer -> r
int
  str :: TypeError -> Expr
str = Literal -> Expr
Lit (Literal -> Expr) -> (TypeError -> Literal) -> TypeError -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeError -> Literal
forall r. LiteralC r => TypeError -> r
str
  dbl :: Double -> Expr
dbl = Literal -> Expr
Lit (Literal -> Expr) -> (Double -> Literal) -> Double -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Literal
forall r. LiteralC r => Double -> r
dbl
  exactDbl :: Integer -> Expr
exactDbl = Literal -> Expr
Lit (Literal -> Expr) -> (Integer -> Literal) -> Integer -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Literal
forall r. LiteralC r => Integer -> r
exactDbl
  perc :: Integer -> Integer -> Expr
perc Integer
l Integer
r = Literal -> Expr
Lit (Literal -> Expr) -> Literal -> Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Integer -> Literal
forall r. LiteralC r => Integer -> Integer -> r
perc Integer
l Integer
r

-- helper function for typechecking to help reduce duplication
vvvInfer :: TypingContext Space -> VVVBinOp -> Expr -> Expr -> Either TypeError Space
vvvInfer :: TypingContext Space
-> VVVBinOp -> Expr -> Expr -> Either TypeError Space
vvvInfer TypingContext Space
ctx VVVBinOp
op Expr
l Expr
r = do
  lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
ctx Expr
l
  rt <- infer ctx r

  let msg TypeError
dir TypeError
sp = TypeError
"Vector operation " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ VVVBinOp -> TypeError
forall p. Pretty p => p -> TypeError
pretty VVVBinOp
op TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
" expects numeric vectors, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` on the " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
dir TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"-hand side."

  lsp <- assertNumericVector lt $ msg "left"
  rsp <- assertNumericVector rt $ msg "right"

  if op == VSub then
    assertNonNatNumeric lsp $ \TypeError
sp ->
      TypeError
"Vector subtraction expects both operands to be vectors of non-natural numbers. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
  else Right ()

  lsp ~== rsp $ \TypeError
lt' TypeError
rt' -> TypeError
"Vector " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ VVVBinOp -> TypeError
forall p. Pretty p => p -> TypeError
pretty VVVBinOp
op TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
" expects both operands to be of the same numeric type. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
lt' TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` and `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rt' TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."

  pure lt

instance Typed Expr Space where
  check :: TypingContext Space -> Expr -> Space -> Either TypeError Space
  check :: TypingContext Space -> Expr -> Space -> Either TypeError Space
check = TypingContext Space -> Expr -> Space -> Either TypeError Space
forall e t.
Typed e t =>
TypingContext t -> e -> t -> Either TypeError t
typeCheckByInfer

  infer :: TypingContext Space -> Expr -> Either TypeError Space
  infer :: TypingContext Space -> Expr -> Either TypeError Space
infer TypingContext Space
cxt (Lit Literal
lit) = TypingContext Space -> Literal -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Literal
lit

  infer TypingContext Space
cxt (AssocA AssocArithOper
_ (Expr
e:[Expr]
exs)) = do
    et <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e
    assertNumeric et $
      \TypeError
sp -> TypeError
"Associative arithmetic operation expects numeric operands, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
    assertAllEq cxt exs et
        "Associative arithmetic operation expects all operands to be of the same type."
    pure et
  infer TypingContext Space
_ (AssocA AssocArithOper
Add [Expr]
_) = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Associative addition requires at least one operand."
  infer TypingContext Space
_ (AssocA AssocArithOper
Mul [Expr]
_) = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Associative multiplication requires at least one operand."

  infer TypingContext Space
cxt (AssocB AssocBoolOper
_ [Expr]
exs) = do
    TypingContext Space
-> [Expr] -> Space -> TypeError -> Either TypeError ()
forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> TypeError -> Either TypeError ()
assertAllEq TypingContext Space
cxt [Expr]
exs Space
S.Boolean (TypeError -> Either TypeError ())
-> TypeError -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ TypeError
"Associative boolean operation expects all operands to be of the same type (" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
S.Boolean TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
")."
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
S.Boolean

  infer TypingContext Space
cxt (AssocC AssocConcatOper
_ (Expr
e:[Expr]
exs)) =
    case TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e of
      Right Space
spaceValue | Space
spaceValue Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
S.Void -> do
          TypingContext Space
-> [Expr] -> Space -> TypeError -> Either TypeError ()
forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> TypeError -> Either TypeError ()
assertAllEq TypingContext Space
cxt [Expr]
exs Space
spaceValue
              TypeError
"Associative arithmetic operation expects all operands to be of the same type."
          Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
spaceValue
      Right Space
r ->
          -- Handle the case when sp is a Left value but spaceValue is invalid
          TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left (TypeError
"Expected all operands in addition/multiplication to be numeric, but found " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
r)
      Left TypeError
l ->
          -- If sp is a Right value containing a TypeError
          TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
l

  infer TypingContext Space
_ (AssocC AssocConcatOper
SUnion [Expr]
_) = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Associative addition requires at least one operand."

  infer TypingContext Space
cxt (C UID
uid) = TypingContext Space -> UID -> Either TypeError Space
forall t. TypingContext t -> UID -> Either TypeError t
inferFromContext TypingContext Space
cxt UID
uid

  infer TypingContext Space
cxt (Variable TypeError
_ Expr
n) = TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
n

  infer TypingContext Space
cxt (FCall UID
uid [Expr]
exs) = do
    ft <- TypingContext Space -> UID -> Either TypeError Space
forall t. TypingContext t -> UID -> Either TypeError t
inferFromContext TypingContext Space
cxt UID
uid
    (params, out) <- assertFunction ft $ \TypeError
t -> TypeError
"Function application on non-function `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ UID -> TypeError
forall a. Show a => a -> TypeError
show UID
uid TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` (" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
t TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
")."
    let exst = (Expr -> Either TypeError Space)
-> [Expr] -> [Either TypeError Space]
forall a b. (a -> b) -> [a] -> [b]
map (TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt) [Expr]
exs
    if NE.toList params == rights exst
      then pure out
      else Left $ "Function `" ++ show uid ++ "` expects parameters of types: " ++ show params ++ ", but received: " ++ show (rights exst) ++ "."

  infer   TypingContext Space
_ (Case Completeness
_ []) = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Case contains no expressions, no type to infer."
  infer TypingContext Space
cxt (Case Completeness
_ [(Expr, Expr)]
ers) = do
    let inferPair :: (Expr, Expr) -> Either TypeError (Space, Space)
inferPair (Expr
e, Expr
r) = (,) (Space -> Space -> (Space, Space))
-> Either TypeError Space
-> Either TypeError (Space -> (Space, Space))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e Either TypeError (Space -> (Space, Space))
-> Either TypeError Space -> Either TypeError (Space, Space)
forall a b.
Either TypeError (a -> b)
-> Either TypeError a -> Either TypeError b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    ers' <- ((Expr, Expr) -> Either TypeError (Space, Space))
-> [(Expr, Expr)] -> Either TypeError [(Space, Space)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Expr, Expr) -> Either TypeError (Space, Space)
inferPair [(Expr, Expr)]
ers -- fail and return immediately on first Left
    let (ets, rts) = unzip ers'
        rt = [Space] -> [Space]
forall a. Eq a => [a] -> [a]
nub [Space]
rts
        et = [Space] -> [Space]
forall a. Eq a => [a] -> [a]
nub [Space]
ets

    if rt /= [S.Boolean] then
      Left $ "Case contains expressions of different types: " ++ show rt
    else if length et /= 1 then
      Left $ "Case contains expressions of different types: " ++ show et
    else
      pure $ head et

  infer TypingContext Space
cxt (Matrix [[Expr]]
exss)
    | [[Expr]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Expr]]
exss = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Matrix has no rows."
    | [Expr] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Expr] -> Bool) -> [Expr] -> Bool
forall a b. (a -> b) -> a -> b
$ [[Expr]] -> [Expr]
forall a. HasCallStack => [a] -> a
head [[Expr]]
exss = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Matrix has no columns."
    | Bool
allRowsHaveSameColumnsAndSpace = Space -> Either TypeError Space
forall a b. b -> Either a b
Right (Space -> Either TypeError Space)
-> Space -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Space -> Space
S.Matrix Int
rows Int
columns Space
t
    | Bool
otherwise = TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left TypeError
"Not all rows have the same number of columns or the same value types."
    where
        rows :: Int
rows = [[Expr]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Expr]]
exss
        columns :: Int
columns = if Int
rows Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 then [Expr] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr] -> Int) -> [Expr] -> Int
forall a b. (a -> b) -> a -> b
$ [[Expr]] -> [Expr]
forall a. HasCallStack => [a] -> a
head [[Expr]]
exss else Int
0
        sss :: [[Either TypeError Space]]
sss = ([Expr] -> [Either TypeError Space])
-> [[Expr]] -> [[Either TypeError Space]]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Either TypeError Space)
-> [Expr] -> [Either TypeError Space]
forall a b. (a -> b) -> [a] -> [b]
map (TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt)) [[Expr]]
exss
        expT :: Either TypeError Space
expT = [Either TypeError Space] -> Either TypeError Space
forall a. HasCallStack => [a] -> a
head ([Either TypeError Space] -> Either TypeError Space)
-> [Either TypeError Space] -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ [[Either TypeError Space]] -> [Either TypeError Space]
forall a. HasCallStack => [a] -> a
head [[Either TypeError Space]]
sss
        allRowsHaveSameColumnsAndSpace :: Bool
allRowsHaveSameColumnsAndSpace
          = (TypeError -> Bool)
-> (Space -> Bool) -> Either TypeError Space -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (\TypeError
_ -> ([Either TypeError Space] -> Bool)
-> [[Either TypeError Space]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ [Either TypeError Space]
r -> [Either TypeError Space] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either TypeError Space]
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
columns Bool -> Bool -> Bool
&& (Either TypeError Space -> Bool)
-> [Either TypeError Space] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Either TypeError Space -> Either TypeError Space -> Bool
forall a. Eq a => a -> a -> Bool
== Either TypeError Space
expT) [Either TypeError Space]
r) [[Either TypeError Space]]
sss)
              (Bool -> Space -> Bool
forall a b. a -> b -> a
const Bool
False) Either TypeError Space
expT
        t :: Space
t = Space -> Either TypeError Space -> Space
forall b a. b -> Either a b -> b
fromRight (TypeError -> Space
forall a. HasCallStack => TypeError -> a
error TypeError
"Infer on Matrix had a strong expectation of Right-valued data.") Either TypeError Space
expT -- This error should never occur.

  infer TypingContext Space
cxt (Set Space
s [Expr]
es) = do
    ets <- (Expr -> Either TypeError Space)
-> [Expr] -> Either TypeError [Space]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt) [Expr]
es
    if all (== s) ets
      then pure s
      else Left $ "Set contains expressions of unexpected type: `" ++ show (filter (/= s) ets) ++ "`. Expected type: `" ++ show s ++ "`."

  infer TypingContext Space
cxt (UnaryOp UFunc
uf Expr
e) = do
    et <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e
    case uf of
      UFunc
Abs -> do
        Space -> ShowS -> Either TypeError ()
assertNonNatNumeric Space
et (\TypeError
sp -> TypeError
"'Absolute value' operator only applies to non-natural numeric types. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
        Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
et
      UFunc
Neg -> do
        Space -> ShowS -> Either TypeError ()
assertNonNatNumeric Space
et (\TypeError
sp -> TypeError
"'Negation' operator only applies to non-natural numeric types. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
        Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
et
      UFunc
Exp -> do
        if Space
et Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Real Bool -> Bool -> Bool
|| Space
et Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Integer
          then Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
S.Real
          else TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left (TypeError -> Either TypeError Space)
-> TypeError -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ TypeError
"'Exponentiation' operator only applies to reals and integers. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
et TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
      UFunc
x -> do
        if Space
et Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Real
          then Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
S.Real
          else TypeError -> Either TypeError Space
forall a b. a -> Either a b
Left (TypeError -> Either TypeError Space)
-> TypeError -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ UFunc -> TypeError
forall a. Show a => a -> TypeError
show UFunc
x TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
" operator only applies to Reals. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
et TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."

  infer TypingContext Space
cxt (UnaryOpB UFuncB
Not Expr
e) = do
    et <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e
    assertBoolean et (\TypeError
sp -> TypeError
"¬ on non-boolean operand of type: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
".")
    pure S.Boolean

  infer TypingContext Space
cxt (UnaryOpVV UFuncVV
NegV Expr
e) = do
    et <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e
    vet <- assertNonNatNumVector (\TypeError
sp -> TypeError
"Vector negation only applies to non-natural numeric vectors. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.") et
    pure $ S.Vect vet

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Norm Expr
e) = do
    et <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e
    assertRealVector et (\TypeError
sp -> TypeError
"Vector norm only applies to vectors of real numbers. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure S.Real

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Dim Expr
e) = do
    et <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
e
    _ <- assertVector et (\TypeError
sp -> TypeError
"Vector dimension only applies to vectors. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure S.Integer

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Frac Expr
n Expr
d) = do
    nt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
n
    dt <- infer cxt d
    assertEquivNumeric nt dt
      (\TypeError
lt TypeError
rt -> TypeError
"Fractions/divisions should only be applied to the same numeric typed operands. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
lt TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` / `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rt TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure nt

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Pow Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    if S.isBasicNumSpace lt && (lt == rt || (lt == S.Real && rt == S.Integer))
      then Right lt
      else Left $
        "Powers should only be applied to the same numeric type in both operands, or real base with integer exponent. Received `" ++ show lt ++ "` ^ `" ++ show rt ++ "`."

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Subt Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    assertEquivNumeric
      lt rt
      (\TypeError
ls TypeError
rs -> TypeError
"Subtraction should only be applied to the same numeric typed operands. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` - `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure lt

  infer TypingContext Space
cxt (EqBinaryOp EqBinOp
_ Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    lt ~== rt $ \TypeError
lsp TypeError
rsp -> TypeError
"Both operands of an (in)equality (=/≠) must be of the same type. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
lsp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` & `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rsp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
    pure S.Boolean

  infer TypingContext Space
cxt (LABinaryOp LABinOp
Index Expr
l Expr
n) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    vet <- assertVector lt (\TypeError
sp -> TypeError
"List accessor expects a vector, but received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")

    nt <- infer cxt n
    assertIndexLike nt
      (\TypeError
sp -> TypeError
"List accessor expects an index-like type (Integer or Natural), but received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")

    pure vet

  infer TypingContext Space
cxt (LABinaryOp LABinOp
IndexOf Expr
l Expr
e) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    vet <- assertVector lt (\TypeError
sp -> TypeError
"List index-of expects a vector, but received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")

    et <- infer cxt e
    vet ~== et
      $ \TypeError
ls TypeError
rs -> TypeError
"List index-of expects an element of the same type as the vector, but received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` and `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."

    pure S.Integer -- TODO: This can also be `S.Natural`, but we don't express that in the type system yet.

  infer TypingContext Space
cxt (OrdBinaryOp OrdBinOp
_ Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    let msg TypeError
ls TypeError
rs = TypeError
"Ordering expression contains non-numeric operand. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` & `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
    assertEquivNumeric lt rt msg
    pure S.Boolean

  infer TypingContext Space
cxt (NVVBinaryOp NVVBinOp
Scale Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    vet <- assertNumericVector rt
      (\TypeError
sp -> TypeError
"Vector scaling expects a numeric vector on the right-hand side, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    assertEquivNumeric lt vet
      (\TypeError
ls TypeError
rs -> TypeError
"Vector scaling expects scalar and vector of scalars of the same type, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` over vector of `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`s.")
    pure rt

  infer TypingContext Space
cxt (VVVBinaryOp VVVBinOp
o Expr
l Expr
r) = TypingContext Space
-> VVVBinOp -> Expr -> Expr -> Either TypeError Space
vvvInfer TypingContext Space
cxt VVVBinOp
o Expr
l Expr
r

  infer TypingContext Space
cxt (VVNBinaryOp VVNBinOp
Dot Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    let msg TypeError
hand TypeError
sp = TypeError
"Vector dot product expects a numeric vector on the " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
hand TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"-hand side, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
    lvet <- assertNumericVector lt (msg "left")
    rvet <- assertNumericVector rt (msg "right")
    assertEquivNumeric lvet rvet
      (\TypeError
ls TypeError
rs -> TypeError
"Vector dot product expects vectors of the same numeric type, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` and `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure lvet

  infer TypingContext Space
cxt (ESSBinaryOp ESSBinOp
_ Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    set <- assertSet rt
      (\TypeError
sp -> TypeError
"Set add/subtract expects a set on the right-hand side, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    assertEquivNumeric lt set
      (\TypeError
ls TypeError
rs -> TypeError
"Set add/subtract expects numeric set operands. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` / `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure rt

  infer TypingContext Space
cxt (ESBBinaryOp ESBBinOp
SContains Expr
l Expr
r) = do
    lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
l
    rt <- infer cxt r
    set <- assertSet rt
      (\TypeError
sp -> TypeError
"Set contains expects a set on the right-hand side, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    assertEquivNumeric lt set
      (\TypeError
ls TypeError
rs -> TypeError
"Set contains should only be applied to Set of numeric type. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` / `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")
    pure S.Boolean

  infer TypingContext Space
cxt (Operator AssocArithOper
_ (S.BoundedDD Symbol
_ RTopology
_ Expr
bot Expr
top) Expr
body) = do
    botTy <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
bot
    topTy <- infer cxt top
    bodyTy <- infer cxt body

    assertNumeric bodyTy
      (\TypeError
sp -> TypeError
"'Big' operator body is not numeric, found: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
".")

    let msg TypeError
dir TypeError
sp = TypeError
"'Big' operator range " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
dir TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
" is not an index-like type (Integer or Natural), found: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"."

    assertIndexLike botTy (msg "start")
    assertIndexLike topTy (msg "stop")

    assertEquivNumeric botTy topTy
      (\TypeError
ls TypeError
rs -> TypeError
"'Big' operator range expects start and stop to be of the same numeric type, but found `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
ls TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` and `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
rs TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`.")

    -- FIXME: We have a `Symbol` in the `S.BoundedDD` but it's not used in type-checking.
    pure bodyTy

  infer TypingContext Space
cxt (RealI UID
uid RealInterval Expr Expr
ri) = do
    uidT <- TypingContext Space -> UID -> Either TypeError Space
forall t. TypingContext t -> UID -> Either TypeError t
inferFromContext TypingContext Space
cxt UID
uid
    riT <- riTy ri
    assertReal uidT $
      \TypeError
sp -> TypeError
"Real interval expects variable to be of type Real, but received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ UID -> TypeError
forall a. Show a => a -> TypeError
show UID
uid TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` of type `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
    assertReal riT $
      \TypeError
sp -> TypeError
"Real interval expects interval bounds to be of type Real, but received: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"."
    pure S.Boolean
    where
      riTy :: RealInterval Expr Expr -> Either TypeError Space
      riTy :: RealInterval Expr Expr -> Either TypeError Space
riTy (S.Bounded (Inclusive
_, Expr
lx) (Inclusive
_, Expr
rx)) = do
        lt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
lx
        rt <- infer cxt rx
        let msg TypeError
dir TypeError
sp = TypeError
"Bounded real interval " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
dir TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
" is not a real number, found: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
sp TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"."
        assertReal lt (msg "lower bound")
        assertReal rt (msg "upper bound")
        pure S.Real
      riTy (S.UpTo (Inclusive
_, Expr
x)) = TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
x
      riTy (S.UpFrom (Inclusive
_, Expr
x)) = TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
x