Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.TypeChecking.Rules.LHS.Unify.LeftInverse
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 { }
- | Illegal { }
- | 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
PrettyTCM DigestedUnifyStep Source # | |
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.
Constructors
UnsupportedYet | |
Illegal | |
NoCubical | |
WithKEnabled | |
SplitOnStrict | splitting on a Strict Set. |
SplitOnFlat | splitting on a @♭ argument |
UnsupportedCxt | |
CantTransport (Closure (Abs Type)) | |
CantTransport' (Closure Type) |
buildLeftInverse :: UnifyState -> UnifyLog -> TCM (Either NoLeftInv (Substitution, Substitution)) Source #
type Retract = (Telescope, Substitution, Substitution, Substitution) Source #
termsS :: DeBruijn a => Impossible -> [a] -> Substitution' a Source #
buildEquiv :: DigestedUnifyLogEntry -> UnifyState -> TCM (Either NoLeftInv (Retract, Term)) Source #
explainStep :: MonadPretty m => UnifyStep -> m Doc Source #