Wiki page updates (#33)

Mostly sprucing up the percent-directive pages

wiki/astro.config.mjs

@@ -48,8 +48,7 @@ export default defineConfig({
             {
               label: "Research with Twelf",
               link: "/wiki/research-projects-using-twelf/",
-            },
-            { label: "External documentation", link: "/wiki/documentation/" },
+            }
           ],
         },
       ],

wiki/elf-to-mdx.mjs

@@ -37,10 +37,10 @@ function escapeBacktickEnv(twelfcode) {
  * @param {string[]} lines
  */
 function mutablyTrimEmptyLines(lines) {
-  while (lines.length > 0 && lines[0]?.trim() === "") {
+  while (lines[0]?.trim() === "") {
     lines.shift();
   }
-  while (lines.length > 0 && lines[lines.length - 1]?.trim() === "") {
+  while (lines[lines.length - 1]?.trim() === "") {
     lines.pop();
   }
 }
@@ -172,7 +172,7 @@ export async function elfToMdx(elfFilename) {
     if (state.type === "twelf") {
       /* Handle recognized special behavior within Twelf sections */
       if (line.trim() === "%{!! begin hidden !!}%") {
-        await reduceTwelfAccum();
+        await reduceTwelfAccum(false, true);
         if (state.subtype !== null) {
           body.push(
             "# Error line " +
@@ -194,7 +194,7 @@ export async function elfToMdx(elfFilename) {
         continue;
       }
       if (line.trim() === "%{!! begin checked !!}%") {
-        await reduceTwelfAccum();
+        await reduceTwelfAccum(false, true);
         if (state.subtype !== null) {
           body.push(
             "# Error line " +

wiki/pages/abbrev-declaration.elf

@@ -1,6 +1,7 @@
-%%! title: "Abbrev declaration"
+%%! title: "%abbrev"
+%%! description: "An %abbrev declaration allows a definition to act merely as syntactic sugar"
 
-%{! The **``%abbrev``** keyword can be placed before any [[definition]] in a Twelf [signature](/wiki/twelf-signature/) to cause the definition to, in the future, act as syntatic shorthand for some other term.
+%{! The **``%abbrev``** keyword can be placed before any <Todo>definition</Todo> in a Twelf [signature](/wiki/twelf-signature/) to cause the definition to, in the future, act as syntatic shorthand for some other term.
 
 ## Example
 
@@ -13,23 +14,19 @@ this-is-a-long-name-for-s : this-is-a-long-name-for-nat -> this-is-a-long-name-f
 %{! We can define ``nat`` and ``z`` from their long names using ``%abbrev``, and ``s`` without ``%abbrev``. !}%
 
 %abbrev nat = this-is-a-long-name-for-nat.
-%abbrev z   = this-is-a-long-name-for-z.
-s   = this-is-a-long-name-for-s.
+%abbrev z = this-is-a-long-name-for-z.
+s = this-is-a-long-name-for-s.
 
 %{! We can see the difference here - while definitions like ``s`` will be expanded only if they have to be, definitions made with the ``%abbrev`` keyword are always expanded by Twelf. !}%
-
-%{! (options removed from twelftag: check=decl) !}%
 
+%{!! begin checked !!}%
 three = s (s (s z)).
+%{!! end checked !!}%
 
 %{! ## See also
 
-* \{\{guide|title=Definitions|chapter=3|section=10\}\}
-\{\{keyword|key=abbrev\}\} !}%
+* <Guide chapter="3" section="10">Definitions</Guide>
+
+<Keyword />
 
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Abbrev_declaration).
 !}%

wiki/pages/debugging-mode-checking-errors.elf

@@ -0,0 +1,63 @@
+%%! title: Troubleshooting mode checking errors
+%%! description: There are some common pitfalls when dealing with mode checking, but many have simple solutions
+
+%{!
+There are some common pitfalls when you're dealing with [`%mode`](/wiki/percent-mode/) declarations.
+
+## Basic mode checking errors
+
+Say we give a definition of the natural numbers with addition: !}%
+
+nat: type.
+z: nat.
+s: nat -> nat.
+
+plus: nat -> nat -> nat -> type.
+%mode plus +N1 +N2 -N3.
+
+pz: plus z N N.
+ps: plus (s N1) N2 (s N3)
+     <- plus N1 N2 N3.
+
+%{! The input of `plus` is the first and second positions, and the output of `plus` is the third position, which means that whenever there are [ground](/wiki/ground/) objects in the first and second positions, that must force a ground object in the third position.
+
+If one of the output arguments is not forced to be a ground, which would be the case if the output of plus no longer matched the output of the [[subgoal]], then we get an error:
+
+```checkedtwelf
+px: plus (s N1) N2 (s N)
+     <- plus N1 N2 N3.
+```
+
+Another problem occurs when the _inputs_ to a subgoal are not known to be ground, which would happen if we mis-named one of the inputs to the subgoal.
+
+```checkedtwelf
+py: plus (s N1) N2 (s N3)
+     <- plus N N2 N3.
+```
+
+## Ordering subgoals
+
+Mode checking considers subgoals _in order_, i.e. from top to bottom when the subgoals are written out in the standard style using backwards arrows. The order of subgoals matters very much for mode checking. Say we have an identity function that maps inputs (the first position) to outputs (the second position). !}%
+
+id: nat -> nat -> type.
+%mode id +N1 -N2.
+
+id/refl: id N N.
+
+%{! The rule ``ps'`` below passes the mode checker, because the call to ``id`` takes the ground argument ``N1`` and creates a ground output ``N1'``, which is then used in the derivation for ``plus N1' N2 N3``.
+
+```checkedtwelf
+ps': plus (s N1) N2 (s N3)
+      <- id N1 N1'
+      <- plus N1' N2 N3.
+```
+
+However, if we reverse the order of the two subgoals, even though the result is logically equivalent, Twelf considers ``plus N1' N2 N3`` before ``id N1 N1'``, and so does consider ``N1'`` to be ground when it encounters it; thus, complaining accordingly:
+
+```checkedtwelf
+ps': plus (s N1) N2 (s N3)
+      <- plus N1' N2 N3
+      <- id N1 N1'.
+```
+
+!}%

wiki/pages/define-declaration.elf

@@ -1,6 +1,8 @@
-%%! title: "Define declaration"
+%%! title: "%define"
+%%! description: "A %define declaration lets the output of a %solve be used again later in an LF signature"
 
-%{! _The name of this article should be %define. There's a quirk of Unicode that causes this to not behave correctly._
+
+%{! 
 
 The **``%define``** declaration allows the outputs of a successful [``%solve``](/wiki/percent-solve/) declaration to be bound to a name which can be used later on in the context.
 
@@ -31,19 +33,20 @@ plus/s : plus (s N1) N2 (s N3)
 
 %{! We can use ``%define`` to define the natural number representing 7 by adding three and four. Note that we don't care about the proof witness in this particular case, just the output of the relation, so we put an underscore instead of an identifier to the left of the colon: !}%
 
-%{! (options removed from twelftag: check="decl") !}%
-
+%{!! begin checked !!}%
 %define n7 = N
 %solve _ : plus n4 n3 N.
+%{!! end checked !!}%
 
-%{! ## See also
-* \{\{guide|chapter=3|section=10|title=Definitions\}\}
+%{! Now `n7` is a definition that can be used again. !}%
 
-\{\{keyword|key=define\}\} !}%
+%{!! begin checked !!}%
+%solve _ : plus n7 n7 N.
+%{!! end checked !!}%
+
+
+%{! ## See also
+* <Guide chapter="3" section="10">Definitions</Guide>
 
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Define_declaration).
+<Keyword/>
 !}%

wiki/pages/deterministic-declaration.elf

@@ -1,4 +1,5 @@
-%%! title: "Deterministic declaration"
+%%! title: "%determinstic"
+%%! description: "A %determinstic declaration changes the behavior of proof search, eliminating some forms of backtracking"
 
 %{! The **``%determinstic``** declaration influences the way [logic programming](/wiki/logic-programming/) behaves in Twelf. If a type family is deterministic, then once Twelf finds a single solution through logic programming search it cannot backtrack to find different solutions.
 
@@ -79,10 +80,6 @@ searchfor : tree -> label -> type.
 * <Guide chapter="5" section="30">Deterministic Type Families</Guide>
 * [Cut](https://en.wikipedia.org/wiki/Cut_(logic_programming)) on Wikipedia
 
-<Keyword name="deterministic"/>
+<Keyword />
 
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Deterministic_declaration).
 !}%

wiki/pages/documentation.elf

@@ -1,48 +1,7 @@
 %%! title: "External documentation"
-%%! next: false
 
 %{! 
 
-The Twelf [User's Guide](/wiki/users-guide/) was the basic reference manual
-for Twelf prior to the Twelf Wiki, and is still the authoritative source for
-some topics.
-
-Besides information on this wiki, there have been a number of papers and
-tutorials explaining how to use Twelf for various purposes, as well as
-commentary on using Twelf.
-
-### Tutorials
-
-- Andrew Appel's [Hints on Proving Theorems in
-  Twelf](http://www.cs.princeton.edu/~appel/twelf-tutorial/) describes a
-  particular methodology for using Twelf that is rather different than the
-  strategy of proving [metatheorems](/wiki/metatheorem/) that predominates on
-  this wiki (also known as "the particular strange way they do it at
-  Princeton").
-- John Boyland's [Using Twelf to Prove Type
-  Theorems](https://cs.nju.edu.cn/_upload/tpl/00/aa/170/template170/proof/using-twelf.pdf)
-  john is a tutorial and experience report.
-- Dan Licata and Bob Harper have written a survey article called [Mechanizing
-  Metatheory in a Logical Framework](http://www.cs.cmu.edu/~drl/pubs/hl06mechanizing/hl06mechanizing.pdf).
-  This paper provides a more formal introduction to the modern way of thinking
-  about LF and Twelf than this site does.
-- Alberto Momigliano's [A Practical Approach to Co-induction in
-  Twelf](http://www.cs.nott.ac.uk/types06/slides/am.pdf) describes a technique
-  for encoding Twelf-unfriendly co-inductive proofs as Twelf-friendly induction
-  proofs (slides from a talk at TYPES 2006).
-- John Altidor's
-  [tutorial](http://jgaltidor.github.io/typetheory_paper.pdf) and
-  [slides](http://jgaltidor.github.io/twelf_slides.pdf) are accessible to folks
-  without a strong background in programming language foundations.
-
-### Experience reports and commentary
-
-- [The POPLmark Challenge](https://www.seas.upenn.edu/~plclub/poplmark/) has
-  commentary on the [POPLmark submission from Carnegie
-  Mellon](https://www.seas.upenn.edu/~plclub/poplmark/cmu.html) that uses Twelf.
-- Andrew Appel and Xavier Leroy's [A list-machine benchmark for mechanized
-  metatheory](https://www.cs.princeton.edu/~appel/listmachine/) serves as both
-  a tutorial and an experience report on using Twelf to prove theroems about
-  compilers.
+See [Introductions to Twelf](/wiki/introductions-to-twelf/)
 
 !}%

wiki/pages/fixity-declaration.elf

@@ -1,10 +1,9 @@
 %%! title: "Fixity declaration"
+%%! description: "The fixity declarations %infix, %prefix, and %postfix allow for fancy syntax"
 
 %{! The **``%infix``**, **``%prefix``** and **``%postfix``** declarations assign **fixity** and precedence to constants for the purpose of parsing (they have no meaning in the logic). 
 
-\{\{needs|a description of the syntax\}\}
-
-**_Higher**_ numbers bind **_tighter,**_ and the pretty printer only prints out necessary information. Hence the following example: !}%
+_**Higher**_ numbers bind **_tighter_**, and the pretty printer only prints out necessary information. Hence the following example: !}%
 
 a : type.
 b : a.
@@ -13,24 +12,16 @@ d : a.
 
 + : a -> a -> a. %infix left 1 +.
 * : a -> a -> a. %infix left 2 *.
-
-%{!  !}%
 
-%{! (options removed from twelftag: check=decl) !}%
+%{!! begin checked !!}%
 
 x : a = (b + c) * d. %% The parenthesis are necessary here
 y : a = b + (c * d). %% This means the same thing as b + c * d.
 
-%{! ## See also
-* \{\{guide|chapter=3|section=11|title=Operator Declaration\}\}
+%{!! end checked !!}%
 
-\{\{keyword|key=Fixity declaration\}\}
-
-\{\{stub\}\} !}%
+%{! ## See also
+* <Guide chapter="3" section="11">Operator Declaration</Guide>
 
-%{!
------
-This page was copied from the MediaWiki version of the Twelf Wiki.
-If anything looks wrong, you can refer to the
-[wayback machine's version here](https://web.archive.org/web/20240303030303/http://twelf.org/wiki/Fixity_declaration).
+<Keyword />
 !}%