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."

fromCoreModule :: [CoreBind] -> [SeqCoreBind]

Translates a list of Core bindings into Sequent Core.

termFromCoreExpr :: CoreExpr -> SeqCoreTerm

Translates a single Core expression as a Sequent Core term.

bindsToCore :: [SeqCoreBind] -> [CoreBind]

Translates a list of top-level bindings into Core.

commandToCoreExpr :: ContId -> SeqCoreCommand -> CoreExpr

Translates a command into Core.

termToCoreExpr :: SeqCoreTerm -> CoreExpr

Translates a term into Core.

contToCoreExpr :: ContId -> 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.).

onCoreExpr :: (SeqCoreTerm -> SeqCoreTerm) -> CoreExpr -> CoreExpr

Take an operation on Sequent Core terms and perform it on Core expressions

onSequentCoreTerm :: (CoreExpr -> CoreExpr) -> SeqCoreTerm -> SeqCoreTerm

Take an operation on Core expressions and perform it on Sequent Core terms