]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_paramodulation/foSubst.ml
Use matita/lib as the new standard library in place of matita/nlibrary.
[helm.git] / matita / components / ng_paramodulation / foSubst.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 Subst (B : Terms.Blob) = struct *)
13   
14   let id_subst = [];;
15   
16   let build_subst n t tail = (n,t) :: tail ;;
17   
18   let rec lookup var subst =
19     match var with
20       | Terms.Var i ->
21           (try
22             lookup (List.assoc i subst) subst
23           with
24               Not_found -> var)
25       | _ -> var
26   ;;
27   let lookup i subst = lookup (Terms.Var i) subst;;
28   
29   let is_in_subst i subst = List.mem_assoc i subst;;
30   
31   (* filter out from metasenv the variables in substs *)
32   let filter subst varlist =
33     List.filter
34       (fun m ->
35          not (is_in_subst m subst))
36       varlist
37   ;;
38
39   let rec reloc_subst subst = function
40     | (Terms.Leaf _) as t -> t
41     | Terms.Var i -> 
42         (try
43            List.assoc i subst
44          with
45              Not_found -> assert false)
46     | (Terms.Node l) ->
47         Terms.Node (List.map (fun t -> reloc_subst subst t) l)
48 ;;
49
50   let rec apply_subst subst = function
51     | (Terms.Leaf _) as t -> t
52     | Terms.Var i -> 
53         (match lookup i subst with
54         | Terms.Node _ as t -> apply_subst subst t
55         | t -> t)
56     | (Terms.Node l) ->
57         Terms.Node (List.map (fun t -> apply_subst subst t) l)
58 ;;
59
60   let flat subst =
61     List.map (fun (x,t) -> (x, apply_subst subst t)) subst
62 ;;
63
64   let concat x y = x @ y;;
65   
66 (* end *)