#include <engine/list.h>
#include <regions.h>
#include <engine/banshee.h>
#include <assert.h>
#include <stdio.h>
#include <engine/bool.h>
#include <engine/ufind.h>
#include <string.h>
#include <engine/setif-sort.h>
#include <engine/flowrow-sort.h>
#include <engine/setif-sort.h>
#define REF_ 11
#define REFPROJ0_ 12
#define REFPROJ1_ 13
#define REFPROJ2_ 14
#define LAM_ 15
#define LAMPROJ0_ 16
#define LAMPROJ1_ 17
#define LAMPROJ2_ 18
typedef gen_e label_term;
typedef gen_e_list label_term_list;
typedef struct flowrow_field *argterm_field;
typedef flowrow_map argterm_map;
typedef gen_e argterm;
typedef gen_e aterm;
typedef gen_e_list aterm_list;
stamp label_term_get_stamp(gen_e arg1);
bool label_term_is_var(gen_e arg1);
DECLARE_OPAQUE_LIST(label_term_list,gen_e)
label_term label_term_zero(void);
label_term label_term_one(void);
label_term label_term_fresh(const char *name);
label_term label_term_union(label_term_list exprs) deletes;
label_term label_term_inter(label_term_list exprs) deletes;
label_term label_term_constant(const char *name) deletes;
bool label_term_is_constant(label_term e,const char *name);
label_term_list label_term_tlb(label_term e) deletes;
void label_term_inclusion(label_term e1,label_term e2) deletes;
void label_term_unify(label_term e1,label_term e2) deletes;
void label_term_print(FILE* arg1,label_term arg2) deletes;
static bool label_term_res_proj(setif_var arg1,gen_e arg2) deletes;
static void label_term_con_match(gen_e arg1,gen_e arg2) deletes;
stamp argterm_get_stamp(gen_e arg1);
bool argterm_is_var(gen_e arg1);
DECLARE_OPAQUE_LIST(argterm_map,flowrow_field)
void argterm_print(FILE *f,argterm row) deletes;
stamp aterm_get_stamp(gen_e arg1);
bool aterm_is_var(gen_e arg1);
DECLARE_OPAQUE_LIST(aterm_list,gen_e)
aterm aterm_zero(void);
aterm aterm_one(void);
aterm aterm_fresh(const char *name);
aterm aterm_union(aterm_list exprs) deletes;
aterm aterm_inter(aterm_list exprs) deletes;
aterm aterm_constant(const char *name) deletes;
bool aterm_is_constant(aterm e,const char *name);
aterm_list aterm_tlb(aterm e) deletes;
void aterm_inclusion(aterm e1,aterm e2) deletes;
void aterm_unify(aterm e1,aterm e2) deletes;
aterm ref(label_term arg1,aterm arg2,aterm arg3) deletes;
struct ref_decon ref_decon(aterm arg1);
struct ref_
{
int type;
stamp st;
label_term f0;
aterm f1;
aterm f2;
};
struct ref_decon
{
label_term f0;
aterm f1;
aterm f2;
};
struct refProj0_
{
int type;
stamp st;
label_term f0;
};
static gen_e ref_pat0_con(gen_e arg1) deletes;
aterm ref_pat0(label_term arg1) deletes;
struct refProj1_
{
int type;
stamp st;
aterm f0;
};
static gen_e ref_pat1_con(gen_e arg1) deletes;
aterm ref_pat1(aterm arg1) deletes;
struct refProj2_
{
int type;
stamp st;
aterm f0;
};
static gen_e ref_pat2_con(gen_e arg1) deletes;
aterm ref_pat2(aterm arg1) deletes;
aterm lam(label_term arg1,argterm arg2,aterm arg3) deletes;
struct lam_decon lam_decon(aterm arg1);
struct lam_
{
int type;
stamp st;
label_term f0;
argterm f1;
aterm f2;
};
struct lam_decon
{
label_term f0;
argterm f1;
aterm f2;
};
struct lamProj0_
{
int type;
stamp st;
label_term f0;
};
static gen_e lam_pat0_con(gen_e arg1) deletes;
aterm lam_pat0(label_term arg1) deletes;
struct lamProj1_
{
int type;
stamp st;
argterm f0;
};
static gen_e lam_pat1_con(gen_e arg1) deletes;
aterm lam_pat1(argterm arg1) deletes;
struct lamProj2_
{
int type;
stamp st;
aterm f0;
};
static gen_e lam_pat2_con(gen_e arg1) deletes;
aterm lam_pat2(aterm arg1) deletes;
void aterm_print(FILE* arg1,aterm arg2) deletes;
static bool aterm_res_proj(setif_var arg1,gen_e arg2) deletes;
static void aterm_con_match(gen_e arg1,gen_e arg2) deletes;
stamp label_term_get_stamp(gen_e arg1)
{
return setif_get_stamp((gen_e)arg1);
}
bool label_term_is_var(gen_e arg1)
{
return setif_is_var((gen_e)arg1);
}
DEFINE_LIST(label_term_list,gen_e)
label_term label_term_zero(void)
{
return setif_zero();
}
label_term label_term_one(void)
{
return setif_one();
}
label_term label_term_fresh(const char *name)
{
return setif_fresh(name);
}
static label_term label_term_fresh_small(const char *name)
{
return setif_fresh_small(name);
}
static label_term label_term_fresh_large(const char *name)
{
return setif_fresh_large(name);
}
label_term label_term_union(label_term_list exprs) deletes
{
return setif_union(exprs);
}
label_term label_term_inter(label_term_list exprs) deletes
{
return setif_inter(exprs);
}
label_term label_term_constant(const char *name) deletes
{
return setif_constant(name);
}
bool label_term_is_constant(label_term e, const char *name)
{
if (setif_is_constant(e))
return (! strcmp(name,setif_get_constant_name(e)));
else return FALSE;
}
label_term_list label_term_tlb(label_term e) deletes
{
return setif_tlb(e);
}
void label_term_inclusion(label_term e1, label_term e2) deletes
{
setif_inclusion(label_term_con_match,label_term_res_proj,e1,e2);
}
static void label_term_inclusion_contra(label_term e1, label_term e2) deletes
{
setif_inclusion(label_term_con_match,label_term_res_proj,e2,e1);
}
void label_term_unify(label_term e1, label_term e2) deletes
{
setif_inclusion(label_term_con_match,label_term_res_proj,e1,e2);
setif_inclusion(label_term_con_match,label_term_res_proj,e2,e1);
}
void label_term_print(FILE* arg1,label_term arg2) deletes
{
switch(((setif_term)arg2)->type)
{
case VAR_TYPE:
fprintf(arg1,"%s",sv_get_name((setif_var)arg2));
break;
case ZERO_TYPE:
fprintf(arg1,"0");
break;
case ONE_TYPE:
fprintf(arg1,"1");
break;
case CONSTANT_TYPE:
fprintf(arg1,setif_get_constant_name(arg2));
break;
case UNION_TYPE:
{
gen_e_list list = setif_get_union(arg2);
gen_e_list_scanner scan;
gen_e temp;
gen_e_list_scan(list,&scan);
if (gen_e_list_next(&scan,&temp))
label_term_print(arg1,temp);
while (gen_e_list_next(&scan,&temp))
{
fprintf(arg1," || ");
label_term_print(arg1,temp);
}
}
break;
case INTER_TYPE:
{
gen_e_list list = setif_get_inter(arg2);
gen_e_list_scanner scan;
gen_e temp;
gen_e_list_scan(list,&scan);
if (gen_e_list_next(&scan,&temp))
label_term_print(arg1,temp);
while (gen_e_list_next(&scan,&temp))
{
fprintf(arg1," && ");
label_term_print(arg1,temp);
}
}
break;
default:
return ;
}
}
static bool label_term_res_proj(setif_var arg1,gen_e arg2) deletes
{
switch(((setif_term)arg2)->type)
{
default:
return FALSE;
}
return FALSE;
}
static void label_term_con_match(gen_e arg1,gen_e arg2) deletes
{
switch(((setif_term)arg1)->type)
{
default:
failure("Inconsistent system of constraints\n");
}
return;
}
stamp argterm_get_stamp(gen_e arg1)
{
return flowrow_get_stamp((gen_e)arg1);
}
bool argterm_is_var(gen_e arg1)
{
return flowrow_is_var((gen_e)arg1);
}
DEFINE_LIST(argterm_map,flowrow_field)
argterm_field argterm_make_field(const char *label, aterm expr)
{
flowrow_field result = ralloc(flowrow_region, struct flowrow_field);
result->label = rstrdup(flowrow_region,label);
result->expr = (gen_e) expr;
return result;
}
argterm argterm_zero(void)
{
return flowrow_zero();
}
argterm argterm_one(void)
{
return flowrow_one();
}
argterm argterm_abs(void)
{
return flowrow_abs();
}
argterm argterm_wild(void)
{
return flowrow_wild();
}
argterm argterm_fresh(const char *name)
{
return flowrow_fresh(name);
}
static argterm argterm_fresh_small(const char *name)
{
return flowrow_fresh_small(name);
}
static argterm argterm_fresh_large(const char *name)
{
return flowrow_fresh_large(name);
}
argterm argterm_row(argterm_map fields,argterm rest) deletes
{
return flowrow_row(aterm_get_stamp,fields,rest);
}
aterm argterm_extract_field(const char *field_name, argterm row)
{
return flowrow_extract_field(field_name,row);
}
argterm argterm_extract_rest(argterm row)
{
return flowrow_extract_rest(row);
}
argterm_map argterm_extract_fields(argterm row)
{
return flowrow_extract_fields(row);
}
void argterm_inclusion(argterm row1, argterm row2) deletes
{
flowrow_inclusion(aterm_fresh,aterm_get_stamp,aterm_inclusion,aterm_zero(), row1,row2);
}
static void argterm_inclusion_contra(argterm row1, argterm row2) deletes
{
flowrow_inclusion(aterm_fresh,aterm_get_stamp,aterm_inclusion,aterm_zero(), row2,row1);
}
void argterm_unify(argterm row1, argterm row2) deletes
{
argterm_inclusion(row1,row2);
argterm_inclusion(row2,row1);
}
void argterm_print(FILE *f,argterm row) deletes
{
flowrow_print(f,aterm_get_stamp,aterm_print,row);
}
stamp aterm_get_stamp(gen_e arg1)
{
return setif_get_stamp((gen_e)arg1);
}
bool aterm_is_var(gen_e arg1)
{
return setif_is_var((gen_e)arg1);
}
DEFINE_LIST(aterm_list,gen_e)
aterm aterm_zero(void)
{
return setif_zero();
}
aterm aterm_one(void)
{
return setif_one();
}
aterm aterm_fresh(const char *name)
{
return setif_fresh(name);
}
static aterm aterm_fresh_small(const char *name)
{
return setif_fresh_small(name);
}
static aterm aterm_fresh_large(const char *name)
{
return setif_fresh_large(name);
}
aterm aterm_union(aterm_list exprs) deletes
{
return setif_union(exprs);
}
aterm aterm_inter(aterm_list exprs) deletes
{
return setif_inter(exprs);
}
aterm aterm_constant(const char *name) deletes
{
return setif_constant(name);
}
bool aterm_is_constant(aterm e, const char *name)
{
if (setif_is_constant(e))
return (! strcmp(name,setif_get_constant_name(e)));
else return FALSE;
}
aterm_list aterm_tlb(aterm e) deletes
{
return setif_tlb(e);
}
void aterm_inclusion(aterm e1, aterm e2) deletes
{
setif_inclusion(aterm_con_match,aterm_res_proj,e1,e2);
}
static void aterm_inclusion_contra(aterm e1, aterm e2) deletes
{
setif_inclusion(aterm_con_match,aterm_res_proj,e2,e1);
}
void aterm_unify(aterm e1, aterm e2) deletes
{
setif_inclusion(aterm_con_match,aterm_res_proj,e1,e2);
setif_inclusion(aterm_con_match,aterm_res_proj,e2,e1);
}
bool aterm_is_ref(aterm e)
{
return ((setif_term)e)->type == 11;
}
aterm ref(label_term arg1,aterm arg2,aterm arg3) deletes
{
struct ref_ *ret;
stamp s[4];
s[0] = REF_;
s[1] = label_term_get_stamp((gen_e)arg1);
s[2] = aterm_get_stamp((gen_e)arg2);
s[3] = aterm_get_stamp((gen_e)arg3);
if ((ret = (struct ref_ *)term_hash_find(setif_hash,s,4)) == NULL)
{
ret = ralloc(setif_region,struct ref_);
ret->type = s[0];
ret->st = stamp_fresh();
ret->f0 = arg1;
ret->f1 = arg2;
ret->f2 = arg3;
term_hash_insert(setif_hash,(gen_e)ret,s,4);
}
return (aterm)ret;
}
struct ref_decon ref_decon(aterm arg1)
{
if (((setif_term)arg1)->type == REF_)
{
struct ref_* c = (struct ref_ *)arg1;
return (struct ref_decon){c->f0,c->f1,c->f2};
}
else
return (struct ref_decon){NULL,NULL,NULL};
}
static gen_e get_ref_proj0_arg(gen_e_list arg1)
{
gen_e temp;
gen_e_list_scanner scan;
gen_e_list_scan(arg1,&scan);
while (gen_e_list_next(&scan,&temp))
{
if (((setif_term)temp)->type == REFPROJ0_)
return (gen_e)((struct refProj0_ * ) temp)->f0;
}
return NULL;
}
label_term ref_proj0(aterm arg1) deletes
{
label_term c;
if (setif_is_var(arg1))
{
setif_var v = (setif_var)arg1;
c = (label_term)sv_get_ub_proj(v,get_ref_proj0_arg);
if (c != NULL)
return c;
else
{
aterm e;
gen_e lb;
gen_e_list_scanner scan;
c = label_term_fresh(NULL);
e = ref_pat0(c);
sv_add_ub_proj(v,e);
gen_e_list_scan(sv_get_lbs(v),&scan);
while (gen_e_list_next(&scan,&lb))
{
setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
}
return c;
}
}
else if ( ((setif_term)arg1)->type == REF_)
return ((struct ref_ * )arg1)->f0;
else if ( setif_is_zero(arg1))
return label_term_zero();
else if ( setif_is_union(arg1))
{
c = get_ref_proj0_arg(setif_get_proj_cache(arg1));
if (c != NULL)
return c;
else
{
aterm e;
c = label_term_fresh(NULL);
e = ref_pat0(c);
setif_set_proj_cache(arg1,e);
aterm_inclusion(arg1,e);
return c;
}
}
else
{
aterm e;
c = label_term_fresh(NULL);
e = ref_pat0(c);
aterm_inclusion(arg1,e);
return c;
}
}
static gen_e ref_pat0_con(gen_e arg1) deletes
{
return (gen_e)ref_pat0((label_term)arg1);
}
aterm ref_pat0(label_term arg1) deletes
{
struct refProj0_* ret;
stamp s[2];
s[0] = REFPROJ0_;
s[1] = label_term_get_stamp((gen_e)arg1);
if ((ret = (struct refProj0_ *)term_hash_find(setif_hash,s,2)) == NULL)
{
ret = ralloc(setif_region,struct refProj0_);
ret->type = REFPROJ0_;
ret->st = stamp_fresh();
ret->f0 = arg1;
term_hash_insert(setif_hash,(gen_e)ret,s,2);
}
return (aterm)ret;
}
static gen_e get_ref_proj1_arg(gen_e_list arg1)
{
gen_e temp;
gen_e_list_scanner scan;
gen_e_list_scan(arg1,&scan);
while (gen_e_list_next(&scan,&temp))
{
if (((setif_term)temp)->type == REFPROJ1_)
return (gen_e)((struct refProj1_ * ) temp)->f0;
}
return NULL;
}
aterm ref_proj1(aterm arg1) deletes
{
aterm c;
if (setif_is_var(arg1))
{
setif_var v = (setif_var)arg1;
c = (aterm)sv_get_ub_proj(v,get_ref_proj1_arg);
if (c != NULL)
return c;
else
{
aterm e;
gen_e lb;
gen_e_list_scanner scan;
c = aterm_fresh(NULL);
e = ref_pat1(c);
sv_add_ub_proj(v,e);
gen_e_list_scan(sv_get_lbs(v),&scan);
while (gen_e_list_next(&scan,&lb))
{
setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
}
return c;
}
}
else if ( ((setif_term)arg1)->type == REF_)
return ((struct ref_ * )arg1)->f1;
else if ( setif_is_zero(arg1))
return aterm_zero();
else if ( setif_is_union(arg1))
{
c = get_ref_proj1_arg(setif_get_proj_cache(arg1));
if (c != NULL)
return c;
else
{
aterm e;
c = aterm_fresh(NULL);
e = ref_pat1(c);
setif_set_proj_cache(arg1,e);
aterm_inclusion(arg1,e);
return c;
}
}
else
{
aterm e;
c = aterm_fresh(NULL);
e = ref_pat1(c);
aterm_inclusion(arg1,e);
return c;
}
}
static gen_e ref_pat1_con(gen_e arg1) deletes
{
return (gen_e)ref_pat1((aterm)arg1);
}
aterm ref_pat1(aterm arg1) deletes
{
struct refProj1_* ret;
stamp s[2];
s[0] = REFPROJ1_;
s[1] = aterm_get_stamp((gen_e)arg1);
if ((ret = (struct refProj1_ *)term_hash_find(setif_hash,s,2)) == NULL)
{
ret = ralloc(setif_region,struct refProj1_);
ret->type = REFPROJ1_;
ret->st = stamp_fresh();
ret->f0 = arg1;
term_hash_insert(setif_hash,(gen_e)ret,s,2);
}
return (aterm)ret;
}
static gen_e get_ref_proj2_arg(gen_e_list arg1)
{
gen_e temp;
gen_e_list_scanner scan;
gen_e_list_scan(arg1,&scan);
while (gen_e_list_next(&scan,&temp))
{
if (((setif_term)temp)->type == REFPROJ2_)
return (gen_e)((struct refProj2_ * ) temp)->f0;
}
return NULL;
}
aterm ref_proj2(aterm arg1) deletes
{
aterm c;
if (setif_is_var(arg1))
{
setif_var v = (setif_var)arg1;
c = (aterm)sv_get_ub_proj(v,get_ref_proj2_arg);
if (c != NULL)
return c;
else
{
aterm e;
gen_e lb;
gen_e_list_scanner scan;
c = aterm_fresh(NULL);
e = ref_pat2(c);
sv_add_ub_proj(v,e);
gen_e_list_scan(sv_get_lbs(v),&scan);
while (gen_e_list_next(&scan,&lb))
{
setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
}
return c;
}
}
else if ( ((setif_term)arg1)->type == REF_)
return ((struct ref_ * )arg1)->f2;
else if ( setif_is_zero(arg1))
return aterm_zero();
else if ( setif_is_union(arg1))
{
c = get_ref_proj2_arg(setif_get_proj_cache(arg1));
if (c != NULL)
return c;
else
{
aterm e;
c = aterm_fresh(NULL);
e = ref_pat2(c);
setif_set_proj_cache(arg1,e);
aterm_inclusion(arg1,e);
return c;
}
}
else
{
aterm e;
c = aterm_fresh(NULL);
e = ref_pat2(c);
aterm_inclusion(arg1,e);
return c;
}
}
static gen_e ref_pat2_con(gen_e arg1) deletes
{
return (gen_e)ref_pat2((aterm)arg1);
}
aterm ref_pat2(aterm arg1) deletes
{
struct refProj2_* ret;
stamp s[2];
s[0] = REFPROJ2_;
s[1] = aterm_get_stamp((gen_e)arg1);
if ((ret = (struct refProj2_ *)term_hash_find(setif_hash,s,2)) == NULL)
{
ret = ralloc(setif_region,struct refProj2_);
ret->type = REFPROJ2_;
ret->st = stamp_fresh();
ret->f0 = arg1;
term_hash_insert(setif_hash,(gen_e)ret,s,2);
}
return (aterm)ret;
}
bool aterm_is_lam(aterm e)
{
return ((setif_term)e)->type == 15;
}
aterm lam(label_term arg1,argterm arg2,aterm arg3) deletes
{
struct lam_ *ret;
stamp s[4];
s[0] = LAM_;
s[1] = label_term_get_stamp((gen_e)arg1);
s[2] = argterm_get_stamp((gen_e)arg2);
s[3] = aterm_get_stamp((gen_e)arg3);
if ((ret = (struct lam_ *)term_hash_find(setif_hash,s,4)) == NULL)
{
ret = ralloc(setif_region,struct lam_);
ret->type = s[0];
ret->st = stamp_fresh();
ret->f0 = arg1;
ret->f1 = arg2;
ret->f2 = arg3;
term_hash_insert(setif_hash,(gen_e)ret,s,4);
}
return (aterm)ret;
}
struct lam_decon lam_decon(aterm arg1)
{
if (((setif_term)arg1)->type == LAM_)
{
struct lam_* c = (struct lam_ *)arg1;
return (struct lam_decon){c->f0,c->f1,c->f2};
}
else
return (struct lam_decon){NULL,NULL,NULL};
}
static gen_e get_lam_proj0_arg(gen_e_list arg1)
{
gen_e temp;
gen_e_list_scanner scan;
gen_e_list_scan(arg1,&scan);
while (gen_e_list_next(&scan,&temp))
{
if (((setif_term)temp)->type == LAMPROJ0_)
return (gen_e)((struct lamProj0_ * ) temp)->f0;
}
return NULL;
}
label_term lam_proj0(aterm arg1) deletes
{
label_term c;
if (setif_is_var(arg1))
{
setif_var v = (setif_var)arg1;
c = (label_term)sv_get_ub_proj(v,get_lam_proj0_arg);
if (c != NULL)
return c;
else
{
aterm e;
gen_e lb;
gen_e_list_scanner scan;
c = label_term_fresh(NULL);
e = lam_pat0(c);
sv_add_ub_proj(v,e);
gen_e_list_scan(sv_get_lbs(v),&scan);
while (gen_e_list_next(&scan,&lb))
{
setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
}
return c;
}
}
else if ( ((setif_term)arg1)->type == LAM_)
return ((struct lam_ * )arg1)->f0;
else if ( setif_is_zero(arg1))
return label_term_zero();
else if ( setif_is_union(arg1))
{
c = get_lam_proj0_arg(setif_get_proj_cache(arg1));
if (c != NULL)
return c;
else
{
aterm e;
c = label_term_fresh(NULL);
e = lam_pat0(c);
setif_set_proj_cache(arg1,e);
aterm_inclusion(arg1,e);
return c;
}
}
else
{
aterm e;
c = label_term_fresh(NULL);
e = lam_pat0(c);
aterm_inclusion(arg1,e);
return c;
}
}
static gen_e lam_pat0_con(gen_e arg1) deletes
{
return (gen_e)lam_pat0((label_term)arg1);
}
aterm lam_pat0(label_term arg1) deletes
{
struct lamProj0_* ret;
stamp s[2];
s[0] = LAMPROJ0_;
s[1] = label_term_get_stamp((gen_e)arg1);
if ((ret = (struct lamProj0_ *)term_hash_find(setif_hash,s,2)) == NULL)
{
ret = ralloc(setif_region,struct lamProj0_);
ret->type = LAMPROJ0_;
ret->st = stamp_fresh();
ret->f0 = arg1;
term_hash_insert(setif_hash,(gen_e)ret,s,2);
}
return (aterm)ret;
}
static gen_e get_lam_proj1_arg(gen_e_list arg1)
{
gen_e temp;
gen_e_list_scanner scan;
gen_e_list_scan(arg1,&scan);
while (gen_e_list_next(&scan,&temp))
{
if (((setif_term)temp)->type == LAMPROJ1_)
return (gen_e)((struct lamProj1_ * ) temp)->f0;
}
return NULL;
}
argterm lam_proj1(aterm arg1) deletes
{
argterm c;
if (setif_is_var(arg1))
{
setif_var v = (setif_var)arg1;
c = (argterm)sv_get_ub_proj(v,get_lam_proj1_arg);
if (c != NULL)
return c;
else
{
aterm e;
gen_e lb;
gen_e_list_scanner scan;
c = argterm_fresh(NULL);
e = lam_pat1(c);
sv_add_ub_proj(v,e);
gen_e_list_scan(sv_get_lbs(v),&scan);
while (gen_e_list_next(&scan,&lb))
{
setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
}
return c;
}
}
else if ( ((setif_term)arg1)->type == LAM_)
return ((struct lam_ * )arg1)->f1;
else if ( setif_is_zero(arg1))
return argterm_zero();
else if ( setif_is_union(arg1))
{
c = get_lam_proj1_arg(setif_get_proj_cache(arg1));
if (c != NULL)
return c;
else
{
aterm e;
c = argterm_fresh(NULL);
e = lam_pat1(c);
setif_set_proj_cache(arg1,e);
aterm_inclusion(arg1,e);
return c;
}
}
else
{
aterm e;
c = argterm_fresh(NULL);
e = lam_pat1(c);
aterm_inclusion(arg1,e);
return c;
}
}
static gen_e lam_pat1_con(gen_e arg1) deletes
{
return (gen_e)lam_pat1((argterm)arg1);
}
aterm lam_pat1(argterm arg1) deletes
{
struct lamProj1_* ret;
stamp s[2];
s[0] = LAMPROJ1_;
s[1] = argterm_get_stamp((gen_e)arg1);
if ((ret = (struct lamProj1_ *)term_hash_find(setif_hash,s,2)) == NULL)
{
ret = ralloc(setif_region,struct lamProj1_);
ret->type = LAMPROJ1_;
ret->st = stamp_fresh();
ret->f0 = arg1;
term_hash_insert(setif_hash,(gen_e)ret,s,2);
}
return (aterm)ret;
}
static gen_e get_lam_proj2_arg(gen_e_list arg1)
{
gen_e temp;
gen_e_list_scanner scan;
gen_e_list_scan(arg1,&scan);
while (gen_e_list_next(&scan,&temp))
{
if (((setif_term)temp)->type == LAMPROJ2_)
return (gen_e)((struct lamProj2_ * ) temp)->f0;
}
return NULL;
}
aterm lam_proj2(aterm arg1) deletes
{
aterm c;
if (setif_is_var(arg1))
{
setif_var v = (setif_var)arg1;
c = (aterm)sv_get_ub_proj(v,get_lam_proj2_arg);
if (c != NULL)
return c;
else
{
aterm e;
gen_e lb;
gen_e_list_scanner scan;
c = aterm_fresh(NULL);
e = lam_pat2(c);
sv_add_ub_proj(v,e);
gen_e_list_scan(sv_get_lbs(v),&scan);
while (gen_e_list_next(&scan,&lb))
{
setif_inclusion(aterm_con_match,aterm_res_proj,lb,e);
}
return c;
}
}
else if ( ((setif_term)arg1)->type == LAM_)
return ((struct lam_ * )arg1)->f2;
else if ( setif_is_zero(arg1))
return aterm_zero();
else if ( setif_is_union(arg1))
{
c = get_lam_proj2_arg(setif_get_proj_cache(arg1));
if (c != NULL)
return c;
else
{
aterm e;
c = aterm_fresh(NULL);
e = lam_pat2(c);
setif_set_proj_cache(arg1,e);
aterm_inclusion(arg1,e);
return c;
}
}
else
{
aterm e;
c = aterm_fresh(NULL);
e = lam_pat2(c);
aterm_inclusion(arg1,e);
return c;
}
}
static gen_e lam_pat2_con(gen_e arg1) deletes
{
return (gen_e)lam_pat2((aterm)arg1);
}
aterm lam_pat2(aterm arg1) deletes
{
struct lamProj2_* ret;
stamp s[2];
s[0] = LAMPROJ2_;
s[1] = aterm_get_stamp((gen_e)arg1);
if ((ret = (struct lamProj2_ *)term_hash_find(setif_hash,s,2)) == NULL)
{
ret = ralloc(setif_region,struct lamProj2_);
ret->type = LAMPROJ2_;
ret->st = stamp_fresh();
ret->f0 = arg1;
term_hash_insert(setif_hash,(gen_e)ret,s,2);
}
return (aterm)ret;
}
void aterm_print(FILE* arg1,aterm arg2) deletes
{
switch(((setif_term)arg2)->type)
{
case VAR_TYPE:
fprintf(arg1,"%s",sv_get_name((setif_var)arg2));
break;
case ZERO_TYPE:
fprintf(arg1,"0");
break;
case ONE_TYPE:
fprintf(arg1,"1");
break;
case CONSTANT_TYPE:
fprintf(arg1,setif_get_constant_name(arg2));
break;
case UNION_TYPE:
{
gen_e_list list = setif_get_union(arg2);
gen_e_list_scanner scan;
gen_e temp;
gen_e_list_scan(list,&scan);
if (gen_e_list_next(&scan,&temp))
aterm_print(arg1,temp);
while (gen_e_list_next(&scan,&temp))
{
fprintf(arg1," || ");
aterm_print(arg1,temp);
}
}
break;
case INTER_TYPE:
{
gen_e_list list = setif_get_inter(arg2);
gen_e_list_scanner scan;
gen_e temp;
gen_e_list_scan(list,&scan);
if (gen_e_list_next(&scan,&temp))
aterm_print(arg1,temp);
while (gen_e_list_next(&scan,&temp))
{
fprintf(arg1," && ");
aterm_print(arg1,temp);
}
}
break;
case REF_:
{
fprintf(arg1,"ref(");
label_term_print(arg1,((struct ref_ *)arg2)->f0);
fprintf(arg1,",");
aterm_print(arg1,((struct ref_ *)arg2)->f1);
fprintf(arg1,",");
aterm_print(arg1,((struct ref_ *)arg2)->f2);
fprintf(arg1,")");
}
break;
case LAM_:
{
fprintf(arg1,"lam(");
label_term_print(arg1,((struct lam_ *)arg2)->f0);
fprintf(arg1,",");
argterm_print(arg1,((struct lam_ *)arg2)->f1);
fprintf(arg1,",");
aterm_print(arg1,((struct lam_ *)arg2)->f2);
fprintf(arg1,")");
}
break;
case REFPROJ0_:
{
fprintf(arg1,"Proj[ref,0,");
label_term_print(arg1,((struct refProj0_ *)arg2)->f0);
fprintf(arg1,"]");
}
break;
case REFPROJ1_:
{
fprintf(arg1,"Proj[ref,1,");
aterm_print(arg1,((struct refProj1_ *)arg2)->f0);
fprintf(arg1,"]");
}
break;
case REFPROJ2_:
{
fprintf(arg1,"Proj[ref,2,");
aterm_print(arg1,((struct refProj2_ *)arg2)->f0);
fprintf(arg1,"]");
}
break;
case LAMPROJ0_:
{
fprintf(arg1,"Proj[lam,0,");
label_term_print(arg1,((struct lamProj0_ *)arg2)->f0);
fprintf(arg1,"]");
}
break;
case LAMPROJ1_:
{
fprintf(arg1,"Proj[lam,1,");
argterm_print(arg1,((struct lamProj1_ *)arg2)->f0);
fprintf(arg1,"]");
}
break;
case LAMPROJ2_:
{
fprintf(arg1,"Proj[lam,2,");
aterm_print(arg1,((struct lamProj2_ *)arg2)->f0);
fprintf(arg1,"]");
}
break;
default:
return ;
}
}
static bool aterm_res_proj(setif_var arg1,gen_e arg2) deletes
{
switch(((setif_term)arg2)->type)
{
case REFPROJ0_:
return setif_proj_merge(arg1,(gen_e)((struct refProj0_ *)arg2)->f0,get_ref_proj0_arg,ref_pat0_con,(fresh_large_fn_ptr)label_term_fresh_large,(incl_fn_ptr)label_term_inclusion,aterm_inclusion);
break;
case REFPROJ1_:
return setif_proj_merge(arg1,(gen_e)((struct refProj1_ *)arg2)->f0,get_ref_proj1_arg,ref_pat1_con,(fresh_large_fn_ptr)aterm_fresh_large,(incl_fn_ptr)aterm_inclusion_contra,aterm_inclusion);
break;
case REFPROJ2_:
return setif_proj_merge(arg1,(gen_e)((struct refProj2_ *)arg2)->f0,get_ref_proj2_arg,ref_pat2_con,(fresh_large_fn_ptr)aterm_fresh_large,(incl_fn_ptr)aterm_inclusion,aterm_inclusion);
break;
case LAMPROJ0_:
return setif_proj_merge(arg1,(gen_e)((struct lamProj0_ *)arg2)->f0,get_lam_proj0_arg,lam_pat0_con,(fresh_large_fn_ptr)label_term_fresh_large,(incl_fn_ptr)label_term_inclusion,aterm_inclusion);
break;
case LAMPROJ1_:
return setif_proj_merge(arg1,(gen_e)((struct lamProj1_ *)arg2)->f0,get_lam_proj1_arg,lam_pat1_con,(fresh_large_fn_ptr)argterm_fresh_large,(incl_fn_ptr)argterm_inclusion_contra,aterm_inclusion);
break;
case LAMPROJ2_:
return setif_proj_merge(arg1,(gen_e)((struct lamProj2_ *)arg2)->f0,get_lam_proj2_arg,lam_pat2_con,(fresh_large_fn_ptr)aterm_fresh_large,(incl_fn_ptr)aterm_inclusion,aterm_inclusion);
break;
default:
return FALSE;
}
return FALSE;
}
static void aterm_con_match(gen_e arg1,gen_e arg2) deletes
{
switch(((setif_term)arg1)->type)
{
case REF_:
switch(((setif_term)arg2)->type)
{
case REF_:
{
label_term_inclusion(((struct ref_ *)arg1)->f0,((struct ref_ *)arg2)->f0);
aterm_inclusion_contra(((struct ref_ *)arg1)->f1,((struct ref_ *)arg2)->f1);
aterm_inclusion(((struct ref_ *)arg1)->f2,((struct ref_ *)arg2)->f2);
}
break;
case REFPROJ0_:
label_term_inclusion(((struct ref_ *)arg1)->f0,((struct refProj0_ *)arg2)->f0);
break;
case REFPROJ1_:
aterm_inclusion_contra(((struct ref_ *)arg1)->f1,((struct refProj1_ *)arg2)->f0);
break;
case REFPROJ2_:
aterm_inclusion(((struct ref_ *)arg1)->f2,((struct refProj2_ *)arg2)->f0);
break;
case LAMPROJ0_:
return ;
break;
case LAMPROJ1_:
return ;
break;
case LAMPROJ2_:
return ;
break;
default:
failure("Inconsistent system of constraints\n");
}
break;
case LAM_:
switch(((setif_term)arg2)->type)
{
case LAM_:
{
label_term_inclusion(((struct lam_ *)arg1)->f0,((struct lam_ *)arg2)->f0);
argterm_inclusion_contra(((struct lam_ *)arg1)->f1,((struct lam_ *)arg2)->f1);
aterm_inclusion(((struct lam_ *)arg1)->f2,((struct lam_ *)arg2)->f2);
}
break;
case LAMPROJ0_:
label_term_inclusion(((struct lam_ *)arg1)->f0,((struct lamProj0_ *)arg2)->f0);
break;
case LAMPROJ1_:
argterm_inclusion_contra(((struct lam_ *)arg1)->f1,((struct lamProj1_ *)arg2)->f0);
break;
case LAMPROJ2_:
aterm_inclusion(((struct lam_ *)arg1)->f2,((struct lamProj2_ *)arg2)->f0);
break;
case REFPROJ0_:
return ;
break;
case REFPROJ1_:
return ;
break;
case REFPROJ2_:
return ;
break;
default:
failure("Inconsistent system of constraints\n");
}
break;
default:
failure("Inconsistent system of constraints\n");
}
return;
}
void andersen_terms_init(void)
{
engine_init();
setif_init();
setif_init();
flowrow_init();
}
void andersen_terms_reset(void) deletes
{
setif_reset();
setif_reset();
flowrow_reset();
engine_reset();
}
void andersen_terms_stats(FILE * arg1)
{
engine_stats(arg1);
}
void andersen_terms_print_graph(FILE * arg1)
{
print_constraint_graphs(arg1);
}