Cryptol.Transform.Specialize

Documentation

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

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

The specializer monad.

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

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

specializeMatch :: Match -> SpecM Match

withDeclGroups :: [DeclGroup] -> SpecM a -> SpecM (a, [DeclGroup], Map QName (TypesMap QName))

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

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

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

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

Reduce `length ts` outermost type abstractions and n proof abstractions.

allDeclGroups :: ModuleEnv -> [DeclGroup]

allLoadedModules :: ModuleEnv -> [LoadedModule]

allPublicQNames :: ModuleEnv -> [QName]

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