change the way we handle ident info. only stateful info is ptr wrappe…

…d idents. dynamically compute isGlobalVar and isStruct, both of which were implicit in complicated isMacro.

goose.go

@@ -176,10 +176,6 @@ func (ctx Ctx) paramList(fs *ast.FieldList) []coq.FieldDecl {
 				Name: name.Name,
 				Type: ty,
 			})
-			ctx.addDef(name, identInfo{
-				IsPtrWrapped: false,
-				IsMacro:      false,
-			})
 		}
 		if len(f.Names) == 0 { // Unnamed parameter
 			decls = append(decls, coq.FieldDecl{
@@ -253,10 +249,6 @@ func (ctx Ctx) typeDecl(doc *ast.CommentGroup, spec *ast.TypeSpec) coq.Decl {
 	}
 	switch goTy := spec.Type.(type) {
 	case *ast.StructType:
-		ctx.addDef(spec.Name, identInfo{
-			IsPtrWrapped: false,
-			IsMacro:      false,
-		})
 		ty := coq.StructDecl{
 			Name: spec.Name.Name,
 		}
@@ -265,10 +257,6 @@ func (ctx Ctx) typeDecl(doc *ast.CommentGroup, spec *ast.TypeSpec) coq.Decl {
 		ty.Fields = ctx.structFields(goTy.Fields)
 		return ty
 	case *ast.InterfaceType:
-		ctx.addDef(spec.Name, identInfo{
-			IsPtrWrapped: false,
-			IsMacro:      false,
-		})
 		ty := coq.InterfaceDecl{
 			Name: spec.Name.Name,
 		}
@@ -277,10 +265,6 @@ func (ctx Ctx) typeDecl(doc *ast.CommentGroup, spec *ast.TypeSpec) coq.Decl {
 		ty.Methods = ctx.structFields(goTy.Methods)
 		return ty
 	default:
-		ctx.addDef(spec.Name, identInfo{
-			IsPtrWrapped: false,
-			IsMacro:      true,
-		})
 		if spec.Assign == 0 {
 			return coq.TypeDef{
 				Name: spec.Name.Name,
@@ -1069,13 +1053,12 @@ func (ctx Ctx) unaryExpr(e *ast.UnaryExpr) coq.Expr {
 }
 
 func (ctx Ctx) variable(s *ast.Ident) coq.Expr {
-	info := ctx.identInfo(s)
-	if info.IsMacro {
+	if ctx.isGlobalVar(s) {
 		ctx.dep.addDep(s.Name)
 		return coq.GallinaIdent(s.Name)
 	}
 	e := coq.IdentExpr(s.Name)
-	if info.IsPtrWrapped {
+	if ctx.isPtrWrapped(s) {
 		return coq.DerefExpr{X: e, Ty: ctx.coqTypeOfType(s, ctx.typeOf(s))}
 	}
 	return e
@@ -1416,9 +1399,7 @@ func (ctx Ctx) forStmt(s *ast.ForStmt) coq.ForLoopExpr {
 	var ident *ast.Ident
 	if s.Init != nil {
 		ident, _ = ctx.loopVar(s.Init)
-		ctx.addDef(ident, identInfo{
-			IsPtrWrapped: true,
-		})
+		ctx.setPtrWrapped(ident)
 		init = ctx.stmt(s.Init)
 	}
 	var cond coq.Expr = coq.True
@@ -1487,18 +1468,6 @@ func (ctx Ctx) identBinder(id *ast.Ident) coq.Binder {
 func (ctx Ctx) sliceRangeStmt(s *ast.RangeStmt) coq.Expr {
 	key := getIdentOrNil(s.Key)
 	val := getIdentOrNil(s.Value)
-	if key != nil {
-		ctx.addDef(key, identInfo{
-			IsPtrWrapped: false,
-			IsMacro:      false,
-		})
-	}
-	if val != nil {
-		ctx.addDef(val, identInfo{
-			IsPtrWrapped: false,
-			IsMacro:      false,
-		})
-	}
 	return coq.SliceLoopExpr{
 		Key:   ctx.identBinder(key),
 		Val:   ctx.identBinder(val),
@@ -1545,12 +1514,6 @@ func (ctx Ctx) defineStmt(s *ast.AssignStmt) coq.Binding {
 	for _, lhsExpr := range s.Lhs {
 		if ident, ok := lhsExpr.(*ast.Ident); ok {
 			idents = append(idents, ident)
-			if !ctx.doesDefHaveInfo(ident) {
-				ctx.addDef(ident, identInfo{
-					IsPtrWrapped: false,
-					IsMacro:      false,
-				})
-			}
 		} else {
 			ctx.nope(lhsExpr, "defining a non-identifier")
 		}
@@ -1562,7 +1525,7 @@ func (ctx Ctx) defineStmt(s *ast.AssignStmt) coq.Binding {
 	// NOTE: this checks whether the identifier being defined is supposed to be
 	// 	pointer wrapped, so to work correctly the caller must set this identInfo
 	// 	before processing the defining expression.
-	if len(idents) == 1 && ctx.definesPtrWrapped(idents[0]) {
+	if len(idents) == 1 && ctx.isPtrWrapped(idents[0]) {
 		return coq.Binding{Names: names, Expr: ctx.referenceTo(rhs)}
 	} else {
 		return coq.Binding{Names: names, Expr: ctx.exprSpecial(rhs, len(idents) == 2)}
@@ -1574,10 +1537,7 @@ func (ctx Ctx) varSpec(s *ast.ValueSpec) coq.Binding {
 		ctx.unsupported(s, "multiple declarations in one block")
 	}
 	lhs := s.Names[0]
-	ctx.addDef(lhs, identInfo{
-		IsPtrWrapped: true,
-		IsMacro:      false,
-	})
+	ctx.setPtrWrapped(lhs)
 	var rhs coq.Expr
 	if len(s.Values) == 0 {
 		ty := ctx.typeOf(lhs)
@@ -1666,7 +1626,7 @@ func (ctx Ctx) assignFromTo(s ast.Node,
 		if lhs.Name == "_" {
 			return coq.NewAnon(rhs)
 		}
-		if ctx.identInfo(lhs).IsPtrWrapped {
+		if ctx.isPtrWrapped(lhs) {
 			return ctx.pointerAssign(lhs, rhs)
 		}
 		ctx.unsupported(s, "variable %s is not assignable\n\t(declare it with 'var' to pointer-wrap in GooseLang and support re-assignment)", lhs.Name)
@@ -1809,7 +1769,7 @@ func (ctx Ctx) incDecStmt(stmt *ast.IncDecStmt) coq.Binding {
 		ctx.todo(stmt, "cannot inc/dec non-var")
 		return coq.Binding{}
 	}
-	if !ctx.identInfo(ident).IsPtrWrapped {
+	if !ctx.isPtrWrapped(ident) {
 		// should also be able to support variables that are of pointer type
 		ctx.todo(stmt, "can only inc/dec pointer-wrapped variables")
 	}
@@ -1999,10 +1959,6 @@ func (ctx Ctx) constSpec(spec *ast.ValueSpec) coq.ConstDecl {
 		Name:     ident.Name,
 		AddTypes: ctx.PkgConfig.TypeCheck,
 	}
-	ctx.addDef(ident, identInfo{
-		IsPtrWrapped: false,
-		IsMacro:      true,
-	})
 	addSourceDoc(spec.Comment, &cd.Comment)
 	val := spec.Values[0]
 	cd.Val = ctx.expr(val)

idents.go

@@ -5,87 +5,52 @@ import (
 	"go/types"
 )
 
-// this file has code that deals with tracking properties about identifiers, when
-// Go's type information isn't enough (for example, we treat var declarations
-// differently, but Go doesn't expose this since it makes no difference to the
-// language)
-
-type identInfo struct {
-	// IsPtrWrapped is true when an identifier is a function binding that is
-	// represented as a pointer in the translation, so uses need an extra
-	// dereferencing. When an identifier is declared with var rather than :=,
-	// we make it pointer-wrapped.
-	IsPtrWrapped bool
-	// IsMacro is true when an identifier refers to a Gallina definition in the
-	// translation (as opposed to a GooseLang variable)
-	IsMacro bool
-}
-
-type scopedName struct {
-	scope *types.Scope
-	name  string
-}
+// This file gives extra info about identifiers.
+// E.g., it helps track ptr wrapping, which Go doesn't easily expose
+// since it's not visible in the language.
 
 type identCtx struct {
-	info map[scopedName]identInfo
+	isPtrWrapped map[types.Object]bool
 }
 
 func newIdentCtx() identCtx {
-	return identCtx{info: make(map[scopedName]identInfo)}
+	return identCtx{isPtrWrapped: make(map[types.Object]bool)}
 }
 
-func (idents identCtx) lookupName(scope *types.Scope, name string) identInfo {
-	if scope == types.Universe {
-		return identInfo{
-			IsPtrWrapped: false,
-			// TODO: setting this to true triggers too often
-			IsMacro: false,
-		}
-	}
-	info, ok := idents.info[scopedName{scope, name}]
-	if ok {
-		return info
-	}
-	return idents.lookupName(scope.Parent(), name)
+func (ctx Ctx) isGlobalVar(ident *ast.Ident) bool {
+	obj := ctx.getObj(ident)
+	return obj.Pkg() != nil && obj.Parent() == obj.Pkg().Scope()
 }
 
-func (ctx Ctx) identInfo(ident *ast.Ident) identInfo {
-	if ident.Name == "_" {
-		ctx.unsupported(ident, "unexpected use of anonymous identifier")
+func (ctx Ctx) isPtrWrapped(ident *ast.Ident) bool {
+	obj := ctx.getObj(ident)
+	isWrapped, ok := ctx.idents.isPtrWrapped[obj]
+	if !ok {
+		return false
 	}
-	scope := ctx.info.Uses[ident].Parent()
-	return ctx.idents.lookupName(scope, ident.Name)
+	return isWrapped
 }
 
-func (ctx Ctx) doesDefHaveInfo(ident *ast.Ident) bool {
-	obj := ctx.info.Defs[ident]
-	if obj == nil {
-		// ident is not actually a definition (this is what happens when you
-		// multiply assign variables and only one of them is fresh - the others
-		// are not being defined but just re-assigned)
-		return true
-	}
-	defScope := obj.Parent()
-	key := scopedName{scope: defScope, name: ident.Name}
-	_, ok := ctx.idents.info[key]
-	return ok
+func (ctx Ctx) setPtrWrapped(ident *ast.Ident) {
+	obj := ctx.getObj(ident)
+	ctx.idents.isPtrWrapped[obj] = true
 }
 
-func (ctx Ctx) addDef(ident *ast.Ident, info identInfo) {
-	if ident.Name == "_" {
-		return
+func (ctx Ctx) getObj(ident *ast.Ident) types.Object {
+	obj := ctx.info.Uses[ident]
+	if obj == nil {
+		obj = ctx.info.Defs[ident]
 	}
-	obj := ctx.info.Defs[ident]
-	defScope := obj.Parent()
-	key := scopedName{scope: defScope, name: ident.Name}
-	ctx.idents.info[key] = info
+	if obj == nil {
+		ctx.unsupported(ident, "type checker doesn't have info about this ident")
+	}
+	return obj
 }
 
-func (ctx Ctx) definesPtrWrapped(ident *ast.Ident) bool {
-	obj := ctx.info.Defs[ident]
-	defScope := obj.Parent()
-	key := scopedName{scope: defScope, name: ident.Name}
-	return ctx.idents.info[key].IsPtrWrapped
+func (ctx Ctx) isStruct(ident *ast.Ident) bool {
+	obj := ctx.getObj(ident)
+	_, ok := obj.Type().Underlying().(*types.Struct)
+	return ok
 }
 
 func getIdent(e ast.Expr) (ident string, ok bool) {

types.go

@@ -165,7 +165,8 @@ func (ctx Ctx) coqType(e ast.Expr) coq.Type {
 	switch e := e.(type) {
 	case *ast.Ident:
 		ctx.dep.addDep(e.Name)
-		if ctx.identInfo(e).IsMacro {
+		// Struct typing is a bit funky.
+		if ctx.isGlobalVar(e) && !ctx.isStruct(e) {
 			return coq.TypeIdent(e.Name)
 		}
 		return ctx.coqTypeOfType(e, ctx.typeOf(e))