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