diff --git a/crates/kind-checker/src/compiler/mod.rs b/crates/kind-checker/src/compiler/mod.rs index 54128cd3..af7ab379 100644 --- a/crates/kind-checker/src/compiler/mod.rs +++ b/crates/kind-checker/src/compiler/mod.rs @@ -125,6 +125,8 @@ fn desugar_str(input: &str, range: Range) -> Box { }) } +// Codegen + fn codegen_str(input: &str) -> Box { input.chars().rfold( Box::new(Term::Ctr { diff --git a/crates/kind-checker/src/compiler/tags.rs b/crates/kind-checker/src/compiler/tags.rs index 0a8b2fa9..0689aaed 100644 --- a/crates/kind-checker/src/compiler/tags.rs +++ b/crates/kind-checker/src/compiler/tags.rs @@ -1,5 +1,6 @@ ///! This module describes tags for internal use /// during compilation + use core::fmt; use kind_tree::Operator; diff --git a/crates/kind-cli/Cargo.toml b/crates/kind-cli/Cargo.toml index ef0cecfe..56d6e0f7 100644 --- a/crates/kind-cli/Cargo.toml +++ b/crates/kind-cli/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "kind-cli" -version = "0.3.1" +version = "0.3.2" edition = "2021" description = "A pure functional functional language that uses the HVM." repository = "https://github.com/Kindelia/Kind2" diff --git a/crates/kind-derive/src/errors.rs b/crates/kind-derive/src/errors.rs index 48ede945..b2608219 100644 --- a/crates/kind-derive/src/errors.rs +++ b/crates/kind-derive/src/errors.rs @@ -3,12 +3,16 @@ use kind_span::Range; pub(crate) enum DeriveError { CannotUseNamedVariable(Range), + CannotUseAll(Range), + InvalidReturnType(Range), } impl Diagnostic for DeriveError { fn get_syntax_ctx(&self) -> Option { match self { DeriveError::CannotUseNamedVariable(range) => Some(range.ctx), + DeriveError::CannotUseAll(range) => Some(range.ctx), + DeriveError::InvalidReturnType(range) => Some(range.ctx), } } @@ -28,6 +32,34 @@ impl Diagnostic for DeriveError { main: true, }], }, + DeriveError::CannotUseAll(range) => DiagnosticFrame { + code: 103, + severity: Severity::Error, + title: "Data constructors cannot return function types.".to_string(), + subtitles: vec![], + hints: vec!["Change all of the function types sequence for explicit arguments like 'cons : x -> T' to 'cons (name: x) : T'".to_string()], + positions: vec![Marker { + position: *range, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }], + }, + DeriveError::InvalidReturnType(range) => DiagnosticFrame { + code: 103, + severity: Severity::Error, + title: "Data constructors cannot return this type".to_string(), + subtitles: vec![], + hints: vec!["Replace it with the type that is being declarated at the current block".to_string()], + positions: vec![Marker { + position: *range, + color: Color::Fst, + text: "Here!".to_string(), + no_code: false, + main: true, + }], + } } } } diff --git a/crates/kind-derive/src/getters.rs b/crates/kind-derive/src/getters.rs index edf7aeff..1141f4c8 100644 --- a/crates/kind-derive/src/getters.rs +++ b/crates/kind-derive/src/getters.rs @@ -7,6 +7,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent}; use kind_tree::concrete::*; use kind_tree::concrete::{self}; use kind_tree::symbol::{Ident, QualifiedIdent}; +use kind_tree::telescope::Telescope; pub fn derive_getters(range: Range, rec: &RecordDecl) -> Vec { let mk_var = |name: Ident| -> Box { diff --git a/crates/kind-derive/src/lib.rs b/crates/kind-derive/src/lib.rs index dc7f9729..1fae1a5b 100644 --- a/crates/kind-derive/src/lib.rs +++ b/crates/kind-derive/src/lib.rs @@ -1,3 +1,5 @@ +#![feature(let_chains)] + //! Utility to derive functions from their definitions. pub mod errors; diff --git a/crates/kind-derive/src/matching.rs b/crates/kind-derive/src/matching.rs index 84a86274..f6e95df1 100644 --- a/crates/kind-derive/src/matching.rs +++ b/crates/kind-derive/src/matching.rs @@ -6,116 +6,75 @@ use kind_report::data::Diagnostic; use kind_span::Range; use kind_tree::concrete::expr::Expr; -use kind_tree::concrete::pat::{Pat, PatIdent}; +use kind_tree::concrete::pat::{Pat, PatIdent, PatKind}; use kind_tree::concrete::*; use kind_tree::concrete::{self}; -use kind_tree::symbol::{Ident, QualifiedIdent}; +use kind_tree::symbol::Ident; +use kind_tree::telescope::Telescope; use crate::errors::DeriveError; use crate::subst::substitute_in_expr; +type Errs = Vec>; + +pub fn to_app_binding(errs: &mut Errs, binding: &Binding) -> AppBinding { + match binding { + Binding::Positional(expr) => AppBinding { + erased: false, + data: expr.clone(), + }, + Binding::Named(_, name, expr) => { + errs.push(Box::new(DeriveError::CannotUseNamedVariable(name.range))); + AppBinding::explicit(expr.clone()) + } + } +} + /// Derives an eliminator from a sum type declaration. -pub fn derive_match( - range: Range, - sum: &SumTypeDecl, -) -> (concrete::Entry, Vec>) { - let mut errs: Vec> = Vec::new(); +pub fn derive_match(range: Range, sum: &SumTypeDecl) -> (concrete::Entry, Errs) { + let mut errs: Errs = Vec::new(); - let mk_var = |name: Ident| -> Box { - Box::new(Expr { - data: ExprKind::Var { name }, - range, - }) - }; + let new_entry_name = sum.name.add_segment("match"); - let mk_cons = |name: QualifiedIdent, args: Vec| -> Box { - Box::new(Expr { - data: ExprKind::Constr { name, args }, - range, - }) - }; + let all_arguments = sum.parameters.extend(&sum.indices); - let mk_app = |fun: Box, args: Vec, range: Range| -> Box { - Box::new(Expr { - data: ExprKind::App { fun, args }, - range, - }) - }; + // Parameters and indices - let mk_pi = |name: Ident, typ: Box, body: Box| -> Box { - Box::new(Expr { - data: ExprKind::All { - param: Some(name), - typ, - body, - erased: false, - }, - range, - }) - }; + let mut types = all_arguments.map(|x| x.to_implicit()); - let mk_typ = || -> Box { - Box::new(Expr { - data: ExprKind::Lit { lit: Literal::Type }, - range, - }) - }; - - let name = sum.name.add_segment("match"); - - let mut types = Telescope::default(); - - for arg in sum.parameters.iter() { - types.push(arg.to_implicit()) - } - - for arg in sum.indices.iter() { - types.push(arg.to_implicit()) - } - - // The type - - let all_args = sum.parameters.extend(&sum.indices); - let res_motive_ty = mk_cons( - sum.name.clone(), - all_args - .iter() - .cloned() - .map(|x| Binding::Positional(mk_var(x.name))) - .collect(), - ); - - let indice_names: Vec = sum - .indices + let all_bindings = all_arguments .iter() - .map(|x| AppBinding::explicit(mk_var(x.name.clone()))) + .cloned() + .map(|x| Binding::Positional(Expr::var(x.name))) .collect(); - // Sccrutinzies + let current_return_type = Expr::cons(sum.name.clone(), all_bindings, range); types.push(Argument { hidden: false, erased: false, name: Ident::generate("scrutinizer"), - typ: Some(res_motive_ty.clone()), + typ: Some(current_return_type.clone()), range, }); - // Motive with indices + // Motive let motive_ident = Ident::new_static("motive", range); - let motive_type = sum.indices.iter().rfold( - mk_pi(Ident::new_static("val_", range), res_motive_ty, mk_typ()), - |out, arg| { - mk_pi( - arg.name.clone(), - arg.typ.clone().unwrap_or_else(mk_typ), - out, - ) - }, + let motive_return = Expr::all( + Ident::new_static("val_", range), + current_return_type, + Expr::typ(range), + false, + range, ); + let motive_type = sum.indices.iter().rfold(motive_return, |out, arg| { + let typ = arg.typ.clone().unwrap_or_else(|| Expr::typ(range)); + Expr::all(arg.name.clone(), typ, out, false, range) + }); + types.push(Argument { hidden: false, erased: true, @@ -124,39 +83,47 @@ pub fn derive_match( range, }); + // Constructors + + let indice_names: Vec = sum + .indices + .iter() + .map(|x| AppBinding::explicit(Expr::var(x.name.clone()))) + .collect(); + + // Parameter binding telescope + let params = sum .parameters - .map(|x| Binding::Positional(mk_var(x.name.clone()))); + .map(|x| Binding::Positional(Expr::var(x.name.clone()))); + let indices = sum .indices - .map(|x| Binding::Positional(mk_var(x.name.clone()))); + .map(|x| Binding::Positional(Expr::var(x.name.clone()))); + + // Types - // Constructors type for cons in &sum.constructors { - let vars: Vec = cons + // Constructor arguments bindings + let vars = cons .args - .iter() - .map(|x| Binding::Positional(mk_var(x.name.clone()))) - .collect(); + .map(|x| Binding::Positional(Expr::var(x.name.clone()))); - let cons_inst = mk_cons( - sum.name.add_segment(cons.name.to_str()), - [ - params.as_slice(), - if cons.typ.is_none() { - indices.as_slice() - } else { - &[] - }, - vars.as_slice(), - ] - .concat(), - ); + let constructor_name = sum.name.add_segment(cons.name.to_str()); - let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) { - Some(ExprKind::Constr { name: _, args }) => { + let default = &Telescope::default(); + let indices = &indices; + + let partial_indices = if cons.typ.is_none() { indices } else { default }; + + let args = params.extend(partial_indices).extend(&vars); + + let instantation_of_the_cons = Expr::cons(constructor_name.clone(), args.to_vec(), range); + + let mut cons_indices = if let Some(res) = &cons.typ { + if let ExprKind::Constr { args, .. } = &res.data { let mut new_args = Vec::with_capacity(args.len()); - for arg in &args[sum.parameters.len()..].to_vec() { + for arg in &args[sum.parameters.len()..] { new_args.push(match arg { Binding::Positional(expr) => AppBinding::explicit(expr.clone()), Binding::Named(range, _, expr) => { @@ -166,13 +133,20 @@ pub fn derive_match( }); } new_args + } else if let ExprKind::All { .. } = &res.data { + errs.push(Box::new(DeriveError::CannotUseAll(res.range))); + [indice_names.as_slice()].concat() + } else { + errs.push(Box::new(DeriveError::InvalidReturnType(res.range))); + [indice_names.as_slice()].concat() } - _ => [indice_names.as_slice()].concat(), + } else { + [indice_names.as_slice()].concat() }; - indices_of_cons.push(AppBinding::explicit(cons_inst)); + cons_indices.push(AppBinding::explicit(instantation_of_the_cons)); - let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range); + let cons_tipo = Expr::app(Expr::var(motive_ident.clone()), cons_indices, range); let args = if cons.typ.is_some() { cons.args.clone() @@ -181,133 +155,109 @@ pub fn derive_match( }; let cons_type = args.iter().rfold(cons_tipo, |out, arg| { - mk_pi( + Expr::all( arg.name.clone(), - arg.typ.clone().unwrap_or_else(mk_typ), + arg.typ.clone().unwrap_or_else(|| Expr::typ(range)), out, + arg.erased, + range, ) }); - types.push(Argument { - hidden: false, - erased: false, - name: Ident::new_static(&format!("{}_", cons.name), range), - typ: Some(cons_type), + types.push(Argument::new_explicit( + Ident::new_static(&format!("{}_", cons.name), range), + cons_type, range, - }); + )); } - if !errs.is_empty() { - let entry = Entry { - name, + let make_incomplete_entry = || { + let typ = Box::new(Expr { + data: ExprKind::Hole, + range, + }); + + Entry { + name: new_entry_name.clone(), docs: Vec::new(), - args: types, - typ: Box::new(Expr { - data: ExprKind::Hole, - range, - }), + args: types.clone(), + typ, rules: vec![], range, attrs: Vec::new(), generated_by: Some(sum.name.to_string()), - }; - return (entry, errs); + } + }; + + if !errs.is_empty() { + return (make_incomplete_entry(), errs); } - let mut res: Vec = [indice_names.as_slice()].concat(); - res.push(AppBinding::explicit(mk_var(Ident::generate("scrutinizer")))); - let ret_ty = mk_app(mk_var(motive_ident.clone()), res, range); + let scrutinizer_ident = Expr::var(Ident::generate("scrutinizer")); + + let mut return_args = indice_names.clone(); + return_args.push(AppBinding::explicit(scrutinizer_ident)); + + let return_type = Expr::app(Expr::var(motive_ident.clone()), return_args, range); + + // Rules let mut rules = Vec::new(); for cons in &sum.constructors { - let cons_ident = sum.name.add_segment(cons.name.to_str()); - let mut pats: Vec> = Vec::new(); + let constructor_name = sum.name.add_segment(cons.name.to_str()); - let irrelev: Vec; - let spine_params: Vec; - let spine: Vec; + let params = sum.parameters.map(|x| x.name.add_underscore()); - let mut args_indices: Vec; + let mut indices_and_args: Telescope; - match &cons.typ { - Some(expr) => match &**expr { - Expr { - data: ExprKind::Constr { args, .. }, - .. - } => { - irrelev = cons.args.map(|x| x.erased).to_vec(); - spine_params = sum - .parameters + let args = if let Some(res) = &cons.typ { + if let ExprKind::Constr { args, .. } = &res.data { + indices_and_args = + Telescope::new(args.clone()).map(|x| to_app_binding(&mut errs, x)); + + let mut indices = indices_and_args.to_vec()[sum.parameters.len()..].to_vec(); + + let renames = FxHashMap::from_iter( + sum.parameters .extend(&cons.args) - .map(|x| x.name.with_name(|f| format!("{}_", f))) - .to_vec(); - spine = cons - .args - .map(|x| x.name.with_name(|f| format!("{}_", f))) - .to_vec(); - args_indices = args + .map(|x| (x.name.to_string(), format!("{}_", x.name))) .iter() - .map(|x| match x { - Binding::Positional(expr) => AppBinding { - erased: false, - data: expr.clone(), - }, - Binding::Named(_, _, _) => unreachable!(), - }) - .collect::>(); - args_indices = { - let mut indices = args_indices[sum.parameters.len()..].to_vec(); + .cloned(), + ); - let renames = FxHashMap::from_iter( - sum.parameters - .extend(&cons.args) - .map(|x| (x.name.to_string(), format!("{}_", x.name))) - .iter() - .cloned(), - ); - - for indice in &mut indices { - substitute_in_expr(&mut indice.data, &renames) - } - indices - }; + for indice in &mut indices { + substitute_in_expr(&mut indice.data, &renames) } - _ => unreachable!(), - }, - None => { - irrelev = sum.indices.extend(&cons.args).map(|x| x.erased).to_vec(); - spine_params = sum - .parameters - .extend(&sum.indices) - .extend(&cons.args) - .map(|x| x.name.with_name(|f| format!("{}_", f))) - .to_vec(); - spine = sum - .indices - .extend(&cons.args) - .map(|x| x.name.with_name(|f| format!("{}_", f))) - .to_vec(); - args_indices = sum - .indices - .clone() - .map(|x| AppBinding { - data: mk_var(x.name.clone()), - erased: false, - }) - .to_vec(); + + indices_and_args = Telescope::new(indices); + + cons.args.clone() + } else { + unreachable!( + "Internal Error: I guess you're using something that is not a constructor!" + ) } - } + } else { + indices_and_args = sum.indices.map(|x| AppBinding::from_ident(x.name.clone())); + sum.indices.extend(&cons.args) + }; + + let irrelevances = args.map(|x| x.erased).to_vec(); + let spine = args.map(|x| x.name.add_underscore()); + + let params_and_spine = params.extend(&spine); + let mut pats = Vec::new(); pats.push(Box::new(Pat { - data: concrete::pat::PatKind::App( - cons_ident.clone(), - spine_params + data: PatKind::App( + constructor_name.clone(), + params_and_spine .iter() .cloned() .map(|x| { Box::new(Pat { - data: concrete::pat::PatKind::Var(PatIdent(x)), + data: PatKind::Var(PatIdent(x)), range, }) }) @@ -317,55 +267,52 @@ pub fn derive_match( })); pats.push(Box::new(Pat { - data: concrete::pat::PatKind::Var(PatIdent(Ident::generate("motive"))), + data: PatKind::Var(PatIdent(Ident::generate("motive"))), range, })); - for cons2 in &sum.constructors { + for cons in &sum.constructors { pats.push(Box::new(Pat { - data: concrete::pat::PatKind::Var(PatIdent(cons2.name.clone())), + data: PatKind::Var(PatIdent(cons.name.clone())), range, })); } - let mut args = args_indices.clone(); + let mut args = indices_and_args.clone(); - args.push(AppBinding { - data: Box::new(Expr { - data: ExprKind::Constr { - name: cons_ident.clone(), - args: spine_params - .iter() - .cloned() - .map(|x| Binding::Positional(mk_var(x))) - .collect(), - }, - range, - }), - erased: false, - }); + args.push(AppBinding::explicit(Expr::cons( + constructor_name.clone(), + params_and_spine + .map(|x| Binding::Positional(Expr::var(x.clone()))) + .to_vec(), + range, + ))); + + let body_typ = Expr::app(Expr::var(motive_ident.clone()), args.to_vec(), range); + + let body_val = Expr::app( + Expr::var(cons.name.clone()), + spine + .iter() + .zip(irrelevances) + .map(|(arg, erased)| AppBinding { + data: Expr::var(arg.clone()), + erased, + }) + .collect(), + cons.name.range, + ); let body = Box::new(Expr { data: ExprKind::Ann { - val: mk_app( - mk_var(cons.name.clone()), - spine - .iter() - .zip(irrelev) - .map(|(arg, erased)| AppBinding { - data: mk_var(arg.clone()), - erased, - }) - .collect(), - cons.name.range, - ), - typ: mk_app(mk_var(motive_ident.clone()), args, range), + val: body_val, + typ: body_typ, }, range, }); let rule = Box::new(Rule { - name: name.clone(), + name: new_entry_name.clone(), pats, body, range: cons.name.range, @@ -373,13 +320,12 @@ pub fn derive_match( rules.push(rule) } - // Rules let entry = Entry { - name, + name: new_entry_name, docs: Vec::new(), args: types, - typ: ret_ty, + typ: return_type, rules, range, attrs: Vec::new(), diff --git a/crates/kind-derive/src/open.rs b/crates/kind-derive/src/open.rs index 6190625e..5ef567f8 100644 --- a/crates/kind-derive/src/open.rs +++ b/crates/kind-derive/src/open.rs @@ -7,6 +7,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent}; use kind_tree::concrete::*; use kind_tree::concrete::{self}; use kind_tree::symbol::{Ident, QualifiedIdent}; +use kind_tree::telescope::Telescope; pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry { let mk_var = |name: Ident| -> Box { diff --git a/crates/kind-derive/src/setters.rs b/crates/kind-derive/src/setters.rs index f3d2fcda..967a914b 100644 --- a/crates/kind-derive/src/setters.rs +++ b/crates/kind-derive/src/setters.rs @@ -7,6 +7,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent}; use kind_tree::concrete::*; use kind_tree::concrete::{self}; use kind_tree::symbol::{Ident, QualifiedIdent}; +use kind_tree::telescope::Telescope; pub fn derive_setters(range: Range, rec: &RecordDecl) -> Vec { let mk_var = |name: Ident| -> Box { diff --git a/crates/kind-parser/src/top_level/mod.rs b/crates/kind-parser/src/top_level/mod.rs index 8e7ae367..3edce95a 100644 --- a/crates/kind-parser/src/top_level/mod.rs +++ b/crates/kind-parser/src/top_level/mod.rs @@ -4,6 +4,7 @@ use kind_tree::concrete::pat::{Pat, PatIdent, PatKind}; use kind_tree::concrete::*; use kind_tree::symbol::QualifiedIdent; +use kind_tree::telescope::Telescope; use crate::errors::SyntaxDiagnostic; use crate::lexer::tokens::Token; diff --git a/crates/kind-parser/src/top_level/type_decl.rs b/crates/kind-parser/src/top_level/type_decl.rs index 7fcc1641..c167ba27 100644 --- a/crates/kind-parser/src/top_level/type_decl.rs +++ b/crates/kind-parser/src/top_level/type_decl.rs @@ -1,5 +1,6 @@ -use kind_tree::concrete::{Attribute, Constructor, RecordDecl, SumTypeDecl, Telescope}; +use kind_tree::concrete::{Attribute, Constructor, RecordDecl, SumTypeDecl}; use kind_tree::symbol::Ident; +use kind_tree::telescope::Telescope; use crate::errors::SyntaxDiagnostic; use crate::lexer::tokens::Token; diff --git a/crates/kind-pass/src/desugar/top_level.rs b/crates/kind-pass/src/desugar/top_level.rs index 5a2c003f..4181079f 100644 --- a/crates/kind-pass/src/desugar/top_level.rs +++ b/crates/kind-pass/src/desugar/top_level.rs @@ -1,7 +1,8 @@ use kind_span::Range; -use kind_tree::concrete::{self, Telescope}; +use kind_tree::concrete::{self}; use kind_tree::desugared::{self, ExprKind}; use kind_tree::symbol::QualifiedIdent; +use kind_tree::telescope::Telescope; use crate::errors::{PassError, Sugar}; diff --git a/crates/kind-pass/src/erasure/mod.rs b/crates/kind-pass/src/erasure/mod.rs index 9c6093bd..ce4e6c00 100644 --- a/crates/kind-pass/src/erasure/mod.rs +++ b/crates/kind-pass/src/erasure/mod.rs @@ -407,7 +407,11 @@ impl<'a> ErasureState<'a> { self.ctx = backup; - untyped::Expr::lambda(expr.range, param.clone(), body, *erased) + if *erased { + body + } else { + untyped::Expr::lambda(expr.range, param.clone(), body, *erased) + } } Let { name, val, next } => { let backup = self.ctx.clone(); @@ -497,9 +501,21 @@ impl<'a> ErasureState<'a> { App { fun, args } => { let fun = self.erase_expr(ambient, edge, fun); let mut spine = Vec::new(); + for arg in args { - spine.push(self.erase_expr(ambient, edge, &arg.data)) + let ambient = if arg.erased { + Ambient::Irrelevant + } else { + ambient + }; + + let res = self.erase_expr(ambient, edge, &arg.data); + + if !arg.erased { + spine.push(res) + } } + untyped::Expr::app(expr.range, fun, spine) } Sub { expr, .. } => self.erase_expr(ambient, edge, expr), diff --git a/crates/kind-pass/src/expand/mod.rs b/crates/kind-pass/src/expand/mod.rs index bd617178..f17a1478 100644 --- a/crates/kind-pass/src/expand/mod.rs +++ b/crates/kind-pass/src/expand/mod.rs @@ -13,21 +13,30 @@ use kind_derive::setters::derive_setters; use kind_report::data::Diagnostic; use kind_span::Locatable; use kind_span::Range; +use kind_tree::concrete::Entry; +use kind_tree::concrete::EntryMeta; use kind_tree::concrete::Module; +use kind_tree::concrete::RecordDecl; +use kind_tree::concrete::SumTypeDecl; use kind_tree::concrete::{Attribute, TopLevel}; use crate::errors::PassError; + /// Expands sum type and record definitions to a lot of /// helper definitions like eliminators and replace qualified identifiers /// by their module names. pub mod uses; +type Derivations = FxHashMap; +type Channel = Sender>; + +/// Tags for each one of the possible derivations. #[derive(Debug, Hash, PartialEq, Eq)] pub enum Derive { Match, Open, Getters, - Setters + Setters, } impl Display for Derive { @@ -41,24 +50,12 @@ impl Display for Derive { } } -pub fn insert_or_report( - channel: Sender>, - hashmap: &mut FxHashMap, - key: Derive, - range: Range, -) { - match hashmap.get(&key) { - Some(last_range) => { - channel - .send(Box::new(PassError::DuplicatedAttributeArgument( - *last_range, - range, - ))) - .unwrap(); - } - None => { - hashmap.insert(key, range); - } +pub fn insert_or_report(channel: Channel, hashmap: &mut Derivations, key: Derive, range: Range) { + if let Some(last_range) = hashmap.get(&key) { + let err = Box::new(PassError::DuplicatedAttributeArgument(*last_range, range)); + channel.send(err).unwrap(); + } else { + hashmap.insert(key, range); } } @@ -72,12 +69,11 @@ fn string_to_derive(name: &str) -> Option { } } -pub fn expand_derive( - error_channel: Sender>, - attrs: &[Attribute], -) -> Option> { +pub fn expand_derive(error_channel: Channel, attrs: &[Attribute]) -> Option { + use kind_tree::concrete::AttributeStyle::*; + let mut failed = false; - let mut def = FxHashMap::default(); + let mut defs = FxHashMap::default(); for attr in attrs { if attr.name.to_str() != "derive" { @@ -85,36 +81,21 @@ pub fn expand_derive( } if let Some(attr) = &attr.value { - error_channel - .send(Box::new(PassError::AttributeDoesNotExpectEqual( - attr.locate(), - ))) - .unwrap(); + let err = Box::new(PassError::AttributeDoesNotExpectEqual(attr.locate())); + error_channel.send(err).unwrap(); failed = true; } - use kind_tree::concrete::AttributeStyle::*; for arg in &attr.args { match arg { - Ident(range, ident) => match string_to_derive(ident.to_str()) { - Some(key) => { - insert_or_report(error_channel.clone(), &mut def, key, *range) - } - _ => { - error_channel - .send(Box::new(PassError::InvalidAttributeArgument( - ident.locate(), - ))) - .unwrap(); - failed = true; - } - }, + Ident(range, ident) if string_to_derive(ident.to_str()).is_some() => { + // Duplicates work but it's something negligible + let key = string_to_derive(ident.to_str()).unwrap(); + insert_or_report(error_channel.clone(), &mut defs, key, *range) + } other => { - error_channel - .send(Box::new(PassError::InvalidAttributeArgument( - other.locate(), - ))) - .unwrap(); + let err = Box::new(PassError::InvalidAttributeArgument(other.locate())); + error_channel.send(err).unwrap(); failed = true; } } @@ -124,11 +105,81 @@ pub fn expand_derive( if failed { None } else { - Some(def) + Some(defs) } } -pub fn expand_module(error_channel: Sender>, module: &mut Module) -> bool { +pub fn expand_sum_type( + error_channel: Channel, + entries: &mut FxHashMap, + sum: &SumTypeDecl, + derivations: Derivations, +) -> bool { + let mut failed = false; + + for (key, val) in derivations { + match key { + Derive::Match => { + let (res, errs) = derive_match(sum.name.range, sum); + let info = res.extract_book_info(); + entries.insert(res.name.to_string(), (res, info)); + for err in errs { + error_channel.send(err).unwrap(); + failed = true; + } + } + other => { + error_channel + .send(Box::new(PassError::CannotDerive(other.to_string(), val))) + .unwrap(); + failed = true; + } + } + } + + failed +} + +pub fn expand_record_type( + error_channel: Channel, + entries: &mut FxHashMap, + rec: &RecordDecl, + derivations: Derivations, +) -> bool { + let mut failed = false; + + for (key, val) in derivations { + match key { + Derive::Open => { + let res = derive_open(rec.name.range, rec); + let info = res.extract_book_info(); + entries.insert(res.name.to_string(), (res, info)); + } + Derive::Getters => { + for res in derive_getters(rec.name.range, rec) { + let info = res.extract_book_info(); + entries.insert(res.name.to_string(), (res, info)); + } + } + Derive::Setters => { + for res in derive_setters(rec.name.range, rec) { + let info = res.extract_book_info(); + entries.insert(res.name.to_string(), (res, info)); + } + } + other => { + error_channel + .send(Box::new(PassError::CannotDerive(other.to_string(), val))) + .unwrap(); + failed = true; + } + } + } + + failed +} + +pub fn expand_module(error_channel: Channel, module: &mut Module) -> bool { let mut failed = false; let mut entries = FxHashMap::default(); @@ -137,58 +188,14 @@ pub fn expand_module(error_channel: Sender>, module: &mut Mo match entry { TopLevel::SumType(sum) => { if let Some(derive) = expand_derive(error_channel.clone(), &sum.attrs) { - for (key, val) in derive { - match key { - Derive::Match => { - let (res, errs) = derive_match(sum.name.range, sum); - let info = res.extract_book_info(); - entries.insert(res.name.to_string(), (res, info)); - for err in errs { - error_channel.send(err).unwrap(); - failed = true; - } - } - other => { - error_channel - .send(Box::new(PassError::CannotDerive(other.to_string(), val))) - .unwrap(); - failed = true; - } - } - } + failed |= expand_sum_type(error_channel.clone(), &mut entries, sum, derive) } else { failed = true; } } TopLevel::RecordType(rec) => { if let Some(derive) = expand_derive(error_channel.clone(), &rec.attrs) { - for (key, val) in derive { - match key { - Derive::Open => { - let res = derive_open(rec.name.range, rec); - let info = res.extract_book_info(); - entries.insert(res.name.to_string(), (res, info)); - } - Derive::Getters => { - for res in derive_getters(rec.name.range, rec) { - let info = res.extract_book_info(); - entries.insert(res.name.to_string(), (res, info)); - } - } - Derive::Setters => { - for res in derive_setters(rec.name.range, rec) { - let info = res.extract_book_info(); - entries.insert(res.name.to_string(), (res, info)); - } - } - other => { - error_channel - .send(Box::new(PassError::CannotDerive(other.to_string(), val))) - .unwrap(); - failed = true; - } - } - } + failed |= expand_record_type(error_channel.clone(), &mut entries, rec, derive) } else { failed = true; } diff --git a/crates/kind-tests/suite/checker/derive/Eq.golden b/crates/kind-tests/suite/checker/derive/Eq.golden new file mode 100644 index 00000000..db814b93 --- /dev/null +++ b/crates/kind-tests/suite/checker/derive/Eq.golden @@ -0,0 +1 @@ +Ok! \ No newline at end of file diff --git a/crates/kind-tests/suite/checker/derive/Eq.kind2 b/crates/kind-tests/suite/checker/derive/Eq.kind2 new file mode 100644 index 00000000..b70b09e7 --- /dev/null +++ b/crates/kind-tests/suite/checker/derive/Eq.kind2 @@ -0,0 +1,4 @@ +#derive[match] +type Equal (a: t) ~ (b: t) { + refl : Equal t a a +} \ No newline at end of file diff --git a/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden b/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden new file mode 100644 index 00000000..92cce827 --- /dev/null +++ b/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.golden @@ -0,0 +1,26 @@ + ERROR Data constructors cannot return function types. + + /--[suite/checker/issues/MatchDerivationWithAll.kind2:3:10] + | + 2 | type WithCtx (a: Type) { + 3 | new: U60 -> (WithCtx a) + | v----------------- + | \Here! + 4 | } + + Hint: Change all of the function types sequence for explicit arguments like 'cons : x -> T' to 'cons (name: x) : T' + + ERROR This is not the type that is being declared. + + /--[suite/checker/issues/MatchDerivationWithAll.kind2:2:6] + | + 2 | type WithCtx (a: Type) { + | v------ + | \This is the type that should be used instead + : + 3 | new: U60 -> (WithCtx a) + | v----------------- + | \This is not the type that is being declared + 4 | } + + diff --git a/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.kind2 b/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.kind2 new file mode 100644 index 00000000..84408b9a --- /dev/null +++ b/crates/kind-tests/suite/checker/issues/MatchDerivationWithAll.kind2 @@ -0,0 +1,4 @@ +#derive[match] +type WithCtx (a: Type) { + new: U60 -> (WithCtx a) +} \ No newline at end of file diff --git a/crates/kind-tests/suite/eval/VecMatch.golden b/crates/kind-tests/suite/eval/VecMatch.golden new file mode 100644 index 00000000..e440e5c8 --- /dev/null +++ b/crates/kind-tests/suite/eval/VecMatch.golden @@ -0,0 +1 @@ +3 \ No newline at end of file diff --git a/crates/kind-tests/suite/eval/VecMatch.kind2 b/crates/kind-tests/suite/eval/VecMatch.kind2 new file mode 100644 index 00000000..36c46ba8 --- /dev/null +++ b/crates/kind-tests/suite/eval/VecMatch.kind2 @@ -0,0 +1,20 @@ +type Nat { + succ (pred : Nat) + zero +} + +#derive[match] +type Vec (t: Type) ~ (n: Nat) { + cons (x : t) (xs : Vec t size) : Vec t (Nat.succ size) + nil : Vec t Nat.zero +} + +Vec.count (v: Vec t n) : U60 +Vec.count vec = + match Vec vec { + cons xs .. => (+ 1 (Vec.count xs)) + nil => 0 + } + +Main : U60 +Main = Vec.count (Vec.cons 10 (Vec.cons 20 (Vec.cons 30 Vec.nil))) \ No newline at end of file diff --git a/crates/kind-tree/src/concrete/expr.rs b/crates/kind-tree/src/concrete/expr.rs index c1a86519..ef259888 100644 --- a/crates/kind-tree/src/concrete/expr.rs +++ b/crates/kind-tree/src/concrete/expr.rs @@ -35,6 +35,13 @@ impl AppBinding { erased: false, } } + + pub fn from_ident(data: Ident) -> AppBinding { + AppBinding { + data: Expr::var(data), + erased: false, + } + } } /// A case binding is a field or a rename of some field @@ -46,8 +53,8 @@ pub enum CaseBinding { } /// A match case with a constructor that will match the -/// strutinizer, bindings to the names of each arguments and -/// a right-hand side value. The ignore_rest flag useful to just +/// strutinizer, bindings to the names of each arguments and +/// a right-hand side value. The ignore_rest flag useful to just /// fill all of the case bindings that are not used with a default name. #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub struct Case { @@ -203,59 +210,78 @@ pub struct Expr { pub range: Range, } -impl Display for Operator { - fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { - use Operator::*; - - match self { - Add => write!(f, "+"), - Sub => write!(f, "-"), - Mul => write!(f, "*"), - Div => write!(f, "/"), - Mod => write!(f, "%"), - And => write!(f, "&"), - Or => write!(f, "|"), - Xor => write!(f, "^"), - Shl => write!(f, "<<"), - Shr => write!(f, ">>"), - Ltn => write!(f, "<"), - Lte => write!(f, "<="), - Eql => write!(f, "=="), - Gte => write!(f, ">="), - Gtn => write!(f, ">"), - Neq => write!(f, "!="), - } - } -} - impl Expr { - pub fn traverse_pi_types(&self) -> String { - match &self.data { - ExprKind::All { + pub fn var(name: Ident) -> Box { + Box::new(Expr { + range: name.range.clone(), + data: ExprKind::Var { name }, + }) + } + + pub fn cons(name: QualifiedIdent, args: Spine, range: Range) -> Box { + Box::new(Expr { + range, + data: ExprKind::Constr { name, args }, + }) + } + + pub fn all( + param: Ident, + typ: Box, + body: Box, + erased: bool, + range: Range, + ) -> Box { + Box::new(Expr { + range, + data: ExprKind::All { + param: Some(param), + typ, + body, + erased, + }, + }) + } + + pub fn lambda( + param: Ident, + typ: Option>, + body: Box, + erased: bool, + range: Range, + ) -> Box { + Box::new(Expr { + data: ExprKind::Lambda { param, typ, body, erased, - } => { - let tilde = if *erased { "~" } else { "" }; - match param { - None => format!("{}{} -> {}", tilde, typ, body.traverse_pi_types()), - Some(binder) => format!( - "{}({} : {}) -> {}", - tilde, - binder, - typ, - body.traverse_pi_types() - ), - } - } - ExprKind::Sigma { param, fst, snd } => match param { - None => format!("{} -> {}", fst, snd.traverse_pi_types()), - Some(binder) => format!("[{} : {}] -> {}", binder, fst, snd.traverse_pi_types()), }, - _ => format!("{}", self), - } + range, + }) } + + pub fn typ(range: Range) -> Box { + Box::new(Expr { + data: ExprKind::Lit { lit: Literal::Type }, + range, + }) + } + + pub fn app(fun: Box, args: Vec, range: Range) -> Box { + Box::new(Expr { + data: ExprKind::App { fun, args }, + range, + }) + } + + pub fn hole(range: Range) -> Box { + Box::new(Expr { + data: ExprKind::Hole, + range, + }) + } + } impl Locatable for Binding { @@ -309,6 +335,36 @@ impl Locatable for Destruct { } } +impl Expr { + pub fn traverse_pi_types(&self) -> String { + match &self.data { + ExprKind::All { + param, + typ, + body, + erased, + } => { + let tilde = if *erased { "~" } else { "" }; + match param { + None => format!("{}{} -> {}", tilde, typ, body.traverse_pi_types()), + Some(binder) => format!( + "{}({} : {}) -> {}", + tilde, + binder, + typ, + body.traverse_pi_types() + ), + } + } + ExprKind::Sigma { param, fst, snd } => match param { + None => format!("{} -> {}", fst, snd.traverse_pi_types()), + Some(binder) => format!("[{} : {}] -> {}", binder, fst, snd.traverse_pi_types()), + }, + _ => format!("{}", self), + } + } +} + impl Display for Literal { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { match self { @@ -430,7 +486,7 @@ impl Display for Binding { impl Display for AppBinding { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { if self.erased { - write!(f, "-({})", self.data) + write!(f, "~({})", self.data) } else { write!(f, "{}", self.data) } @@ -471,7 +527,7 @@ impl Display for Expr { typ: None, body, erased: true, - } => write!(f, "(-({}) => {})", param, body), + } => write!(f, "(~({}) => {})", param, body), Lambda { param, typ: Some(typ), diff --git a/crates/kind-tree/src/concrete/mod.rs b/crates/kind-tree/src/concrete/mod.rs index f0c5f362..b9f58324 100644 --- a/crates/kind-tree/src/concrete/mod.rs +++ b/crates/kind-tree/src/concrete/mod.rs @@ -5,6 +5,8 @@ use std::fmt::{Display, Error, Formatter}; use crate::symbol::{Ident, QualifiedIdent}; +use crate::telescope::Telescope; + use expr::Expr; use fxhash::FxHashMap; use kind_span::{Locatable, Range}; @@ -18,48 +20,6 @@ pub mod visitor; pub use expr::*; -/// A sequence of arguments that depends on the previous sequence -/// it's similar to a iterated sigma type. -#[derive(Debug, Clone, Hash, PartialEq, Eq)] -pub struct Telescope(Vec); - -impl Default for Telescope { - fn default() -> Self { - Self(Default::default()) - } -} - -impl Telescope { - pub fn new(vec: Vec) -> Telescope { - Telescope(vec) - } - - pub fn len(&self) -> usize { - self.0.len() - } - - pub fn push(&mut self, el: T) { - self.0.push(el) - } - - pub fn as_slice(&self) -> &[T] { - self.0.as_slice() - } - - pub fn to_vec(self) -> Vec { - self.0 - } -} - -impl Telescope -where - T: Clone, -{ - pub fn drop(self, num: usize) -> Telescope { - Telescope(self.0[num..].to_vec()) - } -} - /// A value of a attribute #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub enum AttributeStyle { @@ -207,9 +167,14 @@ pub struct EntryMeta { /// by joining a bunch of books that are already resolved. #[derive(Clone, Debug, Default)] pub struct Book { - pub names: LinkedHashMap, // Ordered hashset - pub entries: FxHashMap, // Probably deterministic order everytime - pub count: FxHashMap, // Stores some important information in order to desugarize + // Ordered hashset + pub names: LinkedHashMap, + + // Probably deterministic order everytime + pub entries: FxHashMap, + + // Stores some important information in order to desugarize + pub count: FxHashMap, } impl Book { @@ -234,7 +199,7 @@ impl Display for Constructor { writeln!(f, " /// {}", doc)?; } write!(f, "{}", self.name)?; - for arg in &self.args.0 { + for arg in self.args.iter() { write!(f, " {}", arg)?; } if let Some(res) = &self.typ { @@ -255,13 +220,13 @@ impl Display for TopLevel { writeln!(f, "{}", attr)?; } write!(f, "type {}", sum.name)?; - for arg in &sum.parameters.0 { + for arg in sum.parameters.iter() { write!(f, " {}", arg)?; } if !sum.indices.is_empty() { write!(f, " ~")?; } - for arg in &sum.indices.0 { + for arg in sum.indices.iter() { write!(f, " {}", arg)?; } writeln!(f, " {{")?; @@ -278,7 +243,7 @@ impl Display for TopLevel { writeln!(f, "{}", attr)?; } write!(f, "record {}", rec.name)?; - for arg in &rec.parameters.0 { + for arg in rec.parameters.iter() { write!(f, " {}", arg)?; } writeln!(f, " {{")?; @@ -344,7 +309,7 @@ impl Display for Entry { write!(f, "{}", self.name.clone())?; - for arg in &self.args.0 { + for arg in self.args.iter() { write!(f, " {}", arg)?; } @@ -415,49 +380,11 @@ impl Locatable for AttributeStyle { } } -impl Telescope { - pub fn extend(&self, other: &Telescope) -> Telescope - where - A: Clone, - { - Telescope([self.0.as_slice(), other.0.as_slice()].concat()) - } - - pub fn map(&self, f: F) -> Telescope - where - F: FnMut(&A) -> B, - { - Telescope(self.0.iter().map(f).collect()) - } - - pub fn is_empty(&self) -> bool { - self.0.is_empty() - } - - pub fn iter(&self) -> std::slice::Iter { - self.0.iter() - } - - pub fn iter_mut(&mut self) -> std::slice::IterMut { - self.0.iter_mut() - } -} - -impl IntoIterator for Telescope { - type Item = A; - - type IntoIter = std::vec::IntoIter; - - fn into_iter(self) -> Self::IntoIter { - self.0.into_iter() - } -} - impl Telescope { pub fn count_implicits(&self) -> (usize, usize) { let mut hiddens = 0; let mut erased = 0; - for arg in &self.0 { + for arg in self.iter() { if arg.hidden { hiddens += 1; } @@ -504,20 +431,20 @@ impl Constructor { let mut hiddens = 0; let mut erased = 0; - hiddens += def.parameters.0.len(); - erased += def.parameters.0.len(); + hiddens += def.parameters.len(); + erased += def.parameters.len(); arguments = arguments.extend(&def.parameters.map(|x| x.to_implicit())); // It tries to use all of the indices if no type // is specified. if self.typ.is_none() { - hiddens += def.indices.0.len(); - erased += def.indices.0.len(); + hiddens += def.indices.len(); + erased += def.indices.len(); arguments = arguments.extend(&def.indices.map(|x| x.to_implicit())); } - for arg in &self.args.0 { + for arg in self.args.iter() { if arg.erased { erased += 1; } @@ -541,7 +468,7 @@ impl Constructor { impl RecordDecl { pub fn fields_to_arguments(&self) -> Telescope { - Telescope( + Telescope::new( self.fields .iter() .map(|(name, _docs, typ)| { @@ -593,7 +520,7 @@ impl RecordDecl { }) .collect(); - arguments = arguments.extend(&Telescope(field_args)); + arguments = arguments.extend(&Telescope::new(field_args)); EntryMeta { hiddens, @@ -649,12 +576,4 @@ impl Argument { range: self.range, } } -} - -impl std::ops::Index for Telescope { - type Output = A; - - fn index(&self, index: usize) -> &Self::Output { - &self.0[index] - } -} +} \ No newline at end of file diff --git a/crates/kind-tree/src/concrete/visitor.rs b/crates/kind-tree/src/concrete/visitor.rs index 68ed149e..7fe0f550 100644 --- a/crates/kind-tree/src/concrete/visitor.rs +++ b/crates/kind-tree/src/concrete/visitor.rs @@ -149,7 +149,7 @@ pub fn walk_literal( _: &mut T, _: Range, _: &mut Literal) {} pub fn walk_constructor(ctx: &mut T, cons: &mut Constructor) { ctx.visit_ident(&mut cons.name); - visit_vec!(&mut cons.args.0, arg => ctx.visit_argument(arg)); + visit_vec!(cons.args.get_vec(), arg => ctx.visit_argument(arg)); visit_opt!(&mut cons.typ, arg => ctx.visit_expr(arg)) } @@ -238,7 +238,7 @@ pub fn walk_argument(ctx: &mut T, argument: &mut Argument) { pub fn walk_entry(ctx: &mut T, entry: &mut Entry) { ctx.visit_qualified_ident(&mut entry.name); - for arg in &mut entry.args.0 { + for arg in entry.args.iter_mut() { ctx.visit_argument(arg) } ctx.visit_expr(&mut entry.typ); @@ -317,14 +317,14 @@ pub fn walk_top_level(ctx: &mut T, toplevel: &mut TopLevel) { super::TopLevel::SumType(sum) => { ctx.visit_qualified_ident(&mut sum.name); visit_vec!(&mut sum.attrs, arg => ctx.visit_attr(arg)); - visit_vec!(&mut sum.parameters.0, arg => ctx.visit_argument(arg)); - visit_vec!(&mut sum.indices.0, arg => ctx.visit_argument(arg)); + visit_vec!(sum.parameters.get_vec(), arg => ctx.visit_argument(arg)); + visit_vec!(sum.indices.get_vec(), arg => ctx.visit_argument(arg)); visit_vec!(&mut sum.constructors, arg => ctx.visit_constructor(arg)); } super::TopLevel::RecordType(rec) => { ctx.visit_qualified_ident(&mut rec.name); visit_vec!(&mut rec.attrs, arg => ctx.visit_attr(arg)); - visit_vec!(&mut rec.parameters.0, arg => ctx.visit_argument(arg)); + visit_vec!(rec.parameters.get_vec(), arg => ctx.visit_argument(arg)); visit_vec!(&mut rec.fields, (name, _docs, typ) => { ctx.visit_ident(name); ctx.visit_expr(typ); diff --git a/crates/kind-tree/src/desugared/mod.rs b/crates/kind-tree/src/desugared/mod.rs index c9365841..60a43b53 100644 --- a/crates/kind-tree/src/desugared/mod.rs +++ b/crates/kind-tree/src/desugared/mod.rs @@ -357,7 +357,7 @@ impl Expr { format!("{}{} -> {}", tilde, typ, body.traverse_pi_types()) } else { let body = body.traverse_pi_types(); - format!("({}{} : {}) -> {}", tilde, param, typ, body) + format!("{}({} : {}) -> {}", tilde, param, typ, body) } } _ => format!("{}", self), @@ -368,7 +368,7 @@ impl Expr { impl Display for AppBinding { fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { if self.erased { - write!(f, "-({})", self.data) + write!(f, "~({})", self.data) } else { write!(f, "{}", self.data) } diff --git a/crates/kind-tree/src/lib.rs b/crates/kind-tree/src/lib.rs index d074c862..f4e9cbb6 100644 --- a/crates/kind-tree/src/lib.rs +++ b/crates/kind-tree/src/lib.rs @@ -14,11 +14,16 @@ pub mod desugared; /// The untyped AST. pub mod untyped; +/// Telescope (Iterated sigma type representation) +pub mod telescope; + /// Describes symbols (identifiers) on the language. It will /// be really useful when we change the Symbol to take a number /// instead of a string due to optimizations. pub mod symbol; +use std::fmt::{Formatter, Display, Error}; + pub use hvm::syntax as backend; use symbol::Ident; @@ -55,3 +60,28 @@ pub enum Operator { Gtn, Neq, } + +impl Display for Operator { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + use Operator::*; + + match self { + Add => write!(f, "+"), + Sub => write!(f, "-"), + Mul => write!(f, "*"), + Div => write!(f, "/"), + Mod => write!(f, "%"), + And => write!(f, "&"), + Or => write!(f, "|"), + Xor => write!(f, "^"), + Shl => write!(f, "<<"), + Shr => write!(f, ">>"), + Ltn => write!(f, "<"), + Lte => write!(f, "<="), + Eql => write!(f, "=="), + Gte => write!(f, ">="), + Gtn => write!(f, ">"), + Neq => write!(f, "!="), + } + } +} \ No newline at end of file diff --git a/crates/kind-tree/src/symbol.rs b/crates/kind-tree/src/symbol.rs index 6cda0214..2e7ae3c1 100644 --- a/crates/kind-tree/src/symbol.rs +++ b/crates/kind-tree/src/symbol.rs @@ -171,6 +171,12 @@ impl Ident { new } + pub fn add_underscore(&self) -> Ident { + let mut new = self.clone(); + new.data = Symbol::new(format!("{}_", new.data.data)); + new + } + #[inline] pub fn to_str(&self) -> &str { &self.data.data diff --git a/crates/kind-tree/src/telescope.rs b/crates/kind-tree/src/telescope.rs new file mode 100644 index 00000000..a7fca5c6 --- /dev/null +++ b/crates/kind-tree/src/telescope.rs @@ -0,0 +1,89 @@ +/// A sequence of arguments that depends on the previous sequence +/// it's similar to a iterated sigma type. +#[derive(Debug, Clone, Hash, PartialEq, Eq)] +pub struct Telescope(Vec); + +impl Default for Telescope { + fn default() -> Self { + Self(Default::default()) + } +} + +impl Telescope { + pub fn new(vec: Vec) -> Telescope { + Telescope(vec) + } + + pub fn len(&self) -> usize { + self.0.len() + } + + pub fn push(&mut self, el: T) { + self.0.push(el) + } + + pub fn as_slice(&self) -> &[T] { + self.0.as_slice() + } + + pub fn to_vec(self) -> Vec { + self.0 + } + + pub fn get_vec(&mut self) -> &mut Vec { + &mut self.0 + } + + pub fn extend(&self, other: &Telescope) -> Telescope + where + T: Clone, + { + Telescope([self.as_slice(), other.as_slice()].concat()) + } + + pub fn map(&self, f: F) -> Telescope + where + F: FnMut(&T) -> B, + { + Telescope(self.0.iter().map(f).collect()) + } + + pub fn is_empty(&self) -> bool { + self.0.is_empty() + } + + pub fn iter(&self) -> std::slice::Iter { + self.0.iter() + } + + pub fn iter_mut(&mut self) -> std::slice::IterMut { + self.0.iter_mut() + } +} + +impl Telescope +where + T: Clone, +{ + pub fn drop(self, num: usize) -> Telescope { + Telescope(self.0[num..].to_vec()) + } +} + +impl IntoIterator for Telescope { + type Item = A; + + type IntoIter = std::vec::IntoIter; + + fn into_iter(self) -> Self::IntoIter { + self.0.into_iter() + } +} + +impl std::ops::Index for Telescope { + type Output = A; + + fn index(&self, index: usize) -> &Self::Output { + &self.0[index] + } +} \ No newline at end of file