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
Language | Haskell2010

Cryptol.TypeCheck.Unify

Description

Synopsis

- type MGU = (Subst, [Prop])
- type Result a = Writer [(Path, UnificationError)] a
- runResult :: Result a -> (a, [(Path, UnificationError)])
- data UnificationError
  - = UniTypeMismatch Type Type
  - | UniKindMismatch Kind Kind
  - | UniTypeLenMismatch Int Int
  - | UniRecursive TVar Type
  - | UniNonPolyDepends TVar [TParam]
  - | UniNonPoly TVar Type
- uniError :: Path -> UnificationError -> Result MGU
- newtype Path = Path [PathElement]
- data PathElement
  - = TConArg TC Int
  - | TNewtypeArg Newtype Int
  - | TRecArg Ident
- 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.

type Result a = Writer [(Path, UnificationError)] a Source #

runResult :: Result a -> (a, [(Path, UnificationError)]) Source #

data UnificationError Source #

Constructors

UniTypeMismatch Type Type |
UniKindMismatch Kind Kind |
UniTypeLenMismatch Int Int |
UniRecursive TVar Type |
UniNonPolyDepends TVar [TParam] |
UniNonPoly TVar Type |

uniError :: Path -> UnificationError -> Result MGU Source #

newtype Path Source #

Constructors

Path [PathElement] |

#### Instances

Instances details

Generic Path Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Associated Types type Rep Path :: Type -> Type Source # Methods from :: Path -> Rep Path x Source # to :: Rep Path x -> Path Source #
Show Path Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Methods showsPrec :: Int -> Path -> ShowS Source # show :: Path -> String Source # showList :: [Path] -> ShowS Source #
PP Path Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Methods ppPrec :: Int -> Path -> Doc Source #
NFData Path Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Methods rnf :: Path -> () Source #
type Rep Path Source # |
Instance details Defined in Cryptol.TypeCheck.Unify type Rep Path = D1 ('MetaData "Path" "Cryptol.TypeCheck.Unify" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'True) (C1 ('MetaCons "Path" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PathElement])))

data PathElement Source #

Constructors

TConArg TC Int |
TNewtypeArg Newtype Int |
TRecArg Ident |

#### Instances

Instances details

Generic PathElement Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Associated Types type Rep PathElement :: Type -> Type Source # Methods from :: PathElement -> Rep PathElement x Source # to :: Rep PathElement x -> PathElement Source #
Show PathElement Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Methods showsPrec :: Int -> PathElement -> ShowS Source # show :: PathElement -> String Source # showList :: [PathElement] -> ShowS Source #
NFData PathElement Source # |
Instance details Defined in Cryptol.TypeCheck.Unify Methods rnf :: PathElement -> () Source #
type Rep PathElement Source # |

Instance details

Defined in Cryptol.TypeCheck.Unify

type Rep PathElement = D1 ('MetaData "PathElement" "Cryptol.TypeCheck.Unify" "cryptol-3.0.0-DBVDUAjB1JeD0WzkHH4ckn" 'False) (C1 ('MetaCons "TConArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TC) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "TNewtypeArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Newtype) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "TRecArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Ident))))

rootPath :: Path Source #

isRootPath :: Path -> Bool Source #

extPath :: Path -> PathElement -> Path Source #

emptyMGU :: MGU Source #

doMGU :: Type -> Type -> Result MGU Source #

mgu :: Path -> Type -> Type -> Result MGU Source #

mguMany :: Path -> [Path] -> [Type] -> [Type] -> Result MGU Source #

bindVar :: Path -> TVar -> Type -> Result MGU Source #

ppPathEl :: PathElement -> Int -> (Int -> Doc) -> Doc Source #