Merge pull request #33 from pandaman64/regex-literal

Compile-time regex compilation

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

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

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 => .app (mkConst ``Class.perl) (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

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)]