    -- |
    -- 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
      ) 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)

    -- | 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 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)