Merge pull request #11 from Seasawher/nested-comment

feat: treat nested block comment

Mdgen/ConvertToMd.lean

@@ -6,47 +6,126 @@ syntax ident "++=" term : doElem
 macro_rules
   | `(doElem| $x:ident ++= $e:term) => `(doElem| ($x) := ($x) ++ ($e))
 
+structure RichLine where
+  /-- text content -/
+  content : String
+
+  /-- nest level -/
+  level : Nat
+
+  /-- whether the line ends with the closing symbol or not. -/
+  close : Bool
+  deriving Repr, BEq, Inhabited
+
+instance : ToString RichLine where
+  toString := fun l => l.content
+
+/-- Receive a list of codes and count the nesting of block and sectioning comments.
+* The corresponding opening and closing brackets should have the same level.
+* Also handles the exclusion of ignored targets.
+-/
+def analysis (lines : List String) : List RichLine := Id.run do
+  let mut res : List RichLine := []
+  let mut level := 0
+  for line in lines do
+    if line.endsWith "--#" then
+      continue
+    if line.startsWith "/-" && ! line.startsWith "/--" then
+      level := level + 1
+    res := {content := line, level := level, close := line.endsWith "-/"} :: res
+    if line.endsWith "-/" then
+      level := level - 1
+  return res.reverse
+
+namespace analysis
+
+def runTest (input : List String) (expected : List (Nat × Bool)) (title := "") : IO Unit :=
+  let output := analysis input
+  if output.map (fun x => (x.level, x.close)) = expected then
+    IO.println s!"{title} test passed!"
+  else
+    throw <| .userError s!"Test failed: \n{output}"
+
+#eval runTest
+  (title := "nested block comment")
+  [
+    "/-",
+      "/- hoge",
+      "-/",
+      "/-",
+      "-/",
+      "hoge",
+    "-/",
+    "foo"
+  ]
+  [(1, false), (2, false), (2, true), (2, false), (2, true), (1, false), (1, true), (0, false)]
+
+#eval runTest
+  (title := "sectioning comment and nested block comment")
+  [
+    "/-! hoge fuga",
+      "/- foo! -/",
+    "-/",
+    "def foo := 1",
+  ]
+  [(1, false), (2, true), (1, true), (0, false)]
+
+#eval runTest
+  (title := "one line doc comment")
+  [
+    "/-- hoge -/",
+    "def hoge := \"hoge\"",
+  ]
+  [(0, true), (0, false)]
+
+#eval runTest
+  (title := "multi line doc comment")
+  [
+    "/-- hoge",
+    "fuga -/",
+    "def hoge := 42",
+  ]
+  [(0, false), (0, true), (0, false)]
+
+end analysis
+
 /-- A chunk of grouped code for conversion to markdown. -/
 structure Block where
   content : String
   toCodeBlock : Bool
   deriving Repr
 
-private def buildBlocks (lines : List String) : List Block := Id.run do
-  let mut toCodeBlock := true
-  let mut blocks : List Block := []
-  let mut content := ""
-  for ⟨i, line⟩ in lines.enum do
-    if line.endsWith "--#" then
-      continue
+instance : ToString Block where
+  toString := fun b =>
+    s!"content: \n{b.content}\n toCodeBlock: {b.toCodeBlock}\n\n"
 
-    if line.startsWith "/-" && ! line.startsWith "/--" then
-      if ! toCodeBlock then
-        panic!
-          "Nested lean commentary sections not allowed in:\n" ++
-          s!" line {i+1}: {line}"
-
-      if content != "" then
-        blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
-      toCodeBlock := ! toCodeBlock
-      content := line ++ "\n"
-
-      if line.endsWith "-/" then
-        blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
-        toCodeBlock := ! toCodeBlock
-        content := ""
-
-    else if line.endsWith "-/" && ! toCodeBlock then
-      content ++= line
-      blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
-      toCodeBlock := ! toCodeBlock
-      content := ""
-    else
-      content ++= line ++ "\n"
-
-  if content != "" then
-    blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
-  return blocks.reverse
+def listShift {α : Type} (x : List α × List α) : List α × List α :=
+  let ⟨l, r⟩ := x
+  match r with
+  | [] => (l, [])
+  | y :: ys => (l ++ [y], ys)
+
+partial def buildBlocks (lines : List RichLine) : List Block :=
+  match lines with
+  | [] => []
+  | line :: _ =>
+    let ⟨_, level, _⟩ := line
+
+    let splited := (
+      if level == 0 then
+        lines.span (fun x => x.level == 0)
+      else
+        listShift <| lines.span (fun x => x.level > 1 || ! x.close)
+    )
+    let fstBlock : Block := {
+      content := splited.fst
+        |>.map (·.content)
+        |>.map (· ++ "\n")
+        |>.foldl (· ++ ·) ""
+        |>.trim,
+      toCodeBlock := (level == 0)
+    }
+    fstBlock :: buildBlocks splited.snd
 
 /-- markdown text -/
 abbrev Md := String
@@ -59,15 +138,15 @@ private def Block.toMd (b : Block) : Md :=
   else
     let separator := if b.content.startsWith "/-!" then "/-!" else "/-"
     b.content
-      |> (String.splitOn · separator)
-      |> List.drop 1
-      |> List.foldl (· ++ ·) ""
-      |> (String.splitOn · "-/")
-      |> List.dropLast
-      |> List.foldl (· ++ ·) ""
+      |> (String.drop · separator.length)
+      |> (String.dropRight · "-/".length)
       |> String.trim
       |> (· ++ "\n\n")
 
+instance : ToString Block where
+  toString := fun b =>
+    s!"content: \n{b.content}\n toCodeBlock: {b.toCodeBlock}\n\n"
+
 private def mergeBlocks (blocks : List Block) : Md :=
   let res := blocks
     |>.map Block.toMd
@@ -76,7 +155,7 @@ private def mergeBlocks (blocks : List Block) : Md :=
 
 /-- convert lean contents to markdown contents. -/
 def convertToMd (lines : List String) : Md :=
-  let blocks := buildBlocks lines
+  let blocks := buildBlocks <| analysis lines
   mergeBlocks blocks
 
 namespace ConvertToMd
@@ -89,7 +168,7 @@ def runTest (input : List String) (expected : List String) (title := "") : IO Un
   if output = expected.withBreakLine then
     IO.println s!"{title} test passed!"
   else
-    throw <| .userError s!"Test failed: {output}"
+    throw <| .userError s!"Test failed: \n{output}"
 
 #eval runTest
   (title := "inline comment")
@@ -164,7 +243,7 @@ def runTest (input : List String) (expected : List String) (title := "") : IO Un
   [
     "/-",
     "this is a test",
-    "of multiline block comment -/"
+    "of multiline block comment -/",
   ]
   [
     "this is a test",
@@ -186,4 +265,65 @@ def runTest (input : List String) (expected : List String) (title := "") : IO Un
     "```"
   ]
 
+#eval runTest
+  (title := "block comment repeated")
+  [
+    "/- hoge -/",
+    "/- fuga -/",
+  ]
+  [
+    "hoge",
+    "",
+    "fuga"
+  ]
+
+#eval runTest
+  (title := "nested block comment")
+  [
+    "/-",
+    "this is a test",
+    "/- nested comment -/",
+    "of nested block comment -/"
+  ]
+  [
+    "this is a test",
+    "/- nested comment -/",
+    "of nested block comment"
+  ]
+
+#eval runTest
+  (title := "raw code block")
+  [
+    "/-",
+    "```lean",
+    "/- this is test -/",
+    "```",
+    "fuga",
+    "-/",
+    "/- hoge -/",
+  ]
+  [
+    "```lean",
+    "/- this is test -/",
+    "```",
+    "fuga",
+    "",
+    "hoge"
+  ]
+
+#eval runTest
+  (title := "indent in raw code block")
+  [
+    "/-",
+    "```lean",
+    "  hoge",
+    "```",
+    "-/"
+  ]
+  [
+    "```lean",
+    "  hoge",
+    "```"
+  ]
+
 end ConvertToMd

README.md

@@ -19,6 +19,8 @@ Don't forget to run `lake update mdgen` after editing the `lakefile`. And simply
 
 * The comments enclosed with an `/-! ... -/` or `/- ... -/` are converted as ground text.
 
+* Nested block comments can also be handled.
+
 * The inline comment, doc comment and non-comment parts are converted to lean code blocks.
 
 * Lines ending with `--#` are ignored.

Test/Exp/First.md

@@ -39,3 +39,12 @@ example (h : P) : P ∨ Q := by
   apply Or.inl
   exact h
 ```
+
+## nested comment
+Here is a sample of nested block comment:
+/- Hi. I am a nested comment! -/
+
+Here is another example of nested block comment:
+```lean
+/- wao. this is another sample!! -/
+```

Test/Src/First.lean

@@ -42,3 +42,13 @@ example (h : P) : P ∨ Q := by
   -/
   apply Or.inl
   exact h
+
+/- ## nested comment
+Here is a sample of nested block comment:
+/- Hi. I am a nested comment! -/
+
+Here is another example of nested block comment:
+```lean
+/- wao. this is another sample!! -/
+```
+-/