-
-let string_of_sort = function
- | true -> "Type"
- | false -> "Prop"
-
-let pp_transparent frm a =
- let err () = F.fprintf frm "%s" "=" in
- let f () = F.fprintf frm "%s" "~" in
- E.priv err f a
-
-let pp_list pp opend sep closed frm l =
- let rec aux frm = function
- | [] -> ()
- | [hd] -> pp frm hd
- | hd :: tl -> F.fprintf frm "%a%s%a" pp hd sep aux tl
- in
- if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
-
-let pp_rev_list pp opend sep closed frm l =
- pp_list pp opend sep closed frm (List.rev l)
-
-let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
-
-and pp_term frm = function
- | M.Sort s ->
- F.fprintf frm "@[*%s@]" (string_of_sort s)
- | M.LRef (l, i) ->
- F.fprintf frm "@[%u@@#%u@]" l i
- | M.GRef (l, uri, ts) ->
- F.fprintf frm "@[%u@@$%s%a@]" l (U.string_of_uri uri) pp_args ts
- | M.Appl (v, t) ->
- F.fprintf frm "@[(%a).%a@]" pp_term v pp_term t
- | M.Abst (id, w, t) ->
- F.fprintf frm "@[[%s:%a].%a@]" id pp_term w pp_term t
-
-let pp_par frm (id, w) =
- F.fprintf frm "%s:%a" id pp_term w
-
-let pp_pars = pp_rev_list pp_par "[" "," "]"
-
-let pp_body a frm = function
- | None -> ()
- | Some t -> F.fprintf frm "%a%a" pp_transparent a pp_term t
-
-let pp_entity frm = function
- | a, uri, E.Abst (pars, u, body)
- | a, uri, E.Abbr (pars, u, body) ->
- F.fprintf frm "@[%u@@%s%a%a:%a@]@\n%!"
- (E.mark C.err C.start a) (U.string_of_uri uri)
- pp_pars pars (pp_body a) body pp_term u
- | _, _, E.Void -> assert false
-
-let pp_entity f frm entity =
- pp_entity frm entity; f ()