Parser for STRIPS Planning Tasks

This file contains some general parsing functions and a parser for STRIPS planning tasks.

General Parsing Functionality

@[reducible, inline]

abbrev Validator.Parser (α : Type) : Type

In Certificate.Parser we need to parse certificates in a separate location, hence we use a monadic transformer for combinatorial parsers on the IO monad.

Equations

• Validator.Parser = ParserT Validator.Error String.Slice Char IO

def Validator.parseEol : Parser Unit

Equations

• Validator.parseEol = Validator.parseSpaces✝ <* Parser.optional (Parser.Char.char ';') <* Parser.Char.eol

def Validator.checkString (s : String) : Parser Unit

Equations

• Validator.checkString s = Parser.Char.chars s *> Validator.parseSpaces✝

def Validator.checkLine (s : String) : Parser Unit

Equations

• Validator.checkLine s = Parser.Char.chars s *> Validator.parseEol

def Validator.readLine {α : Type} (s : String) (p : Parser α) : Parser α

Equations

• Validator.readLine s p = Validator.checkString s *> p <* Validator.parseEol

def Validator.dropLine : Parser Unit

Equations

• Validator.dropLine = Parser.dropUntil Parser.Char.eol Parser.anyToken *> pure ()

def Validator.parseWord : Parser String

Equations

• One or more equations did not get rendered due to their size.

def Validator.parseNat : Parser ℕ

Equations

• Validator.parseNat = Parser.Char.ASCII.parseNat <* Validator.parseSpaces✝

def Validator.parseListNat : Parser (List ℕ)

Equations

• Validator.parseListNat = do let n ← Validator.parseNat let __discr ← Parser.take n Validator.parseNat match __discr with | { toList := l } => pure l

def Validator.parseCases {α : Type} (ps1 : List (String × Parser α)) (ps2 : List (Parser Unit × Parser α) := []) : Parser α

For each of the pairs (s, p) in ps1, try to parse the string s. If it succeeds, run the parser p, otherwise proceed with the next pair in the list. If none of parsers for s is successfull, continue with the list ps2. For each pair (p, p') in this list, try the parser p, and if it succeed, run p' and return its result. If it fails continue with the next pair. If all pairs fail, combine the strings in ps1 into one error message.

Equations

• One or more equations did not get rendered due to their size.

STRIPS Parser

def Validator.STRIPS.parse (path : System.FilePath) : IO ((n : ℕ) × STRIPS n)

Equations

• One or more equations did not get rendered due to their size.