adt-utils.rkt (12432B)
1 #lang at-exp racket 2 (provide (except-out (all-defined-out) 3 num-e* 4 num-τ* 5 List…τ* 6 Λc* 7 Λf*)) 8 9 @require["util.rkt" 10 (only-in scribble/base emph) 11 scriblib/render-cond 12 (for-label (only-meta-in 0 typed/racket))] 13 14 @(require racket/list 15 (for-syntax racket/base syntax/parse racket/list)) 16 @(begin-for-syntax 17 (define-syntax-class stringify 18 [pattern x:id #:when (identifier-binding #'x) 19 #:with →str #'x] 20 [pattern x:id #:with →str (datum->syntax #'x 21 (symbol->string (syntax-e #'x)) 22 #'x)] 23 [pattern e #:with →str #'e])) 24 @(define-for-syntax (defop* op) 25 (syntax-parser 26 [(_ :stringify ...) 27 #`@${(@(add-between (list @textbf{@#,op} 28 #,@(syntax->list #'(→str ...))) 29 "\\ "))}] 30 [self 31 (identifier? #'self) 32 #`@textbf{@#,op}])) 33 34 @(begin-for-syntax 35 (require (for-syntax racket/base)) 36 37 (define-syntax (defop stx) 38 (syntax-case stx () 39 [(_ op) 40 (with-syntax ([s (datum->syntax #'op 'syntax)]) 41 #'(defop* (s op)))])) 42 43 (define-syntax (defvop stx) 44 (syntax-case stx () 45 [(_ op) 46 (with-syntax ([s (datum->syntax #'op 47 `@${\mathord{@textbfit{@,#'op}}})]) 48 #'(defop s))]))) 49 50 @(define-syntax stringify 51 (syntax-parser 52 [(_ :stringify) 53 #'→str] 54 [(_ :stringify ...) 55 #'(add-between (list →str ...) "\\ ")])) 56 57 (define (spaces . l) 58 (add-between l "\\ ")) 59 60 (define-syntax ctorτ (defop "Ctor")) 61 (define-syntax ctorv (defvop "ctor")) 62 (define-syntax ctore (defop "ctor")) 63 (define κ @${κ}) 64 (define-syntax κof 65 (syntax-rules () 66 [(_ τ) @${@|κ|\ \mathbf{of}\ @(stringify τ)}] 67 [(_ i τ) @${@|κ|@(stringify i)\ \mathbf{of}\ @(stringify τ)}])) 68 (define-syntax κe 69 (syntax-rules () 70 [(_ e) @${@|κ|\ @(stringify e)}] 71 [(_ i e) @${@|κ|@(stringify i)\ @(stringify e)}])) 72 (define-syntax κv 73 (syntax-rules () 74 [(_ v) @${@|κ|\ @(stringify v)}] 75 [(_ i v) @${@|κ|@(stringify i)\ @(stringify v)}])) 76 (define ɐ @${a}) 77 (define-syntax ctorTop (defop "CtorTop")) 78 (define-syntax-rule (ctor-val κ) 79 @${\mathbf{getval}_@κ}) 80 (define-syntax recordτ (defop "Record")) 81 (define-syntax recordv (defvop "record")) 82 (define-syntax recorde (defop "record")) 83 (define-syntax variantτ (defop "V")) 84 (define-syntax ifop (defop "if")) 85 (define-syntax mapop (defop "map")) 86 (define-syntax-rule (λv (arg ...) expr) 87 @${@mathbfit{λ}(@(list (stringify arg) ...)).@(stringify expr)}) 88 (define-syntax-rule (λe (arg ...) expr) 89 @${\mathbf{λ}(@(spaces (stringify arg) ...)).@(stringify expr)}) 90 (define-syntax-rule (Λe (arg ...) expr) 91 @${\mathbf{Λ}(@(spaces (stringify arg) ...)).@(stringify expr)}) 92 (define-syntax-rule (Λv (arg ...) expr) 93 @${@mathbfit{Λ}(@(spaces (stringify arg) ...)).@(stringify expr)}) ;; TODO: is the env necessary here? It's a type env, right? 94 (define (repeated #:n [n #f] . l) 95 (if n 96 @${\overrightarrow{@l}\overset{\scriptscriptstyle\,\ifmathjax{\raise1mu{@|n|}}\iflatex{@|n|}}{\vphantom{@l}}} 97 @${\overrightarrow{@l}})) 98 (define (repeatset #:w [wide? #f] . l) 99 (define w (if wide? "\\!" "")) 100 ($ (cond-element 101 [html 102 @${\def\overrightbracedarrow#1{\overset{\scriptscriptstyle{\raise1mu{\{}}}{\vphantom{#1}}\overrightarrow{@|w|#1@|w|}\overset{\scriptscriptstyle{\raise1mu{\}}}}{\vphantom{#1}}}\overrightbracedarrow{@l}}] 103 [else 104 ;; Defined in util.rkt 105 @${\overrightbracedarrow{@|w|@|l|@|w|}}]))) 106 (define (repeatSet . l) 107 @${\{@(apply repeatset l)\}}) 108 (define |P| @${\ |\ }) 109 (define ρc @${ρ_{c}}) 110 (define ρf @${ϱ_{f}}) 111 (define ςc @${ς_{c}}) 112 (define ςf @${ς_{f}}) 113 (define-syntax at (defop "@")) 114 (define-syntax atc (defop (list "@" @${{}_{@textbf{c}}}))) 115 (define-syntax atf (defop (list "@" @${{}_{@textbf{f}}}))) 116 (define-syntax Λc* (defop (list "Λ" @${{}_{@textbf{c}}}))) 117 (define-syntax Λf* (defop (list "Λ" @${{}_{@textbf{f}}}))) 118 (define-syntax-rule (Λce (ρ ...) e) 119 (Λc* @${(@(add-between (list ρ ...) "\\ "))} e)) 120 (define-syntax-rule (Λcv (ρ ...) e) 121 (Λc* @${(@(add-between (list ρ ...) "\\ "))} e)) 122 (define-syntax-rule (Λfe (ρ ...) e) 123 (Λf* @${(@(add-between (list ρ ...) "\\ "))} e)) 124 (define-syntax-rule (Λfv (ρ ...) e) 125 (Λf* @${(@(add-between (list ρ ...) "\\ "))} e)) 126 (define-syntax ∀r* (defop @${@mathbm{∀}})) 127 (define-syntax-rule (∀r (α ...) τ) 128 (∀r* @${(@(add-between (list (stringify α) ...) "\\ "))} τ)) 129 (define-syntax ∀c* (defop @${@mathbm{∀}_{@textbf{c}}})) 130 (define-syntax ∀f* (defop @${@mathbm{∀}_{@textbf{f}}})) 131 (define-syntax-rule (∀c (ρ ...) τ) 132 (∀c* @${(@(add-between (list (stringify ρ) ...) "\\ "))} τ)) 133 (define-syntax-rule (∀f (ρ ...) τ) 134 (∀f* @${(@(add-between (list (stringify ρ) ...) "\\ "))} τ)) 135 (define-syntax-rule (ctor-pred c) 136 @${@(stringify c)@textbf{?}}) 137 (define-syntax record-gete 138 (syntax-rules () 139 [(_ e ɐ) @${@(stringify e).@(stringify ɐ)}] 140 [(_ ɐ) @${.@(stringify ɐ)}])) 141 (define-syntax-rule (record-pred . f*) 142 @${(@textbf{record?}\ @(stringify . f*))}) 143 (define-syntax-rule (record-pred* . f*) 144 @${(@textbf{record$\mathbf{*}$?}\ @(stringify . f*))});; TODO text vs math!!! 145 (define-syntax-rule (opwith rec a v) 146 @list{@(stringify rec) @textbf[" with "] @(stringify a) = @(stringify v)}) 147 (define-syntax-rule (opwithout rec a) 148 @list{@(stringify rec) @textbf[" without "] @(stringify a)}) 149 (define pe @${\mathit{pe}}) 150 (define πctor-val @${@textbf{getval}}) 151 (define (πɐ . ɐ) @${\mathbf{@ɐ}}) 152 ;; Associates a variable name or record field name with a value, type or 153 ;; evaluation context. 154 (define-syntax-rule (↦v name val) 155 @${@(stringify name)↦@(stringify val)}) 156 (define-syntax-rule (↦e name val) @${@(stringify name)↦@(stringify val)}) 157 (define-syntax-rule (↦E name val) @${@(stringify name)↦@(stringify val)}) 158 (define-syntax-rule (↦τ name val) @${@(stringify name)↦@(stringify val)}) 159 (define-syntax-rule (app f+args ...) 160 @${\mathbf{(}@(add-between (list (stringify f+args) ...) "\\ ")\mathbf{)}}) 161 162 (define-syntax num-e* (defop "num")) 163 (define-syntax num-v* (defvop "num")) 164 (define-syntax num-τ* (defop "Num")) 165 (define num-e @num-e*[n]) 166 (define num-v @num-v*[n]) 167 (define-syntax num-τ 168 (syntax-parser 169 [(_ n) #'@num-τ*[n]] 170 [self:id #'@num-τ*[n]])) ;; n by default 171 172 (define-syntax null-v (defvop "null")) 173 (define-syntax null-e (defop "null")) 174 (define-syntax null-τ (defop "Null")) 175 176 (define-syntax true-e (defop "true")) 177 (define-syntax true-v (defvop "true")) 178 (define-syntax true-τ (defop "True")) 179 180 (define-syntax false-e (defop "false")) 181 (define-syntax false-v (defvop "false")) 182 (define-syntax false-τ (defop "False")) 183 184 (define-syntax un (defop "∪")) 185 (define-syntax ∩τ (defop "∩")) 186 187 (define-syntax-rule (f→ (from ...) R) 188 @${(@(add-between (list @(stringify from) ...) "\\ ")\ @mathbm{→}\ @(stringify R))}) 189 (define-syntax-rule (f* (from ... rest*) R) 190 (f→ (from ... @${\ @mathbm{.}\ } @${@(stringify rest*)@mathbm{*}}) R)) 191 (define-syntax-rule (f… (from ... polydot) R) 192 (f→ (from ... @${\ @mathbm{.}\ } polydot) R)) 193 (define-syntax (R stx) 194 (syntax-case stx () 195 [(_ to φ⁺ φ⁻ o) 196 #'@${@mathbm{❲}@(stringify to) 197 \;@mathbm{;}\; @(stringify φ⁺) @mathbm{{/}} @(stringify φ⁻) 198 \;@mathbm{;}\; @(stringify o)@mathbm{❳}}] 199 [self (identifier? #'self) 200 #'@${\mathrm{R}}])) 201 202 (define primop "p") 203 204 (define-syntax (consp stx) 205 (syntax-case stx () 206 [(_ a b) #'@${(\mathit{cons}\ @(stringify a)\ @(stringify b)}] 207 [self (identifier? #'self) #'@${\mathit{cons}}])) ;; cons primop 208 (define-syntax-rule (consv a b) @${⟨@(stringify a), @(stringify b)⟩}) 209 (define-syntax listv (defvop "list")) 210 (define-syntax-rule (consτ a b) 211 @${❬@(stringify a)@mathbm{,} @(stringify b)❭}) 212 (define-syntax-rule (polydot τ α) 213 @${@(stringify τ) \mathbf{…}_{@(stringify α)}}) 214 (define-syntax-rule (polydotα α) 215 @${@(stringify α) \mathbf{…}}) 216 (define-syntax List…τ* (defop "List")) 217 (define-syntax-rule (List…τ τ α) 218 @List…τ*[@polydot[τ α]]) 219 (define-syntax Listτ (defop "List")) 220 (define-syntax Listofτ (defop "Listof")) 221 @;(define-syntax →Values (defop "Values")) 222 (define-syntax-rule (→Values v ...) (spaces (stringify v) ...)) 223 (define @emptypath @${ϵ}) 224 (define-syntax-rule (<: a b) 225 @${⊢ @(stringify a) \mathrel{≤:} @(stringify b)}) 226 @define[<:*]{@${{\mathrel{≤:}}}} 227 (define-syntax-rule (=: a b) 228 @${⊢ @(stringify a) \mathrel{=:} @(stringify b)}) 229 (define-syntax-rule (≠: a b) 230 @${⊢ @(stringify a) \mathrel{≠:} @(stringify b)}) 231 (define-syntax-rule (=:def a b) 232 @${@(stringify a) \mathrel{≝} @(stringify b)}) 233 234 (define-syntax-rule (<:R a b) 235 @${⊢ @(stringify a) \mathrel{{≤:}_R} @(stringify b)}) 236 237 @(define-syntax Γ 238 (syntax-parser 239 #:literals (+) #:datum-literals (⊢ Δ) 240 [(_ {~and {~not +} more} ... 241 {~optional {~seq + φ}} 242 {~optional {~seq Δ Δ∪ ...}} 243 ⊢ x τ φ⁺ φ⁻ o) 244 (raise-syntax-error 'Γ "Use of the old gamma syntax" this-syntax)] 245 [(_ {~and {~not +} {~not Δ} more} ... 246 {~optional {~seq + φ}} 247 {~optional {~seq Δ Δ∪ ...}} 248 ⊢ x R) 249 #`@${@(add-between (list "Γ" (stringify more) ...) ", ") 250 ; 251 @(add-between (list "Δ" @#,@(if (attribute Δ∪) 252 #'{(stringify Δ∪) ...} 253 #'{})) 254 "∪") 255 @#,@(if (attribute φ) @list{+ @#'(stringify φ)} @list{}) ⊢ 256 @(stringify x) : @(stringify R)}])) 257 @(define-syntax subst 258 (syntax-parser 259 [(_ {~seq from {~literal ↦} to} ... 260 (~and {~seq repeated ...} 261 {~seq {~optional ({~literal repeated} . _)}})) 262 #'@$["[" (add-between (list (list (stringify from) "↦" (stringify to)) 263 ... 264 repeated 265 ...) 266 "\\ ") "]"]])) 267 @(define-syntax substφo 268 (syntax-parser 269 [(_ from {~literal ↦} to) 270 #'@$["{|}_{{" (stringify from) "}↦{" (stringify to) "}}"]])) 271 272 (define update @${\operatorname{update}}) 273 (define applyfilter @${\operatorname{applyfilter}}) 274 (define combinefilter @${\operatorname{combinefilter}}) 275 (define no-overlap @${\operatorname{no-overlap}}) 276 (define restrict @${\operatorname{restrict}}) 277 (define remove @${\operatorname{remove}}) 278 (define simplify* @${\operatorname{simplify}}) 279 (define-syntax-rule (simplify τ) @${@simplify*(@(stringify τ))}) 280 (define propagate⊥ @${\operatorname{propagate_⊥}}) 281 (define loc @${\mathit{loc}}) 282 (define (! . rest) @${\overline{@rest}}) 283 (define metatrue @${\mathrm{true}}) 284 (define metafalse @${\mathrm{false}}) 285 286 (define carπ @${\mathrm{car}}) 287 (define cdrπ @${\mathrm{cdr}}) 288 (define forceπ @${\mathrm{force}}) 289 (define Numberτ @${\mathbf{Number}}) 290 (define-syntax promisee (defop "delay")) 291 (define-syntax forcee (defop "force")) 292 (define-syntax promiseτ (defop "Promise")) 293 (define-syntax promisev (defvop "promise")) 294 (define-syntax syme (defop "symbol")) 295 (define-syntax symτ (defop "Symbol")) 296 (define-syntax symv (defvop "symbol")) 297 (define Symbolτ @${\mathbf{Symbol}}) 298 (define-syntax gensyme (defop "gensym")) 299 (define-syntax eq?op (defop "eq?")) 300 (define sym* @${s′}) 301 (define 𝒮* @${𝒮′}) 302 (define-syntax recτ* (defop "Rec")) 303 (define-syntax-rule (recτ r τ) (recτ* r τ)) 304 (define Booleanτ @${\mathbf{Boolean}}) 305 (define (transdots a b c) @${\mathit{td_τ}(@a,\ @b,\ @c)}) 306 (define (substdots a b c d) @${\mathit{sd}(@a,\ @b,\ @c,\ @d)}) 307 (define object @emph{object}) 308 (define Objects @emph{Objects}) 309 (define (elim a b) @${\mathit{elim}(@a,\ @b)}) 310 (define-syntax-rule (<:elim r a b) 311 @${⊢ @(stringify a) 312 \mathrel{{≤:}_{\mathrm{elim}\ @(stringify r)}} 313 @(stringify b)}) 314 315 (define-syntax include-equation 316 (syntax-rules () 317 [(_ filename) 318 (let () 319 (local-require (only-in (submod filename equations) [equations tmp])) 320 tmp)] 321 [(_ filename eq) 322 (let () 323 (local-require (only-in filename [eq tmp])) 324 tmp)])) 325 326 (define δe @${δ_{\mathrm{e}}}) 327 (define alldifferent @${\operatorname{AllDifferent}}) 328 (define disjoint-sets @${\operatorname{DisjointSets}})