2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
19 (****************************************************************************)
23 | E.Name (s, true) -> out (P.sprintf "%s;" s)
24 | E.Name (s, false) -> out (P.sprintf "~%s;" s)
25 | E.Apix i -> out (P.sprintf "+%i;" i)
26 | E.Mark i -> out (P.sprintf "@%i;" i)
27 | E.Meta s -> out (P.sprintf "\"%s\";" s)
28 | E.Priv -> out (P.sprintf "%s;" "~")
32 let rec pp_term out = function
33 | D.TSort (a, l) -> pp_attrs out a; out (P.sprintf "*%u" l)
34 | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
35 | D.TGRef (a, u) -> pp_attrs out a; out (P.sprintf "$")
36 | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
37 | D.TProj (a, x, y) -> assert false
38 | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
39 | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
41 and pp_terms bg eg out vs =
42 let rec aux = function
44 | [v] -> pp_term out v
45 | v :: vs -> pp_term out v; out ", "; aux vs
47 out bg; aux vs; out (eg ^ ".")
49 and pp_bind out = function
50 | D.Abst x -> pp_terms "[:" "]" out x
51 | D.Abbr x -> pp_terms "[=" "]" out x
52 | D.Void x -> out (P.sprintf "[%u]" x)
54 let rec pp_lenv out = function
56 | D.EProj (x, a, y) -> assert false
57 | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
59 (****************************************************************************)