TaPAS  0.2
batof-formulas.h
Go to the documentation of this file.
1 /*
2  * batof-formulas.h -- add a comment about this file
3  *
4  * This file is a part of the PresTAF project.
5  *
6  * Copyright (C) 2010 CNRS UMR 5800 & Université Bordeaux I (see AUTHORS file).
7  *
8  * This program is free software; you can redistribute it and/or modify
9  * it under the terms of the GNU General Public License as published by
10  * the Free Software Foundation; either version 2 of the License, or
11  * (at your option) any later version.
12  *
13  * This program is distributed in the hope that it will be useful,
14  * but WITHOUT ANY WARRANTY; without even the implied warranty of
15  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16  * GNU General Public License for more details.
17  *
18  * You should have received a copy of the GNU General Public License
19  * along with this program; if not, write to the Free Software
20  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
21  * 02110-1301 USA
22  */
23 
29 #ifndef __BATOF_FORMULAS_H__
30 # define __BATOF_FORMULAS_H__
31 
32 # include "prestaf-batof-p.h"
33 
34 struct global_definition
35 {
36  ccl_ustring id;
37  armoise_tree *formula;
38 };
39 
40 struct msa2form_compilation_data
41 {
42  int m;
43  ccl_ustring *varnames;
44  ccl_ustring nat_power_m_id;
45  ccl_ustring Z_power_m_id;
46  ccl_list *definitions;
47  ccl_hash *V_defs;
48  ccl_hash *G_defs;
49  ccl_hash *vectors_defs;
50  ccl_hash *H_defs;
51  ccl_hash *patterns_defs;
52 
53  ccl_hash *mi;
54  ccl_hash *def_ids;
55 };
56 
57  /* --------------- */
58 
59 extern void
60 btf_init_compilation_data (struct msa2form_compilation_data *data, int m,
61  const char * const *varnames);
62 
63 extern void
64 btf_clear_compilation_data (struct msa2form_compilation_data *data);
65 
66 extern armoise_tree *
67 btf_add_definition (struct msa2form_compilation_data *data, const char *s,
68  armoise_tree *F);
69 
76 extern armoise_tree *
77 btf_form_crt_synform (struct msa2form_compilation_data *cd, armoise_tree *P);
78 
79 extern armoise_tree *
80 btf_form_crt_definition (const char *id, armoise_tree *P);
81 
82 extern armoise_tree *
83 btf_form_crt_V_definition (struct msa2form_compilation_data *cd,
84  tla_vsp_t V);
85 
86 extern armoise_tree *
87 btf_form_crt_Zm_definition (const char *id, int m);
88 
92 extern armoise_tree *
93 btf_form_crt_VH_definition (struct msa2form_compilation_data *cd,
94  const char *id, tla_vec_t rho, tla_vec_t xhi,
95  tla_vsp_t V, tla_vec_t alpha, int op);
96 
97 # define btf_form_get_def_id(def) ((def)->child->value.id_value)
98 
99 extern armoise_tree *
100 btf_form_crt_H_definition (struct msa2form_compilation_data *cd,
101  ccl_ustring Vid, tla_vec_t alpha, int op);
102 
103 extern armoise_tree *
104 btf_form_crt_PH_definition (struct msa2form_compilation_data *cd,
105  const char *id, ccl_ustring P,
106  tla_vec_t rho, tla_vec_t xhi,
107  tla_vsp_t V, tla_vec_t alpha, int op);
108 
109 extern armoise_tree *
110 btf_form_crt_P_definition (struct msa2form_compilation_data *cd,
111  const char *id, tla_vec_t rho_w, ccl_list *B,
112  tla_group_t G);
113 
114 extern armoise_tree *
115 btf_form_crt_pattern_definition (struct msa2form_compilation_data *cd,
116  ccl_list *B, tla_group_t G);
117 
118 extern armoise_tree *
119 btf_form_crt_G_definition (struct msa2form_compilation_data *cd, tla_group_t G);
120 
121 extern armoise_tree *
122 btf_form_crt_vec_definition (struct msa2form_compilation_data *cd,
123  tla_vec_t v);
124 
125 extern armoise_tree *
126 btf_form_trivial_predicate (struct msa2form_compilation_data *cd, int is_empty);
127 
128 extern armoise_tree *
129 btf_form_crt_vector_of_ids (int m, ccl_ustring *X);
130 
131 extern armoise_tree *
132 btf_form_zero_vec_predicate (int m);
133 
134 extern armoise_tree *
135 btf_form_crt_x_in_nat_power_m (struct msa2form_compilation_data *cd);
136 
137 extern armoise_tree *
138 btf_form_crt_nat_power_m (struct msa2form_compilation_data *cd);
139 
140 extern armoise_tree *
141 btf_form_crt_Z_power_m (struct msa2form_compilation_data *cd);
142 
143 extern armoise_tree *
144 btf_form_crt_gamma (int m, ccl_ustring *dummyX, armoise_tree *phi, int b,
145  int index);
146 
147 extern armoise_tree *
148 btf_form_crt_e_m_i_predicate (int m, int i);
149 
150 extern armoise_tree *
151 btf_form_vec_to_armoise_predicate (tla_vec_t v);
152 
153 extern armoise_tree *
154 btf_form_vec_to_armoise_term (tla_vec_t v);
155 
156 extern armoise_tree *
157 btf_form_simplify_predicate (armoise_tree *P);
158 
159 #endif /* ! __BATOF_FORMULAS_H__ */
ccl_parse_tree_st
Structure encoding of a parse-tree node.
Definition: ccl-parse-tree.h:107
btf_form_crt_VH_definition
armoise_tree * btf_form_crt_VH_definition(struct msa2form_compilation_data *cd, const char *id, tla_vec_t rho, tla_vec_t xhi, tla_vsp_t V, tla_vec_t alpha, int op)
ccl_list
struct ccl_list_st ccl_list
Type of a generic list.
Definition: ccl-list.h:33
ccl_ustring
char * ccl_ustring
Alias type for strings that are stored in an internal dictionary and then can be used as identifiers ...
Definition: ccl-string.h:34
ccl_hash
struct ccl_hash_st ccl_hash
abstract type of an hash table.
Definition: ccl-hash.h:57
btf_form_crt_synform
armoise_tree * btf_form_crt_synform(struct msa2form_compilation_data *cd, armoise_tree *P)
Generated by   doxygen 1.8.5