diff --git a/examples/dune b/examples/dune index 1cdf32ab..53b04e82 100644 --- a/examples/dune +++ b/examples/dune @@ -7,9 +7,3 @@ (ocamlopt_flags :standard -O3 -color always -unbox-closures -unbox-closures-factor 20) ) - -(executable - (name lambda) - (libraries printbox) - (modules lambda) - ) diff --git a/examples/lambda.ml b/examples/lambda.ml deleted file mode 100644 index 03fd6bfe..00000000 --- a/examples/lambda.ml +++ /dev/null @@ -1,112 +0,0 @@ - -(** Example of printing trees: lambda-term evaluation *) - - -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 2 with - | _ when fuel = 1 -> _choose_var ~vars - | 0 -> - let f1,f2 = _split_fuel fuel in - App (_random_term f1 vars, _random_term f2 vars) - | 1 -> - 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 (5 + Random.int 20) [] in - PrintBox_text.output ~indent:2 stdout (print_reduction t)