hyperlight_component_util/
substitute.rs

1/*
2Copyright 2025 The Hyperlight Authors.
3
4Licensed under the Apache License, Version 2.0 (the "License");
5you may not use this file except in compliance with the License.
6You may obtain a copy of the License at
7
8    http://www.apache.org/licenses/LICENSE-2.0
9
10Unless required by applicable law or agreed to in writing, software
11distributed under the License is distributed on an "AS IS" BASIS,
12WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
13See the License for the specific language governing permissions and
14limitations under the License.
15 */
16
17//! Capture-avoiding substitution
18
19use std::primitive::u32;
20
21use crate::etypes::{
22    BoundedTyvar, Component, Ctx, Defined, ExternDecl, ExternDesc, FreeTyvar, Func, Handleable,
23    Instance, Param, QualifiedInstance, RecordField, TypeBound, Tyvar, Value, VariantCase,
24};
25use crate::tv::ResolvedTyvar;
26
27/// A substitution
28///
29/// This trait can be implemented by specific structures that have
30/// specific substitution behavior, which only need to define how the
31/// act on bound/existential/universal variables. The implemented
32/// methods on the trait will then allow applying that substitution in
33/// a capture-avoiding manner to any relevant term.
34///
35/// The [`Shiftable`] bound is required because the implementation of
36/// substitution for components and instances needs to be able to
37/// shift the substitution in order to make substitution
38/// capture-avoiding.
39pub trait Substitution<'a>
40where
41    Self: Shiftable<'a>,
42{
43    /// Some, but not all, substitutions are fallible (i.e. may reveal
44    /// latent misbehaviour in the type they are being applied to), so
45    /// any given [`Substitution`] can provide its own
46    /// [`Substitution::Error`] type.
47    ///
48    /// An infallible substitution can use [`Void`] to reflect
49    /// the fact that error is impossible, and callers can use
50    /// [`Unvoidable::not_void`] to eliminate the impossible case of
51    /// the result neatly.
52    type Error: From<<<Self as Shiftable<'a>>::Inner as Substitution<'a>>::Error>;
53    /// Any substitution should define whether a given bound variable
54    /// should be substituted, and if so with what.
55    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
56    /// Any substitution should define whether a given existential variable
57    /// should be substituted, and if so with what.
58    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
59    /// Any substitution should define whether a given universal variable
60    /// should be substituted, and if so with what.
61    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error>;
62
63    fn record_fields(&self, rfs: &[RecordField<'a>]) -> Result<Vec<RecordField<'a>>, Self::Error> {
64        rfs.iter()
65            .map(|rf| {
66                Ok(RecordField {
67                    name: rf.name,
68                    ty: self.value(&rf.ty)?,
69                })
70            })
71            .collect()
72    }
73
74    fn variant_cases(&self, vcs: &[VariantCase<'a>]) -> Result<Vec<VariantCase<'a>>, Self::Error> {
75        vcs.iter()
76            .map(|vc| {
77                Ok(VariantCase {
78                    name: vc.name,
79                    ty: self.value_option(&vc.ty)?,
80                    refines: vc.refines,
81                })
82            })
83            .collect()
84    }
85
86    fn value_option(&self, vt: &Option<Value<'a>>) -> Result<Option<Value<'a>>, Self::Error> {
87        vt.as_ref().map(|ty| self.value(ty)).transpose()
88    }
89
90    fn value(&self, vt: &Value<'a>) -> Result<Value<'a>, Self::Error> {
91        Ok(match vt {
92            Value::Bool => Value::Bool,
93            Value::S(w) => Value::S(*w),
94            Value::U(w) => Value::U(*w),
95            Value::F(w) => Value::F(*w),
96            Value::Char => Value::Char,
97            Value::String => Value::String,
98            Value::List(vt) => Value::List(Box::new(self.value(vt)?)),
99            Value::Record(rfs) => Value::Record(self.record_fields(rfs)?),
100            Value::Variant(vcs) => Value::Variant(self.variant_cases(vcs)?),
101            Value::Flags(ns) => Value::Flags(ns.clone()),
102            Value::Enum(ns) => Value::Enum(ns.clone()),
103            Value::Option(vt) => Value::Option(Box::new(self.value(vt)?)),
104            Value::Tuple(vts) => Value::Tuple(
105                vts.iter()
106                    .map(|vt| self.value(vt))
107                    .collect::<Result<Vec<Value<'a>>, Self::Error>>()?,
108            ),
109            Value::Result(vt1, vt2) => Value::Result(
110                Box::new(self.value_option(vt1)?),
111                Box::new(self.value_option(vt2)?),
112            ),
113            Value::Own(h) => Value::Own(self.handleable_(h)?),
114            Value::Borrow(h) => Value::Borrow(self.handleable_(h)?),
115            Value::Var(tv, vt) => Value::Var(
116                tv.as_ref().and_then(|tv| match self.var(tv) {
117                    Ok(Some(Defined::Handleable(Handleable::Var(tv)))) => Some(tv),
118                    Ok(None) => Some(tv.clone()),
119                    _ => None,
120                }),
121                Box::new(self.value(vt)?),
122            ),
123        })
124    }
125
126    fn param(&self, pt: &Param<'a>) -> Result<Param<'a>, Self::Error> {
127        Ok(Param {
128            name: pt.name,
129            ty: self.value(&pt.ty)?,
130        })
131    }
132
133    fn params(&self, pts: &Vec<Param<'a>>) -> Result<Vec<Param<'a>>, Self::Error> {
134        pts.iter().map(|pt| self.param(pt)).collect()
135    }
136
137    fn result(
138        &self,
139        rt: &crate::etypes::Result<'a>,
140    ) -> Result<crate::etypes::Result<'a>, Self::Error> {
141        Ok(match rt {
142            crate::etypes::Result::Unnamed(vt) => crate::etypes::Result::Unnamed(self.value(vt)?),
143            crate::etypes::Result::Named(pts) => crate::etypes::Result::Named(self.params(pts)?),
144        })
145    }
146
147    fn func(&self, ft: &Func<'a>) -> Result<Func<'a>, Self::Error> {
148        Ok(Func {
149            params: self.params(&ft.params)?,
150            result: self.result(&ft.result)?,
151        })
152    }
153
154    fn var(&self, tv: &Tyvar) -> Result<Option<Defined<'a>>, Self::Error> {
155        match tv {
156            Tyvar::Bound(i) => self.subst_bvar(*i),
157            Tyvar::Free(FreeTyvar::U(o, i)) => self.subst_uvar(*o, *i),
158            Tyvar::Free(FreeTyvar::E(o, i)) => self.subst_evar(*o, *i),
159        }
160    }
161
162    fn handleable(&self, h: &Handleable) -> Result<Defined<'a>, Self::Error> {
163        let hh = Defined::Handleable(h.clone());
164        match h {
165            Handleable::Resource(_) => Ok(hh),
166            Handleable::Var(tv) => Ok(self.var(tv)?.unwrap_or(hh)),
167        }
168    }
169
170    fn handleable_(&self, h: &Handleable) -> Result<Handleable, Self::Error> {
171        match self.handleable(h)? {
172            Defined::Handleable(h_) => Ok(h_),
173            _ => panic!("internal invariant a violation: owned/borrowed var is not resource"),
174        }
175    }
176
177    fn defined(&self, dt: &Defined<'a>) -> Result<Defined<'a>, Self::Error> {
178        Ok(match dt {
179            Defined::Handleable(h) => self.handleable(h)?,
180            Defined::Value(vt) => Defined::Value(self.value(vt)?),
181            Defined::Func(ft) => Defined::Func(self.func(ft)?),
182            Defined::Instance(it) => Defined::Instance(self.qualified_instance(it)?),
183            Defined::Component(ct) => Defined::Component(self.component(ct)?),
184        })
185    }
186
187    fn type_bound(&self, tb: &TypeBound<'a>) -> Result<TypeBound<'a>, Self::Error> {
188        Ok(match tb {
189            TypeBound::Eq(dt) => TypeBound::Eq(self.defined(dt)?),
190            TypeBound::SubResource => TypeBound::SubResource,
191        })
192    }
193
194    fn bounded_tyvar(&self, btv: &BoundedTyvar<'a>) -> Result<BoundedTyvar<'a>, Self::Error> {
195        Ok(BoundedTyvar {
196            origin: btv.origin.clone(),
197            bound: self.type_bound(&btv.bound)?,
198        })
199    }
200
201    fn extern_desc(&self, ed: &ExternDesc<'a>) -> Result<ExternDesc<'a>, Self::Error> {
202        Ok(match ed {
203            ExternDesc::CoreModule(cmt) => ExternDesc::CoreModule(cmt.clone()),
204            ExternDesc::Func(ft) => ExternDesc::Func(self.func(ft)?),
205            ExternDesc::Type(dt) => ExternDesc::Type(self.defined(dt)?),
206            ExternDesc::Instance(it) => ExternDesc::Instance(self.instance(it)?),
207            ExternDesc::Component(ct) => ExternDesc::Component(self.component(ct)?),
208        })
209    }
210
211    fn extern_decl(&self, ed: &ExternDecl<'a>) -> Result<ExternDecl<'a>, Self::Error> {
212        Ok(ExternDecl {
213            kebab_name: ed.kebab_name,
214            desc: self.extern_desc(&ed.desc)?,
215        })
216    }
217
218    fn instance(&self, it: &Instance<'a>) -> Result<Instance<'a>, Self::Error> {
219        let exports = it
220            .exports
221            .iter()
222            .map(|ed| self.extern_decl(ed))
223            .collect::<Result<Vec<_>, Self::Error>>()?;
224        Ok(Instance { exports })
225    }
226
227    fn qualified_instance(
228        &self,
229        qit: &QualifiedInstance<'a>,
230    ) -> Result<QualifiedInstance<'a>, Self::Error> {
231        let mut evars = Vec::new();
232        let mut sub = self.shifted();
233        for evar in &qit.evars {
234            evars.push(sub.bounded_tyvar(evar)?);
235            sub.bshift(1);
236            sub.rbshift(1);
237        }
238        let it = sub.instance(&qit.unqualified)?;
239        Ok(QualifiedInstance {
240            evars,
241            unqualified: it,
242        })
243    }
244
245    fn component(&self, ct: &Component<'a>) -> Result<Component<'a>, Self::Error> {
246        let mut uvars = Vec::new();
247        let mut sub = self.shifted();
248        for uvar in &ct.uvars {
249            uvars.push(sub.bounded_tyvar(uvar)?);
250            sub.bshift(1);
251            sub.rbshift(1);
252        }
253        let imports = ct
254            .imports
255            .iter()
256            .map(|ed| sub.extern_decl(ed).map_err(Into::into))
257            .collect::<Result<Vec<ExternDecl<'a>>, Self::Error>>()?;
258        let instance = sub.qualified_instance(&ct.instance)?;
259        Ok(Component {
260            uvars,
261            imports,
262            instance,
263        })
264    }
265}
266
267/// A substitution that shifts bound variables up by a defined offset.
268/// This will generally be accessed through [`Shifted`] below.  It is
269/// important to ensure that a bound variable produced by a
270/// substitution is not captured.
271struct RBShift {
272    rbshift: i32,
273}
274impl<'a> Shiftable<'a> for RBShift {
275    type Inner = Self;
276    fn shifted<'b>(&'b self) -> Shifted<'b, Self::Inner> {
277        Shifted::new(self)
278    }
279}
280impl<'a> Substitution<'a> for RBShift {
281    type Error = Void;
282    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
283        Ok(Some(Defined::Handleable(Handleable::Var(Tyvar::Bound(
284            i.checked_add_signed(self.rbshift).unwrap(),
285        )))))
286    }
287    fn subst_evar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
288        Ok(None)
289    }
290    fn subst_uvar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
291        Ok(None)
292    }
293}
294
295/// A substitution that can be converted into a [`Shifted`]
296/// substitution. All types other than [`Shifted`] itself should
297/// implement this with the obvious option of
298/// ```
299/// impl<'a> Shiftable<'a> for A {
300///     type Inner = Self;
301///     fn shifted<'b>(&'b self) -> Shifted<'b, Self::Inner> { Shifted::new(self) }
302/// }
303/// ```
304/// Unfortunately, it is not reasonably possible to provide this
305/// automatically without specialization.
306pub trait Shiftable<'a> {
307    type Inner: ?Sized + Substitution<'a>;
308    fn shifted<'c>(&'c self) -> Shifted<'c, Self::Inner>;
309}
310
311/// A "shifted" version of a substitution, used internally to assure
312/// that substitution is capture-avoiding.
313pub struct Shifted<'b, A: ?Sized> {
314    /// The substitution which is being shifted
315    underlying: &'b A,
316    /// The offset to apply to bound variables before querying the
317    /// original substitution
318    bshift: i32,
319    /// The offset to apply to outer instance indices before
320    /// querying the original substitution
321    oshift: i32,
322    /// The offset to apply to free evar indices before
323    /// querying the original substitution
324    eshift: i32,
325    /// The offset to apply to free uvar indices before
326    /// querying the original substitution
327    ushift: i32,
328    /// The offset to apply to bound variables in the result of the
329    /// original substitution
330    rbshift: i32,
331}
332impl<'b, A: ?Sized> Clone for Shifted<'b, A> {
333    fn clone(&self) -> Self {
334        Self {
335            underlying: self.underlying,
336            bshift: self.bshift,
337            oshift: self.oshift,
338            eshift: self.eshift,
339            ushift: self.ushift,
340            rbshift: self.rbshift,
341        }
342    }
343}
344impl<'a, 'b, A: ?Sized + Substitution<'a>> Shiftable<'a> for Shifted<'b, A> {
345    type Inner = A;
346    fn shifted<'c>(&'c self) -> Shifted<'c, Self::Inner> {
347        self.clone()
348    }
349}
350
351impl<'a, 'b, A: ?Sized + Substitution<'a>> Shifted<'b, A> {
352    fn new(s: &'b A) -> Self {
353        Self {
354            underlying: s,
355            bshift: 0,
356            oshift: 0,
357            eshift: 0,
358            ushift: 0,
359            rbshift: 0,
360        }
361    }
362    fn bshift(&mut self, bshift: i32) {
363        self.bshift += bshift;
364    }
365    #[allow(unused)]
366    fn oshift(&mut self, oshift: i32) {
367        self.oshift += oshift;
368    }
369    #[allow(unused)]
370    fn ushift(&mut self, ushift: i32) {
371        self.ushift += ushift;
372    }
373    #[allow(unused)]
374    fn eshift(&mut self, eshift: i32) {
375        self.eshift += eshift;
376    }
377    fn rbshift(&mut self, rbshift: i32) {
378        self.rbshift += rbshift;
379    }
380
381    fn sub_rbshift(
382        &self,
383        dt: Result<Option<Defined<'a>>, <Self as Substitution<'a>>::Error>,
384    ) -> Result<Option<Defined<'a>>, <Self as Substitution<'a>>::Error> {
385        match dt {
386            Ok(Some(dt)) => {
387                let rbsub = RBShift {
388                    rbshift: self.rbshift,
389                };
390                Ok(Some(rbsub.defined(&dt).not_void()))
391            }
392            _ => dt,
393        }
394    }
395}
396
397impl<'a, 'b, A: ?Sized + Substitution<'a>> Substitution<'a> for Shifted<'b, A> {
398    type Error = A::Error;
399    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
400        match i.checked_add_signed(-self.bshift) {
401            Some(i) => self.sub_rbshift(self.underlying.subst_bvar(i)),
402            _ => Ok(None),
403        }
404    }
405    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
406        match (
407            o.checked_add_signed(-self.oshift),
408            i.checked_add_signed(-self.eshift),
409        ) {
410            (Some(o), Some(i)) => self.sub_rbshift(self.underlying.subst_evar(o, i)),
411            _ => Ok(None),
412        }
413    }
414    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
415        match (
416            o.checked_add_signed(-self.oshift),
417            i.checked_add_signed(-self.ushift),
418        ) {
419            (Some(o), Some(i)) => self.sub_rbshift(self.underlying.subst_uvar(o, i)),
420            _ => Ok(None),
421        }
422    }
423}
424
425/// Innerizing can fail because a type variable needs to be taken
426/// through an `outer_boundary` but cannot be resolved to a concrete
427/// type that can be copied.
428#[derive(Debug)]
429pub enum InnerizeError {
430    IndefiniteTyvar,
431}
432/// An innerize substitution is used to bring an outer type alias
433/// inwards through one context.
434pub struct Innerize<'c, 'p, 'a> {
435    /// What ctx was this type originally in?
436    ctx: &'c Ctx<'p, 'a>,
437    /// Are we crossing an outer_boundary?
438    outer_boundary: bool,
439}
440impl<'c, 'p, 'a> Shiftable<'a> for Innerize<'c, 'p, 'a> {
441    type Inner = Self;
442    fn shifted<'d>(&'d self) -> Shifted<'d, Self::Inner> {
443        Shifted::new(self)
444    }
445}
446impl<'c, 'p, 'a> Substitution<'a> for Innerize<'c, 'p, 'a> {
447    type Error = InnerizeError;
448    fn subst_bvar(&self, _i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
449        Ok(None)
450    }
451    // Note that even if the variables resolve, what they resolve to
452    // needs to itself be innerized, since it was also designed for
453    // this context.
454    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
455        if !self.outer_boundary {
456            Ok(Some(Defined::Handleable(Handleable::Var(Tyvar::Free(
457                FreeTyvar::E(o + 1, i),
458            )))))
459        } else {
460            match self.ctx.resolve_tyvar(&Tyvar::Free(FreeTyvar::E(o, i))) {
461                ResolvedTyvar::Definite(dt) => Ok(Some(self.defined(&dt)?)),
462                _ => Err(InnerizeError::IndefiniteTyvar),
463            }
464        }
465    }
466    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, Self::Error> {
467        if !self.outer_boundary {
468            Ok(Some(Defined::Handleable(Handleable::Var(Tyvar::Free(
469                FreeTyvar::U(o + 1, i),
470            )))))
471        } else {
472            match self.ctx.resolve_tyvar(&Tyvar::Free(FreeTyvar::U(o, i))) {
473                ResolvedTyvar::Definite(dt) => Ok(Some(self.defined(&dt)?)),
474                _ => Err(InnerizeError::IndefiniteTyvar),
475            }
476        }
477    }
478}
479impl<'c, 'p, 'a> Innerize<'c, 'p, 'a> {
480    pub fn new(ctx: &'c Ctx<'p, 'a>, outer_boundary: bool) -> Innerize<'c, 'p, 'a> {
481        Innerize {
482            ctx,
483            outer_boundary,
484        }
485    }
486}
487
488/// The empty (void) type
489pub enum Void {}
490
491/// Things that you can call [`not_void`](Unvoidable::not_void) on
492pub trait Unvoidable {
493    type Result;
494    fn not_void(self) -> Self::Result;
495}
496
497/// Eliminate a Result<_, Void>
498impl<A> Unvoidable for Result<A, Void> {
499    type Result = A;
500    fn not_void(self) -> A {
501        match self {
502            Ok(x) => x,
503            Err(v) => match v {},
504        }
505    }
506}
507
508/// An opening substitution is used to map bound variables into
509/// free variables. Note that because of the differences in ordering
510/// for bound variable indices (inside out) and context variables
511/// (left to right, but variables are inserted in outside-in order),
512/// `Bound(0)` gets mapped to `Free(0, base + n)`.
513pub struct Opening {
514    /// Whether to produce E or U free variables
515    is_universal: bool,
516    /// At what index in the context are the free variables being
517    /// inserted?
518    free_base: u32,
519    /// How many bound variables are being shifted to the context
520    how_many: u32,
521}
522impl<'a> Shiftable<'a> for Opening {
523    type Inner = Self;
524    fn shifted<'d>(&'d self) -> Shifted<'d, Self::Inner> {
525        Shifted::new(self)
526    }
527}
528impl<'a> Substitution<'a> for Opening {
529    type Error = Void;
530    fn subst_bvar(&self, i: u32) -> Result<Option<Defined<'a>>, Void> {
531        let mk = |i| {
532            let fi = self.free_base + self.how_many - i - 1;
533            if self.is_universal {
534                FreeTyvar::U(0, fi)
535            } else {
536                FreeTyvar::E(0, fi)
537            }
538        };
539        Ok(if i < self.how_many {
540            Some(Defined::Handleable(Handleable::Var(Tyvar::Free(mk(i)))))
541        } else {
542            None
543        })
544    }
545    fn subst_evar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Void> {
546        Ok(None)
547    }
548    fn subst_uvar(&self, _o: u32, _i: u32) -> Result<Option<Defined<'a>>, Void> {
549        Ok(None)
550    }
551}
552impl Opening {
553    pub fn new(is_universal: bool, free_base: u32) -> Self {
554        Opening {
555            is_universal,
556            free_base,
557            how_many: 0,
558        }
559    }
560    pub fn next(&mut self) {
561        self.how_many += 1;
562    }
563}
564
565/// A closing substitution is used to map free variables into bound
566/// variables when converting a type being built in a context to a
567/// closed(ish) type that is above that context.
568///
569/// Like [`Opening`], a given [`Closing`] substitution either affects
570/// only existential variables or affects only universal variables, as
571/// these are closed at different times.
572pub struct Closing {
573    /// If this substitution applies to universal variables, this
574    /// keeps track of which ones are imported and which are
575    /// not. Non-imported universal variables may not be referred to
576    /// in types.
577    ///
578    /// Invariant: If this is provided, its length must be equal to
579    /// self.how_many
580    universal_imported: Option<Vec<bool>>,
581    /// How many of the relevant (u/e) free vars are valid at this point.
582    how_many: u32,
583}
584impl Closing {
585    pub fn new(is_universal: bool) -> Self {
586        let universal_imported = if is_universal { Some(Vec::new()) } else { None };
587        Closing {
588            universal_imported,
589            how_many: 0,
590        }
591    }
592    fn is_universal(&self) -> bool {
593        self.universal_imported.is_some()
594    }
595    pub fn next_u(&mut self, imported: bool) {
596        let Some(ref mut importeds) = self.universal_imported else {
597            panic!("next_u called on existential Closing");
598        };
599        importeds.push(imported);
600        self.how_many += 1;
601    }
602    pub fn next_e(&mut self) {
603        if self.is_universal() {
604            panic!("next_e called on universal Closing");
605        };
606        self.how_many += 1;
607    }
608    fn subst_uevar<'a>(
609        &self,
610        ue_is_u: bool,
611        o: u32,
612        i: u32,
613    ) -> Result<Option<Defined<'a>>, ClosingError> {
614        if self.is_universal() ^ ue_is_u {
615            return Ok(None);
616        }
617        let mk_ue = |o, i| {
618            if self.is_universal() {
619                Tyvar::Free(FreeTyvar::U(o, i))
620            } else {
621                Tyvar::Free(FreeTyvar::E(o, i))
622            }
623        };
624        let mk = |v| Ok(Some(Defined::Handleable(Handleable::Var(v))));
625        if o > 0 {
626            return mk(mk_ue(o - 1, i));
627        }
628        if i >= self.how_many {
629            return Err(ClosingError::UnknownVar(false, i));
630        }
631        let bidx = if let Some(imported) = &self.universal_imported {
632            if !imported[i as usize] {
633                return Err(ClosingError::UnimportedVar(i));
634            }
635            imported[i as usize..].iter().filter(|x| **x).count() as u32 - 1
636        } else {
637            self.how_many - i - 1
638        };
639        mk(Tyvar::Bound(bidx))
640    }
641}
642impl<'a> Shiftable<'a> for Closing {
643    type Inner = Self;
644    fn shifted<'d>(&'d self) -> Shifted<'d, Self::Inner> {
645        Shifted::new(self)
646    }
647}
648/// Closing can fail for a few reasons:
649#[derive(Debug)]
650#[allow(unused)]
651pub enum ClosingError {
652    /// A variable was encountered that isn't currently being moved to
653    /// a bound variable. This is an internal invariant violation in
654    /// the typechecker, not an issue of a malformed input type.
655    UnknownVar(bool, u32),
656    /// A universal variable wasn't imported. This is probably an
657    /// internal invariant violation in the typechecker.
658    UnimportedVar(u32),
659}
660impl<'a> Substitution<'a> for Closing {
661    type Error = ClosingError;
662    fn subst_bvar(&self, _: u32) -> Result<Option<Defined<'a>>, ClosingError> {
663        Ok(None)
664    }
665    fn subst_evar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, ClosingError> {
666        self.subst_uevar(false, o, i)
667    }
668    fn subst_uvar(&self, o: u32, i: u32) -> Result<Option<Defined<'a>>, ClosingError> {
669        self.subst_uevar(true, o, i)
670    }
671}
hyperlight_component_util/substitute.rs

hyperlight_component_util/
substitute.rs
