X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmetadata%2Fcreate4%2FMETADATA%2Fmeta_lex.l;fp=helm%2Fmetadata%2Fcreate4%2FMETADATA%2Fmeta_lex.l;h=7c3d0b43f3467dac91663580a1bdc9daf3c48535;hb=d415fd267ae0991619f64412c3b388af4975317e;hp=0000000000000000000000000000000000000000;hpb=20dacdd66818f115aab029824b7408c0d4f804c4;p=helm.git

diff --git a/helm/metadata/create4/METADATA/meta_lex.l b/helm/metadata/create4/METADATA/meta_lex.l
new file mode 100644
index 000000000..7c3d0b43f
--- /dev/null
+++ b/helm/metadata/create4/METADATA/meta_lex.l
@@ -0,0 +1,263 @@
+ /******************************************************************/
+ /*  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         */
+ /***************************************************************/
+
+ /***************************************************************/
+ /* 1. Inclusion of header files.				*/
+ /***************************************************************/
+
+%{
+#include                <string.h>
+#include                <stdlib.h>
+#include                "sthandler.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                 BEFORE    0
+#define                 HERE      1     
+#define                 AFTER     2
+
+
+int			where = NOWHERE;
+int                     found = NOTFOUND;
+int                     position = INBODY;
+int                     first_child = BEFORE;
+int                     no_open_source =0;
+int                     tmp_n;
+char                    sep = '"';
+char                    *xpointer = "#xpointer(1/";
+char                    *uri;
+char                    *tmp;
+%}
+
+ /***************************************************************/
+ /* 3. Regular definitions.					*/
+ /***************************************************************/
+
+uri                     [^"]+
+digits                  [0-9]+                   
+
+ /***************************************************************/
+ /* 4. Rules.							*/
+ /***************************************************************/
+
+
+
+%%
+
+"<type>"           { 
+                     position = INTYPE;
+                     first_child = BEFORE;
+                   }
+
+"<source"          {
+                    if ((position == INTYPE) ||
+                        (position == INHYP))
+                        { position = INHYP;
+                          no_open_source++;};
+                    /* printf("source %d\n", no_open_source); */
+                   }
+
+"</source>"        {
+                    if (position == INHYP)
+                     {
+                      no_open_source--;
+                      /* printf("source %d\n", no_open_source); */
+                      if (no_open_source == 0) 
+                       { position = INTYPE;
+                         first_child = BEFORE; };
+                     };
+                   }
+
+
+"<body>"           { 
+                     position = INBODY;
+                   }
+
+.|\n               {
+                   }
+
+"<APPLY"           {
+                    if (first_child == BEFORE)
+                          first_child = HERE;
+                    else if (first_child == HERE)
+                          first_child = AFTER; 
+                   } 
+
+"<LAMBDA"          |
+"<REL"             |
+"<MUTCASE"         |
+"<FIX"             |
+"<COFIX"           { 
+                    if ((first_child == BEFORE) || (first_child == HERE))
+                          first_child = AFTER;
+                   }
+
+"<CONST"           { 
+                     if (position == INTYPE) /* CONST on the spine */
+                        position = INCONCL;
+                     if (first_child == BEFORE)
+                          first_child = HERE;
+                     where = CONST;
+                   }
+
+"<MUTIND"          { 
+                     if (position == INTYPE) /* MUTIND on the spine */
+                        position = INCONCL;
+                     if (first_child == BEFORE)
+                          first_child = HERE;
+                     where = MUTIND;
+                   }
+
+"<MUTCONSTRUCT"    { 
+                     if (position == INTYPE) /* MUTCONSTRUCT on the spine */
+                        position = INCONCL;
+                     if (first_child == BEFORE)
+                          first_child = HERE;     
+                     where = MUTCONSTRUCT;
+                   }
+
+"uri=\""{uri}      {     
+                         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); 
+                              };
+                   } 
+
+"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[])
+{                  
+                   init_symbol_table();
+                   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=\"http:/www.cs.unibo.it/helm/schemas/schema-h.rdf#\">\n");
+                   printf("<h:Object rdf:about=\"");
+                   printf("%s",argv[1]);
+                   printf("\">\n");
+                   print_all();
+                   printf("</h:Object>\n");
+                   printf("</rdf:RDF>\n");
+                   } 
+
+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;
+             }
+
+
+
+
+
+
+