1use std::any::TypeId;
18use std::collections::HashMap;
19use std::fmt;
20use std::marker::PhantomData;
21use std::sync::{Arc, Mutex, MutexGuard};
22
23use ghost_cell::GhostToken;
24
25use crate::dag::{Dag, DagLike, SharingTracker};
26use crate::jet::Jet;
27
28use super::{
29 Bound, CompleteBound, Error, Final, Incomplete, Type, TypeInner, UbElement, WithGhostToken,
30};
31
32type InvariantLifetime<'brand> = PhantomData<fn(&'brand ()) -> &'brand ()>;
37
38#[derive(Clone)]
48pub struct Context<'brand> {
49 inner: Arc<Mutex<WithGhostToken<'brand, ContextInner<'brand>>>>,
50}
51
52struct ContextInner<'brand> {
53 slab: Vec<Bound<'brand>>,
54 jet_type: Option<TypeId>,
56}
57
58impl fmt::Debug for Context<'_> {
59 fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
60 let id = Arc::as_ptr(&self.inner) as usize;
61 write!(f, "inference_ctx_{:08x}", id)
62 }
63}
64
65impl PartialEq for Context<'_> {
66 fn eq(&self, other: &Self) -> bool {
67 Arc::ptr_eq(&self.inner, &other.inner)
68 }
69}
70impl Eq for Context<'_> {}
71
72impl<'brand> Context<'brand> {
73 pub fn with_context<R, F>(fun: F) -> R
75 where
76 F: for<'new_brand> FnOnce(Context<'new_brand>) -> R,
77 {
78 GhostToken::new(|token| {
79 let ctx = Context::new(token);
80 fun(ctx)
81 })
82 }
83
84 pub fn new(token: GhostToken<'brand>) -> Self {
86 Context {
87 inner: Arc::new(Mutex::new(WithGhostToken {
88 token,
89 inner: ContextInner {
90 slab: vec![],
91 jet_type: None,
92 },
93 })),
94 }
95 }
96
97 fn alloc_bound(&self, bound: Bound<'brand>) -> BoundRef<'brand> {
99 let mut lock = self.lock();
100 lock.alloc_bound(bound)
101 }
102
103 pub fn alloc_free(&self, name: String) -> BoundRef<'brand> {
105 self.alloc_bound(Bound::Free(name))
106 }
107
108 pub fn alloc_unit(&self) -> BoundRef<'brand> {
110 self.alloc_bound(Bound::Complete(Final::unit()))
111 }
112
113 pub fn alloc_complete(&self, data: Arc<Final>) -> BoundRef<'brand> {
115 self.alloc_bound(Bound::Complete(data))
116 }
117
118 pub fn alloc_sum(&self, left: Type<'brand>, right: Type<'brand>) -> BoundRef<'brand> {
120 let mut lock = self.lock();
121 if let Some((data1, data2)) = lock.complete_pair_data(&left.inner, &right.inner) {
122 lock.alloc_bound(Bound::Complete(Final::sum(data1, data2)))
123 } else {
124 lock.alloc_bound(Bound::Sum(left.inner, right.inner))
125 }
126 }
127
128 pub fn alloc_product(&self, left: Type<'brand>, right: Type<'brand>) -> BoundRef<'brand> {
130 let mut lock = self.lock();
131 if let Some((data1, data2)) = lock.complete_pair_data(&left.inner, &right.inner) {
132 lock.alloc_bound(Bound::Complete(Final::product(data1, data2)))
133 } else {
134 lock.alloc_bound(Bound::Product(left.inner, right.inner))
135 }
136 }
137
138 pub fn shallow_clone(&self) -> Self {
144 Self {
145 inner: Arc::clone(&self.inner),
146 }
147 }
148
149 pub fn check_eq(&self, other: &Self) -> Result<(), super::Error> {
151 if self == other {
152 Ok(())
153 } else {
154 Err(super::Error::InferenceContextMismatch)
155 }
156 }
157
158 pub fn check_jet(&self, jet: &dyn Jet) {
163 let new_id = jet.as_any().type_id();
164 let mut lock = self.lock();
165
166 if let Some(existing_id) = lock.inner.jet_type {
167 assert!(existing_id == new_id, "mixed jet types in context");
168
169 return;
170 }
171
172 lock.inner.jet_type = Some(new_id);
173 }
174
175 pub(super) fn get(&self, bound: &BoundRef<'brand>) -> Bound<'brand> {
177 let lock = self.lock();
178 lock.inner.slab[bound.index].shallow_clone()
179 }
180
181 pub(super) fn get_root_ref(
183 &self,
184 bound: &UbElement<'brand, BoundRef<'brand>>,
185 ) -> BoundRef<'brand> {
186 let mut lock = self.lock();
187 bound.root(&mut lock.token)
188 }
189
190 pub(super) fn reassign_non_complete(&self, bound: BoundRef<'brand>, new: Bound<'brand>) {
201 let mut lock = self.lock();
202 lock.reassign_non_complete(bound, new);
203 }
204
205 pub fn bind_product(
210 &self,
211 existing: &Type<'brand>,
212 prod_l: &Type<'brand>,
213 prod_r: &Type<'brand>,
214 hint: &'static str,
215 ) -> Result<(), Error> {
216 let mut lock = self.lock();
217 let existing_root = existing.inner.bound.root(&mut lock.token);
218 let new_bound = Bound::Product(prod_l.inner.shallow_clone(), prod_r.inner.shallow_clone());
219
220 lock.bind(existing_root, new_bound).map_err(|e| {
221 let new_bound = lock.alloc_bound(e.new);
222 drop(lock);
223 Error::Bind {
224 existing_bound: Incomplete::from_bound_ref(self, e.existing),
225 new_bound: Incomplete::from_bound_ref(self, new_bound),
226 hint,
227 }
228 })
229 }
230
231 pub fn unify(
235 &self,
236 ty1: &Type<'brand>,
237 ty2: &Type<'brand>,
238 hint: &'static str,
239 ) -> Result<(), Error> {
240 let mut lock = self.lock();
241 lock.unify(&ty1.inner, &ty2.inner).map_err(|e| {
242 let new_bound = lock.alloc_bound(e.new);
243 drop(lock);
244 Error::Bind {
245 existing_bound: Incomplete::from_bound_ref(self, e.existing),
246 new_bound: Incomplete::from_bound_ref(self, new_bound),
247 hint,
248 }
249 })
250 }
251
252 fn lock(&self) -> MutexGuard<'_, WithGhostToken<'brand, ContextInner<'brand>>> {
254 self.inner.lock().unwrap()
255 }
256}
257
258#[derive(Debug, Clone, PartialEq, Eq, Hash)]
259pub struct BoundRef<'brand> {
260 phantom: InvariantLifetime<'brand>,
261 index: usize,
262}
263
264impl<'brand> BoundRef<'brand> {
265 pub fn occurs_check_id(&self) -> OccursCheckId<'brand> {
269 OccursCheckId {
270 phantom: InvariantLifetime::default(),
271 index: self.index,
272 }
273 }
274}
275
276impl super::PointerLike for BoundRef<'_> {
277 fn ptr_eq(&self, other: &Self) -> bool {
278 self.index == other.index
279 }
280
281 fn shallow_clone(&self) -> Self {
282 BoundRef {
283 phantom: InvariantLifetime::default(),
284 index: self.index,
285 }
286 }
287}
288
289pub type CtxAndBoundRef<'ctx, 'brand> = (&'ctx Context<'brand>, BoundRef<'brand>);
290
291impl<'brand> DagLike for CtxAndBoundRef<'_, 'brand> {
292 type Node = BoundRef<'brand>;
293 fn data(&self) -> &BoundRef<'brand> {
294 &self.1
295 }
296
297 fn as_dag_node(&self) -> Dag<Self> {
298 match self.0.get(&self.1) {
299 Bound::Free(..) | Bound::Complete(..) => Dag::Nullary,
300 Bound::Sum(ref ty1, ref ty2) | Bound::Product(ref ty1, ref ty2) => {
301 let root1 = self.0.get_root_ref(&ty1.bound);
302 let root2 = self.0.get_root_ref(&ty2.bound);
303 Dag::Binary((self.0, root1), (self.0, root2))
304 }
305 }
306 }
307}
308
309#[derive(Clone, Debug, Default)]
310pub struct BoundRefSharing<'brand> {
311 map: HashMap<BoundRef<'brand>, usize>,
312}
313
314impl<'brand> SharingTracker<CtxAndBoundRef<'_, 'brand>> for BoundRefSharing<'brand> {
315 fn record(&mut self, d: &CtxAndBoundRef<'_, 'brand>, index: usize) -> Option<usize> {
316 use std::collections::hash_map::Entry;
317 match self.map.entry(d.1.clone()) {
318 Entry::Occupied(occ) => Some(*occ.get()),
319 Entry::Vacant(vac) => {
320 vac.insert(index);
321 None
322 }
323 }
324 }
325 fn seen_before(&self, d: &CtxAndBoundRef<'_, 'brand>) -> Option<usize> {
326 self.map.get(&d.1).copied()
327 }
328}
329
330#[derive(Copy, Clone, PartialEq, Eq, Debug, Hash)]
331pub struct OccursCheckId<'brand> {
332 phantom: InvariantLifetime<'brand>,
333 index: usize,
334}
335
336struct BindError<'brand> {
337 existing: BoundRef<'brand>,
338 new: Bound<'brand>,
339}
340
341impl<'brand> ContextInner<'brand> {
342 fn alloc_bound(&mut self, bound: Bound<'brand>) -> BoundRef<'brand> {
343 self.slab.push(bound);
344 let index = self.slab.len() - 1;
345
346 BoundRef {
347 phantom: InvariantLifetime::default(),
348 index,
349 }
350 }
351
352 fn reassign_non_complete(&mut self, bound: BoundRef<'brand>, new: Bound<'brand>) {
353 assert!(
354 !matches!(self.slab[bound.index], Bound::Complete(..)),
355 "tried to modify finalized type",
356 );
357 self.slab[bound.index] = new;
358 }
359}
360
361impl<'brand> WithGhostToken<'brand, ContextInner<'brand>> {
362 fn complete_pair_data(
368 &mut self,
369 inn1: &TypeInner<'brand>,
370 inn2: &TypeInner<'brand>,
371 ) -> Option<(Arc<Final>, Arc<Final>)> {
372 let idx1 = inn1.bound.root(&mut self.token).index;
373 let idx2 = inn2.bound.root(&mut self.token).index;
374 let bound1 = &self.slab[idx1];
375 let bound2 = &self.slab[idx2];
376 if let (Bound::Complete(ref data1), Bound::Complete(ref data2)) = (bound1, bound2) {
377 Some((Arc::clone(data1), Arc::clone(data2)))
378 } else {
379 None
380 }
381 }
382 fn unify(
386 &mut self,
387 existing: &TypeInner<'brand>,
388 other: &TypeInner<'brand>,
389 ) -> Result<(), BindError<'brand>> {
390 existing
391 .bound
392 .unify(self, &other.bound, |self_, x_bound, y_bound| {
393 self_.bind(x_bound, self_.slab[y_bound.index].shallow_clone())
394 })
395 }
396
397 fn bind(
398 &mut self,
399 existing: BoundRef<'brand>,
400 new: Bound<'brand>,
401 ) -> Result<(), BindError<'brand>> {
402 let existing_bound = self.slab[existing.index].shallow_clone();
403 let bind_error = || BindError {
404 existing: existing.clone(),
405 new: new.shallow_clone(),
406 };
407
408 match (&existing_bound, &new) {
409 (_, Bound::Free(_)) => Ok(()),
411 (Bound::Free(_), _) => {
413 self.reassign_non_complete(existing, new);
415 Ok(())
416 }
417 (Bound::Complete(ref existing_final), Bound::Complete(ref new_final)) => {
420 if existing_final == new_final {
421 Ok(())
422 } else {
423 Err(bind_error())
424 }
425 }
426 (Bound::Complete(complete), incomplete) | (incomplete, Bound::Complete(complete)) => {
428 match (complete.bound(), incomplete) {
429 (CompleteBound::Unit, _) => Err(bind_error()),
432 (
433 CompleteBound::Product(ref comp1, ref comp2),
434 Bound::Product(ref ty1, ref ty2),
435 )
436 | (CompleteBound::Sum(ref comp1, ref comp2), Bound::Sum(ref ty1, ref ty2)) => {
437 let bound1 = ty1.bound.root(&mut self.token);
438 let bound2 = ty2.bound.root(&mut self.token);
439 self.bind(bound1, Bound::Complete(Arc::clone(comp1)))?;
440 self.bind(bound2, Bound::Complete(Arc::clone(comp2)))
441 }
442 _ => Err(bind_error()),
443 }
444 }
445 (Bound::Sum(ref x1, ref x2), Bound::Sum(ref y1, ref y2))
446 | (Bound::Product(ref x1, ref x2), Bound::Product(ref y1, ref y2)) => {
447 self.unify(x1, y1)?;
448 self.unify(x2, y2)?;
449 if let Some((data1, data2)) = self.complete_pair_data(y1, y2) {
457 self.reassign_non_complete(
458 existing,
459 Bound::Complete(if let Bound::Sum(..) = existing_bound {
460 Final::sum(data1, data2)
461 } else {
462 Final::product(data1, data2)
463 }),
464 );
465 }
466 Ok(())
467 }
468 (_, _) => Err(bind_error()),
469 }
470 }
471}