Copyright | (c) 2013-2016 Galois, Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | None |
Language | Haskell98 |
- type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl))
- type SpecT m a = StateT SpecCache (ModuleT m) a
- type SpecM a = SpecT IO a
- runSpecT :: SpecCache -> SpecT m a -> ModuleT m (a, SpecCache)
- liftSpecT :: Monad m => ModuleT m a -> SpecT m a
- getSpecCache :: Monad m => SpecT m SpecCache
- setSpecCache :: Monad m => SpecCache -> SpecT m ()
- modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m ()
- modify :: StateM m s => (s -> s) -> m ()
- specialize :: Expr -> ModuleCmd Expr
- specializeExpr :: Expr -> SpecM Expr
- specializeMatch :: Match -> SpecM Match
- withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name))
- specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr
- specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name))
- specializeConst :: Expr -> SpecM Expr
- destEProofApps :: Expr -> (Expr, Int)
- destETApps :: Expr -> (Expr, [Type])
- destEProofAbs :: Expr -> ([Prop], Expr)
- destETAbs :: Expr -> ([TParam], Expr)
- freshName :: Name -> [Type] -> SpecM Name
- instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema
- instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- allLoadedModules :: ModuleEnv -> [LoadedModule]
- allPublicNames :: ModuleEnv -> [Name]
- traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c)
Documentation
type SpecCache = Map Name (Decl, TypesMap (Name, Maybe Decl)) Source
A Name should have an entry in the SpecCache iff it is specializable. Each Name starts out with an empty TypesMap.
getSpecCache :: Monad m => SpecT m SpecCache Source
setSpecCache :: Monad m => SpecCache -> SpecT m () Source
specialize :: Expr -> ModuleCmd Expr Source
Add a `where` clause to the given expression containing type-specialized versions of all functions called (transitively) by the body of the expression.
specializeExpr :: Expr -> SpecM Expr Source
specializeMatch :: Match -> SpecM Match Source
withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map Name (TypesMap Name)) Source
Add the declarations to the SpecCache, run the given monadic action, and then pull the specialized declarations back out of the SpecCache state. Return the result along with the declarations and a table of names of specialized bindings.
specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr Source
Compute the specialization of `EWhere e dgs`. A decl within dgs
is replicated once for each monomorphic type instance at which it
is used; decls not mentioned in e
(even monomorphic ones) are
simply dropped.
specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map Name (TypesMap Name)) Source
Transform the given declaration groups into a set of monomorphic declarations. All of the original declarations with monomorphic types are kept; additionally the result set includes instantiated versions of polymorphic decls that are referenced by the monomorphic bindings. We also return a map relating generated names to the names from the original declarations.
specializeConst :: Expr -> SpecM Expr Source
destEProofApps :: Expr -> (Expr, Int) Source
destETApps :: Expr -> (Expr, [Type]) Source
destEProofAbs :: Expr -> ([Prop], Expr) Source
instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr Source
Reduce `length ts` outermost type abstractions and n
proof abstractions.
allDeclGroups :: ModuleEnv -> [DeclGroup] Source
allLoadedModules :: ModuleEnv -> [LoadedModule] Source
allPublicNames :: ModuleEnv -> [Name] Source
traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c) Source