phi-psi-o-path.rkt (1304B)
1 #lang at-exp s-exp phc-thesis/scribblings/equations-lang 2 3 @; This file is NOT under the CC0 license, as it contains rules and definitions 4 @; copied with permission from Sam Tobin-Hochstadt's Ph.D thesis. I obtained the 5 @; permission to copy these rules, but did not ask for a relicensing under the 6 @; CC0 license. 7 8 #:φ 9 10 @cases[@${φ} #:first-sep "⩴" @acase{@repeatset{ψ}@tag*{filter set}}] 11 12 #:ψ 13 14 @cases["ψ" #:first-sep "⩴" 15 @acase{τ_{π(@loc)} 16 @tag*{@${(v = \mathbf{?}) ⇒ π(@loc)@text{ is of type @${τ}}}}} 17 @acase{@!{τ}_{π(@loc)} 18 @tag*{@${(v = \mathbf{?}) ⇒ π(@loc)@text{ is not of type @${τ}}}}} 19 @acase{⊥@tag*{contradiction}}] 20 21 #:loc 22 23 @cases[@loc #:first-sep "⩴" 24 @acase{•@tag*{first argument of the function}} 25 @acase{x@tag*{variable}}] 26 27 #:o 28 29 @cases[@textrm{o} #:first-sep "⩴" 30 @acase{π(@loc)@tag*{@${e} is an alias for @${π(@loc)}}} 31 @acase{∅@tag*{no aliasing information}}] 32 33 #:π 34 35 @cases[@textit{π} #:first-sep "⩴" 36 @acase{pe∷π@tag*{path concatenation}} 37 @acase{@emptypath @tag*{empty path}}] 38 39 #:pe 40 41 @cases[@textit{pe} #:first-sep "⩴" 42 @acase{@carπ @tag*{first element of pair}} 43 @acase{@cdrπ @tag*{second element of pair}} 44 @acase{@forceπ @tag*{result of a promise}}]