1 let (++) f g x = f (g x);;
\r
3 let print_hline = Console.print_hline;;
\r
12 (* | Stuck of var * int *)
\r
16 let rec consts = (* const_apps, const_lambda *)
\r
17 let rec aux1 = function
\r
18 | A(t, _) -> 1 + aux1 t
\r
20 let rec aux2 = function
\r
25 let a1, b1 = consts t1 in
\r
26 let a2, b2 = consts t2 in
\r
27 max (aux1 t) (max a1 a2), max b1 b2
\r
29 let a, b = consts t' in
\r
40 ; matches : (var (* variable originating this match *) * ((bool (* coming from div *) * t (* term to discriminate *) * var (* continuation *))) list) list
\r
41 ; sigma : (var * t) list (* substitutions *)
\r
42 ; stepped : var list
\r
43 ; arities : (var * int) list
\r
48 let dummy_p = {orig_freshno=0; freshno=0; div=B; conv=[]; matches=[]; sigma=[]; stepped=[]; arities=[]; k_app=0;k_lam=0};;
\r
50 let append_conv p t = let len = List.length p.conv in let p = {p with conv=t::p.conv} in p, len;;
\r
51 let get_conv p n = List.nth p.conv (List.length p.conv - 1 - n);;
\r
52 let index_of_conv t conv = List.length conv - 1 - (Util.index_of t conv);;
\r
55 let eq_conv_indices p i j = eq_conv (get_conv p i) (get_conv p j);;
\r
56 let all_terms p = (p.div :: p.conv) @ Util.concat_map (fun (_, lst) -> List.map (fun (_,x,_) -> x) lst) p.matches;;
\r
58 exception Done of (var * t) list (* substitution *);;
\r
59 exception Fail of int * string;;
\r
62 let bound_vars = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"; "x3"; "x4"; "x5"] in
\r
63 let rec string_of_term_w_pars level = function
\r
64 | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)
\r
66 | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"
\r
69 (* | Stuck _ as t -> "(" ^ string_of_term_no_pars_app level t ^ ")" *)
\r
70 (* | Ptr _ as t-> "(" ^ string_of_term_no_pars_app level t ^ ")" *)
\r
71 (* "&" ^ string_of_int n *)
\r
72 and string_of_term_no_pars_app level = function
\r
73 | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)
\r
74 (* | Stuck(v,n) -> ":" ^ string_of_term_no_pars_app level (V v) ^ " " ^ (string_of_term_w_pars level (get_conv p n)) *)
\r
75 (* | Ptr n -> string_of_term_no_pars_app level (get_conv p n) *)
\r
76 (* | Ptr n -> "&" ^ string_of_int n *)
\r
77 | _ as t -> string_of_term_w_pars level t
\r
78 and string_of_term_no_pars_lam level = function
\r
79 | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)
\r
80 | _ as t -> string_of_term_no_pars level t
\r
81 and string_of_term_no_pars level = function
\r
82 | L _ as t -> string_of_term_no_pars_lam level t
\r
83 | _ as t -> string_of_term_no_pars_app level t
\r
84 in string_of_term_no_pars 0
\r
87 let string_of_problem p =
\r
89 "[arities] " ^ String.concat " " (List.map (fun (v,n) -> "`" ^ string_of_int v ^ "=" ^ string_of_int n) p.arities);
\r
90 "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);
\r
91 "[DV] " ^ (string_of_t p p.div);
\r
92 "[CV] " ^ String.concat "\n " (List.map (string_of_t p) p.conv);
\r
94 ] @ 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
95 ^ " -> " ^ string_of_t p (V c)
\r
96 ) lst) p.matches @ [""] in
\r
97 String.concat "\n" lines
\r
100 let problem_fail p reason =
\r
101 print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";
\r
102 print_endline (string_of_problem p);
\r
103 raise (Fail (-1, reason))
\r
106 let freshvar ({freshno} as p) =
\r
107 {p with freshno=freshno+1}, freshno+1
\r
110 let add_to_match p id fromdiv t =
\r
111 let p, v = freshvar p in
\r
112 let arity = (List.assoc id p.arities) - 1 in
\r
113 let entry = fromdiv, t, v in
\r
115 List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry::lst)) p.matches
\r
117 let arities = (v,arity) :: p.arities in
\r
118 {p with matches; arities}, V v
\r
121 let var_occurs_in p v =
\r
122 let rec aux level = function
\r
123 | V v' -> v + level = v'
\r
124 (* | Stuck(v',n) -> assert (v <> v'); aux level (get_conv p n) *)
\r
125 | A(t1,t2) -> (aux level t1) || (aux level t2)
\r
126 | L t -> aux (level+1) t
\r
129 (* | Ptr n -> aux level (get_conv p n) *)
\r
134 let rec is_inert p =
\r
136 | A(t,_) -> is_inert p t
\r
137 (* | Ptr n -> is_inert p (get_conv p n) *)
\r
139 | L _ | B | P -> false
\r
142 let is_var = function V _ -> true | _ -> false;;
\r
143 let is_lambda = function L _ -> true | _ -> false;;
\r
144 let is_pacman = function P -> true | _ -> false;;
\r
146 let rec subst level delift fromdiv sub p =
\r
148 | 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
149 | L t -> let p, t = subst (level + 1) delift fromdiv sub p t in p, L t
\r
151 let p, t1 = subst level delift fromdiv sub p t1 in
\r
152 let p, t2 = subst level delift fromdiv sub p t2 in
\r
153 if t1 = B || t2 = B then p, B else
\r
154 if level = 0 then mk_app fromdiv p t1 t2 else p, A (t1, t2)
\r
157 and mk_app fromdiv p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with
\r
158 | B | _ when t2 = B -> p, B
\r
159 | L t1 -> subst 0 true fromdiv (0, t2) p t1
\r
160 | V v when List.mem v p.stepped ->
\r
161 let p, x = add_to_match p v fromdiv t2 in
\r
163 | t1 -> p, A (t1, t2)
\r
164 and mk_apps fromdiv p t =
\r
167 | t'::ts -> let p, t = mk_app fromdiv p t t' in mk_apps fromdiv p t ts
\r
171 | V m -> V (if m >= n' then m + n else m)
\r
172 | L t -> L (aux (n'+1) t)
\r
173 | A (t1, t2) -> A (aux n' t1, aux n' t2)
\r
179 let subst = subst 0 false;;
\r
181 let mk_lambda t = L (lift 1 t) ;;
\r
183 let subst_conv sub =
\r
184 let rec aux p = function
\r
187 let p, tms = aux p tms in
\r
188 let p, t = subst false sub p t in
\r
193 let subst_in_problem (sub: var * t) (p: problem) =
\r
194 print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));
\r
195 (* BUG QUI FIXME!!!! *)
\r
196 let rec mix l1 l2 = match l1, l2 with
\r
198 | x::xs, _::ys -> x:: (mix xs ys)
\r
199 | _ -> assert false in
\r
200 let p = {p with stepped=(fst sub)::p.stepped} in
\r
201 let p, conv = subst_conv sub p p.conv in
\r
202 let p, div = subst true sub p p.div in
\r
203 let conv = List.rev (mix (List.rev conv) (List.rev p.conv)) in
\r
204 let p = {p with div; conv} in
\r
205 (* print_endline ("after sub: \n" ^ string_of_problem p); *)
\r
206 {p with sigma=sub::p.sigma}
\r
210 let unify_terms p v1 v2 =
\r
211 if List.mem v1 p.stepped
\r
212 then problem_fail p "The collapse of a match came after too many steps :(";
\r
213 subst_in_problem (v1, V v2) p
\r
217 let rec give_duplicates =
\r
218 let rec aux' t = function
\r
220 | (b',t',c')::ts -> if t = t' (* FIXME! eta-eq here *) then ts, Some (b',c') else (
\r
221 let ts, res = aux' t ts in (b',t',c')::ts, res) in
\r
222 let rec aux = function
\r
224 | (b,t,c)::rest -> (
\r
225 match aux' t rest with
\r
226 | rest, None -> aux rest
\r
227 | rest, Some(b',c') -> (b || b', t, c) :: rest, Some(c', c)
\r
231 | (orig,branches) :: ms ->
\r
232 match aux branches with
\r
233 | _, None -> let ms, res = give_duplicates ms in (orig,branches) :: ms, res
\r
234 | branches', Some subst -> (orig,branches') :: ms, Some subst in
\r
235 let matches, vars_to_be_unified = give_duplicates p.matches in
\r
236 let p = {p with matches=matches} in
\r
237 match vars_to_be_unified with
\r
240 (* print_endline ("> unify " ^ string_of_t p (t') ^ " with " ^ string_of_t p t); *)
\r
241 unify (unify_terms p t' t)
\r
244 let problem_done p =
\r
245 let condition (b, t, cont) =
\r
247 (not (List.mem cont p.stepped)) ||
\r
249 let all_separated = List.for_all (fun (_, lst) -> List.for_all condition lst) p.matches in
\r
250 all_separated && p.div = B
\r
253 let free_vars p t =
\r
254 let rec aux level = function
\r
255 | V v -> if v >= level then [v] else []
\r
256 | A(t1,t2) -> (aux level t1) @ (aux level t2)
\r
257 | L t -> aux (level+1) t
\r
259 in Util.sort_uniq (aux 0 t)
\r
262 let visible_vars p t =
\r
263 let rec aux = function
\r
265 | A(t1,t2) -> (aux t1) @ (aux t2)
\r
268 (* | Ptr n -> aux (get_conv p n) *)
\r
269 in Util.sort_uniq (aux t)
\r
273 let rec simple_explode p =
\r
276 let subst = var, B in
\r
277 sanity (subst_in_problem subst p)
\r
281 (* Sanity checks: *)
\r
282 if (function | P | L _ -> true | _ -> false) p.div then problem_fail p "p.div converged";
\r
283 if List.mem B p.conv then problem_fail p "p.conv diverged";
\r
284 let solvable (b,t,c) = (b && not (List.mem c p.stepped)) || is_inert p t in
\r
285 if not (List.for_all (fun (_, lst) -> List.for_all solvable lst) p.matches)
\r
286 then problem_fail p "Unsolvable discrimination";
\r
289 print_endline (string_of_problem p); (* non cancellare *)
\r
290 let p = if problem_done p then raise (Done p.sigma) else p in
\r
291 let p = if is_var p.div then simple_explode p else p in
\r
295 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
\r
297 let rec hd_args t = match t with
\r
299 | A(t1,t2) -> let a, b = hd_args t1 in a, b @ [t2]
\r
303 let max_arity_of_var v =
\r
304 let rec aux level =
\r
307 | A _ as t -> print_string (string_of_t dummy_p t); let hd, args = hd_args t in
\r
308 let acc = if hd = level + v then List.length args else 0 in
\r
309 List.fold_right (max ++ (aux level)) args acc
\r
310 | L t -> aux (level + 1) t
\r
315 let ignore var n p =
\r
316 print_cmd "EAT" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
\r
320 else L (aux (m-1) t) in
\r
321 let p, fresh = freshvar p in
\r
322 let subst = var, aux n (V fresh) in
\r
323 sanity (subst_in_problem subst p)
\r
329 print_cmd "EAT" ("var " ^ string_of_t p (V var));
\r
330 let rec is_hd v' = function
\r
331 | A (t,_) -> is_hd v' t
\r
334 let rec app_length = function
\r
335 | A (t,_) -> 1 + app_length t
\r
337 let rec find_app_no = function
\r
338 | V _ | L _ | P | B -> 0
\r
339 | A (t1,t2) as t ->
\r
340 max (max (find_app_no t1) (find_app_no t2))
\r
341 (if is_hd var t1 then app_length t else 0)
\r
342 in let n = List.fold_right (max ++ find_app_no) (all_terms p) 0 in
\r
346 else L (aux (m-1) t) in
\r
347 let p, fresh = freshvar p in
\r
348 let subst = var, aux n (V fresh) in
\r
349 sanity (subst_in_problem subst p)
\r
353 let fv1 = visible_vars p p.div in
\r
354 let fv2 = List.concat (List.map (visible_vars p) p.conv) in
\r
355 let fv = List.filter (fun x -> not (List.mem x fv2)) fv1 in
\r
356 let fv = List.filter ((<) p.orig_freshno) fv in
\r
359 print_cmd "EXPLODE" ("on " ^ string_of_t p (V var));
\r
360 let subst = var, B in
\r
361 sanity (subst_in_problem subst p)
\r
362 | _ -> raise (Fail (-1,"premature explosion"))
\r
366 print_cmd "STEP" ("on " ^ string_of_t p (V var));
367 let matches = (var,[])::p.matches in
368 let p = {p with matches;stepped=var::p.stepped} in
369 let subst = var, V var in
370 sanity (subst_in_problem subst p)
\r
374 print_cmd "CHOOSE" ("#" ^ string_of_int n);
\r
375 let rec aux n t = match t with
\r
377 | A(t1,_) -> let n', t' = aux n t1 in if n = n' then n', t' else n'+1, t
\r
378 | _ -> assert false
\r
379 in let n', div = aux n p.div in
\r
380 if n' <> n then problem_fail p "wrong choose";
\r
381 let p = {p with div} in
\r
385 let apply var appk p =
\r
387 (string_of_t p (V var) ^ " applies no." ^ string_of_int appk ^ " fresh variables");
\r
388 let rec mk_freshvars n p =
\r
392 let p, vs = mk_freshvars (n-1) p in
\r
393 let p, v = freshvar p in
\r
395 let p, vars = mk_freshvars appk p in
\r
396 let p, t = mk_apps false p (V 0) (List.map (lift 1) vars) in
\r
397 let t = L (A (lift 1 (V var), t)) in
\r
398 let subst = var, t in
\r
399 sanity (subst_in_problem subst p)
\r
402 let find_arities_after_app p =
\r
403 let rec aux level n = function
\r
404 | L t -> assert (n > 0); max_arity_of_var level t :: aux (level+1) (n-1) t
\r
405 | _ -> Array.to_list (Array.make n 0)
\r
408 let find_all_first_args_of v =
\r
409 let rec aux level = function
\r
410 | L t -> aux (level+1) t
\r
412 | A(V v', t2) -> (if v + level = v' then [t2] else []) @ aux level t2
\r
413 | A(t1,t2) -> aux level t1 @ aux level t2
\r
419 let appk = p.k_lam + p.k_app + 1 in
\r
420 print_cmd "STEP'" ("on " ^ string_of_t p (V var) ^ " and applies no." ^ string_of_int appk ^ " fresh variables");
\r
421 let p, vars = (* +1 below because of lifting *)
\r
422 Array.fold_left (fun (p,vars) _ -> let p, v = freshvar p in p, (v+1)::vars)
\r
423 (p, []) (Array.make appk ()) in
\r
424 let p, t = mk_apps false p (V 0) (List.map (fun x -> V x) vars) in
\r
426 let first_args = Util.sort_uniq (List.fold_right ((@) ++ (find_all_first_args_of var)) (all_terms p) []) in
\r
427 let map = List.fold_left (fun acc t -> let acc' = find_arities_after_app p appk t in List.map (fun (x,y) -> max x y) (List.combine acc acc')) (Array.to_list (Array.make appk 0)) first_args in
\r
428 let arities = List.combine (List.map ((+) (-1)) vars) map in
\r
430 (* let p, var' = freshvar p in *)
\r
431 let p, var' = p, var in
\r
432 let matches = (var', []) :: p.matches in
\r
433 let p = {p with matches; arities=arities@p.arities} in
\r
434 let t = L (A (lift 1 (V var'), t)) in
\r
435 let subst = var, t in
\r
436 sanity (subst_in_problem subst p)
\r
440 if n = 1 then p else (
\r
441 print_cmd "PERM" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
\r
442 (* let p, v = freshvar p in *)
\r
443 let p, v = p, var in
\r
444 let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in
\r
448 else L (aux (m-1) t) in
\r
449 let t = aux n (lift n (V v)) in
\r
450 let subst = var, t in
\r
451 (* let p = {p with arities=(v, List.assoc var p.arities)::p.arities} in *)
\r
452 sanity (subst_in_problem subst p)
\r
455 let free_vars_of_p p =
\r
456 Util.sort_uniq (Util.concat_map (free_vars p) (all_terms p));;
\r
458 let rec applied_vars p = function
\r
460 | L _ -> [] (* ??? *)
\r
462 | A(V v,t2) -> v :: applied_vars p t2
\r
463 | A(t1,t2) -> applied_vars p t1 @ applied_vars p t2
\r
466 let applied_vars_of_p p =
\r
467 Util.sort_uniq (Util.concat_map (applied_vars p) (all_terms p));;
\r
474 (* | Done _ as d -> raise d *)
\r
475 | Fail(_, s) -> print_endline ("<<< Backtracking because: " ^ s) in
\r
476 print_endline ">>> auto called";
\r
477 (* Compute useful free variables *)
\r
478 let fv = applied_vars_of_p p in
\r
479 let fv = List.filter (fun v -> not (List.mem v p.stepped)) fv in
\r
480 List.iter (fun v -> print_string ("@`" ^ string_of_int v)) fv;
\r
481 let fv0 = List.filter (fun v -> List.assoc v p.arities > 0) fv in (* remove variable with arity left 0, cannot step there *)
\r
482 if fv0 = [] then (print_endline "warning! empty step fv0"; List.iter (fun v -> print_string ("@`" ^ string_of_int v)) fv);
\r
483 let permute_and_step p v =
\r
484 let step'' problem prm var =
\r
485 let problem = perm var prm problem in
\r
486 (* let _ = read_line () in *)
\r
487 let problem = step' var problem in
\r
489 let arity = List.assoc v p.arities in
\r
490 let _, perms = Array.fold_left (fun (arity, acc) () -> let a = arity + 1 in a, a::acc) (1,[1]) (Array.make (arity-1) ()) in
\r
491 List.iter (fun perm -> aux (step'' p perm) v) perms
\r
493 List.iter (permute_and_step p) fv0;
\r
494 List.iter (aux (fun v -> eat v p)) fv;
\r
495 (* mancano: applicazioni e choose; ??? *)
\r
499 let rec aux level = function
\r
500 | Parser.Lam t -> L (aux (level + 1) t)
\r
501 | Parser.App (t1, t2) ->
\r
502 if level = 0 then snd (mk_app false dummy_p (aux level t1) (aux level t2))
\r
503 else A(aux level t1, aux level t2)
\r
504 | Parser.Var v -> V v
\r
505 in let (tms, free) = Parser.parse_many strs
\r
506 in (List.map (aux 0) tms, free)
\r
509 let magic6 div conv cmds =
\r
511 let all_tms, var_names = parse (div :: conv) in
\r
512 let div, conv = List.hd all_tms, List.tl all_tms in
\r
513 let varno = List.length var_names in
\r
514 let k_app, k_lam = List.fold_left (fun (a, b) t -> let a', b' = consts t in max a a', max b b') (0,0) all_tms in
\r
515 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]; stepped=[];k_app;k_lam;arities=[]} in
\r
516 let fv = Util.sort_uniq (Util.concat_map (free_vars p) all_tms) in
\r
517 let arities = List.map (fun var -> var, k_app) fv in
\r
518 let p = {p with arities} in
\r
520 let subst = Util.index_of "BOMB" var_names, L B in
\r
521 let p = subst_in_problem subst p in p
\r
522 with Not_found -> p in
\r
523 let p = sanity p in
\r
525 problem_fail (List.fold_left (|>) p cmds) "Problem not completed"
\r
530 let auto div conv =
\r
532 let all_tms, var_names = parse (div :: conv) in
\r
533 let div, conv = List.hd all_tms, List.tl all_tms in
\r
534 let varno = List.length var_names in
\r
535 let k_app, k_lam = List.fold_left (fun (a, b) t -> let a', b' = consts t in max a a', max b b') (0,0) all_tms in
\r
536 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]; stepped=[];k_app;k_lam;arities=[]} in
\r
537 let fv = Util.sort_uniq (Util.concat_map (free_vars p) all_tms) in
\r
538 let max_arity_of_var_in_p var p =
\r
539 1 + List.fold_right (max ++ (max_arity_of_var var)) (all_terms p) 0 in
\r
540 let arities = List.map (fun var -> var, max_arity_of_var_in_p var p) fv in
\r
541 let p = {p with arities} in
\r
543 let subst = Util.index_of "BOMB" var_names, L B in
\r
544 let p = subst_in_problem subst p in p
\r
545 with Not_found -> p in
\r
546 let p = sanity p in
\r
549 failwith "auto failed."
\r
551 | Done _ -> print_endline "<<< auto ok >>>"; (* TODO: print and verify substitution *)
\r
554 (* let interactive div conv cmds =
\r
556 let all_tms, var_names = parse (div @ conv) in
\r
557 let div, conv = list_split (List.length div) all_tms in
\r
558 let varno = List.length var_names in
\r
559 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in
\r
560 (* activate bombs *)
\r
562 let subst = Util.index_of "BOMB" var_names, L B in
\r
563 subst_in_problem subst p
\r
564 with Not_found -> p in
\r
565 (* activate pacmans *)
\r
567 let subst = Util.index_of "PACMAN" var_names, P in
\r
568 let p = subst_in_problem subst p in
\r
569 (print_endline ("after subst in problem " ^ string_of_problem p); p)
\r
570 with Not_found -> p in
\r
571 (* initial sanity check *)
\r
572 let p = sanity p in
\r
573 let p = List.fold_left (|>) p cmds in
\r
575 let nth spl n = int_of_string (List.nth spl n) in
\r
577 let s = read_line () in
\r
578 let spl = Str.split (Str.regexp " +") s in
\r
579 s, let uno = List.hd spl in
\r
580 try if uno = "explode" then explode
\r
581 else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)
\r
582 else if uno = "step" then step (nth spl 1)
\r
583 else if uno = "perm" then perm (nth spl 1) (nth spl 2)
\r
584 else if uno = "apply" then apply (nth spl 1) (nth spl 2)
\r
585 (* else if uno = "forget" then forget (nth spl 1) (nth spl 2) *)
\r
586 else if uno = "id" then id (nth spl 1)
\r
587 else failwith "Wrong input."
\r
588 with Failure s -> print_endline s; (fun x -> x) in
\r
589 let str, cmd = read_cmd () in
\r
590 let cmds = (" " ^ str ^ ";")::cmds in
\r
592 let p = cmd p in f p cmds
\r
594 | Done -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)
\r
608 (* [ perm 1 3; step' 8 ; eat 4; eat 5; eat 15; ] *)
\r
614 [ "x y BOMB d"; "x BOMB a2 c" ]
\r
615 (* [ perm 1 3 ; step' 10 ; eat 4; eat 6; step' 17; eat 3; eat 7; eat 27; ] *)
\r
621 [ "x x" ; "x x x" ]
\r
624 eat 6; eat 9; eat 13;
\r
631 [ "x (_._. BOMB)" ]
\r
632 (* [ apply 1 2; ] *)
\r
639 (* [ apply 1 1; ignore 1 1; explode; ] *)
\r
644 "y (x a1 BOMB c) (x BOMB b1 d)"
\r
645 [ "y (x a2 BOMB c) (x BOMB b1 d)";
\r
646 "y (x a1 BOMB c) (x BOMB b2 d)";]
\r
663 "PACMAN (x x x)" ["PACMAN (x x)"];;
\r
668 [ "z (y (x.x))"; "y (_. BOMB)" ]
\r
669 [ apply 2 1; step 3; explode; ]
\r
674 [ "y (x.x)"; "x (_. BOMB)" ]
\r
675 [ apply 1 1; ignore 2 1; step 1; explode; ]
\r
680 [ "z (y (x.x))"; "y (_. BOMB)" ]
\r
681 [ step 1; explode; apply 2 1; id 2; ignore 3 1; ]
\r
686 [ "y (x b)"; "x BOMB" ] [
\r
693 ["y (x a)"] [ "y (x b)"; "x BOMB"; "y a" ]
\r
702 [ "y (b c)"; "y (x a)"; "y (x b)"; "x BOMB" ] *)
\r
705 ["x a (x (a.y BOMB))"]
\r
706 [ "x b"; "x (y c)"; "x (y d)" ]
\r
714 (* ma si puo' fare anche senza forget *) *)
\r
718 (* dipendente dalla codifica? no, ma si risolve solo con id *)
\r
720 ["y a"] ["y b"; "x (y (_.BOMB))"]
\r
726 (* [id 1; explode];; *)
\r
729 ["PACMAN (x x x)"] ["PACMAN (x x)"]
\r
736 print_endline "ALL DONE. "
\r