summaryrefslogtreecommitdiff
path: root/tools/Scanner/Parser.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tools/Scanner/Parser.lean')
-rw-r--r--tools/Scanner/Parser.lean54
1 files changed, 27 insertions, 27 deletions
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean
index 5d4e837..efe09bd 100644
--- a/tools/Scanner/Parser.lean
+++ b/tools/Scanner/Parser.lean
@@ -10,24 +10,24 @@ This converts a protocol description XML into a `Raw.ProtocolDesc`.
private def String.toNat (s : String) : Except String Nat :=
match Lean.Syntax.decodeNatLitVal? s with
- | .some n => .ok n
- | .none => .error s!"Expected a natural number, but got {s}"
+ | .some n => .ok n
+ | .none => .error s!"Expected a natural number, but got {s}"
private def String.toBool : String → Except String Bool
-| "true" => .ok true
-| "false" => .ok false
-| s => .error s!"Expected a boolean value, but got {s}"
+ | "true" => .ok true
+ | "false" => .ok false
+ | s => .error s!"Expected a boolean value, but got {s}"
namespace Lean.Xml
private def Element.name : Xml.Element → String
-| .Element name _ _ => name
+ | .Element name _ _ => name
private def Element.attributes : Xml.Element → Xml.Attributes
-| .Element _ attrs _ => attrs
+ | .Element _ attrs _ => attrs
private def Element.content : Xml.Element → Array Xml.Content
-| .Element _ _ content => content
+ | .Element _ _ content => content
private def Element.ensureName (el : Xml.Element) (name : String) : Except String Unit :=
if name == el.name
@@ -45,20 +45,20 @@ private def Element.textContent (el : Xml.Element) : String :=
|>.trimAscii
|>.toString
reformat <| String.join <| Array.toList <| el.content.flatMap fun
- | .Element _ => #[]
- | .Comment _ => #[]
- | .Character s => #[s]
+ | .Element _ => #[]
+ | .Comment _ => #[]
+ | .Character s => #[s]
private def Element.getChildrenByName (el : Xml.Element) (name : String) : Array Xml.Element :=
el.content.flatMap fun
- | .Element child => if child.name == name then #[child] else #[]
- | .Comment _ => #[]
- | .Character _ => #[]
+ | .Element child => if child.name == name then #[child] else #[]
+ | .Comment _ => #[]
+ | .Character _ => #[]
private def Element.getChildByName (el : Xml.Element) (name : String) : Option Xml.Element :=
match el.getChildrenByName name with
- | #[single] => .some single
- | _ => .none
+ | #[single] => .some single
+ | _ => .none
private def Element.getAttribute (el : Xml.Element) (attr : String) : Option String :=
el.attributes.get? attr
@@ -77,19 +77,19 @@ namespace WaylandScanner
open Raw
private def MessageType.ofString : String → Except String MessageType
-| "destructor" => .ok .destructor
-| s => .error s!"Expected \"destructor\", but got {s}"
+ | "destructor" => .ok .destructor
+ | s => .error s!"Expected \"destructor\", but got {s}"
private def ArgumentType.ofString : String → Except String ArgumentType
-| "int" => .ok .int
-| "uint" => .ok .uint
-| "fixed" => .ok .fixed
-| "string" => .ok .string
-| "array" => .ok .array
-| "fd" => .ok .fd
-| "new_id" => .ok .newID
-| "object" => .ok .object
-| s => .error s!"Expected an argument type, but got {s}"
+ | "int" => .ok .int
+ | "uint" => .ok .uint
+ | "fixed" => .ok .fixed
+ | "string" => .ok .string
+ | "array" => .ok .array
+ | "fd" => .ok .fd
+ | "new_id" => .ok .newID
+ | "object" => .ok .object
+ | s => .error s!"Expected an argument type, but got {s}"
private def processDescription (el : Xml.Element) : Except String Description := do
el.ensureName "description"