<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(* ========================================================================= *)
(* Untyped lambda calculus.                                                  *)
(*                                                                           *)
(*                   Freek Wiedijk, Radboud University Nijmegen              *)
(* ========================================================================= *)

open List;;

let id x = x;;

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

let rec index s l =
  match l with
    [] -> raise Not_found
  | t::k -> if s = t then 0 else (index s k) + 1;;

(* ------------------------------------------------------------------------- *)
(* Type of lambda terms.                                                     *)
(* ------------------------------------------------------------------------- *)

type term =
  Const of string
| App of term * term
| Abstr of string * term
| Var of int;;

(* ------------------------------------------------------------------------- *)
(* Reading lambda terms.                                                     *)
(* ------------------------------------------------------------------------- *)

let explode s =
  let rec explode1 n =
    try let s1 = String.make 1 s.[n] in s1::(explode1 (n + 1))
    with Invalid_argument _ -> [] in
  explode1 0;;

let implode l = fold_right (^) l "";;

let lex l =
  let rec lex1 l =
    match l with
      [] -> []
    | c::k ->
        if mem c [" "; "\t"; "\n"] then lex1 k else
        if mem c ["^"; "."; "("; ")"] then c::(lex1 k) else
        if c = "'" then failwith "lex" else lex2 [c] k
  and lex2 v l =
    match l with
      [] -> [implode v]
    | c::k -> if c = "'" then lex2 (v@[c]) k else (implode v)::(lex1 l) in
  lex1 l;;

let parse l =
  let rec apps l =
    match l with
      [] -> failwith "parse"
    | [t] -> t
    | t::u::v -> apps (App(t,u)::v) in
  let rec parse1 c l =
    let t,k = parse2 c l in (apps t),k
  and parse2 c l =
    match l with
      [] -> [],[]
    | "^"::k -> let t,j = parse3 c k in [t],j
    | "."::_ -> failwith "parse"
    | "("::k ->
       (let t,j = parse1 c k in
          match j with
            ")"::i ->
              let u,h = parse2 c i in (t::u),h
          | _ -> failwith "parse")
    | ")"::_ -> [],l
    | s::k ->
       (let t = try Var(index s c) with Not_found -> Const(s) in
        let u,j = parse2 c k in
          (t::u),j)
  and parse3 c l =
    match l with
      [] -> failwith "parse"
    | "."::k -> parse1 c k
    | s::k ->
        if mem s ["^"; "("; ")"] then failwith "parse" else
          let t,j = parse3 (s::c) k in
            Abstr(s,t),j in
  let t,k = parse1 [] l in
    if k = [] then t else failwith "parse";;

let term = parse ** lex ** explode;;

(* ------------------------------------------------------------------------- *)
(* Writing lambda terms.                                                     *)
(* ------------------------------------------------------------------------- *)

let term_to_string t =
  let rec term_to_string1 b1 b2 c t =
    match t with
      Const(s) -> s
    | Var(n) -> (try nth c n with Failure "nth" -> failwith "term_to_string")
    | App(f,x) ->
        let s = (term_to_string1 false true c f)^
            (term_to_string1 true (not b1 & b2) c x) in
        if b1 then "("^s^")" else s
    | Abstr(v,a) ->
        let s = "^"^(term_to_string2 c t) in
        if b2 then "("^s^")" else s
  and term_to_string2 c t =
    match t with
      Abstr(v,a) -> v^(term_to_string2 (v::c) a)
    | _ -> "."^(term_to_string1 false false c t) in
  term_to_string1 false false [] t;;

let alpha t =
  let rec occurs c t n v =
    match t with
      Const(w) -> v = w
    | Var(m) -> m > n & v = nth c m
    | App(f,x) -> (occurs c f n v) or (occurs c x n v)
    | Abstr(w,a) -> occurs (w::c) a (n + 1) v in
  let rec alpha1 c t =
    match t with
      App(f,x) -> App(alpha1 c f,alpha1 c x)
    | Abstr(v,a) -> alpha2 c a v
    | _ -> t
  and alpha2 c t v =
    if occurs (v::c) t 0 v then alpha2 c t (v^"'")
      else Abstr(v,alpha1 (v::c) t) in
  alpha1 [] t;;

let print_term f t =
  Format.pp_print_string f ("term \""^(term_to_string (alpha t))^"\"");;

(* #install_printer print_term;; *)

(* ------------------------------------------------------------------------- *)
(* Combinators.                                                              *)
(* ------------------------------------------------------------------------- *)

let combinators = ref (rev
  ["I", term "^x.x";
   "K", term "^xy.x";
   "S", term "^xyz.(xz)(yz)";
   "B", term "^xyz.x(yz)";
   "C", term "^xyz.xzy";
   "W", term "^xy.xyy";
   "1", term "^xy.xy";
   "Y", term "^f.(^x.f(xx))(^x.f(xx))";
   "T", term "^xy.x";
   "F", term "^xy.y";
   "D", term "^x.xx";
   "J", term "^abcd.ab(adc)";
   "C'", term "JII"]);;

let unfold f =
  match f with
    Const(s) -> (try assoc s !combinators with Not_found -> f)
  | _ -> f;;

(* ------------------------------------------------------------------------- *)
(* Reduction.                                                                *)
(* ------------------------------------------------------------------------- *)

let rec lift d n t =
  match t with
    Var(m) -> if m >= n then Var(m + d) else Var(m)
  | App(f,x) -> App(lift d n f,lift d n x)
  | Abstr(v,a) -> Abstr(v,lift d (n + 1) a)
  | _ -> t;;

let rec subst d n u t =
  match t with
    Var(m) -> if m = n then lift d 0 u else if m > n then Var(m - 1) else t
  | App(f,x) -> App(subst d n u f,subst d n u x)
  | Abstr(v,a) -> Abstr(v,subst (d + 1) (n + 1) u a)
  | _ -> t;;

exception Normal;;

let maybe f x = try f x with Normal -> x;;

let beta i j t =
  match t with
    App(f,x) ->
      let f' = unfold f in
     (match f' with
        Abstr(_,a) -> subst 0 0 (maybe i x) (maybe i a)
      | _ -> if f' <> f then j (App(f',x)) else raise Normal)
  | _ -> raise Normal;;

let current_beta = ref beta;;
let current_eta = ref (fun i t -> raise Normal);;

let rec leftmost_innermost t =
  match t with
    App(f,x) ->
     (try App(leftmost_innermost f,x)
      with Normal ->
        try App(f,leftmost_innermost x)
        with Normal ->
          !current_beta id leftmost_innermost t)
  | Abstr(v,a) ->
     (try Abstr(v,leftmost_innermost a)
      with Normal ->
        !current_eta id t)
  | _ -> raise Normal;;

let rec leftmost_outermost t =
  match t with
    App(f,x) ->
     (try !current_beta id leftmost_outermost t
      with Normal ->
        try App(leftmost_outermost f,x)
        with Normal ->
          App(f,leftmost_outermost x))
  | Abstr(v,a) ->
     (try !current_eta id t
      with Normal ->
        Abstr(v,leftmost_outermost a))
  | _ -> raise Normal;;

let rec parallel_outermost t =
  match t with
    App(f,x) ->
     (try !current_beta id parallel_outermost t
      with Normal ->
        try let g = parallel_outermost f in
          App(g,maybe parallel_outermost x)
        with Normal ->
          App(f,parallel_outermost x))
  | Abstr(v,a) ->
     (try !current_eta id t
      with Normal ->
        Abstr(v,parallel_outermost a))
  | _ -> raise Normal;;

let rec gross_knuth t =
  match t with
    App(f,x) ->
     (try !current_beta gross_knuth gross_knuth t
      with Normal ->
        try let g = gross_knuth f in
          App(g,maybe gross_knuth x)
        with Normal ->
          App(f,gross_knuth x))
  | Abstr(v,a) ->
     (try !current_eta gross_knuth t
      with Normal ->
        Abstr(v,gross_knuth a))
  | _ -> raise Normal;;

let rec reduce x z n t =
  if n = 0 then z else
    try let u = x t in t::(reduce x z (n - 1) u) with Normal -> [t];;

let rec normal_form x t =
  try normal_form x (x t) with Normal -> t;;

(* ------------------------------------------------------------------------- *)
(* Abbrevs.                                                                  *)
(* ------------------------------------------------------------------------- *)

let etc = [Const("...")];;
let all = -1;;

let nf = normal_form leftmost_outermost ** term;;

let red n = reduce leftmost_outermost etc n ** term;;
let red_eager n = reduce leftmost_innermost etc n ** term;;
let red_par n = reduce parallel_outermost etc n ** term;;
let red_gk n = reduce gross_knuth etc n ** term;;

(* ------------------------------------------------------------------------- *)
(* Examples.                                                                 *)
(* ------------------------------------------------------------------------- *)

(*
nf "(^x.fx)a";;
nf "(KISS)(KISS)";;
red_gk all "SKK";;
red 7 "(^x.xx)(^x.xx)";;
*)

(* ========================================================================= *)
(* Extra code for Jan-Willem                                                 *)
(* ========================================================================= *)

let rec free n t =
  match t with
    App(f,x) -> free n f && free n x
  | Abstr(_,t') -> free (n + 1) t'
  | Var(n') -> n <> n'
  | _ -> true;;

let eta i t =
  match t with
    Abstr(_,App(f,Var(0))) ->
      if free 0 f then lift (-1) 0 (maybe i f) else raise Normal
  | _ -> raise Normal;;

let translate e =
  let rec translate t =
    match t with
      App(f,x) -> App(translate f,translate x)
    | Abstr(v,u) ->
        if u = Var(0) then Const("I") else
        if free 0 u then App(Const("K"),translate (lift (-1) 0 u)) else
       (match translate u with
          Var(0) -> Const("I")
        | App(a,b) ->
            if e && b = Var(0) && free 0 a then lift (-1) 0 a else
            App(App(Const("S"),translate (Abstr(v,a))),translate (Abstr(v,b)))
        | _ -> failwith "translate")
    | _ -> t
  in translate;;

let translate_henk e =
  let rec translate t =
    match t with
      App(f,x) -> App(translate f,translate x)
    | Abstr(v,u) ->
        if u = Var(0) then Const("I") else
        if free 0 u then App(Const("K"),translate (lift (-1) 0 u)) else
       (match translate u with
          Var(0) -> Const("I")
        | App(a,b) ->
            if free 0 a then
              if e && b = Var(0) then lift (-1) 0 a else
              App(App(Const("B"),lift (-1) 0 a),translate (Abstr(v,b)))
            else
            if free 0 b then
              App(App(Const("C"),translate (Abstr(v,a))),lift (-1) 0 b)
            else
              App(App(Const("S"),translate (Abstr(v,a))),translate (Abstr(v,b)))
        | _ -> failwith "translate")
    | _ -> t
  in translate;;

let translate_church e =
  let tau = term "JII" in
  let _JI = term "JI" in
  let _J = term "J" in
  let _Jt = App(_J,tau) in
  let _Jtt = App(_Jt,tau) in
  let rec translate t =
    match t with
      App(f,x) -> App(translate f,translate x)
    | Abstr(v,u) ->
        if u = Var(0) then Const("I") else
        if free 0 u then App(Const("K"),translate (lift (-1) 0 u)) else
       (match translate u with
          Var(0) -> Const("I")
        | App(a,b) ->
            if free 0 a then
              if e && b = Var(0) then lift (-1) 0 a else
              App(App(App(_J,tau),translate (Abstr(v,b))),
                App(_JI,lift (-1) 0 a))
            else
            if free 0 b then
              App(App(_Jt,lift (-1) 0 b),translate (Abstr(v,a)))
            else
              App(_Jtt,App(_JI,App(_Jtt,
                App(App(_Jt,translate (Abstr(v,b))),
                  App(App(_Jt,translate (Abstr(v,a))),_J)))))
        | _ -> failwith "translate")
    | _ -> t
  in translate;;

let rec term_size t =
      match t with
        App(f,x) -> term_size f + term_size x
      | Abstr(v,t') -> term_size t' + 1
      | _ -> 1;;

let rec equal t t' =
  if t = t' then true else
  let t = unfold t in
  let t' = unfold t' in
  match t with
    App(f,x) ->
     (match t' with
        App(f',x') -> equal f f' && equal x x'
      | _ -> false)
  | Abstr(_,u) ->
     (match t' with
        Abstr(_,u') -> equal u u'
      | _ -> false)
  | _ -> t = t';;

let assoc' t l =
  let rec assoc' l =
    match l with
      [] -> raise Not_found
    | (v,t')::l' -> if equal t' t then v else assoc' l' in
  assoc' l;;

let current_fold = ref id;;

let rec fold t =
  try let v = assoc' t !combinators in Const(v)
  with _ ->
    match t with
      App(f,x) -> App(fold f,fold x)
    | Abstr(v,t') -> Abstr(v,fold t')
    | _ -> t;;

let sub c1 c2 =
  implode ** map (fun c -> if c = c1 then c2 else c) ** explode;;

let term_to_string' t =
  sub "^" "\\" (term_to_string (alpha t));;

let rec occurs t' t =
  if equal t' t then true else
  match unfold t with
    App(f,x) -> occurs t' f || occurs t' x
  | Abstr(_,u) -> occurs t' u
  | _ -> false;;

let rec flatten t =
  match t with
    App(f,x) -> let f',l' = flatten f in f',(l'@[x])
  | _ -> t,[];;

let rec unflatten (f,l) =
  match l with
    [] -> f
  | x::l' -> unflatten (App(f,x),l');;

let rec lambda_count t =
  match t with
    Abstr(_,a) -> 1 + lambda_count a
  | _ -> 0;;

let beta_combinator i j t =
  let rec red_combinator f l =
    if l = [] then f,l else
    match f with
      Abstr(_,a) ->
       (match l with
          [] -> failwith "beta_combinator"
        | x::l' -> red_combinator (subst 0 0 (maybe i x) a) l')
    | _ -> f,l in
  match t with
    App(f,x) ->
     (match f with
        Abstr(_,a) -> subst 0 0 (maybe i x) (maybe i a)
      | _ ->
          let f,l = flatten t in
         (match f with
            Const(_) ->
              let f' = unfold f in
              let n = lambda_count f' in
              let m = length l in
              if n = m then
                let f'',l' = red_combinator f' l in
                if l' = [] then f'' else failwith "beta_combinator"
              else if f' <> f && n = 0 then
               (match l with
                  [x] -> App(f',x)
                | _ -> raise Normal)
              else raise Normal
          | _ -> raise Normal))
  | _ -> raise Normal;;

let current_term = ref None;;
let current_history = ref [];;
let current_future = ref [[]];;
let current_strategy = ref leftmost_outermost;;

let set_current_term t =
  current_term := Some t (* ; current_future := [[]] *) ;;

let clear_current_term () =
  current_term := None;;

let rec unfold_combinators t =
  match unfold t with
    App(f,x) -> App(unfold_combinators f,unfold_combinators x)
  | Abstr(v,u) -> Abstr(v,unfold_combinators u)
  | t -> t;;

let unfold_combinator s' =
  let t' = assoc s' !combinators in
  let rec unfold_combinator t =
    match t with
      App(f,x) -> App(unfold_combinator f,unfold_combinator x)
    | Abstr(v,u) -> Abstr(v,unfold_combinator u)
    | Const(s) -> if s = s' then t' else t
    | _ -> t in
  unfold_combinator;;

let add_combinator s =
  let l = lex (explode s) in
  match l with
    [v;"="] ->
      combinators := filter (fun x -> fst x <> v) !combinators;
      true
  | v::"="::l' ->
      (try
        let t = parse l' in
        try
          let t' = assoc v !combinators in
          print_string ("      "^v^" already defined\n"^
            "    "^v^"="^(term_to_string' t')^"\n");
          true
        with Not_found ->
          let s' = term_to_string' t in
          if occurs (Const(v)) t then
           (print_string ("      cyclic definition: "^v^" occurs in "^s'^"\n");
            true)
          else
          match t with
            Const _ ->
              print_string ("      will not abbreviate single variable\n");
              true
          | _ ->
             (print_string ("    "^v^"="^s'^"\n");
              combinators := (v,t)::!combinators;
              true)
      with Failure "parse" -> false)
  | ["^";v] ->
     (match v with
        "^" ->
         (match !current_term with
            Some t -> set_current_term (unfold_combinators t)
          | None -> print_string "      no term to unfold\n");
          true
      | "." -> false
      | "(" -> false
      | ")" -> false
      | _ ->
         (match !current_term with
            Some t ->
             (try set_current_term (unfold_combinator v t)
              with Not_found ->
                print_string ("      no definition for "^v^"\n"))
          | None -> print_string "      no term to unfold\n");
          true)
  | _ -> false;;

let rec split_last l =
  match l with
    [] -> raise Not_found
  | h::t -> let l,x = split_last t in (h::l),x;;

let pop_history () =
  match !current_history with
    (t::l)::h ->
      current_history := l::h;
      current_term := Some t
  | _ -> raise Not_found;;

let prev_history () =
  match !current_history with
    [] -> raise Not_found
  | [t]::h ->
      if h = [] then raise Not_found else
      current_history := h;
     (match !current_future with
        [] -> failwith "prev_history"
      | l'::h' -> current_future := []::(t::l')::h')
  | (t::l)::h ->
      current_history := l::h;
     (match !current_future with
        [] -> failwith "prev_history"
      | l'::h' -> current_future := (t::l')::h')
  | _ -> failwith "prev_history";;

let next_history () =
  match !current_future with
    [[]] -> raise Not_found
  | []::(t::l)::h ->
      current_history := [t]::!current_history;
      current_future := l::h
  | (t::l)::h ->
     (match !current_history with
        [] -> failwith "next_history"
      | l'::h' ->
          current_history := (t::l')::h';
          current_future := l::h)
  | _ -> failwith "next_history";;

let prev_term () =
  try
    if !current_term <> None then prev_history();
    pop_history()
  with Not_found -> print_string "      no previous term\n";;

let next_term () =
  try
    next_history();
    pop_history()
  with Not_found -> print_string "      no next term\n";;

let at_input () =
  match !current_history with
    [_]::_ -> true
  | _ -> false;;

let prev_input () =
  try
    if !current_term <> None then prev_history();
    while not (at_input()) do prev_history() done;
    pop_history()
  with Not_found -> print_string "      no previous input term\n";;

let next_input () =
  try
    next_history();
    while not (at_input()) do next_history() done;
    pop_history()
  with Not_found -> print_string "      no next input term\n";;

let interactive_normal_form () =
 let n = ref 0 in
 (try
    Sys.catch_break true;
    while true do
      match !current_term with
        Some t ->
          set_current_term (!current_strategy t);
          n := !n + 1
      | None ->
          print_string "      no term to normalize\n";
          raise Normal
    done
  with
    Normal -> ()
  | Sys.Break ->
      print_string "      normalization interrupted\n");
  print_string ("      "^(string_of_int !n)^" reduction step"^
    (if !n = 1 then "" else "s")^"\n");
  Sys.catch_break false;
  match !current_term with
    Some t ->
      let m = term_size t in
     (if m > 1000 then
        print_string ("      the term has "^(string_of_int m)^
          " nodes, printing it might take very long\n"));
      flush stdout
  | None -> ();;

let interactive_translate e () =
  match !current_term with
    Some t -> set_current_term (translate e (unfold t))
  | None -> print_string "      no term to translate\n";;

let interactive_translate_henk e () =
  match !current_term with
    Some t -> set_current_term (translate_henk e (unfold t))
  | None -> print_string "      no term to translate\n";;

let interactive_translate_church e () =
  match !current_term with
    Some t -> set_current_term (translate_church e (unfold t))
  | None -> print_string "      no term to translate\n";;

let fold_current_term () =
  match !current_term with
    Some t -> set_current_term (fold t)
  | None -> print_string "      no term to fold\n";;

let rec help () =
  let _ = map (fun xy ->
      let x,y = xy in
      print_string ("    "^x^"="^(term_to_string' y)^"\n"))
    (rev !combinators) in
  let _ = map (fun xy ->
      let x,(y,_) = xy in
      print_string ("      "^x^" "^y^"\n"))
    commands in
  ()

and commands =
  [".li",      ("leftmost innermost",
                fun () -> current_strategy := leftmost_innermost);
   ".lo",      ("leftmost outermost [default]",
                fun () -> current_strategy := leftmost_outermost);
   ".po",      ("parallel outermost",
                fun () -> current_strategy := parallel_outermost);
   ".gk",      ("gross knuth",
                fun () -> current_strategy := gross_knuth);
   ".l",       ("lambda reduction [default]",
                fun () -> current_beta := beta);
   ".c",       ("combinator reduction",
                fun () -> current_beta := beta_combinator);
   ".ex",      ("eta reduction",
                fun () -> current_eta := eta);
   ".in",      ("no eta reduction [default]",
                fun () -> current_eta := fun i t -> raise Normal);
   "./",       ("fold combinators", fold_current_term);
   "./IKS",    ("translate to IKS",
                interactive_translate false);
   ".//IKS",   ("translate to IKS using eta",
                interactive_translate true);
   "./IKBCS",  ("translate to IKBCS",
                interactive_translate_henk false);
   ".//IKBCS", ("translate to IKBCS using eta",
                interactive_translate_henk true);
   "./IJK",    ("translate to IJK",
                interactive_translate_church false);
   ".//IJK",   ("translate to IJK using eta",
                interactive_translate_church true);
   "..",       ("normalize", interactive_normal_form);
   ".<<",      ("previous input term", prev_input);
   ".<",       ("previous term", prev_term);
   ".>",       ("next term", next_term);
   ".>>",      ("next input term", next_input);
   ".?",       ("help", help);
   ".",        ("exit", fun () -> failwith "exit")];;

let rec step_term n m =
  if n > 0 then
    match !current_term with
      Some t ->
        (try set_current_term (!current_strategy t);
	   step_term (n - 1) (m + 1)
         with Normal -> m);
    | None -> m
  else m;;

let main () =
  help();
  while true
  do
   (let s = sub "\\" "^" (read_line()) in
    if s = "." then
      if !current_term = None then
        failwith "main"
      else
        clear_current_term ()
    else
    try
      let _,y = assoc s commands in y()
    with Not_found ->
      if add_combinator s then () else
     (if s = "" then
         (if step_term 1 0 < 1 then clear_current_term ())
       else
         try let m = step_term (int_of_string s) 0 in
	   print_string ("      "^(string_of_int m)^" reduction step"^
	     (if m = 1 then "" else "s")^"\n")
	 with
	 | Normal -> ()
	 | _ ->
         try
           let t = term s in
           set_current_term t;
           current_history := []::!current_history
         with Failure "parse" ->
           print_string "      syntax error\n"));
    match !current_term with
      Some t ->
        let t = !current_fold t in
        current_term := Some t;
       (match !current_history with
          [] -> failwith "history"
        | l::h -> current_history := (t::l)::h);
        Sys.catch_break true;
       (try
          print_string ("  "^(term_to_string' t)^" ")
        with Sys.Break ->
          print_string ("      term printing interrupted\n"^
            "  [term with "^(string_of_int (term_size t))^" nodes] "));
        Sys.catch_break false;
    | None -> ()
  done;;

try main() with Failure "main" -> () | End_of_file -> ();;