{-# 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ArithBinOp -> ArithBinOp -> Bool
$c/= :: ArithBinOp -> ArithBinOp -> Bool
== :: ArithBinOp -> ArithBinOp -> Bool
$c== :: ArithBinOp -> ArithBinOp -> Bool
Eq

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

-- | Index operator.
data LABinOp = Index
  deriving LABinOp -> LABinOp -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LABinOp -> LABinOp -> Bool
$c/= :: LABinOp -> LABinOp -> Bool
== :: LABinOp -> LABinOp -> Bool
$c== :: 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: OrdBinOp -> OrdBinOp -> Bool
$c/= :: OrdBinOp -> OrdBinOp -> Bool
== :: OrdBinOp -> OrdBinOp -> Bool
$c== :: OrdBinOp -> OrdBinOp -> Bool
Eq

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

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

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

-- TODO: I suppose these can be merged to just Add and Mul?
-- | Associative operators (adding and multiplication). Also specifies whether it is for integers or for real numbers.
data AssocArithOper = AddI | AddRe | MulI | MulRe
  deriving AssocArithOper -> AssocArithOper -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssocArithOper -> AssocArithOper -> Bool
$c/= :: AssocArithOper -> AssocArithOper -> Bool
== :: AssocArithOper -> AssocArithOper -> Bool
$c== :: AssocArithOper -> AssocArithOper -> Bool
Eq

-- | Associative boolean operators (and, or).
data AssocBoolOper = And | Or
  deriving AssocBoolOper -> AssocBoolOper -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssocBoolOper -> AssocBoolOper -> Bool
$c/= :: AssocBoolOper -> AssocBoolOper -> Bool
== :: AssocBoolOper -> AssocBoolOper -> Bool
$c== :: 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UFunc -> UFunc -> Bool
$c/= :: UFunc -> UFunc -> Bool
== :: UFunc -> UFunc -> Bool
$c== :: UFunc -> UFunc -> Bool
Eq, Int -> UFunc -> ShowS
[UFunc] -> ShowS
UFunc -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UFunc] -> ShowS
$cshowList :: [UFunc] -> ShowS
show :: UFunc -> String
$cshow :: UFunc -> String
showsPrec :: Int -> UFunc -> ShowS
$cshowsPrec :: Int -> UFunc -> ShowS
Show)

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

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

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

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

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

  -- | 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 forall a. Eq a => a -> a -> Bool
== Literal
b
  AssocA AssocArithOper
o1 [Expr]
l1        == AssocA AssocArithOper
o2 [Expr]
l2        =  AssocArithOper
o1 forall a. Eq a => a -> a -> Bool
== AssocArithOper
o2 Bool -> Bool -> Bool
&& [Expr]
l1 forall a. Eq a => a -> a -> Bool
== [Expr]
l2
  AssocB AssocBoolOper
o1 [Expr]
l1        == AssocB AssocBoolOper
o2 [Expr]
l2        =  AssocBoolOper
o1 forall a. Eq a => a -> a -> Bool
== AssocBoolOper
o2 Bool -> Bool -> Bool
&& [Expr]
l1 forall a. Eq a => a -> a -> Bool
== [Expr]
l2
  C UID
a                 == C UID
b                 =   UID
a forall a. Eq a => a -> a -> Bool
== UID
b
  FCall UID
a [Expr]
b           == FCall UID
c [Expr]
d           =   UID
a forall a. Eq a => a -> a -> Bool
== UID
c Bool -> Bool -> Bool
&& [Expr]
b forall a. Eq a => a -> a -> Bool
== [Expr]
d
  Case Completeness
a [(Expr, Expr)]
b            == Case Completeness
c [(Expr, Expr)]
d            =   Completeness
a forall a. Eq a => a -> a -> Bool
== Completeness
c Bool -> Bool -> Bool
&& [(Expr, Expr)]
b forall a. Eq a => a -> a -> Bool
== [(Expr, Expr)]
d
  UnaryOp UFunc
a Expr
b         == UnaryOp UFunc
c Expr
d         =   UFunc
a forall a. Eq a => a -> a -> Bool
== UFunc
c Bool -> Bool -> Bool
&& Expr
b forall a. Eq a => a -> a -> Bool
== Expr
d
  UnaryOpB UFuncB
a Expr
b        == UnaryOpB UFuncB
c Expr
d        =   UFuncB
a forall a. Eq a => a -> a -> Bool
== UFuncB
c Bool -> Bool -> Bool
&& Expr
b forall a. Eq a => a -> a -> Bool
== Expr
d
  UnaryOpVV UFuncVV
a Expr
b       == UnaryOpVV UFuncVV
c Expr
d       =   UFuncVV
a forall a. Eq a => a -> a -> Bool
== UFuncVV
c Bool -> Bool -> Bool
&& Expr
b forall a. Eq a => a -> a -> Bool
== Expr
d
  UnaryOpVN UFuncVN
a Expr
b       == UnaryOpVN UFuncVN
c Expr
d       =   UFuncVN
a forall a. Eq a => a -> a -> Bool
== UFuncVN
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== ArithBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== BoolBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== EqBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== OrdBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== LABinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== VVVBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== VVNBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall a. Eq a => a -> a -> Bool
== NVVBinOp
p Bool -> Bool -> Bool
&& Expr
a forall a. Eq a => a -> a -> Bool
== Expr
c Bool -> Bool -> Bool
&& Expr
b 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. LiteralC r => Integer -> r
int
  str :: String -> Expr
str = Literal -> Expr
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. LiteralC r => String -> r
str
  dbl :: Double -> Expr
dbl = Literal -> Expr
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. LiteralC r => Double -> r
dbl
  exactDbl :: Integer -> Expr
exactDbl = Literal -> Expr
Lit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall r. LiteralC r => Integer -> r
exactDbl
  perc :: Integer -> Integer -> Expr
perc Integer
l Integer
r = Literal -> Expr
Lit forall a b. (a -> b) -> a -> b
$ forall r. LiteralC r => Integer -> Integer -> r
perc Integer
l Integer
r

assocArithOperToTy :: AssocArithOper -> Space
assocArithOperToTy :: AssocArithOper -> Space
assocArithOperToTy AssocArithOper
AddI  = Space
S.Integer
assocArithOperToTy AssocArithOper
MulI  = Space
S.Integer
assocArithOperToTy AssocArithOper
AddRe = Space
S.Real
assocArithOperToTy AssocArithOper
MulRe = Space
S.Real

-- 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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
ctx Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rsp Bool -> Bool -> Bool
&& Space -> Bool
S.isBasicNumSpace Space
lsp then
        if VVVBinOp
op forall a. Eq a => a -> a -> Bool
== VVVBinOp
VSub Bool -> Bool -> Bool
&& (Space
lsp forall a. Eq a => a -> a -> Bool
== Space
S.Natural Bool -> Bool -> Bool
|| Space
rsp forall a. Eq a => a -> a -> Bool
== Space
S.Natural) then
          forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector subtraction expects both operands to be vectors of non-natural numbers. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lsp forall a. [a] -> [a] -> [a]
++ String
"` and `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rsp forall a. [a] -> [a] -> [a]
++ String
"`."
        else forall a b. a -> Either a b
Left Space
lt
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector " forall a. [a] -> [a] -> [a]
++ forall p. Pretty p => p -> String
pretty VVVBinOp
op forall a. [a] -> [a] -> [a]
++ String
" expects both operands to be vectors of non-natural numbers. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lsp forall a. [a] -> [a] -> [a]
++ String
"` and `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rsp forall a. [a] -> [a] -> [a]
++ String
"`."
    (Left Space
lsp, Left Space
rsp) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector operation " forall a. [a] -> [a] -> [a]
++ forall p. Pretty p => p -> String
pretty VVVBinOp
op forall a. [a] -> [a] -> [a]
++ String
" expects vector operands. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lsp forall a. [a] -> [a] -> [a]
++ String
"` and `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rsp forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_       , Right String
re) -> forall a b. b -> Either a b
Right String
re
    (Right String
le, 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 = 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) = forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Literal
lit

  infer TypingContext Space
cxt (AssocA AssocArithOper
op [Expr]
exs) = forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> t -> String -> Either t String
allOfType TypingContext Space
cxt [Expr]
exs Space
sp Space
sp
      forall a b. (a -> b) -> a -> b
$ String
"Associative arithmetic operation expects all operands to be of the same expected type (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
sp forall a. [a] -> [a] -> [a]
++ String
")."
    where
      sp :: Space
sp = AssocArithOper -> Space
assocArithOperToTy AssocArithOper
op

  infer TypingContext Space
cxt (AssocB AssocBoolOper
_ [Expr]
exs) = 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
    forall a b. (a -> b) -> a -> b
$ String
"Associative boolean operation expects all operands to be of the same type (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
S.Boolean forall a. [a] -> [a] -> [a]
++ String
")."

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

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

  infer TypingContext Space
cxt (Case Completeness
_ [(Expr, Expr)]
ers)
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Expr, Expr)]
ers = forall a b. b -> Either a b
Right String
"Case contains no expressions, no type to infer."
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Expr
ne, Expr
_) -> forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
ne forall a. Eq a => a -> a -> Bool
== Either Space String
eT) (forall a. [a] -> [a]
tail [(Expr, Expr)]
ers) = Either Space String
eT
    | Bool
otherwise = forall a b. b -> Either a b
Right String
"Expressions in case statement contain different types."
      where
        (Expr
fe, Expr
_) = forall a. [a] -> a
head [(Expr, Expr)]
ers
        eT :: Either Space String
eT = 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)
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Expr]]
exss = forall a b. b -> Either a b
Right String
"Matrix has no rows."
    | forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [[Expr]]
exss = forall a b. b -> Either a b
Right String
"Matrix has no columns."
    | Bool
allRowsHaveSameColumnsAndSpace = forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Int -> Int -> Space -> Space
S.Matrix Int
rows Int
columns Space
t
    | Bool
otherwise = 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Expr]]
exss
        columns :: Int
columns = if Int
rows forall a. Ord a => a -> a -> Bool
> Int
0 then forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [[Expr]]
exss else Int
0
        sss :: [[Either Space String]]
sss = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt)) [[Expr]]
exss
        expT :: Either Space String
expT = forall a. [a] -> a
head forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
head [[Either Space String]]
sss
        allRowsHaveSameColumnsAndSpace :: Bool
allRowsHaveSameColumnsAndSpace
          = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (\Space
_ -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ [Either Space String]
r -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Space String]
r forall a. Eq a => a -> a -> Bool
== Int
columns Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall a. Eq a => a -> a -> Bool
== Either Space String
expT) [Either Space String]
r) [[Either Space String]]
sss)
              (forall a b. a -> b -> a
const Bool
False) Either Space String
expT
        t :: Space
t = forall a b. a -> Either a b -> a
fromLeft (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
cxt (UnaryOp UFunc
uf Expr
ex) = case 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 forall a. Eq a => a -> a -> Bool
/= Space
S.Natural
        then forall a b. a -> Either a b
Left Space
sp
        else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Numeric 'absolute' value operator only applies to, non-natural, numeric types. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
sp forall a. [a] -> [a] -> [a]
++ String
"`."
      UFunc
Neg -> if Space -> Bool
S.isBasicNumSpace Space
sp Bool -> Bool -> Bool
&& Space
sp forall a. Eq a => a -> a -> Bool
/= Space
S.Natural
        then forall a b. a -> Either a b
Left Space
sp
        else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Negation only applies to, non-natural, numeric types. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
sp forall a. [a] -> [a] -> [a]
++ String
"`."
      UFunc
Exp -> if Space
sp forall a. Eq a => a -> a -> Bool
== Space
S.Real Bool -> Bool -> Bool
|| Space
sp forall a. Eq a => a -> a -> Bool
== Space
S.Integer then forall a b. a -> Either a b
Left Space
S.Real else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show UFunc
Exp forall a. [a] -> [a] -> [a]
++ String
" only applies to reals."
      UFunc
x -> if Space
sp forall a. Eq a => a -> a -> Bool
== Space
S.Real
        then forall a b. a -> Either a b
Left Space
S.Real
        else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show UFunc
x forall a. [a] -> [a] -> [a]
++ String
" only applies to Reals. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
sp forall a. [a] -> [a] -> [a]
++ String
"`."
    Either Space String
x       -> Either Space String
x

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

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

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

  infer TypingContext Space
cxt (UnaryOpVN UFuncVN
Dim Expr
e) = case forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
e of
    Left (S.Vect Space
_) -> 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 -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector 'dim' only applies to vectors. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
sp 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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rt
      then forall a b. a -> Either a b
Left Space
lt
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Fractions/divisions should only be applied to the same numeric typed operands. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` / `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_      , Right String
e) -> forall a b. b -> Either a b
Right String
e
    (Right String
e, 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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rt Bool -> Bool -> Bool
|| (Space
lt forall a. Eq a => a -> a -> Bool
== Space
S.Real Bool -> Bool -> Bool
&& Space
rt forall a. Eq a => a -> a -> Bool
== Space
S.Integer))
      then forall a b. a -> Either a b
Left Space
lt
      else forall a b. b -> Either a b
Right 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 `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` ^ `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_      , Right String
x) -> forall a b. b -> Either a b
Right String
x
    (Right String
x, 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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rt
      then forall a b. a -> Either a b
Left Space
lt
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Both operands of a subtraction must be the same numeric type. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` - `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
re) -> forall a b. b -> Either a b
Right String
re
    (Right String
le, Either Space String
_) -> forall a b. b -> Either a b
Right String
le

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

  infer TypingContext Space
cxt (EqBinaryOp EqBinOp
_ Expr
l Expr
r) = case (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rt
      then forall a b. a -> Either a b
Left Space
S.Boolean
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Both operands of an (in)equality (=/≠) must be of the same type. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` & `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
re) -> forall a b. b -> Either a b
Right String
re
    (Right String
le, 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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
S.Integer Bool -> Bool -> Bool
|| Space
nt 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 forall a b. a -> Either a b
Left Space
lt
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"List accessor not of type Integer nor Natural, but of type `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
nt forall a. [a] -> [a] -> [a]
++ String
"`"
    (Left Space
lt         , Left Space
_)  -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"List accessor expects a list/vector, but received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_               , Right String
e) -> forall a b. b -> Either a b
Right String
e
    (Right String
e         , Either Space String
_      ) -> forall a b. b -> Either a b
Right String
e

  infer TypingContext Space
cxt (OrdBinaryOp OrdBinOp
_ Expr
l Expr
r) = case (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rt
      then forall a b. a -> Either a b
Left Space
S.Boolean
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Both operands of a numeric comparison must be the same numeric type, got: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"."
    (Either Space String
_, Right String
re) -> forall a b. b -> Either a b
Right String
re
    (Right String
le, Either Space String
_) -> forall a b. b -> Either a b
Right String
le

  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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rsp Bool -> Bool -> Bool
&& Space -> Bool
S.isBasicNumSpace Space
lsp
      then forall a b. a -> Either a b
Left Space
lsp
      else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector dot product expects same numeric vector types, but found `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` · `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Left Space
lsp, Left Space
rsp) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector dot product expects vector operands. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lsp forall a. [a] -> [a] -> [a]
++ String
"` · `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rsp forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
rx) -> forall a b. b -> Either a b
Right String
rx
    (Right String
lx, Either Space String
_) -> forall a b. b -> Either a b
Right String
lx

  infer TypingContext Space
cxt (NVVBinaryOp NVVBinOp
Scale Expr
l Expr
r) = case (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
l, 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 forall a. Eq a => a -> a -> Bool
== Space
rsp
      then forall a b. a -> Either a b
Left Space
rsp
      else if Space
lt forall a. Eq a => a -> a -> Bool
/= Space
rsp then
        forall a b. b -> Either a b
Right 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`" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` over vectors of type `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rsp forall a. [a] -> [a] -> [a]
++ String
"`."
      else
        forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector scaling expects a numeric scaling, but found `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"`."
    (Left Space
_, Left Space
rsp) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"Vector scaling expects vector as second operand. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rsp forall a. [a] -> [a] -> [a]
++ String
"`."
    (Either Space String
_, Right String
rx) -> forall a b. b -> Either a b
Right String
rx
    (Right String
lx, Either Space String
_) -> forall a b. b -> Either a b
Right String
lx

  infer TypingContext Space
cxt (Operator AssocArithOper
aao (S.BoundedDD Symbol
_ RTopology
_ Expr
bot Expr
top) Expr
body) = 
    let expTy :: Space
expTy = AssocArithOper -> Space
assocArithOperToTy AssocArithOper
aao in
    case (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
bot, forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
top, 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 forall a. Eq a => a -> a -> Bool
== Space
S.Integer
        then if Space
topTy forall a. Eq a => a -> a -> Bool
== Space
S.Integer
          then if Space
expTy forall a. Eq a => a -> a -> Bool
== Space
bodyTy
            then forall a b. a -> Either a b
Left Space
expTy
            else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"'Big' operator range body not Integer, found: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
bodyTy forall a. [a] -> [a] -> [a]
++ String
"."
          else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"'Big' operator range top not Integer, found: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
topTy forall a. [a] -> [a] -> [a]
++ String
"."
        else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ String
"'Big' operator range bottom not of expected type: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
expTy forall a. [a] -> [a] -> [a]
++ String
", found: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
botTy forall a. [a] -> [a] -> [a]
++ String
"."
      (Either Space String
_         , Either Space String
_         , Right String
x    ) -> forall a b. b -> Either a b
Right String
x
      (Either Space String
_         , Right String
x   , Either Space String
_          ) -> forall a b. b -> Either a b
Right String
x
      (Right String
x   , Either Space 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 (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 forall a. Eq a => a -> a -> Bool
== Space
S.Real
        then forall a b. a -> Either a b
Left Space
S.Boolean
        else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
          String
"Real interval expects interval bounds to be of type Real, but received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
riSp forall a. [a] -> [a] -> [a]
++ String
"."
      (Left Space
uidSp, Either Space String
_         ) -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
        String
"Real interval expects variable to be of type Real, but received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UID
uid forall a. [a] -> [a] -> [a]
++ String
"` of type `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
uidSp forall a. [a] -> [a] -> [a]
++ String
"`."
      (Either Space String
_          , Right String
x  ) -> forall a b. b -> Either a b
Right String
x
      (Right String
x    , 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 (forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
lx, 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 forall a. Eq a => a -> a -> Bool
== Space
rt
          then forall a b. a -> Either a b
Left Space
lt
          else forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$
            String
"Bounded real interval contains mismatched types for bottom and top. Received `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
lt forall a. [a] -> [a] -> [a]
++ String
"` to `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Space
rt forall a. [a] -> [a] -> [a]
++ String
"`."
        (Either Space String
_      , Right String
x) -> forall a b. b -> Either a b
Right String
x
        (Right String
x, Either Space String
_      ) -> forall a b. b -> Either a b
Right String
x
      riTy (S.UpTo (Inclusive
_, Expr
x)) = forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
x
      riTy (S.UpFrom (Inclusive
_, Expr
x)) = forall e t. Typed e t => TypingContext t -> e -> Either t String
infer TypingContext Space
cxt Expr
x