Skip to content

Commit

Permalink
format
Browse files Browse the repository at this point in the history
  • Loading branch information
c-cube committed Jan 29, 2024
1 parent 7a4baa3 commit ff06355
Show file tree
Hide file tree
Showing 18 changed files with 1,589 additions and 1,041 deletions.
15 changes: 15 additions & 0 deletions .ocamlformat
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
version = 0.24.1
profile=conventional
margin=80
if-then-else=k-r
parens-ite=true
parens-tuple=multi-line-only
sequence-style=terminator
type-decl=sparse
break-cases=toplevel
cases-exp-indent=2
field-space=tight-decl
leading-nested-match-parens=true
module-item-spacing=compact
quiet=true
ocaml-version=4.08.0
1 change: 0 additions & 1 deletion dune
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@

(mdx
(package printbox-html)
(libraries printbox printbox-text printbox-html)
Expand Down
101 changes: 53 additions & 48 deletions examples/lambda.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@

(** Example of printing trees: lambda-term evaluation *)


type term =
| Lambda of string * term
| App of term * term
Expand All @@ -14,92 +12,99 @@ let _gensym =
incr r;
s

module SSet = Set.Make(String)
module SMap = Map.Make(String)
module SSet = Set.Make (String)
module SMap = Map.Make (String)

let rec fvars t = match t with
let rec fvars t =
match t with
| Var s -> SSet.singleton s
| Lambda (v,t') ->
let set' = fvars t' in
SSet.remove v set'
| 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 *)
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
if SSet.mem var (fvars t) then
replace t ~var ~by:(Var (_gensym ()))
else
t

let (>>=) o f = match o with
let ( >>= ) o f =
match o with
| None -> None
| Some x -> f x

let rec one_step t = match t with
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')
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
(match one_step t1 with
| None -> one_step t2 >>= fun t2' -> Some (App (t1, t2'))
| Some t1' -> Some (App (t1', t2)))
| Var _ -> None
| Lambda (v,t') ->
one_step t' >>= fun t'' ->
Some (Lambda (v, t''))
| 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'
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
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
let _choose_var ~vars =
match vars with
| [] -> Var (_random_var ())
| _::_ ->
let i = Random.int (List.length vars) in
List.nth vars i
| _ :: _ ->
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)
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))
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
| 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
Expand Down
Loading

0 comments on commit ff06355

Please sign in to comment.