{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE LambdaCase #-}

module Language.Drasil.WellTyped where

import qualified Data.Map.Strict as M
import Language.Drasil.UID (UID)
import Data.List (intercalate)

-- TODO: Rather than using a flat String, it would be better to a
--       ``breadcrumb''-style error data type that can provide a traceable path
--       to issues in an expression. The breadcrumbs could then be formatted
--       into a flat String, such as it is now, or into alternative AST views
--       that show exactly where typing went awry.
type TypeError = String

-- | We can only type check 'UID's within a type context relating 'UID's to
--   types since they don't carry any type information.
type TypingContext t = M.Map UID t

-- | Look for a known type of a specific 'UID'.
inferFromContext :: TypingContext t -> UID -> Either t TypeError
inferFromContext :: forall t. TypingContext t -> UID -> Either t TypeError
inferFromContext TypingContext t
cxt UID
u = Either t TypeError
-> (t -> Either t TypeError) -> Maybe t -> Either t TypeError
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
    (TypeError -> Either t TypeError
forall a b. b -> Either a b
Right (TypeError -> Either t TypeError)
-> TypeError -> Either t TypeError
forall a b. (a -> b) -> a -> b
$ TypeError
"`" TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ UID -> TypeError
forall a. Show a => a -> TypeError
show UID
u TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
"` lacks type binding in context")
    t -> Either t TypeError
forall a b. a -> Either a b
Left
    (UID -> TypingContext t -> Maybe t
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UID
u TypingContext t
cxt)

-- | Build a bidirectional type checker for your expression language, e, with
--   respect to a specific type universe, t.
class (Eq t, Show t) => Typed e t where
  
  -- | Given a typing context and an expression, infer a unique type or explain
  --   what went awry.
  infer :: TypingContext t -> e -> Either t TypeError

  -- | Given a typing context, an expression, and an expected type, check if the
  --   expression can satisfy the expectation.
  check :: TypingContext t -> e -> t -> Either t TypeError

-- | For all containers, c, which contain typed expressions, e, against a
--   specific type universe, t, expose all expressions and relations that need
--   to be type-checked.
class Typed e t => RequiresChecking c e t where
  -- | All things that need type checking.
  requiredChecks :: c -> [(e, t)]

-- | ``Check'' an expressions type based by an inference.
typeCheckByInfer :: Typed e t => TypingContext t -> e -> t -> Either t TypeError
typeCheckByInfer :: forall e t.
Typed e t =>
TypingContext t -> e -> t -> Either t TypeError
typeCheckByInfer TypingContext t
cxt e
e t
t = (t -> Either t TypeError)
-> (TypeError -> Either t TypeError)
-> Either t TypeError
-> Either t TypeError
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
    (\t
infT -> if t
t t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
infT
      then t -> Either t TypeError
forall a b. a -> Either a b
Left t
t
      else TypeError -> Either t TypeError
forall a b. b -> Either a b
Right (TypeError -> Either t TypeError)
-> TypeError -> Either t TypeError
forall a b. (a -> b) -> a -> b
$ TypeError
"Inferred type `" TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ t -> TypeError
forall a. Show a => a -> TypeError
show t
t TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
"` does not match expected type `" TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ t -> TypeError
forall a. Show a => a -> TypeError
show t
infT TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
"`")
    TypeError -> Either t TypeError
forall a b. b -> Either a b
Right
    (TypingContext t -> e -> Either t TypeError
forall e t. Typed e t => TypingContext t -> e -> Either t TypeError
infer TypingContext t
cxt e
e)

{- FIXME: temporary hacks below (they're aware of the "printing" code!), pending
          replacement when TypeError is upgraded -}

allOfType :: Typed e t => TypingContext t -> [e] -> t -> t -> TypeError -> Either t TypeError
allOfType :: forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> t -> TypeError -> Either t TypeError
allOfType TypingContext t
cxt [e]
es t
expect t
ret TypeError
s
  | Bool
allTsAreSp = t -> Either t TypeError
forall a b. a -> Either a b
Left t
ret
  | Bool
otherwise  = TypeError -> Either t TypeError
forall a b. b -> Either a b
Right (TypeError -> Either t TypeError)
-> TypeError -> Either t TypeError
forall a b. (a -> b) -> a -> b
$ TypeError -> TypeError -> TypeError
temporaryIndent TypeError
"  " (TypeError
s TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
"\nReceived:\n" TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
dumpAllTs)
  where
    allTs :: [Either t TypeError]
allTs = (e -> Either t TypeError) -> [e] -> [Either t TypeError]
forall a b. (a -> b) -> [a] -> [b]
map (TypingContext t -> e -> Either t TypeError
forall e t. Typed e t => TypingContext t -> e -> Either t TypeError
infer TypingContext t
cxt) [e]
es
    allTsAreSp :: Bool
allTsAreSp = (Either t TypeError -> Bool) -> [Either t TypeError] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
      Left  t
t -> t
t t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
expect
      Right TypeError
_ -> Bool
False) [Either t TypeError]
allTs
    dumpAllTs :: TypeError
dumpAllTs = TypeError -> [TypeError] -> TypeError
forall a. [a] -> [[a]] -> [a]
intercalate TypeError
"\n" ([TypeError] -> TypeError) -> [TypeError] -> TypeError
forall a b. (a -> b) -> a -> b
$ (Either t TypeError -> TypeError)
-> [Either t TypeError] -> [TypeError]
forall a b. (a -> b) -> [a] -> [b]
map ((TypeError
"- " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++) (TypeError -> TypeError)
-> (Either t TypeError -> TypeError)
-> Either t TypeError
-> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t -> TypeError)
-> (TypeError -> TypeError) -> Either t TypeError -> TypeError
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either t -> TypeError
forall a. Show a => a -> TypeError
show (TypeError
"ERROR: " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++)) [Either t TypeError]
allTs

-- | A temporary, hacky, indentation function. It should be removed when we
-- switch to using something else for error messages, which can be later
-- formatted nicely.
temporaryIndent :: String -> String -> String
temporaryIndent :: TypeError -> TypeError -> TypeError
temporaryIndent TypeError
r (Char
'\n' : TypeError
s) = Char
'\n' Char -> TypeError -> TypeError
forall a. a -> [a] -> [a]
: (TypeError
r TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError -> TypeError -> TypeError
temporaryIndent TypeError
r TypeError
s)
temporaryIndent TypeError
r (Char
c    : TypeError
s) = Char
c Char -> TypeError -> TypeError
forall a. a -> [a] -> [a]
: TypeError -> TypeError -> TypeError
temporaryIndent TypeError
r TypeError
s
temporaryIndent TypeError
_ []         = []