Merge pull request #55 from tchajed/alias-only-parse

prior alias gen caused all terms to print as alias. change to use Notation (only parsing).
goose-lang · Jul 16, 2024 · d0cf574 · d0cf574
2 parents 20cad8d + 974e7f0
commit d0cf574
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 5 deletions.
diff --git a/internal/coq/coq.go b/internal/coq/coq.go
@@ -278,7 +278,10 @@ type AliasDecl struct {
 
 func (t AliasDecl) CoqDecl() string {
 	var pp buffer
-	pp.Add("Notation %s := %s.", t.Name, t.Type.Coq(true))
+	// (only parsing) so that terms don't get printed as their aliases.
+	// All aliases get printed as their underlying type, but that seems
+	// similar to their Go interpretation.
+	pp.Add("Notation %s := %s (only parsing).", t.Name, t.Type.Coq(true))
 	return pp.Build()
 }
 

diff --git a/internal/examples/semantics/semantics.gold.v b/internal/examples/semantics/semantics.gold.v
@@ -107,9 +107,9 @@ Definition testAssignBitwise: val :=
 
 (* closures.go *)
 
-Notation AdderType := (uint64T -> uint64T)%ht.
+Notation AdderType := (uint64T -> uint64T)%ht (only parsing).
 
-Notation MultipleArgsType := (uint64T -> boolT -> uint64T)%ht.
+Notation MultipleArgsType := (uint64T -> boolT -> uint64T)%ht (only parsing).
 
 Definition adder: val :=
   rec: "adder" <> :=

diff --git a/internal/examples/unittest/unittest.gold.v b/internal/examples/unittest/unittest.gold.v
@@ -1121,9 +1121,9 @@ Definition TyMethodDriver: val :=
 
 (* type_alias.go *)
 
-Notation my_u64 := uint64T.
+Notation my_u64 := uint64T (only parsing).
 
-Notation my_slice := (slice.T byteT).
+Notation my_slice := (slice.T byteT) (only parsing).
 
 Definition Timestamp: ty := uint64T.