let (++) f g x = f (g x);;

let print_hline = Console.print_hline;;

type var = int;;
type t =
 | V of var
 | A of t * t
 | L of t
 | B (* bottom *)
 | P (* pacman *)
 | Stuck of var * int
 (* | Ptr of int *)
;;

let rec consts = (* const_apps, const_lambda *)
 let rec aux1 = function
 | A(t, _) -> 1 + aux1 t
 | _ -> 0 in
 let rec aux2 = function
 | L t -> 1 + aux2 t
 | _ -> 0 in
 function
 | A(t1, t2) as t ->
    let a1, b1 = consts t1 in
    let a2, b2 = consts t2 in
    max (aux1 t) (max a1 a2), max b1 b2
 | L t' as t ->
    let a, b = consts t' in
    a, max (aux2 t) b
 | _ -> 0, 0
;;


type problem = {
   orig_freshno: int
 ; freshno : int
 ; div : t
 ; conv : t list
 ; matches : (var (* variable originating this match *) * ((int (* index of the term to discriminate *) * var option (* continuation *))) list) list
 ; sigma : (var * t) list (* substitutions *)
 ; stepped : var list
 ; arities : (var * int) list
 ; k_app : int
 ; k_lam : int
}

let dummy_p = {orig_freshno=0; freshno=0; div=B; conv=[]; matches=[]; sigma=[]; stepped=[]; arities=[]; k_app=0;k_lam=0};;

let append_conv p t = let len = List.length p.conv in let p = {p with conv=t::p.conv} in p, len;;
let get_conv p n = List.nth p.conv (List.length p.conv - 1 - n);;
let index_of_conv t conv = List.length conv - 1 - (Util.index_of t conv);;

let eq_conv = (=);;
let eq_conv_indices p i j = eq_conv (get_conv p i) (get_conv p j);;
let all_terms p = p.div :: p.conv;;

exception Done of (var * t) list (* substitution *);;
exception Fail of int * string;;

let string_of_t p =
  let bound_vars = ["x"; "y"; "z"; "w"; "q"; "x1"; "x2"; "x3"; "x4"; "x5"] in
  let rec string_of_term_w_pars level = function
    | V v -> if v >= level then "`" ^ string_of_int (v-level) else List.nth bound_vars (level - v-1)
    | A _
    | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"
    | B -> "BOT"
    | P -> "PAC"
    | Stuck _ as t -> "(" ^ string_of_term_no_pars_app level t ^ ")"
    (* | Ptr _ as t-> "(" ^ string_of_term_no_pars_app level t ^ ")" *)
    (* "&" ^ string_of_int n *)
  and string_of_term_no_pars_app level = function
    | A(t1,t2) -> (string_of_term_no_pars_app level t1) ^ " " ^ (string_of_term_w_pars level t2)
    | Stuck(v,n) -> ":" ^ string_of_term_no_pars_app level (V v) ^ " " ^ (string_of_term_w_pars level (get_conv p n))
    (* | Ptr n -> string_of_term_no_pars_app level (get_conv p n) *)
    (* | Ptr n -> "&" ^ string_of_int n *)
    | _ as t -> string_of_term_w_pars level t
  and string_of_term_no_pars_lam level = function
    | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)
    | _ as t -> string_of_term_no_pars level t
  and string_of_term_no_pars level = function
    | L _ as t -> string_of_term_no_pars_lam level t
    | _ as t -> string_of_term_no_pars_app level t
  in string_of_term_no_pars 0
;;

let string_of_problem p =
 let lines = [
  "[arities] " ^ String.concat " " (List.map (fun (v,n) -> "`" ^ string_of_int v ^ "=" ^ string_of_int n) p.arities);
  "[stepped]" ^ String.concat " " (List.map string_of_int p.stepped);
  "[DV] " ^ (string_of_t p p.div);
  "[CV] " ^ String.concat "\n     " (List.map (string_of_t p) p.conv);
  (* "" ; *)
 ] @ Util.concat_map (fun (v, lst) -> ("[<>] of "^(string_of_t p (V v))) :: List.map (fun (n,c) -> "   " ^ string_of_t p (get_conv p n)
 ^ (match c with None -> "" | Some v -> " -> " ^ string_of_t p (V v))
 ) lst) p.matches @ [""] in
 String.concat "\n" lines
;;

let problem_fail p reason =
 print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";
 print_endline (string_of_problem p);
 raise (Fail (-1, reason))
;;

let freshvar ({freshno} as p) =
 {p with freshno=freshno+1}, freshno+1
;;

let add_to_match p id t =
 let p, entry =
  try
   p, index_of_conv t p.conv
  with
  | Not_found -> append_conv p t in
 let entry' = entry, None in
 let matches =
  List.map (fun (id',lst as x) -> if id <> id' then x else (id, entry'::lst)) p.matches
  in
 {p with matches}, entry
;;

let var_occurs_in p v =
 let rec aux level = function
 | V v' -> v + level = v'
 | Stuck(v',n) -> assert (v <> v'); aux level (get_conv p n)
 | A(t1,t2) -> (aux level t1) || (aux level t2)
 | L t -> aux (level+1) t
 | B -> false
 | P -> false
 (* | Ptr n -> aux level (get_conv p n) *)

 in aux 0
;;

let rec is_inert p =
 function
 | A(t,_) -> is_inert p t
 (* | Ptr n -> is_inert p (get_conv p n) *)
 | V _ | Stuck _ -> true
 | L _ | B | P -> false
;;

let is_var = function V _ -> true | _ -> false;;
let is_lambda = function L _ -> true | _ -> false;;
let is_pacman = function P -> true | _ -> false;;

let rec subst level delift sub p =
 function
 | V v -> p, if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)
 | L t -> let p, t = subst (level + 1) delift sub p t in p, L t
 | A (t1,t2) ->
  let p, t1 = subst level delift sub p t1 in
  let p, t2 = subst level delift sub p t2 in
  if t1 = B || t2 = B then p, B else
  if level = 0 then mk_app p t1 t2 else p, A (t1, t2)
 | B -> p, B
 | P -> p, P
 (* | Ptr _ as t -> p, t *)
 | Stuck(v,_) as t ->
    assert (v <> level + fst sub); (* can't instantiate v twice after a step *)
    (* FIXME!!!! URGENT!!! *)
    p, t
and mk_app p t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with
 | L t1 -> subst 0 true (0, t2) p t1
 | V v when List.mem v p.stepped ->
    let p, n = add_to_match p v t2 in
    p, Stuck(v, n)
 | B | _ when t2 = B -> p, B
 | t1 -> p, A (t1, t2)
and mk_apps p t =
 function
 | [] -> p, t
 | t'::ts -> let p, t = mk_app p t t' in mk_apps p t ts
and lift n =
 let rec aux n' =
  function
  | V m -> V (if m >= n' then m + n else m)
  | L t -> L (aux (n'+1) t)
  | A (t1, t2) -> A (aux n' t1, aux n' t2)
  | B -> B
  | P -> P
  | Stuck(m,ptr) -> assert (m >= n'); Stuck(m + n, ptr)
  (* | Ptr _ as t -> t *)
 in aux 0
;;

let subst = subst 0 false;;

let mk_lambda t = L (lift 1 t) ;;

let subst_many sub =
 let rec aux p = function
 | [] -> p, []
 | t::tms ->
  let p, tms = aux p tms in
  let p, t = subst sub p t in
  p, t :: tms
 in aux
;;

let subst_in_problem (sub: var * t) (p: problem) =
(* print_endline ("SUBST IN PROBLEM: " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub)); *)
(* BUG QUI FIXME!!!! *)
 let rec mix l1 l2 = match l1, l2 with
 | [], l2 -> l2
 | x::xs, _::ys -> x:: (mix xs ys)
 | _ -> assert false in
 let p, conv = subst_many sub p p.conv in
 let p, div = subst sub p p.div in
 let conv = List.rev (mix (List.rev conv) (List.rev p.conv)) in
 let p = {p with div; conv} in
 (* print_endline ("after sub: \n" ^ string_of_problem p); *)
 {p with sigma=sub::p.sigma}
;;

let problem_done p =
  let all_separated = List.for_all (fun (_, lst) -> List.for_all (fun (n,_) -> is_var (get_conv p n)) lst) p.matches in
  all_separated && p.div = B
;;

let free_vars p t =
 let rec aux level = function
 | V v -> if v >= level then [v] else []
 | A(t1,t2) -> (aux level t1) @ (aux level t2)
 | L t -> aux (level+1) t
 | B | P
 | Stuck _ -> []
 (* | Ptr n -> aux 0 (get_conv p n) *)
 in Util.sort_uniq (aux 0 t)
;;

let visible_vars p t =
 let rec aux = function
 | V v -> [v]
 | A(t1,t2) -> (aux t1) @ (aux t2)
 | B | P
 | Stuck _ | L _ -> []
 (* | Ptr n -> aux (get_conv p n) *)
 in Util.sort_uniq (aux t)
;;

(* TODO FIXME *)
let apply_substs p t = t;;

let unblock var index cont p =
 let rec aux p = function
 | Stuck(v',n') as t -> p, (if var = v' && index = n' then apply_substs p (V cont) else t)
 | A (t1, t2) ->
    let p, t1 = aux p t1 in
    let p, t2 = aux p t2 in
    mk_app p t1 t2
 | _ as t -> p, t in
 let p, div = aux p p.div in
 let _, conv = List.fold_right (fun c (p, conv) -> let p, c = aux p c in p, c::conv) p.conv (p,[]) in
 {p with div; conv}
;;

let rec unblock_all p =
 let aux (orig, m) (matches, news, p) =
  let nn = List.filter (fun (n,c) -> is_var (get_conv p n) && c = None) m in
  let p, conts = List.fold_left (fun (p,conts) (n,_) ->
    match Util.find_opt (function (n', c) when eq_conv_indices p n' n -> c | _ -> None) m
    with Some c -> p, (n, c)::conts | None ->
     (* c is the new continuation *)
     let p, c = freshvar p in
     let arity = c, List.assoc orig p.arities - 1 in
     print_endline ("``" ^ string_of_int orig);
     assert ((snd arity) > -1 );
     let p = {p with arities=arity::p.arities} in
     p, (n, c)::conts
   ) (p, []) nn in
  let m = List.map (fun (n,c) -> n, try
   Some (List.assoc n conts)
  with
  | Not_found -> c) m in
  (orig, m) :: matches, (List.map (fun x -> orig, x) conts) @ news, p
 in
 let matches, news, p = List.fold_right aux p.matches ([],[], p) in
 (* FIXPOINT *)
 if news <> [] then
 let f = List.fold_left (fun f (a,(b,c)) -> f ++ (unblock a b c)) (fun p -> p) news in
 unblock_all (f {p with matches}) else p
;;

let rec simple_explode p =
 match p.div with
 | V var ->
  let subst = var, B in
  sanity (subst_in_problem subst p)
 | _ -> p

and sanity p =
 (* Sanity checks: *)
 if (function | P | L _ -> true | _ -> false) p.div then problem_fail p "p.div converged";
 if List.mem B p.conv then problem_fail p "p.conv diverged";
 if not (List.for_all (fun (_, lst) -> List.for_all (fun (n,_) -> is_inert p (get_conv p n)) lst) p.matches)
  then problem_fail p "Unsolvable discrimination";

 let p = unblock_all p in
 print_endline (string_of_problem p); (* non cancellare *)
 let p = if problem_done p then raise (Done p.sigma) else p in
 let p = if is_var p.div then simple_explode p else p in
 p
;;

let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;

let rec hd_args t = match t with
 | V v -> v, []
 | A(t1,t2) -> let a, b = hd_args t1 in a, b @ [t2]
 | _ -> -666, []
;;

let max_arity_of_var v =
 let rec aux level =
 function
 | V _ -> 0
 | A _ as t -> print_string (string_of_t dummy_p t); let hd, args = hd_args t in
    let acc = if hd = level + v then List.length args else 0 in
    List.fold_right (max ++ (aux level)) args acc
 | L t -> aux (level + 1) t
 | Stuck(v,n) -> 0
 (* | Ptr n -> assert false *)
 | P | B -> 0
 in aux 0
;;

let ignore var n p =
 print_cmd "EAT" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
 let rec aux m t =
  if m = 0
   then lift n t
   else L (aux (m-1) t) in
 let p, fresh = freshvar p in
 let subst = var, aux n (V fresh) in
 sanity (subst_in_problem subst p)
;;



let eat var p =
 print_cmd "EAT" ("var " ^ string_of_t p (V var));
 let rec is_hd v' = function
 | A (t,_) -> is_hd v' t
 | V v -> v' = v
 | _ -> false in
 let rec app_length = function
 | A (t,_) -> 1 + app_length t
 | _ -> 0 in
 let rec find_app_no = function
 | V _ | L _ | P | B -> 0
 | A (t1,t2) as t ->
    max (max (find_app_no t1) (find_app_no t2))
     (if is_hd var t1 then app_length t else 0)
 | Stuck _ -> 0
 (* | Ptr n -> find_app_no (get_conv p n) *)
 in let n = List.fold_right (max ++ find_app_no) (all_terms p) 0 in
 let rec aux m t =
  if m = 0
   then lift n t
   else L (aux (m-1) t) in
 let p, fresh = freshvar p in
 let subst = var, aux n (V fresh) in
 sanity (subst_in_problem subst p)
;;

(* let explode p =
 let fv1 = visible_vars p p.div in
 let fv2 = List.concat (List.map (visible_vars p) p.conv) in
 let fv = List.filter (fun x -> not (List.mem x fv2)) fv1 in
 let fv = List.filter ((<) p.orig_freshno) fv in
 match fv with
 | var::_ ->
  print_cmd "EXPLODE" ("on " ^ string_of_t p (V var));
  let subst = var, B in
  sanity (subst_in_problem subst p)
 | _ -> raise (Fail (-1,"premature explosion"))
;; *)

(* let step var p =
 print_cmd "STEP" ("on " ^ string_of_t p (V var));
 let matches = (var,[])::p.matches in
 let p = {p with matches;stepped=var::p.stepped} in
 let subst = var, V var in
 sanity (subst_in_problem subst p)
;; *)

let choose n p =
 print_cmd "CHOOSE" ("#" ^ string_of_int n);
 let rec aux n t = match t with
 | V _ -> 0, t
 | A(t1,_) -> let n', t' = aux n t1 in if n = n' then n', t' else n'+1, t
 | _ -> assert false
 in let n', div = aux n p.div in
 if n' <> n then problem_fail p "wrong choose";
 let p = {p with div} in
 sanity p
;;

let apply var appk p =
 print_cmd "APPLY"
  (string_of_t p (V var) ^ " applies no." ^ string_of_int appk ^ " fresh variables");
 let rec mk_freshvars n p =
  if n = 0
   then p, []
   else
    let p, vs = mk_freshvars (n-1) p in
    let p, v = freshvar p in
    p, V(v)::vs in
 let p, vars = mk_freshvars appk p in
 let p, t = mk_apps p (V 0) (List.map (lift 1) vars) in
 let t = L (A (lift 1 (V var), t))  in
 let subst = var, t in
 sanity (subst_in_problem subst p)
;;

let find_arities_after_app p =
 let rec aux level n = function
 | L t -> assert (n > 0); max_arity_of_var level t :: aux (level+1) (n-1) t
 | _ -> Array.to_list (Array.make n 0)
 in aux 0
;;
let find_all_first_args_of v =
 let rec aux level = function
 | L t -> aux (level+1) t
 | V _ -> []
 | A(V v', t2) -> (if v + level = v' then [t2] else []) @ aux level t2
 | A(t1,t2) -> aux level t1 @ aux level t2
 | _ -> []
 in aux 0
;;

let step' var p =
 let appk = p.k_lam + p.k_app + 1 in
 print_cmd "STEP'" ("on " ^ string_of_t p (V var) ^ " and applies no." ^ string_of_int appk ^ " fresh variables");
 let p, vars = (* +1 below because of lifting *)
  Array.fold_left (fun (p,vars) _ -> let p, v = freshvar p in p, (v+1)::vars)
   (p, []) (Array.make appk ()) in
 let p, t = mk_apps p (V 0) (List.map (fun x -> V x) vars) in

 let first_args = Util.sort_uniq (List.fold_right ((@) ++ (find_all_first_args_of var)) (all_terms p) []) in
 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
 let arities = List.combine (List.map ((+) (-1)) vars) map in

 (* let p, var' = freshvar p in *)
 let p, var' = p, var in
 let matches = (var', []) :: p.matches in
 let p = {p with matches; stepped=var'::p.stepped; arities=arities@p.arities} in
 let t = L (A (lift 1 (V var'), t))  in
 let subst = var, t in
 sanity (subst_in_problem subst p)
;;

let perm var n p =
 if n = 1 then p else (
 print_cmd "PERM" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");
 (* let p, v = freshvar p in *)
 let p, v = p, var in
 let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V m) in
 let rec aux m t =
  if m = 0
   then aux' (n-1) t
   else L (aux (m-1) t) in
 let t = aux n (lift n (V v)) in
 let subst = var, t in
 (* let p = {p with arities=(v, List.assoc var p.arities)::p.arities} in *)
 sanity (subst_in_problem subst p)
) ;;

let free_vars_of_p p =
 Util.sort_uniq (Util.concat_map (free_vars p) (all_terms p));;

let rec applied_vars p = function
| B | P -> []
| L _ -> [] (* ??? *)
| V _ -> []
| A(V v,t2) -> v :: applied_vars p t2
| A(t1,t2) -> applied_vars p t1 @ applied_vars p t2
(* | Ptr n -> applied_vars p (get_conv p n) *)
| Stuck _ -> [] (* ??? *)
;;

let applied_vars_of_p p =
 Util.sort_uniq (Util.concat_map (applied_vars p) (all_terms p));;

let rec auto p =
 let aux f var =
  try
   auto (f var); ()
  with
  | Done _ as d -> raise d
  | Fail(_, s) -> print_endline ("<<< Backtracking because: " ^ s) in
 print_endline ">>> auto called";
 (* Compute useful free variables *)
 let fv = applied_vars_of_p p in
 let fv = List.filter (fun v -> not (List.mem v p.stepped)) fv in
 List.iter (fun v -> print_string ("@`" ^ string_of_int v)) fv;
 let fv0 = List.filter (fun v -> List.assoc v p.arities > 0) fv in (* remove variable with arity left 0, cannot step there *)
 if fv0 = [] then (print_endline "warning! empty step fv0"; List.iter (fun v -> print_string ("@`" ^ string_of_int v)) fv);
 let permute_and_step p v =
  let step'' problem prm var =
   let problem = perm var prm problem in
   (* let _ = read_line () in *)
   let problem = step' var problem in
   problem in
  let arity = List.assoc v p.arities in
  let _, perms = Array.fold_left (fun (arity, acc) () -> let a = arity + 1 in a, a::acc) (1,[1]) (Array.make (arity-1) ()) in
  List.iter (fun perm -> aux (step'' p perm) v) perms
 in
 List.iter (permute_and_step p) fv0;
 List.iter (aux (fun v -> eat v p)) fv;
 (* mancano: applicazioni e choose; ??? *)
;;

let parse strs =
  let rec aux level = function
  | Parser.Lam t -> L (aux (level + 1) t)
  | Parser.App (t1, t2) ->
   if level = 0 then snd (mk_app dummy_p (aux level t1) (aux level t2))
    else A(aux level t1, aux level t2)
  | Parser.Var v -> V v
  in let (tms, free) = Parser.parse_many strs
  in (List.map (aux 0) tms, free)
;;

let magic6 div conv cmds =
 print_hline ();
 let all_tms, var_names = parse (div :: conv) in
 let div, conv = List.hd all_tms, List.tl all_tms in
 let varno = List.length var_names in
 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
 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]; stepped=[];k_app;k_lam;arities=[]} in
 let fv = Util.sort_uniq (Util.concat_map (free_vars p) all_tms) in
 let arities = List.map (fun var -> var, k_app) fv in
 let p = {p with arities} in
 let p = try
  let subst = Util.index_of "BOMB" var_names, L B in
  let p = subst_in_problem subst p in p
  with Not_found -> p in
 let p = sanity p in
 try
  problem_fail (List.fold_left (|>) p cmds) "Problem not completed"
 with
 | Done _ -> ()
;;

let auto div conv =
 print_hline ();
 let all_tms, var_names = parse (div :: conv) in
 let div, conv = List.hd all_tms, List.tl all_tms in
 let varno = List.length var_names in
 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
 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]; stepped=[];k_app;k_lam;arities=[]} in
 let fv = Util.sort_uniq (Util.concat_map (free_vars p) all_tms) in
 let max_arity_of_var_in_p var p =
  1 + List.fold_right (max ++ (max_arity_of_var var)) (all_terms p) 0 in
 let arities = List.map (fun var -> var, max_arity_of_var_in_p var p) fv in
 let p = {p with arities} in
 let p = try
  let subst = Util.index_of "BOMB" var_names, L B in
  let p = subst_in_problem subst p in p
  with Not_found -> p in
 let p = sanity p in
 try
  auto p;
  failwith "auto failed."
 with
 | Done _ -> print_endline "<<< auto ok >>>"; (* TODO: print and verify substitution *)
;;

(* let interactive div conv cmds =
 print_hline ();
 let all_tms, var_names = parse (div @ conv) in
 let div, conv = list_split (List.length div) all_tms in
 let varno = List.length var_names in
 let p = {orig_freshno=varno; freshno=1+varno; div; conv; matches=[]; sigma=[]} in
 (* activate bombs *)
 let p = try
  let subst = Util.index_of "BOMB" var_names, L B in
   subst_in_problem subst p
  with Not_found -> p in
 (* activate pacmans *)
 let p = try
  let subst = Util.index_of "PACMAN" var_names, P in
   let p = subst_in_problem subst p in
   (print_endline ("after subst in problem " ^ string_of_problem p); p)
  with Not_found -> p in
 (* initial sanity check *)
 let p = sanity p in
 let p = List.fold_left (|>) p cmds in
 let rec f p cmds =
  let nth spl n = int_of_string (List.nth spl n) in
  let read_cmd () =
   let s = read_line () in
   let spl = Str.split (Str.regexp " +") s in
   s, let uno = List.hd spl in
    try if uno = "explode" then explode
    else if uno = "ignore" then ignore (nth spl 1) (nth spl 2)
    else if uno = "step" then step (nth spl 1)
    else if uno = "perm" then perm (nth spl 1) (nth spl 2)
    else if uno = "apply" then apply (nth spl 1) (nth spl 2)
    (* else if uno = "forget" then forget (nth spl 1) (nth spl 2) *)
    else if uno = "id" then id (nth spl 1)
    else failwith "Wrong input."
    with Failure s -> print_endline s; (fun x -> x) in
  let str, cmd = read_cmd () in
  let cmds = (" " ^ str ^ ";")::cmds in
  try
   let p = cmd p in f p cmds
  with
  | Done -> print_endline "Done! Commands history: "; List.iter print_endline (List.rev cmds)
 in f p []
;; *)

let _ = auto
 "x x"
 [ "_. BOMB" ]
 (* [ eat 1 ] *)
;;


let _ = auto
   "x y BOMB b"
 [ "x BOMB y c" ]
 (* [ perm 1 3; step' 8 ; eat 4; eat 5; eat 15; ] *)
;;


let _ = auto
 "x BOMB a1 c"
 [ "x y BOMB d"; "x BOMB a2 c" ]
 (* [ perm 1 3 ; step' 10 ; eat 4; eat 6;  step' 17; eat 3; eat 7; eat 27; ] *)
;;


let _ = auto
 "x (x x)"
 [ "x x" ; "x x x" ]
 (* [
 step' 1;
 eat 6; eat 9; eat 13;
]*)
;;


(* let _ = auto
 "x (_.BOMB)"
 [ "x (_._. BOMB)" ]
 (* [ apply 1 2; ] *)
;; *)


let _ = auto
 "x (_.y)"
 [ "y (_. x)" ]
 (* [ apply 1 1; ignore 1 1;  explode; ] *)
;;


let _ = auto
 "y (x a1 BOMB c) (x BOMB b1 d)"
 [ "y (x a2 BOMB c) (x BOMB b1 d)";
 "y (x a1 BOMB c) (x BOMB b2 d)";]
 (* [perm 2 3;
 step 12;
 perm 17 2;
 step 19;
 step 18;
 ignore 22 1;
 ignore 21 1;
 ignore 24 1;
 ignore 25 1;
 step 1;
 step 32;
 explode;
 ] *)
;;

(*
let _ = magic6
 ["z (y x)"]
 [ "z (y (x.x))"; "y (_. BOMB)" ]
 [ apply 2 1; step 3; explode; ]
;;

let _ = magic6
 ["y x"]
 [ "y (x.x)"; "x (_. BOMB)" ]
 [ apply 1 1; ignore 2 1; step 1; explode; ]
;;

let _ = magic6
 ["z (y x)"]
 [ "z (y (x.x))"; "y (_. BOMB)" ]
 [ step 1; explode; apply 2 1; id 2; ignore 3 1; ]
;;

let _ = magic6
 ["y (x a)"]
 [ "y (x b)"; "x BOMB" ] [
 id 2;
 step 1;
 explode;
];;

magic6
 ["y (x a)"] [ "y (x b)"; "x BOMB"; "y a" ]
 [
 apply 1 1;
 perm 2 2;
 ignore 9 1;
 step 10;
 explode;
 ];;
(* "y (a c)"
[ "y (b c)"; "y (x a)"; "y (x b)"; "x BOMB" ]  *)

magic6
["x a (x (a.y BOMB))"]
[ "x b"; "x (y c)"; "x (y d)" ]
[apply 1 1;
apply 2 1;
explode;]
(* [
step 1;
step 3;
explode' 10;
(* ma si puo' fare anche senza forget *) *)
(* ] *)
;;

(* dipendente dalla codifica? no, ma si risolve solo con id *)
magic6
 ["y a"] ["y b"; "x (y (_.BOMB))"]
[
apply 1 1;
apply 2 1;
explode;
];;
 (* [id 1; explode];; *)

magic6
 ["PACMAN (x x x)"] ["PACMAN (x x)"]
 [
 ignore 2 2;
 explode;
 ];; *)

print_hline();
print_endline "ALL DONE. "