cryptol-3.0.0: Cryptol: The Language of Cryptography

Copyright | (c) 2013-2016 Galois Inc.
License | BSD3
Maintainer | cryptol@galois.com
Stability | provisional
Portability | portable
Safe Haskell | Safe-Inferred
Language | Haskell2010

Cryptol.Transform.Specialize

Description

Synopsis

- 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]
- 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`.

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 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 #

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

freshName :: Name -> [Type] -> SpecM Name Source #

Freshen a name by giving it a new unique.

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 #

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