hermit-0.5.0.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone
LanguageHaskell2010

HERMIT.Dictionary.Fold

Contents

Synopsis

Fold/Unfold Transformation

externals :: [External] Source

foldR :: ReadBindings c => String -> Rewrite c HermitM CoreExpr Source

foldVarR :: ReadBindings c => Var -> Maybe BindingDepth -> Rewrite c HermitM CoreExpr Source

stashFoldR :: ReadBindings c => Label -> Rewrite c HermitM CoreExpr Source

stashFoldAnyR :: ReadBindings c => Rewrite c HermitM CoreExpr Source

Unlifted fold interface

fold :: Id -> CoreExpr -> CoreExpr -> Maybe CoreExpr Source

unifyTypes :: [TyVar] -> Type -> Type -> Maybe [(TyVar, Type)] Source

Given list of TyVars which can match any type (the holes), a pattern, and a concrete type, return mapping from hole to type for successful unification.

tyMatchesToCoreExpr :: [(TyVar, Type)] -> [(Var, CoreExpr)] Source