X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;fp=ocaml%2Fsimple.ml;h=2cbb448a956a9da8d7506ed57c6019c41fdb3979;hb=3af742bc49d1fbdf6c2c044abde8ec8a8b081654;hp=f61ce5e3a22608ea55a81a8f5c169a44238d9aa2;hpb=bc7b3bd553626969b2c22a5ec3e431f67fcd2ff1;p=fireball-separation.git

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