From ee16b2a6009ce853af2ebf668ec134218702f318 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tim=20S=C3=BCberkr=C3=BCb?= Date: Wed, 6 Nov 2024 16:24:50 +0100 Subject: [PATCH] Split Ident --- lang/ast/src/ctx/values.rs | 2 +- lang/ast/src/decls.rs | 72 +- lang/ast/src/exp.rs | 1827 +++++++++++++++++ lang/ast/src/ident.rs | 134 +- lang/ast/src/traits/identifiable.rs | 21 + lang/ast/src/traits/mod.rs | 4 +- lang/ast/src/traits/named.rs | 21 - lang/ast/src/traits/subst.rs | 2 +- lang/driver/src/info/lookup.rs | 16 +- lang/driver/src/xfunc.rs | 22 +- lang/elaborator/src/normalizer/env.rs | 6 +- lang/elaborator/src/normalizer/eval.rs | 15 +- lang/elaborator/src/normalizer/val.rs | 18 +- lang/elaborator/src/result.rs | 12 +- .../src/typechecker/decls/codatatype.rs | 2 +- .../src/typechecker/decls/datatype.rs | 2 +- lang/elaborator/src/typechecker/decls/mod.rs | 2 +- lang/elaborator/src/typechecker/exprs/call.rs | 8 +- .../src/typechecker/exprs/dot_call.rs | 4 +- .../src/typechecker/exprs/local_comatch.rs | 16 +- .../src/typechecker/exprs/local_match.rs | 14 +- lang/elaborator/src/typechecker/exprs/mod.rs | 4 +- .../src/typechecker/type_info_table/build.rs | 18 +- .../src/typechecker/type_info_table/lookup.rs | 44 +- .../src/typechecker/type_info_table/mod.rs | 16 +- lang/lowering/src/ctx.rs | 4 +- .../src/lower/decls/codata_declaration.rs | 5 +- lang/lowering/src/lower/decls/codefinition.rs | 3 +- .../src/lower/decls/data_declaration.rs | 7 +- lang/lowering/src/lower/decls/definition.rs | 3 +- lang/lowering/src/lower/decls/mod.rs | 5 +- lang/lowering/src/lower/decls/toplevel_let.rs | 3 +- lang/lowering/src/lower/exp/mod.rs | 42 +- lang/transformations/src/lifting/fv.rs | 19 +- lang/transformations/src/lifting/mod.rs | 28 +- lang/transformations/src/renaming/ast.rs | 2 +- lang/transformations/src/renaming/ctx.rs | 14 +- lang/transformations/src/renaming/util.rs | 8 +- lang/transformations/src/xfunc/matrix.rs | 40 +- lang/transformations/src/xfunc/mod.rs | 14 +- 40 files changed, 2225 insertions(+), 274 deletions(-) create mode 100644 lang/ast/src/exp.rs create mode 100644 lang/ast/src/traits/identifiable.rs delete mode 100644 lang/ast/src/traits/named.rs diff --git a/lang/ast/src/ctx/values.rs b/lang/ast/src/ctx/values.rs index 3f02fe2422..6f47a3bc3d 100644 --- a/lang/ast/src/ctx/values.rs +++ b/lang/ast/src/ctx/values.rs @@ -96,7 +96,7 @@ impl Print for TypeCtx { #[derive(Debug, Clone)] pub struct Binder { - pub name: Ident, + pub name: VarBind, pub typ: Box, } diff --git a/lang/ast/src/decls.rs b/lang/ast/src/decls.rs index 1ba71be0b6..5bee5c90a7 100644 --- a/lang/ast/src/decls.rs +++ b/lang/ast/src/decls.rs @@ -23,7 +23,7 @@ use printer::PrintCfg; use url::Url; use crate::ctx::LevelCtx; -use crate::named::Named; +use crate::identifiable::GloballyIdentifiable; use crate::shift_and_clone; use crate::ContainsMetaVars; use crate::Zonk; @@ -184,7 +184,7 @@ pub struct Module { } impl Module { - pub fn xdefs_for_type(&self, type_name: &str) -> Vec { + pub fn xdefs_for_type(&self, type_name: &str) -> Vec { let mut out = vec![]; for decl in &self.decls { @@ -206,7 +206,7 @@ impl Module { out } - pub fn xtors_for_type(&self, type_name: &str) -> Vec { + pub fn xtors_for_type(&self, type_name: &str) -> Vec { let mut out = vec![]; for decl in &self.decls { @@ -232,25 +232,25 @@ impl Module { out } - pub fn lookup_decl(&self, name: &Ident) -> Option<&Decl> { - self.decls.iter().find(|decl| decl.name() == name) + pub fn lookup_decl(&self, name: &IdBind) -> Option<&Decl> { + self.decls.iter().find(|decl| decl.ident() == name) } - pub fn lookup_let(&self, name: &Ident) -> Option<&Let> { + 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: &Ident) -> Option<&Def> { + 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: &Ident) -> Option<&Codef> { + 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, @@ -367,8 +367,8 @@ impl Decl { } } -impl Named for Decl { - fn name(&self) -> &Ident { +impl GloballyIdentifiable for Decl { + fn ident(&self) -> &IdBind { match self { Decl::Data(Data { name, .. }) => name, Decl::Codata(Codata { name, .. }) => name, @@ -435,7 +435,7 @@ impl ContainsMetaVars for Decl { pub struct Data { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub attr: Attributes, pub typ: Box, pub ctors: Vec, @@ -503,7 +503,7 @@ impl ContainsMetaVars for Data { pub struct Codata { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub attr: Attributes, pub typ: Box, pub dtors: Vec, @@ -571,7 +571,7 @@ impl ContainsMetaVars for Codata { pub struct Ctor { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub params: Telescope, pub typ: TypCtor, } @@ -619,7 +619,7 @@ impl ContainsMetaVars for Ctor { pub struct Dtor { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub params: Telescope, pub self_param: SelfParam, pub ret_typ: Box, @@ -670,7 +670,7 @@ impl ContainsMetaVars for Dtor { pub struct Def { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub attr: Attributes, pub params: Telescope, pub self_param: SelfParam, @@ -748,7 +748,7 @@ impl ContainsMetaVars for Def { pub struct Codef { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub attr: Attributes, pub params: Telescope, pub typ: TypCtor, @@ -822,7 +822,7 @@ impl ContainsMetaVars for Codef { pub struct Let { pub span: Option, pub doc: Option, - pub name: Ident, + pub name: IdBind, pub attr: Attributes, pub params: Telescope, pub typ: Box, @@ -884,7 +884,7 @@ impl ContainsMetaVars for Let { #[derive(Debug, Clone)] pub struct SelfParam { pub info: Option, - pub name: Option, + pub name: Option, pub typ: TypCtor, } @@ -893,7 +893,7 @@ impl SelfParam { Telescope { params: vec![Param { implicit: false, - name: self.name.clone().unwrap_or_else(|| Ident::from_string("")), + name: self.name.clone().unwrap_or_else(|| VarBind::from_string("")), typ: Box::new(self.typ.to_exp()), }], } @@ -1083,12 +1083,12 @@ mod print_telescope_tests { fn print_simple_chunk() { let param1 = Param { implicit: false, - name: Ident::from_string("x"), + name: VarBind::from_string("x"), typ: Box::new(TypeUniv::new().into()), }; let param2 = Param { implicit: false, - name: Ident::from_string("y"), + name: VarBind::from_string("y"), typ: Box::new(TypeUniv::new().into()), }; let tele = Telescope { params: vec![param1, param2] }; @@ -1099,12 +1099,12 @@ mod print_telescope_tests { fn print_simple_implicit_chunk() { let param1 = Param { implicit: true, - name: Ident::from_string("x"), + name: VarBind::from_string("x"), typ: Box::new(TypeUniv::new().into()), }; let param2 = Param { implicit: true, - name: Ident::from_string("y"), + name: VarBind::from_string("y"), typ: Box::new(TypeUniv::new().into()), }; let tele = Telescope { params: vec![param1, param2] }; @@ -1115,12 +1115,12 @@ mod print_telescope_tests { fn print_mixed_implicit_chunk_1() { let param1 = Param { implicit: true, - name: Ident::from_string("x"), + name: VarBind::from_string("x"), typ: Box::new(TypeUniv::new().into()), }; let param2 = Param { implicit: false, - name: Ident::from_string("y"), + name: VarBind::from_string("y"), typ: Box::new(TypeUniv::new().into()), }; let tele = Telescope { params: vec![param1, param2] }; @@ -1131,12 +1131,12 @@ mod print_telescope_tests { fn print_mixed_implicit_chunk_2() { let param1 = Param { implicit: false, - name: Ident::from_string("x"), + name: VarBind::from_string("x"), typ: Box::new(TypeUniv::new().into()), }; let param2 = Param { implicit: true, - name: Ident::from_string("y"), + name: VarBind::from_string("y"), typ: Box::new(TypeUniv::new().into()), }; let tele = Telescope { params: vec![param1, param2] }; @@ -1147,26 +1147,26 @@ mod print_telescope_tests { fn print_shifting_example() { let param1 = Param { implicit: false, - name: Ident::from_string("a"), + name: VarBind::from_string("a"), typ: Box::new(TypeUniv::new().into()), }; let param2 = Param { implicit: false, - name: Ident::from_string("x"), + name: VarBind::from_string("x"), typ: Box::new(Exp::Variable(Variable { span: None, idx: Idx { fst: 0, snd: 0 }, - name: Ident::from_string("a"), + name: VarBound::from_string("a"), inferred_type: None, })), }; let param3 = Param { implicit: false, - name: Ident::from_string("y"), + name: VarBind::from_string("y"), typ: Box::new(Exp::Variable(Variable { span: None, idx: Idx { fst: 0, snd: 1 }, - name: Ident::from_string("a"), + name: VarBound::from_string("a"), inferred_type: None, })), }; @@ -1184,16 +1184,10 @@ mod print_telescope_tests { pub struct Param { pub implicit: bool, #[derivative(PartialEq = "ignore", Hash = "ignore")] - pub name: Ident, + pub name: VarBind, pub typ: Box, } -impl Named for Param { - fn name(&self) -> &Ident { - &self.name - } -} - impl Substitutable for Param { type Result = Param; fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self { diff --git a/lang/ast/src/exp.rs b/lang/ast/src/exp.rs new file mode 100644 index 0000000000..6e1d10d325 --- /dev/null +++ b/lang/ast/src/exp.rs @@ -0,0 +1,1827 @@ +use std::fmt; +use std::hash::Hash; + +use codespan::Span; +use derivative::Derivative; +use pretty::DocAllocator; +use printer::theme::ThemeExt; +use printer::tokens::{ + ABSURD, ARROW, AS, COLON, COLONEQ, COMATCH, COMMA, DOT, FAT_ARROW, MATCH, QUESTION_MARK, TYPE, + UNDERSCORE, +}; +use printer::util::{BackslashExt, BracesExt}; +use printer::{Alloc, Builder, Precedence, Print, PrintCfg}; + +use crate::ctx::values::TypeCtx; +use crate::ctx::{BindContext, LevelCtx}; +use crate::{ContainsMetaVars, SubstUnderCtx, Zonk, ZonkError}; + +use super::subst::{Substitutable, Substitution}; +use super::traits::HasSpan; +use super::traits::Occurs; +use super::HasType; +use super::{ident::*, Shift, ShiftRange, ShiftRangeExt}; + +// Prints "{ }" +pub fn empty_braces<'a>(alloc: &'a Alloc<'a>) -> Builder<'a> { + alloc.space().braces_anno() +} + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Label { + /// A machine-generated, unique id + pub id: usize, + /// A user-annotated name + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub user_name: Option, +} + +impl fmt::Display for Label { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match &self.user_name { + None => Ok(()), + Some(user_name) => user_name.fmt(f), + } + } +} + +// Arg +// +// + +/// Arguments in an argument list can either be unnamed or named. +/// Example for named arguments: `f(x := 1, y := 2)` +/// Example for unnamed arguments: `f(1, 2)` +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub enum Arg { + UnnamedArg(Box), + NamedArg(VarBound, Box), + InsertedImplicitArg(Hole), +} + +impl Arg { + pub fn is_inserted_implicit(&self) -> bool { + matches!(self, Arg::InsertedImplicitArg(_)) + } + + pub fn exp(&self) -> Box { + match self { + Arg::UnnamedArg(e) => e.clone(), + Arg::NamedArg(_, e) => e.clone(), + Arg::InsertedImplicitArg(hole) => Box::new(hole.clone().into()), + } + } +} + +impl HasSpan for Arg { + fn span(&self) -> Option { + match self { + Arg::UnnamedArg(e) => e.span(), + Arg::NamedArg(_, e) => e.span(), + Arg::InsertedImplicitArg(hole) => hole.span(), + } + } +} + +impl Shift for Arg { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + match self { + Arg::UnnamedArg(e) => e.shift_in_range(range, by), + Arg::NamedArg(_, e) => e.shift_in_range(range, by), + Arg::InsertedImplicitArg(hole) => hole.shift_in_range(range, by), + } + } +} + +impl Occurs for Arg { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + match self { + Arg::UnnamedArg(e) => e.occurs(ctx, lvl), + Arg::NamedArg(_, e) => e.occurs(ctx, lvl), + Arg::InsertedImplicitArg(hole) => hole.occurs(ctx, lvl), + } + } +} + +impl HasType for Arg { + fn typ(&self) -> Option> { + match self { + Arg::UnnamedArg(e) => e.typ(), + Arg::NamedArg(_, e) => e.typ(), + Arg::InsertedImplicitArg(hole) => hole.typ(), + } + } +} + +impl Substitutable for Arg { + type Result = Arg; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + match self { + Arg::UnnamedArg(e) => Arg::UnnamedArg(e.subst(ctx, by)), + Arg::NamedArg(i, e) => Arg::NamedArg(i.clone(), e.subst(ctx, by)), + Arg::InsertedImplicitArg(hole) => Arg::InsertedImplicitArg(hole.subst(ctx, by)), + } + } +} + +impl Print for Arg { + fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + match self { + Arg::UnnamedArg(e) => e.print(cfg, alloc), + Arg::NamedArg(i, e) => alloc.text(&i.id).append(COLONEQ).append(e.print(cfg, alloc)), + Arg::InsertedImplicitArg(_) => { + panic!("Inserted implicit arguments should not be printed") + } + } + } +} + +impl Zonk for Arg { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + match self { + Arg::UnnamedArg(e) => e.zonk(meta_vars), + Arg::NamedArg(_, e) => e.zonk(meta_vars), + Arg::InsertedImplicitArg(hole) => hole.zonk(meta_vars), + } + } +} + +impl ContainsMetaVars for Arg { + fn contains_metavars(&self) -> bool { + match self { + Arg::UnnamedArg(e) => e.contains_metavars(), + Arg::NamedArg(_, e) => e.contains_metavars(), + Arg::InsertedImplicitArg(hole) => hole.contains_metavars(), + } + } +} + +// Exp +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub enum Exp { + Variable(Variable), + TypCtor(TypCtor), + Call(Call), + DotCall(DotCall), + Anno(Anno), + TypeUniv(TypeUniv), + LocalMatch(LocalMatch), + LocalComatch(LocalComatch), + Hole(Hole), +} + +impl Exp { + pub fn to_typctor(self) -> Option { + match self { + Exp::TypCtor(e) => Some(e), + _ => None, + } + } +} + +impl HasSpan for Exp { + fn span(&self) -> Option { + match self { + Exp::Variable(e) => e.span(), + Exp::TypCtor(e) => e.span(), + Exp::Call(e) => e.span(), + Exp::DotCall(e) => e.span(), + Exp::Anno(e) => e.span(), + Exp::TypeUniv(e) => e.span(), + Exp::LocalMatch(e) => e.span(), + Exp::LocalComatch(e) => e.span(), + Exp::Hole(e) => e.span(), + } + } +} + +impl Shift for Exp { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + match self { + Exp::Variable(e) => e.shift_in_range(range, by), + Exp::TypCtor(e) => e.shift_in_range(range, by), + Exp::Call(e) => e.shift_in_range(range, by), + Exp::DotCall(e) => e.shift_in_range(range, by), + Exp::Anno(e) => e.shift_in_range(range, by), + Exp::TypeUniv(e) => e.shift_in_range(range, by), + Exp::LocalMatch(e) => e.shift_in_range(range, by), + Exp::LocalComatch(e) => e.shift_in_range(range, by), + Exp::Hole(e) => e.shift_in_range(range, by), + } + } +} + +impl Occurs for Exp { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + match self { + Exp::Variable(e) => e.occurs(ctx, lvl), + Exp::TypCtor(e) => e.occurs(ctx, lvl), + Exp::Call(e) => e.occurs(ctx, lvl), + Exp::DotCall(e) => e.occurs(ctx, lvl), + Exp::Anno(e) => e.occurs(ctx, lvl), + Exp::TypeUniv(e) => e.occurs(ctx, lvl), + Exp::LocalMatch(e) => e.occurs(ctx, lvl), + Exp::LocalComatch(e) => e.occurs(ctx, lvl), + Exp::Hole(e) => e.occurs(ctx, lvl), + } + } +} + +impl HasType for Exp { + fn typ(&self) -> Option> { + match self { + Exp::Variable(e) => e.typ(), + Exp::TypCtor(e) => e.typ(), + Exp::Call(e) => e.typ(), + Exp::DotCall(e) => e.typ(), + Exp::Anno(e) => e.typ(), + Exp::TypeUniv(e) => e.typ(), + Exp::LocalMatch(e) => e.typ(), + Exp::LocalComatch(e) => e.typ(), + Exp::Hole(e) => e.typ(), + } + } +} + +impl Substitutable for Exp { + type Result = Exp; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + match self { + Exp::Variable(e) => *e.subst(ctx, by), + Exp::TypCtor(e) => e.subst(ctx, by).into(), + Exp::Call(e) => e.subst(ctx, by).into(), + Exp::DotCall(e) => e.subst(ctx, by).into(), + Exp::Anno(e) => e.subst(ctx, by).into(), + Exp::TypeUniv(e) => e.subst(ctx, by).into(), + Exp::LocalMatch(e) => e.subst(ctx, by).into(), + Exp::LocalComatch(e) => e.subst(ctx, by).into(), + Exp::Hole(e) => e.subst(ctx, by).into(), + } + } +} + +impl Print for Exp { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + prec: Precedence, + ) -> Builder<'a> { + match self { + Exp::Variable(e) => e.print_prec(cfg, alloc, prec), + Exp::TypCtor(e) => e.print_prec(cfg, alloc, prec), + Exp::Call(e) => e.print_prec(cfg, alloc, prec), + Exp::DotCall(e) => e.print_prec(cfg, alloc, prec), + Exp::Anno(e) => e.print_prec(cfg, alloc, prec), + Exp::TypeUniv(e) => e.print_prec(cfg, alloc, prec), + Exp::LocalMatch(e) => e.print_prec(cfg, alloc, prec), + Exp::LocalComatch(e) => e.print_prec(cfg, alloc, prec), + Exp::Hole(e) => e.print_prec(cfg, alloc, prec), + } + } +} + +impl Zonk for Exp { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + match self { + Exp::Variable(e) => e.zonk(meta_vars), + Exp::TypCtor(e) => e.zonk(meta_vars), + Exp::Call(e) => e.zonk(meta_vars), + Exp::DotCall(e) => e.zonk(meta_vars), + Exp::Anno(e) => e.zonk(meta_vars), + Exp::TypeUniv(e) => e.zonk(meta_vars), + Exp::LocalMatch(e) => e.zonk(meta_vars), + Exp::LocalComatch(e) => e.zonk(meta_vars), + Exp::Hole(e) => e.zonk(meta_vars), + } + } +} + +impl ContainsMetaVars for Exp { + fn contains_metavars(&self) -> bool { + match self { + Exp::Variable(variable) => variable.contains_metavars(), + Exp::TypCtor(typ_ctor) => typ_ctor.contains_metavars(), + Exp::Call(call) => call.contains_metavars(), + Exp::DotCall(dot_call) => dot_call.contains_metavars(), + Exp::Anno(anno) => anno.contains_metavars(), + Exp::TypeUniv(type_univ) => type_univ.contains_metavars(), + Exp::LocalMatch(local_match) => local_match.contains_metavars(), + Exp::LocalComatch(local_comatch) => local_comatch.contains_metavars(), + Exp::Hole(hole) => hole.contains_metavars(), + } + } +} + +// Variable +// +// + +/// A bound variable occurrence. The variable is represented +/// using a de-Bruijn index, but we keep the information +/// about the name that was originally annotated in the program. +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Variable { + /// Source code location + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + /// The de-Bruijn index that is used to represent the + /// binding structure of terms. + pub idx: Idx, + /// The name that was originally annotated in the program + /// We do not use this information for tracking the binding + /// structure, but only for prettyprinting code. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub name: VarBound, + /// Inferred type annotated after elaboration. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_type: Option>, +} + +impl HasSpan for Variable { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: Variable) -> Self { + Exp::Variable(val) + } +} + +impl Shift for Variable { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.idx.shift_in_range(range, by); + self.inferred_type = None; + } +} + +impl Occurs for Variable { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let Variable { idx, .. } = self; + ctx.idx_to_lvl(*idx) == lvl + } +} + +impl HasType for Variable { + fn typ(&self) -> Option> { + self.inferred_type.clone() + } +} + +impl Substitutable for Variable { + type Result = Box; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let Variable { span, idx, name, .. } = self; + match by.get_subst(ctx, ctx.idx_to_lvl(*idx)) { + Some(exp) => exp, + None => Box::new(Exp::Variable(Variable { + span: *span, + idx: *idx, + name: name.clone(), + inferred_type: None, + })), + } + } +} + +impl Print for Variable { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + let Variable { name, idx, .. } = self; + if cfg.de_bruijn { + alloc.text(format!("{name}@{idx}")) + } else if name.id.is_empty() { + alloc.text(format!("@{idx}")) + } else { + alloc.text(&name.id) + } + } +} + +impl Zonk for Variable { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Variable { span: _, idx: _, name: _, inferred_type } = self; + inferred_type.zonk(meta_vars)?; + Ok(()) + } +} + +impl ContainsMetaVars for Variable { + fn contains_metavars(&self) -> bool { + let Variable { span: _, idx: _, name: _, inferred_type } = self; + + inferred_type.contains_metavars() + } +} + +// TypCtor +// +// + +/// A type constructor applied to arguments. The type of `TypCtor` +/// is always the type universe `Type`. +/// Examples: `Nat`, `List(Nat)` +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct TypCtor { + /// Source code location + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + /// Name of the type constructor + pub name: IdBound, + /// Arguments to the type constructor + pub args: Args, +} + +impl TypCtor { + pub fn to_exp(&self) -> Exp { + Exp::TypCtor(self.clone()) + } + + /// A type application is simple if the list of arguments is empty. + pub fn is_simple(&self) -> bool { + self.args.is_empty() + } +} + +impl HasSpan for TypCtor { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: TypCtor) -> Self { + Exp::TypCtor(val) + } +} + +impl Shift for TypCtor { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.args.shift_in_range(range, by); + } +} + +impl Occurs for TypCtor { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let TypCtor { args, .. } = self; + args.args.iter().any(|arg| arg.occurs(ctx, lvl)) + } +} + +impl HasType for TypCtor { + fn typ(&self) -> Option> { + Some(Box::new(TypeUniv::new().into())) + } +} + +impl Substitutable for TypCtor { + type Result = TypCtor; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self { + let TypCtor { span, name, args } = self; + TypCtor { span: *span, name: name.clone(), args: args.subst(ctx, by) } + } +} + +impl Print for TypCtor { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + prec: Precedence, + ) -> Builder<'a> { + let TypCtor { span: _, name, args } = self; + if name.id == "Fun" && args.len() == 2 && cfg.print_function_sugar { + let arg = args.args[0].print_prec(cfg, alloc, 1); + let res = args.args[1].print_prec(cfg, alloc, 0); + let fun = arg.append(alloc.space()).append(ARROW).append(alloc.space()).append(res); + if prec == 0 { + fun + } else { + fun.parens() + } + } else { + let psubst = if args.is_empty() { alloc.nil() } else { args.print(cfg, alloc) }; + alloc.typ(&name.id).append(psubst) + } + } +} + +/// Implement Zonk for TypCtor +impl Zonk for TypCtor { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let TypCtor { span: _, name: _, args } = self; + args.zonk(meta_vars) + } +} + +impl ContainsMetaVars for TypCtor { + fn contains_metavars(&self) -> bool { + let TypCtor { span: _, name: _, args } = self; + + args.contains_metavars() + } +} + +// Call +// +// + +/// A Call expression can be one of three different kinds: +/// - A constructor introduced by a data type declaration +/// - A codefinition introduced at the toplevel +/// - A LetBound definition introduced at the toplevel +#[derive(Debug, Clone, Copy, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub enum CallKind { + Constructor, + Codefinition, + LetBound, +} + +/// A Call invokes a constructor, a codefinition or a toplevel let-bound definition. +/// Examples: `Zero`, `Cons(True, Nil)`, `minimum(x,y)` +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Call { + /// Source code location + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + /// Whether the call is a constructor, codefinition or let bound definition. + pub kind: CallKind, + /// The name of the call. + /// The `f` in `f(e1...en)` + pub name: IdBound, + /// The arguments to the call. + /// The `(e1...en)` in `f(e1...en)` + pub args: Args, + /// The inferred result type of the call. + /// This type is annotated during elaboration. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_type: Option>, +} + +impl HasSpan for Call { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: Call) -> Self { + Exp::Call(val) + } +} + +impl Shift for Call { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.args.shift_in_range(range, by); + self.inferred_type = None; + } +} + +impl Occurs for Call { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let Call { args, .. } = self; + args.args.iter().any(|arg| arg.occurs(ctx, lvl)) + } +} + +impl HasType for Call { + fn typ(&self) -> Option> { + self.inferred_type.clone() + } +} + +impl Substitutable for Call { + type Result = Call; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let Call { span, name, args, kind, .. } = self; + Call { + span: *span, + kind: *kind, + name: name.clone(), + args: args.subst(ctx, by), + inferred_type: None, + } + } +} + +impl Print for Call { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + let Call { name, args, .. } = self; + let psubst = if args.is_empty() { alloc.nil() } else { args.print(cfg, alloc) }; + alloc.ctor(&name.id).append(psubst) + } +} + +impl Zonk for Call { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Call { span: _, kind: _, name: _, args, inferred_type } = self; + args.zonk(meta_vars)?; + inferred_type.zonk(meta_vars)?; + Ok(()) + } +} + +impl ContainsMetaVars for Call { + fn contains_metavars(&self) -> bool { + let Call { span: _, kind: _, name: _, args, inferred_type } = self; + + args.contains_metavars() || inferred_type.contains_metavars() + } +} + +// DotCall +// +// + +/// A DotCall expression can be one of two different kinds: +/// - A destructor introduced by a codata type declaration +/// - A definition introduced at the toplevel +#[derive(Debug, Clone, Copy, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub enum DotCallKind { + Destructor, + Definition, +} + +/// A DotCall is either a destructor or a definition, applied to a destructee +/// Examples: `e.head` `xs.append(ys)` +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct DotCall { + /// Source code location + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + /// Whether the dotcall is a destructor or codefinition. + pub kind: DotCallKind, + /// The expression to which the dotcall is applied. + /// The `e` in `e.f(e1...en)` + pub exp: Box, + /// The name of the dotcall. + /// The `f` in `e.f(e1...en)` + pub name: IdBound, + /// The arguments of the dotcall. + /// The `(e1...en)` in `e.f(e1...en)` + pub args: Args, + /// The inferred result type of the dotcall. + /// This type is annotated during elaboration. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_type: Option>, +} + +impl HasSpan for DotCall { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: DotCall) -> Self { + Exp::DotCall(val) + } +} + +impl Shift for DotCall { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.exp.shift_in_range(range, by); + self.args.shift_in_range(range, by); + self.inferred_type = None; + } +} + +impl Occurs for DotCall { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let DotCall { exp, args, .. } = self; + exp.occurs(ctx, lvl) || args.args.iter().any(|arg| arg.occurs(ctx, lvl)) + } +} + +impl HasType for DotCall { + fn typ(&self) -> Option> { + self.inferred_type.clone() + } +} + +impl Substitutable for DotCall { + type Result = DotCall; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let DotCall { span, kind, exp, name, args, .. } = self; + DotCall { + span: *span, + kind: *kind, + exp: exp.subst(ctx, by), + name: name.clone(), + args: args.subst(ctx, by), + inferred_type: None, + } + } +} + +impl Zonk for DotCall { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let DotCall { span: _, kind: _, exp, name: _, args, inferred_type } = self; + exp.zonk(meta_vars)?; + args.zonk(meta_vars)?; + inferred_type.zonk(meta_vars)?; + Ok(()) + } +} + +impl ContainsMetaVars for DotCall { + fn contains_metavars(&self) -> bool { + let DotCall { span: _, kind: _, exp, name: _, args, inferred_type } = self; + + exp.contains_metavars() || args.contains_metavars() || inferred_type.contains_metavars() + } +} + +impl Print for DotCall { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + // A series of destructors forms an aligned group + let mut dtors_group = alloc.nil(); + + // First DotCall + let psubst = if self.args.is_empty() { alloc.nil() } else { self.args.print(cfg, alloc) }; + dtors_group = + alloc.text(DOT).append(alloc.dtor(&self.name.id)).append(psubst).append(dtors_group); + + // Remaining DotCalls + let mut dtor: &Exp = &self.exp; + while let Exp::DotCall(DotCall { exp, name, args, .. }) = &dtor { + let psubst = if args.is_empty() { alloc.nil() } else { args.print(cfg, alloc) }; + dtors_group = alloc.line_().append(dtors_group); + dtors_group = + alloc.text(DOT).append(alloc.dtor(&name.id)).append(psubst).append(dtors_group); + dtor = exp; + } + dtor.print(cfg, alloc).append(dtors_group.align().group()) + } +} +// Anno +// +// + +/// Type annotated term `e : t` +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Anno { + /// Source code location + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + /// The annotated term, i.e. `e` in `e : t` + pub exp: Box, + /// The annotated type, i.e. `t` in `e : t` + pub typ: Box, + /// The annotated type written by the user might not + /// be in normal form. After elaboration we therefore + /// annotate the normalized type. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub normalized_type: Option>, +} + +impl HasSpan for Anno { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: Anno) -> Self { + Exp::Anno(val) + } +} + +impl Shift for Anno { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.exp.shift_in_range(range, by); + self.typ.shift_in_range(range, by); + self.normalized_type = None; + } +} + +impl Occurs for Anno { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let Anno { exp, typ, .. } = self; + exp.occurs(ctx, lvl) || typ.occurs(ctx, lvl) + } +} + +impl HasType for Anno { + fn typ(&self) -> Option> { + self.normalized_type.clone() + } +} + +impl Substitutable for Anno { + type Result = Anno; + + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let Anno { span, exp, typ, .. } = self; + Anno { + span: *span, + exp: exp.subst(ctx, by), + typ: typ.subst(ctx, by), + normalized_type: None, + } + } +} + +impl Print for Anno { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + let Anno { exp, typ, .. } = self; + exp.print(cfg, alloc).parens().append(COLON).append(typ.print(cfg, alloc)) + } +} + +impl Zonk for Anno { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Anno { span: _, exp, typ, normalized_type } = self; + exp.zonk(meta_vars)?; + typ.zonk(meta_vars)?; + normalized_type.zonk(meta_vars)?; + Ok(()) + } +} + +impl ContainsMetaVars for Anno { + fn contains_metavars(&self) -> bool { + let Anno { span: _, exp, typ, normalized_type } = self; + + exp.contains_metavars() || typ.contains_metavars() || normalized_type.contains_metavars() + } +} + +// TypeUniv +// +// + +/// The impredicative type universe "Type" is used +/// for typing data and codata types. I.e. we have +/// - `Nat : Type` +/// - `Stream(Nat) : Type` +/// - `Type : Type` +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct TypeUniv { + /// Source code location + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, +} + +impl TypeUniv { + pub fn new() -> TypeUniv { + TypeUniv { span: None } + } +} + +impl HasSpan for TypeUniv { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: TypeUniv) -> Self { + Exp::TypeUniv(val) + } +} + +impl Default for TypeUniv { + fn default() -> Self { + Self::new() + } +} + +impl Shift for TypeUniv { + fn shift_in_range(&mut self, _range: &R, _by: (isize, isize)) {} +} + +impl Occurs for TypeUniv { + fn occurs(&self, _ctx: &mut LevelCtx, _lvl: Lvl) -> bool { + false + } +} + +impl HasType for TypeUniv { + fn typ(&self) -> Option> { + Some(Box::new(TypeUniv::new().into())) + } +} + +impl Substitutable for TypeUniv { + type Result = TypeUniv; + + fn subst(&self, _ctx: &mut LevelCtx, _by: &S) -> Self::Result { + let TypeUniv { span } = self; + TypeUniv { span: *span } + } +} + +impl Print for TypeUniv { + fn print_prec<'a>( + &'a self, + _cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + alloc.keyword(TYPE) + } +} + +/// Implement Zonk for TypeUniv +impl Zonk for TypeUniv { + fn zonk( + &mut self, + _meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + // TypeUniv has no fields that require zonking + Ok(()) + } +} + +impl ContainsMetaVars for TypeUniv { + fn contains_metavars(&self) -> bool { + false + } +} + +// LocalMatch +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct LocalMatch { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub ctx: Option, + pub name: Label, + pub on_exp: Box, + pub motive: Option, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub ret_typ: Option>, + pub cases: Vec, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_type: Option, +} + +impl HasSpan for LocalMatch { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: LocalMatch) -> Self { + Exp::LocalMatch(val) + } +} + +impl Shift for LocalMatch { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.ctx = None; + self.on_exp.shift_in_range(range, by); + self.motive.shift_in_range(range, by); + self.ret_typ = None; + self.cases.shift_in_range(range, by); + self.inferred_type = None; + } +} + +impl Occurs for LocalMatch { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let LocalMatch { on_exp, cases, .. } = self; + on_exp.occurs(ctx, lvl) || cases.occurs(ctx, lvl) + } +} + +impl HasType for LocalMatch { + fn typ(&self) -> Option> { + self.inferred_type.clone().map(|x| Box::new(x.into())) + } +} + +impl Substitutable for LocalMatch { + type Result = LocalMatch; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let LocalMatch { span, name, on_exp, motive, ret_typ, cases, .. } = self; + LocalMatch { + span: *span, + ctx: None, + name: name.clone(), + on_exp: on_exp.subst(ctx, by), + motive: motive.subst(ctx, by), + ret_typ: ret_typ.subst(ctx, by), + cases: cases.iter().map(|case| case.subst(ctx, by)).collect(), + inferred_type: None, + } + } +} + +impl Print for LocalMatch { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + let LocalMatch { name, on_exp, motive, cases, .. } = self; + on_exp + .print(cfg, alloc) + .append(DOT) + .append(alloc.keyword(MATCH)) + .append(match &name.user_name { + Some(name) => alloc.space().append(alloc.dtor(&name.id)), + None => alloc.nil(), + }) + .append(motive.as_ref().map(|m| m.print(cfg, alloc)).unwrap_or(alloc.nil())) + .append(alloc.space()) + .append(print_cases(cases, cfg, alloc)) + } +} + +impl Zonk for LocalMatch { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let LocalMatch { span: _, ctx: _, name: _, on_exp, motive, ret_typ, cases, inferred_type } = + self; + on_exp.zonk(meta_vars)?; + motive.zonk(meta_vars)?; + ret_typ.zonk(meta_vars)?; + inferred_type.zonk(meta_vars)?; + for case in cases { + case.zonk(meta_vars)?; + } + Ok(()) + } +} + +impl ContainsMetaVars for LocalMatch { + fn contains_metavars(&self) -> bool { + let LocalMatch { span: _, ctx: _, name: _, on_exp, motive, ret_typ, cases, inferred_type } = + self; + + on_exp.contains_metavars() + || motive.contains_metavars() + || ret_typ.contains_metavars() + || cases.contains_metavars() + || inferred_type.contains_metavars() + } +} + +// LocalComatch +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct LocalComatch { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub ctx: Option, + pub name: Label, + pub is_lambda_sugar: bool, + pub cases: Vec, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_type: Option, +} + +impl HasSpan for LocalComatch { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: LocalComatch) -> Self { + Exp::LocalComatch(val) + } +} + +impl Shift for LocalComatch { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.ctx = None; + self.cases.shift_in_range(range, by); + self.inferred_type = None; + } +} + +impl Occurs for LocalComatch { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let LocalComatch { cases, .. } = self; + cases.occurs(ctx, lvl) + } +} + +impl HasType for LocalComatch { + fn typ(&self) -> Option> { + self.inferred_type.clone().map(|x| Box::new(x.into())) + } +} + +impl Substitutable for LocalComatch { + type Result = LocalComatch; + + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let LocalComatch { span, name, is_lambda_sugar, cases, .. } = self; + LocalComatch { + span: *span, + ctx: None, + name: name.clone(), + is_lambda_sugar: *is_lambda_sugar, + cases: cases.iter().map(|case| case.subst(ctx, by)).collect(), + inferred_type: None, + } + } +} + +impl Print for LocalComatch { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + _prec: Precedence, + ) -> Builder<'a> { + let LocalComatch { name, is_lambda_sugar, cases, .. } = self; + if *is_lambda_sugar && cfg.print_lambda_sugar { + print_lambda_sugar(cases, cfg, alloc) + } else { + alloc + .keyword(COMATCH) + .append(match &name.user_name { + Some(name) => alloc.space().append(alloc.ctor(&name.id)), + None => alloc.nil(), + }) + .append(alloc.space()) + .append(print_cases(cases, cfg, alloc)) + } + } +} + +impl Zonk for LocalComatch { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let LocalComatch { span: _, ctx: _, name: _, is_lambda_sugar: _, cases, inferred_type } = + self; + inferred_type.zonk(meta_vars)?; + for case in cases { + case.zonk(meta_vars)?; + } + Ok(()) + } +} + +impl ContainsMetaVars for LocalComatch { + fn contains_metavars(&self) -> bool { + let LocalComatch { span: _, ctx: _, name: _, is_lambda_sugar: _, cases, inferred_type } = + self; + + cases.contains_metavars() || inferred_type.contains_metavars() + } +} + +/// Print the Comatch as a lambda abstraction. +/// Only invoke this function if the comatch contains exactly +/// one cocase "ap" with three arguments; the function will +/// panic otherwise. +fn print_lambda_sugar<'a>(cases: &'a [Case], cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + let Case { pattern, body, .. } = cases.first().expect("Empty comatch marked as lambda sugar"); + let var_name = &pattern + .params + .params + .get(2) // The variable we want to print is at the third position: comatch { ap(_,_,x) => ...} + .expect("No parameter bound in comatch marked as lambda sugar") + .name; + alloc + .backslash_anno(cfg) + .append(&var_name.id) + .append(DOT) + .append(alloc.space()) + .append(body.print(cfg, alloc)) +} + +// Hole +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Hole { + /// Source code location + pub span: Option, + /// Whether the hole must be solved during typechecking or not. + pub kind: MetaVarKind, + /// The metavariable that we want to solve for that hole + pub metavar: MetaVar, + /// The inferred type of the hole annotated during elaboration. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_type: Option>, + /// The type context in which the hole occurs. + /// This context is annotated during elaboration. + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub inferred_ctx: Option, + /// When a hole is lowered, we apply it to all variables available in the + /// context, since intuitively, a hole stands for an unknown term which can use + /// any of these variables. + /// Some other implementations use a functional application to all variables instead, + /// but since we do not have a function type we have to use an explicit substitution. + /// Since our system uses 2-level De-Bruijn indices, the explicit substitution id_Г + /// is a nested vector. + /// + /// Example: + /// [x, y][z][v, w] |- ?[x, y][z][v,w] + pub args: Vec>>, + /// The solution found by unification. It is propagated during zonking. + pub solution: Option>, +} + +impl HasSpan for Hole { + fn span(&self) -> Option { + self.span + } +} + +impl From for Exp { + fn from(val: Hole) -> Self { + Exp::Hole(val) + } +} + +impl Shift for Hole { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + let Hole { span: _, kind: _, metavar: _, inferred_type, inferred_ctx, args, solution } = + self; + + *inferred_type = None; + *inferred_ctx = None; + args.shift_in_range(range, by); + solution.shift_in_range(range, by); + } +} + +impl Occurs for Hole { + fn occurs(&self, _ctx: &mut LevelCtx, _lvl: Lvl) -> bool { + false + } +} + +impl HasType for Hole { + fn typ(&self) -> Option> { + self.inferred_type.clone() + } +} + +impl Substitutable for Hole { + type Result = Hole; + + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let Hole { span, kind, metavar, args, .. } = self; + Hole { + span: *span, + kind: *kind, + metavar: *metavar, + inferred_type: None, + inferred_ctx: None, + args: args.subst(ctx, by), + solution: self.solution.subst(ctx, by), + } + } +} + +impl Print for Hole { + fn print_prec<'a>( + &'a self, + cfg: &PrintCfg, + alloc: &'a Alloc<'a>, + prec: Precedence, + ) -> Builder<'a> { + match self.kind { + MetaVarKind::MustSolve => { + let mut doc = alloc.keyword(UNDERSCORE); + + if cfg.print_metavar_ids { + doc = doc.append(self.metavar.id.to_string()); + } + + if let Some(solution) = &self.solution { + doc = doc.append("<").append(solution.print_prec(cfg, alloc, prec)).append(">") + } + + doc + } + MetaVarKind::CanSolve => { + let mut doc = alloc.keyword(QUESTION_MARK); + + if cfg.print_metavar_ids { + doc = doc.append(self.metavar.id.to_string()); + } + + if let Some(solution) = &self.solution { + doc = doc.append("<").append(solution.print_prec(cfg, alloc, prec)).append(">") + } + + doc + } + MetaVarKind::Inserted => { + let mut doc = alloc.nil(); + + if cfg.print_metavar_ids { + doc = doc.append(self.metavar.id.to_string()); + } + + match &self.solution { + Some(solution) => { + doc = doc + .append("<") + .append(solution.print_prec(cfg, alloc, prec)) + .append(">") + } + None => doc = doc.append(""), + } + + doc + } + } + } +} + +impl Zonk for Hole { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + match meta_vars.get(&self.metavar) { + Some(crate::MetaVarState::Solved { ctx, solution }) => { + self.solution = Some(solution.subst_under_ctx(ctx.levels(), &self.args)); + } + Some(crate::MetaVarState::Unsolved { .. }) => { + // Nothing to do, the hole remains unsolved + } + None => { + return Err(ZonkError::UnboundMetaVar(self.metavar)); + } + } + + Ok(()) + } +} + +impl ContainsMetaVars for Hole { + fn contains_metavars(&self) -> bool { + let Hole { span: _, kind: _, metavar, inferred_type, inferred_ctx: _, args, solution } = + self; + + inferred_type.contains_metavars() + || args.contains_metavars() + || solution.contains_metavars() + || metavar.must_be_solved() && solution.is_none() + } +} + +// Pattern +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Pattern { + pub is_copattern: bool, + pub name: IdBound, + pub params: TelescopeInst, +} + +impl Print for Pattern { + fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + let Pattern { is_copattern, name, params } = self; + if *is_copattern { + alloc.text(DOT).append(alloc.ctor(&name.id)).append(params.print(cfg, alloc)) + } else { + alloc.ctor(&name.id).append(params.print(cfg, alloc)) + } + } +} + +impl Zonk for Pattern { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Pattern { is_copattern: _, name: _, params } = self; + params.zonk(meta_vars) + } +} + +// Case +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Case { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + pub pattern: Pattern, + /// Body being `None` represents an absurd pattern + pub body: Option>, +} + +impl Shift for Case { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.body.shift_in_range(&range.clone().shift(1), by); + } +} + +impl Occurs for Case { + fn occurs(&self, ctx: &mut LevelCtx, lvl: Lvl) -> bool { + let Case { pattern, body, .. } = self; + ctx.bind_iter(pattern.params.params.iter().map(|_| ()), |ctx| body.occurs(ctx, lvl)) + } +} + +impl Substitutable for Case { + type Result = Case; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self { + let Case { span, pattern, body } = self; + ctx.bind_iter(pattern.params.params.iter(), |ctx| Case { + span: *span, + pattern: pattern.clone(), + body: body.as_ref().map(|body| { + let mut by = (*by).clone(); + by.shift((1, 0)); + body.subst(ctx, &by) + }), + }) + } +} + +impl Print for Case { + fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + let Case { span: _, pattern, body } = self; + + let body = match body { + None => alloc.keyword(ABSURD), + Some(body) => alloc + .text(FAT_ARROW) + .append(alloc.line()) + .append(body.print(cfg, alloc)) + .nest(cfg.indent), + }; + + pattern.print(cfg, alloc).append(alloc.space()).append(body).group() + } +} + +impl Zonk for Case { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Case { span: _, pattern, body } = self; + pattern.zonk(meta_vars)?; + body.zonk(meta_vars)?; + Ok(()) + } +} + +pub fn print_cases<'a>(cases: &'a [Case], cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + match cases.len() { + 0 => empty_braces(alloc), + + 1 => alloc + .line() + .append(cases[0].print(cfg, alloc)) + .nest(cfg.indent) + .append(alloc.line()) + .braces_anno() + .group(), + _ => { + let sep = alloc.text(COMMA).append(alloc.hardline()); + alloc + .hardline() + .append(alloc.intersperse(cases.iter().map(|x| x.print(cfg, alloc)), sep.clone())) + .nest(cfg.indent) + .append(alloc.hardline()) + .braces_anno() + } + } +} + +impl ContainsMetaVars for Case { + fn contains_metavars(&self) -> bool { + let Case { span: _, pattern: _, body } = self; + + body.contains_metavars() + } +} + +// Telescope Inst +// +// + +/// Instantiation of a previously declared telescope +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct TelescopeInst { + pub params: Vec, +} + +impl TelescopeInst { + pub fn len(&self) -> usize { + self.params.len() + } + + pub fn is_empty(&self) -> bool { + self.params.is_empty() + } +} + +impl Print for TelescopeInst { + fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + if self.params.is_empty() { + alloc.nil() + } else { + self.params.print(cfg, alloc).parens() + } + } +} + +impl Zonk for TelescopeInst { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let TelescopeInst { params } = self; + + for param in params { + param.zonk(meta_vars)?; + } + Ok(()) + } +} + +impl ContainsMetaVars for TelescopeInst { + fn contains_metavars(&self) -> bool { + let TelescopeInst { params } = self; + + params.contains_metavars() + } +} + +// ParamInst +// +// + +/// Instantiation of a previously declared parameter +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct ParamInst { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub info: Option>, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub name: VarBind, + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub typ: Option>, +} + +impl Print for ParamInst { + fn print<'a>(&'a self, _cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + let ParamInst { span: _, info: _, name, typ: _ } = self; + alloc.text(&name.id) + } +} + +impl Zonk for ParamInst { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let ParamInst { span: _, info, name: _, typ } = self; + + info.zonk(meta_vars)?; + typ.zonk(meta_vars)?; + Ok(()) + } +} + +impl ContainsMetaVars for ParamInst { + fn contains_metavars(&self) -> bool { + let ParamInst { span: _, info, name: _, typ } = self; + + info.contains_metavars() || typ.contains_metavars() + } +} + +// Args +// +// + +/// A list of arguments +/// In dependent type theory, this concept is usually called a "substitution" but that name would be confusing in this implementation +/// because it conflicts with the operation of substitution (i.e. substituting a terms for a variable in another term). +/// In particular, while we often substitute argument lists for telescopes, this is not always the case. +/// Substitutions in the sense of argument lists are a special case of a more general concept of context morphisms. +/// Unifiers are another example of context morphisms and applying a unifier to an expression mean substituting various terms, +/// which are not necessarily part of a single argument list. +#[derive(Debug, Clone, Eq, PartialEq, Hash)] +pub struct Args { + pub args: Vec, +} + +impl Args { + pub fn to_exps(&self) -> Vec> { + self.args.iter().map(|arg| arg.exp().clone()).collect() + } + + pub fn len(&self) -> usize { + self.args.len() + } + + pub fn is_empty(&self) -> bool { + self.args.is_empty() + } +} + +impl Shift for Args { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.args.shift_in_range(range, by); + } +} + +impl Substitutable for Args { + type Result = Args; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self { + Args { args: self.args.subst(ctx, by) } + } +} + +impl Print for Args { + fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + let mut doc = alloc.nil(); + let mut first = true; + + for arg in &self.args { + if !arg.is_inserted_implicit() { + if !first { + doc = doc.append(COMMA).append(alloc.line()); + } + doc = doc.append(arg.print(cfg, alloc)); + first = false; + } + } + + doc.align().parens().group() + } +} + +impl Zonk for Args { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Args { args } = self; + + for arg in args { + arg.zonk(meta_vars)?; + } + Ok(()) + } +} + +impl ContainsMetaVars for Args { + fn contains_metavars(&self) -> bool { + let Args { args } = self; + + args.contains_metavars() + } +} + +// Motive +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct Motive { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + pub param: ParamInst, + pub ret_typ: Box, +} + +impl Shift for Motive { + fn shift_in_range(&mut self, range: &R, by: (isize, isize)) { + self.ret_typ.shift_in_range(&range.clone().shift(1), by); + } +} + +impl Substitutable for Motive { + type Result = Motive; + fn subst(&self, ctx: &mut LevelCtx, by: &S) -> Self::Result { + let Motive { span, param, ret_typ } = self; + + Motive { + span: *span, + param: param.clone(), + ret_typ: ctx.bind_single((), |ctx| { + let mut by = (*by).clone(); + by.shift((1, 0)); + ret_typ.subst(ctx, &by) + }), + } + } +} + +impl Print for Motive { + fn print<'a>(&'a self, cfg: &PrintCfg, alloc: &'a Alloc<'a>) -> Builder<'a> { + let Motive { span: _, param, ret_typ } = self; + + alloc + .space() + .append(alloc.keyword(AS)) + .append(alloc.space()) + .append(param.print(cfg, alloc)) + .append(alloc.space()) + .append(alloc.text(FAT_ARROW)) + .append(alloc.space()) + .append(ret_typ.print(cfg, alloc)) + } +} + +impl Zonk for Motive { + fn zonk( + &mut self, + meta_vars: &crate::HashMap, + ) -> Result<(), ZonkError> { + let Motive { span: _, param, ret_typ } = self; + param.zonk(meta_vars)?; + ret_typ.zonk(meta_vars)?; + Ok(()) + } +} + +impl ContainsMetaVars for Motive { + fn contains_metavars(&self) -> bool { + let Motive { span: _, param, ret_typ } = self; + + param.contains_metavars() || ret_typ.contains_metavars() + } +} diff --git a/lang/ast/src/ident.rs b/lang/ast/src/ident.rs index 5b3565f456..657d815d7d 100644 --- a/lang/ast/src/ident.rs +++ b/lang/ast/src/ident.rs @@ -10,32 +10,156 @@ use printer::{ use crate::HasSpan; +// Local variables (binding site) +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct VarBind { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + pub id: String, +} + +impl VarBind { + pub fn from_string(id: &str) -> Self { + VarBind { span: None, id: id.to_owned() } + } +} + +impl fmt::Display for VarBind { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.id) + } +} + +impl HasSpan for VarBind { + fn span(&self) -> Option { + self.span + } +} + +// Local variables (bound occurence) +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct VarBound { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + pub id: String, +} + +impl VarBound { + pub fn from_string(id: &str) -> Self { + VarBound { span: None, id: id.to_owned() } + } +} + +impl fmt::Display for VarBound { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.id) + } +} + +impl HasSpan for VarBound { + fn span(&self) -> Option { + self.span + } +} + +impl From for VarBound { + fn from(var: VarBind) -> Self { + VarBound { span: var.span, id: var.id } + } +} + +// Global identifiers (binding site) +// +// + #[derive(Debug, Clone, Derivative)] #[derivative(Eq, PartialEq, Hash)] -pub struct Ident { +pub struct IdBind { #[derivative(PartialEq = "ignore", Hash = "ignore")] pub span: Option, pub id: String, } -impl Ident { +impl IdBind { pub fn from_string(id: &str) -> Self { - Ident { span: None, id: id.to_owned() } + IdBind { span: None, id: id.to_owned() } } } -impl fmt::Display for Ident { +impl fmt::Display for IdBind { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { write!(f, "{}", self.id) } } -impl HasSpan for Ident { +impl HasSpan for IdBind { fn span(&self) -> Option { self.span } } +impl From for IdBind { + fn from(id: IdBound) -> Self { + IdBind { span: id.span, id: id.id } + } +} + +impl PartialEq for IdBind { + fn eq(&self, other: &IdBound) -> bool { + self.id == other.id + } +} + +impl PartialEq for IdBound { + fn eq(&self, other: &IdBind) -> bool { + self.id == other.id + } +} + +// Global identifiers (bound occurence) +// +// + +#[derive(Debug, Clone, Derivative)] +#[derivative(Eq, PartialEq, Hash)] +pub struct IdBound { + #[derivative(PartialEq = "ignore", Hash = "ignore")] + pub span: Option, + pub id: String, +} + +impl IdBound { + pub fn from_string(id: &str) -> Self { + IdBound { span: None, id: id.to_owned() } + } +} + +impl fmt::Display for IdBound { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.id) + } +} + +impl HasSpan for IdBound { + fn span(&self) -> Option { + self.span + } +} + +impl From for IdBound { + fn from(id: IdBind) -> Self { + IdBound { span: id.span, id: id.id } + } +} + /// Whether the metavariable corresponds to a typed hole written by the user /// or whether it was inserted during lowering for an implicit argument. #[derive(Debug, Clone, Copy, Derivative)] diff --git a/lang/ast/src/traits/identifiable.rs b/lang/ast/src/traits/identifiable.rs new file mode 100644 index 0000000000..76b5aa91f2 --- /dev/null +++ b/lang/ast/src/traits/identifiable.rs @@ -0,0 +1,21 @@ +use crate::IdBind; + +/// Trait for syntactic items which have a unique `name`. +pub trait GloballyIdentifiable { + fn ident(&self) -> &IdBind; +} + +impl GloballyIdentifiable for IdBind { + fn ident(&self) -> &IdBind { + self + } +} + +impl<'a, T> GloballyIdentifiable for &'a T +where + T: GloballyIdentifiable, +{ + fn ident(&self) -> &IdBind { + T::ident(self) + } +} diff --git a/lang/ast/src/traits/mod.rs b/lang/ast/src/traits/mod.rs index 679b26186c..30115523bf 100644 --- a/lang/ast/src/traits/mod.rs +++ b/lang/ast/src/traits/mod.rs @@ -1,7 +1,7 @@ mod contains_metavars; mod has_span; mod has_type; -pub mod named; +pub mod identifiable; mod occurs; mod shift; pub mod subst; @@ -10,7 +10,7 @@ mod zonk; pub use contains_metavars::*; pub use has_span::*; pub use has_type::*; -pub use named::*; +pub use identifiable::*; pub use occurs::*; pub use shift::*; pub use subst::*; diff --git a/lang/ast/src/traits/named.rs b/lang/ast/src/traits/named.rs deleted file mode 100644 index 04c5c610d3..0000000000 --- a/lang/ast/src/traits/named.rs +++ /dev/null @@ -1,21 +0,0 @@ -use crate::Ident; - -/// Trait for syntactic items which have a unique `name`. -pub trait Named { - fn name(&self) -> &Ident; -} - -impl Named for Ident { - fn name(&self) -> &Ident { - self - } -} - -impl<'a, T> Named for &'a T -where - T: Named, -{ - fn name(&self) -> &Ident { - T::name(self) - } -} diff --git a/lang/ast/src/traits/subst.rs b/lang/ast/src/traits/subst.rs index 470b6c3cae..e8adc7de82 100644 --- a/lang/ast/src/traits/subst.rs +++ b/lang/ast/src/traits/subst.rs @@ -146,7 +146,7 @@ impl Substitution for SwapSubst { Box::new(Exp::Variable(Variable { span: None, idx: new_ctx.lvl_to_idx(new_lvl), - name: Ident::from_string(""), + name: VarBound::from_string(""), inferred_type: None, })) }) diff --git a/lang/driver/src/info/lookup.rs b/lang/driver/src/info/lookup.rs index a53c0c41db..843b6b884b 100644 --- a/lang/driver/src/info/lookup.rs +++ b/lang/driver/src/info/lookup.rs @@ -1,13 +1,13 @@ -use ast::{Codef, Ctor, Decl, Def, Dtor, Ident, Let, Named}; +use ast::{Codef, Ctor, Decl, Def, Dtor, GloballyIdentifiable, IdBound, Let}; use url::Url; use crate::Database; -pub fn lookup_decl<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Decl)> { +pub fn lookup_decl<'a>(db: &'a Database, name: &IdBound) -> Option<(Url, &'a Decl)> { for uri in db.ust.keys() { match db.ust.get_unless_stale(uri) { Some(Ok(module)) => { - if let Some(decl) = module.decls.iter().find(|decl| decl.name() == name) { + if let Some(decl) = module.decls.iter().find(|decl| decl.ident() == name) { return Some((uri.clone(), decl)); } continue; @@ -18,7 +18,7 @@ pub fn lookup_decl<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Decl) None } -pub fn lookup_ctor<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Ctor)> { +pub fn lookup_ctor<'a>(db: &'a Database, name: &IdBound) -> Option<(Url, &'a Ctor)> { for uri in db.ust.keys() { match db.ust.get_unless_stale(uri) { Some(Ok(module)) => { @@ -35,7 +35,7 @@ pub fn lookup_ctor<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Ctor) None } -pub fn lookup_codef<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Codef)> { +pub fn lookup_codef<'a>(db: &'a Database, name: &IdBound) -> Option<(Url, &'a Codef)> { for uri in db.ust.keys() { match db.ust.get_unless_stale(uri) { Some(Ok(module)) => { @@ -52,7 +52,7 @@ pub fn lookup_codef<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Code None } -pub fn lookup_let<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Let)> { +pub fn lookup_let<'a>(db: &'a Database, name: &IdBound) -> Option<(Url, &'a Let)> { for uri in db.ust.keys() { match db.ust.get_unless_stale(uri) { Some(Ok(module)) => { @@ -69,7 +69,7 @@ pub fn lookup_let<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Let)> None } -pub fn lookup_dtor<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Dtor)> { +pub fn lookup_dtor<'a>(db: &'a Database, name: &IdBound) -> Option<(Url, &'a Dtor)> { for uri in db.ust.keys() { match db.ust.get_unless_stale(uri) { Some(Ok(module)) => { @@ -86,7 +86,7 @@ pub fn lookup_dtor<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Dtor) None } -pub fn lookup_def<'a>(db: &'a Database, name: &Ident) -> Option<(Url, &'a Def)> { +pub fn lookup_def<'a>(db: &'a Database, name: &IdBound) -> Option<(Url, &'a Def)> { for uri in db.ust.keys() { match db.ust.get_unless_stale(uri) { Some(Ok(module)) => { diff --git a/lang/driver/src/xfunc.rs b/lang/driver/src/xfunc.rs index a00190cc31..ee95a73cde 100644 --- a/lang/driver/src/xfunc.rs +++ b/lang/driver/src/xfunc.rs @@ -35,7 +35,7 @@ impl Database { let module = self.ast(uri)?; let decl_spans = - module.decls.iter().map(|decl| (decl.name().clone(), decl.span().unwrap())).collect(); + module.decls.iter().map(|decl| (decl.ident().clone(), decl.span().unwrap())).collect(); // xdefs and xtors before xfunc let xdefs = module.xdefs_for_type(type_name); @@ -52,16 +52,15 @@ impl Database { let mat = transformations::as_matrix(&module)?; - let type_span = mat.map.get(&Ident::from_string(type_name)).and_then(|x| x.span).ok_or( - XfuncError::Impossible { + let type_span = + mat.map.get(type_name).and_then(|x| x.span).ok_or(XfuncError::Impossible { message: format!("Could not resolve {type_name}"), span: None, - }, - )?; + })?; let original = Original { type_span, decl_spans, xdefs }; - let repr = transformations::repr(&mat, &Ident::from_string(type_name))?; + let repr = transformations::repr(&mat, &IdBound::from_string(type_name))?; let result = match repr { transformations::matrix::Repr::Data => refunctionalize(&mat, type_name), @@ -73,9 +72,9 @@ impl Database { } struct Original { - xdefs: Vec, + xdefs: Vec, type_span: Span, - decl_spans: HashMap, + decl_spans: HashMap, } struct XfuncResult { @@ -87,7 +86,7 @@ struct XfuncResult { fn generate_edits( module: &Module, original: Original, - dirty_decls: HashSet, + dirty_decls: HashSet, result: XfuncResult, ) -> Xfunc { let XfuncResult { title, new_decls } = result; @@ -125,7 +124,8 @@ fn generate_edits( } fn refunctionalize(mat: &matrix::Prg, type_name: &str) -> Result { - let (mut codata, mut codefs) = transformations::as_codata(mat, &Ident::from_string(type_name))?; + let (mut codata, mut codefs) = + transformations::as_codata(mat, &IdBound::from_string(type_name))?; codata.rename(); codefs.iter_mut().for_each(|codef| codef.rename()); @@ -137,7 +137,7 @@ fn refunctionalize(mat: &matrix::Prg, type_name: &str) -> Result Result { - let (mut data, mut defs) = transformations::as_data(mat, &Ident::from_string(type_name))?; + let (mut data, mut defs) = transformations::as_data(mat, &IdBound::from_string(type_name))?; data.rename(); defs.iter_mut().for_each(|def| def.rename()); diff --git a/lang/elaborator/src/normalizer/env.rs b/lang/elaborator/src/normalizer/env.rs index 20cd9c1308..badf5b8a5f 100644 --- a/lang/elaborator/src/normalizer/env.rs +++ b/lang/elaborator/src/normalizer/env.rs @@ -1,6 +1,6 @@ use derivative::Derivative; -use ast::{Ident, Shift, ShiftRange}; +use ast::{Shift, ShiftRange, VarBound}; use pretty::DocAllocator; use ast::ctx::values::TypeCtx; @@ -107,7 +107,7 @@ impl ToEnv for LevelCtx { let idx = Idx { fst: self.bound.len() - 1 - fst, snd: v.len() - 1 - snd }; Box::new(Val::Neu(Neu::Variable(Variable { span: None, - name: Ident::from_string(""), + name: VarBound::from_string(""), idx, }))) }) @@ -127,7 +127,7 @@ impl ToEnv for TypeCtx { Box::new(Val::Neu(Neu::Variable(Variable { // FIXME: handle info span: None, - name: binder.name.clone(), + name: binder.name.clone().into(), idx, }))) }) diff --git a/lang/elaborator/src/normalizer/eval.rs b/lang/elaborator/src/normalizer/eval.rs index 313d2af9c9..2e8260c378 100644 --- a/lang/elaborator/src/normalizer/eval.rs +++ b/lang/elaborator/src/normalizer/eval.rs @@ -73,7 +73,7 @@ impl Eval for Call { match kind { CallKind::LetBound => { let Let { attr, body, .. } = - prg.lookup_let(name).ok_or_else(|| TypeError::Impossible { + prg.lookup_let(&name.clone().into()).ok_or_else(|| TypeError::Impossible { message: format!("Top-level let {name} not found"), span: span.to_miette(), })?; @@ -147,9 +147,11 @@ impl Eval for DotCall { // First, we have to find the corresponding case in the toplevel definition `d`. let Def { cases, .. } = - prg.lookup_def(name).ok_or_else(|| TypeError::Impossible { - message: format!("Definition {name} not found"), - span: None, + 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 = @@ -180,8 +182,9 @@ 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).ok_or_else(|| TypeError::Impossible { + let Codef { cases, .. } = prg + .lookup_codef(&call_name.clone().into()) + .ok_or_else(|| TypeError::Impossible { message: format!("Codefinition {call_name} not found"), span: None, })?; diff --git a/lang/elaborator/src/normalizer/val.rs b/lang/elaborator/src/normalizer/val.rs index 7eb6bef933..acc75a6079 100644 --- a/lang/elaborator/src/normalizer/val.rs +++ b/lang/elaborator/src/normalizer/val.rs @@ -1,12 +1,12 @@ use ast; use ast::ctx::BindContext; use ast::shift_and_clone; -use ast::Ident; use ast::Idx; use ast::MetaVar; use ast::Shift; use ast::ShiftRange; use ast::ShiftRangeExt; +use ast::VarBound; use codespan::Span; use derivative::Derivative; use log::trace; @@ -134,7 +134,7 @@ impl ReadBack for Val { pub struct TypCtor { #[derivative(PartialEq = "ignore", Hash = "ignore")] pub span: Option, - pub name: ast::Ident, + pub name: ast::IdBound, pub args: Args, } @@ -181,7 +181,7 @@ pub struct Call { #[derivative(PartialEq = "ignore", Hash = "ignore")] pub span: Option, pub kind: ast::CallKind, - pub name: ast::Ident, + pub name: ast::IdBound, pub args: Args, } @@ -381,7 +381,7 @@ pub struct Variable { #[derivative(PartialEq = "ignore", Hash = "ignore")] pub span: Option, #[derivative(PartialEq = "ignore", Hash = "ignore")] - pub name: ast::Ident, + pub name: ast::VarBound, pub idx: Idx, } @@ -424,7 +424,7 @@ pub struct DotCall { pub span: Option, pub kind: ast::DotCallKind, pub exp: Box, - pub name: ast::Ident, + pub name: ast::IdBound, pub args: Args, } @@ -589,7 +589,7 @@ pub struct Case { #[derivative(PartialEq = "ignore", Hash = "ignore")] pub span: Option, pub is_copattern: bool, - pub name: ast::Ident, + pub name: ast::IdBound, pub params: ast::TelescopeInst, /// Body being `None` represents an absurd pattern pub body: Option, @@ -651,7 +651,7 @@ impl ReadBack for Case { pub struct OpaqueCall { #[derivative(PartialEq = "ignore", Hash = "ignore")] pub span: Option, - pub name: ast::Ident, + pub name: ast::IdBound, pub args: Args, } @@ -749,7 +749,7 @@ impl Print for Args { #[derivative(Eq, PartialEq, Hash)] pub enum Arg { UnnamedArg(Box), - NamedArg(ast::Ident, Box), + NamedArg(ast::VarBound, Box), InsertedImplicitArg(Box), } @@ -841,7 +841,7 @@ impl ReadBack for Closure { .map(|snd| { Val::Neu(Neu::Variable(Variable { span: None, - name: Ident::from_string(""), + name: VarBound::from_string(""), idx: Idx { fst: 0, snd }, })) }) diff --git a/lang/elaborator/src/result.rs b/lang/elaborator/src/result.rs index f5d33ef4fc..08b1bf0589 100644 --- a/lang/elaborator/src/result.rs +++ b/lang/elaborator/src/result.rs @@ -39,14 +39,14 @@ pub enum TypeError { #[error("Cannot match on codata type {name}")] #[diagnostic(code("T-003"))] MatchOnCodata { - name: Ident, + name: IdBound, #[label] span: Option, }, #[error("Cannot comatch on data type {name}")] #[diagnostic(code("T-004"))] ComatchOnData { - name: Ident, + name: IdBound, #[label] span: Option, }, @@ -60,22 +60,22 @@ pub enum TypeError { #[error("Got {actual}, which is not in type {expected}")] #[diagnostic(code("T-006"))] NotInType { - expected: Ident, - actual: Ident, + expected: IdBind, + actual: IdBound, #[label] span: Option, }, #[error("Pattern for {name} is marked as absurd but that could not be proven")] #[diagnostic(code("T-007"))] PatternIsNotAbsurd { - name: Ident, + name: IdBound, #[label] span: Option, }, #[error("Pattern for {name} is absurd and must be marked accordingly")] #[diagnostic(code("T-008"))] PatternIsAbsurd { - name: Ident, + name: IdBound, #[label] span: Option, }, diff --git a/lang/elaborator/src/typechecker/decls/codatatype.rs b/lang/elaborator/src/typechecker/decls/codatatype.rs index eb87830de0..68dd192a78 100644 --- a/lang/elaborator/src/typechecker/decls/codatatype.rs +++ b/lang/elaborator/src/typechecker/decls/codatatype.rs @@ -36,7 +36,7 @@ impl CheckToplevel for Codata { } /// Infer a destructor declaration -fn check_dtor_wf(codata_name: &Ident, dtor: &Dtor, ctx: &mut Ctx) -> Result { +fn check_dtor_wf(codata_name: &IdBind, dtor: &Dtor, ctx: &mut Ctx) -> Result { trace!("Checking well-formedness of destructor: {}", dtor.name); let Dtor { span, doc, name, params, self_param, ret_typ } = dtor; diff --git a/lang/elaborator/src/typechecker/decls/datatype.rs b/lang/elaborator/src/typechecker/decls/datatype.rs index ca7218a21a..7d8c48299c 100644 --- a/lang/elaborator/src/typechecker/decls/datatype.rs +++ b/lang/elaborator/src/typechecker/decls/datatype.rs @@ -36,7 +36,7 @@ impl CheckToplevel for Data { } /// Infer a constructor declaration -fn check_ctor_wf(data_type_name: &Ident, ctor: &Ctor, ctx: &mut Ctx) -> Result { +fn check_ctor_wf(data_type_name: &IdBind, ctor: &Ctor, ctx: &mut Ctx) -> Result { trace!("Checking well-formedness of constructor: {}", ctor.name); let Ctor { span, doc, name, params, typ } = ctor; diff --git a/lang/elaborator/src/typechecker/decls/mod.rs b/lang/elaborator/src/typechecker/decls/mod.rs index 42baae5883..7e91357810 100644 --- a/lang/elaborator/src/typechecker/decls/mod.rs +++ b/lang/elaborator/src/typechecker/decls/mod.rs @@ -84,7 +84,7 @@ fn check_metavars_resolved( for decl in decls { if decl.contains_metavars() { return Err(TypeError::Impossible { - message: format!("Declaration {} contains unresolved metavariables", decl.name()), + message: format!("Declaration {} contains unresolved metavariables", decl.ident()), span: None, }); } diff --git a/lang/elaborator/src/typechecker/exprs/call.rs b/lang/elaborator/src/typechecker/exprs/call.rs index a6b68fc098..f7a5ca2c7b 100644 --- a/lang/elaborator/src/typechecker/exprs/call.rs +++ b/lang/elaborator/src/typechecker/exprs/call.rs @@ -40,8 +40,8 @@ impl CheckInfer for Call { match kind { CallKind::Codefinition | CallKind::Constructor => { let CtorMeta { params, typ, .. } = - &ctx.type_info_table.lookup_ctor_or_codef(name)?; - let args_out = check_args(args, name, ctx, params, *span)?; + &ctx.type_info_table.lookup_ctor_or_codef(&name.clone())?; + let args_out = check_args(args, &name.clone(), ctx, params, *span)?; let typ_out = typ .subst_under_ctx(vec![params.len()].into(), &vec![args.args.clone()]) .to_exp(); @@ -55,10 +55,10 @@ impl CheckInfer for Call { }) } CallKind::LetBound => { - let LetMeta { params, typ, .. } = ctx.type_info_table.lookup_let(name)?; + let LetMeta { 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, ctx, ¶ms, *span)?; + 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())?; diff --git a/lang/elaborator/src/typechecker/exprs/dot_call.rs b/lang/elaborator/src/typechecker/exprs/dot_call.rs index 291a3ee058..5fa7b4b52a 100644 --- a/lang/elaborator/src/typechecker/exprs/dot_call.rs +++ b/lang/elaborator/src/typechecker/exprs/dot_call.rs @@ -37,9 +37,9 @@ impl CheckInfer for DotCall { fn infer(&self, ctx: &mut Ctx) -> Result { let DotCall { span, kind, exp, name, args, .. } = self; let DtorMeta { params, self_param, ret_typ, .. } = - &ctx.type_info_table.lookup_dtor_or_def(name)?; + &ctx.type_info_table.lookup_dtor_or_def(&name.clone())?; - let args_out = check_args(args, name, ctx, params, *span)?; + let args_out = check_args(args, &name.clone(), ctx, params, *span)?; let self_param_out = self_param .typ diff --git a/lang/elaborator/src/typechecker/exprs/local_comatch.rs b/lang/elaborator/src/typechecker/exprs/local_comatch.rs index 08f088c075..0b231657c6 100644 --- a/lang/elaborator/src/typechecker/exprs/local_comatch.rs +++ b/lang/elaborator/src/typechecker/exprs/local_comatch.rs @@ -57,7 +57,7 @@ pub struct WithExpectedType<'a> { pub cases: &'a Vec, /// Name of the global codefinition that gets substituted for the destructor's self parameters /// This is `None` for a local comatch. - pub label: Option<(Ident, usize)>, + pub label: Option<(IdBind, usize)>, /// The expected type of the comatch, i.e. `Stream(Int)` for `comatch { hd => 1, tl => ... }`. pub expected_type: TypCtor, } @@ -74,14 +74,14 @@ impl<'a> WithExpectedType<'a> { // Check exhaustiveness let dtors_expected: HashSet<_> = codata.dtors.iter().map(|dtor| dtor.name.to_owned()).collect(); - let mut dtors_actual = HashSet::default(); - let mut dtors_duplicate = HashSet::default(); + let mut dtors_actual = HashSet::::default(); + let mut dtors_duplicate = HashSet::::default(); for name in cases.iter().map(|case| &case.pattern.name) { - if dtors_actual.contains(name) { - dtors_duplicate.insert(name.clone()); + if dtors_actual.contains(&name.clone().into()) { + dtors_duplicate.insert(name.clone().into()); } - dtors_actual.insert(name.clone()); + dtors_actual.insert(name.clone().into()); } let mut dtors_missing = dtors_expected.difference(&dtors_actual).peekable(); @@ -227,7 +227,7 @@ impl<'a> WithExpectedType<'a> { // - The arguments to the toplevel codefinition // - The arguments bound by the destructor copattern. idx: Idx { fst: 2, snd }, - name: Ident::from_string(""), + name: VarBound::from_string(""), inferred_type: None, }))) }) @@ -235,7 +235,7 @@ impl<'a> WithExpectedType<'a> { let ctor = Box::new(Exp::Call(Call { span: None, kind: CallKind::Codefinition, - name: label.clone(), + name: label.clone().into(), args: Args { args }, inferred_type: None, })); diff --git a/lang/elaborator/src/typechecker/exprs/local_match.rs b/lang/elaborator/src/typechecker/exprs/local_match.rs index a7d8f1e395..26a0cb22a1 100644 --- a/lang/elaborator/src/typechecker/exprs/local_match.rs +++ b/lang/elaborator/src/typechecker/exprs/local_match.rs @@ -1,5 +1,7 @@ //! Bidirectional type checker +use std::collections::HashSet; + use ast::ctx::values::Binder; use ast::ctx::{BindContext, LevelCtx}; use ast::*; @@ -119,14 +121,14 @@ impl<'a> WithScrutinee<'a> { // Check exhaustiveness let ctors_expected: HashSet<_> = data.ctors.iter().map(|ctor| ctor.name.to_owned()).collect(); - let mut ctors_actual = HashSet::default(); - let mut ctors_duplicate = HashSet::default(); + let mut ctors_actual: HashSet = HashSet::default(); + let mut ctors_duplicate: HashSet = HashSet::default(); for name in cases.iter().map(|case| &case.pattern.name) { - if ctors_actual.contains(name) { - ctors_duplicate.insert(name.clone()); + if ctors_actual.contains(&name.clone().into()) { + ctors_duplicate.insert(name.clone().into()); } - ctors_actual.insert(name.clone()); + ctors_actual.insert(name.clone().into()); } let mut ctors_missing = ctors_expected.difference(&ctors_actual).peekable(); let mut ctors_undeclared = ctors_actual.difference(&ctors_expected).peekable(); @@ -186,7 +188,7 @@ impl<'a> WithScrutinee<'a> { Arg::UnnamedArg(Box::new(Exp::Variable(Variable { span: None, idx: Idx { fst: 1, snd }, - name: Ident::from_string(""), + name: VarBound::from_string(""), inferred_type: None, }))) }) diff --git a/lang/elaborator/src/typechecker/exprs/mod.rs b/lang/elaborator/src/typechecker/exprs/mod.rs index 8fb6f0d515..d71f2e6f35 100644 --- a/lang/elaborator/src/typechecker/exprs/mod.rs +++ b/lang/elaborator/src/typechecker/exprs/mod.rs @@ -120,7 +120,7 @@ impl CheckInfer for Arg { fn check_args( this: &Args, - name: &Ident, + name: &IdBound, ctx: &mut Ctx, params: &Telescope, span: Option, @@ -263,7 +263,7 @@ impl InferTelescope for SelfParam { let typ_out = typ.infer(ctx)?; let param_out = SelfParam { info: *info, name: name.clone(), typ: typ_out }; let elem = - Binder { name: name.clone().unwrap_or_else(|| Ident::from_string("")), typ: typ_nf }; + Binder { name: name.clone().unwrap_or_else(|| VarBind::from_string("")), typ: typ_nf }; // We need to shift the self parameter type here because we treat it as a 1-element telescope ctx.bind_single(&shift_and_clone(&elem, (1, 0)), |ctx| f(ctx, param_out)) diff --git a/lang/elaborator/src/typechecker/type_info_table/build.rs b/lang/elaborator/src/typechecker/type_info_table/build.rs index daa8858cd5..48ace23bd7 100644 --- a/lang/elaborator/src/typechecker/type_info_table/build.rs +++ b/lang/elaborator/src/typechecker/type_info_table/build.rs @@ -30,9 +30,9 @@ impl BuildTypeInfoTable for Decl { impl BuildTypeInfoTable for Data { fn build(&self, info_table: &mut ModuleTypeInfoTable) { - info_table.map_data.insert(self.name.clone(), self.clone()); + info_table.map_data.insert(self.name.id.clone(), self.clone()); let Data { name, typ, ctors, .. } = self; - info_table.map_tyctor.insert(name.clone(), TyCtorMeta { params: typ.clone() }); + info_table.map_tyctor.insert(name.id.clone(), TyCtorMeta { params: typ.clone() }); for ctor in ctors { ctor.build(info_table); } @@ -44,15 +44,15 @@ impl BuildTypeInfoTable for Ctor { let Ctor { name, params, typ, .. } = self; info_table .map_ctor - .insert(name.clone(), CtorMeta { params: params.clone(), typ: typ.clone() }); + .insert(name.id.clone(), CtorMeta { params: params.clone(), typ: typ.clone() }); } } impl BuildTypeInfoTable for Codata { fn build(&self, info_table: &mut ModuleTypeInfoTable) { - info_table.map_codata.insert(self.name.clone(), self.clone()); + info_table.map_codata.insert(self.name.id.clone(), self.clone()); let Codata { name, typ, dtors, .. } = self; - info_table.map_tyctor.insert(name.clone(), TyCtorMeta { params: typ.clone() }); + info_table.map_tyctor.insert(name.id.clone(), TyCtorMeta { params: typ.clone() }); for dtor in dtors { dtor.build(info_table); } @@ -63,7 +63,7 @@ impl BuildTypeInfoTable for Dtor { fn build(&self, info_table: &mut ModuleTypeInfoTable) { let Dtor { name, params, self_param, ret_typ, .. } = self; info_table.map_dtor.insert( - name.clone(), + name.id.clone(), DtorMeta { params: params.clone(), self_param: self_param.clone(), @@ -77,7 +77,7 @@ 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.clone(), + name.id.clone(), DefMeta { params: params.clone(), self_param: self_param.clone(), @@ -92,7 +92,7 @@ impl BuildTypeInfoTable for Codef { let Codef { name, params, typ, .. } = self; info_table .map_codef - .insert(name.clone(), CodefMeta { params: params.clone(), typ: typ.clone() }); + .insert(name.id.clone(), CodefMeta { params: params.clone(), typ: typ.clone() }); } } @@ -101,6 +101,6 @@ impl BuildTypeInfoTable for Let { let Let { name, params, typ, .. } = self; info_table .map_let - .insert(name.clone(), LetMeta { params: params.clone(), typ: typ.clone() }); + .insert(name.id.clone(), LetMeta { params: params.clone(), typ: typ.clone() }); } } diff --git a/lang/elaborator/src/typechecker/type_info_table/lookup.rs b/lang/elaborator/src/typechecker/type_info_table/lookup.rs index 4344831c26..11bbfbbe5a 100644 --- a/lang/elaborator/src/typechecker/type_info_table/lookup.rs +++ b/lang/elaborator/src/typechecker/type_info_table/lookup.rs @@ -5,9 +5,9 @@ use super::{ }; impl TypeInfoTable { - pub fn lookup_data(&self, name: &Ident) -> Result<&Data, TypeError> { + pub fn lookup_data(&self, name: &IdBound) -> Result<&Data, TypeError> { for map in self.map.values() { - if let Some(data) = map.map_data.get(name) { + if let Some(data) = map.map_data.get(&name.id) { return Ok(data); } } @@ -17,9 +17,9 @@ impl TypeInfoTable { }) } - pub fn lookup_codata(&self, name: &Ident) -> Result<&Codata, TypeError> { + pub fn lookup_codata(&self, name: &IdBound) -> Result<&Codata, TypeError> { for map in self.map.values() { - if let Some(codata) = map.map_codata.get(name) { + if let Some(codata) = map.map_codata.get(&name.id) { return Ok(codata); } } @@ -29,12 +29,12 @@ impl TypeInfoTable { }) } - pub fn lookup_ctor_or_codef(&self, name: &Ident) -> Result { + pub fn lookup_ctor_or_codef(&self, name: &IdBound) -> Result { for map in self.map.values() { - if let Some(meta) = map.map_ctor.get(name) { + if let Some(meta) = map.map_ctor.get(&name.id) { return Ok(meta.clone()); } - if let Some(meta) = map.map_codef.get(name) { + if let Some(meta) = map.map_codef.get(&name.id) { return Ok(meta.to_ctor().clone()); } } @@ -44,12 +44,12 @@ impl TypeInfoTable { }) } - pub fn lookup_dtor_or_def(&self, name: &Ident) -> Result { + pub fn lookup_dtor_or_def(&self, name: &IdBound) -> Result { for map in self.map.values() { - if let Some(meta) = map.map_dtor.get(name) { + if let Some(meta) = map.map_dtor.get(&name.id) { return Ok(meta.clone()); } - if let Some(meta) = map.map_def.get(name) { + if let Some(meta) = map.map_def.get(&name.id) { return Ok(meta.to_dtor().clone()); } } @@ -59,9 +59,9 @@ impl TypeInfoTable { }) } - pub fn lookup_let(&self, name: &Ident) -> Result<&LetMeta, TypeError> { + pub fn lookup_let(&self, name: &IdBound) -> Result<&LetMeta, TypeError> { for map in self.map.values() { - if let Some(meta) = map.map_let.get(name) { + if let Some(meta) = map.map_let.get(&name.id) { return Ok(meta); } } @@ -71,9 +71,9 @@ impl TypeInfoTable { }) } - pub fn lookup_tyctor(&self, name: &Ident) -> Result<&TyCtorMeta, TypeError> { + pub fn lookup_tyctor(&self, name: &IdBound) -> Result<&TyCtorMeta, TypeError> { for map in self.map.values() { - if let Some(meta) = map.map_tyctor.get(name) { + if let Some(meta) = map.map_tyctor.get(&name.id) { return Ok(meta); } } @@ -83,9 +83,9 @@ impl TypeInfoTable { }) } - pub fn lookup_codef(&self, name: &Ident) -> Result<&CodefMeta, TypeError> { + pub fn lookup_codef(&self, name: &IdBound) -> Result<&CodefMeta, TypeError> { for map in self.map.values() { - if let Some(meta) = map.map_codef.get(name) { + if let Some(meta) = map.map_codef.get(&name.id) { return Ok(meta); } } @@ -95,9 +95,9 @@ impl TypeInfoTable { }) } - pub fn lookup_ctor(&self, name: &Ident) -> Result<&CtorMeta, TypeError> { + pub fn lookup_ctor(&self, name: &IdBound) -> Result<&CtorMeta, TypeError> { for map in self.map.values() { - if let Some(meta) = map.map_ctor.get(name) { + if let Some(meta) = map.map_ctor.get(&name.id) { return Ok(meta); } } @@ -107,9 +107,9 @@ impl TypeInfoTable { }) } - pub fn lookup_def(&self, name: &Ident) -> Result<&DefMeta, TypeError> { + pub fn lookup_def(&self, name: &IdBound) -> Result<&DefMeta, TypeError> { for map in self.map.values() { - if let Some(meta) = map.map_def.get(name) { + if let Some(meta) = map.map_def.get(&name.id) { return Ok(meta); } } @@ -119,9 +119,9 @@ impl TypeInfoTable { }) } - pub fn lookup_dtor(&self, name: &Ident) -> Result<&DtorMeta, TypeError> { + pub fn lookup_dtor(&self, name: &IdBound) -> Result<&DtorMeta, TypeError> { for map in self.map.values() { - if let Some(meta) = map.map_dtor.get(name) { + if let Some(meta) = map.map_dtor.get(&name.id) { return Ok(meta); } } diff --git a/lang/elaborator/src/typechecker/type_info_table/mod.rs b/lang/elaborator/src/typechecker/type_info_table/mod.rs index f0c7e155a4..6530138501 100644 --- a/lang/elaborator/src/typechecker/type_info_table/mod.rs +++ b/lang/elaborator/src/typechecker/type_info_table/mod.rs @@ -22,20 +22,20 @@ pub struct ModuleTypeInfoTable { // Data and Codata Types // // - map_data: HashMap, - map_codata: HashMap, + map_data: HashMap, + map_codata: HashMap, // Calls // // - map_let: HashMap, - map_tyctor: HashMap, - map_codef: HashMap, - map_ctor: HashMap, + map_let: HashMap, + map_tyctor: HashMap, + map_codef: HashMap, + map_ctor: HashMap, // DotCalls // // - map_def: HashMap, - map_dtor: HashMap, + map_def: HashMap, + map_dtor: HashMap, } #[derive(Debug, Clone)] diff --git a/lang/lowering/src/ctx.rs b/lang/lowering/src/ctx.rs index e0c20423c7..b89530bca4 100644 --- a/lang/lowering/src/ctx.rs +++ b/lang/lowering/src/ctx.rs @@ -87,7 +87,7 @@ impl Ctx { self.next_label_id += 1; Ok(ast::Label { id, - user_name: user_name.map(|name| ast::Ident { span: Some(name.span), id: name.id }), + user_name: user_name.map(|name| ast::IdBind { span: Some(name.span), id: name.id }), }) } @@ -135,7 +135,7 @@ impl Ctx { ast::Variable { span: None, idx: self.level_to_index(Lvl { fst, snd }), - name: ast::Ident { span: None, id: name.to_owned() }, + name: ast::VarBound { span: None, id: name.to_owned() }, inferred_type: None, } .into(), diff --git a/lang/lowering/src/lower/decls/codata_declaration.rs b/lang/lowering/src/lower/decls/codata_declaration.rs index fb3b5b9a73..8e526b48b0 100644 --- a/lang/lowering/src/lower/decls/codata_declaration.rs +++ b/lang/lowering/src/lower/decls/codata_declaration.rs @@ -1,3 +1,4 @@ +use ast::IdBind; use miette_util::ToMiette; use parser::cst::ident::Ident; use parser::cst::{self}; @@ -21,7 +22,7 @@ impl Lower for cst::decls::Codata { Ok(ast::Codata { span: Some(*span), doc: doc.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBind { span: Some(name.span), id: name.id.clone() }, attr: attr.lower(ctx)?, typ: Box::new(lower_telescope(params, ctx, |_, out| Ok(out))?), dtors, @@ -69,7 +70,7 @@ fn lower_destructor( Ok(ast::Dtor { span: Some(*span), doc: doc.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBind { span: Some(name.span), id: name.id.clone() }, params, self_param, ret_typ: ret_typ.lower(ctx)?, diff --git a/lang/lowering/src/lower/decls/codefinition.rs b/lang/lowering/src/lower/decls/codefinition.rs index b0298b3b28..d0d44ac227 100644 --- a/lang/lowering/src/lower/decls/codefinition.rs +++ b/lang/lowering/src/lower/decls/codefinition.rs @@ -1,3 +1,4 @@ +use ast::IdBind; use miette_util::ToMiette; use parser::cst::{self}; @@ -20,7 +21,7 @@ impl Lower for cst::decls::Codef { Ok(ast::Codef { span: Some(*span), doc: doc.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBind { span: Some(name.span), id: name.id.clone() }, attr: attr.lower(ctx)?, params, typ: typ_ctor, diff --git a/lang/lowering/src/lower/decls/data_declaration.rs b/lang/lowering/src/lower/decls/data_declaration.rs index 39e1239ae5..f922ace57c 100644 --- a/lang/lowering/src/lower/decls/data_declaration.rs +++ b/lang/lowering/src/lower/decls/data_declaration.rs @@ -1,3 +1,4 @@ +use ast::{IdBind, IdBound}; use miette_util::ToMiette; use parser::cst::ident::Ident; use parser::cst::{self}; @@ -20,7 +21,7 @@ impl Lower for cst::decls::Data { Ok(ast::Data { span: Some(*span), doc: doc.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBind { span: Some(name.span), id: name.id.clone() }, attr: attr.lower(ctx)?, typ: Box::new(lower_telescope(params, ctx, |_, out| Ok(out))?), ctors, @@ -48,7 +49,7 @@ fn lower_constructor( if type_arity == 0 { ast::TypCtor { span: None, - name: typ_name.lower(ctx)?, + name: IdBound { span: Some(typ_name.span), id: typ_name.id.clone() }, args: ast::Args { args: vec![] }, } } else { @@ -64,7 +65,7 @@ fn lower_constructor( Ok(ast::Ctor { span: Some(*span), doc: doc.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBind { span: Some(name.span), id: name.id.clone() }, params, typ, }) diff --git a/lang/lowering/src/lower/decls/definition.rs b/lang/lowering/src/lower/decls/definition.rs index 20eecf65bd..7923181715 100644 --- a/lang/lowering/src/lower/decls/definition.rs +++ b/lang/lowering/src/lower/decls/definition.rs @@ -1,3 +1,4 @@ +use ast::IdBind; use parser::cst::{self}; use super::super::*; @@ -20,7 +21,7 @@ impl Lower for cst::decls::Def { Ok(ast::Def { span: Some(*span), doc: doc.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBind { span: Some(name.span), id: name.id.clone() }, attr: attr.lower(ctx)?, params, self_param, diff --git a/lang/lowering/src/lower/decls/mod.rs b/lang/lowering/src/lower/decls/mod.rs index ee6ed7b77e..2a94f947ad 100644 --- a/lang/lowering/src/lower/decls/mod.rs +++ b/lang/lowering/src/lower/decls/mod.rs @@ -1,3 +1,4 @@ +use ast::VarBind; use miette_util::ToMiette; use parser::cst::exp::BindingSite; use parser::cst::{self}; @@ -97,7 +98,7 @@ fn lower_self_param Result Result { - let Ident { span, id } = self; - Ok(ast::Ident { span: Some(*span), id: id.clone() }) - } -} - impl Lower for cst::exp::Exp { type Target = ast::Exp; @@ -60,7 +54,7 @@ fn lower_telescope_inst Result { let cst::exp::Case { span, pattern, body } = self; lower_telescope_inst(&pattern.params, ctx, |ctx, params| { - let name = pattern.name.lower(ctx)?; + let name = IdBound { span: Some(pattern.name.span), id: pattern.name.id.clone() }; Ok(ast::Case { span: Some(*span), pattern: ast::Pattern { is_copattern: false, name, params }, @@ -259,7 +253,7 @@ impl Lower for cst::exp::Case { let cst::exp::Case { span, pattern, body } = self; lower_telescope_inst(&pattern.params, ctx, |ctx, params| { - let name = pattern.name.lower(ctx)?; + let name = ast::IdBound { span: Some(pattern.name.span), id: pattern.name.id.clone() }; Ok(ast::Case { span: Some(*span), pattern: ast::Pattern { is_copattern: true, name, params }, @@ -278,7 +272,7 @@ impl Lower for cst::exp::Call { // If we find the identifier in the local context then we have to lower // it to a variable. if let Some(idx) = ctx.lookup_local(name) { - let name = name.lower(ctx)?; + let name = VarBound { span: Some(name.span), id: name.id.clone() }; return Ok(ast::Exp::Variable(Variable { span: Some(*span), idx, @@ -292,7 +286,7 @@ impl Lower for cst::exp::Call { let meta = ctx.symbol_table.lookup(name).cloned()?; match meta { DeclMeta::Data { params, .. } | DeclMeta::Codata { params, .. } => { - let name = name.lower(ctx)?; + let name = IdBound { span: Some(name.span), id: name.id.clone() }; Ok(ast::Exp::TypCtor(ast::TypCtor { span: Some(*span), name, @@ -303,7 +297,7 @@ impl Lower for cst::exp::Call { Err(LoweringError::MustUseAsDotCall { name: name.clone(), span: span.to_miette() }) } DeclMeta::Ctor { params, .. } => { - let name = name.lower(ctx)?; + let name = IdBound { span: Some(name.span), id: name.id.clone() }; Ok(ast::Exp::Call(ast::Call { span: Some(*span), kind: ast::CallKind::Constructor, @@ -313,7 +307,7 @@ impl Lower for cst::exp::Call { })) } DeclMeta::Codef { params, .. } => { - let name = name.lower(ctx)?; + let name = IdBound { span: Some(name.span), id: name.id.clone() }; Ok(ast::Exp::Call(ast::Call { span: Some(*span), kind: ast::CallKind::Codefinition, @@ -323,7 +317,7 @@ impl Lower for cst::exp::Call { })) } DeclMeta::Let { params, .. } => { - let name = name.lower(ctx)?; + let name = IdBound { span: Some(name.span), id: name.id.clone() }; Ok(ast::Exp::Call(ast::Call { span: Some(*span), kind: ast::CallKind::LetBound, @@ -349,7 +343,7 @@ impl Lower for cst::exp::DotCall { span: Some(*span), kind: ast::DotCallKind::Destructor, exp: exp.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBound { span: Some(name.span), id: name.id.clone() }, args: lower_args(args, params, ctx)?, inferred_type: None, })), @@ -357,7 +351,7 @@ impl Lower for cst::exp::DotCall { span: Some(*span), kind: ast::DotCallKind::Definition, exp: exp.lower(ctx)?, - name: name.lower(ctx)?, + name: IdBound { span: Some(name.span), id: name.id.clone() }, args: lower_args(args, params, ctx)?, inferred_type: None, })), @@ -482,7 +476,7 @@ impl Lower for cst::exp::NatLit { let mut out = ast::Exp::Call(ast::Call { span: Some(*span), kind: call_kind, - name: ast::Ident::from_string("Z"), + name: ast::IdBound::from_string("Z"), args: ast::Args { args: vec![] }, inferred_type: None, }); @@ -494,7 +488,7 @@ impl Lower for cst::exp::NatLit { out = ast::Exp::Call(ast::Call { span: Some(*span), kind: call_kind, - name: ast::Ident::from_string("S"), + name: ast::IdBound::from_string("S"), args: ast::Args { args: vec![ast::Arg::UnnamedArg(Box::new(out))] }, inferred_type: None, }); @@ -510,7 +504,7 @@ impl Lower for cst::exp::Fun { let cst::exp::Fun { span, from, to } = self; Ok(ast::TypCtor { span: Some(*span), - name: ast::Ident::from_string("Fun"), + name: ast::IdBound::from_string("Fun"), args: ast::Args { args: vec![ ast::Arg::UnnamedArg(from.lower(ctx)?), @@ -575,7 +569,7 @@ impl Lower for cst::exp::Motive { param: ast::ParamInst { span: Some(bs_to_span(param)), info: None, - name: ast::Ident { span: Some(bs_to_span(param)), id: bs_to_name(param).id }, + name: ast::VarBind { span: Some(bs_to_span(param)), id: bs_to_name(param).id }, typ: None, }, ret_typ: ctx.bind_single(param, |ctx| ret_typ.lower(ctx))?, diff --git a/lang/transformations/src/lifting/fv.rs b/lang/transformations/src/lifting/fv.rs index 19df4b7e76..6b903758dc 100644 --- a/lang/transformations/src/lifting/fv.rs +++ b/lang/transformations/src/lifting/fv.rs @@ -77,7 +77,7 @@ impl FV for Variable { &v.type_ctx.lookup(lvl).typ, ((v.lvl_ctx.len() - v.type_ctx.len()) as isize, 0), ); - v.add_fv(name.clone(), lvl, typ, v.lvl_ctx.clone()) + v.add_fv(name.id.clone(), lvl, typ, v.lvl_ctx.clone()) } } } @@ -194,11 +194,12 @@ impl FreeVars { let typ = typ.subst(&mut ctx, &subst.in_param()); - let param = Param { implicit: false, name: name.clone(), typ: typ.clone() }; + let param = + Param { implicit: false, name: VarBind::from_string(&name), typ: typ.clone() }; let arg = Arg::UnnamedArg(Box::new(Exp::Variable(Variable { span: None, idx: base_ctx.lvl_to_idx(fv.lvl), - name: name.clone(), + name: VarBound::from_string(&name), inferred_type: None, }))); args.push(arg); @@ -264,7 +265,7 @@ impl FreeVars { pub struct FreeVar { /// Name of the free variable #[derivative(PartialEq = "ignore", Hash = "ignore")] - pub name: Ident, + pub name: String, /// The original De-Bruijn level pub lvl: Lvl, /// Type of the free variable @@ -310,7 +311,7 @@ pub struct USTVisitor<'a> { impl<'a> USTVisitor<'a> { /// Add a free variable as well as all free variables its type - fn add_fv(&mut self, name: Ident, lvl: Lvl, typ: Box, ctx: LevelCtx) { + fn add_fv(&mut self, name: String, lvl: Lvl, typ: Box, ctx: LevelCtx) { // Add the free variable let fv = FreeVar { name, lvl, typ: typ.clone(), ctx }; if self.fvs.insert(fv) { @@ -342,7 +343,7 @@ pub struct FVSubst { #[derive(Clone, Debug)] struct NewVar { /// Name of the free variable - name: Ident, + name: String, /// New De-Bruijn level lvl: Lvl, } @@ -364,7 +365,7 @@ impl FVSubst { Self { subst: Default::default(), cutoff } } - fn add(&mut self, name: Ident, lvl: Lvl) { + fn add(&mut self, name: String, lvl: Lvl) { self.subst.insert(lvl, NewVar { name, lvl: Lvl { fst: 0, snd: self.subst.len() } }); } @@ -412,7 +413,7 @@ impl<'a> Substitution for FVBodySubst<'a> { Box::new(Exp::Variable(Variable { span: None, idx: new_ctx.lvl_to_idx(fv.lvl), - name: fv.name.clone(), + name: VarBound::from_string(&fv.name), inferred_type: None, })) }) @@ -425,7 +426,7 @@ impl<'a> Substitution for FVParamSubst<'a> { Box::new(Exp::Variable(Variable { span: None, idx: Idx { fst: 0, snd: self.inner.subst.len() - 1 - fv.lvl.snd }, - name: fv.name.clone(), + name: VarBound::from_string(&fv.name), inferred_type: None, })) }) diff --git a/lang/transformations/src/lifting/mod.rs b/lang/transformations/src/lifting/mod.rs index d3a29c82a5..87b2af4397 100644 --- a/lang/transformations/src/lifting/mod.rs +++ b/lang/transformations/src/lifting/mod.rs @@ -15,13 +15,13 @@ pub fn lift(module: Arc, name: &str) -> LiftResult { let mut ctx = Ctx { name: name.to_owned(), new_decls: vec![], - curr_decl: Ident::from_string(""), + curr_decl: IdBind::from_string(""), modified_decls: HashSet::default(), ctx: LevelCtx::default(), }; let mut module = module.lift(&mut ctx); - let new_decl_names = HashSet::from_iter(ctx.new_decls.iter().map(|decl| decl.name().clone())); + let new_decl_names = HashSet::from_iter(ctx.new_decls.iter().map(|decl| decl.ident().clone())); module.decls.extend(ctx.new_decls); module.rename(); @@ -33,9 +33,9 @@ pub struct LiftResult { /// The resulting program pub module: Module, /// List of new top-level definitions - pub new_decls: HashSet, + pub new_decls: HashSet, /// List of top-level declarations that have been modified in the lifting process - pub modified_decls: HashSet, + pub modified_decls: HashSet, } #[derive(Debug)] @@ -45,9 +45,9 @@ struct Ctx { /// List of new top-level declarations that got created in the lifting process new_decls: Vec, /// Current declaration being visited for lifting - curr_decl: Ident, + curr_decl: IdBind, /// List of declarations that got modified in the lifting process - modified_decls: HashSet, + modified_decls: HashSet, /// Tracks the current binders in scope ctx: LevelCtx, } @@ -93,7 +93,7 @@ impl Lift for Decl { type Target = Decl; fn lift(&self, ctx: &mut Ctx) -> Self::Target { - ctx.set_curr_decl(self.name().clone()); + ctx.set_curr_decl(self.ident().clone()); match self { Decl::Data(data) => Decl::Data(data.lift(ctx)), Decl::Codata(cotata) => Decl::Codata(cotata.lift(ctx)), @@ -604,7 +604,7 @@ impl Ctx { span: None, kind: DotCallKind::Definition, exp: Box::new(on_exp.lift(self)), - name, + name: name.clone().into(), args, inferred_type: None, }) @@ -665,14 +665,14 @@ impl Ctx { Exp::Call(Call { span: None, kind: CallKind::Codefinition, - name, + name: name.clone().into(), args, inferred_type: None, }) } /// Set the current declaration - fn set_curr_decl(&mut self, name: Ident) { + fn set_curr_decl(&mut self, name: IdBind) { self.curr_decl = name; } @@ -682,19 +682,19 @@ impl Ctx { } /// Generate a definition name based on the label and type information - fn unique_def_name(&self, label: &Label, type_name: &str) -> Ident { + fn unique_def_name(&self, label: &Label, type_name: &str) -> IdBind { label.user_name.clone().unwrap_or_else(|| { let lowered = type_name.to_lowercase(); let id = label.id; - Ident::from_string(&format!("d_{lowered}{id}")) + IdBind::from_string(&format!("d_{lowered}{id}")) }) } /// Generate a codefinition name based on the label and type information - fn unique_codef_name(&self, label: &Label, type_name: &str) -> Ident { + fn unique_codef_name(&self, label: &Label, type_name: &str) -> IdBind { label.user_name.clone().unwrap_or_else(|| { let id = label.id; - Ident::from_string(&format!("Mk{type_name}{id}")) + IdBind::from_string(&format!("Mk{type_name}{id}")) }) } } diff --git a/lang/transformations/src/renaming/ast.rs b/lang/transformations/src/renaming/ast.rs index 7281dc9e08..b3a50d5132 100644 --- a/lang/transformations/src/renaming/ast.rs +++ b/lang/transformations/src/renaming/ast.rs @@ -225,7 +225,7 @@ impl Rename for DotCall { } impl Rename for Variable { fn rename_in_ctx(&mut self, ctx: &mut Ctx) { - self.name = ctx.lookup(self.idx); + self.name = ctx.lookup(self.idx).into(); self.inferred_type.rename_in_ctx(ctx); } } diff --git a/lang/transformations/src/renaming/ctx.rs b/lang/transformations/src/renaming/ctx.rs index 3f79e5429c..dea4ba0a5a 100644 --- a/lang/transformations/src/renaming/ctx.rs +++ b/lang/transformations/src/renaming/ctx.rs @@ -4,17 +4,17 @@ use ast::*; use super::util::increment_name; pub struct Ctx { - ctx: GenericCtx, + ctx: GenericCtx, } -impl From> for Ctx { - fn from(value: GenericCtx) -> Self { +impl From> for Ctx { + fn from(value: GenericCtx) -> Self { Ctx { ctx: value } } } impl Context for Ctx { - type Elem = Ident; + type Elem = VarBind; fn push_telescope(&mut self) { self.ctx.bound.push(vec![]); @@ -50,7 +50,7 @@ impl Context for Ctx { } impl Ctx { - pub(super) fn disambiguate_name(&self, mut name: Ident) -> Ident { + pub(super) fn disambiguate_name(&self, mut name: VarBind) -> VarBind { if name.id == "_" || name.id.is_empty() { "x".clone_into(&mut name.id); } @@ -60,7 +60,7 @@ impl Ctx { name } - fn contains_name(&self, name: &Ident) -> bool { + fn contains_name(&self, name: &VarBind) -> bool { for telescope in &self.ctx.bound { if telescope.contains(name) { return true; @@ -84,6 +84,6 @@ impl ContextElem for ParamInst { impl ContextElem for SelfParam { fn as_element(&self) -> ::Elem { - self.name.to_owned().unwrap_or_else(|| Ident::from_string("")) + self.name.to_owned().unwrap_or_else(|| VarBind::from_string("")) } } diff --git a/lang/transformations/src/renaming/util.rs b/lang/transformations/src/renaming/util.rs index de36f078f2..a6ec6609f3 100644 --- a/lang/transformations/src/renaming/util.rs +++ b/lang/transformations/src/renaming/util.rs @@ -1,14 +1,14 @@ -use ast::Ident; +use ast::VarBind; -pub fn increment_name(mut name: Ident) -> Ident { +pub fn increment_name(mut name: VarBind) -> VarBind { if name.id.ends_with('\'') { name.id.push('\''); return name; } let (s, digits) = split_trailing_digits(&name.id); match digits { - None => Ident::from_string(&format!("{s}0")), - Some(n) => Ident::from_string(&format!("{s}{}", n + 1)), + None => VarBind::from_string(&format!("{s}0")), + Some(n) => VarBind::from_string(&format!("{s}{}", n + 1)), } } diff --git a/lang/transformations/src/xfunc/matrix.rs b/lang/transformations/src/xfunc/matrix.rs index 0a82b9d5f6..22fc3a67cd 100644 --- a/lang/transformations/src/xfunc/matrix.rs +++ b/lang/transformations/src/xfunc/matrix.rs @@ -7,7 +7,7 @@ use codespan::Span; #[derive(Debug, Clone)] pub struct Prg { - pub map: HashMap, + pub map: HashMap, } #[derive(Debug, Clone)] @@ -15,10 +15,10 @@ pub struct XData { pub repr: Repr, pub span: Option, pub doc: Option, - pub name: ast::Ident, + pub name: ast::IdBind, pub typ: Box, - pub ctors: HashMap, - pub dtors: HashMap, + pub ctors: HashMap, + pub dtors: HashMap, pub exprs: HashMap>>, } @@ -32,8 +32,8 @@ pub struct XData { /// between the matrix and other representations #[derive(Debug, Clone, PartialEq, Eq, Hash)] pub struct Key { - pub ctor: ast::Ident, - pub dtor: ast::Ident, + pub ctor: String, + pub dtor: String, } #[derive(Debug, Clone, Copy)] @@ -92,10 +92,10 @@ impl BuildMatrix for ast::Data { exprs: HashMap::default(), }; for ctor in ctors { - xdata.ctors.insert(ctor.name.clone(), ctor.clone()); + xdata.ctors.insert(ctor.name.id.clone(), ctor.clone()); } - out.map.insert(name.clone(), xdata); + out.map.insert(name.id.clone(), xdata); Ok(()) } } @@ -115,10 +115,10 @@ impl BuildMatrix for ast::Codata { }; for dtor in dtors { - xdata.dtors.insert(dtor.name.clone(), dtor.clone()); + xdata.dtors.insert(dtor.name.id.clone(), dtor.clone()); } - out.map.insert(name.clone(), xdata); + out.map.insert(name.id.clone(), xdata); Ok(()) } } @@ -126,17 +126,17 @@ impl BuildMatrix for ast::Codata { impl BuildMatrix for ast::Def { fn build_matrix(&self, out: &mut Prg) -> Result<(), XfuncError> { let type_name = &self.self_param.typ.name; - let xdata = out.map.get_mut(type_name).ok_or(XfuncError::Impossible { + let xdata = out.map.get_mut(&type_name.id).ok_or(XfuncError::Impossible { message: format!("Could not resolve {type_name}"), span: None, })?; - xdata.dtors.insert(self.name.clone(), self.to_dtor()); + xdata.dtors.insert(self.name.id.clone(), self.to_dtor()); let cases = &self.cases; for case in cases { let ast::Case { pattern, body, .. } = case; - let key = Key { dtor: self.name.clone(), ctor: pattern.name.clone() }; + let key = Key { dtor: self.name.id.clone(), ctor: pattern.name.id.clone() }; xdata.exprs.insert(key, body.clone()); } Ok(()) @@ -146,17 +146,17 @@ impl BuildMatrix for ast::Def { impl BuildMatrix for ast::Codef { fn build_matrix(&self, out: &mut Prg) -> Result<(), XfuncError> { let type_name = &self.typ.name; - let xdata = out.map.get_mut(type_name).ok_or(XfuncError::Impossible { + let xdata = out.map.get_mut(&type_name.id).ok_or(XfuncError::Impossible { message: format!("Could not resolve {type_name}"), span: None, })?; - xdata.ctors.insert(self.name.clone(), self.to_ctor()); + xdata.ctors.insert(self.name.id.clone(), self.to_ctor()); let cases = &self.cases; for case in cases { let ast::Case { pattern, body, .. } = case; - let key = Key { ctor: self.name.clone(), dtor: pattern.name.clone() }; + let key = Key { ctor: self.name.id.clone(), dtor: pattern.name.id.clone() }; // Swap binding order to the order imposed by the matrix representation let body = body.as_ref().map(|body| { let mut ctx = LevelCtx::empty(); @@ -192,13 +192,13 @@ impl XData { let cases = ctors .values() .flat_map(|ctor| { - let key = Key { dtor: dtor.name.clone(), ctor: ctor.name.clone() }; + let key = Key { dtor: dtor.name.id.clone(), ctor: ctor.name.id.clone() }; let body = exprs.get(&key).cloned(); body.map(|body| ast::Case { span: None, pattern: ast::Pattern { is_copattern: false, - name: ctor.name.clone(), + name: ctor.name.clone().into(), params: ctor.params.instantiate(), }, body, @@ -240,7 +240,7 @@ impl XData { let cases = dtors .values() .flat_map(|dtor| { - let key = Key { dtor: dtor.name.clone(), ctor: ctor.name.clone() }; + let key = Key { dtor: dtor.name.id.clone(), ctor: ctor.name.id.clone() }; let body = &exprs.get(&key); // Swap binding order (which is different in the matrix representation) let body = body.as_ref().map(|body| { @@ -255,7 +255,7 @@ impl XData { span: None, pattern: ast::Pattern { is_copattern: true, - name: dtor.name.clone(), + name: dtor.name.clone().into(), params: dtor.params.instantiate(), }, body, diff --git a/lang/transformations/src/xfunc/mod.rs b/lang/transformations/src/xfunc/mod.rs index aff8fb2e50..ea35d73e5e 100644 --- a/lang/transformations/src/xfunc/mod.rs +++ b/lang/transformations/src/xfunc/mod.rs @@ -1,4 +1,4 @@ -use ast::Ident; +use ast::IdBound; pub mod matrix; pub mod result; @@ -7,9 +7,9 @@ pub fn as_matrix(prg: &ast::Module) -> Result Result { +pub fn repr(prg: &matrix::Prg, name: &IdBound) -> Result { prg.map - .get(name) + .get(&name.id) .ok_or_else(|| crate::result::XfuncError::Impossible { message: format!("Could not resolve {name}"), span: None, @@ -19,10 +19,10 @@ pub fn repr(prg: &matrix::Prg, name: &Ident) -> Result Result<(ast::Data, Vec), crate::result::XfuncError> { prg.map - .get(name) + .get(&name.id) .ok_or_else(|| crate::result::XfuncError::Impossible { message: format!("Could not resolve {name}"), span: None, @@ -32,10 +32,10 @@ pub fn as_data( pub fn as_codata( prg: &matrix::Prg, - name: &Ident, + name: &IdBound, ) -> Result<(ast::Codata, Vec), crate::result::XfuncError> { prg.map - .get(name) + .get(&name.id) .ok_or_else(|| crate::result::XfuncError::Impossible { message: format!("Could not resolve {name}"), span: None,