(* utility functions for sets of gclauses.
   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 "gclauseutils_h";

fun range_restrict (named_gcl, dompred, varname, defcst) =
    let val gcl = [gc | (_, _, gc) in list named_gcl]
	val fsig0 = gclause_list_sig gcl
	val fsig = if empty (fsig0 |> {0})
		       then fsig0 ++ {defcst => 0}
		   else fsig0
	memofun varlist 0 = nil
	      | varlist k = V (varname k)::varlist (k-1)
	memofun dompred_body 0 = nil
	      | dompred_body k =
		(dompred $ [V (varname k)])::dompred_body (k-1)
	val needs_dompred = ref false
	fun make_rr (gc as GCLAUSE (negs, poss)) =
	    let val newvars = union {tvars t | t in list poss}
		    \ union {tvars t | t in list negs}
	    in
		if empty newvars
		    then gc
		else (needs_dompred := true;
		      GCLAUSE ([dompred $ [V x]
			       | x in set newvars] @ negs,
				 poss))
	    end
	val newgcl = [(name, stat, make_rr gc)
		     | (name, stat, gc) in list named_gcl]
    in
	if !needs_dompred
	    then [(dompred ^ "_" ^ f, "axiom",
		   GCLAUSE (dompred_body k,
			    [dompred $ [f $ varlist k]]))
		 | f => k in map fsig]
		@ newgcl
	else named_gcl
    end;
