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 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
14 exception UnificationFailure of string Lazy.t;;
16 module Founif (B : Terms.Blob) = struct
17 module Subst = FoSubst (*.Subst(B)*)
18 module U = FoUtils.Utils(B)
20 let unification vars locked_vars t1 t2 =
21 let rec occurs_check subst what where =
23 | Terms.Var i when i = what -> true
25 let t = Subst.lookup i subst in
26 if not (U.eq_foterm t where) then occurs_check subst what t else false
27 | Terms.Node l -> List.exists (occurs_check subst what) l
30 let rec unif subst s t =
31 let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
32 and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
36 | s, t when U.eq_foterm s t -> subst
37 | Terms.Var i, Terms.Var j
38 when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
40 (UnificationFailure (lazy "Inference.unification.unif"))
41 | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
43 | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
45 | Terms.Var i, t when occurs_check subst i t ->
47 (UnificationFailure (lazy "Inference.unification.unif"))
48 | Terms.Var i, t when (List.mem i locked_vars) ->
50 (UnificationFailure (lazy "Inference.unification.unif"))
52 let subst = Subst.build_subst i t subst in
54 | _, Terms.Var _ -> unif subst t s
55 | Terms.Node l1, Terms.Node l2 -> (
58 (fun subst' s t -> unif subst' s t)
60 with Invalid_argument _ ->
61 raise (UnificationFailure (lazy "Inference.unification.unif"))
64 raise (UnificationFailure (lazy "Inference.unification.unif"))
66 let subst = unif Subst.id_subst t1 t2 in
67 let vars = Subst.filter subst vars in
72 let rec equiv subst s t =
73 let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
74 and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
78 | s, t when U.eq_foterm s t -> subst
79 | Terms.Var i, Terms.Var j
80 when (not (List.exists (fun (_,k) -> k=t) subst)) ->
81 let subst = Subst.build_subst i t subst in
83 | Terms.Node l1, Terms.Node l2 -> (
86 (fun subst' s t -> equiv subst' s t)
88 with Invalid_argument _ ->
89 raise (UnificationFailure (lazy "Inference.unification.unif"))
92 raise (UnificationFailure (lazy "Inference.unification.unif"))
94 equiv Subst.id_subst s t