{-# LANGUAGE PatternGuards, OverloadedStrings #-}
module Cryptol.TypeCheck
( tcModule
, tcExpr
, tcDecls
, InferInput(..)
, InferOutput(..)
, SolverConfig(..)
, defaultSolverConfig
, NameSeeds
, nameSeeds
, Error(..)
, Warning(..)
, ppWarning
, ppError
, WithNames(..)
, NameMap
, ppNamedWarning
, ppNamedError
) where
import Data.Map(Map)
import Cryptol.ModuleSystem.Name
(liftSupply,mkDeclared,NameSource(..),ModPath(..))
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Position(Range,emptyRange)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Monad
( runInferM
, InferInput(..)
, InferOutput(..)
, NameSeeds
, nameSeeds
, lookupVar
, newLocalScope, endLocalScope
)
import Cryptol.TypeCheck.Infer (inferTopModule, inferBinds, checkTopDecls)
import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..), defaultSolverConfig)
import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
import Cryptol.TypeCheck.PP(WithNames(..),NameMap)
import Cryptol.Utils.Ident (exprModName,packIdent,Namespace(..))
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
tcModule :: P.Module Name -> InferInput -> IO (InferOutput TCTopEntity)
tcModule :: Module Name -> InferInput -> IO (InferOutput TCTopEntity)
tcModule Module Name
m InferInput
inp = forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp (Module Name -> InferM TCTopEntity
inferTopModule Module Name
m)
tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))
tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema))
tcExpr Expr Name
e0 InferInput
inp = forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp
forall a b. (a -> b) -> a -> b
$ do (Expr, Schema)
x <- Range -> Expr Name -> InferM (Expr, Schema)
go Range
emptyRange Expr Name
e0
InferM ()
proveModuleTopLevel
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr, Schema)
x
where
go :: Range -> Expr Name -> InferM (Expr, Schema)
go Range
loc Expr Name
expr =
case Expr Name
expr of
P.ELocated Expr Name
e Range
loc' ->
do (Expr
te, Schema
sch) <- Range -> Expr Name -> InferM (Expr, Schema)
go Range
loc' Expr Name
e
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$! if InferInput -> Bool
inpCallStacks InferInput
inp then (Range -> Expr -> Expr
ELocated Range
loc' Expr
te, Schema
sch) else (Expr
te,Schema
sch)
P.EVar Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
case VarType
res of
ExtVar Schema
s -> forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
x, Schema
s)
CurSCC Expr
e' Type
t -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.tcExpr"
[ String
"CurSCC outside binder checking:"
, forall a. Show a => a -> String
show Expr
e'
, forall a. Show a => a -> String
show Type
t
]
Expr Name
_ -> do Name
fresh <- forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply forall a b. (a -> b) -> a -> b
$
Namespace
-> ModPath
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared Namespace
NSValue (ModName -> ModPath
TopModule ModName
exprModName) NameSource
SystemName
(String -> Ident
packIdent String
"(expression)") forall a. Maybe a
Nothing Range
loc
[Decl]
res <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
True Bool
False
[ P.Bind
{ bName :: Located Name
P.bName = P.Located { srcRange :: Range
P.srcRange = Range
loc, thing :: Name
P.thing = Name
fresh }
, bParams :: [Pattern Name]
P.bParams = []
, bDef :: Located (BindDef Name)
P.bDef = forall a. Range -> a -> Located a
P.Located (InferInput -> Range
inpRange InferInput
inp) (forall name. Expr name -> BindDef name
P.DExpr Expr Name
expr)
, bPragmas :: [Pragma]
P.bPragmas = []
, bSignature :: Maybe (Schema Name)
P.bSignature = forall a. Maybe a
Nothing
, bMono :: Bool
P.bMono = Bool
False
, bInfix :: Bool
P.bInfix = Bool
False
, bFixity :: Maybe Fixity
P.bFixity = forall a. Maybe a
Nothing
, bDoc :: Maybe Text
P.bDoc = forall a. Maybe a
Nothing
, bExport :: ExportType
P.bExport = ExportType
Public
} ]
case [Decl]
res of
[Decl
d] | DExpr Expr
e <- Decl -> DeclDef
dDefinition Decl
d -> forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Decl -> Schema
dSignature Decl
d)
| Bool
otherwise ->
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.tcExpr"
[ String
"Expected an expression in definition"
, forall a. Show a => a -> String
show Decl
d ]
[Decl]
_ -> forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.tcExpr"
( String
"Multiple declarations when check expression:"
forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [Decl]
res
)
tcDecls :: [P.TopDecl Name] -> InferInput -> IO (InferOutput ([DeclGroup],Map Name TySyn))
tcDecls :: [TopDecl Name]
-> InferInput -> IO (InferOutput ([DeclGroup], Map Name TySyn))
tcDecls [TopDecl Name]
ds InferInput
inp = forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp forall a b. (a -> b) -> a -> b
$
do InferM ()
newLocalScope
[TopDecl Name] -> InferM ()
checkTopDecls [TopDecl Name]
ds
InferM ()
proveModuleTopLevel
InferM ([DeclGroup], Map Name TySyn)
endLocalScope
ppWarning :: (Range,Warning) -> Doc
ppWarning :: (Range, Warning) -> Doc
ppWarning (Range
r,Warning
w) = Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
"[warning] at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ forall a. PP a => a -> Doc
pp Warning
w)
ppError :: (Range,Error) -> Doc
ppError :: (Range, Error) -> Doc
ppError (Range
r,Error
w) = Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
"[error] at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ forall a. PP a => a -> Doc
pp Error
w)
ppNamedWarning :: NameMap -> (Range,Warning) -> Doc
ppNamedWarning :: NameMap -> (Range, Warning) -> Doc
ppNamedWarning NameMap
nm (Range
r,Warning
w) =
Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
"[warning] at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ forall a. PP a => a -> Doc
pp (forall a. a -> NameMap -> WithNames a
WithNames Warning
w NameMap
nm))
ppNamedError :: NameMap -> (Range,Error) -> Doc
ppNamedError :: NameMap -> (Range, Error) -> Doc
ppNamedError NameMap
nm (Range
r,Error
e) =
Int -> Doc -> Doc
nest Int
2 (String -> Doc
text String
"[error] at" Doc -> Doc -> Doc
<+> forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ forall a. PP a => a -> Doc
pp (forall a. a -> NameMap -> WithNames a
WithNames Error
e NameMap
nm))