+++ /dev/null
- /******************************************************************/
- /* 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;
- }
-
-
-
-
projects / helm.git / blobdiff