{-# LANGUAGE FlexibleContexts #-}
module Language.Drasil.TypeCheck where

import qualified Data.Map.Strict as M

import Language.Drasil
import Database.Drasil (symbolTable)
import Data.Either (isRight, rights)
import Control.Lens ((^.))
import Data.Bifunctor (second)
import Data.List (partition)
import SysInfo.Drasil (SystemInformation(SI))

typeCheckSI :: SystemInformation -> IO ()
typeCheckSI :: SystemInformation -> IO ()
typeCheckSI
  (SI a
_ b
_ People
_ Purpose
_ Purpose
_ Purpose
_ Purpose
_ [e]
_ [f]
_ [InstanceModel]
ims [DataDefinition]
dds [String]
_ [h]
_ [i]
_ [Block SimpleQDef]
_ [j]
_ [ConstQDef]
_ ChunkDB
chks ChunkDB
_ ReferenceDB
_)
  = do
    -- build a variable context (a map of UIDs to "Space"s [types])
    let cxt :: Map UID Space
cxt = ((QuantityDict, Int) -> Space)
-> Map UID (QuantityDict, Int) -> Map UID Space
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\(QuantityDict
dict, Int
_) -> QuantityDict
dict QuantityDict -> Getting Space QuantityDict Space -> Space
forall s a. s -> Getting a s a -> a
^. Getting Space QuantityDict Space
forall c. HasSpace c => Getter c Space
Getter QuantityDict Space
typ) (ChunkDB -> Map UID (QuantityDict, Int)
symbolTable ChunkDB
chks)

    -- dump out the list of variables
    String -> IO ()
putStr String
"Symbol Table: "
    [(UID, Space)] -> IO ()
forall a. Show a => a -> IO ()
print ([(UID, Space)] -> IO ()) -> [(UID, Space)] -> IO ()
forall a b. (a -> b) -> a -> b
$ Map UID Space -> [(UID, Space)]
forall k a. Map k a -> [(k, a)]
M.toList Map UID Space
cxt

    String -> IO ()
putStrLn String
"=====[ Start type checking ]====="
    let
      exprSpaceTups :: (HasUID t, RequiresChecking t Expr Space) => [t] -> [(UID, [(Expr, Space)])] 
      exprSpaceTups :: forall t.
(HasUID t, RequiresChecking t Expr Space) =>
[t] -> [(UID, [(Expr, Space)])]
exprSpaceTups = (t -> (UID, [(Expr, Space)])) -> [t] -> [(UID, [(Expr, Space)])]
forall a b. (a -> b) -> [a] -> [b]
map (\t
t -> (t
t t -> Getting UID t UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID t UID
forall c. HasUID c => Getter c UID
Getter t UID
uid, t -> [(Expr, Space)]
forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks t
t))

    -- grab all type-check-able expressions (w.r.t. Space) from DDs and IMs
    let toChk :: [(UID, [(Expr, Space)])]
toChk = [InstanceModel] -> [(UID, [(Expr, Space)])]
forall t.
(HasUID t, RequiresChecking t Expr Space) =>
[t] -> [(UID, [(Expr, Space)])]
exprSpaceTups [InstanceModel]
ims [(UID, [(Expr, Space)])]
-> [(UID, [(Expr, Space)])] -> [(UID, [(Expr, Space)])]
forall a. [a] -> [a] -> [a]
++ [DataDefinition] -> [(UID, [(Expr, Space)])]
forall t.
(HasUID t, RequiresChecking t Expr Space) =>
[t] -> [(UID, [(Expr, Space)])]
exprSpaceTups [DataDefinition]
dds

    -- split up theories by "ones that contain things to type check" vs "not",
    -- but in reverse
    let ([(UID, [(Expr, Space)])]
notChkd, [(UID, [(Expr, Space)])]
chkd) = ((UID, [(Expr, Space)]) -> Bool)
-> [(UID, [(Expr, Space)])]
-> ([(UID, [(Expr, Space)])], [(UID, [(Expr, Space)])])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(UID
_, [(Expr, Space)]
exsps) -> [(Expr, Space)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Expr, Space)]
exsps) [(UID, [(Expr, Space)])]
toChk

    -- note that some theories didn't expose anything to type-check
    ((UID, [(Expr, Space)]) -> IO ())
-> [(UID, [(Expr, Space)])] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ 
      (\(UID
t, [(Expr, Space)]
_) -> String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"WARNING: `" String -> String -> String
forall a. [a] -> [a] -> [a]
++ UID -> String
forall a. Show a => a -> String
show UID
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"` does not expose any expressions to type check.")
      [(UID, [(Expr, Space)])]
notChkd

    -- type check them
    let chkdd :: [(UID, [Either Space String])]
chkdd = ((UID, [(Expr, Space)]) -> (UID, [Either Space String]))
-> [(UID, [(Expr, Space)])] -> [(UID, [Either Space String])]
forall a b. (a -> b) -> [a] -> [b]
map (([(Expr, Space)] -> [Either Space String])
-> (UID, [(Expr, Space)]) -> (UID, [Either Space String])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (((Expr, Space) -> Either Space String)
-> [(Expr, Space)] -> [Either Space String]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Space -> Either Space String)
-> (Expr, Space) -> Either Space String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Map UID Space -> Expr -> Space -> Either Space String
forall e t.
Typed e t =>
TypingContext t -> e -> t -> Either t String
check Map UID Space
cxt)))) [(UID, [(Expr, Space)])]
chkd

    -- format 'ok' messages and 'type error' messages, as applicable
    let formattedChkd :: [Either [Char] ([Char], [Either Space TypeError])]
        formattedChkd :: [Either String (String, [Either Space String])]
formattedChkd = ((UID, [Either Space String])
 -> Either String (String, [Either Space String]))
-> [(UID, [Either Space String])]
-> [Either String (String, [Either Space String])]
forall a b. (a -> b) -> [a] -> [b]
map 
                          (\(UID
t, [Either Space String]
tcs) -> if (Either Space String -> Bool) -> [Either Space String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Either Space String -> Bool
forall a b. Either a b -> Bool
isRight [Either Space String]
tcs
                            then (String, [Either Space String])
-> Either String (String, [Either Space String])
forall a b. b -> Either a b
Right (String
"`" String -> String -> String
forall a. [a] -> [a] -> [a]
++ UID -> String
forall a. Show a => a -> String
show UID
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"` exposes ill-typed expressions!", (Either Space String -> Bool)
-> [Either Space String] -> [Either Space String]
forall a. (a -> Bool) -> [a] -> [a]
filter Either Space String -> Bool
forall a b. Either a b -> Bool
isRight [Either Space String]
tcs)
                            else String -> Either String (String, [Either Space String])
forall a b. a -> Either a b
Left (String -> Either String (String, [Either Space String]))
-> String -> Either String (String, [Either Space String])
forall a b. (a -> b) -> a -> b
$ String
"`" String -> String -> String
forall a. [a] -> [a] -> [a]
++ UID -> String
forall a. Show a => a -> String
show UID
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"` OK!") 
                          [(UID, [Either Space String])]
chkdd

    let errConsumer :: String -> IO ()
errConsumer String
s = do 
          String -> IO ()
putStr String
"  - ERROR: "
          String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> String
temporaryIndent String
"  " String
s

    (Either String (String, [Either Space String]) -> IO ())
-> [Either String (String, [Either Space String])] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((String -> IO ())
-> ((String, [Either Space String]) -> IO ())
-> Either String (String, [Either Space String])
-> IO ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
            String -> IO ()
putStrLn
            (\(String
tMsg, [Either Space String]
tcs) -> do
              String -> IO ()
putStrLn String
tMsg
              (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
errConsumer ([Either Space String] -> [String]
forall a b. [Either a b] -> [b]
rights [Either Space String]
tcs)
            )
      ) [Either String (String, [Either Space String])]
formattedChkd
    String -> IO ()
putStrLn String
"=====[ Finished type checking ]====="

    -- TODO: When we want to have Drasil panic on type-errors, use the following code:
    -- add back import: Control.Monad (when)
    -- when (any isRight formattedChkd) $ error "Type errors occurred, please check your expressions and adjust accordingly"