diff options
| -rw-r--r-- | tools/Scanner/Parser.lean | 6 | ||||
| -rw-r--r-- | tools/Scanner/Processor.lean | 44 | ||||
| -rw-r--r-- | tools/Scanner/Protocol.lean | 50 |
3 files changed, 67 insertions, 33 deletions
diff --git a/tools/Scanner/Parser.lean b/tools/Scanner/Parser.lean index 630b3fc..f89c239 100644 --- a/tools/Scanner/Parser.lean +++ b/tools/Scanner/Parser.lean @@ -2,6 +2,12 @@ import Scanner.Protocol import Lean.Data.Xml.Basic import Lean.Data.Xml.Parser +/-! +# Parsing of Protocol Description + +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 diff --git a/tools/Scanner/Processor.lean b/tools/Scanner/Processor.lean index 88853a6..d591ee7 100644 --- a/tools/Scanner/Processor.lean +++ b/tools/Scanner/Processor.lean @@ -1,5 +1,14 @@ import Scanner.Protocol import Std.Data.TreeMap +import Std.Data.TreeSet + +/-! +# Processing of Protocol Descriptions + +This is mainly used to resolve interface/enum references within protocols, converting a `Raw.ProtocolDesc` into a +`Client.ProtocolDesc`. Note that this requires a global view of all protocols since interfaces can mention interfaces +from other protocols. Thus, this needs to be done after parsing all protocols. +-/ namespace WaylandScanner @@ -12,7 +21,7 @@ private abbrev InterfaceMap := Std.TreeMap String InterfaceInfo private structure Context where interfaces : InterfaceMap currentInterface : Client.InterfaceRef - referencedInterfaces : Array Client.InterfaceRef + referencedInterfaces : Std.TreeSet Client.InterfaceRef private abbrev Processor : Type → Type := StateT Context (Except String) @@ -37,7 +46,7 @@ private def resolveInterface (name : String) : Processor Client.InterfaceRef := typeName := name } let old ← get - set { old with referencedInterfaces := old.referencedInterfaces ++ #[ref] } + set { old with referencedInterfaces := old.referencedInterfaces.insert ref } return ref private def resolveEnum (name : String) : Processor Client.EnumRef := do @@ -114,7 +123,7 @@ private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.Interf let requests ← raw.requests.mapM processRequest let events ← raw.events.mapM processEvent let state ← get - let referencedInterfaces := state.referencedInterfaces ++ #[state.currentInterface] + let referencedInterfaces := state.referencedInterfaces.insert state.currentInterface return { name := raw.name version := raw.version @@ -123,9 +132,6 @@ private def processInterface (raw : Raw.InterfaceDesc) : Processor Client.Interf requests := requests events := events referencedInterfaces := referencedInterfaces - |>.toList - |>.eraseDups - |>.toArray } private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) : Except String Client.ProtocolDesc := do @@ -137,14 +143,34 @@ private def processProtocol (interfaces : InterfaceMap) (raw : Raw.ProtocolDesc) fun iface ↦ (processInterface iface).run' { interfaces := interfaces currentInterface := { moduleName := raw.name, typeName := iface.name } - referencedInterfaces := #[] + referencedInterfaces := .empty } } -def processProtocols (raw : Array Raw.ProtocolDesc) : Except String (Array Client.ProtocolDesc) := +/-! Compute the transitive closure w.r.t. `referencedInterfaces`. -/ +private partial def transitiveClosure (protocols : Array Client.ProtocolDesc) : Array Client.ProtocolDesc := + let successors : Std.TreeMap Client.InterfaceRef (List Client.InterfaceRef) := .ofArray <| protocols.flatMap + fun protocol ↦ protocol.interfaces.map + fun iface ↦ ((⟨protocol.name, iface.name⟩ : Client.InterfaceRef), iface.referencedInterfaces.toList) + let rec dfs : Std.TreeSet Client.InterfaceRef → List Client.InterfaceRef → Std.TreeSet Client.InterfaceRef + | visited, [] => visited + | visited, (x::xs) => + if visited.contains x + then dfs visited xs + else dfs (visited.insert x) (successors.get! x ++ xs) + let interfaceClosure (iface : Client.InterfaceDesc) : Client.InterfaceDesc := + { iface with referencedInterfaces := dfs .empty iface.referencedInterfaces.toList } + let protocolClosure (protocol : Client.ProtocolDesc) : Client.ProtocolDesc := + { protocol with interfaces := protocol.interfaces.map interfaceClosure } + protocols.map protocolClosure + +-- TODO: Correctness proof for `transitiveClosure` + +def processProtocols (raw : Array Raw.ProtocolDesc) : Except String (Array Client.ProtocolDesc) := do let interfaces : InterfaceMap := .ofArray <| raw.flatMap fun protocol ↦ protocol.interfaces.map fun iface ↦ (iface.name, (⟨protocol.name, iface.enums.map Raw.EnumDesc.name⟩ : InterfaceInfo)) - raw.mapM (processProtocol interfaces) + let res ← raw.mapM (processProtocol interfaces) + return transitiveClosure res end WaylandScanner diff --git a/tools/Scanner/Protocol.lean b/tools/Scanner/Protocol.lean index c90ab56..77908d9 100644 --- a/tools/Scanner/Protocol.lean +++ b/tools/Scanner/Protocol.lean @@ -1,9 +1,11 @@ +import Std.Data.TreeSet + namespace WaylandScanner structure Description where summary : Option String body : Option String - deriving Repr, BEq + deriving Repr, BEq, Inhabited def Description.ofSummary (s : String) : Description := { summary := s @@ -11,7 +13,7 @@ def Description.ofSummary (s : String) : Description := /-! Identifiers, stored in their original representation (i.e., camel case). -/ def Identifier := String - deriving Repr, BEq + deriving Repr, BEq, Ord, Inhabited namespace Raw @@ -21,7 +23,7 @@ structure EnumEntryDesc where description : Option Description since : Nat deprecatedSince : Option Nat - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure EnumDesc where name : String @@ -29,7 +31,7 @@ structure EnumDesc where since : Nat bitfield : Bool entries: Array EnumEntryDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited inductive ArgumentType where | int @@ -40,7 +42,7 @@ inductive ArgumentType where | fd | newID | object -deriving Repr, BEq +deriving Repr, BEq, Inhabited structure ArgumentDesc where name : String @@ -49,12 +51,12 @@ structure ArgumentDesc where interface : Option String enum : Option String allowNull : Bool - deriving Repr, BEq + deriving Repr, BEq, Inhabited inductive MessageType where | normal | destructor -deriving Repr, BEq +deriving Repr, BEq, Inhabited structure MessageDesc where name : String @@ -64,7 +66,7 @@ structure MessageDesc where since : Nat deprecatedSince : Option Nat arguments : Array ArgumentDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure InterfaceDesc where name : String @@ -73,14 +75,14 @@ structure InterfaceDesc where enums : Array EnumDesc requests : Array MessageDesc events : Array MessageDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure ProtocolDesc where name : String copyright : Option String description : Option Description interfaces : Array InterfaceDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited end Raw @@ -89,11 +91,11 @@ namespace Client structure InterfaceRef where moduleName : Identifier typeName : Identifier - deriving Repr, BEq + deriving Repr, BEq, Ord, Inhabited structure EnumRef extends InterfaceRef where enumName : Identifier - deriving Repr, BEq + deriving Repr, BEq, Ord, Inhabited structure EnumEntryDesc where name : Identifier @@ -101,7 +103,7 @@ structure EnumEntryDesc where description : Option Description since : Nat deprecatedSince : Option Nat - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure EnumDesc where name : Identifier @@ -109,12 +111,12 @@ structure EnumDesc where since : Nat bitfield : Bool entries: Array EnumEntryDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited inductive Nullability where | nullable | notNull -deriving Repr, BEq +deriving Repr, BEq, Inhabited def Nullability.ofAllowNull (allowNull : Bool) : Nullability := if allowNull then .nullable else .notNull @@ -127,13 +129,13 @@ inductive ArgumentType where | array | fd | object (nullability : Nullability) (interface : Option InterfaceRef) -deriving Repr, BEq +deriving Repr, BEq, Inhabited structure ArgumentDesc where name : Identifier type : ArgumentType description : Option Description - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure MessageDesc where name : Identifier @@ -143,19 +145,19 @@ structure MessageDesc where since : Nat deprecatedSince : Option Nat arguments : Array ArgumentDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited inductive ReturnType where | unit | object (type : Option InterfaceRef) -deriving Repr, BEq +deriving Repr, BEq, Inhabited structure RequestDesc extends MessageDesc where returnType : ReturnType - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure EventDesc extends MessageDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited structure InterfaceDesc where name : Identifier @@ -164,15 +166,15 @@ structure InterfaceDesc where enums : Array EnumDesc requests : Array RequestDesc events : Array EventDesc - referencedInterfaces : Array InterfaceRef - deriving Repr, BEq + referencedInterfaces : Std.TreeSet InterfaceRef + deriving Repr, BEq, Inhabited structure ProtocolDesc where name : Identifier copyright : Option String description : Option Description interfaces : Array InterfaceDesc - deriving Repr, BEq + deriving Repr, BEq, Inhabited end Client |