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

module Language.Drasil.WellTyped where

import qualified Data.Map.Strict as M
import Drasil.Database.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 TypeError t
inferFromContext :: forall t. TypingContext t -> UID -> Either TypeError t
inferFromContext TypingContext t
cxt UID
u =
  case UID -> TypingContext t -> Maybe t
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup UID
u TypingContext t
cxt of
    Just t
t  -> t -> Either TypeError t
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
t
    Maybe t
Nothing -> TypeError -> Either TypeError t
forall a b. a -> Either a b
Left (TypeError -> Either TypeError t)
-> TypeError -> Either TypeError t
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"

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

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

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

assertEq :: (Show t, Eq t) => t -> t -> (String -> String -> TypeError) -> Either TypeError ()
assertEq :: forall t.
(Show t, Eq t) =>
t
-> t
-> (TypeError -> TypeError -> TypeError)
-> Either TypeError ()
assertEq t
lt t
rt TypeError -> TypeError -> TypeError
te
  | t
lt t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
rt  = () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise = TypeError -> Either TypeError ()
forall a b. a -> Either a b
Left (TypeError -> Either TypeError ())
-> TypeError -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ TypeError -> TypeError -> TypeError
te (t -> TypeError
forall a. Show a => a -> TypeError
show t
lt) (t -> TypeError
forall a. Show a => a -> TypeError
show t
rt)

infix 4 ~==
(~==) :: (Show t, Eq t) => t -> t -> (String -> String -> TypeError) -> Either TypeError ()
~== :: forall t.
(Show t, Eq t) =>
t
-> t
-> (TypeError -> TypeError -> TypeError)
-> Either TypeError ()
(~==) = t
-> t
-> (TypeError -> TypeError -> TypeError)
-> Either TypeError ()
forall t.
(Show t, Eq t) =>
t
-> t
-> (TypeError -> TypeError -> TypeError)
-> Either TypeError ()
assertEq

-- | ``Check'' an expressions type based by an inference.
typeCheckByInfer :: Typed e t => TypingContext t -> e -> t -> Either TypeError t
typeCheckByInfer :: forall e t.
Typed e t =>
TypingContext t -> e -> t -> Either TypeError t
typeCheckByInfer TypingContext t
cxt e
e t
t = do
  t
et <- TypingContext t -> e -> Either TypeError t
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext t
cxt e
e
  t
et t
-> t
-> (TypeError -> TypeError -> TypeError)
-> Either TypeError ()
forall t.
(Show t, Eq t) =>
t
-> t
-> (TypeError -> TypeError -> TypeError)
-> Either TypeError ()
~== t
t 
    ((TypeError -> TypeError -> TypeError) -> Either TypeError ())
-> (TypeError -> TypeError -> TypeError) -> Either TypeError ()
forall a b. (a -> b) -> a -> b
$ \TypeError
lt TypeError
rt -> TypeError
"Inferred type `" TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
lt TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
"` does not match expected type `" TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
rt TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++ TypeError
"`"
  t -> Either TypeError t
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
et

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

assertAllEq :: Typed e t => TypingContext t -> [e] -> t -> TypeError -> Either TypeError ()
assertAllEq :: forall e t.
Typed e t =>
TypingContext t -> [e] -> t -> TypeError -> Either TypeError ()
assertAllEq TypingContext t
cxt [e]
es t
expect TypeError
s
  | Bool
allTsAreSp = () -> Either TypeError ()
forall a. a -> Either TypeError a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise  = TypeError -> Either TypeError ()
forall a b. a -> Either a b
Left (TypeError -> Either TypeError ())
-> TypeError -> Either 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 TypeError t]
allTs = (e -> Either TypeError t) -> [e] -> [Either TypeError t]
forall a b. (a -> b) -> [a] -> [b]
map (TypingContext t -> e -> Either TypeError t
forall e t. Typed e t => TypingContext t -> e -> Either TypeError t
infer TypingContext t
cxt) [e]
es
    allTsAreSp :: Bool
allTsAreSp = (Either TypeError t -> Bool) -> [Either TypeError t] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\case
      Right  t
t -> t
t t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
expect
      Left TypeError
_   -> Bool
False) [Either TypeError t]
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 TypeError t -> TypeError)
-> [Either TypeError t] -> [TypeError]
forall a b. (a -> b) -> [a] -> [b]
map ((TypeError
"- " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++) (TypeError -> TypeError)
-> (Either TypeError t -> TypeError)
-> Either TypeError t
-> TypeError
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeError -> TypeError)
-> (t -> TypeError) -> Either TypeError t -> TypeError
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (TypeError
"ERROR: " TypeError -> TypeError -> TypeError
forall a. [a] -> [a] -> [a]
++) t -> TypeError
forall a. Show a => a -> TypeError
show) [Either TypeError t]
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
_ []         = []