-- |
-- 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
  , tcModuleInst
  , tcExpr
  , tcDecls
  , InferInput(..)
  , InferOutput(..)
  , SolverConfig(..)
  , NameSeeds
  , nameSeeds
  , Error(..)
  , Warning(..)
  , ppWarning
  , ppError
  , WithNames(..)
  , NameMap
  , ppNamedWarning
  , ppNamedError
  ) 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.TypeCheck.PP(WithNames(..),NameMap)
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 Module Name
m 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)

-- | Check a module instantiation, assuming that the functor has already
-- been checked.
tcModuleInst :: Module                  {- ^ functor -} ->
                P.Module Name           {- params -} ->
                InferInput              {- ^ TC settings -} ->
                IO (InferOutput Module) {- ^ new version of instance -}
tcModuleInst :: Module -> Module Name -> InferInput -> IO (InferOutput Module)
tcModuleInst Module
func Module Name
m 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
                             (InferM Module -> Map Name ModTParam -> InferM Module)
-> Map Name ModTParam -> InferM Module -> InferM Module
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((ModTParam -> InferM Module -> InferM Module)
-> InferM Module -> Map Name ModTParam -> InferM Module
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ModTParam -> InferM Module -> InferM Module
forall a. ModTParam -> InferM a -> InferM a
withParamType) (Module -> Map Name ModTParam
mParamTypes Module
x) (InferM Module -> InferM Module) -> InferM Module -> InferM Module
forall a b. (a -> b) -> a -> b
$
                               [Located Prop] -> InferM Module -> InferM Module
forall a. [Located Prop] -> InferM a -> InferM a
withParameterConstraints (Module -> [Located Prop]
mParamConstraints Module
x) (InferM Module -> InferM Module) -> InferM Module -> InferM Module
forall a b. (a -> b) -> a -> b
$
                               do Module
y <- Module -> Module -> InferM Module
checkModuleInstance Module
func Module
x
                                  InferM ()
proveModuleTopLevel
                                  Module -> InferM Module
forall (f :: * -> *) a. Applicative f => a -> f a
pure Module
y

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 (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 (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 (m :: * -> *) a. Monad m => a -> m a
return (Name -> Expr
EVar Name
x, Schema
s)
             CurSCC Expr
e' Prop
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'
                             , Prop -> String
forall a. Show a => a -> String
show Prop
t
                             ]
      Expr Name
_ -> 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 String
"(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 Text
-> Bind name
P.Bind
                    { bName :: Located Name
P.bName      = Located :: 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 Text
P.bDoc       = Maybe Text
forall a. Maybe a
Nothing
                    } ]

              case [Decl]
res of
                [Decl
d] | DExpr 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 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 :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
tcDecls :: [d] -> InferInput -> IO (InferOutput [DeclGroup])
tcDecls [d]
ds 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
$ \[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 (Range
r,Warning
w) = 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
$$ Int -> Doc -> Doc
nest Int
2 (Warning -> Doc
forall a. PP a => a -> Doc
pp Warning
w)

ppError :: (Range,Error) -> Doc
ppError :: (Range, Error) -> Doc
ppError (Range
r,Error
w) = 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
$$ Int -> Doc -> Doc
nest Int
2 (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) =
  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
$$ Int -> Doc -> Doc
nest Int
2 (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) =
  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
$$ Int -> Doc -> Doc
nest Int
2 (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))