--- /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.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 *source_uri;
+char *source_uri_prefix;
+
+void search(char *uri, int first_child, int position, int depth);
+%}
+
+ /***************************************************************/
+ /* 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(source_uri,source_uri_prefix);
+ sprintf(tmp,"#xpointer(1/%d)", inductive_type);
+ strcat(source_uri,tmp);
+ /* fprintf(stderr,"cinque"); */
+ free(tmp);
+ print_all(source_uri);
+ /* print_file(); */
+ }
+
+"<Constructor" { init_symbol_table();
+ no_open_source = 0;
+ depth = 0;
+ spine_depth = 0;
+ constructor++;
+ position = INTYPE;
+ first_child = HERE;
+ }
+
+"</Constructor>" { 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);
+ /* 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. */
+ /***************************************************************/
+
+int main(int argc, char *argv[])
+{
+ /* FILE *debug; */
+
+ if (argc != 3)
+ {
+ fprintf(stderr, "Usage: meta_ind <object_uri> <inductive_type_file>\n");
+ exit(1);
+ }
+
+ source_uri = malloc((sizeof('a')*2000));
+ source_uri_prefix=argv[1];
+ /* fprintf(stderr,"qua"); */
+ yyin = fopen(argv[2], "r");
+ yylex();
+
+ return 0;
+}
+
+void 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