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 module Founif (B : Terms.Blob) = struct
  17   module Subst = FoSubst (*.Subst(B)*)
  18   module U = FoUtils.Utils(B)
  19
  20   let unification vars locked_vars t1 t2 =
  21     let rec occurs_check subst what where =
  22       match where with
  23       | Terms.Var i when i = what -> true
  24       | Terms.Var i ->
  25           let t = Subst.lookup i subst in
  26           if not (U.eq_foterm t where) then occurs_check subst what t else false
  27       | Terms.Node l -> List.exists (occurs_check subst what) l
  28       | _ -> false
  29     in
  30     let rec unif subst s t =
  31       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
  32       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
  33
  34       in
  35       match s, t with
  36       | s, t when U.eq_foterm s t -> subst
  37       | Terms.Var i, Terms.Var j
  38           when (List.mem i locked_vars) &&(List.mem j locked_vars) ->
  39           raise
  40             (UnificationFailure (lazy "Inference.unification.unif"))
  41       | Terms.Var i, Terms.Var j when (List.mem i locked_vars) ->
  42           unif subst t s
  43       | Terms.Var i, Terms.Var j when (i > j) && not (List.mem j locked_vars) ->
  44           unif subst t s
  45       | Terms.Var i, t when occurs_check subst i t ->
  46           raise
  47             (UnificationFailure (lazy "Inference.unification.unif"))
  48       | Terms.Var i, t when (List.mem i locked_vars) ->
  49           raise
  50             (UnificationFailure (lazy "Inference.unification.unif"))
  51       | Terms.Var i, t ->
  52           let subst = Subst.build_subst i t subst in
  53           subst
  54       | _, Terms.Var _ -> unif subst t s
  55       | Terms.Node l1, Terms.Node l2 -> (
  56           try
  57             List.fold_left2
  58               (fun subst' s t -> unif subst' s t)
  59               subst l1 l2
  60           with Invalid_argument _ ->
  61             raise (UnificationFailure (lazy "Inference.unification.unif"))
  62         )
  63       | _, _ ->
  64           raise (UnificationFailure (lazy "Inference.unification.unif"))
  65     in
  66     let subst = unif Subst.id_subst t1 t2 in
  67     let vars = Subst.filter subst vars in
  68     subst, vars
  69 ;;
  70
  71   let alpha_eq s t =
  72     let rec equiv subst s t =
  73       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
  74       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
  75
  76       in
  77       match s, t with
  78         | s, t when U.eq_foterm s t -> subst
  79         | Terms.Var i, Terms.Var j
  80             when (not (List.exists (fun (_,k) -> k=t) subst)) ->
  81             let subst = Subst.build_subst i t subst in
  82               subst
  83         | Terms.Node l1, Terms.Node l2 -> (
  84             try
  85               List.fold_left2
  86                 (fun subst' s t -> equiv subst' s t)
  87                 subst l1 l2
  88             with Invalid_argument _ ->
  89               raise (UnificationFailure (lazy "Inference.unification.unif"))
  90           )
  91         | _, _ ->
  92             raise (UnificationFailure (lazy "Inference.unification.unif"))
  93     in
  94       equiv Subst.id_subst s t
  95 ;;
  96
  97 end