Added support for global variables except for initialization

glang/coq.go

@@ -844,20 +844,6 @@ func (d FuncDecl) Signature() string {
 	return strings.Join(args, " ")
 }
 
-func (d FuncDecl) Type() string {
-	// FIXME: doesn't deal with type parameters
-	types := []string{}
-	for _, a := range d.Args {
-		types = append(types, a.Type.Coq(true))
-	}
-	if len(d.Args) == 0 {
-		types = append(types, TypeIdent("unitT").Coq(true))
-	}
-	types = append(types, d.ReturnType.Coq(true))
-	panic("include RecvArg")
-	// return strings.Join(types, " -> ")
-}
-
 // CoqDecl implements the Decl interface
 //
 // For FuncDecl this emits the Coq vernacular Definition that defines the whole
@@ -957,6 +943,19 @@ func (d MethodSetDecl) DefName() (bool, string) {
 	return true, d.DeclName
 }
 
+type VarDecl struct {
+	DeclName    string
+	VarUniqueId string
+}
+
+func (d VarDecl) CoqDecl() string {
+	return fmt.Sprintf("Definition %s : val := #\"%s\".", d.DeclName, d.VarUniqueId)
+}
+
+func (d VarDecl) DefName() (bool, string) {
+	return true, d.DeclName
+}
+
 // Decl is a FuncDecl, StructDecl, CommentDecl, or ConstDecl
 type Decl interface {
 	CoqDecl() string

goose.go

@@ -553,10 +553,14 @@ func (ctx Ctx) selectorExprAddr(e *ast.SelectorExpr) glang.Expr {
 		if !ok {
 			ctx.unsupported(e, "expected package selector with idtent, got %T", e.X)
 		}
-		ctx.unsupported(e, "address of external package selection")
-		return glang.PackageIdent{
-			Package: pkg,
-			Ident:   e.Sel.Name,
+		if _, ok := ctx.info.ObjectOf(e.Sel).(*types.Var); ok {
+			return glang.NewCallExpr(glang.GallinaIdent("globals.get"),
+				glang.PackageIdent{
+					Package: pkg,
+					Ident:   e.Sel.Name,
+				})
+		} else {
+			ctx.unsupported(e, "address of external package selection that is not a variable")
 		}
 	}
 
@@ -736,7 +740,8 @@ func (ctx Ctx) selectorExpr(e *ast.SelectorExpr) glang.Expr {
 			ctx.unsupported(e, "expected package selector with ident, got %T", e.X)
 		}
 		if _, ok := ctx.info.ObjectOf(e.Sel).(*types.Var); ok {
-			return glang.IdentExpr(fmt.Sprintf("global:%s", e.Sel.Name))
+			ctx.nope(e, "global variable from external package should be handled by exprAddr")
+			// return glang.IdentExpr(fmt.Sprintf("global:%s", e.Sel.Name))
 		} else {
 
 			return ctx.handleImplicitConversion(e,
@@ -1248,8 +1253,7 @@ func (ctx Ctx) identExpr(e *ast.Ident, isSpecial bool) glang.Expr {
 		return ctx.handleImplicitConversion(e, constObj.Type(), ctx.typeOf(e), glang.GallinaIdent(e.Name))
 	}
 	if _, ok := obj.(*types.Var); ok {
-		// is a variable
-		return glang.DerefExpr{X: glang.IdentExpr(e.Name), Ty: ctx.glangType(e, ctx.typeOf(e))}
+		ctx.nope(e, "variable references should get translated via exprAddr")
 	}
 	if _, ok := obj.(*types.Func); ok {
 		// is a function
@@ -1309,7 +1313,11 @@ func (ctx Ctx) derefExpr(e ast.Expr) glang.Expr {
 }
 
 func (ctx Ctx) expr(e ast.Expr) glang.Expr {
-	return ctx.exprSpecial(e, false)
+	if ctx.info.Types[e].Addressable() {
+		return glang.DerefExpr{X: ctx.exprAddr(e), Ty: ctx.glangType(e, ctx.typeOf(e))}
+	} else {
+		return ctx.exprSpecial(e, false)
+	}
 }
 
 func (ctx Ctx) funcLit(e *ast.FuncLit) glang.FuncLit {
@@ -1639,7 +1647,16 @@ func (ctx Ctx) exprAddr(e ast.Expr) glang.Expr {
 	case *ast.ParenExpr:
 		return ctx.exprAddr(e.X)
 	case *ast.Ident:
-		return glang.IdentExpr(e.Name)
+		obj := ctx.info.ObjectOf(e)
+		if _, ok := obj.(*types.Var); ok {
+			if obj.Pkg().Scope() == obj.Parent() {
+				return glang.NewCallExpr(glang.GallinaIdent("globals.get"), glang.GallinaIdent(e.Name))
+			} else {
+				return glang.IdentExpr(e.Name)
+			}
+		} else {
+			ctx.unsupported(e, "exprAddr of ident that is not a var")
+		}
 	case *ast.IndexExpr:
 		targetTy := ctx.typeOf(e.X)
 		switch targetTy := targetTy.Underlying().(type) {
@@ -2294,8 +2311,17 @@ func (ctx Ctx) constDecl(d *ast.GenDecl) []glang.Decl {
 }
 
 func (ctx Ctx) globalVarDecl(d *ast.GenDecl) []glang.Decl {
-	ctx.unsupported(d, "global vars")
-	return nil
+	var decls []glang.Decl
+	for _, spec := range d.Specs {
+		s := spec.(*ast.ValueSpec)
+		for _, name := range s.Names {
+			decls = append(decls, glang.VarDecl{
+				DeclName:    name.Name,
+				VarUniqueId: ctx.pkgPath + "." + name.Name,
+			})
+		}
+	}
+	return decls
 }
 
 func stringLitValue(lit *ast.BasicLit) string {
@@ -2363,3 +2389,15 @@ func (ctx Ctx) maybeDecls(d ast.Decl) []glang.Decl {
 	}
 	return nil
 }
+
+func (ctx Ctx) initFunction() glang.Decl {
+	fd := glang.FuncDecl{Name: "init'"}
+
+	fd.Body = glang.Tt
+
+	for _, init := range ctx.info.InitOrder {
+		ctx.unsupported(init.Rhs, "initializer")
+	}
+
+	return fd
+}

interface.go

@@ -30,6 +30,21 @@ func (ctx Ctx) declsOrError(stmt ast.Decl) (decls []glang.Decl, err error) {
 	return ctx.maybeDecls(stmt), nil
 }
 
+// catching Goose translation errors and returning them as a regular Go error
+func (ctx Ctx) initsOrError() (decls glang.Decl, err error) {
+	defer func() {
+		if r := recover(); r != nil {
+			if gooseErr, ok := r.(gooseError); ok {
+				err = gooseErr.err
+			} else {
+				// r is an error from a non-goose error, indicating a bug
+				panic(r)
+			}
+		}
+	}()
+	return ctx.initFunction(), nil
+}
+
 func filterImports(decls []glang.Decl) (nonImports []glang.Decl, imports glang.ImportDecls) {
 	for _, d := range decls {
 		switch d := d.(type) {
@@ -91,6 +106,16 @@ func (ctx Ctx) decls(fs []*ast.File) (imports glang.ImportDecls, sortedDecls []g
 		}
 	}
 
+	newDecl, err := ctx.initsOrError()
+	if err != nil {
+		errs = append(errs, err)
+	} else {
+		_, name := newDecl.DefName()
+		declNames = append(declNames, name)
+		// declNameToId[newDecl.DefName()] =
+		decls[name] = newDecl
+	}
+
 	// Sort Glang decls based on dependencies
 
 	generated := make(map[string]bool)

testdata/examples/unittest/globals.go

@@ -4,7 +4,7 @@ func foo() uint64 {
 	return 10
 }
 
-var globalX uint64 = foo()
+var GlobalX uint64 = foo()
 var globalY string
 
 func other() {
@@ -13,7 +13,7 @@ func other() {
 
 func bar() {
 	other()
-	if x != 10 || globalY != "ok" {
+	if GlobalX != 10 || globalY != "ok" {
 		panic("bad")
 	}
 }