{-# LANGUAGE PatternGuards, OverloadedStrings #-}
module Cryptol.TypeCheck
( tcModule
, tcModuleInst
, tcExpr
, tcDecls
, InferInput(..)
, InferOutput(..)
, SolverConfig(..)
, NameSeeds
, nameSeeds
, Error(..)
, Warning(..)
, ppWarning
, ppError
) where
import Cryptol.ModuleSystem.Name
(liftSupply,mkDeclared,NameSource(..))
import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Position(Range,emptyRange)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.Depends (FromDecl)
import Cryptol.TypeCheck.Error
import Cryptol.TypeCheck.Monad
( runInferM
, InferInput(..)
, InferOutput(..)
, NameSeeds
, nameSeeds
, lookupVar
)
import Cryptol.TypeCheck.Infer (inferModule, inferBinds, inferDs)
import Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..))
import Cryptol.TypeCheck.Solve(proveModuleTopLevel)
import Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance)
import Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
import Cryptol.Utils.Ident (exprModName,packIdent)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic(panic)
tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
tcModule :: Module Name -> InferInput -> IO (InferOutput Module)
tcModule m :: Module Name
m inp :: InferInput
inp = InferInput -> InferM Module -> IO (InferOutput Module)
forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp (Module Name -> InferM Module
inferModule Module Name
m)
tcModuleInst :: Module ->
P.Module Name ->
InferInput ->
IO (InferOutput Module)
tcModuleInst :: Module -> Module Name -> InferInput -> IO (InferOutput Module)
tcModuleInst func :: Module
func m :: Module Name
m inp :: InferInput
inp = InferInput -> InferM Module -> IO (InferOutput Module)
forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp
(InferM Module -> IO (InferOutput Module))
-> InferM Module -> IO (InferOutput Module)
forall a b. (a -> b) -> a -> b
$ do Module
x <- Module Name -> InferM Module
inferModule Module Name
m
Module
y <- Module -> Module -> InferM Module
checkModuleInstance Module
func Module
x
(InferM () -> Map Name ModTParam -> InferM ())
-> Map Name ModTParam -> InferM () -> InferM ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((ModTParam -> InferM () -> InferM ())
-> InferM () -> Map Name ModTParam -> InferM ()
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ModTParam -> InferM () -> InferM ()
forall a. ModTParam -> InferM a -> InferM a
withParamType) (Module -> Map Name ModTParam
mParamTypes Module
x) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
[Located Prop] -> InferM () -> InferM ()
forall a. [Located Prop] -> InferM a -> InferM a
withParameterConstraints (Module -> [Located Prop]
mParamConstraints Module
x) (InferM () -> InferM ()) -> InferM () -> InferM ()
forall a b. (a -> b) -> a -> b
$
InferM ()
proveModuleTopLevel
Module -> InferM Module
forall (m :: * -> *) a. Monad m => a -> m a
return Module
y
tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))
tcExpr :: Expr Name -> InferInput -> IO (InferOutput (Expr, Schema))
tcExpr e0 :: Expr Name
e0 inp :: InferInput
inp = InferInput
-> InferM (Expr, Schema) -> IO (InferOutput (Expr, Schema))
forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp
(InferM (Expr, Schema) -> IO (InferOutput (Expr, Schema)))
-> InferM (Expr, Schema) -> IO (InferOutput (Expr, Schema))
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
(Expr, Schema) -> InferM (Expr, Schema)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr, Schema)
x
where
go :: Range -> Expr Name -> InferM (Expr, Schema)
go loc :: Range
loc expr :: Expr Name
expr =
case Expr Name
expr of
P.ELocated e :: Expr Name
e loc' :: Range
loc' -> Range -> Expr Name -> InferM (Expr, Schema)
go Range
loc' Expr Name
e
P.EVar x :: Name
x ->
do VarType
res <- Name -> InferM VarType
lookupVar Name
x
case VarType
res of
ExtVar s :: Schema
s -> (Expr, Schema) -> InferM (Expr, Schema)
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
x, Schema
s)
CurSCC e' :: Expr
e' t :: Prop
t -> String -> [String] -> InferM (Expr, Schema)
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.TypeCheck.tcExpr"
[ "CurSCC outside binder checking:"
, Expr -> String
forall a. Show a => a -> String
show Expr
e'
, Prop -> String
forall a. Show a => a -> String
show Prop
t
]
_ -> do Name
fresh <- (Supply -> (Name, Supply)) -> InferM Name
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply (ModName
-> NameSource
-> Ident
-> Maybe Fixity
-> Range
-> Supply
-> (Name, Supply)
mkDeclared ModName
exprModName NameSource
SystemName
(String -> Ident
packIdent "(expression)") Maybe Fixity
forall a. Maybe a
Nothing Range
loc)
[Decl]
res <- Bool -> Bool -> [Bind Name] -> InferM [Decl]
inferBinds Bool
True Bool
False
[ Bind :: forall name.
Located name
-> [Pattern name]
-> Located (BindDef name)
-> Maybe (Schema name)
-> Bool
-> Maybe Fixity
-> [Pragma]
-> Bool
-> Maybe String
-> Bind name
P.Bind
{ bName :: Located Name
P.bName = $WLocated :: forall a. Range -> a -> Located a
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 = Range -> BindDef Name -> Located (BindDef Name)
forall a. Range -> a -> Located a
P.Located (InferInput -> Range
inpRange InferInput
inp) (Expr Name -> BindDef Name
forall name. Expr name -> BindDef name
P.DExpr Expr Name
expr)
, bPragmas :: [Pragma]
P.bPragmas = []
, bSignature :: Maybe (Schema Name)
P.bSignature = Maybe (Schema Name)
forall a. Maybe a
Nothing
, bMono :: Bool
P.bMono = Bool
False
, bInfix :: Bool
P.bInfix = Bool
False
, bFixity :: Maybe Fixity
P.bFixity = Maybe Fixity
forall a. Maybe a
Nothing
, bDoc :: Maybe String
P.bDoc = Maybe String
forall a. Maybe a
Nothing
} ]
case [Decl]
res of
[d :: Decl
d] | DExpr e :: Expr
e <- Decl -> DeclDef
dDefinition Decl
d -> (Expr, Schema) -> InferM (Expr, Schema)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Decl -> Schema
dSignature Decl
d)
| Bool
otherwise ->
String -> [String] -> InferM (Expr, Schema)
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.TypeCheck.tcExpr"
[ "Expected an expression in definition"
, Decl -> String
forall a. Show a => a -> String
show Decl
d ]
_ -> String -> [String] -> InferM (Expr, Schema)
forall a. HasCallStack => String -> [String] -> a
panic "Cryptol.TypeCheck.tcExpr"
( "Multiple declarations when check expression:"
String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Decl -> String) -> [Decl] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> String
forall a. Show a => a -> String
show [Decl]
res
)
tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
tcDecls :: [d] -> InferInput -> IO (InferOutput [DeclGroup])
tcDecls ds :: [d]
ds inp :: InferInput
inp = InferInput -> InferM [DeclGroup] -> IO (InferOutput [DeclGroup])
forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp (InferM [DeclGroup] -> IO (InferOutput [DeclGroup]))
-> InferM [DeclGroup] -> IO (InferOutput [DeclGroup])
forall a b. (a -> b) -> a -> b
$ [d] -> ([DeclGroup] -> InferM [DeclGroup]) -> InferM [DeclGroup]
forall d a.
FromDecl d =>
[d] -> ([DeclGroup] -> InferM a) -> InferM a
inferDs [d]
ds (([DeclGroup] -> InferM [DeclGroup]) -> InferM [DeclGroup])
-> ([DeclGroup] -> InferM [DeclGroup]) -> InferM [DeclGroup]
forall a b. (a -> b) -> a -> b
$ \dgs :: [DeclGroup]
dgs -> do
InferM ()
proveModuleTopLevel
[DeclGroup] -> InferM [DeclGroup]
forall (m :: * -> *) a. Monad m => a -> m a
return [DeclGroup]
dgs
ppWarning :: (Range,Warning) -> Doc
ppWarning :: (Range, Warning) -> Doc
ppWarning (r :: Range
r,w :: Warning
w) = String -> Doc
text "[warning] at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (Warning -> Doc
forall a. PP a => a -> Doc
pp Warning
w)
ppError :: (Range,Error) -> Doc
ppError :: (Range, Error) -> Doc
ppError (r :: Range
r,w :: Error
w) = String -> Doc
text "[error] at" Doc -> Doc -> Doc
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ Int -> Doc -> Doc
nest 2 (Error -> Doc
forall a. PP a => a -> Doc
pp Error
w)