flowrow-sort.c   [plain text]

/*
 * Copyright (c) 2000-2001
 *      The Regents of the University of California.  All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions
 * are met:
 * 1. Redistributions of source code must retain the above copyright
 *    notice, this list of conditions and the following disclaimer.
 * 2. Redistributions in binary form must reproduce the above copyright
 *    notice, this list of conditions and the following disclaimer in the
 *    documentation and/or other materials provided with the distribution.
 * 3. Neither the name of the University nor the names of its contributors
 *    may be used to endorse or promote products derived from this software
 *    without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
 * ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED.  IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
 * OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
 * HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
 * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
 * OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
 * SUCH DAMAGE.
 *
 */

#include <regions.h>
#include <assert.h>
#include <stdio.h>
#include <string.h>
#include <ansidecl.h>
#include "flowrow-sort.h"
#include "termhash.h"

#include "setif-sort.h"

#define ABS_TYPE 2
#define WILD_TYPE 3
#define ROW_TYPE 4

/* generic flow row */
struct flowrow_gen
{
#ifdef NONSPEC
  sort_kind sort;
#endif
  int type;
  stamp st;
#ifdef NONSPEC
  sort_kind base_sort; 
#endif
};

typedef struct flowrow_gen *flowrow_gen;

struct flowrow
{
#ifdef NONSPEC
  sort_kind sort;
#endif 
  int type;		
  stamp st;	
#ifdef NONSPEC
  sort_kind base_sort; 
#endif
  flowrow_map fields;
  gen_e rest;
};

typedef struct flowrow *flowrow;

struct field_split
{
  gen_e_list matched1;
  gen_e_list matched2;
  flowrow_map nomatch1;
  flowrow_map nomatch2;
};

region flowrow_region;
term_hash flowrow_hash;
struct flowrow_stats flowrow_stats;
static void fields_print(FILE *f,flowrow_map m,field_print_fn_ptr field_print) deletes;

stamp flowrow_get_stamp(gen_e e)
{
  if ( ((flowrow_gen)e)->type == ALIAS_TYPE)
    return ((flowrow_gen)fv_get_alias( (flow_var)e ))->st;
  else
    return ((flowrow_gen)e)->st;
  
}

static flowrow_map flowrow_get_fields(gen_e e)
{
  assert (flowrow_is_row(e));
  
  return ((flowrow)e)->fields;
}

static gen_e flowrow_get_rest(gen_e e)
{
  assert(flowrow_is_row(e));

  return ((flowrow)e)->rest;
}


static int field_compare(const flowrow_field f1,const flowrow_field f2)
			
{
  int compare = strcmp(f1->label,f2->label);
  return compare;
}


static int field_compare_ne(const flowrow_field f1,const flowrow_field f2)
			
{
  int compare = strcmp(f1->label,f2->label);

  if (! compare) /* rows should never have two fields with the same labels */
    {
      failure("Multiple fields in this row share the same label\n");
    }
  return compare;
}

static struct field_split split_fields(region r, flowrow_map fields1,
				       flowrow_map fields2)
{
  struct field_split split;
  flowrow_map_scanner scan1, scan2;
  flowrow_field field1,field2;
  bool consumed1 = TRUE,consumed2 = TRUE, 
    fields1_remain = TRUE, fields2_remain = TRUE;;

  split.matched1 = new_gen_e_list(r);
  split.matched2 = new_gen_e_list(r);
  split.nomatch1 = new_flowrow_map(r);
  split.nomatch2 = new_flowrow_map(r);

  flowrow_map_scan(fields1,&scan1);
  flowrow_map_scan(fields2,&scan2);
 
  while (TRUE)
    {
      if (consumed1)
	fields1_remain = flowrow_map_next(&scan1,&field1);
      if (consumed2)
     	fields2_remain = flowrow_map_next(&scan2,&field2);

      if (fields1_remain && fields2_remain)
	{
	  int compare_fields = field_compare(field1,field2);

	  if (compare_fields < 0)
	    {
	      flowrow_map_cons(field1,split.nomatch1);
	      consumed1 = TRUE;
	      consumed2 = FALSE;
	    }
	  else if (compare_fields > 0)
	    {
	      flowrow_map_cons(field2,split.nomatch2);
	      consumed2 = TRUE;
	      consumed1 = FALSE;
	    }
	  else /* two fields are equal */
	    {
	      gen_e_list_cons(field1->expr,split.matched1);
	      gen_e_list_cons(field2->expr,split.matched2);
	      consumed1 = TRUE;
	      consumed2 = TRUE;
	      continue;
	    }
	}
      else if (fields1_remain)
	{
	  /* flowrow_map_append(split.nomatch1,flowrow_map_copy(r,fields1)); */
	  flowrow_map_cons(field1,split.nomatch1);
	  
	  while (flowrow_map_next(&scan1,&field1))
	    {
	      flowrow_map_cons(field1,split.nomatch1);
	    }

	  break;
	}
      else if (fields2_remain)
	{
	  /* flowrow_map_append(split.nomatch2,flowrow_map_copy(r,fields2)); */
	  flowrow_map_cons(field2,split.nomatch2);
	  while (flowrow_map_next(&scan2,&field2))
	    {
	      flowrow_map_cons(field2,split.nomatch2);
	    }
	  break;
	}
      else /* no remaining fields, so */ break;
    }
  
  return split;
}

static bool flowrow_is_normalized(gen_e r)
{
 if ( flowrow_is_row(r) )
    {
      gen_e rest = flowrow_get_rest(r);
      
      if ( flowrow_is_row(rest) || flowrow_is_alias(rest) )
	return FALSE;
    }
 else if ( flowrow_is_alias(r) )
    return FALSE;

  return TRUE;
}

static gen_e normalize(get_stamp_fn_ptr get_stamp,
			 flowrow_map m,gen_e r) deletes
{
  if (flowrow_is_row(r))
    {
      flowrow_map_append(m,
			 flowrow_map_copy(flowrow_region,
					  flowrow_get_fields(r)));
      return normalize(get_stamp,m,flowrow_get_rest(r));
    }
  else if (flowrow_is_alias(r))
    {
      assert (! flowrow_is_alias(fv_get_alias((flow_var)r)) );
      return normalize(get_stamp, m,fv_get_alias((flow_var)r));
    }
  else
    return flowrow_row(get_stamp,m,r);
}

static gen_e normalize_row(get_stamp_fn_ptr get_stamp, gen_e r) deletes
{
  if (flowrow_is_normalized(r))
    return r;
  else /* normalize the row */
    return normalize(get_stamp,new_flowrow_map(flowrow_region),r);
}

static bool eq(gen_e e1, gen_e e2)
{
  return ( flowrow_get_stamp(e1) == flowrow_get_stamp(e2) ); 
}


/*
  A row constraint row1 <= row2 is l-inductive iff row2 is a var and for all 
  X = tlv(row1), o(row2) > o(X). 
  
  tlv(row) = {X} if row is a var X, {} otherwise 
*/
static bool l_inductive(gen_e e1, gen_e e2)
{
  if (flowrow_is_var(e2))
    {
      if (flowrow_is_var(e1))
	return flowrow_get_stamp(e2) > flowrow_get_stamp(e1);
      else return TRUE;
    }
  return FALSE;
}
      
/* 
   A row constraint row1 <= row2 is r-inductive iff row1 is a var and for all
   X = tlv(row2), o(row1) > o(X)
*/
static bool r_inductive(gen_e e1, gen_e e2)
{
  if (flowrow_is_var(e1))
    {
      if (flowrow_is_var(e2))
	return flowrow_get_stamp(e1) > flowrow_get_stamp(e2);
      else return TRUE;
    }
  return FALSE;
}

static inline bool flowrow_minimal(flowrow r)
{
  return flowrow_is_zero(r->rest);
}

static inline bool flowrow_maximal(flowrow r)
{
  return flowrow_is_one(r->rest);
}

static inline bool flowrow_closed(flowrow r)
{
  return flowrow_is_abs(r->rest);
}

static inline bool flowrow_wildcard(flowrow r)
{
  return flowrow_is_wild(r->rest);
}

static inline bool flowrow_var(flowrow r)
{
  return flowrow_is_var(r->rest);
}

static gen_e contour_instantiate(fresh_fn_ptr fresh,
				 get_stamp_fn_ptr get_stamp, 
				 gen_e e) deletes
{
  if (flowrow_is_row(e))
    {
      gen_e result;
      flowrow_map_scanner scan;
      flowrow_field f;
      gen_e row = normalize_row(get_stamp,e);

      region scratch_rgn = newregion();

      flowrow_map new_fields = new_flowrow_map(scratch_rgn);
            
      flowrow_map_scan(flowrow_get_fields(row),&scan);

      while (flowrow_map_next(&scan,&f))
	{
	  flowrow_field new_field =
	    ralloc(flowrow_region,struct flowrow_field);
	  new_field->label = f->label;
	  new_field->expr = fresh(NULL);
	  
	  flowrow_map_cons(new_field,new_fields);
	}
      
      result = flowrow_row(get_stamp,new_fields,flowrow_fresh(NULL));

      deleteregion(scratch_rgn);

      assert( flowrow_is_row(result) );
      
      return result;
    }
  
  else /* TODO */
    {
      failure("Unmatched contour\n");
      return NULL;
    }
}

static contour get_contour(fresh_fn_ptr fresh,get_stamp_fn_ptr get_stamp, 
			   gen_e zero_elem ATTRIBUTE_UNUSED,gen_e e)
{
  if (flowrow_is_row(e))
    {
      contour result;

      result = ralloc(flowrow_region,struct contour);
      result->shape = e;
      result->fresh = fresh;
      result->get_stamp = get_stamp;
      result->instantiate = contour_instantiate;
	  
      return result;
    }
  else /* TODO */
    {
      failure("Unmatched contour\n");
      return NULL;
    }
}
  

static  void trans_lbs(fresh_fn_ptr fresh,get_stamp_fn_ptr get_stamp, 
		       incl_fn_ptr field_incl, gen_e zero_elem,
		       flow_var v, gen_e e) deletes
{
  gen_e temp;
  gen_e_list_scanner scan;
  
  gen_e_list_scan(fv_get_lbs(v),&scan);
  while (gen_e_list_next(&scan,&temp))
      flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,temp,e);
  
}

static  void trans_ubs(fresh_fn_ptr fresh,get_stamp_fn_ptr get_stamp, 
		       incl_fn_ptr field_incl, gen_e zero_elem,
		       flow_var v, gen_e e) deletes
{
  gen_e temp;
  gen_e_list_scanner scan;
  
  gen_e_list_scan(fv_get_ubs(v),&scan);
  while (gen_e_list_next(&scan,&temp))
    flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,e,temp);
}

static  void update_lower_bound(fresh_fn_ptr fresh,get_stamp_fn_ptr get_stamp, 
				incl_fn_ptr field_incl, gen_e zero_elem,
				flow_var v,gen_e e) deletes
{
  if (fv_has_contour(v)) /* _ <= v, and v has a contour */
    {
      gen_e shape = fv_instantiate_contour(v);
      
      fv_set_alias(v,shape);
      trans_ubs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      trans_lbs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      
      flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,e,shape);
      
    }
  
  else if (flowrow_is_var(e)) 
    {
      flow_var v_lb = (flow_var)e;
      
      if (fv_has_contour(v_lb)) /* v1 <= v2, v1 has a contour */
	{
	  gen_e shape = fv_instantiate_contour(v_lb);
	  
	  fv_set_alias(v_lb,shape);
	  trans_ubs(fresh,get_stamp,field_incl,zero_elem,v_lb,shape);
	  trans_lbs(fresh,get_stamp,field_incl,zero_elem,v_lb,shape);
	  
	  flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,
			    shape,(gen_e)v);
	  
	}
      
      else /* we have v1 <= v2, no contours */
	{
	  bool redundant;
	  
	  fv_unify_contour(v,(flow_var)e);
	  redundant = fv_add_lb(v,e,flowrow_get_stamp(e));
	  
	  if (! redundant)
	    trans_ubs(fresh,get_stamp,field_incl,zero_elem,v,e);
	      
	}
    }
  else /* we have c(...) <= v, and v has no contour */
    {
      gen_e shape = NULL;
      fv_set_contour(v,get_contour(fresh,get_stamp,zero_elem,e));
      
      shape = fv_instantiate_contour(v);
      fv_set_alias(v,shape);
      trans_ubs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      trans_lbs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      
      flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,e,shape);
      
    }
}

static  void update_upper_bound(fresh_fn_ptr fresh,get_stamp_fn_ptr get_stamp, 
				incl_fn_ptr field_incl, gen_e zero_elem,
				flow_var v,gen_e e) deletes
{
  if (fv_has_contour(v)) /* v isn't aliased, and we discovered a contour*/
    {
      gen_e shape = fv_instantiate_contour(v);
      
      fv_set_alias(v,shape);
      trans_ubs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      trans_lbs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      
      flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,shape,e);
	  
    }
  
  else if (flowrow_is_var(e)) 
    {
      flow_var v2 = (flow_var)e;
	  
      if (fv_has_contour(v2)) // v2 isn't aliased, and we discovered a contour
	{
	  gen_e shape = fv_instantiate_contour(v2);
	     
	  fv_set_alias(v2,shape);
	  trans_ubs(fresh,get_stamp,field_incl,zero_elem,v2,shape);
	  trans_lbs(fresh,get_stamp,field_incl,zero_elem,v2,shape);	      


	  flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,
			    (gen_e)v,shape);

	}

      else /* we have v1 <= v2, no contours */
	{
	  bool redundant;
	    
	  fv_unify_contour(v,(flow_var)e);
	  redundant = fv_add_ub(v,e,flowrow_get_stamp(e));

	  if (! redundant)
	    trans_lbs(fresh,get_stamp,field_incl,zero_elem,v,e);
	      
	}
    }
  else /* we have v <= c(...), and v has no contour */
    {
      gen_e shape = NULL;
      fv_set_contour(v,get_contour(fresh,get_stamp,zero_elem,e));
	  
      shape = fv_instantiate_contour(v);

      if (! flowrow_is_row(shape) )
	{
	  assert(0);
	}
	  
      fv_set_alias(v,shape);
      trans_ubs(fresh,get_stamp,field_incl,zero_elem,v,shape);
      trans_lbs(fresh,get_stamp,field_incl,zero_elem,v,shape);
	  
	
      flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,shape,e);
	  
    }

}

// END


void flowrow_inclusion(fresh_fn_ptr fresh,get_stamp_fn_ptr get_stamp, 
		       incl_fn_ptr field_incl, gen_e zero_elem, gen_e a, 
		       gen_e b) deletes
{
  gen_e e1 = normalize_row(get_stamp, a),
    e2 = normalize_row(get_stamp, b);

  if (eq(e1,e2))
    return;
  else if (flowrow_is_zero(e1) || flowrow_is_wild(e1))
    return;
  else if (flowrow_is_one(e2) || flowrow_is_wild(e2))
    return;

  else if ( l_inductive(e1,e2) )
    {
      flow_var v2 = (flow_var)e2;
      
      flowrow_stats.rows_l_inductive++;
      
      update_lower_bound(fresh,get_stamp,field_incl,zero_elem,v2,e1);
      return;
    }
  
  else if ( r_inductive(e1,e2) )
    {
      flow_var v1 = (flow_var)e1;

      flowrow_stats.rows_r_inductive++;

      update_upper_bound(fresh,get_stamp,field_incl,zero_elem,v1,e2);
      return;
    }

  else if ( flowrow_is_row(e1) && flowrow_is_row(e2))
    {
      region scratch_rgn = newregion();
  
      flowrow r1 = (flowrow)e1,
	r2 = (flowrow)e2;

      struct field_split split = 
	split_fields(scratch_rgn,r1->fields,r2->fields);
      
      if ( gen_e_list_empty(split.matched1) ) 
	{
	  assert ( gen_e_list_empty(split.matched2) );

	  if (flowrow_wildcard(r1) || flowrow_minimal(r1))
	    {
	      gen_e newrow = 
		flowrow_row(get_stamp,split.nomatch1,flowrow_get_rest(e1));
		
	      flowrow_inclusion(fresh,get_stamp,field_incl, zero_elem,newrow, 
				flowrow_get_rest(e2));
	    }
	  else if (flowrow_maximal(r2) || flowrow_closed(r2))
	    {
	      gen_e newrow =
		flowrow_row(get_stamp,split.nomatch2,flowrow_get_rest(e2));

	      flowrow_inclusion(fresh, get_stamp,field_incl,zero_elem,
				flowrow_get_rest(e1),newrow);
	    }
	  else 
	    {
	      gen_e rest1 = flowrow_get_rest(e1),
		rest2 = flowrow_get_rest(e2);

	      //assert( flowrow_is_var(rest1) && flowrow_is_var(rest2));

	      if ( eq(rest1,rest2))
		  failure("Recursive row resolution\n");
	      else
		{
		  gen_e fv = flowrow_fresh(NULL);
		  gen_e newrow1 = flowrow_row(get_stamp,split.nomatch1,fv);
		  gen_e newrow2 = flowrow_row(get_stamp,split.nomatch2,fv);
		    
		  flowrow_inclusion(fresh,get_stamp,field_incl,
				    zero_elem,rest1,newrow2);
		  flowrow_inclusion(fresh,get_stamp,field_incl,
				    zero_elem,newrow1,rest2);
		}

	    } 
	}

      else /* some fields matched */
	{
	  gen_e_list_scanner scan1, scan2;
	  gen_e f1,f2;

	  assert( gen_e_list_length(split.matched1) 
		  == gen_e_list_length(split.matched2) );
	  
	  gen_e_list_scan(split.matched1,&scan1);
	  gen_e_list_scan(split.matched2,&scan2);

	  while (gen_e_list_next(&scan1,&f1) &&
		 gen_e_list_next(&scan2,&f2) )
	    {
	      field_incl(f1,f2);
	    }
	  
	  if ( flowrow_wildcard(r1) && flowrow_wildcard(r2) )
	    {
	      goto END;
	    }
	  else
	    {
	      flowrow_map fields1 = split.nomatch1;
	      flowrow_map fields2 = split.nomatch2;
		     
	      gen_e newrow1 = flowrow_row(get_stamp,fields1,r1->rest);
	      gen_e newrow2 = flowrow_row(get_stamp,fields2,r2->rest);
	      
	      flowrow_inclusion(fresh,get_stamp,field_incl,zero_elem,
				newrow1, newrow2);
	    }
	}
    END:
      deleteregion(scratch_rgn);
    }
  
  else /* potentially a problem normalizing a row? */
    {
      failure("Unmatched case in row inclusion\n");
      return;
    }
}

gen_e flowrow_row(get_stamp_fn_ptr get_stamp,flowrow_map f, gen_e rest) deletes
{
  flowrow_map fields = flowrow_map_copy(flowrow_region,f);

  if (flowrow_map_empty(fields))
    {
      return rest;
    }
  else
    { 
      flowrow_map_scanner scan;
      flowrow_field temp;
      gen_e result;
      int i = 2,
	length = flowrow_map_length(fields);
      stamp st[2+2*length];

      st[0] = ROW_TYPE;
      if (rest)
	st[1] = flowrow_get_stamp(rest);
      else
	assert(0);

      flowrow_map_sort(fields,field_compare_ne);
  
      flowrow_map_scan(fields,&scan);
      while(flowrow_map_next(&scan,&temp))
      {
	st[i++] = stamp_string(temp->label);
	if (temp->expr)
	  st[i++] = get_stamp(temp->expr);
	else
	  assert(0);
      }

      if ( (result = term_hash_find(flowrow_hash,st,2 + 2*length)) == NULL)
	{
	  flowrow r = ralloc(flowrow_region, struct flowrow);
	  r->type = ROW_TYPE;
	  r->st = stamp_fresh();
	  r->fields = fields;
	  r->rest = rest;

#ifdef NONSPEC
	  r->base_sort = row_map_head(fields)->expr->sort;
	  r->sort = flowrow_sort;
#endif
	  result = (gen_e) r;
	  term_hash_insert(flowrow_hash,result,st,2+2*length);
	}
      /*  assert(flowrow_is_normalized(result)); */
      return result;

    }
}

#ifndef NONSPEC
static struct flowrow_gen zero_row = {ZERO_TYPE,ZERO_TYPE};
static struct flowrow_gen one_row = {ONE_TYPE,ONE_TYPE};
static struct flowrow_gen abs_row = {ABS_TYPE, ABS_TYPE};
static struct flowrow_gen wild_row = {WILD_TYPE, WILD_TYPE};

gen_e flowrow_zero(void)
{
  return (gen_e)&zero_row;
}

gen_e flowrow_one(void)
{
  return (gen_e)&one_row;
}

gen_e flowrow_abs(void)
{
  return (gen_e)&abs_row;
}

gen_e flowrow_wild(void)
{
  return (gen_e)&wild_row;
}

gen_e flowrow_fresh(const char *name)
{
  flowrow_stats.fresh++;
  return (gen_e)fv_fresh(flowrow_region,name);
}

gen_e flowrow_fresh_small(const char *name)
{
  flowrow_stats.fresh_small++;
  return (gen_e)fv_fresh_small(flowrow_region,name);
}

gen_e flowrow_fresh_large(const char *name)
{
  flowrow_stats.fresh_large++;
  return (gen_e)fv_fresh_large(flowrow_region,name);
}

#else
static struct flowrow_gen term_zero_row = {flowrow_sort,ZERO_TYPE,ZERO_TYPE,term_sort};
static struct flowrow_gen term_one_row = {flowrow_sort,ONE_TYPE,ONE_TYPE,term_sort};
static struct flowrow_gen term_abs_row = {flowrow_sort,ABS_TYPE, ABS_TYPE,term_sort};
static struct flowrow_gen term_wild_row = {flowrow_sort,WILD_TYPE, WILD_TYPE,term_sort};


static struct flowrow_gen setif_zero_row = {flowrow_sort,ZERO_TYPE,ZERO_TYPE,setif_sort};
static struct flowrow_gen setif_one_row = {flowrow_sort,ONE_TYPE,ONE_TYPE,setif_sort};
static struct flowrow_gen setif_abs_row = {flowrow_sort,ABS_TYPE, ABS_TYPE,setif_sort};
static struct flowrow_gen setif_wild_row = {flowrow_sort,WILD_TYPE, WILD_TYPE,setif_sort};

static struct flowrow_gen setst_zero_row = {flowrow_sort,ZERO_TYPE,ZERO_TYPE,setst_sort};
static struct flowrow_gen setst_one_row = {flowrow_sort,ONE_TYPE,ONE_TYPE,setst_sort};
static struct flowrow_gen setst_abs_row = {flowrow_sort,ABS_TYPE, ABS_TYPE,setst_sort};
static struct flowrow_gen setst_wild_row = {flowrow_sort,WILD_TYPE, WILD_TYPE,setst_sort};


gen_e flowrow_zero(sort_kind base_sort)
{
  switch (base_sort)
    {
    case setif_sort:
      return (gen_e)&setif_zero_row;
    case setst_sort:
      return (gen_e)&setst_zero_row;
    case term_sort:
      return (gen_e)&term_zero_row;
    default:
      {
	failure("No matching base sort: flowrow_zero\n");
	return NULL;
      }
    }
  
  return NULL;
}

gen_e flowrow_one(sort_kind base_sort)
{
  switch (base_sort)
    {
    case setif_sort:
      return (gen_e)&setif_one_row;
    case setst_sort:
      return (gen_e)&setst_one_row;
    case term_sort:
      return (gen_e)&term_one_row;
    default:
      {
	failure("No matching base sort: flowrow_one\n");
	return NULL;
      }
    }
  
  return NULL;
}

gen_e flowrow_abs(sort_kind base_sort)
{
  switch (base_sort)
    {
    case setif_sort:
      return (gen_e)&setif_abs_row;
    case setst_sort:
      return (gen_e)&setst_abs_row;
    case term_sort:
      return (gen_e)&term_abs_row;
    default:
      {
	failure("No matching base sort: flowrow_abs\n");
	return NULL;
      }
    }
  
  return NULL;
}

gen_e flowrow_wild(sort_kind base_sort)
{

  switch (base_sort)
    {
    case setif_sort:
      return (gen_e)&setif_wild_row;
    case setst_sort:
      return (gen_e)&setst_wild_row;
    case term_sort:
      return (gen_e)&term_wild_row;
    default:
      {
	failure("No matching base sort: flowrow_wild\n");
	return NULL;
      }
    }
  
  return NULL;
}

gen_e flowrow_fresh(const char *name,sort_kind base_sort)
{

  switch (base_sort)
    {
    case setif_sort:
      return 
    case setst_sort:
      return (gen_e)&setst_one_row;
    case term_sort:
      return (gen_e)&term_one_row;
    default:
      {
	failure("No matching base sort: flowrow_one\n");
	return NULL;
      }
    }
  
  return NULL;
}

gen_e flowrow_fresh_small(sort_kind base_sort)
{

  switch (base_sort)
    {
    case setif_sort:
      return (gen_e)&setif_one_row;
    case setst_sort:
      return (gen_e)&setst_one_row;
    case term_sort:
      return (gen_e)&term_one_row;
    default:
      {
	failure("No matching base sort: flowrow_one\n");
	return NULL;
      }
    }
  
  return NULL;
}

gen_e flowrow_fresh_large(sort_kind base_sort)
{

}

sort_kind flowrow_base_sort(gen_e e)
{

}
#endif /* NONSPEC */


gen_e flowrow_extract_field(const char *name, gen_e e)
{
  
  static bool field_eq(const flowrow_field f)
    {
      return (! strcmp(f->label,name));
    }
  
  if (flowrow_is_row(e))
    {
      flowrow_map fields = flowrow_get_fields(e);
      flowrow_field f = flowrow_map_find(fields,field_eq);

      if (f)
	return f->expr;
    }
  return NULL;
}

gen_e flowrow_extract_rest(gen_e e)
{
  if (flowrow_is_row(e))
    return flowrow_get_rest(e);
  else
    return NULL;
}

flowrow_map flowrow_extract_fields(gen_e e)
{
  if (flowrow_is_row(e))
    return flowrow_map_copy(flowrow_region,flowrow_get_fields(e));
  else
    return NULL;
}


bool flowrow_is_alias(gen_e e)
{
  return ((flowrow_gen)e)->type == ALIAS_TYPE;
}

bool flowrow_is_zero(gen_e e)
{
  return ((flowrow_gen)e)->type == ZERO_TYPE;
}

bool flowrow_is_one(gen_e e)
{
  return ((flowrow_gen)e)->type == ONE_TYPE;
}

bool flowrow_is_abs(gen_e e)
{
  return ((flowrow_gen)e)->type == ABS_TYPE;
}

bool flowrow_is_wild(gen_e e)
{
  return ((flowrow_gen)e)->type == WILD_TYPE;
}

bool flowrow_is_var(gen_e e)
{
  return ((flowrow_gen)e)->type == VAR_TYPE;
}

bool flowrow_is_row(gen_e e)
{
  return ((flowrow_gen)e)->type == ROW_TYPE;
}

void flowrow_init(void)
{
  flowrow_region = newregion();
  flowrow_hash = make_term_hash(flowrow_region);
}

static void flowrow_reset_stats(void)
{
  flowrow_stats.fresh = 0;
  flowrow_stats.fresh_small = 0;
  flowrow_stats.fresh_large = 0;

  flowrow_stats.rows_disjoint_wild = 0;
  flowrow_stats.rows_equal = 0;
  flowrow_stats.rows_zero_one_wild = 0;
  flowrow_stats.rows_l_inductive = 0;
  flowrow_stats.rows_r_inductive = 0;
  flowrow_stats.rows_disjoint_r1_minimal = 0;
  flowrow_stats.rows_disjoint_r1_var_r2_minimal = 0;
  flowrow_stats.rows_disjoint_r1_var_r2_maximal = 0;
  flowrow_stats.rows_disjoint_r1_var_r2_closed = 0;
  flowrow_stats.rows_disjoint_r1_var_r2_var_lt = 0;
  flowrow_stats.rows_disjoint_r1_var_r2_var_gt = 0;
  flowrow_stats.rows_equal_domains = 0;
  flowrow_stats.rows_nonempty_intersection = 0;
  flowrow_stats.rows_fresh = 0;
  flowrow_stats.rows_fresh_large = 0;
}

void flowrow_reset(void) deletes
{
  term_hash_delete(flowrow_hash);
  deleteregion_ptr(&flowrow_region);

  flowrow_reset_stats();

  flowrow_region = newregion();
  flowrow_hash = make_term_hash(flowrow_region);

}

static void fields_print(FILE *f,flowrow_map m,field_print_fn_ptr field_print) deletes
{
  flowrow_map_scanner scan;
  flowrow_field temp;

  flowrow_map_scan(m,&scan);

  if (flowrow_map_next(&scan,&temp))
    {
      fprintf(f,"%s : ",temp->label);
      
      if (field_print)
	field_print(f,temp->expr);
      else
	fprintf(f,"?");
    }

  while (flowrow_map_next(&scan,&temp))
    {
      fprintf(f,",%s : ",temp->label);
     
      if (field_print)
	field_print(f,temp->expr);
      else
 	fprintf(f,"?");
    }
}

void flowrow_print(FILE *f,get_stamp_fn_ptr get_stamp, 
		   field_print_fn_ptr field_print,gen_e row) deletes
{
  gen_e e = normalize_row(get_stamp,row);

  switch ( ((flowrow_gen)e)->type)
    {
    case ZERO_TYPE:
      fprintf(f, "0");
      break;
    case ONE_TYPE:
      fprintf(f, "1");
      break;
    case ABS_TYPE:
      fprintf(f, "abs");
      break;
    case WILD_TYPE:
      fprintf(f, "wild");
      break;
    case VAR_TYPE:
      fprintf(f, fv_get_name((flow_var)e));
      break;
    case ROW_TYPE:
      fprintf(f, "<");
      fields_print(f, flowrow_get_fields(e), field_print);
      fprintf(f, "|");
      flowrow_print(f, get_stamp, field_print, flowrow_get_rest(e));
      fprintf(f, ">");
      break;
    default:
      assert(0);
      break;
    }
}

void flowrow_print_stats(FILE *f)
{
  fprintf(f,"\n========== Flow Var Stats ==========\n");
  fprintf(f,"Fresh : %d\n",flowrow_stats.fresh); 
  fprintf(f,"Fresh Small : %d\n",flowrow_stats.fresh_small);
  fprintf(f,"Fresh Large : %d\n",flowrow_stats.fresh_large);
  fprintf(f,"=====================================\n");
}

DEFINE_LIST(flowrow_map,flowrow_field)