Skip to content

Commit

Permalink
Revert "add dep on all idents, regardless of IsMacro"
Browse files Browse the repository at this point in the history
This reverts commit 952b944.
  • Loading branch information
sanjit-bhat committed Jun 26, 2024
1 parent 952b944 commit b2ae939
Show file tree
Hide file tree
Showing 2 changed files with 14 additions and 14 deletions.
2 changes: 1 addition & 1 deletion goose.go
Original file line number Diff line number Diff line change
Expand Up @@ -1070,8 +1070,8 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {

func (ctx Ctx) variable(s *ast.Ident) coq.Expr {
info := ctx.identInfo(s)
ctx.dep.addDep(s.Name)
if info.IsMacro {
ctx.dep.addDep(s.Name)
return coq.GallinaIdent(s.Name)
}
e := coq.IdentExpr(s.Name)
Expand Down
26 changes: 13 additions & 13 deletions internal/examples/simpledb/simpledb.gold.v
Original file line number Diff line number Diff line change
Expand Up @@ -94,19 +94,6 @@ Definition lazyFileBuf := struct.decl [
"next" :: slice.T byteT
].

Definition bufFile := struct.decl [
"file" :: fileT;
"buf" :: ptrT
].

Definition newBuf: val :=
rec: "newBuf" "f" :=
let: "buf" := ref (zero_val (slice.T byteT)) in
struct.mk bufFile [
"file" ::= "f";
"buf" ::= "buf"
].

(* readTableIndex parses a complete table on disk into a key->offset index *)
Definition readTableIndex: val :=
rec: "readTableIndex" "f" "index" :=
Expand Down Expand Up @@ -176,6 +163,19 @@ Definition tableRead: val :=
let: "p" := readValue (struct.get Table "File" "t") "off" in
("p", #true)).

Definition bufFile := struct.decl [
"file" :: fileT;
"buf" :: ptrT
].

Definition newBuf: val :=
rec: "newBuf" "f" :=
let: "buf" := ref (zero_val (slice.T byteT)) in
struct.mk bufFile [
"file" ::= "f";
"buf" ::= "buf"
].

Definition bufFlush: val :=
rec: "bufFlush" "f" :=
let: "buf" := ![slice.T byteT] (struct.get bufFile "buf" "f") in
Expand Down

0 comments on commit b2ae939

Please sign in to comment.