From 617f07d4902bca871a376f09f1a3e7903c9aefa1 Mon Sep 17 00:00:00 2001
From: pandaman64 <kointosudesuyo@infoseek.jp>
Date: Sun, 8 Dec 2024 20:55:26 +0900
Subject: [PATCH 1/2] Implements the re! syntax for generating a Regex object
 at compile time

---
 Regex/NFA/Basic.lean  | 20 +++++++++++
 Regex/Regex.lean      |  1 +
 Regex/Regex/Elab.lean | 79 +++++++++++++++++++++++++++++++++++++++++++
 Test.lean             |  3 +-
 4 files changed, 102 insertions(+), 1 deletion(-)
 create mode 100644 Regex/Regex/Elab.lean

diff --git a/Regex/NFA/Basic.lean b/Regex/NFA/Basic.lean
index 455f58e..08afc76 100644
--- a/Regex/NFA/Basic.lean
+++ b/Regex/NFA/Basic.lean
@@ -87,6 +87,16 @@ theorem Node.inBounds_of_inBounds_of_le {n : Node} (h : n.inBounds size) (le : s
   next => exact Nat.lt_of_lt_of_le h le
   next => exact Nat.lt_of_lt_of_le h le
 
+instance Node.decInBounds {node : Node} {size : Nat} : Decidable (node.inBounds size) :=
+  match node with
+  | .done => isTrue trivial
+  | .fail => isTrue trivial
+  | .epsilon next => inferInstanceAs (Decidable (next < size))
+  | .char _ next => inferInstanceAs (Decidable (next < size))
+  | .sparse _ next => inferInstanceAs (Decidable (next < size))
+  | .split next₁ next₂ => inferInstanceAs (Decidable (next₁ < size ∧ next₂ < size))
+  | .save _ next => inferInstanceAs (Decidable (next < size))
+
 end Regex.NFA
 
 namespace Regex
@@ -151,5 +161,15 @@ theorem done_WellFormed : done.WellFormed :=
     | ⟨_ + 1, isLt⟩ => contradiction
   ⟨start_lt, inBounds⟩
 
+instance decWellFormed (nfa : NFA) : Decidable nfa.WellFormed :=
+  let decStartLt := inferInstanceAs (Decidable (nfa.start < nfa.nodes.size))
+  match decStartLt with
+  | isTrue h₁ =>
+    let decInBounds := inferInstanceAs (Decidable (∀ i : Fin nfa.nodes.size, nfa[i].inBounds nfa.nodes.size))
+    match decInBounds with
+    | isTrue h₂ => isTrue ⟨h₁, h₂⟩
+    | isFalse h₂ => isFalse (fun h => absurd h.2 h₂)
+  | isFalse h₁ => isFalse (fun h => absurd h.1 h₁)
+
 end NFA
 end Regex
diff --git a/Regex/Regex.lean b/Regex/Regex.lean
index 1be703e..8a910c3 100644
--- a/Regex/Regex.lean
+++ b/Regex/Regex.lean
@@ -2,3 +2,4 @@ import Regex.Regex.Basic
 import Regex.Regex.Matches
 import Regex.Regex.Captures
 import Regex.Regex.Utilities
+import Regex.Regex.Elab
diff --git a/Regex/Regex/Elab.lean b/Regex/Regex/Elab.lean
new file mode 100644
index 0000000..63ae6a6
--- /dev/null
+++ b/Regex/Regex/Elab.lean
@@ -0,0 +1,79 @@
+import Regex.Regex.Basic
+import Lean
+
+open Regex.Data (PerlClassKind PerlClass Class Classes)
+open Regex NFA Node
+open Lean Syntax Elab Term
+
+set_option autoImplicit false
+
+namespace Regex.Elab
+
+-- A term representing a proof of `prop` given by letting kernel decide `prop`
+-- using an `Decidable` instance `inst`.
+private def mkDecidableProof (prop : Expr) (inst : Expr) : Expr :=
+  let refl := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Bool) (mkConst ``true)
+  mkApp3 (mkConst ``of_decide_eq_true) prop inst refl
+
+instance : ToExpr PerlClassKind where
+  toTypeExpr := mkConst ``PerlClassKind
+  toExpr
+    | .digit => mkConst ``PerlClassKind.digit
+    | .space => mkConst ``PerlClassKind.space
+    | .word => mkConst ``PerlClassKind.word
+
+instance : ToExpr PerlClass where
+  toTypeExpr := mkConst ``PerlClass
+  toExpr pc := mkApp2 (mkConst ``PerlClass.mk) (toExpr pc.negated) (toExpr pc.kind)
+
+instance : ToExpr Class where
+  toTypeExpr := mkConst ``Class
+  toExpr
+    | .single c => .app (mkConst ``Class.single) (toExpr c)
+    | .range s e _ =>
+      let s := toExpr s
+      let e := toExpr e
+      -- Construct a term representing `s ≤ e` using a decidable instance.
+      let leType := mkApp4 (mkConst ``LE.le [0]) (mkConst ``Char) (mkConst ``Char.instLE) s e
+      let leInstance := mkApp2 (mkConst ``Char.instDecidableLe) s e
+      let le := mkDecidableProof leType leInstance
+
+      mkApp3 (mkConst ``Class.range) s e le
+    | .perl pc => toExpr pc
+
+instance : ToExpr Classes where
+  toTypeExpr := mkConst ``Classes
+  toExpr cs := mkApp2 (mkConst ``Classes.mk) (toExpr cs.negated) (toExpr cs.classes)
+
+instance : ToExpr Node where
+  toTypeExpr := mkConst ``Node
+  toExpr
+    | .done => mkConst ``Node.done
+    | .fail => mkConst ``Node.fail
+    | .epsilon next => .app (mkConst ``Node.epsilon) (toExpr next)
+    | .char c next => mkApp2 (mkConst ``Node.char) (toExpr c) (toExpr next)
+    | .sparse cs next => mkApp2 (mkConst ``Node.sparse) (toExpr cs) (toExpr next)
+    | .split next₁ next₂ => mkApp2 (mkConst ``Node.split) (toExpr next₁) (toExpr next₂)
+    | .save tag next => mkApp2 (mkConst ``Node.save) (toExpr tag) (toExpr next)
+
+instance : ToExpr NFA where
+  toTypeExpr := mkConst ``NFA
+  toExpr nfa := mkApp2 (mkConst ``NFA.mk) (toExpr nfa.nodes) (toExpr nfa.start)
+
+instance : ToExpr Regex where
+  toTypeExpr := mkConst ``Regex
+  toExpr re :=
+    let nfa := toExpr re.nfa
+    -- Construct a term representing `nfa.WellFormed` using a decidable instance.
+    let wfType := Expr.app (mkConst ``NFA.WellFormed) nfa
+    let wfInstance := Expr.app (mkConst ``NFA.decWellFormed) nfa
+    let wf := mkDecidableProof wfType wfInstance
+    let maxTag := toExpr re.maxTag
+    mkApp3 (mkConst ``Regex.mk) nfa wf maxTag
+
+elab "re!" lit:str : term => do
+  match Regex.parse lit.getString with
+  | Except.ok re => return toExpr re
+  | Except.error e => throwError s!"failed to parse regex: {e}"
+
+end Regex.Elab
diff --git a/Test.lean b/Test.lean
index 20e6395..e968ea9 100644
--- a/Test.lean
+++ b/Test.lean
@@ -14,7 +14,8 @@ def main : IO Unit := do
   IO.println replaced
 
   -- Search/replace all non-overlapping matches
-  let regex := Regex.parse! "もも"
+  -- The re! literal checks for regex errors at compile time and creates a compiled `Regex` object
+  let regex := re!"もも"
   let haystack := "すもももももももものうち"
 
   -- prints: #[(3, 9), (9, 15), (15, 21), (21, 27)]

From 675fe4f615bc2daa8902ecf2e1a5612b166e405a Mon Sep 17 00:00:00 2001
From: pandaman64 <kointosudesuyo@infoseek.jp>
Date: Sun, 8 Dec 2024 21:22:47 +0900
Subject: [PATCH 2/2] Fix elaboration of perl classes

---
 Regex/Regex/Elab.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Regex/Regex/Elab.lean b/Regex/Regex/Elab.lean
index 63ae6a6..4cee94b 100644
--- a/Regex/Regex/Elab.lean
+++ b/Regex/Regex/Elab.lean
@@ -39,7 +39,7 @@ instance : ToExpr Class where
       let le := mkDecidableProof leType leInstance
 
       mkApp3 (mkConst ``Class.range) s e le
-    | .perl pc => toExpr pc
+    | .perl pc => .app (mkConst ``Class.perl) (toExpr pc)
 
 instance : ToExpr Classes where
   toTypeExpr := mkConst ``Classes