Skip to content

Commit

Permalink
Merge UnifyError, TypeError and EvalError
Browse files Browse the repository at this point in the history
  • Loading branch information
@BinderDavid
BinderDavid committed Mar 25, 2024
1 parent 6cc8990 commit e12bb26
Show file tree
Hide file tree
Showing 8 changed files with 71 additions and 105 deletions.
2 changes: 1 addition & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,14 +49,14 @@ pol --help
├── app CLI application
├── examples Example code in the object language
├── lang Language implementation
│ ├── elaborator Elaborating an untyped syntax tree into a typed syntax tree.
│ ├── lifting Lift local (co)matches to top-level definitions
│ ├── lowering Lowering concrete to (untyped) abstract syntax tree
│ ├── parser Parse text to concrete syntax tree
│ ├── printer Print abstract syntax tree to text
│ ├── query Index data structures for annotated source code files and spans
│ ├── renaming Rename abstract syntax tree s.t. it can be reparsed
│ ├── syntax Syntax tree definitions
│ ├── elaborator Elaborating an untyped syntax tree into a typed syntax tree.
│ └── xfunc De-/Refunctionalization implementation
├── test Integration tests
│ ├── suites Test cases
Expand Down
28 changes: 14 additions & 14 deletions lang/elaborator/src/normalizer/eval.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,18 +14,18 @@ use crate::result::*;
pub trait Eval {
type Val;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError>;
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError>;
}

pub trait Apply {
fn apply(self, prg: &Prg, args: &[Rc<Val>]) -> Result<Rc<Val>, EvalError>;
fn apply(self, prg: &Prg, args: &[Rc<Val>]) -> Result<Rc<Val>, TypeError>;
}

impl Eval for Exp {
type Val = Rc<Val>;

#[trace("{:P} |- {:P} ▷ {return:P}", env, self, std::convert::identity)]
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let res = match self {
Exp::Var { idx, .. } => env.lookup(*idx),
Exp::TypCtor { info, name, args } => Rc::new(Val::TypCtor {
Expand Down Expand Up @@ -64,7 +64,7 @@ fn eval_dtor(
exp: Rc<Val>,
dtor_name: &str,
dtor_args: Vec<Rc<Val>>,
) -> Result<Rc<Val>, EvalError> {
) -> Result<Rc<Val>, TypeError> {
match (*exp).clone() {
Val::Ctor { name: ctor_name, args: ctor_args, info } => {
let type_decl = prg.decls.type_decl_for_member(&ctor_name, info)?;
Expand Down Expand Up @@ -101,7 +101,7 @@ fn eval_match(
match_name: &Label,
on_exp: Rc<Val>,
body: val::Match,
) -> Result<Rc<Val>, EvalError> {
) -> Result<Rc<Val>, TypeError> {
match (*on_exp).clone() {
Val::Ctor { name: ctor_name, args, .. } => beta_match(prg, body, &ctor_name, &args),
Val::Neu { exp } => Ok(Rc::new(Val::Neu {
Expand All @@ -117,7 +117,7 @@ fn beta_match(
body: val::Match,
ctor_name: &str,
args: &[Rc<Val>],
) -> Result<Rc<Val>, EvalError> {
) -> Result<Rc<Val>, TypeError> {
let case = body.clone().cases.into_iter().find(|case| case.name == ctor_name).unwrap();
let val::Case { body, .. } = case;
let body = body.unwrap();
Expand All @@ -130,7 +130,7 @@ fn beta_comatch(
body: val::Match,
dtor_name: &str,
args: &[Rc<Val>],
) -> Result<Rc<Val>, EvalError> {
) -> Result<Rc<Val>, TypeError> {
let cocase = body.clone().cases.into_iter().find(|cocase| cocase.name == dtor_name).unwrap();
let val::Case { body, .. } = cocase;
let body = body.unwrap();
Expand All @@ -140,7 +140,7 @@ fn beta_comatch(
impl Eval for ust::Match {
type Val = val::Match;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let ust::Match { info, cases, omit_absurd } = self;

Ok(val::Match { info: *info, cases: cases.eval(prg, env)?, omit_absurd: *omit_absurd })
Expand All @@ -150,7 +150,7 @@ impl Eval for ust::Match {
impl Eval for ust::Case {
type Val = val::Case;

fn eval(&self, _prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, _prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let ust::Case { info, name, args, body } = self;

let body = body.as_ref().map(|body| Closure {
Expand All @@ -166,7 +166,7 @@ impl Eval for ust::Case {
impl Eval for ust::TypApp {
type Val = val::TypApp;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let ust::TypApp { info, name, args } = self;

Ok(val::TypApp { info: *info, name: name.clone(), args: args.eval(prg, env)? })
Expand All @@ -176,29 +176,29 @@ impl Eval for ust::TypApp {
impl Eval for ust::Args {
type Val = Vec<Rc<Val>>;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
self.args.eval(prg, env)
}
}

impl Apply for Closure {
fn apply(mut self, prg: &Prg, args: &[Rc<Val>]) -> Result<Rc<Val>, EvalError> {
fn apply(mut self, prg: &Prg, args: &[Rc<Val>]) -> Result<Rc<Val>, TypeError> {
self.env.bind_iter(args.iter(), |env| self.body.eval(prg, env))
}
}

impl<T: Eval> Eval for Vec<T> {
type Val = Vec<T::Val>;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
self.iter().map(|x| x.eval(prg, env)).collect()
}
}

impl Eval for Rc<Exp> {
type Val = Rc<Val>;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, EvalError> {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
(**self).eval(prg, env)
}
}
6 changes: 3 additions & 3 deletions lang/elaborator/src/normalizer/normalize.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,9 @@ use crate::result::*;
pub trait Normalize {
type Nf;

fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result<Self::Nf, EvalError>;
fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result<Self::Nf, TypeError>;

fn normalize_in_empty_env(&self, prg: &ust::Prg) -> Result<Self::Nf, EvalError> {
fn normalize_in_empty_env(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
self.normalize(prg, &mut Env::empty())
}
}
Expand All @@ -22,7 +22,7 @@ where
{
type Nf = <<T as Eval>::Val as ReadBack>::Nf;

fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result<Self::Nf, EvalError> {
fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result<Self::Nf, TypeError> {
let val = self.eval(prg, env)?;
val.read_back(prg)
}
Expand Down
20 changes: 10 additions & 10 deletions lang/elaborator/src/normalizer/read_back.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,14 +14,14 @@ use crate::result::*;
pub trait ReadBack {
type Nf;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError>;
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError>;
}

impl ReadBack for val::Val {
type Nf = nf::Nf;

#[trace("↓{:P} ~> {return:P}", self, std::convert::identity)]
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let res = match self {
val::Val::TypCtor { info, name, args } => {
nf::Nf::TypCtor { info: *info, name: name.clone(), args: args.read_back(prg)? }
Expand All @@ -45,7 +45,7 @@ impl ReadBack for val::Val {
impl ReadBack for val::Neu {
type Nf = nf::Neu;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let res = match self {
val::Neu::Var { info, name, idx } => {
nf::Neu::Var { info: *info, name: name.clone(), idx: *idx }
Expand All @@ -71,7 +71,7 @@ impl ReadBack for val::Neu {
impl ReadBack for val::Match {
type Nf = nf::Match;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let val::Match { info, cases, omit_absurd } = self;
Ok(nf::Match { info: *info, cases: cases.read_back(prg)?, omit_absurd: *omit_absurd })
}
Expand All @@ -80,7 +80,7 @@ impl ReadBack for val::Match {
impl ReadBack for val::Case {
type Nf = nf::Case;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let val::Case { info, name, args, body } = self;

Ok(nf::Case {
Expand All @@ -95,7 +95,7 @@ impl ReadBack for val::Case {
impl ReadBack for val::TypApp {
type Nf = nf::TypApp;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let val::TypApp { info, name, args } = self;

Ok(nf::TypApp { info: *info, name: name.clone(), args: args.read_back(prg)? })
Expand All @@ -105,7 +105,7 @@ impl ReadBack for val::TypApp {
impl ReadBack for val::Closure {
type Nf = Rc<nf::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let args: Vec<Rc<val::Val>> = (0..self.n_args)
.rev()
.map(|snd| val::Val::Neu {
Expand All @@ -123,23 +123,23 @@ impl ReadBack for val::Closure {
impl<T: ReadBack> ReadBack for Vec<T> {
type Nf = Vec<T::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
self.iter().map(|x| x.read_back(prg)).collect()
}
}

impl<T: ReadBack> ReadBack for Rc<T> {
type Nf = Rc<T::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
(**self).read_back(prg).map(Rc::new)
}
}

impl<T: ReadBack> ReadBack for Option<T> {
type Nf = Option<T::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, EvalError> {
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
self.as_ref().map(|x| x.read_back(prg)).transpose()
}
}
78 changes: 25 additions & 53 deletions lang/elaborator/src/result.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,22 +12,6 @@ use syntax::ust;

use printer::PrintToString;

#[derive(Error, Diagnostic, Debug)]
pub enum EvalError {
#[error(transparent)]
#[diagnostic(transparent)]
Lookup(#[from] LookupError),
#[error("An unexpected internal error occurred: {message}")]
#[diagnostic(code("E-XXX"))]
/// This error should not occur.
/// Some internal invariant has been violated.
Impossible {
message: String,
#[label]
span: Option<SourceSpan>,
},
}

fn comma_separated<I: IntoIterator<Item = String>>(iter: I) -> String {
separated(", ", iter)
}
Expand Down Expand Up @@ -127,6 +111,31 @@ pub enum TypeError {
#[label]
span: Option<SourceSpan>,
},
#[error("{idx} occurs in {exp}")]
#[diagnostic(code("T-013"))]
OccursCheckFailed {
idx: Idx,
exp: String,
#[label]
span: Option<SourceSpan>,
},
#[error("Cannot unify annotated expression {exp}")]
#[diagnostic(code("T-014"))]
UnsupportedAnnotation {
exp: String,
#[label]
span: Option<SourceSpan>,
},
#[error("Cannot automatically decide whether {lhs} and {rhs} unify")]
#[diagnostic(code("T-015"))]
CannotDecide {
lhs: String,
rhs: String,
#[label]
lhs_span: Option<SourceSpan>,
#[label]
rhs_span: Option<SourceSpan>,
},
#[error("An unexpected internal error occurred: {message}")]
#[diagnostic(code("T-XXX"))]
/// This error should not occur.
Expand All @@ -138,12 +147,6 @@ pub enum TypeError {
},
#[error(transparent)]
#[diagnostic(transparent)]
Unify(#[from] UnifyError),
#[error(transparent)]
#[diagnostic(transparent)]
Eval(#[from] EvalError),
#[error(transparent)]
#[diagnostic(transparent)]
Lookup(#[from] LookupError),
}

Expand Down Expand Up @@ -181,38 +184,7 @@ impl TypeError {
pub fn expected_typ_app(got: Rc<nf::Nf>) -> Self {
Self::ExpectedTypApp { got: got.print_to_string(None), span: got.span().to_miette() }
}
}

#[derive(Error, Diagnostic, Debug)]
pub enum UnifyError {
#[error("{idx} occurs in {exp}")]
#[diagnostic(code("U-001"))]
OccursCheckFailed {
idx: Idx,
exp: String,
#[label]
span: Option<SourceSpan>,
},
#[error("Cannot unify annotated expression {exp}")]
#[diagnostic(code("U-002"))]
UnsupportedAnnotation {
exp: String,
#[label]
span: Option<SourceSpan>,
},
#[error("Cannot automatically decide whether {lhs} and {rhs} unify")]
#[diagnostic(code("U-003"))]
CannotDecide {
lhs: String,
rhs: String,
#[label]
lhs_span: Option<SourceSpan>,
#[label]
rhs_span: Option<SourceSpan>,
},
}

impl UnifyError {
pub fn occurs_check_failed(idx: Idx, exp: Rc<ust::Exp>) -> Self {
Self::OccursCheckFailed {
idx,
Expand Down
12 changes: 4 additions & 8 deletions lang/elaborator/src/typechecker/typecheck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -578,8 +578,7 @@ fn check_case(

let body_out = match body {
Some(body) => {
let unif = unify(ctx.levels(), eqns.clone())
.map_err(TypeError::Unify)?
let unif = unify(ctx.levels(), eqns.clone())?
.map_no(|()| TypeError::PatternIsAbsurd {
name: name.clone(),
span: info.to_miette(),
Expand All @@ -599,8 +598,7 @@ fn check_case(
})?
}
None => {
unify(ctx.levels(), eqns.clone())
.map_err(TypeError::Unify)?
unify(ctx.levels(), eqns.clone())?
.map_yes(|_| TypeError::PatternIsNotAbsurd {
name: name.clone(),
span: info.to_miette(),
Expand Down Expand Up @@ -637,8 +635,7 @@ fn check_cocase(
|ctx, args_out| {
let body_out = match body {
Some(body) => {
let unif = unify(ctx.levels(), eqns.clone())
.map_err(TypeError::Unify)?
let unif = unify(ctx.levels(), eqns.clone())?
.map_no(|()| TypeError::PatternIsAbsurd {
name: name.clone(),
span: info.to_miette(),
Expand All @@ -658,8 +655,7 @@ fn check_cocase(
})?
}
None => {
unify(ctx.levels(), eqns.clone())
.map_err(TypeError::Unify)?
unify(ctx.levels(), eqns.clone())?
.map_yes(|_| TypeError::PatternIsNotAbsurd {
name: name.clone(),
span: info.to_miette(),
Expand Down
Loading

0 comments on commit e12bb26

Please sign in to comment.