helm/software/lambda-delta/basic_ag/bagSubstitution.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 S = Share
  13 module B = Bag
  14
  15 (* Internal functions *******************************************************)
  16
  17 let rec lref_map_bind f map b = match b with
  18    | B.Abbr v ->
  19       let f v' = f (S.sh1 v v' b B.abbr) in
  20       lref_map f map v
  21    | B.Abst w ->
  22       let f w' = f (S.sh1 w w' b B.abst) in
  23       lref_map f map w
  24    | B.Void   -> f b
  25
  26 and lref_map f map t = match t with
  27    | B.LRef i            ->
  28       let ii = map i in f (S.sh1 i ii t B.lref)
  29    | B.GRef _            -> f t
  30    | B.Sort _            -> f t
  31    | B.Cast (w, u)       ->
  32       let f w' u' = f (S.sh2 w w' u u' t B.cast) in
  33       let f w' = lref_map (f w') map u in
  34       lref_map f map w
  35    | B.Appl (w, u)       ->
  36       let f w' u' = f (S.sh2 w w' u u' t B.appl) in
  37       let f w' = lref_map (f w') map u in
  38       lref_map f map w
  39    | B.Bind (l, id, b, u) ->
  40       let f b' u' = f (S.sh2 b b' u u' t (B.bind l id)) in
  41       let f b' = lref_map (f b') map u in
  42       lref_map_bind f map b
  43
  44 (* Interface functions ******************************************************)
  45
  46 let subst f new_l old_l t =
  47    let map i = if i = old_l then new_l else i in
  48    if new_l = old_l then f t else lref_map f map t