Skip to content

Commit

Permalink
Support if statement init
Browse files Browse the repository at this point in the history
  • Loading branch information
upamanyus committed Aug 4, 2024
1 parent 6812153 commit 16022bf
Show file tree
Hide file tree
Showing 3 changed files with 66 additions and 2 deletions.
4 changes: 2 additions & 2 deletions goose.go
Original file line number Diff line number Diff line change
Expand Up @@ -1180,14 +1180,14 @@ func (ctx Ctx) ifStmt(s *ast.IfStmt, cont glang.Expr) glang.Expr {
if s.Else != nil {
elseExpr = ctx.stmt(s.Else, glang.Tt)
}
ife := glang.IfExpr{
var ife glang.Expr = glang.IfExpr{
Cond: ctx.expr(s.Cond),
Then: ctx.blockStmt(s.Body),
Else: elseExpr,
}

if s.Init != nil {
ctx.unsupported(s.Init, "if statement initializations")
ife = glang.ParenExpr{Inner: ctx.stmt(s.Init, ife)}
}
return glang.LetExpr{ValExpr: ife, Cont: cont}
}
Expand Down
18 changes: 18 additions & 0 deletions testdata/examples/unittest/control_flow.go
Original file line number Diff line number Diff line change
Expand Up @@ -55,3 +55,21 @@ func elseIf(x, y bool) uint64 {
return 2
}
}

func ifStmtInitialization(x uint64) uint64 {
f := func() uint64 {
return x
}

if f(); x == 2 {
} else if z := x; z == 1 {
} else if y := 94; y == 30 {
} else if z = 10; x == 30 {
}

if y := uint64(10); x == 0 {
return y
} else {
return y - 1
}
}
46 changes: 46 additions & 0 deletions testdata/examples/unittest/unittest.gold.v
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,52 @@ Definition elseIf : val :=
#());;;
do: #()).

(* go: control_flow.go:59:6 *)
Definition ifStmtInitialization : val :=
rec: "ifStmtInitialization" "x" :=
exception_do (let: "x" := ref_ty uint64T "x" in
let: "f" := ref_ty funcT (zero_val funcT) in
let: "$r0" := (λ: <>,
return: (![uint64T] "x");;;
do: #()
) in
do: ("f" <-[funcT] "$r0");;;
(do: ((![funcT] "f") #());;;
(if: (![uint64T] "x") = #2
then do: #()
else
(let: "z" := ref_ty uint64T (zero_val uint64T) in
let: "$r0" := ![uint64T] "x" in
do: ("z" <-[uint64T] "$r0");;;
(if: (![uint64T] "z") = #1
then do: #()
else
(let: "y" := ref_ty intT (zero_val intT) in
let: "$r0" := #94 in
do: ("y" <-[intT] "$r0");;;
(if: (![intT] "y") = #30
then do: #()
else
(let: "$r0" := #10 in
do: ("z" <-[uint64T] "$r0");;;
(if: (![uint64T] "x") = #30
then do: #()
else do: #()));;;
#()));;;
#()));;;
#()));;;
(let: "y" := ref_ty uint64T (zero_val uint64T) in
let: "$r0" := #10 in
do: ("y" <-[uint64T] "$r0");;;
(if: (![uint64T] "x") = #0
then
return: (![uint64T] "y");;;
do: #()
else
return: ((![uint64T] "y") - #1);;;
do: #()));;;
do: #()).

Definition stringWrapper : go_type := stringT.

Definition stringWrapper__mset : list (string * val) := [
Expand Down

0 comments on commit 16022bf

Please sign in to comment.