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

Safe HaskellNone

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

Documentation

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

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

type Sub = Map Nat Term

data UnifyState

Constructors

USt 

Fields

uniSub :: Sub
 
uniConstr :: [Equality]
 

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

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

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.

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.

class UReduce t where

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

Methods

ureduce :: t -> Unify t

Instances

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 substs?

data HomHet a

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

Constructors

Hom a

homogeneous

Het a a

heterogeneous

isHom :: HomHet a -> Bool

fromHom :: HomHet a -> a

leftHH :: HomHet a -> a

rightHH :: HomHet a -> a

type TelHH = Tele (Arg TypeHH)

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

class ApplyHH t where

Methods

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

Instances

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 (Arg a) (Arg b) 
SubstHH a b => SubstHH (Abs a) (Abs b) 
SubstHH a b => SubstHH (Tele a) (Tele 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 -> [Arg Term] -> [Arg Term] -> tcm Substitution

Unify indices.

dataOrRecordType

Arguments

:: QName

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

:: QName

Constructor name.

-> Type

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

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

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

dataOrRecordTypeHH

Arguments

:: QName

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))

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 (Arg a) (Abs a) 
FunSh (Arg 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

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