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.Priv            -> out (P.sprintf "%s;" "~")
  29    in
  30    List.iter map a
  31
  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
  40
  41 and pp_terms bg eg out vs =
  42    let rec aux = function
  43       | []      -> ()
  44       | [v]     -> pp_term out v
  45       | v :: vs -> pp_term out v; out ", "; aux vs
  46    in
  47    out bg; aux vs; out (eg ^ ".")
  48
  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)
  53
  54 let rec pp_lenv out = function
  55    | D.ESort           -> ()
  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
  58
  59 (****************************************************************************)
  60
  61 let rec list_iter map l out tab = match l with
  62    | []       -> ()
  63    | hd :: tl -> map hd out tab; list_iter map tl out tab
  64
  65 let list_rev_iter map e ns l out tab =
  66    let rec aux err f e = function
  67       | [], []            -> f e
  68       | n :: ns, hd :: tl ->
  69         let f e =
  70 (*
  71            pp_lenv print_string e; print_string " |- ";
  72            pp_term print_string hd; print_newline ();
  73 *)
  74            map e hd out tab; f (D.push2 C.err C.start e n ~t:hd)
  75         in
  76         aux err f e (ns, tl)
  77       | _                 -> err ()
  78    in
  79    ignore (aux C.err C.start e (ns, l))
  80
  81 let lenv_iter map1 map2 l out tab =
  82    let rec aux f = function
  83       | D.ESort              -> f ()
  84       | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
  85       | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
  86    in
  87    aux C.start l
  88
  89 let rec exp_term e t out tab = match t with
  90    | D.TSort (a, l)       ->
  91       let a =
  92          let err _ = a in
  93          let f s = Y.Name (s, true) :: a in
  94          H.get_sort err f l
  95       in
  96       let attrs = [X.position l; X.name a] in
  97       X.tag X.sort attrs out tab
  98    | D.TLRef (a, i, j)    ->
  99       let a =
 100          let err _ = a in
 101          let f n r = Y.Name (n, r) :: a in
 102          D.get_name err f i j e
 103       in
 104       let attrs = [X.position i; X.offset j; X.name a] in
 105       X.tag X.lref attrs out tab
 106    | D.TGRef (a, n)       ->
 107       let a = Y.Name (U.name_of_uri n, true) :: a in
 108       let attrs = [X.uri n; X.name a] in
 109       X.tag X.gref attrs out tab
 110    | D.TCast (a, u, t)    ->
 111       let attrs = [] in
 112       X.tag X.cast attrs ~contents:(exp_term e u) out tab;
 113       exp_term e t out tab
 114    | D.TAppl (a, vs, t)   ->
 115       let attrs = [X.arity (List.length vs)] in
 116       X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
 117       exp_term e t out tab
 118    | D.TProj (a, lenv, t) ->
 119       let attrs = [] in
 120       X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
 121       exp_term (D.push_proj C.start e a lenv) t out tab
 122    | D.TBind (a, b, t) ->
 123       exp_bind e a b out tab;
 124       exp_term (D.push_bind C.start e a b) t out tab
 125
 126 and exp_bind e a b out tab =
 127    let f a ns = a, ns in
 128    let a, ns = Y.get_names f a in
 129    match b with
 130       | D.Abst ws ->
 131          let e = D.push_bind C.start e a (D.Abst []) in
 132          let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
 133          X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
 134       | D.Abbr vs ->
 135          let e = D.push_bind C.start e a (D.Abbr []) in
 136          let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
 137          X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
 138       | D.Void n ->
 139          let attrs = [X.name a; X.mark a; X.arity n] in
 140          X.tag X.void attrs out tab
 141
 142 and exp_eproj e a lenv out tab =
 143    let attrs = [] in
 144    X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
 145
 146 (****************************************************************************)
 147
 148 let export_term = exp_term D.empty_lenv