(* Congruence closure, headers.
   Copyright (C) 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

   h1 is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 2, or (at your option)
   any later version.

   h1 is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "term_h";

exception NotColor;
(* raised when a color was expected (see below, comment on find),
 but a term was provided. *)
exception NotRewrite;
(* raised when add_rewrite is given a rule u->v
 with some variable x free in v but not in u. *)

type ''var color = ''var term;

type (''var, 'a) cc =
    |[find : ''var term -> ''var color,
      (* yields a unique representative of each term (its _color_). *)
      universe : unit -> ''var term -m> ''var color,
      (* return full map from universe (subterm-closed set of terms)
       to colors of terms.  If t in universe (), and is mapped to c,
       then find t=c.  In general, find t expands the universe. *)
      colors : unit -> ''var color -m> ''var term set,
      (* converse of previous map: maps each color to the collection
       of terms in the universe of the given color. *)
      equate : ''var term * ''var term -> unit, (* equate two terms *)
      class : ''var color -> ''var term set,
      (* return equivalence class denoted by color. *)
      select : string set * ''var color -> ''var term set,
      (* return set of terms f $ l
       in equivalence class with f in given set. *)
      equate_all : ''var term * ''var term * (''var -m> 'a) -> unit,
      (* equate_all (u, v, vars) instantiates the rewrite rule
       forall x1..xn . u = v,
       where vars={x1,...,xn}, to all instances u.sigma = v.sigma
       such that sigma maps variables in vars to elements of
       the current universe.  This may expand the
       universe, if v.sigma is not already in it. *)
(*
set_varnames : (''var -> string) -> unit, (* for debugging purposes *)
*)
      reset : unit -> unit
      (* erase the entire universe, to save memory.
	All information are lost. *)
      ]|;

extern val cc : unit -> (''_var, '_a) cc;
