From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 23 Feb 2004 14:03:49 +0000 (+0000)
Subject: The metadata extractor now generates also
X-Git-Tag: v0_0_4~107
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ba1f274e210f575dc5cd94500611f6bd5ad67186;p=helm.git

The metadata extractor now generates also
"INSERT INTO objectName ..."
---

diff --git a/helm/metadata/extractor/meta_lex.l b/helm/metadata/extractor/meta_lex.l
index 35bfcc9ba..a8621ea38 100644
--- a/helm/metadata/extractor/meta_lex.l
+++ b/helm/metadata/extractor/meta_lex.l
@@ -272,6 +272,9 @@ value                   [^"]+
 int main(int argc, char *argv[])
 {                  
     struct stat buf;
+    char *name;
+    char *poss;
+    char *posd;
 
     /* FILE *debug; */
 
@@ -304,6 +307,13 @@ int main(int argc, char *argv[])
     yylex(); 
     fclose(yyin);
     print_all(argv[1]);
+    poss = rindex(argv[1],'/');
+    posd = rindex(argv[1],'.');
+    name = (char *)malloc((posd - poss) * sizeof(char));
+    strncpy(name, poss + 1, posd - poss - 1);
+    name[posd - poss - 1] = '\0';
+    print_name(name,argv[1]);
+    free(name);
 
     return 0;
 } 
diff --git a/helm/metadata/extractor/meta_lex_ind.l b/helm/metadata/extractor/meta_lex_ind.l
index 2f844f9b6..271bd7db4 100644
--- a/helm/metadata/extractor/meta_lex_ind.l
+++ b/helm/metadata/extractor/meta_lex_ind.l
@@ -83,6 +83,7 @@ char                    *uri;
 char                    *tmp;
 char                    *source_uri; 
 char                    *source_uri_prefix;
+int                     waiting_for_name = 0;
 
 void search(char *uri, int first_child, int position, int depth);
 %}
@@ -94,6 +95,7 @@ void search(char *uri, int first_child, int position, int depth);
 uri                     [^"]+
 digits                  [0-9]+ 
 value                   [^"]+                  
+id                      [a-zA-Z]([-_a-zA-Z])+
 
  /***************************************************************/
  /* 4. Rules.							*/
@@ -113,14 +115,17 @@ value                   [^"]+
                      constructor=0;
                      position = INTYPE;
                      first_child = HERE;
-                   }
+                     waiting_for_name = 1;
 
-"</arity>"         { tmp = (char *)malloc(sizeof('a')*128);
+                     tmp = (char *)malloc(sizeof('a')*128);
                      strcpy(source_uri,source_uri_prefix);
                      sprintf(tmp,"#xpointer(1/%d)", inductive_type);
                      strcat(source_uri,tmp);
                      /* fprintf(stderr,"cinque"); */
                      free(tmp);
+                   }
+
+"</arity>"         {
                      print_all(source_uri);
                      /* print_file(); */
                    }
@@ -132,14 +137,16 @@ value                   [^"]+
                      constructor++;
                      position = INTYPE;
                      first_child = HERE;
-                   }
+                     waiting_for_name = 1;
 
-"</Constructor>"   { tmp = (char *)malloc(sizeof('a')*128);
+                     tmp = (char *)malloc(sizeof('a')*128);
                      strcpy(source_uri,source_uri_prefix);
                      sprintf(tmp,"#xpointer(1/%d/%d)",inductive_type,constructor);
                      strcat(source_uri,tmp);
                      free(tmp);
-                     print_all(source_uri);
+                   }
+
+"</Constructor>"   { print_all(source_uri);
                      /* print_file(); */
                    }
 
@@ -294,6 +301,16 @@ value                   [^"]+
                             first_child = AFTER;};
                    } 
 
+"name=\""{id} {
+                 if (waiting_for_name == 1) {
+                    waiting_for_name = 0;
+                    strsep(&yytext,&sep);
+                    tmp=(char *)malloc((sizeof(sep)*(strlen(yytext)+1)));
+                    strcpy(tmp,yytext);
+                    print_name(tmp,source_uri);
+                    free(tmp);
+                 }
+              } 
 
 
 %%
diff --git a/helm/metadata/extractor/sthandler.c b/helm/metadata/extractor/sthandler.c
index 6f87cdfb5..d02895293 100644
--- a/helm/metadata/extractor/sthandler.c
+++ b/helm/metadata/extractor/sthandler.c
@@ -247,6 +247,10 @@ void print_all(about,conn)
           }
 }
 
+void print_name(char *name, char *uri)
+{
+  printf("INSERT INTO objectName VALUES ('%s', '%s');\n",uri,name);
+}
 
 /****************************************************************/
 /* 5. Definitions of functions local to the module.	        */
diff --git a/helm/metadata/extractor/sthandler.h b/helm/metadata/extractor/sthandler.h
index b0305d1ec..f4e8284d5 100644
--- a/helm/metadata/extractor/sthandler.h
+++ b/helm/metadata/extractor/sthandler.h
@@ -5,4 +5,5 @@
             
 extern  void            init_symbol_table();
 extern  void            print_all(char *);
+extern  void            print_name(char *, char *);
 extern  int             search_bucket(char *, int, int);