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)
19 let unification vars locked_vars t1 t2 =
20 let lookup = Subst.lookup_subst in
21 let rec occurs_check subst what where =
23 | Terms.Var i when i = what -> true
25 let t = lookup where subst in
26 if 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 vars s t =
31 let s = match s with Terms.Var _ -> lookup s subst | _ -> s
32 and t = match t with Terms.Var _ -> lookup t subst | _ -> t
36 | s, t when s = t -> subst, vars
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.buildsubst i t subst in
54 | _, Terms.Var _ -> unif subst vars t s
55 | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
56 raise (UnificationFailure (lazy "Inference.unification.unif"))
57 | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
60 (fun (subst', vars) s t -> unif subst' vars s t)
62 with Invalid_argument _ ->
63 raise (UnificationFailure (lazy "Inference.unification.unif"))
66 raise (UnificationFailure (lazy "Inference.unification.unif"))
68 let subst, vars = unif Subst.empty_subst vars t1 t2 in
69 let vars = Subst.filter subst vars in