RSolve.HM

HM unification implementations based on propositional logics, based on nominal type system. Author: Taine Zhao(thautwarm) Date: 2019-08-04 License: MIT

Documentation

type Fix a = a -> a

data T

Constructors

TVar Int

TFresh String

T :-> T infixl 6

T :* T infixl 6

TForall (Set String) T

TApp T T

TNom Int

Instances

Eq T

Defined in RSolve.HM

Methods

(==) :: T -> T -> Bool

(/=) :: T -> T -> Bool

Ord T

Defined in RSolve.HM

Methods

compare :: T -> T -> Ordering

(<) :: T -> T -> Bool

(<=) :: T -> T -> Bool

(>) :: T -> T -> Bool

(>=) :: T -> T -> Bool

max :: T -> T -> T

min :: T -> T -> T

Show T

Defined in RSolve.HM

Methods

showsPrec :: Int -> T -> ShowS

show :: T -> String

showList :: [T] -> ShowS

deConsTOp :: T -> Maybe (T -> T -> T, T, T)

data Unif

Constructors

Unif

Fields

• lhs :: T
• rhs :: T
• neq :: Bool

Instances

Eq Unif

Defined in RSolve.HM

Methods

(==) :: Unif -> Unif -> Bool

(/=) :: Unif -> Unif -> Bool

Ord Unif

Defined in RSolve.HM

Methods

compare :: Unif -> Unif -> Ordering

(<) :: Unif -> Unif -> Bool

(<=) :: Unif -> Unif -> Bool

(>) :: Unif -> Unif -> Bool

(>=) :: Unif -> Unif -> Bool

max :: Unif -> Unif -> Unif

min :: Unif -> Unif -> Unif

Show Unif

Defined in RSolve.HM

Methods

showsPrec :: Int -> Unif -> ShowS

show :: Unif -> String

showList :: [Unif] -> ShowS

AtomF Unif

Defined in RSolve.HM

Methods

notA :: Unif -> [Unif]

CtxSolver TCEnv Unif

Defined in RSolve.HM

Methods

solve :: Unif -> MS TCEnv ()

data TCEnv

Constructors

TCEnv

Fields

• _noms :: Map Int T
• _tvars :: Map Int T
• _neqs :: Set (T, T)

Instances

Show TCEnv

Defined in RSolve.HM

Methods

showsPrec :: Int -> TCEnv -> ShowS

show :: TCEnv -> String

showList :: [TCEnv] -> ShowS

CtxSolver TCEnv Unif

Defined in RSolve.HM

Methods

solve :: Unif -> MS TCEnv ()

emptyTCEnv :: TCEnv

tvars :: Lens' TCEnv (Map Int T)

noms :: Lens' TCEnv (Map Int T)

neqs :: Lens' TCEnv (Set (T, T))

newTVar :: MS TCEnv Int

newTNom :: MS TCEnv Int

loadTVar :: Int -> MS TCEnv T

occurIn :: Int -> T -> MS TCEnv Bool

free :: Map String T -> T -> T

prune :: T -> MS TCEnv T

update :: Int -> T -> MS TCEnv ()

addNEq :: (T, T) -> MS TCEnv ()

unify :: Fix (Unif -> MS TCEnv ())