From bdf24a054dada01b6bd802ff0ed04da4032fcbb9 Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 13:55:43 +0200 Subject: [PATCH 1/6] Refactor parser and bump lalrpop to 0.20 --- Cargo.lock | 112 +++++++++++++++++++++++++--- lang/parser/Cargo.toml | 4 +- lang/parser/src/grammar/cst.lalrpop | 110 ++++++++++++++++++++++----- lang/parser/src/result.rs | 4 +- 4 files changed, 196 insertions(+), 34 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0270990e31..2e7b011a8c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -37,6 +37,15 @@ dependencies = [ "memchr", ] +[[package]] +name = "aho-corasick" +version = "1.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916" +dependencies = [ + "memchr", +] + [[package]] name = "anstream" version = "0.2.6" @@ -1000,6 +1009,15 @@ dependencies = [ "either", ] +[[package]] +name = "itertools" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b1c173a5686ce8bfa551b3563d0c2170bf24ca44da99c7ca4bfdab5418c3fe57" +dependencies = [ + "either", +] + [[package]] name = "itoa" version = "1.0.6" @@ -1045,10 +1063,10 @@ dependencies = [ "diff", "ena", "is-terminal", - "itertools", - "lalrpop-util", + "itertools 0.10.5", + "lalrpop-util 0.19.9", "petgraph", - "pico-args", + "pico-args 0.4.2", "regex", "regex-syntax 0.6.29", "string_cache", @@ -1057,6 +1075,28 @@ dependencies = [ "unicode-xid", ] +[[package]] +name = "lalrpop" +version = "0.20.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "55cb077ad656299f160924eb2912aa147d7339ea7d69e1b5517326fdcec3c1ca" +dependencies = [ + "ascii-canvas", + "bit-set", + "ena", + "itertools 0.11.0", + "lalrpop-util 0.20.2", + "petgraph", + "pico-args 0.5.0", + "regex", + "regex-syntax 0.8.3", + "string_cache", + "term", + "tiny-keccak", + "unicode-xid", + "walkdir", +] + [[package]] name = "lalrpop-util" version = "0.19.9" @@ -1066,6 +1106,15 @@ dependencies = [ "regex", ] +[[package]] +name = "lalrpop-util" +version = "0.20.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "507460a910eb7b32ee961886ff48539633b788a36b65692b95f225b844c82553" +dependencies = [ + "regex-automata 0.4.6", +] + [[package]] name = "lazy_static" version = "1.4.0" @@ -1210,7 +1259,7 @@ version = "0.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8263075bb86c5a1b1427b5ae862e8889656f126e9f77c484496e8b47cf5c5558" dependencies = [ - "regex-automata", + "regex-automata 0.1.10", ] [[package]] @@ -1225,9 +1274,9 @@ dependencies = [ [[package]] name = "memchr" -version = "2.5.0" +version = "2.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" +checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d" [[package]] name = "memmap2" @@ -1455,8 +1504,9 @@ name = "parser" version = "0.1.0" dependencies = [ "codespan", - "lalrpop", - "lalrpop-util", + "lalrpop 0.19.9", + "lalrpop 0.20.2", + "lalrpop-util 0.20.2", "miette", "num-bigint", "thiserror", @@ -1493,6 +1543,12 @@ version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "db8bcd96cb740d03149cbad5518db9fd87126a10ab519c011893b1754134c468" +[[package]] +name = "pico-args" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315" + [[package]] name = "pin-project" version = "1.0.12" @@ -1762,7 +1818,7 @@ version = "1.7.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8b1f693b24f6ac912f4893ef08244d70b6067480d2f1a46e950c9691e6749d1d" dependencies = [ - "aho-corasick", + "aho-corasick 0.7.20", "memchr", "regex-syntax 0.6.29", ] @@ -1776,6 +1832,17 @@ dependencies = [ "regex-syntax 0.6.29", ] +[[package]] +name = "regex-automata" +version = "0.4.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "86b83b8b9847f9bf95ef68afb0b8e6cdb80f498442f5179a29fad448fcc1eaea" +dependencies = [ + "aho-corasick 1.1.3", + "memchr", + "regex-syntax 0.8.3", +] + [[package]] name = "regex-syntax" version = "0.4.2" @@ -1788,6 +1855,12 @@ version = "0.6.29" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1" +[[package]] +name = "regex-syntax" +version = "0.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "adad44e29e4c806119491a7f06f03de4d1af22c3a680dd47f1e6e179439d1f56" + [[package]] name = "renaming" version = "0.1.0" @@ -1857,6 +1930,15 @@ version = "1.0.13" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f91339c0467de62360649f8d3e185ca8de4224ff281f66000de5eb2a77a79041" +[[package]] +name = "same-file" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502" +dependencies = [ + "winapi-util", +] + [[package]] name = "scoped-tls" version = "1.0.1" @@ -2071,7 +2153,7 @@ dependencies = [ "fnv", "fs2", "htmlescape", - "itertools", + "itertools 0.10.5", "levenshtein_automata", "log", "lru", @@ -2593,6 +2675,16 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9d5b2c62b4012a3e1eca5a7e077d13b3bf498c4073e33ccd58626607748ceeca" +[[package]] +name = "walkdir" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b" +dependencies = [ + "same-file", + "winapi-util", +] + [[package]] name = "wasi" version = "0.11.0+wasi-snapshot-preview1" diff --git a/lang/parser/Cargo.toml b/lang/parser/Cargo.toml index 7be17f74ea..774089091a 100644 --- a/lang/parser/Cargo.toml +++ b/lang/parser/Cargo.toml @@ -5,8 +5,8 @@ edition = "2021" [dependencies] # parser generator -lalrpop = "0.19" -lalrpop-util = "0.19" +lalrpop = "0.20" +lalrpop-util = "0.20" # source code locations codespan = "0.11" # fancy error messages diff --git a/lang/parser/src/grammar/cst.lalrpop b/lang/parser/src/grammar/cst.lalrpop index 5557c66cb7..214d659bc1 100644 --- a/lang/parser/src/grammar/cst.lalrpop +++ b/lang/parser/src/grammar/cst.lalrpop @@ -84,29 +84,54 @@ OmitAbsurd: bool = => absurd.is_some(); DocCommentHelper: String = => doc.strip_prefix("-- |").unwrap().trim().to_owned(); DocComment: DocComment = => DocComment { docs }; -// Program +// Modules +// +// pub Prg: Prg = { => Prg { items, }, } pub Decl: Decl = { - "data" "{" > "}" => Decl::Data(Data { span: span(l, r), doc, name, attr, params, ctors }), - "codata" "{" > "}" => Decl::Codata(Codata { span: span(l, r), doc, name, attr, params, dtors }), - "def" "." ":" "{" "}" => Decl::Def(Def { span: span(l, r), doc, name, attr, params, scrutinee, ret_typ, body }), - "codef" ":" "{" "}" => Decl::Codef(Codef { span: span(l, r), doc, name, attr, params, typ, body }), - "let" ":" "{" "}" => - Decl::Let(Let { span: span(l,r), doc, name, attr, params, typ, body }), + => Decl::Data(d), + => Decl::Codata(d), + => Decl::Def(d), + => Decl::Codef(d), + => Decl::Let(d), } +// Toplevel declarations +// +// + Ctor: Ctor = { )?> => Ctor { span: span(l, r), doc, name, params, typ }, } +// Toplevel data type declaration +Data: Data = "data" "{" > "}" => + Data { span: span(l, r), doc, name, attr, params, ctors }; + Dtor: Dtor = { ":" => Dtor { span: span(l, r), doc, name, params, destructee, ret_typ }, } +// Toplevel codata type declaration +Codata: Codata = "codata" "{" > "}" => + Codata { span: span(l, r), doc, name, attr, params, dtors }; + +// Toplevel definition +Def: Def = "def" "." ":" "{" "}" => + Def { span: span(l, r), doc, name, attr, params, scrutinee, ret_typ, body }; + +// Toplevel codefinition +Codef: Codef = "codef" ":" "{" "}" => + Codef { span: span(l, r), doc, name, attr, params, typ, body }; + +// Toplevel let binding +Let: Let = "let" ":" "{" "}" => + Let { span: span(l,r), doc, name, attr, params, typ, body }; + pub Match : Match = { > => Match { span: span(l, r), cases, omit_absurd }, } @@ -136,41 +161,86 @@ pub TypApp: TypApp = { => TypApp { span: span(l, r), name, args }, } +// Expressions +// +// + pub Exp: Rc = { - ":" => Rc::new(Exp::Anno { span: span(l, r), exp, typ }), - "->" => Rc::new(Exp::Fun { span: span(l, r), from, to }), - "\\" "." => Rc::new(Exp::Lam { span: span(l, r), var, body }), + => Rc::new(e), + => Rc::new(e), + => Rc::new(e), Ops, } pub Ops = { - "." => Rc::new(Exp::DotCall { span: span(l, r), exp, name, args }), - "." "match" "{" "}" => Rc::new(Exp::Match { span: span(l, r), name, on_exp, motive, body }), + => Rc::new(e), + => Rc::new(e), App, } pub App = { - => Rc::new(Exp::Call { span: span(l, r), name, args }), - "comatch" "{" "}" => Rc::new(Exp::Comatch { span: span(l, r), name, is_lambda_sugar: false, body }), + => Rc::new(e), + => Rc::new(e), Builtins, } pub Builtins: Rc = { - "Type" => Rc::new(Exp::Type { span: span(l, r) }), - Hole, + => Rc::new(e), + Holes, } -pub Hole: Rc = { - "?" => Rc::new(Exp::Hole { span: span(l, r) }), +pub Holes: Rc = { + => Rc::new(e), Atom, } pub Atom: Rc = { - => Rc::new(Exp::NatLit { span: span(l, r), val: BigUint::parse_bytes(s.as_ref(), 10).unwrap() }), + => Rc::new(e), "(" ")" => exp, - => Rc::new(Exp::Call { span: span(l, r), name, args: Args::new() }), + => Rc::new(e), } +// Constituent parts of expressions +// +// + +Anno: Exp = ":" => + Exp::Anno { span: span(l, r), exp, typ }; + +Fun: Exp = "->" => + Exp::Fun { span: span(l, r), from, to }; + +Lam: Exp = "\\" "." => + Exp::Lam { span: span(l, r), var, body }; + +DotCall: Exp = "." => + Exp::DotCall { span: span(l, r), exp, name, args }; + +LocalMatch: Exp = "." "match" "{" "}" => + Exp::Match { span: span(l, r), name, on_exp, motive, body }; + +CallWithArgs: Exp = => + Exp::Call { span: span(l, r), name, args }; + +CallWithoutArgs: Exp = => + Exp::Call { span: span(l, r), name, args: Args::new() }; + +LocalComatch: Exp = "comatch" "{" "}" => + Exp::Comatch { span: span(l, r), name, is_lambda_sugar: false, body }; + +TypeUniv: Exp = "Type" => + Exp::Type { span: span(l, r) }; + +Hole: Exp = "?" => + Exp::Hole { span: span(l, r) }; + +NatLit: Exp = => + Exp::NatLit { span: span(l, r), val: BigUint::parse_bytes(s.as_ref(), 10).unwrap() }; + +// Helpers +// +// + Motive: Motive = { "as" "=>" => Motive { span: span(l, r), param, ret_typ }, } diff --git a/lang/parser/src/result.rs b/lang/parser/src/result.rs index b1a987e8dd..c4ecfe812f 100644 --- a/lang/parser/src/result.rs +++ b/lang/parser/src/result.rs @@ -25,7 +25,7 @@ pub enum ParseError { /// Generated by the parser when it encounters an EOF it did not expect. #[error("Unexpected end of file. Expected {expected}")] #[diagnostic(code("P-002"))] - UnrecognizedEOF { + UnrecognizedEof { #[label] location: SourceOffset, expected: String, @@ -59,7 +59,7 @@ impl From, &'static str>> for ParseErr use lalrpop_util::ParseError::*; match err { InvalidToken { location } => ParseError::InvalidToken { location: location.into() }, - UnrecognizedEOF { location, expected } => ParseError::UnrecognizedEOF { + UnrecognizedEof { location, expected } => ParseError::UnrecognizedEof { location: location.into(), expected: comma_separated(expected), }, From b4466f7fbb858cf017ce9b4dd232d65b4907de2c Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 14:21:21 +0200 Subject: [PATCH 2/6] Split cst into cst::exp and cst::decls --- lang/lowering/src/ctx.rs | 6 +- lang/lowering/src/imp.rs | 160 ++++++++++++----------- lang/lowering/src/result.rs | 2 +- lang/parser/src/{cst.rs => cst/decls.rs} | 127 +++++------------- lang/parser/src/cst/exp.rs | 63 +++++++++ lang/parser/src/cst/mod.rs | 2 + lang/parser/src/grammar/cst.lalrpop | 3 +- lang/parser/src/lib.rs | 4 +- lang/query/src/view/rt.rs | 2 +- test/test-runner/src/phases.rs | 6 +- 10 files changed, 196 insertions(+), 179 deletions(-) rename lang/parser/src/{cst.rs => cst/decls.rs} (58%) create mode 100644 lang/parser/src/cst/exp.rs create mode 100644 lang/parser/src/cst/mod.rs diff --git a/lang/lowering/src/ctx.rs b/lang/lowering/src/ctx.rs index a9b703b021..ce847dc683 100644 --- a/lang/lowering/src/ctx.rs +++ b/lang/lowering/src/ctx.rs @@ -1,7 +1,7 @@ use codespan::Span; use miette_util::ToMiette; use parser::cst; -use parser::cst::{BindingSite, Ident}; +use parser::cst::exp::{BindingSite, Ident}; use syntax::common::*; use syntax::ctx::{Context, ContextElem}; use syntax::generic::lookup_table::DeclMeta; @@ -171,7 +171,7 @@ impl ContextElem for Ident { } } -impl ContextElem for &cst::Param { +impl ContextElem for &cst::decls::Param { fn as_element(&self) -> ::ElemIn { match &self.name { BindingSite::Var { name } => name.to_owned(), @@ -180,7 +180,7 @@ impl ContextElem for &cst::Param { } } -impl ContextElem for &cst::ParamInst { +impl ContextElem for &cst::exp::ParamInst { fn as_element(&self) -> ::ElemIn { match &self.name { BindingSite::Var { name } => name.to_owned(), diff --git a/lang/lowering/src/imp.rs b/lang/lowering/src/imp.rs index 521636e9c2..f4be96c665 100644 --- a/lang/lowering/src/imp.rs +++ b/lang/lowering/src/imp.rs @@ -5,8 +5,8 @@ use num_bigint::BigUint; use miette_util::ToMiette; use parser::cst; -use parser::cst::BindingSite; -use parser::cst::Ident; +use parser::cst::exp::BindingSite; +use parser::cst::exp::Ident; use syntax::common::*; use syntax::ctx::BindContext; use syntax::generic::lookup_table; @@ -23,8 +23,8 @@ pub trait Lower { fn lower(&self, ctx: &mut Ctx) -> Result; } -pub fn lower_prg(prg: &cst::Prg) -> Result { - let cst::Prg { items } = prg; +pub fn lower_prg(prg: &cst::decls::Prg) -> Result { + let cst::decls::Prg { items } = prg; let (top_level_map, lookup_table) = build_lookup_table(items)?; @@ -39,7 +39,7 @@ pub fn lower_prg(prg: &cst::Prg) -> Result { /// Build the structure tracking the declaration order in the source code fn build_lookup_table( - items: &[cst::Decl], + items: &[cst::decls::Decl], ) -> Result<(HashMap, lookup_table::LookupTable), LoweringError> { let mut lookup_table = lookup_table::LookupTable::default(); let mut top_level_map = HashMap::default(); @@ -57,7 +57,7 @@ fn build_lookup_table( for item in items { match item { - cst::Decl::Data(data) => { + cst::decls::Decl::Data(data) => { // top_level_map add_top_level_decl( &data.name, @@ -77,7 +77,7 @@ fn build_lookup_table( let xtors = data.ctors.iter().map(|ctor| ctor.name.clone()); typ_decl.set_xtors(xtors); } - cst::Decl::Codata(codata) => { + cst::decls::Decl::Codata(codata) => { // top_level_map add_top_level_decl( &codata.name, @@ -97,7 +97,7 @@ fn build_lookup_table( let xtors = codata.dtors.iter().map(|ctor| ctor.name.clone()); typ_decl.set_xtors(xtors); } - cst::Decl::Def(def) => { + cst::decls::Decl::Def(def) => { // top_level_map add_top_level_decl(&def.name, &def.span, DeclMeta::Def)?; @@ -105,7 +105,7 @@ fn build_lookup_table( let type_name = def.scrutinee.typ.name.clone(); lookup_table.add_def(type_name, def.name.to_owned()); } - cst::Decl::Codef(codef) => { + cst::decls::Decl::Codef(codef) => { // top_level_map add_top_level_decl(&codef.name, &codef.span, DeclMeta::Codef)?; @@ -113,7 +113,7 @@ fn build_lookup_table( let type_name = codef.typ.name.clone(); lookup_table.add_def(type_name, codef.name.to_owned()) } - cst::Decl::Let(tl_let) => { + cst::decls::Decl::Let(tl_let) => { // top_level_map add_top_level_decl(&tl_let.name, &tl_let.span, DeclMeta::Let)?; @@ -125,7 +125,7 @@ fn build_lookup_table( Ok((top_level_map, lookup_table)) } -impl Lower for cst::DocComment { +impl Lower for cst::decls::DocComment { type Target = ust::DocComment; fn lower(&self, _ctx: &mut Ctx) -> Result { @@ -133,7 +133,7 @@ impl Lower for cst::DocComment { } } -impl Lower for cst::Attribute { +impl Lower for cst::decls::Attribute { type Target = ust::Attribute; fn lower(&self, _ctx: &mut Ctx) -> Result { @@ -141,27 +141,27 @@ impl Lower for cst::Attribute { } } -impl Lower for cst::Decl { +impl Lower for cst::decls::Decl { type Target = (); fn lower(&self, ctx: &mut Ctx) -> Result { let decl = match self { - cst::Decl::Data(data) => ust::Decl::Data(data.lower(ctx)?), - cst::Decl::Codata(codata) => ust::Decl::Codata(codata.lower(ctx)?), - cst::Decl::Def(def) => ust::Decl::Def(def.lower(ctx)?), - cst::Decl::Codef(codef) => ust::Decl::Codef(codef.lower(ctx)?), - cst::Decl::Let(tl_let) => ust::Decl::Let(tl_let.lower(ctx)?), + cst::decls::Decl::Data(data) => ust::Decl::Data(data.lower(ctx)?), + cst::decls::Decl::Codata(codata) => ust::Decl::Codata(codata.lower(ctx)?), + cst::decls::Decl::Def(def) => ust::Decl::Def(def.lower(ctx)?), + cst::decls::Decl::Codef(codef) => ust::Decl::Codef(codef.lower(ctx)?), + cst::decls::Decl::Let(tl_let) => ust::Decl::Let(tl_let.lower(ctx)?), }; ctx.add_decl(decl)?; Ok(()) } } -impl Lower for cst::Data { +impl Lower for cst::decls::Data { type Target = ust::Data; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Data { span, doc, name, attr, params, ctors } = self; + let cst::decls::Data { span, doc, name, attr, params, ctors } = self; let ctor_decls = ctors.lower(ctx)?.into_iter().map(ust::Decl::Ctor); @@ -180,11 +180,11 @@ impl Lower for cst::Data { } } -impl Lower for cst::Codata { +impl Lower for cst::decls::Codata { type Target = ust::Codata; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Codata { span, doc, name, attr, params, dtors } = self; + let cst::decls::Codata { span, doc, name, attr, params, dtors } = self; let dtor_decls = dtors.lower(ctx)?.into_iter().map(ust::Decl::Dtor); @@ -203,11 +203,11 @@ impl Lower for cst::Codata { } } -impl Lower for cst::Ctor { +impl Lower for cst::decls::Ctor { type Target = ust::Ctor; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Ctor { span, doc, name, params, typ } = self; + let cst::decls::Ctor { span, doc, name, params, typ } = self; let typ_name = match ctx.lookup_top_level_decl(name, span)? { DeclMeta::Ctor { ret_typ } => ret_typ, @@ -263,11 +263,11 @@ impl Lower for cst::Ctor { } } -impl Lower for cst::Dtor { +impl Lower for cst::decls::Dtor { type Target = ust::Dtor; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Dtor { span, doc, name, params, destructee, ret_typ } = self; + let cst::decls::Dtor { span, doc, name, params, destructee, ret_typ } = self; let typ_name = match ctx.lookup_top_level_decl(name, span)? { DeclMeta::Dtor { self_typ } => self_typ, @@ -297,7 +297,7 @@ impl Lower for cst::Dtor { Some(on_typ) => on_typ.clone(), None => { if type_arity == 0 { - cst::TypApp { + cst::decls::TypApp { span: Default::default(), name: typ_name.clone(), args: vec![], @@ -312,7 +312,7 @@ impl Lower for cst::Dtor { } }; - let self_param = cst::SelfParam { + let self_param = cst::decls::SelfParam { span: destructee.span, name: destructee.name.clone(), typ: on_typ, @@ -332,13 +332,13 @@ impl Lower for cst::Dtor { } } -impl Lower for cst::Def { +impl Lower for cst::decls::Def { type Target = ust::Def; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Def { span, doc, name, attr, params, scrutinee, ret_typ, body } = self; + let cst::decls::Def { span, doc, name, attr, params, scrutinee, ret_typ, body } = self; - let self_param: cst::SelfParam = scrutinee.clone().into(); + let self_param: cst::decls::SelfParam = scrutinee.clone().into(); lower_telescope(params, ctx, |ctx, params| { let body = body.lower(ctx)?; @@ -359,11 +359,11 @@ impl Lower for cst::Def { } } -impl Lower for cst::Codef { +impl Lower for cst::decls::Codef { type Target = ust::Codef; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Codef { span, doc, name, attr, params, typ, body, .. } = self; + let cst::decls::Codef { span, doc, name, attr, params, typ, body, .. } = self; lower_telescope(params, ctx, |ctx, params| { Ok(ust::Codef { @@ -379,11 +379,11 @@ impl Lower for cst::Codef { } } -impl Lower for cst::Let { +impl Lower for cst::decls::Let { type Target = ust::Let; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Let { span, doc, name, attr, params, typ, body } = self; + let cst::decls::Let { span, doc, name, attr, params, typ, body } = self; lower_telescope(params, ctx, |ctx, params| { Ok(ust::Let { @@ -399,21 +399,21 @@ impl Lower for cst::Let { } } -impl Lower for cst::Match { +impl Lower for cst::exp::Match { type Target = ust::Match; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Match { span, cases, omit_absurd } = self; + let cst::exp::Match { span, cases, omit_absurd } = self; Ok(ust::Match { info: Some(*span), cases: cases.lower(ctx)?, omit_absurd: *omit_absurd }) } } -impl Lower for cst::Case { +impl Lower for cst::exp::Case { type Target = ust::Case; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Case { span, name, args, body } = self; + let cst::exp::Case { span, name, args, body } = self; lower_telescope_inst(args, ctx, |ctx, args| { Ok(ust::Case { info: Some(*span), name: name.clone(), args, body: body.lower(ctx)? }) @@ -421,11 +421,11 @@ impl Lower for cst::Case { } } -impl Lower for cst::TypApp { +impl Lower for cst::decls::TypApp { type Target = ust::TypApp; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::TypApp { span, name, args } = self; + let cst::decls::TypApp { span, name, args } = self; Ok(ust::TypApp { info: Some(*span), @@ -435,12 +435,12 @@ impl Lower for cst::TypApp { } } -impl Lower for cst::Exp { +impl Lower for cst::exp::Exp { type Target = ust::Exp; fn lower(&self, ctx: &mut Ctx) -> Result { match self { - cst::Exp::Call { span, name, args } => match ctx.lookup(name, span)? { + cst::exp::Exp::Call { span, name, args } => match ctx.lookup(name, span)? { Elem::Bound(lvl) => Ok(ust::Exp::Var { info: Some(*span), name: name.clone(), @@ -469,7 +469,7 @@ impl Lower for cst::Exp { }), }, }, - cst::Exp::DotCall { span, exp, name, args } => match ctx.lookup(name, span)? { + cst::exp::Exp::DotCall { span, exp, name, args } => match ctx.lookup(name, span)? { Elem::Bound(_) => Err(LoweringError::CannotUseAsDtor { name: name.clone(), span: span.to_miette(), @@ -487,11 +487,11 @@ impl Lower for cst::Exp { }), }, }, - cst::Exp::Anno { span, exp, typ } => { + cst::exp::Exp::Anno { span, exp, typ } => { Ok(ust::Exp::Anno { info: Some(*span), exp: exp.lower(ctx)?, typ: typ.lower(ctx)? }) } - cst::Exp::Type { span } => Ok(ust::Exp::Type { info: Some(*span) }), - cst::Exp::Match { span, name, on_exp, motive, body } => Ok(ust::Exp::Match { + cst::exp::Exp::Type { span } => Ok(ust::Exp::Type { info: Some(*span) }), + cst::exp::Exp::Match { span, name, on_exp, motive, body } => Ok(ust::Exp::Match { info: Some(*span), ctx: (), name: ctx.unique_label(name.to_owned(), span)?, @@ -500,15 +500,15 @@ impl Lower for cst::Exp { ret_typ: (), body: body.lower(ctx)?, }), - cst::Exp::Comatch { span, name, is_lambda_sugar, body } => Ok(ust::Exp::Comatch { + cst::exp::Exp::Comatch { span, name, is_lambda_sugar, body } => Ok(ust::Exp::Comatch { info: Some(*span), ctx: (), name: ctx.unique_label(name.to_owned(), span)?, is_lambda_sugar: *is_lambda_sugar, body: body.lower(ctx)?, }), - cst::Exp::Hole { span } => Ok(ust::Exp::Hole { info: Some(*span) }), - cst::Exp::NatLit { span, val } => { + cst::exp::Exp::Hole { span } => Ok(ust::Exp::Hole { info: Some(*span) }), + cst::exp::Exp::NatLit { span, val } => { let mut out = ust::Exp::Ctor { info: Some(*span), name: "Z".to_owned(), @@ -528,27 +528,27 @@ impl Lower for cst::Exp { Ok(out) } - cst::Exp::Fun { span, from, to } => Ok(ust::Exp::TypCtor { + cst::exp::Exp::Fun { span, from, to } => Ok(ust::Exp::TypCtor { info: Some(*span), name: "Fun".to_owned(), args: ust::Args { args: vec![from.lower(ctx)?, to.lower(ctx)?] }, }), - cst::Exp::Lam { span, var, body } => { - let comatch = cst::Exp::Comatch { + cst::exp::Exp::Lam { span, var, body } => { + let comatch = cst::exp::Exp::Comatch { span: *span, name: None, is_lambda_sugar: true, - body: cst::Match { + body: cst::exp::Match { span: *span, - cases: vec![cst::Case { + cases: vec![cst::exp::Case { span: *span, name: "ap".to_owned(), - args: cst::TelescopeInst(vec![ - cst::ParamInst { + args: cst::exp::TelescopeInst(vec![ + cst::exp::ParamInst { span: Default::default(), name: BindingSite::Wildcard, }, - cst::ParamInst { + cst::exp::ParamInst { span: Default::default(), name: BindingSite::Wildcard, }, @@ -565,17 +565,17 @@ impl Lower for cst::Exp { } } -fn bs_to_name(bs: &cst::BindingSite) -> Ident { +fn bs_to_name(bs: &cst::exp::BindingSite) -> Ident { match bs { BindingSite::Var { name } => name.clone(), BindingSite::Wildcard => "_".to_owned(), } } -impl Lower for cst::Motive { +impl Lower for cst::exp::Motive { type Target = ust::Motive; fn lower(&self, ctx: &mut Ctx) -> Result { - let cst::Motive { span, param, ret_typ } = self; + let cst::exp::Motive { span, param, ret_typ } = self; Ok(ust::Motive { info: Some(*span), @@ -614,28 +614,32 @@ impl Lower for Rc { } fn lower_self_param Result>( - self_param: &cst::SelfParam, + self_param: &cst::decls::SelfParam, ctx: &mut Ctx, f: F, ) -> Result { - let cst::SelfParam { span, name, typ } = self_param; + let cst::decls::SelfParam { span, name, typ } = self_param; let typ_out = typ.lower(ctx)?; ctx.bind_single(name.clone().unwrap_or_default(), |ctx| { f(ctx, ust::SelfParam { info: Some(*span), name: name.clone(), typ: typ_out }) }) } -fn desugar_telescope(tel: &cst::Telescope) -> cst::Telescope { - let cst::Telescope(params) = tel; - let params: Vec = params.iter().flat_map(desugar_param).collect(); - cst::Telescope(params) +fn desugar_telescope(tel: &cst::decls::Telescope) -> cst::decls::Telescope { + let cst::decls::Telescope(params) = tel; + let params: Vec = params.iter().flat_map(desugar_param).collect(); + cst::decls::Telescope(params) } -fn desugar_param(param: &cst::Param) -> Vec { - let cst::Param { name, names, typ } = param; - let mut params: Vec = - vec![cst::Param { name: name.clone(), names: vec![], typ: typ.clone() }]; +fn desugar_param(param: &cst::decls::Param) -> Vec { + let cst::decls::Param { name, names, typ } = param; + let mut params: Vec = + vec![cst::decls::Param { name: name.clone(), names: vec![], typ: typ.clone() }]; for extra_name in names { - params.push(cst::Param { name: extra_name.clone(), names: vec![], typ: typ.clone() }); + params.push(cst::decls::Param { + name: extra_name.clone(), + names: vec![], + typ: typ.clone(), + }); } params } @@ -644,7 +648,11 @@ fn desugar_param(param: &cst::Param) -> Vec { /// /// Execute a function `f` under the context where all binders /// of the telescope are in scope. -fn lower_telescope(tele: &cst::Telescope, ctx: &mut Ctx, f: F) -> Result +fn lower_telescope( + tele: &cst::decls::Telescope, + ctx: &mut Ctx, + f: F, +) -> Result where F: FnOnce(&mut Ctx, ust::Telescope) -> Result, { @@ -654,7 +662,7 @@ where Ok(vec![]), |ctx, params_out, param| { let mut params_out = params_out?; - let cst::Param { name, names: _, typ } = param; // The `names` field has been removed by `desugar_telescope`. + let cst::decls::Param { name, names: _, typ } = param; // The `names` field has been removed by `desugar_telescope`. let typ_out = typ.lower(ctx)?; let name = match name { BindingSite::Var { name } => name.clone(), @@ -669,7 +677,7 @@ where } fn lower_telescope_inst Result>( - tel_inst: &cst::TelescopeInst, + tel_inst: &cst::exp::TelescopeInst, ctx: &mut Ctx, f: F, ) -> Result { @@ -678,7 +686,7 @@ fn lower_telescope_inst Result, } -#[derive(Debug, Clone)] -pub enum BindingSite { - Var { name: Ident }, - Wildcard, -} - #[derive(Debug, Clone)] pub struct Prg { pub items: Vec, @@ -43,7 +35,7 @@ pub struct Data { pub span: Span, pub doc: Option, pub attr: Attribute, - pub name: Ident, + pub name: exp::Ident, pub params: Telescope, pub ctors: Vec, } @@ -53,7 +45,7 @@ pub struct Codata { pub span: Span, pub doc: Option, pub attr: Attribute, - pub name: Ident, + pub name: exp::Ident, pub params: Telescope, pub dtors: Vec, } @@ -62,7 +54,7 @@ pub struct Codata { pub struct Ctor { pub span: Span, pub doc: Option, - pub name: Ident, + pub name: exp::Ident, pub params: Telescope, pub typ: Option, } @@ -71,123 +63,97 @@ pub struct Ctor { pub struct Dtor { pub span: Span, pub doc: Option, - pub name: Ident, + pub name: exp::Ident, pub params: Telescope, pub destructee: Destructee, - pub ret_typ: Rc, + pub ret_typ: Rc, } #[derive(Debug, Clone)] pub struct Def { pub span: Span, pub doc: Option, - pub name: Ident, + pub name: exp::Ident, pub attr: Attribute, pub params: Telescope, pub scrutinee: Scrutinee, - pub ret_typ: Rc, - pub body: Match, + pub ret_typ: Rc, + pub body: exp::Match, } #[derive(Debug, Clone)] pub struct Codef { pub span: Span, pub doc: Option, - pub name: Ident, + pub name: exp::Ident, pub attr: Attribute, pub params: Telescope, pub typ: TypApp, - pub body: Match, + pub body: exp::Match, } #[derive(Debug, Clone)] pub struct Let { pub span: Span, pub doc: Option, - pub name: Ident, + pub name: exp::Ident, pub attr: Attribute, pub params: Telescope, - pub typ: Rc, - pub body: Rc, -} - -#[derive(Debug, Clone)] -pub struct Match { - pub span: Span, - pub cases: Vec, - pub omit_absurd: bool, -} - -#[derive(Debug, Clone)] -pub struct Case { - pub span: Span, - pub name: Ident, - pub args: TelescopeInst, - /// Body being `None` represents an absurd pattern - pub body: Option>, + pub typ: Rc, + pub body: Rc, } #[derive(Debug, Clone)] pub struct Scrutinee { pub span: Span, - pub name: Option, + pub name: Option, pub typ: TypApp, } #[derive(Debug, Clone)] pub struct Destructee { pub span: Span, - pub name: Option, + pub name: Option, pub typ: Option, } #[derive(Debug, Clone)] pub struct SelfParam { pub span: Span, - pub name: Option, + pub name: Option, pub typ: TypApp, } -impl From for SelfParam { - fn from(scrutinee: Scrutinee) -> Self { - let Scrutinee { span, name, typ } = scrutinee; - - SelfParam { span, name, typ } - } -} - #[derive(Debug, Clone)] pub struct TypApp { pub span: Span, - pub name: Ident, - pub args: Args, + pub name: exp::Ident, + pub args: exp::Args, } impl TypApp { - pub fn to_exp(&self) -> Exp { - Exp::Call { span: self.span, name: self.name.clone(), args: self.args.clone() } + pub fn to_exp(&self) -> exp::Exp { + exp::Exp::Call { span: self.span, name: self.name.clone(), args: self.args.clone() } } } -#[derive(Debug, Clone)] -pub enum Exp { - Call { span: Span, name: Ident, args: Args }, - DotCall { span: Span, exp: Rc, name: Ident, args: Args }, - Anno { span: Span, exp: Rc, typ: Rc }, - Type { span: Span }, - Match { span: Span, name: Option, on_exp: Rc, motive: Option, body: Match }, - Comatch { span: Span, name: Option, is_lambda_sugar: bool, body: Match }, - Hole { span: Span }, - NatLit { span: Span, val: BigUint }, - Fun { span: Span, from: Rc, to: Rc }, - Lam { span: Span, var: ParamInst, body: Rc }, +impl From for SelfParam { + fn from(scrutinee: Scrutinee) -> Self { + let Scrutinee { span, name, typ } = scrutinee; + + SelfParam { span, name, typ } + } } +/// A `Param` can either be a single parameter, like `x : T`, or a list of parameters, like `x, y, z : T`. #[derive(Debug, Clone)] -pub struct Motive { - pub span: Span, - pub param: ParamInst, - pub ret_typ: Rc, +pub struct Param { + /// The obligatory parameter. + pub name: exp::BindingSite, + /// A possible list of additional parameters. + pub names: Vec, + /// The type of the parameter. + pub typ: Rc, } /// Wrapper type signifying the wrapped parameters have telescope @@ -196,10 +162,6 @@ pub struct Motive { #[derive(Debug, Clone)] pub struct Telescope(pub Params); -/// Instantiation of a previously declared telescope -#[derive(Debug, Clone)] -pub struct TelescopeInst(pub Vec); - impl Telescope { pub fn is_empty(&self) -> bool { self.0.is_empty() @@ -211,22 +173,3 @@ impl Telescope { } pub type Params = Vec; -pub type Args = Vec>; - -/// A `Param` can either be a single parameter, like `x : T`, or a list of parameters, like `x, y, z : T`. -#[derive(Debug, Clone)] -pub struct Param { - /// The obligatory parameter. - pub name: BindingSite, - /// A possible list of additional parameters. - pub names: Vec, - /// The type of the parameter. - pub typ: Rc, -} - -/// Instantiation of a previously declared parameter -#[derive(Debug, Clone)] -pub struct ParamInst { - pub span: Span, - pub name: BindingSite, -} diff --git a/lang/parser/src/cst/exp.rs b/lang/parser/src/cst/exp.rs new file mode 100644 index 0000000000..aeebe2ca32 --- /dev/null +++ b/lang/parser/src/cst/exp.rs @@ -0,0 +1,63 @@ +use std::rc::Rc; + +use codespan::Span; + +use num_bigint::BigUint; + +pub type Ident = String; + +#[derive(Debug, Clone)] +pub enum BindingSite { + Var { name: Ident }, + Wildcard, +} + +#[derive(Debug, Clone)] +pub struct Match { + pub span: Span, + pub cases: Vec, + pub omit_absurd: bool, +} + +#[derive(Debug, Clone)] +pub struct Case { + pub span: Span, + pub name: Ident, + pub args: TelescopeInst, + /// Body being `None` represents an absurd pattern + pub body: Option>, +} + +#[derive(Debug, Clone)] +pub enum Exp { + Call { span: Span, name: Ident, args: Args }, + DotCall { span: Span, exp: Rc, name: Ident, args: Args }, + Anno { span: Span, exp: Rc, typ: Rc }, + Type { span: Span }, + Match { span: Span, name: Option, on_exp: Rc, motive: Option, body: Match }, + Comatch { span: Span, name: Option, is_lambda_sugar: bool, body: Match }, + Hole { span: Span }, + NatLit { span: Span, val: BigUint }, + Fun { span: Span, from: Rc, to: Rc }, + Lam { span: Span, var: ParamInst, body: Rc }, +} + +#[derive(Debug, Clone)] +pub struct Motive { + pub span: Span, + pub param: ParamInst, + pub ret_typ: Rc, +} + +pub type Args = Vec>; + +/// Instantiation of a previously declared parameter +#[derive(Debug, Clone)] +pub struct ParamInst { + pub span: Span, + pub name: BindingSite, +} + +/// Instantiation of a previously declared telescope +#[derive(Debug, Clone)] +pub struct TelescopeInst(pub Vec); diff --git a/lang/parser/src/cst/mod.rs b/lang/parser/src/cst/mod.rs new file mode 100644 index 0000000000..613d48334f --- /dev/null +++ b/lang/parser/src/cst/mod.rs @@ -0,0 +1,2 @@ +pub mod decls; +pub mod exp; diff --git a/lang/parser/src/grammar/cst.lalrpop b/lang/parser/src/grammar/cst.lalrpop index 214d659bc1..f8c5548fe0 100644 --- a/lang/parser/src/grammar/cst.lalrpop +++ b/lang/parser/src/grammar/cst.lalrpop @@ -2,7 +2,8 @@ use std::rc::Rc; use num_bigint::BigUint; -use crate::cst::*; +use crate::cst::exp::*; +use crate::cst::decls::*; use super::util::span; diff --git a/lang/parser/src/lib.rs b/lang/parser/src/lib.rs index 9e84e1d95c..d512f816f1 100644 --- a/lang/parser/src/lib.rs +++ b/lang/parser/src/lib.rs @@ -7,10 +7,10 @@ use std::rc::Rc; use grammar::cst::{ExpParser, PrgParser}; pub use result::*; -pub fn parse_exp(s: &str) -> Result, ParseError> { +pub fn parse_exp(s: &str) -> Result, ParseError> { ExpParser::new().parse(s).map_err(From::from) } -pub fn parse_program(s: &str) -> Result { +pub fn parse_program(s: &str) -> Result { PrgParser::new().parse(s).map_err(From::from) } diff --git a/lang/query/src/view/rt.rs b/lang/query/src/view/rt.rs index 97f72028f4..7400ddccf4 100644 --- a/lang/query/src/view/rt.rs +++ b/lang/query/src/view/rt.rs @@ -19,7 +19,7 @@ impl<'a> DatabaseView<'a> { database.files.source(*file_id) } - pub fn cst(&self) -> Result { + pub fn cst(&self) -> Result { let source = self.source(); parser::parse_program(source).map_err(Error::Parser) } diff --git a/test/test-runner/src/phases.rs b/test/test-runner/src/phases.rs index f52419bb5a..e7e7e3fae9 100644 --- a/test/test-runner/src/phases.rs +++ b/test/test-runner/src/phases.rs @@ -186,7 +186,7 @@ pub struct Print { impl Phase for Parse { type In = String; - type Out = cst::Prg; + type Out = cst::decls::Prg; type Err = parser::ParseError; fn new(name: &'static str) -> Self { @@ -203,7 +203,7 @@ impl Phase for Parse { } impl Phase for Lower { - type In = cst::Prg; + type In = cst::decls::Prg; type Out = ust::Prg; type Err = lowering::LoweringError; @@ -274,7 +274,7 @@ impl Phase for Forget { } } -impl TestOutput for cst::Prg { +impl TestOutput for cst::decls::Prg { fn test_output(&self) -> String { // TODO: Improve test output format!("{self:?}") From 0eba5b0e7e8aecedfc36d5cac1ec9a78c73aaac2 Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 14:43:49 +0200 Subject: [PATCH 3/6] Factor out the constituents of cst::Exp All the constituent parts of cst::Exp are now individual structs. --- lang/lowering/src/imp.rs | 71 ++++++++++++++--------- lang/parser/src/cst/decls.rs | 6 +- lang/parser/src/cst/exp.rs | 89 +++++++++++++++++++++++++---- lang/parser/src/grammar/cst.lalrpop | 66 ++++++++++----------- 4 files changed, 162 insertions(+), 70 deletions(-) diff --git a/lang/lowering/src/imp.rs b/lang/lowering/src/imp.rs index f4be96c665..11fe5af04e 100644 --- a/lang/lowering/src/imp.rs +++ b/lang/lowering/src/imp.rs @@ -440,7 +440,9 @@ impl Lower for cst::exp::Exp { fn lower(&self, ctx: &mut Ctx) -> Result { match self { - cst::exp::Exp::Call { span, name, args } => match ctx.lookup(name, span)? { + cst::exp::Exp::Call(cst::exp::Call { span, name, args }) => match ctx + .lookup(name, span)? + { Elem::Bound(lvl) => Ok(ust::Exp::Var { info: Some(*span), name: name.clone(), @@ -469,29 +471,39 @@ impl Lower for cst::exp::Exp { }), }, }, - cst::exp::Exp::DotCall { span, exp, name, args } => match ctx.lookup(name, span)? { - Elem::Bound(_) => Err(LoweringError::CannotUseAsDtor { - name: name.clone(), - span: span.to_miette(), - }), - Elem::Decl(meta) => match meta.kind() { - DeclKind::Def | DeclKind::Dtor => Ok(ust::Exp::Dtor { - info: Some(*span), - exp: exp.lower(ctx)?, - name: name.clone(), - args: ust::Args { args: args.lower(ctx)? }, - }), - _ => Err(LoweringError::CannotUseAsDtor { + cst::exp::Exp::DotCall(cst::exp::DotCall { span, exp, name, args }) => { + match ctx.lookup(name, span)? { + Elem::Bound(_) => Err(LoweringError::CannotUseAsDtor { name: name.clone(), span: span.to_miette(), }), - }, - }, - cst::exp::Exp::Anno { span, exp, typ } => { + Elem::Decl(meta) => match meta.kind() { + DeclKind::Def | DeclKind::Dtor => Ok(ust::Exp::Dtor { + info: Some(*span), + exp: exp.lower(ctx)?, + name: name.clone(), + args: ust::Args { args: args.lower(ctx)? }, + }), + _ => Err(LoweringError::CannotUseAsDtor { + name: name.clone(), + span: span.to_miette(), + }), + }, + } + } + cst::exp::Exp::Anno(cst::exp::Anno { span, exp, typ }) => { Ok(ust::Exp::Anno { info: Some(*span), exp: exp.lower(ctx)?, typ: typ.lower(ctx)? }) } - cst::exp::Exp::Type { span } => Ok(ust::Exp::Type { info: Some(*span) }), - cst::exp::Exp::Match { span, name, on_exp, motive, body } => Ok(ust::Exp::Match { + cst::exp::Exp::Type(cst::exp::Type { span }) => { + Ok(ust::Exp::Type { info: Some(*span) }) + } + cst::exp::Exp::LocalMatch(cst::exp::LocalMatch { + span, + name, + on_exp, + motive, + body, + }) => Ok(ust::Exp::Match { info: Some(*span), ctx: (), name: ctx.unique_label(name.to_owned(), span)?, @@ -500,15 +512,22 @@ impl Lower for cst::exp::Exp { ret_typ: (), body: body.lower(ctx)?, }), - cst::exp::Exp::Comatch { span, name, is_lambda_sugar, body } => Ok(ust::Exp::Comatch { + cst::exp::Exp::LocalComatch(cst::exp::LocalComatch { + span, + name, + is_lambda_sugar, + body, + }) => Ok(ust::Exp::Comatch { info: Some(*span), ctx: (), name: ctx.unique_label(name.to_owned(), span)?, is_lambda_sugar: *is_lambda_sugar, body: body.lower(ctx)?, }), - cst::exp::Exp::Hole { span } => Ok(ust::Exp::Hole { info: Some(*span) }), - cst::exp::Exp::NatLit { span, val } => { + cst::exp::Exp::Hole(cst::exp::Hole { span }) => { + Ok(ust::Exp::Hole { info: Some(*span) }) + } + cst::exp::Exp::NatLit(cst::exp::NatLit { span, val }) => { let mut out = ust::Exp::Ctor { info: Some(*span), name: "Z".to_owned(), @@ -528,13 +547,13 @@ impl Lower for cst::exp::Exp { Ok(out) } - cst::exp::Exp::Fun { span, from, to } => Ok(ust::Exp::TypCtor { + cst::exp::Exp::Fun(cst::exp::Fun { span, from, to }) => Ok(ust::Exp::TypCtor { info: Some(*span), name: "Fun".to_owned(), args: ust::Args { args: vec![from.lower(ctx)?, to.lower(ctx)?] }, }), - cst::exp::Exp::Lam { span, var, body } => { - let comatch = cst::exp::Exp::Comatch { + cst::exp::Exp::Lam(cst::exp::Lam { span, var, body }) => { + let comatch = cst::exp::Exp::LocalComatch(cst::exp::LocalComatch { span: *span, name: None, is_lambda_sugar: true, @@ -558,7 +577,7 @@ impl Lower for cst::exp::Exp { }], omit_absurd: false, }, - }; + }); comatch.lower(ctx) } } diff --git a/lang/parser/src/cst/decls.rs b/lang/parser/src/cst/decls.rs index 8eb33c9697..4d36adb8eb 100644 --- a/lang/parser/src/cst/decls.rs +++ b/lang/parser/src/cst/decls.rs @@ -133,7 +133,11 @@ pub struct TypApp { impl TypApp { pub fn to_exp(&self) -> exp::Exp { - exp::Exp::Call { span: self.span, name: self.name.clone(), args: self.args.clone() } + exp::Exp::Call(exp::Call { + span: self.span, + name: self.name.clone(), + args: self.args.clone(), + }) } } diff --git a/lang/parser/src/cst/exp.rs b/lang/parser/src/cst/exp.rs index aeebe2ca32..f9edd0b6c0 100644 --- a/lang/parser/src/cst/exp.rs +++ b/lang/parser/src/cst/exp.rs @@ -30,16 +30,85 @@ pub struct Case { #[derive(Debug, Clone)] pub enum Exp { - Call { span: Span, name: Ident, args: Args }, - DotCall { span: Span, exp: Rc, name: Ident, args: Args }, - Anno { span: Span, exp: Rc, typ: Rc }, - Type { span: Span }, - Match { span: Span, name: Option, on_exp: Rc, motive: Option, body: Match }, - Comatch { span: Span, name: Option, is_lambda_sugar: bool, body: Match }, - Hole { span: Span }, - NatLit { span: Span, val: BigUint }, - Fun { span: Span, from: Rc, to: Rc }, - Lam { span: Span, var: ParamInst, body: Rc }, + Call(Call), + DotCall(DotCall), + Anno(Anno), + Type(Type), + LocalMatch(LocalMatch), + LocalComatch(LocalComatch), + Hole(Hole), + NatLit(NatLit), + Fun(Fun), + Lam(Lam), +} + +#[derive(Debug, Clone)] +pub struct Call { + pub span: Span, + pub name: Ident, + pub args: Args, +} + +#[derive(Debug, Clone)] +pub struct DotCall { + pub span: Span, + pub exp: Rc, + pub name: Ident, + pub args: Args, +} + +#[derive(Debug, Clone)] +pub struct Anno { + pub span: Span, + pub exp: Rc, + pub typ: Rc, +} + +#[derive(Debug, Clone)] +pub struct Type { + pub span: Span, +} + +#[derive(Debug, Clone)] +pub struct LocalMatch { + pub span: Span, + pub name: Option, + pub on_exp: Rc, + pub motive: Option, + pub body: Match, +} + +#[derive(Debug, Clone)] +pub struct LocalComatch { + pub span: Span, + pub name: Option, + pub is_lambda_sugar: bool, + pub body: Match, +} + +#[derive(Debug, Clone)] +pub struct Hole { + pub span: Span, +} + +#[derive(Debug, Clone)] +pub struct NatLit { + pub span: Span, + pub val: BigUint, +} + +#[derive(Debug, Clone)] +pub struct Fun { + pub span: Span, + pub from: Rc, + pub to: Rc, +} + +#[derive(Debug, Clone)] +pub struct Lam { + pub span: Span, + pub var: ParamInst, + pub body: Rc, } #[derive(Debug, Clone)] diff --git a/lang/parser/src/grammar/cst.lalrpop b/lang/parser/src/grammar/cst.lalrpop index f8c5548fe0..b9b6413381 100644 --- a/lang/parser/src/grammar/cst.lalrpop +++ b/lang/parser/src/grammar/cst.lalrpop @@ -167,76 +167,76 @@ pub TypApp: TypApp = { // pub Exp: Rc = { - => Rc::new(e), - => Rc::new(e), - => Rc::new(e), + => Rc::new(Exp::Anno(e)), + => Rc::new(Exp::Fun(e)), + => Rc::new(Exp::Lam(e)), Ops, } pub Ops = { - => Rc::new(e), - => Rc::new(e), + => Rc::new(Exp::DotCall(e)), + => Rc::new(Exp::LocalMatch(e)), App, } pub App = { - => Rc::new(e), - => Rc::new(e), + => Rc::new(Exp::Call(e)), + => Rc::new(Exp::LocalComatch(e)), Builtins, } pub Builtins: Rc = { - => Rc::new(e), + => Rc::new(Exp::Type(e)), Holes, } pub Holes: Rc = { - => Rc::new(e), + => Rc::new(Exp::Hole(e)), Atom, } pub Atom: Rc = { - => Rc::new(e), + => Rc::new(Exp::NatLit(e)), "(" ")" => exp, - => Rc::new(e), + => Rc::new(Exp::Call(e)), } // Constituent parts of expressions // // -Anno: Exp = ":" => - Exp::Anno { span: span(l, r), exp, typ }; +Anno: Anno = ":" => + Anno { span: span(l, r), exp, typ }; -Fun: Exp = "->" => - Exp::Fun { span: span(l, r), from, to }; +Fun: Fun = "->" => + Fun { span: span(l, r), from, to }; -Lam: Exp = "\\" "." => - Exp::Lam { span: span(l, r), var, body }; +Lam: Lam = "\\" "." => + Lam { span: span(l, r), var, body }; -DotCall: Exp = "." => - Exp::DotCall { span: span(l, r), exp, name, args }; +DotCall: DotCall = "." => + DotCall { span: span(l, r), exp, name, args }; -LocalMatch: Exp = "." "match" "{" "}" => - Exp::Match { span: span(l, r), name, on_exp, motive, body }; +LocalMatch: LocalMatch = "." "match" "{" "}" => + LocalMatch { span: span(l, r), name, on_exp, motive, body }; -CallWithArgs: Exp = => - Exp::Call { span: span(l, r), name, args }; +CallWithArgs: Call = => + Call { span: span(l, r), name, args }; -CallWithoutArgs: Exp = => - Exp::Call { span: span(l, r), name, args: Args::new() }; +CallWithoutArgs: Call = => + Call { span: span(l, r), name, args: Args::new() }; -LocalComatch: Exp = "comatch" "{" "}" => - Exp::Comatch { span: span(l, r), name, is_lambda_sugar: false, body }; +LocalComatch: LocalComatch = "comatch" "{" "}" => + LocalComatch { span: span(l, r), name, is_lambda_sugar: false, body }; -TypeUniv: Exp = "Type" => - Exp::Type { span: span(l, r) }; +TypeUniv: Type = "Type" => + Type { span: span(l, r) }; -Hole: Exp = "?" => - Exp::Hole { span: span(l, r) }; +Hole: Hole = "?" => + Hole { span: span(l, r) }; -NatLit: Exp = => - Exp::NatLit { span: span(l, r), val: BigUint::parse_bytes(s.as_ref(), 10).unwrap() }; +NatLit: NatLit = => + NatLit { span: span(l, r), val: BigUint::parse_bytes(s.as_ref(), 10).unwrap() }; // Helpers // From 774bf4f1738d954d748010b8848bbecb9fb08c5e Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 15:05:22 +0200 Subject: [PATCH 4/6] Split lowering of cst::Exp into multiple impls --- lang/lowering/src/imp.rs | 332 +++++++++++++++++++++++---------------- 1 file changed, 198 insertions(+), 134 deletions(-) diff --git a/lang/lowering/src/imp.rs b/lang/lowering/src/imp.rs index 11fe5af04e..acff084b15 100644 --- a/lang/lowering/src/imp.rs +++ b/lang/lowering/src/imp.rs @@ -435,151 +435,215 @@ impl Lower for cst::decls::TypApp { } } -impl Lower for cst::exp::Exp { +impl Lower for cst::exp::Call { type Target = ust::Exp; fn lower(&self, ctx: &mut Ctx) -> Result { - match self { - cst::exp::Exp::Call(cst::exp::Call { span, name, args }) => match ctx - .lookup(name, span)? - { - Elem::Bound(lvl) => Ok(ust::Exp::Var { - info: Some(*span), - name: name.clone(), - ctx: (), - idx: ctx.level_to_index(lvl), - }), - Elem::Decl(meta) => match meta.kind() { - DeclKind::Data | DeclKind::Codata => Ok(ust::Exp::TypCtor { - info: Some(*span), - name: name.to_owned(), - args: ust::Args { args: args.lower(ctx)? }, - }), - DeclKind::Def | DeclKind::Dtor => Err(LoweringError::MustUseAsDtor { - name: name.to_owned(), - span: span.to_miette(), - }), - DeclKind::Codef | DeclKind::Ctor => Ok(ust::Exp::Ctor { - info: Some(*span), - name: name.to_owned(), - args: ust::Args { args: args.lower(ctx)? }, - }), - DeclKind::Let => Err(LoweringError::Impossible { - message: "Referencing top-level let definitions is not implemented, yet" - .to_owned(), - span: Some(span.to_miette()), - }), - }, - }, - cst::exp::Exp::DotCall(cst::exp::DotCall { span, exp, name, args }) => { - match ctx.lookup(name, span)? { - Elem::Bound(_) => Err(LoweringError::CannotUseAsDtor { - name: name.clone(), - span: span.to_miette(), - }), - Elem::Decl(meta) => match meta.kind() { - DeclKind::Def | DeclKind::Dtor => Ok(ust::Exp::Dtor { - info: Some(*span), - exp: exp.lower(ctx)?, - name: name.clone(), - args: ust::Args { args: args.lower(ctx)? }, - }), - _ => Err(LoweringError::CannotUseAsDtor { - name: name.clone(), - span: span.to_miette(), - }), - }, - } - } - cst::exp::Exp::Anno(cst::exp::Anno { span, exp, typ }) => { - Ok(ust::Exp::Anno { info: Some(*span), exp: exp.lower(ctx)?, typ: typ.lower(ctx)? }) - } - cst::exp::Exp::Type(cst::exp::Type { span }) => { - Ok(ust::Exp::Type { info: Some(*span) }) - } - cst::exp::Exp::LocalMatch(cst::exp::LocalMatch { - span, - name, - on_exp, - motive, - body, - }) => Ok(ust::Exp::Match { - info: Some(*span), - ctx: (), - name: ctx.unique_label(name.to_owned(), span)?, - on_exp: on_exp.lower(ctx)?, - motive: motive.lower(ctx)?, - ret_typ: (), - body: body.lower(ctx)?, - }), - cst::exp::Exp::LocalComatch(cst::exp::LocalComatch { - span, - name, - is_lambda_sugar, - body, - }) => Ok(ust::Exp::Comatch { + let cst::exp::Call { span, name, args } = self; + match ctx.lookup(name, span)? { + Elem::Bound(lvl) => Ok(ust::Exp::Var { info: Some(*span), + name: name.clone(), ctx: (), - name: ctx.unique_label(name.to_owned(), span)?, - is_lambda_sugar: *is_lambda_sugar, - body: body.lower(ctx)?, + idx: ctx.level_to_index(lvl), }), - cst::exp::Exp::Hole(cst::exp::Hole { span }) => { - Ok(ust::Exp::Hole { info: Some(*span) }) - } - cst::exp::Exp::NatLit(cst::exp::NatLit { span, val }) => { - let mut out = ust::Exp::Ctor { + Elem::Decl(meta) => match meta.kind() { + DeclKind::Data | DeclKind::Codata => Ok(ust::Exp::TypCtor { info: Some(*span), - name: "Z".to_owned(), - args: ust::Args { args: vec![] }, - }; - - let mut i = BigUint::from(0usize); - - while &i != val { - i += 1usize; - out = ust::Exp::Ctor { - info: Some(*span), - name: "S".to_owned(), - args: ust::Args { args: vec![Rc::new(out)] }, - }; - } + name: name.to_owned(), + args: ust::Args { args: args.lower(ctx)? }, + }), + DeclKind::Def | DeclKind::Dtor => Err(LoweringError::MustUseAsDtor { + name: name.to_owned(), + span: span.to_miette(), + }), + DeclKind::Codef | DeclKind::Ctor => Ok(ust::Exp::Ctor { + info: Some(*span), + name: name.to_owned(), + args: ust::Args { args: args.lower(ctx)? }, + }), + DeclKind::Let => Err(LoweringError::Impossible { + message: "Referencing top-level let definitions is not implemented, yet" + .to_owned(), + span: Some(span.to_miette()), + }), + }, + } + } +} - Ok(out) +impl Lower for cst::exp::DotCall { + type Target = ust::Exp; + + fn lower(&self, ctx: &mut Ctx) -> Result { + let cst::exp::DotCall { span, exp, name, args } = self; + + match ctx.lookup(name, span)? { + Elem::Bound(_) => { + Err(LoweringError::CannotUseAsDtor { name: name.clone(), span: span.to_miette() }) } - cst::exp::Exp::Fun(cst::exp::Fun { span, from, to }) => Ok(ust::Exp::TypCtor { + Elem::Decl(meta) => match meta.kind() { + DeclKind::Def | DeclKind::Dtor => Ok(ust::Exp::Dtor { + info: Some(*span), + exp: exp.lower(ctx)?, + name: name.clone(), + args: ust::Args { args: args.lower(ctx)? }, + }), + _ => Err(LoweringError::CannotUseAsDtor { + name: name.clone(), + span: span.to_miette(), + }), + }, + } + } +} + +impl Lower for cst::exp::Anno { + type Target = ust::Exp; + + fn lower(&self, ctx: &mut Ctx) -> Result { + let cst::exp::Anno { span, exp, typ } = self; + Ok(ust::Exp::Anno { info: Some(*span), exp: exp.lower(ctx)?, typ: typ.lower(ctx)? }) + } +} + +impl Lower for cst::exp::Type { + type Target = ust::Exp; + + fn lower(&self, _ctx: &mut Ctx) -> Result { + let cst::exp::Type { span } = self; + Ok(ust::Exp::Type { info: Some(*span) }) + } +} + +impl Lower for cst::exp::LocalMatch { + type Target = ust::Exp; + + fn lower(&self, ctx: &mut Ctx) -> Result { + let cst::exp::LocalMatch { span, name, on_exp, motive, body } = self; + Ok(ust::Exp::Match { + info: Some(*span), + ctx: (), + name: ctx.unique_label(name.to_owned(), span)?, + on_exp: on_exp.lower(ctx)?, + motive: motive.lower(ctx)?, + ret_typ: (), + body: body.lower(ctx)?, + }) + } +} + +impl Lower for cst::exp::LocalComatch { + type Target = ust::Exp; + + fn lower(&self, ctx: &mut Ctx) -> Result { + let cst::exp::LocalComatch { span, name, is_lambda_sugar, body } = self; + Ok(ust::Exp::Comatch { + info: Some(*span), + ctx: (), + name: ctx.unique_label(name.to_owned(), span)?, + is_lambda_sugar: *is_lambda_sugar, + body: body.lower(ctx)?, + }) + } +} + +impl Lower for cst::exp::Hole { + type Target = ust::Exp; + + fn lower(&self, _ctx: &mut Ctx) -> Result { + let cst::exp::Hole { span } = self; + Ok(ust::Exp::Hole { info: Some(*span) }) + } +} + +impl Lower for cst::exp::NatLit { + type Target = ust::Exp; + + fn lower(&self, _ctx: &mut Ctx) -> Result { + let cst::exp::NatLit { span, val } = self; + let mut out = ust::Exp::Ctor { + info: Some(*span), + name: "Z".to_owned(), + args: ust::Args { args: vec![] }, + }; + + let mut i = BigUint::from(0usize); + + while &i != val { + i += 1usize; + out = ust::Exp::Ctor { info: Some(*span), - name: "Fun".to_owned(), - args: ust::Args { args: vec![from.lower(ctx)?, to.lower(ctx)?] }, - }), - cst::exp::Exp::Lam(cst::exp::Lam { span, var, body }) => { - let comatch = cst::exp::Exp::LocalComatch(cst::exp::LocalComatch { + name: "S".to_owned(), + args: ust::Args { args: vec![Rc::new(out)] }, + }; + } + + Ok(out) + } +} + +impl Lower for cst::exp::Fun { + type Target = ust::Exp; + fn lower(&self, ctx: &mut Ctx) -> Result { + let cst::exp::Fun { span, from, to } = self; + Ok(ust::Exp::TypCtor { + info: Some(*span), + name: "Fun".to_owned(), + args: ust::Args { args: vec![from.lower(ctx)?, to.lower(ctx)?] }, + }) + } +} + +impl Lower for cst::exp::Lam { + type Target = ust::Exp; + + fn lower(&self, ctx: &mut Ctx) -> Result { + let cst::exp::Lam { span, var, body } = self; + let comatch = cst::exp::Exp::LocalComatch(cst::exp::LocalComatch { + span: *span, + name: None, + is_lambda_sugar: true, + body: cst::exp::Match { + span: *span, + cases: vec![cst::exp::Case { span: *span, - name: None, - is_lambda_sugar: true, - body: cst::exp::Match { - span: *span, - cases: vec![cst::exp::Case { - span: *span, - name: "ap".to_owned(), - args: cst::exp::TelescopeInst(vec![ - cst::exp::ParamInst { - span: Default::default(), - name: BindingSite::Wildcard, - }, - cst::exp::ParamInst { - span: Default::default(), - name: BindingSite::Wildcard, - }, - var.clone(), - ]), - body: Some(body.clone()), - }], - omit_absurd: false, - }, - }); - comatch.lower(ctx) - } + name: "ap".to_owned(), + args: cst::exp::TelescopeInst(vec![ + cst::exp::ParamInst { + span: Default::default(), + name: BindingSite::Wildcard, + }, + cst::exp::ParamInst { + span: Default::default(), + name: BindingSite::Wildcard, + }, + var.clone(), + ]), + body: Some(body.clone()), + }], + omit_absurd: false, + }, + }); + comatch.lower(ctx) + } +} + +impl Lower for cst::exp::Exp { + type Target = ust::Exp; + + fn lower(&self, ctx: &mut Ctx) -> Result { + match self { + cst::exp::Exp::Call(e) => e.lower(ctx), + cst::exp::Exp::DotCall(e) => e.lower(ctx), + cst::exp::Exp::Anno(e) => e.lower(ctx), + cst::exp::Exp::Type(e) => e.lower(ctx), + cst::exp::Exp::LocalMatch(e) => e.lower(ctx), + cst::exp::Exp::LocalComatch(e) => e.lower(ctx), + cst::exp::Exp::Hole(e) => e.lower(ctx), + cst::exp::Exp::NatLit(e) => e.lower(ctx), + cst::exp::Exp::Fun(e) => e.lower(ctx), + cst::exp::Exp::Lam(e) => e.lower(ctx), } } } From cb548cf3911a17f688fd5513821109cf3b3bc21f Mon Sep 17 00:00:00 2001 From: David Binder Date: Tue, 16 Apr 2024 15:25:48 +0200 Subject: [PATCH 5/6] Remove ParamInst and Telescope from CST --- lang/lowering/src/ctx.rs | 12 ++++---- lang/lowering/src/imp.rs | 44 +++++++++++++++-------------- lang/parser/src/cst/decls.rs | 2 +- lang/parser/src/cst/exp.rs | 27 +++++------------- lang/parser/src/grammar/cst.lalrpop | 18 ++++++------ 5 files changed, 45 insertions(+), 58 deletions(-) diff --git a/lang/lowering/src/ctx.rs b/lang/lowering/src/ctx.rs index ce847dc683..793960a182 100644 --- a/lang/lowering/src/ctx.rs +++ b/lang/lowering/src/ctx.rs @@ -174,17 +174,17 @@ impl ContextElem for Ident { impl ContextElem for &cst::decls::Param { fn as_element(&self) -> ::ElemIn { match &self.name { - BindingSite::Var { name } => name.to_owned(), - BindingSite::Wildcard => "_".to_owned(), + BindingSite::Var { name, .. } => name.to_owned(), + BindingSite::Wildcard { .. } => "_".to_owned(), } } } -impl ContextElem for &cst::exp::ParamInst { +impl ContextElem for &cst::exp::BindingSite { fn as_element(&self) -> ::ElemIn { - match &self.name { - BindingSite::Var { name } => name.to_owned(), - BindingSite::Wildcard => "_".to_owned(), + match self { + BindingSite::Var { name, .. } => name.to_owned(), + BindingSite::Wildcard { .. } => "_".to_owned(), } } } diff --git a/lang/lowering/src/imp.rs b/lang/lowering/src/imp.rs index acff084b15..64bcae0833 100644 --- a/lang/lowering/src/imp.rs +++ b/lang/lowering/src/imp.rs @@ -609,17 +609,11 @@ impl Lower for cst::exp::Lam { cases: vec![cst::exp::Case { span: *span, name: "ap".to_owned(), - args: cst::exp::TelescopeInst(vec![ - cst::exp::ParamInst { - span: Default::default(), - name: BindingSite::Wildcard, - }, - cst::exp::ParamInst { - span: Default::default(), - name: BindingSite::Wildcard, - }, + args: vec![ + cst::exp::BindingSite::Wildcard { span: Default::default() }, + cst::exp::BindingSite::Wildcard { span: Default::default() }, var.clone(), - ]), + ], body: Some(body.clone()), }], omit_absurd: false, @@ -650,10 +644,18 @@ impl Lower for cst::exp::Exp { fn bs_to_name(bs: &cst::exp::BindingSite) -> Ident { match bs { - BindingSite::Var { name } => name.clone(), - BindingSite::Wildcard => "_".to_owned(), + BindingSite::Var { name, .. } => name.clone(), + BindingSite::Wildcard { .. } => "_".to_owned(), } } + +fn bs_to_span(bs: &cst::exp::BindingSite) -> Span { + match bs { + BindingSite::Var { span, .. } => *span, + BindingSite::Wildcard { span } => *span, + } +} + impl Lower for cst::exp::Motive { type Target = ust::Motive; @@ -663,8 +665,8 @@ impl Lower for cst::exp::Motive { Ok(ust::Motive { info: Some(*span), param: ust::ParamInst { - info: Some(param.span), - name: bs_to_name(¶m.name), + info: Some(bs_to_span(param)), + name: bs_to_name(param), typ: (), }, ret_typ: ctx.bind_single(param, |ctx| ret_typ.lower(ctx))?, @@ -748,8 +750,8 @@ where let cst::decls::Param { name, names: _, typ } = param; // The `names` field has been removed by `desugar_telescope`. let typ_out = typ.lower(ctx)?; let name = match name { - BindingSite::Var { name } => name.clone(), - BindingSite::Wildcard => "_".to_owned(), + BindingSite::Var { name, .. } => name.clone(), + BindingSite::Wildcard { .. } => "_".to_owned(), }; let param_out = ust::Param { name, typ: typ_out }; params_out.push(param_out); @@ -760,18 +762,18 @@ where } fn lower_telescope_inst Result>( - tel_inst: &cst::exp::TelescopeInst, + tel_inst: &[cst::exp::BindingSite], ctx: &mut Ctx, f: F, ) -> Result { ctx.bind_fold( - tel_inst.0.iter(), + tel_inst.iter(), Ok(vec![]), |_ctx, params_out, param| { let mut params_out = params_out?; - let cst::exp::ParamInst { span, name } = param; - let param_out = - ust::ParamInst { info: Some(*span), name: bs_to_name(name).clone(), typ: () }; + let span = bs_to_span(param); + let name = bs_to_name(param); + let param_out = ust::ParamInst { info: Some(span), name, typ: () }; params_out.push(param_out); Ok(params_out) }, diff --git a/lang/parser/src/cst/decls.rs b/lang/parser/src/cst/decls.rs index 4d36adb8eb..29b1ce8290 100644 --- a/lang/parser/src/cst/decls.rs +++ b/lang/parser/src/cst/decls.rs @@ -128,7 +128,7 @@ pub struct SelfParam { pub struct TypApp { pub span: Span, pub name: exp::Ident, - pub args: exp::Args, + pub args: Vec>, } impl TypApp { diff --git a/lang/parser/src/cst/exp.rs b/lang/parser/src/cst/exp.rs index f9edd0b6c0..8a4ce6a33a 100644 --- a/lang/parser/src/cst/exp.rs +++ b/lang/parser/src/cst/exp.rs @@ -8,8 +8,8 @@ pub type Ident = String; #[derive(Debug, Clone)] pub enum BindingSite { - Var { name: Ident }, - Wildcard, + Var { span: Span, name: Ident }, + Wildcard { span: Span }, } #[derive(Debug, Clone)] @@ -23,7 +23,7 @@ pub struct Match { pub struct Case { pub span: Span, pub name: Ident, - pub args: TelescopeInst, + pub args: Vec, /// Body being `None` represents an absurd pattern pub body: Option>, } @@ -46,7 +46,7 @@ pub enum Exp { pub struct Call { pub span: Span, pub name: Ident, - pub args: Args, + pub args: Vec>, } #[derive(Debug, Clone)] @@ -54,7 +54,7 @@ pub struct DotCall { pub span: Span, pub exp: Rc, pub name: Ident, - pub args: Args, + pub args: Vec>, } #[derive(Debug, Clone)] @@ -107,26 +107,13 @@ pub struct Fun { #[derive(Debug, Clone)] pub struct Lam { pub span: Span, - pub var: ParamInst, + pub var: BindingSite, pub body: Rc, } #[derive(Debug, Clone)] pub struct Motive { pub span: Span, - pub param: ParamInst, + pub param: BindingSite, pub ret_typ: Rc, } - -pub type Args = Vec>; - -/// Instantiation of a previously declared parameter -#[derive(Debug, Clone)] -pub struct ParamInst { - pub span: Span, - pub name: BindingSite, -} - -/// Instantiation of a previously declared telescope -#[derive(Debug, Clone)] -pub struct TelescopeInst(pub Vec); diff --git a/lang/parser/src/grammar/cst.lalrpop b/lang/parser/src/grammar/cst.lalrpop index b9b6413381..e2da5f9a43 100644 --- a/lang/parser/src/grammar/cst.lalrpop +++ b/lang/parser/src/grammar/cst.lalrpop @@ -63,16 +63,14 @@ OptBracketedArgs: Vec = >?> => args.unwra Param: Param = ":" => Param { name, names, typ } ; -ParamInst: ParamInst = => ParamInst { span: span(l, r), name }; - Params: Vec = ParenthesizedArgs; OptParams: Vec = OptParenthesizedArgs; Telescope: Telescope = => Telescope(params); OptTelescope: Telescope = => Telescope(params); -TelescopeInst: TelescopeInst = >> => TelescopeInst(params); -OptTelescopeInst: TelescopeInst = >?> => TelescopeInst(params.unwrap_or_default()); + +OptTelescopeInst: Vec = >?> => params.unwrap_or_default(); Args: Vec> = ParenthesizedArgs; OptArgs: Vec> = OptParenthesizedArgs; @@ -154,7 +152,7 @@ pub Destructee: Destructee = { } pub Scrutinee: Scrutinee = { - "(" ":" ")" => Scrutinee { span: span(l, r), name: match name { BindingSite::Wildcard => None, BindingSite::Var { name } => Some(name) }, typ }, + "(" ":" ")" => Scrutinee { span: span(l, r), name: match name { BindingSite::Wildcard{..} => None, BindingSite::Var { name,.. } => Some(name) }, typ }, => Scrutinee { span: span(l, r), name: None, typ }, } @@ -211,7 +209,7 @@ Anno: Anno = ":" => Fun: Fun = "->" => Fun { span: span(l, r), from, to }; -Lam: Lam = "\\" "." => +Lam: Lam = "\\" "." => Lam { span: span(l, r), var, body }; DotCall: DotCall = "." => @@ -224,7 +222,7 @@ CallWithArgs: Call = => Call { span: span(l, r), name, args }; CallWithoutArgs: Call = => - Call { span: span(l, r), name, args: Args::new() }; + Call { span: span(l, r), name, args: vec![] }; LocalComatch: LocalComatch = "comatch" "{" "}" => LocalComatch { span: span(l, r), name, is_lambda_sugar: false, body }; @@ -243,14 +241,14 @@ NatLit: NatLit = => // Motive: Motive = { - "as" "=>" => Motive { span: span(l, r), param, ret_typ }, + "as" "=>" => Motive { span: span(l, r), param, ret_typ }, } // Names BindingSite: BindingSite = { - => BindingSite::Var { name: i }, - "_" => BindingSite::Wildcard, + => BindingSite::Var { span: span(l,r), name: i }, + "_" => BindingSite::Wildcard { span: span(l,r) }, } Ident: String = { From 9863cd256f2c833f448feca2782095d537b9e64f Mon Sep 17 00:00:00 2001 From: David Binder Date: Wed, 17 Apr 2024 13:14:35 +0200 Subject: [PATCH 6/6] Apply suggestions from code review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tim Süberkrüb --- lang/parser/src/cst/decls.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lang/parser/src/cst/decls.rs b/lang/parser/src/cst/decls.rs index 29b1ce8290..073382fdb9 100644 --- a/lang/parser/src/cst/decls.rs +++ b/lang/parser/src/cst/decls.rs @@ -152,11 +152,11 @@ impl From for SelfParam { /// A `Param` can either be a single parameter, like `x : T`, or a list of parameters, like `x, y, z : T`. #[derive(Debug, Clone)] pub struct Param { - /// The obligatory parameter. + /// The obligatory parameter name. pub name: exp::BindingSite, - /// A possible list of additional parameters. + /// A possible list of additional parameter names. pub names: Vec, - /// The type of the parameter. + /// The type of the parameter(s). pub typ: Rc, }