ugly but useful printing of sharing for bool refs

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index f61ce5e3a22608ea55a81a8f5c169a44238d9aa2..2cbb448a956a9da8d7506ed57c6019c41fdb3979 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -24,6 +24,29 @@ let measure_of_t =
  in snd ++ (aux [])\r
 ;;\r
 \r
+let index_of x =\r
+ let rec aux n =\r
+  function\r
+    [] -> None\r
+  | x'::_ when x == x' -> Some n\r
+  | _::xs -> aux (n+1) xs\r
+ in aux 1\r
+;;\r
+\r
+let sep_of_app =\r
+ let apps = ref [] in\r
+ function\r
+    r when not !r -> " "\r
+  | r ->\r
+    let i =\r
+     match index_of r !apps with\r
+        Some i -> i\r
+      | None ->\r
+         apps := !apps @ [r];\r
+         List.length !apps\r
+    in "," ^ string_of_int i ^ " "\r
+;;\r
+\r
 let string_of_t =\r
   let string_of_bvar =\r
    let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
@@ -35,7 +58,7 @@ let string_of_t =
     | A _\r
     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
   and string_of_term_no_pars_app level = function\r
-    | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ (if !b then "," else " ") ^ string_of_term_w_pars level t2\r
+    | A(b,t1,t2) -> string_of_term_no_pars_app level t1 ^ sep_of_app b ^ string_of_term_w_pars level t2\r
     | _ as t -> string_of_term_w_pars level t\r
   and string_of_term_no_pars level = function\r
     | L(_,t) -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r