]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/basic_rg/brgCrg.ml
new options activated
[helm.git] / helm / software / helena / src / basic_rg / brgCrg.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 C = Cps
13 module N = Layer
14 module E = Entity
15 module D = Crg
16 module B = Brg
17
18 (* internal functions: crg to brg term **************************************)
19
20 let rec xlate_term f = function
21    | D.TSort (a, l)       -> f (B.Sort (a, l))
22    | D.TGRef (a, n)       -> f (B.GRef (a, n))
23    | D.TLRef (a, i)       -> f (B.LRef (a, i))
24    | D.TCast (a, u, t)    ->
25       let f tt uu = f (B.Cast (a, uu, tt)) in
26       let f tt = xlate_term (f tt) u in
27       xlate_term f t 
28    | D.TAppl (a, x, v, t) ->
29       let f tt vv = f (B.Appl (a, x, vv, tt)) in
30       let f tt = xlate_term (f tt) v in
31       xlate_term f t 
32    | D.TProj (_, e, t)    -> 
33       D.shift (xlate_term f) e t
34    | D.TBind (a, b, t)    -> 
35       xlate_term (xlate_bind f a b) t
36
37 and xlate_bind f a b t = match b with
38    | D.Abst (r, n, w) ->
39       let f ww = f (B.Bind (a, B.Abst (r, n, ww), t)) in 
40       xlate_term f w
41    | D.Abbr v         ->
42       let f vv = f (B.Bind (a, B.Abbr vv, t)) in 
43       xlate_term f v
44    | D.Void           ->
45       f (B.Bind (a, B.Void, t))
46
47 (* internal functions: brg to crg term **************************************)
48
49 let rec xlate_bk_term f = function
50    | B.Sort (a, l)       -> f (D.TSort (a, l))
51    | B.GRef (a, n)       -> f (D.TGRef (a, n))
52    | B.LRef (a, i)       -> f (D.TLRef (a, i))
53    | B.Cast (a, u, t)    ->
54       let f tt uu = f (D.TCast (a, uu, tt)) in
55       let f tt = xlate_bk_term (f tt) u in
56       xlate_bk_term f t 
57    | B.Appl (a, x, u, t) ->
58       let f tt uu = f (D.TAppl (a, x, uu, tt)) in
59       let f tt = xlate_bk_term (f tt) u in
60       xlate_bk_term f t 
61    | B.Bind (a, b, t)    ->
62       let f tt bb = f (D.TBind (a, bb, tt)) in
63       let f tt = xlate_bk_bind (f tt) b in
64       xlate_bk_term f t 
65
66 and xlate_bk_bind f = function
67    | B.Abst (r, n, t) ->
68       let f tt = f (D.Abst (r, n, tt)) in
69       xlate_bk_term f t
70    | B.Abbr t         ->
71       let f tt = f (D.Abbr tt) in
72       xlate_bk_term f t
73    | B.Void           -> f D.Void
74    
75 (* interface functions ******************************************************)
76
77 let brg_of_crg f t = f (xlate_term C.start t)
78
79 let crg_of_brg = xlate_bk_term