]> matita.cs.unibo.it Git - helm.git/blob - helm/metadata/create_V7_mowgli/METADATA/sthandler.c
Initial revision
[helm.git] / helm / metadata / create_V7_mowgli / METADATA / sthandler.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); */
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              printf("uno=%s\n", id);
160              printf("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,outrel,outsort)
184      char       *about;
185      FILE       *outrel,
186                 *outsort;
187 {
188
189         int i;
190         struct st_bucket *curr;
191         curr = all;
192         while (curr != NULL)
193           {
194             for (i = 0; i < 5; ++i)
195               if ((curr->pos[i]) == 1)
196                 {
197                   if (i == MAINHYP)
198                     print_mainhyp(about,outrel,outsort,curr->id,curr->depths);
199                   else if (i == MAINCONCL)
200                     print_mainconcl(about,outrel,outsort,curr->id,curr->main_depth);
201                   else
202                     print_one(curr->id,i);
203                 }
204             curr = curr->all_next;
205           }
206 }
207
208
209 /****************************************************************/
210 /* 5. Definitions of functions local to the module.             */
211 /****************************************************************/
212
213 struct int_list  *add(l,m)
214      struct int_list    *l;
215      int                m;
216 {
217         struct int_list *curr;
218         /* scan the list looking for m */
219         curr = l;
220         while ((curr != NULL) && (m != (curr->val)))
221             curr = curr->next;
222         if (curr == NULL)
223           /* m is not in the list */
224           {
225             curr = (struct int_list *)malloc(sizeof(struct int_list));
226             curr->val = m;
227             curr->next = l;
228             return curr;
229           }
230         else
231         return l;
232        
233 }
234
235 print_mainhyp(about,outrel,outsort,uri,l)
236      char                *about;
237      FILE                *outrel,
238                          *outsort;
239      char                *uri;
240      struct int_list     *l;
241 {
242     struct int_list *curr;
243     curr = l;
244     if (!strcmp(uri,"Rel"))
245       {
246         /* scan the list */
247         while (curr != NULL)
248           {
249             fprintf(outrel,"\t<h:Object rdf:about=\"");
250             fprintf(outrel,"%s",about);
251             fprintf(outrel,"\">\n");
252             fprintf(outrel,"\t\t<h:refRel rdf:parseType=\"Resource\">");
253             fprintf(outrel,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
254             fprintf(outrel,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
255             fprintf(outrel,"\n\t\t</h:refRel>\n");
256             fprintf(outrel,"\t</h:Object>\n");
257             curr = curr->next;
258           }
259       }
260    else if ((!strcmp(uri,"Prop")) || (!strcmp(uri,"Type")) ||
261             (!strcmp(uri,"Set")))
262       {
263         /* scan the list */
264         while (curr != NULL)
265           {
266             fprintf(outsort,"\t<h:Object rdf:about=\"");
267             fprintf(outsort,"%s",about);
268             fprintf(outsort,"\">\n");
269             fprintf(outsort,"\t\t<h:refSort rdf:parseType=\"Resource\">");
270             fprintf(outsort,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
271             fprintf(outsort,"\n\t\t\t\t<h:sort rdf:resource=\"&hns;%s\"/>",uri);
272             fprintf(outsort,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
273             fprintf(outsort,"\n\t\t</h:refSort>\n");
274             fprintf(outsort,"\t</h:Object>\n");
275             curr = curr->next;
276           }
277       }
278     else 
279      {
280         /* scan the list */
281         while (curr != NULL)
282           {
283             printf("\t\t<h:refObj rdf:parseType=\"Resource\">");
284             printf("\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
285             printf("\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
286             printf("\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>",uri);
287             printf("\n\t\t</h:refObj>\n");
288             curr = curr->next;
289           }
290       }
291 }
292
293 print_mainconcl(about,outrel,outsort,uri,depth)
294      char    *about;
295      FILE    *outrel,
296              *outsort;
297      char    *uri;
298      int     depth;
299      
300 {
301     if (!strcmp(uri,"Rel"))
302       { 
303         fprintf(outrel,"\t<h:Object rdf:about=\"");
304         fprintf(outrel,"%s",about);
305         fprintf(outrel,"\">\n");
306         fprintf(outrel,"\t\t<h:refRel rdf:parseType=\"Resource\">");
307         fprintf(outrel,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
308         fprintf(outrel,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
309         fprintf(outrel,"\n\t\t</h:refRel>\n");
310         fprintf(outrel,"\t</h:Object>\n");
311       }
312     else if ((!strcmp(uri,"Prop")) || (!strcmp(uri,"Type")) ||
313             (!strcmp(uri,"Set")))
314       {
315         fprintf(outsort,"\t<h:Object rdf:about=\"");
316         fprintf(outsort,"%s",about);
317         fprintf(outsort,"\">\n");
318         fprintf(outsort,"\t\t<h:refSort rdf:parseType=\"Resource\">");
319         fprintf(outsort,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
320         fprintf(outsort,"\n\t\t\t\t<h:sort rdf:resource=\"&hns;%s\"/>",uri);
321         fprintf(outsort,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
322         fprintf(outsort,"\n\t\t</h:refSort>\n");
323         fprintf(outsort,"\t</h:Object>\n");
324       }
325     else
326       {
327         printf("\t\t<h:refObj rdf:parseType=\"Resource\">");
328         printf("\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
329         printf("\n\t\t\t\t<h:depth>%d</h:depth>",depth);
330         printf("\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>",uri);
331         printf("\n\t\t</h:refObj>\n");
332       }
333 }
334
335 // dome: cambiata per usare il modello con position
336 print_one(uri,pos)
337      char    *uri;
338      int     pos;
339 {
340     printf("\t\t<h:refObj rdf:parseType=\"Resource\">");
341     printf("\n\t\t\t\t<h:position rdf:resource=\"&hns;");
342     if (pos == INBODY)
343        printf("InBody");
344     else if (pos == MAINHYP)
345        printf("MainHypothesis");
346     else if (pos == INHYP)
347        printf("InHypothesis");
348     else if (pos == INCONCL)
349        printf("InConclusion");
350     else if (pos == MAINCONCL)
351        printf("MainConclusion");
352     printf("\"/>\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>\n\t\t</h:refObj>\n", uri);
353 }
354
355  /* The following function allocates a bucket for an identifier. */
356 allocate_bucket(st, id, where)
357         struct st_bucket
358                         **st;
359                                         /* pointer to the bucket to be */
360                                         /* allocated */
361         char            *id;
362                                         /* identifier */
363         int             where;
364 {
365         int i;
366
367         *st = (struct st_bucket *)malloc(sizeof(struct st_bucket));
368         (*st)->id = (char *)malloc(sizeof('a')*(strlen(id) + 1));
369         strcpy((*st)->id,id);
370         (*st)->main_depth = 0;
371         (*st)->depths = NULL;
372         (*st)->next_st_bucket = NULL;
373         (*st)->all_next = all;
374         all = *st;
375         for (i = 0; i < 5; ++i)
376           (*st)->pos[i] = 0;
377         (*st)->pos[where] = 1;
378 }
379
380  /* The following function moves a bucket to the head of the */
381  /* list in which it lies. */
382 move_bucket(st, dict_index)
383         struct st_bucket 
384                         *st;
385                                         /* pointer to the bucket to */
386                                         /* be moved */
387         int             dict_index;
388                                         /* index corresponding to */
389                                         /* the list in which the */
390                                         /* bucket lies */
391 {
392         st->next_st_bucket = dictionary[dict_index];
393         dictionary[dict_index] = st;
394 }
395
396  /* The following function implements Weinberger's hash function. */
397 int
398 hash_pjw(id)
399         char            *id;
400                                         /* identifier to be hashed */
401 {
402         unsigned        h,
403                         g;
404
405         for (h = 0; *id != EOS; id++)
406         {
407                 h = (h << HASH1) + (*id);
408                 if (g = h & HASH2)
409                         h = h ^ (g >> HASH3) ^ g;
410         }
411         return(h % DICTSIZE);
412 }
413
414
415
416
417
418