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