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

Safe Haskell | None

Agda.TypeChecking.Rules.LHS.Unify

Synopsis

- newtype Unify a = U {
  - unUnify :: ReaderT UnifyEnv (WriterT UnifyOutput (ExceptionT UnifyException (StateT UnifyState TCM))) a
  }
- data UnifyMayPostpone
  - = MayPostpone
  - | MayNotPostpone
- type UnifyEnv = UnifyMayPostpone
- emptyUEnv :: UnifyMayPostpone
- noPostponing :: Unify a -> Unify a
- askPostpone :: Unify UnifyMayPostpone
- type UnifyOutput = Unifiable
- emptyUOutput :: UnifyOutput
- data Unifiable
  - = Definitely
  - | Possibly
- reportPostponing :: Unify ()
- ifClean :: Unify () -> Unify a -> Unify a -> Unify a
- data Equality = Equal TypeHH Term Term
- type Sub = Map Nat Term
- data UnifyException
  - = ConstructorMismatch Type Term Term
  - | StronglyRigidOccurrence Type Term Term
  - | GenericUnifyException String
- data UnifyState = USt {
  - uniSub :: Sub
  - uniConstr :: [Equality]
  }
- emptyUState :: UnifyState
- 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 ()
- checkEqualityHH :: TypeHH -> Term -> Term -> Unify ()
- forceHom :: TypeHH -> TCM Type
- addEquality :: Type -> Term -> Term -> Unify ()
- addEqualityHH :: TypeHH -> Term -> Term -> Unify ()
- takeEqualities :: Unify [Equality]
- occursCheck :: Nat -> Term -> Type -> Unify ()
- (|->) :: Nat -> (Term, Type) -> Unify ()
- makeSubstitution :: Sub -> Substitution
- class UReduce t where
  - ureduce :: t -> Unify t
- flattenSubstitution :: Substitution -> Substitution
- data UnificationResult
  - = Unifies Substitution
  - | NoUnify Type Term Term
  - | DontKnow TCErr
- data HomHet a
  - = Hom a
  - | Het a 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
- absAppHH :: SubstHH t tHH => Abs t -> TermHH -> tHH
- class ApplyHH t where
  - applyHH :: t -> HomHet Args -> HomHet t
- substHH :: SubstHH t tHH => TermHH -> t -> tHH
- class SubstHH t tHH where
  - substUnderHH :: Nat -> TermHH -> t -> tHH
  - trivialHH :: t -> tHH
- unifyIndices_ :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm Substitution
- unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult
- dataOrRecordType :: QName -> Type -> TCM (Maybe Type)
- dataOrRecordType' :: QName -> Type -> TCM (Maybe (QName, Type, Args))
- dataOrRecordTypeHH :: QName -> TypeHH -> TCM (Maybe TypeHH)
- isEtaRecordTypeHH :: MonadTCM tcm => TypeHH -> tcm (Maybe (QName, HomHet Args))
- data ShapeView a
  - = PiSh (Dom a) (Abs a)
  - | FunSh (Dom a) a
  - | DefSh QName
  - | VarSh Nat
  - | LitSh Literal
  - | SortSh
  - | MetaSh
  - | ElseSh
- shapeView :: Type -> Unify (Type, ShapeView Type)
- shapeViewHH :: TypeHH -> Unify (TypeHH, ShapeView TypeHH)
- telViewUpToHH :: Int -> TypeHH -> Unify TelViewHH

# 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 |
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 |
GenericUnifyException String |

Instances

Error UnifyException |
MonadException UnifyException Unify |

data UnifyState

Constructors

USt |
Fields uniSub :: Sub uniConstr :: [Equality]

emptyUState :: UnifyState

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.

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 t => UReduce (Maybe t) |
UReduce t => UReduce (HomHet t) |

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

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 (Arg a) (Arg b) |
SubstHH a b => SubstHH (Dom a) (Dom b) |
SubstHH a b => SubstHH (Tele a) (Tele b) |
SubstHH a b => SubstHH (Abs a) (Abs 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.

unifyIndices :: MonadTCM tcm => FlexibleVars -> Type -> [Arg Term] -> [Arg Term] -> tcm UnificationResult

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