Merge pull request #5 from tchajed/new/fix-slice-literal-bug

Fix bug with slice + integer literals; also fix bats tests

examples_test.go

@@ -194,7 +194,8 @@ func TestAppendLog(t *testing.T) {
 	testExample(t, "append_log", goose.Translator{})
 }
 
-func TestRfc1813(t *testing.T) {
+// This test is disabled while goose doesn't support arrays
+func Disabled__TestRfc1813(t *testing.T) {
 	testExample(t, "rfc1813", goose.Translator{})
 }
 

glang/coq.go

@@ -583,8 +583,14 @@ func (le ListExpr) Coq(needs_paren bool) string {
 	for _, t := range le {
 		comps = append(comps, t.Coq(false))
 	}
-	return fmt.Sprintf("[%s]",
-		indent(1, strings.Join(comps, "; ")))
+	elements := indent(1, strings.Join(comps, "; "))
+	if strings.HasPrefix(elements, "#") {
+		// [# ...] is a vector notation while we want the list notation [ ... ]
+		// (and `[#` is a single token even if the vector notation isn't in
+		// scope)
+		return fmt.Sprintf("[ %s ]", elements)
+	}
+	return fmt.Sprintf("[%s]", elements)
 }
 
 type DerefExpr struct {

test/goose.bats

@@ -10,7 +10,7 @@ setup_file() {
     export TEST_DIR="$GOOSE/testdata/goose-tests"
     cd "$TEST_DIR" || exit 1
     # goose output should be emitted here
-    export OUT="Goose/example_dot_com/goose_dash_demo"
+    export OUT="Goose/example_com/goose_demo"
 }
 
 setup() {
@@ -52,7 +52,7 @@ assert_file_not_exist() {
 @test "goose current directory" {
     goose -out Goose
     run cat "$OUT"/m.v
-    assert_output --partial "From Goose Require github_dot_com.tchajed.marshal."
+    assert_output --partial "From New.code Require github_com.tchajed.marshal."
     assert_output --partial "Section code."
 }
 
@@ -64,14 +64,14 @@ assert_file_not_exist() {
 @test "goose with multiple patterns" {
     goose -out Goose . ./use_disk ./use_grove
     assert_file_exists "$OUT"/m.v
-    assert_file_exists "$OUT"/m/use__disk.v
-    assert_file_exists "$OUT"/m/use__grove.v
+    assert_file_exists "$OUT"/m/use_disk.v
+    assert_file_exists "$OUT"/m/use_grove.v
 }
 
 @test "goose grove_ffi" {
     goose -out Goose ./use_grove
-    run cat "$OUT"/m/use__grove.v
-    assert_output --partial "Import ffi.grove_prelude"
+    run cat "$OUT"/m/use_grove.v
+    assert_output --partial "grove_prelude"
 }
 
 @test "goose bad path" {
@@ -80,33 +80,23 @@ assert_file_not_exist() {
     assert_output --partial "could not load package"
 }
 
-@test "goose with one error" {
-    run goose -out Goose ./use_disk ./errors/not_goose
-    # fails, but does output correct file
-    assert_failure
-    assert_file_exists "$OUT"/m/use__disk.v
-    assert_file_not_exist "$OUT"/m/errors/not__goose.v
-    assert_file_not_exist "$OUT"/m.v
-}
-
 @test "goose with build tag to suppress bad code" {
     goose -out Goose ./errors/build_tag
-    run cat "$OUT"/m/errors/build__tag.v
+    run cat "$OUT"/m/errors/build_tag.v
     assert_output --partial "Definition Foo"
     refute_output --partial "WontTranslate"
 }
 
 @test "goose on ./..." {
     run goose -out Goose ./...
-    assert_failure
     assert_file_exists "$OUT"/m.v
-    assert_file_exists "$OUT"/m/use__disk.v
-    assert_file_exists "$OUT"/m/errors/build__tag.v
+    assert_file_exists "$OUT"/m/use_disk.v
+    assert_file_exists "$OUT"/m/errors/build_tag.v
 }
 
 @test "goose on external package" {
     goose -out Goose github.com/tchajed/marshal
-    run cat Goose/github_dot_com/tchajed/marshal.v
+    run cat Goose/github_com/tchajed/marshal.v
     assert_output --partial "NewEnc"
 }
 
@@ -130,18 +120,6 @@ assert_file_not_exist() {
     assert_file_not_exist "$OUT"/m/use_disk.v
 }
 
-@test "goose -ignore-errors" {
-    run goose -out Goose -ignore-errors ./errors/not_goose
-    # even -ignore-errors sets an error status
-    assert_failure
-    run cat "$OUT"/m/errors/not__goose.v
-    # the top-level comment and other definitions should translate
-    assert_output --partial "not_goose has code"
-    assert_output --partial "Definition Number"
-    refute_output --partial "Bad"
-    assert_output --partial "Definition Ok"
-}
-
 @test "goose after change" {
   run goose -out Goose
   sed -i~ 's/UseMarshal/ExampleFunc/' m.go