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