difftree.ml

(* #require "containers";; *)
(* open Containers;; *)

type expr =
  | Hole
  | One
  | Plus of expr * expr

type t = int * (expr list -> expr)

(* Plus (One, __) *)
let example = (1, fun [e] -> Plus (One, e))

let sub ts (i, t) =
  assert (List.length ts = i);
  let f r =
    let _rem, ts1 =
      List.fold_right
        (fun (i, ct) (tr, t) ->
          let used, rem = List.take_drop i tr in
          (rem, ct used :: t))
        ts (r, [])
    in
    t ts1
  in
  let sum_ts = List.fold_right (fun (i, _) t -> i + t) ts 0 in
  (sum_ts, f)

let concretize ((i, t) : t) : expr = t (List.init i (fun _ -> Hole))
let a = (1, fun [e] -> Plus (e, One))
let b = (1, fun [e] -> Plus (One, e))
let c = (2, fun [e1; e2] -> Plus (e1, e2))
let c' = concretize (sub [a; b] c)

let sub dts (i, t) =
  assert (List.length dts <= i);
  let dts_arities = List.fold_right (fun (i, _) t -> i + t) dts 0 in
  let remaining = i - List.length dts in
  let f r =
    assert (List.length r <= dts_arities + remaining);
    let rem_trees, r = List.take_drop remaining r in
    let _rem, child_trees =
      List.fold_right
        (fun (i, ct) (tr, t) ->
          let used, rem = List.take_drop i tr in
          (rem, ct used :: t))
        dts (r, [])
    in
    t (child_trees @ rem_trees)
  in
  (dts_arities + remaining, f)

let a = (1, fun [e] -> Plus (e, One))
let b = (1, fun [e] -> Plus (One, e))
let c = (2, fun [e1; e2] -> Plus (e1, e2))
let c' = concretize (sub [b] (sub [a] c))

type z = Z
type 'a s = S of 'a

type _ holes =
  | S : 'a holes -> (expr -> 'a) holes
  | Z : expr holes

type 'a t = 'a holes * 'a

let a : (expr -> expr) t = (S Z, fun e -> Plus (e, One))
let b : (expr -> expr) t = (S Z, fun e -> Plus (One, e))
let c : (expr -> expr -> expr) t = (S (S Z), fun e1 e2 -> Plus (e1, e2))

let rec count_holes : type a. a holes -> int =
 fun h -> match h with Z -> 0 | S h -> count_holes h

let rec concretize : type a. a t -> expr =
 fun (i, t) -> match i with S i -> concretize (i, t Hole) | Z -> t

let c' = concretize c