+++ /dev/null
-/*********************************************************************/
-/* Copyright (C) 2000, HELM Team */
-/* */
-/* This file is part of HELM, an Hypertextual, Electronic */
-/* Library of Mathematics, developed at the Computer Science */
-/* Department, University of Bologna, Italy. */
-/* */
-/* HELM is free software; you can redistribute it and/or */
-/* modify it under the terms of the GNU General Public License */
-/* as published by the Free Software Foundation; either version 2 */
-/* of the License, or (at your option) any later version. */
-/* */
-/* HELM is distributed in the hope that it will be useful, */
-/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
-/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
-/* GNU General Public License for more details. */
-/* */
-/* You should have received a copy of the GNU General Public License */
-/* along with HELM; if not, write to the Free Software */
-/* Foundation, Inc., 59 Temple Place - Suite 330, Boston, */
-/* MA 02111-1307, USA. */
-/* */
-/* For details, see the HELM World-Wide-Web page, */
-/* http://cs.unibo.it/helm/. */
- /*********************************************************************/
-
-/****************************************************************/
-/* STHANDLER.C */
-/****************************************************************/
-/* This module supplies routines for symbol table handling. */
-/* - init_symbol_table(): it initializes the symbol table */
-/* to void. */
-/* - search_bucket(): it searches the symbol table for the */
-/* bucket containing a given identifier, and */
-/* inserts it if it is not present; */
-/****************************************************************/
-/* First draft 11/12/2001, by Andrea Asperti */
-/****************************************************************/
-
-/****************************************************************/
-/* 1. Inclusion of header files. */
-/****************************************************************/
-
-#include <stdio.h>
-#include <malloc.h>
-
-/****************************************************************/
-/* 2. Declarations */
-/****************************************************************/
-
-
-#define DICTSIZE 211
-#define HASH1 4
-#define HASH2 0xf0000000
-#define HASH3 24
-#define EOS '\0'
-
-#define INBODY 0
-#define MAINHYP 1
-#define INHYP 2
-#define INCONCL 3
-#define MAINCONCL 4
-#define INTYPE 5
-#define NOTFOUND 6
-
-/****************************************************************/
-/* 3. Types. */
-/****************************************************************/
-
-struct int_list {
- int val;
- struct int_list *next;
- };
-
-struct st_bucket {
- char *id;
- /* identifier */
- int main_depth;
- struct int_list *depths;
- struct st_bucket *next_st_bucket;
- /* next bucket in the list */
- struct st_bucket *all_next;
- /* all buckets in symbol
- table are linked together */
- int pos[5];
-
- };
-
-struct st_bucket *dictionary[DICTSIZE];
- /* pointers to bucket lists */
-
-/****************************************************************/
-/* 4. Local functions. */
-/****************************************************************/
-struct int_list *add(struct int_list *,int);
-
-/****************************************************************/
-/* 5. Definitions of functions to be exported. */
-/****************************************************************/
-
-struct st_bucket *all;
-
- /* The following function initializes the symbol table to NULL */
-void init_symbol_table()
-{
- struct st_bucket *st;
- int i;
-
- /* initialize the dictionary */
- for (i = 0; i < DICTSIZE; i++)
- dictionary[i] = NULL;
- all = NULL;
-}
-
- /* The following function searches the symbol table for an identifier */
- /* and inserts it if it is not present.
- /* The bucket associated with the given identifier */
- /* becomes the first one in its list. */
-
-search_bucket(id, where, depth)
- char *id;
- /* identifier */
- int where;
- int depth;
-{
- int dict_index;
- /* value returned by the */
- /* hash function */
- struct st_bucket
- *prev,
- *curr;
-
- struct st_bucket *st;
-
- /* apply the hash function */
- dict_index = hash_pjw(id);
- /* fprintf(stderr,"%d\n", dict_index); fflush(stdout); */
-
- /* scan the bucket list indicated by the hash function */
- prev = curr = dictionary[dict_index];
- while ((curr != NULL) && (strcmp(id, curr->id)))
- {
- prev = curr;
- curr = curr->next_st_bucket;
- }
- if (curr == NULL)
- /* the identifier is not in the list */
- {
- allocate_bucket(&st,id,where);
- if (where == MAINCONCL)
- st->main_depth = depth;
- else if (where == MAINHYP)
- st->depths = add(st->depths,depth);
- move_bucket(st,dict_index);
- return NOTFOUND;
- }
- else
- /*
- fprintf(stderr,"uno=%s\n", id);
- fprintf(stderr,"st=%s\n", curr->id); fflush(stdout) */
-
- /* the identifier is already in the list */
- {
- /* st = curr; */
- curr->pos[where] = 1;
- if (where >= 1)
- curr->pos[INBODY] = 0; /* it will never be set again to 1 */
- if (where == MAINHYP)
- curr->depths=add(curr->depths,depth);
- else if (where == MAINCONCL)
- curr->main_depth = depth;
- if (prev != curr)
- /* the identifier is not in the first position */
- {
- prev->next_st_bucket = curr->next_st_bucket;
- move_bucket(curr,
- dict_index);
- };
- return where;
- }
-}
-
-print_all(about,out,outrel,outsort)
- char *about;
- FILE *out,
- *outrel,
- *outsort;
-{
-
- int i;
- struct st_bucket *curr;
- curr = all;
- while (curr != NULL)
- {
- for (i = 0; i < 5; ++i)
- if ((curr->pos[i]) == 1)
- {
- if (i == MAINHYP)
- print_mainhyp(about,out,outrel,outsort,curr->id,curr->depths);
- else if (i == MAINCONCL)
- print_mainconcl(about,out,outrel,outsort,curr->id,curr->main_depth);
- else
- print_one(out,curr->id,i);
- }
- curr = curr->all_next;
- }
-}
-
-
-/****************************************************************/
-/* 5. Definitions of functions local to the module. */
-/****************************************************************/
-
-struct int_list *add(l,m)
- struct int_list *l;
- int m;
-{
- struct int_list *curr;
- /* scan the list looking for m */
- curr = l;
- while ((curr != NULL) && (m != (curr->val)))
- curr = curr->next;
- if (curr == NULL)
- /* m is not in the list */
- {
- curr = (struct int_list *)malloc(sizeof(struct int_list));
- curr->val = m;
- curr->next = l;
- return curr;
- }
- else
- return l;
-
-}
-
-print_mainhyp(about,out,outrel,outsort,uri,l)
- char *about;
- FILE *out,
- *outrel,
- *outsort;
- char *uri;
- struct int_list *l;
-{
- struct int_list *curr;
- curr = l;
- if (!strcmp(uri,"Rel"))
- {
- /* scan the list */
- while (curr != NULL)
- {
- fprintf(outrel,"\t<h:Object rdf:about=\"");
- fprintf(outrel,"%s",about);
- fprintf(outrel,"\">\n");
- fprintf(outrel,"\t\t<h:refRel rdf:parseType=\"Resource\">");
- fprintf(outrel,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
- fprintf(outrel,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
- fprintf(outrel,"\n\t\t</h:refRel>\n");
- fprintf(outrel,"\t</h:Object>\n");
- curr = curr->next;
- }
- }
- else if ((!strcmp(uri,"Prop")) || (!strcmp(uri,"Type")) ||
- (!strcmp(uri,"Set")))
- {
- /* scan the list */
- while (curr != NULL)
- {
- fprintf(outsort,"\t<h:Object rdf:about=\"");
- fprintf(outsort,"%s",about);
- fprintf(outsort,"\">\n");
- fprintf(outsort,"\t\t<h:refSort rdf:parseType=\"Resource\">");
- fprintf(outsort,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
- fprintf(outsort,"\n\t\t\t\t<h:sort rdf:resource=\"&hns;%s\"/>",uri);
- fprintf(outsort,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
- fprintf(outsort,"\n\t\t</h:refSort>\n");
- fprintf(outsort,"\t</h:Object>\n");
- curr = curr->next;
- }
- }
- else
- {
- /* scan the list */
- while (curr != NULL)
- {
- fprintf(out,"\t\t<h:refObj rdf:parseType=\"Resource\">");
- fprintf(out,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainHypothesis\"/>");
- fprintf(out,"\n\t\t\t\t<h:depth>%d</h:depth>",curr->val);
- fprintf(out,"\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>",uri);
- fprintf(out,"\n\t\t</h:refObj>\n");
- curr = curr->next;
- }
- }
-}
-
-print_mainconcl(about,out,outrel,outsort,uri,depth)
- char *about;
- FILE *out,
- *outrel,
- *outsort;
- char *uri;
- int depth;
-
-{
- if (!strcmp(uri,"Rel"))
- {
- fprintf(outrel,"\t<h:Object rdf:about=\"");
- fprintf(outrel,"%s",about);
- fprintf(outrel,"\">\n");
- fprintf(outrel,"\t\t<h:refRel rdf:parseType=\"Resource\">");
- fprintf(outrel,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
- fprintf(outrel,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
- fprintf(outrel,"\n\t\t</h:refRel>\n");
- fprintf(outrel,"\t</h:Object>\n");
- }
- else if ((!strcmp(uri,"Prop")) || (!strcmp(uri,"Type")) ||
- (!strcmp(uri,"Set")))
- {
- fprintf(outsort,"\t<h:Object rdf:about=\"");
- fprintf(outsort,"%s",about);
- fprintf(outsort,"\">\n");
- fprintf(outsort,"\t\t<h:refSort rdf:parseType=\"Resource\">");
- fprintf(outsort,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
- fprintf(outsort,"\n\t\t\t\t<h:sort rdf:resource=\"&hns;%s\"/>",uri);
- fprintf(outsort,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
- fprintf(outsort,"\n\t\t</h:refSort>\n");
- fprintf(outsort,"\t</h:Object>\n");
- }
- else
- {
- fprintf(out,"\t\t<h:refObj rdf:parseType=\"Resource\">");
- fprintf(out,"\n\t\t\t\t<h:position rdf:resource=\"&hns;MainConclusion\"/>");
- fprintf(out,"\n\t\t\t\t<h:depth>%d</h:depth>",depth);
- fprintf(out,"\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>",uri);
- fprintf(out,"\n\t\t</h:refObj>\n");
- }
-}
-
-// dome: cambiata per usare il modello con position
-print_one(out,uri,pos)
- FILE *out;
- char *uri;
- int pos;
-{
- fprintf(out,"\t\t<h:refObj df:parseType=\"Resource\">");
- fprintf(out,"\n\t\t\t\t<h:position rdf:resource=\"&hns;");
- if (pos == INBODY)
- fprintf(out,"InBody");
- else if (pos == MAINHYP)
- fprintf(out,"MainHypothesis");
- else if (pos == INHYP)
- fprintf(out,"InHypothesis");
- else if (pos == INCONCL)
- fprintf(out,"InConclusion");
- else if (pos == MAINCONCL)
- fprintf(out,"MainConclusion");
- fprintf(out,"\"/>\n\t\t\t\t<h:occurrence><h:Object rdf:about=\"%s\"/></h:occurrence>\n\t\t</h:refObj>\n", uri);
-
-}
-
- /* The following function allocates a bucket for an identifier. */
-allocate_bucket(st, id, where)
- struct st_bucket
- **st;
- /* pointer to the bucket to be */
- /* allocated */
- char *id;
- /* identifier */
- int where;
-{
- int i;
-
- *st = (struct st_bucket *)malloc(sizeof(struct st_bucket));
- (*st)->id = (char *)malloc(sizeof('a')*(strlen(id) + 1));
- strcpy((*st)->id,id);
- (*st)->main_depth = 0;
- (*st)->depths = NULL;
- (*st)->next_st_bucket = NULL;
- (*st)->all_next = all;
- all = *st;
- for (i = 0; i < 5; ++i)
- (*st)->pos[i] = 0;
- (*st)->pos[where] = 1;
-}
-
- /* The following function moves a bucket to the head of the */
- /* list in which it lies. */
-move_bucket(st, dict_index)
- struct st_bucket
- *st;
- /* pointer to the bucket to */
- /* be moved */
- int dict_index;
- /* index corresponding to */
- /* the list in which the */
- /* bucket lies */
-{
- st->next_st_bucket = dictionary[dict_index];
- dictionary[dict_index] = st;
-}
-
- /* The following function implements Weinberger's hash function. */
-int
-hash_pjw(id)
- char *id;
- /* identifier to be hashed */
-{
- unsigned h,
- g;
-
- for (h = 0; *id != EOS; id++)
- {
- h = (h << HASH1) + (*id);
- if (g = h & HASH2)
- h = h ^ (g >> HASH3) ^ g;
- }
- return(h % DICTSIZE);
-}
-
-
-
-
-
-
projects / helm.git / blobdiff