Finished proposal?

[fireball-separation.git] / ocaml / num.ml

diff --git a/ocaml/num.ml b/ocaml/num.ml
index 6f3cae56c327c103eeb42c127bc626cbd28aa3eb..01787b02d1da3055087ae46bcf1c06cad70ea0e3 100644 (file)
--- a/ocaml/num.ml
+++ b/ocaml/num.ml
@@ -138,7 +138,6 @@ let rec string_of_term l =
 ;;
 
 let print ?(l=[]) = string_of_term l;;
-let string_of_nf t = string_of_term [] (t:>nf);;
 
 (************ Hereditary substitutions ************************************)
 
@@ -292,3 +291,14 @@ let rec eta_subterm sub t =
 ;;
 
 let eta_subterm (#nf as x) (#nf as y) = eta_subterm x y;;
+
+let compute_special_k tms =
+  let rec aux k (t: nf) = Pervasives.max k (match t with
+    | `Lam(b,t) -> aux (k + if b then 1 else 0) t
+    | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
+    | `Match(t, liftno, bs, args) ->
+        List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
+    | `N _ -> 0
+    | `Var _ -> 0
+  ) in Listx.max (Listx.map (aux 0) tms)
+;;