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