From 2f6ce455ec512f3b0cfff0f3ca9c5016e6a4e9de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Wed, 13 Nov 2024 18:46:42 +0100 Subject: [PATCH] Support normalizing definitions from other modules (#370) * Support normalizing definitions from other modules * Fix URI scheme change --- examples/boolrep.pol | 26 ++- lang/ast/src/ctx/def.rs | 2 +- lang/ast/src/decls.rs | 23 +-- lang/driver/src/database.rs | 39 +++-- lang/driver/src/xfunc.rs | 22 ++- lang/elaborator/src/normalizer/env.rs | 43 +++-- lang/elaborator/src/normalizer/eval.rs | 156 +++++++++--------- lang/elaborator/src/normalizer/normalize.rs | 31 ++-- lang/elaborator/src/normalizer/val.rs | 101 ++++++------ lang/elaborator/src/typechecker/ctx.rs | 14 +- .../src/typechecker/decls/codefinition.rs | 5 +- .../src/typechecker/decls/definition.rs | 7 +- .../src/typechecker/decls/global_let.rs | 5 +- lang/elaborator/src/typechecker/exprs/anno.rs | 2 +- lang/elaborator/src/typechecker/exprs/call.rs | 7 +- .../src/typechecker/exprs/dot_call.rs | 4 +- .../src/typechecker/exprs/local_comatch.rs | 19 ++- .../src/typechecker/exprs/local_match.rs | 16 +- lang/elaborator/src/typechecker/exprs/mod.rs | 8 +- .../src/typechecker/type_info_table/build.rs | 22 +-- .../src/typechecker/type_info_table/lookup.rs | 14 +- .../src/typechecker/type_info_table/mod.rs | 45 ++--- test/test-runner/src/phases.rs | 5 +- 23 files changed, 299 insertions(+), 317 deletions(-) diff --git a/examples/boolrep.pol b/examples/boolrep.pol index 565536a9f9..c6b7a2cd35 100644 --- a/examples/boolrep.pol +++ b/examples/boolrep.pol @@ -1,28 +1,24 @@ -data Bool { T, F } - -def Bool.not: Bool { - T => F, - F => T -} +use "../std/data/bool.pol" data BoolRep(x: Bool) { TrueRep: BoolRep(T), - FalseRep: BoolRep(F) + FalseRep: BoolRep(F), } def BoolRep(x).extract(x: Bool): Bool { TrueRep => T, - FalseRep => F + FalseRep => F, } data Top { Unit } -def Top.flipRep(x: Bool, rep: BoolRep(x)): BoolRep(x.not) { - Unit => - rep.match { - TrueRep => FalseRep, - FalseRep => TrueRep - } +def Top.flipRep(x: Bool, rep: BoolRep(x)): BoolRep(x.neg) { + Unit => rep.match { + TrueRep => FalseRep, + FalseRep => TrueRep, + } } -def Top.example: Bool { Unit => Unit.flipRep(T, TrueRep).extract(F) } +def Top.example: Bool { + Unit => Unit.flipRep(T, TrueRep).extract(F) +} \ No newline at end of file diff --git a/lang/ast/src/ctx/def.rs b/lang/ast/src/ctx/def.rs index b3ded50b3b..a8b3742a30 100644 --- a/lang/ast/src/ctx/def.rs +++ b/lang/ast/src/ctx/def.rs @@ -91,7 +91,7 @@ pub trait Context: Sized { /// Interface to bind variables to anything that has a `Context` /// -/// There are two use cases for this trait. +/// There are two ways to use this trait. /// /// Case 1: You have a type that implements `Context`. /// Then, a blanket impl ensures that this type also implements `BindContext`. diff --git a/lang/ast/src/decls.rs b/lang/ast/src/decls.rs index a7c840b1e2..ae4dbbb529 100644 --- a/lang/ast/src/decls.rs +++ b/lang/ast/src/decls.rs @@ -231,31 +231,10 @@ impl Module { out } - pub fn lookup_decl(&self, name: &IdBind) -> Option<&Decl> { + pub fn lookup_decl(&self, name: &IdBound) -> Option<&Decl> { self.decls.iter().find(|decl| decl.ident() == name) } - pub fn lookup_let(&self, name: &IdBind) -> Option<&Let> { - self.decls.iter().find_map(|decl| match decl { - Decl::Let(tl_let) if tl_let.name == *name => Some(tl_let), - _ => None, - }) - } - - pub fn lookup_def(&self, name: &IdBind) -> Option<&Def> { - self.decls.iter().find_map(|decl| match decl { - Decl::Def(def) if def.name == *name => Some(def), - _ => None, - }) - } - - pub fn lookup_codef(&self, name: &IdBind) -> Option<&Codef> { - self.decls.iter().find_map(|decl| match decl { - Decl::Codef(codef) if codef.name == *name => Some(codef), - _ => None, - }) - } - pub fn find_main(&self) -> Option> { self.decls.iter().find_map(|decl| match decl { Decl::Let(tl_let) if tl_let.is_main() => Some(tl_let.body.clone()), diff --git a/lang/driver/src/database.rs b/lang/driver/src/database.rs index 63e5aeaaec..bd1213ad9d 100644 --- a/lang/driver/src/database.rs +++ b/lang/driver/src/database.rs @@ -36,7 +36,7 @@ pub struct Database { /// The typechecked AST of a module pub ast: Cache, Error>>, /// The type info table constructed during typechecking - pub type_info_table: Cache, + pub module_type_info_table: Cache, /// Hover information for spans pub info_by_id: Cache>, /// Spans of top-level items @@ -179,8 +179,23 @@ impl Database { // // - pub fn type_info_table(&mut self, uri: &Url) -> Result { - match self.type_info_table.get_unless_stale(uri) { + pub fn type_info_table(&mut self, uri: &Url) -> Result { + let deps = self.deps(uri)?; + + // Compute the type info table + let mut info_table = TypeInfoTable::default(); + let mod_info_table = self.module_type_info_table(uri)?; + info_table.insert(uri.clone(), mod_info_table); + for dep_url in deps { + let mod_info_table = self.module_type_info_table(&dep_url)?; + info_table.insert(dep_url.clone(), mod_info_table); + } + + Ok(info_table) + } + + pub fn module_type_info_table(&mut self, uri: &Url) -> Result { + match self.module_type_info_table.get_unless_stale(uri) { Some(table) => { log::debug!("Found type info table in cache: {}", uri); Ok(table.clone()) @@ -193,7 +208,7 @@ impl Database { log::debug!("Recomputing type info table for: {}", uri); let ust = self.ust(uri)?; let info_table = build_type_info_table(&ust); - self.type_info_table.insert(uri.clone(), info_table.clone()); + self.module_type_info_table.insert(uri.clone(), info_table.clone()); Ok(info_table) } @@ -213,16 +228,9 @@ impl Database { pub fn recompute_ast(&mut self, uri: &Url) -> Result, Error> { log::debug!("Recomputing ast for: {}", uri); - let deps = self.deps(uri)?; // Compute the type info table - let mut info_table = TypeInfoTable::default(); - let mod_info_table = self.type_info_table(uri)?; - info_table.insert(uri.clone(), mod_info_table); - for dep_url in deps { - let mod_info_table = self.type_info_table(&dep_url)?; - info_table.insert(dep_url.clone(), mod_info_table); - } + let info_table = self.type_info_table(uri)?; // Typecheck module let ust = self.ust(uri).map(|x| (*x).clone())?; @@ -315,7 +323,7 @@ impl Database { symbol_table: Cache::default(), ust: Cache::default(), ast: Cache::default(), - type_info_table: Cache::default(), + module_type_info_table: Cache::default(), info_by_id: Cache::default(), item_by_id: Cache::default(), } @@ -358,7 +366,7 @@ impl Database { self.symbol_table.invalidate(uri); self.ust.invalidate(uri); self.ast.invalidate(uri); - self.type_info_table.invalidate(uri); + self.module_type_info_table.invalidate(uri); self.info_by_id.invalidate(uri); self.item_by_id.invalidate(uri); } @@ -367,10 +375,11 @@ impl Database { let ast = self.ast(uri)?; let main = ast.find_main(); + let info_table = self.type_info_table(uri)?; match main { Some(exp) => { - let nf = exp.normalize_in_empty_env(&ast)?; + let nf = exp.normalize_in_empty_env(&Rc::new(info_table))?; Ok(Some(nf)) } None => Ok(None), diff --git a/lang/driver/src/xfunc.rs b/lang/driver/src/xfunc.rs index 1663d59314..34ea409363 100644 --- a/lang/driver/src/xfunc.rs +++ b/lang/driver/src/xfunc.rs @@ -4,7 +4,6 @@ use transformations::LiftResult; use transformations::Rename; use ast::*; -use lowering::DeclMeta; use parser::cst; use transformations::matrix; use transformations::result::XfuncError; @@ -20,14 +19,16 @@ pub struct Xfunc { } impl Database { - pub fn all_type_names(&mut self, uri: &Url) -> Result, crate::Error> { - let symbol_table = self.symbol_table(uri)?; - Ok(symbol_table + pub fn all_declared_type_names(&mut self, uri: &Url) -> Result, crate::Error> { + let ust = self.cst(uri)?; + Ok(ust + .decls .iter() - .filter(|(_, decl_meta)| { - matches!(decl_meta, DeclMeta::Data { .. } | DeclMeta::Codata { .. }) + .filter_map(|decl| match decl { + cst::decls::Decl::Data(data) => Some(data.name.clone()), + cst::decls::Decl::Codata(codata) => Some(codata.name.clone()), + _ => None, }) - .map(|(name, _)| name.clone()) .collect()) } @@ -95,7 +96,8 @@ fn generate_edits( // Here we rewrite the entire (co)data declaration and its associated (co)definitions let new_items = Module { uri: module.uri.clone(), - use_decls: module.use_decls.clone(), + // Use declarations don't change, and we are only printing an excerpt of the module + use_decls: vec![], decls: new_decls, meta_vars: module.meta_vars.clone(), }; @@ -106,7 +108,9 @@ fn generate_edits( // Edits for all other declarations that have been touched // Here we surgically rewrite only the declarations that have been changed for name in dirty_decls { - let decl = module.lookup_decl(&name).unwrap(); + let decl = module + .lookup_decl(&IdBound { span: None, id: name.id.clone(), uri: module.uri.clone() }) + .unwrap(); let mut decl = decl.clone(); decl.rename(); let span = original.decl_spans[&name]; diff --git a/lang/elaborator/src/normalizer/env.rs b/lang/elaborator/src/normalizer/env.rs index badf5b8a5f..3145423a4e 100644 --- a/lang/elaborator/src/normalizer/env.rs +++ b/lang/elaborator/src/normalizer/env.rs @@ -15,21 +15,16 @@ use crate::normalizer::val::*; #[derive(Debug, Clone, Derivative)] #[derivative(Eq, PartialEq, Hash)] pub struct Env { - ctx: GenericCtx>, -} - -impl From>> for Env { - fn from(value: GenericCtx>) -> Self { - Env { ctx: value } - } + /// Environment for locally bound variables + bound_vars: GenericCtx>, } impl Context for Env { type Elem = Box; fn lookup>(&self, idx: V) -> Self::Elem { - let lvl = self.ctx.var_to_lvl(idx.into()); - self.ctx + let lvl = self.bound_vars.var_to_lvl(idx.into()); + self.bound_vars .bound .get(lvl.fst) .and_then(|ctx| ctx.get(lvl.snd)) @@ -38,15 +33,15 @@ impl Context for Env { } fn push_telescope(&mut self) { - self.ctx.bound.push(vec![]); + self.bound_vars.bound.push(vec![]); } fn pop_telescope(&mut self) { - self.ctx.bound.pop().unwrap(); + self.bound_vars.bound.pop().unwrap(); } fn push_binder(&mut self, elem: Self::Elem) { - self.ctx + self.bound_vars .bound .last_mut() .expect("Cannot push without calling push_telescope first") @@ -55,7 +50,7 @@ impl Context for Env { fn pop_binder(&mut self, _elem: Self::Elem) { let err = "Cannot pop from empty context"; - self.ctx.bound.last_mut().expect(err).pop().expect(err); + self.bound_vars.bound.last_mut().expect(err).pop().expect(err); } } @@ -66,11 +61,19 @@ impl ContextElem for &Box { } impl Env { + pub fn empty() -> Self { + Self { bound_vars: GenericCtx::empty() } + } + + pub fn from_vec(bound: Vec>>) -> Self { + Self { bound_vars: GenericCtx::from(bound) } + } + pub(super) fn for_each(&mut self, f: F) where F: Fn(&mut Box), { - for outer in self.ctx.bound.iter_mut() { + for outer in self.bound_vars.bound.iter_mut() { for inner in outer { f(inner) } @@ -78,12 +81,6 @@ impl Env { } } -impl From>>> for Env { - fn from(bound: Vec>>) -> Self { - Self { ctx: bound.into() } - } -} - impl Shift for Env { fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { self.for_each(|val| val.shift_in_range(range, by)) @@ -115,7 +112,7 @@ impl ToEnv for LevelCtx { }) .collect(); - Env::from(bound) + Env::from_vec(bound) } } @@ -133,7 +130,7 @@ impl ToEnv for TypeCtx { }) .collect(); - Env::from(bound) + Env::from_vec(bound) } } @@ -143,7 +140,7 @@ impl Print for Env { cfg: &printer::PrintCfg, alloc: &'a printer::Alloc<'a>, ) -> printer::Builder<'a> { - let iter = self.ctx.iter().map(|ctx| { + let iter = self.bound_vars.iter().map(|ctx| { alloc .intersperse(ctx.iter().map(|typ| typ.print(cfg, alloc)), alloc.text(COMMA)) .brackets() diff --git a/lang/elaborator/src/normalizer/eval.rs b/lang/elaborator/src/normalizer/eval.rs index 2e8260c378..0bd977b1d3 100644 --- a/lang/elaborator/src/normalizer/eval.rs +++ b/lang/elaborator/src/normalizer/eval.rs @@ -1,39 +1,44 @@ +use std::rc::Rc; + use log::trace; -use ast::ctx::{BindContext, Context, GenericCtx}; +use ast::ctx::{BindContext, Context}; use ast::*; -use miette_util::ToMiette; use printer::types::Print; use crate::normalizer::env::*; use crate::normalizer::val::{self, Closure, Val}; -use crate::result::*; +use crate::{result::*, TypeInfoTable}; pub trait Eval { type Val; - fn eval(&self, prg: &Module, env: &mut Env) -> Result; + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result; } pub trait Apply { - fn apply(self, prg: &Module, args: &[Box]) -> Result, TypeError>; + fn apply( + self, + info_table: &Rc, + args: &[Box], + ) -> Result, TypeError>; } impl Eval for Exp { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let e = match self { - Exp::Variable(e) => e.eval(prg, env), - Exp::TypCtor(e) => e.eval(prg, env), - Exp::Call(e) => e.eval(prg, env), - Exp::DotCall(e) => e.eval(prg, env), - Exp::Anno(e) => e.eval(prg, env), - Exp::TypeUniv(e) => e.eval(prg, env), - Exp::LocalMatch(e) => e.eval(prg, env), - Exp::LocalComatch(e) => e.eval(prg, env), - Exp::Hole(e) => e.eval(prg, env), + Exp::Variable(e) => e.eval(info_table, env), + Exp::TypCtor(e) => e.eval(info_table, env), + Exp::Call(e) => e.eval(info_table, env), + Exp::DotCall(e) => e.eval(info_table, env), + Exp::Anno(e) => e.eval(info_table, env), + Exp::TypeUniv(e) => e.eval(info_table, env), + Exp::LocalMatch(e) => e.eval(info_table, env), + Exp::LocalComatch(e) => e.eval(info_table, env), + Exp::Hole(e) => e.eval(info_table, env), }; trace!( "{} |- {} ▷ {}", @@ -48,7 +53,7 @@ impl Eval for Exp { impl Eval for Variable { type Val = Box; - fn eval(&self, _prg: &Module, env: &mut Env) -> Result { + fn eval(&self, _info_table: &Rc, env: &mut Env) -> Result { let Variable { idx, .. } = self; Ok(env.lookup(*idx)) } @@ -57,10 +62,11 @@ impl Eval for Variable { impl Eval for TypCtor { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let TypCtor { span, name, args } = self; Ok(Box::new( - val::TypCtor { span: *span, name: name.clone(), args: args.eval(prg, env)? }.into(), + val::TypCtor { span: *span, name: name.clone(), args: args.eval(info_table, env)? } + .into(), )) } } @@ -68,28 +74,24 @@ impl Eval for TypCtor { impl Eval for Call { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let Call { span, name, kind, args, .. } = self; match kind { CallKind::LetBound => { - let Let { attr, body, .. } = - prg.lookup_let(&name.clone().into()).ok_or_else(|| TypeError::Impossible { - message: format!("Top-level let {name} not found"), - span: span.to_miette(), - })?; + let Let { attr, body, .. } = info_table.lookup_let(name)?; // We now have to distinguish two cases: // If the let-bound definition is transparent, then we substitute the // arguments for the body of the definition. If it is opaque, then // the further computation is blocked so we return a neutral value. if attr.attrs.contains(&Attribute::Transparent) { - let args = args.eval(prg, env)?; - return env.bind_iter(args.to_vals().iter(), |env| body.eval(prg, env)); + let args = args.eval(info_table, env)?; + return env.bind_iter(args.to_vals().iter(), |env| body.eval(info_table, env)); } else { Ok(Box::new(Val::Neu( val::OpaqueCall { span: *span, name: name.clone(), - args: args.eval(prg, env)?, + args: args.eval(info_table, env)?, } .into(), ))) @@ -100,7 +102,7 @@ impl Eval for Call { span: *span, kind: *kind, name: name.clone(), - args: args.eval(prg, env)?, + args: args.eval(info_table, env)?, } .into(), )), @@ -120,12 +122,12 @@ impl Eval for DotCall { /// ┃ ┗━━━━━━━━━━━━ name /// ┗━━━━━━━━━━━━━━ exp /// ``` - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let DotCall { span, kind, exp, name, args, .. } = self; // We first evaluate `exp` and then the arguments `args` to `d` from left to right. - let exp = exp.eval(prg, env)?; - let args = args.eval(prg, env)?; + let exp = exp.eval(info_table, env)?; + let args = args.eval(info_table, env)?; match (*exp).clone() { Val::Call(val::Call { name: call_name, kind, args: call_args, .. }) => { @@ -146,16 +148,10 @@ impl Eval for DotCall { // data type, and `d` is the name of a toplevel definition. // First, we have to find the corresponding case in the toplevel definition `d`. - let Def { cases, .. } = - prg.lookup_def(&name.clone().into()).ok_or_else(|| { - TypeError::Impossible { - message: format!("Definition {name} not found"), - span: None, - } - })?; - let mut env: Env = GenericCtx::empty().into(); - let cases = - env.bind_iter(args.to_vals().iter(), |env| cases.eval(prg, env))?; + let Def { cases, .. } = info_table.lookup_def(&name.clone())?; + let mut env = Env::empty(); + let cases = env + .bind_iter(args.to_vals().iter(), |env| cases.eval(info_table, env))?; let val::Case { body, .. } = cases .clone() .into_iter() @@ -163,7 +159,7 @@ impl Eval for DotCall { .ok_or_else(|| TypeError::MissingCase { name: call_name.id.clone() })?; // Then we apply the body to the `call_args`. - body.clone().unwrap().apply(prg, &call_args.to_vals()) + body.clone().unwrap().apply(info_table, &call_args.to_vals()) } CallKind::Codefinition => { // The specific instance of the DotCall we are evaluating is: @@ -182,15 +178,11 @@ impl Eval for DotCall { // First, we have to find the corresponding cocase in the toplevel // codefinition `C`. - let Codef { cases, .. } = prg - .lookup_codef(&call_name.clone().into()) - .ok_or_else(|| TypeError::Impossible { - message: format!("Codefinition {call_name} not found"), - span: None, - })?; - let mut env: Env = GenericCtx::empty().into(); - let cases = - env.bind_iter(call_args.to_vals().iter(), |env| cases.eval(prg, env))?; + let Codef { cases, .. } = info_table.lookup_codef(&call_name.clone())?; + let mut env = Env::empty(); + let cases = env.bind_iter(call_args.to_vals().iter(), |env| { + cases.eval(info_table, env) + })?; let val::Case { body, .. } = cases .clone() .into_iter() @@ -198,7 +190,7 @@ impl Eval for DotCall { .ok_or_else(|| TypeError::MissingCocase { name: name.id.clone() })?; // Then we apply the body to the `args`. - body.clone().unwrap().apply(prg, &args.to_vals()) + body.clone().unwrap().apply(info_table, &args.to_vals()) } CallKind::LetBound => { // This case is unreachable because all let-bound calls have either already @@ -230,7 +222,7 @@ impl Eval for DotCall { .ok_or_else(|| TypeError::MissingCocase { name: name.id.clone() })?; // Then we apply the body to the `args`. - body.clone().unwrap().apply(prg, &args.to_vals()) + body.clone().unwrap().apply(info_table, &args.to_vals()) } Val::Neu(exp) => { // The specific instance of the DotCall we are evaluating is: @@ -262,16 +254,20 @@ impl Eval for DotCall { impl Eval for Anno { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let Anno { exp, .. } = self; - exp.eval(prg, env) + exp.eval(info_table, env) } } impl Eval for TypeUniv { type Val = Box; - fn eval(&self, _prg: &Module, _env: &mut Env) -> Result { + fn eval( + &self, + _info_table: &Rc, + _env: &mut Env, + ) -> Result { let TypeUniv { span } = self; Ok(Box::new(val::TypeUniv { span: *span }.into())) } @@ -288,11 +284,11 @@ impl Eval for LocalMatch { /// ┃ ┗━━━━ cases /// ┗━━━━━━━━━━━━━━━ on_exp /// ``` - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let LocalMatch { name: match_name, on_exp, cases, .. } = self; // We first evaluate `on_exp` and `cases` - let on_exp = on_exp.eval(prg, env)?; - let cases = cases.eval(prg, env)?; + let on_exp = on_exp.eval(info_table, env)?; + let cases = cases.eval(info_table, env)?; match (*on_exp).clone() { Val::Call(val::Call { name: ctor_name, args, .. }) => { @@ -316,7 +312,7 @@ impl Eval for LocalMatch { .ok_or_else(|| TypeError::MissingCase { name: ctor_name.id.clone() })?; // Then we substitute the `args` in the body. - body.clone().unwrap().apply(prg, &args.to_vals()) + body.clone().unwrap().apply(info_table, &args.to_vals()) } Val::Neu(exp) => { // The specific instance of the LocalMatch we are evaluating is: @@ -346,14 +342,14 @@ impl Eval for LocalMatch { impl Eval for LocalComatch { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let LocalComatch { span, name, is_lambda_sugar, cases, .. } = self; Ok(Box::new( val::LocalComatch { span: *span, name: name.clone(), is_lambda_sugar: *is_lambda_sugar, - cases: cases.eval(prg, env)?, + cases: cases.eval(info_table, env)?, } .into(), )) @@ -363,9 +359,9 @@ impl Eval for LocalComatch { impl Eval for Hole { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { let Hole { span, kind, metavar, args, .. } = self; - let args = args.eval(prg, env)?; + let args = args.eval(info_table, env)?; Ok(Box::new(Val::Neu( val::Hole { span: *span, kind: *kind, metavar: *metavar, args }.into(), ))) @@ -375,7 +371,7 @@ impl Eval for Hole { impl Eval for Case { type Val = val::Case; - fn eval(&self, _prg: &Module, env: &mut Env) -> Result { + fn eval(&self, _info_table: &Rc, env: &mut Env) -> Result { let Case { span, pattern, body } = self; let body = body.as_ref().map(|body| Closure { @@ -397,43 +393,49 @@ impl Eval for Case { impl Eval for Args { type Val = val::Args; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { - Ok(val::Args(self.args.eval(prg, env)?)) + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { + Ok(val::Args(self.args.eval(info_table, env)?)) } } impl Eval for Arg { type Val = val::Arg; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { match self { - Arg::UnnamedArg(exp) => Ok(val::Arg::UnnamedArg(exp.eval(prg, env)?)), - Arg::NamedArg(name, exp) => Ok(val::Arg::NamedArg(name.clone(), exp.eval(prg, env)?)), + Arg::UnnamedArg(exp) => Ok(val::Arg::UnnamedArg(exp.eval(info_table, env)?)), + Arg::NamedArg(name, exp) => { + Ok(val::Arg::NamedArg(name.clone(), exp.eval(info_table, env)?)) + } Arg::InsertedImplicitArg(hole) => { - Ok(val::Arg::InsertedImplicitArg(hole.eval(prg, env)?)) + Ok(val::Arg::InsertedImplicitArg(hole.eval(info_table, env)?)) } } } } impl Apply for Closure { - fn apply(mut self, prg: &Module, args: &[Box]) -> Result, TypeError> { - self.env.bind_iter(args.iter(), |env| self.body.eval(prg, env)) + fn apply( + mut self, + info_table: &Rc, + args: &[Box], + ) -> Result, TypeError> { + self.env.bind_iter(args.iter(), |env| self.body.eval(info_table, env)) } } impl Eval for Vec { type Val = Vec; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { - self.iter().map(|x| x.eval(prg, env)).collect() + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { + self.iter().map(|x| x.eval(info_table, env)).collect() } } impl Eval for Box { type Val = Box; - fn eval(&self, prg: &Module, env: &mut Env) -> Result { - (**self).eval(prg, env) + fn eval(&self, info_table: &Rc, env: &mut Env) -> Result { + (**self).eval(info_table, env) } } diff --git a/lang/elaborator/src/normalizer/normalize.rs b/lang/elaborator/src/normalizer/normalize.rs index 3bc682bdd8..584fa6ddc6 100644 --- a/lang/elaborator/src/normalizer/normalize.rs +++ b/lang/elaborator/src/normalizer/normalize.rs @@ -1,18 +1,25 @@ -use ast::ctx::GenericCtx; -use ast::*; +use std::rc::Rc; + +use crate::normalizer::val::ReadBack; +use crate::{result::*, TypeInfoTable}; use super::env::Env; use super::eval::*; -use crate::normalizer::val::ReadBack; -use crate::result::*; pub trait Normalize { type Nf; - fn normalize(&self, prg: &Module, env: &mut Env) -> Result; + fn normalize( + &self, + info_table: &Rc, + env: &mut Env, + ) -> Result; - fn normalize_in_empty_env(&self, prg: &Module) -> Result { - self.normalize(prg, &mut GenericCtx::empty().into()) + fn normalize_in_empty_env( + &self, + info_table: &Rc, + ) -> Result { + self.normalize(info_table, &mut Env::empty()) } } @@ -23,8 +30,12 @@ where { type Nf = <::Val as ReadBack>::Nf; - fn normalize(&self, prg: &Module, env: &mut Env) -> Result { - let val = self.eval(prg, env)?; - val.read_back(prg) + fn normalize( + &self, + info_table: &Rc, + env: &mut Env, + ) -> Result { + let val = self.eval(info_table, env)?; + val.read_back(info_table) } } diff --git a/lang/elaborator/src/normalizer/val.rs b/lang/elaborator/src/normalizer/val.rs index acc75a6079..b4f4c123f9 100644 --- a/lang/elaborator/src/normalizer/val.rs +++ b/lang/elaborator/src/normalizer/val.rs @@ -1,3 +1,5 @@ +use std::rc::Rc; + use ast; use ast::ctx::BindContext; use ast::shift_and_clone; @@ -18,6 +20,7 @@ use printer::types::*; use printer::util::*; use crate::normalizer::env::*; +use crate::TypeInfoTable; use super::eval::Eval; use crate::result::*; @@ -42,30 +45,30 @@ fn print_cases<'a>(cases: &'a [Case], cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> B pub trait ReadBack { type Nf; - fn read_back(&self, prg: &ast::Module) -> Result; + fn read_back(&self, info_table: &Rc) -> Result; } impl ReadBack for Vec { type Nf = Vec; - fn read_back(&self, prg: &ast::Module) -> Result { - self.iter().map(|x| x.read_back(prg)).collect() + fn read_back(&self, info_table: &Rc) -> Result { + self.iter().map(|x| x.read_back(info_table)).collect() } } impl ReadBack for Box { type Nf = Box; - fn read_back(&self, prg: &ast::Module) -> Result { - (**self).read_back(prg).map(Box::new) + fn read_back(&self, info_table: &Rc) -> Result { + (**self).read_back(info_table).map(Box::new) } } impl ReadBack for Option { type Nf = Option; - fn read_back(&self, prg: &ast::Module) -> Result { - self.as_ref().map(|x| x.read_back(prg)).transpose() + fn read_back(&self, info_table: &Rc) -> Result { + self.as_ref().map(|x| x.read_back(info_table)).transpose() } } @@ -112,13 +115,13 @@ impl Print for Val { impl ReadBack for Val { type Nf = ast::Exp; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let res = match self { - Val::TypCtor(e) => e.read_back(prg)?.into(), - Val::Call(e) => e.read_back(prg)?.into(), - Val::TypeUniv(e) => e.read_back(prg)?.into(), - Val::LocalComatch(e) => e.read_back(prg)?.into(), - Val::Neu(exp) => exp.read_back(prg)?, + Val::TypCtor(e) => e.read_back(info_table)?.into(), + Val::Call(e) => e.read_back(info_table)?.into(), + Val::TypeUniv(e) => e.read_back(info_table)?.into(), + Val::LocalComatch(e) => e.read_back(info_table)?.into(), + Val::Neu(exp) => exp.read_back(info_table)?, }; trace!("↓{} ~> {}", self.print_trace(), res.print_trace()); Ok(res) @@ -161,12 +164,12 @@ impl From for Val { impl ReadBack for TypCtor { type Nf = ast::TypCtor; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let TypCtor { span, name, args } = self; Ok(ast::TypCtor { span: *span, name: name.clone(), - args: ast::Args { args: args.read_back(prg)? }, + args: ast::Args { args: args.read_back(info_table)? }, }) } } @@ -208,13 +211,13 @@ impl From for Val { impl ReadBack for Call { type Nf = ast::Call; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let Call { span, kind, name, args } = self; Ok(ast::Call { span: *span, kind: *kind, name: name.clone(), - args: ast::Args { args: args.read_back(prg)? }, + args: ast::Args { args: args.read_back(info_table)? }, inferred_type: None, }) } @@ -250,7 +253,7 @@ impl From for Val { impl ReadBack for TypeUniv { type Nf = ast::TypeUniv; - fn read_back(&self, _prg: &ast::Module) -> Result { + fn read_back(&self, _info_table: &Rc) -> Result { let TypeUniv { span } = self; Ok(ast::TypeUniv { span: *span }) } @@ -296,14 +299,14 @@ impl From for Val { impl ReadBack for LocalComatch { type Nf = ast::LocalComatch; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let LocalComatch { span, name, is_lambda_sugar, cases } = self; Ok(ast::LocalComatch { span: *span, ctx: None, name: name.clone(), is_lambda_sugar: *is_lambda_sugar, - cases: cases.read_back(prg)?, + cases: cases.read_back(info_table)?, inferred_type: None, }) } @@ -359,13 +362,13 @@ impl From for Val { impl ReadBack for Neu { type Nf = ast::Exp; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let res = match self { - Neu::Variable(e) => e.read_back(prg)?.into(), - Neu::DotCall(e) => e.read_back(prg)?.into(), - Neu::LocalMatch(e) => e.read_back(prg)?.into(), - Neu::Hole(e) => e.read_back(prg)?.into(), - Neu::OpaqueCall(e) => e.read_back(prg)?.into(), + Neu::Variable(e) => e.read_back(info_table)?.into(), + Neu::DotCall(e) => e.read_back(info_table)?.into(), + Neu::LocalMatch(e) => e.read_back(info_table)?.into(), + Neu::Hole(e) => e.read_back(info_table)?.into(), + Neu::OpaqueCall(e) => e.read_back(info_table)?.into(), }; Ok(res) } @@ -407,7 +410,7 @@ impl From for Neu { impl ReadBack for Variable { type Nf = ast::Variable; - fn read_back(&self, _prg: &ast::Module) -> Result { + fn read_back(&self, _info_table: &Rc) -> Result { let Variable { span, name, idx } = self; Ok(ast::Variable { span: *span, idx: *idx, name: name.clone(), inferred_type: None }) } @@ -452,14 +455,14 @@ impl From for Neu { impl ReadBack for DotCall { type Nf = ast::DotCall; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let DotCall { span, kind, exp, name, args } = self; Ok(ast::DotCall { span: *span, kind: *kind, - exp: exp.read_back(prg)?, + exp: exp.read_back(info_table)?, name: name.clone(), - args: ast::Args { args: args.read_back(prg)? }, + args: ast::Args { args: args.read_back(info_table)? }, inferred_type: None, }) } @@ -509,7 +512,7 @@ impl From for Neu { impl ReadBack for LocalMatch { type Nf = ast::LocalMatch; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let LocalMatch { span, name, on_exp, cases } = self; Ok(ast::LocalMatch { span: *span, @@ -517,8 +520,8 @@ impl ReadBack for LocalMatch { motive: None, ret_typ: None, name: name.clone(), - on_exp: on_exp.read_back(prg)?, - cases: cases.read_back(prg)?, + on_exp: on_exp.read_back(info_table)?, + cases: cases.read_back(info_table)?, inferred_type: None, }) } @@ -564,9 +567,9 @@ impl From for Neu { impl ReadBack for Hole { type Nf = ast::Hole; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let Hole { span, kind, metavar, args } = self; - let args = args.read_back(prg)?; + let args = args.read_back(info_table)?; Ok(ast::Hole { span: *span, kind: *kind, @@ -627,7 +630,7 @@ impl Print for Case { impl ReadBack for Case { type Nf = ast::Case; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let Case { span, is_copattern, name, params, body } = self; Ok(ast::Case { @@ -637,7 +640,7 @@ impl ReadBack for Case { name: name.clone(), params: params.clone(), }, - body: body.read_back(prg)?, + body: body.read_back(info_table)?, }) } } @@ -678,13 +681,13 @@ impl From for Neu { impl ReadBack for OpaqueCall { type Nf = ast::Call; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let OpaqueCall { span, name, args } = self; Ok(ast::Call { span: *span, kind: ast::CallKind::LetBound, name: name.clone(), - args: ast::Args { args: args.read_back(prg)? }, + args: ast::Args { args: args.read_back(info_table)? }, inferred_type: None, }) } @@ -721,8 +724,8 @@ impl Shift for Args { impl ReadBack for Args { type Nf = Vec; - fn read_back(&self, prg: &ast::Module) -> Result { - self.0.read_back(prg) + fn read_back(&self, info_table: &Rc) -> Result { + self.0.read_back(info_table) } } @@ -772,11 +775,13 @@ impl Shift for Arg { impl ReadBack for Arg { type Nf = ast::Arg; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { match self { - Arg::UnnamedArg(val) => Ok(ast::Arg::UnnamedArg(val.read_back(prg)?)), - Arg::NamedArg(name, val) => Ok(ast::Arg::NamedArg(name.clone(), val.read_back(prg)?)), - Arg::InsertedImplicitArg(val) => Ok(ast::Arg::UnnamedArg(val.read_back(prg)?)), + Arg::UnnamedArg(val) => Ok(ast::Arg::UnnamedArg(val.read_back(info_table)?)), + Arg::NamedArg(name, val) => { + Ok(ast::Arg::NamedArg(name.clone(), val.read_back(info_table)?)) + } + Arg::InsertedImplicitArg(val) => Ok(ast::Arg::UnnamedArg(val.read_back(info_table)?)), } } } @@ -835,7 +840,7 @@ impl Print for Closure { impl ReadBack for Closure { type Nf = Box; - fn read_back(&self, prg: &ast::Module) -> Result { + fn read_back(&self, info_table: &Rc) -> Result { let args: Vec> = (0..self.n_args) .rev() .map(|snd| { @@ -848,6 +853,8 @@ impl ReadBack for Closure { .map(Box::new) .collect(); let mut shifted_env = shift_and_clone(&self.env, (1, 0)); - shifted_env.bind_iter(args.iter(), |env| self.body.eval(prg, env))?.read_back(prg) + shifted_env + .bind_iter(args.iter(), |env| self.body.eval(info_table, env))? + .read_back(info_table) } } diff --git a/lang/elaborator/src/typechecker/ctx.rs b/lang/elaborator/src/typechecker/ctx.rs index de8a0dd5f1..09c78a4081 100644 --- a/lang/elaborator/src/typechecker/ctx.rs +++ b/lang/elaborator/src/typechecker/ctx.rs @@ -42,16 +42,24 @@ impl Ctx { } } pub trait ContextSubstExt: Sized { - fn subst(&mut self, prg: &Module, s: &S) -> Result<(), TypeError>; + fn subst( + &mut self, + type_info_table: &Rc, + s: &S, + ) -> Result<(), TypeError>; } impl ContextSubstExt for Ctx { - fn subst(&mut self, prg: &Module, s: &S) -> Result<(), TypeError> { + fn subst( + &mut self, + type_info_table: &Rc, + s: &S, + ) -> Result<(), TypeError> { let env = self.vars.env(); let levels = self.vars.levels(); self.map_failable(|nf| { let exp = nf.subst(&mut levels.clone(), s); - let nf = exp.normalize(prg, &mut env.clone())?; + let nf = exp.normalize(type_info_table, &mut env.clone())?; Ok(nf) }) } diff --git a/lang/elaborator/src/typechecker/decls/codefinition.rs b/lang/elaborator/src/typechecker/decls/codefinition.rs index 3f759dcd23..c31955f5e6 100644 --- a/lang/elaborator/src/typechecker/decls/codefinition.rs +++ b/lang/elaborator/src/typechecker/decls/codefinition.rs @@ -4,7 +4,8 @@ use log::trace; use ast::*; -use crate::normalizer::{env::ToEnv, normalize::Normalize}; +use crate::normalizer::env::ToEnv; +use crate::normalizer::normalize::Normalize; use crate::typechecker::exprs::local_comatch::WithExpectedType; use crate::typechecker::{ @@ -27,7 +28,7 @@ impl CheckToplevel for Codef { params.infer_telescope(ctx, |ctx, params_out| { let typ_out = typ.check(ctx, &Box::new(TypeUniv::new().into()))?; - let typ_nf = typ.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?; let wd = WithExpectedType { cases, label: Some((label, params.len())), diff --git a/lang/elaborator/src/typechecker/decls/definition.rs b/lang/elaborator/src/typechecker/decls/definition.rs index 36976739dd..76f71320eb 100644 --- a/lang/elaborator/src/typechecker/decls/definition.rs +++ b/lang/elaborator/src/typechecker/decls/definition.rs @@ -4,7 +4,8 @@ use log::trace; use ast::*; use super::CheckToplevel; -use crate::normalizer::{env::ToEnv, normalize::Normalize}; +use crate::normalizer::env::ToEnv; +use crate::normalizer::normalize::Normalize; use crate::typechecker::exprs::local_match::WithScrutinee; use crate::typechecker::{ ctx::Ctx, @@ -21,12 +22,12 @@ impl CheckToplevel for Def { let Def { span, doc, name, attr, params, self_param, ret_typ, cases } = self; params.infer_telescope(ctx, |ctx, params_out| { - let self_param_nf = self_param.typ.normalize(&ctx.module, &mut ctx.env())?; + let self_param_nf = self_param.typ.normalize(&ctx.type_info_table, &mut ctx.env())?; let (ret_typ_out, ret_typ_nf, self_param_out) = self_param.infer_telescope(ctx, |ctx, self_param_out| { let ret_typ_out = ret_typ.infer(ctx)?; - let ret_typ_nf = ret_typ.normalize(&ctx.module, &mut ctx.env())?; + let ret_typ_nf = ret_typ.normalize(&ctx.type_info_table, &mut ctx.env())?; Ok((ret_typ_out, ret_typ_nf, self_param_out)) })?; diff --git a/lang/elaborator/src/typechecker/decls/global_let.rs b/lang/elaborator/src/typechecker/decls/global_let.rs index fdf70bdf82..ae1df3512d 100644 --- a/lang/elaborator/src/typechecker/decls/global_let.rs +++ b/lang/elaborator/src/typechecker/decls/global_let.rs @@ -5,7 +5,8 @@ use log::trace; use ast::*; use super::CheckToplevel; -use crate::normalizer::{env::ToEnv, normalize::Normalize}; +use crate::normalizer::env::ToEnv; +use crate::normalizer::normalize::Normalize; use crate::typechecker::{ ctx::Ctx, exprs::{CheckInfer, InferTelescope}, @@ -20,7 +21,7 @@ impl CheckToplevel for Let { params.infer_telescope(ctx, |ctx, params_out| { let typ_out = typ.infer(ctx)?; - let typ_nf = typ.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?; let body_out = body.check(ctx, &typ_nf)?; Ok(Let { diff --git a/lang/elaborator/src/typechecker/exprs/anno.rs b/lang/elaborator/src/typechecker/exprs/anno.rs index 7e8e720025..b0a123cc29 100644 --- a/lang/elaborator/src/typechecker/exprs/anno.rs +++ b/lang/elaborator/src/typechecker/exprs/anno.rs @@ -31,7 +31,7 @@ impl CheckInfer for Anno { fn infer(&self, ctx: &mut Ctx) -> Result { let Anno { span, exp, typ, .. } = self; let typ_out = typ.check(ctx, &Box::new(TypeUniv::new().into()))?; - let typ_nf = typ.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?; let exp_out = (**exp).check(ctx, &typ_nf)?; Ok(Anno { span: *span, diff --git a/lang/elaborator/src/typechecker/exprs/call.rs b/lang/elaborator/src/typechecker/exprs/call.rs index f7a5ca2c7b..49e3882ab8 100644 --- a/lang/elaborator/src/typechecker/exprs/call.rs +++ b/lang/elaborator/src/typechecker/exprs/call.rs @@ -3,7 +3,6 @@ use crate::normalizer::env::ToEnv; use crate::normalizer::normalize::Normalize; use crate::typechecker::type_info_table::CtorMeta; -use crate::typechecker::type_info_table::LetMeta; use ast::*; use super::super::ctx::*; @@ -45,7 +44,7 @@ impl CheckInfer for Call { let typ_out = typ .subst_under_ctx(vec![params.len()].into(), &vec![args.args.clone()]) .to_exp(); - let typ_nf = typ_out.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ_out.normalize(&ctx.type_info_table, &mut ctx.env())?; Ok(Call { span: *span, kind: *kind, @@ -55,13 +54,13 @@ impl CheckInfer for Call { }) } CallKind::LetBound => { - let LetMeta { params, typ, .. } = ctx.type_info_table.lookup_let(&name.clone())?; + let Let { params, typ, .. } = ctx.type_info_table.lookup_let(&name.clone())?; let params = params.clone(); let typ = typ.clone(); let args_out = check_args(args, &name.clone(), ctx, ¶ms, *span)?; let typ_out = typ.subst_under_ctx(vec![params.len()].into(), &vec![args.args.clone()]); - let typ_nf = typ_out.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ_out.normalize(&ctx.type_info_table, &mut ctx.env())?; Ok(Call { span: *span, kind: *kind, diff --git a/lang/elaborator/src/typechecker/exprs/dot_call.rs b/lang/elaborator/src/typechecker/exprs/dot_call.rs index 5fa7b4b52a..11f8cf19a0 100644 --- a/lang/elaborator/src/typechecker/exprs/dot_call.rs +++ b/lang/elaborator/src/typechecker/exprs/dot_call.rs @@ -45,13 +45,13 @@ impl CheckInfer for DotCall { .typ .subst_under_ctx(vec![params.len()].into(), &vec![args.args.clone()]) .to_exp(); - let self_param_nf = self_param_out.normalize(&ctx.module, &mut ctx.env())?; + let self_param_nf = self_param_out.normalize(&ctx.type_info_table, &mut ctx.env())?; let exp_out = exp.check(ctx, &self_param_nf)?; let subst = vec![args.to_exps(), vec![exp.clone()]]; let typ_out = ret_typ.subst_under_ctx(vec![params.len(), 1].into(), &subst); - let typ_out_nf = typ_out.normalize(&ctx.module, &mut ctx.env())?; + let typ_out_nf = typ_out.normalize(&ctx.type_info_table, &mut ctx.env())?; Ok(DotCall { span: *span, diff --git a/lang/elaborator/src/typechecker/exprs/local_comatch.rs b/lang/elaborator/src/typechecker/exprs/local_comatch.rs index 11506d22c7..30758add1f 100644 --- a/lang/elaborator/src/typechecker/exprs/local_comatch.rs +++ b/lang/elaborator/src/typechecker/exprs/local_comatch.rs @@ -139,14 +139,15 @@ impl<'a> WithExpectedType<'a> { // Normalize the arguments of the return type and the arguments to the self-parameter // of the destructor declaration. // TODO: Why can't we do this once *before* we repeatedly look them up in the context? - let def_args = - def_args.normalize(&ctx.module, &mut LevelCtx::from(vec![params.len()]).env())?; - let ret_typ = - ret_typ.normalize(&ctx.module, &mut LevelCtx::from(vec![params.len(), 1]).env())?; + let def_args = def_args + .normalize(&ctx.type_info_table, &mut LevelCtx::from(vec![params.len()]).env())?; + let ret_typ = ret_typ.normalize( + &ctx.type_info_table, + &mut LevelCtx::from(vec![params.len(), 1]).env(), + )?; let name = name.clone(); let params = params.clone(); - let module = ctx.module.clone(); params_inst.check_telescope( &name.id, @@ -274,7 +275,7 @@ impl<'a> WithExpectedType<'a> { let mut ret_typ = ret_typ.subst(&mut subst_ctx, &subst); ret_typ.shift((-1, 0)); ret_typ.normalize( - &ctx.module, + &ctx.type_info_table, &mut LevelCtx::from(vec![*n_label_args, params.len()]) .env(), )? @@ -295,11 +296,13 @@ impl<'a> WithExpectedType<'a> { .ok_yes()?; ctx.fork::, _>(|ctx| { - ctx.subst(&module, &unif)?; + let type_info_table = ctx.type_info_table.clone(); + ctx.subst(&type_info_table, &unif)?; let body = body.subst(&mut ctx.levels(), &unif); let t_subst = ret_typ_nf.subst(&mut ctx.levels(), &unif); - let t_nf = t_subst.normalize(&module, &mut ctx.env())?; + let t_nf = + t_subst.normalize(&ctx.type_info_table, &mut ctx.env())?; let body_out = body.check(ctx, &t_nf)?; diff --git a/lang/elaborator/src/typechecker/exprs/local_match.rs b/lang/elaborator/src/typechecker/exprs/local_match.rs index 38cc116a7b..91a8cc9aa8 100644 --- a/lang/elaborator/src/typechecker/exprs/local_match.rs +++ b/lang/elaborator/src/typechecker/exprs/local_match.rs @@ -44,7 +44,8 @@ impl CheckInfer for LocalMatch { // Pattern matching with motive Some(m) => { let Motive { span: info, param, ret_typ } = m; - let mut self_t_nf = typ_app.to_exp().normalize(&ctx.module, &mut ctx.env())?; + let mut self_t_nf = + typ_app.to_exp().normalize(&ctx.type_info_table, &mut ctx.env())?; self_t_nf.shift((1, 0)); let self_binder = Binder { name: param.name.clone(), typ: self_t_nf.clone() }; @@ -59,11 +60,11 @@ impl CheckInfer for LocalMatch { let subst = Assign { lvl: Lvl { fst: subst_ctx.len() - 1, snd: 0 }, exp: on_exp }; let mut motive_t = ret_typ.subst(&mut subst_ctx, &subst); motive_t.shift((-1, 0)); - let motive_t_nf = motive_t.normalize(&ctx.module, &mut ctx.env())?; + let motive_t_nf = motive_t.normalize(&ctx.type_info_table, &mut ctx.env())?; convert(subst_ctx, &mut ctx.meta_vars, motive_t_nf, t)?; body_t = ctx.bind_single(&self_binder, |ctx| { - ret_typ.normalize(&ctx.module, &mut ctx.env()) + ret_typ.normalize(&ctx.type_info_table, &mut ctx.env()) })?; motive_out = Some(Motive { span: *info, @@ -160,7 +161,7 @@ impl<'a> WithScrutinee<'a> { ctx.type_info_table.lookup_ctor(&name)?; let def_args_nf = LevelCtx::empty().bind_iter(params.params.iter(), |ctx_| { - def_args.normalize(&ctx.module, &mut ctx_.env()) + def_args.normalize(&ctx.type_info_table, &mut ctx_.env()) })?; let TypCtor { args: on_args, .. } = &self.scrutinee; @@ -172,7 +173,6 @@ impl<'a> WithScrutinee<'a> { let mut subst_ctx_2 = ctx.levels().append(&vec![params.len(), 1].into()); let curr_lvl = subst_ctx_2.len() - 1; - let module = ctx.module.clone(); let name = name.clone(); let params = params.clone(); @@ -223,11 +223,13 @@ impl<'a> WithScrutinee<'a> { .ok_yes()?; ctx.fork::, _>(|ctx| { - ctx.subst(&module, &unif)?; + let type_info_table = ctx.type_info_table.clone(); + ctx.subst(&type_info_table, &unif)?; let body = body.subst(&mut ctx.levels(), &unif); let t_subst = t.subst(&mut ctx.levels(), &unif); - let t_nf = t_subst.normalize(&module, &mut ctx.env())?; + let t_nf = + t_subst.normalize(&ctx.type_info_table, &mut ctx.env())?; let body_out = body.check(ctx, &t_nf)?; diff --git a/lang/elaborator/src/typechecker/exprs/mod.rs b/lang/elaborator/src/typechecker/exprs/mod.rs index d71f2e6f35..46472ad645 100644 --- a/lang/elaborator/src/typechecker/exprs/mod.rs +++ b/lang/elaborator/src/typechecker/exprs/mod.rs @@ -142,7 +142,7 @@ fn check_args( .iter() .zip(params) .map(|(exp, Param { typ, .. })| { - let typ = typ.normalize(&ctx.module, &mut ctx.env())?; + let typ = typ.normalize(&ctx.type_info_table, &mut ctx.env())?; exp.check(ctx, &typ) }) .collect::>()?; @@ -205,7 +205,7 @@ impl CheckTelescope for TelescopeInst { let ParamInst { span, name, .. } = param_actual; let Param { typ, .. } = param_expected; let typ_out = typ.check(ctx, &Box::new(TypeUniv::new().into()))?; - let typ_nf = typ.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?; let mut params_out = params_out; let param_out = ParamInst { span: *span, @@ -238,7 +238,7 @@ impl InferTelescope for Telescope { |ctx, mut params_out, param| { let Param { implicit, typ, name } = param; let typ_out = typ.check(ctx, &Box::new(TypeUniv::new().into()))?; - let typ_nf = typ.normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ.normalize(&ctx.type_info_table, &mut ctx.env())?; let param_out = Param { implicit: *implicit, name: name.clone(), typ: typ_out }; params_out.push(param_out); let elem = Binder { name: param.name.clone(), typ: typ_nf }; @@ -259,7 +259,7 @@ impl InferTelescope for SelfParam { ) -> Result { let SelfParam { info, name, typ } = self; - let typ_nf = typ.to_exp().normalize(&ctx.module, &mut ctx.env())?; + let typ_nf = typ.to_exp().normalize(&ctx.type_info_table, &mut ctx.env())?; let typ_out = typ.infer(ctx)?; let param_out = SelfParam { info: *info, name: name.clone(), typ: typ_out }; let elem = diff --git a/lang/elaborator/src/typechecker/type_info_table/build.rs b/lang/elaborator/src/typechecker/type_info_table/build.rs index 48ace23bd7..fef5b2f179 100644 --- a/lang/elaborator/src/typechecker/type_info_table/build.rs +++ b/lang/elaborator/src/typechecker/type_info_table/build.rs @@ -1,6 +1,6 @@ use ast::*; -use super::{CodefMeta, CtorMeta, DefMeta, DtorMeta, LetMeta, ModuleTypeInfoTable, TyCtorMeta}; +use super::{CtorMeta, DtorMeta, ModuleTypeInfoTable, TyCtorMeta}; pub fn build_type_info_table(module: &Module) -> ModuleTypeInfoTable { let mut info_table = ModuleTypeInfoTable::default(); @@ -75,32 +75,18 @@ impl BuildTypeInfoTable for Dtor { impl BuildTypeInfoTable for Def { fn build(&self, info_table: &mut ModuleTypeInfoTable) { - let Def { name, params, self_param, ret_typ, .. } = self; - info_table.map_def.insert( - name.id.clone(), - DefMeta { - params: params.clone(), - self_param: self_param.clone(), - ret_typ: ret_typ.clone(), - }, - ); + info_table.map_def.insert(self.name.id.clone(), self.clone()); } } impl BuildTypeInfoTable for Codef { fn build(&self, info_table: &mut ModuleTypeInfoTable) { - let Codef { name, params, typ, .. } = self; - info_table - .map_codef - .insert(name.id.clone(), CodefMeta { params: params.clone(), typ: typ.clone() }); + info_table.map_codef.insert(self.name.id.clone(), self.clone()); } } impl BuildTypeInfoTable for Let { fn build(&self, info_table: &mut ModuleTypeInfoTable) { - let Let { name, params, typ, .. } = self; - info_table - .map_let - .insert(name.id.clone(), LetMeta { params: params.clone(), typ: typ.clone() }); + info_table.map_let.insert(self.name.id.clone(), self.clone()); } } diff --git a/lang/elaborator/src/typechecker/type_info_table/lookup.rs b/lang/elaborator/src/typechecker/type_info_table/lookup.rs index c846ee99a5..afa4c17108 100644 --- a/lang/elaborator/src/typechecker/type_info_table/lookup.rs +++ b/lang/elaborator/src/typechecker/type_info_table/lookup.rs @@ -1,8 +1,6 @@ use ast::*; -use super::{ - CodefMeta, CtorMeta, DefMeta, DtorMeta, LetMeta, TyCtorMeta, TypeError, TypeInfoTable, -}; +use super::{CtorMeta, DtorMeta, TyCtorMeta, TypeError, TypeInfoTable}; impl TypeInfoTable { pub fn lookup_data(&self, name: &IdBound) -> Result<&Data, TypeError> { @@ -41,7 +39,7 @@ impl TypeInfoTable { return Ok(meta.clone()); } if let Some(meta) = map.map_codef.get(&name.id) { - return Ok(meta.to_ctor().clone()); + return Ok(meta.to_ctor().into()); } Err(TypeError::Impossible { message: format!("Top-level ctor or codef {name} not found"), @@ -58,7 +56,7 @@ impl TypeInfoTable { return Ok(meta.clone()); } if let Some(meta) = map.map_def.get(&name.id) { - return Ok(meta.to_dtor().clone()); + return Ok(meta.to_dtor().into()); } Err(TypeError::Impossible { message: format!("Top-level dtor or def {name} not found"), @@ -66,7 +64,7 @@ impl TypeInfoTable { }) } - pub fn lookup_let(&self, name: &IdBound) -> Result<&LetMeta, TypeError> { + pub fn lookup_let(&self, name: &IdBound) -> Result<&Let, TypeError> { let map = self.map.get(&name.uri).ok_or(TypeError::Impossible { message: format!("Module with URI {} not found", name.uri), span: None, @@ -94,7 +92,7 @@ impl TypeInfoTable { }) } - pub fn lookup_codef(&self, name: &IdBound) -> Result<&CodefMeta, TypeError> { + pub fn lookup_codef(&self, name: &IdBound) -> Result<&Codef, TypeError> { let map = self.map.get(&name.uri).ok_or(TypeError::Impossible { message: format!("Module with URI {} not found", name.uri), span: None, @@ -122,7 +120,7 @@ impl TypeInfoTable { }) } - pub fn lookup_def(&self, name: &IdBound) -> Result<&DefMeta, TypeError> { + pub fn lookup_def(&self, name: &IdBound) -> Result<&Def, TypeError> { let map = self.map.get(&name.uri).ok_or(TypeError::Impossible { message: format!("Module with URI {} not found", name.uri), span: None, diff --git a/lang/elaborator/src/typechecker/type_info_table/mod.rs b/lang/elaborator/src/typechecker/type_info_table/mod.rs index 6530138501..530a396402 100644 --- a/lang/elaborator/src/typechecker/type_info_table/mod.rs +++ b/lang/elaborator/src/typechecker/type_info_table/mod.rs @@ -27,66 +27,43 @@ pub struct ModuleTypeInfoTable { // Calls // // - map_let: HashMap, + map_let: HashMap, map_tyctor: HashMap, - map_codef: HashMap, + map_codef: HashMap, map_ctor: HashMap, // DotCalls // // - map_def: HashMap, + map_def: HashMap, map_dtor: HashMap, } -#[derive(Debug, Clone)] -pub struct LetMeta { - pub params: Telescope, - pub typ: Box, -} - #[derive(Debug, Clone)] pub struct TyCtorMeta { pub params: Box, } #[derive(Debug, Clone)] -pub struct CodefMeta { +pub struct CtorMeta { pub params: Telescope, pub typ: TypCtor, } -impl CodefMeta { - pub fn to_ctor(&self) -> CtorMeta { - CtorMeta { params: self.params.clone(), typ: self.typ.clone() } +impl From for CtorMeta { + fn from(ctor: Ctor) -> Self { + CtorMeta { params: ctor.params, typ: ctor.typ } } } #[derive(Debug, Clone)] -pub struct CtorMeta { - pub params: Telescope, - pub typ: TypCtor, -} - -#[derive(Debug, Clone)] -pub struct DefMeta { +pub struct DtorMeta { pub params: Telescope, pub self_param: SelfParam, pub ret_typ: Box, } -impl DefMeta { - fn to_dtor(&self) -> DtorMeta { - DtorMeta { - params: self.params.clone(), - self_param: self.self_param.clone(), - ret_typ: self.ret_typ.clone(), - } +impl From for DtorMeta { + fn from(dtor: Dtor) -> Self { + DtorMeta { params: dtor.params, self_param: dtor.self_param, ret_typ: dtor.ret_typ } } } - -#[derive(Debug, Clone)] -pub struct DtorMeta { - pub params: Telescope, - pub self_param: SelfParam, - pub ret_typ: Box, -} diff --git a/test/test-runner/src/phases.rs b/test/test-runner/src/phases.rs index 6dad5adf2a..d75175f113 100644 --- a/test/test-runner/src/phases.rs +++ b/test/test-runner/src/phases.rs @@ -353,9 +353,10 @@ impl Phase for Xfunc { return Ok(()); } - let type_names = db.all_type_names(uri)?; + let type_names = db.all_declared_type_names(uri)?; - let new_uri = Url::parse("inmemory:///scratch.pol").unwrap(); + let new_uri = + uri.to_string().replacen("file", "inmemory", 1).parse().expect("Failed to parse URI"); db.source.manage(&new_uri); for type_name in type_names.iter().map(|tn| &tn.id) {