X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate_V7_mowgli%2FMETADATA%2Fmeta_lex.l;h=18ea05cc9941127c6f4b8712bcdd34d35a9b5f84;hb=0de1b960f42ac368414b7405a79e7933445ee8af;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..18ea05cc9 100644
--- a/helm/metadata/create_V7_mowgli/METADATA/meta_lex.l
+++ b/helm/metadata/create_V7_mowgli/METADATA/meta_lex.l
@@ -39,6 +39,7 @@
 #include                <string.h>
 #include                <stdlib.h>
 #include                <sys/stat.h>
+#include                <postgresql/libpq-fe.h>
 #include                "sthandler.h"
 %}
 
@@ -51,6 +52,7 @@
 #define                 CONST     1
 #define                 MUTIND    2
 #define                 MUTCONSTRUCT  3
+#define                 SORT      4
 
 #define                 INBODY    0
 #define                 MAINHYP   1
@@ -69,7 +71,9 @@ int                     found = NOTFOUND;
 int                     position = INBODY;
 int                     first_child = HERE;
 int			skip = 0;     // boolean to skip the insertion of a URI
-int                     no_open_source =0;
+int                     no_open_source = 0;
+int                     spine_depth = 0;
+int                     depth = 0;
 int                     tmp_n;
 char                    sep = '"';
 char                    *xpointer = "#xpointer(1/";
@@ -82,7 +86,8 @@ char                    *tmp;
  /***************************************************************/
 
 uri                     [^"]+
-digits                  [0-9]+                   
+digits                  [0-9]+ 
+value                   [^"]+                  
 
  /***************************************************************/
  /* 4. Rules.							*/
@@ -97,25 +102,41 @@ digits                  [0-9]+
 
 "</body>"(" "|\n)*"<type" {
                     position = INTYPE; // Variables have both a body and a type
+                    first_child = HERE;
+                    no_open_source = 0;
+                    spine_depth = 0;
+                    depth = 0;   
                    }
 
 "<decl"            |
 "<def"             {
-                    if ((position == INTYPE) ||
-                        (position == INHYP))
+                    if (position == INTYPE)
+                       position = MAINHYP;
+                    else if (position == MAINHYP)
                         { position = INHYP;
                           no_open_source++;};
                    }
 
 "</decl>"          |
-"</def"            {
+"</def>"           {
                     if (position == INHYP)
                      {
                       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;
+                      }
+                    /* bug? first_child = HERE; */
                    }
 
 
@@ -123,13 +144,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 +210,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 +234,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 +251,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; 
@@ -213,53 +270,124 @@ digits                  [0-9]+
 
 main(int argc, char *argv[])
 {                  
-                   struct stat buf;
-                   init_symbol_table();
-
-                   // We process the body
-                   if (!stat("tmp/body.xml",&buf)) {
-                      yyin = fopen("tmp/body.xml", "r");
-                      position = INBODY;
-                      yylex();
-                      fclose(yyin);
-                   }
-
-                   // We process the type
-                   yyin = fopen("tmp/type.xml", "r");
-                   position = INTYPE;
-                   first_child = HERE;
-                   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("\t<h:Object rdf:about=\"");
-                   printf("%s",argv[1]);
-                   printf("\">\n");
-                   print_all();
-                   printf("\t</h:Object>\n");
-                   printf("</rdf:RDF>\n");
-                   fclose(yyin);
-                   } 
-
-search(uri,first_child,position)
+    struct stat buf;
+
+    char       *pghost,
+               *pgport,
+               *pgoptions,
+               *pgtty;
+    char       *dbName;
+
+    /* FILE *debug; */
+
+    PGconn     *conn;
+    PGresult   *res;
+
+    if (argc != 4)
+    {
+        fprintf(stderr, "Usage: meta <object_uri> <body_file> <type_file>\n");
+        exit(1);
+    }
+
+    /*
+     * begin, by setting the parameters for a backend connection if the
+     * parameters are null, then the system will try to use reasonable
+     * defaults by looking up environment variables or, failing that,
+     * using hardwired constants
+     */
+
+    /* make a connection to the database */
+    conn = PQconnectdb("user=helm dbname=mowgli_test");
+
+    /*
+     * check to see that the backend connection was successfully made
+     */
+    if (PQstatus(conn) == CONNECTION_BAD)
+    {
+        fprintf(stderr, "Connection to database '%s' failed.\n", dbName);
+        fprintf(stderr, "%s", PQerrorMessage(conn));
+        exit_nicely(conn);
+    }
+
+    /* debug = fopen("/tmp/trace.out","w"); */
+    /* PQtrace(conn, debug);  */
+
+    /* initialize the symbol table */
+    init_symbol_table();
+
+    // We process the body
+    if (!stat(argv[2],&buf)) 
+    {
+        yyin = fopen(argv[2], "r");
+        position = INBODY;
+        yylex();
+        fclose(yyin);
+     }
+
+    // We process the type
+    yyin = fopen(argv[3], "r");
+    position = INTYPE;
+    first_child = HERE;
+    no_open_source = 0;
+    spine_depth = 0;
+    depth = 0;
+    yylex(); 
+    fclose(yyin);
+    print_all(argv[1],conn);
+
+    return 0;
+} 
+
+
+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,"here = %d, pos = %d, uri = %s\n", first_child,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;
              }
+
+
+
+