Solve all pending constraints
(
&mut self,
arena: &mut Arena,
env: &Environment,
ctx: &Context,
)
| 103 | |
| 104 | /// Solve all pending constraints |
| 105 | pub fn solve( |
| 106 | &mut self, |
| 107 | arena: &mut Arena, |
| 108 | env: &Environment, |
| 109 | ctx: &Context, |
| 110 | ) -> crate::Result<()> { |
| 111 | while let Some(constraint) = self.constraints.pop_front() { |
| 112 | match constraint { |
| 113 | Constraint::Unify(t1, t2) => { |
| 114 | self.solve_unify(arena, env, ctx, t1, t2)?; |
| 115 | } |
| 116 | Constraint::IsSort(term) => { |
| 117 | // Check if term is or unifies to a sort |
| 118 | let term = self.apply_subst(arena, term)?; |
| 119 | if let Some(TermKind::Sort(_)) = arena.kind(term) { |
| 120 | // OK |
| 121 | } else if let Some(TermKind::MVar(_mvar)) = arena.kind(term) { |
| 122 | // Defer: we need more information |
| 123 | self.add_constraint(Constraint::IsSort(term)); |
| 124 | } else { |
| 125 | return Err(crate::Error::UnificationError( |
| 126 | "Expected sort".to_string(), |
| 127 | )); |
| 128 | } |
| 129 | } |
| 130 | Constraint::HasType(mvar, ty) => { |
| 131 | // Record the type constraint |
| 132 | self.mvar_types.insert(mvar, ty); |
| 133 | } |
| 134 | } |
| 135 | } |
| 136 | |
| 137 | Ok(()) |
| 138 | } |
| 139 | |
| 140 | /// Solve a unification constraint |
| 141 | fn solve_unify( |