Commits

Paweł Wieczorek  committed 9a1d144

better organisation for test files

  • Participants
  • Parent commits 175e09b
  • Branches analysis_infastructure

Comments (0)

Files changed (49)

File test/01.sl

-DEF main =
-    let k = fun (x:int) => fun (y:int) => x
-    in k 1 2

File test/02.sl

-DEF main = 1 + 2

File test/03.sl

-SIG main : int
-DEF main = (fun x => fun (y:int) => x) 1 2

File test/04.sl

-DEF main = (fun (x:int) (y:int) => x + y) 1
-

File test/05.sl

-DEF main =
-    let add = fun (x:int) => 5 + x
-     in add 3
-

File test/06.sl

-DEF main = 
-    let nil c1 c2 = c1 in
-    let cons x xs d1 d2 = d2 x xs in
-    let isnil ys = ys 1 (fun q w => 0) in
-    let iscons bs = bs 0 (fun e r => 1) in
-    let head zs = zs 0 (fun a b => a) in
-    let list1 = cons 10 nil in
-    head list1 

File test/07.sl

-DEF main = 
-    let nil c1 c2 = c1 in
-    let cons x xs d1 d2 = d2 x xs in
-    let cons2 xx xxs dd1 dd2 = dd2 xx xxs in
-    let isnil ys = ys 1 (fun q w => 0) in
-    let iscons bs = bs 0 (fun e r => 1) in
-    let head zs = zs 0 (fun a b => a) in
-    let tail zs = zs 0 (fun aa bb => bb) in
-    let list1 = cons 10 (cons2 20 nil) in
-    head (tail list1)

File test/08.sl

-DEF main =
-    if a == a
-        then 10
-        else 20

File test/09.sl

-DEF main =
-    if (a == b) && (a == b)
-        then 10
-        else 20

File test/10.sl

-SIG add : int -> int -> int
-DEF add (x:int) (y:int) = x + y
-DEF main = add 1 2

File test/11.sl

-SIG frac : int -> int -> int
-DEF frac aux n =
-    if n == 0
-        then aux
-        else frac (n*aux) (n - 1)
-DEF main = frac 1 0
-

File test/12.sl

-DEF nil c1 c2 = c1
-DEF cons x xs c1 c2 = c2 x xs
-DEF map f xs = xs nil (fun y ys => cons (f y) (map f ys))
-DEF list = cons 0 (cons 1 (cons 2 nil))
-DEF head xs = xs 0 (fun x xs => x)
-DEF main = head (map (fun x => x + 1) list)

File test/13.sl

-DEF nil c1 c2 = c1
-DEF cons x xs d1 d2 = d2 x xs
-DEF cons2 xx xxs dd1 dd2 = dd2 xx xxs
-DEF isnil ys = ys 1 (fun q w => 0)
-DEF iscons bs = bs 0 (fun e r => 1)
-DEF head zs = zs 0 (fun a b => a)
-DEF tail zs = zs 0 (fun aa bb => bb)
-DEF list1 = cons 10 (cons2 20 nil)
-DEF main = head (tail list1)

File test/14.sl

-SIG add : int -> int -> int
-DEF add x y = x + y
-DEF main = add 1 2 * add 1 3

File test/16.sl

-SIG f : int -> int -> int
-SIG g : int -> int
-DEF f x (y:int) = g x
-DEF g x = f x x
-
-DEF main = 4
-

File test/basic/K_01.sl

+DEF main =
+    let k = fun (x:int) => fun (y:int) => x
+    in k 1 2

File test/basic/K_02.sl

+SIG main : int
+DEF main = (fun x => fun (y:int) => x) 1 2

File test/basic/K_partial.sl

+DEF main = (fun (x:int) (y:int) => x + y) 1
+

File test/basic/add_01.sl

+DEF main = 1 + 2

File test/basic/add_1_2.sl

+SIG add : int -> int -> int
+DEF add (x:int) (y:int) = x + y
+DEF main = add 1 2

File test/basic/inc3by5.sl

+DEF main =
+    let add = fun (x:int) => 5 + x
+     in add 3
+

File test/beta_contraction/head_list.sl

+DEF main = 
+    let nil c1 c2 = c1 in
+    let cons x xs d1 d2 = d2 x xs in
+    let isnil ys = ys 1 (fun q w => 0) in
+    let iscons bs = bs 0 (fun e r => 1) in
+    let head zs = zs 0 (fun a b => a) in
+    let list1 = cons 10 nil in
+    head list1 

File test/beta_contraction/head_tail_list.sl

+DEF main = 
+    let nil c1 c2 = c1 in
+    let cons x xs d1 d2 = d2 x xs in
+    let cons2 xx xxs dd1 dd2 = dd2 xx xxs in
+    let isnil ys = ys 1 (fun q w => 0) in
+    let iscons bs = bs 0 (fun e r => 1) in
+    let head zs = zs 0 (fun a b => a) in
+    let tail zs = zs 0 (fun aa bb => bb) in
+    let list1 = cons 10 (cons2 20 nil) in
+    head (tail list1)

File test/beta_contraction/head_tail_list_defs.sl

+DEF nil c1 c2 = c1
+DEF cons x xs d1 d2 = d2 x xs
+DEF cons2 xx xxs dd1 dd2 = dd2 xx xxs
+DEF isnil ys = ys 1 (fun q w => 0)
+DEF iscons bs = bs 0 (fun e r => 1)
+DEF head zs = zs 0 (fun a b => a)
+DEF tail zs = zs 0 (fun aa bb => bb)
+DEF list1 = cons 10 (cons2 20 nil)
+DEF main = head (tail list1)

File test/conditions/a_eq_a.sl

+DEF main =
+    if a == a
+        then 10
+        else 20

File test/conditions/a_eq_b_twice.sl

+DEF main =
+    if (a == b) && (a == b)
+        then 10
+        else 20

File test/fib01.sl

-SIG fib : int -> int
-DEF fib n =
-    if n == 0
-        then 1
-        else if n == 1
-            then 1
-            else fib (n-1) + fib (n-2)
-DEF main = fib 0

File test/fib02.sl

-SIG fib : int -> int
-DEF fib n =
-    if n == 0
-        then 1
-        else if n == 1
-            then 1
-            else fib (n-1) + fib (n-2)
-DEF main = fib 1

File test/fib03.sl

-SIG fib : int -> int
-DEF fib n =
-    if n == 0
-        then 1
-        else if n == 1
-            then 1
-            else fib (n-1) + fib (n-2)
-DEF main = fib 3

File test/frac01.sl

-SIG frac : int -> int -> int
-DEF frac aux n =
-    if n == 0
-        then aux
-        else frac (n*aux) (n - 1)
-DEF main = frac 1 0
-

File test/frac02.sl

-SIG frac : int -> int -> int
-DEF frac aux n =
-    if n == 0
-        then aux
-        else frac (n*aux) (n - 1)
-DEF main = frac 1 2
-

File test/frac03.sl

-SIG frac : int ->  int -> int
-DEF frac aux n =
-    if n == 0
-        then aux
-        else frac (n*aux) (n - 1)
-DEF main = frac 1 5
-

File test/frac04.sl

-SIG frac2 : int -> int -> int
-DEF frac2 aux n =
-    if n == 0
-        then aux
-        else frac2 (n*aux) (n - 1)
-
-SIG frac : int -> int
-DEF frac x = frac2 1 x
-DEF main = frac 3
-

File test/inliner/add_1_2_mult_add_1_3.sl

+SIG add : int -> int -> int
+DEF add x y = x + y
+DEF main = add 1 2 * add 1 3

File test/inliner/fib_0.sl

+SIG fib : int -> int
+DEF fib n =
+    if n == 0
+        then 1
+        else if n == 1
+            then 1
+            else fib (n-1) + fib (n-2)
+DEF main = fib 0

File test/inliner/fib_1.sl

+SIG fib : int -> int
+DEF fib n =
+    if n == 0
+        then 1
+        else if n == 1
+            then 1
+            else fib (n-1) + fib (n-2)
+DEF main = fib 1

File test/inliner/fib_3.sl

+SIG fib : int -> int
+DEF fib n =
+    if n == 0
+        then 1
+        else if n == 1
+            then 1
+            else fib (n-1) + fib (n-2)
+DEF main = fib 3

File test/inliner/frac_tail_1_0.sl

+SIG frac : int -> int -> int
+DEF frac aux n =
+    if n == 0
+        then aux
+        else frac (n*aux) (n - 1)
+DEF main = frac 1 0
+

File test/inliner/frac_tail_1_2.sl

+SIG frac : int -> int -> int
+DEF frac aux n =
+    if n == 0
+        then aux
+        else frac (n*aux) (n - 1)
+DEF main = frac 1 2
+

File test/inliner/frac_tail_1_5.sl

+SIG frac : int ->  int -> int
+DEF frac aux n =
+    if n == 0
+        then aux
+        else frac (n*aux) (n - 1)
+DEF main = frac 1 5
+

File test/inliner/frac_tail_helper_3.sl

+SIG frac2 : int -> int -> int
+DEF frac2 aux n =
+    if n == 0
+        then aux
+        else frac2 (n*aux) (n - 1)
+
+SIG frac : int -> int
+DEF frac x = frac2 1 x
+DEF main = frac 3
+

File test/inliner/head_map_list.sl

+DEF nil c1 c2 = c1
+DEF cons x xs c1 c2 = c2 x xs
+DEF map f xs = xs nil (fun y ys => cons (f y) (map f ys))
+DEF list = cons 0 (cons 1 (cons 2 nil))
+DEF head xs = xs 0 (fun x xs => x)
+DEF main = head (map (fun x => x + 1) list)

File test/inliner/mutual_not_wf.sl

+SIG f : int -> int -> int
+SIG g : int -> int
+DEF f x (y:int) = g x
+DEF g x = f x x
+
+DEF main = 4
+

File test/inliner/rebuild_nat_3.sl

+SIG rebuild : int -> int
+DEF succ n = n + 1
+DEF pred n = n - 1
+
+DEF rebuild n = if n == 0 then 0 else succ (rebuild (pred n))
+DEF main = rebuild 3
+

File test/inliner/rebuild_nat_3_add_2.sl

+SIG rebuild : int -> int
+DEF succ n = n + 1
+DEF pred n = n - 1
+
+DEF rebuild n = if n == 0 then 0 else succ (rebuild (pred n))
+DEF main = rebuild 3 + rebuild 2
+

File test/inliner/rebuild_nat_rebuild_3_add_2.sl

+SIG rebuild : int -> int
+DEF succ n = n + 1
+DEF pred n = n - 1
+
+DEF rebuild n = if n == 0 then 0 else succ (rebuild (pred n))
+DEF main = rebuild (rebuild 3 + rebuild 2)
+

File test/rebuild01.sl

-SIG rebuild : int -> int
-DEF succ n = n + 1
-DEF pred n = n - 1
-
-DEF rebuild n = if n == 0 then 0 else succ (rebuild (pred n))
-DEF main = rebuild 3
-

File test/rebuild02.sl

-SIG rebuild : int -> int
-DEF succ n = n + 1
-DEF pred n = n - 1
-
-DEF rebuild n = if n == 0 then 0 else succ (rebuild (pred n))
-DEF main = rebuild 3 + rebuild 2
-

File test/rebuild03.sl

-SIG rebuild : int -> int
-DEF succ n = n + 1
-DEF pred n = n - 1
-
-DEF rebuild n = if n == 0 then 0 else succ (rebuild (pred n))
-DEF main = rebuild (rebuild 3 + rebuild 2)
-