Unifier.mli 2.74 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
(* 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) : sig

  (* The type of unification variables. *)

  type variable

  (* [fresh s] creates a fresh variable that carries the structure [s]. *)

  val fresh: variable S.structure option -> variable

51 52 53 54
  (* [structure x] returns the structure (currently) carried by variable [x]. *)

  val structure: variable -> variable S.structure option

55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75
  (* [unify x y] attempts to unify the terms represented by the variables
     [x] and [y]. The creation of cycles is not permitted; an eager occurs
     check rules them out. *)

  exception Unify of variable * variable
  exception Occurs of variable * variable
  val unify: variable -> variable -> unit

  (* This is the type of deep terms over the signature [S]. *)

  type term =
    | TVar of int (* the variable's unique identity *)
    | TNode of term S.structure

  (* [decode x] turns the variable [x] into the term that it represents.
     Sharing is lost, so this operation can in the worst case have
     exponential cost. *)

  val decode: variable -> term

end