1-- |
2-- Module      :  Cryptol.ModuleSystem
3-- Copyright   :  (c) 2013-2016 Galois, Inc.
4-- License     :  BSD3
5-- Maintainer  :  cryptol@galois.com
6-- Stability   :  provisional
7-- Portability :  portable
8
9{-# LANGUAGE FlexibleContexts #-}
10
11module Cryptol.ModuleSystem (
12    -- * Module System
13    ModuleEnv(..), initialModuleEnv
14  , DynamicEnv(..)
15  , ModuleError(..), ModuleWarning(..)
16  , ModuleCmd, ModuleRes
17  , ModuleInput(..)
18  , findModule
19  , loadModuleByPath
20  , loadModuleByName
21  , checkExpr
22  , evalExpr
23  , checkDecls
24  , evalDecls
25  , noPat
26  , focusedEnv
27  , getPrimMap
28  , renameVar
29  , renameType
30
31    -- * Interfaces
32  , Iface(..), IfaceParams(..), IfaceDecls(..), genIface
33  , IfaceTySyn, IfaceDecl(..)
34  ) where
35
36import qualified Cryptol.Eval.Concrete as Concrete
37import           Cryptol.ModuleSystem.Env
38import           Cryptol.ModuleSystem.Interface
39import           Cryptol.ModuleSystem.Monad
40import           Cryptol.ModuleSystem.Name (Name,PrimMap)
41import qualified Cryptol.ModuleSystem.Renamer as R
42import qualified Cryptol.ModuleSystem.Base as Base
43import qualified Cryptol.Parser.AST        as P
44import           Cryptol.Parser.Name (PName)
45import           Cryptol.Parser.NoPat (RemovePatterns)
46import qualified Cryptol.TypeCheck.AST     as T
47import qualified Cryptol.Utils.Ident as M
48
49-- Public Interface ------------------------------------------------------------
50
51type ModuleCmd a = ModuleInput IO -> IO (ModuleRes a)
52
53type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning])
54
55getPrimMap :: ModuleCmd PrimMap
56getPrimMap me = runModuleM me Base.getPrimMap
57
58-- | Find the file associated with a module name in the module search path.
59findModule :: P.ModName -> ModuleCmd ModulePath
60findModule n env = runModuleM env (Base.findModule n)
61
62-- | Load the module contained in the given file.
63loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)
64loadModuleByPath path minp =
65  runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do
66    unloadModule ((InFile path ==) . lmFilePath)
67    m <- Base.loadModuleByPath path
68    setFocusedModule (T.mName m)
69    return (InFile path,m)
70
71-- | Load the given parsed module.
72loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
73loadModuleByName n minp =
74  runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do
75    unloadModule ((n ==) . lmName)
76    (path,m') <- Base.loadModuleFrom False (FromModule n)
77    setFocusedModule (T.mName m')
78    return (path,m')
79
80-- Extended Environments -------------------------------------------------------
81
82-- These functions are particularly useful for interactive modes, as
83-- they allow for expressions to be evaluated in an environment that
84-- can extend dynamically outside of the context of a module.
85
86-- | Check the type of an expression.  Give back the renamed expression, the
87-- core expression, and its type schema.
88checkExpr :: P.Expr PName -> ModuleCmd (P.Expr Name,T.Expr,T.Schema)
89checkExpr e env = runModuleM env (interactive (Base.checkExpr e))
90
91-- | Evaluate an expression.
92evalExpr :: T.Expr -> ModuleCmd Concrete.Value
93evalExpr e env = runModuleM env (interactive (Base.evalExpr e))
94
95-- | Typecheck top-level declarations.
96checkDecls :: [P.TopDecl PName] -> ModuleCmd (R.NamingEnv,[T.DeclGroup])
97checkDecls ds env = runModuleM env
98                  $ interactive
99                  $ Base.checkDecls ds
100
101-- | Evaluate declarations and add them to the extended environment.
102evalDecls :: [T.DeclGroup] -> ModuleCmd ()
103evalDecls dgs env = runModuleM env (interactive (Base.evalDecls dgs))
104
105noPat :: RemovePatterns a => a -> ModuleCmd a
106noPat a env = runModuleM env (interactive (Base.noPat a))
107
108renameVar :: R.NamingEnv -> PName -> ModuleCmd Name
109renameVar names n env = runModuleM env $ interactive $
110  Base.rename M.interactiveName names (R.renameVar n)
111
112renameType :: R.NamingEnv -> PName -> ModuleCmd Name
113renameType names n env = runModuleM env $ interactive $
114  Base.rename M.interactiveName names (R.renameType n)
115