]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
New version for the new DTD.
[helm.git] / helm / metadata / create_V7_mowgli / METADATA / meta_lex_ind.l
diff --git a/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l b/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
new file mode 100644 (file)
index 0000000..6d09578
--- /dev/null
@@ -0,0 +1,331 @@
+ /******************************************************************/
+ /*  Copyright (C) 2000, HELM Team                                 */ 
+ /*                                                                */
+ /* This file is part of HELM, an Hypertextual, Electronic         */
+ /* Library of Mathematics, developed at the Computer Science      */
+ /* Department, University of Bologna, Italy.                      */
+ /*                                                                */
+ /* HELM is free software; you can redistribute it and/or          */
+ /* modify it under the terms of the GNU General Public License    */
+ /* as published by the Free Software Foundation; either version   */
+ /* 2 of the License, or (at your option) any later version.       */
+ /*                                                                */
+ /* HELM is distributed in the hope that it will be useful,        */
+ /* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+ /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the   */
+ /* GNU General Public License for more details.                   */
+ /*                                                                */
+ /* You should have received a copy of the GNU General Public      */
+ /* License along with HELM; if not, write to the Free Software    */
+ /* Foundation, Inc., 59 Temple Place - Suite 330, Boston,         */
+ /* MA  02111-1307, USA.                                           */
+ /*                                                                */
+ /* For details, see the HELM World-Wide-Web page,                 */
+ /* http://cs.unibo.it/helm/.                                      */
+ /******************************************************************/
+
+ /***************************************************************/
+ /*                       META_LEXAN                           */
+ /*                 Automatic Metadata Extractor                */
+ /*           First draft 11/12/2001, by Andrea Asperti         */
+ /*      more bugs added by domenico lordi on mon 12/17/2001    */
+ /***************************************************************/
+
+ /***************************************************************/
+ /* 1. Inclusion of header files.                              */
+ /***************************************************************/
+
+%{
+#include                <string.h>
+#include                <stdlib.h>
+#include                "sthandler_ind.h"
+%}
+
+ /***************************************************************/
+ /* 2. Constants and Variables Definitions                      */
+ /***************************************************************/
+
+%{
+#define                 NOWHERE   0
+#define                 CONST     1
+#define                 MUTIND    2
+#define                 MUTCONSTRUCT  3
+
+#define                 INBODY    0
+#define                 MAINHYP   1
+#define                 INHYP     2
+#define                 INCONCL   3
+#define                 MAINCONCL 4
+#define                 INTYPE    5
+#define                 NOTFOUND  6
+
+#define                 HERE      0     
+#define                 AFTER     1
+
+
+int                    where = NOWHERE;
+int                     found = NOTFOUND;
+int                     position = INTYPE;
+int                     first_child = HERE;
+int                    skip = 0;     // boolean to skip the insertion of a URI
+int                     no_open_source =0;
+int                     tmp_n;
+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;
+
+%}
+
+/*%x deeptype*/
+
+
+ /***************************************************************/
+ /* 3. Regular definitions.                                    */
+ /***************************************************************/
+
+uri                     [^"]+
+digits                  [0-9]+                   
+
+ /***************************************************************/
+ /* 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");
+                     init_symbol_table();
+                     fprintf(stderr,"due");
+                     inductive_type++;
+                     constructor=0;
+                     position = INTYPE;
+                     first_child = HERE;
+                   }
+
+"</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);
+                     sprintf(tmp,"#xpointer(1/%d)", inductive_type);
+                     strcat(file_uri,tmp);
+                     fprintf(stderr,"cinque");
+                     free(tmp);
+                     print_file();
+                   }
+
+"<Constructor"     { init_symbol_table();
+                     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);
+                     sprintf(tmp,"#xpointer(1/%d/%d)",inductive_type,constructor);
+                     strcat(file_uri,tmp);
+                     free(tmp);
+                     print_file();
+                   }
+
+"<decl"            |
+"<def"             {
+                    if ((position == INTYPE) ||
+                        (position == INHYP))
+                        { position = INHYP;
+                          no_open_source++;};
+                   }
+
+"</decl>"          |
+"</def"            {
+                    if (position == INHYP)
+                     {
+                      no_open_source--;
+                      if (no_open_source == 0) 
+                       { position = INTYPE;
+                         first_child = HERE; };
+                     };
+                   }
+
+.|\n               {
+                   }
+
+"<LAMBDA"          |
+"<REL"             |
+"<MUTCASE"         |
+"<FIX"             |
+"<COFIX"           { 
+                          first_child = AFTER;
+                   }
+
+"<VAR"             {
+                     skip = 1;
+                     first_child = AFTER;
+                   }
+
+"<CONST"           { 
+                     if (position == INTYPE) /* CONST on the spine */
+                        position = INCONCL;
+                     where = CONST;
+                   }
+
+"<MUTIND"          { 
+                     if (position == INTYPE) /* MUTIND on the spine */
+                        position = INCONCL;
+                     where = MUTIND;
+                   }
+
+"<MUTCONSTRUCT"    { 
+                     if (position == INTYPE) /* MUTCONSTRUCT on the spine */
+                        position = INCONCL;
+                     where = MUTCONSTRUCT;
+                   }
+
+"uri=\""{uri}      {     
+                         if (!skip) {
+                            uri=(char *)malloc((sizeof('a')*200)); 
+                            strcpy(uri,yytext);
+                            strsep(&uri,&sep);
+                            if (where == CONST)
+                                {
+                                   search(uri,first_child,position); 
+                                   where = NOWHERE;
+                                   first_child = AFTER;
+                                   free(uri); 
+                                 };
+                         } else skip = 0;
+                   } 
+
+"noType=\""{digits} {
+                         if ((where == MUTIND) || (where == MUTCONSTRUCT))
+                          { strsep(&yytext,&sep);
+                            tmp=(char *)malloc((sizeof(sep)*(strlen(yytext)+1)));
+                            strcpy(tmp,yytext);
+                            tmp_n = atoi(tmp)+1;
+                            sprintf(tmp,"%d",tmp_n);
+                            strcat(uri,"#xpointer(1/"); 
+                            strcat(uri,tmp); 
+                          };
+                         if (where == MUTIND) 
+                             { 
+                               strcat(uri,")");
+                               search(uri,first_child,position); 
+                               free(uri);
+                               free(tmp);
+                               where = NOWHERE; 
+                               first_child = AFTER;};
+                   } 
+
+"noConstr=\""{digits} {
+                         if (where == MUTCONSTRUCT)
+                          { strsep(&yytext,&sep);
+                            tmp=(char *)malloc((sizeof(sep)*(strlen(yytext)+1)));
+                            strcpy(tmp,yytext);
+                            strcat(uri,"/");
+                            strcat(uri,tmp);
+                            strcat(uri,")");
+                            search(uri,first_child,position);
+                            free(uri);
+                            free(tmp);
+                            where = NOWHERE; 
+                            first_child = AFTER;};
+                   } 
+
+
+%%
+
+ /***************************************************************/
+ /* 6. Auxiliary functions.                                    */
+ /***************************************************************/
+
+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=\"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);
+                     }
+}
+
+search(uri,first_child,position)
+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); */
+                    }
+
+int yywrap() {
+               return 1;
+             }