-let free_vars p t =\r
- let rec aux level = function\r
- | V v -> if v >= level then [v] else []\r
- | A(t1,t2) -> (aux level t1) @ (aux level t2)\r
- | L t -> aux (level+1) t\r
- | B | P -> []\r
- in Util.sort_uniq (aux 0 t)\r
-;;\r
-\r
-let visible_vars p t =\r
- let rec aux = function\r
- | V v -> [v]\r
- | A(t1,t2) -> (aux t1) @ (aux t2)\r
- | B | P\r
- | L _ -> []\r
- (* | Ptr n -> aux (get_conv p n) *)\r
- in Util.sort_uniq (aux t)\r
-;;\r
-\r
-let rec hd_of = function\r
- | V n -> n\r
- | A(t, _) -> hd_of t\r
- | _ -> assert false\r
-;;\r
-\r
-let rec nargs = function\r
- | V _ -> 0\r
- | A(t, _) -> 1 + nargs t\r
- | _ -> assert false\r
-;;\r
-\r