Add global vars and init function to axiomgen

axiomgen/goose.go

@@ -49,7 +49,14 @@ func Decl(w io.Writer, info types.Info, d ast.Decl) {
 				}
 			}
 		case token.VAR:
-			// return ctx.globalVarDecl(d)
+			for _, spec := range d.Specs {
+				spec := spec.(*ast.ValueSpec)
+				for _, name := range spec.Names {
+					if name.IsExported() {
+						fmt.Fprintf(w, "Axiom %s : (string * string).\n", name)
+					}
+				}
+			}
 		case token.TYPE:
 			for _, spec := range d.Specs {
 				spec := spec.(*ast.TypeSpec)
@@ -64,3 +71,7 @@ func Decl(w io.Writer, info types.Info, d ast.Decl) {
 	default:
 	}
 }
+
+func InitializeDecl(w io.Writer) {
+	fmt.Fprintf(w, "Axiom initialize' : val.")
+}

cmd/goose_axiom/main.go

@@ -62,6 +62,7 @@ func translate(pkgPatterns []string, outRootDir string, modDir string,
 				axiomgen.Decl(w, *pkg.TypesInfo, d)
 			}
 		}
+		axiomgen.InitializeDecl(w)
 		fmt.Fprintln(w, "\nEnd axioms.")
 		outFile := path.Join(outRootDir, glang.ImportToPath(pkg.PkgPath, pkg.Name))
 		outDir := path.Dir(outFile)