helm/software/components/ng_paramodulation/founif.ml

   1 (*
   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.
   5     ||I||
   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_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 exception UnificationFailure of string Lazy.t;;
  15
  16 let unification vars locked_vars t1 t2 =
  17   let lookup = Subst.lookup_subst in
  18   let rec occurs_check subst what where =
  19     match where with
  20     | Terms.Var i when i = what -> true
  21     | Terms.Var _ ->
  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
  25     | _ -> false
  26   in
  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
  30
  31     in
  32     match s, t with
  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) ->
  36         raise
  37           (UnificationFailure (lazy "Inference.unification.unif"))
  38     | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
  39         unif subst vars t s
  40     | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
  41         unif subst vars t s
  42     | Terms.Var i, t when occurs_check subst i t ->
  43         raise
  44           (UnificationFailure (lazy "Inference.unification.unif"))
  45     | Terms.Var i, t when (List.mem i locked_vars) ->
  46         raise
  47           (UnificationFailure (lazy "Inference.unification.unif"))
  48     | Terms.Var i, t ->
  49         let subst = Subst.buildsubst i t subst in
  50         subst, vars
  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) -> (
  55         try
  56           List.fold_left2
  57             (fun (subst', vars) s t -> unif subst' vars s t)
  58             (subst, vars) tls tlt
  59         with Invalid_argument _ ->
  60           raise (UnificationFailure (lazy "Inference.unification.unif"))
  61       )
  62     | _, _ ->
  63         raise (UnificationFailure (lazy "Inference.unification.unif"))
  64   in
  65   let subst, vars = unif Subst.empty_subst vars t1 t2 in
  66   let vars = Subst.filter subst vars in
  67   subst, vars