Idris.Core.Unify

Unification is applied inside the theorem prover. We're looking for holes which can be filled in, by matching one term's normal form against another. Returns a list of hole names paired with the term which solves them, and a list of things which need to be injective.

Documentation

match_unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [FailContext] -> TC [(Name, TT Name)]

unify :: Context -> Env -> (TT Name, Maybe Provenance) -> (TT Name, Maybe Provenance) -> [Name] -> [Name] -> [Name] -> [FailContext] -> TC ([(Name, TT Name)], Fails)

type Fails = [(TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)]

data FailContext

Constructors

FailContext

Fields

• fail_sourceloc :: FC
• fail_fn :: Name
• fail_param :: Name

Instances

Eq FailContext

Methods

(==) :: FailContext -> FailContext -> Bool

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

Show FailContext

Methods

showsPrec :: Int -> FailContext -> ShowS

show :: FailContext -> String

showList :: [FailContext] -> ShowS

data FailAt

Constructors

Match

Unify

Instances

Eq FailAt

Methods

(==) :: FailAt -> FailAt -> Bool

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

Show FailAt

Methods

showsPrec :: Int -> FailAt -> ShowS

show :: FailAt -> String

showList :: [FailAt] -> ShowS

unrecoverable :: Fails -> Bool