helm/software/lambda-delta/src/xml/XmlCrg.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 U = NUri
  13 module C = Cps
  14 module H = Hierarchy
  15 module Y = Entity
  16 module A = Alpha
  17 module X = Library
  18 module D = Crg
  19
  20 (* internal functions *******************************************************)
  21
  22 let rec list_iter map l out tab = match l with
  23    | []       -> ()
  24    | hd :: tl -> map hd out tab; list_iter map tl out tab
  25
  26 let list_rev_iter map e ns l out tab =
  27    let rec aux err f e = function
  28       | [], []            -> f e
  29       | n :: ns, hd :: tl ->
  30         let f e =
  31 (*
  32            pp_lenv print_string e; print_string " |- ";
  33            pp_term print_string hd; print_newline ();
  34 *)
  35            map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
  36         in
  37         aux err f e (ns, tl)
  38       | _                 -> err ()
  39    in
  40    ignore (aux C.err C.start e (ns, l))
  41
  42 let lenv_iter map1 map2 l out tab =
  43    let rec aux f = function
  44       | D.ESort              -> f ()
  45       | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
  46       | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
  47    in
  48    aux C.start l
  49
  50 let rec exp_term e t out tab = match t with
  51    | D.TSort (a, l)       ->
  52       let a =
  53          let err _ = a in
  54          let f s = Y.Name (s, true) :: a in
  55          H.string_of_sort err f l
  56       in
  57       let attrs = [X.position l; X.name a] in
  58       X.tag X.sort attrs out tab
  59    | D.TLRef (a, i, j)    ->
  60       let a =
  61          let err _ = a in
  62          let f n r = Y.Name (n, r) :: a in
  63          D.get_name err f i j e
  64       in
  65       let attrs = [X.position i; X.offset j; X.name a] in
  66       X.tag X.lref attrs out tab
  67    | D.TGRef (a, n)       ->
  68       let a = Y.Name (U.name_of_uri n, true) :: a in
  69       let attrs = [X.uri n; X.name a] in
  70       X.tag X.gref attrs out tab
  71    | D.TCast (a, u, t)    ->
  72       let attrs = [] in
  73       X.tag X.cast attrs ~contents:(exp_term e u) out tab;
  74       exp_term e t out tab
  75    | D.TAppl (a, vs, t)   ->
  76       let attrs = [X.arity (List.length vs)] in
  77       X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
  78       exp_term e t out tab
  79    | D.TProj (a, lenv, t) ->
  80       let attrs = [] in
  81       X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
  82       exp_term (D.push_proj C.start e a lenv) t out tab
  83    | D.TBind (a, b, t) ->
  84 (* NOTE: the inner binders are alpha-converted first *)
  85 (*       so undesirable renamings might occur        *)
  86 (* EX:   we rename [x][x]x to [x][x_]x_              *)
  87 (*       whereas [x_][x]x would be more desirable    *)
  88       let a = A.alpha (D.names_of_lenv [] e) a in
  89       exp_bind e a b out tab;
  90       exp_term (D.push_bind C.start e a b) t out tab
  91
  92 and exp_bind e a b out tab =
  93    let f a ns = a, ns in
  94    let a, ns = Y.get_names f a in
  95    match b with
  96       | D.Abst ws ->
  97          let e = D.push_bind C.start e a (D.Abst []) in
  98          let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
  99          X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
 100       | D.Abbr vs ->
 101          let e = D.push_bind C.start e a (D.Abbr []) in
 102          let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
 103          X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
 104       | D.Void n ->
 105          let attrs = [X.name a; X.mark a; X.arity n] in
 106          X.tag X.void attrs out tab
 107
 108 and exp_eproj e a lenv out tab =
 109    let attrs = [] in
 110    X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
 111
 112 (* interface functions ******************************************************)
 113
 114 let export_term = exp_term D.empty_lenv