HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-08-16 03:40:33 +03:00
Code Issues Packages Projects Releases Wiki Activity

fix: fixed erasure

Browse Source
This commit is contained in:
felipegchi 2022-11-24 11:01:41 -03:00
parent d1c536db01
commit 57cbe3a828
9 changed files with 67 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
crates/kind-checker/src/compiler/mod.rs
View File

@ -113,6 +113,32 @@ fn lam(name: &Ident, body: Box<Term>) -> Box<Term> {
})
}
fn desugar_str(input: &str, span: Span) -> Box<desugared::Expr> {
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<Term> {
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"),
}

2
crates/kind-derive/src/lib.rs
View File

@ -3,4 +3,4 @@
pub mod errors;
pub mod matching;
pub mod open;
pub mod subst;
pub mod subst;

14
crates/kind-derive/src/matching.rs
View File

@ -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

2
crates/kind-derive/src/open.rs
View File

@ -106,7 +106,7 @@ pub fn derive_open(range: Range, rec: &RecordDecl) -> concrete::Entry {
let spine: Vec<Ident> = 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 {

2
crates/kind-pass/src/desugar/destruct.rs
View File

@ -248,7 +248,7 @@ impl<'a> DesugarState<'a> {
self.desugar_expr(res)
} else {
let mut idx: Vec<Ident> = 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)
})

34
crates/kind-pass/src/desugar/expr.rs
View File

@ -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<desugared::Expr> {
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<desugared::Expr> {
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<desugared::Expr> {
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);
}

2
crates/kind-pass/src/desugar/mod.rs
View File

@ -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<desugared::Expr> {

5
crates/kind-pass/src/erasure/mod.rs
View File

@ -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));
}

4
crates/kind-pass/src/errors.rs
View File

@ -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),
}],