LOOP parser

This file defines a simple parser for the LOOP language, written using the standard Parsec library. The accepted syntax for a loop program is defined as follows: $$ \begin{array}{lclcl} \texttt{Ident} & \ni & x, y & & \\ \texttt{Com} & \ni & P, Q & ::= & \texttt{SKIP} \mid x \; \texttt{=} \; \texttt{0} \mid x \; \texttt{=} \; y \mid x \; \texttt{=} \; x \; \texttt{+} \; \texttt{1} \\ & & & & \mid P \texttt{;} Q \mid \texttt{LOOP} \; x \; \texttt{DO} \; P \; \texttt{END} \end{array} $$

Some example programs can be found in the Examples folder.

References

This work is strongly based on the following resources:

• https://jakewheat.github.io/intro_to_parsing
• https://wiki.haskell.org/Parsing_a_simple_imperative_language
• https://leanprover-community.github.io/mathlib4_docs/Lean/Data/Json/Parser.html

def var : Lean.Parsec String

Parses a variable.

Equations

• var = do let fc ← var.firstChar let rest ← var.nonFirstChar.many pure { data := fc :: rest.toList }

def var.firstChar : Lean.Parsec Char

Equations

• var.firstChar = Lean.Parsec.satisfy Char.isAlpha

def var.nonFirstChar : Lean.Parsec Char

Equations

• var.nonFirstChar = Lean.Parsec.satisfy fun (c : Char) => c.isAlpha || c.isDigit || c == '_'

def lexeme {α : Type} (p : Lean.Parsec α) : Lean.Parsec α

Parses a syntactic construct followed by a sequence of blank or tab characters.

Equations

• lexeme p = do let x ← p let __discr ← (Lean.Parsec.satisfy fun (c : Char) => c == ' ' || c == '\t').many let x_1 : Array Char := __discr pure x

def newline : Lean.Parsec Unit

Parses a newline character.

Equations

• newline = do HOrElse.hOrElse (Lean.Parsec.skipChar '\n') fun (x : Unit) => Lean.Parsec.skipString "\x0d\n" Lean.Parsec.ws

def parse : Lean.Parsec LOOP.Com

Parses a program file.

Equations

• parse = do Lean.Parsec.ws let prog ← pCom Lean.Parsec.ws Lean.Parsec.eof pure prog

partial def pCom : Lean.Parsec LOOP.Com

Parses one or more commands.

partial def pSingle : Lean.Parsec LOOP.Com

Parses a single command.

def pSKIP : Lean.Parsec LOOP.Com

Parses a SKIP command with 'SKIP' syntax.

Equations

• pSKIP = do lexeme (Lean.Parsec.skipString "SKIP") pure LOOP.Com.SKIP

def pZER : Lean.Parsec LOOP.Com

Parses a zeroing command with 'x = 0' syntax.

Equations

• pZER = do let i ← lexeme var lexeme (Lean.Parsec.skipChar '=') lexeme (Lean.Parsec.skipChar '0') pure (LOOP.Com.ZER i)

def pASN : Lean.Parsec LOOP.Com

Parses an assignment command with 'x = y' syntax.

Equations

• pASN = do let i1 ← lexeme var lexeme (Lean.Parsec.skipChar '=') let i2 ← lexeme var pure (LOOP.Com.ASN i1 i2)

def pINC : Lean.Parsec LOOP.Com

Parses an increment command with 'x += 1' syntax.

Equations

• pINC = do let i ← lexeme var lexeme (Lean.Parsec.skipString "+=") lexeme (Lean.Parsec.skipChar '1') pure (LOOP.Com.INC i)

partial def pSEQ : Lean.Parsec LOOP.Com

Parses a sequential command

partial def pLOOP : Lean.Parsec LOOP.Com

Parses a LOOP command with 'LOOP x DO P END' syntax.