matita/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 mem2 a b l =
  17   let rec aux found_a found_b = function
  18     | x :: tl ->
  19        let found_a = found_a || x = a in
  20        let found_b = found_b || x = b in
  21        if found_a && found_b then true, true
  22        else aux found_a found_b tl
  23     | [] -> found_a, found_b
  24   in
  25    aux false false l
  26 ;;
  27
  28 module Founif (B : Orderings.Blob) = struct
  29   module Subst = FoSubst
  30   module U = FoUtils.Utils(B)
  31
  32   let unification (* vars *) locked_vars t1 t2 =
  33     let rec occurs_check subst what where =
  34       match where with
  35       | Terms.Var i when i = what -> true
  36       | Terms.Var i ->
  37           let t = Subst.lookup i subst in
  38           if not (U.eq_foterm t where) then occurs_check subst what t else false
  39       | Terms.Node l -> List.exists (occurs_check subst what) l
  40       | _ -> false
  41     in
  42     let rec unif subst s t =
  43       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
  44       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
  45
  46       in
  47       match s, t with
  48       | s, t when U.eq_foterm s t -> subst
  49       | Terms.Var i, Terms.Var j ->
  50           (* TODO: look in locked vars for both i and j at once *)
  51           let i_locked, j_locked = mem2 i j locked_vars in
  52           if i_locked then
  53             if j_locked then
  54               raise (UnificationFailure (lazy "Inference.unification.unif"))
  55             else
  56               Subst.build_subst j s subst
  57           else
  58             Subst.build_subst i t subst
  59       | Terms.Var i, t when occurs_check subst i t ->
  60           raise (UnificationFailure (lazy "Inference.unification.unif"))
  61       | Terms.Var i, _t when (List.mem i locked_vars) ->
  62           raise (UnificationFailure (lazy "Inference.unification.unif"))
  63       | Terms.Var i, t -> Subst.build_subst i t subst
  64       | t, Terms.Var i when occurs_check subst i t ->
  65           raise (UnificationFailure (lazy "Inference.unification.unif"))
  66       | _t, Terms.Var i when (List.mem i locked_vars) ->
  67           raise (UnificationFailure (lazy "Inference.unification.unif"))
  68       | t, Terms.Var i -> Subst.build_subst i t subst
  69       | Terms.Node l1, Terms.Node l2 -> (
  70           try
  71             List.fold_left2
  72               (fun subst' s t -> unif subst' s t)
  73               subst l1 l2
  74           with Invalid_argument _ ->
  75             raise (UnificationFailure (lazy "Inference.unification.unif"))
  76         )
  77       | _, _ ->
  78           raise (UnificationFailure (lazy "Inference.unification.unif"))
  79     in
  80     let subst = unif Subst.id_subst t1 t2 in
  81     subst
  82 ;;
  83
  84 (* Sets of variables in s and t are assumed to be disjoint  *)
  85   let alpha_eq s t =
  86     let rec equiv subst s t =
  87       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
  88       and t = match t with Terms.Var i -> Subst.lookup i subst | _ -> t
  89
  90       in
  91       match s, t with
  92         | s, t when U.eq_foterm s t -> subst
  93         | Terms.Var i, Terms.Var _j
  94             when (not (List.exists (fun (_,k) -> k=t) subst)) ->
  95             let subst = Subst.build_subst i t subst in
  96               subst
  97         | Terms.Node l1, Terms.Node l2 -> (
  98             try
  99               List.fold_left2
 100                 (fun subst' s t -> equiv subst' s t)
 101                 subst l1 l2
 102             with Invalid_argument _ ->
 103               raise (UnificationFailure (lazy "Inference.unification.unif"))
 104           )
 105         | _, _ ->
 106             raise (UnificationFailure (lazy "Inference.unification.unif"))
 107     in
 108       equiv Subst.id_subst s t
 109 ;;
 110
 111
 112 end