]> matita.cs.unibo.it Git - helm.git/blob - helm/metadata/extractor/meta_lex_ind.l
New framework for metadata generation.
[helm.git] / helm / metadata / extractor / meta_lex_ind.l
1  /******************************************************************/
2  /*  Copyright (C) 2000, HELM Team                                 */ 
3  /*                                                                */
4  /* This file is part of HELM, an Hypertextual, Electronic         */
5  /* Library of Mathematics, developed at the Computer Science      */
6  /* Department, University of Bologna, Italy.                      */
7  /*                                                                */
8  /* HELM is free software; you can redistribute it and/or          */
9  /* modify it under the terms of the GNU General Public License    */
10  /* as published by the Free Software Foundation; either version   */
11  /* 2 of the License, or (at your option) any later version.       */
12  /*                                                                */
13  /* HELM is distributed in the hope that it will be useful,        */
14  /* but WITHOUT ANY WARRANTY; without even the implied warranty of */
15  /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the   */
16  /* GNU General Public License for more details.                   */
17  /*                                                                */
18  /* You should have received a copy of the GNU General Public      */
19  /* License along with HELM; if not, write to the Free Software    */
20  /* Foundation, Inc., 59 Temple Place - Suite 330, Boston,         */
21  /* MA  02111-1307, USA.                                           */
22  /*                                                                */
23  /* For details, see the HELM World-Wide-Web page,                 */
24  /* http://cs.unibo.it/helm/.                                      */
25  /******************************************************************/
26
27  /***************************************************************/
28  /*                        META_LEXAN                           */
29  /*                 Automatic Metadata Extractor                */
30  /*           First draft 11/12/2001, by Andrea Asperti         */
31  /*      more bugs added by domenico lordi on mon 12/17/2001    */
32  /***************************************************************/
33
34  /***************************************************************/
35  /* 1. Inclusion of header files.                               */
36  /***************************************************************/
37
38 %{
39 #include                <string.h>
40 #include                <stdlib.h>
41 #include                <sys/stat.h>
42 #include                "sthandler.h"
43 %}
44
45  /***************************************************************/
46  /* 2. Constants and Variables Definitions                      */
47  /***************************************************************/
48
49 %{
50 #define                 NOWHERE   0
51 #define                 CONST     1
52 #define                 MUTIND    2
53 #define                 MUTCONSTRUCT  3
54 #define                 SORT      4
55
56 #define                 INBODY    0
57 #define                 MAINHYP   1
58 #define                 INHYP     2
59 #define                 INCONCL   3
60 #define                 MAINCONCL 4
61 #define                 INTYPE    5
62 #define                 NOTFOUND  6
63
64 #define                 HERE      0     
65 #define                 AFTER     1
66
67
68 int                     where = NOWHERE;
69 int                     found = NOTFOUND;
70 int                     position = INBODY;
71 int                     first_child = HERE;
72 int                     skip = 0;     // boolean to skip the insertion of a URI
73 int                     no_open_source =0;
74 int                     spine_depth = 0;
75 int                     depth = 0;
76 int                     tmp_n;
77 int                     inductive_type = 0;
78 int                     constructor = 0;
79 int                     deep_type = 0;
80 char                    sep = '"';
81 char                    *xpointer = "#xpointer(1/";
82 char                    *uri;
83 char                    *tmp;
84 char                    *source_uri; 
85 char                    *source_uri_prefix;
86
87 void search(char *uri, int first_child, int position, int depth);
88 %}
89
90  /***************************************************************/
91  /* 3. Regular definitions.                                     */
92  /***************************************************************/
93
94 uri                     [^"]+
95 digits                  [0-9]+ 
96 value                   [^"]+                  
97
98  /***************************************************************/
99  /* 4. Rules.                                                   */
100  /***************************************************************/
101
102
103 %%
104
105 "<InductiveType"   { 
106                      /* fprintf(stderr,"uno"); */
107                      init_symbol_table();
108                      no_open_source = 0;
109                      depth = 0;
110                      spine_depth = 0;
111                      /* fprintf(stderr,"due"); */
112                      inductive_type++;
113                      constructor=0;
114                      position = INTYPE;
115                      first_child = HERE;
116                    }
117
118 "</arity>"         { tmp = (char *)malloc(sizeof('a')*128);
119                      strcpy(source_uri,source_uri_prefix);
120                      sprintf(tmp,"#xpointer(1/%d)", inductive_type);
121                      strcat(source_uri,tmp);
122                      /* fprintf(stderr,"cinque"); */
123                      free(tmp);
124                      print_all(source_uri);
125                      /* print_file(); */
126                    }
127
128 "<Constructor"     { init_symbol_table();
129                      no_open_source = 0;
130                      depth = 0;
131                      spine_depth = 0;
132                      constructor++;
133                      position = INTYPE;
134                      first_child = HERE;
135                    }
136
137 "</Constructor>"   { tmp = (char *)malloc(sizeof('a')*128);
138                      strcpy(source_uri,source_uri_prefix);
139                      sprintf(tmp,"#xpointer(1/%d/%d)",inductive_type,constructor);
140                      strcat(source_uri,tmp);
141                      free(tmp);
142                      print_all(source_uri);
143                      /* print_file(); */
144                    }
145
146 "<decl"            |
147 "<def"            {
148                     if (position == INTYPE)
149                        position = MAINHYP;
150                     else if (position == MAINHYP)
151                         { position = INHYP;
152                           no_open_source++;};
153                    }
154
155 "</decl>"          |
156 "</def>"           {
157                     if (position == INHYP)
158                      {
159                       no_open_source--;
160                       if (no_open_source == 0) 
161                         {
162                          position = MAINHYP;
163                          depth++;
164                          first_child = HERE;
165                         }
166                      }
167                     else if (position == MAINHYP)
168                       {
169                        position = INTYPE;
170                        spine_depth++;
171                        depth = 0;
172                        first_child = HERE;
173                       }
174                    }
175
176
177 .|\n               {
178                    }
179
180 "<LAMBDA"          |
181 "<MUTCASE"         |
182 "<FIX"             |
183 "<COFIX"           { 
184                           first_child = AFTER;
185                    }
186
187 "<REL"             {
188                     if (((position == INTYPE) | (position == MAINHYP)) &&
189                        (first_child == HERE))
190                      {
191                        if (position == INTYPE) /* REL on the spine */
192                          {
193                            position = INCONCL;
194                            search("Rel",first_child,position,spine_depth);
195                          }
196                        else search("Rel",first_child,position,depth);
197                        first_child = AFTER;
198                      }
199                    }
200
201 "<SORT"(" "|\n)+"value=\""{value}   {         
202                     if (((position == INTYPE) | (position == MAINHYP)) &&
203                        (first_child == HERE))
204                      {
205                        tmp=(char *)malloc((sizeof('a')*200)); 
206                        strcpy(tmp,yytext);
207                        strsep(&tmp,&sep); 
208                        if (position == INTYPE) /* SORT on the spine */
209                          { 
210                            position = INCONCL;
211                            search(tmp,first_child,position,spine_depth);
212                          }
213                        else search(tmp,first_child,position,depth);
214                        first_child = AFTER;
215                      }
216                    }
217
218 "<VAR"             {
219                      skip = 1;
220                      first_child = AFTER;
221                    }
222
223 "<CONST"           { 
224                      if (position == INTYPE) /* CONST on the spine */
225                         position = INCONCL;
226                      where = CONST;
227                    }
228
229 "<MUTIND"          { 
230                      if (position == INTYPE) /* MUTIND on the spine */
231                         position = INCONCL;
232                      where = MUTIND;
233                    }
234
235 "<MUTCONSTRUCT"    { 
236                      if (position == INTYPE) /* MUTCONSTRUCT on the spine */
237                         position = INCONCL;
238                      where = MUTCONSTRUCT;
239                    }
240
241 "uri=\""{uri}      {     
242                          if (!skip) {
243                             uri=(char *)malloc((sizeof('a')*200)); 
244                             strcpy(uri,yytext);
245                             strsep(&uri,&sep);
246                             if (where == CONST)
247                               {
248                                 if (position == INCONCL)
249                                   search(uri,first_child,position,spine_depth);
250                                 else search(uri,first_child,position,depth);
251                                 where = NOWHERE;
252                                 first_child = AFTER;
253                                 free(uri); 
254                               };
255                          } else skip = 0;
256                    } 
257
258 "noType=\""{digits} {
259                          if ((where == MUTIND) || (where == MUTCONSTRUCT))
260                           { strsep(&yytext,&sep);
261                             tmp=(char *)malloc((sizeof(sep)*(strlen(yytext)+1)));
262                             strcpy(tmp,yytext);
263                             tmp_n = atoi(tmp)+1;
264                             sprintf(tmp,"%d",tmp_n);
265                             strcat(uri,"#xpointer(1/"); 
266                             strcat(uri,tmp); 
267                           };
268                          if (where == MUTIND) 
269                              { 
270                                strcat(uri,")");
271                                if (position == INCONCL)
272                                   search(uri,first_child,position,spine_depth);
273                                else search(uri,first_child,position,depth);
274                                free(uri);
275                                free(tmp);
276                                where = NOWHERE; 
277                                first_child = AFTER;};
278                    } 
279
280 "noConstr=\""{digits} {
281                          if (where == MUTCONSTRUCT)
282                           { strsep(&yytext,&sep);
283                             tmp=(char *)malloc((sizeof(sep)*(strlen(yytext)+1)));
284                             strcpy(tmp,yytext);
285                             strcat(uri,"/");
286                             strcat(uri,tmp);
287                             strcat(uri,")");
288                             if (position == INCONCL)
289                               search(uri,first_child,position,spine_depth);
290                             else search(uri,first_child,position,depth);
291                             free(uri);
292                             free(tmp);
293                             where = NOWHERE; 
294                             first_child = AFTER;};
295                    } 
296
297
298
299 %%
300
301  /***************************************************************/
302  /* 6. Auxiliary functions.                                     */
303  /***************************************************************/
304
305 int main(int argc, char *argv[])
306 {
307     /* FILE *debug; */
308
309     if (argc != 3)
310     {
311         fprintf(stderr, "Usage: meta_ind <object_uri> <inductive_type_file>\n");
312         exit(1);
313     }
314
315     source_uri = malloc((sizeof('a')*2000));
316     source_uri_prefix=argv[1];
317     /* fprintf(stderr,"qua"); */
318     yyin = fopen(argv[2], "r");
319     yylex();
320
321     return 0;
322 }
323
324 void search(uri,first_child,position,depth)
325 char               *uri;
326 int                first_child;
327 int                position; 
328 {                  
329                    if (position == MAINHYP)
330                       { 
331                        if (first_child == HERE) 
332                            found = search_bucket(uri,MAINHYP,depth);
333                        else 
334                            found = search_bucket(uri,INHYP,0);
335                       }
336                    else if (position == INCONCL)
337                       { 
338                        if (first_child == HERE) 
339                            found = search_bucket(uri,MAINCONCL,depth);
340                        else
341                            found = search_bucket(uri,INCONCL,0);
342                       }
343                         
344                    else 
345                       found = search_bucket(uri,position,depth);
346                    /* if (found == NOTFOUND)
347                          printf( "pos = %d, uri = %s\n", position, uri);  */
348 }
349
350
351 int yywrap() {
352                return 1;
353              }
354
355
356
357