go_up when we have tree list in the definition of tree

[Kerl13]

Hand-written source code

type hole = Hole [@@deriving show {with_path = false}]

(** Lists ******************************)

type 'a mylist = Cons of 'a * 'a mylist | Nil

let pp_mylist pp_elt fmt =
  let rec aux fmt = function
    | Nil -> ()
    | Cons (x, Nil) -> Format.fprintf fmt "%a" pp_elt x
    | Cons (x, xs) -> Format.fprintf fmt "%a; %a" pp_elt x aux xs
  in
  Format.fprintf fmt "[%a]" aux

type 'a mylist_ancestors =
  | Cons0 of 'a * hole * 'a mylist_ancestors
  | NoAncestor
[@@deriving show {with_path = false}]

type 'a mylist_poly_zda = Cons0 of hole * 'a mylist
[@@deriving show {with_path = false}]

type 'a mylist_d0 = 'a mylist_poly_zda * 'a mylist_ancestors
[@@deriving show {with_path = false}]

type 'a mylist_zipper = 'a mylist * 'a mylist_ancestors
[@@deriving show {with_path = false}]

(** Trees ******************************)

type tree = Leaf of int | Node of tree * tree mylist
[@@deriving show {with_path = false}]

let pp_tree fmt = function
  | Node (Leaf x, Cons (Leaf y, Nil)) when x land 1 = 0 && y = x + 1 ->
    Format.fprintf fmt "cherry %d" (x lsr 1)
  | tree -> pp_tree fmt tree

type tree_ancestors =
  | Node0 of hole * tree mylist * tree_ancestors
  | Node1 of tree * (tree mylist_d0 * hole) * tree_ancestors
  | NoAncestor
[@@deriving show {with_path = false}]

type tree_zipper = tree * tree_ancestors
[@@deriving show {with_path = false}]

let go_up_tree (zipper : tree_zipper) : tree_zipper option =
  let pending, ancestors = zipper in
  match ancestors with
  | NoAncestor -> None
  | Node0 (Hole, trees, ancestors) -> Some (Node (pending, trees), ancestors)
  | Node1 (tree, (something, Hole), ancestors) -> (
    let Cons0 (Hole, trees), mylist_ancestors = something in
    match mylist_ancestors with
    | NoAncestor ->
      let trees = Cons (pending, trees) in
      Some (Node (tree, trees), ancestors)
    | Cons0 (new_pending, Hole, mylist_ancestors) ->
      let new_something =
        (Cons0 (Hole, Cons (pending, trees)), mylist_ancestors)
      in
      Some (new_pending, Node1 (tree, (new_something, Hole), ancestors)) )

let () =
  let cherry n = Node (Leaf (n lsl 1), Cons (Leaf (1 lor (n lsl 1)), Nil)) in
  let ( // ) x xs = Cons (x, xs) in
  let example : tree_zipper =
    let ancestors = NoAncestor in
    let something : _ mylist_d0 =
      ( Cons0 (Hole, cherry 4 // Nil),
        Cons0 (cherry 2, Hole, Cons0 (cherry 1, Hole, NoAncestor)) )
    in
    (cherry 3, Node1 (cherry 0, (something, Hole), ancestors))
  in
  Format.printf "let before = %a\n" pp_tree_zipper example;
  Format.printf "let after = %a@."
    pp_tree_zipper
    (go_up_tree example |> Option.get);
  ()

Output

let before =
  ( cherry 3,
    Node1
      ( cherry 0,
        ( ( Cons0 (Hole, [cherry 4]),
            Cons0 (cherry 2, Hole, Cons0 (cherry 1, Hole, NoAncestor)) ),
          Hole ),
        NoAncestor ) )

let after =
  ( cherry 2,
    Node1
      ( cherry 0,
        ( ( Cons0 (Hole, [cherry 3; cherry 4]),
            Cons0 (cherry 1, Hole, NoAncestor) ),
          Hole ),
        NoAncestor ) )

[Niols]

On a white board: