src/Tools/Metis/src/AtomNet.sml

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

(* ========================================================================= *)
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC ATOMS              *)
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

structure AtomNet :> AtomNet =
struct

open Useful;

(* ------------------------------------------------------------------------- *)
(* Helper functions.                                                         *)
(* ------------------------------------------------------------------------- *)

fun atomToTerm atom = Term.Fn atom;

fun termToAtom (Term.Var _) = raise Bug "AtomNet.termToAtom"
  | termToAtom (Term.Fn atom) = atom;

(* ------------------------------------------------------------------------- *)
(* A type of atom sets that can be efficiently matched and unified.          *)
(* ------------------------------------------------------------------------- *)

type parameters = TermNet.parameters;

type 'a atomNet = 'a TermNet.termNet;

(* ------------------------------------------------------------------------- *)
(* Basic operations.                                                         *)
(* ------------------------------------------------------------------------- *)

val new = TermNet.new;

val size = TermNet.size;

fun insert net (atm,a) = TermNet.insert net (atomToTerm atm, a);

fun fromList parm l = List.foldl (fn (atm_a,n) => insert n atm_a) (new parm) l;

val filter = TermNet.filter;

fun toString net = "AtomNet[" ^ Int.toString (size net) ^ "]";

val pp = TermNet.pp;

(* ------------------------------------------------------------------------- *)
(* Matching and unification queries.                                         *)
(*                                                                           *)
(* These function return OVER-APPROXIMATIONS!                                *)
(* Filter afterwards to get the precise set of satisfying values.            *)
(* ------------------------------------------------------------------------- *)

fun match net atm = TermNet.match net (atomToTerm atm);

fun matched net atm = TermNet.matched net (atomToTerm atm);

fun unify net atm = TermNet.unify net (atomToTerm atm);

end