-- |
-- Module      :  Cryptol.TypeCheck
-- Copyright   :  (c) 2013-2016 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable
{-# 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.Monad(withParamType,withParameterConstraints)
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 = InferInput -> InferM TCTopEntity -> IO (InferOutput TCTopEntity)
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 = 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 a. a -> InferM a
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
           (Expr, Schema) -> InferM (Expr, Schema)
forall a. a -> InferM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Expr, Schema) -> InferM (Expr, Schema))
-> (Expr, Schema) -> InferM (Expr, Schema)
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    -> (Expr, Schema) -> InferM (Expr, Schema)
forall a. a -> InferM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
x, Schema
s)
             CurSCC Expr
e' Type
t -> String -> [String] -> InferM (Expr, Schema)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.tcExpr"
                             [ String
"CurSCC outside binder checking:"
                             , Expr -> String
forall a. Show a => a -> String
show Expr
e'
                             , Type -> String
forall a. Show a => a -> String
show Type
t
                             ]
      Expr Name
_ -> do Name
fresh <- (Supply -> (Name, Supply)) -> InferM Name
forall a. (Supply -> (a, Supply)) -> InferM a
forall (m :: * -> *) a. FreshM m => (Supply -> (a, Supply)) -> m a
liftSupply ((Supply -> (Name, Supply)) -> InferM Name)
-> (Supply -> (Name, Supply)) -> InferM Name
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)") Maybe Fixity
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 :: BindParams Name
P.bParams    = BindParams Name
forall name. BindParams name
P.noParams
                    , 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.exprDef 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 (Located Text)
P.bDoc       = Maybe (Located Text)
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 -> (Expr, Schema) -> InferM (Expr, Schema)
forall a. a -> InferM a
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 String
"Cryptol.TypeCheck.tcExpr"
                          [ String
"Expected an expression in definition"
                          , Decl -> String
forall a. Show a => a -> String
show Decl
d ]

                [Decl]
_   -> String -> [String] -> InferM (Expr, Schema)
forall a. HasCallStack => String -> [String] -> a
panic String
"Cryptol.TypeCheck.tcExpr"
                          ( String
"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 :: [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 = InferInput
-> InferM ([DeclGroup], Map Name TySyn)
-> IO (InferOutput ([DeclGroup], Map Name TySyn))
forall a. TVars a => InferInput -> InferM a -> IO (InferOutput a)
runInferM InferInput
inp (InferM ([DeclGroup], Map Name TySyn)
 -> IO (InferOutput ([DeclGroup], Map Name TySyn)))
-> InferM ([DeclGroup], Map Name TySyn)
-> IO (InferOutput ([DeclGroup], Map Name TySyn))
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
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ Warning -> 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
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ Error -> 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
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ WithNames Warning -> Doc
forall a. PP a => a -> Doc
pp (Warning -> NameMap -> WithNames Warning
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
<+> Range -> Doc
forall a. PP a => a -> Doc
pp Range
r Doc -> Doc -> Doc
<.> Doc
colon Doc -> Doc -> Doc
$$ WithNames Error -> Doc
forall a. PP a => a -> Doc
pp (Error -> NameMap -> WithNames Error
forall a. a -> NameMap -> WithNames a
WithNames Error
e NameMap
nm))