Minor fixes

goose-lang · Jan 21, 2025 · 08b3fe7 · 08b3fe7
1 parent 2d7da9f
commit 08b3fe7
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 7 deletions.
diff --git a/namegen/namegen.go b/namegen/namegen.go
@@ -56,7 +56,7 @@ func Package(w io.Writer, pkg *packages.Package) {
 
 	coqPath := strings.ReplaceAll(glang.ThisIsBadAndShouldBeDeprecatedGoPathToCoqPath(pkg.PkgPath), "/", ".")
 	fmt.Fprintf(w, "From New.code Require Import %s.\n", coqPath)
-	fmt.Fprintf(w, "From New.golang Require Import theory.\n\n")
+	fmt.Fprintf(w, "From New.proof Require Export grove_prelude.\n")
 
 	ctx := &Ctx{info: pkg.TypesInfo}
 
@@ -66,7 +66,7 @@ func Package(w io.Writer, pkg *packages.Package) {
 		}
 	}
 
-	fmt.Fprintf(w, "Module %s.\nSection defs.", pkg.Name)
+	fmt.Fprintf(w, "Module %s.\nSection defs.\n", pkg.Name)
 	// emit record for global addrs
 	fmt.Fprintf(w, `Class GlobalAddrs :=
 {
@@ -75,7 +75,9 @@ func Package(w io.Writer, pkg *packages.Package) {
 		fmt.Fprintf(w, "  %s : loc;\n", varName)
 	}
 	fmt.Fprint(w, "}.\n\n")
-	fmt.Fprint(w, "Context `{!GlobalAddrs}.\n\n")
+	fmt.Fprint(w, "Context `{!GlobalAddrs}.\n")
+	fmt.Fprint(w, "Context `{!heapGS Σ}.\n")
+	fmt.Fprint(w, "Context `{!goGlobalsGS Σ}.\n\n")
 
 	// emit `var_addrs` which converts GlobalAddrs into alist
 	fmt.Fprint(w, "Definition var_addrs `{!GlobalAddrs} : list (go_string * loc) := [")
@@ -112,20 +114,20 @@ Definition is_defined := is_global_definitions %s.pkg_name' var_addrs %s.functio
 		for i := range goMset.Len() {
 			methodName := goMset.At(i).Obj().Name()
 			fmt.Fprintf(w, "\nGlobal Instance wp_method_call_%s_%s : \n", typeName, methodName)
-			fmt.Fprintf(w, "  WpMethodCall %s.pkg_name' \"%s\" \"%s\" _ is_defined.\n",
+			fmt.Fprintf(w, "  WpMethodCall %s.pkg_name' \"%s\" \"%s\" _ is_defined :=\n",
 				pkg.Name, typeName, methodName)
+			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
 			// XXX: by using an ltac expression to generate the instance, we can
 			// leave an evar for the method val, avoiding the need to write out
 			// the promoted methods.
-			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
 		}
 
 		typeName = namedType.Obj().Name() + "'ptr"
 		goMset = types.NewMethodSet(types.NewPointer(namedType))
 		for i := range goMset.Len() {
 			methodName := goMset.At(i).Obj().Name()
 			fmt.Fprintf(w, "\nGlobal Instance wp_method_call_%s_%s : \n", typeName, methodName)
-			fmt.Fprintf(w, "  WpMethodCall %s.pkg_name' \"%s\" \"%s\" _ is_defined.\n",
+			fmt.Fprintf(w, "  WpMethodCall %s.pkg_name' \"%s\" \"%s\" _ is_defined :=\n",
 				pkg.Name, typeName, methodName)
 			fmt.Fprintf(w, "  ltac:(apply wp_method_call'; reflexivity).\n")
 		}

diff --git a/recordgen/recordgen.go b/recordgen/recordgen.go
@@ -223,7 +223,7 @@ func Package(w io.Writer, pkg *packages.Package) {
 
 	// print in sorted order, printing error if there's a cycle
 	for _, imp := range ctx.importsList {
-		fmt.Fprintf(w, "From New.proof.structs Require %s.\n", imp)
+		fmt.Fprintf(w, "From New.generatedproof.structs Require %s.\n", imp)
 	}
 	fmt.Fprintf(w, "Axiom falso : False.\n\n") // FIXME: get rid of this
 	var printingOrdered []string