Re: [mizar] vocabularies

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

Hi Josef,

On Wed, 7 Jan 2009, Josef Urban wrote:

> On Wed, 7 Jan 2009, trybulec wrote:
>
> > Freek Wiedijk wrote:
> >
> > > Of course you could also have a _separate_ tool that would
> > > find all theorems used by your article, and then update the
> > > article if necessary, by adding missing references to the
> > > theorems directive.
> > OK with me. You have to write new SCANNER.  If SCANNER would pass the token 
> > as the file name,
> > then action for PARSER is clear: take the spelling and write in on a file 
> > or somewhere.
>
> something like:
> perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;]*);/g) 
> {@a=$1=~m/[\s,](\w*)\s*:/g; @h{@a}=()} print join(",", sort keys %h),"\n"' 
> foo.miz

I like your 'constructive' argument in the discussion very much :-) 
Indeed, it seems to work fast enough to simply put it in the user 
interface (either the mizf script or Emacs mode) as an independent pass 
and not complicate the parser at all. But I noticed that your hack, as it 
stands now, won't work well with iterative equalities (no semicolon after 
some by's), if a reference starts the justification of the first iteration 
step (no extra space or comma) and also if terms like the Cartesian 
product ([:X,Y:]) occur in the equalities. Still, a slightly modified 
version passed a few tests I could think of right now:

perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;.]*)(;|\.)/g) 
{@a=$1=~m/,?(\w*)\s*:/g; @h{@a}=()}
print join(",", sort keys %h),"\n"' foo.miz

Best,

Adam

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================