Handle methods more consistently; for a method with a receiver but no

arguments, there is now a BAnon argument expected in the Goose-generated
code. E.g. `m.Lock()` becomes `Mutex__Lock #m #()`. This simplifies the
handling for selectorExprs in Goose and gives more correct semantics to
Goose's translation of code like `f = m.Lock; f()`.

goose.go

@@ -1443,7 +1443,8 @@ func (ctx Ctx) funcDecl(d *ast.FuncDecl) glang.FuncDecl {
 		typeName := namedType.Obj().Name()
 
 		fd.Name = glang.TypeMethod(typeName, d.Name.Name)
-		fd.Args = append(fd.Args, ctx.field(receiver))
+		f := ctx.field(receiver)
+		fd.RecvArg = &f
 	}
 
 	fd.Args = append(fd.Args, ctx.paramList(d.Type.Params)...)
@@ -1457,6 +1458,13 @@ func (ctx Ctx) funcDecl(d *ast.FuncDecl) glang.FuncDecl {
 			Cont:    fd.Body,
 		}
 	}
+	if fd.RecvArg != nil {
+		fd.Body = glang.LetExpr{
+			Names:   []string{fd.RecvArg.Name},
+			ValExpr: glang.RefExpr{Ty: fd.RecvArg.Type, X: glang.IdentExpr(fd.RecvArg.Name)},
+			Cont:    fd.Body,
+		}
+	}
 	fd.Body = glang.NewCallExpr(glang.GallinaIdent("exception_do"), fd.Body)
 	ctx.dep.addName(fd.Name)
 	return fd

interface.go

@@ -226,8 +226,7 @@ func ffiHeaderFooter(ffi string) (header string, footer string) {
 			"Local Coercion Var' s: expr := Var s."
 		footer = "\nEnd code.\n"
 	} else {
-		header += fmt.Sprintf("From Perennial.new_goose_lang Require Import ffi."+
-			"%s_prelude.", ffi)
+		header += fmt.Sprintf("From New Require Import %s_prelude.", ffi)
 	}
 	return
 }

internal/glang/coq.go

@@ -872,6 +872,7 @@ func (e FuncLit) Coq(needs_paren bool) string {
 // FuncDecl declares a function, including its parameters and body.
 type FuncDecl struct {
 	Name       string
+	RecvArg    *FieldDecl
 	Args       []FieldDecl
 	ReturnType Type
 	Body       Expr
@@ -882,11 +883,14 @@ type FuncDecl struct {
 // Signature renders the function declaration's bindings
 func (d FuncDecl) Signature() string {
 	var args []string
+	if d.RecvArg != nil {
+		args = append(args, d.RecvArg.CoqBinder())
+	}
 	for _, a := range d.Args {
 		args = append(args, a.CoqBinder())
 	}
 	if len(args) == 0 {
-		args = []string{"<>"}
+		args = append(args, "<>")
 	}
 	return strings.Join(args, " ")
 }
@@ -901,7 +905,8 @@ func (d FuncDecl) Type() string {
 		types = append(types, TypeIdent("unitT").Coq(true))
 	}
 	types = append(types, d.ReturnType.Coq(true))
-	return strings.Join(types, " -> ")
+	panic("include RecvArg")
+	// return strings.Join(types, " -> ")
 }
 
 // CoqDecl implements the Decl interface
@@ -1010,7 +1015,7 @@ func InterfaceMethod(interfaceName string, methodName string) string {
 }
 
 const importHeader string = `
-From Perennial.new_goose_lang Require Import prelude.
+From New.golang Require Import defn.
 `
 
 // These will not end up in `File.Decls`, they are put into `File.Imports` by `translatePackage`.
@@ -1048,7 +1053,7 @@ func ImportToPath(pkgPath, pkgName string) string {
 
 func (decl ImportDecl) CoqDecl() string {
 	coqImportQualid := strings.ReplaceAll(thisIsBadAndShouldBeDeprecatedGoPathToCoqPath(decl.Path), "/", ".")
-	return fmt.Sprintf("From Goose Require %s.", coqImportQualid)
+	return fmt.Sprintf("From New.code Require %s.", coqImportQualid)
 }
 
 // ImportDecls groups imports into one declaration so they can be printed