Add support for recursive structs using a generic for indirection

glang/types.go

@@ -115,6 +115,16 @@ func (d StructType) Coq(needs_paren bool) string {
 	return addParens(needs_paren, pp.Build())
 }
 
+type TtType struct{}
+
+func (_ TtType) Coq(needs_paren bool) string {
+	return "#()"
+}
+
+func (_ TtType) Gallina(needs_paren bool) string {
+	return addParens(needs_paren, "type.structT []")
+}
+
 type TypeDecl struct {
 	Name       string
 	Body       Type
@@ -134,6 +144,7 @@ func (d TypeDecl) CoqDecl() string {
 	pp.Add("Definition %s : val :=", GallinaIdent(d.Name).Coq(false))
 	pp.Indent(2)
 	pp.Add("λ: %s, %s.", typeBinders(d.TypeParams), d.Body.Coq(false))
+	pp.Indent(-2)
 	// XXX: Opaque does not imply Typeclasses Opaque.
 	// https://rocq-prover.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Opaque.20does.20not.20imply.20Typeclasses.20Opaque
 	// https://github.com/rocq-prover/rocq/issues/19482

goose.go

@@ -55,6 +55,10 @@ type Ctx struct {
 	// include a defer prelude+prologue.
 	usesDefer bool
 
+	// The top-level type declaration being processed, if there is one. Used to
+	// detect recursive ocurrences.
+	curTypeDecl *types.TypeName
+
 	// One of these tracks *all* the dependencies for an entire package
 	dep *deptracker.Deps
 

testdata/examples/unittest/generics/generics.gold.v

@@ -43,8 +43,8 @@ Definition Box : val :=
   λ: "T", type.structT [
     (#"Value"%go, "T")
   ].
-  #[global] Typeclasses Opaque Box.
-  #[global] Opaque Box.
+#[global] Typeclasses Opaque Box.
+#[global] Opaque Box.
 
 Definition BoxGet : go_string := "github.com/goose-lang/goose/testdata/examples/unittest/generics.BoxGet"%go.
 
@@ -109,8 +109,8 @@ Definition Container : val :=
     (#"Z"%go, #ptrT);
     (#"W"%go, #uint64T)
   ].
-  #[global] Typeclasses Opaque Container.
-  #[global] Opaque Container.
+#[global] Typeclasses Opaque Container.
+#[global] Opaque Container.
 
 Definition useContainer : go_string := "github.com/goose-lang/goose/testdata/examples/unittest/generics.useContainer"%go.
 
@@ -145,24 +145,24 @@ Definition UseContainer : val :=
   λ: <>, type.structT [
     (#"X"%go, Container #uint64T)
   ].
-  #[global] Typeclasses Opaque UseContainer.
-  #[global] Opaque UseContainer.
+#[global] Typeclasses Opaque UseContainer.
+#[global] Opaque UseContainer.
 
 Definition OnlyIndirect : val :=
   λ: "T", type.structT [
     (#"X"%go, #sliceT);
     (#"Y"%go, #ptrT)
   ].
-  #[global] Typeclasses Opaque OnlyIndirect.
-  #[global] Opaque OnlyIndirect.
+#[global] Typeclasses Opaque OnlyIndirect.
+#[global] Opaque OnlyIndirect.
 
 Definition MultiParam : val :=
   λ: "A" "B", type.structT [
     (#"Y"%go, "B");
     (#"X"%go, "A")
   ].
-  #[global] Typeclasses Opaque MultiParam.
-  #[global] Opaque MultiParam.
+#[global] Typeclasses Opaque MultiParam.
+#[global] Opaque MultiParam.
 
 Definition useMultiParam : go_string := "github.com/goose-lang/goose/testdata/examples/unittest/generics.useMultiParam"%go.
 

testdata/examples/unittest/recursive_struct.go

@@ -0,0 +1,15 @@
+package unittest
+
+type LinkedList struct {
+	Value int
+	Next  *LinkedList
+}
+
+type Box[T any] struct {
+	Value *T
+}
+
+type List struct {
+	Value int
+	Next  Box[List]
+}

testdata/examples/unittest/unittest.gold.v

@@ -44,6 +44,9 @@ Module composite. Definition id : go_string := "github.com/goose-lang/goose/test
 Module R. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.R"%go. End R.
 Module Other. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.Other"%go. End Other.
 Module RecursiveEmbedded. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.RecursiveEmbedded"%go. End RecursiveEmbedded.
+Module LinkedList. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.LinkedList"%go. End LinkedList.
+Module Box. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.Box"%go. End Box.
+Module List. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.List"%go. End List.
 Module Block. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.Block"%go. End Block.
 Module SliceAlias. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.SliceAlias"%go. End SliceAlias.
 Module thing. Definition id : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.thing"%go. End thing.
@@ -2296,6 +2299,28 @@ Definition RecursiveEmbedded__recurEmbeddedMethodⁱᵐᵖˡ : val :=
     do:  ((method_call #Other.id #"recurEmbeddedMethod"%go (![#Other] (struct.field_ref #RecursiveEmbedded #"Other"%go (![#ptrT] "r")))) #());;;
     return: #()).
 
+Definition LinkedList : go_type := structT [
+  "Value" :: intT;
+  "Next" :: ptrT
+].
+#[global] Typeclasses Opaque LinkedList.
+#[global] Opaque LinkedList.
+
+Definition Box : val :=
+  λ: "T", type.structT [
+    (#"Value"%go, #ptrT)
+  ].
+#[global] Typeclasses Opaque Box.
+#[global] Opaque Box.
+
+Definition List : val :=
+  λ: <>, type.structT [
+    (#"Value"%go, #intT);
+    (#"Next"%go, Box #())
+  ].
+#[global] Typeclasses Opaque List.
+#[global] Opaque List.
+
 Definition useRenamedImport : go_string := "github.com/goose-lang/goose/testdata/examples/unittest.useRenamedImport"%go.
 
 (* go: renamedImport.go:7:6 *)
@@ -3168,7 +3193,7 @@ Definition msets' : list (go_string * (list (go_string * val))) := [(Foo.id, [])
                  method_call #(ptrT.id RecursiveEmbedded.id) #"recurEmbeddedMethod"%go (struct.field_get #Other #"RecursiveEmbedded"%go "$r")
                  )%V)]); (ptrT.id Other.id, [("recurEmbeddedMethod"%go, (λ: "$r",
                  method_call #(ptrT.id RecursiveEmbedded.id) #"recurEmbeddedMethod"%go (![#ptrT] (struct.field_ref #Other #"RecursiveEmbedded"%go "$r"))
-                 )%V)]); (RecursiveEmbedded.id, []); (ptrT.id RecursiveEmbedded.id, [("recurEmbeddedMethod"%go, RecursiveEmbedded__recurEmbeddedMethodⁱᵐᵖˡ)]); (Block.id, []); (ptrT.id Block.id, []); (SliceAlias.id, []); (ptrT.id SliceAlias.id, []); (thing.id, []); (ptrT.id thing.id, []); (sliceOfThings.id, [("getThingRef"%go, sliceOfThings__getThingRefⁱᵐᵖˡ)]); (ptrT.id sliceOfThings.id, [("getThingRef"%go, (λ: "$r",
+                 )%V)]); (RecursiveEmbedded.id, []); (ptrT.id RecursiveEmbedded.id, [("recurEmbeddedMethod"%go, RecursiveEmbedded__recurEmbeddedMethodⁱᵐᵖˡ)]); (LinkedList.id, []); (ptrT.id LinkedList.id, []); (Box.id, []); (ptrT.id Box.id, []); (List.id, []); (ptrT.id List.id, []); (Block.id, []); (ptrT.id Block.id, []); (SliceAlias.id, []); (ptrT.id SliceAlias.id, []); (thing.id, []); (ptrT.id thing.id, []); (sliceOfThings.id, [("getThingRef"%go, sliceOfThings__getThingRefⁱᵐᵖˡ)]); (ptrT.id sliceOfThings.id, [("getThingRef"%go, (λ: "$r",
                  method_call #sliceOfThings.id #"getThingRef"%go (![#sliceOfThings] "$r")
                  )%V)]); (Point.id, [("Add"%go, Point__Addⁱᵐᵖˡ); ("GetField"%go, Point__GetFieldⁱᵐᵖˡ); ("IgnoreReceiver"%go, Point__IgnoreReceiverⁱᵐᵖˡ)]); (ptrT.id Point.id, [("Add"%go, (λ: "$r",
                  method_call #Point.id #"Add"%go (![#Point] "$r")

types.go

@@ -82,6 +82,10 @@ func (ctx *Ctx) typeDecl(spec *ast.TypeSpec) (decls []glang.Decl) {
 		defer ctx.dep.UnsetCurrentName()
 
 		if t, ok := ctx.typeOf(spec.Name).(*types.Named); ok {
+			ctx.curTypeDecl = t.Obj()
+			defer func() {
+				ctx.curTypeDecl = nil
+			}()
 			if _, ok := t.Underlying().(*types.Interface); !ok {
 				ctx.namedTypes = append(ctx.namedTypes, t)
 			}
@@ -324,6 +328,9 @@ func (ctx *Ctx) glangType(n locatable, t types.Type) glang.Type {
 		if t.Obj().Pkg() == nil {
 			ctx.unsupported(n, "unexpected built-in type %v", t.Obj())
 		}
+		if ctx.curTypeDecl != nil && ctx.curTypeDecl == t.Obj() {
+			return glang.TtType{}
+		}
 		if info, ok := ctx.getStructInfo(t); ok {
 			return ctx.structInfoToGlangType(info)
 		}
@@ -418,7 +425,9 @@ type structTypeInfo struct {
 func (ctx *Ctx) structInfoToGlangType(info structTypeInfo) glang.Type {
 	ctx.dep.Add(info.name)
 	if TypeIsGooseLang(info.namedType) {
-		return glang.TypeCallExpr{MethodName: glang.GallinaIdent(info.name), Args: ctx.convertTypeArgsToGlang(nil, info.typeArgs)}
+		return glang.TypeCallExpr{
+			MethodName: glang.GallinaIdent(info.name),
+			Args:       ctx.convertTypeArgsToGlang(nil, info.typeArgs)}
 	} else {
 		return glang.TypeIdent(info.name)
 	}