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 let unification vars locked_vars t1 t2 =
17 let lookup = Subst.lookup_subst in
18 let rec occurs_check subst what where =
20 | Terms.Var i when i = what -> true
22 let t = lookup where subst in
23 if t <> where then occurs_check subst what t else false
24 | Terms.Node l -> List.exists (occurs_check subst what) l
27 let rec unif subst vars s t =
28 let s = match s with Terms.Var _ -> lookup s subst | _ -> s
29 and t = match t with Terms.Var _ -> lookup t subst | _ -> t
33 | s, t when s = t -> subst, vars
34 | Terms.Var i, Terms.Var j
35 when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
37 (UnificationFailure (lazy "Inference.unification.unif"))
38 | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
40 | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
42 | Terms.Var i, t when occurs_check subst i t ->
44 (UnificationFailure (lazy "Inference.unification.unif"))
45 | Terms.Var i, t when (List.mem i locked_vars) ->
47 (UnificationFailure (lazy "Inference.unification.unif"))
49 let subst = Subst.buildsubst i t subst in
51 | _, Terms.Var _ -> unif subst vars t s
52 | Terms.Node (hds::_), Terms.Node (hdt::_) when hds <> hdt ->
53 raise (UnificationFailure (lazy "Inference.unification.unif"))
54 | Terms.Node (hds::tls), Terms.Node (hdt::tlt) -> (
57 (fun (subst', vars) s t -> unif subst' vars s t)
59 with Invalid_argument _ ->
60 raise (UnificationFailure (lazy "Inference.unification.unif"))
63 raise (UnificationFailure (lazy "Inference.unification.unif"))
65 let subst, vars = unif Subst.empty_subst vars t1 t2 in
66 let vars = Subst.filter subst vars in