Only initialize a package once

deptracker.go

@@ -32,6 +32,9 @@ func (dt *depTracker) unsetCurrentName() {
 }
 
 func (dt *depTracker) addDep(s string) {
+	if !dt.currentNameValid {
+		panic("depTracker: tried to add dep without name set")
+	}
 	dt.nameToDeps[dt.currentName] = append(dt.nameToDeps[dt.currentName], s)
 }
 

glang/coq.go

@@ -945,11 +945,11 @@ func (d MethodSetDecl) DefName() (bool, string) {
 
 type VarDecl struct {
 	DeclName    string
-	VarUniqueId string
+	VarUniqueId Expr
 }
 
 func (d VarDecl) CoqDecl() string {
-	return fmt.Sprintf("Definition %s : val := #\"%s\".", d.DeclName, d.VarUniqueId)
+	return fmt.Sprintf("Definition %s : val := %s.", d.DeclName, d.VarUniqueId.Coq(false))
 }
 
 func (d VarDecl) DefName() (bool, string) {

goose.go

@@ -2204,6 +2204,7 @@ func (ctx *Ctx) funcDecl(d *ast.FuncDecl) []glang.Decl {
 	addSourceDoc(d.Doc, &fd.Comment)
 	ctx.addSourceFile(d, &fd.Comment)
 	fd.TypeParams = ctx.typeParamList(d.Type.TypeParams)
+
 	if d.Recv != nil {
 		if len(d.Recv.List) != 1 {
 			ctx.nope(d, "function with multiple receivers")
@@ -2221,12 +2222,14 @@ func (ctx *Ctx) funcDecl(d *ast.FuncDecl) []glang.Decl {
 		typeName := namedType.Obj().Name()
 
 		fd.Name = glang.TypeMethod(typeName, d.Name.Name)
+		ctx.dep.setCurrentName(fd.Name)
 		f := ctx.field(receiver)
 		fd.RecvArg = &f
+	} else {
+		ctx.dep.setCurrentName(fd.Name)
 	}
-
-	ctx.dep.setCurrentName(fd.Name)
 	defer ctx.dep.unsetCurrentName()
+
 	body := ctx.blockStmt(d.Body, nil)
 
 	if d.Name.Name == "init" {
@@ -2344,10 +2347,17 @@ func (ctx *Ctx) globalVarDecl(d *ast.GenDecl) []glang.Decl {
 				ctx.globalVars[name.Name] = ctx.glangType(name, ctx.info.TypeOf(name))
 				ctx.globalVarsOrdered = append(ctx.globalVarsOrdered, name.Name)
 			}
+			ctx.dep.setCurrentName(name.Name)
 			decls = append(decls, glang.VarDecl{
-				DeclName:    name.Name,
-				VarUniqueId: ctx.pkgPath + "." + name.Name,
+				DeclName: name.Name,
+				VarUniqueId: glang.BinaryExpr{
+					X:  glang.GallinaIdent("global_id'"),
+					Op: glang.OpPlus,
+					Y:  glang.StringLiteral{Value: name.Name},
+				},
 			})
+			ctx.dep.addDep("global_id'")
+			ctx.dep.unsetCurrentName()
 		}
 	}
 	return decls
@@ -2427,6 +2437,12 @@ func (ctx *Ctx) initFunctions() []glang.Decl {
 	//   initializing vars of the current package.
 	// - should only `init` a package once, even if imported multiple times.
 
+	packageIdDecl := glang.ConstDecl{
+		Name: "global_id'",
+		Val:  glang.GallinaString(ctx.pkgPath),
+		Type: glang.GallinaIdent("string"),
+	}
+
 	defineFunc := glang.FuncDecl{Name: "define'"}
 	ctx.dep.setCurrentName("define'")
 	var e glang.Expr
@@ -2521,7 +2537,13 @@ func (ctx *Ctx) initFunctions() []glang.Decl {
 	// FIXME: initialize imported packages.
 
 	e = glang.NewDoSeq(glang.NewCallExpr(glang.GallinaIdent("define'"), glang.Tt), e)
+	e = glang.IfExpr{
+		Cond: glang.NewCallExpr(glang.GallinaIdent("globals.is_uninitialized"),
+			glang.GallinaIdent("global_id'")),
+		Then: e,
+		Else: glang.DoExpr{Expr: glang.Tt},
+	}
 	initFunc.Body = glang.NewCallExpr(glang.GallinaIdent("exception_do"), e)
 
-	return []glang.Decl{defineFunc, initFunc}
+	return []glang.Decl{packageIdDecl, defineFunc, initFunc}
 }