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 lookup = Subst.lookup_subst in
22 let rec occurs_check subst what where =
24 | Terms.Var i when i = what -> true
26 let t = lookup i subst in
27 if not (U.eq_foterm t where) then occurs_check subst what t else false
28 | Terms.Node l -> List.exists (occurs_check subst what) l
31 let rec unif subst s t =
32 let s = match s with Terms.Var i -> lookup i subst | _ -> s
33 and t = match t with Terms.Var i -> lookup i subst | _ -> t
37 | s, t when U.eq_foterm s t -> subst
38 | Terms.Var i, Terms.Var j
39 when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
41 (UnificationFailure (lazy "Inference.unification.unif"))
42 | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
44 | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
46 | Terms.Var i, t when occurs_check subst i t ->
48 (UnificationFailure (lazy "Inference.unification.unif"))
49 | Terms.Var i, t when (List.mem i locked_vars) ->
51 (UnificationFailure (lazy "Inference.unification.unif"))
53 let subst = Subst.build_subst i t subst in
55 | _, Terms.Var _ -> unif subst t s
56 | Terms.Node l1, Terms.Node l2 -> (
59 (fun subst' s t -> unif subst' s t)
61 with Invalid_argument _ ->
62 raise (UnificationFailure (lazy "Inference.unification.unif"))
65 raise (UnificationFailure (lazy "Inference.unification.unif"))
67 let subst = unif Subst.id_subst t1 t2 in
68 let vars = Subst.filter subst vars in