From f37a1f53f41614e69e4cfab578a2b5c891e1c096 Mon Sep 17 00:00:00 2001
From: John Tristan <jean.baptiste.tristan@gmail.com>
Date: Fri, 13 Sep 2024 15:10:54 -0400
Subject: [PATCH] Fixed parsing of modules

---
 SHerLOC/Parsing/Modules.lean | 11 +++++++----
 SHerLOC/Parsing/Parser.lean  | 18 +++++++++++-------
 2 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/SHerLOC/Parsing/Modules.lean b/SHerLOC/Parsing/Modules.lean
index 5542af6..2f94ba6 100644
--- a/SHerLOC/Parsing/Modules.lean
+++ b/SHerLOC/Parsing/Modules.lean
@@ -45,13 +45,16 @@ def parseModule : PState Module := do
 
 partial def parseModules : PState (List Module) := do
   push "parseModules"
-  if (← is "\"builtin.module\"") then
+  let done ← done?
+  if done then
+    pop "parseModules"
+    return []
+  else
     let mod ← parseModule
     let mods ← parseModules
     pop "parseModules"
     return mod :: mods
-  else
-    pop "parseModules"
-    return []
+
+
 
 end StableHLO.Parsing
diff --git a/SHerLOC/Parsing/Parser.lean b/SHerLOC/Parsing/Parser.lean
index d470101..f92fdd7 100644
--- a/SHerLOC/Parsing/Parser.lean
+++ b/SHerLOC/Parsing/Parser.lean
@@ -67,9 +67,9 @@ def error (msg : String) : PState (String × (List Trace) × (List Derivation) )
   let errorMsg := s!"Parsing error line {st.lineNumber}, column {st.columnNumber} : expected {msg} but found {token}"
   return (errorMsg, st.trace, st.derivations)
 
-def skipComment (st : ParsingState) : Nat := Id.run do
+def skipComment (index : Nat) (st : ParsingState) : Nat := Id.run do
   let mut count := 0
-  for i in [st.index:st.stop] do
+  for i in [index:st.stop] do
     let c := st.source.get! ⟨ i ⟩
     count := count + 1
     if c = '\n' then
@@ -93,11 +93,10 @@ def skip : PState Unit := do
     else if c = '\t' then
       count := count + 1
       column := column + 8
-    else if c = '/' then
-      if st.source.get! ⟨ i + 1 ⟩ = '/' then -- comment
-        count := count + skipComment (← get) + 2
-        lines := lines + 1
-        column := 0
+    else if c = '/' && st.source.get! ⟨ i + 1 ⟩ = '/' then
+      count := count + skipComment (st.index + count) (← get)
+      lines := lines + 1
+      column := 0
     else break
   set { st with
     index := st.index + count,
@@ -105,6 +104,11 @@ def skip : PState Unit := do
     columnNumber := column
     }
 
+def done? : PState Bool := do
+  skip
+  let st ← get
+  if st.index >= st.stop then return true else return false
+
 def parseItem (keyword : String) : PState Unit := do
   skip
   let st ← get