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

hyperlight_component_util/
tv.rs
