Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Judgment codegen_stmt at crates/formality-rust/src/codegen/mod.rs:119

Signature:

codegen_stmt(global: CodegenGlobal, cfn: CodegenFn, scope: CodegenScope, stmt: Stmt,) => (CodeBlock, CodegenScope, CodegenGlobal, CodegenFn)

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

let-init
LineCoverageSource
129✗(let (local, cfn) = cfn.alloc_temp(ty)?)
130✗(let scope = scope.push_var(id, local, ty)?)
131✗(codegen_expr_into(global, cfn, scope, local, &init.expr) => (code, global, cfn))
──────── ("let-init")
133✗(codegen_stmt(global, cfn, scope, Stmt::Let { label: _, id, ty, init: Some(init) }) => (code, scope, global, cfn))
let-no-init
LineCoverageSource
137✗(let (local, cfn) = cfn.alloc_temp(ty)?)
138✗(let scope = scope.push_var(id, local, ty)?)
139N/A(let code = cfn.fresh_code_block())
──────── ("let-no-init")
141✗(codegen_stmt(global, cfn, scope, Stmt::Let { label: _, id, ty, init: None }) => (code, scope, global, cfn))
return
LineCoverageSource
145✗(codegen_expr_into(global, cfn, scope, scope.ret_local, expr) => (code, global, cfn))
146N/A(let (code, cfn) = cfn.terminated(code, terminator_return()))
──────── ("return")
148✗(codegen_stmt(global, cfn, scope, Stmt::Return { expr }) => (code, scope, global, cfn))
print
LineCoverageSource
152✗(type_expr(cfn, scope, expr) => expr_ty)
153✗(let (temp, cfn) = cfn.alloc_temp(&expr_ty)?)
154✗(codegen_expr_into(global, cfn, scope, temp, expr) => (code, global, cfn))
155✗(let (code, cfn) = cfn.print_intrinsic(code, temp)?)
──────── ("print")
157✗(codegen_stmt(global, cfn, scope, Stmt::Print { expr }) => (code, scope, global, cfn))
if
LineCoverageSource
161N/A(let (ct, cfn) = cfn.alloc_local(bool_ty()))
162✗(codegen_expr_into(global, cfn, scope, ct, condition) => (cond_code, global, cfn))
163✗(codegen_block(global, cfn, scope, then_block) => (then_code, global, cfn))
164✗(codegen_block(global, cfn, scope, &else_block.block) => (else_code, global, cfn))
165N/A(let (code, cfn) = cfn.branch_on_bool_from(cond_code, ct, then_code, else_code))
──────── ("if")
167✗(codegen_stmt(global, cfn, scope, Stmt::If { condition, then_block, else_block }) => (code, scope, global, cfn))
expr
LineCoverageSource
171✗(type_expr(cfn, scope, expr) => expr_ty)
172✗(let (temp, cfn) = cfn.alloc_temp(&expr_ty)?)
173✗(codegen_expr_into(global, cfn, scope, temp, expr) => (code, global, cfn))
──────── ("expr")
175✗(codegen_stmt(global, cfn, scope, Stmt::Expr { expr }) => (code, scope, global, cfn))
loop
LineCoverageSource
179✗(let label = require_label(label)?)
180N/A(let (loop_start, cfn) = cfn.fresh_bb())
181N/A(let (exit_block, cfn) = cfn.fresh_bb())
182N/A(let scope = scope.with_label(&label.id, Some(loop_start), exit_block))
183✗(codegen_block(global, cfn, scope, body) => (body_code, global, cfn))
184✗(let (code, cfn) = build_loop(cfn, loop_start, exit_block, body_code)?)
──────── ("loop")
186✗(codegen_stmt(global, cfn, scope, Stmt::Loop { label, body }) => (code, scope, global, cfn))
break
LineCoverageSource
190✗(let (_, exit) = scope.lookup_label(label)?)
191N/A(let code = cfn.fresh_code_block())
192N/A(let (code, cfn) = cfn.terminated(code, terminator_goto(exit)))
──────── ("break")
194✗(codegen_stmt(global, cfn, scope, Stmt::Break { label }) => (code, scope, global, cfn))
continue
LineCoverageSource
198✗(let (continue_target, _) = scope.lookup_label(label)?)
199✗(if let Some(start) = continue_target)
200N/A(let code = cfn.fresh_code_block())
201N/A(let (code, cfn) = cfn.terminated(code, terminator_goto(start)))
──────── ("continue")
203✗(codegen_stmt(global, cfn, scope, Stmt::Continue { label }) => (code, scope, global, cfn))
block
LineCoverageSource
207✗(codegen_block(global, cfn, scope, block) => (code, global, cfn))
──────── ("block")
209✗(codegen_stmt(global, cfn, scope, Stmt::Block(block)) => (code, scope, global, cfn))
exists
LineCoverageSource
213✗(let block = instantiate_erased(binder)?)
214✗(codegen_block(global, cfn, scope, block) => (code, global, cfn))
──────── ("exists")
216✗(codegen_stmt(global, cfn, scope, Stmt::Exists { binder }) => (code, scope, global, cfn))