+let rec rename s = function
+ | [] -> s
+ | (s1, s2) :: _ when s1 = s -> s2
+ | _ :: tl -> rename s tl
+
+let mk_lname s = s
+
+let mk_gname s =
+ rename s !G.alpha_gref
+
+let mk_ptr st name =
+ if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
+
+let get_macro s l =
+ let rec aux = function
+ | [] ->
+ if !G.log_missing then missing s l;
+ "", 0
+ | (r, m, a, x) :: _ when r = s && a = l -> m, x
+ | _ :: tl -> aux tl
+ in
+ aux !G.macro_gref
+
+let get_head = function
+ | C.Const c :: ts ->
+ let s, _ = K.resolve_reference c in
+ let l = L.length ts in
+ let macro, x = get_macro s l in
+ begin match macro with
+ | ""
+ | "APPL" -> None
+ | _ ->
+ let ts1, ts2 = X.split_at x ts in
+ Some (macro, s, ts1, ts2)
+ end
+ | _ -> None
+
+let proc_sort st is = function