From 57cbe3a828f342b118d750f5c3eae6d7ad114cf7 Mon Sep 17 00:00:00 2001 From: felipegchi Date: Thu, 24 Nov 2022 11:01:41 -0300 Subject: [PATCH] fix: fixed erasure --- crates/kind-checker/src/compiler/mod.rs | 28 ++++++++++++++++++- crates/kind-derive/src/lib.rs | 2 +- crates/kind-derive/src/matching.rs | 14 +++++----- crates/kind-derive/src/open.rs | 2 +- crates/kind-pass/src/desugar/destruct.rs | 2 +- crates/kind-pass/src/desugar/expr.rs | 34 +++++++++++++++++------- crates/kind-pass/src/desugar/mod.rs | 2 +- crates/kind-pass/src/erasure/mod.rs | 5 ---- crates/kind-pass/src/errors.rs | 4 +++ 9 files changed, 67 insertions(+), 26 deletions(-) diff --git a/crates/kind-checker/src/compiler/mod.rs b/crates/kind-checker/src/compiler/mod.rs index 06054e4c..39422840 100644 --- a/crates/kind-checker/src/compiler/mod.rs +++ b/crates/kind-checker/src/compiler/mod.rs @@ -113,6 +113,32 @@ fn lam(name: &Ident, body: Box) -> Box { }) } +fn desugar_str(input: &str, span: Span) -> Box { + let nil = QualifiedIdent::new_static("String.nil", None, span.to_range().unwrap()); + let cons = QualifiedIdent::new_static("String.cons", None, span.to_range().unwrap()); + input.chars().rfold( + Box::new(desugared::Expr { + data: desugared::ExprKind::Ctr(nil, vec![]), + span, + }), + |right, chr| { + Box::new(desugared::Expr { + data: desugared::ExprKind::Ctr( + cons.clone(), + vec![ + Box::new(desugared::Expr { + data: desugared::ExprKind::Num(kind_tree::Number::U60(chr as u64)), + span, + }), + right, + ], + ), + span, + }) + }, + ) +} + fn codegen_str(input: &str) -> Box { input.chars().rfold( Box::new(Term::Ctr { @@ -267,7 +293,7 @@ fn codegen_all_expr( eval_ctr(quote, TermTag::Hole), vec![span_to_num(expr.span), mk_u60(*num)], ), - Str(str) => codegen_str(str), + Str(str) => codegen_all_expr(lhs_rule, lhs, num, quote, &desugar_str(str, expr.span)), Hlp(_) => mk_lifted_ctr(eval_ctr(quote, TermTag::Hlp), vec![span_to_num(expr.span)]), Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"), } diff --git a/crates/kind-derive/src/lib.rs b/crates/kind-derive/src/lib.rs index 06fb4eee..f142aa3a 100644 --- a/crates/kind-derive/src/lib.rs +++ b/crates/kind-derive/src/lib.rs @@ -3,4 +3,4 @@ pub mod errors; pub mod matching; pub mod open; -pub mod subst; +pub mod subst; \ No newline at end of file diff --git a/crates/kind-derive/src/matching.rs b/crates/kind-derive/src/matching.rs index 69de0b3b..ac979c66 100644 --- a/crates/kind-derive/src/matching.rs +++ b/crates/kind-derive/src/matching.rs @@ -106,7 +106,7 @@ pub fn derive_match( 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()), + mk_pi(Ident::new_static("val_", range), res_motive_ty, mk_typ()), |out, arg| { mk_pi( arg.name.clone(), @@ -191,7 +191,7 @@ pub fn derive_match( types.push(Argument { hidden: false, erased: false, - name: Ident::new_static(&format!("_{}", cons.name.to_string()), range), + name: Ident::new_static(&format!("{}_", cons.name.to_string()), range), typ: Some(cons_type), range, }); @@ -239,11 +239,11 @@ pub fn derive_match( spine_params = sum .parameters .extend(&cons.args) - .map(|x| x.name.with_name(|f| format!("_{}", f))) + .map(|x| x.name.with_name(|f| format!("{}_", f))) .to_vec(); spine = cons .args - .map(|x| x.name.with_name(|f| format!("_{}", f))) + .map(|x| x.name.with_name(|f| format!("{}_", f))) .to_vec(); args_indices = args .iter() @@ -261,7 +261,7 @@ pub fn derive_match( let renames = FxHashMap::from_iter( sum.parameters .extend(&cons.args) - .map(|x| (x.name.to_string(), format!("_{}", x.name.to_string()))) + .map(|x| (x.name.to_string(), format!("{}_", x.name.to_string()))) .iter() .cloned(), ); @@ -280,12 +280,12 @@ pub fn derive_match( .parameters .extend(&sum.indices) .extend(&cons.args) - .map(|x| x.name.with_name(|f| format!("_{}", f))) + .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))) + .map(|x| x.name.with_name(|f| format!("{}_", f))) .to_vec(); args_indices = sum .indices diff --git a/crates/kind-derive/src/open.rs b/crates/kind-derive/src/open.rs index 5c808a40..55d8903a 100644 --- a/crates/kind-derive/src/open.rs +++ b/crates/kind-derive/src/open.rs @@ -106,7 +106,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry { let spine: Vec = rec .fields .iter() - .map(|(name, _, _)| name.with_name(|f| format!("_{}", f))) + .map(|(name, _, _)| name.with_name(|f| format!("{}_", f))) .collect(); pats.push(Box::new(Pat { diff --git a/crates/kind-pass/src/desugar/destruct.rs b/crates/kind-pass/src/desugar/destruct.rs index bb7eafeb..68d1c8bb 100644 --- a/crates/kind-pass/src/desugar/destruct.rs +++ b/crates/kind-pass/src/desugar/destruct.rs @@ -248,7 +248,7 @@ impl<'a> DesugarState<'a> { self.desugar_expr(res) } else { let mut idx: Vec = sum.indices.iter().map(|x| x.name.clone()).collect(); - idx.push(Ident::generate("_val")); + idx.push(Ident::generate("val_")); idx.iter().rfold(self.gen_hole_expr(match_.typ.range), |expr, l| { desugared::Expr::lambda(l.range, l.clone(), expr, false) }) diff --git a/crates/kind-pass/src/desugar/expr.rs b/crates/kind-pass/src/desugar/expr.rs index 823d11ed..5fc8da7e 100644 --- a/crates/kind-pass/src/desugar/expr.rs +++ b/crates/kind-pass/src/desugar/expr.rs @@ -8,19 +8,40 @@ use crate::errors::{PassError, Sugar}; use super::DesugarState; impl<'a> DesugarState<'a> { + pub fn check_implementation(&mut self, name: &str, range: Range, sugar: Sugar) -> bool { + if !self.old_book.names.contains_key(&name.to_string()) { + self.send_err(PassError::NeedToImplementMethods(range, sugar)); + false + } else { + true + } + } + pub(crate) fn desugar_literal( &mut self, range: Range, literal: &expr::Literal, ) -> Box { match literal { + Literal::Number(kind_tree::Number::U120(num)) => { + if !self.check_implementation("U120.new", range, Sugar::U120) { + return desugared::Expr::err(range); + } + desugared::Expr::num120(range, *num) + } + Literal::String(string) => { + if !self.check_implementation("String.cons", range, Sugar::String) + || !self.check_implementation("String.nil", range, Sugar::String) + { + return desugared::Expr::err(range); + } + desugared::Expr::str(range, string.clone()) + } Literal::Type => desugared::Expr::typ(range), Literal::Help(name) => desugared::Expr::hlp(range, name.clone()), Literal::NumType(kind_tree::NumType::U60) => desugared::Expr::u60(range), Literal::NumType(kind_tree::NumType::U120) => desugared::Expr::u120(range), Literal::Number(kind_tree::Number::U60(num)) => desugared::Expr::num60(range, *num), - Literal::Number(kind_tree::Number::U120(num)) => desugared::Expr::num120(range, *num), - Literal::String(string) => desugared::Expr::str(range, string.clone()), Literal::Char(cht) => desugared::Expr::num60(range, *cht as u64), } } @@ -138,9 +159,7 @@ impl<'a> DesugarState<'a> { ) -> Box { let sigma = QualifiedIdent::new_static("Sigma", None, range); - let entry = self.old_book.entries.get(sigma.to_string().as_str()); - if entry.is_none() { - self.send_err(PassError::NeedToImplementMethods(range, Sugar::Sigma)); + if !self.check_implementation(sigma.to_str(), range, Sugar::Sigma) { return desugared::Expr::err(range); } @@ -221,10 +240,7 @@ impl<'a> DesugarState<'a> { ) -> Box { let sigma_new = QualifiedIdent::new_sugared("Sigma", "new", range); - let entry = self.old_book.entries.get(sigma_new.to_string().as_str()); - - if entry.is_none() { - self.send_err(PassError::NeedToImplementMethods(range, Sugar::Pair)); + if !self.check_implementation(sigma_new.to_str(), range, Sugar::Pair) { return desugared::Expr::err(range); } diff --git a/crates/kind-pass/src/desugar/mod.rs b/crates/kind-pass/src/desugar/mod.rs index 10f802d5..cb9ad5ca 100644 --- a/crates/kind-pass/src/desugar/mod.rs +++ b/crates/kind-pass/src/desugar/mod.rs @@ -61,7 +61,7 @@ impl<'a> DesugarState<'a> { fn gen_name(&mut self, range: Range) -> Ident { self.name_count += 1; - Ident::new(format!("_x{}", self.name_count), range) + Ident::new(format!("x_{}", self.name_count), range) } fn gen_hole_expr(&mut self, range: Range) -> Box { diff --git a/crates/kind-pass/src/erasure/mod.rs b/crates/kind-pass/src/erasure/mod.rs index 00dfac48..ea2dc81b 100644 --- a/crates/kind-pass/src/erasure/mod.rs +++ b/crates/kind-pass/src/erasure/mod.rs @@ -305,11 +305,6 @@ impl<'a> ErasureState<'a> { name.to_string(), (name.range, (None, Relevance::Irrelevant)), ); - - let span = expr.span.to_range().unwrap_or_else(|| name.range.clone()); - if !self.unify(span, *on, (None, Relevance::Irrelevant), false) { - self.err_irrelevant(None, span, None) - } } else { self.ctx.insert(name.to_string(), (name.range, *on)); } diff --git a/crates/kind-pass/src/errors.rs b/crates/kind-pass/src/errors.rs index fe168b69..78dbb3b2 100644 --- a/crates/kind-pass/src/errors.rs +++ b/crates/kind-pass/src/errors.rs @@ -8,6 +8,8 @@ pub enum Sugar { Sigma, Pair, BoolIf, + String, + U120, Match(String), Open(String), } @@ -217,6 +219,8 @@ impl Diagnostic for PassError { Sugar::Sigma => "You must implement 'Sigma' in order to use the sigma notation.".to_string(), Sugar::Pair => "You must implement 'Sigma' and 'Sigma.new' in order to use the sigma notation.".to_string(), Sugar::BoolIf => "You must implement 'Bool.if' in order to use the if notation.".to_string(), + Sugar::String => "You must implement 'String.cons' in order to use the string notation.".to_string(), + Sugar::U120 => "You must implement 'U120.new' in order to use the u120 notation.".to_string(), Sugar::Match(name) => format!("You must implement '{}.match' in order to use the match notation (or derive match with #derive[match]).", name), Sugar::Open(name) => format!("You must implement '{}.open' in order to use the open notation (or derive open with #derive[open]).", name), }],