X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate_V7_mowgli%2FMETADATA%2Fmeta_lex_ind.l;h=acf86244658752e9388088e775fb963d18ee5e7e;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=6d09578f90a94a7673efaa7e7d6b81c03485ca5c;hpb=0e6b8620b9c128c3f256c00b422cee7708321171;p=helm.git

diff --git a/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l b/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
index 6d09578f9..acf862446 100644
--- a/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
+++ b/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
@@ -38,6 +38,7 @@
 %{
 #include                <string.h>
 #include                <stdlib.h>
+#include                <sys/stat.h>
 #include                "sthandler_ind.h"
 %}
 
@@ -50,6 +51,7 @@
 #define                 CONST     1
 #define                 MUTIND    2
 #define                 MUTCONSTRUCT  3
+#define                 SORT      4
 
 #define                 INBODY    0
 #define                 MAINHYP   1
@@ -65,12 +67,14 @@
 
 int			where = NOWHERE;
 int                     found = NOTFOUND;
-int                     position = INTYPE;
+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;
-int                     inductive_type =0;
+int                     inductive_type = 0;
 int                     constructor = 0;
 int                     deep_type = 0;
 char                    sep = '"';
@@ -82,48 +86,30 @@ char                    *file_uri;
 char                    *inductive_uri;
 char                    *filename_prefix;
 char                    *file_uri_prefix;
-
 %}
 
-/*%x deeptype*/
-
-
  /***************************************************************/
  /* 3. Regular definitions.					*/
  /***************************************************************/
 
 uri                     [^"]+
-digits                  [0-9]+                   
+digits                  [0-9]+ 
+value                   [^"]+                  
 
  /***************************************************************/
  /* 4. Rules.							*/
  /***************************************************************/
 
-/*
-"<type>"           {
-                     BEGIN(deeptype);
-                     deep_type++;
-                   }
-
-<deeptype>"<type>" {
-                     deep_type++;
-                   }
-
-<deeptype>"</type>" {
-                     deep_type--;
-                     if (deeptype == 0) BEGIN(0);
-		    }
-
-<deeptype>.|\n     {
-                   }
-*/
 
 %%
 
 "<InductiveType"   { 
-                     fprintf(stderr,"uno");
+                     /* fprintf(stderr,"uno"); */
                      init_symbol_table();
-                     fprintf(stderr,"due");
+                     no_open_source = 0;
+                     depth = 0;
+                     spine_depth = 0;
+                     /* fprintf(stderr,"due"); */
                      inductive_type++;
                      constructor=0;
                      position = INTYPE;
@@ -132,19 +118,22 @@ digits                  [0-9]+
 
 "</arity>"         { tmp = (char *)malloc(sizeof('a')*128);
                      strcpy(filename,filename_prefix);
-                     fprintf(stderr,"tre");
+                     /* fprintf(stderr,"tre"); */
                      strcpy(file_uri,file_uri_prefix);
                      sprintf(tmp,",%d.xml", inductive_type);
-                     fprintf(stderr,"quattro");
+                     /* fprintf(stderr,"quattro"); */
                      strcat(filename,tmp);
                      sprintf(tmp,"#xpointer(1/%d)", inductive_type);
                      strcat(file_uri,tmp);
-                     fprintf(stderr,"cinque");
+                     /* fprintf(stderr,"cinque"); */
                      free(tmp);
                      print_file();
                    }
 
 "<Constructor"     { init_symbol_table();
+                     no_open_source = 0;
+                     depth = 0;
+                     spine_depth = 0;
                      constructor++;
                      strcpy(inductive_uri,file_uri_prefix);
                      position = INTYPE;
@@ -165,8 +154,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++;};
                    }
@@ -177,22 +167,63 @@ 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;
                    }
 
+
 .|\n               {
                    }
 
 "<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;
@@ -222,12 +253,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;
                    } 
 
@@ -244,7 +277,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; 
@@ -259,7 +294,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; 
@@ -267,6 +304,7 @@ digits                  [0-9]+
                    } 
 
 
+
 %%
 
  /***************************************************************/
@@ -274,58 +312,89 @@ digits                  [0-9]+
  /***************************************************************/
 
 main(int argc, char *argv[])
-{                  
+{
                    filename = malloc((sizeof('a')*2000));
                    file_uri = malloc((sizeof('a')*2000));
                    inductive_uri = malloc((sizeof('a')*2000));
                    filename_prefix=argv[1];
                    file_uri_prefix=argv[2];
-                   fprintf(stderr,"qua");
+                   /* fprintf(stderr,"qua"); */
                    yyin = fopen("tmp/inductive_type.xml", "r");
                    yylex();
-                   } 
+}
 
 print_file()
-{
-                   FILE *out;
+{                  
+                   FILE *out, *outrel, *outsort;
+
                    if (!(out = fopen(filename,"w"))) 
                      {
 		      fprintf(stderr, "error in openinf file %s\n", filename);
                       exit(-1);
+                     } 
+                   if (!(outrel = fopen("forward_rel.xml","a"))) 
+                     {
+		      fprintf(stderr, "error in openinf file forward_rel.xml\n");
+                      exit(-1);
                      }
-                   else
+                   if (!(outsort = fopen("forward_sort.xml","a"))) 
                      {
-                      fprintf(out,"<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n");
-                      fprintf(out,"<rdf:RDF xml:lang=\"en\" xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\" xmlns:h=\"file:mattone.rdf#\">\n");
-                      fprintf(out,"\t<h:Object rdf:about=\"");
-                      fprintf(out,"%s",file_uri);
-                      fprintf(out,"\">\n");
-                      print_all(out);
-                      fprintf(out,"\t</h:Object>\n");
-                      fprintf(out,"</rdf:RDF>\n");
-                      fclose(out);
+		      fprintf(stderr, "error in openinf file forward_rel.xml\n");
+                      exit(-1);
                      }
+                 
+                   // We process the type
+
+                   fprintf(out,"<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n");
+fprintf(out,"<!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");
+                   fprintf(out,"<rdf:RDF xml:lang=\"en\" xmlns:rdf=\"&rdfns;\" xmlns:h=\"&hns;\" xmlns:hth=\"&hthns;\">\n");
+                   fprintf(out,"\t<h:Object rdf:about=\"");
+                   fprintf(out,"%s",file_uri);
+                   fprintf(out,"\">\n");
+                   print_all(file_uri,out,outrel,outsort);
+                   fprintf(out,"\t</h:Object>\n");
+                   fprintf(out,"</rdf:RDF>\n");
+                   fclose(out);
+                   fclose(outrel);
+                   fclose(outsort);
 }
 
-search(uri,first_child,position)
+search(uri,first_child,position,depth)
 char               *uri;
 int                first_child;
 int                position; 
 {                  
-                   if (first_child == HERE)
-                      {
-                       if (position == INHYP)
-                          found = search_bucket(uri,MAINHYP);
-                       else if (position == INCONCL)
-                          found = search_bucket(uri,MAINCONCL);
-                       /* 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); */
-                    }
+                   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)
+                         printf( "pos = %d, uri = %s\n", position, uri); */
+}
+
 
 int yywrap() {
                return 1;
              }
+
+
+
+