Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

added channels #49

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

added channels #49

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8b763f5
added channels
jzhang025 Apr 22, 2024
57d523e
some changes
jzhang025 Sep 30, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions go.mod
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,15 @@ require (
github.com/pkg/errors v0.9.1
github.com/stretchr/testify v1.6.1
github.com/tchajed/marshal v0.2.0
golang.org/x/sys v0.0.0-20220319134239-a9b59b0215f8
golang.org/x/tools v0.1.10
golang.org/x/sys v0.6.0
golang.org/x/tools v0.7.0
)

require (
github.com/mattn/go-colorable v0.1.12 // indirect
github.com/mattn/go-isatty v0.0.14 // indirect
github.com/pmezard/go-difflib v1.0.0 // indirect
golang.org/x/mod v0.6.0-dev.0.20220106191415-9b9b3d81d5e3 // indirect
golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1 // indirect
golang.org/x/mod v0.9.0 // indirect
golang.org/x/xerrors v0.0.0-20220907171357-04be3eba64a2 // indirect
gopkg.in/yaml.v3 v3.0.0-20200615113413-eeeca48fe776 // indirect
)
8 changes: 8 additions & 0 deletions go.sum
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,8 @@ github.com/tchajed/marshal v0.2.0 h1:6syf2SG3//AE891aHhj6BS+fv3OCMxFM322x05ot3QE
github.com/tchajed/marshal v0.2.0/go.mod h1:jq2B5uP+QvY51sZB57Td/OsareaZEzm3HVuvVKhC22I=
golang.org/x/mod v0.6.0-dev.0.20220106191415-9b9b3d81d5e3 h1:kQgndtyPBW/JIYERgdxfwMYh3AVStj88WQTlNDi2a+o=
golang.org/x/mod v0.6.0-dev.0.20220106191415-9b9b3d81d5e3/go.mod h1:3p9vT2HGsQu2K1YbXdKPJLVgG5VJdoTa1poYQBtP1AY=
golang.org/x/mod v0.9.0 h1:KENHtAZL2y3NLMYZeHY9DW8HW8V+kQyJsY/V9JlKvCs=
golang.org/x/mod v0.9.0/go.mod h1:iBbtSCu2XBx23ZKBPSOrRkjjQPZFPuis4dIYUhu/chs=
golang.org/x/sys v0.0.0-20190222072716-a9d3bda3a223/go.mod h1:STP8DvDyc/dI5b8T5hshtkjS+E42TnysNCUPdjciGhY=
golang.org/x/sys v0.0.0-20191008105621-543471e840be/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
golang.org/x/sys v0.0.0-20191026070338-33540a1f6037/go.mod h1:h1NjWce9XRLGQEsW7wpKNCjG9DtNlClVuFLEZdDNbEs=
Expand All @@ -56,10 +58,16 @@ golang.org/x/sys v0.0.0-20210630005230-0f9fa26af87c/go.mod h1:oPkhp1MJrh7nUepCBc
golang.org/x/sys v0.0.0-20210927094055-39ccf1dd6fa6/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/sys v0.0.0-20220319134239-a9b59b0215f8 h1:OH54vjqzRWmbJ62fjuhxy7AxFFgoHN0/DPc/UrL8cAs=
golang.org/x/sys v0.0.0-20220319134239-a9b59b0215f8/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/sys v0.6.0 h1:MVltZSvRTcU2ljQOhs94SXPftV6DCNnZViHeQps87pQ=
golang.org/x/sys v0.6.0/go.mod h1:oPkhp1MJrh7nUepCBck5+mAzfO9JrbApNNgaTdGDITg=
golang.org/x/tools v0.1.10 h1:QjFRCZxdOhBJ/UNgnBZLbNV13DlbnK0quyivTnXJM20=
golang.org/x/tools v0.1.10/go.mod h1:Uh6Zz+xoGYZom868N8YTex3t7RhtHDBrE8Gzo9bV56E=
golang.org/x/tools v0.7.0 h1:W4OVu8VVOaIO0yzWMNdepAulS7YfoS3Zabrm8DOXXU4=
golang.org/x/tools v0.7.0/go.mod h1:4pg6aUX35JBAogB10C9AtvVL+qowtN4pT3CGSQex14s=
golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1 h1:go1bK/D/BFZV2I8cIQd1NKEZ+0owSTG1fDTci4IqFcE=
golang.org/x/xerrors v0.0.0-20200804184101-5ec99f83aff1/go.mod h1:I/5z698sn9Ka8TeJc9MKroUUfqBBauWjQqLJ2OPfmY0=
golang.org/x/xerrors v0.0.0-20220907171357-04be3eba64a2 h1:H2TDz8ibqkAF6YGhCdN3jS9O0/s90v0rJh3X/OLHEUk=
golang.org/x/xerrors v0.0.0-20220907171357-04be3eba64a2/go.mod h1:K8+ghG5WaK9qNqU5K3HdILfMLy1f3aNYFI/wnl100a8=
gopkg.in/check.v1 v0.0.0-20161208181325-20d25e280405/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
gopkg.in/check.v1 v1.0.0-20190902080502-41f04d3bba15/go.mod h1:Co6ibVJAznAaIkqp8huTwlJQCZ016jof/cbN4VW5Yz0=
gopkg.in/check.v1 v1.0.0-20200227125254-8fa46927fb4f h1:BLraFXnmrev5lT+xlilqcH8XK9/i0At2xKjWk4p6zsU=
Expand Down
43 changes: 40 additions & 3 deletions goose.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -641,6 +641,9 @@ func (ctx Ctx) makeExpr(args []ast.Expr) coq.CallExpr {
case *types.Map:
return coq.NewCallExpr(coq.GallinaIdent("NewMap"),
ctx.coqTypeOfType(args[0], ty.Elem()), coq.UnitLiteral{})
case *types.Chan:
return coq.NewCallExpr(coq.GallinaIdent("NewChan"),
ctx.coqTypeOfType(args[0], ty.Elem()), ctx.expr(args[1]))
default:
ctx.unsupported(args[0],
"make of should be slice or map, got %v", ty)
Expand Down Expand Up @@ -1013,7 +1016,13 @@ func (ctx Ctx) nilExpr(e *ast.Ident) coq.Expr {
}
}

func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
func (ctx Ctx) receiveExpr(e *ast.UnaryExpr) coq.Expr {
return coq.NewCallExpr(
coq.GallinaIdent("ChannelReceive"),
ctx.expr(e.X))
}

func (ctx Ctx) unaryExpr(e *ast.UnaryExpr, isSpecial bool) coq.Expr {
if e.Op == token.NOT {
return coq.NotExpr{ctx.expr(e.X)}
}
Expand Down Expand Up @@ -1041,6 +1050,13 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
// e is something else
return ctx.refExpr(e.X)
}
if e.Op == token.ARROW {
e2 := ctx.receiveExpr(e)
if !isSpecial {
e2 = coq.NewCallExpr(coq.GallinaIdent("Fst"), e2)
}
return e2
}
ctx.unsupported(e, "unary expression %s", e.Op)
return nil
}
Expand Down Expand Up @@ -1165,7 +1181,7 @@ func (ctx Ctx) exprSpecial(e ast.Expr, isSpecial bool) coq.Expr {
case *ast.IndexExpr:
return ctx.indexExpr(e, isSpecial)
case *ast.UnaryExpr:
return ctx.unaryExpr(e)
return ctx.unaryExpr(e, isSpecial)
case *ast.ParenExpr:
return ctx.expr(e.X)
case *ast.StarExpr:
Expand Down Expand Up @@ -1695,6 +1711,13 @@ func (ctx Ctx) assignFromTo(s ast.Node,
return coq.Binding{}
}

func (ctx Ctx) channelSend(channel ast.Expr, value coq.Expr) coq.Binding {
// assignments can mean various things
return coq.NewAnon(coq.NewCallExpr(
coq.GallinaIdent("ChannelSend"),
ctx.expr(channel), value))
}

func (ctx Ctx) multipleAssignStmt(s *ast.AssignStmt) coq.Binding {
// Translates a, b, c = SomeCall(args)
// into
Expand All @@ -1711,7 +1734,13 @@ func (ctx Ctx) multipleAssignStmt(s *ast.AssignStmt) coq.Binding {
if len(s.Rhs) > 1 {
ctx.unsupported(s, "multiple assignments on right hand side")
}
rhs := ctx.expr(s.Rhs[0])
var rhs coq.Expr
switch s.Rhs[0].(type) {
case *ast.UnaryExpr:
rhs = ctx.exprSpecial(s.Rhs[0], true)
default:
rhs = ctx.expr(s.Rhs[0])
}

if s.Tok != token.ASSIGN {
// This should be invalid Go syntax anyway
Expand Down Expand Up @@ -1779,6 +1808,12 @@ func (ctx Ctx) incDecStmt(stmt *ast.IncDecStmt) coq.Binding {
})
}

func (ctx Ctx) sendStmt(s *ast.SendStmt) coq.Binding {
channel := s.Chan
value := ctx.expr(s.Value)
return ctx.channelSend(channel, value)
}

func (ctx Ctx) spawnExpr(thread ast.Expr) coq.SpawnExpr {
f, ok := thread.(*ast.FuncLit)
if !ok {
Expand Down Expand Up @@ -1861,6 +1896,8 @@ func (ctx Ctx) stmtInBlock(s ast.Stmt, usage ExprValUsage) (coq.Binding, bool) {
ctx.todo(s, "check for switch statement")
case *ast.TypeSwitchStmt:
ctx.todo(s, "check for type switch statement")
case *ast.SendStmt:
binding = ctx.sendStmt(s)
default:
ctx.unsupported(s, "statement")
}
Expand Down
8 changes: 8 additions & 0 deletions internal/coq/coq.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -350,6 +350,14 @@ func (t SliceType) Coq() string {
return fmt.Sprintf("slice.T %s", addParens(t.Value.Coq()))
}

type ChanType struct {
Value Type
}

func (t ChanType) Coq() string {
return fmt.Sprintf("chanT %s", t.Value.Coq())
}

type ArrayType struct {
Len uint64
Elt Type
Expand Down
3 changes: 3 additions & 0 deletions types.go
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -101,6 +101,9 @@ func (ctx Ctx) coqTypeOfType(n ast.Node, t types.Type) coq.Type {
ctx.unsupported(n, "function type")
case *types.Interface:
return coq.InterfaceDecl{Name: ""}
case *types.Chan:
// panic(fmt.Errorf("t.Elem(): %v", n))
return coq.ChanType{ctx.coqTypeOfType(n, t.Elem())}
}
ctx.nope(n, "unknown type %v", t)
return nil // unreachable
Expand Down