{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE InstanceSigs          #-}
{-# LANGUAGE MultiParamTypeClasses #-}

-- | The Drasil Expression language
module Language.Drasil.Expr.Lang where

import Drasil.Database.UID (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

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

-- * Expression Types

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

-- | The variable type is just a renamed 'String'.
type Variable = String

-- 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

-- | Conditional and Biconditional operators (Expressions can imply
-- one another, or exist if and only if another expression exists).
data BoolBinOp = Impl | Iff
  deriving BoolBinOp -> BoolBinOp -> Bool
(BoolBinOp -> BoolBinOp -> Bool)
-> (BoolBinOp -> BoolBinOp -> Bool) -> Eq BoolBinOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BoolBinOp -> BoolBinOp -> Bool
== :: BoolBinOp -> BoolBinOp -> Bool
$c/= :: BoolBinOp -> BoolBinOp -> Bool
/= :: BoolBinOp -> BoolBinOp -> 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
  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 boolean operators (implies, iff).
  BoolBinaryOp  :: BoolBinOp -> 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
  BoolBinaryOp BoolBinOp
o Expr
a Expr
b  == BoolBinaryOp BoolBinOp
p Expr
c Expr
d  =   BoolBinOp
o BoolBinOp -> BoolBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== BoolBinOp
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
  Space
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
  Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
ctx Expr
r

  let msg :: TypeError -> ShowS
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."

  Space
lsp <- Space -> ShowS -> Either TypeError Space
assertNumericVector Space
lt (ShowS -> Either TypeError Space)
-> ShowS -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ TypeError -> ShowS
msg TypeError
"left"
  Space
rsp <- Space -> ShowS -> Either TypeError Space
assertNumericVector Space
rt (ShowS -> Either TypeError Space)
-> ShowS -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ TypeError -> ShowS
msg TypeError
"right"

  if VVVBinOp
op VVVBinOp -> VVVBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== VVVBinOp
VSub then
    Space -> ShowS -> Either TypeError ()
assertNonNatNumeric Space
lsp (ShowS -> Either TypeError ()) -> ShowS -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ \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 () -> Either TypeError ()
forall a b. b -> Either a b
Right ()

  Space
lsp Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
forall t.
(Show t, Eq t) =>
t -> t -> (TypeError -> ShowS) -> Either TypeError ()
~== Space
rsp ((TypeError -> ShowS) -> Either TypeError ())
-> (TypeError -> ShowS) -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ \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
"`."

  Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
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
    Space
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
    Space -> ShowS -> Either TypeError ()
assertNumeric Space
et (ShowS -> Either TypeError ()) -> ShowS -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
      \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
"`."
    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
et
        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
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
    Space
ft <- TypingContext Space -> UID -> Either TypeError Space
forall t. TypingContext t -> UID -> Either TypeError t
inferFromContext TypingContext Space
cxt UID
uid
    (NonEmpty Space
params, Space
out) <- Space -> ShowS -> Either TypeError (NonEmpty Space, Space)
assertFunction Space
ft (ShowS -> Either TypeError (NonEmpty Space, Space))
-> ShowS -> Either TypeError (NonEmpty Space, Space)
forall a b. (a -> b) -> a -> b
$ \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 :: [Either TypeError Space]
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 NonEmpty Space -> [Space]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
NE.toList NonEmpty Space
params [Space] -> [Space] -> Bool
forall a. Eq a => a -> a -> Bool
== [Either TypeError Space] -> [Space]
forall a b. [Either a b] -> [b]
rights [Either TypeError Space]
exst
      then Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
out
      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
"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
"` expects parameters of types: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ NonEmpty Space -> TypeError
forall a. Show a => a -> TypeError
show NonEmpty Space
params TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
", but received: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ [Space] -> TypeError
forall a. Show a => a -> TypeError
show ([Either TypeError Space] -> [Space]
forall a b. [Either a b] -> [b]
rights [Either TypeError Space]
exst) TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"."

  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
    [(Space, Space)]
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 ([Space]
ets, [Space]
rts) = [(Space, Space)] -> ([Space], [Space])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Space, Space)]
ers'
        rt :: [Space]
rt = [Space] -> [Space]
forall a. Eq a => [a] -> [a]
nub [Space]
rts
        et :: [Space]
et = [Space] -> [Space]
forall a. Eq a => [a] -> [a]
nub [Space]
ets

    if [Space]
rt [Space] -> [Space] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Space
S.Boolean] then
      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
"Case contains expressions of different types: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ [Space] -> TypeError
forall a. Show a => a -> TypeError
show [Space]
rt
    else if [Space] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Space]
et Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1 then
      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
"Case contains expressions of different types: " TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ [Space] -> TypeError
forall a. Show a => a -> TypeError
show [Space]
et
    else
      Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Space -> Either TypeError Space)
-> Space -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ [Space] -> Space
forall a. HasCallStack => [a] -> a
head [Space]
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
    [Space]
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 (Space -> Bool) -> [Space] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
s) [Space]
ets
      then Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
s
      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
"Set contains expressions of unexpected type: `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ [Space] -> TypeError
forall a. Show a => a -> TypeError
show ((Space -> Bool) -> [Space] -> [Space]
forall a. (a -> Bool) -> [a] -> [a]
filter (Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
s) [Space]
ets) TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`. Expected type: `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
s TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."

  infer TypingContext Space
cxt (UnaryOp UFunc
uf Expr
e) = do
    Space
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 UFunc
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
    Space
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
    Space -> ShowS -> Either TypeError ()
assertBoolean Space
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
".")
    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 (UnaryOpVV UFuncVV
NegV Expr
e) = do
    Space
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
    Space
vet <- ShowS -> Space -> Either TypeError Space
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
"`.") Space
et
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Space -> Either TypeError Space)
-> Space -> Either TypeError Space
forall a b. (a -> b) -> a -> b
$ Space -> Space
S.Vect Space
vet

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Norm Expr
e) = do
    Space
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
    Space -> ShowS -> Either TypeError ()
assertRealVector Space
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
"`.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
et

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Dim Expr
e) = do
    Space
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
    Space
_ <- Space -> ShowS -> Either TypeError Space
assertVector Space
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
"`.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
S.Integer

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Frac Expr
n Expr
d) = do
    Space
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
    Space
dt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
d
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
nt Space
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
"`.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
nt

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

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Subt Expr
l Expr
r) = do
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric
      Space
lt Space
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
"`.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
lt

  infer TypingContext Space
cxt (BoolBinaryOp BoolBinOp
_ Expr
l Expr
r) = do
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    let msg :: ShowS
msg = TypeError -> ShowS
forall a b. a -> b -> a
const (TypeError -> ShowS) -> TypeError -> ShowS
forall a b. (a -> b) -> a -> b
$ TypeError
"Boolean expression contains non-boolean operand. Received `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
lt TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"` & `" TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> TypeError
forall a. Show a => a -> TypeError
show Space
rt TypeError -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeError
"`."
    Space -> ShowS -> Either TypeError ()
assertBoolean Space
lt ShowS
msg
    Space -> ShowS -> Either TypeError ()
assertBoolean Space
rt ShowS
msg
    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 (EqBinaryOp EqBinOp
_ Expr
l Expr
r) = do
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    Space
lt Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
forall t.
(Show t, Eq t) =>
t -> t -> (TypeError -> ShowS) -> Either TypeError ()
~== Space
rt ((TypeError -> ShowS) -> Either TypeError ())
-> (TypeError -> ShowS) -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ \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
"`."
    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 (LABinaryOp LABinOp
Index Expr
l Expr
n) = do
    Space
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
    Space
vet <- Space -> ShowS -> Either TypeError Space
assertVector Space
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
"`.")

    Space
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
    Space -> ShowS -> Either TypeError ()
assertIndexLike Space
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
"`.")

    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
vet

  infer TypingContext Space
cxt (LABinaryOp LABinOp
IndexOf Expr
l Expr
e) = do
    Space
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
    Space
vet <- Space -> ShowS -> Either TypeError Space
assertVector Space
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
"`.")

    Space
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
    Space
vet Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
forall t.
(Show t, Eq t) =>
t -> t -> (TypeError -> ShowS) -> Either TypeError ()
~== Space
et
      ((TypeError -> ShowS) -> Either TypeError ())
-> (TypeError -> ShowS) -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ \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
"`."

    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
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
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    let msg :: TypeError -> ShowS
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
"`."
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
lt Space
rt TypeError -> ShowS
msg
    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 (NVVBinaryOp NVVBinOp
Scale Expr
l Expr
r) = do
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    Space
vet <- Space -> ShowS -> Either TypeError Space
assertNumericVector Space
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
"`.")
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
lt Space
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.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
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
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    let msg :: TypeError -> ShowS
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
"`."
    Space
lvet <- Space -> ShowS -> Either TypeError Space
assertNumericVector Space
lt (TypeError -> ShowS
msg TypeError
"left")
    Space
rvet <- Space -> ShowS -> Either TypeError Space
assertNumericVector Space
rt (TypeError -> ShowS
msg TypeError
"right")
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
lvet Space
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
"`.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
lvet

  infer TypingContext Space
cxt (ESSBinaryOp ESSBinOp
_ Expr
l Expr
r) = do
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    Space
set <- Space -> ShowS -> Either TypeError Space
assertSet Space
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
"`.")
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
lt Space
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
"`.")
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
rt

  infer TypingContext Space
cxt (ESBBinaryOp ESBBinOp
SContains Expr
l Expr
r) = do
    Space
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
    Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
r
    Space
set <- Space -> ShowS -> Either TypeError Space
assertSet Space
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
"`.")
    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
lt Space
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
"`.")
    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 (Operator AssocArithOper
_ (S.BoundedDD Symbol
_ RTopology
_ Expr
bot Expr
top) Expr
body) = do
    Space
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
    Space
topTy <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
top
    Space
bodyTy <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
body

    Space -> ShowS -> Either TypeError ()
assertNumeric Space
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 -> ShowS
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
"."

    Space -> ShowS -> Either TypeError ()
assertIndexLike Space
botTy (TypeError -> ShowS
msg TypeError
"start")
    Space -> ShowS -> Either TypeError ()
assertIndexLike Space
topTy (TypeError -> ShowS
msg TypeError
"stop")

    Space -> Space -> (TypeError -> ShowS) -> Either TypeError ()
assertEquivNumeric Space
botTy Space
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.
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
bodyTy

  infer TypingContext Space
cxt (RealI UID
uid RealInterval Expr Expr
ri) = do
    Space
uidT <- TypingContext Space -> UID -> Either TypeError Space
forall t. TypingContext t -> UID -> Either TypeError t
inferFromContext TypingContext Space
cxt UID
uid
    Space
riT <- RealInterval Expr Expr -> Either TypeError Space
riTy RealInterval Expr Expr
ri
    Space -> ShowS -> Either TypeError ()
assertReal Space
uidT (ShowS -> Either TypeError ()) -> ShowS -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
      \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
"`."
    Space -> ShowS -> Either TypeError ()
assertReal Space
riT (ShowS -> Either TypeError ()) -> ShowS -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$
      \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
"."
    Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
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
        Space
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
        Space
rt <- TypingContext Space -> Expr -> Either TypeError Space
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext Space
cxt Expr
rx
        let msg :: TypeError -> ShowS
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
"."
        Space -> ShowS -> Either TypeError ()
assertReal Space
lt (TypeError -> ShowS
msg TypeError
"lower bound")
        Space -> ShowS -> Either TypeError ()
assertReal Space
rt (TypeError -> ShowS
msg TypeError
"upper bound")
        Space -> Either TypeError Space
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Space
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