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