hyperlight_component_util/
tv.rs

1// SPDX-License-Identifier: Apache-2.0
2// Copyright 2025 The Hyperlight Authors.
3
4use crate::etypes::{
5    BoundedTyvar, Ctx, Defined, FreeTyvar, Handleable, ImportExport, TypeBound, Tyvar,
6};
7use crate::substitute::{self, Substitution, Unvoidable};
8
9/// The most information we possibly have about a type variable
10pub enum ResolvedTyvar<'a> {
11    /// Invariant: the head of this [`Defined`] is not `[Defined::Handleable]([HHandleable::Var](...))`
12    Definite(Defined<'a>),
13    /// It's just some bound var... so there is no way to look it up.
14    #[allow(unused)]
15    Bound(u32),
16    /// Invariant: the `TypeBound` is not `TypeBound::Eq`
17    E(u32, u32, TypeBound<'a>),
18    /// Invariant: the `TypeBound` is not `TypeBound::Eq`
19    U(u32, u32, TypeBound<'a>),
20}
21
22impl<'p, 'a> Ctx<'p, 'a> {
23    /// Look up a universal variable in the context, panicking if it doesn't exist
24    fn lookup_uvar<'c>(&'c self, o: u32, i: u32) -> &'c (BoundedTyvar<'a>, bool) {
25        // unwrap because failure is an internal invariant violation
26        &self.parents().nth(o as usize).unwrap().uvars[i as usize]
27    }
28    /// Look up an existential variable in the context, panicking if it doesn't exist
29    fn lookup_evar<'c>(&'c self, o: u32, i: u32) -> &'c (BoundedTyvar<'a>, Option<Defined<'a>>) {
30        // unwrap because failure is an internal invariant violation
31        &self.parents().nth(o as usize).unwrap().evars[i as usize]
32    }
33    /// Find a bound for the given free tyvar. Panics if given a
34    /// TV_bound; by the time you call this, you should have used
35    /// bound_to_[e/u]var.
36    pub fn var_bound<'c>(&'c self, tv: &Tyvar) -> &'c TypeBound<'a> {
37        match tv {
38            Tyvar::Bound(_) => panic!("Requested bound for Bound tyvar"),
39            Tyvar::Free(FreeTyvar::U(o, i)) => &self.lookup_uvar(*o, *i).0.bound,
40            Tyvar::Free(FreeTyvar::E(o, i)) => &self.lookup_evar(*o, *i).0.bound,
41        }
42    }
43    /// Try really hard to resolve a tyvar to a definite type or a
44    /// descriptive bound.
45    pub fn resolve_tyvar<'c>(&'c self, v: &Tyvar) -> ResolvedTyvar<'a> {
46        let check_deftype = |dt: &Defined<'a>| match dt {
47            Defined::Handleable(Handleable::Var(v_)) => self.resolve_tyvar(v_),
48            _ => ResolvedTyvar::Definite(dt.clone()),
49        };
50        match *v {
51            Tyvar::Bound(i) => ResolvedTyvar::Bound(i),
52            Tyvar::Free(FreeTyvar::E(o, i)) => {
53                let (tv, def) = self.lookup_evar(o, i);
54                match (&tv.bound, def) {
55                    (TypeBound::Eq(dt), _) => check_deftype(dt),
56                    (_, Some(dt)) => check_deftype(dt),
57                    (tb, _) => ResolvedTyvar::E(o, i, tb.clone()),
58                }
59            }
60            Tyvar::Free(FreeTyvar::U(o, i)) => {
61                let (tv, _) = self.lookup_uvar(o, i);
62                match &tv.bound {
63                    TypeBound::Eq(dt) => check_deftype(dt),
64                    tb => ResolvedTyvar::U(o, i, tb.clone()),
65                }
66            }
67        }
68    }
69    /// Modify the context to move the given variables into it as
70    /// existential variables and compute a substitution
71    /// that replaces bound variable references to them with free
72    /// variable references
73    pub fn bound_to_evars(
74        &mut self,
75        origin: Option<&'a str>,
76        vs: &[BoundedTyvar<'a>],
77    ) -> substitute::Opening {
78        let mut sub = substitute::Opening::new(false, self.evars.len() as u32);
79        for var in vs {
80            let var = var.push_origin(origin.map(ImportExport::Export));
81            let bound = sub.bounded_tyvar(&var).not_void();
82            self.evars.push((bound, None));
83            sub.next();
84        }
85        sub
86    }
87    /// Modify the context to move the given variables into it as
88    /// universal variables and compute a substitution that replaces
89    /// bound variable references to them with free variable
90    /// references
91    pub fn bound_to_uvars(
92        &mut self,
93        origin: Option<&'a str>,
94        vs: &[BoundedTyvar<'a>],
95        imported: bool,
96    ) -> substitute::Opening {
97        let mut sub = substitute::Opening::new(true, self.uvars.len() as u32);
98        for var in vs {
99            let var = var.push_origin(origin.map(ImportExport::Import));
100            let bound = sub.bounded_tyvar(&var).not_void();
101            self.uvars.push((bound, imported));
102            sub.next();
103        }
104        sub
105    }
106}
hyperlight_component_util/tv.rs

hyperlight_component_util/
tv.rs
