helm/software/lambda-delta/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 B = Brg
  13
  14 let iter map d =
  15    let rec iter_bind d = function
  16       | B.Void as b -> b
  17       | B.Abst w    -> B.Abst (iter_term d w)
  18       | B.Abbr v    -> B.Abbr (iter_term d v)
  19    and iter_term d = function
  20       | B.Sort _ as t      -> t
  21       | B.GRef _ as t      -> t
  22       | B.LRef (a, i) as t -> if i < d then t else map d a i
  23       | B.Cast (a, w, v)   -> B.Cast (a, iter_term d w, iter_term d v)
  24       | B.Appl (a, w, u)   -> B.Appl (a, iter_term d w, iter_term d u)
  25       | B.Bind (a, b, u)   -> B.Bind (a, iter_bind d b, iter_term (succ d) u)
  26    in
  27    iter_term d
  28
  29 let lift_map h _ a i =
  30    if i + h >= 0 then B.LRef (a, i + h) else assert false
  31
  32 let lift g h d t =
  33    if h = 0 then g t else g (iter (lift_map h) d t)
  34
  35 let lift_bind g h d = function
  36    | B.Void   -> g B.Void
  37    | B.Abst w -> let g w = g (B.Abst w) in lift g h d w
  38    | B.Abbr v -> let g v = g (B.Abbr v) in lift g h d v