profound/traversal.ml at master · direct-manipulation/profound · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
(*
 * Author: Kaustuv Chaudhuri <kaustuv.chaudhuri@inria.fr>
 * Copyright (C) 2013  Inria (Institut National de Recherche
 *                     en Informatique et en Automatique)
 * See LICENSE for licensing details.
 *)

open Batteries
open Log

open Syntax

type traversal_error =
  | At_leaf
  | At_top
  | At_edge
  | No_such_child of int

exception Traversal_failure of traversal_error
let travfail err = raise (Traversal_failure err)
let explain = function
  | At_leaf -> "cannot descend further"
  | At_top -> "cannot ascend further"
  | At_edge -> "no siblings in that direction"
  | No_such_child n ->
      Printf.sprintf "could not descend to child #%d -- THIS IS A BUG (please report)" (n + 1)

let rec split3_ err n ls rs =
  begin match rs with
  | [] -> travfail err
  | x :: rs ->
      if n = 0 then (ls, x, rs)
      else split3_ err (n - 1) (x :: ls) rs
  end

let split3 n xs =
  split3_ (No_such_child n) n [] xs

let go_down n f =
  let (fcx, f) = unsubst f in
  let (fr, f) =
    begin match f with
    | Mark _
    | Atom _ ->
        travfail At_leaf
    | Conn (c, fs) ->
        let (lfs, f, rfs) = split3 n fs in
        assert (fs = List.rev_append lfs (f :: rfs)) ;
        let fr = {
          conn = c ;
          left = lfs ;
          right = rfs ;
        } in
        (fr, f)
    | Subst _ -> assert false
    end in
  let fcx = Fcx.snoc fcx fr in
  subst fcx f

let go_up f =
  let (fcx, f) = unsubst f in
  begin match Fcx.rear fcx with
  | Some (fcx, fr) ->
      subst fcx (unframe fr f)
  | None -> travfail At_top
  end

let rec go_top f =
  begin match f with
  | Subst _ -> go_top (go_up f)
  | _ -> f
  end

let go_left f =
  let (fcx, f) = unsubst f in
  begin match Fcx.rear fcx with
  | Some (fcx, fr) ->
      begin match fr.left with
      | lf :: lfs ->
          let fr = { fr with
                     left = lfs ;
                     right = f :: fr.right ;
                   } in
          let fcx = Fcx.snoc fcx fr in
          subst fcx lf
      | [] -> travfail At_edge
      end
  | None -> travfail At_edge
  end

let go_right f =
  let (fcx, f) = unsubst f in
  begin match Fcx.rear fcx with
  | Some (fcx, fr) ->
      begin match fr.right with
      | rf :: rfs ->
          let fr = { fr with
                     right = rfs ;
                     left = f :: fr.left ;
                   } in
          let fcx = Fcx.snoc fcx fr in
          subst fcx rf
      | [] -> travfail At_edge
      end
  | None -> travfail At_edge
  end

type trail = int list

let rec descend (tr : trail) f =
  begin match tr with
  | [] -> f
  | cr :: tr ->
      let f = go_down cr f in
      descend tr f
  end

let rec cleanup f =
  begin match head1 f with
  | Atom _ as f -> f
  | Mark (_, f) -> cleanup f
  | Conn (c, fs) ->
      let fs = List.map cleanup fs in
      conn c fs
  | Subst _ -> assert false
  end