+++ /dev/null
-/*
-
-DO NOT edit this file
-
-*/
-#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);
-}
-
OSDN Git Service
