{-# 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
_ [c]
_ 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 = forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\(QuantityDict
dict, Int
_) -> QuantityDict
dict forall s a. s -> Getting a s a -> a
^. forall c. HasSpace c => Getter c Space
typ) (ChunkDB -> SymbolMap
symbolTable ChunkDB
chks)

    -- dump out the list of variables
    String -> IO ()
putStr String
"Symbol Table: "
    forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ 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 = forall a b. (a -> b) -> [a] -> [b]
map (\t
t -> (t
t forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid, 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 = forall t.
(HasUID t, RequiresChecking t Expr Space) =>
[t] -> [(UID, [(Expr, Space)])]
exprSpaceTups [InstanceModel]
ims forall a. [a] -> [a] -> [a]
++ 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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(UID
_, [(Expr, Space)]
exsps) -> 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
    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ 
      (\(UID
t, [(Expr, Space)]
_) -> String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ String
"WARNING: `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UID
t 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 = forall a b. (a -> b) -> [a] -> [b]
map (forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (forall a b. (a -> b) -> [a] -> [b]
map (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (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 = forall a b. (a -> b) -> [a] -> [b]
map 
                          (\(UID
t, [Either Space String]
tcs) -> if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a b. Either a b -> Bool
isRight [Either Space String]
tcs
                            then forall a b. b -> Either a b
Right (String
"`" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UID
t forall a. [a] -> [a] -> [a]
++ String
"` exposes ill-typed expressions!", forall a. (a -> Bool) -> [a] -> [a]
filter forall a b. Either a b -> Bool
isRight [Either Space String]
tcs)
                            else forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"`" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UID
t 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 forall a b. (a -> b) -> a -> b
$ String -> String -> String
temporaryIndent String
"  " String
s

    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (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
              forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
errConsumer (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"