]> matita.cs.unibo.it Git - helm.git/blob - helm/metadata/create_V7_mowgli/METADATA/sthandler_ind.c
- the mathql interpreter is not helm-dependent any more
[helm.git] / helm / metadata / create_V7_mowgli / METADATA / sthandler_ind.c
1 /*********************************************************************/
2 /*  Copyright (C) 2000, HELM Team                                    */ 
3 /*                                                                   */
4 /* This file is part of HELM, an Hypertextual, Electronic            */
5 /* Library of Mathematics, developed at the Computer Science         */
6 /* Department, University of Bologna, Italy.                         */
7 /*                                                                   */
8 /* HELM is free software; you can redistribute it and/or             */
9 /* modify it under the terms of the GNU General Public License       */
10 /* as published by the Free Software Foundation; either version 2    */
11 /* of the License, or (at your option) any later version.            */
12 /*                                                                   */
13 /* HELM 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 HELM; if not, write to the Free Software               */
20 /* Foundation, Inc., 59 Temple Place - Suite 330, Boston,            */
21 /* MA  02111-1307, USA.                                              */
22 /*                                                                   */
23 /* For details, see the HELM World-Wide-Web page,                    */
24 /* http://cs.unibo.it/helm/.                                         */
25  /*********************************************************************/
26
27 /****************************************************************/
28 /*                        STHANDLER.C                           */
29 /****************************************************************/
30 /* This module supplies routines for symbol table handling.     */
31 /* - init_symbol_table(): it initializes the symbol table       */
32 /*                        to void.                              */
33 /* - search_bucket(): it searches the symbol table for the      */
34 /*                    bucket containing a given identifier, and */
35 /*                    inserts it if it is not present;          */
36 /****************************************************************/
37 /*           First draft 11/12/2001, by Andrea Asperti          */
38 /****************************************************************/
39
40 /****************************************************************/
41 /* 1. Inclusion of header files.                                */
42 /****************************************************************/
43
44 #include                <stdio.h>
45 #include                <malloc.h>
46
47 /****************************************************************/
48 /* 2. Declarations                                              */
49 /****************************************************************/
50
51
52 #define         DICTSIZE                        211
53 #define         HASH1                           4
54 #define         HASH2                           0xf0000000
55 #define         HASH3                           24
56 #define         EOS                             '\0'
57
58 #define                 INBODY    0
59 #define                 MAINHYP   1
60 #define                 INHYP     2
61 #define                 INCONCL   3
62 #define                 MAINCONCL 4
63 #define                 INTYPE    5
64 #define                 NOTFOUND  6
65
66 /****************************************************************/
67 /* 3. Types.                                                    */
68 /****************************************************************/
69
70 struct int_list {
71                 int                     val;
72                 struct int_list         *next;
73                   }; 
74
75 struct st_bucket {
76                 char                    *id;
77                                                 /* identifier */
78                 int                     main_depth;
79                 struct int_list         *depths;
80                 struct st_bucket        *next_st_bucket;
81                                                 /* next bucket in the list */
82                 struct st_bucket        *all_next;
83                                                /* all buckets in symbol
84                                                   table are linked together */
85                 int                     pos[5];
86
87                   };                              
88
89 struct st_bucket    *dictionary[DICTSIZE];
90                                /* pointers to bucket lists */
91
92 /****************************************************************/
93 /* 4. Local functions.                                          */
94 /****************************************************************/
95 struct int_list  *add(struct int_list  *,int);
96
97 /****************************************************************/
98 /* 5. Definitions of functions to be exported.                  */
99 /****************************************************************/
100
101 struct st_bucket        *all;
102
103  /* The following function initializes the symbol table to NULL */
104 void init_symbol_table()
105 {
106         struct st_bucket        *st;
107         int                     i;
108
109         /* initialize the dictionary */
110         for (i = 0; i < DICTSIZE; i++)
111                 dictionary[i] = NULL;
112         all = NULL;
113 }
114
115  /* The following function searches the symbol table for an identifier */
116  /* and inserts it if it is not present. 
117  /* The bucket associated with the given identifier */
118  /* becomes the first one in its list. */
119
120 search_bucket(id, where, depth)
121         char            *id;
122                                         /* identifier */
123         int             where;
124         int             depth;
125 {
126         int             dict_index;
127                                         /* value returned by the */
128                                         /* hash function */
129         struct st_bucket
130                         *prev,
131                         *curr;
132
133         struct st_bucket *st;
134
135         /* apply the hash function */
136         dict_index = hash_pjw(id);
137         /* fprintf(stderr,"%d\n", dict_index); fflush(stdout); */
138         
139         /* scan the bucket list indicated by the hash function */
140         prev = curr = dictionary[dict_index];
141         while ((curr != NULL) && (strcmp(id, curr->id)))
142           {
143             prev = curr;
144             curr = curr->next_st_bucket;
145           }
146         if (curr == NULL)
147           /* the identifier is not in the list */
148           {
149             allocate_bucket(&st,id,where);
150             if (where == MAINCONCL)
151               st->main_depth = depth;
152             else if (where == MAINHYP)
153               st->depths = add(st->depths,depth);
154             move_bucket(st,dict_index);
155             return NOTFOUND;
156           }
157         else
158           /*
159              fprintf(stderr,"uno=%s\n", id);
160              fprintf(stderr,"st=%s\n", curr->id); fflush(stdout) */
161
162           /* the identifier is already in the list */
163           {
164             /* st = curr; */
165             curr->pos[where] = 1;
166             if (where >= 1) 
167               curr->pos[INBODY] = 0; /* it will never be set again to 1 */
168             if (where == MAINHYP)
169               curr->depths=add(curr->depths,depth); 
170             else if (where == MAINCONCL)
171               curr->main_depth = depth; 
172             if (prev != curr)
173               /* the identifier is not in the first position */
174               {
175                 prev->next_st_bucket = curr->next_st_bucket;
176                 move_bucket(curr,
177                             dict_index);
178               };
179             return where;
180           }
181 }
182
183 print_all(about,out,outrel,outsort)
184      char       *about;
185      FILE       *out,
186                 *outrel,
187                 *outsort;
188 {
189
190         int i;
191         struct st_bucket *curr;
192         curr = all;
193         while (curr != NULL)
194           {
195             for (i = 0; i < 5; ++i)
196               if ((curr->pos[i]) == 1)
197                 {
198                   if (i == MAINHYP)
199                     print_mainhyp(about,out,outrel,outsort,curr->id,curr->depths);
200                   else if (i == MAINCONCL)
201                     print_mainconcl(about,out,outrel,outsort,curr->id,curr->main_depth);
202                   else
203                     print_one(out,curr->id,i);
204                 }
205             curr = curr->all_next;
206           }
207 }
208
209
210 /****************************************************************/
211 /* 5. Definitions of functions local to the module.             */
212 /****************************************************************/
213
214 struct int_list  *add(l,m)
215      struct int_list    *l;
216      int                m;
217 {
218         struct int_list *curr;
219         /* scan the list looking for m */
220         curr = l;
221         while ((curr != NULL) && (m != (curr->val)))
222             curr = curr->next;
223         if (curr == NULL)
224           /* m is not in the list */
225           {
226             curr = (struct int_list *)malloc(sizeof(struct int_list));
227             curr->val = m;
228             curr->next = l;
229             return curr;
230           }
231         else
232         return l;
233        
234 }
235
236 print_mainhyp(about,out,outrel,outsort,uri,l)
237      char                *about;
238      FILE                *out,
239                          *outrel,
240                          *outsort;
241      char                *uri;
242      struct int_list     *l;
243 {
244     struct int_list *curr;
245     curr = l;
246     if (!strcmp(uri,"Rel"))
247       {
248         /* scan the list */
249         while (curr != NULL)
250           {
251             fprintf(outrel,"\t<h:Object rdf:about=\"");
252             fprintf(outrel,"%s",about);
253             fprintf(outrel,"\">\n");
254             fprintf(outrel,"\t\t<h:refRel rdf:parseType=\"Resource\">");
255             fprintf(outrel,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
256             fprintf(outrel,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
257             fprintf(outrel,"\n\t\t</h:refRel>\n");
258             fprintf(outrel,"\t</h:Object>\n");
259             curr = curr->next;
260           }
261       }
262    else if ((!strcmp(uri,"Prop")) || (!strcmp(uri,"Type")) ||
263             (!strcmp(uri,"Set")))
264       {
265         /* scan the list */
266         while (curr != NULL)
267           {
268             fprintf(outsort,"\t<h:Object rdf:about=\"");
269             fprintf(outsort,"%s",about);
270             fprintf(outsort,"\">\n");
271             fprintf(outsort,"\t\t<h:refSort rdf:parseType=\"Resource\">");
272             fprintf(outsort,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
273             fprintf(outsort,"\n\t\t\t\t<h:sort rdf:resource=\"&hns;%s\"/>",uri);
274             fprintf(outsort,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
275             fprintf(outsort,"\n\t\t</h:refSort>\n");
276             fprintf(outsort,"\t</h:Object>\n");
277             curr = curr->next;
278           }
279       }
280     else 
281      {
282         /* scan the list */
283         while (curr != NULL)
284           {
285             fprintf(out,"\t\t<h:refObj rdf:parseType=\"Resource\">");
286             fprintf(out,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
287             fprintf(out,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
288             fprintf(out,"\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>",uri);
289             fprintf(out,"\n\t\t</h:refObj>\n");
290             curr = curr->next;
291           }
292       }
293 }
294
295 print_mainconcl(about,out,outrel,outsort,uri,depth)
296      char    *about;
297      FILE    *out,
298              *outrel,
299              *outsort;
300      char    *uri;
301      int     depth;
302      
303 {
304     if (!strcmp(uri,"Rel"))
305       { 
306         fprintf(outrel,"\t<h:Object rdf:about=\"");
307         fprintf(outrel,"%s",about);
308         fprintf(outrel,"\">\n");
309         fprintf(outrel,"\t\t<h:refRel rdf:parseType=\"Resource\">");
310         fprintf(outrel,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
311         fprintf(outrel,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
312         fprintf(outrel,"\n\t\t</h:refRel>\n");
313         fprintf(outrel,"\t</h:Object>\n");
314       }
315     else if ((!strcmp(uri,"Prop")) || (!strcmp(uri,"Type")) ||
316             (!strcmp(uri,"Set")))
317       {
318         fprintf(outsort,"\t<h:Object rdf:about=\"");
319         fprintf(outsort,"%s",about);
320         fprintf(outsort,"\">\n");
321         fprintf(outsort,"\t\t<h:refSort rdf:parseType=\"Resource\">");
322         fprintf(outsort,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
323         fprintf(outsort,"\n\t\t\t\t<h:sort rdf:resource=\"&hns;%s\"/>",uri);
324         fprintf(outsort,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
325         fprintf(outsort,"\n\t\t</h:refSort>\n");
326         fprintf(outsort,"\t</h:Object>\n");
327       }
328     else
329       {
330         fprintf(out,"\t\t<h:refObj rdf:parseType=\"Resource\">");
331         fprintf(out,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
332         fprintf(out,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
333         fprintf(out,"\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>",uri);
334         fprintf(out,"\n\t\t</h:refObj>\n");
335       }
336 }
337
338 // dome: cambiata per usare il modello con position
339 print_one(out,uri,pos)
340      FILE    *out;
341      char    *uri;
342      int     pos;
343 {
344     fprintf(out,"\t\t<h:refObj df:parseType=\"Resource\">");
345     fprintf(out,"\n\t\t\t\t<h:position rdf:resource=\"&hns;");
346     if (pos == INBODY)
347        fprintf(out,"InBody");
348     else if (pos == MAINHYP)
349        fprintf(out,"MainHypothesis");
350     else if (pos == INHYP)
351        fprintf(out,"InHypothesis");
352     else if (pos == INCONCL)
353        fprintf(out,"InConclusion");
354     else if (pos == MAINCONCL)
355        fprintf(out,"MainConclusion");
356     fprintf(out,"\"/>\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>\n\t\t</h:refObj>\n", uri);
357     
358 }
359
360  /* The following function allocates a bucket for an identifier. */
361 allocate_bucket(st, id, where)
362         struct st_bucket
363                         **st;
364                                         /* pointer to the bucket to be */
365                                         /* allocated */
366         char            *id;
367                                         /* identifier */
368         int             where;
369 {
370         int i;
371
372         *st = (struct st_bucket *)malloc(sizeof(struct st_bucket));
373         (*st)->id = (char *)malloc(sizeof('a')*(strlen(id) + 1));
374         strcpy((*st)->id,id);
375         (*st)->main_depth = 0;
376         (*st)->depths = NULL;
377         (*st)->next_st_bucket = NULL;
378         (*st)->all_next = all;
379         all = *st;
380         for (i = 0; i < 5; ++i)
381           (*st)->pos[i] = 0;
382         (*st)->pos[where] = 1;
383 }
384
385  /* The following function moves a bucket to the head of the */
386  /* list in which it lies. */
387 move_bucket(st, dict_index)
388         struct st_bucket 
389                         *st;
390                                         /* pointer to the bucket to */
391                                         /* be moved */
392         int             dict_index;
393                                         /* index corresponding to */
394                                         /* the list in which the */
395                                         /* bucket lies */
396 {
397         st->next_st_bucket = dictionary[dict_index];
398         dictionary[dict_index] = st;
399 }
400
401  /* The following function implements Weinberger's hash function. */
402 int
403 hash_pjw(id)
404         char            *id;
405                                         /* identifier to be hashed */
406 {
407         unsigned        h,
408                         g;
409
410         for (h = 0; *id != EOS; id++)
411         {
412                 h = (h << HASH1) + (*id);
413                 if (g = h & HASH2)
414                         h = h ^ (g >> HASH3) ^ g;
415         }
416         return(h % DICTSIZE);
417 }
418
419
420
421
422
423