-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathassertions.rkt
154 lines (138 loc) · 6.99 KB
/
assertions.rkt
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
#lang racket
(require "common.rkt" "dom.rkt" "selectors.rkt" "encode.rkt" "smt.rkt" "spec/utils.rkt")
(provide compile-assertion auxiliary-definitions assertion-helpers helper-dict)
(define auxiliary-definitions (make-parameter '()))
(define auxiliary-defs (make-hash))
;; The strange duplication of `helper-dict` and `assertion-helpers` is
;; temporary, waiting on a better way to define optional or variary
;; arguments in `define` blocks. The main issue is that
;; `assertion-helpers` contains functions, and thus can't easily be
;; shipped to a different thread, while `helper-dict` has no optional
;; argument mechanism.
(define helper-dict (make-hash))
(define assertion-helpers
(make-hash
`((descends . ,(λ (b . sels) `(!= (ancestor ,b (matches ? ,@sels)) null)))
(is-interactive . ,(λ (b) `(matches ,b (tag a) (tag input) (tag button))))
(viewable . ,(λ (b) `(and (> (right ,b) (left root)) (> (bottom ,b) (top root)))))
(onscreen . ,(λ (b) `(and (>= (top ,b) 0) (>= (left ,b) 0) )))
(!= . ,(λ (a b) `(not (= ,a ,b))))
(width . ,(λ (b [dir 'border]) `(- (right ,b ,dir) (left ,b ,dir))))
(height . ,(λ (b [dir 'border]) `(- (bottom ,b ,dir) (top ,b ,dir))))
(no-floats-enter . ,(λ (b) `(let ([b ,b]) (raw (ez.outside (ez.in b) b)))))
(no-floats-exit . ,(λ (b) `(let ([b ,b]) (raw (ez.inside (ez.out b) b)))))
(no-floats-exit* . ,(λ (b) `(let ([b ,b]) (raw (ez.inside* (ez.out b) b)))))
(float-flow-in . ,(λ (b1 b2) `(raw (and (= (ez.in ,b1) (ez.in ,b2)) (<= (top-border ,b1) (top-border ,b2))))))
(float-flow-out . ,(λ (b1 b2) `(raw (and (= (ez.out ,b2) (ez.out ,b1)) (<= (bottom-border ,b1) (bottom-border ,b2))))))
(float-flow-across . ,(λ bs (apply smt-and
(for/list ([b bs] [b* (cdr bs)])
`(raw (and (= (ez.out ,b) (ez.in ,b*))
(<= (bottom-border ,b) (top-border ,b*))))))))
(float-flow-skip . ,(λ (b) `(raw (= (ez.out ,b) (ez.in ,b)))))
(floats-tracked . ,(λ (b) `(raw (- ez.registers (ez.free-registers (ez.in ,b))))))
(non-negative-margins . ,(λ (b) `(let ([b ,b]) (raw (non-negative-margins b)))))
(luminance . ,(λ (color) `(let ([color ,color]) (raw (lum (color.rgb color))))))
(overlaps . ,(λ (b1 b2) `(let ([b1 ,b1] [b2 ,b2]) (raw (overlaps b1 b2)))))
(within . ,(λ (b1 b2) `(let ([b1 ,b1] [b2 ,b2]) (raw (within-outer b1 b2))))))))
(define (compile-assertion doms body ctx)
(match-define (list dom) doms)
(let loop ([expr body] [ctx ctx])
(match expr
;; Booleans
[(or 'true 'false) expr]
[`(and ,parts ...) `(and ,@(map (curryr loop ctx) parts))]
[`(or ,parts ...) `(or ,@(map (curryr loop ctx) parts))]
[`(,(or '=> '=>*) ,as ... ,b)
`(=> ,@(map (curryr loop ctx) as) ,(loop b ctx))]
[`(not ,part) `(not ,(loop part ctx))]
;; Real numbers
[(? number?) expr]
[(list (and (or '= '< '> '<= '>=) op) parts ...)
(cons op (map (curryr loop ctx) parts))]
[(list (and (or '+ '- '* '/) op) parts ...)
(cons op (map (curryr loop ctx) parts))]
[`(max ,a ,b)
`(max ,(loop a ctx) ,(loop b ctx))]
;; Boxes
['null 'no-box]
[(list (and (or 'parent 'next 'prev 'first 'last) field) box)
(define function
(match field ['parent 'pflow] ['next 'nflow] ['prev 'vflow] ['first 'fflow] ['last 'lflow]))
`(,function ,(loop box ctx))]
[`(ancestor ,box ,cond*)
(define cond (loop cond* #hash((? . b))))
(define id (hash-ref! auxiliary-defs cond (hash-count auxiliary-defs)))
(define fun-name (sformat "aux~a" id))
(define aux-def
`((declare-fun ,fun-name (Box) Box)
(assert (forall ((b Box)) (= (,fun-name b) (ite ,cond b (,fun-name (pflow b))))))
(assert (= (,fun-name no-box) no-box))))
(auxiliary-definitions (remove-duplicates (append (auxiliary-definitions) aux-def)))
`(,fun-name ,(loop box ctx))]
[`(has-contents ,box) `(has-contents ,(loop box ctx))]
[`(is-component ,box) `(is-component ,(loop box ctx))]
[`(has-type ,box ,(and (or 'root 'text 'inline 'block 'line) boxtype))
(define function (sformat "is-box/~a" boxtype))
`(,function (type ,(loop box ctx)))]
[(list-rest (and (or 'top 'right 'bottom 'left) dir) box edge*)
(define edge
(match edge* [(list edge) edge] [(list) 'border]))
(define adjustment
(match dir [(or 'top 'bottom) 'yo] [(or 'left 'right) 'xo]))
(define function (sformat "~a-~a" dir edge))
`(+ (,function ,(loop box ctx)) (,adjustment ,(loop box ctx)))]
[`(text-height ,box)
`(let ([b ,(loop box ctx)]) (height-text b))]
;; Colors
[`(fg ,box) `(fg-color ,(loop box ctx))]
[`(bg ,box) `(bg-color ,(loop box ctx))]
['transparent 'color/transparent]
[`(color ,name) (sformat "color/~a" name)]
[`(rgb ,(? number? r) ,(? number? g) ,(? number? b))
(dump-value (list 'rgb r g b))]
[(list (and (or 'r 'g 'b) component) `(gamma ,color))
(define function (sformat "color.~a-corr" component))
`(,function (color.rgb ,(loop color ctx)))]
[(list (and (or 'r 'g 'b) component) color)
(define function (sformat "color.~a" component))
`(,function (color.rgb ,(loop color ctx)))]
;; Elements
[`(anonymous? ,b)
(define b* (loop b ctx))
(apply smt-or
(for*/list ([dom doms] [box (in-boxes dom)]
#:unless (dom-box->elt dom box))
`(= ,b* ,(dump-box box))))]
[`(matches ,b ,sels ...)
(define b* (loop b ctx))
(apply smt-or
(for*/list ([dom doms] [box (in-boxes dom)])
(define elt (dom-box->elt dom box))
(if (and elt (ormap (curryr selector-matches? elt) sels))
`(= ,b* ,(dump-box box))
'false)))]
;; Extra syntax
[`(if ,c ,t ,f)
`(if ,(loop c ctx) ,(loop t ctx) ,(loop f ctx))]
[`(let ([,vars ,vals] ...) ,body)
(define vals* (for/list ([val vals]) (loop val ctx)))
(define ctx*
(for/fold ([ctx ctx]) ([var vars])
(dict-set ctx var var)))
`(let (,@(map list vars vals*)) ,(loop body ctx*))]
;; Expandable
[(list (? (curry dict-has-key? assertion-helpers) fname) args ...)
(loop (apply (dict-ref assertion-helpers fname) args) ctx)]
[`(luminance ,color)
`(lum (color.rgb ,(loop color ctx)))]
[`(overlaps ,b1 ,b2)
`(overlaps ,(loop b1 ctx) ,(loop b2 ctx))]
[`(within ,b1 ,b2)
`(within-outer ,(loop b1 ctx) ,(loop b2 ctx))]
[`(raw ,expr)
`(let (,@(for/list ([(var expr) (in-dict ctx)]) (list var expr)))
,expr)]
;; Variables
[(? symbol?)
(with-handlers ([exn:fail:contract? (λ (e) (raise-user-error 'visual-logic "Could not find ~a (context includes ~a)\n\t~a\n" expr (dict-keys ctx) body))])
(dict-ref ctx expr))])))