STELF's grammar

The grammar of STELF was designed with a couple goals in mind:

• To be parsable with a finite amount of lookahead (usually only 1 token)

• Produce at most one output

• Substituting one identifier for another will either change only the output at that identifier, or cause the parser to fail (all identifiers are syntactically equivalent), where an identifier is a sequence of non-whitespace charecters excluding ()[]{}%

Apart from this, there are a couple of other design choices that were made, including making STELF literate by default (per as a matter of fact STELF starts in markup mode)

Caution

The STELF grammar is not the exact same as the STELF grammar, and in many places completly different

The Core Lexical Syntax

The core lexical syntax of STELF involves a couple different lexical classes.

1. Whitespace: any sequence of charecters that have the property White_Space=yes TODO
2. Commands any sequence of non-whitespace charecters that begins with % and does not contain ()[]{}%
3. Identifiers: any sequence of non-whitespace charecters that does not begin with % and does not contain ()[]{}%, this uses the longest match rule.
4. Special characters: ()[]{}%
5. Outer: any sequence of charecters up to %
6. String literals, %[, with variants %[[, %[[[, etc, that are terminated by %] with the same number of ]s as [s. String literals can contain any charecters, including newlines and special characters, except %

Expressions

expr1 ::=

<identifier>

( <expr> )

expr_trail ::=

[ <decl> ] <expr>

{ <decl> } <expr>

{{

<name> ...

}} <expr>

Full grammar

The complete grammar, as expressed by the tree-sitter parser:

source_file ::=

<command> <outer_text>

...

outer_text ::= ([^%]|\%\%\%)+

comment ::=

%[ \t][^\n]*

ident ::= [^ \t\n(){}\[\]%]+

nat ::= [0-9]+

atom ::=

<ident> <qualified>

qualified ::=

%val

<ident>

( <ident> + )

%( <ident> + )

_expr1 ::=

<atom>

( <expr> )

lam ::=

[ <decl> ] <expr>

pi ::=

{ <decl> } <expr>

impl ::=

{{ <ident> + }} <expr>

_expr_trail ::=

<lam> <pi> <impl>

app ::=

<_expr1>

<_expr1> ...

<_expr_trail> ε

ascription ::=

%the <_expr1> <expr>

arrow_chain ::=

%-> <_expr1>

%-> <_expr1>

...

backarrow_chain ::=

%<- <_expr1>

%<- <_expr1>

...

expr ::=

<ascription> <arrow_chain> <backarrow_chain> <app>

decl ::=

<arg>

( <arg> )

<expr> ε

arg ::=

_ <ident>

pdecl ::=

( <decl> )

sdecl ::=

[ <decl> ]

bdecl ::=

{ <decl> }

mode ::=

%in%out%out1%star

mode_dec ::=

{ <mode> <decl> }

...

<expr>

<mode> ...

id_list ::=

<ident>

( <ident> + )

order ::=

<id_list>

[ <order> + ]

{ <order> + }

order_list ::=

<order>

( <order> + )

_expr1_list ::= <_expr1> +

_decl ::= <decl>

_term_trailing ::= <_expr_trail>

_term_small ::= <_expr1>

_expr_trailing ::= <_expr_trail>

_any ::= .+?

_value ::=

<_expr1>

<begin_string> <_any> <end_string>

command ::=

<stop> <sort_cmd> <term_cmd> <mode_cmd> <worlds_cmd> <total_cmd> <terminates_cmd> <reduces_cmd> <query_cmd> <qtab_cmd> <adhoc_query> <define_cmd> <decl_cmd> <inline_cmd> <unique_cmd> <prec_cmd> <block_cmd> <union_cmd> <repl_cmd> <name_cmd> <symbol_cmd> <freeze_cmd> <thaw_cmd> <deterministic_cmd> <use_cmd> <open_cmd> <eval_cmd> <covers_cmd>

stop ::= %.

sort_cmd ::=

%sort

<ident>

( <ident> + )

<bdecl> ...

term_cmd ::=

%term <_decl>

mode_cmd ::=

%mode <mode_dec>

worlds_cmd ::=

%worlds(

<ident> ...

) <expr>

total_cmd ::=

%total <order_list>

<_expr1> ...

terminates_cmd ::=

%terminates <order_list>

<_expr1> ...

reduces_cmd ::=

%reduces

<=

>=

<>=

<_expr1> +

query_cmd ::=

%query

_ <nat>

_ <nat>

_ <nat>

<expr>

qtab_cmd ::=

%querytabled

_ <nat>

_ <nat>

_ <nat>

<expr>

adhoc_query ::=

%? <expr>

define_cmd ::=

%define%def

<ident> _

<_expr1> <expr>

decl_cmd ::=

%decl <expr>

inline_cmd ::=

%inline <ident> <expr>

unique_cmd ::=

%unique <expr>

prec_cmd ::=

%prec

%left%right%prefix%postfix%middle%none

<nat> <id_list>

block_cmd ::=

%block <ident>

<bdecl> <sdecl>

...

union_cmd ::=

%union <ident> ( <ident> + )

repl_cmd ::=

%quit

%help

<ident> ε

%get <ident>

%set <ident> <ident>

%version

name_cmd ::=

%name <ident>

symbol_cmd ::=

%symbol <ident> <ident>

freeze_cmd ::=

%freeze <id_list>

thaw_cmd ::=

%thaw <id_list>

deterministic_cmd ::=

%deterministic <id_list>

use_cmd ::=

%use <ident> <ident> (

<ident> ...

)

open_cmd ::=

%open <ident> <id_list>

eval_cmd ::=

%eval%{

<command> ...

%}

covers_cmd ::=

%covers <mode_dec>