staged-miniKanren/tests/applications/grammars.rkt at main · namin/staged-miniKanren · GitHub

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
148
149
150
151
152
153
154
155
#lang racket

(require "../../main.rkt"
         "../../test-check.rkt")

(provide get-timing-data)

#|
Grammar syntax:
- (or A B C) is disjunction
- (seq A B C) is sequencing
- (quote A) (where A is a symbol) refers to nonterminal named A
- A (where A is a symbol/number) refers to the terminal written 'A'
|#

(define E-grammar
  '((E . (or 'S (seq 'S * 'S)))
    (S . (or 'T (seq 'T + 'T)))
    (T . (or 0 (seq < 'E >)))))

(defrel/staged (lookupo map key res)
  (fresh (first rest)
    (== map (cons first rest))
    (conde
     [(== first `(,key . ,res))]
     [(lookupo rest key res)])))

(defrel/staged (appendo xs ys res)
  (conde
   [(== xs '()) (== ys res)]
   [(fresh (a d resp)
      (== xs (cons a d))
      (appendo d ys resp)
      (== res (cons a resp)))]))

#|
This is the version I'd like to write - I have two staging-time parameters,
the grammar and the expression I'm interpreting. The one run-time parameter,
then, is true only of strings which fit the given expression within the given grammar.

It works fine normally, but staging it doesn't terminate. We'd like to use the
recursive parameter, but we can't, as the relation is already specialized on the
expression to be evalued.

(defrel-partial/staged (interp-grammar rel [grammar expr] [res])
  (conde
   [(conde [(symbolo expr)] [(numbero expr)])
    (later (== res (list expr)))]
   [(fresh (first rest c1 c2)
      (== expr `(or ,first . ,rest))
      (specialize-partial-apply c1 interp-grammar grammar first)
      (specialize-partial-apply c2 interp-grammar grammar `(or . ,rest))
      (later
       (conde
        [(finish-apply c1 interp-grammar res)]
        [(finish-apply c2 interp-grammar res)])))]
   [(== expr '(seq))
    (later (== res '()))]
   [(fresh (first rest c1 c2)
      (== expr `(seq ,first . ,rest))
      (specialize-partial-apply c1 interp-grammar grammar first)
      (specialize-partial-apply c2 interp-grammar grammar `(seq . ,rest))
      (later
       (fresh (a d)
         (finish-apply c1 interp-grammar a)
         (finish-apply c2 interp-grammar d)
         (appendo a d res))))]
   [(fresh (nt ref c)
      (== expr `(quote ,nt))
      (lookupo grammar nt ref)
      (specialize-partial-apply c interp-grammar grammar ref)
      (later
       (finish-apply c interp-grammar res)))]))

(defrel/staged (interp-E res)
  (fresh (c)
    (specialize-partial-apply c interp-grammar grammar ''E)
    (later (finish-apply c interp-grammar res))))
|#

(defrel-partial/staged (interp-grammar rel [grammar] [nt res])
  (gather
   (fresh (expr)
     (lookupo grammar nt expr)
     (interp-rhs rel expr res))))

(defrel/staged (interp-rhs recur expr res)
  (conde
   [(conde [(symbolo expr)] [(numbero expr)])
    (== res (list expr))]
   [(fresh (first rest)
      (== expr `(or ,first . ,rest))
      (conde
       [(interp-rhs recur first res)]
       [(interp-rhs recur `(or . ,rest) res)]))]
   [(== expr '(seq))
    (== res '())]
   [(fresh (first rest c1 c2 c3)
      (== expr `(seq ,first . ,rest))
      (interp-rhs recur first c1)
      (interp-rhs recur `(seq . ,rest) c2)
      (later (appendo c1 c2 res)))]
   [(fresh (nt)
      (== expr `(quote ,nt))
      (later (finish-apply recur interp-grammar nt res)))]))

(defrel/staged (recognizeo grammar nt str)
  (fresh (rel)
    (specialize-partial-apply rel interp-grammar grammar)
    (later (finish-apply rel interp-grammar nt str))))

(defrel/staged (recognize-Eo str)
  (recognizeo E-grammar 'E str))

(parameterize ([*test-result-same?* set=?])
  (test (run 4 (q r s)
          (recognize-Eo `(< 0 ,q ,r ,s)))
        '((+ 0 >) (> + 0) (* 0 >) (> * 0)))
  (test (run 4 (q r s)
          (staged (recognize-Eo `(< 0 ,q ,r ,s))))
        '((+ 0 >) (> + 0) (* 0 >) (> * 0)))
  (pretty-print (generated-code)))

(record-bench 'simple 'staging 'grammar-synthesis)
(defrel (interp-E-staged r)
  (time-staged (recognize-Eo r)))

(let ((size 200))
  (record-bench 'simple 'unstaged 'grammar-synthesis #:description "Find 200 strings that match a given grammar as in \\cref{sec:parser}")
  (time
   (run size (str)
     (recognize-Eo str)))

  (record-bench 'simple 'staged 'grammar-synthesis)
  (time
   (run size (str)
     (interp-E-staged str))))

(define (get-timing-data size)
  (define-values (ures ucpu ureal ugc)
    (time-apply
     (lambda ()
       (run size (r)
         (recognize-Eo r)))
     '()))
  (define-values (sres scpu sreal sgc)
    (time-apply
     (lambda ()
       (run size (r)
         (staged (recognize-Eo r))))
     '()))
  (list ureal sreal))

(require plot)
(plot-new-window? #t)