open Grammar
open Hashtbl
open Scanf
open Utils
open String
open List

open Grammar

module Set = Set.Make(String)

let rec print_expr expr = match expr with
    | Var (Id v) -> v
    | Appl (t1, t2) -> "(" ^ print_expr t1 ^ " " ^ print_expr t2 ^ ")"
    | Abst (Id x, t) -> "(\\" ^ x ^ "." ^ print_expr t ^ ")"

let rec fill_set_with_vars_from_term term mySet = match term with
    | Abst (Id x, t) -> fill_set_with_vars_from_term t (Set.add x mySet)
    | Appl (t1, t2)  -> Set.union (fill_set_with_vars_from_term t1 mySet) (fill_set_with_vars_from_term t2 mySet)
    | Var (Id v)     -> if Set.mem v mySet then Set.empty else Set.singleton v


let beta_reduction term1 var term2 =
  let filledSet = fill_set_with_vars_from_term term2 Set.empty in
    let namesHashtbl = Hashtbl.create 100 in
      let rec reduce tree flag = match tree with
        | Appl (t1, t2)  -> Appl (reduce t1 flag, reduce t2 flag)
        | Abst (Id x, t) -> if x = var then Abst (Id x, reduce t false) else
                            if Set.mem x filledSet then
                                let new_name = x ^ (string_of_int (Random.int 100)) in
                                 let add_to_hashtbl = Hashtbl.add namesHashtbl x new_name in
                                  let new_tsubtree = ref nil in
                                    add_to_hashtbl;
                                    new_tsubtree := Abst (Id new_name, reduce t flag);
                                    Hashtbl.remove namesHashtbl x;
                                    !new_tsubtree;
                            else Abst (Id x, reduce t flag)
        | Var (Id v)     -> if Hashtbl.mem namesHashtbl v then
                              Var (Id (Hashtbl.find namesHashtbl v))
                            else if flag && v = var then term2 (* deferred substitution ?? *) else tree
      in reduce term1 true

(*  let rec rect_redex tree flag = if !flag == true then tree else match tree with
  | Var (Id v)                 -> tree
  | Abst (Id x, t)             -> Abst (Id x, rect_redex t flag)
  | Appl (Abst(Id x, t1), t2)  -> flag := true; beta_reduction t1 x t2
  | Appl (Var x, t2)           -> Appl (Var x, rect_redex t2 flag)
  | Appl (t1, t2)              ->
    let new_tree1 = rect_redex t1 flag in
        if !flag == true then Appl(new_tree1, t2) else
          Appl (t1, rect_redex t2 flag) *)


let rec rect_redex tree flag = (*if !flag == true then tree else*) match tree with
  | Var (Id v)                 -> tree
  | Abst (Id x, t)             -> Abst (Id x, rect_redex t flag)
  | Appl (Abst(Id x, t1), t2)  -> flag := true; beta_reduction t1 x t2 (*not one...*)
  | Appl (Var x, t2)           -> Appl (Var x, rect_redex t2 flag)
  | Appl (t1, t2)              ->
    let new_tree1 = rect_redex t1 flag in
    let new_tree2 = rect_redex t2 flag in
        Appl (new_tree1, new_tree2)

let rec one_step tree n k m =
let flag = ref true in
  if ((n mod k) = 0) then begin
      print_string (print_expr tree);
      print_char '\n';
      flag := false;
    end;
  if n > m then tree else
    let has_redex = ref false in
    let new_tree = rect_redex tree has_redex in
    if !has_redex then one_step new_tree (n + 1) k m else
      if !flag then begin
          print_string (print_expr tree);
          print_char '\n';
          tree;
        end
      else tree
;;

let km = split_on_char ' ' (read_line()) in
  let k = match km with
  | kk :: [mm] -> int_of_string kk in
  let m = match km with
  | kk :: [mm] -> int_of_string mm in
    one_step (Parser.main Lexer.main (Lexing.from_string (read_line()))) 0 k m

(* (\x.x x x x)((\x.x)(\x.x)) *)