Agda-2.4.2.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

Documentation

type UnifyOutput = Unifiable Source

Output the result of unification (success or maybe).

data Unifiable Source

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

reportPostponing :: Unify () Source

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

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

Check whether unification proceeded without postponement.

data Equality Source

Constructors

Equal TypeHH Term Term 

Instances

data UnifyState Source

Constructors

USt 

Fields

uniSub :: Sub
 
uniConstr :: [Equality]
 

projectionMismatch :: QName -> QName -> Unify a Source

Throw-away error message.

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

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

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

Force equality now instead of postponing it using addEquality.

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

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 Source

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

makeHom :: TypeHH -> TCM (Maybe Type) Source

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

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

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

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

Assignment with preceding occurs check.

class UReduce t where Source

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

Methods

ureduce :: t -> Unify t Source

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 Source

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 Source

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

Constructors

Hom a

homogeneous

Het a a

heterogeneous

leftHH :: HomHet a -> a Source

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

class ApplyHH t where Source

Methods

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

Instances

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

class SubstHH t tHH where Source

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

Methods

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

trivialHH :: t -> tHH Source

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 Source

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.

dataOrRecordType Source

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' Source

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 Source

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.

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

Return record type identifier if argument is a record type.

data ShapeView a Source

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) 
Typeable (* -> *) ShapeView 

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

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

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

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

telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH Source

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