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

import qualified Data.Map.Strict as M

import Language.Drasil
import Database.Drasil (symbolTable)
import Data.Either (isLeft, lefts)
import Control.Lens ((^.))
import Data.Bifunctor (second)
import Data.List (partition)
import Drasil.System (System, HasSystem (instModels, dataDefns, systemdb))

typeCheckSI :: System -> IO ()
typeCheckSI :: System -> IO ()
typeCheckSI System
sys = do
    let ims :: [InstanceModel]
ims = System
sys System
-> Getting [InstanceModel] System [InstanceModel]
-> [InstanceModel]
forall s a. s -> Getting a s a -> a
^. Getting [InstanceModel] System [InstanceModel]
forall c. HasSystem c => Lens' c [InstanceModel]
Lens' System [InstanceModel]
instModels
        dds :: [DataDefinition]
dds = System
sys System
-> Getting [DataDefinition] System [DataDefinition]
-> [DataDefinition]
forall s a. s -> Getting a s a -> a
^. Getting [DataDefinition] System [DataDefinition]
forall c. HasSystem c => Lens' c [DataDefinition]
Lens' System [DataDefinition]
dataDefns
        chks :: ChunkDB
chks = System
sys System -> Getting ChunkDB System ChunkDB -> ChunkDB
forall s a. s -> Getting a s a -> a
^. Getting ChunkDB System ChunkDB
forall c. HasSystem c => Lens' c ChunkDB
Lens' System ChunkDB
systemdb
    -- build a variable context (a map of UIDs to "Space"s [types])
    let cxt :: Map UID Space
cxt = ((DefinedQuantityDict, Int) -> Space)
-> Map UID (DefinedQuantityDict, Int) -> Map UID Space
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\(DefinedQuantityDict
dict, Int
_) -> DefinedQuantityDict
dict DefinedQuantityDict
-> Getting Space DefinedQuantityDict Space -> Space
forall s a. s -> Getting a s a -> a
^. Getting Space DefinedQuantityDict Space
forall c. HasSpace c => Getter c Space
Getter DefinedQuantityDict Space
typ) (ChunkDB -> Map UID (DefinedQuantityDict, 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 String Space])]
chkdd = ((UID, [(Expr, Space)]) -> (UID, [Either String Space]))
-> [(UID, [(Expr, Space)])] -> [(UID, [Either String Space])]
forall a b. (a -> b) -> [a] -> [b]
map (([(Expr, Space)] -> [Either String Space])
-> (UID, [(Expr, Space)]) -> (UID, [Either String Space])
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 String Space)
-> [(Expr, Space)] -> [Either String Space]
forall a b. (a -> b) -> [a] -> [b]
map ((Expr -> Space -> Either String Space)
-> (Expr, Space) -> Either String Space
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Map UID Space -> Expr -> Space -> Either String Space
forall e t.
Typed e t =>
TypingContext t -> e -> t -> Either String t
check Map UID Space
cxt)))) [(UID, [(Expr, Space)])]
chkd

    -- format 'ok' messages and 'type error' messages, as applicable
    let formattedChkd :: [Either (String, [Either TypeError Space]) String]
        formattedChkd :: [Either (String, [Either String Space]) String]
formattedChkd = ((UID, [Either String Space])
 -> Either (String, [Either String Space]) String)
-> [(UID, [Either String Space])]
-> [Either (String, [Either String Space]) String]
forall a b. (a -> b) -> [a] -> [b]
map 
                          (\(UID
t, [Either String Space]
tcs) -> if (Either String Space -> Bool) -> [Either String Space] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Either String Space -> Bool
forall a b. Either a b -> Bool
isLeft [Either String Space]
tcs
                            then (String, [Either String Space])
-> Either (String, [Either String Space]) String
forall a b. a -> Either a b
Left (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 String Space -> Bool)
-> [Either String Space] -> [Either String Space]
forall a. (a -> Bool) -> [a] -> [a]
filter Either String Space -> Bool
forall a b. Either a b -> Bool
isLeft [Either String Space]
tcs)
                            else String -> Either (String, [Either String Space]) String
forall a. a -> Either (String, [Either String Space]) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either (String, [Either String Space]) String)
-> String -> Either (String, [Either String 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 String Space])]
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, [Either String Space]) String -> IO ())
-> [Either (String, [Either String Space]) String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (((String, [Either String Space]) -> IO ())
-> (String -> IO ())
-> Either (String, [Either String Space]) String
-> IO ()
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
            (\(String
tMsg, [Either String Space]
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 String Space] -> [String]
forall a b. [Either a b] -> [a]
lefts [Either String Space]
tcs)
            )
            String -> IO ()
putStrLn
      ) [Either (String, [Either String 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"