X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmetadata%2Fcreate_V7_mowgli%2FMETADATA%2Fmeta_lex_ind.l;fp=helm%2Fmetadata%2Fcreate_V7_mowgli%2FMETADATA%2Fmeta_lex_ind.l;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=acf86244658752e9388088e775fb963d18ee5e7e;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git

diff --git a/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l b/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
deleted file mode 100644
index acf862446..000000000
--- a/helm/metadata/create_V7_mowgli/METADATA/meta_lex_ind.l
+++ /dev/null
@@ -1,400 +0,0 @@
- /******************************************************************/
- /*  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                <sys/stat.h>
-#include                "sthandler_ind.h"
-%}
-
- /***************************************************************/
- /* 2. Constants and Variables Definitions                      */
- /***************************************************************/
-
-%{
-#define                 NOWHERE   0
-#define                 CONST     1
-#define                 MUTIND    2
-#define                 MUTCONSTRUCT  3
-#define                 SORT      4
-
-#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 = 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                     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;
-%}
-
- /***************************************************************/
- /* 3. Regular definitions.					*/
- /***************************************************************/
-
-uri                     [^"]+
-digits                  [0-9]+ 
-value                   [^"]+                  
-
- /***************************************************************/
- /* 4. Rules.							*/
- /***************************************************************/
-
-
-%%
-
-"<InductiveType"   { 
-                     /* fprintf(stderr,"uno"); */
-                     init_symbol_table();
-                     no_open_source = 0;
-                     depth = 0;
-                     spine_depth = 0;
-                     /* 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();
-                     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);
-                     sprintf(tmp,"#xpointer(1/%d/%d)",inductive_type,constructor);
-                     strcat(file_uri,tmp);
-                     free(tmp);
-                     print_file();
-                   }
-
-"<decl"            |
-"<def"             {
-                    if (position == INTYPE)
-                       position = MAINHYP;
-                    else if (position == MAINHYP)
-                        { position = INHYP;
-                          no_open_source++;};
-                   }
-
-"</decl>"          |
-"</def"            {
-                    if (position == INHYP)
-                     {
-                      no_open_source--;
-                      if (no_open_source == 0) 
-                        {
-                         position = MAINHYP;
-                         depth++;
-                         first_child = HERE;
-                        }
-                     }
-                    else if (position == MAINHYP)
-                      {
-                       position = INTYPE;
-                       spine_depth++;
-                       depth = 0;
-                      }
-                    first_child = HERE;
-                   }
-
-
-.|\n               {
-                   }
-
-"<LAMBDA"          |
-"<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;
-                   }
-
-"<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)
-                              {
-                                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;
-                   } 
-
-"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,")");
-                               if (position == INCONCL)
-                                  search(uri,first_child,position,spine_depth);
-                               else search(uri,first_child,position,depth);
-                               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,")");
-                            if (position == INCONCL)
-                              search(uri,first_child,position,spine_depth);
-                            else search(uri,first_child,position,depth);
-                            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, *outrel, *outsort;
-
-                   if (!(out = fopen(filename,"w"))) 
-                     {
-		      fprintf(stderr, "error in openinf file %s\n", filename);
-                      exit(-1);
-                     } 
-                   if (!(outrel = fopen("forward_rel.xml","a"))) 
-                     {
-		      fprintf(stderr, "error in openinf file forward_rel.xml\n");
-                      exit(-1);
-                     }
-                   if (!(outsort = fopen("forward_sort.xml","a"))) 
-                     {
-		      fprintf(stderr, "error in openinf file forward_rel.xml\n");
-                      exit(-1);
-                     }
-                 
-                   // We process the type
-
-                   fprintf(out,"<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n\n");
-fprintf(out,"<!DOCTYPE rdf:RDF [
-        <!ENTITY rdfns 'http://www.w3.org/1999/02/22-rdf-syntax-ns#'>
-        <!ENTITY hthns 'http://www.cs.unibo.it/helm/schemas/schema-helmth#'>
-        <!ENTITY hns 'http://www.cs.unibo.it/helm/schemas/schema-helm#'>
-
-   ]>\n");
-                   fprintf(out,"<rdf:RDF xml:lang=\"en\" xmlns:rdf=\"&rdfns;\" xmlns:h=\"&hns;\" xmlns:hth=\"&hthns;\">\n");
-                   fprintf(out,"\t<h:Object rdf:about=\"");
-                   fprintf(out,"%s",file_uri);
-                   fprintf(out,"\">\n");
-                   print_all(file_uri,out,outrel,outsort);
-                   fprintf(out,"\t</h:Object>\n");
-                   fprintf(out,"</rdf:RDF>\n");
-                   fclose(out);
-                   fclose(outrel);
-                   fclose(outsort);
-}
-
-search(uri,first_child,position,depth)
-char               *uri;
-int                first_child;
-int                position; 
-{                  
-                   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;
-             }
-
-
-
-