(* Make and parse intersection and "exactly" predicates.
   Copyright (C) 2005 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 "intersym_h";
open "intersymlex_h";
open "exactsymlex_h";
open "sort_h";

val alpha_sort = sort (op strless);

fun _stringify s =
    let val f as |[put, convert, ... ]| = outstring ""
    in
	iterate
	  (case c of
	       "_" => put "__"
	     | "#" => put "_sharp_"
	     | _ => put c)
	| c in list explode s
	end;
	convert ()
    end;

exception NotInterEvt;

fun block_of_inter "__all" = {}
  | block_of_inter P =
    let val f = instring P
	val yyd = glex_data (f, fn _ => true)
	val yyloc = glex_loc yyd
	fun do_block_of_inter B =
	    case intersymlex yyd of
		ISL_ERR => {P}
	      | ISL_P Q => do_block_of_inter (B U {Q})
	      | ISL_END Q => B U {Q}
    in
	do_block_of_inter {}
    end

fun block_of_exact "__bot" = {}
  | block_of_exact P =
    let val f = instring P
	val yyd = glex_data (f, fn _ => true)
	val yyloc = glex_loc yyd
	fun do_block_of_exact B =
	    case exactsymlex yyd of
		ESL_ERR => raise BlockOfExactEvt
	      | ESL_P Q => do_block_of_exact (B U {Q})
	      | ESL_END Q => B U {Q}
    in
	do_block_of_exact {}
    end

fun mk_inter {} = "__all"
  | mk_inter {P} = P
  | mk_inter B =
    let val Pl = alpha_sort (union {block_of_inter P
				   | P in set B})
	val f as |[put, convert, ... ]| = outstring "__inter_"
	val delimr = ref ""
    in
	iterate
	  (put (!delimr);
	   delimr := "_and_";
	   put (_stringify P))
	| P in list Pl
	end;
	convert ()
    end;

fun mk_detval {} = "__bot"
  | mk_detval B =
    let val Pl = alpha_sort (union {block_of_inter P
				   | P in set B})
	val f as |[put, convert, ... ]| = outstring "__exactly_"
	val delimr = ref ""
    in
	iterate
	  (put (!delimr);
	   delimr := "_and_";
	   put (_stringify P))
	| P in list Pl
	end;
	convert ()
    end;
