Change prelude to include channel model.

To make this work, I had to split the current prelude.v into "base_prelude" and "translated_prelude", where "base_prelude" will contain the current prelude and "translated_prelude" will include the channel model as well as any future features that are modeled as goose compatible go code.

goose.go

@@ -27,6 +27,14 @@ import (
 	"golang.org/x/tools/go/packages"
 )
 
+const preludeImport string = `
+From Perennial.goose_lang Require Import prelude.
+`
+
+const basePreludeImport string = `
+From Perennial.goose_lang Require Import base_prelude.
+`
+
 // Ctx is a context for resolving Go code's types and source code
 type Ctx struct {
 	idents  identCtx
@@ -58,7 +66,8 @@ const (
 // PkgConfig holds package configuration for Coq conversion
 type PkgConfig struct {
 	TranslationConfig
-	Ffi string
+	Ffi     string
+	Prelude string
 }
 
 func getFfi(pkg *packages.Package) string {
@@ -88,12 +97,21 @@ func getFfi(pkg *packages.Package) string {
 	return "none"
 }
 
+// Get the prelude import, which in most cases will include both the base prelude and the prelude for translated Go models. When we are translating the Go models themselves, we include only the base prelude so we don't create a circular dependency.
+func getPrelude(pkgPath string) string {
+	if isTranslatedPreludeFile[pkgPath] {
+		return basePreludeImport
+	}
+	return preludeImport
+}
+
 // NewPkgCtx initializes a context based on a properly loaded package
 func NewPkgCtx(pkg *packages.Package, tr TranslationConfig) Ctx {
 	// Figure out which FFI we're using
 	config := PkgConfig{
 		TranslationConfig: tr,
 		Ffi:               getFfi(pkg),
+		Prelude:           getPrelude(pkg.PkgPath),
 	}
 
 	return Ctx{
@@ -2140,6 +2158,10 @@ var ffiMapping = map[string]string{
 	"github.com/goose-lang/primitive/async_disk":     "async_disk",
 }
 
+var isTranslatedPreludeFile = map[string]bool{
+	"github.com/goose-lang/goose/channel": true,
+}
+
 func (ctx Ctx) imports(d []ast.Spec) []coq.Decl {
 	var decls []coq.Decl
 	for _, s := range d {

interface.go

@@ -201,7 +201,10 @@ func (tr TranslationConfig) translatePackage(pkg *packages.Package) (coq.File, e
 		PkgPath:   pkg.PkgPath,
 		GoPackage: pkg.Name,
 	}
-	coqFile.ImportHeader, coqFile.Footer = ffiHeaderFooter(ctx.PkgConfig.Ffi)
+	coqFile.CodeHeader, coqFile.CodeFooter = codeHeaderFooter(ctx.PkgConfig.Ffi, isTranslatedPreludeFile[coqFile.PkgPath])
+	coqFile.TranslatedModelHeader, coqFile.TranslatedModelFooter = translatedModelHeaderFooter(isTranslatedPreludeFile[coqFile.PkgPath])
+	coqFile.FfiHeader = ffiHeaderFooter(ctx.PkgConfig.Ffi)
+	coqFile.Prelude = ctx.PkgConfig.Prelude
 
 	imports, decls, errs := ctx.Decls(files...)
 	coqFile.Imports = imports
@@ -213,14 +216,35 @@ func (tr TranslationConfig) translatePackage(pkg *packages.Package) (coq.File, e
 	return coqFile, nil
 }
 
-func ffiHeaderFooter(ffi string) (header string, footer string) {
-	if ffi == "none" {
+func ffiHeaderFooter(ffi string) string {
+	if ffi != "none" {
+		return fmt.Sprintf("From Perennial.goose_lang Require Import ffi."+
+			"%s_prelude.", ffi)
+	}
+	return ""
+}
+
+func codeHeaderFooter(ffi string, isTranslatedPreludeFile bool) (header string, footer string) {
+	if ffi == "none" && !isTranslatedPreludeFile {
 		header = "Section code.\n" +
 			"Context `{ext_ty: ext_types}."
 		footer = "\nEnd code.\n"
 	} else {
-		header = fmt.Sprintf("From Perennial.goose_lang Require Import ffi."+
-			"%s_prelude.", ffi)
+		header = ""
+		footer = ""
+	}
+	return
+}
+
+func translatedModelHeaderFooter(isTranslatedPreludeFile bool) (header string, footer string) {
+	fmt.Println(isTranslatedPreludeFile)
+	if isTranslatedPreludeFile {
+		header = "Section goose_lang.\n" +
+			"Context `{ext_ty: ext_types}."
+		footer = "\nEnd goose_lang.\n"
+	} else {
+		header = ""
+		footer = ""
 	}
 	return
 }

internal/coq/coq.go

@@ -1147,10 +1147,6 @@ func InterfaceMethodName(interfaceName string, funcName string) string {
 	return fmt.Sprintf("(struct.get %s \"%s\")", interfaceName, funcName)
 }
 
-const importHeader string = `
-From Perennial.goose_lang Require Import prelude.
-`
-
 // These will not end up in `File.Decls`, they are put into `File.Imports` by `translatePackage`.
 type ImportDecl struct {
 	Path    string
@@ -1206,12 +1202,16 @@ func (decls ImportDecls) PrintImports() string {
 
 // File represents a complete Coq file (a sequence of declarations).
 type File struct {
-	ImportHeader string
-	Footer       string
-	PkgPath      string
-	GoPackage    string
-	Imports      ImportDecls
-	Decls        []Decl
+	Prelude               string
+	CodeHeader            string
+	CodeFooter            string
+	TranslatedModelHeader string
+	TranslatedModelFooter string
+	FfiHeader             string
+	PkgPath               string
+	GoPackage             string
+	Imports               ImportDecls
+	Decls                 []Decl
 }
 
 func (f File) autogeneratedNotice() CommentDecl {
@@ -1223,12 +1223,20 @@ func (f File) autogeneratedNotice() CommentDecl {
 // noinspection GoUnhandledErrorResult
 func (f File) Write(w io.Writer) {
 	fmt.Fprintln(w, f.autogeneratedNotice().CoqDecl())
-	fmt.Fprintln(w, strings.Trim(importHeader, "\n"))
+	fmt.Fprintln(w, strings.Trim(f.Prelude, "\n"))
 	fmt.Fprintln(w, f.Imports.PrintImports())
 	if len(f.Imports) > 0 {
 		fmt.Fprintln(w)
 	}
-	fmt.Fprintln(w, f.ImportHeader)
+	if len(f.CodeHeader) > 0 {
+		fmt.Fprintln(w, f.CodeHeader)
+	}
+	if len(f.TranslatedModelHeader) > 0 {
+		fmt.Fprintln(w, f.TranslatedModelHeader)
+	}
+	if len(f.FfiHeader) > 0 {
+		fmt.Fprintln(w, f.FfiHeader)
+	}
 	fmt.Fprintln(w)
 	decls := make(map[string]bool)
 	for i, d := range f.Decls {
@@ -1245,5 +1253,10 @@ func (f File) Write(w io.Writer) {
 			}
 		}
 	}
-	fmt.Fprint(w, f.Footer)
+	if len(f.CodeFooter) > 0 {
+		fmt.Fprint(w, f.CodeFooter)
+	}
+	if len(f.TranslatedModelFooter) > 0 {
+		fmt.Fprint(w, f.TranslatedModelFooter)
+	}
 }