]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/xml/xmlCrg.ml
new options activated
[helm.git] / 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