| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Constraint.Fresh
- class (Applicative m, Monad m) => Freshable m a where
- refreshTy :: SpecType -> CG SpecType
- refreshVV :: Freshable m Integer => SpecType -> m SpecType
- refreshArgs :: SpecType -> CG SpecType
- refreshArgsTop :: (Var, SpecType) -> CG SpecType
- refreshHoles :: (Symbolic t, Reftable r, TyConable c, Freshable f r) => [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)])
- freshTy_type :: KVKind -> CoreExpr -> Type -> CG SpecType
- freshTy_expr :: KVKind -> CoreExpr -> Type -> CG SpecType
- trueTy :: Type -> CG SpecType
- addKuts :: PPrint a => a -> SpecType -> CG ()
Documentation
class (Applicative m, Monad m) => Freshable m a where Source #
Minimal complete definition
Instances
| Freshable m Integer => Freshable m Strata Source # | |
| Freshable m Integer => Freshable m RReft Source # | |
| (Freshable m Integer, Monad m, Applicative m) => Freshable m Reft Source # | |
| (Freshable m Integer, Monad m, Applicative m) => Freshable m Expr Source # | |
| (Freshable m Integer, Monad m, Applicative m) => Freshable m Symbol Source # | |
| Freshable CG Integer Source # | |
| (Freshable m Integer, Freshable m r, Reftable r) => Freshable m (RRType r) Source # | |
| (Freshable m Integer, Monad m, Applicative m) => Freshable m [Expr] Source # | |
refreshHoles :: (Symbolic t, Reftable r, TyConable c, Freshable f r) => [(t, RType c tv r)] -> f ([Symbol], [(t, RType c tv r)]) Source #
freshTy_type :: KVKind -> CoreExpr -> Type -> CG SpecType Source #
Generation: Freshness -----------------------------------------------------
Right now, we generate NO new pvars. Rather than clutter code
with uRType calls, put it in one place where the above
invariant is obviously enforced.
Constraint generation should ONLY use freshTy_type and freshTy_expr