    -- |
    -- 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 :: [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
                        , 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))