ddci-core-0.2.0.1: DDCI/Core/Command/Check.hs
module DDCI.Core.Command.Check
( cmdShowKind
, cmdTypeEquiv
, cmdShowWType
, cmdShowType
, cmdExpRecon
, ShowTypeMode(..)
, cmdParseCheckExp)
where
import DDCI.Core.State
import DDCI.Core.IO
import DDC.Core.Eval.Env
import DDC.Core.Eval.Name
import DDC.Core.Eval.Check
import DDC.Type.Equiv
import DDC.Core.Exp
import DDC.Core.Check
import DDC.Core.Pretty
import DDC.Core.Parser
import DDC.Core.Parser.Tokens
import DDC.Core.Collect
import DDC.Core.Transform.SpreadX
import DDC.Type.Transform.SpreadT
import qualified DDC.Type.Parser as T
import qualified DDC.Type.Check as T
import qualified DDC.Base.Parser as BP
import qualified Data.Set as Set
-- kind ------------------------------------------------------------------------
-- | Show the kind of a type.
cmdShowKind :: State -> Int -> String -> IO ()
cmdShowKind state lineStart ss
= goParse (lexString lineStart ss)
where
goParse toks
= case BP.runTokenParser describeTok "<interactive>" T.pType toks of
Left err -> putStrLn $ renderIndent $ text "parse error " <> ppr err
Right t -> goCheck t
goCheck t
= case T.checkType primKindEnv (spreadT primKindEnv t) of
Left err -> putStrLn $ renderIndent $ ppr err
Right k -> outDocLn state $ ppr t <+> text "::" <+> ppr k
-- tequiv ---------------------------------------------------------------------
-- | Check if two types are equivlant.
cmdTypeEquiv :: State -> Int -> String -> IO ()
cmdTypeEquiv _state lineStart ss
= goParse (lexString lineStart ss)
where
goParse toks
= case BP.runTokenParser describeTok "<interactive>"
(do t1 <- T.pTypeAtom
t2 <- T.pTypeAtom
return (t1, t2))
toks
of Left err -> putStrLn $ renderIndent $ text "parse error " <> ppr err
Right tt -> goEquiv tt
goEquiv (t1, t2)
= do b1 <- checkT t1
b2 <- checkT t2
if b1 && b2
then putStrLn $ show $ equivT t1 t2
else return ()
checkT t
= case T.checkType primKindEnv (spreadT primKindEnv t) of
Left err
-> do putStrLn $ renderIndent $ ppr err
return False
Right{}
-> return True
-- wtype ----------------------------------------------------------------------
-- | Show the type of a witness.
cmdShowWType :: State -> Int -> String -> IO ()
cmdShowWType state lineStart ss
= cmdParseCheckWitness state lineStart ss >>= goResult
where
goResult Nothing
= return ()
goResult (Just (w, t))
= putStrLn $ renderIndent $ ppr w <> text " :: " <> ppr t
-- | Parse the given witness, and return it along with its type.
--
-- If the expression had a parse error, undefined vars, or type error
-- then print this to the console.
cmdParseCheckWitness
:: State
-> Int -- Starting line number for lexer.
-> String
-> IO (Maybe (Witness Name, Type Name))
cmdParseCheckWitness state lineStart str
= goParse (lexString lineStart str)
where
-- Lex and parse the string.
goParse toks
= case BP.runTokenParser describeTok "<interactive>" pWitness toks of
Left err
-> do putStrLn $ renderIndent $ text "parse error " <> ppr err
return Nothing
Right x -> goCheck x
-- Spread type annotations into binders,
-- check for undefined variables,
-- and check its type.
goCheck x
= let fvs = freeX primTypeEnv x -- TODO: also check for free type vars
x' = spreadX primKindEnv primTypeEnv x
in if Set.null fvs
then goResult x' (checkWitness primKindEnv primTypeEnv x')
else do
outDocLn state $ text "Undefined variables: " <> ppr fvs
return Nothing
-- Expression had a type error.
goResult _ (Left err)
= do putStrLn $ renderIndent $ ppr err
return Nothing
goResult x (Right t)
= return $ Just (x, t)
-- check / type / effect / closure --------------------------------------------
-- | What components of the checked type to display.
data ShowTypeMode
= ShowTypeAll
| ShowTypeValue
| ShowTypeEffect
| ShowTypeClosure
deriving (Eq, Show)
-- | Show the type of an expression.
cmdShowType :: State -> ShowTypeMode -> Int -> String -> IO ()
cmdShowType state mode lineStart ss
= cmdParseCheckExp state lineStart ss >>= goResult
where
goResult Nothing
= return ()
goResult (Just (x, t, eff, clo))
= case mode of
ShowTypeAll
-> do outDocLn state $ ppr x
outDocLn state $ text ":*: " <+> ppr t
outDocLn state $ text ":!:" <+> ppr eff
outDocLn state $ text ":$:" <+> ppr clo
ShowTypeValue
-> outDocLn state $ ppr x <+> text "::" <+> ppr t
ShowTypeEffect
-> outDocLn state $ ppr x <+> text ":!" <+> ppr eff
ShowTypeClosure
-> outDocLn state $ ppr x <+> text ":$" <+> ppr clo
-- | Check expression and reconstruct type annotations on binders.
cmdExpRecon :: State -> Int -> String -> IO ()
cmdExpRecon state lineStart ss
= cmdParseCheckExp state lineStart ss >>= goResult
where
goResult Nothing
= return ()
goResult (Just (x, _, _, _))
= outDocLn state $ ppr x
-- | Parse the given core expression,
-- and return it, along with its type, effect and closure.
--
-- If the expression had a parse error, undefined vars, or type error
-- then print this to the console.
cmdParseCheckExp
:: State
-> Int -- Starting line number.
-> String
-> IO (Maybe ( Exp () Name
, Type Name, Effect Name, Closure Name))
cmdParseCheckExp state lineStart str
= goParse (lexString lineStart str)
where
-- Lex and parse the string.
goParse toks
= case BP.runTokenParser describeTok "<interactive>" pExp toks of
Left err
-> do putStrLn $ renderIndent $ ppr err
return Nothing
Right x -> goCheckVars x
-- Check for undefined variables, and spread type annotations into
-- bound occurrences of variables.
goCheckVars x
= let fvs = freeX primTypeEnv x -- TODO also check for free type vars
x' = spreadX primKindEnv primTypeEnv x
in if Set.null fvs
then goCheckType x'
else do outDocLn state $ text "Undefined variables: " <> ppr fvs
return Nothing
-- Check the type of the expression.
goCheckType x
= case checkExp primDataDefs primKindEnv primTypeEnv x of
Left err
-> do putStrLn $ renderIndent $ ppr err
return Nothing
Right (x', t, eff, clo)
-> goCheckCaps x' t eff clo
-- Check the initial capabilities in the expression.
goCheckCaps x t eff clo
= case checkCapsX x of
Just err
-> do putStrLn $ renderIndent $ ppr err
return Nothing
Nothing
-> return $ Just (x, t, eff, clo)