(* Binary relations.
   Copyright (C) 2003 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 "rel_h";

fun invrel ({} : ''a -m> ''b) : ''b -m> ''a set = {}
  | invrel {x => y} = {y => {x}}
  | invrel m = let val (m1, m2) = split m
		   val im1 = invrel m1
		   val im2 = invrel m2
	       in
		   (im1 delta im2) ++ {y => xs1 U xs2
				      | y => xs2 in map im1 <| im2
					val xs1 = ?im1 y}
	       end;

fun inv_rel {} = {}
  | inv_rel {x => ys} = {y => {x} | y in set ys}
  | inv_rel m = let val (m1, m2) = split m
		    val im1 = inv_rel m1
		    val im2 = inv_rel m2
		in
		    (im1 delta im2) ++ {y => xs1 U xs2
				       | y => xs2 in map im1 <| im2
					   val xs1 = ?im1 y}
		end;

fun m1 Urel m2 =
    (m1 delta m2) ++ {x => ys1 U ys2
		     | x => ys2 in map m1 <| m2
			 val ys1 = ?m1 x};

fun union_rel {} = {}
  | union_rel {r} = r
  | union_rel rs = let val (rs1, rs2) = split rs
		   in
		       union_rel rs1 Urel union_rel rs2
		   end;

fun diff_rel (r1, r2) =
    (r2 <-| r1) ++ {x => diff
		   | x => ys in map r2 <| r1
		     val ys' = ?r2 x
		     val diff = ys \ ys'
			 such that not (empty diff)};

fun comp_rel (r1, r2) = {x => zs
			| x => ys in map r2
			  val zs = union (rng (ys <| r1))
			      such that not (empty zs)};

fun transitive_closure r =
    let val r' = comp_rel (r, r) Urel r
    in
	if r=r'
	    then r
	else transitive_closure r'
    end;
