Agda

Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.LHS.Unify.LeftInverse

Description

Functions for building the left inverse part of a UnifyEquiv.

Synopsis

data DigestedUnifyStep
- = DSolution Int (Dom Type) (FlexibleVar Int) Term (Either () ())
- | DEtaExpandVar (FlexibleVar Int) QName Args
data DigestedUnifyLogEntry = DUnificationStep UnifyState DigestedUnifyStep UnifyOutput
type DigestedUnifyLog = [(DigestedUnifyLogEntry, UnifyState)]
digestUnifyLog :: UnifyLog -> Either NoLeftInv DigestedUnifyLog
data NoLeftInv
- = UnsupportedYet {
  - badStep :: UnifyStep
  }
- | Illegal {
  - badStep :: UnifyStep
  }
- | NoCubical
- | WithKEnabled
- | SplitOnStrict
- | SplitOnFlat
- | UnsupportedCxt
- | CantTransport (Closure (Abs Type))
- | CantTransport' (Closure Type)
buildLeftInverse :: UnifyState -> UnifyLog -> TCM (Either NoLeftInv (Substitution, Substitution))
type Retract = (Telescope, Substitution, Substitution, Substitution)
termsS :: DeBruijn a => Impossible -> [a] -> Substitution' a
composeRetract :: Retract -> Term -> Retract -> TCM (Either (Closure (Abs Type)) Retract)
buildEquiv :: DigestedUnifyLogEntry -> UnifyState -> TCM (Either NoLeftInv (Retract, Term))
explainStep :: MonadPretty m => UnifyStep -> m Doc

Documentation

data DigestedUnifyStep Source #

Constructors

DSolution Int (Dom Type) (FlexibleVar Int) Term (Either () ())
DEtaExpandVar (FlexibleVar Int) QName Args

Instances

Instances details

PrettyTCM DigestedUnifyStep Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => DigestedUnifyStep -> m Doc Source #

data DigestedUnifyLogEntry Source #

Constructors

DUnificationStep UnifyState DigestedUnifyStep UnifyOutput

type DigestedUnifyLog = [(DigestedUnifyLogEntry, UnifyState)] Source #

digestUnifyLog :: UnifyLog -> Either NoLeftInv DigestedUnifyLog Source #

Pre-process a UnifyLog so that we catch unsupported steps early.

data NoLeftInv Source #

Constructors

UnsupportedYet
Fields badStep :: UnifyStep
Illegal
Fields badStep :: UnifyStep
NoCubical
WithKEnabled
SplitOnStrict	splitting on a Strict Set.
SplitOnFlat	splitting on a @♭ argument
UnsupportedCxt
CantTransport (Closure (Abs Type))
CantTransport' (Closure Type)

Instances

Instances details

PrettyTCM NoLeftInv Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods prettyTCM :: MonadPretty m => NoLeftInv -> m Doc Source #
Show NoLeftInv Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Unify.LeftInverse Methods showsPrec :: Int -> NoLeftInv -> ShowS # show :: NoLeftInv -> String # showList :: [NoLeftInv] -> ShowS #

buildLeftInverse :: UnifyState -> UnifyLog -> TCM (Either NoLeftInv (Substitution, Substitution)) Source #

Build the left inverse part of a UnifyEquiv (τ, leftInv).

type Retract = (Telescope, Substitution, Substitution, Substitution) Source #

termsS :: DeBruijn a => Impossible -> [a] -> Substitution' a Source #

composeRetract :: Retract -> Term -> Retract -> TCM (Either (Closure (Abs Type)) Retract) Source #

buildEquiv :: DigestedUnifyLogEntry -> UnifyState -> TCM (Either NoLeftInv (Retract, Term)) Source #

Build the left inverse corresponding to a single unification step.

explainStep :: MonadPretty m => UnifyStep -> m Doc Source #