max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/init/lean/ir): allow uint32 in case instruction

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-10 12:56:55 -07:00
parent ad61772c72
commit 552ca3bb11
2 changed files with 13 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
library/init/lean/ir/extract_cpp.lean
View file

@ -98,12 +98,18 @@ def emit_cases : list blockid → nat → extract_m unit
def emit_case : var → list blockid → extract_m unit
| x [b] := emit "goto " >> emit_blockid b >> emit_eos
| x [b₁,b₂] :=
do env ← read,
if env.ctx.find x = some type.bool
then emit "if (" >> emit_var x >> emit ") goto " >> emit_blockid b₂ >> emit "; else goto " >> emit_blockid b₁ >> emit_eos
else emit "if (" >> emit_tag x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂ >> emit_eos
| x bs := emit "switch (" >> emit_tag x >> emit ") {" >> emit_cases bs 0 >> emit "}" >> emit_line
| x [b₁,b₂] := do
env ← read,
(match env.ctx.find x with
| some type.bool := emit "if (" >> emit_var x >> emit ") goto " >> emit_blockid b₂ >> emit "; else goto " >> emit_blockid b₁
| some type.uint32 := emit "if (" >> emit_var x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂
| _ := emit "if (" >> emit_tag x >> emit " == 0) goto " >> emit_blockid b₁ >> emit "; else goto " >> emit_blockid b₂),
emit_eos
| x bs := do
env ← read,
emit "switch ",
paren (if env.ctx.find x = some type.uint32 then emit_var x else emit_tag x),
emit " {" >> emit_line >> emit_cases bs 0 >> emit "}" >> emit_line
def emit_terminator (term : terminator) : extract_m unit :=
term.decorate_error $

2
library/init/lean/ir/type_check.lean
View file

@ -210,7 +210,7 @@ def terminator.check (term : terminator) : type_checker_m unit :=
term.decorate_error $
match term with
| (terminator.ret ys) := do (_, rs) ← read, check_result_types ys rs
| (terminator.case x _) := do t ← get_type x, unless (t = type.object || t = type.bool) $ throw "variable must be an object or bool"
| (terminator.case x _) := do t ← get_type x, unless (t = type.object || t = type.bool || t = type.uint32) $ throw "variable must be an object, uint32 or bool"
| (terminator.jmp _) := return ()
def block.check (b : block) : type_checker_m unit :=