cryptol-3.3.0: Cryptol: The Language of Cryptography
Copyright(c) 2013-2016 Galois Inc.
LicenseBSD3
Maintainercryptol@galois.com
Stabilityprovisional
Portabilityportable
Safe HaskellSafe
LanguageHaskell2010

Cryptol.TypeCheck.Unify

Description

 
Synopsis

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 #

Methods

from :: Path -> Rep Path x #

to :: Rep Path x -> Path #

Show Path Source # 
Instance details

Defined in Cryptol.TypeCheck.Unify

Methods

showsPrec :: Int -> Path -> ShowS #

show :: Path -> String #

showList :: [Path] -> ShowS #

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

type Rep Path Source # 
Instance details

Defined in Cryptol.TypeCheck.Unify

type Rep Path = D1 ('MetaData "Path" "Cryptol.TypeCheck.Unify" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" 'True) (C1 ('MetaCons "Path" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [PathElement])))

data PathElement Source #

Constructors

TConArg TC Int 
TNominalArg NominalType Int 
TRecArg Ident 

Instances

Instances details
Generic PathElement Source # 
Instance details

Defined in Cryptol.TypeCheck.Unify

Associated Types

type Rep PathElement :: Type -> Type #

Methods

from :: PathElement -> Rep PathElement x #

to :: Rep PathElement x -> PathElement #

Show PathElement Source # 
Instance details

Defined in Cryptol.TypeCheck.Unify

Methods

showsPrec :: Int -> PathElement -> ShowS #

show :: PathElement -> String #

showList :: [PathElement] -> ShowS #

NFData PathElement Source # 
Instance details

Defined in Cryptol.TypeCheck.Unify

Methods

rnf :: PathElement -> () #

type Rep PathElement Source # 
Instance details

Defined in Cryptol.TypeCheck.Unify

type Rep PathElement = D1 ('MetaData "PathElement" "Cryptol.TypeCheck.Unify" "cryptol-3.3.0-7OIQa8lMv7L2xoAlM9JEI6" '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 "TNominalArg" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NominalType) :*: 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 #