hermit-0.3.1.0: Haskell Equational Reasoning Model-to-Implementation Tunnel

Safe HaskellNone

HERMIT.Dictionary.Undefined

Contents

Synopsis

Working with Undefined Values

Note that many of these operations require undefined to be explicitly imported if it is not used in the source file.

verifyStrictT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => CoreExpr -> Rewrite c m CoreExpr -> Translate c m a ()Source

Verify that the given rewrite is a proof that the given expression is a strict function.

mkUndefinedValT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Type -> Translate c m a CoreExprSource

Make an undefined value of the given type.

isUndefinedValT :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Translate c m CoreExpr ()Source

Check if the current expression is an undefined value.

errorToUndefinedR :: (BoundVars c, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

error ty string ==> undefined ty

undefinedExprR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

undefinedExprR = undefinedAppR <+ undefinedLamR <+ undefinedLetR <+ undefinedCastR <+ undefinedTickR <+ undefinedCaseR

undefinedAppR :: (BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

(undefined ty1) e ==> undefined ty2

undefinedLamR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

( v -> undefined ty1) ==> undefined ty2 (where v is not a TyVar)

undefinedLetR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

let bds in (undefined ty) ==> undefined ty

undefinedCaseScrutineeR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

case (undefined ty) of alts ==> undefined ty

undefinedCaseAltsR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

case e of {pat_1 -> undefined ty ; pat_2 -> undefined ty ; ... ; pat_n -> undefined ty} ==> undefined ty

undefinedCaseR :: (AddBindings c, BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

undefinedCaseR = undefinedCaseScrutineeR <+ undefinedCaseAltsR

undefinedCastR :: (BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

Cast (undefined ty1) co ==> undefined ty2

undefinedTickR :: (BoundVars c, ExtendPath c Crumb, HasGlobalRdrEnv c, MonadCatch m, HasDynFlags m, MonadThings m) => Rewrite c m CoreExprSource

Tick tick (undefined ty1) ==> undefined ty1