J main dev (#14)

Main.lean

@@ -40,13 +40,13 @@ def main (args : List String) : IO UInt32 := do
       return 0
   else if args.length = 1 then
     let file := args[0]!
-    let fp : FilePath := System.mkFilePath ["Tests", file]
+    let fp : FilePath := System.mkFilePath [file]
     let content ← readFile fp
     let content := StableHLO.Parsing.parse content
     match content with
     | .ok p =>
-      let fpAST : FilePath := System.mkFilePath ["Tests", file ++ ".ast"]
-      let fpReport : FilePath := System.mkFilePath ["Tests", file ++ ".report"]
+      let fpAST : FilePath := System.mkFilePath [file ++ ".ast"]
+      let fpReport : FilePath := System.mkFilePath [file ++ ".report"]
       writeFile fpAST s!"{repr p.1}\n"
       writeFile fpReport s!"{p.2.report}\n"
       return 0

SHerLOC/Parsing/Functions.lean

@@ -91,7 +91,6 @@ def parseFunctionDictionaryAttributes : PState (String × FunctionType × (List
     throw <| ← error "A6"
 
 def parseFunction : PState Function := do
-  push "parseFunction"
   parseItems ["\"func.func\"", "(", ")"]
   parseItem "<{"
   let (name,typ,argAttrs,resAttrs) ← parseFunctionDictionaryAttributes
@@ -107,13 +106,9 @@ def parseFunction : PState Function := do
   parseItem "})"
   parseItems [":","(",")","->","(",")"]
   let r : Function := { funcId := name , funcArgAttrs := argAttrs , funcResAttrs := resAttrs , funcType := typ, funcBody := body }
-  pop "parseFunction"
   return r
 
 def parseFunctions : PState (List Function) := do
-  push "parseFunctions"
-  let r ← parseListAuxNoSep "}" parseFunction []
-  pop "parseFunctions"
-  return r
+  parseListAuxNoSep "}" parseFunction []
 
 end StableHLO.Parsing

SHerLOC/Parsing/Identifiers.lean

@@ -9,52 +9,36 @@ import SHerLOC.Parsing.Parser
 namespace StableHLO.Parsing
 
 def parseValueId : PState String := do
-  push "parseValueId"
   parseItem "%"
-  let r ← parseId
-  pop "parseValueId"
-  return r
+  parseId
 
 def parseValueIdRes : PState String := do
-  push "parseValueIdRes"
   let r ← parseValueId
   let mut r' := ""
   if ← isParse ":" then
     r' ← parseId
     r' := ":" ++ r'
   let r := r ++ r'
-  pop "parseValueIdRes"
   return r
 
 def parseValueIdOpArg : PState String := do
-  push "parseValueOpArg"
   let r ← parseValueId
   let mut r' := ""
   if ← isParse "#" then
     r' ← parseId
     r' := "#" ++ r'
   let r := r ++ r'
-  pop "parseValueOpArg"
   return r
 
 def parseFuncId : PState String := do
-  push "parseFuncId"
   parseItem "@"
-  let r ← parseFId
-  pop "parseFuncId"
-  return r
+  parseFId
 
 def parseUnusedId : PState String := do
-  push "parseUnusedId"
   parseItem "^"
-  let r ← parseId
-  pop "parseUnusedId"
-  return r
+  parseId
 
 def parseAttrId : PState String := do
-  push "parseAttrId"
-  let r ← parseId
-  pop "parseAttrId"
-  return r
+  parseId
 
 end StableHLO.Parsing

SHerLOC/Parsing/Intermediate.lean

@@ -7,7 +7,6 @@ import SHerLOC.AST1
 import SHerLOC.Parsing.Parser
 import SHerLOC.Parsing.Identifiers
 import SHerLOC.Parsing.Types
-import SHerLOC.Parsing.Constants
 
 namespace StableHLO.Parsing
 
@@ -27,17 +26,13 @@ def parseStableHLORecordFieldValue : PState (StableHLORecordFieldValue) := do
     return StableHLORecordFieldValue.type type
 
 def parseStableHLORecordField : PState (StableHLORecordField) := do
-  push "parseStableHLORecordField"
   let name ← parseId
   parseItem "="
   let value ← parseStableHLORecordFieldValue
-  pop "parseStableHLORecordField"
   return StableHLORecordField.mk name value
 
 def parseRecord : PState (List StableHLORecordField) := do
-  push "parseRecord"
   let r ← parseList "<" ">" "," parseStableHLORecordField
-  pop "parseRecord"
   return r
 
 mutual
@@ -85,41 +80,30 @@ mutual
     throw <| (← error "literal")
 
   partial def parseConstant : PState Constant := do
-    push "parseConstant"
     let literal ← parseLiteral
     let mut typ : Option SType := none
     if ← isParse ":" then
       typ ← parseType
     let r : Constant := Constant.mk literal typ
-    pop "parseConstant"
     return r
 
   partial def parseAttribute : PState Attribute := do
-    push "parseAttribute"
     if ← isParse "use_global_device_ids" then
       report "literal use_global_device_ids"
-      pop "parseAttribute"
       return Attribute.mk "use_global_device_ids" <| Constant.mk (Literal.element (ElementLiteral.booleanLiteral BooleanLiteral.true)) none
     else
       let id ← parseId
       parseItem "="
       let constant ← parseConstant
-      pop "parseAttribute"
       return Attribute.mk id constant
 
 partial def parseAttributes : PState (List Attribute) := do
-  push "parseAttributes"
-  let r ← parseList "{" "}" "," parseAttribute
-  pop "parseAttributes"
-  return r
+  parseList "{" "}" "," parseAttribute
 
 end
 
 def parseValueUseList : PState (List ValueId) := do
-  push "parseValueUseList"
-  let r ← parseList "(" ")" "," parseValueIdOpArg
-  pop "parseValueUseList"
-  return r
+  parseList "(" ")" "," parseValueIdOpArg
 
 def tryParseDictionaryEntry (name : String) (parser : PState T) : PState (Option T) := do
   if ← is name then
@@ -130,9 +114,6 @@ def tryParseDictionaryEntry (name : String) (parser : PState T) : PState (Option
   else return none
 
 def parseDictionaryProperties : PState (List Attribute) := do
-  push "parseDictionaryProperties"
-  let r ← parseList "<{" "}>" "," parseAttribute
-  pop "parseDictionaryProperties"
-  return r
+  parseList "<{" "}>" "," parseAttribute
 
 end StableHLO.Parsing

SHerLOC/Parsing/Modules.lean

@@ -12,7 +12,6 @@ import SHerLOC.Parsing.Intermediate
 namespace StableHLO.Parsing
 
 def parseModule : PState Module := do
-  push "parseModule"
   parseItems ["\"builtin.module\"", "(", ")"]
   let mut name : Option FuncId := none
   if ← is "<{" then
@@ -27,7 +26,6 @@ def parseModule : PState Module := do
       let r : Module := { modId := name, modAttrs := [], modFuncs := [] }
       parseItems ["}",")"]
       parseItems [":","(",")","->","(",")"]
-      pop "parseModule"
       return r
     let region ← parseFunctions
     parseItems ["}",")"]
@@ -36,23 +34,18 @@ def parseModule : PState Module := do
       attributes ← parseAttributes
     parseItems [":","(",")","->","(",")"]
     let r : Module := { modId := name, modAttrs := attributes, modFuncs := region }
-    pop "parseModule"
     return r
   else
     let r : Module := { modId := name, modAttrs := [], modFuncs := [] }
-    pop "parseModule"
     return r
 
 partial def parseModules : PState (List Module) := do
-  push "parseModules"
   let done ← done?
   if done then
-    pop "parseModules"
     return []
   else
     let mod ← parseModule
     let mods ← parseModules
-    pop "parseModules"
     return mod :: mods