1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
{-# OPTIONS --guardedness #-}
module Main where
open import Data.Bool.Base using (true; false)
open import Data.List.Base using (_∷_; [])
open import Data.List.Relation.Binary.Infix.Heterogeneous using (toView; MkView)
open import Data.String using (String; toList; fromList; lines; concat)
open import IO
open import Function.Base using (_$_; case_of_)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary
open import Text.Regex.String
show : ∀ e {xs} → Dec (Match (Span e _≡_) xs (Regex.expression e)) → String
show _ (no _) = "No match found"
show e (yes match) = case toView (toInfix e (match .Match.related)) of λ where
(MkView pref x suff) → concat
$ "Match found: "
∷ fromList pref
∷ "["
∷ fromList (match .Match.list)
∷ "]"
∷ fromList suff
∷ []
agdaFile : Exp
agdaFile = [ 'a' ─ 'z' ∷ 'A' ─ 'Z' ∷ [] ] +
∙ singleton '.'
∙ singleton 'a'
∙ singleton 'g'
∙ singleton 'd'
∙ singleton 'a'
buildDir : Exp
buildDir = singleton '_'
∙ ([ 'a' ─ 'z' ∷ 'A' ─ 'Z' ∷ [] ] + ∙ singleton '/') +
regex : Regex
regex .Regex.fromStart = false
regex .Regex.tillEnd = false
regex .Regex.expression
= agdaFile ∣ buildDir
main : Main
main = run $ do
text ← readFiniteFile "run"
List.forM′ (lines text) $ λ l →
putStrLn (show regex $ search (toList l) regex)
|
