Language.SequentCore.Translate

Translation between Sequent Core and native GHC Core.

Documentation

The translations to and from Sequent Core are not guaranteed to be perfect inverses. However, any differences between e and commandToCoreExpr (fromCoreExpr e) should be operationally insignificant, such as a let floating out from a function being applied. A more precise characterization of the indended invariants of these functions would entail some sort of bisimulation, but it should suffice to know that the translations are "faithful enough."

fromCoreExpr :: CoreExpr -> SeqCoreCommand

Translates a Core expression into Sequent Core.

fromCoreBind :: CoreBind -> SeqCoreBind

Translates a Core binding into Sequent Core.

fromCoreBinds :: [CoreBind] -> [SeqCoreBind]

Translates a list of Core bindings into Sequent Core.

fromCoreAlt :: CoreAlt -> SeqCoreAlt

Translates a Core case alternative into Sequent Core.

commandToCoreExpr :: SeqCoreCommand -> CoreExpr

Translates a command into Core.

valueToCoreExpr :: SeqCoreValue -> CoreExpr

Translates a value into Core.

contToCoreExpr :: SeqCoreCont -> CoreExpr -> CoreExpr

Translates a continuation into a function that will wrap a Core expression with a fragment of context (an argument to apply to, a case expression to run, etc.).

bindToCore :: SeqCoreBind -> CoreBind

Translates a binding into Core.

bindsToCore :: [SeqCoreBind] -> [CoreBind]

Translates a list of bindings into Core.

altToCore :: SeqCoreAlt -> CoreAlt

Translates a case alternative into Core.