ocaml/andrea6.ml

   1 let print_hline = Console.print_hline;;\r
   2 \r
   3 type var = int;;\r
   4 \r
   5 type t =\r
   6  | V of var\r
   7  | A of t * t\r
   8  | L of t\r
   9  | LM of\r
  10     t list (* body of the match *)\r
  11   * int (* explicit liftno *)\r
  12   * int (* variable which originated this match (id) *)\r
  13  | B (* bottom *)\r
  14  | P (* pacman *)\r
  15 ;;\r
  16 \r
  17 \r
  18 type problem = {\r
  19    orig_freshno: int\r
  20  ; freshno : int\r
  21  ; div : t list\r
  22  ; conv : t list\r
  23  ; matches : (var (* variable originating this match *) * (bool (* term comes from div*) * (t (* term to discriminate *) * t (* continuation *))) list) list\r
  24  ; sigma : (var * t) list (* substitutions *)\r
  25 }\r
  26 \r
  27 let string_of_t p =\r
  28  let bound_vars = ["x"; "y"; "z"; "z1"; "z2"] in\r
  29  let rec aux level = function\r
  30  | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)\r
  31  | A (t1,t2) -> "("^aux level t1^" "^aux level t2^")"\r
  32  | L t -> "(\\" ^ aux (level+1) (V 0) ^ ". " ^ aux (level+1) t ^ ")"\r
  33  | LM (ts,liftno,id) -> "[match orig="^aux 0 (V id)^"]"\r
  34  | B -> "BOT"\r
  35  | P -> "PAC"\r
  36  in aux 0\r
  37 ;;\r
  38 \r
  39 let string_of_t p =\r
  40   let bound_vars = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"] in\r
  41   let rec string_of_term_w_pars level = function\r
  42     | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)\r
  43     | A _ as t -> "(" ^ string_of_term_no_pars_app level t ^ ")"\r
  44     | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"\r
  45     | LM (ts,liftno,id) -> "[match orig="^ string_of_term_w_pars 0 (V id)^"]"\r
  46     | B -> "BOT"\r
  47     | P -> "PAC"\r
  48   and string_of_term_no_pars_app level = function\r
  49     | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)\r
  50     | _ as t -> string_of_term_w_pars level t\r
  51   and string_of_term_no_pars_lam level = function\r
  52     | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)\r
  53     | _ as t -> string_of_term_no_pars level t\r
  54   and string_of_term_no_pars level = function\r
  55     | L _ as t -> string_of_term_no_pars_lam level t\r
  56     | _ as t -> string_of_term_no_pars_app level t\r
  57   in string_of_term_no_pars 0\r
  58 ;;\r
  59 \r
  60 let string_of_problem p =\r
  61  let lines = [\r
  62   "[DV] " ^ String.concat "\n     " (List.map (string_of_t p) p.div);\r
  63   "[CV] " ^ String.concat "\n     " (List.map (string_of_t p) p.conv);\r
  64   (* "" ; *)\r
  65  ] @ Util.concat_map (fun (v, lst) -> ("[<>] of "^(string_of_t p (V v))) :: List.map (fun (b,(t,c)) -> "   " ^ (if b then "*" else " ") ^ " " ^ string_of_t p t\r
  66  (* ^" -> " ^ string_of_t p c *)\r
  67  ) lst) p.matches @ [""] in\r
  68  String.concat "\n" lines\r
  69 ;;\r
  70 \r
  71 let problem_fail p reason =\r
  72  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
  73  print_endline (string_of_problem p);\r
  74  failwith reason\r
  75 ;;\r
  76 \r
  77 let freshvar ({freshno} as p) =\r
  78  {p with freshno=freshno+1}, freshno+1\r
  79 ;;\r
  80 \r
  81 let add_to_match p id entry =\r
  82  let matches = try\r
  83    let _ = List.assoc id p.matches in\r
  84    List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst) ) p.matches\r
  85   with\r
  86   | Not_found -> (id,[entry]) :: p.matches in\r
  87  {p with matches}\r
  88 ;;\r
  89 \r
  90 let var_occurs_in v =\r
  91  let rec aux level = function\r
  92  | V v' -> v + level = v'\r
  93  | A(t1,t2) -> (aux level t1) || (aux level t2)\r
  94  | L t -> aux (level+1) t\r
  95  | LM(ts,_,_) -> List.fold_left (fun a b -> a || aux (level+1) b) false ts\r
  96  | B -> false\r
  97  | P -> false\r
  98  in aux 0\r
  99 ;;\r
 100 \r
 101 let rec is_inert =\r
 102  function\r
 103  | A(t,_) -> is_inert t\r
 104  | V _ -> true\r
 105  | L _ | LM _ | B | P -> false\r
 106 ;;\r
 107 \r
 108 let is_var = function V _ -> true | _ -> false;;\r
 109 let is_lambda = function L _ -> true | _ -> false;;\r
 110 let is_pacman = function P -> true | _ -> false;;\r
 111 \r
 112 let rec subst isdiv level delift sub p =\r
 113  function\r
 114  | V v -> p, if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
 115  | L t -> let p, t = subst isdiv (level + 1) delift sub p t in p, L t\r
 116  | A (t1,t2) ->\r
 117   let p, t1 = subst isdiv level delift sub p t1 in\r
 118   let p, t2 = subst isdiv level delift sub p t2 in\r
 119   if t1 = B || t2 = B then p, B else\r
 120   if level = 0 then mk_app isdiv p t1 t2 else p, A (t1, t2)\r
 121  | LM (ts, liftno, id) ->\r
 122    let p, ts =\r
 123     let rec aux p = function\r
 124     | [] -> p, []\r
 125     | t::ts ->\r
 126      let p, ts = aux p ts in\r
 127      let p, t = subst isdiv (level+1) delift sub p t in\r
 128      p, t::ts in\r
 129     aux p ts in\r
 130    p, LM(ts, liftno, id)\r
 131  | B -> p, B\r
 132  | P -> p, P\r
 133 and mk_app isdiv p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
 134  | L t1 ->\r
 135  (* FIXME BUG HERE! *)\r
 136   if is_inert t2 && (match t2 with V v -> v > p.orig_freshno | _ -> true ) && not (var_occurs_in 0 t1)\r
 137    then (if isdiv then {p with div=p.div @ [t2]} else {p with conv=p.conv @ [t2]}), lift (-1) t1\r
 138    else subst isdiv 0 true (0, t2) p t1\r
 139  | LM(ts,liftno,id) ->\r
 140   let p, t = mk_apps isdiv p t2 (List.map (lift ~-1) ts) in\r
 141   if t = B\r
 142    then p, B\r
 143    else\r
 144     let p, cont = freshvar p in\r
 145     let newvar = V cont in\r
 146     let p = add_to_match p id (isdiv,(t,newvar)) in\r
 147       p, newvar\r
 148  | B\r
 149  | _ when t2 = B -> p, B\r
 150  | t1 -> p, A (t1, t2)\r
 151 and mk_apps isdiv p t =\r
 152  function\r
 153  | [] -> p, t\r
 154  | t'::ts -> let p, t = mk_app isdiv p t t' in mk_apps isdiv p t ts\r
 155  and lift n =\r
 156   let rec aux n' =\r
 157    function\r
 158    | V m -> V (if m >= n' then m + n else m)\r
 159    | L t -> L (aux (n'+1) t)\r
 160    | A (t1, t2) -> A (aux n' t1, aux n' t2)\r
 161    | LM (ts, liftno, id) -> LM (List.map (aux (n'+1)) ts, n + liftno, id)\r
 162    | B -> B\r
 163    | P -> P\r
 164   in aux 0\r
 165  ;;\r
 166 \r
 167 let subst isdiv = subst isdiv 0 false;;\r
 168 \r
 169 let mk_lambda t = L (lift 1 t) ;;\r
 170 \r
 171 let subst_many b sub =\r
 172  let rec aux p = function\r
 173  | [] -> p, []\r
 174  | t::tms ->\r
 175   let p, t = subst b sub p t in\r
 176   let p, tms = aux p tms in\r
 177   p, t :: tms\r
 178  in aux\r
 179 ;;\r
 180 \r
 181 let rec subst_in_matches sub p =\r
 182  function\r
 183  | [] -> p, []\r
 184  | (v, branches) :: ms->\r
 185   let a, b = List.split branches in\r
 186   let b, c = List.split b in\r
 187   let p, b = subst_many false sub p b in\r
 188   let p, c = subst_many false sub p c in\r
 189   let b = List.combine b c in\r
 190   let branches = List.combine a b in\r
 191   let p, ms = subst_in_matches sub p ms in\r
 192   p, (v, branches) :: ms\r
 193 ;;\r
 194 \r
 195 let subst_in_problem (sub: var * t) (p: problem) =\r
 196 (* print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " " ^ string_of_t p (snd sub)); *)\r
 197  let div, conv = p.div, p.conv in\r
 198  let p = {p with div=[]; conv=[]} in\r
 199  let p, div' = subst_many true sub p div in\r
 200  let p, conv' = subst_many false sub p conv in\r
 201  let p, matches = subst_in_matches sub p p.matches in\r
 202  let p = {p with div=div'@p.div; conv=conv'@p.conv; matches} in\r
 203  (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
 204  {p with sigma=sub::p.sigma}\r
 205 ;;\r
 206 \r
 207 (* FIXME *)\r
 208 let unify_terms p t1 t2 =\r
 209  match t1 with\r
 210  | V v -> subst_in_problem (v, t2) p\r
 211  | _ -> problem_fail p "The collapse of a match came after too many steps :(";;\r
 212 \r
 213 let rec unify p =\r
 214  let rec give_duplicates =\r
 215   let rec aux' t = function\r
 216   | [] -> [], None\r
 217   | (b',(t',c'))::ts -> if t = t' (* FIXME! eta-eq here *)then ts, Some (b',c') else (\r
 218    let ts, res = aux' t ts in (b',(t',c'))::ts, res) in\r
 219   let rec aux = function\r
 220    | [] -> [], None\r
 221    | (b,(t,c))::rest -> (\r
 222     match aux' t rest with\r
 223     | rest, None -> aux rest\r
 224     | rest, Some (b',c') -> ((if not b' then false else b),(t,c))::rest, Some (c', c)\r
 225     ) in\r
 226   function\r
 227   | [] -> [], None\r
 228   | (orig,branches) :: ms ->\r
 229    match aux branches with\r
 230    | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res\r
 231    | branches', Some subst -> (orig,branches') :: ms, Some subst in\r
 232  let matches, vars_to_be_unified = give_duplicates p.matches in\r
 233  let p = {p with matches=matches} in\r
 234  match vars_to_be_unified with\r
 235   | None -> p\r
 236   | Some(t', t) ->\r
 237    (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *)\r
 238    unify (unify_terms p t' t)\r
 239 ;;\r
 240 \r
 241 let problem_done p =\r
 242   let all_separated = List.for_all (fun (_, lst) -> List.length lst = 1 || List.for_all (fun (_,(t,_)) -> is_var t) lst) p.matches in\r
 243   all_separated && List.exists ((=) B) p.div\r
 244 ;;\r
 245 \r
 246 let free_vars p t =\r
 247  let rec aux level = function\r
 248  | V v -> if v >= level then [v] else []\r
 249  | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
 250  | L t -> aux (level+1) t\r
 251  | LM(ts,_,id) -> (List.concat (List.map (aux level) ts)) @ (\r
 252   let lst = List.assoc id p.matches in\r
 253   List.concat (List.map (fun (_,(t1,t2)) -> (aux 0 t1) @ (aux 0 t2)) lst)\r
 254  )\r
 255  | B -> []\r
 256  | P -> []\r
 257  in Util.sort_uniq (aux 0 t)\r
 258 ;;\r
 259 \r
 260 let visible_vars p t =\r
 261  let rec aux = function\r
 262  | V v -> [v]\r
 263  | A(t1,t2) -> (aux t1) @ (aux t2)\r
 264  | L t -> []\r
 265  | LM(ts,_,id) -> (List.concat (List.map aux ts)) @ (\r
 266   let lst = List.assoc id p.matches in\r
 267   List.concat (List.map (fun (_,(t1,t2)) -> (aux t1) @ (aux t2)) lst)\r
 268  )\r
 269  | B -> []\r
 270  | P -> []\r
 271  in Util.sort_uniq (aux t)\r
 272 ;;\r
 273 \r
 274 let forget_variable var p =\r
 275  let p', div = subst_many true (var, P) p p.div in\r
 276  let p = {p' with conv=p.conv} in\r
 277  let p, conv = subst_many false (var, B) p p.conv in\r
 278  let p, matches = subst_in_matches (var, B) p p.matches in\r
 279  {p with div; conv; matches; sigma=p.sigma}\r
 280 ;;\r
 281 let rec remove_divergent_discriminators p =\r
 282  let f = fun (b,(t,_)) -> b && (t = B || is_lambda t) in\r
 283  try\r
 284   let v,l = List.find (fun (_,lst) -> List.exists f lst) p.matches in\r
 285   let (_,(_,c)) as entry = List.find f l in\r
 286   let l = List.filter ((<>) entry) l in\r
 287   let matches = List.map (fun (v', l') -> v', if v' = v then l else l') p.matches in\r
 288   let vars = free_vars p c in\r
 289   let p = {p with matches} in\r
 290   List.fold_right forget_variable vars p\r
 291  with Not_found -> p\r
 292 ;;\r
 293 \r
 294 exception Done;;\r
 295 \r
 296 let sanity p =\r
 297  (* try to fix divergent discriminators *)\r
 298  let p = remove_divergent_discriminators p in\r
 299  (* Remove lambdas from conv TODO remove duplicates *)\r
 300  let div = List.filter (function | P | L _ -> false | _ -> true) p.div in\r
 301  let conv = List.filter (function | B | V _ | A _ -> true | _ -> false) p.conv in\r
 302  let p = {p with div;conv} in\r
 303  (* Sanity checks: *)\r
 304  if p.div = [] then problem_fail p "p.div converged";\r
 305  if List.mem B p.conv then problem_fail p "p.conv diverged";\r
 306  if not (List.for_all (fun (_, lst) -> List.for_all (fun (b,(t,_)) -> is_inert t) lst) p.matches)\r
 307   then problem_fail p "Unsolvable discrimination";\r
 308 \r
 309  (* unify! :( *)\r
 310  let p = unify p in\r
 311  print_endline (string_of_problem p); (* non cancellare *)\r
 312  if problem_done p then raise Done else p\r
 313 ;;\r
 314 \r
 315 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
 316 \r
 317 let ignore var n p =\r
 318  print_cmd "EAT" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 319  let rec aux m t =\r
 320   if m = 0\r
 321    then lift n t\r
 322    else L (aux (m-1) t) in\r
 323  let p, fresh = freshvar p in\r
 324  let subst = var, aux n (V fresh) in\r
 325  sanity (subst_in_problem subst p)\r
 326 ;;\r
 327 \r
 328 let explode p =\r
 329  let fv1 = List.concat (List.map (visible_vars p) p.div) in\r
 330  let fv2 = List.concat (List.map (visible_vars p) p.conv) in\r
 331  let fv = List.filter (fun x -> not (List.mem x fv2)) fv1 in\r
 332  let fv = List.filter ((<) p.orig_freshno) fv in\r
 333  match fv with\r
 334  | var::_ ->\r
 335   print_cmd "EXPLODE" ("on " ^ string_of_t p (V var));\r
 336   let subst = var, B in\r
 337   sanity (subst_in_problem subst p)\r
 338  | _ -> problem_fail p "premature explosion"\r
 339 ;;\r
 340 \r
 341 let step var p =\r
 342  print_cmd "STEP" ("on " ^ string_of_t p (V var));\r
 343  let subst = var, LM([], 0, var) in\r
 344  sanity (subst_in_problem subst p)\r
 345 ;;\r
 346 \r
 347 let id var p =\r
 348  print_cmd "ID" ("on " ^ string_of_t p (V var));\r
 349  let subst = var, L(V 0) in\r
 350  sanity (subst_in_problem subst p)\r
 351 ;;\r
 352 \r
 353 let apply var appk p =\r
 354  print_cmd "APPLY"\r
 355   (string_of_t p (V var) ^ " applies no." ^ string_of_int appk ^ " fresh variables");\r
 356  let rec mk_freshvars n p =\r
 357   if n = 0\r
 358    then p, []\r
 359    else\r
 360     let p, vs = mk_freshvars (n-1) p in\r
 361     let p, v = freshvar p in\r
 362     p, V(v)::vs in\r
 363  let p, vars = mk_freshvars appk p in\r
 364  let p, t = mk_apps false p (V 0) (List.map (lift 1) vars) in\r
 365  let t = L (A (lift 1 (V var), t))  in\r
 366  let subst = var, t in\r
 367  sanity (subst_in_problem subst p)\r
 368 ;;\r
 369 \r
 370 let perm var n p =\r
 371  print_cmd "PERM" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
 372  let p, v = freshvar p in\r
 373  let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in\r
 374  let rec aux m t =\r
 375   if m = 0\r
 376    then aux' (n-1) t\r
 377    else L (aux (m-1) t) in\r
 378  let t = aux n (lift n (V v)) in\r
 379  let subst = var, t in\r
 380  sanity (subst_in_problem subst p)\r
 381 ;;\r
 382 \r
 383 (* TODO:\r
 384 - cosi' come e' possibile unificare rami di branch solo se vanno -> a variabili,\r
 385   allo stesso modo e' possibile ignorare dei rami se vanno in variabili, e quelle variabili\r
 386   vengono sostituite ovunque: con bombe in conv e con pacman in div\r
 387 *)\r
 388 let forget var no p =\r
 389  try\r
 390   let l = List.assoc var p.matches in\r
 391   let (b,(tm,c)) = List.nth l no in\r
 392   let l = List.mapi (fun n x -> if n = no then (b,(B,c)) else x) l in\r
 393   let matches = List.map (fun (v,lst) -> v, if v = var then l else lst) p.matches in\r
 394   let p = {p with matches} in\r
 395   print_cmd "FORGET" (string_of_t p tm ^ " from the match of " ^ string_of_t p (V var));\r
 396   sanity p\r
 397   (* (match c with\r
 398    | V var ->\r
 399    print_endline (\r
 400     "--- FORGET " ^ string_of_t p tm ^ " from the match of " ^ string_of_t p (V var));\r
 401    let p = forget_variable var p in\r
 402 \r
 403    | _ -> print_endline "too late to forget that term"; p\r
 404   ) *)\r
 405  with Failure "nth" ->\r
 406   print_endline "wtf?"; p\r
 407 ;;\r
 408 \r
 409 let parse strs =\r
 410  let dummy_p = {orig_freshno=0; freshno=0; div=[]; conv=[]; matches=[]; sigma=[]} in\r
 411   let rec aux level = function\r
 412   | Parser.Lam t -> L (aux (level + 1) t)\r
 413   | Parser.App (t1, t2) ->\r
 414    if level = 0 then snd (mk_app false dummy_p (aux level t1) (aux level t2))\r
 415     else A(aux level t1, aux level t2)\r
 416   | Parser.Var v -> V v\r
 417   in let (tms, free) = Parser.parse_many strs\r
 418   in (List.map (aux 0) tms, free)\r
 419 ;;\r
 420 \r
 421 let rec list_split n =\r
 422  function\r
 423  | [] -> [], []\r
 424  | x::xs as l -> if n = 0 then [], l else let a, b = list_split (n-1) xs in x::a, b\r
 425 ;;\r
 426 \r
 427 let magic6 div conv cmds =\r
 428  print_hline ();\r
 429  let all_tms, var_names = parse (div @ conv) in\r
 430  let div, conv = list_split (List.length div) all_tms in\r
 431  let varno = List.length var_names in\r
 432  let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in\r
 433  let p = try\r
 434   let subst = Util.index_of "BOMB" var_names, L B in\r
 435   let p = subst_in_problem subst p in p\r
 436   with Not_found -> p in\r
 437  let p = sanity p in\r
 438  try\r
 439   problem_fail (List.fold_left (|>) p cmds) "Problem not completed"\r
 440  with\r
 441  | Done -> ()\r
 442 ;;\r
 443 \r
 444 let interactive div conv cmds =\r
 445  print_hline ();\r
 446  let all_tms, var_names = parse (div @ conv) in\r
 447  let div, conv = list_split (List.length div) all_tms in\r
 448  let varno = List.length var_names in\r
 449  let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in\r
 450  (* activate bombs *)\r
 451  let p = try\r
 452   let subst = Util.index_of "BOMB" var_names, L B in\r
 453    subst_in_problem subst p\r
 454   with Not_found -> p in\r
 455  (* activate pacmans *)\r
 456  let p = try\r
 457   let subst = Util.index_of "PACMAN" var_names, P in\r
 458    let p = subst_in_problem subst p in\r
 459    (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
 460   with Not_found -> p in\r
 461  (* initial sanity check *)\r
 462  let p = sanity p in\r
 463  let p = List.fold_left (|>) p cmds in\r
 464  let rec f p cmds =\r
 465   let nth spl n = int_of_string (List.nth spl n) in\r
 466   let read_cmd () =\r
 467    let s = read_line () in\r
 468    let spl = Str.split (Str.regexp " +") s in\r
 469    s, let uno = List.hd spl in\r
 470     try if uno = "explode" then explode\r
 471     else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)\r
 472     else if uno = "step" then step (nth spl 1)\r
 473     else if uno = "perm" then perm (nth spl 1) (nth spl 2)\r
 474     else if uno = "apply" then apply (nth spl 1) (nth spl 2)\r
 475     else if uno = "forget" then forget (nth spl 1) (nth spl 2)\r
 476     else if uno = "id" then id (nth spl 1)\r
 477     else failwith "Wrong input."\r
 478     with Failure s -> print_endline s; (fun x -> x) in\r
 479   let str, cmd = read_cmd () in\r
 480   let cmds = (" " ^ str ^ ";")::cmds in\r
 481   try\r
 482    let p = cmd p in f p cmds\r
 483   with\r
 484   | Done -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)\r
 485  in f p []\r
 486 ;;\r
 487 \r
 488 let _ = magic6\r
 489  ["x x"]\r
 490  [ "_. BOMB" ]\r
 491  [ ignore 1 1; explode ]\r
 492 ;;\r
 493 \r
 494  let _ = magic6\r
 495   ["x y BOMB b"]\r
 496   [ "x BOMB y c" ]\r
 497   [ perm 1 3; step 8 ; explode; ];;\r
 498 \r
 499 let _ = magic6\r
 500  ["x BOMB a1 c"]\r
 501  [ "x y BOMB d"; "x BOMB a2 c" ]\r
 502  [ perm 1 3 ; step 10 ; step 13; explode; ]\r
 503 ;;\r
 504 \r
 505 let _ = magic6\r
 506  ["x (x x)"]\r
 507  [ "x x" ; "x x x" ] [\r
 508  apply 1 1;\r
 509  step 1;\r
 510  explode;\r
 511  step 9;\r
 512 ];;\r
 513 \r
 514 let _ = magic6\r
 515  ["x (_.BOMB)"]\r
 516  [ "x (_._. BOMB)" ]\r
 517  [ apply 1 2; ]\r
 518 ;;\r
 519 \r
 520 let _ = magic6\r
 521  ["x (_.y)"]\r
 522  [ "y (_. x)" ]\r
 523  [ apply 1 1; ignore 1 1;  explode; ]\r
 524 ;;\r
 525 \r
 526 let _ = magic6\r
 527  ["y (x a1 BOMB c) (x BOMB b1 d)"]\r
 528  [ "y (x a2 BOMB c) (x BOMB b1 d)";\r
 529  "y (x a1 BOMB c) (x BOMB b2 d)";] [\r
 530  perm 2 3;\r
 531  step 12;\r
 532  perm 17 2;\r
 533  step 19;\r
 534  step 18;\r
 535  ignore 22 1;\r
 536  ignore 21 1;\r
 537  ignore 24 1;\r
 538  ignore 25 1;\r
 539  step 1;\r
 540  step 32;\r
 541  explode;\r
 542  ]\r
 543 ;;\r
 544 \r
 545 let _ = magic6\r
 546  ["z (y x)"]\r
 547  [ "z (y (x.x))"; "y (_. BOMB)" ]\r
 548  [ apply 2 1; step 3; explode; ]\r
 549 ;;\r
 550 \r
 551 let _ = magic6\r
 552  ["y x"]\r
 553  [ "y (x.x)"; "x (_. BOMB)" ]\r
 554  [ apply 1 1; ignore 2 1; step 1; explode; ]\r
 555 ;;\r
 556 \r
 557 let _ = magic6\r
 558  ["z (y x)"]\r
 559  [ "z (y (x.x))"; "y (_. BOMB)" ]\r
 560  [ step 1; explode; apply 2 1; id 2; ignore 3 1; ]\r
 561 ;;\r
 562 \r
 563 let _ = magic6\r
 564  ["y (x a)"]\r
 565  [ "y (x b)"; "x BOMB" ] [\r
 566  id 2;\r
 567  step 1;\r
 568  explode;\r
 569 ];;\r
 570 \r
 571 magic6\r
 572  ["y (x a)"] [ "y (x b)"; "x BOMB"; "y a" ]\r
 573  [\r
 574  apply 1 1;\r
 575  perm 2 2;\r
 576  ignore 9 1;\r
 577  step 10;\r
 578  explode;\r
 579  ];;\r
 580 (* "y (a c)"\r
 581 [ "y (b c)"; "y (x a)"; "y (x b)"; "x BOMB" ]  *)\r
 582 \r
 583 magic6\r
 584 ["x a (x (a.y BOMB))"]\r
 585 [ "x b"; "x (y c)"; "x (y d)" ]\r
 586 [apply 1 1;\r
 587 apply 2 1;\r
 588 explode;]\r
 589 (* [\r
 590 step 1;\r
 591 step 3;\r
 592 explode' 10;\r
 593 (* ma si puo' fare anche senza forget *) *)\r
 594 (* ] *)\r
 595 ;;\r
 596 \r
 597 (* dipendente dalla codifica? no, ma si risolve solo con id *)\r
 598 magic6\r
 599  ["y a"] ["y b"; "x (y (_.BOMB))"]\r
 600 [\r
 601 apply 1 1;\r
 602 apply 2 1;\r
 603 explode;\r
 604 ];;\r
 605  (* [id 1; explode];; *)\r
 606 \r
 607 magic6\r
 608  ["PACMAN (x x x)"] ["PACMAN (x x)"]\r
 609  [\r
 610  ignore 2 2;\r
 611  explode;\r
 612  ];;\r
 613 \r
 614 print_hline();\r
 615 print_endline "ALL DONE. "\r