Agda.TypeChecking.Rules.LHS.Unify

Documentation

type UnificationResult = UnificationResult' Substitution

Result of unifyIndices.

data UnificationResult' a

Constructors

Unifies a

Unification succeeded.

NoUnify TCErr

Terms are not unifiable.

DontKnow TCErr

Some other error happened, unification got stuck.

Instances

Functor UnificationResult'

Foldable UnificationResult'

Traversable UnificationResult'

Show a => Show (UnificationResult' a)

newtype Unify a

Monad for unification.

Constructors

U

Fields

unUnify :: ReaderT UnifyEnv (WriterT UnifyOutput (ExceptionT UnifyException (StateT UnifyState TCM))) a

Instances

Monad Unify

Functor Unify

Applicative Unify

MonadIO Unify

MonadTCM Unify

HasConstInfo Unify

MonadWriter UnifyOutput Unify

MonadState TCState Unify

MonadReader TCEnv Unify

MonadException UnifyException Unify

data UnifyMayPostpone

Constructors

MayPostpone

MayNotPostpone

type UnifyEnv = UnifyMayPostpone

emptyUEnv :: UnifyEnv

noPostponing :: Unify a -> Unify a

askPostpone :: Unify UnifyMayPostpone

type UnifyOutput = Unifiable

Output the result of unification (success or maybe).

data Unifiable

Were two terms unifiable or did we have to postpone some equation such that we are not sure?

Constructors

Definitely

Unification succeeded.

Possibly

Unification did not fail, but we had to postpone a part.

Instances

Monoid Unifiable

Conjunctive monoid.

MonadWriter UnifyOutput Unify

reportPostponing :: Unify ()

Tell that something could not be unified right now, so the unification succeeds only Possibly.

ifClean :: Unify () -> Unify a -> Unify a -> Unify a

Check whether unification proceeded without postponement.

data Equality

Constructors

Equal TypeHH Term Term

Instances

Subst Equality

type Sub = IntMap Term

data UnifyException

Constructors

ConstructorMismatch Type Term Term

StronglyRigidOccurrence Type Term Term

UnclearOccurrence Type Term Term

WithoutKException Type Term Term

GenericUnifyException String

Instances

Error UnifyException

MonadException UnifyException Unify

data UnifyState

Constructors

USt

Fields

uniSub :: Sub

uniConstr :: [Equality]

emptyUState :: UnifyState

projectionMismatch :: QName -> QName -> Unify a

Throw-away error message.

constructorMismatch :: Type -> Term -> Term -> Unify a

constructorMismatchHH :: TypeHH -> Term -> Term -> Unify a

getSub :: Unify Sub

modSub :: (Sub -> Sub) -> Unify ()

checkEqualities :: [Equality] -> TCM ()

checkEquality :: Type -> Term -> Term -> TCM ()

Force equality now instead of postponing it using addEquality.

checkEqualityHH :: TypeHH -> Term -> Term -> Unify ()

Try equality. If constraints remain, postpone (enter unsafe mode). Heterogeneous equalities cannot be tried nor reawakened, so we can throw them away and flag "dirty".

forceHom :: TypeHH -> TCM Type

Check whether heterogeneous situation is really homogeneous. If not, give up.

makeHom :: TypeHH -> TCM (Maybe Type)

Check whether heterogeneous situation is really homogeneous. If not, return Nothing.

tryHom :: TypeHH -> Term -> Term -> TCM TermHH

Try to make a possibly heterogeneous term situation homogeneous.

addEquality :: Type -> Term -> Term -> Unify ()

addEqualityHH :: TypeHH -> Term -> Term -> Unify ()

takeEqualities :: Unify [Equality]

occursCheck :: Nat -> Term -> Type -> Unify ()

Includes flexible occurrences, metas need to be solved. TODO: relax? TODO: later solutions may remove flexible occurences

(|->) :: Nat -> (Term, Type) -> Unify ()

Assignment with preceding occurs check.

makeSubstitution :: Sub -> Substitution

class UReduce t where

Apply the current substitution on a term and reduce to weak head normal form.

Methods

ureduce :: t -> Unify t

Instances

UReduce Type

UReduce Term

UReduce a => UReduce [a]

UReduce t => UReduce (Maybe t)

UReduce a => UReduce (Arg a)

UReduce t => UReduce (HomHet t)

(UReduce a, UReduce b) => UReduce (a, b)

(UReduce a, UReduce b, UReduce c) => UReduce (a, b, c)

flattenSubstitution :: Substitution -> Substitution

Take a substitution σ and ensure that no variables from the domain appear in the targets. The context of the targets is not changed. TODO: can this be expressed using makeSubstitution and applySubst?

data HomHet a

Are we in a homogeneous (one type) or heterogeneous (two types) situation?

Constructors

Hom a

homogeneous

Het a a

heterogeneous

Instances

Functor HomHet

Foldable HomHet

Traversable HomHet

SubstHH Type (HomHet Type)

SubstHH Term (HomHet Term)

Eq a => Eq (HomHet a)

Ord a => Ord (HomHet a)

Show a => Show (HomHet a)

Subst a => Subst (HomHet a)

PrettyTCM a => PrettyTCM (HomHet a)

UReduce t => UReduce (HomHet t)

(Free a, Subst a) => SubstHH (HomHet a) (HomHet a)

isHom :: HomHet a -> Bool

fromHom :: HomHet a -> a

leftHH :: HomHet a -> a

rightHH :: HomHet a -> a

type TermHH = HomHet Term

type TypeHH = HomHet Type

type TelHH = Tele (Dom TypeHH)

type TelViewHH = TelV TypeHH

type ArgsHH = HomHet Args

absAppHH :: SubstHH t tHH => Abs t -> TermHH -> tHH

class ApplyHH t where

Methods

applyHH :: t -> HomHet Args -> HomHet t

Instances

ApplyHH Type

ApplyHH Term

substHH :: SubstHH t tHH => TermHH -> t -> tHH

class SubstHH t tHH where

substHH u t substitutes u for the 0th variable in t.

Methods

substUnderHH :: Nat -> TermHH -> t -> tHH

trivialHH :: t -> tHH

Instances

SubstHH Type (HomHet Type)

SubstHH Term (HomHet Term)

SubstHH a b => SubstHH (Tele a) (Tele b)

SubstHH a b => SubstHH (Abs a) (Abs b)

SubstHH a b => SubstHH (Dom a) (Dom b)

SubstHH a b => SubstHH (Arg a) (Arg b)

(Free a, Subst a) => SubstHH (HomHet a) (HomHet a)

(SubstHH a a', SubstHH b b') => SubstHH (a, b) (a', b')

unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> Args -> Args -> tcm Substitution

Unify indices.

In unifyIndices_ flex a us vs,

a is the type eliminated by us and vs (usally the type of a constructor), need not be reduced,

us and vs are the argument lists to unify,

flex is the set of flexible (instantiable) variabes in us and vs.

The result is the most general unifier of us and vs.

unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> Args -> Args -> tcm UnificationResult

dataOrRecordType

Arguments

:: ConHead

Constructor name.

-> Type

Type of constructor application (must end in data/record).

-> TCM (Maybe Type)

Type of constructor, applied to pars.

Given the type of a constructor application the corresponding data or record type, applied to its parameters (extracted from the given type), is returned.

Precondition: The type has to correspond to an application of the given constructor.

dataOrRecordType'

Arguments

:: ConHead

Constructor name.

-> Type

Type of constructor application (must end in data/record).

-> TCM (Maybe (QName, Type, Args, Args))

Name of data/record type, type of constructor to be applied, data/record parameters, and data indices

dataOrRecordTypeHH

Arguments

:: ConHead

Constructor name.

-> TypeHH

Type(s) of constructor application (must end in same data/record).

-> TCM (Maybe TypeHH)

Type of constructor, instantiated possibly heterogeneously to parameters.

Heterogeneous situation. a1 and a2 need to end in same datatype/record.

dataOrRecordTypeHH' :: ConHead -> TypeHH -> TCM (Maybe (QName, Type, HomHet (Args, Args)))

isEtaRecordTypeHH :: MonadTCM tcm => TypeHH -> tcm (Maybe (QName, HomHet Args))

Return record type identifier if argument is a record type.

data ShapeView a

Views an expression (pair) as type shape. Fails if not same shape.

Constructors

PiSh (Dom a) (Abs a)

FunSh (Dom a) a

DefSh QName

data/record

VarSh Nat

neutral type

LitSh Literal

built-in type

SortSh

MetaSh

some meta

ElseSh

not a type or not definitely same shape

Instances

Functor ShapeView

(Eq a, Subst a) => Eq (ShapeView a)

(Ord a, Subst a) => Ord (ShapeView a)

Show a => Show (ShapeView a)

shapeView :: Type -> Unify (Type, ShapeView Type)

Return the type and its shape. Expects input in (u)reduced form.

shapeViewHH :: TypeHH -> Unify (TypeHH, ShapeView TypeHH)

Return the reduced type(s) and the common shape.

telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH

telViewUpToHH n t takes off the first n function types of t. Takes off all if $n < 0$.