From e12bb26b972d3ed35c536445f5bb5c0e67a19e65 Mon Sep 17 00:00:00 2001 From: David Binder Date: Mon, 25 Mar 2024 14:50:22 +0100 Subject: [PATCH] Merge UnifyError, TypeError and EvalError --- README.md | 2 +- lang/elaborator/src/normalizer/eval.rs | 28 +++---- lang/elaborator/src/normalizer/normalize.rs | 6 +- lang/elaborator/src/normalizer/read_back.rs | 20 ++--- lang/elaborator/src/result.rs | 78 +++++++------------- lang/elaborator/src/typechecker/typecheck.rs | 12 +-- lang/elaborator/src/unifier/unify.rs | 24 +++--- lang/query/src/view/rt.rs | 6 +- 8 files changed, 71 insertions(+), 105 deletions(-) diff --git a/README.md b/README.md index a99ef383d..0be010aa5 100644 --- a/README.md +++ b/README.md @@ -49,6 +49,7 @@ 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 @@ -56,7 +57,6 @@ pol --help │ ├── 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 diff --git a/lang/elaborator/src/normalizer/eval.rs b/lang/elaborator/src/normalizer/eval.rs index 5d0df6b07..14707577f 100644 --- a/lang/elaborator/src/normalizer/eval.rs +++ b/lang/elaborator/src/normalizer/eval.rs @@ -14,18 +14,18 @@ use crate::result::*; pub trait Eval { type Val; - fn eval(&self, prg: &Prg, env: &mut Env) -> Result; + fn eval(&self, prg: &Prg, env: &mut Env) -> Result; } pub trait Apply { - fn apply(self, prg: &Prg, args: &[Rc]) -> Result, EvalError>; + fn apply(self, prg: &Prg, args: &[Rc]) -> Result, TypeError>; } impl Eval for Exp { type Val = Rc; #[trace("{:P} |- {:P} ▷ {return:P}", env, self, std::convert::identity)] - fn eval(&self, prg: &Prg, env: &mut Env) -> Result { + fn eval(&self, prg: &Prg, env: &mut Env) -> Result { let res = match self { Exp::Var { idx, .. } => env.lookup(*idx), Exp::TypCtor { info, name, args } => Rc::new(Val::TypCtor { @@ -64,7 +64,7 @@ fn eval_dtor( exp: Rc, dtor_name: &str, dtor_args: Vec>, -) -> Result, EvalError> { +) -> Result, 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)?; @@ -101,7 +101,7 @@ fn eval_match( match_name: &Label, on_exp: Rc, body: val::Match, -) -> Result, EvalError> { +) -> Result, 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 { @@ -117,7 +117,7 @@ fn beta_match( body: val::Match, ctor_name: &str, args: &[Rc], -) -> Result, EvalError> { +) -> Result, TypeError> { let case = body.clone().cases.into_iter().find(|case| case.name == ctor_name).unwrap(); let val::Case { body, .. } = case; let body = body.unwrap(); @@ -130,7 +130,7 @@ fn beta_comatch( body: val::Match, dtor_name: &str, args: &[Rc], -) -> Result, EvalError> { +) -> Result, TypeError> { let cocase = body.clone().cases.into_iter().find(|cocase| cocase.name == dtor_name).unwrap(); let val::Case { body, .. } = cocase; let body = body.unwrap(); @@ -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 { + fn eval(&self, prg: &Prg, env: &mut Env) -> Result { let ust::Match { info, cases, omit_absurd } = self; Ok(val::Match { info: *info, cases: cases.eval(prg, env)?, omit_absurd: *omit_absurd }) @@ -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 { + fn eval(&self, _prg: &Prg, env: &mut Env) -> Result { let ust::Case { info, name, args, body } = self; let body = body.as_ref().map(|body| Closure { @@ -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 { + fn eval(&self, prg: &Prg, env: &mut Env) -> Result { let ust::TypApp { info, name, args } = self; Ok(val::TypApp { info: *info, name: name.clone(), args: args.eval(prg, env)? }) @@ -176,13 +176,13 @@ impl Eval for ust::TypApp { impl Eval for ust::Args { type Val = Vec>; - fn eval(&self, prg: &Prg, env: &mut Env) -> Result { + fn eval(&self, prg: &Prg, env: &mut Env) -> Result { self.args.eval(prg, env) } } impl Apply for Closure { - fn apply(mut self, prg: &Prg, args: &[Rc]) -> Result, EvalError> { + fn apply(mut self, prg: &Prg, args: &[Rc]) -> Result, TypeError> { self.env.bind_iter(args.iter(), |env| self.body.eval(prg, env)) } } @@ -190,7 +190,7 @@ impl Apply for Closure { impl Eval for Vec { type Val = Vec; - fn eval(&self, prg: &Prg, env: &mut Env) -> Result { + fn eval(&self, prg: &Prg, env: &mut Env) -> Result { self.iter().map(|x| x.eval(prg, env)).collect() } } @@ -198,7 +198,7 @@ impl Eval for Vec { impl Eval for Rc { type Val = Rc; - fn eval(&self, prg: &Prg, env: &mut Env) -> Result { + fn eval(&self, prg: &Prg, env: &mut Env) -> Result { (**self).eval(prg, env) } } diff --git a/lang/elaborator/src/normalizer/normalize.rs b/lang/elaborator/src/normalizer/normalize.rs index 5a9895a31..1c3a3ab4c 100644 --- a/lang/elaborator/src/normalizer/normalize.rs +++ b/lang/elaborator/src/normalizer/normalize.rs @@ -8,9 +8,9 @@ use crate::result::*; pub trait Normalize { type Nf; - fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result; + fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result; - fn normalize_in_empty_env(&self, prg: &ust::Prg) -> Result { + fn normalize_in_empty_env(&self, prg: &ust::Prg) -> Result { self.normalize(prg, &mut Env::empty()) } } @@ -22,7 +22,7 @@ where { type Nf = <::Val as ReadBack>::Nf; - fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result { + fn normalize(&self, prg: &ust::Prg, env: &mut Env) -> Result { let val = self.eval(prg, env)?; val.read_back(prg) } diff --git a/lang/elaborator/src/normalizer/read_back.rs b/lang/elaborator/src/normalizer/read_back.rs index 383424edc..d4cbc5d93 100644 --- a/lang/elaborator/src/normalizer/read_back.rs +++ b/lang/elaborator/src/normalizer/read_back.rs @@ -14,14 +14,14 @@ use crate::result::*; pub trait ReadBack { type Nf; - fn read_back(&self, prg: &Prg) -> Result; + fn read_back(&self, prg: &Prg) -> Result; } impl ReadBack for val::Val { type Nf = nf::Nf; #[trace("↓{:P} ~> {return:P}", self, std::convert::identity)] - fn read_back(&self, prg: &Prg) -> Result { + fn read_back(&self, prg: &Prg) -> Result { let res = match self { val::Val::TypCtor { info, name, args } => { nf::Nf::TypCtor { info: *info, name: name.clone(), args: args.read_back(prg)? } @@ -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 { + fn read_back(&self, prg: &Prg) -> Result { let res = match self { val::Neu::Var { info, name, idx } => { nf::Neu::Var { info: *info, name: name.clone(), idx: *idx } @@ -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 { + fn read_back(&self, prg: &Prg) -> Result { let val::Match { info, cases, omit_absurd } = self; Ok(nf::Match { info: *info, cases: cases.read_back(prg)?, omit_absurd: *omit_absurd }) } @@ -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 { + fn read_back(&self, prg: &Prg) -> Result { let val::Case { info, name, args, body } = self; Ok(nf::Case { @@ -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 { + fn read_back(&self, prg: &Prg) -> Result { let val::TypApp { info, name, args } = self; Ok(nf::TypApp { info: *info, name: name.clone(), args: args.read_back(prg)? }) @@ -105,7 +105,7 @@ impl ReadBack for val::TypApp { impl ReadBack for val::Closure { type Nf = Rc; - fn read_back(&self, prg: &Prg) -> Result { + fn read_back(&self, prg: &Prg) -> Result { let args: Vec> = (0..self.n_args) .rev() .map(|snd| val::Val::Neu { @@ -123,7 +123,7 @@ impl ReadBack for val::Closure { impl ReadBack for Vec { type Nf = Vec; - fn read_back(&self, prg: &Prg) -> Result { + fn read_back(&self, prg: &Prg) -> Result { self.iter().map(|x| x.read_back(prg)).collect() } } @@ -131,7 +131,7 @@ impl ReadBack for Vec { impl ReadBack for Rc { type Nf = Rc; - fn read_back(&self, prg: &Prg) -> Result { + fn read_back(&self, prg: &Prg) -> Result { (**self).read_back(prg).map(Rc::new) } } @@ -139,7 +139,7 @@ impl ReadBack for Rc { impl ReadBack for Option { type Nf = Option; - fn read_back(&self, prg: &Prg) -> Result { + fn read_back(&self, prg: &Prg) -> Result { self.as_ref().map(|x| x.read_back(prg)).transpose() } } diff --git a/lang/elaborator/src/result.rs b/lang/elaborator/src/result.rs index f7c036b4b..dae4cd7c4 100644 --- a/lang/elaborator/src/result.rs +++ b/lang/elaborator/src/result.rs @@ -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, - }, -} - fn comma_separated>(iter: I) -> String { separated(", ", iter) } @@ -127,6 +111,31 @@ pub enum TypeError { #[label] span: Option, }, + #[error("{idx} occurs in {exp}")] + #[diagnostic(code("T-013"))] + OccursCheckFailed { + idx: Idx, + exp: String, + #[label] + span: Option, + }, + #[error("Cannot unify annotated expression {exp}")] + #[diagnostic(code("T-014"))] + UnsupportedAnnotation { + exp: String, + #[label] + span: Option, + }, + #[error("Cannot automatically decide whether {lhs} and {rhs} unify")] + #[diagnostic(code("T-015"))] + CannotDecide { + lhs: String, + rhs: String, + #[label] + lhs_span: Option, + #[label] + rhs_span: Option, + }, #[error("An unexpected internal error occurred: {message}")] #[diagnostic(code("T-XXX"))] /// This error should not occur. @@ -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), } @@ -181,38 +184,7 @@ impl TypeError { pub fn expected_typ_app(got: Rc) -> 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, - }, - #[error("Cannot unify annotated expression {exp}")] - #[diagnostic(code("U-002"))] - UnsupportedAnnotation { - exp: String, - #[label] - span: Option, - }, - #[error("Cannot automatically decide whether {lhs} and {rhs} unify")] - #[diagnostic(code("U-003"))] - CannotDecide { - lhs: String, - rhs: String, - #[label] - lhs_span: Option, - #[label] - rhs_span: Option, - }, -} -impl UnifyError { pub fn occurs_check_failed(idx: Idx, exp: Rc) -> Self { Self::OccursCheckFailed { idx, diff --git a/lang/elaborator/src/typechecker/typecheck.rs b/lang/elaborator/src/typechecker/typecheck.rs index 28f1a18ea..3ab4144d4 100644 --- a/lang/elaborator/src/typechecker/typecheck.rs +++ b/lang/elaborator/src/typechecker/typecheck.rs @@ -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(), @@ -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(), @@ -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(), @@ -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(), diff --git a/lang/elaborator/src/unifier/unify.rs b/lang/elaborator/src/unifier/unify.rs index 664973df8..fa81a8795 100644 --- a/lang/elaborator/src/unifier/unify.rs +++ b/lang/elaborator/src/unifier/unify.rs @@ -2,7 +2,7 @@ use std::rc::Rc; use syntax::ctx::LevelCtx; -use crate::result::UnifyError; +use crate::result::TypeError; use crate::unifier::dec::{Dec, No, Yes}; use printer::{DocAllocator, Print}; use syntax::common::*; @@ -75,7 +75,7 @@ impl Unificator { } } -pub fn unify(ctx: LevelCtx, eqns: Vec) -> Result, UnifyError> { +pub fn unify(ctx: LevelCtx, eqns: Vec) -> Result, TypeError> { let mut ctx = Ctx::new(eqns.clone(), ctx.clone()); let res = match ctx.unify()? { Yes(_) => Yes(ctx.unif), @@ -96,7 +96,7 @@ impl Ctx { Self { eqns, done: HashSet::default(), ctx, unif: Unificator::empty() } } - fn unify(&mut self) -> Result { + fn unify(&mut self) -> Result { while let Some(eqn) = self.eqns.pop() { match self.unify_eqn(&eqn)? { Yes(_) => { @@ -109,7 +109,7 @@ impl Ctx { Ok(Yes(())) } - fn unify_eqn(&mut self, eqn: &Eqn) -> Result { + fn unify_eqn(&mut self, eqn: &Eqn) -> Result { use generic::Exp::*; let Eqn { lhs, rhs, .. } = eqn; @@ -140,21 +140,21 @@ impl Ctx { self.unify_args(args, args2) } (Type { .. }, Type { .. }) => Ok(Yes(())), - (Anno { .. }, _) => Err(UnifyError::unsupported_annotation(lhs.clone())), - (_, Anno { .. }) => Err(UnifyError::unsupported_annotation(rhs.clone())), - (_, _) => Err(UnifyError::cannot_decide(lhs.clone(), rhs.clone())), + (Anno { .. }, _) => Err(TypeError::unsupported_annotation(lhs.clone())), + (_, Anno { .. }) => Err(TypeError::unsupported_annotation(rhs.clone())), + (_, _) => Err(TypeError::cannot_decide(lhs.clone(), rhs.clone())), } } - fn unify_args(&mut self, lhs: &ust::Args, rhs: &ust::Args) -> Result { + fn unify_args(&mut self, lhs: &ust::Args, rhs: &ust::Args) -> Result { let new_eqns = lhs.args.iter().cloned().zip(rhs.args.iter().cloned()).map(Eqn::from); self.add_equations(new_eqns)?; Ok(Yes(())) } - fn add_assignment(&mut self, idx: Idx, exp: Rc) -> Result { + fn add_assignment(&mut self, idx: Idx, exp: Rc) -> Result { if ust::occurs_in(&mut self.ctx, idx, &exp) { - return Err(UnifyError::occurs_check_failed(idx, exp)); + return Err(TypeError::occurs_check_failed(idx, exp)); } let insert_lvl = self.ctx.idx_to_lvl(idx); let exp = exp.subst(&mut self.ctx, &self.unif); @@ -171,11 +171,11 @@ impl Ctx { } } - fn add_equation(&mut self, eqn: Eqn) -> Result { + fn add_equation(&mut self, eqn: Eqn) -> Result { self.add_equations([eqn]) } - fn add_equations>(&mut self, iter: I) -> Result { + fn add_equations>(&mut self, iter: I) -> Result { self.eqns.extend(iter.into_iter().filter(|eqn| !self.done.contains(eqn))); Ok(Yes(())) } diff --git a/lang/query/src/view/rt.rs b/lang/query/src/view/rt.rs index ca7b43487..7cb4b71db 100644 --- a/lang/query/src/view/rt.rs +++ b/lang/query/src/view/rt.rs @@ -2,7 +2,7 @@ use std::rc::Rc; use super::DatabaseView; -use normalizer::normalize::Normalize; +use elaborator::normalizer::normalize::Normalize; use parser::cst; use syntax::{nf, tst, ust}; @@ -41,9 +41,7 @@ impl<'a> DatabaseView<'a> { match main { Some(exp) => { - let nf = exp - .normalize_in_empty_env(&ust) - .map_err(|err| Error::Type(typechecker::TypeError::Eval(err)))?; + let nf = exp.normalize_in_empty_env(&ust)?; Ok(Some(nf)) } None => Ok(None),