License	BSD3
Maintainer	The Idris Community.
Safe Haskell	None
Language	Haskell2010

Idris.Core.Unify

Description

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)] Source #

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

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

data FailContext Source #

Constructors

FailContext
Fields fail_sourceloc :: FC fail_fn :: Name fail_param :: Name

Instances

Eq FailContext Source #
Methods (==) :: FailContext -> FailContext -> Bool # (/=) :: FailContext -> FailContext -> Bool #
Show FailContext Source #
Methods showsPrec :: Int -> FailContext -> ShowS # show :: FailContext -> String # showList :: [FailContext] -> ShowS #

data FailAt Source #

Constructors

Match
Unify

Instances

Eq FailAt Source #
Methods (==) :: FailAt -> FailAt -> Bool # (/=) :: FailAt -> FailAt -> Bool #
Show FailAt Source #
Methods showsPrec :: Int -> FailAt -> ShowS # show :: FailAt -> String # showList :: [FailAt] -> ShowS #

unrecoverable :: Fails -> Bool Source #