helm/software/lambda-delta/complete_rg/crgOutput.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 P = Printf
  13 module U = NUri
  14 module C = Cps
  15 module H = Hierarchy
  16 module Y = Entity
  17 module X = Library
  18 module D = Crg
  19
  20 (****************************************************************************)
  21
  22 let pp_attrs out a =
  23    let map = function
  24       | Y.Name (s, true)  -> out (P.sprintf "%s;" s)
  25       | Y.Name (s, false) -> out (P.sprintf "~%s;" s)
  26       | Y.Apix i          -> out (P.sprintf "+%i;" i)
  27       | Y.Mark i          -> out (P.sprintf "@%i;" i)
  28       | Y.Meta s          -> out (P.sprintf "\"%s\";" s)
  29       | Y.Priv            -> out (P.sprintf "%s;" "~")
  30    in
  31    List.iter map a
  32
  33 let rec pp_term out = function
  34    | D.TSort (a, l)    -> pp_attrs out a; out (P.sprintf "*%u" l)
  35    | D.TLRef (a, i, j) -> pp_attrs out a; out (P.sprintf "#(%u,%u)" i j)
  36    | D.TGRef (a, u)    -> pp_attrs out a; out (P.sprintf "$")
  37    | D.TCast (a, x, y) -> pp_attrs out a; out "<"; pp_term out x; out ">."; pp_term out y
  38    | D.TProj (a, x, y) -> assert false
  39    | D.TAppl (a, x, y) -> pp_attrs out a; pp_terms "(" ")" out x; pp_term out y
  40    | D.TBind (a, x, y) -> pp_attrs out a; pp_bind out x; pp_term out y
  41
  42 and pp_terms bg eg out vs =
  43    let rec aux = function
  44       | []      -> ()
  45       | [v]     -> pp_term out v
  46       | v :: vs -> pp_term out v; out ", "; aux vs
  47    in
  48    out bg; aux vs; out (eg ^ ".")
  49
  50 and pp_bind out = function
  51    | D.Abst x -> pp_terms "[:" "]" out x
  52    | D.Abbr x -> pp_terms "[=" "]" out x
  53    | D.Void x -> out (P.sprintf "[%u]" x)
  54
  55 let rec pp_lenv out = function
  56    | D.ESort           -> ()
  57    | D.EProj (x, a, y) -> assert false
  58    | D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
  59
  60 (****************************************************************************)
  61
  62 let rec list_iter map l out tab = match l with
  63    | []       -> ()
  64    | hd :: tl -> map hd out tab; list_iter map tl out tab
  65
  66 let list_rev_iter map e ns l out tab =
  67    let rec aux err f e = function
  68       | [], []            -> f e
  69       | n :: ns, hd :: tl ->
  70         let f e =
  71 (*
  72            pp_lenv print_string e; print_string " |- ";
  73            pp_term print_string hd; print_newline ();
  74 *)
  75            map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
  76         in
  77         aux err f e (ns, tl)
  78       | _                 -> err ()
  79    in
  80    ignore (aux C.err C.start e (ns, l))
  81
  82 let lenv_iter map1 map2 l out tab =
  83    let rec aux f = function
  84       | D.ESort              -> f ()
  85       | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
  86       | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
  87    in
  88    aux C.start l
  89
  90 let rec exp_term e t out tab = match t with
  91    | D.TSort (a, l)       ->
  92       let a =
  93          let err _ = a in
  94          let f s = Y.Name (s, true) :: a in
  95          H.string_of_sort err f l
  96       in
  97       let attrs = [X.position l; X.name a] in
  98       X.tag X.sort attrs out tab
  99    | D.TLRef (a, i, j)    ->
 100       let a =
 101          let err _ = a in
 102          let f n r = Y.Name (n, r) :: a in
 103          D.get_name err f i j e
 104       in
 105       let attrs = [X.position i; X.offset j; X.name a] in
 106       X.tag X.lref attrs out tab
 107    | D.TGRef (a, n)       ->
 108       let a = Y.Name (U.name_of_uri n, true) :: a in
 109       let attrs = [X.uri n; X.name a] in
 110       X.tag X.gref attrs out tab
 111    | D.TCast (a, u, t)    ->
 112       let attrs = [] in
 113       X.tag X.cast attrs ~contents:(exp_term e u) out tab;
 114       exp_term e t out tab
 115    | D.TAppl (a, vs, t)   ->
 116       let attrs = [X.arity (List.length vs)] in
 117       X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
 118       exp_term e t out tab
 119    | D.TProj (a, lenv, t) ->
 120       let attrs = [] in
 121       X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
 122       exp_term (D.push_proj C.start e a lenv) t out tab
 123    | D.TBind (a, b, t) ->
 124       exp_bind e a b out tab;
 125       exp_term (D.push_bind C.start e a b) t out tab
 126
 127 and exp_bind e a b out tab =
 128    let f a ns = a, ns in
 129    let a, ns = Y.get_names f a in
 130    match b with
 131       | D.Abst ws ->
 132          let e = D.push_bind C.start e a (D.Abst []) in
 133          let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
 134          X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
 135       | D.Abbr vs ->
 136          let e = D.push_bind C.start e a (D.Abbr []) in
 137          let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
 138          X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
 139       | D.Void n ->
 140          let attrs = [X.name a; X.mark a; X.arity n] in
 141          X.tag X.void attrs out tab
 142
 143 and exp_eproj e a lenv out tab =
 144    let attrs = [] in
 145    X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
 146
 147 (****************************************************************************)
 148
 149 let export_term = exp_term D.empty_lenv