helm/software/helena/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 R  = Alpha
  17 module XL = XmlLibrary
  18 module D  = Crg
  19
  20 (* internal functions *******************************************************)
  21
  22 let lenv_iter map_bind map_appl map_proj e lenv out tab =
  23    let rec aux = function
  24       | D.ESort           -> e
  25       | D.EBind (e, a, b) ->
  26          let e = aux e in
  27          map_bind e a b out tab; D.EBind (e, a, b)
  28       | D.EAppl (e, a, v) ->
  29          let e = aux e in
  30          map_appl e a v out tab; D.EAppl (e, a, v)
  31       | D.EProj (e, a, d) ->
  32          let e = aux e in
  33          map_proj e a d out tab; D.EProj (e, a, d)
  34    in
  35    ignore (aux lenv)
  36
  37 let rec exp_term e t out tab = match t with
  38    | D.TSort (a, l)       ->
  39       let a =
  40          let err _ = a in
  41          let f s = Y.Name (s, true) :: a in
  42          H.string_of_sort err f l
  43       in
  44       let attrs = [XL.position l; XL.name a] in
  45       XL.tag XL.sort attrs out tab
  46    | D.TLRef (a, i)       ->
  47       let a =
  48          let err _ = a in
  49          let f n r = Y.Name (n, r) :: a in
  50          D.get_name err f i e
  51       in
  52       let attrs = [XL.position i; XL.name a] in
  53       XL.tag XL.lref attrs out tab
  54    | D.TGRef (a, n)       ->
  55       let a = Y.Name (U.name_of_uri n, true) :: a in
  56       let attrs = [XL.uri n; XL.name a; XL.apix a] in
  57       XL.tag XL.gref attrs out tab
  58    | D.TCast (a, u, t)    ->
  59       let attrs = [] in
  60       XL.tag XL.cast attrs ~contents:(exp_term e u) out tab;
  61       exp_term e t out tab
  62    | D.TAppl (a, v, t)    ->
  63       let attrs = [] in
  64       XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
  65       exp_term e t out tab
  66    | D.TProj (a, lenv, t) ->
  67       let attrs = [] in
  68       XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab;
  69       exp_term (D.push_proj C.start a lenv e) t out tab
  70    | D.TBind (a, b, t) ->
  71 (* NOTE: the inner binders are alpha-converted first *)
  72       let a = R.alpha (D.names_of_lenv [] e) a in
  73       exp_bind e a b out tab;
  74       exp_term (D.push_bind C.start a b e) t out tab
  75
  76 and exp_appl e a v out tab =
  77    let attrs = [] in
  78    XL.tag XL.appl attrs ~contents:(exp_term e v) out tab;
  79
  80 and exp_bind e a b out tab = match b with
  81    | D.Abst (n, w) ->
  82       let attrs = [XL.level n; XL.name a; XL.mark a] in
  83       XL.tag XL.abst attrs ~contents:(exp_term e w) out tab
  84    | D.Abbr v      ->
  85       let attrs = [XL.name a] in
  86       XL.tag XL.abbr attrs ~contents:(exp_term e v) out tab
  87    | D.Void        ->
  88       let attrs = [XL.name a] in
  89       XL.tag XL.void attrs out tab
  90
  91 and exp_proj e a lenv out tab =
  92    let attrs = [] in
  93    XL.tag XL.proj attrs ~contents:(lenv_iter exp_bind exp_appl exp_proj e lenv) out tab
  94
  95 (* interface functions ******************************************************)
  96
  97 let export_term = exp_term D.empty_lenv