]> matita.cs.unibo.it Git - helm.git/blobdiff - 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
index 07612d6f8115a9e51ad37447a0f1fb395b0cf023..bfdc795d56e9f71717cb8088e57f78f3cfea6ef4 100644 (file)
 /* 3. Types.                                                   */
 /****************************************************************/
 
+struct int_list {
+               int                     val;
+                struct int_list                *next;
+                  }; 
+
 struct st_bucket {
                char                    *id;
-                                               /* identifier */
+                                                /* identifier */
+                int                     main_depth;
+                struct int_list                *depths;
                struct st_bucket        *next_st_bucket;
                                                /* next bucket in the list */
                 struct st_bucket       *all_next;
@@ -83,7 +90,12 @@ struct st_bucket    *dictionary[DICTSIZE];
                               /* pointers to bucket lists */
 
 /****************************************************************/
-/* 4. Definitions of functions to be exported.                 */
+/* 4. Local functions.                                         */
+/****************************************************************/
+struct int_list  *add(struct int_list  *,int);
+
+/****************************************************************/
+/* 5. Definitions of functions to be exported.                 */
 /****************************************************************/
 
 struct st_bucket       *all;
@@ -105,10 +117,11 @@ void init_symbol_table()
  /* The bucket associated with the given identifier */
  /* becomes the first one in its list. */
 
-search_bucket(id, where)
+search_bucket(id, where, depth)
        char            *id;
                                        /* identifier */
         int             where;
+        int             depth;
 {
        int             dict_index;
                                        /* value returned by the */
@@ -121,7 +134,7 @@ search_bucket(id, where)
 
         /* apply the hash function */
         dict_index = hash_pjw(id);
-        /* printf( "%d\n", dict_index); */
+        /* fprintf(stderr,"%d\n", dict_index); fflush(stdout); */
         
         /* scan the bucket list indicated by the hash function */
         prev = curr = dictionary[dict_index];
@@ -134,12 +147,17 @@ search_bucket(id, where)
           /* 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
-         /* printf("uno=%s\n", id);
-            printf("st=%s\n", curr->id); */
+          /*
+            fprintf(stderr,"uno=%s\n", id);
+            fprintf(stderr,"st=%s\n", curr->id); fflush(stdout) */
 
           /* the identifier is already in the list */
           {
@@ -147,6 +165,10 @@ search_bucket(id, where)
             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 */
               {
@@ -158,18 +180,28 @@ search_bucket(id, where)
           }
 }
 
-print_all(out)
-     FILE *out;
+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)
-               print_one(out,curr->id,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;
           }
 }
@@ -179,6 +211,129 @@ print_all(out)
 /* 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)
@@ -186,7 +341,8 @@ print_one(out,uri,pos)
      char    *uri;
      int     pos;
 {
-    fprintf(out,"\t\t<h:refObj>\n\t\t\t<h:Occurrence>\n\t\t\t\t<h:position>");
+    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)
@@ -197,7 +353,8 @@ print_one(out,uri,pos)
        fprintf(out,"InConclusion");
     else if (pos == MAINCONCL)
        fprintf(out,"MainConclusion");
-    fprintf(out,"</h:position>\n\t\t\t\t<h:occurrence>%s</h:occurrence>\n\t\t\t</h:Occurrence>\n\t\t</h:refObj>\n", uri);
+    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. */
@@ -215,6 +372,8 @@ allocate_bucket(st, id, where)
        *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;
@@ -261,3 +420,4 @@ hash_pjw(id)
 
 
 
+