1-- |
2-- Module      :  Cryptol.TypeCheck
3-- Copyright   :  (c) 2013-2016 Galois, Inc.
4-- License     :  BSD3
5-- Maintainer  :  cryptol@galois.com
6-- Stability   :  provisional
7-- Portability :  portable
8{-# LANGUAGE PatternGuards, OverloadedStrings #-}
9
10module Cryptol.TypeCheck
11  ( tcModule
12  , tcModuleInst
13  , tcExpr
14  , tcDecls
15  , InferInput(..)
16  , InferOutput(..)
17  , SolverConfig(..)
18  , NameSeeds
19  , nameSeeds
20  , Error(..)
21  , Warning(..)
22  , ppWarning
23  , ppError
24  , WithNames(..)
25  , NameMap
26  , ppNamedWarning
27  , ppNamedError
28  ) where
29
30import           Cryptol.ModuleSystem.Name
31                    (liftSupply,mkDeclared,NameSource(..))
32import qualified Cryptol.Parser.AST as P
33import           Cryptol.Parser.Position(Range,emptyRange)
34import           Cryptol.TypeCheck.AST
35import           Cryptol.TypeCheck.Depends (FromDecl)
36import           Cryptol.TypeCheck.Error
37import           Cryptol.TypeCheck.Monad
38                   ( runInferM
39                   , InferInput(..)
40                   , InferOutput(..)
41                   , NameSeeds
42                   , nameSeeds
43                   , lookupVar
44                   )
45import           Cryptol.TypeCheck.Infer (inferModule, inferBinds, inferDs)
46import           Cryptol.TypeCheck.InferTypes(VarType(..), SolverConfig(..))
47import           Cryptol.TypeCheck.Solve(proveModuleTopLevel)
48import           Cryptol.TypeCheck.CheckModuleInstance(checkModuleInstance)
49import           Cryptol.TypeCheck.Monad(withParamType,withParameterConstraints)
50import           Cryptol.TypeCheck.PP(WithNames(..),NameMap)
51import           Cryptol.Utils.Ident (exprModName,packIdent)
52import           Cryptol.Utils.PP
53import           Cryptol.Utils.Panic(panic)
54
55
56
57tcModule :: P.Module Name -> InferInput -> IO (InferOutput Module)
58tcModule m inp = runInferM inp (inferModule m)
59
60-- | Check a module instantiation, assuming that the functor has already
61-- been checked.
62tcModuleInst :: Module                  {- ^ functor -} ->
63                P.Module Name           {- params -} ->
64                InferInput              {- ^ TC settings -} ->
65                IO (InferOutput Module) {- ^ new version of instance -}
66tcModuleInst func m inp = runInferM inp
67                        $ do x <- inferModule m
68                             flip (foldr withParamType) (mParamTypes x) $
69                               withParameterConstraints (mParamConstraints x) $
70                               do y <- checkModuleInstance func x
71                                  proveModuleTopLevel
72                                  pure y
73
74tcExpr :: P.Expr Name -> InferInput -> IO (InferOutput (Expr,Schema))
75tcExpr e0 inp = runInferM inp
76                $ do x <- go emptyRange e0
77                     proveModuleTopLevel
78                     return x
79
80  where
81  go loc expr =
82    case expr of
83      P.ELocated e loc' ->
84        do (te, sch) <- go loc' e
85           pure $! if inpCallStacks inp then (ELocated loc' te, sch) else (te,sch)
86      P.EVar x  ->
87        do res <- lookupVar x
88           case res of
89             ExtVar s    -> return (EVar x, s)
90             CurSCC e' t -> panic "Cryptol.TypeCheck.tcExpr"
91                             [ "CurSCC outside binder checking:"
92                             , show e'
93                             , show t
94                             ]
95      _ -> do fresh <- liftSupply (mkDeclared exprModName SystemName
96                                      (packIdent "(expression)") Nothing loc)
97              res   <- inferBinds True False
98                [ P.Bind
99                    { P.bName      = P.Located { P.srcRange = loc, P.thing = fresh }
100                    , P.bParams    = []
101                    , P.bDef       = P.Located (inpRange inp) (P.DExpr expr)
102                    , P.bPragmas   = []
103                    , P.bSignature = Nothing
104                    , P.bMono      = False
105                    , P.bInfix     = False
106                    , P.bFixity    = Nothing
107                    , P.bDoc       = Nothing
108                    } ]
109
110              case res of
111                [d] | DExpr e <- dDefinition d -> return (e, dSignature d)
112                    | otherwise                ->
113                       panic "Cryptol.TypeCheck.tcExpr"
114                          [ "Expected an expression in definition"
115                          , show d ]
116
117                _   -> panic "Cryptol.TypeCheck.tcExpr"
118                          ( "Multiple declarations when check expression:"
119                          : map show res
120                          )
121
122tcDecls :: FromDecl d => [d] -> InferInput -> IO (InferOutput [DeclGroup])
123tcDecls ds inp = runInferM inp $ inferDs ds $ \dgs -> do
124                   proveModuleTopLevel
125                   return dgs
126
127ppWarning :: (Range,Warning) -> Doc
128ppWarning (r,w) = text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp w)
129
130ppError :: (Range,Error) -> Doc
131ppError (r,w) = text "[error] at" <+> pp r <.> colon $$ nest 2 (pp w)
132
133
134ppNamedWarning :: NameMap -> (Range,Warning) -> Doc
135ppNamedWarning nm (r,w) =
136  text "[warning] at" <+> pp r <.> colon $$ nest 2 (pp (WithNames w nm))
137
138ppNamedError :: NameMap -> (Range,Error) -> Doc
139ppNamedError nm (r,e) =
140  text "[error] at" <+> pp r <.> colon $$ nest 2 (pp (WithNames e nm))
141
142
143