#ifndef QUALS_H
#define QUALS_H

#include "linkage.h"

typedef struct type_qualifier *qual;

#include <location.h>
#include "cqual.h"
#include "regions.h"

EXTERN_C_BEGIN

/* True if we should print out the qualifier constraint graph in dot
   form. */
extern int flag_print_quals_graph;

typedef enum { level_value, level_ref } level_qual_t;
typedef enum { sign_pos, sign_neg, sign_eq } sign_qual_t;

extern qual const_qual;
extern qual nonconst_qual;
extern qual volatile_qual;
extern qual restrict_qual;

/*
 * State transitions
 *
 * These functions are in general called in the order listed in this file
 */

void init_quals(void);        /* Called before any other functions in
				 quals.h are called. */
void end_define_pos(void);    /* Called when no more partial orders will
				 be defined.  You *must* call this function
			         before creating any qualifier variables. */
void finish_quals(void);      /* Called when no more constraints will
				 be generated. */
void dispose_quals(void);     /* Disposes of all memory internally
			         allocated by functions in quals.c.
			         All qualifiers and qualifier
			         variables become invalid after
			         calling this function. */

/*
 * Partial order elements
 */

/* Begin and end defining a partial order.  All the qualifiers created
   between calls to begin and end are exclusively related. */
void begin_po_qual(void);
void end_po_qual(void);

void set_po_dynamic(void);                /* Marks the current partial order
					     as dynamic */
void set_po_nonprop(void);                /* Marks the current partial order
					     as non-propagating */

qual add_qual(const char *name);          /* Make a new (constant) qualifier */
void add_qual_lt(qual left, qual right);  /* Add assumption left < right */
void add_color_qual(qual q, const char *color); /* Add color for qualifier */
void add_level_qual(qual q, level_qual_t lev);
                                          /* Assert that q qualifies lev */
void add_sign_qual(qual q, sign_qual_t sign);
                                          /* Assert that q has variance sign */

qual find_qual(const char *name);        /* Look up a qualifier */
level_qual_t level_qual(qual q);         /* Return the level of qualifier q */
sign_qual_t sign_qual(qual q);           /* Return the sign of qualifier q */
bool dynamic_qual(qual q);               /* Return TRUE iff q is dynamic */
bool nonprop_qual(qual q);               /* Return TRUE iff q is
					    non-propagating */
bool variable_qual(qual q);              /* Return TRUE iff q is a variable */
bool constant_qual(qual q);              /* Return TRUE iff q is a constant */

/*
 * Qualifier sets
 */

typedef struct Qual_Set *qual_set;
struct qual_set_elt_S;
typedef struct qual_set_elt_S *qual_set_scanner;
qual_set new_qual_set(region r);
bool qual_set_empty(qual_set quals);
bool qual_set_insert(qual_set quals, qual q);
bool qual_set_member(qual_set quals, qual q);
void qual_set_scan(qual_set quals, qual_set_scanner *);
qual qual_set_next(qual_set_scanner *);
int qual_set_size(qual_set quals);

#define scan_quals(var, scanner, list) \
  for (qual_set_scan(list, &scanner), var = qual_set_next(&scanner); \
       var; var = qual_set_next(&scanner))

/*
 * Qualifier variables
 */

/* Make a new, distinct qualifier variable */
qual make_qvar(const char *name, location loc, bool preferred);

/* Make a fresh qualifier variable with a unique name */
qual make_fresh_qvar(location loc);

location location_qual(qual);      /* Location qvar came from */
qual_set lbv_qual(qual);           /* Lower-bound variables of q */
qual_set ubv_qual(qual);           /* Upper-bound variables of q */
qual_set lbc_qual(qual);           /* Lower-bound constants of q */
qual_set ubc_qual(qual);           /* Upper-bound constants of q */
qual_set orig_lbc_qual(qual);      /* Lower-bound constants of q added
				      directly, not through transitivity */
qual_set orig_ubc_qual(qual);      /* Upper-bound constants of q added
				      directly, not through transitivity */

/*
 * Qualifier sequences
 */

typedef struct Qual_Seq_Element *qual_seq_element;
typedef struct Qual_Seq *qual_seq;
qual_seq new_qual_seq(region r);
bool qual_seq_empty(qual_seq qs);
qual_seq_element qual_seq_head(qual_seq qs);
qual_seq_element qual_seq_tail(qual_seq qs);
qual get_qual_seq_element(qual_seq_element qse);
qual_seq_element qual_seq_next(qual_seq_element qse);
qual_seq_element qual_seq_prev(qual_seq_element qse);
void qual_seq_push_left(qual_seq qs, qual q);
void qual_seq_push_right(qual_seq qs, qual q);
void qual_seq_pop_left(qual_seq qs);
void qual_seq_pop_right(qual_seq qs);

/*
 * Generate/solve constraints
 */

bool mkleq_qual(qual left, qual right);
bool mkeq_qual(qual left, qual right);
bool unify_qual(qual left, qual right);

/* Adds the conditional constraint l1<=r1 ==> l2<=r2.  This constraint
   is allowed only if at least one of {l1,r1} is a constant. */
bool cond_mkleq_qual(qual l1, qual r1, qual l2, qual r2);

/*
 * Utilities
 */

bool eq_qual(qual left, qual right);     /* Returns TRUE iff left and
					    right are the same.  Does
					    not generate a constraint. */
bool leq_qual(qual left, qual right);    /* Returns TRUE iff left <=
					    right.  Requires that at
					    least one of left, right
					    is a constant.  By defn,
					    returns TRUE if left and
					    right are in distinct
					    partial orders. */
int cmp_qual(qual left, qual right);     /* A total ordering on qualifiers.
					    Returns 0 if left = right, a
					    value <0 if left < right, or
					    a value >0 if left > right */

typedef int (*pr_qual_fn)(printf_func, qual);
int print_qual(printf_func, qual);       /* Print a qualifier, nice. */
int print_qual_raw(printf_func, qual);   /* Print a qualifier, ugly */
            /* Both functions return the number of characters printed. */
const char *name_qual(qual q);           /* Return the name of
					    qualifier q.  q may be a
					    constant or a variable. */
const char *color_qual(qual q);          /* Return the color of
					    qualifier q.  q may be a
					    constant or a variable. */

/* Traverse the qualifier graph */

/* Print the graph of qualifiers for q to file.  If po_bounds_only is
   true, then only print the graph showing how partial order elements
   affect q; otherwise print all qualifiers reachable from q. */
void print_qual_graph(qual q, const char *file, bool po_bounds_only);

typedef void (*qual_traverse_node_func)(qual q, void *arg);
typedef void (*qual_traverse_edge_func)(qual left, qual right, void *arg);

/* Call f(q1, q2, arg) for every edge q1->q2 on a shortest
   unidirectional path from qualifier variable q to constant qualifier
   c.  Does nothing if there is no such path.  If there are paths in
   both directions, traverses both. */
void traverse_shortest_path_edges(qual q, qual c, qual_traverse_edge_func f,
				  void *arg);

/* Traverse the edges in the qualifier graph.  po_bounds_only as above.
   arg is passed to f. */
void traverse_qual_graph_edges(qual q, bool po_bounds_only,
			       qual_traverse_edge_func f, void *arg);

/* Hacks */

/* Change dynamic quals from nonprop to regular quals for this pass */
void reset_dynamic_quals(void);

EXTERN_C_END

#endif