-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathex-regexp.scm
147 lines (136 loc) · 4.1 KB
/
ex-regexp.scm
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
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
;; inspired by https://github.com/webyrd/relational-parsing-with-derivatives
(define regexp-NULL #f) ; -- the empty set
(define regexp-BLANK #t) ; -- the empty string
(define (valid-seqo exp)
(fresh (pat1 pat2)
(== `(seq ,pat1 ,pat2) exp)
(=/= regexp-NULL pat1)
(=/= regexp-BLANK pat1)
(=/= regexp-NULL pat2)
(=/= regexp-BLANK pat2)))
(define (seqo pat1 pat2 out)
(conde
[(== regexp-NULL pat1) (== regexp-NULL out)]
[(== regexp-NULL pat2) (== regexp-NULL out) (=/= regexp-NULL pat1)]
[(== regexp-BLANK pat1) (== pat2 out) (=/= regexp-NULL pat2)]
[(== regexp-BLANK pat2) (== pat1 out) (=/= regexp-NULL pat1) (=/= regexp-BLANK pat1)]
[(=/= regexp-NULL pat1) (=/= regexp-BLANK pat1) (=/= regexp-NULL pat2) (=/= regexp-BLANK pat2) (== `(seq ,pat1 ,pat2) out)]))
(define (valid-alto exp)
(fresh (pat1 pat2)
(== `(alt ,pat1 ,pat2) exp)
(=/= regexp-NULL pat1)
(=/= regexp-NULL pat2)
(=/= pat1 pat2)))
(define (alto pat1 pat2 out)
(conde
[(== pat1 pat2) (== pat1 out)]
[(=/= pat1 pat2)
(conde
[(== regexp-NULL pat1) (== pat2 out)]
[(== regexp-NULL pat2) (== pat1 out) (=/= regexp-NULL pat1)]
[(=/= regexp-NULL pat1) (=/= regexp-NULL pat2) (== `(alt ,pat1 ,pat2) out)])]))
(define (valid-repo exp)
(fresh (pat)
(== `(rep ,pat) exp)
(=/= regexp-BLANK pat)
(=/= regexp-NULL pat)
(fresh (re1 re2)
(conde
((symbolo pat))
((== `(seq ,re1 ,re2) pat))
((== `(alt ,re1 ,re2) pat))))))
(define (repo pat out)
(conde
[(== regexp-BLANK out)
(conde
[(== regexp-NULL pat)]
[(== regexp-BLANK pat)])]
[(conde
((symbolo pat) (== `(rep ,pat) out))
((fresh (re1 re2)
(conde
((== `(rep ,re1) pat)
; remove nested reps
(== pat out))
((== `(seq ,re1 ,re2) pat)
(== `(rep ,pat) out))
((== `(alt ,re1 ,re2) pat)
(== `(rep ,pat) out))))))]))
(define-rel
(regexp-matcho pattern data out)
((regexp-matcho-clause regexp-matcho deltao derivo))
()
(conde
((== '() data) (deltao pattern out))
((fresh (a d res)
(== (cons a d) data)
(derivo pattern a res)
(regexp-matcho res d out)))))
(define-rel
(deltao re out)
((deltao-clause deltao))
()
(conde
[(== regexp-BLANK re) (== #t out)]
[(== regexp-NULL re) (== #f out)]
[(symbolo re) (== #f out)]
[(fresh (re1)
(== `(rep ,re1) re)
(== #t out)
(valid-repo re))]
[(fresh (re1 re2 res1 res2)
(== `(seq ,re1 ,re2) re)
(valid-seqo re)
(conde
((== #f res1) (== #f out))
((== #t res1) (== #f res2) (== #f out))
((== #t res1) (== #t res2) (== #t out)))
(deltao re1 res1)
(deltao re2 res2))]
[(fresh (re1 re2 res1 res2)
(== `(alt ,re1 ,re2) re)
(valid-alto re)
(conde
((== #t res1) (== #t out))
((== #f res1) (== #t res2) (== #t out))
((== #f res1) (== #f res2) (== #f out)))
(deltao re1 res1)
(deltao re2 res2))]))
(define-rel
(derivo re c out)
((derivo-clause derivo deltao))
()
(fresh ()
(symbolo c)
(conde
[(== regexp-BLANK re) (== regexp-NULL out)]
[(== regexp-NULL re) (== regexp-NULL out)]
[(symbolo re)
(conde
[(== c re) (== regexp-BLANK out)]
[(=/= c re) (== regexp-NULL out)])]
[(fresh (re1 res1)
(== `(rep ,re1) re)
(valid-repo re)
(seqo res1 re out)
(derivo re1 c res1))]
[(fresh (re1 re2 res1 res2)
(== `(alt ,re1 ,re2) re)
(valid-alto re)
(derivo re1 c res1)
(derivo re2 c res2)
(alto res1 res2 out))]
[(fresh (re1 re2 res1 res2 res3 res4 res5)
(== `(seq ,re1 ,re2) re)
(valid-seqo re)
(derivo re1 c res1)
(deltao re1 res3)
(derivo re2 c res4)
(seqo res1 re2 res2)
(seqo res3 res4 res5)
(alto res2 res5 out))])))
(define (regexp-clause a b)
(conde
((deltao-clause a b))
((derivo-clause a b))
((regexp-matcho-clause a b))))