Change some naming for consistency

upamanyus · Jun 18, 2024 · 5aba9fa · 5aba9fa
1 parent a6145be
commit 5aba9fa
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/goose.go b/goose.go
@@ -670,7 +670,7 @@ func (ctx Ctx) structSelector(info structTypeInfo, e *ast.SelectorExpr) glang.Ex
 			X:              ctx.expr(e.X),
 			ThroughPointer: info.throughPointer,
 		},
-		Ty: glang.NewCallExpr(glang.GallinaIdent("struct.fieldTy"),
+		Ty: glang.NewCallExpr(glang.GallinaIdent("struct.field_ty"),
 			glang.GallinaIdent(info.name),
 			glang.IdentExpr(e.Sel.Name),
 		),
@@ -1297,7 +1297,7 @@ func (ctx Ctx) refExpr(s ast.Expr) glang.Expr {
 		} else {
 			structExpr = ctx.refExpr(s.X)
 		}
-		return glang.NewCallExpr(glang.GallinaIdent("struct.fieldRef"), glang.StructDesc(info.name),
+		return glang.NewCallExpr(glang.GallinaIdent("struct.field_ref"), glang.StructDesc(info.name),
 			glang.GallinaString(fieldName), structExpr)
 	// TODO: should move support for slice indexing here as well
 	default:
@@ -1376,12 +1376,12 @@ func (ctx Ctx) assignFromTo(s ast.Node, lhs ast.Expr, rhs glang.Expr, cont glang
 		if ok {
 			fieldName := lhs.Sel.Name
 			return glang.NewDoSeq(glang.StoreStmt{
-				Dst: glang.NewCallExpr(glang.GallinaIdent("struct.fieldRef"),
+				Dst: glang.NewCallExpr(glang.GallinaIdent("struct.field_ref"),
 					glang.StructDesc(info.name),
 					glang.GallinaString(fieldName),
 					structExpr,
 					rhs),
-				Ty: glang.NewCallExpr(glang.GallinaIdent("struct.fieldTy"),
+				Ty: glang.NewCallExpr(glang.GallinaIdent("struct.field_ty"),
 					glang.GallinaIdent(info.name),
 					glang.IdentExpr(lhs.Sel.Name),
 				),

diff --git a/internal/glang/coq.go b/internal/glang/coq.go
@@ -124,7 +124,7 @@ type StructDecl struct {
 func (d StructDecl) CoqDecl() string {
 	var pp buffer
 	pp.AddComment(d.Comment)
-	pp.Add("Definition %s := struct.decl [", d.Name)
+	pp.Add("Definition %s := [", d.Name)
 	pp.Indent(2)
 	for i, fd := range d.Fields {
 		sep := ";"
@@ -453,7 +453,7 @@ func StructDesc(name string) Expr {
 
 func (e StructFieldAccessExpr) Coq(needs_paren bool) string {
 	if e.ThroughPointer {
-		return NewCallExpr(GallinaIdent("struct.fieldRef"),
+		return NewCallExpr(GallinaIdent("struct.field_ref"),
 			StructDesc(e.Struct), GallinaString(e.Field), e.X).Coq(needs_paren)
 	}
 	return NewCallExpr(GallinaIdent("struct.get"), StructDesc(e.Struct),