(* https://github.com/kayceesrk/cs3100_f19/blob/cc71e59a081543257adc72a2428685e891bcd307/assignments/assignment1.ipynb *)

(* cond_dup: 'a list -> ('a -> bool) -> 'a list *)
let cond_dup l f =
  List.fold_right
    (fun a acc ->
      (if f a then a :: a :: acc 
       else a :: acc))
    l []
(* # cond_dup [3;4;5] (fun x -> x mod 2 = 1);; *)
(* - : int list = [3; 3; 4; 5; 5] *)

let rec n_times (f, n, v) =
  if n <= 0 then v
  else n_times (f, n-1, f v)
(* # n_times((fun x-> x+1), 50, 0);; *)
(* - : int = 50 *)

let rec range start stop =
  if stop - start >= 0 then start :: (range (start+1) stop)
  else []
(* # range 2 5;; *)
(* - : int list = [2; 3; 4; 5] *)

let rec zipwith f a b =
  match a, b with
  | [], _
  | _, [] -> []
  | a'::aa, b'::bb -> (f a' b') :: (zipWith f aa bb)
(* # zipwith (+) [1;2;3] [4;5];; *)
(* - : int list = [5; 7] *)

(* let rec flatten l = *)
(*   match l with *)
(*   | [] -> [] *)
(*   | l :: ls -> l @ (flatten ls) *)
let rec flatten = function
  | [] -> []
  | l :: ls -> l @ (flatten ls)
(* # flatten ([[1;2];[3;4]]);; *)
(* - : int list = [1; 2; 3; 4] *)

let remove_stutter l = snd (List.fold_right
    (fun x (prev, res) ->
       match prev with
       | None -> (Some x, x::res)
       | Some prev' ->
           if x=prev' then (prev, res)
           else (Some x, x::res))
    l (None, []))
(* # remove_stutter [1;2;2;3;1;1;1;4;4;2;2];; *)
(* - : int list = [1; 2; 3; 1; 4; 2] *)


(*********************************************************************)


(* https://github.com/kayceesrk/cs3100_f19/blob/cc71e59a081543257adc72a2428685e891bcd307/assignments/assignment2.zip *)

type expr
  = Var of string
  | App of expr * expr
  | Lam of string * expr

(* prettify: expr -> string *)
let rec prettify e =
  match e with
  | Var v -> v
  | App (e1, e2) -> "(" ^ (prettify e1) ^ "  " ^ (prettify e2) ^ ")"
  | Lam (v, e') -> "λ" ^ v ^ "." ^ (prettify e')

let mem v vars = List.exists (fun x -> x=v) vars

(* # mem "b" ["a";"b";"c"];; *)
(* - : bool = true *)
(*                           *)
(* # mem "x" ["a";"b";"c"];; *)
(* - : bool = false *)

let remove v vars = List.filter (fun x -> not (v=x)) vars

(* # remove "b" ["a";"b";"c"];; *)
(* - : string list = ["a"; "c"] *)
(*                              *)
(* # remove "x" ["a";"b";"c"];; *)
(* - : string list = ["a"; "b"; "c"] *)

(* union: string list -> string list -> string list *)
let union s1 s2 =
  remove_stutter (List.sort String.compare (s1 @ s2))

(* # union ["a"; "c"; "b"] ["d"; "b"; "x"; "a"];;  *)
(* - : String.t list = ["a"; "b"; "c"; "d"; "x"] *)

let add a l =
  let l' =
    (if List.exists (fun x -> x=a) l then l
    else a::l) in
  List.sort
    (fun x y ->
       if x < y then -1
       else if x = y then 0
       else 1) l'

(* # add "b" ["a";"c"];; *)
(* - : string list = ["a"; "b"; "c"] *)
(*                       *)
(* # add "a" ["c"; "a"];; *)
(* - : string list = ["a"; "c"] *)

let varcount = ref 0
let fresh s =
  let v = !varcount in
  s ^ (string_of_int v)
  
(* free_variables: expr -> string list *)
let rec free_variables = function
  | Var v -> [v]
  | App (e1, e2) ->
      let fv1 = free_variables e1 in
      let fv2 = free_variables e2 in
      union fv1 fv2
  | Lam (v, e') ->
      let fv = free_variables e' in
      remove v fv

(* # free_variables (Lam ("x", Var "x"));; *)
(* - : String.t list = [] *)
(*                        *)
(* # free_variables (Lam ("x", Var "y"));; *)
(* - : String.t list = ["y"] *)

(* substitute : expr -> string -> expr -> expr *)
(* substitute e1 var e2 means e1[e2/var] *)
let rec substitute e var repl =
  match e with
  | Var v -> repl
  | App (e1, e2) -> App (substitute e1 var repl, substitute e2 var repl)
  | Lam (v, body) -> 
      if v=var then
        (* A bound variable. Can be interfered with only on a beta-reduction *)
        e
      else
        let v' = 
          (* Avoid free variable capture *)
          if mem v (free_variables repl) then fresh v
          else v in
        let body' = substitute body var repl in
        Lam (v', body')

(* (λy.x)[(λz.z w)/x] is (λy.λz.z w) *)
(* # substitute (Lam ("y", Var "x")) "x" (Lam ("z", App (Var "z", (Var "w"))));; *)
(* - : expr = Lam ("y", Lam ("z", App (Var "z", Var "w"))) *)
(*                                                   *)
(* (λx.x)[y/x] is (λx.x) *)
(* # substitute (Lam ("x", Var "x")) "x" (Var "y");; *)
(* - : expr = Lam ("x", Var "x") *)
(*                                                   *)
(* (λx.y)[x/y] is (λx0. x) *)
(* # substitute (Lam ("x", Var "y")) "y" (Var "x");; *)
(* - : expr = Lam ("x0", Var "x") *)


(* reduce_cbv : expr -> expr * bool *)
let reduce_cbv e =
  match e with
  | App (e1, e2) -> 
      (match e1 with
      | Lam (v, e') -> (substitute e' v e2, true)
      | _ ->
         (* Still got space to reduce *)
         let (e1', flag) = reduce_cbv e1 in
         (App (e1', e2), flag))
  | _ -> (e, false)

(* # let e, flag = *)
(* reduce_cbv ( *)
(* App ( *)
(*   App ( *)
(*     Lam ("x", Var "x"), *)
(*     Lam ("x", Var "x")), *)
(*   Lam ("z", *)
(*     App (Lam ("x", Var "x"), *)
(*          Var "z")))) in (prettify e, flag);; *)
(* - : string * bool = ("(λx.x  λz.(λx.x  z))", true) *)

(* prettify ( *)
(* App ( *)
(*   Lam ("x", Var "x), *)
(*   Lam ("z", *)
(*        App ( *)
(*          Lam ("x", Var "x), *)
(*          Var "z")))) *)
               
(* App (Lam ("z",  *)
(*           Lam ("x", Var "x")), *)
(*      Var "z" *)

(* let expr, reduced = reduce_cbv (parse_string "(λx.x) (λz.(λx.x) z)") in *)
(* assert (reduced = true && *)
(*         alpha_equiv expr (parse_string "λz.(λx.x) z")); *)
        
(* let expr, reduced = reduce_cbv (parse_string "λz.(λx.x) z") in *)
(* assert (reduced = false && *)
(*         alpha_equiv expr (parse_string "λz.(λx.x) z")); *)
        
(* let expr, reduced = reduce_cbv (parse_string "(λx.y) ((λx.x x) (λx.x x))") in *)
(* assert (reduced = true && *)
(*         alpha_equiv expr (parse_string "(λx.y) ((λx.x x) (λx.x x))")); *)

(* let expr, reduced = reduce_cbv (parse_string "x y z") in *)
(* assert (reduced = false && *)
(*         alpha_equiv expr (parse_string "x y z")) *)

let rec reduce_normal e =
  let e', flag = reduce_cbv e in
  if flag then reduce_normal e'
  else e'