X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate_V7_mowgli%2FMETADATA%2Fmeta_lex.l;h=eca7c383d6a1a96568d20a31521b3ca7d82b75c5;hb=3c7ca719c304eb7de7d8d4e9a90ebe0db8d8ecab;hp=967fbc00cf869764c1d67f48e15017afc0eab4ea;hpb=0e6b8620b9c128c3f256c00b422cee7708321171;p=helm.git

diff --git a/helm/metadata/create_V7_mowgli/METADATA/meta_lex.l b/helm/metadata/create_V7_mowgli/METADATA/meta_lex.l
index 967fbc00c..eca7c383d 100644
--- a/helm/metadata/create_V7_mowgli/METADATA/meta_lex.l
+++ b/helm/metadata/create_V7_mowgli/METADATA/meta_lex.l
@@ -51,6 +51,7 @@
 #define                 CONST     1
 #define                 MUTIND    2
 #define                 MUTCONSTRUCT  3
+#define                 SORT      4
 
 #define                 INBODY    0
 #define                 MAINHYP   1
@@ -70,6 +71,8 @@ int                     position = INBODY;
 int                     first_child = HERE;
 int			skip = 0;     // boolean to skip the insertion of a URI
 int                     no_open_source =0;
+int                     spine_depth = 0;
+int                     depth = 0;
 int                     tmp_n;
 char                    sep = '"';
 char                    *xpointer = "#xpointer(1/";
@@ -82,7 +85,8 @@ char                    *tmp;
  /***************************************************************/
 
 uri                     [^"]+
-digits                  [0-9]+                   
+digits                  [0-9]+ 
+value                   [^"]+                  
 
  /***************************************************************/
  /* 4. Rules.							*/
@@ -101,8 +105,9 @@ digits                  [0-9]+
 
 "<decl"            |
 "<def"             {
-                    if ((position == INTYPE) ||
-                        (position == INHYP))
+                    if (position == INTYPE)
+                       position = MAINHYP;
+                    else if (position == MAINHYP)
                         { position = INHYP;
                           no_open_source++;};
                    }
@@ -113,9 +118,19 @@ digits                  [0-9]+
                      {
                       no_open_source--;
                       if (no_open_source == 0) 
-                       { position = INTYPE;
-                         first_child = HERE; };
-                     };
+                        {
+                         position = MAINHYP;
+                         depth++;
+                         first_child = HERE;
+                        }
+                     }
+                    else if (position == MAINHYP)
+                      {
+                       position = INTYPE;
+                       spine_depth++;
+                       depth = 0;
+                      }
+                    first_child = HERE;
                    }
 
 
@@ -123,13 +138,43 @@ digits                  [0-9]+
                    }
 
 "<LAMBDA"          |
-"<REL"             |
 "<MUTCASE"         |
 "<FIX"             |
 "<COFIX"           { 
                           first_child = AFTER;
                    }
 
+"<REL"             {
+                    if (((position == INTYPE) | (position == MAINHYP)) &&
+                       (first_child == HERE))
+                     {
+                       if (position == INTYPE) /* REL on the spine */
+                         {
+                           position = INCONCL;
+                           search("Rel",first_child,position,spine_depth);
+                         }
+                       else search("Rel",first_child,position,depth);
+                       first_child = AFTER;
+                     }
+                   }
+
+"<SORT"(" "|\n)+"value=\""{value}   {         
+                    if (((position == INTYPE) | (position == MAINHYP)) &&
+                       (first_child == HERE))
+                     {
+                       tmp=(char *)malloc((sizeof('a')*200)); 
+                       strcpy(tmp,yytext);
+                       strsep(&tmp,&sep); 
+                       if (position == INTYPE) /* SORT on the spine */
+                         { 
+                           position = INCONCL;
+                           search(tmp,first_child,position,spine_depth);
+                         }
+                       else search(tmp,first_child,position,depth);
+                       first_child = AFTER;
+                     }
+                   }
+
 "<VAR"             {
                      skip = 1;
                      first_child = AFTER;
@@ -159,12 +204,14 @@ digits                  [0-9]+
                             strcpy(uri,yytext);
                             strsep(&uri,&sep);
                             if (where == CONST)
-                                {
-                                   search(uri,first_child,position); 
-                                   where = NOWHERE;
-                                   first_child = AFTER;
-                                   free(uri); 
-                                 };
+                              {
+                                if (position == INCONCL)
+                                  search(uri,first_child,position,spine_depth);
+                                else search(uri,first_child,position,depth);
+                                where = NOWHERE;
+                                first_child = AFTER;
+                                free(uri); 
+                              };
                          } else skip = 0;
                    } 
 
@@ -181,7 +228,9 @@ digits                  [0-9]+
                          if (where == MUTIND) 
                              { 
                                strcat(uri,")");
-                               search(uri,first_child,position); 
+                               if (position == INCONCL)
+                                  search(uri,first_child,position,spine_depth);
+                               else search(uri,first_child,position,depth);
                                free(uri);
                                free(tmp);
                                where = NOWHERE; 
@@ -196,7 +245,9 @@ digits                  [0-9]+
                             strcat(uri,"/");
                             strcat(uri,tmp);
                             strcat(uri,")");
-                            search(uri,first_child,position);
+                            if (position == INCONCL)
+                              search(uri,first_child,position,spine_depth);
+                            else search(uri,first_child,position,depth);
                             free(uri);
                             free(tmp);
                             where = NOWHERE; 
@@ -214,8 +265,19 @@ digits                  [0-9]+
 main(int argc, char *argv[])
 {                  
                    struct stat buf;
-                   init_symbol_table();
+                   FILE *outrel, *outsort;
 
+                   init_symbol_table();
+                   if (!(outrel = fopen("forward_rel.xml","a"))) 
+                     {
+		      fprintf(stderr, "error in openinf file forward_rel.xml\n");
+                      exit(-1);
+                     }
+                   if (!(outsort = fopen("forward_sort.xml","a"))) 
+                     {
+		      fprintf(stderr, "error in openinf file forward_rel.xml\n");
+                      exit(-1);
+                     }
                    // We process the body
                    if (!stat("tmp/body.xml",&buf)) {
                       yyin = fopen("tmp/body.xml", "r");
@@ -228,38 +290,74 @@ main(int argc, char *argv[])
                    yyin = fopen("tmp/type.xml", "r");
                    position = INTYPE;
                    first_child = HERE;
-                   yylex();
+                   no_open_source = 0;
+                   spine_depth = 0;
+                   depth = 0;
+                   yylex(); 
 
                    printf("<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n");
-                   printf("<rdf:RDF xml:lang=\"en\" xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\" xmlns:h=\"file:mattone.rdf#\">\n");
+printf("<!DOCTYPE rdf:RDF [
+        <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
+        <!ENTITY hthns 'http://www.cs.unibo.it/helm/schemas/schema-helmth#'>
+        <!ENTITY hns 'http://www.cs.unibo.it/helm/schemas/schema-helm#'>
+
+   ]>\n");
+
+                   printf("<rdf:RDF xml:lang=\"en\" xmlns:rdf=\"&rdfns;\" xmlns:h=\"&hns;\" xmlns:hth=\"&hthns;\">\n");
                    printf("\t<h:Object rdf:about=\"");
                    printf("%s",argv[1]);
                    printf("\">\n");
-                   print_all();
+                   print_all(argv[1],outrel,outsort);
                    printf("\t</h:Object>\n");
                    printf("</rdf:RDF>\n");
                    fclose(yyin);
                    } 
 
-search(uri,first_child,position)
+search(uri,first_child,position,depth)
 char               *uri;
 int                first_child;
 int                position; 
 {                  
-                   if (first_child == HERE)
+                   if (position == MAINHYP)
+                      { 
+                       if (first_child == HERE) 
+                           found = search_bucket(uri,MAINHYP,depth);
+                       else 
+                           found = search_bucket(uri,INHYP,0);
+                      }
+                   else if (position == INCONCL)
+                      { 
+                       if (first_child == HERE) 
+                           found = search_bucket(uri,MAINCONCL,depth);
+                       else
+                           found = search_bucket(uri,INCONCL,0);
+                      }
+                        
+                   else 
+                      found = search_bucket(uri,position,depth);
+                   /* if (found == NOTFOUND)
+                         fprintf(stderr,"pos = %d, uri = %s\n", position, uri); */
+} 
+/*                  
+                      (first_child == HERE) 
                       {
-                       if (position == INHYP)
-                          found = search_bucket(uri,MAINHYP);
+                       if (position == MAINHYP)
+                          found = search_bucket(uri,MAINHYP,depth);
                        else if (position == INCONCL)
-                          found = search_bucket(uri,MAINCONCL);
-                       /* if (found == NOTFOUND)
-                          printf( "pos = %d, uri = %s\n", MAINCONCL, uri); */
+                          found = search_bucket(uri,MAINCONCL,0);
+                       else if (position == INHYP)
+                          found = search_bucket(uri,INHYP,0);
+                          if (found == NOTFOUND)
+                          printf( "pos = %d, uri = %s\n", MAINCONCL, uri); 
                        }
-                    else found = search_bucket(uri,position);
-                    /* if (found == NOTFOUND)
-                          printf( "pos = %d, uri = %s\n", position, uri); */
-                    }
+                   else if ((position == MAINHYP) && (first_child == AFTER))
+                        found = search_bucket(uri,INHYP,0);
+                   else found = search_bucket(uri,position,0);
+                   if (found == NOTFOUND)
+                         printf( "pos = %d, uri = %s\n", position, uri); 
+                   } */
 
 int yywrap() {
                return 1;
              }
+