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