ocaml/andrea9.ml

   1 let (++) f g x = f (g x);;\r
   2 \r
   3 let print_hline = Console.print_hline;;\r
   4 \r
   5 type var = int;;\r
   6 type t =\r
   7  | V of var\r
   8  | A of t * t\r
   9  | L of t\r
  10  | B (* bottom *)\r
  11  | P (* pacman *)\r
  12 ;;\r
  13 \r
  14 type problem = {\r
  15    orig_freshno: int\r
  16  ; freshno : int\r
  17  ; div : t\r
  18  ; conv : t\r
  19  ; sigma : (var * t) list (* substitutions *)\r
  20  ; stepped : var list\r
  21 }\r
  22 \r
  23 let all_terms p = [p.div; p.conv];;\r
  24 \r
  25 exception Done of (var * t) list (* substitution *);;\r
  26 exception Fail of int * string;;\r
  27 \r
  28 let string_of_t p =\r
  29   let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
  30   let rec string_of_term_w_pars level = function\r
  31     | V v -> if v >= level then "`" ^ string_of_int (v-level) else\r
  32      let nn = level - v-1 in\r
  33       if nn < 5 then List.nth bound_vars nn else "x" ^ (string_of_int (nn-4))\r
  34     | A _\r
  35     | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"\r
  36     | B -> "BOT"\r
  37     | P -> "PAC"\r
  38   and string_of_term_no_pars_app level = function\r
  39     | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)\r
  40     | _ as t -> string_of_term_w_pars level t\r
  41   and string_of_term_no_pars_lam level = function\r
  42     | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)\r
  43     | _ as t -> string_of_term_no_pars level t\r
  44   and string_of_term_no_pars level = function\r
  45     | L _ as t -> string_of_term_no_pars_lam level t\r
  46     | _ as t -> string_of_term_no_pars_app level t\r
  47   in string_of_term_no_pars 0\r
  48 ;;\r
  49 \r
  50 let string_of_problem p =\r
  51  let lines = [\r
  52   "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);\r
  53   "[DV] " ^ (string_of_t p p.div);\r
  54   "[CV] " ^ (string_of_t p p.conv);\r
  55  ] in\r
  56  String.concat "\n" lines\r
  57 ;;\r
  58 \r
  59 let problem_fail p reason =\r
  60  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
  61  print_endline (string_of_problem p);\r
  62  raise (Fail (-1, reason))\r
  63 ;;\r
  64 \r
  65 let freshvar ({freshno} as p) =\r
  66  {p with freshno=freshno+1}, freshno+1\r
  67 ;;\r
  68 \r
  69 let rec is_inert p =\r
  70  function\r
  71  | A(t,_) -> is_inert p t\r
  72  | V _ -> true\r
  73  | L _ | B | P -> false\r
  74 ;;\r
  75 \r
  76 let is_var = function V _ -> true | _ -> false;;\r
  77 let is_lambda = function L _ -> true | _ -> false;;\r
  78 let is_pacman = function P -> true | _ -> false;;\r
  79 \r
  80 let rec subst level delift fromdiv sub =\r
  81  function\r
  82  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
  83  | L t -> L (subst (level + 1) delift fromdiv sub t)\r
  84  | A (t1,t2) ->\r
  85   let t1 = subst level delift fromdiv sub t1 in\r
  86   let t2 = subst level delift fromdiv sub t2 in\r
  87   if t1 = B || t2 = B then B else mk_app fromdiv t1 t2\r
  88  | B -> B\r
  89  | P -> P\r
  90 and mk_app fromdiv t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
  91  | B | _ when t2 = B -> B\r
  92  | L t1 -> subst 0 true fromdiv (0, t2) t1\r
  93  | t1 -> A (t1, t2)\r
  94 and lift n =\r
  95  let rec aux n' =\r
  96   function\r
  97   | V m -> V (if m >= n' then m + n else m)\r
  98   | L t -> L (aux (n'+1) t)\r
  99   | A (t1, t2) -> A (aux n' t1, aux n' t2)\r
 100   | B -> B\r
 101   | P -> P\r
 102  in aux 0\r
 103 ;;\r
 104 let subst = subst 0 false;;\r
 105 \r
 106 let subst_in_problem (sub: var * t) (p: problem) =\r
 107 print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
 108  let p = {p with stepped=(fst sub)::p.stepped} in\r
 109  let conv = subst false sub p.conv in\r
 110  let div = subst true sub p.div in\r
 111  let p = {p with div; conv} in\r
 112  (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
 113  {p with sigma=sub::p.sigma}\r
 114 ;;\r
 115 \r
 116 let free_vars p t =\r
 117  let rec aux level = function\r
 118  | V v -> if v >= level then [v] else []\r
 119  | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
 120  | L t -> aux (level+1) t\r
 121  | B | P -> []\r
 122  in Util.sort_uniq (aux 0 t)\r
 123 ;;\r
 124 \r
 125 let visible_vars p t =\r
 126  let rec aux = function\r
 127  | V v -> [v]\r
 128  | A(t1,t2) -> (aux t1) @ (aux t2)\r
 129  | B | P\r
 130  | L _ -> []\r
 131  (* | Ptr n -> aux (get_conv p n) *)\r
 132  in Util.sort_uniq (aux t)\r
 133 ;;\r
 134 \r
 135 let rec hd_of = function\r
 136  | V n -> n\r
 137  | A(t, _) -> hd_of t\r
 138  | _ -> assert false\r
 139 ;;\r
 140 \r
 141 let rec nargs = function\r
 142  | V _ -> 0\r
 143  | A(t, _) -> 1 + nargs t\r
 144  | _ -> assert false\r
 145 ;;\r
 146 \r
 147 let get_subterm_with_head_and_args hd_var n_args =\r
 148  let rec aux = function\r
 149  | V _ | L _ | B | P -> None\r
 150  | A(t1,t2) as t ->\r
 151    if hd_of t1 = hd_var && n_args <= 1 + nargs t1\r
 152     then Some t\r
 153      else match aux t2 with\r
 154      | None -> aux t1\r
 155      | Some _ as res -> res\r
 156  in aux\r
 157 ;;\r
 158 \r
 159 let rec eta_eq l1 l2 t1 t2 = match t1, t2 with\r
 160  | L t1, L t2 -> eta_eq l1 l2 t1 t2\r
 161  | L t1, t2 -> eta_eq l1 (l2+1) t1 t2\r
 162  | t1, L t2 -> eta_eq (l1+1) l2 t1 t2\r
 163  | V a, V b -> a + l1 = b + l2\r
 164  | A(t1,t2), A(u1,u2) -> eta_eq l1 l2 t1 u1 && eta_eq l1 l2 t2 u2\r
 165  | _, _ -> false\r
 166 ;;\r
 167 let eta_eq = eta_eq 0 0;;\r
 168 \r
 169 \r
 170 let rec simple_explode p =\r
 171  match p.div with\r
 172  | V var ->\r
 173   let subst = var, B in\r
 174   sanity (subst_in_problem subst p)\r
 175  | _ -> p\r
 176 \r
 177 and sanity p =\r
 178  (* Sanity checks: *)\r
 179  if (function | P | L _ -> true | _ -> false) p.div then problem_fail p "p.div converged";\r
 180  if p.conv = B then problem_fail p "p.conv diverged";\r
 181 \r
 182  print_endline (string_of_problem p); (* non cancellare *)\r
 183  if p.div = B then raise (Done p.sigma);\r
 184  let p = if is_var p.div then simple_explode p else p in\r
 185  p\r
 186 ;;\r
 187 \r
 188 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 189 \r
 190 let eat p =\r
 191 print_cmd "EAT" "";\r
 192  let var = hd_of p.div in\r
 193  let n = nargs p.div in\r
 194  let rec aux m t =\r
 195   if m = 0\r
 196    then lift n t\r
 197    else L (aux (m-1) t) in\r
 198  let subst = var, aux n B in\r
 199  sanity (subst_in_problem subst p)\r
 200 ;;\r
 201 \r
 202 let step k n p =\r
 203  let var = hd_of p.div in\r
 204  print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 205  let rec aux' p m t =\r
 206   if m < 0\r
 207    then p, t\r
 208     else\r
 209      let p, v = freshvar p in\r
 210      let p, t = aux' p (m-1) t in\r
 211       p, A(t, V (v + k + 1)) in\r
 212  let p, t = aux' p n (V 0) in\r
 213  let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in\r
 214  let rec aux m t =\r
 215   if m < 0\r
 216    then aux' (k-1) t\r
 217    else L (aux (m-1) t) in\r
 218  let t = aux k t in\r
 219  let subst = var, t in\r
 220  sanity (subst_in_problem subst p)\r
 221 ;;\r
 222 \r
 223 let parse strs =\r
 224   let rec aux level = function\r
 225   | Parser.Lam t -> L (aux (level + 1) t)\r
 226   | Parser.App (t1, t2) ->\r
 227    if level = 0 then mk_app false (aux level t1) (aux level t2)\r
 228     else A(aux level t1, aux level t2)\r
 229   | Parser.Var v -> V v\r
 230   in let (tms, free) = Parser.parse_many strs\r
 231   in (List.map (aux 0) tms, free)\r
 232 ;;\r
 233 \r
 234 let problem_of div conv =\r
 235  print_hline ();\r
 236  let all_tms, var_names = parse ([div; conv]) in\r
 237  let div, conv = List.hd all_tms, List.hd (List.tl all_tms) in\r
 238  let varno = List.length var_names in\r
 239  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]} in\r
 240  (* activate bombs *)\r
 241  let p = try\r
 242   let subst = Util.index_of "BOMB" var_names, L B in\r
 243    subst_in_problem subst p\r
 244   with Not_found -> p in\r
 245  (* activate pacmans *)\r
 246  let p = try\r
 247   let subst = Util.index_of "PACMAN" var_names, P in\r
 248    let p = subst_in_problem subst p in\r
 249    (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
 250   with Not_found -> p in\r
 251  (* initial sanity check *)\r
 252  sanity p\r
 253 ;;\r
 254 \r
 255 let exec div conv cmds =\r
 256  let p = problem_of div conv in\r
 257  try\r
 258   problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
 259  with\r
 260  | Done _ -> ()\r
 261 ;;\r
 262 \r
 263 let cut_app n t =\r
 264  let rec aux t =\r
 265   match t with\r
 266   | V _ as t -> 0, t\r
 267   | A(t1,_) as t ->\r
 268     let k', t' = aux t1 in\r
 269      if k' = n then n, t'\r
 270       else k'+1, t\r
 271   | _ -> assert false\r
 272  in snd (aux t)\r
 273 ;;\r
 274 \r
 275 let find_difference p t n_args =\r
 276  let t = cut_app n_args t in\r
 277  let rec aux t u k = match t, u with\r
 278  | V _, V _ -> assert false (* div subterm of conv *)\r
 279  | A(t1,t2), A(u1,u2) ->\r
 280     if not (eta_eq t2 u2) then (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k)\r
 281     else aux t1 u1 (k-1)\r
 282  | _, _ -> assert false\r
 283  in aux p.div t n_args\r
 284 ;;\r
 285 \r
 286 let rec count_lams = function\r
 287  | L t -> 1 + count_lams t\r
 288  | _ -> 0\r
 289 ;;\r
 290 \r
 291 let compute_k_from_args p hd_var j =\r
 292  let rec aux hd = function\r
 293  | A(t1,t2) -> max (\r
 294     if hd_of t1 = hd && (nargs t1) = j\r
 295      then (print_endline(string_of_t p t2);if t2 = V hd then j else count_lams t2)\r
 296      else 0) (max (aux hd t1) (aux hd t2))\r
 297  | L t -> aux (hd+1) t\r
 298  | V _ -> 0\r
 299  | _ -> assert false\r
 300  in aux hd_var\r
 301 ;;\r
 302 \r
 303 let rec auto p =\r
 304  let hd_var = hd_of p.div in\r
 305  let n_args = nargs p.div in\r
 306  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
 307  | None ->\r
 308     (try let p = eat p in problem_fail p "Auto did not complete the problem"  with Done _ -> ())\r
 309  | Some t ->\r
 310   let j = find_difference p t n_args - 1 in\r
 311   let k = max\r
 312    (compute_k_from_args p hd_var j p.div)\r
 313     (compute_k_from_args p hd_var j p.conv) in\r
 314   let p = step j k p in\r
 315   auto p\r
 316 ;;\r
 317 \r
 318 let interactive div conv cmds =\r
 319  let p = problem_of div conv in\r
 320  try (\r
 321  let p = List.fold_left (|>) p cmds in\r
 322  let rec f p cmds =\r
 323   let nth spl n = int_of_string (List.nth spl n) in\r
 324   let read_cmd () =\r
 325    let s = read_line () in\r
 326    let spl = Str.split (Str.regexp " +") s in\r
 327    s, let uno = List.hd spl in\r
 328     try if uno = "eat" then eat\r
 329     else if uno = "step" then step (nth spl 1) (nth spl 2)\r
 330     else failwith "Wrong input."\r
 331     with Failure s -> print_endline s; (fun x -> x) in\r
 332   let str, cmd = read_cmd () in\r
 333   let cmds = (" " ^ str ^ ";")::cmds in\r
 334   try\r
 335    let p = cmd p in f p cmds\r
 336   with\r
 337   | Done _ -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
 338  in f p []\r
 339  ) with Done _ -> ()\r
 340 ;;\r
 341 \r
 342 let _ = exec\r
 343  "x x"\r
 344  "@ (x y) (y y) (y x)"\r
 345  [ step 0 0; eat ]\r
 346 ;;\r
 347 \r
 348 auto (problem_of "x x" "@ (x y) (y y) (y x)");;\r
 349 auto (problem_of "x y" "@ (x (_. x)) (y z) (y x)");;\r
 350 auto (problem_of "a (x. x b) (x. x c)" "@ (a (x. b b) @) (a @ c) (a (x. x x) a) (a (a a a) (a c c))");;\r
 351 \r
 352 interactive "x y"\r
 353 "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat] ;;\r
 354 \r
 355 auto (problem_of "x (y. x y y)" "x (y. x y x)");;\r
 356 \r
 357 let rec conv_join = function\r
 358  | [] -> "@"\r
 359  | x::xs -> conv_join xs ^ " ("^ x ^")"\r
 360 ;;\r
 361 \r
 362 (* auto (problem_of "x a a a" (conv_join[\r
 363  "x b a a";\r
 364  "x a b a";\r
 365  "x a a b";\r
 366 ]));; *)\r
 367 \r
 368 auto (problem_of "x a a a a" (conv_join[\r
 369  "x b a a a";\r
 370  "x a b a a";\r
 371  "x a a b a";\r
 372  "x a a a b";\r
 373 ]));\r
 374 \r
 375 (* Controesempio ad usare un conto dei lambda che non considere le permutazioni *)\r
 376 auto (problem_of "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" (conv_join[\r
 377  "x a a a a (_. a) b b b";\r
 378  "x a a a a (_. _. _. _. x. y. x y)";\r
 379 ]));\r
 380 \r
 381 (* let _ = exec\r
 382  "x y"\r
 383  [ "x x"; "y z"; "y x" ]\r
 384  [ step 0 0 0; step 1 0 1; eat 5; ]\r
 385 ;;\r
 386 \r
 387 let _ = exec\r
 388  "a b c"\r
 389  [ "a b @"; "a @ c"; "a a a" ]\r
 390  [ step 0 0 0; step 1 1 0; eat 2; ]\r
 391 ;;\r
 392 \r
 393 let _ = exec\r
 394  "a (a b c) (a d e)"\r
 395  [ "a (a b @) (a @ e)"; "a a a" ]\r
 396  [ step 0 0 0; step 1 1 0; eat 2]\r
 397 ;; *)\r
 398 \r
 399 print_hline();\r
 400 print_endline "ALL DONE. "\r
 401 \r
 402 (* TEMPORARY TESTING FACILITY BELOW HERE *)\r
 403 \r
 404 let acaso l =\r
 405     let n = Random.int (List.length l) in\r
 406     List.nth l n\r
 407 ;;\r
 408 \r
 409 let acaso2 l1 l2 =\r
 410   let n1 = List.length l1 in\r
 411   let n = Random.int (n1 + List.length l2) in\r
 412   if n >= n1 then List.nth l2 (n - n1) else List.nth l1 n\r
 413 ;;\r
 414 \r
 415 let gen n vars =\r
 416   let rec aux n inerts lams =\r
 417     if n = 0 then List.hd inerts, List.hd (Util.sort_uniq (List.tl inerts))\r
 418     else let inerts, lams = if Random.int 2 = 0\r
 419       then inerts, ("(" ^ acaso vars ^ ". " ^ acaso2 inerts lams ^ ")") :: lams\r
 420       else ("(" ^ acaso inerts ^ " " ^ acaso2 inerts lams^ ")") :: inerts, lams\r
 421     in aux (n-1) inerts lams\r
 422   in aux (2*n) vars []\r
 423 ;;\r
 424 \r
 425 let f () =\r
 426   let complex = 200 in\r
 427   let vars = ["x"; "y"; "z"; "v" ; "w"; "a"; "b"; "c"] in\r
 428   gen complex vars\r
 429 \r
 430   let rec repeat f n =\r
 431     prerr_endline "\n########################### NEW TEST ###########################";\r
 432     f () ;\r
 433     if n > 0 then repeat f (n-1)\r
 434   ;;\r
 435 \r
 436 \r
 437 let main () =\r
 438  Random.self_init ();\r
 439  repeat (fun _ ->\r
 440    let div, conv = f () in\r
 441    auto (problem_of div conv)\r
 442  ) 100;\r
 443 ;;\r
 444 \r
 445 (* main ();; *)\r