ocaml/tmp.ml

   1 (((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c)))) (((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)))\r
   2 ((((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a)) (x. (w. (w. c))))\r
   3 (((((b (a v)) (a. (y c))) z) (w. w)) ((a c) c))\r
   4 (((((v (((a v) w) (((a v) w) v))) (w. c)) (b (a v))) c) (z. a))\r
   5 ((((a (y c)) ((y c) ((a v) (w (z. a))))) (w. c)) (x. w))\r
   6 \r
   7 \r
   8 \r
   9 \r
  10 \r
  11 \r
  12 \r
  13 \r
  14 \r
  15 \r
  16 \r
  17 \r
  18 \r
  19 \r
  20 let fancy_of_term : nf -> Console.fancyobj =\r
  21   let open Console in\r
  22   let of_var level n =\r
  23     if n < level\r
  24     then fancy_of_string (string_of_var n)\r
  25     else (("x" ^ string_of_int (level-n-1)) / ("var<sup>" ^ string_of_int (n-level) ^ "</sup>"))\r
  26   in let rec aux level = function\r
  27     `Var n -> of_var level n\r
  28   | `N n -> fancy_of_string (string_of_int n)\r
  29   | `Match(t,bs_lift,bs,args) ->\r
  30      "([" ^^ aux level (t :> nf) ^^\r
  31      " ? " ^ String.concat " | " (List.map (fun (n,t) -> string_of_int n ^ " => " ^ print ~l (lift bs_lift t)) !bs) ^ "] " ^\r
  32      String.concat " " (List.map (print ~l) args) ^ ")"\r
  33   | `I(n,args) -> "(" ^ print_name l n ^ " " ^ String.concat " " (Listx.to_list (Listx.map (print ~l) args)) ^ ")"\r
  34   | `Lam nf ->\r
  35      let name = string_of_var (List.length l) in\r
  36      "λ" ^ name ^ "." ^ print ~l:(name::l) (nf : nf)\r
  37   in aux 0\r
  38 ;;\r