|
141
|
1 module lang-text where
|
|
|
2
|
|
|
3 open import Data.List
|
|
|
4 open import Data.String
|
|
|
5 open import Data.Char
|
|
405
|
6 -- open import Data.Char.Unsafe
|
|
141
|
7 open import Relation.Binary.PropositionalEquality
|
|
|
8 open import Relation.Nullary
|
|
|
9 open import logic
|
|
|
10
|
|
|
11 split : {Σ : Set} → (List Σ → Bool)
|
|
|
12 → ( List Σ → Bool) → List Σ → Bool
|
|
|
13 split x y [] = x [] /\ y []
|
|
|
14 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
|
15 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
16
|
|
|
17 contains : String → String → Bool
|
|
|
18 contains x y = contains1 (toList x ) ( toList y ) where
|
|
|
19 contains1 : List Char → List Char → Bool
|
|
|
20 contains1 [] [] = false
|
|
|
21 contains1 [] ( cx ∷ ly ) = false
|
|
|
22 contains1 (cx ∷ lx) [] = true
|
|
|
23 contains1 (cx ∷ lx ) ( cy ∷ ly ) with cx ≟ cy
|
|
|
24 ... | yes refl = contains1 lx ly
|
|
|
25 ... | no n = false
|
|
|
26
|
|
|
27 -- w does not contain the substring ab
|
|
|
28 ex15a : Set
|
|
|
29 ex15a = (w : String ) → ¬ (contains w "ab" ≡ true )
|
|
|
30
|
|
|
31 -- w does not contains substring baba
|
|
|
32 ex15b : Set
|
|
|
33 ex15b = (w : String ) → ¬ (contains w "baba" ≡ true )
|
|
|
34
|
|
|
35 -- w contains neither the substing ab nor ba
|
|
|
36 ex15c : Set
|
|
|
37
|
|
|
38 -- w is any string not in a*b*
|
|
405
|
39 ex15c = (w : String ) → ( ¬ (contains w "ab" ≡ true )) /\ ( ¬ (contains w "ba" ≡ true ) )
|
|
141
|
40
|
|
405
|
41 ex15d : ?
|
|
|
42 ex15d = ?
|
|
141
|
43
|
|
405
|
44 ex15e : ?
|
|
|
45 ex15e = ?
|
|
141
|
46
|
|
405
|
47 ex15f : ?
|
|
|
48 ex15f = ?
|
|
141
|
49
|
|
405
|
50 ex15g : ?
|
|
|
51 ex15g = ?
|
|
141
|
52
|
|
405
|
53 ex15h : ?
|
|
|
54 ex15h = ?
|
