module Language.Drasil.WellTyped (
  RequiresChecking(..), Typed(..), TypingContext,
  TypeError, inferFromContext, temporaryIndent,
  typeCheckByInfer, assertAllEq, (~==)
) where

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

import Drasil.Database (UID)

-- 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 [Char] 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 [Char] t
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure t
t
    Maybe t
Nothing -> [Char] -> Either [Char] t
forall a b. a -> Either a b
Left ([Char] -> Either [Char] t) -> [Char] -> Either [Char] t
forall a b. (a -> b) -> a -> b
$ [Char]
"`" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> UID -> [Char]
forall a. Show a => a -> [Char]
show UID
u [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"` 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 -> ([Char] -> [Char] -> [Char]) -> Either [Char] ()
assertEq t
lt t
rt [Char] -> [Char] -> [Char]
te
  | t
lt t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
rt  = () -> Either [Char] ()
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise = [Char] -> Either [Char] ()
forall a b. a -> Either a b
Left ([Char] -> Either [Char] ()) -> [Char] -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
te (t -> [Char]
forall a. Show a => a -> [Char]
show t
lt) (t -> [Char]
forall a. Show a => a -> [Char]
show t
rt)

infix 4 ~==
(~==) :: (Show t, Eq t) => t -> t -> (String -> String -> TypeError) -> Either TypeError ()
~== :: forall t.
(Show t, Eq t) =>
t -> t -> ([Char] -> [Char] -> [Char]) -> Either [Char] ()
(~==) = t -> t -> ([Char] -> [Char] -> [Char]) -> Either [Char] ()
forall t.
(Show t, Eq t) =>
t -> t -> ([Char] -> [Char] -> [Char]) -> Either [Char] ()
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 [Char] t
typeCheckByInfer TypingContext t
cxt e
e t
t = do
  et <- TypingContext t -> e -> Either [Char] t
forall e t. Typed e t => TypingContext t -> e -> Either [Char] t
infer TypingContext t
cxt e
e
  et ~== t
    $ \[Char]
lt [Char]
rt -> [Char]
"Inferred type `" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
lt [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"` does not match expected type `" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
rt [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"`"
  pure 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 -> [Char] -> Either [Char] ()
assertAllEq TypingContext t
cxt [e]
es t
expect [Char]
s
  | Bool
allTsAreSp = () -> Either [Char] ()
forall a. a -> Either [Char] a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  | Bool
otherwise  = [Char] -> Either [Char] ()
forall a b. a -> Either a b
Left ([Char] -> Either [Char] ()) -> [Char] -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> [Char]
temporaryIndent [Char]
"  " ([Char]
s [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
"\nReceived:\n" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
dumpAllTs)
  where
    allTs :: [Either [Char] t]
allTs = TypingContext t -> e -> Either [Char] t
forall e t. Typed e t => TypingContext t -> e -> Either [Char] t
infer TypingContext t
cxt (e -> Either [Char] t) -> [e] -> [Either [Char] t]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [e]
es
    allTsAreSp :: Bool
allTsAreSp = (Either [Char] t -> Bool) -> [Either [Char] 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 [Char]
_   -> Bool
False) [Either [Char] t]
allTs
    dumpAllTs :: [Char]
dumpAllTs = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ ([Char]
"- " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char])
-> (Either [Char] t -> [Char]) -> Either [Char] t -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char] -> [Char]) -> (t -> [Char]) -> Either [Char] t -> [Char]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Char]
"ERROR: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) t -> [Char]
forall a. Show a => a -> [Char]
show (Either [Char] t -> [Char]) -> [Either [Char] t] -> [[Char]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Either [Char] 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 :: [Char] -> [Char] -> [Char]
temporaryIndent [Char]
r (Char
'\n' : [Char]
s) = Char
'\n' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: ([Char]
r [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char] -> [Char] -> [Char]
temporaryIndent [Char]
r [Char]
s)
temporaryIndent [Char]
r (Char
c    : [Char]
s) = Char
c Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char] -> [Char] -> [Char]
temporaryIndent [Char]
r [Char]
s
temporaryIndent [Char]
_ []         = []