% !TEX root = roll_your_own.tex
\chapter{The paragraph and formula languages}
\label{appx:paraformlang}

The paragraph language is the one in which logics, their syntax, their rules, the tactics you intend to use and the menus of commands you intend to display are all defined. It uses a lot of reserved words: I add to the list as the need arises but all are multi-letter upper-case words, so it is a good idea to avoid use of that kind of word in your encodings.

At the time of writing the complete list of reserved words is
\begin{quote}
\textsc{abstraction, and, are, automatch, autounify, bag, beforebutton, beforeentry, bind, button, checkbox, children, class, command, concfresh, conchit, conjecturepanel, constant, currentproof, cut, derived, distinct, disproof, end, entry, fonts, forcedef, formula, formulae, fresh, from, givenpanel, hypfresh, hyphit, identity, impconcfresh, impfresh, imphypfresh, in, infer, infix, infixc, initially, initialise, is, juxtfix, keyboard, label, labels, leftfix, leftweaken, list, macro, menu, menukey, midfix, notin, notoneof, number, object, outfix, patchalert, popsyntax, postfix, prefix, proof, pushsyntax, radiobutton, reflexive, renameentry, rightfix, rightweaken, rule, rules, scope, semantics, semanticturnstile, separator, sequent, string, structurerule, substfix, tactic, tacticpanel, theorem, theorems, theory, transitive, umenu, unifieswith, use, variable, view, weaken, where, world}
\end{quote}

%     ""; "";   
%(what the hell are these for? I put them here as a reminder, but I can't remember what's going on ...)
 
\section{Directives}

In this description I use [... {\textbar} ... ] to describe alternatives, \{ ... \} to describe optional components, and ellipsis to denote optional repetition. I've used $|-$ as an entailment symbol: you choose the actual symbol in a \textsc{sequent} directive (see \secref{paraformlang:flexisyntax}).

\begin{description}
\item[\textsc{abstraction}]: decorates a parameter in a \textsc{rule} or \textsc{theorem} directive. When the rule is instantiated, applications of this parameter to arguments are translated into substitutions, with a substitution variable which is made an \textsc{object} parameter of the rule. The effect is to simulate predicate notation with that parameter.

\item[\textsc{and}]: separator.

\item[\textsc{are}]: separator.

\item[\textsc{automatch} %\textit{tacticname ... tacticname}] 
\textit{tactic}]: at the end of each proof step, run the %tactics (usually they are rules) 
tactic (usually a rule) over each open tip of the tree, but only allow %them 
it to work by `matching' --- that is, don't allow any unknowns in the tree to change as a result (see also \textsc{match} in the tactic language). (\textsc{automatch} is supposed to work with a space-separated sequence of tactics, and it used to, but at present it doesn't. )

\item[\textsc{autounify} %\textit{tacticname ... tacticname}] 
\textit{tactic}]: same as \textsc{automatch} but without the restriction on working by `matching'. This directive is less used than \textsc{automatch}, chiefly because it is easy to make automatic steps which make large and/or unexpected and/or unhelpful changes to a proof. But sometimes it is the right thing: see for example the way that the Hindley-Milner algorithm encodings use \textsc{autounify} to determine the type of constants. (\textsc{autounify} is supposed to work with a space-separated sequence of tactics, and it used to, but at present it doesn't. )

\item[\textsc{bag \{} \texttt{<}kind\texttt{>} \textsc{\}} \textit{names}]: see \secref{paraformlang:flexisyntax}.

\item[\textsc{beforeentry} \textit{label} \textsc{entry}]: inserts an entry into a menu at a particular point.

\item[\textsc{bind} \textit{variable ... variable} \textsc{scope} \textit{name ... name} \textsc{in} \textit{formula}]: see \secref{paraformlang:flexisyntax}.

\item[\textsc{button} \textit{label} \{ \textsc{is} \} \textit{command}]: allows you to attach a command to a label in a menu or a button on a panel (see \appxref{GUIlang}).

\item[\textsc{checkbox} \textit{variable label} \{ \textsc{initially [} true {\textbar} false \textsc{]} \}]: a checkbox is created associated with the named variable. If the variable doesn't exist in Jape's default environment this directive declares it, and its range of values will be true and false; if it exists, those must already be its range. The initial value, if included, is immediately assigned to the variable.

In a menu, \textit{label} appears ticked or unticked according to whether or not the value of \textit{variable} is true or false; in a panel you see a proper user-interface checkbox with that label.

\item[\textsc{children}]: see \textsc{world}. 

\item[\textsc{class}  \texttt{<}kind\texttt{>} \textit{names}]: see \secref{paraformlang:flexisyntax}.

\item[\textsc{command}]: in a panel button description, replaced by the command of the selected entry.

\item[\textsc{concfresh} \textit{variable}]: proviso that \textit{variable} doesn't occur free in any right-hand-side formula of the consequent of a proof step. See \textsc{fresh}.

\item[\textsc{conchit} \{ \{ \textit{formula1} \} |- \} \textit{formula2} \textsc{is} \textit{tactic}]: if the user double-clicks on a right-hand-side formula matching \textit{formula2} then run \textit{tactic}. If \textit{formula1} also appears, then either the sequent must have a single left-hand-side formula matching it, or the user must also have selected a left-hand-side formula matching it. See also \textsc{hyphit}.

\item[\textsc{conjecturepanel} \textit{name} \{ \textsc{is} \} {[} \textit{entry} {\textbar} \textit{button} {]}* \textsc{end}]: build a panel of conjectures. Each \textit{entry} is one of \textsc{theorem, theorems, derived rule, proof, currentproof} (the last two in saved-proof files); each \textit{button} is either \textsc{entry} or \textsc{button}. Entries add to the list of conjectures in the panel. 

In addition to the buttons explicitly described, every conjecture panel always has ``New\dots'', ``Prove'' and ``Show Proof'' buttons, and if there isn't a description of an ``Apply'' button then one is added as if you had written ``\textsc{button} Apply \textsc{is} apply \textsc{command}''. Like \textsc{menu}, a panel description can be divided into sections, and the complete description is just the concatenation of the various parts.

\item[\textsc{constant} \textit{name ... name}]: the \textit{name}s are defined to have the syntactic class \textsc{constant}. See \secref{paraformlang:flexisyntax}.

\item[\textsc{currentproof} \textit{name sequent} \{ \textsc{where} \textit{provisos} \} \{ \textsc{formulae} \textit{formulae} \} \textsc{is} \textit{tactic}]: same as \textsc{proof}, except that the proof of \textit{sequent} built by \textit{tactic} need not be complete, is not recorded in the proof store, and is displayed on the screen.

\item[\textsc{cut} \textit{rulename}]: synonym for \textsc{structurerule} \textsc{cut}; see \secref{paraformlang:structurerules}.

\item[\textsc{derived}]: used in \textsc{derived rule} to specify a rule that needs proof.

\item[\textsc{distinct} \textit{variable, ..., variable}]: synonym for lots of \textsc{notin} provisos. Used, especially, to shorten proof display of provisos.

\item[\textsc{disproof}]: obsolete; see \textsc{currentproof} and \textsc{proof}.

\item[\textsc{end}]: closer in lots of directives.

\item[\textsc{entry} \textit{name} \{ \{ \textsc{is} \} \textit{tactic} \} \{ \textsc{menukey} \textit{letter} \}]: describes an entry in a menu or in the list of a panel. May only appear as part of a \textsc{menu} or \textsc{panel} directive; \textsc{menukey} is permitted when part of a \textsc{menu} directive. The label is \textit{name}; if the \textit{tactic} component is omitted then the tactic expression \textit{name} is used; if the \textsc{menukey} component is included then \textit{letter} is used as the `command key' of that label. When the label is selected in a menu, the command ``apply \textit{tactic}'' is transmitted to the proof engine; when the label is selected in a panel, there is no effect until a \textsc{button} is pressed.

\item[\textsc{fonts} \textit{name}]: Obsolete.

\item[\textsc{forcedef} \textit{formula} {[}\textsc{is}{]} \textit{forcing\_definition}]: Part of the way that Kripke semantics is described. See \textj{I2L\_disproof.j}.

\item[\textsc{formula} \textit{name ... name}]: the \textit{name}s are declared to be in the syntactic class \textsc{formula}. See \secref{paraformlang:flexisyntax}.

\item[\textsc{formulae}]: separator in \textsc{proof} and \textsc{currentproof}.

\item[\textsc{fresh} \textit{variable}]: proviso in a rule or theorem. \textit{Variable} mustn't appear free in any hypothesis or conclusion of the sequent to which the rule or theorem is applied. This proviso is translated into \textsc{notin} provisos for each of the formulae of that sequent.

\item[\textsc{from}]: separator.

\item[\textsc{givenpanel}]: you can make panels of `given' antecedents when proving derived rules.

\item[\textsc{hypfresh} \textit{variable}]: \textit{variable} doesn't occur free in any hypothesis of the problem sequent. See \textsc{fresh.}

\item[\textsc{hyphit} \textit{formula1} |- \{ \textit{formula}2 \} \textsc{is} \textit{tactic}]: if the user double-clicks on a left-hand-side \textit{formula}1 then run \textit{tactic}. If \textit{formula}2 appears then either the sequent must have a single right-hand side which matches \textit{formula}2, or the user must also select a right-hand-side formula matching \textit{formula}2 in order for \textit{tactic} to fire.

\item[\textsc{identity} \textit{rulename}]: synonym for \textsc{structurerule} \textsc{identity}; see \secref{paraformlang:structurerules}.

\item[\textsc{in}]: connective in binding directive.

\item[\textsc{impconcfresh}, \textsc{impfresh}, \textsc{imphypfresh}]: something internal to do with the processing of \textsc{fresh} provisos. I can't remember what they do; I hope you never see one.

\item[\textsc{ infer }]: connective in \textsc{rule} directive.

\item[\textsc{infix} \textit{precedence} \textsc{[} L {\textbar} R {\textbar} T \textsc{]} \textit{operatorname ... operatorname}]: the names are declared to be infix binary operators with the given precedence; L means left-associative, R right-associative, T tupling. Instances of formulae such as \textit{A} \textit{op} \textit{B} are then treated internally as if they were `uncurried' function applications --- that is, as if you had written (\textit{op})(\textit{A},\textit{B}). Note no commas. See \secref{paraformlang:flexisyntax}.

\item[\textsc{infixc} \textit{precedence} \textsc{[} L {\textbar} R {\textbar} T \textsc{]} \textit{operatorname ... operatorname}]: similar to \textsc{infix}, but parsed `curried' so that \textit{A} \textit{op} \textit{B} is then treated internally as if you had written (\textit{op}) \textit{A} \textit{B}.

\item[\textsc{initially}]: part of the \textsc{radiobutton} and \textsc{checkbox} directives.

\item[\textsc{initialise} \textit{variablename} \textit{value}]: the variable named is assigned the value given. See the discussion of variables in \appxref{GUIlang}.

\item[\textsc{is}]: connective, often omitted.

\item[\textsc{judgement}]: Obsolete.

\item[\textsc{juxtfix} \textit{precedence}]: defines syntactic precedence of juxtaposition: see \secref{paraformlang:flexisyntax}.

\item[\textsc{keyboard} \textit{symbol} ... \textit{symbol}]: defines the symbols to be included on the on-screen keyboard in appropriate input windows (Unify, Text Command, etc.). In the absence of a \textsc{keyboard} directive, you get all the symbols that don't appear on the average real keyboard, in no particular order.

\item[\textsc{label}]: in a panel button description, insert the label of the selected entry. Cf. \textsc{command}.

\item[\textsc{labels}]: part of the notation used to define Kripke trees in saved proofs/disproofs.

\item[\textsc{leftfix} \textit{precedence} \textit{bra} \{ \textit{punct}1 \textit{... punctN} \}]: defines bracketed form which misses a closing bracket. See \secref{paraformlang:flexisyntax}.

\item[\textsc{leftweaken} \textit{rulename}]: synonym for \textsc{structurerule} \textsc{leftweaken}; see \secref{paraformlang:structurerules}.

\item[\textsc{list \texttt{<}}kind\textsc{\texttt{>}} \textit{names}]: the names are declared to be in the syntactic class \textsc{list}; see \secref{paraformlang:flexisyntax}.

\item[\textsc{macro}]: a variant of \textsc{tactic}. A \textsc{macro}'s arguments aren't evaluated; they are useful mostly because you can pass patterns like \_A=\_B as arguments.

\item[\textsc{menu} \textit{name} \textsc{is} \textit{entry ... entry} \textsc{end}]: the effect of the entries (which can be \textsc{rule, rules, derived rule, tactic, theorem, theorems, theory, proof, currentproof, entry, button, radiobutton, checkbox} or \textsc{separator)} are added to the menu named \textit{name}. \textsc{menu} directives for the same menu are accumulated in sequence, and need not be given all in one place.

\item[\textsc{menukey} \textit{letter}]: part of the \textsc{entry} directive when used inside a \textsc{menu} description.

\item[\textsc{midfix} \textit{priority} \textit{symbol} ... \textit{symbol}]\! like \textsc{leftfix} and \textsc{rightfix}, but without an opening or closing bracket, only separators.
 
\item[\textit{name} \textsc{notin} \textit{formula}]: a proviso that \textit{name} must not occur free in \textit{formula}. Often generated as the result of a \textsc{fresh, hypfresh} or \textsc{concfresh} proviso; sometimes included in its own right.

\item[\textsc{number} \textit{name ... name}]: the \textit{name}s are declared to be in the syntactic class \textsc{number}. See \secref{paraformlang:flexisyntax}.

\item[\textsc{notoneof}]: directive is \textit{variable} \textsc{in} \textit{pattern} \textsc{notoneof} \textit{listformula}. It's a terrible hack, used (so far only in) the Hindley-Milner encoding to try to implement an environment stack in the context (oh dear!). Example:
\begin{japeish}
RULE "C ⊢ x⇒S" WHERE x IN x⇒S' NOTONEOF C' IS INFER C,x⇒S,C' ⊢ x⇒S
\end{japeish}

\item[\textsc{object} \textit{name}]: decorates a parameter in a \textsc{rule} or \textsc{theorem} directive. When the rule is instantiated, the parameter is replaced by a newly-minted variable rather than an unknown (e.g. x rather than \_x), unless this default assignment is overridden by provision of an argument formula.

\item[\textsc{outfix} \textit{bra} \{ \textit{punct1} ... \textit{punctN} \} \textit{ket}]: bracketed form with optional internal separators; see \secref{paraformlang:flexisyntax}.

\item[\textsc{patchalert}]: for overriding alert messages. See \chapref{Hoare}.

\item[\textsc{popsyntax}]: see \textsc{pushsyntax}.

\item[\textsc{pushsyntax} \textit{syntax definitions} \textsc{popsyntax}]: It's possible to inherit  syntactic descriptions by enclosing them in \textsc{pushsyntax} / \textsc{popsyntax} brackets. The outer syntax must express all the symbols of the inner, but not necessarily with the same syntactic priorities.

\item[\textsc{postfix} \textit{precedence operator ... operator}]: postfix operators; see \secref{paraformlang:flexisyntax}.

\item[\textsc{prefix} \textit{precedence operator ... operator}]: prefix operators; see \secref{paraformlang:flexisyntax}.

\item[\textsc{proof} \textit{name sequent} \{ \textsc{where} \textit{provisos} \} \{ \textsc{formulae} \textit{formulae} \} \textsc{is} \textit{tactic}]: generated when you save proofs. \textit{Sequent} (together with \textit{provisos} if present) is a statement of the conjecture named \textit{name}, and \textit{tactic}, when run, will produce a proof of that conjecture. \textit{Formulae}, if present, are a numbered list of the formulae that occur in \textit{tactic}, provided to reduce the size of the directive and thus the cost of reading it all in (really!). If it all works out: if \textit{sequent} unifies with the statement of conjecture \textit{name}, if \textit{tactic} produces a completed proof without introducing any additional unifications or inventing more or less provisos, then the resulting proof is stored under \textit{name} in the proof store.

\item[\textsc{radiobutton} \textit{variablename} \{ \textsc{is} \} \textit{label} \{ \textsc{is} \} \textit{value} \{ \textsc{and} \textit{label} \{ \textsc{is} \} \textit{value} \}* \{ \textsc{initially} \textit{value} \} \textsc{end}]: a radio button with the list of labels given is associated with the named variable. If that variable doesn't exist it is declared by this directive, and its range of possible values is those given here; if it does exist the values given here must be in its range. If an initial value is given, the variable is assigned that value immediately.

In a menu a radio button is shown as a sequence of labels, one of which is ticked according to the value of the variable. Currently you can't put a radio button in a panel (sorry).%; in a panel it is a proper Macintosh-style radio button.

\item[\textsc{reflexive} \textit{rule name}]: declares r\^ole of a rule. Rule must be of the form A \textit{op} A.

\item[\textsc{renameentry} \textit{oldlabel} \textit{newlabel}]: change the labelling in a menu.

\item[\textsc{rightfix} \textit{precedence} \{ \textit{punct}1 ... \textit{punctN} \} \textit{ket}]: defines bracketed form with closing bracket but no opening bracket. See \secref{paraformlang:flexisyntax}.

\item[\textsc{rightweaken}]: synonym for \textsc{structurerule} \textsc{rightweaken}; see \secref{paraformlang:structurerules}.

\item[\textsc{rule} \textit{rule}]: definition of a rule. Puts a \textit{rule} into the tactic store with name \textit{name}; if it appears inside a \textsc{menu} or \textsc{panel} definition then the effect is also of \textsc{entry} \textit{name} \textsc{is} \textit{name}. See \secref{paraformlang:rulestacticsconjectures}.

\item[\textsc{rules} \textit{name} \{ ( \textit{params} ) \} \{ \textsc{where} \textit{provisos} \} \textsc{are} \textit{rule1} \textsc{and ... and} \textit{ruleN} \textsc{end}]: definition of a number of rules, organised automatically into an \textsc{alt} tactic.

Each \textit{rule} is an unnamed rule definition (see \secref{paraformlang:rulestacticsconjectures}); each is considered to be qualified by \textit{params} and \textit{provisos} from the head of the directive, filtered according to the names that occur in each rule (that is, if a particular parameter doesn't occur in a rule, you don't get that parameter declaration with that rule, and you don't get any provisos that mention it). The rules are entered into the tactic store under the names \textit{name'1 ... name'N}; at the same time a tactic \textsc{alt} \textit{name'1 ... name'N} is entered under \textit{name}.

If it occurs in a \textsc{menu} or a \textsc{panel} directive, \textsc{rules} \textit{name ...} has the effect also of \textsc{entry} \textit{name}: several rules are defined, but only one entry appears.

\item[\textsc{scope}]: part of the \textsc{bind} directive.

\item[\textsc{semantics}]: see \textsc{world} (I'll add more here soon).

\item[\textsc{semanticturnstile} \textsc{entailssymbol} \textsc{semanticturnstile}]: defines the semantic turnstile associated with a particular entails symbol (syntactic turnstile).

\item[\textsc{separator}]: used in the definition of a \textsc{menu}, gives a division between entries. %On a panel, probably has no effect.

\item[\textsc{sequent is} {[} \textsc{bag} {\textbar} \textsc{list} {\textbar} \textsc{formula} {]} |- {[} \textsc{bag} {\textbar} \textsc{list} {\textbar} \textsc{formula} {]}]: definition of sequent syntax. |- is declared as the entails symbol. See \secref{paraformlang:flexisyntax}.

\item[\textsc{string} \textit{name ... name}]: names defined to be in syntactic class \textsc{string}; see \secref{paraformlang:flexisyntax}.

\item[\textsc{structurerule} {[} \textsc{cut} {\textbar} \textsc{identity} {\textbar} \textsc{leftweaken} {\textbar} \textsc{rightweaken} {\textbar} \textsc{weaken} {]} \textsc{is} \textit{name}]: the rule called \textit{name} is defined to have a particular property. See \secref{paraformlang:structurerules}.

\item[\textsc{substfix} \textit{precedence} \{ \textit{bra fst sep snd ket} \}]: defines the syntactic precedence of substitution forms and, optionally, their appearance as well. See \secref{paraformlang:flexisyntax}.

\item[\textsc{tactic} \textit{name} \{ ( \textit{name1}, \dots, \textit{nameN} ) \} \{ \textsc{is} \} \textit{tactic}]: puts a tactic with name \textit{name} and parameters \textit{name1}, \dots, \textit{nameN} into the tactic store. If it appears inside a \textsc{menu} or \textsc{panel} definition then the effect is also of \textsc{entry} \textit{name}.%; in a \textsc{tacticpanel} it has the effect of \textsc{entry} \textit{name} \textsc{is} apply \textit{name}. 
See \secref{paraformlang:rulestacticsconjectures}.

\item[\textsc{tacticpanel} \textit{name} \{ \textsc{is} \} \textsc{[} \textit{entry} {\textbar} \textit{button} \textsc{]}* \textsc{end}]: very like \textsc{conjecturepanel}, except that there are no extra buttons and no default buttons and each entry labels a command, rule or tactic rather than a conjecture. %Tactics, rules and conjectures included in a \textsc{tacticpanel} description are associated with the command ``apply \textit{name}'' where \textit{name} is the name of the tactic, rule or conjecture.

\item[\textsc{theorem} \textit{conjecture}]: puts a conjecture into the tactic store. Jape's conjectures are always `theorem schemata', in the sense that they stand for any substitution-instance of the theorem's sequent. See \secref{paraformlang:rulestacticsconjectures}.

\item[\textsc{theorems} \textit{name} \{ \textit{params} \} \{ \textsc{where} \textit{provisos} \} \textsc{are} \textit{theorem1} \textsc{and} ... \textsc{and} \textit{theoremN} \textsc{end}]: define a collection of conjectures which are organised into an \textsc{alt} tactic.

Each \textit{theorem} is an unnamed conjecture (see \secref{paraformlang:rulestacticsconjectures}); each theorem is added to the tactic store prefixed by \textit{params} and \textit{provisos} in the same way as in the \textsc{rules} directive; at the same time a tactic \textsc{alt} \textit{theorem1 \dots theoremN} is added to the tactic store under \textit{name}. If included in a menu or panel description, an \textsc{entry} is created for each conjecture. The effect is to define a number of conjectures with evocative names, and to allow searching of the collection if desired. See also \textsc{theorem}.

\item[\textsc{theory} \textit{name} \{ \textsc{is} \} \textit{directive ... directive} \textsc{end}]: the directives may be \textsc{rule, rules, tactic, theorem, theorems} or \textsc{theory}; an \textsc{alt} tactic is made of the various directives and added to the tactic store under \textit{name}. If \textsc{theory} occurs in a menu or panel description, the effect is as if the directives occurred separately (that is, Jape does not add an entry corresponding to the overall \textsc{alt} tactic).

\item[\textsc{transitive}]: like \textsc{reflexive} (I'll put more here soon).

\item[\textsc{umenu}]: for the life of me I can't remember.
     
\item[\textit{formula}\textsc{unifieswith} \textit{formula}]: a proviso which requires that the two formulae should unify. Used to delay unification when difficult substitutions get in the way.


\item[\textit{collection} \textsc{unifieswith} \textit{collection}]: a proviso which helps when contexts are split. See \chapref{sequentvariations}.

\item[\textsc{use} ``\textit{filename}'']: same effect as C's \#include ``\textit{filename}''.

\item[\textsc{variable} \textit{name ... name}]: names defined to be of syntactic class \textsc{variable}; see \secref{paraformlang:flexisyntax}.

\item[\textsc{weaken}]: synonym for \textsc{leftweaken}.

\item[\textsc{where}]: prefixes a list of proviso declarations.

\item[\textsc{world}]: something to do with Kripke trees. When I remember anything about it, I'll come back and fill this in.

\end{description}
 
\section{Rules, tactics and conjectures}
\label{sec:paraformlang:rulestacticsconjectures}

The syntax of rules and conjectures (confusingly called \textsc{theorem}s --- a battle with Bernard that I lost) can take various forms. The syntax is:

\{ \textit{name} \} \{ ( \textit{param},..., \textit{param} ) \} \{ \textsc{where} \textit{proviso} \textsc{and \dots and} \textit{proviso} \} \{ \textsc{is} \} \textit{body}

Note that almost every part is optional, apart from the body of the rule or conjecture. Note also that, for obvious reasons, if parameters or provisos are included then either the \textsc{is} word must be included, or else \textit{body} must start with \textsc{from} or \textsc{ infer }.

In a conjecture, \textit{body} is

\{ \textsc{infer \}} \textit{consequent}

In a rule, \textit{body} is

\{ \textsc{from} \textit{antecedent} \textsc{and ... and} \textit{antecedent} \} \textsc{ infer } \textit{consequent}

where \textit{antecedent}s and \textit{consequent} are sequents. If a conjecture or rule is un-named, its name is taken to be \textit{consequent}.

Each \textit{param} is \textsc{[} \textsc{object} {\textbar} \textsc{abstraction} \textsc{]} \textit{name}. The name must have been declared in a \textsc{class} directive. 

Each proviso is

\quad \parbox{200pt}{
\textsc{concfresh} \textit{name},..., \textit{name} or\\
\textsc{hypfresh} \textit{name},..., \textit{name} or\\
\textsc{fresh} \textit{name},..., \textit{name} or\\
\textit{name} \textsc{notin} \textit{formula} or\\
\textit{formula} \textsc{unifieswith} \textit{formula}}

where the names used must be parameters of the rule or conjecture.

\subsection{The meaning of a \textsc{rule} directive}

Ignoring parameters for the moment, the rule

$\infer[\textit{(prov1,...,provN)\;rule}]
       {\textit{conse}}
       {\textit{ante1} & \dots & \textit{anteM}}$

with name \textit{rule}, antecedent sequents \textit{ante1} ... \textit{anteM}, consequent \textit{conse} and provisos \textit{prov1} ... \textit{provN}, is stated as the rule directive

\textsc{rule} \textit{rule} \textsc{where} \textit{prov1} \textsc{and ... and} \textit{provN} \textsc{is from} \textit{ante1} \textsc{and .... and} \textit{anteM} \textsc{ infer } \textit{conse}

A rule is schematic in all names appearing in the antecedents, consequents or provisos which are declared in a \textsc{class} directive. When the rule is applied to a problem sequent, a version of the rule is produced in which all the schematic names have been replaced by new unknowns, and then the consequent of that version is unified with the problem sequent.

If either of the \textit{autoAdditive} variables is set to $\<true>$ (see \appxref{GUIlang}) then rules can be defined as they often are in natural deduction presentation, without mentioning unmatched hypotheses and/or conclusions. For example, if \textit{autoAdditiveLeft} is $\<true>$, the rule

$\infer[\reason{$->|- $}]
       {\Gamma,A->B |- C}
       {\Gamma  |- A\quad \Gamma,B |- C}$

can be stated as

\textsc{rule} ``$->$|-'' \textsc{is from} \textit{A} \textsc{and} \textit{B} |- \textit{C} \textsc{ infer } \textit{A}$->$\textit{B} |- \textit{C}

\subsection{Parameters in \textsc{rule} directives}

Rule parameters are used for a number of reasons:

\begin{itemize}
\item On instantiation the first parameter is replaced by the user's text selection, rather than an unknown. This is useful when that parameter doesn't appear in the consequent or is the replacing formula in a substitution form in the consequent (see the discussions of substitution matching somewhere or other);

\item A parameter which is decorated with \textsc{object} is replaced with a freshly-minted name, rather than a new unknown;

\item A parameter which is decorated with \textsc{abstraction} is treated as a predicate, and juxtapositions involving that parameter are translated into substitution forms;

\item Parameters are used to drive the `proof reload' mechanism (no idea what this means).
\end{itemize}

\subsection{Instantiating a rule, including interpretation of predicate notation}

When a rule is instantiated, each of its schematic names is replaced by a freshly-minted unknown, whose name is based on the schematic name itself. This instantiation is modified in case the name is a parameter, if an \textj{autoAdditive} parameter is set to true, or if \textj{interpretpredicates} is true.\\
When an \textj{autoAdditive} parameter is true, a rule is automatically extended so that all the hypotheses (\textj{autoAdditiveLeft}) and/or the conclusions (\textj{autoAdditiveRight}) are extended with a freshly-minted segment variable, and all the antecedents likewise; then the augmented rule is instantiated normally.

When \textj{interpretpredicates} is true, juxtapositions in the rule are interpreted as predicate formulae and replaced by substitution forms; at the same time the parameter list is extended with \textsc{object} parameters as appropriate and the rule is augmented with invisible provisos. For example, a juxtaposition $P$(\textit{x},\textit{y}) will be replaced by $P\left[ u,v\backslash x,y\right] $ ; the parameter list will be extended with \textsc{object} \textit{u}, \textsc{object} \textit{v}, and an invisible proviso \textit{x,y} \textsc{notin} $P$ will be added to the rule; every other `predicate' application of $P$ in the rule then has to have exactly two `arguments' and the same variables \textit{u} and \textit{v} will be used in those cases as well. Jape avoids substitution forms wherever possible by noting the context: for example, it will translate $@*x.@*y.P\left( x,y\right) $ as $@*x.@*y.P$ and then would translate $P\left( E,F\right) $ as $P\left[ x,y\backslash E,F\right] $ and in such an example there is no need for extra \textsc{object} parameters. For example, it will translate $\infer{|*x.P\left( x\right) }
       {P\left( E\right) }$ into $\infer{|*x.P}
       {P\left[ x\backslash E\right] }$ .

The latter form of rule is well-suited to backwards reasoning. The effect is to allow a kind of predicate notation while preserving Jape's existing unification mechanisms.

\subsection{The meaning of provisos in \textsc{rule} and \textsc{theorem} directives}

Provisos are side conditions. At present we have a small number of built-in provisos, listed in \secref{basics:provisos}. All the forms of \textsc{fresh} provisos are automatically translated into a collection of \textsc{notin} provisos --- one for each unmatched hypothesis and/or conclusion as appropriate.

Each time a rule is applied, its provisos are added to the set which is displayed in the bottom pane of the proof window. At the end of each proof step, that set of provisos is checked, and if any proviso is violated, the proof step is cancelled (memo to implementers: change the proof engine so that this is more obviously the way that things happen ...). At the same time provisos which are satisfied are deleted from the set. The ones that are left are those whose status can't be decided, because of the presence of unknowns, substitution forms or names over which the conjecture being proved is quantified.

\subsection{The meaning of conjectures (stated in \textsc{theorem} directives)}

A conjecture is stated as a rule without antecedents. Normally the first thing you do with a conjecture is to try to prove it. If that proof is successful, you can store it in the proof store and it will appear in the conjecture panel as a proved theorem. The provisos of a proved theorem are those given in the statement of the conjecture, plus any which arise and aren't satisfied during the proof.

Jape will normally refuse to apply a conjecture until it is proved, but you can tell it not to be so cautious if you wish by setting \textj{applyconjectures} \texttt{none} (or \texttt{rules}, if you want to apply unproved derived rules).

If the consequent of a theorem matches a problem sequent, but in so doing it doesn't use up all the hypotheses and conclusion formulae of the problem, then Jape is cautious. If the logic you are using has a declared \textsc{leftweaken} rule and there are too many hypotheses, then you could have first eliminated the extra hypotheses by applications of that rule, and then the theorem would have exactly used up all the remaining ones; similarly if it has a declared \textsc{rightweaken} rule and there are too many conclusions. But unless all that applies, the theorem will be said to be inapplicable.

\subsection{Proof by resolution}

There is a facility to use a sort of resolution step when applying a theorem. If a theorem's conclusion(s) match but its hypotheses don't, and if there is a declared \textsc{cut} rule, then it would be possible to use a sequence of cuts to introduce the necessary extra hypotheses. In those circumstances Jape can introduce an antecedent for each of the hypotheses, and label the step with the name of the theorem. This feature is turned on and off by assigning to \textj{tryresolution} (see \appxref{GUIlang}). The effect is that if you have both right-weakening and cut, we treat a theorem $H_{1},...,H_{n}  |- C$ as equivalent to the rule $\infer{\Gamma  |- C}{\Gamma  |- H_{1} & ... & \Gamma  |- H_{n} } $ provided that $\Gamma,H_{1},...,H_{n}  |- C$ is a theorem; if you have cut but not right-weakening, we treat it as equivalent to $\infer{\Gamma  |- C} {\Gamma  |- H_{1} & \Gamma,H_{1}  |- H_{2} & ... & \Gamma,H_{1},...,H_{n-1}  |- H_{n} }$ with the same proviso.

\subsection{The meaning of \textsc{structurerule} directives}
\label{sec:paraformlang:structurerules}
It is necessary for the application of conjectures as rules, and for the proper operation of the box display mechanism, for Jape to be informed of the presence of certain kinds of structural rules in the logic. The rules we cater for are the various kinds of identity (hypothesis, axiom), cut and weakening rules.

\begin{description}
\item[\textsc{cut}]: declares a `cut' rule. Applications of the rule will normally be hidden in the box display mode of Jape. This directive is required before Jape will properly interpret \textj{tryresolution} (see \appxref{GUIlang}). Cut rules have to be one of the following forms: 
\begin{itemize}
\item $(B) \textsc{ from } \Gamma |- B \textsc{ and } \Gamma, B |- C \textsc{ infer } \Gamma |- C$; 
\item $(B) \textsc{ from } \Gamma |- B, \Delta \textsc{ and } \Gamma, B |- \Delta \textsc{ infer } \Gamma |- \Delta$;
\item $(B) \textsc{ from } \Gamma |- B, \Delta \textsc{ and } \Theta, B |- \Pi \textsc{ infer } \Gamma, \Theta |- \Delta, \Pi$.
\end{itemize}

\item[identity]: declares an `identity' rule. Instances of the application of this rule are normally hidden in box display mode. Allowable forms are:
\begin{itemize}
\item $\Gamma, B |- B$;
\item $\Gamma, B |- B, \Delta$
\item $\Gamma, B, \Delta |- B$.
\end{itemize}

\item[leftweaken]: declares a `left weakening' rule. Essential if Jape is to be able to apply theorems which don't have enough hypotheses to match the whole of the problem sequent. Valid forms are:
\begin{itemize}
\item $(B) \textsc{ from } \Gamma |- C \textsc{ infer } \Gamma, B |- C$;
\item $(B) \textsc{ from } \Gamma |- \Delta \textsc{ infer } \Gamma, B |- \Delta$.
\end{itemize}

\item[rightweaken]: similar to \textsc{leftweaken}, and plays a similar r\^{o}le in theorem application. The only allowable form of the rule is $(B) \textsc{ from } \Gamma |- \Delta \textsc{ infer } \Gamma |- B, \Delta$

\item[weaken]: see \textsc{leftweaken}.

\end{description}

\subsection{Substitution matching}

Substitution forms are used in Jape to describe the operation of rules. They aren't intended to be interpreted as themselves --- that is, they are not a special sort of formula with associated introduction and elimination rules. There are instead mechanisms inside the proof engine designed to eliminate substitution forms whenever they arise by carrying out the substitutions they describe, and the intention is that substitution forms should normally be read as naming the formula to which they simplify. 

For example, consider Hoare logic's variable-assignment rule $\infer{\{ R^{x}_{e} \} x:=e \{R\}}{}$. This can be expressed (see \textj{hoare\_rules.j}) in Japeish as \textj{RULE ``:='' IS INFER \{R«E/x»\} (x:=E) \{R\}}.

Now consider the problem sequent \textj{\{\_Q\} (x:=1) \{x=1\}}. If we apply the variable-assignment rule then a version will be generated expressed in terms of new unknowns, which will be \textj{\{\_R«\_E/\_x1»\} (\_x1:=\_E) \{\_R\}}. However the unification proceeds, it will eventually have unified \textj{(x=1)«1/x»} with \textj{\_Q}. Before that formula is displayed to the user it will be simplified to \textj{1=1}, and the rule will have done its job.

If the problem sequent had been \textj{\{1=1\} (x:=1) \{x=1\}}, then the unification process might first come across the problem of unifying \textj{\_R«\_E/\_x1»} with \textj{1=1}. Since that involves a substitution which won't simplify, it is deferred until later on. Unification of \textj{x:=1} with \textj{\_x1:=\_E} and of \textj{x=1} with \textj{\_R} mean that when the deferred problem must finally be considered, it has been transformed into that of unifying \textj{(x=1)«1/x»} with \textj{1=1}: the substitution form simplifies to \textj{1=1} and the unification is trivial.

Not every use of substitution forms in rules gives so little difficulty. When you define a rule with a substitution form in the consequent, and there aren't other occurrences of the components of the substitution form which will help to simplify it, matching becomes a problem. 

For example, consider the natural deduction ∀ elimination rule $\infer{\Gamma  |- P[x\backslash E]}{\Gamma  |- @*x.P}$, which can be expressed in Japeish as

\begin{japeish}
RULE ``$\forall$ elim''($E$, OBJECT x) IS FROM $\Gamma$ |- $\forall$ x.$P$ INFER $\Gamma$ |- $P$[x\textbackslash E]
\end{japeish}

If the problem sequent is \textj{a=b,b=c |- (a+b)+c=a+(b+c)}, then there are fourteen significantly different ways in which the consequent of the rule can match the problem:

\begin{enumerate}
\item $P$ : (\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{a}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : $E$
\item $P$ : (\textit{x}+\textit{b})+$c$\ensuremath{=}\textit{a}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : \textit{a}
\item $P$ : (\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{x}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : \textit{a}
\item $P$ : \label{match:a-all}(\textit{x}+\textit{b})+$c$\ensuremath{=}\textit{x}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : \textit{a}
\item $P$ : (\textit{a}+\textit{x})+$c$\ensuremath{=}\textit{a}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : \textit{b}
\item $P$ : (\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{a}+(\textit{x}+$c$); \textit{x} : \textit{x}; $E$ : \textit{b}
\item $P$ : \label{match:b-all}(\textit{a}+\textit{x})+$c$\ensuremath{=}\textit{a}+(\textit{x}+$c$); \textit{x} : \textit{x}; $E$ : \textit{b}
\item $P$ : (\textit{a}+\textit{b})+\textit{x}\ensuremath{=}\textit{a}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : $c$
\item $P$ : (\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{a}+(\textit{b}+\textit{x}); \textit{x} : \textit{x}; $E$ : $c$
\item $P$ : \label{match:c-all}(\textit{a}+\textit{b})+\textit{x}\ensuremath{=}\textit{a}+(\textit{b}+\textit{x}); \textit{x} : \textit{x}; $E$ : $c$
\item $P$ : \label{match:a+b}\textit{x}+$c$\ensuremath{=}\textit{a}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : \textit{a}+\textit{b}
\item $P$ : \label{match:(a+b)+c}\textit{x}\ensuremath{=}\textit{a}+(\textit{b}+$c$); \textit{x} : \textit{x}; $E$ : (\textit{a}+\textit{b})+$c$
\item $P$ : \label{match:b+c}(\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{a}+\textit{x}; \textit{x} : \textit{x}; $E$ : \textit{b}+$c$
\item $P$ : \label{match:a+(b+c)}(\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{x}; \textit{x} : \textit{x}; $E$ : \textit{a}+(\textit{b}+$c$)
\end{enumerate}

It's clearly necessary to say in just which way the formula should match. Jape has two mechanisms which help. The first mechanism, called `abstraction', finds matches in which every instance of a particular subformula is replaced by the substitution variable: for example, numbers \ref{match:a-all}, \ref{match:b-all}, \ref{match:c-all}, \ref{match:a+b}, \ref{match:(a+b)+c}, \ref{match:b+c} and \ref{match:a+(b+c)} in the list above. The abstraction mechanism is a kind of higher-order unification. To use this mechanism effectively you nominate the formula which should match $E$ by text-selecting it. It's unnecessary to nominate anything to match $x$, since it's an \textsc{object} parameter. You don't provide an argument for $P$, since it's $P$ that the unification in effect discovers. Given an $E$, Jape finds the corresponding match which replaces \emph{all} occurrences of $E$ in the consequent by $x$ to give $P$.

The abstraction mechanism doesn't work at all well if you don't subformula-select an $E$: an unknown in $E$'s position just makes it impossible to identify subformulae of the problem sequent which should be replaced by $x$.

Suppose, now, that you text-select \textit{a} and apply the rule. The generated consequent will be $\Gamma$ |-\_$P$[\textit{x{\textbackslash}a}], and the problem sequent $a=b,b=c |- (a+b)+c=a+(b+c)$ . Jape will try to unify \_$P$[\textit{x{\textbackslash}a}] with (\textit{a}+\textit{b})+$c$\ensuremath{=}\textit{a}+(\textit{b}+$c$) and, by default, will try to turn the problem formula into a substitution by finding every occurrence of \textit{a} (the replacement formula in the substitution form) in the problem formula and replacing each of them by \textit{x} (the replacement variable in the substitution form). It succeeds, producing the formula (\textit{x}+\textit{b})+$c$\ensuremath{=}\textit{x}+(\textit{b}+$c$), which it unifies with \_$P$. That is, of course, does \textit{not} generate a most general unifier of the original pair of formulae, but pragmatically it often finds the one which you want.

If Jape can't find every instance of the replacement formula in the problem formula --- for example, if there are unknowns in either or both of them, or if either or both of them contain names over which the theorem being proved is quantified --- then it will generate a `deferred unification' proviso. That's a proviso \textit{formula} \textsc{unifieswith} \textit{formula}. When those appear it is often because you have done something silly: either you are going through the proof in an unhelpful order, or there is some additional information which could help to clarify the situation and avoid the deferred unifications.

The second mechanism is user-defined substitution matching. The mechanism works together with the \textsc{withsubstsel} tactic (see \appxref{tacticlang} and \chapref{funcprog}). The user must text-select all the subformulas in the problem sequent which they want to be considered --- both the \textit{a}s, for example, or one of the \textit{bs}. Then the tactic \textsc{withsubstsel}(``\ensuremath{\forall} elim'') firsts constructs a `stable substitution form' based on those selections: if both the \textit{a}s it would build ((\_\textit{v}+\textit{b})+$c$\ensuremath{=}\_\textit{v}+(\textit{b}+$c$))[\_\textit{v}{\textbackslash}\textit{a}]; if the first \textit{b} it would build ((\textit{a}+\_\textit{v})+$c$\ensuremath{=}\textit{a}+(\textit{b}+$c$))[\_\textit{v}{\textbackslash}\textit{b}]. Then it applies the rule ``\ensuremath{\forall} elim'', which causes it to unify the new substitution form with \_$P$[\textit{x}{\textbackslash}\_$E$] from the rule: the unification process recognises the stable substitution form as something special, and pattern-matches the two, unifying \_$P$ with its body, \textit{x} with \textit{v} and \_$E$ with its replacement formula (\textit{a} in the first example, \textit{b} in the second). Jape hasn't constructed the most general unifier this time either, but it has justification, because it constructs the one which you asked for.

\subsection{The tactic store}

Theorems are a kind of rule; rules are a kind of tactic. Tactics are programs whose primitive proof steps are the application of rules and/or theorems to problem sequents. The tactic store therefore contains all three in a single soup, indexed by name.

\section{Forcing semantics for Kripke trees}

shouldn't there be something in here?

\section{Flexible syntax}
\label{sec:paraformlang:flexisyntax}

There are various ways in which you control what formulae can be written down and how they will be interpreted by Jape.

\subsection{Symbols}

The rules of a logic are written in terms of various symbols --- logical operators and connectives as well as identifiers like \textit{A}, \textit{B} or \textit{x}. Jape reserves a few special characters --- they are double-quote, underscore, opening or closing parenthesis (round bracket), space, newline or tab --- which can't be used in symbols.

Jape recognises four distinct kinds of symbol:

\begin{description}
\item[identifiers], which are rather like programming language identifiers or mathematical variable names: sequences of characters which start with an alphabetic character and optionally continue with any sequence of alphabetic and/or numeric characters and/or primes (\textsc{ascii} single quotes). Actually Jape's identifiers can start with any defined sequence of characters, given in a \textsc{class} directive, though some choices --- like using commas or arithmetic operator characters --- may be more confusing than useful.

\item[unknowns], which are are written as an underscore followed by an identifier.

\item[numbers], which are sequences of numeric characters.

\item[strings], which start with an \textsc{ascii} double-quote, continue with any sequence of characters not including newline or double-quote, and end with an \textsc{ascii} double-quote.

\item[special symbols], which are user-defined sequences of characters containing anything other than Jape's reserved characters. Everything else goes, though some choices --- like using primes or commas inside a special symbol --- may be more confusing than useful. Special symbols are defined in \textsc{infix, prefix, postfix, leftfix} and \textsc{outfix} directives.
\end{description}

Special symbols are always used as constants, and usually as operators or some kind of brackets, and they are defined implicitly by including them in various kinds of syntactic definitions. Identifiers can also be used as operators or brackets, by using them in just the same kind of syntactic definition.

Numbers, strings and special symbols are always constants of a logic --- they stand for themselves and not for anything else. Identifiers can be constants or they can stand for classes of things, like formulae, variables, or whatever\footnote{We haven't done the `whatever' bit, or not very much of it. But we know what we want to do, and we know how to do it ...}.

\subsection{Juxtaposition may need care}

Jape's syntax allows juxtaposition of formulae. You may have to use white space (blanks, spaces, newlines) to separate juxtaposed identifiers in some way --- \textit{xy}, without spacing, is usually a single identifier, whereas \textit{x y} is usually two juxtaposed identifiers and is equivalent to \textit{x}(\textit{y}), (\textit{x)y} or (\textit{x})(\textit{y}). Similarly, \textit{x}1 is usually a single identifier, whereas \textit{x} 1 is an identifier followed by a number. The syntactic priority of juxtaposition is user-defined.

Usually you can juxtapose special symbols without separation. If you define ¬ to be a special symbol, for example, and you don't also define ¬¬, then ¬¬\textit{x} is read as two ¬ symbols followed by an identifier.

\subsection{Identifier classes}

Typically, you start the definition of a logic by saying what the various identifiers you are going to use `stand for' or `range over'. You can say that an identifier ranges over formulae, variables, numbers, strings, or constants; you can say that any identifier which starts with a particular prefix ranges over one of those categories. The directives are

\begin{japeish}
<kind> name ... name \\
CLASS <kind> name ... name
\end{japeish}

where \texttt{<}kind\texttt{>} is \textsc{formula, variable}, \textsc{constant, string}, \textsc{number}, \textsc{bag} \texttt{<}kind\texttt{>} or \textsc{list} \texttt{<}kind\texttt{>} and \textit{names} is a comma-separated list of identifiers or identifier prefixes.

The unprefixed directives --- such as, for example, \textsc{constant} \textit{map}, \textit{fold}, \textit{filter} --- define particular identifiers to be of a particular class. They are `object language' names and when they appear in rules or theorems, they won't be instantiated with anything. But they will unify with unknowns of the same kind.

The prefixed directives --- such as, for example, \textsc{class variable} \textit{x}, \textit{y}, $z$ --- define identifier prefixes which are of a particular kind. Every identifier or unknown which starts with one of those prefixes is of the specified kind and they are all `general' or `schematic' or `meta-language' names: when they appear in rules they are always instantiated with an unknown or an argument of the same kind.

Unknowns follow the same rules as identifiers: given the same directives, \_\textit{map} would be an unknown that would only unify with constants, \_\textit{x33} would be one that unified only with variables.

There isn't, at present, any way of defining a name that is of a kind which is a mixture of primitive kinds (\textsc{variable} and \textsc{constant}, for example), but \textsc{formula} includes all the other kinds.

\subsection{Syntactic hierarchy}

Jape has a built-in notion of certain syntactic forms:

\begin{itemize}
\item identifiers --- like \textit{A, ABC, A1, x, y, y37f, ...};
\item strings --- ``\textit{anything at all}''; 
\item numbers --- 1, 2, 46;
\item fully-bracketed formulae --- (\textit{formula});
\item substitutions --- by default \textit{formula} [ \textit{variable list} {\textbackslash} \textit{formula list} ], but the order of \textit{variable list} and \textit{formula list} can be reversed if you wish, and you can choose different symbols in place of `[', `{\textbackslash}' and `]';
\item juxtaposition (like function application in functional languages) --- \textit{formula formula};
\item prefix operators --- \textit{op formula};
\item postfix operators --- \textit{formula op};
\item infix operators --- \textit{formula op formula};
\item \textsc{leftfix} bracketing --- $\textit{bra}\; f_{1} \;\textit{sep}_{1} \;f_{2} \;\textit{sep}_{2} ... \textit{sep}_{n-1} \;f_{n}$;
\item \textsc{outfix} bracketing --- $\textit{bra}\; f_{1} \;\textit{sep}_{1} \;f_{2} \;\textit{sep}_{2} ... \textit{sep}_{n-1} \;f_{n} \; ket$;
\item \textsc{rightfix} bracketing --- $f_{1} \;\textit{sep}_{1} \;f_{2} \;\textit{sep}_{2} ... \textit{sep}_{n-1} \;f_{n} \; ket$.
\end{itemize}

In addition, comma (`,') is always a zero-precedence tupling operator, so that tuples --- \textit{formula}, \textit{formula},..., \textit{formula} --- are automatically available, with or without brackets.

Both substitution and juxtaposition associate to the left\footnote{Substitution \textit{has} to associate to the left, but we can imagine right-associative juxtaposition. Another enhancement for the fugure (sigh).}; you define the associativity of infix operators as well as their precedence. Prefix operators, postfix operators, substitution forms, juxtaposition and \textsc{leftfix} bracketed forms all have user-defined precedence.

There are well-known pitfalls in the definition of flexible precedence grammars (but probably no deeper than the holes beneath other forms of grammar). If your definition falls into a hole, Jape may not give much assistance, nor even provide readable parsing diagnostics.

\subsection{Bracketed formulae}

Jape recognises bracketed formulae which use round brackets (parentheses). You can define other kinds of brackets for yourself in \textsc{leftfix} and \textsc{outfix} directives.

\begin{description}
\item[\textsc{outfix}]  directives allow you to define new kinds of opening and closing brackets together with internal punctuation as well. You list the opening bracket, the internal separators and the closing bracket. For example you might write

\begin{japeish}
\textsc{outfix} if then else fi
\end{japeish}

and then Jape will recognise

\begin{japeish}
if \textit{formula} then \textit{formula} else \textit{formula} fi
\end{japeish}

At present the parser allows you to bring in the closing bracket early, before the list of internal punctuation symbols is exhausted, so that given the \textsc{outfix} directive above any of the following will be recognised as a formula:

\begin{japeish}
if fi\\
if \textit{formula} fi\\
if \textit{formula} then \textit{formula} fi\\
if \textit{formula} then \textit{formula} else \textit{formula} fi
\end{japeish}

This is a temporary hack, pending a more flexible parser-generator.

\item[\textsc{leftfix}] directives allow you to define opening brackets which have no corresponding closing bracket: you list the syntactic precedence, the opening bracket and the separating symbols. For example you might write

\begin{japeish}
\textsc{leftfix 100} letrec be in
\end{japeish}

and then Jape will recognise formulae of the form

\begin{japeish}
letrec \textit{formula} be \textit{formula} in \textit{formula}
\end{japeish}

\textsc{leftfix} formulae are notoriously ambiguous --- experts will recognise this as the `dangling else' problem. In effect the final separator has the priority given in the declaration, and Jape will not allow the opening bracket to be preceded by an operator which is of higher priority than that given in the declaration. For example, if you have

\begin{japeish}
\textsc{infix 120} \textsc{∧}\\
\textsc{leftfix 100} ∀.
\end{japeish}

then you could write \ensuremath{\forall}\textit{x}.\textit{A}\textsc{∧}\textit{B}, but not \textit{C}\textsc{∧}\ensuremath{\forall}\textit{x}.\textit{A}\textsc{∧}\textit{B}. That restriction, we hope, eliminates visual ambiguity in the use of bracketed forms without a closing bracket. If you want to write a formula which breaks these rules, you can always use brackets, as for example in \textit{C}\textsc{∧}(\ensuremath{\forall}\textit{x}.\textit{A}\textsc{∧}\textit{B}).

\item [\textsc{rightfix}] is very like \textsc{leftfix}. I have no memory of how it works: see examples to see if it's ever used.
\end{description}

\subsection{Substitution and juxtaposition forms}

You can define the relative priority of substitution and juxtaposition as well as that of operators. Normally substitution is the highest priority form, and juxtaposition is either the next or follows some prefix/postfix operators, but the choice is yours. You write

\begin{japeish}
\textsc{juxtfix} \textit{precedence}\\
\textsc{substfix} \textit{precedence}\\
\textsc{substfix} \textit{precedence bra id1 sep id2 ket}
\end{japeish}


The second form of \textsc{substfix} allows you to define the syntax of a substitution form, choosing opening bracket (by default `['), separator (by default `/') and closing bracket (by default `]'). At the same time you choose whether the variable list or the formula list comes first, by putting a variable identifier and a formula identifier in place of \textit{id1} and \textit{id2}. Because Jape uses this directive as a definition of some of the symbols, there must always be white space between its various components.

\subsection{Operator syntax}

You define connectives and other such symbols in your logic by defining (unary) \textsc{prefix}, (unary) \textsc{postfix} operators and (binary) \textsc{infix} operators together with their syntactic precedence; in addition infix operators need an associativity. You write

\begin{japeish}
\textsc{prefix} \textit{precedence op op ...}\\
\textsc{postfix} \textit{precedence op op ...}\\
\textsc{infix} \textit{precedence} \texttt{<}associativity\texttt{>} \textit{op op ...}\\
\textsc{infixc} \textit{precedence} \texttt{<}associativity\texttt{>} \textit{op op ...}
\end{japeish}


The \textit{op}s are special symbols, but they may be made up of any characters that you wish --- they don't have to be made up of non-alphanumeric characters. \texttt{<}Associativity\texttt{>} is a single character: L means left-associative, so that \textit{A op B op C} means (\textit{A op B}) \textit{op C}; R means right-associative, so that \textit{A op B op C} means \textit{A op} (\textit{B op C}); T means tupling or non-associative, so that \textit{A op B op C} means \textit{A op B op C}. Mixing operators of the same precedence and different associativity may cause confusion, but Jape doesn't prohibit it. The difference between \textsc{infix} and \textsc{infixc} is to do with the way that formulae are parsed.

As in many modern programming languages, we permit a bracketed operator as a formula, so you can write formulae like (+), (\ensuremath{@}), (++) once those symbols have been defined as operators. Operation formulae are parsed as juxtapositions, so that \textit{prefixop formula} is parsed as the juxtaposition (\textit{prefixop) formula}, \textit{formula postfixop} is parsed as (\textit{postfixop}) \textit{formula}, \textit{f1 infixop f2} (\textsc{infix} \textit{infixop}) is parsed as (\textit{infixop}) (\textit{f1,f2}) and \textit{f1 infixCop f2} (\textsc{infixc} \textit{infixCop})is parsed as (\textit{infixCop}) \textit{f1 f2}; the reverse transcription is made when the formulae are printed out.

\subsection{Binding structure}

Binding structure is defined by pattern: you give some variable names and some formula names and then give a pattern using those names. Any formula or subformula which matches the pattern is automatically a binding formula. Because substitution or unification mustn't be allowed to change the structure of a formula, Jape checks for `near miss' patterns and complains if it finds them.

The sort of thing you write is

\begin{japeish}
BIND x SCOPE P IN ∃x. P\\
BIND y SCOPE P IN \{ y {\textbar} P \}\\
BIND x, y SCOPE P IN ∀x,y. P
\end{japeish}


It's normal to use \textsc{leftfix} or \textsc{outfix} patterns, as in these examples, but it isn't obligatory.

The last of the three examples above defines a parallel binding: one that at the same time binds two variable names. At present Jape has no means of defining families of parallel binding formula structures except by exhaustively listing each alternative. And it has no way of defining serial bindings at all.

\subsection{Sequent structure}

At present sequents are always double-sided, and each side is one of

\begin{itemize}
\item an optionally-empty comma-separated bag/multiset of formulae --- say \textsc{bag} or \textsc{bag formula};
\item an optionally-empty comma-separated list/sequence of formulae --- say \textsc{list} or \textsc{list formula};
\item a single formula --- say \textsc{formula}
\end{itemize}

The \textsc{sequent} directive gives you the opportunity to say what can appear on either side, and what the entailment symbol is. You write

\begin{japeish}
SEQUENT \textit{lhs entailment rhs} \{ AND \textit{lhs entailment rhs ...} \}
\end{japeish}


You can have as many different kinds of sequent as you wish, provided that their entailment symbols are unique.

\subsection{Future work}

If I knew how to do more, I would. Over to you?

