Unifier.ml 6.3 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13
(******************************************************************************)
(*                                                                            *)
(*                                   Menhir                                   *)
(*                                                                            *)
(*                       François Pottier, Inria Paris                        *)
(*              Yann Régis-Gianas, PPS, Université Paris Diderot              *)
(*                                                                            *)
(*  Copyright Inria. All rights reserved. This file is distributed under the  *)
(*  terms of the GNU General Public License version 2, as described in the    *)
(*  file LICENSE.                                                             *)
(*                                                                            *)
(******************************************************************************)

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95
(* This module provides a simple-minded implementation of first-order
   unification over an arbitrary signature. *)

(* -------------------------------------------------------------------------- *)

(* The signature must be described by the client, as follows. *)

module type STRUCTURE = sig

  (* The type ['a structure] should be understood as a type of shallow terms
     whose leaves have type ['a]. *)
  type 'a structure

  val map: ('a -> 'b) -> 'a structure -> 'b structure

  val iter: ('a -> unit) -> 'a structure -> unit

  (* [iter2] fails if the head constructors differ. *)
  exception Iter2
  val iter2: ('a -> 'b -> unit) -> 'a structure -> 'b structure -> unit

end

(* -------------------------------------------------------------------------- *)

(* The unifier. *)

module Make (S : STRUCTURE) = struct

type 'a structure = 'a S.structure

(* The data structure maintained by the unifier is as follows. *)

(* A unifier variable is a point of the union-find algorithm. *)

type variable =
    descriptor UnionFind.point

and descriptor = {

  (* Every equivalence class carries a globally unique identifier. When
     a new equivalence class is created, a fresh identifier is chosen,
     and when two classes are merged, one of the two identifiers is kept.
     This identifier can be used as a key in a hash table. One should be
     aware, though, that identifiers are stable only as long as no unions
     are performed. *)

  id : int;

  (* Every equivalence class carries a structure, which is either [None],
     which means that the variable is just that, a variable; or [Some t],
     which means that the variable represents (has been equated with) the
     term [t]. *)

  structure : variable structure option;

  (* Every equivalence class carries a mutable mark, which is used only by the
     occurs check. We could also remove this field altogether and use a
     separate hash table, where [id]s serve as keys, but this should be
     faster. The occurs check is performed eagerly, so this could matter. *)

  mutable mark : Mark.t;

}

(* -------------------------------------------------------------------------- *)

(* Accessors. *)

let id v =
  (UnionFind.get v).id

let structure v =
  (UnionFind.get v).structure

(* -------------------------------------------------------------------------- *)

(* [fresh] creates a fresh variable with specified structure. *)

let fresh =
  let c = ref 0 in
  fun structure ->
96
    let id = Misc.postincrement c in
97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134
    let mark = Mark.none in
    UnionFind.fresh { id; structure; mark }

(* -------------------------------------------------------------------------- *)

(* [occurs_check x y] checks that [x] does not occur within [y]. *)

exception Occurs of variable * variable

let occurs_check x y =
  (* Generate a fresh color for this particular traversal. *)
  let black = Mark.fresh () in
  (* The traversal code -- a depth-first search. *)
  let rec visit z =
    let desc = UnionFind.get z in
    if not (Mark.same desc.mark black) then begin
      desc.mark <- black;
      (* We are looking for [x]. *)
      if UnionFind.equivalent x z then
        raise (Occurs (x, y))
      else
        Option.iter (S.iter visit) desc.structure
    end
  in
  (* The root is [y]. *)
  visit y

(* -------------------------------------------------------------------------- *)

(* The internal function [unify v1 v2] equates the variables [v1] and [v2] and
   propagates the consequences of this equation until a cycle is detected, an
   inconsistency is found, or a solved form is reached. The exceptions that
   can be raised are [Occurs] and [S.Iter2]. *)

let rec unify (v1 : variable) (v2 : variable) : unit =
  if not (UnionFind.equivalent v1 v2) then begin
    let desc1 = UnionFind.get v1
    and desc2 = UnionFind.get v2 in
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158
    (* Unify the two descriptors. *)
    let desc =
      match desc1.structure, desc2.structure with
      | None, None   ->
          (* variable/variable *)
          desc1
      | None, Some _ ->
          (* variable/term *)
          occurs_check v1 v2;
          desc2
      | Some _, None ->
          (* term/variable *)
          occurs_check v2 v1;
          desc1
      | Some s1, Some s2 ->
          (* term/term *)
          S.iter2 unify s1 s2;
          { desc1 with structure = Some s1 }
    in
    (* Merge the equivalence classes. Do this last, so we get more meaningful
       output if the recursive call (above) fails and we have to print the
       two terms. *)
    UnionFind.union v1 v2;
    UnionFind.set v1 desc
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
  end

(* -------------------------------------------------------------------------- *)

(* The public version of [unify]. *)

exception Unify of variable * variable

let unify v1 v2 =
  try
    unify v1 v2
  with S.Iter2 ->
    raise (Unify (v1, v2))

(* -------------------------------------------------------------------------- *)

(* Decoding an acyclic graph as a deep term. *)

(* This is a simple-minded version of the code, where sharing is lost. Its
   cost could be exponential if there is a lot of sharing. In practice, its
   use is usually appropriate, especially in the scenario where the term is
   meant to be printed as a tree. *)

type term =
  | TVar of int
  | TNode of term structure

let rec decode (v : variable) : term =
  match structure v with
  | None ->
     TVar (id v)
  | Some t ->
     TNode (S.map decode t)

(* -------------------------------------------------------------------------- *)

end