101 lines
2.9 KiB
C
101 lines
2.9 KiB
C
|
/*
|
||
|
|
|
||
|
|
DO NOT edit this file
|
||
|
|
|
||
|
|
*/
|
||
|
|
#ifndef ANDERSEN_TERMS_H
|
||
|
|
#define ANDERSEN_TERMS_H
|
||
|
|
#include <engine/list.h>
|
||
|
|
#include <stdio.h>
|
||
|
|
#include <engine/bool.h>
|
||
|
|
|
||
|
|
|
||
|
|
typedef struct label_term_* label_term;
|
||
|
|
typedef struct argterm_* argterm;
|
||
|
|
typedef struct argterm_field_* argterm_field;
|
||
|
|
typedef struct aterm_* aterm;
|
||
|
|
|
||
|
|
extern bool flag_merge_projections;
|
||
|
|
extern bool flag_eliminate_cycles;
|
||
|
|
DECLARE_LIST(label_term_list,label_term)
|
||
|
|
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) ;
|
||
|
|
label_term label_term_inter(label_term_list exprs) ;
|
||
|
|
label_term label_term_constant(const char *name) ;
|
||
|
|
bool label_term_is_constant(label_term e,const char *name);
|
||
|
|
void label_term_inclusion(label_term e1,label_term e2) ;
|
||
|
|
void label_term_unify(label_term e1,label_term e2) ;
|
||
|
|
label_term_list label_term_tlb(label_term e) ;
|
||
|
|
|
||
|
|
void label_term_print(FILE* arg1,label_term arg2) ;
|
||
|
|
DECLARE_LIST(argterm_map,argterm_field)
|
||
|
|
argterm_field argterm_make_field(const char *label,aterm expr);
|
||
|
|
argterm argterm_zero(void);
|
||
|
|
argterm argterm_one(void);
|
||
|
|
argterm argterm_abs(void);
|
||
|
|
argterm argterm_wild(void);
|
||
|
|
argterm argterm_fresh(const char *name);
|
||
|
|
argterm argterm_row(argterm_map fields,argterm rest) ;
|
||
|
|
aterm argterm_extract_field(const char *field_name,argterm row);
|
||
|
|
argterm argterm_extract_rest(argterm row);
|
||
|
|
argterm_map argterm_extract_fields(argterm row);
|
||
|
|
void argterm_inclusion(argterm row1,argterm row2) ;
|
||
|
|
void argterm_unify(argterm row1,argterm row2) ;
|
||
|
|
void argterm_print(FILE *f,argterm row) ;
|
||
|
|
|
||
|
|
DECLARE_LIST(aterm_list,aterm)
|
||
|
|
aterm aterm_zero(void);
|
||
|
|
aterm aterm_one(void);
|
||
|
|
aterm aterm_fresh(const char *name);
|
||
|
|
aterm aterm_union(aterm_list exprs) ;
|
||
|
|
aterm aterm_inter(aterm_list exprs) ;
|
||
|
|
aterm aterm_constant(const char *name) ;
|
||
|
|
bool aterm_is_constant(aterm e,const char *name);
|
||
|
|
void aterm_inclusion(aterm e1,aterm e2) ;
|
||
|
|
void aterm_unify(aterm e1,aterm e2) ;
|
||
|
|
aterm_list aterm_tlb(aterm e) ;
|
||
|
|
|
||
|
|
bool aterm_is_ref(aterm e);
|
||
|
|
aterm ref(label_term arg1,aterm arg2,aterm arg3) ;
|
||
|
|
struct ref_decon ref_decon(aterm arg1);
|
||
|
|
struct ref_decon
|
||
|
|
{
|
||
|
|
label_term f0;
|
||
|
|
aterm f1;
|
||
|
|
aterm f2;
|
||
|
|
};
|
||
|
|
label_term ref_proj0(aterm arg1) ;
|
||
|
|
aterm ref_pat0(label_term arg1) ;
|
||
|
|
aterm ref_proj1(aterm arg1) ;
|
||
|
|
aterm ref_pat1(aterm arg1) ;
|
||
|
|
aterm ref_proj2(aterm arg1) ;
|
||
|
|
aterm ref_pat2(aterm arg1) ;
|
||
|
|
bool aterm_is_lam(aterm e);
|
||
|
|
aterm lam(label_term arg1,argterm arg2,aterm arg3) ;
|
||
|
|
struct lam_decon lam_decon(aterm arg1);
|
||
|
|
struct lam_decon
|
||
|
|
{
|
||
|
|
label_term f0;
|
||
|
|
argterm f1;
|
||
|
|
aterm f2;
|
||
|
|
};
|
||
|
|
label_term lam_proj0(aterm arg1) ;
|
||
|
|
aterm lam_pat0(label_term arg1) ;
|
||
|
|
argterm lam_proj1(aterm arg1) ;
|
||
|
|
aterm lam_pat1(argterm arg1) ;
|
||
|
|
aterm lam_proj2(aterm arg1) ;
|
||
|
|
aterm lam_pat2(aterm arg1) ;
|
||
|
|
void aterm_print(FILE* arg1,aterm arg2) ;
|
||
|
|
/*
|
||
|
|
|
||
|
|
Init/reset engine, print constraint graphs
|
||
|
|
|
||
|
|
*/
|
||
|
|
void andersen_terms_init(void);
|
||
|
|
void andersen_terms_reset(void) ;
|
||
|
|
void andersen_terms_stats(FILE * arg1);
|
||
|
|
void andersen_terms_print_graph(FILE * arg1);
|
||
|
|
#endif
|