simplify.rkt (2471B)
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 #:Simplify1 9 10 @$${ 11 \begin{aligned} 12 @simplify[@∩τ[τ τ′ @repeatset{τ″}]] 13 &= @simplify[@∩τ[@∩τ[τ τ′] @repeatset{τ″}]] \\ 14 @simplify[@∩τ[@un[@repeatset{τ}] @repeatset{σ}]] 15 &= @propagate⊥(@un[@repeatset{@simplify[@∩τ[τ @repeatset{σ}]]}])\\ 16 @simplify[@∩τ[@consτ[τ τ′] @consτ[σ σ′]]] 17 &= @${@propagate⊥(@(consτ @simplify[@∩τ[τ σ]] 18 @simplify[@∩τ[τ′ σ′]]))}\\ 19 @simplify[@∩τ[@repeatset{σ}]] 20 &= \begin{cases} 21 ⊥ & \hspace{-1.5em}@textif ∃ τ, τ′ ∈ \{@repeatset{σ}\} . @no-overlap(τ, τ′) \\ 22 @∩τ[@repeatset{@simplify[σ]}] &\hspace{-1em}@otherwise 23 \end{cases} 24 \end{aligned} 25 } 26 27 #:Simplify2 28 29 @$${ 30 \begin{aligned} 31 @simplify[@f→[(@repeated{τ}) R]] 32 &= @f→[(@repeated{@simplify[τ]}) @simplify[R]] \\ 33 @simplify[@f*[(@repeated{τ} τ) R]] 34 &= @f*[(@repeated{@simplify[τ]} @simplify[τ]) @simplify[R]]\\ 35 @simplify[@f…[(@repeated{τ} @polydot[τ α]) R]] 36 &= @f…[(@repeated{@simplify[τ]} @polydot[@simplify[τ] α]) @simplify[R]]\\ 37 @simplify[@∀r[(@repeated{α}) τ]] 38 &= @∀r[(@repeated{α}) @simplify[τ]]\\ 39 @simplify[@∀r[(@repeated{α} @polydotα[α]) τ]] 40 &= @∀r[(@repeated{α} @polydotα[α]) @simplify[τ]]\\ 41 @simplify[@consτ[τ σ]] 42 &= @consτ[@${@simplify[τ]} @${@simplify[σ]}]\\ 43 @simplify[@List…τ[τ α]] 44 &= @List…τ[@simplify[τ] α]\\ 45 @simplify[@promiseτ[R]] 46 &= @promiseτ[@simplify[R]]\\ 47 @simplify[@recτ[r τ]] 48 &= @recτ[r @simplify[τ]] \\ 49 @simplify[τ] &= τ \qquad @otherwise \\ 50 @simplify[@R[τ φ⁺ φ⁻ o]] &= @R[@simplify[τ] @simplify[φ⁺] @simplify[φ⁻] o]\\ 51 @simplify[@repeatset{ψ}] &= @repeatset{@simplify[ψ]}\\ 52 @simplify[@${τ_{π(loc)}}] &= @simplify[τ]_{π(loc)}\\ 53 @simplify[@${@!{τ}_{π(loc)}}] &= @!{@simplify[τ]}_{π(loc)}\\ 54 @simplify[⊥] = ⊥ 55 \end{aligned} 56 } 57 58 #:Propagate⊥ 59 60 @$${ 61 \begin{aligned} 62 @propagate⊥(@consτ[τ σ]) &= ⊥ & @textif @=:[τ ⊥]\\ 63 @propagate⊥(@consτ[τ σ]) &= ⊥ & @textif @=:[σ ⊥]\\ 64 @propagate⊥(τ) &= ⊥ &@textif @=:[τ ⊥]\\@; For unions (subtyping will dispatch) 65 @propagate⊥(τ) &= τ &@otherwise 66 \end{aligned} 67 }