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

Equations

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

def Validator.parseSpaces : Parser Unit

Equations

• Validator.parseSpaces = Parser.dropMany (Parser.Char.char ' ')

def Validator.parseSpaces1 : Parser Unit

Equations

• Validator.parseSpaces1 = Parser.dropMany1 (Parser.Char.char ' ')

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.parseLine : Parser String

Equations

• Validator.parseLine = do let __discr ← Parser.takeUntil Parser.Char.eol Parser.anyToken match __discr with | ({ toList := l }, snd) => pure (String.ofList l)

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

@[reducible, inline]

abbrev Validator.push? {α : Type u_1} : Array α → Option α → Array α

Equations

• Validator.push? x✝ none = x✝
• Validator.push? x✝ (some x_2) = x✝.push x_2

def Validator.parseCases' {α : Type} (ps : List (Parser Unit × Parser α × Option String)) : Parser α

For each tuple (p, p', e) in the given list, try the parser p. If it succeeds, run the parser p', otherwise proceed with the next tuple in the list. The optional error messages e are combined into one error message if none of the parsers p succeed.

Equations

• Validator.parseCases' ps = Validator.parseCases'.go ps #[]

def Validator.parseCases'.go {α : Type} : List (Parser Unit × Parser α × Option String) → Array String → String.Slice → Id (Parser.Result Error String.Slice α)

Equations

• One or more equations did not get rendered due to their size.
• Validator.parseCases'.go [] { toList := e } x✝ = Parser.throwUnexpectedWithMessage none (toString "expected one of the following : " ++ toString e) x✝

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)

Try to read the file corresponding to the given path, and parse its content into a STRIPS planning task. The file is expected to have the following format:

begin_atoms: <#atoms>
<atom 0>
<atom 1>
... (names of all atoms, one on each line)
end_atoms
begin_init
<initital state atom index 0>
<initital state atom index 1>
... (indexes of atoms that are true in initial state, one on each line)
end_init
begin_goal
<goal atom index 0>
<goal atom index 1>
... (indexes of atoms that are true in goal, one on each line)
end_goal
begin_actions: <#actions>
begin_action
<action_name>
cost: <action_cost>
PRE: <precondition atom index 0>
ADD: <added atom index 0>
DEL: <deleted atom index 0>
... (more PRE, ADD and DEL in any order, one on each line)
end_action
... (more actions)
end_actions

Equations

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