Agda.TypeChecking.Rules.LHS.Unify

Documentation

newtype Unify a

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

MonadReader TCEnv Unify

MonadState TCState Unify

MonadWriter UnifyOutput Unify

MonadException UnifyException Unify

data UnifyMayPostpone

Constructors

MayPostpone

MayNotPostpone

type UnifyEnv = UnifyMayPostpone

emptyUEnv :: UnifyMayPostpone

noPostponing :: Unify a -> Unify a

askPostpone :: Unify UnifyMayPostpone

type UnifyOutput = Unifiable

Output the result of unification (success or maybe).

emptyUOutput :: UnifyOutput

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 = Map Nat 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

onSub :: (Sub -> a) -> Unify a

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.

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 UnificationResult

Constructors

Unifies Substitution

NoUnify Type Term Term

DontKnow TCErr

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

Typeable1 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, HomHet (Type, 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

Typeable1 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$.