Re: vocabularies
Adam Naumowicz <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <Pine.GSO.4.61.0901072248110.22113@math> |
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: [email protected]
Sosnowa 64, 15-887 Bialystok, Poland http://math.uwb.edu.pl/~adamn/
======================================================================