Copyright | (c) 2013-2016 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | cryptol@galois.com |
Stability | provisional |
Portability | portable |
Safe Haskell | Safe |
Language | Haskell2010 |
Synopsis
- type MGU = (Subst, [Prop])
- type Result a = Writer [(Path, UnificationError)] a
- runResult :: Result a -> (a, [(Path, UnificationError)])
- data UnificationError
- uniError :: Path -> UnificationError -> Result MGU
- newtype Path = Path [PathElement]
- data PathElement
- rootPath :: Path
- isRootPath :: Path -> Bool
- extPath :: Path -> PathElement -> Path
- emptyMGU :: MGU
- doMGU :: Type -> Type -> Result MGU
- mgu :: Path -> Type -> Type -> Result MGU
- mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU
- bindVar :: Path -> TVar -> Type -> Result MGU
- ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc
Documentation
type MGU = (Subst, [Prop]) Source #
The most general unifier is a substitution and a set of constraints on bound variables.
data UnificationError Source #
Instances
Show Path Source # | |
Generic Path Source # | |
NFData Path Source # | |
Defined in Cryptol.TypeCheck.Unify | |
PP Path Source # | |
type Rep Path Source # | |
Defined in Cryptol.TypeCheck.Unify type Rep Path = D1 ('MetaData "Path" "Cryptol.TypeCheck.Unify" "cryptol-2.13.0-BA7OuzmYZ3M9j8JsJfXs6b" 'True) (C1 ('MetaCons "Path" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PathElement]))) |
data PathElement Source #
Instances
isRootPath :: Path -> Bool Source #