+
+
+let max_arity_tms n =
+ let max a b = match a, b with
+ | None, None -> None
+ | None, Some x
+ | Some x, None -> Some x
+ | Some x, Some y -> Some (Pervasives.max x y) in
+ let aux_var l (m,a) = if n + l = m then Some a else None in
+ let rec aux l = function
+ | `Var v -> aux_var l v
+ | `I(v,tms) -> max (aux_var l v) (aux_tms l (Listx.to_list tms))
+ | `Lam(_,t, g) -> List.fold_left (fun n t -> max n (aux (l+1) t)) None (t::g)
+ | `Match(u,_,_,bs,args) -> max (max (aux l (u :> nf)) (aux_tms l args)) (aux_tms l (List.map snd !bs))
+ | `N _ -> None
+ and aux_tms l =
+ List.fold_left (fun acc t -> max acc (aux l t)) None in
+ fun tms -> aux_tms 0 (tms :> nf list)
+;;
+
+let get_first_args var =
+let rec aux l = function
+| `Lam(_,t,_) -> aux (l+1) t
+| `Match(u,orig,liftno,bs,args) -> Util.concat_map (aux l) args
+| `I((n,_), args) -> if n = var + l then [Listx.last args] else []
+| `N _
+| `Var _ -> []
+in aux 0
+;;
+
+let compute_arities m =
+ let rec aux n tms =
+ if n = 0
+ then []
+ else
+ let tms = Util.filter_map (function `Lam(_,t,_) -> Some t | _ -> None ) tms in
+ let arity = match max_arity_tms (m-n) tms with None -> -666 | Some x -> x in
+ arity :: (aux (n-1) tms)
+ in fun tms -> List.rev (aux m tms)
+;;
+
+let compute_arities var special_k all_tms =
+ let tms = List.fold_left (fun acc t -> acc @ (get_first_args var t)) [] all_tms in
+ compute_arities special_k tms
+;;