ocaml/problems.ml

   1 let use_lambda3 = Array.length Sys.argv = 1;;
   2
   3 let discriminator = ( module Lambda4 : Discriminator.Discriminator );;
   4 module Pippo = (val discriminator);;
   5 open Pippo;;
   6
   7 let p2 = magic [ "x y"; "x z" ; "x (y z)"] ["*"]
   8
   9 let p4 = magic
  10   [ "x y"; "x (a. a x)" ; "y (y z)" ] ["*"]
  11
  12 let p5 = magic
  13   ["a (x. x a) b"; "b (x. x b) a"]
  14   ["*"]
  15 ;;
  16
  17 let p6 = magic
  18   ["a (x. x a) b"; "b (x. x b) (c a)"]
  19   ["*"]
  20 ;;
  21
  22 let p7 = magic
  23   ["a (x. (x a)(a x x a)(x x) )"]
  24   ["*"]
  25 ;;
  26
  27 let p8 = magic
  28   ["x x (x x)"]
  29   ["*"]
  30 ;;
  31
  32 let p9 = magic
  33   ["x x (x x x) (x x (x x)) (x x (x x x)) x x"]
  34   ["*"]
  35 ;;
  36
  37 let p10 = magic
  38   ["x (y (x a b c))"]
  39   ["*"]
  40 ;;
  41
  42 let p11 = magic
  43   ["x x"; "x (y.y)"]
  44   ["*"]
  45 ;;
  46
  47 let p12 = magic
  48   ["x x (x x)"; "x x (x (y.y))"]
  49   ["*"]
  50 ;;
  51
  52 let p13 = magic
  53   ["x x (x x (x x x x x (x x)))"]
  54   ["*"]
  55 ;;
  56
  57 let p14 = magic
  58   ["a (a a (a (a a)) (a (a a)))"]
  59   ["*"]
  60 ;;
  61
  62 let p15 = magic
  63   ["a (a (a a)) (a a (a a) (a (a (a a))) (a (a a)) (a a (a a) (a (a (a a))) (a (a a)))) (a a (a a) (a (a (a a))) (a (a a)))"]
  64   ["*"]
  65 ;;
  66
  67 let p16 = magic
  68   ["a (a a) (a a (a (a a)) (a (a a)) (a a (a (a a)) a))"]
  69   ["*"]
  70 ;;
  71
  72 let p17 = magic
  73   ["b a"; "b (c.a)"]
  74   ["*"]
  75 ;;
  76
  77 let p18 = magic
  78   ["a (a a) (a a a (a (a (a a) a)) (a a a (a (a (a a) a))))" ; "a a" ; "a (a a)"]
  79   ["*"]
  80 ;;
  81
  82 let p19 = magic
  83   ["a (a a) (a a a (a (a (a a) a)) a)"]
  84   ["*"]
  85 ;;
  86
  87 let p20 = magic
  88   ["a (a b) (b (a b) (a (a b))) (a (a b) (a (a b)) (a (a b)) c) (a (a b) (a (a b)) (b (a b)) c (a a (a (a b) (a (a b)) b)) (a (a b) (a (a b)) (b (a b)) (a a) (a c (b (a b)))))"]["*"];;
  89
  90 let p21 = magic
  91   ["(((y z) (y z)) ((z (y z)) ((y z) (z z))))";
  92    "(((z z) x) (y z))";
  93    "((z (y z)) ((y z) (z z)))"
  94 ] ["*"];;
  95
  96 let p22 = magic
  97 ["((z y) ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))";
  98 "((z y) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) (((((y (z y)) x) (y (z y))) ((y (z y)) (z z))) ((x y) (z z)))))";
  99 "(y ((((y (z y)) x) (y (z y))) ((y (z y)) (z z))))"] ["*"];;
 100
 101 (* diverging tests *)
 102 (* test p23 leads to test p24 *)
 103 let p23 = magic
 104 ["z z z"; "z (z z) (x. x)"] ["*"];;
 105
 106 (* because of the last term, the magic number is 1 and we diverge;
 107    but setting the magic number to 0 allows to solve the problem;
 108    thus our strategy is incomplete *)
 109 let p24 = magic
 110 ["b b"; "b f"; "f b"; "a (x.x)"] ["*"];;
 111
 112 (* because of the last term, the magic number is 1 and we diverge;
 113    but setting the magic number to 0 allows to solve the problem;
 114    thus our strategy is incomplete *)
 115 let p25 = magic
 116 ["b b"; "b f"; "f b"; "f (x.x)"] ["*"];;
 117
 118 (* BUG:
 119    0 (n (d (o.n) ...)))
 120    After instantiating n, the magic number (for d) should be 2, not 1! *)
 121 let p26 = magic
 122 ["(((x y) (z. (y. (y. z)))) (z. y))";
 123 "(((x y) x) (y y))"] ["*"];;
 124
 125 let p27 = magic
 126 ["(((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))) ((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))))";
 127 "((((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)) (((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y)))";
 128 "(((((z y) (z (z y))) (z (z y))) ((z y) (((z y) (z (z y))) ((z y) x)))) (((((z y) (z (z y))) (z (z y))) x) y))"] ["*"];;
 129
 130 let p28 = magic
 131 ["((((z (x. (z. (x. x)))) (z x)) x) (z (x. (z. (x. x)))))";
 132  "(((z (x. (z. (x. x)))) (z x)) ((z x) (x. (z. (x. x)))))" ] ["*"];;
 133
 134 let p29 = magic
 135 ["((((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y) ((x x) y))";
 136 "(((((x x) (x x)) (z. (y x))) (z. ((x x) y))) y)"] ["*"];;
 137
 138 let p30 = magic
 139 ["((b c) (b. (z a)))";
 140 "((v (a. (z v))) ((y (b c)) ((z a) (v y))))";
 141 "((v (v. c)) z)";
 142 "((v y) (v (a. (z v))))";
 143 "((y (b c)) ((z a) (v y)))"] ["*"];;
 144
 145 let p31 = magic
 146 [" (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))";
 147 "((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))";
 148 "(((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))";
 149 "(((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))";
 150 "((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))"] ["*"];;
 151
 152 let p32 = magic
 153 ["(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) (y. (a y)))";
 154 "(((((a y) v) (z a)) (z (((z a) (z a)) (w. v)))) a)";
 155 "(((((z a) (z a)) b) (v. (v. (z a)))) (v. ((a y) v)))";
 156 "((((a y) v) (z a)) (z (((z a) (z a)) (w. v))))";
 157 "((((w (a. (z. ((z a) (z a))))) (v. ((a y) v))) (((z a) (z a)) b)) (w. (((z a) (z a)) (c. (c ((z a) (z a)))))))"
 158 ] ["*"];;
 159
 160 (* Shows an error when the strategy that minimizes special_k is NOT used *)
 161 let p33 = magic
 162 [
 163 "((((((v (y. v)) (w. (c. y))) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b))) (((y (y (v w))) z) ((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)))) (b c)) (((v w) (z (a (c. y)))) ((y b) (b (z (a (c. y)))))))";
 164 "((((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y)) (c. y))";
 165 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) ((a (c. y)) b)) (c. y))";
 166 "(((((a (c. y)) (v w)) ((b (z (a (c. y)))) (b (z (a (c. y)))))) (b (z (a (c. y))))) ((c b) (b. (b w))))";
 167 (* "(((((a (c. y)) b) v) (z (a (c. y)))) (a. (b (z (a (c. y))))))" *)
 168 ] ["*"];;
 169
 170 let p34 = magic [
 171 "b c (b c) (c (d (j. e))) (b c (b c) (j.c f)) (b f (j. k. d)) (b (j. k. l. b c (b c)) (b g)) a";
 172 "d (j. e) e (j. c f) (j. c j) b a";
 173 "d (j. e) e (j. c f) b (b c (b c) (j. c f)) a";
 174 "d (j. e) e (j. c f) b (b c (b c) (j. c f) (g b)) a";
 175 "d (j. e) e (j. c f) b (j. k. j (l. e) e (l. k f) b) a";
 176 ] ["*"];;
 177 (* 0: (b c (b c) (c (d j.e)) (b c (b c) j.(c f)) (b f j.k.d) (b j.k.l.(b c (b c)) (b g)) a)
 178 1: (d j.e e j.(c f) j.(c j) b a)
 179 2: (d j.e e j.(c f) b (b c (b c) j.(c f)) a)
 180 3: (d j.e e j.(c f) b (b c (b c) j.(c f) (g b)) a)
 181 4: (d j.e e j.(c f) b j.k.(j l.e e l.(k f) b) a) *)
 182
 183 let p35 = magic [
 184 "(((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (z (z b))) ((y y) (((b z) v) (a ((v (y y)) (v (y y)))))))";
 185 "((((((((a b) z) w) (((b z) v) (a ((v (y y)) (v (y y)))))) ((y y) ((y (v (y y))) b))) ((((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) (((((c (a b)) (y y)) (y (v (y y)))) (z w)) ((w (((v (y y)) (v (y y))) a)) (w (z ((y (v (y y))) b)))))) (z w))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (c (a b)))) (((((b z) (c b)) (c ((v (y y)) (v (y y))))) (((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))) ((c b) (z (z b))))) (((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b)))))) (((((w ((a b) z)) (a ((v (y y)) (v (y y))))) (((v (y y)) (v (y y))) a)) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) (b (((v (y y)) (v (y y))) ((y y) (z (z b))))))) (b z))) ((x ((c b) (c b))) (((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y))))))))))";
 186 "((((((((b z) v) (a ((v (y y)) (v (y y))))) (y (v (y y)))) ((w ((a b) z)) (a ((v (y y)) (v (y y)))))) (z ((y (v (y y))) b))) (((y (v (y y))) ((y (v (y y))) x)) ((((c (a b)) (y y)) ((y (v (y y))) b)) (((c (a b)) (y y)) ((y (v (y y))) b))))) (v (y y)))"
 187 ] ["*"];;
 188
 189 let p36 = magic
 190 [
 191 "(((((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (((y c) (x a)) (v (((y a) (((z v) (y a)) (b a))) z)))) ((b a) (b a))) ((a c) (b (((y a) (((z v) (y a)) (b a))) (z a))))) ((((((b (((y a) (((z v) (y a)) (b a))) z)) (c ((y (x a)) ((z v) (y a))))) (v (((y a) (((z v) (y a)) (b a))) z))) (((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))) ((x a) (((y a) (((z v) (y a)) (b a))) z)))) ((c ((y (x a)) ((z v) (y a)))) (b (((y a) (((z v) (y a)) (b a))) z)))) ((((b (z a)) (y a)) (y c)) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y))))))))";
 192 "(((((((z v) (y a)) (b a)) w) b) (((b a) ((((z v) (y a)) (b a)) w)) ((((z v) (y a)) (b a)) w))) (((b a) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) w)) (((c y) a) v)))";
 193 "(((((((z v) (y a)) (b a)) w) b) (a (((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a)) ((((y a) (((z v) (y a)) (b a))) z) (((z v) (y a)) (c y)))))) ((((y a) (((z v) (y a)) (b a))) ((((y a) (((z v) (y a)) (b a))) ((b a) (b a))) (x a))) x))"
 194 ] ["*"];;
 195
 196 (* issue with eta-equality of terms in ps *)
 197 let p37 = magic
 198   ["x (a y) z"; "x (a z. y z) w"; "a c"]
 199   ["*"];;
 200
 201 (**********************)
 202
 203 let q1 () = magic_conv
 204  None
 205  ["a d e"]
 206  ["a b"; "a c"]
 207  ["*"];;
 208
 209 let q2 () = magic_conv
 210  None
 211  ["a d e"]
 212  ["a b" ]
 213  ["*"];;
 214
 215 let q3 () = magic_conv
 216  (Some "x")
 217  ["a d e f"]
 218  ["a b" ]
 219  ["*"];;
 220
 221 let q4 () = magic_conv
 222  None
 223  ["f (x.a b c d)"]
 224  ["a b" ]
 225  ["*"];;
 226
 227 let q5 () = magic_conv
 228  (Some"x")
 229  ["(y. x)"]
 230  ["x"]
 231  ["*"];;
 232
 233 let q6 () = magic_conv
 234  (Some"x")
 235  ["(y. x z)"]
 236  ["y"]
 237  ["*"];;
 238
 239 let q7 () = magic_conv
 240  (Some "(b (c d (e f f k.(g e))) f)")
 241  ["(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (f d k.g (b (g (e f)) (b (g (e f)) (e f)) (g (e f) (g e h)))) k.l.(h f (b i)))";
 242   "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (b (g (e f))) k.l.(g f (k f f (k f f m.(g k)))))";
 243   "(b (g (e f)) f k.e k.l.(f d (e f)) (c d (e f f k.(g e)) (g k.(e f f))) (h f (i (h k.(i b l.m.n.e)))))"]
 244  ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)";
 245   "(f d (e f) k.e k.l.(c d) (b (g e) k.h) (d k.e) (f d (e f) k.e) a)";
 246   "(g (e f) (g e h) (f d (e f) k.e) k.(c d l.(c d)) (g e h) (g f (e f f (e f f k.(g e))) (g (e f)) (b (c d (e f f k.(g e))) (b (g (e f)) (e f)) (b (g (e f)) k.l.e))) a)"]
 247  ["*"];;
 248
 249 (**********************)
 250
 251 let q8 () = magic_conv
 252  (Some"x a")
 253  ["y (x b c)"] ["j"] ["*"]
 254 ;;
 255
 256 let q9 () = magic_conv
 257  (Some"x a")
 258  ["y x"] ["a (y a b b b)"] ["*"]
 259 ;;
 260
 261 let q11 () = magic_conv
 262  (Some "x y")
 263  ["a (x z)"] [] ["*"];;
 264
 265 let q10 () = magic_conv
 266  (Some "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f)
 267 (k. e (f g))) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b
 268  (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))")
 269 ["e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c))) (c f (k. b (l. c)) (k. l. b (m. c))) (k. l. b (m. c) d (l (f k) (m. k)) (m. n. c)) (c f (k. b (l. c)) (k. b (l. c) d) (k. c k))";
 270 "e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k))";
 271 "b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c))";
 272 "b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (b (k. c) (k. e) (k. l. m. b (n. c))) (e (f g) (k. g) (c f) (k. i) (k. l. h) (k. l. m. n. m) (b (k. c) (k. l. b (m. c)) (k. c f)) (k. l. m. k (f g) (n. g) (c f) (n. k)))";
 273 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (b (k. c) (k. l. b (m. c)) (k. c f) (k. e (f g)))"]
 274 [
 275 "b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f)) (b (k. c) (k. e) f (b (k. c) (k. l. b (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))";
 276 "b (k. c) d (e (f g) (k. g)) (k. l. m. n. m) (k. l. m. b (n. k) d (b (n. k))) (e (f g) (k. g) (c f) (k. e) (k. b (l. c) d (b (l. c)))) (k. e (f g) (l. g) (c f) (l. k) (l. m. h))";
 277 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. m. n. o. p. o) (e (f g) (k. g) (c f) (k. i) f)";
 278 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)";
 279 "e (f g) (k. g) (c f) (k. e) (k. b (l. c)) (c f (k. b (l. c)) (k. l. b (m. k))) (k. b (l. k)) (e (f g) (k. g) (c f) (c f (k. b (l. c)) (k. e)))";
 280 ] ["*"];;
 281
 282 let m1 () = magic_conv None []
 283  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 284  ["*"]
 285 ;;
 286
 287 let m2 () = magic_conv None []
 288  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 289  ["*"]
 290 ;;
 291
 292 main ([
 293  (* p2 ; p4 ; p5 ; p6 ; p7 ; p8 ; p9 ; p10 ; p11 ; p12 ; p13 ; p14 ; p15 ; p16 ; p17 ; p18 ; p19 ; p20 ; p21 ; p22 ; p23 ; p24 ; p25 ; p26 ; p27 ; p28 ; p29 ; p30 ; p31 ; p32 ; p33 ; p34 ; p35 ; p36 ; p37 ; *)
 294  p24 ; p25 ;
 295 ] @ if use_lambda3 then [] else List.map ((|>) ()) [
 296  q1 ; q2; q3; q4 ; q5 ; q6 ;
 297  (* q7 ; *)
 298  q8 ;
 299  q9 ;
 300  q10 ;
 301  q11 ;
 302  m1 ;
 303 ]);;