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

hyperlight_component_util/
substitute.rs
