|
2 | 2 |
|
3 | 3 | use std::fmt;
|
4 | 4 |
|
5 |
| -use crate::env::{Index, Level}; |
6 |
| -use crate::source::{FileRange, Span, StringId}; |
| 5 | +use scoped_arena::Scope; |
| 6 | + |
| 7 | +use crate::env::{EnvLen, Index, Level}; |
| 8 | +use crate::source::{Span, StringId}; |
7 | 9 |
|
8 | 10 | pub mod binary;
|
9 | 11 | pub mod pretty;
|
@@ -205,6 +207,10 @@ pub enum Term<'arena> {
|
205 | 207 | }
|
206 | 208 |
|
207 | 209 | impl<'arena> Term<'arena> {
|
| 210 | + pub fn error(span: impl Into<Span>) -> Self { |
| 211 | + Self::Prim(span.into(), Prim::ReportedError) |
| 212 | + } |
| 213 | + |
208 | 214 | /// Get the source span of the term.
|
209 | 215 | pub fn span(&self) -> Span {
|
210 | 216 | match self {
|
@@ -280,8 +286,153 @@ impl<'arena> Term<'arena> {
|
280 | 286 | matches!(self, Term::Prim(_, Prim::ReportedError))
|
281 | 287 | }
|
282 | 288 |
|
283 |
| - pub fn error(range: FileRange) -> Self { |
284 |
| - Self::Prim(range.into(), Prim::ReportedError) |
| 289 | + // TODO: Add a new `Weaken` variant to `core::Term` instead of eagerly |
| 290 | + // traversing the term? See [Andras Kovacs’ staged language](https://github.com/AndrasKovacs/staged/blob/9e381eb162f44912d70fb843c4ca6567b0d1683a/demo/Syntax.hs#L52) for an example |
| 291 | + pub fn shift(&self, scope: &'arena Scope<'arena>, amount: EnvLen) -> Term<'arena> { |
| 292 | + self.shift_inner(scope, Index::last(), amount) |
| 293 | + } |
| 294 | + |
| 295 | + /// Increment all `LocalVar`s greater than or equal to `min` by `amount` |
| 296 | + fn shift_inner( |
| 297 | + &self, |
| 298 | + scope: &'arena Scope<'arena>, |
| 299 | + mut min: Index, |
| 300 | + amount: EnvLen, |
| 301 | + ) -> Term<'arena> { |
| 302 | + // Skip traversing and rebuilding the term if it would make no change. Increases |
| 303 | + // sharing. |
| 304 | + if amount == EnvLen::new() { |
| 305 | + return self.clone(); |
| 306 | + } |
| 307 | + |
| 308 | + match self { |
| 309 | + Term::LocalVar(span, var) if *var >= min => Term::LocalVar(*span, *var + amount), |
| 310 | + Term::LocalVar(..) |
| 311 | + | Term::ItemVar(..) |
| 312 | + | Term::MetaVar(..) |
| 313 | + | Term::InsertedMeta(..) |
| 314 | + | Term::Prim(..) |
| 315 | + | Term::ConstLit(..) |
| 316 | + | Term::Universe(..) => self.clone(), |
| 317 | + Term::Ann(span, expr, r#type) => Term::Ann( |
| 318 | + *span, |
| 319 | + scope.to_scope(expr.shift_inner(scope, min, amount)), |
| 320 | + scope.to_scope(r#type.shift_inner(scope, min, amount)), |
| 321 | + ), |
| 322 | + Term::Let(span, name, def_type, def_expr, body) => Term::Let( |
| 323 | + *span, |
| 324 | + *name, |
| 325 | + scope.to_scope(def_type.shift_inner(scope, min, amount)), |
| 326 | + scope.to_scope(def_expr.shift_inner(scope, min, amount)), |
| 327 | + scope.to_scope(body.shift_inner(scope, min.prev(), amount)), |
| 328 | + ), |
| 329 | + Term::FunType(span, plicity, name, input, output) => Term::FunType( |
| 330 | + *span, |
| 331 | + *plicity, |
| 332 | + *name, |
| 333 | + scope.to_scope(input.shift_inner(scope, min, amount)), |
| 334 | + scope.to_scope(output.shift_inner(scope, min.prev(), amount)), |
| 335 | + ), |
| 336 | + Term::FunLit(span, plicity, name, body) => Term::FunLit( |
| 337 | + *span, |
| 338 | + *plicity, |
| 339 | + *name, |
| 340 | + scope.to_scope(body.shift_inner(scope, min.prev(), amount)), |
| 341 | + ), |
| 342 | + Term::FunApp(span, plicity, fun, arg) => Term::FunApp( |
| 343 | + *span, |
| 344 | + *plicity, |
| 345 | + scope.to_scope(fun.shift_inner(scope, min, amount)), |
| 346 | + scope.to_scope(arg.shift_inner(scope, min, amount)), |
| 347 | + ), |
| 348 | + Term::RecordType(span, labels, types) => Term::RecordType( |
| 349 | + *span, |
| 350 | + labels, |
| 351 | + scope.to_scope_from_iter(types.iter().map(|r#type| { |
| 352 | + let ret = r#type.shift_inner(scope, min, amount); |
| 353 | + min = min.prev(); |
| 354 | + ret |
| 355 | + })), |
| 356 | + ), |
| 357 | + Term::RecordLit(span, labels, exprs) => Term::RecordLit( |
| 358 | + *span, |
| 359 | + labels, |
| 360 | + scope.to_scope_from_iter( |
| 361 | + exprs |
| 362 | + .iter() |
| 363 | + .map(|expr| expr.shift_inner(scope, min, amount)), |
| 364 | + ), |
| 365 | + ), |
| 366 | + Term::RecordProj(span, head, label) => Term::RecordProj( |
| 367 | + *span, |
| 368 | + scope.to_scope(head.shift_inner(scope, min, amount)), |
| 369 | + *label, |
| 370 | + ), |
| 371 | + Term::ArrayLit(span, terms) => Term::ArrayLit( |
| 372 | + *span, |
| 373 | + scope.to_scope_from_iter( |
| 374 | + terms |
| 375 | + .iter() |
| 376 | + .map(|term| term.shift_inner(scope, min, amount)), |
| 377 | + ), |
| 378 | + ), |
| 379 | + Term::FormatRecord(span, labels, terms) => Term::FormatRecord( |
| 380 | + *span, |
| 381 | + labels, |
| 382 | + scope.to_scope_from_iter(terms.iter().map(|term| { |
| 383 | + let ret = term.shift_inner(scope, min, amount); |
| 384 | + min = min.prev(); |
| 385 | + ret |
| 386 | + })), |
| 387 | + ), |
| 388 | + Term::FormatCond(span, name, format, pred) => Term::FormatCond( |
| 389 | + *span, |
| 390 | + *name, |
| 391 | + scope.to_scope(format.shift_inner(scope, min, amount)), |
| 392 | + scope.to_scope(pred.shift_inner(scope, min.prev(), amount)), |
| 393 | + ), |
| 394 | + Term::FormatOverlap(span, labels, terms) => Term::FormatOverlap( |
| 395 | + *span, |
| 396 | + labels, |
| 397 | + scope.to_scope_from_iter(terms.iter().map(|term| { |
| 398 | + let ret = term.shift_inner(scope, min, amount); |
| 399 | + min = min.prev(); |
| 400 | + ret |
| 401 | + })), |
| 402 | + ), |
| 403 | + Term::ConstMatch(span, scrut, branches, default) => Term::ConstMatch( |
| 404 | + *span, |
| 405 | + scope.to_scope(scrut.shift_inner(scope, min, amount)), |
| 406 | + scope.to_scope_from_iter( |
| 407 | + branches |
| 408 | + .iter() |
| 409 | + .map(|(r#const, term)| (*r#const, term.shift_inner(scope, min, amount))), |
| 410 | + ), |
| 411 | + default.map(|(name, term)| { |
| 412 | + ( |
| 413 | + name, |
| 414 | + scope.to_scope(term.shift_inner(scope, min.prev(), amount)) as &_, |
| 415 | + ) |
| 416 | + }), |
| 417 | + ), |
| 418 | + } |
| 419 | + } |
| 420 | + |
| 421 | + /// Returns `true` if `self` can be evaluated in a single step. |
| 422 | + /// Used as a heuristic to prevent increase in runtime when expanding |
| 423 | + /// pattern matches |
| 424 | + pub fn is_atomic(&self) -> bool { |
| 425 | + match self { |
| 426 | + Term::ItemVar(_, _) |
| 427 | + | Term::LocalVar(_, _) |
| 428 | + | Term::MetaVar(_, _) |
| 429 | + | Term::InsertedMeta(_, _, _) |
| 430 | + | Term::Universe(_) |
| 431 | + | Term::Prim(_, _) |
| 432 | + | Term::ConstLit(_, _) => true, |
| 433 | + Term::RecordProj(_, head, _) => head.is_atomic(), |
| 434 | + _ => false, |
| 435 | + } |
285 | 436 | }
|
286 | 437 | }
|
287 | 438 |
|
@@ -603,6 +754,21 @@ pub enum Const {
|
603 | 754 | Ref(usize),
|
604 | 755 | }
|
605 | 756 |
|
| 757 | +impl Const { |
| 758 | + /// Return the number of inhabitants of `self`. |
| 759 | + /// `None` represents infinity |
| 760 | + pub fn num_inhabitants(&self) -> Option<u128> { |
| 761 | + match self { |
| 762 | + Const::Bool(_) => Some(2), |
| 763 | + Const::U8(_, _) | Const::S8(_) => Some(1 << 8), |
| 764 | + Const::U16(_, _) | Const::S16(_) => Some(1 << 16), |
| 765 | + Const::U32(_, _) | Const::S32(_) => Some(1 << 32), |
| 766 | + Const::U64(_, _) | Const::S64(_) => Some(1 << 64), |
| 767 | + Const::F32(_) | Const::F64(_) | Const::Pos(_) | Const::Ref(_) => None, |
| 768 | + } |
| 769 | + } |
| 770 | +} |
| 771 | + |
606 | 772 | impl PartialEq for Const {
|
607 | 773 | fn eq(&self, other: &Self) -> bool {
|
608 | 774 | match (*self, *other) {
|
|
0 commit comments