+let mk_ptr st name =
+ if G.is_global_id name then P.sprintf "%s.%s" st.i name else ""
+
+let get_macro s =
+ let rec aux = function
+ | [] -> "", G.nan
+ | (r, m, a) :: _ when r = s -> m, a
+ | _ :: tl -> aux tl
+ in
+ aux !G.macro
+
+let get_head = function
+ | C.Const c :: ts ->
+ let s, _ = K.resolve_reference c in
+ let macro, arity = get_macro s in
+ if arity = L.length ts then Some (macro, ts) else begin missing s; None end
+ | _ -> None
+
+let proc_sort st is = function