.

Main.lean

@@ -17,7 +17,7 @@ def main (args : List String) : IO UInt32 := do
     for file in files do
       let fp : FilePath := System.mkFilePath ["Tests", file]
       let content ← readFile fp
-      let content := StableHLO.parse content
+      let content := StableHLO.Parsing.parse content
       IO.print s!"Parsing {file}... "
       match content with
       | .ok _ =>
@@ -39,7 +39,7 @@ def main (args : List String) : IO UInt32 := do
     let file := args[0]!
     let fp : FilePath := System.mkFilePath ["Tests", file]
     let content ← readFile fp
-    let content := StableHLO.parse content
+    let content := StableHLO.Parsing.parse content
     match content with
     | .ok p =>
       IO.println s!"{repr p}"

SHerLOC/AST1.lean

@@ -9,7 +9,7 @@ Authors: Jean-Baptiste Tristan
 
 -/
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 abbrev FuncId := String
 
@@ -205,11 +205,15 @@ structure QuantizationParameter where
   quantizationZeroPoint: IntegerLiteral
   deriving Repr, Inhabited, Nonempty
 
-structure QuantizedTensorElementType where
+structure QuantizationBasics where
   quantizationStorageType : IntegerType
   quantizationStorageMinMax : Option (IntegerLiteral × IntegerLiteral)
   quantizationExpressedType : FloatType
   quantizationDimension : Option IntegerLiteral
+  deriving Repr, Inhabited, Nonempty
+
+structure QuantizedTensorElementType where
+  quantizationBasics : QuantizationBasics
   quantizationParameters : List QuantizationParameter
   deriving Repr, Inhabited, Nonempty
 
@@ -306,4 +310,4 @@ structure Module where
 def Program := List Module
   deriving Repr, Inhabited, Nonempty
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Constants.lean

@@ -7,7 +7,7 @@ import SHerLOC.AST1
 import SHerLOC.Parsing.Parser
 import SHerLOC.Parsing.Types
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parseConstant : PState Constant := do
   push "parseConstant"
@@ -19,4 +19,4 @@ def parseConstant : PState Constant := do
   pop "parseConstant"
   return r
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Functions.lean

@@ -8,7 +8,7 @@ import SHerLOC.Parsing.Parser
 import SHerLOC.Parsing.Operations
 import SHerLOC.Parsing.Intermediate
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def tryParseDEntryFunctionType : PState (Option FunctionType) := do
   tryParseDictionaryEntry "function_type" parseFunctionType
@@ -116,4 +116,4 @@ def parseFunctions : PState (List Function) := do
   pop "parseFunctions"
   return r
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Identifiers.lean

@@ -6,7 +6,7 @@ Authors: Jean-Baptiste Tristan
 import SHerLOC.AST1
 import SHerLOC.Parsing.Parser
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parseValueId : PState String := do
   push "parseValueId"
@@ -57,4 +57,4 @@ def parseAttrId : PState String := do
   pop "parseAttrId"
   return r
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Intermediate.lean

@@ -9,7 +9,7 @@ import SHerLOC.Parsing.Identifiers
 import SHerLOC.Parsing.Types
 import SHerLOC.Parsing.Constants
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parseAttribute : PState Attribute := do
   push "parseAttribute"
@@ -49,4 +49,4 @@ def parseDictionaryProperties : PState (List Attribute) := do
   pop "parseDictionaryProperties"
   return r
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Modules.lean

@@ -9,7 +9,7 @@ import SHerLOC.Parsing.Operations
 import SHerLOC.Parsing.Functions
 import SHerLOC.Parsing.Intermediate
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parseModule : PState Module := do
   push "parseModule"
@@ -47,4 +47,4 @@ def parseModules : PState (List Module) := do
       r := [← parseModule]
   return r
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Numbers.lean

@@ -7,7 +7,7 @@ import SHerLOC.AST1
 import SHerLOC.Parsing.Parser
 import SHerLOC.Parsing.Identifiers
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parseBooleanLiteral : PState BooleanLiteral := do
   if ← isParse "true" then return BooleanLiteral.true
@@ -309,4 +309,4 @@ def parseLiteral : PState Literal := do
 
   throw <| ← error "literal"
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Operations.lean

@@ -9,7 +9,7 @@ import SHerLOC.Parsing.Constants
 import SHerLOC.Parsing.Identifiers
 import SHerLOC.Parsing.Intermediate
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parseOpOutputs : PState (List ValueId) := do
   push "parseOpOutputs"
@@ -121,4 +121,4 @@ partial def parseInputFuncBody : PState (List Operation) := do
 
 end
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Parser.lean

@@ -5,7 +5,7 @@ Authors: Jean-Baptiste Tristan
 -/
 import SHerLOC.AST1
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 structure Trace where
   startLine : Nat
@@ -305,4 +305,4 @@ def parseListNoSep (openingMark closingMark : String) (parse : PState T) : PStat
   parseItem closingMark
   return attrs
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Programs.lean

@@ -7,9 +7,9 @@ import SHerLOC.AST1
 import SHerLOC.Parsing.Parser
 import SHerLOC.Parsing.Modules
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def parse (src : String) : Except (String × List Trace × List Derivation) Program := do
   parseModules.run' <| ParsingState.mk src 0 src.length 1 0 [] []
 
-end StableHLO
+end StableHLO.Parsing

SHerLOC/Parsing/Types.lean

@@ -7,7 +7,7 @@ import SHerLOC.AST1
 import SHerLOC.Parsing.Parser
 import SHerLOC.Parsing.Numbers
 
-namespace StableHLO
+namespace StableHLO.Parsing
 
 def tryParseIntegerType : PState (Option IntegerType) := do
   push "tryParseIntegerType"
@@ -134,15 +134,18 @@ def parseQuantizedTensorElementType : PState QuantizedTensorElementType := do
   let quantizationExpressedType ← parseFloatType
   let mut quantizationDimension := none
   if ← isParse ":" then
-    quantizationDimension ← parseIntegerLiteral
+    quantizationDimension := some (← parseIntegerLiteral)
   parseItem ","
   let quantizationParameters ← parseQuantizationParameters
   parseItem ">"
-  let parseResult : QuantizedTensorElementType :=
+  let quantizationBasics : QuantizationBasics :=
     { quantizationStorageType := quantizationStorageType,
       quantizationStorageMinMax := quantizationStorageMinMax,
       quantizationExpressedType := quantizationExpressedType,
-      quantizationDimension := quantizationDimension,
+      quantizationDimension := quantizationDimension
+    }
+  let parseResult : QuantizedTensorElementType :=
+    { quantizationBasics := quantizationBasics
       quantizationParameters := quantizationParameters
     }
   pop "parseQuantizedTensorElementType"
@@ -238,4 +241,4 @@ def parseType : PState SType := do
     return SType.valueType <|  ← parseValueType
   return SType.nonValueType <| NonValueType.tensorElementType <| ← parseTensorElementType
 
-end StableHLO
+end StableHLO.Parsing