commit 44b8c21

make dot printing not be quadratic and use a shared helper with template

1@@ -18,6 +18,6 @@ main.o graph.o: graph.sats types.sats
2 
3 .PHONY: clean
4 clean:  
5-	rm monk
6+	rm -f monk
7 	rm -f *.c
8 	rm -f $(OBJ)

 1@@ -190,17 +190,6 @@ implement mkedges(g, edges) =
 2         mkedge (g, edge);
 3         mkedges(g, rest) )
 4 
 5-fun dotnodes(g: &graph, i: usize): void = 
 6-    if i < dynarray_get_size(g.nodes) then
 7-        let
 8-            val n  = dynarray_takeout_at_exn<node>(g.nodes, i)
 9-            val () = println!("  n", i, " [shape=box, label=\"", n.path, "\"];")
10-            val () = dynarray_insert_at_exn<node>(g.nodes, i, n)
11-        in
12-            dotnodes(g, i + i2sz(1))
13-        end
14-    else ()
15-
16 fun inputarrows(nodes: !List0_vt(node_id), aid: action_id): void = 
17     case+ nodes of 
18     | nil_vt() => ()
19@@ -217,23 +206,45 @@ fun outputarrows(nodes: !List0_vt(node_id), aid: action_id): void =
20         outputarrows(rest, aid);
21         fold@(nodes) )
22 
23-fun dotactions(g: &graph, i: usize): void = 
24-    if i < dynarray_get_size(g.actions) then
25-        let 
26-            val a  = dynarray_takeout_at_exn<action>(g.actions, i)
27-            val () = println!("  a", i, "[shape=ellipse, label=\"", a.rule, "\"];");
28-            val () = inputarrows (a.inp, i)
29-            val () = outputarrows(a.out, i)
30-            val () = dynarray_insert_at_exn<action>(g.actions, i, a)
31-        in
32-            dotactions(g, i + i2sz(1))
33+fun dotnode(n: &node, i: usize): void = 
34+    println!("  n", i, " [shape=box, label=\"", n.path, "\"];")
35+
36+fun dotaction(a: &action, i: usize): void = (
37+    println!("  a", i, "[shape=ellipse, label=\"", a.rule, "\"];");
38+    inputarrows (a.inp, i);
39+    outputarrows(a.out, i))
40+
41+(*take a template type (either action or node is intended.) 
42+ * then a dynarray of that type. then a index that we increment,
43+ * and finally a function that returns void (which will be dotaction or dotnode depending on type *)
44+fun{a:vt0p} visitarray(items: !dynarray(a), i: usize, visit: (&a, usize) -<fun1> void): void =
45+        let
46+            var len: usize
47+            val (pf, putback | p)  = dynarray_get_array(items, len)
48+            val idx = g1ofg0_uint(i)
49+        in 
50+            if idx < len then
51+                let 
52+                    val (pfnode, restore | pn) = array_ptr_takeout<a>(pf | p, idx)
53+                    (* check that the proof belongs to the pointer and hive them a shared address...*)
54+                    val (pfnode | pn) = viewptr_match(pfnode | pn) 
55+                    (*... so we can borrow it here and !pn can find pfnode*)
56+                    val   () = visit(!pn, i)
57+                    prval pf = restore(pfnode)
58+                    prval () = putback(pf)
59+                in 
60+                    visitarray<a>(items, i + i2sz(1), visit) 
61+                end
62+            else
63+                let prval () = putback(pf)
64+                in () 
65+                end
66         end
67-     else()
68 
69 implement dot(g) = (
70     println!("digraph build {");
71     println!("  rankdir=LR;");
72-    dotnodes(g, i2sz(0));
73-    dotactions(g, i2sz(0));
74+    visitarray<node>  (g.nodes,   i2sz(0), dotnode  );
75+    visitarray<action>(g.actions, i2sz(0), dotaction);
76     println!("}") )
77