example: lambda, that print reduction of random lambda-terms using PrintBox

_oasis

@@ -189,6 +189,13 @@ Executable web_pwd
   Build$: flag(cgi)
   BuildDepends: containers, containers.cgi, threads, CamlGI
 
+Executable lambda
+  Path: examples/
+  Install: false
+  MainIs: lambda.ml
+  Build$: flag(misc)
+  BuildDepends: containers,containers.misc
+
 SourceRepository head
   Type: git
   Location: https://github.com/c-cube/ocaml-containers

examples/lambda.ml

@@ -0,0 +1,114 @@
+
+(** Example of printing trees: lambda-term evaluation *)
+
+open Containers_misc
+
+type term =
+  | Lambda of string * term
+  | App of term * term
+  | Var of string
+
+let _gensym =
+  let r = ref 0 in
+  fun () ->
+    let s = Printf.sprintf "x%d" !r in
+    incr r;
+    s
+
+module SSet = Set.Make(String)
+module SMap = Map.Make(String)
+
+let rec fvars t = match t with
+  | Var s -> SSet.singleton s
+  | Lambda (v,t') ->
+      let set' = fvars t' in
+      SSet.remove v set'
+  | App (t1, t2) -> SSet.union (fvars t1) (fvars t2)
+
+(* replace [var] with the term [by] *)
+let rec replace t ~var ~by = match t with
+  | Var s -> if s=var then by else t
+  | App (t1,t2) -> App (replace t1 ~var ~by, replace t2 ~var ~by)
+  | Lambda (v, t') when v=var -> t  (* no risk *)
+  | Lambda (v, t') -> Lambda (v, replace t' ~var ~by)
+
+(* rename [t] so that [var] doesn't occur in it *)
+let rename ~var t =
+  if SSet.mem var (fvars t)
+    then replace t ~var ~by:(Var (_gensym ()))
+    else t
+
+let (>>=) o f = match o with
+  | None -> None
+  | Some x -> f x
+
+let rec one_step t = match t with
+  | App (Lambda (var, t1), t2) ->
+      let t2' = rename ~var t2 in
+      Some (replace t1 ~var ~by:t2')
+  | App (t1, t2) ->
+      begin match one_step t1 with
+      | None ->
+          one_step t2 >>= fun t2' ->
+          Some (App (t1,t2'))
+      | Some t1' ->
+          Some (App (t1',t2))
+      end
+  | Var _ -> None
+  | Lambda (v,t') ->
+      one_step t' >>= fun t'' ->
+      Some (Lambda (v, t''))
+
+let normal_form t =
+  let rec aux acc t = match one_step t with
+    | None -> List.rev (t::acc)
+    | Some t' -> aux (t::acc) t'
+  in
+  aux [] t
+
+let _split_fuel f =
+  assert (f>=2);
+  if f=2 then 1,1
+  else
+    let x = 1+Random.int (f-1) in
+    f-x, x
+
+let _random_var () =
+  let v = [| "x"; "y"; "z"; "u"; "w" |] in
+  v.(Random.int (Array.length v))
+
+let  _choose_var ~vars = match vars with
+  | [] -> Var (_random_var ())
+  | _::_ ->
+      let i = Random.int (List.length vars) in
+      List.nth vars i
+
+let rec _random_term fuel vars =
+  match Random.int 3 with
+  | _ when fuel = 1 -> _choose_var ~vars
+  | 0 -> _choose_var ~vars
+  | 1 ->
+      let f1,f2 = _split_fuel fuel in
+      App (_random_term f1 vars, _random_term f2 vars)
+  | 2 ->
+      let v = _random_var () in
+      Lambda (v, _random_term (fuel-1) (Var v::vars))
+  | _ -> assert false
+
+let print_term t =
+  PrintBox.mk_tree
+    (function
+      | Var v -> PrintBox.line v, []
+      | App (t1,t2) -> PrintBox.line "app", [t1;t2]
+      | Lambda (v,t') -> PrintBox.line "lambda", [Var v; t']
+    ) t
+
+let print_reduction t =
+  let l = normal_form t in
+  let l = List.map (fun t -> PrintBox.pad (print_term t)) l in
+  PrintBox.vlist ~bars:false l
+
+let () =
+  Random.self_init ();
+  let t = _random_term (15 + Random.int 30) [] in
+  PrintBox.output ~indent:2 stdout (print_reduction t)

misc/printBox.ml

@@ -36,6 +36,10 @@ let _minus pos1 pos2 = _move pos1 (- pos2.x) (- pos2.y)
 let _move_x pos x = _move pos x 0
 let _move_y pos y = _move pos 0 y
 
+let _string_len = ref String.length
+
+let set_string_len f = _string_len := f
+
 (** {2 Output: where to print to} *)
 
 module Output = struct
@@ -72,7 +76,7 @@ module Output = struct
     )
 
   let _ensure_line line i =
-    if i >= String.length line.bl_str
+    if i >= !_string_len line.bl_str
     then (
       let str' = String.make (2 * i + 5) ' ' in
       String.blit line.bl_str 0 str' 0 line.bl_len;
@@ -96,7 +100,7 @@ module Output = struct
     line.bl_len <- max line.bl_len (pos.x+s_len)
 
   let _buf_put_string buf pos s =
-    _buf_put_sub_string buf pos s 0 (String.length s)
+    _buf_put_sub_string buf pos s 0 (!_string_len s)
 
   (* create a new buffer *)
   let make_buffer () =
@@ -151,10 +155,12 @@ module Box = struct
     | GridBars
 
   type 'a shape =
+    | Empty
     | Text of string list  (* list of lines *)
     | Frame of 'a
     | Pad of position * 'a (* vertical and horizontal padding *)
     | Grid of grid_shape * 'a array array
+    | Tree of int * 'a * 'a array
 
   type t = {
     shape : t shape;
@@ -193,6 +199,17 @@ module Box = struct
     done;
     !acc
 
+  (* width and height of a column as an array *)
+  let _dim_vertical_array a =
+    let w = ref 0 and h = ref 0 in
+    Array.iter
+      (fun b ->
+        let s = size b in
+        w := max !w s.x;
+        h := !h + s.y
+      ) a;
+    {x= !w; y= !h;} 
+
   (* from a matrix [m] (line,column), return two arrays [lines] and [columns],
     with [col.(i)] being the start offset of column [i] and
     [lines.(j)] being the start offset of line [j].
@@ -218,9 +235,10 @@ module Box = struct
     lines, columns
 
   let _size = function
+    | Empty -> origin
     | Text l ->
         let width = List.fold_left
-          (fun acc line -> max acc (String.length line)) 0 l
+          (fun acc line -> max acc (!_string_len line)) 0 l
         in
         { x=width; y=List.length l; }
     | Frame t ->
@@ -237,11 +255,19 @@ module Box = struct
         let dim = _dim_matrix m in
         let lines, columns = _size_matrix ~bars m in
         { y=lines.(dim.y); x=columns.(dim.x)}
+    | Tree (indent, node, children) ->
+        let dim_children = _dim_vertical_array children in
+        let s = size node in
+        { x=max s.x (dim_children.x+2+indent)
+        ; y=s.y + dim_children.y + (Array.length children-1)
+        }
 
   let _make shape =
     { shape; size=(lazy (_size shape)); }
 end
 
+let empty = Box._make Box.Empty
+
 let line s =
   assert (_find s '\n' 0 = None);
   Box._make (Box.Text [s])
@@ -300,6 +326,29 @@ let transpose m =
   Array.init dim.x
     (fun i -> Array.init dim.y (fun j -> m.(j).(i)))
 
+let tree ?(indent=1) node children =
+  let children =
+    List.filter
+    (function
+      | {Box.shape=Box.Empty} -> false
+      | _ -> true
+    ) children
+  in
+  match children with
+  | [] -> node
+  | _::_ ->
+    let children = Array.of_list children in
+    Box._make (Box.Tree (indent, node, children))
+
+let mk_tree ?indent f root =
+  let rec make x = match f x with
+    | b, [] -> b
+    | b, children -> tree ?indent b (List.map make children)
+  in
+  make root
+
+(** {2 Rendering} *)
+
 let _write_vline ~out pos n =
   for j=0 to n-1 do
     Output.put_char out (_move_y pos j) '|'
@@ -316,6 +365,7 @@ let _write_hline ~out pos n =
     w.r.t the surrounding box *)
 let rec _render ?(offset=origin) ?expected_size ~out b pos =
   match Box.shape b with
+    | Box.Empty -> ()
     | Box.Text l ->
         List.iteri
           (fun i line ->
@@ -376,6 +426,25 @@ let rec _render ?(offset=origin) ?expected_size ~out b pos =
             done
           done
         end
+    | Box.Tree (indent, n, a) ->
+        _render ~out n pos;
+        (* star position for the children *)
+        let pos' = _move pos indent (Box.size n).y in
+        Output.put_char out (_move_x pos' ~-1) '`';
+        assert (Array.length a > 0);
+        let _ = Box._array_foldi
+          (fun pos' i b ->
+            Output.put_string out pos' "+ ";
+            if i<Array.length a-1
+              then (
+                _write_vline ~out (_move_y pos' 1) (Box.size b).y
+              );
+            _render ~out b (_move_x pos' 2);
+            let interline = if i<Array.length a-1 then 1 else 0 in
+            _move_y pos' ((Box.size b).y + interline)
+          ) pos' a
+        in
+        ()
 
 let render out b =
   _render ~out b origin

misc/printBox.mli

@@ -72,6 +72,12 @@ we go toward the bottom (same order as a printer) *)
 val origin : position
 (** Initial position *)
 
+val set_string_len : (string -> int) -> unit
+(** Set which function is used to compute string length. Typically
+    to be used with a unicode-sensitive length function *)
+
+(** {2 Output} *)
+
 module Output : sig
   type t = {
     put_char : position -> char -> unit;
@@ -95,6 +101,8 @@ module Output : sig
   (** Print the buffer on the given channel *)
 end
 
+(** {2 Box Combinators} *)
+
 module Box : sig
   type t
 
@@ -102,6 +110,9 @@ module Box : sig
   (** Size needed to print the box *)
 end
 
+val empty : Box.t
+(** Empty box, of size 0 *)
+
 val line : string -> Box.t
 (** Make a single-line box.
     @raise Invalid_argument if the string contains ['\n'] *)
@@ -164,6 +175,15 @@ val vlist_map : ?bars:bool -> ('a -> Box.t) -> 'a list -> Box.t
 
 val hlist_map : ?bars:bool -> ('a -> Box.t) -> 'a list -> Box.t
 
+val tree : ?indent:int -> Box.t -> Box.t list -> Box.t
+(** Tree structure, with a node label and a list of children nodes *)
+
+val mk_tree : ?indent:int -> ('a -> Box.t * 'a list) -> 'a -> Box.t
+(** Definition of a tree with a local function that maps nodes to
+    their content and children *)
+
+(** {2 Rendering} *)
+
 val render : Output.t -> Box.t -> unit
 
 val to_string : Box.t -> string