regression tests

[helm.git] / helm / gTopLevel / tests / fix00.cic.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))))))))