{-# 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)
type TypeError = String
type TypingContext t = M.Map UID t
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"
class (Eq t, Show t) => Typed e t where
infer :: TypingContext t -> e -> Either TypeError t
check :: TypingContext t -> e -> t -> Either TypeError t
class Typed e t => RequiresChecking c e t where
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
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
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
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
_ [] = []