Cortex to Core

programToCore turns an ordered Cortex program into a Core program. Each procedure body becomes a Core CFG body (.cfg), block for block: labels, commands and transfers are kept, so no control flow is rebuilt. Core can type-check and print the result. The verifier (Core.verify) and the evaluator behind Core.Program.interpretEntries accept only structured bodies, so they do not run it.

Core's CFG type checker puts two requirements on the Cortex CFG:

• Every init sits in a block that dominates the uses of its variable and that is not on a cycle. FromLaurel output meets this: it declares every local in one block that runs once, before the body, and the passes declare theirs in blocks that run before that one. Nothing here hoists declarations; a frontend that declares a local inside a loop has to hoist it first.
• Every block that uses a local is reachable from the entry. An unreachable block is scoped without the locals of any dominator, so its uses are rejected. PruneUnreachable removes unreachable blocks.

structure Cortex.ToCore.Sig : Type

• inputs : List String
• outputs : List String

def Cortex.ToCore.toMono (t : Lambda.LTy) : Except String Lambda.LMonoTy

Equations

• Cortex.ToCore.toMono (Lambda.LTy.forAll [] m) = Except.ok m
• Cortex.ToCore.toMono t = Except.error "polymorphic type in Cortex"

def Cortex.ToCore.callArgs (sig : Option Sig) (lhs : List Core.Expression.Ident) (args : List Expr) : Except String (List (Imperative.CallArg Core.Expression))

Equations

• One or more equations did not get rendered due to their size.
• Cortex.ToCore.callArgs none lhs args = pure (List.map Imperative.CallArg.inArg args ++ List.map Imperative.CallArg.outArg lhs)

def Cortex.ToCore.toCoreCmd (sigs : Std.HashMap String Sig) : IRCmd → Except String Core.Command

Equations

• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.cmd c) = Except.ok (Imperative.CmdExt.cmd c)
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.call lhs p args md) = do let __do_lift ← Cortex.ToCore.callArgs (sigs.get? p) lhs args pure (Imperative.CmdExt.call p __do_lift md)
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.virtualCall lhs owner method args md) = Except.error "Cortex `virtualCall` must be lowered by LowerDispatch before Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.new lhs ty md) = Except.error "Cortex `new` must be lowered before Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.cast lhs ty e mode md) = Except.error "Cortex `cast` must be lowered by LowerCTE before Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.readField lhs obj field md) = Except.error "Cortex field read must be lowered before Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.writeField obj field rhs md) = Except.error "Cortex field write must be lowered before Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.instanceOf lhs obj ty md) = Except.error "Cortex `instanceOf` must be lowered before Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.newArray lhs ty len md) = Except.error "Cortex array commands are not lowered to Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.readElem lhs arr index elemTy md) = Except.error "Cortex array commands are not lowered to Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.writeElem arr index rhs elemTy md) = Except.error "Cortex array commands are not lowered to Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.arrayLength lhs arr md) = Except.error "Cortex array commands are not lowered to Core"
• Cortex.ToCore.toCoreCmd sigs (Cortex.IRCmd.throw exn md) = Except.error "Cortex `throw` must be lowered before Core"

def Cortex.ToCore.procedureHeader (p : Procedure) : Except String Core.Procedure.Header

The Core header of a procedure: its name and its parameters with monomorphic types. A body may assign only its outputs and its locals, so an assigned input that is not an output is an error: the CopyAssignedInputs pass replaces such an assignment by one to a local copy.

Equations

• One or more equations did not get rendered due to their size.

def Cortex.ToCore.procedureSpec (p : Procedure) : Core.Procedure.Spec

A procedure's preconditions as Core's, labelled requires_<i>.

Equations

• One or more equations did not get rendered due to their size.

def Cortex.ToCore.procedureToCore (sigs : Std.HashMap String Sig) (p : Procedure) : Except String Core.Procedure

A Cortex procedure as a Core procedure with a CFG body. A procedure without a body gets a structured body that assumes true.

Equations

• One or more equations did not get rendered due to their size.

def Cortex.ToCore.programToCore : Program → Except String Core.Program

An ordered Cortex program as a Core program whose procedure bodies are CFGs.

Equations

• One or more equations did not get rendered due to their size.
• Cortex.ToCore.programToCore (Cortex.Program.unordered p) = Except.error "Internal error: Cortex must be ordered by the Ordering pass before Core"