Skip to content

Commit

Permalink
feat(sol-thir): move to one single file
Browse files Browse the repository at this point in the history
  • Loading branch information
aripiprazole committed May 8, 2024
1 parent 19fff4a commit a0cb4d3
Show file tree
Hide file tree
Showing 2 changed files with 89 additions and 91 deletions.
81 changes: 0 additions & 81 deletions sol-thir/src/desugar.rs

This file was deleted.

99 changes: 89 additions & 10 deletions sol-thir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,18 +7,22 @@

use salsa::DbWithJar;
use sol_diagnostic::{Diagnostic, DiagnosticDb, ErrorId, ErrorKind};
use sol_hir::debruijin::{Index, Level};
use sol_hir::lowering::HirLowering;
use sol_hir::package::HasManifest;
use sol_hir::primitives::PrimitiveProvider;
use sol_hir::solver::{Definition, Reference};
use sol_hir::source::expr::{Expr, Meta};
use sol_hir::source::{HirError, Location};
use sol_hir::HirDb;
use sol_hir::{
debruijin::{Index, Level},
lowering::HirLowering,
package::HasManifest,
primitives::PrimitiveProvider,
solver::{Definition, Reference},
source::{
expr::{CallExpr, Expr, Meta},
literal::Literal,
pattern::Pattern,
HirElement, HirError, Location,
},
HirDb,
};
use sol_syntax::ParseDb;

pub mod desugar;

extern crate salsa_2022 as salsa;

#[salsa::jar(db = ThirDb)]
Expand Down Expand Up @@ -172,3 +176,78 @@ impl Term {
Term::Sorry(Location::CallSite, None)
}
}

pub fn literal_to_constructor_kind(literal: Literal) -> ConstructorKind {
match literal {
Literal::Empty => todo!(),
Literal::Int8(_) => todo!(),
Literal::UInt8(_) => todo!(),
Literal::Int16(_) => todo!(),
Literal::UInt16(_) => todo!(),
Literal::Int32(_) => todo!(),
Literal::UInt32(_) => todo!(),
Literal::Int64(_) => todo!(),
Literal::UInt64(_) => todo!(),
Literal::String(_) => todo!(),
Literal::Boolean(_) => todo!(),
Literal::Char(_) => todo!(),
}
}

pub fn get_definition(db: &dyn crate::ThirDb, pattern: Pattern) -> Definition {
match pattern {
Pattern::Hole => todo!(),
Pattern::Literal(_) => todo!(),
Pattern::Wildcard(_) => todo!(),
Pattern::Rest(_) => todo!(),
Pattern::Error(_) => todo!(),
Pattern::Constructor(_) => todo!(),
Pattern::Binding(binding) => binding.name,
}
}

#[salsa::tracked]
pub fn eval(db: &dyn crate::ThirDb, env: Env, expr: Expr) -> Term {
Term::located(expr.location(db), match expr {
Expr::Meta(Meta(location, value)) => Term::sorry_but_no(value),
Expr::Literal(ref literal) => Term::Constructor(Constructor {
location: literal.location.clone().unwrap_or(expr.location(db)),
kind: literal_to_constructor_kind(literal.value.clone()),
}),
Expr::Path(path) => Term::Constructor(Constructor {
location: path.location(db),
kind: ConstructorKind::Definition(path.definition(db)),
}),
Expr::Call(call) => todo!(),
Expr::Ann(ann) => todo!(),
Expr::Abs(abs) => abs
.parameters
.into_iter()
.fold(Err(*abs.value), |acc, param| {
let definition = get_definition(db, param.binding(db));
let location = param.location(db);
let term = Term::Lam(definition, param.is_implicit(db).into(), Closure {
env,
expr: match acc {
Ok(value) => quote(db, value),
Err(expr) => expr,
},
});

Ok(Term::located(location, term))
})
.expect("no first parameter"),
Expr::Match(expr) => Term::sorry(expr.location(db), ThirError::MatchNotSupported),
Expr::Upgrade(upgrade) => Term::sorry(upgrade.location(db), ThirError::UpgradeNotSupported),
Expr::Error(error) => Term::sorry(error.location(db), ThirError::HirError(error)),
Expr::Empty => Term::no(),
})
}

pub fn quote(db: &dyn crate::ThirDb, term: Term) -> Expr {
todo!()
}

pub fn infer(db: &dyn crate::ThirDb, env: Env, expr: Expr) -> (Expr, Type) {
todo!()
}

0 comments on commit a0cb4d3

Please sign in to comment.