[ fix #835 ] Text.Regex (#1391)

Author: gallais

CHANGELOG.md

@@ -291,6 +291,31 @@ New modules
   Algebra.Morphism.LatticeMonomorphism
   ```
 
+* New ternary relation on lists:
+  ```
+  Data.List.Relation.Ternary.Appending
+  Data.List.Relation.Ternary.Appending.Properties
+  Data.List.Relation.Ternary.Appending.Propositional
+  Data.List.Relation.Ternary.Appending.Propositional.Properties
+  Data.List.Relation.Ternary.Appending.Setoid
+  Data.List.Relation.Ternary.Appending.Setoid.Properties
+  ```
+
+* New modules formalising regular expressions:
+  ```
+  Text.Regex
+  Text.Regex.Base
+  Text.Regex.Derivative.Brzozowski
+  Text.Regex.Properties.Core
+  Text.Regex.Properties
+  Text.Regex.Search
+  Text.Regex.SmartConstructors
+  Text.Regex.String
+  Text.Regex.String.Unsafe
+
+  README.Text.Regex
+  ```
+
 Other major changes
 -------------------
 
@@ -694,6 +719,14 @@ Other minor additions
   ```agda
   linesBy : Decidable P → String → List String
   lines   : String → List String
+
+  _≤_ : Rel String zero
+  ```
+
+* Added new proofs to `Data.String.Properties`:
+  ```agda
+  ≤-isDecPartialOrder-≈ : IsDecPartialOrder _≈_ _≤_
+  ≤-decPoset-≈          : DecPoset _ _ _
   ```
 
 * Added new function to `Data.Maybe.Base`:
@@ -757,6 +790,22 @@ Other minor additions
   resp : (P : Pred A ℓ) → P Respects _≡_
   ```
 
+* Added new proof to `Data.List.Relation.Binary.Lex.Strict`:
+  ```agda
+  ≤-isDecPartialOrder : IsStrictTotalOrder _≈_ _≺_ → IsDecPartialOrder _≋_ _≤_
+  ≤-decPoset          : StrictTotalOrder a ℓ₁ ℓ₂ → DecPoset _ _ _
+  ```
+
+* Added new function to `Data.List.Relation.Binary.Prefix.Heterogeneous`:
+  ```agda
+  _++ᵖ_ : Prefix R as bs → ∀ suf → Prefix R as (bs ++ suf)
+  ```
+
+* Added new function to `Data.List.Relation.Binary.Suffix.Heterogeneous`:
+  ```agda
+  _++ˢ_ : ∀ pre → Suffix R as bs → Suffix R as (pre ++ bs)
+  ```
+
 * Added new function to `Data.Fin` (the inverse of `splitAt`:
   ```agda
   join : ∀ m n → Fin m ⊎ Fin n → Fin (m ℕ.+ n)

GenerateEverything.hs

@@ -73,6 +73,7 @@ withKModules = map modToFile
   , "Relation.Binary.PropositionalEquality.TrustMe"
   , "Text.Pretty.Core"
   , "Text.Pretty"
+  , "Text.Regex.String.Unsafe"
   ]
 
 isWithKModule :: FilePath -> Bool

README.agda

@@ -91,6 +91,9 @@ import README.Data
 -- • Tactic
 --     Tactics for automatic proof generation
 
+-- ∙ Text
+--     Format-based printing, Pretty-printing, and regular expressions
+
 
 ------------------------------------------------------------------------
 -- Library design
@@ -184,6 +187,29 @@ import Codata.Thunk
 
 import IO
 
+-- ∙ Text
+
+-- Explaining string formats and the behaviour of printf
+
+import README.Text.Printf
+
+-- Showcasing the pretty printing module
+
+import README.Text.Pretty
+
+-- Demonstrating the regular expression matching
+
+import README.Text.Regex
+
+-- Explaining how to display tables of strings:
+
+import README.Text.Tabular
+
+-- Explaining how to display a tree:
+
+import README.Text.Tree
+
+
 
 ------------------------------------------------------------------------
 -- More documentation
@@ -213,22 +239,6 @@ import README.Nary
 
 import README.Inspect
 
--- Explaining string formats and the behaviour of printf
-
-import README.Text.Printf
-
--- Showcasing the pretty printing module
-
-import README.Text.Pretty
-
--- Explaining how to display tables of strings:
-
-import README.Text.Tabular
-
--- Explaining how to display a tree:
-
-import README.Text.Tree
-
 -- Explaining how to use the automatic solvers
 
 import README.Tactic.MonoidSolver

README/Text/Regex.agda

@@ -0,0 +1,175 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Examples of regular expressions and matching
+------------------------------------------------------------------------
+
+{-# OPTIONS --with-K #-}
+
+module README.Text.Regex where
+
+open import Data.Bool using (true; false)
+open import Data.List using (_∷_; [])
+open import Data.String
+open import Function.Base using () renaming (_$′_ to _$_)
+open import Relation.Nullary using (yes)
+open import Relation.Nullary.Decidable using (True; False; from-yes)
+
+-- Our library available via the Text.Regex module is safe but it works on
+-- lists of characters.
+
+-- To use it on strings we have to rely on unsafe theorems about the
+-- conversions between strings and lists of characters being inverses.
+-- For convenience we use the following unsafe module for this README.
+open import Text.Regex.String.Unsafe
+
+------------------------------------------------------------------------
+-- Defining regular expressions
+
+-- The type of regular expressions is Exp.
+
+-- Some examples of regular expressions using:
+
+-- [_]        for the union of ranges it contains
+-- _─_        for a range
+-- singleton  for an exact character
+-- _∙_        for the concatenation of two regular expressions
+-- _∣_        for the sum of two regular expressions
+-- _⋆         for the Kleene star (zero or more matches of the regular expression)
+-- _⁇         for an optional regular expression
+
+ℕ* : Exp
+ℕ* = [ '1' ─ '9' ∷ [] ]   -- a non-zero digit
+   ∙ [ '0' ─ '9' ∷ [] ] ⋆ -- followed by zero or more digits
+
+ℕ : Exp
+ℕ = ℕ* ∣ singleton '0' -- ℕ* or exactly 0
+
+ℤ : Exp
+ℤ = ((singleton '-') ⁇ ∙ ℕ*) -- an optional minus sign followed by a ℕ*
+  ∣ singleton '0'            -- or exactly 0
+
+------------------------------------------------------------------------
+-- An expression's semantics
+
+-- The semantics of these regular expression is defined in terms of the
+-- lists of characters they match. The type (str ∈ e) states that the
+-- string str matches the expression e.
+
+-- It is decidable, and the proof is called _∈?_.
+-- We can run it on a few examples to check that it matches our intuition:
+
+-- Valid: starts with a non-zero digit, followed by 3 digits
+_ : True ("1848" ∈? ℕ*)
+_ = _
+
+-- Valid: exactly 0
+_ : True ("0" ∈? ℕ)
+_ = _
+
+-- Invalid: starts with a leading 0
+_ : False ("007" ∈? ℕ)
+_ = _
+
+-- Invalid: no negative ℕ number
+_ : False ("-666" ∈? ℕ)
+_ = _
+
+-- Valid: a negative integer
+_ : True ("-666" ∈? ℤ)
+_ = _
+
+-- Invalid: no negative 0
+_ : False ("-0" ∈? ℤ)
+_ = _
+
+------------------------------------------------------------------------
+-- Matching algorithms
+
+-- The proof that _∈_ is decidable gives us the ability to check whether
+-- a whole string matches a regular expression. But we may want to use
+-- other matching algorithms detecting a prefix, infix, or suffix of the
+-- input string that matches the regular expression.
+
+-- This is what the Regex type gives us.
+
+-- For instance, the following value corresponds to finding an infix
+-- substring matching the string "agda" or "agdai"
+
+agda : Exp
+agda = singleton 'a'
+     ∙ singleton 'g'
+     ∙ singleton 'd'
+     ∙ singleton 'a'
+     ∙ (singleton 'i' ⁇)
+
+infixAgda : Regex
+infixAgda = record
+  { fromStart  = false
+  ; tillEnd    = false
+  ; expression = agda
+  }
+
+-- The search function gives us the ability to look for matches
+
+-- Valid: agda in the middle
+_ : True (search "Maria Magdalena" infixAgda)
+_ = _
+
+-- By changing the value of fromStart and tillEnd we can control where the
+-- substring should be. We can insist on the match being at the end of the
+-- input for instance:
+
+suffixAgda : Regex
+suffixAgda = record
+  { fromStart  = false
+  ; tillEnd    = true
+  ; expression = agda
+  }
+
+-- Invalid: agda is in the middle
+_ : False (search "Maria Magdalena" suffixAgda)
+_ = _
+
+-- Valid: agda as a suffix
+_ : True (search "README.agda" suffixAgda)
+_ = _
+
+-- Valid: agdai as a suffix
+_ : True (search "README.agdai" suffixAgda)
+_ = _
+
+
+------------------------------------------------------------------------
+-- Advanced uses
+
+-- Search does not just return a boolean, it returns an informative answer.
+-- Infix matches are for instance represented using the `Infix` relation on
+-- list. Such a proof pinpoints the exact position of the match:
+
+open import Data.List.Relation.Binary.Infix.Heterogeneous
+open import Data.List.Relation.Binary.Infix.Heterogeneous.Properties
+open import Data.List.Relation.Binary.Pointwise using (≡⇒Pointwise-≡)
+open import Relation.Binary.PropositionalEquality
+
+-- Here is an example of a match: it gives back the substring, the inductive
+-- proof that it is accepted by the regular expression and its precise location
+-- inside the input string
+mariamAGDAlena : Match "Maria Magdalena" infixAgda
+mariamAGDAlena = record
+  { string  = "agda"                     -- we have found "agda"
+  ; match   = from-yes ("agda" ∈? agda)  -- a proof of the match
+  ; related = proof                      -- and its location
+  }
+
+  where
+
+    proof : Infix _≡_ (toList "agda") (toList "Maria Magdalena")
+    proof = toList "Maria M"
+        ++ⁱ fromPointwise (≡⇒Pointwise-≡ refl)
+        ⁱ++ toList "lena"
+
+
+-- And here is the proof that search returns such an object
+_ : search "Maria Magdalena" infixAgda ≡ yes mariamAGDAlena
+_ = refl

src/Data/List/Relation/Binary/Infix/Heterogeneous.agda

@@ -10,11 +10,11 @@ module Data.List.Relation.Binary.Infix.Heterogeneous where
 
 open import Level
 open import Relation.Binary using (REL; _⇒_)
-open import Data.List.Base as List using (List; []; _∷_)
+open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise)
 open import Data.List.Relation.Binary.Prefix.Heterogeneous
-  as Prefix using (Prefix; []; _∷_)
+  as Prefix using (Prefix; []; _∷_; _++ᵖ_)
 
 private
   variable
@@ -34,6 +34,16 @@ module _ {A : Set a} {B : Set b} (R : REL A B r) where
     MkView : ∀ pref {inf} → Pointwise R as inf → ∀ suff →
             View as (pref List.++ inf List.++ suff)
 
+infixr 5 _++ⁱ_ _ⁱ++_
+
+_++ⁱ_ : ∀ xs {as bs} → Infix R as bs → Infix R as (xs ++ bs)
+[]       ++ⁱ rs = rs
+(x ∷ xs) ++ⁱ rs = there (xs ++ⁱ rs)
+
+_ⁱ++_ : ∀ {as bs} → Infix R as bs → ∀ xs → Infix R as (bs ++ xs)
+here  rs ⁱ++ xs = here (rs ++ᵖ xs)
+there rs ⁱ++ xs = there (rs ⁱ++ xs)
+
 map : R ⇒ S → Infix R ⇒ Infix S
 map R⇒S (here pref) = here (Prefix.map R⇒S pref)
 map R⇒S (there inf) = there (map R⇒S inf)

src/Data/List/Relation/Binary/Lex/Strict.agda

@@ -196,6 +196,14 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
       }
       where open IsStrictPartialOrder spo
 
+    ≤-isDecPartialOrder : IsStrictTotalOrder _≈_ _≺_ →
+                          IsDecPartialOrder _≋_ _≤_
+    ≤-isDecPartialOrder sto = record
+      { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
+      ; _≟_            = Pointwise.decidable _≟_
+      ; _≤?_           = ≤-decidable _≟_ _<?_
+      } where open IsStrictTotalOrder sto
+
     ≤-isTotalOrder : IsStrictTotalOrder _≈_ _≺_ → IsTotalOrder _≋_ _≤_
     ≤-isTotalOrder sto = record
       { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
@@ -222,6 +230,13 @@ module _ {a ℓ₁ ℓ₂} {A : Set a} where
   { isPartialOrder = ≤-isPartialOrder isStrictPartialOrder
   } where open StrictPartialOrder spo
 
+≤-decPoset : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
+             DecPoset _ _ _
+≤-decPoset sto = record
+  { isDecPartialOrder = ≤-isDecPartialOrder isStrictTotalOrder
+  } where open StrictTotalOrder sto
+
+
 ≤-decTotalOrder : ∀ {a ℓ₁ ℓ₂} → StrictTotalOrder a ℓ₁ ℓ₂ →
                   DecTotalOrder _ _ _
 ≤-decTotalOrder sto = record

src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda

@@ -45,6 +45,10 @@ module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
 
 module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
 
+  _++ᵖ_ : ∀ {as bs} → Prefix R as bs → ∀ suf → Prefix R as (bs List.++ suf)
+  []       ++ᵖ suf = []
+  (r ∷ rs) ++ᵖ suf = r ∷ (rs ++ᵖ suf)
+
   toView : ∀ {as bs} → Prefix R as bs → PrefixView R as bs
   toView []       = [] ++ _
   toView (r ∷ rs) with toView rs

src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda

@@ -31,6 +31,10 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where
   tail (here (_ ∷ rs)) = there (here rs)
   tail (there x) = there (tail x)
 
+  _++ˢ_ : ∀ pre {as bs} → Suffix R as bs → Suffix R as (pre List.++ bs)
+  []       ++ˢ rs = rs
+  (x ∷ xs) ++ˢ rs = there (xs ++ˢ rs)
+
 module _ {a b r s} {A : Set a} {B : Set b} {R : REL A B r} {S : REL A B s} where
 
   map : R ⇒ S → Suffix R ⇒ Suffix S