Handle machine vs primitive in one more place

Author: tchajed

go.mod

@@ -1,6 +1,6 @@
 module github.com/goose-lang/goose
 
-go 1.21
+go 1.22
 
 require (
 	github.com/fatih/color v1.17.0
@@ -13,6 +13,7 @@ require (
 
 require (
 	github.com/davecgh/go-spew v1.1.1 // indirect
+	github.com/goose-lang/primitive v0.1.0
 	github.com/goose-lang/std v0.3.2 // indirect
 	github.com/mattn/go-colorable v0.1.13 // indirect
 	github.com/mattn/go-isatty v0.0.20 // indirect

go.sum

@@ -2,6 +2,8 @@ github.com/davecgh/go-spew v1.1.1 h1:vj9j/u1bqnvCEfJOwUhtlOARqs3+rkHYY13jYWTU97c
 github.com/davecgh/go-spew v1.1.1/go.mod h1:J7Y8YcW2NihsgmVo/mv3lAwl/skON4iLHjSsI+c5H38=
 github.com/fatih/color v1.17.0 h1:GlRw1BRJxkpqUCBKzKOw098ed57fEsKeNjpTe3cSjK4=
 github.com/fatih/color v1.17.0/go.mod h1:YZ7TlrGPkiz6ku9fK3TLD/pl3CpsiFyu8N92HLgmosI=
+github.com/goose-lang/primitive v0.1.0 h1:JReOdFzUdGD7f8nWTC/uOlNpBdVFU4q8HzMSgn8edaY=
+github.com/goose-lang/primitive v0.1.0/go.mod h1:sDE72zVH81ASwPXc1m9OgSfaaY0aZHu4Ty19FgONpOc=
 github.com/goose-lang/std v0.3.2 h1:dYnOsrrbfSG5Bx/rE/X2PylIX6ObTavUosXqzbIzRys=
 github.com/goose-lang/std v0.3.2/go.mod h1:0IoDUCIC80Msc7h/SqpbZY1ytjhV39rgKnyHG/tjdis=
 github.com/kr/text v0.2.0 h1:5Nx0Ya0ZqY2ygV366QzturHI13Jq95ApcVaJBhpS+AY=

goose.go

@@ -368,7 +368,7 @@ func (ctx Ctx) prophIdMethod(f *ast.SelectorExpr, args []ast.Expr) coq.CallExpr
 	case "ResolveBool", "ResolveU64":
 		return ctx.newCoqCall("ResolveProph", callArgs)
 	default:
-		ctx.unsupported(f, "method %s of machine.ProphId", f.Sel.Name)
+		ctx.unsupported(f, "method %s of primitive.ProphId", f.Sel.Name)
 		return coq.CallExpr{}
 	}
 }
@@ -411,7 +411,7 @@ func (ctx Ctx) packageMethod(f *ast.SelectorExpr,
 		case "NewProph":
 			return ctx.newCoqCall("NewProph", args)
 		default:
-			ctx.futureWork(f, "unhandled call to machine.%s", f.Sel.Name)
+			ctx.futureWork(f, "unhandled call to primitive.%s", f.Sel.Name)
 			return coq.CallExpr{}
 		}
 	}

machine/prims.go

@@ -10,6 +10,8 @@ import (
 	"os"
 	"sync"
 	"time"
+
+	"github.com/goose-lang/primitive"
 )
 
 // UInt64Get converts the first 8 bytes of p to a uint64.
@@ -96,22 +98,7 @@ func Exit(n uint64) {
 // Not provided by sync.Cond, so we have to (inefficiently) implement this
 // ourselves.
 func WaitTimeout(cond *sync.Cond, timeoutMs uint64) {
-	done := make(chan struct{})
-	go func() {
-		cond.Wait()
-		cond.L.Unlock()
-		close(done)
-	}()
-	select {
-	case <-time.After(time.Duration(timeoutMs) * time.Millisecond):
-		// timed out
-		cond.L.Lock()
-		return
-	case <-done:
-		// Wait returned
-		cond.L.Lock()
-		return
-	}
+	primitive.WaitTimeout(cond, timeoutMs)
 }
 
 func TimeNow() uint64 {

machine/proph.go

@@ -1,19 +1,11 @@
 package machine
 
-// Prophecy variables.
-//
-// We represent the name of a prophecy variable via an opaque type. In Go, it
-// does not actually carry any data, but in GooseLang we store the ProphId.
-// However, making a type opaque in Go seems to be tricky. Let's hope adding a
-// private field helps.
-//
-//lint:ignore U1000 p is unused, see above comment.
-type prophId struct{ p struct{} }
-type ProphId = *prophId
+// Wrap goose-lang/primitive for backwards compatibility
+
+import "github.com/goose-lang/primitive"
+
+type ProphId = primitive.ProphId
 
 func NewProph() ProphId {
-	return &prophId{}
+	return primitive.NewProph()
 }
-
-func (p ProphId) ResolveBool(b bool)  {}
-func (p ProphId) ResolveU64(i uint64) {}

types.go

@@ -249,7 +249,7 @@ func isProphId(t types.Type) bool {
 	if t, ok := t.(*types.Pointer); ok {
 		if t, ok := t.Elem().(*types.Named); ok {
 			name := t.Obj()
-			return name.Pkg().Name() == "machine" &&
+			return (name.Pkg().Name() == "machine" || name.Pkg().Name() == "primitive") &&
 				name.Name() == "prophId"
 		}
 	}
@@ -275,7 +275,7 @@ func isString(t types.Type) bool {
 func isDisk(t types.Type) bool {
 	if t, ok := t.(*types.Named); ok {
 		obj := t.Obj()
-		if obj.Pkg().Path() == "github.com/goose-lang/goose/machine/disk" &&
+		if (obj.Pkg().Path() == "github.com/goose-lang/goose/machine/disk" || obj.Pkg().Path() == "github.com/goose-lang/primitive/disk") &&
 			obj.Name() == "Disk" {
 			return true
 		}