180 lines
4.5 KiB
OCaml
180 lines
4.5 KiB
OCaml
type t =
|
|
| Var of Id.t
|
|
| Lit of int
|
|
| Add of t * t
|
|
| Let of t * bound1
|
|
| Hole of t Id.subst
|
|
|
|
and bound1 = B of Id.t * t
|
|
|
|
let rec pp ff = function
|
|
| Var x ->
|
|
Id.pp ff x
|
|
| Lit n ->
|
|
Format.fprintf ff "%d" n
|
|
| Add (e1, e2) ->
|
|
Format.fprintf ff "add(@[@[%a@],@ @[%a@]@])"
|
|
pp e1
|
|
pp e2
|
|
| Let (e1, e2) ->
|
|
Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
|
|
pp e1
|
|
pp_bound1 e2
|
|
| Hole s ->
|
|
Format.fprintf ff "[]{@[%a@]}"
|
|
pp_substitution s
|
|
|
|
and pp_bound1 ff (B (x, e)) =
|
|
Format.fprintf ff "@[%a.@,@[%a@]@]"
|
|
Id.pp x
|
|
pp e
|
|
|
|
and pp_substitution ff xs =
|
|
Fmt.list ~sep:Fmt.comma
|
|
(fun ff (x, e) ->
|
|
Format.fprintf ff "%a\\@[%a@]" Id.pp x pp e)
|
|
ff xs
|
|
|
|
module Builder = struct
|
|
let v x = Var x
|
|
let l i = Lit i
|
|
let ( + ) e1 e2 = Add (e1, e2)
|
|
let ( let* ) e1 mk_e2 = let x = Id.fresh () in Let (e1, B (x, mk_e2 (Var x)))
|
|
let h = Hole []
|
|
end
|
|
|
|
let rec subst s = function
|
|
| Var x ->
|
|
begin try Id.assoc x s with Not_found -> Var x end
|
|
| Lit k ->
|
|
Lit k
|
|
| Add (e1, e2) ->
|
|
Add (subst s e1, subst s e2)
|
|
| Let (e1, e2) ->
|
|
Let (subst s e1, subst_bound1 s e2)
|
|
| Hole s' ->
|
|
Hole (compose s' s)
|
|
|
|
and subst_bound1 s (B (x, e)) =
|
|
let x' = Id.fresh () in
|
|
B (x', subst (Id.extend x (Var x') s) e)
|
|
|
|
and compose s1 s2 =
|
|
match s1 with
|
|
| [] -> s2
|
|
| (x, t) :: s1 -> (x, subst s2 t) :: compose s1 s2
|
|
|
|
let rec equal e e' =
|
|
match e, e' with
|
|
| Var x, Var x' ->
|
|
x = x'
|
|
| Lit i, Lit i' ->
|
|
i = i'
|
|
| Add (e1, e2), Add (e1', e2') ->
|
|
equal e1 e1' && equal e2 e2'
|
|
| Let (e1, e2), Let (e1', e2') ->
|
|
equal e1 e1' && equal_bound1 e2 e2'
|
|
| Hole sub1, Hole sub2 ->
|
|
equal_subst sub1 sub2
|
|
| _ ->
|
|
false
|
|
|
|
and equal_bound1 (B (x, e)) (B (x', e')) =
|
|
let y = Id.fresh () in
|
|
equal
|
|
(subst Id.(singleton x (Var y)) e)
|
|
(subst Id.(singleton x' (Var y)) e')
|
|
|
|
and equal_subst sub1 sub2 = Id.equal_subst equal sub1 sub2
|
|
|
|
let%expect_test "e1" =
|
|
Id.reset ();
|
|
let print e1 e2 =
|
|
Format.printf "@[@[%a@]@ = @[%a@]: %b@]@."
|
|
pp e1
|
|
pp e2
|
|
(equal e1 e2)
|
|
in
|
|
let open Builder in
|
|
print (let* x = l 1 in x) (let* y = l 1 in y);
|
|
[%expect {| let(1, _x2._x2) = let(1, _x1._x1): true |}];
|
|
print (let* x = l 1 in x) (let* y = l 2 in y);
|
|
[%expect {| let(1, _x5._x5) = let(2, _x4._x4): false |}];
|
|
print
|
|
(let* x = l 1 in let* k = l 2 in x + k)
|
|
(let* y = l 1 in let* k = l 2 in y + k);
|
|
[%expect {|
|
|
let(1, _x8.let(2, _x9.add(_x8, _x9)))
|
|
= let(1, _x6.let(2, _x7.add(_x6, _x7))): true |}];
|
|
print
|
|
(let* x = l 1 in let* k = l 2 in x + k)
|
|
(let* y = l 1 in let* k = l 2 in k + y);
|
|
[%expect {|
|
|
let(1, _x16.let(2, _x17.add(_x16, _x17)))
|
|
= let(1, _x14.let(2, _x15.add(_x15, _x14))): false |}];;
|
|
|
|
let close_with (B (x, e)) e' = subst Id.(singleton x e') e
|
|
|
|
let rec plug k e =
|
|
match k with
|
|
| (Var _ | Lit _) as k -> k
|
|
| Add (k1, k2) -> Add (plug k1 e, plug k2 e)
|
|
| Let (k1, k2) -> Let (plug k1 e, plug_bound1 k2 e)
|
|
| Hole s -> subst s e
|
|
|
|
and plug_bound1 (B (x, k)) e = B (x, plug k e)
|
|
|
|
let beta0 : t -> t option
|
|
= function
|
|
| Add (Lit k1, Lit k2) ->
|
|
Some (Lit (k1 + k2))
|
|
| Let (e1, e2) ->
|
|
Some (close_with e2 e1)
|
|
| _ ->
|
|
None
|
|
|
|
let wrap f (k, e) = (f k, e)
|
|
|
|
let rec decompose t =
|
|
Seq.cons (Hole [], t) (decompose_subterms t)
|
|
|
|
and decompose_subterms = function
|
|
| Var _ | Lit _ | Hole _ ->
|
|
Seq.empty
|
|
| Add (e1, e2) ->
|
|
Seq.interleave
|
|
(decompose e1 |> Seq.map (wrap (fun k -> Add (k, e2))))
|
|
(decompose e2 |> Seq.map (wrap (fun k -> Add (e1, k))))
|
|
| Let (e1, B (x, e2)) ->
|
|
Seq.interleave
|
|
(decompose e1 |> Seq.map (wrap (fun k -> Let (k, B (x, e2)))))
|
|
(decompose e2 |> Seq.map (wrap (fun k -> Let (e1, B (x, k)))))
|
|
|
|
let rewrite e =
|
|
decompose e
|
|
|> Seq.filter_map (fun (k, e) -> beta0 e |> Option.map (fun e -> (k, e)))
|
|
|> Seq.map (fun (k, e) -> plug k e)
|
|
|
|
(* Test fixtures *)
|
|
|
|
let e1, e2, e3, e4 =
|
|
Id.reset ();
|
|
let open Builder in
|
|
(l 1 + l 1),
|
|
(let* x = l 1 + l 1 in x),
|
|
(let* x = l 1 + l 1 in l 40 + x),
|
|
(let* x = l 1 + l 1 in let* y = x + l 1 in let* x = l 3 in x + y)
|
|
|
|
let%expect_test "rew0" =
|
|
Id.reset ();
|
|
let e = Builder.(let* x = l 1 + l 1 in l 28 + l 12 + x) in
|
|
Format.printf "%a@." pp e;
|
|
[%expect {| let(add(1, 1), _x1.add(add(28, 12), _x1)) |}];
|
|
Format.printf "@[@[%a@]@ -> @[<hv 2>%a@]@]@."
|
|
pp e
|
|
Fmt.(list ~sep:comma pp) (rewrite e |> List.of_seq);
|
|
[%expect {|
|
|
let(add(1, 1), _x1.add(add(28, 12), _x1))
|
|
-> add(add(28, 12), add(1, 1)),
|
|
let(2, _x1.add(add(28, 12), _x1)),
|
|
let(add(1, 1), _x1.add(40, _x1)) |}]
|