-- Here: λ-term = λ-letrec-term
-- The relevant attributes: scoped and dfa
module {Lambda} {Λ (..), V, Params (..), LetPrefixLengths (..), LambdaDfa, State, Symbol (..),
showNameless, showTR, showTRNameless, combinations, synthesise,
scoped_Syn_R, deBruijn_Syn_R, dfa_Syn_R, readback_Syn_R, proof_Syn_R, unscoped_Syn_R}
{
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Monoid.Unicode
import Prelude.Unicode
import Data.Char (toLower)
import Language.HaLex.Dfa (Dfa (..))
import Text.PrettyPrint.Boxes
import Data.Functor
import Data.Graph
import Data.Tree (flatten)
import Data.List ((\\), delete, partition)
import Data.Either (partitionEithers)
}
{type V = String} -- variables
data Λ -- multi-purpose type for λ-terms
| V var ∷ V -- variable
| A fun ∷ Λ arg ∷ Λ -- application
| Λ var ∷ V body ∷ Λ -- lambda
| S var ∷ V body ∷ Λ -- abdmal / scope delimiter
| I var ∷ V body ∷ Λ -- indirection node
| L binds ∷ Binds body ∷ Λ -- let binding
type Binds = [Bind]
type Bind = (V,Λ)
data R | R body ∷ Λ -- a root for λ-terms; for supplying initial values of inherited attributes
{ -- `execution' of the attribute grammar
synthesise params t = wrap_R (sem_R $ R t) (Inh_R params False)
}
-- pretty printing
attr R Λ Bind Binds
inh ppNameless ∷ Bool
attr R Λ Bind
syn pp ∷ Box
attr R Λ
syn ppTR ∷ Box -- pretty printing using term rewriting syntax
attr Binds
syn pps ∷ {[Box]}
attr Λ
syn isComposed ∷ Bool
syn isApp ∷ Bool
sem Λ
| A Λ I L lhs.isComposed = True
| V S lhs.isComposed = False
| A lhs.isApp = True
| V Λ S I L lhs.isApp = False
{
maybeWrap ∷ Bool → Box → Box
maybeWrap isComposed box = if isComposed then char '(' <> box <#> char ')' else box
}
sem Λ
| A loc.pp = @loc.funPP <#> nullBox <+> @loc.argPP
loc.funPP = if @fun.isApp then @fun.pp else maybeWrap @fun.isComposed @fun.pp
loc.argPP = maybeWrap @arg.isComposed @arg.pp
| Λ loc.pp = text ("λ" ⧺ (if @lhs.ppNameless then "" else @var) ⧺ ".") <+> @body.pp
| S loc.pp = if @lhs.ppNameless
then text "S(" <> maybeWrap @body.isComposed @body.pp <> char ')'
else text ("/" ⧺ @var ⧺ ".") <+> @body.pp
| I loc.pp = text ("|" ⧺ @var ⧺ ".") <+> @body.pp
| V loc.pp = if @lhs.ppNameless ∧ @loc.varType == Λ_Bound then char '0' else text @var
| L loc.pp = let
binds = vcat left [f <+> char '=' <+> e | (f,e) <- zip fs' @binds.pps]
width = maximum $ map cols fs
fs = map text @binds.binders
fs' = map (alignHoriz left width) fs
in text "let" <+> binds // (text "in" <+> @body.pp)
sem Binds
| Nil loc.pps = []
| Cons loc.pps = @hd.pp : @tl.pps
{
app ∷ String → [Box] → Box
app f xs = text f <> char '(' <> punctuateH bottom (text ", ") xs <> char ')'
}
sem Λ
| A loc.ppTR = app "@" [@fun.ppTR, @arg.ppTR]
| Λ loc.ppTR = app (if @lhs.ppNameless then "L" else "L" ⧺ @var) [@body.ppTR]
| S loc.ppTR = app (if @lhs.ppNameless then "S" else "/" ⧺ @var ⧺ ".") [@body.ppTR]
| I loc.ppTR = app ("|" ⧺ @var) [@body.ppTR]
| V loc.ppTR = if @lhs.ppNameless ∧ @loc.varType == Λ_Bound then char '0' else text @var
| L loc.ppTR = error "term rewriting syntax currently only supported for let-bindings"
{
(<#>) ∷ Box → Box → Box
(<#>) l r = hcat bottom [l,r]
instance Show Λ where
show = render ∘ pp False
showNameless ∷ Λ → String
showNameless = render ∘ pp True
showTRNameless ∷ Λ → String
showTRNameless = render ∘ ppTR True
showTR ∷ Λ → String
showTR = render ∘ ppTR False
pp ∷ Bool → Λ → Box
pp nameless t = pp_Syn_R $ wrap_R (sem_R $ R t) (Inh_R undefined nameless)
ppTR ∷ Bool → Λ → Box
ppTR nameless t = ppTR_Syn_R $ wrap_R (sem_R $ R t) (Inh_R undefined nameless)
combinations ∷ [a] → [[a]]
combinations xs = [[x] | x ← xs] ⧺ [x : c | c ← combinations xs, x ← xs]
}
-- Generic attributes ---------------------------------------------------------
{
data Params = Params -- various parameters to customise the attribute grammar by
{letPrefixLengths ∷ LetPrefixLengths, -- which abstraction prefixes to use in the let-rule
withVarBacklinks, -- whether to use backlinks for variable vertices
withSBacklinks, -- whether to use backlinks for scope delimiters
withSharedVars ∷ Bool} -- whether variables are shared implicitely
-- TODO: del-rule
}
attr R Λ Bind Binds
inh params ∷ Params
-- binders
attr Bind
syn binder ∷ V
attr Binds
syn binders ∷ {[V]}
sem Bind | Tuple loc.binder = @x1
sem Binds
| Nil lhs.binders = []
| Cons lhs.binders = @hd.binder : @tl.binders
{data VarType = Free | LetBound | Λ_Bound deriving (Eq, Show)}
attr Λ Bind Binds
inh varTypeEnv ∷ {Map V VarType}
sem R | R body.varTypeEnv = ∅
sem Λ
| Λ body.varTypeEnv = Map.insert @var Λ_Bound @lhs.varTypeEnv
| L loc.varTypeEnv = @lhs.varTypeEnv ⊕ Map.fromList [(b, LetBound) | b <- @binds.binders]
binds.varTypeEnv = @loc.varTypeEnv
body.varTypeEnv = @loc.varTypeEnv
| V loc.varType = Map.findWithDefault Free @var @lhs.varTypeEnv
-- 'unscoped' synthesises an S-less version of the term
attr R
syn unscoped ∷ Λ
attr Λ Bind Binds
syn unscoped ∷ self
sem Λ | S lhs.unscoped = @body.unscoped
-- The set of free/used variables ---------------------------------------------
attr Λ Bind -- the sets contain both recursion and abstraction variables
syn fv ∷ {Set V} -- the set of free variables
syn uv ∷ {Set V} -- the set of used variables is very similar to the set of free variables
-- but it only takes into account function bindings that are actually used
sem Λ
| V loc.fv = Set.singleton @var -- O(1)
loc.uv = Set.singleton @var -- O(1)
| Λ loc.fv = Set.delete @var @body.fv -- O(log(n))
loc.uv = Set.delete @var @body.uv -- O(log(n))
| A loc.fv = @fun.fv ⊕ @arg.fv -- O(n)
loc.uv = @fun.uv ⊕ @arg.uv -- O(n)
| L loc.deleteBinders = flip (foldr Set.delete) @binds.binders -- O(n)
loc.fv = @loc.deleteBinders $ Set.unions $ @body.fv : @binds.fvs -- O(n)
loc.uv = @loc.deleteBinders $ Set.unions $ @body.uv : -- O(n)
[Map.findWithDefault (∅) v @loc.uvsTC | v <- Set.elems @body.uv] -- O(n) (if intersection is used)
-- transitive closure of the local call graph; O(n^2) but O(n) possible if SCCs are used instead
loc.uvsTC = transClos $ Map.fromList $ zip @binds.binders @binds.uvs
| S I loc.fv = undefined
loc.uv = undefined
{
-- TODO: Use Tarjan's algorithm instead (http://hackage.haskell.org/package/GraphSCC)
-- since SCCs is sufficient for our purposes.
transClos ∷ Ord a ⇒ Map a (Set a) → Map a (Set a)
transClos = converge $ \m → fmap (\ys → Set.unions $ ys : [Map.findWithDefault (∅) y m | y ← Set.elems ys]) m
-- compute fixpoint of a function by iterating it until it becomes monotonous
converge ∷ Eq a ⇒ (a → a) → a → a
converge step = fixPoint ∘ iterate step where
fixPoint (x:y:zs) = if x == y then x else fixPoint (y:zs)
}
attr Binds
syn fvs ∷ {[Set V]}
syn uvs ∷ {[Set V]}
sem Binds
| Nil loc.fvs = []
loc.uvs = []
| Cons loc.fvs = @hd.fv : @tl.fvs
loc.uvs = @hd.uv : @tl.uvs
-- used functions / garbage collection
attr Λ Binds Bind
inh usedBinds ∷ {Set V}
sem R | R body.usedBinds = ∅
sem Λ | L loc.usedBinds = @loc.uv `Set.intersection` Set.fromList @binds.binders
attr Bind
syn alive ∷ Bool
sem Bind | Tuple loc.alive = @loc.binder `Set.member` @lhs.usedBinds
attr R
syn garbageFree ∷ Λ
syn hasGarbage ∷ Bool
attr Λ Binds Bind
syn garbageFree ∷ self
syn hasGarbage use {∨} {False} ∷ Bool
sem Binds | Cons
lhs.garbageFree = if @hd.alive then @hd.garbageFree : @tl.garbageFree else @tl.garbageFree
lhs.hasGarbage = not @hd.alive ∨ @tl.hasGarbage
-- The set of required variables (TODO: currently requires unique naming) ----
attr Λ Bind Binds
inh rvEnv ∷ {Map V (Set V)} -- rv-sets of functions defined further above
syn rv use {⊕} {∅} ∷ {Set V} -- O(n)
attr Binds
syn rvs ∷ {[Set V]}
sem Binds
| Nil lhs.rvs = []
| Cons lhs.rvs = @hd.rv : @tl.rvs
sem R | R body.rvEnv = ∅
sem Λ
| Λ body.rvEnv = Map.delete @var @lhs.rvEnv -- O(log(n))
loc.rv = Set.delete @var @body.rv -- O(log(n))
| S loc.rv = @body.rv
| V loc.rv = Map.findWithDefault (Set.singleton @var) @var @lhs.rvEnv -- O(log(n))
| A loc.rv = @fun.rv ⊕ @arg.rv -- O(n)
| L loc.rvEnv = @lhs.rvEnv ⊕ fmap (substVars @lhs.rvEnv) @loc.uvsTC -- TODO: O(n) when using SCCs?
loc.rv = @loc.deleteBinders @body.rv -- O(n)
| I loc.rv = undefined
{
substVars ∷ Map V (Set V) → Set V → Set V
substVars rvEnv vs = Set.unions [Map.findWithDefault (Set.singleton v) v rvEnv | v ← Set.elems vs]
}
-- Scoped representation of a λ-term with de Bruijn indexes ------------------
-- TODO: currently only works (properly) for non-letrec λ-terms
attr R
syn deBruijn ∷ Λ
attr Λ Bind Binds
inh scope ∷ {[V]} -- all bound variables (extended scope / prefix with lazy scope-closure)
syn deBruijn ∷ self
sem R | R body.scope = []
sem Λ
| V lhs.deBruijn = if @loc.varType == LetBound
then V @var
else churnr (S <$> takeWhile (/= @var) @lhs.scope) (V @var)
| Λ body.scope = @var : @lhs.scope
-- Scoped representation of λ-terms ------------------------------------------
attr R
syn scoped ∷ Λ
data LetPrefixLengths -- abstraction prefixes chosen for the bindings of a binding group
| MaxPrefix -- maximal lengths, i.e. the inherited prefix is used for all bindings
| MinPrefix -- minimal lengths, resulting in unshared scope delimiters
| MaxEagPre -- maximal lengths that still guarantee eager scope-closure
| MaxEagTmp -- internal policy used my MaxEagPre that determines the prefixes of functions at all use sites
{
instance Show LetPrefixLengths where
show lpl = case lpl of
MaxPrefix → "maximal prefix lengths"
MinPrefix → "minimal prefix lengths"
MaxEagPre → "maximal prefix lengths while maintaining eager scope-closure"
}
-- {type Prefix = [V]}
{type Prefix = [(V, Set V)]}
attr Λ Bind Binds
inh mkPrefix ∷ {LetPrefixLengths -> Prefix}
syn maxEagTmp use {unionMaxPrefixes} {∅} ∷ {Map V Int} -- O(n)
syn scoped ∷ self
sem R | R body.mkPrefix = const [("*", (∅))]
{
-- Apply a list of functions to a value
churnr ∷ [a → a] → a → a
churnr = foldr (.) id
shortenPrefix ∷ Prefix → Set V → Prefix
shortenPrefix ps fv = dropWhile noFv ps where
noFv ("*",fs) = False
noFv (v,fs) = Set.null $ fv `Set.intersection` Set.insert v fs
-- Add a function symbol to a prefix at the given position
enrichPrefix ∷ (V, Int) → Prefix → Prefix
enrichPrefix (f,l) ps = updateAt (length ps - l) (\(x,fs) → (x, Set.insert f fs)) ps
updateAt ∷ Int → (a → a) → [a] → [a]
updateAt i f xs = let (ls,r:rs) = splitAt i xs in ls ⧺ f r : rs
unionMaxPrefixes ∷ Map V Int → Map V Int → Map V Int
unionMaxPrefixes = Map.unionWith min
}
sem Λ Bind
| * loc.prefix = @loc.mkPrefix $ letPrefixLengths @lhs.params
loc.parentPrefix = @lhs.mkPrefix $ letPrefixLengths @lhs.params
sem Λ
| * loc.mkPrefix = \strat -> case strat of
MaxEagTmp -> shortenPrefix (@lhs.mkPrefix MaxEagTmp) @loc.rv
strat -> shortenPrefix (@lhs.mkPrefix strat) @loc.fv
| Λ body.mkPrefix = ((@var, (∅)) :) ∘ @loc.mkPrefix
| L loc.mkPrefixLengths = \strat -> case strat of
MinPrefix -> map (length ∘ shortenPrefix @loc.prefix) @binds.rvs
MaxPrefix -> replicate (length @binds.binders) (length $ @loc.mkPrefix MaxPrefix)
MaxEagPre -> [Map.findWithDefault 0 f @loc.maxEagTmp | f <- @binds.binders]
MaxEagTmp -> replicate (length @binds.binders) (length $ @loc.mkPrefix MaxPrefix)
loc.newPrefix = \strat -> case strat of
MaxEagTmp -> @loc.mkPrefix MaxPrefix
strat -> foldr enrichPrefix @loc.prefix $ zip @binds.binders (@loc.mkPrefixLengths strat)
binds.mkPrefix = @loc.newPrefix
body.mkPrefix = @loc.newPrefix
attr Binds
inh mkPrefixLengths ∷ {LetPrefixLengths → [Int]}
sem Binds | Cons
hd.mkPrefix = \strat -> drop (length (@lhs.mkPrefix strat) - head (@lhs.mkPrefixLengths strat)) (@lhs.mkPrefix strat)
tl.mkPrefixLengths = tail ∘ @lhs.mkPrefixLengths
sem Bind | Tuple
loc.mkPrefix = @lhs.mkPrefix
sem Λ
| V lhs.maxEagTmp = if @loc.varType == LetBound then Map.singleton @var (length $ @lhs.mkPrefix MaxEagTmp) else (∅)
| Λ lhs.maxEagTmp = Map.delete @var @body.maxEagTmp
| L lhs.maxEagTmp = foldr Map.delete @loc.maxEagTmp @binds.binders -- O(n)
loc.maxEagTmp = @body.maxEagTmp `unionMaxPrefixes` @binds.maxEagTmp
sem Λ
| Λ A V L loc.scoped = churnr [S x | x <- @loc.killVars] @loc.scoped'
| * loc.killVars = take (length @loc.parentPrefix - length @loc.prefix) (map fst @loc.parentPrefix)
| Λ loc.scoped' = Λ @var @body.scoped
| A loc.scoped' = A @fun.scoped @arg.scoped
| V loc.scoped' = V @var
| L loc.scoped' = L @binds.scoped @body.scoped
| S I loc.scoped' = undefined
sem Bind | Tuple lhs.scoped = (@loc.binder, @x2.scoped)
sem Binds
| Nil lhs.scoped = []
| Cons lhs.scoped = @hd.scoped : @tl.scoped
-- DFA generation ------------------------------------------------------------
{
type LambdaDfa = Dfa State Symbol
type State = Int
dummyState, freevarState ∷ State
freevarState = 0
dummyState = -1 -- this is where `non-existing' transitions point
nextState = succ
firstState = 1
data Symbol = S_Λ | S_A0 | S_A1 | S_V | S_S0 | S_S1 | S_F V | S_I deriving (Eq, Ord)
instance Show Symbol where
show l = case l of
S_Λ → "L"
S_A0 → "A0"
S_A1 → "A1"
S_V → "0"
S_S0 → "S0"
S_S1 → "S1"
S_F v → v
S_I → "I"
type Transition = (State,Symbol,State)
data VarOcc = LamOcc State State | LetOcc State
-- | Transforms a λ-DFA by contracting all I-connected components (ICCs).
-- If an ICC is cyclic it becomes a blackhole (no outgoing edges), otherwise it vanishes.
contractI ∷ LambdaDfa → LambdaDfa
contractI (Dfa symbols states start accept trans) =
Dfa symbols states' start' (delete dummyState states') trans' where
states' = (states \\ concatMap fst iTrees) \\ concatMap tail blackholes
start' = Map.findWithDefault start start combinedMap
trans' state symbol = if state `Map.member` blackholeMap
then dummyState
else let target = trans state symbol in Map.findWithDefault target target combinedMap
combinedMap = blackholeMap ⊕ indirectionMap
blackholeMap ∷ Map State State
blackholeMap = Map.fromList [(s, head ss) | ss ← blackholes, s ← ss]
indirectionMap ∷ Map State State
indirectionMap = Map.fromList [(s, exit) | (ss, exit) ← iTrees, s ← ss]
blackholes ∷ [[State]] -- ^ I-cycles
iTrees ∷ [([State], State)] -- ^ non-cyclic I-connected components together with the non-I successor
(blackholes, iTrees) = partitionEithers $ map (blackholeOrNot ∘ flatten) (components iGraph) where
-- graph containing only the I-vertices of the DFA
iGraph = buildG (0, maximum states) iEdges where
iEdges = [(source,target) | source ← states, let target = trans source S_I, target ≢ dummyState]
blackholeOrNot states = case partition isI states of
(ss, [exit]) → Right (ss, exit)
(ss, [ ]) → Left ss -- blackhole
anythingElse → error "Infringement!1" -- cannot occur since I-vertices have only one exit
where isI s = trans s S_I ≢ dummyState
mkDfa ∷ State → [Transition] → LambdaDfa
mkDfa start transitions = contractI $ Dfa symbols (dummyState : states) start states trans where
states = nub $ concat [[source,target] | (source,label,target) ← transitions]
symbols = S_Λ : S_A0 : S_A1 : S_V : S_S0 : S_S1 : S_I : nub [S_F v | (from, S_F v, to) ← transitions]
trans state symbol = Map.findWithDefault dummyState (state,symbol) mapping where
mapping = Map.fromList $ map mkTrans transitions
mkTrans (source, label, target) = ((source, label), target)
nub ∷ Ord a ⇒ [a] → [a]
nub = Set.elems ∘ Set.fromList
}
attr R
syn dfa ∷ {LambdaDfa}
sem R | R lhs.dfa = mkDfa @body.node @body.transitions
body.freshState = firstState
body.dfaEnv = ∅
{nextUnique n = (nextState n, n)}
attr Λ Bind Binds
inh dfaEnv ∷ {Map V VarOcc} -- environment for the backlinks
chn freshState ∷ State
syn transitions ∷ {[Transition]}
attr Λ Bind
syn node ∷ State
attr Binds
syn nodes ∷ {[State]}
sem Binds
| Nil lhs.transitions = []
lhs.nodes = []
| Cons lhs.transitions = @hd.transitions ⧺ @tl.transitions
lhs.nodes = @hd.node : @tl.nodes
sem Bind | Tuple
lhs.transitions = (@loc.node, S_I, @x2.node) : @x2.transitions
loc.node ∷ uniqueref freshState
sem Λ
| Λ loc.node ∷ uniqueref freshState
loc.occ ∷ uniqueref freshState
body.dfaEnv = Map.insert @var (LamOcc @loc.occ @loc.node) @lhs.dfaEnv
lhs.transitions = (@loc.node, S_Λ, @body.node) : @body.transitions
| A loc.node ∷ uniqueref freshState
lhs.transitions = (@loc.node, S_A0, @fun.node) : (@loc.node, S_A1, @arg.node) : @fun.transitions ⧺ @arg.transitions
| L lhs.node = @body.node
loc.newDfaEnv = @lhs.dfaEnv ⊕ Map.fromList [(v, LetOcc i) | (v,i) <- zip @binds.binders @binds.nodes]
binds.dfaEnv = @loc.newDfaEnv
body.dfaEnv = @loc.newDfaEnv
lhs.transitions = @body.transitions ⧺ @binds.transitions
| V loc.dfaLookup = Map.lookup @var @lhs.dfaEnv
lhs.transitions = case @loc.dfaLookup of
Nothing -> [(@loc.node, S_F @var, freevarState)] -- free variable
Just (LamOcc occ abs) -> [(@loc.node, S_V, if withVarBacklinks @lhs.params then abs else freevarState)]
Just (LetOcc i) -> []
loc.node = case @loc.dfaLookup of
Nothing -> @loc.maybeNode -- free variable. TODO: take into account withSharedVars
Just (LamOcc occ abs) -> if withSharedVars @lhs.params then occ else @loc.maybeNode
Just (LetOcc i) -> i
loc.maybeNode ∷ uniqueref freshState
| S loc.abs = case Map.lookup @var @lhs.dfaEnv of
Just (LamOcc occ abs) -> abs
_ -> error $ "delimiter couldn't find his abstraction: " ⧺ @var
lhs.transitions = (@loc.node, S_S0, @body.node) : (@loc.node, S_S1, @loc.abs) : @body.transitions
loc.node ∷ uniqueref freshState
-- readback ------------------------------------------------------------
attr R
syn readback ∷ Λ
sem R
| R lhs.readback = case head @body.bindings of
[] -> @body.readback
bs -> L bs @body.readback
attr Λ
syn readback ∷ Λ
syn bindings ∷ {[Binds]}
sem Λ
| Λ lhs.bindings = tail @body.bindings
lhs.readback = Λ @var $ @loc.addL @body.readback
loc.addL = case head @body.bindings of
[] -> id
bs -> L bs
| S lhs.bindings = [] : @body.bindings
lhs.readback = S @var @body.readback
| A lhs.bindings = zipWith (⧺) @fun.bindings @arg.bindings
lhs.readback = A @fun.readback @arg.readback
| I lhs.bindings = let (bs:bss) = @body.bindings in ((@var,@body.readback) : bs) : bss
lhs.readback = V @var
| V lhs.bindings = repeat []
lhs.readback = V @var
| L lhs.bindings = @loc.readbackError
lhs.readback = @loc.readbackError
loc.readbackError = error "readback is only defined for λ-spanning-trees"
-- proof generation ----------------------------------------------------
{
infer ∷ String → [Box] → Box → Box
infer step assumptions conclusion = vcat left [asBox, line, conclusion] where
line = text (replicate (max (cols asBox) (cols conclusion)) '-') <+> text step
asBox = hsep 2 bottom assumptions
mkProof ∷ Bool → String → [Box] → Prefix → Box → Int → Box
mkProof isLetVar name assumptions prefix term numS = let conclusion = mkPrefix prefix <+> term in
if numS ≡ 0
then if isLetVar then conclusion else infer name assumptions conclusion
else infer "S" [mkProof isLetVar name assumptions (tail prefix) term (numS - 1)] conclusion
mkPrefix ∷ Prefix → Box
mkPrefix prefix = text $ "(" ⧺ unwords (map showVar $ reverse prefix) ⧺ ")"
where showVar (v,fs) = v ⧺ if Set.null fs then "" else "[" ⧺ unwords (Set.toList fs) ⧺ "]"
}
attr R Λ Bind
syn proof ∷ Box
sem Λ
| * loc.proof = mkProof @loc.isLvar @loc.proofstep @loc.assumptions @loc.parentPrefix @loc.pp (length @loc.killVars)
| V loc.proofstep = "0"
loc.assumptions = []
| A loc.proofstep = "@"
loc.assumptions = [@fun.proof, @arg.proof]
| Λ loc.proofstep = "λ"
loc.assumptions = [@body.proof]
| S loc.proofstep = "S"
loc.assumptions = [@body.proof]
| L loc.proofstep = "let"
loc.assumptions = @binds.proofs ⧺ [@body.proof]
| I loc.proofstep = undefined
loc.assumptions = undefined
| V loc.isLvar = @loc.varType == LetBound
| A S Λ L I loc.isLvar = False
sem Bind | Tuple lhs.proof = @x2.proof
attr Binds
syn proofs ∷ {[Box]}
sem Binds
| Nil lhs.proofs = []
| Cons lhs.proofs = @hd.proof : @tl.proofs