Add the usual dependency ordering stuff

recordgen/recordgen.go

@@ -6,13 +6,14 @@ import (
 	"go/token"
 	"go/types"
 	"io"
+	"log"
 	"strings"
 
 	"github.com/goose-lang/goose/glang"
 	"golang.org/x/tools/go/packages"
 )
 
-func toCoqType(t types.Type) string {
+func (ctx *Ctx) toCoqType(t types.Type) string {
 	switch t := t.(type) {
 	case *types.Basic:
 		switch t.Name() {
@@ -44,9 +45,13 @@ func toCoqType(t types.Type) string {
 	case *types.Named:
 		u := t.Underlying()
 		if _, ok := u.(*types.Struct); ok {
-			return t.String() + ".t"
+			if ctx.pkgPath == t.Obj().Pkg().Path() {
+				return t.Obj().Name() + ".t"
+			} else {
+				return fmt.Sprintf("%s.%s.t", t.Obj().Pkg().Name(), t.Obj().Name())
+			}
 		}
-		return toCoqType(u)
+		return ctx.toCoqType(u)
 	}
 	panic(fmt.Sprint("Unknown type", t))
 }
@@ -58,25 +63,56 @@ func toCoqName(n string) string {
 	return n
 }
 
-func Decl(w io.Writer, info types.Info, d ast.Decl) {
+type Ctx struct {
+	pkgPath string
+
+	deps        map[string][]string
+	currentName string
+	defs        map[string]string
+	defNames    []string
+}
+
+func (ctx *Ctx) setCurrent(s string) {
+	if ctx.currentName != "" {
+		panic("recordgen: setting currentName before unsetting")
+	}
+	ctx.currentName = s
+}
+
+func (ctx *Ctx) unsetCurrent() {
+	ctx.currentName = ""
+}
+
+func (ctx *Ctx) addDep(s string) {
+	ctx.deps[ctx.currentName] = append(ctx.deps[ctx.currentName], s)
+}
+
+func (ctx *Ctx) Decl(info types.Info, d ast.Decl) {
 	switch d := d.(type) {
 	case *ast.FuncDecl:
 	case *ast.GenDecl:
 		switch d.Tok {
 		case token.TYPE:
 			for _, spec := range d.Specs {
 				spec := spec.(*ast.TypeSpec)
+				defName := spec.Name.Name + ".t"
+				ctx.setCurrent(defName)
+				defer ctx.unsetCurrent()
+
 				if s, ok := info.TypeOf(spec.Type).(*types.Struct); ok {
 					// Emit record type
 					fieldVals := new(strings.Builder)
 					for i := 0; i < s.NumFields(); i++ {
+						t := ctx.toCoqType(s.Field(i).Type())
+						ctx.addDep(t)
 						fmt.Fprintf(fieldVals, "  %s : %s;\n",
-							s.Field(i).Name(),
-							toCoqType(s.Field(i).Type()),
+							toCoqName(s.Field(i).Name()),
+							t,
 						)
 					}
 
-					fmt.Fprintf(w, `
+					ctx.defNames = append(ctx.defNames, defName)
+					ctx.defs[defName] = fmt.Sprintf(`
 Module %s.
 Record t := mk {
 %s}.
@@ -92,14 +128,48 @@ End %s.
 
 func Package(w io.Writer, pkg *packages.Package) {
 	fmt.Fprintf(w, "(* autogenerated by goose record generator; do not modify *)\n")
-	// FIXME: import package code
 	coqPath := strings.ReplaceAll(glang.ThisIsBadAndShouldBeDeprecatedGoPathToCoqPath(pkg.PkgPath), "/", ".")
 	fmt.Fprintf(w, "From New.code Require %s.\n", coqPath)
 	fmt.Fprintf(w, "From New.golang Require Import theory.\n\n")
 
+	ctx := &Ctx{
+		deps:    make(map[string][]string),
+		defs:    make(map[string]string),
+		pkgPath: pkg.PkgPath,
+	}
 	for _, f := range pkg.Syntax {
 		for _, d := range f.Decls {
-			Decl(w, *pkg.TypesInfo, d)
+			ctx.Decl(*pkg.TypesInfo, d)
+		}
+	}
+
+	// print in sorted order, printing error if there's a cycle
+	var printingOrdered []string
+	printing := make(map[string]bool)
+	printed := make(map[string]bool)
+	var printDefAndDeps func(string)
+
+	printDefAndDeps = func(n string) {
+		if printed[n] {
+			return
+		} else if printing[n] {
+			log.Fatal("Found a cyclic dependency: ", printingOrdered)
 		}
+
+		printingOrdered = append(printingOrdered, n)
+		printing[n] = true
+		defer func() {
+			printingOrdered = printingOrdered[:len(printingOrdered)-1]
+			delete(printing, n)
+		}()
+
+		for _, depName := range ctx.deps[n] {
+			printDefAndDeps(depName)
+		}
+		fmt.Fprintf(w, ctx.defs[n])
+		printed[n] = true
+	}
+	for _, d := range ctx.defNames {
+		printDefAndDeps(d)
 	}
 }