ocaml/problems.ml

   1 open Lambda4;;
   2 open Util;;
   3
   4 (* Syntax for problem files in problem/ folder:
   5
   6 - dollar ($) on newline
   7   begin new problem
   8   $! means that the problem is expected to be separable,
   9   $? means that it is expected to be unseparable
  10
  11 - (#) on new line
  12   comment line
  13
  14 - (D) (C) (N) stand respectively for divergent, convergent, numeric
  15
  16 - lines starting with spaces inherit the type from the last line
  17
  18 *)
  19
  20 let assert_separable x =
  21  match solve x with
  22  | `Separable _ -> ()
  23  | `Unseparable s ->
  24    failwith ("assert_separable: unseparable because: " ^ s ^ ".")
  25 ;;
  26
  27 let assert_unseparable x =
  28  match solve x with
  29  | `Unseparable _ -> ()
  30  | `Separable _ ->
  31    failwith ("assert_unseparable: separable.")
  32 ;;
  33
  34 let assert_depends x =
  35  let c = String.sub (Lambda4.label_of_problem x) 0 1 in
  36  if c = "!" then assert_separable x
  37   else if c = "?" then assert_unseparable x
  38    else (solve x; ())
  39 ;;
  40
  41 let main () =
  42 ((* <main> *)
  43
  44 let solve_many = List.iter assert_separable in
  45
  46 (* TODO *)
  47 (* div under a lambda in conv *)
  48 (* assert_unseparable (problem_of (Some"`y y") ["x (_. y y)"] []);; *)
  49
  50 List.iter (assert_separable ++ Lambda4.tmp) (Parser.from_file "problems/p");
  51
  52 (* q-series problems *)
  53
  54 let q1 () = problem_of
  55  None
  56  ["a d e"]
  57  ["a b"; "a c"]
  58  in
  59
  60 let q2 () = problem_of
  61  None
  62  ["a d e"]
  63  ["a b" ]
  64  in
  65
  66 let q4 () = problem_of
  67  None
  68  ["f (x.a b c d)"]
  69  ["a b" ]
  70  in
  71
  72 let q5 () = problem_of
  73  (Some"x x")
  74  ["x"]
  75  ["x"]
  76  in
  77
  78 let q6 () = problem_of
  79  (Some"x x")
  80  ["(y. x z)"]
  81  ["y"]
  82  in
  83
  84 let q7 () = problem_of
  85  (Some "(b (c d (e f f k.(g e))) f)")
  86  ["(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)))";
  87   "(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)))))";
  88   "(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)))))"]
  89  ["(f d (e f) k.e k.l.(c d) (b (g e) k.h) (i b k.l.m.e b) a)";
  90   "(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)";
  91   "(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)"]
  92  in
  93
  94 (**********************)
  95
  96 let q8 () = problem_of
  97  (Some"x a")
  98  ["y (x b c)"] ["j"]
  99 in
 100
 101 let q9 () = problem_of
 102  (Some"x a")
 103  ["y x"] ["a (y a b b b)"]
 104 in
 105
 106 let q11 () = problem_of
 107  (Some "x y")
 108  ["a (x z)"] [] in
 109
 110 let q10 () = problem_of
 111  (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)
 112 (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
 113  (m. c)) (k. c f))) (k. b (l. c) b (l. b (m. c))) (k. b (l. c)))")
 114 ["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))";
 115 "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))";
 116 "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))";
 117 "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)))";
 118 "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)))"]
 119 [
 120 "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)))";
 121 "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))";
 122 "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)";
 123 "b (k. c) d (e (f g) (k. g)) (k. l. c) (k. l. b (m. c)) (k. l. c) (k. b)";
 124 "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)))";
 125 ] in
 126
 127 let m1 () = problem_of None []
 128  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 129
 130 in
 131
 132 let m2 () = problem_of None []
 133  ["y z"; "x z"; "x (a k) u"; "x (a r)"; "x (a k) v"]
 134
 135 in
 136
 137
 138 let n1 () = problem_of (Some"b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (g (k. c e) (k. i) (c b) (f c) b)")
 139 [
 140 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. i))";
 141 "g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. l. g (m. c e) (m. i) (c b) (l c) b) (e c (d d (d c)) (c e (k. f)) (b (c b) (k. l. c b d) (c e) (k. l. m. f)))";
 142 "b (c b) (k. l. c b d) (c e) (k. l. m. f) (g (k. c e) (b (c b) (k. l. c b d) (c e) b)) (f c (h (k. c c g))) (g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e))";
 143 "b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. l. m. c c g) (e c (b (k. f))) (k. f c)";
 144 "c (c e) (e c (d d (d c)) (k. c e (f c))) (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d) (k. c e (l. f) (k (l. c e) (l. i)))) (k. l. l (m. c e) (m. i) (c b) (f c) b) (k. l. c k) (f (f c) (b (c b) (k. l. c b d) (c e)) (b (k. f) (g (k. c e) (k. i) (c b) (c (c e))) (k. l. m. f) (g (k. c e) (k. i) f e) (k. l. m. c c g) (e c (b (k. f)))))";
 145 ] [
 146 "b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (h (g (k. c e) (k. i) (c b) (c (c e)))) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a";
 147 "c c g (k. b (c b) (l. m. c b k) (c e)) (k. b (c b) (l. m. c b d) (c k) b) (k. e c (d h) k) (g (k. c e) (b (c b) (k. l. c b d) (c e) b) (g (k. c e) (k. i) (g (k. c e) (k. i) e) (e c (d d (d c)) (k. c e (f c))))) a";
 148 "d h (b (c b) (k. l. c b d) (c e)) (k. g (l. c e) (l. i) (c b) (k c) b) d b (b (c b) (k. l. c b d) (c e) b (g (k. c e) (k. i) (c b)) (k. c)) a";
 149 "g (k. c e) (k. d d) (k. k k) (e c (d d (d c)) i) (k. g (l. k e) (l. d d)) (g i (b (c b) (k. l. c b d) (e c (d d (d c)) (k. c e (f c)) (k. k (c k) (l. m. c k d) (c e) k (g (l. c e) (l. i) (c k)) (l. c))))) (c b) a";
 150 "g (k. c e) (k. i) f e (g (k. c e) (k. i) (c b) (c (c e)) (k. l. c b d)) (k. e c (k (l. f))) (g (k. c e) (k. i) e) a"
 151 ] in
 152
 153 let n2 () = problem_of
 154 (Some"b b (c d) (k. d e) (k. k) (k. l. b)")
 155 [
 156 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))))) (d e (k. d e) g (i (k. k)))";
 157 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (d (g (de) (g (k. e)) h) (g (k. b b)))";
 158 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. l. l) (k. g (d e) (l. m. m))";
 159 "b b (d e (k. d e)) (g (k. e) (k. k)) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (k. k (k k) (l. l))) (f (e (c d))) (b b (d e (k. d e)) (b b) (b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h)))))";
 160 "d (g (d e) (g (k. e)) h) (g (g (d e)) (d e (k. d e) (k. b (l. h)) (k. l. d e))) (b (k. h) (k. k e (l. m. b b)) (k. k (k k) (l. l))) (k. b) (b b (k. l. i)(k. c))";
 161 ] [
 162 "b (b b) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k))) (k. l. d (g (d k) (g (m. k)) h) (d k (m. n. b b))) (e (c d) (e (c d))) a";
 163 "d (g (d e) (g (k. e)) h) (d e (k. l. b b)) (b b) h (k. g (l. e) (l. l)) a";
 164 "d e (k. d e) (k. b (l. h)) (k. l. d e) (d (g (d e) (g (k. e)) h) (g (d e) (k. l. l))) a";
 165 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (k. c) (k. l. m. b b) a";
 166 "f (g (k. e)) (k. b b) (c d (k. k d) (k. l. l) c) (k. c d) (b (b b) (d (g(d e) (g (k. e)) h) (b b (c d) (k. l. b)) (b (k. h))) (e (b b (c d))) (d (g (d e) (g (k. e)) h) (b b (c d) (k. l. b)) (g (k. e) (k. k)))) (k. d e (l. d e) f) a";
 167 ]
 168 in
 169
 170 let n3 () = problem_of
 171 (Some"b (k. c (c d e f)) (k. l. f (m. f) (m. f) (m. n. n))")
 172 [
 173 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) (k. l. l (m. l))";
 174 "c d e (f i) (e e) (g e) (k. l. e) (k. c (g (k (l. i)))) (c d e (k. k))";
 175 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (c d e (f i) (e e) (f (k. h))) (g e (b (k. i)) (e e (e e)))";
 176 "f (k. f) (k. f) (k. e) (c d e (f i) (e e) (g e)) (k. e e) (k. l. m. e) (k. e)";
 177 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f)";
 178 ][
 179 "b (g (k. e e)) (k. b (g (l. e e))) (g (h (k. i)) (k. e)) (f (k. f) (k. f) i) (i (k. c (c d e f)) (k. l. l) (k. g (h (l. i)) (k d) f) e) (k. l. h) (k. f (l. f) (l. f) (l. e)) a";
 180 "c d e (f i) (e e) (g e) (b (g (k. e e)) (k. c (g (h (l. i))) (l. f l))) (k. f (l. f) (l. f)) a";
 181 "e e (k. k d e (l. l)) (g e) (c d e b (e e (c (c d e f)))) (d (e e (k. k d e (l. l))) (k. k i)) (k. i (l. c (c d e f))) (k. h) a";
 182 "f (k. f) (k. f) (f h) (f h (c d e (f i))) (k. b) (f i (c d e)) (k. h) a";
 183 "g e f (f (k. f) (f (k. f) (k. l. f)) (c d e b)) (f (k. f) (k. f) (k. l. l) b) (f (k. h)) (c d e (f i) (e e) (g e) (k. l. e)) (f (k. f) f) (f (k. f) (k. f) (k. l. l) (c (k. i (l. c (c d e f))))) a";
 184 ] in
 185
 186 solve_many [
 187  problem_of
 188  (* DISPLAY PROBLEM (main) - measure=965
 189     Discriminating sets (deltas):
 190     0 <> 1 <> 2 <> 3 <> 4
 191  *)(* DIVERGENT  *)
 192       (Some"b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (k. b c d (l. c (l k)) (b c (l. e e) (b c d (l. e l) (e e (b (l. m. b)) d (l. d))) (l. c)))")
 193    (* CONVERGENT *) [
 194    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e) (k. g (l. g (m. b c)) (l. i (f g)))";
 195    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h))) (b c (k. c (e h)))";
 196    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. e e)";
 197    (* _ *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. d k (k (l. m. k)) (c (e h)))";
 198    (* _ *) "b (k. l. b) (e f) (b c d) (e e (b (k. l. b)) d) (e (k. l. b c) (k. l. b k) (b c)) d (e e (e e) (d (k. f)) (b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))))) (e e (b (k. l. b)) (b (k. l. b) (e f) (b c
 199  d)) (e e (b (k. l. b)) d (k. d) (b (k. l. b))) (k. b c k (l. e l) (e e (b (l. m. b)) k (l. k)) (f g (c (e h))) (k b (l. b) (f g (e f))) (c (e h))) (k. i (f g) (l. l)))";
 200  ] (* NUMERIC    *) [
 201    (* 0 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (d b (k. b)) (k. l. c (l k)) a";
 202    (* 1 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) a";
 203    (* 2 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) a";
 204    (* 3 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. l. c (k h)) (d b (b c d (k. c (k h))) (b c d (k. e k) (b c))) a";
 205    (* 4 *) "b c d (k. e k) (e e (b (k. l. b)) d (k. d)) (f g (c (e h))) (d b (k. b) (f g (e f))) (c (e h)) (e e (b (k. l. b)) (k. e k)) (k. b k d (l. e l) (e e (b (l. m. b)) d (l. d)) (f g (k (e h)))) a";
 206  ];
 207  problem_of
 208  (* DISPLAY PROBLEM (main) - measure=561
 209     Discriminating sets (deltas):
 210     0 <> 1 <> 2 <> 3 <> 4
 211  *)(* DIVERGENT  *)
 212       (Some"b (c b) (k. d) (e f (k. e) (k. b) (f d)) (e f (k. g k) d) (k. c k (c k g))")
 213    (* CONVERGENT *) [
 214    (* _ *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g) (e f (k. k (g e) h) b (e (k. g) (h c (g c) f)))";
 215    (* _ *) "e f (k. k) (k. l. c b) (k. l. l (k b) g) (k. e f (l. l)) (h c (c (k. l. l b k) (k. l. d) (e f (k. k) (g e))) (k. g e (g e))) (k. g (l. e f g) (l. h c) (g (l. e f g) (l. h c)))";
 216    (* _ *) "e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (k. l. g l (g l) (m. c b))";
 217    (* _ *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. g)";
 218    (* _ *) "e f (k. k) (g e) (e f (k. e)) (e f (k. e)) (h c (b (g e) h (k. c (l. m. m k l))))";
 219  ] (* NUMERIC    *) [
 220    (* 0 *) "c (k. l. l b k) (k. l. d) (e f (k. k) (g e)) (k. l. m. n. n b m) (k. b (b (k e))) (k. i) a";
 221    (* 1 *) "e f (k. k (g e) h) (g (k. e f g) (c (c b g) (k. l. l b g))) (k. k (g e) h) (k. h) (b (b (g e)) (k. c (l. m. m b l))) (h (c b) g i) a";
 222    (* 2 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) a";
 223    (* 3 *) "e f (k. k) (g e) (e f (k. e)) (h (k. g e (g e)) (h (k. g e (g e)))) (k. d) (k. l. m. c k) a";
 224    (* 4 *) "g (k. e f g) (k. h c) (b (g e) h (k. c (l. m. m k l))) (k. c b g) (k. e f (l. l) (g e) (e f (l. e))) f a";
 225  ]
 226 ];
 227
 228 solve_many (List.map ((|>) ()) ([
 229  q1 ; q2; (*q3;*) q4 ; q5 ; q6 ;
 230  q7 ;
 231  q8 ;
 232  q9 ;
 233  q10 ;
 234  q11 ;
 235  m1 ;
 236  m2 ;
 237 ] @ [
 238  n1 ;
 239  n2 ;
 240  n3
 241 ]));
 242
 243 (* </main> *));;
 244
 245 if Array.length Sys.argv = 1
 246  then main ()
 247 else Array.iteri (fun i filename -> if i > 0 then
 248  List.iter (assert_depends ++ Lambda4.tmp) (Parser.from_file filename)
 249  ) Sys.argv
 250 ;;