]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
* added popup menu, implemented some functions
[helm.git] / helm / metadata / create_V7_mowgli / METADATA / meta_lex_ind.l
index 7fd23b21aa936a6f9293976685befe2947189b63..31e1416f0fbf6e833adc003e4da89d9d06e46589 100644 (file)
@@ -38,7 +38,9 @@
 %{
 #include                <string.h>
 #include                <stdlib.h>
-#include                "sthandler_ind.h"
+#include                <sys/stat.h>
+#include                <postgresql/libpq-fe.h>
+#include                "sthandler.h"
 %}
 
  /***************************************************************/
@@ -50,6 +52,7 @@
 #define                 CONST     1
 #define                 MUTIND    2
 #define                 MUTCONSTRUCT  3
+#define                 SORT      4
 
 #define                 INBODY    0
 #define                 MAINHYP   1
 
 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 = '"';
 char                    *xpointer = "#xpointer(1/";
 char                    *uri;
 char                    *tmp;
-char                    *filename;
-char                    *file_uri; 
-char                    *inductive_uri;
-char                    *filename_prefix;
-char                    *file_uri_prefix;
-
+char                    *source_uri; 
+char                    *source_uri_prefix;
+PGconn                  *conn;
 %}
 
-/*%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;
@@ -131,68 +116,105 @@ digits                  [0-9]+
                    }
 
 "</arity>"         { tmp = (char *)malloc(sizeof('a')*128);
-                     strcpy(filename,filename_prefix);
-                     fprintf(stderr,"tre");
-                     strcpy(file_uri,file_uri_prefix);
-                     sprintf(tmp,",%d.xml", inductive_type);
-                     fprintf(stderr,"quattro");
-                     strcat(filename,tmp);
+                     strcpy(source_uri,source_uri_prefix);
                      sprintf(tmp,"#xpointer(1/%d)", inductive_type);
-                     strcat(file_uri,tmp);
-                     fprintf(stderr,"cinque");
+                     strcat(source_uri,tmp);
+                     /* fprintf(stderr,"cinque"); */
                      free(tmp);
-                     print_file();
+                     print_all(source_uri,conn);
+                     /* print_file(); */
                    }
 
 "<Constructor"     { init_symbol_table();
+                     no_open_source = 0;
+                     depth = 0;
+                     spine_depth = 0;
                      constructor++;
-                     strcpy(inductive_uri,file_uri_prefix);
                      position = INTYPE;
                      first_child = HERE;
                    }
 
 "</Constructor>"   { tmp = (char *)malloc(sizeof('a')*128);
-                     strcpy(filename,filename_prefix);
-                     strcpy(file_uri,file_uri_prefix);
-                     strcpy(inductive_uri,file_uri_prefix);
-                     sprintf(tmp,",%d,%d.xml", inductive_type,constructor);
-                     strcat(filename,tmp);
+                     strcpy(source_uri,source_uri_prefix);
                      sprintf(tmp,"#xpointer(1/%d/%d)",inductive_type,constructor);
-                     strcat(file_uri,tmp);
+                     strcat(source_uri,tmp);
                      free(tmp);
-                     print_file();
+                     print_all(source_uri,conn);
+                     /* print_file(); */
                    }
 
 "<decl"            |
-"<def"             {
-                    if ((position == INTYPE) ||
-                        (position == INHYP))
+"<def"            {
+                    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;
+                      }
                    }
 
+
 .|\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 +244,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 +268,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 +285,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 +295,7 @@ digits                  [0-9]+
                    } 
 
 
+
 %%
 
  /***************************************************************/
@@ -274,58 +303,88 @@ 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");
-                   yyin = fopen("tmp/inductive_type.xml", "r");
-                   yylex();
-                   } 
-
-print_file()
 {
-                   FILE *out;
-                   if (!(out = fopen(filename,"w"))) 
-                     {
-                     fprintf(stderr, "error in openinf file %s\n", filename);
-                      exit(-1);
-                     }
-                   else
-                     {
-                      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=\"http://www.cs.unibo.it/helm/schemas/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);
-                     }
+    struct stat buf;
+
+    char       *pghost,
+               *pgport,
+               *pgoptions,
+               *pgtty;
+    char       *dbName;
+
+    /* FILE *debug; */
+
+    PGresult   *res;
+
+    if (argc != 3)
+    {
+        fprintf(stderr, "Usage: meta_ind <object_uri> <inductive_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");
+
+    /*
+     * 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);  */
+
+    source_uri = malloc((sizeof('a')*2000));
+    source_uri_prefix=argv[1];
+    /* fprintf(stderr,"qua"); */
+    yyin = fopen(argv[2], "r");
+    yylex();
+
+    return 0;
 }
 
-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;
              }
+
+
+
+