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