]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/basic_rg/brgSubstitution.ml
Fixed indentation, which is semantic in Haskell.
[helm.git] / helm / software / helena / src / basic_rg / brgSubstitution.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 G = Options
13 module B = Brg
14
15 let rec icm a = function
16    | B.Sort _
17    | B.LRef _
18    | B.GRef _                     -> succ a
19    | B.Bind (_, B.Void, t)        -> icm (succ a) t
20    | B.Cast (_, u, t)             -> icm (icm a u) t
21    | B.Appl (_, u, t)
22    | B.Bind (_, B.Abst (_, u), t)
23    | B.Bind (_, B.Abbr u, t)      -> icm (icm (succ a) u) t
24
25 let iter map d =
26    let rec iter_bind d = function
27       | B.Void        -> B.Void
28       | B.Abst (n, w) -> B.Abst (n, iter_term d w)
29       | B.Abbr v      -> B.Abbr (iter_term d v)
30    and iter_term d = function
31       | B.Sort _ as t      -> t
32       | B.GRef _ as t      -> t
33       | B.LRef (a, i) as t -> if i < d then t else map d a i
34       | B.Cast (a, w, v)   -> B.Cast (a, iter_term d w, iter_term d v)
35       | B.Appl (a, w, u)   -> B.Appl (a, iter_term d w, iter_term d u)
36       | B.Bind (a, b, u)   -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
37    in
38    iter_term d
39
40 let lift_map h _ a i =
41    if i + h >= 0 then B.LRef (a, i + h) else assert false
42
43 let lift h d t =
44    if h = 0 then t else begin
45 (*
46       G.icm := succ !G.icm; 
47       G.icm := icm !G.icm t;
48 *)
49       iter (lift_map h) d t
50    end