matita/matita/contribs/lambdadelta/bin/roles/rolesOutput.ml

   1 (*
   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.
   5     ||I||
   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_______________________________________________________________ *)
  11
  12 module ET = RolesTypes
  13 module EU = RolesUtils
  14
  15 let indent n =
  16   String.make (2*n) ' '
  17
  18 let out_tag i tag h map och l =
  19   let aux och = List.iter (map (succ i) och) l in
  20   if h then Printf.fprintf och "%s(%s%t)\n" (indent i) tag aux
  21   else Printf.fprintf och "%s(%s\n%t%s)\n" (indent i) tag aux (indent i)
  22
  23 let string_map f _i och x =
  24   Printf.fprintf och " %S" (f x)
  25
  26 let out_version i och v =
  27   out_tag i "ver" true (string_map EU.string_of_version) och [v]
  28
  29 let out_old i och os =
  30   let map (_,o) = EU.string_of_obj o in
  31   out_tag i "old" true (string_map map) och os
  32
  33 let out_new i och ns =
  34   let map (_,n) = EU.string_of_name n in
  35   out_tag i "new" true (string_map map) och ns
  36
  37 let out_role i och (_,r) =
  38   let map i och r =
  39     out_version i och r.ET.v;
  40     out_old i och r.ET.o;
  41     out_new i och r.ET.n
  42   in
  43   out_tag i "rel" false map och [r]
  44
  45 let out_roles i och rs =
  46   out_tag i "base" false out_role och rs
  47
  48 let out_status och st =
  49   let map i och st =
  50     out_roles i och st.ET.r;
  51     out_version i och st.ET.s;
  52     out_old i och st.ET.t;
  53     out_new i och st.ET.w
  54   in
  55   output_string och "roles:";
  56   out_tag 0 "top" false map och [st]