regression tests

diff --git a/helm/gTopLevel/tests/.cvsignore b/helm/gTopLevel/tests/.cvsignore
index 9ed3b07cefec8bb2f98df9eacb0ccdf3b72a0738..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 100644 (file)
--- a/helm/gTopLevel/tests/.cvsignore
+++ b/helm/gTopLevel/tests/.cvsignore
@@ -1 +0,0 @@
-*.test

diff --git a/helm/gTopLevel/tests/fix00.cic.test b/helm/gTopLevel/tests/fix00.cic.test
new file mode 100644 (file)
index 0000000..f688c40
--- /dev/null
+++ b/helm/gTopLevel/tests/fix00.cic.test
@@ -0,0 +1,217 @@
+let rec fact =
+  \lambda x:nat.
+    [\lambda x:nat. nat]
+    match x:nat with
+    [ O \Rightarrow 1
+    | (S (x: nat)) \Rightarrow (mult (S x) (fact x)) ]
+in
+(fact 4)
+### (* METASENV after disambiguation  *)
+ |- ?2: Type
+ |- ?3: ?2[]
+### (* TERM after disambiguation      *)
+[fact:=
+Fix fact {
+fact / 0 : (nat->nat) := 
+[x:nat]
+<[x:nat]nat>Cases x of 
+ O => (S O)
+ S => [x:nat](mult (S x) (fact x))
+end}
+](fact (S (S (S (S O)))))
+### (* TYPE_OF the disambiguated term *)
+nat
+### (* REDUCED disambiguated term     *)
+(S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ (S (
+Fix plus {
+plus / 0 : (n:nat)(nat->nat) := 
+[n:nat][m:nat]
+<[n0:nat]nat>Cases n of 
+ O => m
+ S => [p:nat](S (plus p m))
+end}
+ O O)) O)))))) O))))))))

diff --git a/helm/gTopLevel/tests/forall00.cic.test b/helm/gTopLevel/tests/forall00.cic.test
new file mode 100644 (file)
index 0000000..1665098
--- /dev/null
+++ b/helm/gTopLevel/tests/forall00.cic.test
@@ -0,0 +1,9 @@
+\forall n:nat. \forall m. n + m = n
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+(n:nat)(m:nat)(eq nat (plus n m) n)
+### (* TYPE_OF the disambiguated term *)
+Prop
+### (* REDUCED disambiguated term     *)
+(n:nat)(m:nat)(eq nat (plus n m) n)

diff --git a/helm/gTopLevel/tests/lambda01.cic.test b/helm/gTopLevel/tests/lambda01.cic.test
new file mode 100644 (file)
index 0000000..0e1f8c2
--- /dev/null
+++ b/helm/gTopLevel/tests/lambda01.cic.test
@@ -0,0 +1,11 @@
+(\lambda f. (f 0 (le_n 0))
+  \lambda n. \lambda H. (refl_equal nat 0)))
+### (* METASENV after disambiguation  *)
+f : (nat->((le O O)->(eq nat O O))); _ : nat |- ?14: Type
+f : (nat->((le O O)->(eq nat O O))); _ : nat |- ?15: ?14[-2 ; -1]
+### (* TERM after disambiguation      *)
+([f:(nat->((le O O)->(eq nat O O)))](f O (le_n O)) [n:nat][H:(le O O)](refl_equal nat O))
+### (* TYPE_OF the disambiguated term *)
+(eq nat O O)
+### (* REDUCED disambiguated term     *)
+(refl_equal nat O)

diff --git a/helm/gTopLevel/tests/lambda02.cic.test b/helm/gTopLevel/tests/lambda02.cic.test
new file mode 100644 (file)
index 0000000..ee8c6b1
--- /dev/null
+++ b/helm/gTopLevel/tests/lambda02.cic.test
@@ -0,0 +1,9 @@
+\lambda f:(\forall n:nat. (\forall H:(le 0 n). (n=n))). (f 0 (le_n 0))
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))
+### (* TYPE_OF the disambiguated term *)
+(f:(n:nat)(H:(le O n))(eq nat n n))(eq nat O O)
+### (* REDUCED disambiguated term     *)
+[f:(n:nat)(H:(le O n))(eq nat n n)](f O (le_n O))

diff --git a/helm/gTopLevel/tests/match00.cic.test b/helm/gTopLevel/tests/match00.cic.test
new file mode 100644 (file)
index 0000000..03db533
--- /dev/null
+++ b/helm/gTopLevel/tests/match00.cic.test
@@ -0,0 +1,26 @@
+[\lambda x:nat.
+  [\lambda y:nat. Set]
+    match x:nat with [ O \Rightarrow nat | (S x) \Rightarrow bool ]]
+match (S O):nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow false ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[x:nat]
+<[y:nat]Set>Cases x of 
+ O => nat
+ S => [x:nat]bool
+end>Cases (S O) of 
+ O => O
+ S => [x:nat]false
+end
+### (* TYPE_OF the disambiguated term *)
+([x:nat]
+<[y:nat]Set>Cases x of 
+ O => nat
+ S => [x:nat]bool
+end (S O))
+### (* REDUCED disambiguated term     *)
+false

diff --git a/helm/gTopLevel/tests/match01.cic.test b/helm/gTopLevel/tests/match01.cic.test
new file mode 100644 (file)
index 0000000..089665f
--- /dev/null
+++ b/helm/gTopLevel/tests/match01.cic.test
@@ -0,0 +1,16 @@
+[\lambda z:nat. \lambda h:(le O z). (eq nat O O)]
+match (le_n O): le with
+[ le_n \Rightarrow (refl_equal nat O)
+| (le_S x y) \Rightarrow (refl_equal nat O) ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[z:nat][h:(le O z)](eq nat O O)>Cases (le_n O) of 
+ le_n => (refl_equal nat O)
+ le_S => [x:nat][y:(le O x)](refl_equal nat O)
+end
+### (* TYPE_OF the disambiguated term *)
+([z:nat][h:(le O z)](eq nat O O) O (le_n O))
+### (* REDUCED disambiguated term     *)
+(refl_equal nat O)

diff --git a/helm/gTopLevel/tests/match02.cic.test b/helm/gTopLevel/tests/match02.cic.test
new file mode 100644 (file)
index 0000000..c265102
--- /dev/null
+++ b/helm/gTopLevel/tests/match02.cic.test
@@ -0,0 +1,16 @@
+[\lambda z:nat. \lambda h:(le 0 z). (le 0 (S z))]
+match (le_S 0 0 (le_n 0)): le with
+[ le_n \Rightarrow (le_S 0 0 (le_n 0))
+| (le_S x y) \Rightarrow (le_S 0 (S x) (le_S 0 x y)) ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[z:nat][h:(le O z)](le O (S z))>Cases (le_S O O (le_n O)) of 
+ le_n => (le_S O O (le_n O))
+ le_S => [x:nat][y:(le O x)](le_S O (S x) (le_S O x y))
+end
+### (* TYPE_OF the disambiguated term *)
+([z:nat][h:(le O z)](le O (S z)) (S O) (le_S O O (le_n O)))
+### (* REDUCED disambiguated term     *)
+(le_S O (S O) (le_S O O (le_n O)))

diff --git a/helm/gTopLevel/tests/match03.cic.test b/helm/gTopLevel/tests/match03.cic.test
new file mode 100644 (file)
index 0000000..16b4097
--- /dev/null
+++ b/helm/gTopLevel/tests/match03.cic.test
@@ -0,0 +1,16 @@
+[\lambda x:bool. nat]
+match true:bool with
+[ true \Rightarrow O
+| false \Rightarrow (S O) ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[x:bool]nat>Cases true of 
+ true => O
+ false => (S O)
+end
+### (* TYPE_OF the disambiguated term *)
+([x:bool]nat true)
+### (* REDUCED disambiguated term     *)
+O

diff --git a/helm/gTopLevel/tests/match04.cic.test b/helm/gTopLevel/tests/match04.cic.test
new file mode 100644 (file)
index 0000000..280bfbf
--- /dev/null
+++ b/helm/gTopLevel/tests/match04.cic.test
@@ -0,0 +1,16 @@
+[\lambda x:nat. nat]
+match O:nat with
+[ O \Rightarrow O
+| (S x) \Rightarrow (S (S x)) ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[x:nat]nat>Cases O of 
+ O => O
+ S => [x:nat](S (S x))
+end
+### (* TYPE_OF the disambiguated term *)
+([x:nat]nat O)
+### (* REDUCED disambiguated term     *)
+O

diff --git a/helm/gTopLevel/tests/match05.cic.test b/helm/gTopLevel/tests/match05.cic.test
new file mode 100644 (file)
index 0000000..6bda244
--- /dev/null
+++ b/helm/gTopLevel/tests/match05.cic.test
@@ -0,0 +1,16 @@
+[\lambda x:list. list]
+match nil:list with
+[ nil \Rightarrow nil
+| (cons x y) \Rightarrow (cons x y) ]
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+
+<[x:list]list>Cases nil of 
+ nil => nil
+ cons => [x:A][y:list](cons x y)
+end
+### (* TYPE_OF the disambiguated term *)
+([x:list]list nil)
+### (* REDUCED disambiguated term     *)
+nil

diff --git a/helm/gTopLevel/tests/match06.cic.test b/helm/gTopLevel/tests/match06.cic.test
new file mode 100644 (file)
index 0000000..d7078f0
--- /dev/null
+++ b/helm/gTopLevel/tests/match06.cic.test
@@ -0,0 +1,15 @@
+\lambda x:False.
+  [\lambda h:False. True]
+  match x:False with []
+### (* METASENV after disambiguation  *)
+
+### (* TERM after disambiguation      *)
+[x:False]
+<[h:False]True>Cases x of 
+end
+### (* TYPE_OF the disambiguated term *)
+(x:False)([h:False]True x)
+### (* REDUCED disambiguated term     *)
+[x:False]
+<[h:False]True>Cases x of 
+end