The Twelf Project:TwelfTag

From The Twelf Project
Jump to: navigation, search

TwelfTag is Rob's system for non-interactively checking Twelf code. This is a guide to TwelfTag for contributors; if you are a reader, then this article may be more helpful. While Twelf Live allows people to interact with signatures, TwelfTag is designed for writing and checking code for use in wiki articles.

Neither the <twelf> tag nor the <twelflink> tag have any required arguments. The optional arguments for <twelf> tags are:

  • check={true|false|decl} (default false) - cannot be used when hidden=true
  • discard={true|false} (default false)
  • hidden={true|false} (default false)
  • import="..something.." (default "main")
  • export="..something.." (default "main")

The optional arguments for <twelflink> tags are:

  • check={true|false} (default false)
  • import="..something.." (default "main")

The following document discusses the function of each of these tags.

The <twelf> tag for syntax highlighting

The <twelf> tag itself is simple enough, it works much like an HTML <pre> environment with syntax highlighting.

However, the <twelf> tag also does a number of other interesting and useful things. At the most basic level, it crops out any whitespace at the beginning or end of the environment so that this:

<twelf>

exp : type.

abs : (exp -> exp) -> exp.

</twelf>

Will look like this:

exp : type.

abs : (exp -> exp) -> exp.

The <twelf> and <twelflink> tags

Behind the scenes, the content of every <twelf> tag is grouped together. So if you have a series of Twelf tags that are defining a single signature, like this (continuing from the example above):

app : exp -> exp -> exp.

and this:

step : exp -> exp -> type.

then TwelfTag, at this point in the process, has code for exp, abs, app, and step gathered in a group (this group is named ("main"), though it hasn't done anything with it yet.

The <twelflink> tag

You can link to a collection of all the code that has been presented so far by using <twelflink> tags in the same way you would use <a href=...> tags in normal HTML code.

As an example, <twelflink>OMG link!</twelflink>, will appear like this: OMG link!, pointing to the four lines of code declared so far throughout the file.

The filenames are just the MD5 hashes of the code which they contain; the code directory contains all these stored files.

The check=true option

We are not collecting code in the background just to link to it, we're creating code so we can check it in Twelf! If you use the twelf tag with the check=true option, Twelf will execute the collected segments in Twelf and link to the output.

<twelf check=true>
step/app1 : step (app E1 E2) (app E1' E2)
             <- step E1 E1'.
step/app2 : step (app E1 E2) (app E1 E2')
             <- step E2 E2'.
step/appabs : step (app (abs [x] E x) E') (E E').
</twelf>
step/app1 : step (app E1 E2) (app E1' E2)
             <- step E1 E1'.
step/app2 : step (app E1 E2) (app E1 E2')
             <- step E2 E2'.
step/appabs : step (app (abs [x] E x) E') (E E').
See Twelf's output

You may notice that the link above links to a file "twelf.plparty.org/code/<obvious md5 hash>.chk". The code that was checked is just at "twelf.plparty.org/code/<exact sameobvious md5 hash>" - that is, without the ".chk".

You can use <twelflink check=true> to link to the Twelf output of checking the most recent code instead of just linking to that code code - so <twelflink check=true>See?</twelflink> just duplicates the link that was automatically entered in above. See?. This works even if you haven't set check=true in any of your <twelf> tags; you could just avoid using the check=true option in your code in favor of causing checks only with <twelflink check=true>.

The check=decl option

If you want to concentrate on the output of the last code fragment, for instance to examine a particular case of type reconstruction, you can use the check=decl option for the Twelf tag. In the background, TwelfTag loads the previous portions of the signature on chatter 0, and then returns to the default chatter 3 to run the current code snippet. It then does some simple manipulations on Twelf's response to remove things like useless %% OK %% notices, and then inlines the result.

<twelf check=decl>

test = step/app1(step/app2 step/appabs).

</twelf>
test = step/app1(step/app2 step/appabs).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

test : {X1:exp} {X2:exp -> exp} {X3:exp} {X4:exp} step (app (app X1 (app (abs ([x:exp] X2 x)) X3)) X4) (app (app X1 (X2 X3)) X4) = [X1:exp] [X2:exp -> exp] [X3:exp] [X4:exp] step/app1 (step/app2 step/appabs).

%% OK %%

The discard=true option

If you add <twelf discard=true> then it will syntax highlight but will not incorporate the segment into the collected code. This is important when you want to demonstrate mistake, because otherwise Twelf will get caught up on that mistake in the future. As a result, this option is frequently used with check=decl.

<twelf discard=true check=decl>
% Don't do this!

step/appabs : step E1 E2 <- step E1 E2.
</twelf>
% Don't do this!

step/appabs : step E1 E2 <- step E1 E2.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

step/appabs : {E1:exp} {E2:exp} step E1 E2 -> step E1 E2.

%% OK %%

The import= and export= options

This is a tricky feature that allows you to run parallel segments of code on a single page. It should be used sparingly, as otherwise it can become extremely confusing to both readers and editors. Each <twelf> tag is associated with a value, import, that defines where it gets its code from, and a value, export, that defines where it binds the concatenation of the code the previous code and the new code within the tag.

  • If import= is not defined, it is assumed to be "main".
  • If export= is not defined, it is assumed to be the value of import. If you try to clobber an existing export, for instance by importing from "main" and exporting to "alt" twice, Twelf will complain.

In most cases discard=true should be sufficient for one's purposes.

This example is hopefully revealing:

<twelf import="nat">
nat : type.
</twelf>

This is a simple way of expressing nats:
<twelf import="nat" export="natsimple">
z : nat.
s : nat -> nat.
</twelf>

This is a verbose way of expressing nats:
<twelf import="nat" export="natverbose">
nat/z : nat.
nat/s : nat -> nat.
</twelf>

<twelflink import="natsimple">See the simple code</twelflink>

<twelflink import="natverbose">See the verbose code</twelflink>
nat : type.

This is a simple way of expressing nats:

z : nat.
s : nat -> nat.

This is a verbose way of expressing nats:

nat/z : nat.
nat/s : nat -> nat.

See the simple code

See the verbose code

The hidden=true option

You can use the hidden=true option to insert Twelf into a page without having it appear to the reader. You can't use the check option in conjunction with this setting, but it is quite useful in conjunction with import and export.

By inserting this code into the wiki you can add a definition of "plus" to the code group named "natsimple".

<twelf import="natsimple" hidden=true>
plus : nat -> nat -> nat -> type.

plus/z : plus z N N.
plus/s : plus (s N1) N2 (s N3)
          <- plus N1 N2 N3.
</twelf>

See the hidden code added to the existing natural number development.