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 = Subst.Subst(B)
18 module U = Terms.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 where 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 vars s t =
32 let s = match s with Terms.Var _ -> lookup s subst | _ -> s
33 and t = match t with Terms.Var _ -> lookup t subst | _ -> t
37 | s, t when U.eq_foterm s t -> subst, vars
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.buildsubst i t subst in
55 | _, Terms.Var _ -> unif subst vars t s
56 | Terms.Node (hds::_),Terms.Node (hdt::_) when not(U.eq_foterm hds hdt)->
57 raise (UnificationFailure (lazy "Inference.unification.unif"))
58 | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
61 (fun (subst', vars) s t -> unif subst' vars s t)
63 with Invalid_argument _ ->
64 raise (UnificationFailure (lazy "Inference.unification.unif"))
67 raise (UnificationFailure (lazy "Inference.unification.unif"))
69 let subst, vars = unif Subst.empty_subst vars t1 t2 in
70 let vars = Subst.filter subst vars in