]> matita.cs.unibo.it Git - helm.git/blob - matitaB/components/ng_paramodulation/foUnif.ml
Fixed indentation, which is semantic in Haskell.
[helm.git] / matitaB / components / ng_paramodulation / foUnif.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 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
13
14 exception UnificationFailure of string Lazy.t;;
15
16 let mem2 a b l =
17   let rec aux found_a found_b = function
18     | x :: tl ->
19        let found_a = found_a || x = a in
20        let found_b = found_b || x = b in
21        if found_a && found_b then true, true
22        else aux found_a found_b tl
23     | [] -> found_a, found_b
24   in
25    aux false false l
26 ;;
27
28 module Founif (B : Orderings.Blob) = struct
29   module Subst = FoSubst 
30   module U = FoUtils.Utils(B)
31
32   let unification (* vars *) locked_vars t1 t2 =
33     let rec occurs_check subst what where =
34       match where with
35       | Terms.Var i when i = what -> true
36       | Terms.Var i ->
37           let t = Subst.lookup i subst in
38           if not (U.eq_foterm t where) then occurs_check subst what t else false
39       | Terms.Node l -> List.exists (occurs_check subst what) l
40       | _ -> false
41     in
42     let rec unif subst s t =
43       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
44       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
45       
46       in
47       match s, t with
48       | s, t when U.eq_foterm s t -> subst
49       | Terms.Var i, Terms.Var j ->
50           (* TODO: look in locked vars for both i and j at once *)
51           let i_locked, j_locked = mem2 i j locked_vars in
52           if i_locked then
53             if j_locked then
54               raise (UnificationFailure (lazy "Inference.unification.unif"))
55             else
56               Subst.build_subst j s subst
57           else
58             Subst.build_subst i t subst
59       | Terms.Var i, t when occurs_check subst i t ->
60           raise (UnificationFailure (lazy "Inference.unification.unif"))
61       | Terms.Var i, t when (List.mem i locked_vars) -> 
62           raise (UnificationFailure (lazy "Inference.unification.unif"))
63       | Terms.Var i, t -> Subst.build_subst i t subst
64       | t, Terms.Var i when occurs_check subst i t ->
65           raise (UnificationFailure (lazy "Inference.unification.unif"))
66       | t, Terms.Var i when (List.mem i locked_vars) -> 
67           raise (UnificationFailure (lazy "Inference.unification.unif"))
68       | t, Terms.Var i -> Subst.build_subst i t subst
69       | Terms.Node l1, Terms.Node l2 -> (
70           try
71             List.fold_left2
72               (fun subst' s t -> unif subst' s t)
73               subst l1 l2
74           with Invalid_argument _ ->
75             raise (UnificationFailure (lazy "Inference.unification.unif"))
76         )
77       | _, _ ->
78           raise (UnificationFailure (lazy "Inference.unification.unif"))
79     in
80     let subst = unif Subst.id_subst t1 t2 in
81     subst
82 ;;
83
84 (* Sets of variables in s and t are assumed to be disjoint  *)
85   let alpha_eq s t =
86     let rec equiv subst s t =
87       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
88       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
89         
90       in
91       match s, t with
92         | s, t when U.eq_foterm s t -> subst
93         | Terms.Var i, Terms.Var j
94             when (not (List.exists (fun (_,k) -> k=t) subst)) ->
95             let subst = Subst.build_subst i t subst in
96               subst
97         | Terms.Node l1, Terms.Node l2 -> (
98             try
99               List.fold_left2
100                 (fun subst' s t -> equiv subst' s t)
101                 subst l1 l2
102             with Invalid_argument _ ->
103               raise (UnificationFailure (lazy "Inference.unification.unif"))
104           )
105         | _, _ ->
106             raise (UnificationFailure (lazy "Inference.unification.unif"))
107     in
108       equiv Subst.id_subst s t
109 ;;
110         
111
112 end