Auxiliary functions (Revised7.0 Report on the Algorithmic Language Scheme (Unofficial))

Previous: Semantic functions, Up: Formal semantics [Contents][Index]

7.2.4 Auxiliary functions ¶

$lookup : U \to Ide \to L$

$lookup = λ, ρ, I . ρ, I$

$extends : U \to {Ide}^{*} \to L^{*} \to U$

$extends =$

$λ, ρ, I^{*} α^{*} .$

$# I^{*} = 0 \to ρ,$

$extends (ρ [(α^{*} ↓ 1) / (I^{*} ↓ 1)]), (I^{*} † 1), (α^{*} † 1)$

$wrong : X \to C [implementation-dependent]$

$send : E \to K \to C$

$send = λ, ϵ, κ . κ ⟨ ϵ ⟩$

$single : (E \to C) \to K$

$single =$

$λ, ψ, ϵ^{*} .$

$# ϵ^{*} = 1 \to ψ (ϵ^{*} ↓ 1),$

$wrong “ wrong number of return values ”$

$new : S \to (L + {error}) [implementation-dependent]$

$hold : L \to K \to C$

$hold = λ, α, κ, σ . send (σ, α ↓ 1), κ, σ$

$assign : L \to E \to C \to C$

$assign = λ, α, ϵ, θ, σ . θ (update α, ϵ, σ)$

$update : L \to E \to S \to S$

$update = λ α, ϵ, σ . σ, [⟨ ϵ, true ⟩ / α]$

$tievals : (L^{*} \to C) \to E^{*} \to C$

$tievals =$

$λ, ψ, ϵ^{*} σ .$

$# ϵ^{*} = 0 \to ψ, ⟨ ⟩, σ,$

$new σ \in L \to tievals$

$(λ, α^{*} . ψ (⟨ new σ | L ⟩ § α^{*}))$

$(ϵ^{*} † 1)$

$(update (new σ | L), (ϵ^{*} ↓ 1), σ),$

$wrong “ out of memory ”, σ$

$tievalsrest : (L^{*} \to C) \to E^{*} \to N \to C$

$tievalsrest =$

$λ, ψ, ϵ^{*} ν . list$

$(dropfirst ϵ^{*}, ν)$

$(single (λ, ϵ . tievals ψ, ((takefirst ϵ^{*}, ν) § ⟨ ϵ ⟩)))$

$dropfirst = λ, l, n . n = 0 \to l, dropfirst (l † 1), (n - 1)$

$takefirst = λ, l, n . n = 0 \to ⟨ ⟩, ⟨ l ↓ 1 ⟩ § (takefirst (l † 1), (n - 1))$

$truish : E \to T$

$truish = λ, ϵ . ϵ = false \to false, true$

$permute : {Exp}^{*} \to {Exp}^{*} [implementation-dependent]$

$unpermute : E^{*} \to E^{*} [inverse of permute]$

$applicate : E \to E^{*} \to P \to K \to C$

$applicate =$

$λ, ϵ, ϵ^{*}, ω, κ . ϵ \in F \to (ϵ | F ↓ 2), ϵ^{*}, ω, κ, wrong “ bad procedure ”$

$onearg : (E \to P \to K \to C) \to (E^{*} \to P \to K \to C)$

$onearg =$

$λ, ζ, ϵ^{*}, ω, κ .$

$# ϵ^{*} = 1 \to ζ, (ϵ^{*} ↓ 1), ω, κ,$

$wrong “ wrong number of arguments ”$

$twoarg : (E \to E \to P \to K \to C) \to (E^{*} \to P \to K \to C)$

$twoarg =$

$λ, ζ, ϵ^{*}, ω, κ .$

$# ϵ^{*} = 2 \to ζ, (ϵ^{*} ↓ 1) (ϵ^{*} ↓ 2), ω, κ,$

$wrong “ wrong number of arguments ”$

$threearg : (E \to E \to E \to P \to K \to C) \to (E^{*} \to P \to K \to C)$

$threearg =$

$λ, ζ, ϵ^{*}, ω, κ .$

$# ϵ^{*} = 3 \to ζ, (ϵ^{*} ↓ 1) (ϵ^{*} ↓ 2) (ϵ^{*} ↓ 3), ω, κ,$

$wrong “ wrong number of arguments ”$

$list : E^{*} \to P \to K \to C$

$list =$

$λ, ϵ^{*}, ω, κ .$

$# ϵ^{*} = 0 \to send null κ,$

$list (ϵ^{*} † 1), (single (λ, ϵ . cons ⟨ ϵ^{*} ↓ 1, ϵ ⟩, κ))$

$cons : E^{*} \to P \to K \to C$

$cons =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, κ, ω σ .$

$new σ \in L \to$

$(λ, σ^{'} . new σ^{'} \in L \to$

$send$

$(⟨$

$new σ | L, new σ^{'} | L, true ⟩$

$in E$

$κ$

$(update (new σ^{'} | L), ϵ_{2}, σ^{'}),$

$wrong “ out of memory ”, σ^{'})$

$(update (new σ | L), ϵ_{1}, σ),$

$wrong “ out of memory ”, σ)$

$less : E^{*} \to P \to K \to C$

$less =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, ω, κ .$

$(ϵ_{1} \in R \land ϵ_{2} \in R) \to$

$send (ϵ_{1} | R < ϵ_{2} | R \to true, false), κ,$

$wrong “ non-numeric argument to < ”)$

$add : E^{*} \to P \to K \to C$

$add =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, ω, κ .$

$(ϵ_{1} \in R \land ϵ_{2} \in R) \to$

$send ((ϵ_{1} | R + ϵ_{2} | R) in E), κ,$

$wrong “ non-numeric argument to + ”)$

$car : E^{*} \to P \to K \to C$

$car =$

$onearg (λ, ϵ, ω, κ .$

$ϵ \in E_{p} \to car-internal ϵ, κ,$

$wrong “ non-pair argument to car ”)$

$car-internal : E \to K \to C$

$car-internal = λ, ϵ, ω, κ . hold (ϵ | E_{p} ↓ 1), κ$

$cdr : E^{*} \to P \to K \to C [similar to car]$

$cdr-internal : E \to K \to C [similar to car-internal]$

$setcar : E^{*} \to P \to K \to C$

$setcar =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, ω, κ .$

$ϵ_{1} \in E_{p} \to$

$(ϵ_{1} | E_{p} ↓ 3) \to assign$

$(ϵ_{1} | E_{p} ↓ 1)$

$ϵ_{2}$

$(send unspecified κ),$

$wrong “ immutable argument to set-car! ”,$

$wrong “ non-pair argument to set-car! ”)$

$eqv : E^{*} \to P \to K \to C$

$eqv =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, ω, κ .$

$(ϵ_{1} \in M \land ϵ_{2} \in M) \to$

$send (ϵ_{1} | M = ϵ_{2} | M \to true, false), κ,$

$(ϵ_{1} \in Q \land ϵ_{2} \in Q) \to$

$send (ϵ_{1} | Q = ϵ_{2} | Q \to true, false), κ,$

$(ϵ_{1} \in H \land ϵ_{2} \in H) \to$

$send (ϵ_{1} | H = ϵ_{2} | H \to true, false), κ,$

$(ϵ_{1} \in R \land ϵ_{2} \in R) \to$

$send (ϵ_{1} | R = ϵ_{2} | R \to true, false), κ,$

$(ϵ_{1} \in E_{p} \land ϵ_{2} \in E_{p}) \to$

$send$

$($

$(λ, p_{1}, p_{2} . ($

$(p_{1} ↓ 1) = (p_{2} ↓ 1) \land$

$(p_{1} ↓ 2) = (p_{2} ↓ 2)) \to true,$

$false)$

$(ϵ_{1} | E_{p})$

$(ϵ_{2} | E_{p}))$

$κ,$

$(ϵ_{1} \in E_{v} \land ϵ_{2} \in E_{v}) \to \dots,$

$(ϵ_{1} \in E_{s} \land ϵ_{2} \in E_{s}) \to \dots,$

$(ϵ_{1} \in F \land ϵ_{2} \in F) \to$

$send$

$((ϵ_{1} | F ↓ 1) = (ϵ_{2} | F ↓ 1) \to true, false)$

$κ,$

$send false κ)$

$apply : E^{*} \to P \to K \to C$

$apply =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, ω, κ .$

$ϵ_{1} \in F \to valueslist ϵ_{2}, (λ, ϵ^{*} . applicate ϵ_{1}, ϵ^{*}, ω, κ),$

$wrong “ bad procedure argument to apply ”)$

$valueslist : E \to K \to C$

$valueslist =$

$λ, ϵ, κ .$

$ϵ \in E_{p} \to$

$cdr-internal$

$ϵ$

$(λ, ϵ^{*} .$

$valueslist$

$ϵ^{*}$

$(λ, ϵ^{*} .$

$car-internal$

$ϵ$

$(single (λ, ϵ . κ (⟨ ϵ ⟩ § ϵ^{*}))))),$

$ϵ = null \to κ ⟨ ⟩,$

$wrong “ non-list argument to values-list ”$

$cwcc$

$: E^{*} \to P \to K \to C$

$[call-with-current-continuation]$

$cwcc =$

$onearg (λ, ϵ, ω, κ .$

$ϵ \in F \to$

$(λ, σ .$

$new σ \in L \to$

$applicate$

$ϵ$

$⟨$

$new σ | L,$

$λ, ϵ^{*}, ω^{'}, κ^{'} . travel ω^{'}, ω (κ, ϵ^{*}) ⟩$

$in E ⟩$

$ω$

$κ$

$(update$

$(new σ | L)$

$unspecified$

$σ),$

$wrong “ out of memory ” σ),$

$wrong “ bad procedure argument ”)$

$travel : P \to P \to C \to C$

$travel =$

$λ, ω_{1}, ω_{2} . travelpath ($

$(pathup ω_{1}, (commonancest ω_{1}, ω_{2})) §$

$(pathdown (commonancest ω_{1}, ω_{2}), ω_{2}))$

$pointdepth : P \to N$

$pointdepth =$

$λ, ω . ω = root \to 0, 1 + (pointdepth (ω | (F \times F \times P) ↓ 3))$

$ancestors : P \to 𝒫, P$

$ancestors =$

$λ, ω . ω = root \to {ω}, {ω} \cup (ancestors (ω | (F \times F \times P) ↓ 3))$

$commonancest : P \to P \to P$

$commonancest =$

$λ, ω_{1}, ω_{2} .$

$the only element of$

${ω^{'} ∣$

$ω^{'} \in (ancestors ω_{1}) \cap (ancestors ω_{2}),$

$pointdepth ω^{'} \geq pointdepth ω^{″}$

$\forall ω^{″} \in (ancestors ω_{1}) \cap (ancestors ω_{2})}$

$pathup : P \to P \to {(P \times F)}^{*}$

$pathup =$

$λ, ω_{1}, ω_{2} .$

$ω_{1} = ω_{2} \to ⟨ ⟩,$

$⟨ (ω_{1}, ω_{1} | (F \times F \times P) ↓ 2) ⟩ §$

$(pathup (ω_{1} | (F \times F \times P) ↓ 3) ω_{2})$

$pathdown : P \to P \to {(P \times F)}^{*}$

$pathdown =$

$λ, ω_{1}, ω_{2} .$

$ω_{1} = ω_{2} \to ⟨ ⟩,$

$(pathdown ω_{1} (ω_{2} | (F \times F \times P) ↓ 3)) §$

$⟨ (ω_{2}, ω_{2} | (F \times F \times P) ↓ 1) ⟩$

$travelpath : {(P \times F)}^{*} \to C \to C$

$travelpath =$

$λ, π^{*}, θ .$

$# π^{*} = 0 \to θ,$

$((π^{*} ↓ 1) ↓ 2)$

$⟨ ⟩ ((π^{*} ↓ 1) ↓ 1)$

$(λ, ϵ^{*} . travelpath (π^{*} † 1) θ)$

$dynamicwind : E^{*} \to P \to K \to C$

$dynamicwind =$

$threearg$

$(λ, ϵ_{1}, ϵ_{2}, ϵ_{3}, ω, κ . (ϵ_{1} \in F \land ϵ_{2} \in F \land ϵ_{3} \in F) \to$

$applicate$

$ϵ_{1}, ⟨ ⟩, ω (λ, ζ^{*} .$

$applicate$

$ϵ_{2}, ⟨ ⟩, ((ϵ_{1} | F, ϵ_{3} | F, ω) in P)$

$(λ, ϵ^{*} . applicate ϵ_{3}, ⟨ ⟩ ω (λ, ζ^{*} . κ, ϵ^{*}))),$

$wrong “ bad procedure argument ”)$

$values : E^{*} \to P \to K \to C$

$values = λ, ϵ^{*}, ω, κ . κ, ϵ^{*}$

$cwv : E^{*} \to P \to K \to C [call-with-values]$

$cwv =$

$twoarg (λ, ϵ_{1}, ϵ_{2}, ω, κ . applicate ϵ_{1}, ⟨ ⟩ ω, (λ, ϵ^{*} . applicate ϵ_{2}, ϵ^{*}, ω))$