cryptol-2.2.6: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2015 Galois, Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | None
Language | Haskell98

Cryptol.Transform.Specialize

Description

Synopsis

- type SpecCache = Map QName (Decl, TypesMap (QName, 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 QName (TypesMap QName))
- specializeEWhere :: Expr -> [DeclGroup] -> SpecM Expr
- specializeDeclGroups :: [DeclGroup] -> SpecM ([DeclGroup], Map QName (TypesMap QName))
- specializeConst :: Expr -> SpecM Expr
- destEProofApps :: Expr -> (Expr, Int)
- destETApps :: Expr -> (Expr, [Type])
- destEProofAbs :: Expr -> ([Prop], Expr)
- destETAbs :: Expr -> ([TParam], Expr)
- freshName :: QName -> [Type] -> SpecM QName
- matchingBoundNames :: Maybe ModName -> SpecM [String]
- reifyName :: Name -> [Type] -> String
- instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema
- instantiateExpr :: [Type] -> Int -> Expr -> SpecM Expr
- allDeclGroups :: ModuleEnv -> [DeclGroup]
- allLoadedModules :: ModuleEnv -> [LoadedModule]
- allPublicQNames :: ModuleEnv -> [QName]
- traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c)

# Documentation

type SpecCache = Map QName (Decl, TypesMap (QName, Maybe Decl)) Source

A QName should have an entry in the SpecCache iff it is specializable. Each QName starts out with an empty TypesMap.

type SpecT m a = StateT SpecCache (ModuleT m) a Source

The specializer monad.

type SpecM a = SpecT IO a Source

runSpecT :: SpecCache -> SpecT m a -> ModuleT m (a, SpecCache) Source

liftSpecT :: Monad m => ModuleT m a -> SpecT m a Source

getSpecCache :: Monad m => SpecT m SpecCache Source

setSpecCache :: Monad m => SpecCache -> SpecT m () Source

modifySpecCache :: Monad m => (SpecCache -> SpecCache) -> SpecT m () Source

modify :: StateM m s => (s -> s) -> 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 QName (TypesMap QName)) 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 QName (TypesMap QName)) 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

destETAbs :: Expr -> ([TParam], Expr) Source

freshName :: QName -> [Type] -> SpecM QName Source

matchingBoundNames :: Maybe ModName -> SpecM [String] Source

reifyName :: Name -> [Type] -> String Source

instantiateSchema :: [Type] -> Int -> Schema -> SpecM Schema 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

allPublicQNames :: ModuleEnv -> [QName] Source

traverseSnd :: Functor f => (b -> f c) -> (a, b) -> f (a, c) Source