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

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

import           Language.Drasil.Literal.Class (LiteralC (..))
import           Language.Drasil.Literal.Lang  (Literal (..))
import           Language.Drasil.Space         (DiscreteDomainDesc,
                                                RealInterval, Space)
import qualified Language.Drasil.Space         as S
import           Language.Drasil.UID           (UID)
import           Language.Drasil.WellTyped
import Data.Either (lefts, fromLeft)
import qualified Data.Foldable as NE

-- * 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.
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 -> String
(Int -> UFunc -> ShowS)
-> (UFunc -> String) -> ([UFunc] -> ShowS) -> Show UFunc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UFunc -> ShowS
showsPrec :: Int -> UFunc -> ShowS
$cshow :: UFunc -> String
show :: UFunc -> String
$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 -> String
pretty VVVBinOp
Cross = String
"cross product"
  pretty VVVBinOp
VAdd  = String
"vector addition"
  pretty VVVBinOp
VSub  = String
"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 :: String -> Expr
str = Literal -> Expr
Lit (Literal -> Expr) -> (String -> Literal) -> String -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Literal
forall r. LiteralC r => String -> 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 Space TypeError
vvvInfer :: TypingContext Space
-> VVVBinOp -> Expr -> Expr -> Either Space String
vvvInfer TypingContext Space
ctx VVVBinOp
op Expr
l Expr
r = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
ctx Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
ctx Expr
r) of
    (Left lt :: Space
lt@(S.Vect Space
lsp), Left (S.Vect Space
rsp)) ->
      if Space
lsp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rsp Bool -> Bool -> Bool
&& Space -> Bool
S.isBasicNumSpace Space
lsp then
        if VVVBinOp
op VVVBinOp -> VVVBinOp -> Bool
forall a. Eq a => a -> a -> Bool
== VVVBinOp
VSub Bool -> Bool -> Bool
&& (Space
lsp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Natural Bool -> Bool -> Bool
|| Space
rsp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Natural) then
          String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector subtraction expects both operands to be vectors of non-natural numbers. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` and `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
        else Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VVVBinOp -> String
forall p. Pretty p => p -> String
pretty VVVBinOp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" expects both operands to be vectors of non-natural numbers. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` and `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Left Space
lsp, Left Space
rsp) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector operation " String -> ShowS
forall a. [a] -> [a] -> [a]
++ VVVBinOp -> String
forall p. Pretty p => p -> String
pretty VVVBinOp
op String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" expects vector operands. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` and `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_       , Right String
re) -> String -> Either Space String
forall a b. b -> Either a b
Right String
re
    (Right String
le, Either Space String
_       ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
le


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

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

  infer TypingContext Space
cxt (AssocA AssocArithOper
_ (Expr
e:[Expr]
exs)) = 
    case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
e of
      Left Space
spaceValue | Space -> Bool
S.isBasicNumSpace Space
spaceValue -> 
          -- If the inferred type of e is a valid Space, call allOfType with spaceValue
          TypingContext Space
-> [Expr] -> Space -> Space -> String -> Either Space String
forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> t -> String -> Either t String
allOfType TypingContext Space
cxt [Expr]
exs Space
spaceValue Space
spaceValue 
              String
"Associative arithmetic operation expects all operands to be of the same expected type."
      Left Space
l ->
          -- Handle the case when sp is a Left value but spaceValue is invalid
          String -> Either Space String
forall a b. b -> Either a b
Right (String
"Expected all operands in addition/multiplication to be numeric, but found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
l)
      Right String
r ->
          -- If sp is a Right value containing a TypeError
          String -> Either Space String
forall a b. b -> Either a b
Right String
r
  infer TypingContext Space
_ (AssocA AssocArithOper
Add [Expr]
_) = String -> Either Space String
forall a b. b -> Either a b
Right String
"Associative addition requires at least one operand."
  infer TypingContext Space
_ (AssocA AssocArithOper
Mul [Expr]
_) = String -> Either Space String
forall a b. b -> Either a b
Right String
"Associative multiplication requires at least one operand."

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

  infer TypingContext Space
cxt (AssocC AssocConcatOper
_ (Expr
e:[Expr]
exs)) = 
    case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
e of
      Left Space
spaceValue | Space
spaceValue Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
S.Void -> 
          -- If the inferred type of e is a valid Space, call allOfType with spaceValue
          TypingContext Space
-> [Expr] -> Space -> Space -> String -> Either Space String
forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> t -> String -> Either t String
allOfType TypingContext Space
cxt [Expr]
exs Space
spaceValue Space
spaceValue 
              String
"Associative arithmetic operation expects all operands to be of the same expected type."
      Left Space
l ->
          -- Handle the case when sp is a Left value but spaceValue is invalid
          String -> Either Space String
forall a b. b -> Either a b
Right (String
"Expected all operands in addition/multiplication to be numeric, but found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
l)
      Right String
r ->
          -- If sp is a Right value containing a TypeError
          String -> Either Space String
forall a b. b -> Either a b
Right String
r
  infer TypingContext Space
_ (AssocC AssocConcatOper
SUnion [Expr]
_) = String -> Either Space String
forall a b. b -> Either a b
Right String
"Associative addition requires at least one operand."
    
  infer TypingContext Space
cxt (C UID
uid) = TypingContext Space -> UID -> Either Space String
forall t. TypingContext t -> UID -> Either t String
inferFromContext TypingContext Space
cxt UID
uid

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

  infer TypingContext Space
cxt (FCall UID
uid [Expr]
exs) = case (TypingContext Space -> UID -> Either Space String
forall t. TypingContext t -> UID -> Either t String
inferFromContext TypingContext Space
cxt UID
uid, (Expr -> Either Space String) -> [Expr] -> [Either Space String]
forall a b. (a -> b) -> [a] -> [b]
map (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt) [Expr]
exs) of
    (Left (S.Function NonEmpty Space
params Space
out), [Either Space String]
exst) -> 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 Space String] -> [Space]
forall a b. [Either a b] -> [a]
lefts [Either Space String]
exst
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
out
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Function `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UID -> String
forall a. Show a => a -> String
show UID
uid String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` expects parameters of types: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NonEmpty Space -> String
forall a. Show a => a -> String
show NonEmpty Space
params String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Space] -> String
forall a. Show a => a -> String
show ([Either Space String] -> [Space]
forall a b. [Either a b] -> [a]
lefts [Either Space String]
exst) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    (Left Space
s, [Either Space String]
_) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Function application on non-function `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UID -> String
forall a. Show a => a -> String
show UID
uid String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")."
    (Right String
x, [Either Space String]
_) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x

  infer TypingContext Space
cxt (Case Completeness
_ [(Expr, Expr)]
ers)
    | [(Expr, Expr)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Expr, Expr)]
ers = String -> Either Space String
forall a b. b -> Either a b
Right String
"Case contains no expressions, no type to infer."
    | ((Expr, Expr) -> Bool) -> [(Expr, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Expr
ne, Expr
_) -> TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
ne Either Space String -> Either Space String -> Bool
forall a. Eq a => a -> a -> Bool
== Either Space String
eT) ([(Expr, Expr)] -> [(Expr, Expr)]
forall a. HasCallStack => [a] -> [a]
tail [(Expr, Expr)]
ers) = Either Space String
eT
    | Bool
otherwise = String -> Either Space String
forall a b. b -> Either a b
Right String
"Expressions in case statement contain different types."
      where
        (Expr
fe, Expr
_) = [(Expr, Expr)] -> (Expr, Expr)
forall a. HasCallStack => [a] -> a
head [(Expr, Expr)]
ers
        eT :: Either Space String
eT = TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
fe

  infer TypingContext Space
cxt (Matrix [[Expr]]
exss)
    | [[Expr]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Expr]]
exss = String -> Either Space String
forall a b. b -> Either a b
Right String
"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 = String -> Either Space String
forall a b. b -> Either a b
Right String
"Matrix has no columns."
    | Bool
allRowsHaveSameColumnsAndSpace = Space -> Either Space String
forall a b. a -> Either a b
Left (Space -> Either Space String) -> Space -> Either Space String
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Space -> Space
S.Matrix Int
rows Int
columns Space
t
    | Bool
otherwise = String -> Either Space String
forall a b. b -> Either a b
Right String
"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 Space String]]
sss = ([Expr] -> [Either Space String])
-> [[Expr]] -> [[Either Space String]]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Either Space String) -> [Expr] -> [Either Space String]
forall a b. (a -> b) -> [a] -> [b]
map (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt)) [[Expr]]
exss
        expT :: Either Space String
expT = [Either Space String] -> Either Space String
forall a. HasCallStack => [a] -> a
head ([Either Space String] -> Either Space String)
-> [Either Space String] -> Either Space String
forall a b. (a -> b) -> a -> b
$ [[Either Space String]] -> [Either Space String]
forall a. HasCallStack => [a] -> a
head [[Either Space String]]
sss
        allRowsHaveSameColumnsAndSpace :: Bool
allRowsHaveSameColumnsAndSpace
          = (Space -> Bool) -> (String -> Bool) -> Either Space String -> Bool
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (\Space
_ -> ([Either Space String] -> Bool) -> [[Either Space String]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ [Either Space String]
r -> [Either Space String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Space String]
r Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
columns Bool -> Bool -> Bool
&& (Either Space String -> Bool) -> [Either Space String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Either Space String -> Either Space String -> Bool
forall a. Eq a => a -> a -> Bool
== Either Space String
expT) [Either Space String]
r) [[Either Space String]]
sss)
              (Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
False) Either Space String
expT
        t :: Space
t = Space -> Either Space String -> Space
forall a b. a -> Either a b -> a
fromLeft (String -> Space
forall a. HasCallStack => String -> a
error String
"Infer on Matrix had a strong expectation of Left-valued data.") Either Space String
expT -- This error should never occur.

  infer TypingContext Space
_ (Set Space
s [Expr]
_) = Space -> Either Space String
forall a b. a -> Either a b
Left Space
s

  infer TypingContext Space
cxt (UnaryOp UFunc
uf Expr
ex) = case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
ex of
    Left Space
sp -> case UFunc
uf of
      UFunc
Abs -> if Space -> Bool
S.isBasicNumSpace Space
sp Bool -> Bool -> Bool
&& Space
sp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
S.Natural
        then Space -> Either Space String
forall a b. a -> Either a b
Left Space
sp
        else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Numeric 'absolute' value operator only applies to, non-natural, numeric types. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
      UFunc
Neg -> if Space -> Bool
S.isBasicNumSpace Space
sp Bool -> Bool -> Bool
&& Space
sp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
S.Natural
        then Space -> Either Space String
forall a b. a -> Either a b
Left Space
sp
        else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Negation only applies to, non-natural, numeric types. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
      UFunc
Exp -> if Space
sp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Real Bool -> Bool -> Bool
|| Space
sp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Integer then Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Real else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ UFunc -> String
forall a. Show a => a -> String
show UFunc
Exp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" only applies to reals."
      UFunc
x -> if Space
sp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Real
        then Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Real
        else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ UFunc -> String
forall a. Show a => a -> String
show UFunc
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" only applies to Reals. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    Either Space String
x       -> Either Space String
x

  infer TypingContext Space
cxt (UnaryOpB UFuncB
Not Expr
ex) = case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
ex of
    Left Space
S.Boolean -> Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Boolean
    Left Space
sp        -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"¬ on non-boolean operand, " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    Either Space String
x              -> Either Space String
x

  infer TypingContext Space
cxt (UnaryOpVV UFuncVV
NegV Expr
e) = case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
e of
    Left (S.Vect Space
sp) -> if Space -> Bool
S.isBasicNumSpace Space
sp Bool -> Bool -> Bool
&& Space
sp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
S.Natural
      then Space -> Either Space String
forall a b. a -> Either a b
Left (Space -> Either Space String) -> Space -> Either Space String
forall a b. (a -> b) -> a -> b
$ Space -> Space
S.Vect Space
sp
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector negation only applies to, non-natural, numbered vectors. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    Left Space
sp -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector negation should only be applied to numeric vectors. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    Either Space String
x -> Either Space String
x

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Norm Expr
e) = case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
e of
    Left (S.Vect Space
S.Real) -> Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Real
    Left Space
sp -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector norm only applies to vectors of real numbers. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    Either Space String
x -> Either Space String
x

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Dim Expr
e) = case TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
e of
    Left (S.Vect Space
_) -> Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Integer -- FIXME: I feel like Integer would be more usable, but S.Natural is the 'real' expectation here
    Left Space
sp -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector 'dim' only applies to vectors. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
sp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    Either Space String
x -> Either Space String
x

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Frac Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left Space
rt) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rt
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Fractions/divisions should only be applied to the same numeric typed operands. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` / `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_      , Right String
e) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Right String
e, Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Pow Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left Space
rt) -> 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 Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$
        String
"Powers should only be applied to the same numeric type in both operands, or real base with integer exponent. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` ^ `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_      , Right String
x) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
    (Right String
x, Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x

  infer TypingContext Space
cxt (ArithBinaryOp ArithBinOp
Subt Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left Space
rt) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rt
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Both operands of a subtraction must be the same numeric type. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` - `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
re) -> String -> Either Space String
forall a b. b -> Either a b
Right String
re
    (Right String
le, Either Space String
_) -> String -> Either Space String
forall a b. b -> Either a b
Right String
le

  infer TypingContext Space
cxt (BoolBinaryOp BoolBinOp
_ Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
S.Boolean, Left Space
S.Boolean) -> Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Boolean
    (Left Space
lt, Left Space
rt) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Boolean expression contains non-boolean operand. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` & `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_     , Right String
er) -> String -> Either Space String
forall a b. b -> Either a b
Right String
er
    (Right String
el, Either Space String
_     ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
el

  infer TypingContext Space
cxt (EqBinaryOp EqBinOp
_ Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left Space
rt) -> if Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rt
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Boolean
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Both operands of an (in)equality (=/≠) must be of the same type. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` & `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
re) -> String -> Either Space String
forall a b. b -> Either a b
Right String
re
    (Right String
le, Either Space String
_) -> String -> Either Space String
forall a b. b -> Either a b
Right String
le

  infer TypingContext Space
cxt (LABinaryOp LABinOp
Index Expr
l Expr
n) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
n) of
    (Left (S.Vect Space
lt), Left Space
nt) -> if Space
nt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Integer Bool -> Bool -> Bool
|| Space
nt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Natural -- I guess we should only want it to be natural numbers, but integers or naturals is fine for now
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"List accessor not of type Integer nor Natural, but of type `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
nt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`"
    (Left Space
lt         , Left Space
_)  -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"List accessor expects a list/vector, but received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_               , Right String
e) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Right String
e         , Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
  infer TypingContext Space
cxt (LABinaryOp LABinOp
IndexOf Expr
l Expr
n) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
n) of
    (Left (S.Set Space
lt), Left Space
nt) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
nt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
lt-- I guess we should only want it to be natural numbers, but integers or naturals is fine for now
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"List accessor not of type Integer nor Natural, but of type `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
nt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`"
    (Left Space
lt         , Left Space
_)  -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"List accessor expects a list/vector, but received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_               , Right String
e) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Right String
e         , Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
  infer TypingContext Space
cxt (OrdBinaryOp OrdBinOp
_ Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left Space
rt) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rt
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Boolean
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Both operands of a numeric comparison must be the same numeric type, got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
    (Either Space String
_, Right String
re) -> String -> Either Space String
forall a b. b -> Either a b
Right String
re
    (Right String
le, Either Space String
_) -> String -> Either Space String
forall a b. b -> Either a b
Right String
le

  infer TypingContext Space
cxt (NVVBinaryOp NVVBinOp
Scale Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left (S.Vect Space
rsp)) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rsp
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
rsp
      else if Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
/= Space
rsp then
        String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector scaling expects a scaling by the same kind as the vector's but found scaling by`" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` over vectors of type `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
      else
        String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector scaling expects a numeric scaling, but found `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Left Space
_, Left Space
rsp) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector scaling expects vector as second operand. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
rx) -> String -> Either Space String
forall a b. b -> Either a b
Right String
rx
    (Right String
lx, Either Space String
_) -> String -> Either Space String
forall a b. b -> Either a b
Right String
lx

  infer TypingContext Space
cxt (VVVBinaryOp VVVBinOp
o Expr
l Expr
r) = TypingContext Space
-> VVVBinOp -> Expr -> Expr -> Either Space String
vvvInfer TypingContext Space
cxt VVVBinOp
o Expr
l Expr
r
    {- case (infer cxt l, infer cxt r) of
    (Left lTy, Left rTy) -> if lTy == rTy && S.isBasicNumSpace lTy && lTy /= S.Natural
      then Left lTy
      else Right $ "Vector cross product expects both operands to be vectors of non-natural numbers. Received `" ++ show lTy ++ "` X `" ++ show rTy ++ "`."
    (_       , Right re) -> Right re
    (Right le, _       ) -> Right le
    -}

  infer TypingContext Space
cxt (VVNBinaryOp VVNBinOp
Dot Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left lt :: Space
lt@(S.Vect Space
lsp), Left rt :: Space
rt@(S.Vect Space
rsp)) -> if Space
lsp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rsp Bool -> Bool -> Bool
&& Space -> Bool
S.isBasicNumSpace Space
lsp
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lsp
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector dot product expects same numeric vector types, but found `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` · `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Left Space
lsp, Left Space
rsp) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Vector dot product expects vector operands. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` · `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
rx) -> String -> Either Space String
forall a b. b -> Either a b
Right String
rx
    (Right String
lx, Either Space String
_) -> String -> Either Space String
forall a b. b -> Either a b
Right String
lx

  infer TypingContext Space
cxt (ESSBinaryOp ESSBinOp
_ Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left rt :: Space
rt@(S.Set Space
rsp)) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rsp
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Set Add/Sub should only be applied to Set of same space. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` / `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_      , Right String
e) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Right String
e, Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Left Space
lt, Left Space
rsp) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Set union expects set operands. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` · `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."

  infer TypingContext Space
cxt (ESBBinaryOp ESBBinOp
_ Expr
l Expr
r) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
r) of
    (Left Space
lt, Left rt :: Space
rt@(S.Set Space
rsp)) -> if Space -> Bool
S.isBasicNumSpace Space
lt Bool -> Bool -> Bool
&& Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rsp
      then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
      else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Set contains should only be applied to Set of same space. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` / `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_      , Right String
e) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Right String
e, Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
e
    (Left Space
lt, Left Space
rsp) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"Set union expects set operands. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` · `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rsp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."

  infer TypingContext Space
cxt (Operator AssocArithOper
_ (S.BoundedDD Symbol
_ RTopology
_ Expr
bot Expr
top) Expr
body) =
    let expTy :: Space
expTy = Space
S.Integer in
    case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
bot, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
top, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
body) of
      (Left Space
botTy, Left Space
topTy, Left Space
bodyTy) -> if Space
botTy Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Integer
        then if Space
topTy Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Integer
          then if Space
expTy Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
bodyTy
            then Space -> Either Space String
forall a b. a -> Either a b
Left Space
expTy
            else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"'Big' operator range body not Integer, found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
bodyTy String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
          else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"'Big' operator range top not Integer, found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
topTy String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
        else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$ String
"'Big' operator range bottom not of expected type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
expTy String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", found: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
botTy String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
      (Either Space String
_         , Either Space String
_         , Right String
x    ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
      (Either Space String
_         , Right String
x   , Either Space String
_          ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
      (Right String
x   , Either Space String
_         , Either Space String
_          ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x

  infer TypingContext Space
cxt (RealI UID
uid RealInterval Expr Expr
ri) =
    case (TypingContext Space -> UID -> Either Space String
forall t. TypingContext t -> UID -> Either t String
inferFromContext TypingContext Space
cxt UID
uid, RealInterval Expr Expr -> Either Space String
riTy RealInterval Expr Expr
ri) of
      (Left Space
S.Real, Left Space
riSp) -> if Space
riSp Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
S.Real
        then Space -> Either Space String
forall a b. a -> Either a b
Left Space
S.Boolean
        else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$
          String
"Real interval expects interval bounds to be of type Real, but received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
riSp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"."
      (Left Space
uidSp, Either Space String
_         ) -> String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$
        String
"Real interval expects variable to be of type Real, but received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ UID -> String
forall a. Show a => a -> String
show UID
uid String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` of type `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
uidSp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
      (Either Space String
_          , Right String
x  ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
      (Right String
x    , Either Space String
_        ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
    where
      riTy :: RealInterval Expr Expr -> Either Space TypeError
      riTy :: RealInterval Expr Expr -> Either Space String
riTy (S.Bounded (Inclusive
_, Expr
lx) (Inclusive
_, Expr
rx)) = case (TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
lx, TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
rx) of
        (Left Space
lt, Left Space
rt) -> if Space
lt Space -> Space -> Bool
forall a. Eq a => a -> a -> Bool
== Space
rt
          then Space -> Either Space String
forall a b. a -> Either a b
Left Space
lt
          else String -> Either Space String
forall a b. b -> Either a b
Right (String -> Either Space String) -> String -> Either Space String
forall a b. (a -> b) -> a -> b
$
            String
"Bounded real interval contains mismatched types for bottom and top. Received `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
lt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"` to `" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Space -> String
forall a. Show a => a -> String
show Space
rt String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"`."
        (Either Space String
_      , Right String
x) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
        (Right String
x, Either Space String
_      ) -> String -> Either Space String
forall a b. b -> Either a b
Right String
x
      riTy (S.UpTo (Inclusive
_, Expr
x)) = TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
x
      riTy (S.UpFrom (Inclusive
_, Expr
x)) = TypingContext Space -> Expr -> Either Space String
forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
x