msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

testsuite: fix test of generate_trees

Browse Source 
There were two differences between the current output and the old gold file: 

  1. The trees are no longer generated with increasing depth
  2. The meaning of the -depth flag has changed: for example, 
     "gt -cat=Nat -depth=1" used to generate only "zero",
     now you also get "succ zero".
This commit is contained in:
hallgren
2013-12-10 16:49:40 +00:00
parent 0851308099
commit dd1b474a22
2 changed files with 15 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
testsuite/compiler/check/abstract-operations/abstract-operations.gfs
View File

@@ -1,5 +1,5 @@
-- here we test that the abstract operations are not used for proof search
i testsuite/compiler/check/abstract-operations/Nat.gf
gt -cat=Nat -number=10 -depth=10
gt -cat=Nat -number=11 -depth=10
pt -compute (twice (succ zero))

27
testsuite/compiler/check/abstract-operations/abstract-operations.gfs.gold
View File

@@ -1,13 +1,14 @@
zero
succ zero
succ (succ zero)
succ (succ (succ zero))
succ (succ (succ (succ zero)))
succ (succ (succ (succ (succ zero))))
succ (succ (succ (succ (succ (succ zero)))))
succ (succ (succ (succ (succ (succ (succ zero))))))
succ (succ (succ (succ (succ (succ (succ (succ zero)))))))
succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))
succ (succ zero)
succ (succ (succ (succ (succ (succ (succ (succ (succ (succ zero)))))))))
succ (succ (succ (succ (succ (succ (succ (succ (succ zero))))))))
succ (succ (succ (succ (succ (succ (succ (succ zero)))))))
succ (succ (succ (succ (succ (succ (succ zero))))))
succ (succ (succ (succ (succ (succ zero)))))
succ (succ (succ (succ (succ zero))))
succ (succ (succ (succ zero)))
succ (succ (succ zero))
succ (succ zero)
succ zero
zero
succ (succ zero)