summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-09 11:46:33 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-09 11:46:33 -0400
commit4960cd8c2ec1e02c90e42d16db13f045427b4173 (patch)
treea2823b006b357561d5866e778cb3ff2046836f8b /tests
parent27bece20a8abae9a2b4251e065010a4e52590c45 (diff)
Termination checking
Diffstat (limited to 'tests')
-rw-r--r--tests/termination.ur28
-rw-r--r--tests/termination.urp5
2 files changed, 33 insertions, 0 deletions
diff --git a/tests/termination.ur b/tests/termination.ur
new file mode 100644
index 00000000..64acd996
--- /dev/null
+++ b/tests/termination.ur
@@ -0,0 +1,28 @@
+datatype list a = Nil | Cons of a * list a
+
+fun isNil (t ::: Type) (ls : list t) : bool =
+ case ls of
+ Nil => True
+ | Cons _ => False
+
+fun append (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
+ case ls1 of
+ Nil => ls2
+ | Cons (x, ls1') => Cons (x, append ls1' ls2)
+
+fun appendR (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
+ case ls1 of
+ Nil => ls2
+ | Cons (x, ls1') => Cons (x, appendR ls2 ls1')
+
+(*fun naughty (t ::: Type) (ls : list t) : list t = naughty ls*)
+
+fun append1 (t ::: Type) (ls1 : list t) (ls2 : list t) : list t =
+ case ls1 of
+ Nil => ls2
+ | Cons (x, ls1') => Cons (x, append2 ls2 ls1')
+
+and append2 (t ::: Type) (ls2 : list t) (ls1 : list t) : list t =
+ case ls1 of
+ Nil => ls2
+ | Cons (x, ls1') => Cons (x, append1 ls1' ls2)
diff --git a/tests/termination.urp b/tests/termination.urp
new file mode 100644
index 00000000..24df4847
--- /dev/null
+++ b/tests/termination.urp
@@ -0,0 +1,5 @@
+debug
+database dbname=test
+exe /tmp/webapp
+
+termination