From 373e4e85022838c3bc4bc015444dbc0e5828e346 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 16 Jun 2014 20:54:29 +0200 Subject: [PATCH] example: lambda, that print reduction of random lambda-terms using PrintBox --- _oasis | 7 +++ examples/lambda.ml | 114 +++++++++++++++++++++++++++++++++++++++++++++ misc/printBox.ml | 75 +++++++++++++++++++++++++++-- misc/printBox.mli | 20 ++++++++ 4 files changed, 213 insertions(+), 3 deletions(-) create mode 100644 examples/lambda.ml diff --git a/_oasis b/_oasis index 1c953ae7..e4567f67 100644 --- a/_oasis +++ b/_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 diff --git a/examples/lambda.ml b/examples/lambda.ml new file mode 100644 index 00000000..2111cb86 --- /dev/null +++ b/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) diff --git a/misc/printBox.ml b/misc/printBox.ml index 8983894a..fdaf5547 100644 --- a/misc/printBox.ml +++ b/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 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