-let proc_sort = function
- | C.Prop -> [T.Macro "PROP"]
- | C.Type [`Type, u] -> [T.Macro "TYPE"; T.arg (U.string_of_uri u)]
- | C.Type [`CProp, u] -> [T.Macro "CROP"; T.arg (U.string_of_uri u)]
+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
+ | C.Prop -> T.Macro "PROP" :: is
+ | C.Type [`Type, u] -> T.Macro "TYPE" :: T.arg (U.string_of_uri u) :: is
+ | C.Type [`CProp, u] -> T.Macro "CROP" :: T.arg (U.string_of_uri u) :: is