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.
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_______________________________________________________________ *)
12 (* module Subst (B : Terms.Blob) = struct *)
16 let build_subst n t tail = (n,t) :: tail ;;
18 let rec lookup var subst =
22 lookup (List.assoc i subst) subst
27 let lookup i subst = lookup (Terms.Var i) subst;;
29 let is_in_subst i subst = List.mem_assoc i subst;;
31 (* filter out from metasenv the variables in substs *)
32 let filter subst varlist =
35 not (is_in_subst m subst))
39 let rec apply_subst subst = function
40 | (Terms.Leaf _) as t -> t
42 (match lookup i subst with
43 | Terms.Node _ as t -> apply_subst subst t
46 Terms.Node (List.map (fun t -> apply_subst subst t) l)
49 let concat x y = x @ y;;