From c011978fabf1af92dad7de007379e6c62cbf3ac9 Mon Sep 17 00:00:00 2001 From: Felipe g Date: Thu, 10 Nov 2022 20:15:15 -0300 Subject: [PATCH] feat: fixed erasure (wip app, pi and forall erasure) --- src/kind-checker/src/compiler/mod.rs | 150 +++++++------------------- src/kind-checker/src/report.rs | 84 +++++---------- src/kind-derive/src/matching.rs | 106 +++++++----------- src/kind-derive/src/open.rs | 4 +- src/kind-driver/src/lib.rs | 1 - src/kind-driver/src/resolution.rs | 6 +- src/kind-parser/src/expr.rs | 98 ++++++++--------- src/kind-pass/src/desugar/app.rs | 11 +- src/kind-pass/src/desugar/destruct.rs | 2 +- src/kind-pass/src/erasure/mod.rs | 111 +++++++++++-------- src/kind-pass/src/unbound/mod.rs | 2 +- src/kind-span/src/lib.rs | 7 ++ src/kind-target-hvm/src/lib.rs | 2 +- src/kind-tree/src/concrete/expr.rs | 27 ++++- src/kind-tree/src/concrete/visitor.rs | 11 +- src/kind-tree/src/desugared/mod.rs | 20 +++- 16 files changed, 288 insertions(+), 354 deletions(-) diff --git a/src/kind-checker/src/compiler/mod.rs b/src/kind-checker/src/compiler/mod.rs index 483f3585..6089b026 100644 --- a/src/kind-checker/src/compiler/mod.rs +++ b/src/kind-checker/src/compiler/mod.rs @@ -62,9 +62,7 @@ fn mk_ctr(name: String, args: Vec>) -> Box { } fn mk_var(ident: &str) -> Box { - Box::new(Term::Var { - name: ident.to_string(), - }) + Box::new(Term::Var { name: ident.to_string() }) } fn mk_u60(numb: u64) -> Box { @@ -72,10 +70,7 @@ fn mk_u60(numb: u64) -> Box { } fn mk_single_ctr(head: String) -> Box { - Box::new(Term::Ctr { - name: head, - args: vec![], - }) + Box::new(Term::Ctr { name: head, args: vec![] }) } fn mk_ctr_name(ident: &QualifiedIdent) -> Box { @@ -84,26 +79,15 @@ fn mk_ctr_name(ident: &QualifiedIdent) -> Box { } fn span_to_num(span: Span) -> Box { - Box::new(Term::Num { - numb: span.encode().0, - }) + Box::new(Term::Num { numb: span.encode().0 }) } fn set_origin(ident: &Ident) -> Box { - mk_quoted_ctr( - "Kind.Term.set_origin".to_owned(), - vec![ - span_to_num(Span::Locatable(ident.range)), - mk_var(ident.to_str()), - ], - ) + mk_quoted_ctr("Kind.Term.set_origin".to_owned(), vec![span_to_num(Span::Locatable(ident.range)), mk_var(ident.to_str())]) } fn lam(name: &Ident, body: Box) -> Box { - Box::new(Term::Lam { - name: name.to_string(), - body, - }) + Box::new(Term::Lam { name: name.to_string(), body }) } fn codegen_str(input: &str) -> Box { @@ -121,13 +105,7 @@ fn codegen_str(input: &str) -> Box { ) } -fn codegen_all_expr( - lhs_rule: bool, - lhs: bool, - num: &mut usize, - quote: bool, - expr: &Expr, -) -> Box { +fn codegen_all_expr(lhs_rule: bool, lhs: bool, num: &mut usize, quote: bool, expr: &Expr) -> Box { use kind_tree::desugared::ExprKind::*; match &expr.data { @@ -141,11 +119,7 @@ fn codegen_all_expr( *num += 1; mk_quoted_ctr( eval_ctr(quote, TermTag::Var), - vec![ - span_to_num(expr.span), - mk_u60(ident.encode()), - mk_u60((*num - 1) as u64), - ], + vec![span_to_num(expr.span), mk_u60(ident.encode()), mk_u60((*num - 1) as u64)], ) } else { mk_var(ident.to_str()) @@ -162,25 +136,24 @@ fn codegen_all_expr( ), Lambda(name, body) => mk_quoted_ctr( eval_ctr(quote, TermTag::Lambda), - vec![ - span_to_num(expr.span), - mk_u60(name.encode()), - lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body)), - ], - ), - App(head, spine) => spine.iter().fold( - codegen_all_expr(lhs_rule, lhs, num, quote, head), - |left, right| { - mk_quoted_ctr( - eval_ctr(quote, TermTag::App), - vec![ - span_to_num(expr.span), - left, - codegen_all_expr(lhs_rule, lhs, num, quote, &right.clone()), - ], - ) - }, + vec![span_to_num(expr.span), mk_u60(name.encode()), lam(name, codegen_all_expr(lhs_rule, lhs, num, quote, body))], ), + App(head, spine) => spine.iter().fold(codegen_all_expr(lhs_rule, lhs, num, quote, head), |left, right| { + mk_quoted_ctr( + eval_ctr(quote, TermTag::App), + vec![ + span_to_num(expr.span), + left, + codegen_all_expr( + lhs_rule, + lhs, + num, + quote, + &right.data + ), + ], + ) + }), Ctr(name, spine) => mk_quoted_ctr( eval_ctr(quote, TermTag::Ctr(spine.len())), vec_preppend![ @@ -190,11 +163,7 @@ fn codegen_all_expr( ], ), Fun(name, spine) => { - let new_spine: Vec> = spine - .iter() - .cloned() - .map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)) - .collect(); + let new_spine: Vec> = spine.iter().cloned().map(|x| codegen_all_expr(lhs_rule, lhs, num, quote, &x)).collect(); if quote { mk_quoted_ctr( eval_ctr(quote, TermTag::Fun(new_spine.len())), @@ -241,11 +210,8 @@ fn codegen_all_expr( codegen_all_expr(lhs_rule, lhs, num, quote, expr), ], ), - Num(desugared::Num::U60(n)) => mk_quoted_ctr( - eval_ctr(quote, TermTag::Num), - vec![span_to_num(expr.span), mk_u60(*n)], - ), - Num(desugared::Num::U120(n)) => todo!(), + Num(desugared::Num::U60(n)) => mk_quoted_ctr(eval_ctr(quote, TermTag::Num), vec![span_to_num(expr.span), mk_u60(*n)]), + Num(desugared::Num::U120(_)) => todo!(), Binary(operator, left, right) => mk_quoted_ctr( eval_ctr(quote, TermTag::Binary), vec![ @@ -255,10 +221,7 @@ fn codegen_all_expr( codegen_all_expr(lhs_rule, lhs, num, quote, right), ], ), - Hole(num) => mk_quoted_ctr( - eval_ctr(quote, TermTag::Hole), - vec![span_to_num(expr.span), mk_u60(*num)], - ), + Hole(num) => mk_quoted_ctr(eval_ctr(quote, TermTag::Hole), vec![span_to_num(expr.span), mk_u60(*num)]), Hlp(_) => mk_quoted_ctr(eval_ctr(quote, TermTag::Hlp), vec![span_to_num(expr.span)]), Str(input) => codegen_str(input), Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"), @@ -294,17 +257,11 @@ fn codegen_vec(exprs: T) -> Box where T: Iterator>, { - exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| { - mk_ctr("List.cons".to_string(), vec![right, left]) - }) + exprs.fold(mk_ctr("List.nil".to_string(), vec![]), |left, right| mk_ctr("List.cons".to_string(), vec![right, left])) } fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) { - let base_vars = lift_spine( - (0..rule.pats.len()) - .map(|x| mk_var(&format!("x{}", x))) - .collect::>>(), - ); + let base_vars = lift_spine((0..rule.pats.len()).map(|x| mk_var(&format!("x{}", x))).collect::>>()); file.rules.push(lang::Rule { lhs: mk_ctr( @@ -346,11 +303,7 @@ fn codegen_rule_end(file: &mut lang::File, rule: &desugared::Rule) { fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { let mut count = 0; - let lhs_args = rule - .pats - .iter() - .map(|x| codegen_pattern(&mut count, false, x)) - .collect::>>(); + let lhs_args = rule.pats.iter().map(|x| codegen_pattern(&mut count, false, x)).collect::>>(); file.rules.push(lang::Rule { lhs: mk_ctr( @@ -367,21 +320,9 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { file.rules.push(lang::Rule { lhs: mk_ctr( TermTag::HoasF(rule.name.to_string()).to_string(), - vec![ - mk_var("orig"), - mk_var("a"), - mk_var("r"), - mk_var("log"), - mk_var("ret"), - ], - ), - rhs: mk_ctr( - "HVM.put".to_owned(), - vec![ - mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]), - mk_var("ret"), - ], + vec![mk_var("orig"), mk_var("a"), mk_var("r"), mk_var("log"), mk_var("ret")], ), + rhs: mk_ctr("HVM.put".to_owned(), vec![mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]), mk_var("ret")]), }); } else { file.rules.push(lang::Rule { @@ -397,13 +338,7 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) { } } -fn codegen_entry_rules( - count: &mut usize, - index: usize, - args: &mut Vec>, - entry: &desugared::Rule, - pats: &[Box], -) -> Box { +fn codegen_entry_rules(count: &mut usize, index: usize, args: &mut Vec>, entry: &desugared::Rule, pats: &[Box]) -> Box { if pats.is_empty() { mk_ctr( "Kind.Rule.rhs".to_owned(), @@ -420,13 +355,7 @@ fn codegen_entry_rules( let pat = &pats[0]; let expr = codegen_all_expr(true, false, count, false, pat); args.push(expr.clone()); - mk_ctr( - "Kind.Rule.lhs".to_owned(), - vec![ - expr, - codegen_entry_rules(count, index + 1, args, entry, &pats[1..]), - ], - ) + mk_ctr("Kind.Rule.lhs".to_owned(), vec![expr, codegen_entry_rules(count, index + 1, args, entry, &pats[1..])]) } } @@ -446,9 +375,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { rhs: codegen_type(&entry.args, &entry.typ), }); - let base_vars = (0..entry.args.len()) - .map(|x| mk_var(&format!("x{}", x))) - .collect::>>(); + let base_vars = (0..entry.args.len()).map(|x| mk_var(&format!("x{}", x))).collect::>>(); file.rules.push(lang::Rule { lhs: mk_ctr( @@ -494,10 +421,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) { codegen_rule_end(file, &entry.rules[0]) } - let rules = entry - .rules - .iter() - .map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats)); + let rules = entry.rules.iter().map(|rule| codegen_entry_rules(&mut 0, 0, &mut Vec::new(), rule, &rule.pats)); file.rules.push(lang::Rule { lhs: mk_ctr("RuleOf".to_owned(), vec![mk_ctr_name(&entry.name)]), diff --git a/src/kind-checker/src/report.rs b/src/kind-checker/src/report.rs index 13c8b17e..24890c81 100644 --- a/src/kind-checker/src/report.rs +++ b/src/kind-checker/src/report.rs @@ -63,14 +63,8 @@ fn parse_name(term: &Term) -> Result { fn parse_qualified(term: &Term) -> Result { match term { - Term::Num { numb } => Ok(QualifiedIdent::new_static( - &Ident::decode(*numb), - None, - Range::ghost_range(), - )), - Term::Ctr { name, args: _ } => { - Ok(QualifiedIdent::new_static(name, None, Range::ghost_range())) - } + Term::Num { numb } => Ok(QualifiedIdent::new_static(&Ident::decode(*numb), None, Range::ghost_range())), + Term::Ctr { name, args: _ } => Ok(QualifiedIdent::new_static(name, None, Range::ghost_range())), _ => Err("Error while matching opt".to_string()), } } @@ -79,10 +73,7 @@ fn parse_expr(term: &Term) -> Result, String> { parse_all_expr(Default::default(), term) } -fn parse_all_expr( - names: im::HashMap, - term: &Term, -) -> Result, String> { +fn parse_all_expr(names: im::HashMap, term: &Term) -> Result, String> { match term { Term::Ctr { name, args } => match name.as_str() { "Kind.Quoted.all" => Ok(Expr::all( @@ -103,16 +94,9 @@ fn parse_all_expr( parse_all_expr(names, &args[3])?, )), "Kind.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)), - "Kind.Quoted.var" => Ok(Expr::var(Ident::new( - parse_name(&args[1])?, - parse_orig(&args[0])?, - ))), + "Kind.Quoted.var" => Ok(Expr::var(Ident::new(parse_name(&args[1])?, parse_orig(&args[0])?))), "Kind.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)), - "Kind.Quoted.ann" => Ok(Expr::ann( - parse_orig(&args[0])?, - parse_all_expr(names.clone(), &args[1])?, - parse_all_expr(names, &args[2])?, - )), + "Kind.Quoted.ann" => Ok(Expr::ann(parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, parse_all_expr(names, &args[2])?)), "Kind.Quoted.sub" => Ok(Expr::sub( parse_orig(&args[0])?, Ident::generate(&parse_name(&args[1])?), @@ -123,43 +107,37 @@ fn parse_all_expr( "Kind.Quoted.app" => Ok(Expr::app( parse_orig(&args[0])?, parse_all_expr(names.clone(), &args[1])?, - vec![parse_all_expr(names, &args[2])?], - )), - "Kind.Quoted.ctr" => Ok(Expr::ctr( - parse_orig(&args[1])?, - parse_qualified(&args[0])?, - { - let mut res = Vec::new(); - for arg in parse_list(&args[2])? { - res.push(parse_all_expr(names.clone(), &arg)?); + vec![ + desugared::AppBinding { + data: parse_all_expr(names, &args[2])?, + erased: false, } - res - }, - )), - "Kind.Quoted.fun" => Ok(Expr::fun( - parse_orig(&args[0])?, - parse_qualified(&args[1])?, - { - let mut res = Vec::new(); - for arg in &args[1..] { - res.push(parse_all_expr(names.clone(), arg)?); - } - res - }, + ], )), + "Kind.Quoted.ctr" => Ok(Expr::ctr(parse_orig(&args[1])?, parse_qualified(&args[0])?, { + let mut res = Vec::new(); + for arg in parse_list(&args[2])? { + res.push(parse_all_expr(names.clone(), &arg)?); + } + res + })), + "Kind.Quoted.fun" => Ok(Expr::fun(parse_orig(&args[0])?, parse_qualified(&args[1])?, { + let mut res = Vec::new(); + for arg in &args[1..] { + res.push(parse_all_expr(names.clone(), arg)?); + } + res + })), "Kind.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))), "Kind.Quoted.u60" => Ok(Expr::u60(parse_orig(&args[0])?)), - "Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120? + "Kind.Quoted.num" => Ok(Expr::num60(parse_orig(&args[0])?, parse_num(&args[1])?)), // TODO: do something about u120? "Kind.Quoted.op2" => Ok(Expr::binary( parse_orig(&args[0])?, parse_op(&args[1])?, parse_all_expr(names.clone(), &args[2])?, parse_all_expr(names, &args[3])?, )), - tag => Err(format!( - "Unexpected tag on transforming quoted term {:?}", - tag - )), + tag => Err(format!("Unexpected tag on transforming quoted term {:?}", tag)), }, _ => Err("Unexpected term on transforming quoted term".to_string()), } @@ -222,14 +200,8 @@ fn parse_type_error(expr: &Term) -> Result { parse_all_expr(im::HashMap::new(), &args[2])?, parse_all_expr(im::HashMap::new(), &args[3])?, )), - "Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection( - ctx, - orig, - parse_all_expr(im::HashMap::new(), &args[2])?, - )), - "Kind.Error.Quoted.too_many_arguments" => { - Ok(TypeError::TooManyArguments(ctx, orig)) - } + "Kind.Error.Quoted.inspection" => Ok(TypeError::Inspection(ctx, orig, parse_all_expr(im::HashMap::new(), &args[2])?)), + "Kind.Error.Quoted.too_many_arguments" => Ok(TypeError::TooManyArguments(ctx, orig)), "Kind.Error.Quoted.type_mismatch" => Ok(TypeError::TypeMismatch( ctx, orig, diff --git a/src/kind-derive/src/matching.rs b/src/kind-derive/src/matching.rs index d7ac75bf..a4f5655c 100644 --- a/src/kind-derive/src/matching.rs +++ b/src/kind-derive/src/matching.rs @@ -10,12 +10,7 @@ use kind_tree::symbol::{Ident, QualifiedIdent}; /// Derives an eliminator from a sum type declaration. pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { - let mk_var = |name: Ident| -> Box { - Box::new(Expr { - data: ExprKind::Var(name), - range, - }) - }; + let mk_var = |name: Ident| -> Box { Box::new(Expr { data: ExprKind::Var(name), range }) }; let mk_cons = |name: QualifiedIdent, spine: Vec| -> Box { Box::new(Expr { @@ -24,7 +19,7 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { }) }; - let mk_app = |left: Box, right: Vec, range: Range| -> Box { + let mk_app = |left: Box, right: Vec, range: Range| -> Box { Box::new(Expr { data: ExprKind::App(left, right), range, @@ -60,26 +55,11 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { // 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 res_motive_ty = mk_cons(sum.name.clone(), all_args.iter().cloned().map(|x| Binding::Positional(mk_var(x.name))).collect()); - let parameter_names: Vec = sum - .parameters - .iter() - .map(|x| Binding::Positional(mk_var(x.name.clone()))) - .collect(); + let parameter_names: Vec = sum.parameters.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect(); - let indice_names: Vec = sum - .indices - .iter() - .map(|x| Binding::Positional(mk_var(x.name.clone()))) - .collect(); + let indice_names: Vec = sum.indices.iter().map(|x| AppBinding::explicit(mk_var(x.name.clone()))).collect(); // Sccrutinzies @@ -95,16 +75,13 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { let motive_ident = Ident::new_static("motive", range); - let motive_type = sum.parameters.extend(&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_type = sum + .parameters + .extend(&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) + }); types.push(Argument { hidden: false, @@ -114,39 +91,33 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { range, }); - let params = sum - .parameters - .map(|x| Binding::Positional(mk_var(x.name.clone()))); + let params = sum.parameters.map(|x| Binding::Positional(mk_var(x.name.clone()))); // Constructors type for cons in &sum.constructors { - let vars: Vec = cons - .args - .iter() - .map(|x| Binding::Positional(mk_var(x.name.clone()))) - .collect(); + let vars: Vec = cons.args.iter().map(|x| Binding::Positional(mk_var(x.name.clone()))).collect(); - let cons_inst = mk_cons( - sum.name.add_segment(cons.name.to_str()), - [params.as_slice(), vars.as_slice()].concat(), - ); + let cons_inst = mk_cons(sum.name.add_segment(cons.name.to_str()), [params.as_slice(), vars.as_slice()].concat()); let mut indices_of_cons = match cons.typ.clone().map(|x| x.data) { - Some(ExprKind::Constr(_, spine)) => spine.to_vec(), + Some(ExprKind::Constr(_, spine)) => spine + .iter() + .map(|x| match x { + Binding::Positional(expr) => AppBinding::explicit(expr.clone()), + Binding::Named(_, _, _) => todo!("Internal Error: Need to reorder"), + }) + .collect(), _ => [parameter_names.as_slice(), indice_names.as_slice()].concat(), }; - indices_of_cons.push(Binding::Positional(cons_inst)); + indices_of_cons.push(AppBinding::explicit(cons_inst)); let cons_tipo = mk_app(mk_var(motive_ident.clone()), indices_of_cons, range); - let cons_type = cons.args.iter().rfold(cons_tipo, |out, arg| { - mk_pi( - arg.name.clone(), - arg.typ.clone().unwrap_or_else(mk_typ), - out, - ) - }); + let cons_type = cons + .args + .iter() + .rfold(cons_tipo, |out, arg| mk_pi(arg.name.clone(), arg.typ.clone().unwrap_or_else(mk_typ), out)); types.push(Argument { hidden: false, @@ -157,8 +128,8 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { }); } - let mut res: Vec = [parameter_names.as_slice(), indice_names.as_slice()].concat(); - res.push(Binding::Positional(mk_var(Ident::generate("scrutinizer")))); + let mut res: Vec = [parameter_names.as_slice(), indice_names.as_slice()].concat(); + res.push(AppBinding::explicit(mk_var(Ident::generate("scrutinizer")))); let ret_ty = mk_app(mk_var(motive_ident), res, range); let mut rules = Vec::new(); @@ -167,16 +138,11 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { let cons_ident = sum.name.add_segment(cons.name.to_str()); let mut pats: Vec> = Vec::new(); - let spine_params: Vec = sum - .parameters - .extend(&cons.args) - .map(|x| x.name.with_name(|f| format!("{}_", f))) - .to_vec(); + let irrelev = cons.args.map(|x| x.hidden).to_vec(); - let spine: Vec = cons - .args - .map(|x| x.name.with_name(|f| format!("{}_", f))) - .to_vec(); + let spine_params: Vec = sum.parameters.extend(&cons.args).map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec(); + + let spine: Vec = cons.args.map(|x| x.name.with_name(|f| format!("{}_", f))).to_vec(); pats.push(Box::new(Pat { data: concrete::pat::PatKind::App( @@ -211,7 +177,11 @@ pub fn derive_match(range: Range, sum: &SumTypeDecl) -> concrete::Entry { mk_var(cons.name.clone()), spine .iter() - .map(|arg| Binding::Positional(mk_var(arg.clone()))) + .zip(irrelev) + .map(|(arg, erased)| AppBinding { + data: mk_var(arg.clone()), + erased, + }) .collect(), cons.name.range, ); diff --git a/src/kind-derive/src/open.rs b/src/kind-derive/src/open.rs index a051bbb2..5e2cf097 100644 --- a/src/kind-derive/src/open.rs +++ b/src/kind-derive/src/open.rs @@ -22,7 +22,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry { }) }; - let mk_app = |left: Box, right: Vec| -> Box { + let mk_app = |left: Box, right: Vec| -> Box { Box::new(Expr { data: ExprKind::App(left, right), range, @@ -126,7 +126,7 @@ pub fn derive_open(range: Range, sum: &RecordDecl) -> concrete::Entry { mk_var(Ident::generate("fun_")), spine .iter() - .map(|arg| Binding::Positional(mk_var(arg.clone()))) + .map(|arg| AppBinding { data: mk_var(arg.clone()), erased: false }) .collect(), ); diff --git a/src/kind-driver/src/lib.rs b/src/kind-driver/src/lib.rs index 6bc7f18f..b8d7f51e 100644 --- a/src/kind-driver/src/lib.rs +++ b/src/kind-driver/src/lib.rs @@ -49,7 +49,6 @@ pub fn to_book(session: &mut Session, path: &PathBuf) -> Option pub fn erase_book(session: &mut Session, path: &PathBuf) -> Option { let concrete_book = to_book(session, path)?; let desugared_book = desugar::desugar_book(session.diagnostic_sender.clone(), &concrete_book)?; - println!("Desugared: {}", desugared_book); erasure::erase_book( &desugared_book, session.diagnostic_sender.clone(), diff --git a/src/kind-driver/src/resolution.rs b/src/kind-driver/src/resolution.rs index addb11d1..f12238cc 100644 --- a/src/kind-driver/src/resolution.rs +++ b/src/kind-driver/src/resolution.rs @@ -152,7 +152,7 @@ fn parse_and_store_book_by_identifier<'a>( match ident_to_path(&session.root, ident, true) { Ok(Some(path)) => parse_and_store_book_by_path(session, &path, book), - Ok(None) => true, + Ok(None) => false, Err(err) => { session.diagnostic_sender.send(err).unwrap(); true @@ -179,8 +179,8 @@ fn parse_and_store_book_by_path<'a>( return true; } }; - let ctx_id = session.book_counter; + let ctx_id = session.book_counter; session.add_path(Rc::new(path.to_path_buf()), input.clone()); let (mut module, mut failed) = @@ -200,7 +200,7 @@ fn parse_and_store_book_by_path<'a>( } } - failed |= expand_uses(&mut module, session.diagnostic_sender.clone()); + expand_uses(&mut module, session.diagnostic_sender.clone()); module_to_book(&mut failed, session, &module, book); diff --git a/src/kind-parser/src/expr.rs b/src/kind-parser/src/expr.rs index 0fcf72f2..4668062c 100644 --- a/src/kind-parser/src/expr.rs +++ b/src/kind-parser/src/expr.rs @@ -66,22 +66,16 @@ impl<'a> Parser<'a> { unused = true; } if unused { - self.errs - .send(SyntaxError::UnusedDocString(start.mix(last)).into()) - .unwrap() + self.errs.send(SyntaxError::UnusedDocString(start.mix(last)).into()).unwrap() } } pub fn is_pi_type(&self) -> bool { - self.get().same_variant(&Token::LPar) - && self.peek(1).is_lower_id() - && self.peek(2).same_variant(&Token::Colon) + self.get().same_variant(&Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Colon) } pub fn is_named_parameter(&self) -> bool { - self.get().same_variant(&Token::LPar) - && self.peek(1).is_lower_id() - && self.peek(2).same_variant(&Token::Eq) + self.get().same_variant(&Token::LPar) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Eq) } pub fn is_lambda(&self) -> bool { @@ -89,9 +83,7 @@ impl<'a> Parser<'a> { } pub fn is_sigma_type(&self) -> bool { - self.get().same_variant(&Token::LBracket) - && self.peek(1).is_lower_id() - && self.peek(2).same_variant(&Token::Colon) + self.get().same_variant(&Token::LBracket) && self.peek(1).is_lower_id() && self.peek(2).same_variant(&Token::Colon) } pub fn is_substitution(&self) -> bool { @@ -126,8 +118,7 @@ impl<'a> Parser<'a> { pub fn parse_upper_id(&mut self) -> Result { let range = self.range(); - let (start, end) = - eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?; + let (start, end) = eat_single!(self, Token::UpperId(start, end) => (start.clone(), end.clone()))?; let ident = QualifiedIdent::new_static(start.as_str(), end, range); Ok(ident) } @@ -217,10 +208,7 @@ impl<'a> Parser<'a> { "U60" => ExprKind::Lit(Literal::U60), _ => ExprKind::Constr(id.clone(), vec![]), }; - Ok(Box::new(Expr { - range: id.range, - data, - })) + Ok(Box::new(Expr { range: id.range, data })) } fn parse_data(&mut self, multiline: bool) -> Result, SyntaxError> { @@ -283,10 +271,7 @@ impl<'a> Parser<'a> { if self.check_actual(Token::RBracket) { let range = self.advance().1.mix(range); - return Ok(Box::new(Expr { - range, - data: ExprKind::List(vec), - })); + return Ok(Box::new(Expr { range, data: ExprKind::List(vec) })); } vec.push(*self.parse_expr(false)?); @@ -316,10 +301,7 @@ impl<'a> Parser<'a> { let end = self.eat_variant(Token::RBracket)?.1; let range = range.mix(end); - Ok(Box::new(Expr { - range, - data: ExprKind::List(vec), - })) + Ok(Box::new(Expr { range, data: ExprKind::List(vec) })) } fn parse_paren(&mut self) -> Result, SyntaxError> { @@ -400,13 +382,39 @@ impl<'a> Parser<'a> { } } + fn parse_app_binding(&mut self) -> Result { + self.ignore_docs(); + let (erased, data) = if self.get().same_variant(&Token::LBrace) { + let start = self.range(); + self.advance(); // '{' + let atom = self.parse_expr(true)?; + self.eat_closing_keyword(Token::RBrace, start)?; + (true, atom) + } else { + (false, self.parse_expr(false)?) + }; + Ok(AppBinding { data, erased }) + } + fn parse_call(&mut self, multiline: bool) -> Result, SyntaxError> { if self.get().is_upper_id() { self.parse_data(multiline) } else { let head = self.parse_atom()?; let start = head.range; - let (end, spine) = self.parse_call_tail(start, multiline)?; + + let mut spine = Vec::new(); + let mut end = start; + + while (!self.is_linebreak() || multiline) && !self.get().same_variant(&Token::Eof) { + if let Some(atom) = self.try_single(&|parser| parser.parse_app_binding())? { + end = atom.data.range; + spine.push(atom) + } else { + break; + } + } + if spine.is_empty() { Ok(head) } else { @@ -418,21 +426,15 @@ impl<'a> Parser<'a> { } } - fn parse_call_tail( - &mut self, - start: Range, - multiline: bool, - ) -> Result<(Range, Vec), SyntaxError> { + fn parse_call_tail(&mut self, start: Range, multiline: bool) -> Result<(Range, Vec), SyntaxError> { let mut spine = Vec::new(); let mut end = start; while (!self.is_linebreak() || multiline) && !self.get().same_variant(&Token::Eof) { - let res = self.try_single(&|parser| parser.parse_binding())?; - match res { - Some(atom) => { - end = atom.locate(); - spine.push(atom) - } - None => break, + if let Some(atom) = self.try_single(&|parser| parser.parse_binding())? { + end = atom.locate(); + spine.push(atom) + } else { + break; } } Ok((end, spine)) @@ -478,12 +480,7 @@ impl<'a> Parser<'a> { if self.get().is_upper_id() { let upper = self.parse_upper_id()?; let (range, bindings, ignore_rest) = self.parse_pat_destruct_bindings()?; - Ok(Destruct::Destruct( - upper.range.mix(range.unwrap_or(upper.range)), - upper, - bindings, - ignore_rest, - )) + Ok(Destruct::Destruct(upper.range.mix(range.unwrap_or(upper.range)), upper, bindings, ignore_rest)) } else { let name = self.parse_id()?; Ok(Destruct::Ident(name)) @@ -556,9 +553,7 @@ impl<'a> Parser<'a> { })) } - pub fn parse_pat_destruct_bindings( - &mut self, - ) -> Result<(Option, Vec, bool), SyntaxError> { + pub fn parse_pat_destruct_bindings(&mut self) -> Result<(Option, Vec, bool), SyntaxError> { let mut ignore_rest_range = None; let mut bindings = Vec::new(); let mut range = None; @@ -629,12 +624,7 @@ impl<'a> Parser<'a> { None }; - let match_ = Box::new(Match { - typ, - scrutinizer, - cases, - motive, - }); + let match_ = Box::new(Match { typ, scrutinizer, cases, motive }); Ok(Box::new(Expr { data: ExprKind::Match(match_), diff --git a/src/kind-pass/src/desugar/app.rs b/src/kind-pass/src/desugar/app.rs index 6839510c..188b8765 100644 --- a/src/kind-pass/src/desugar/app.rs +++ b/src/kind-pass/src/desugar/app.rs @@ -175,13 +175,10 @@ impl<'a> DesugarState<'a> { let mut new_spine = Vec::new(); let new_head = self.desugar_expr(head); for arg in spine { - match arg { - Binding::Positional(v) => new_spine.push(self.desugar_expr(v)), - Binding::Named(r, _, v) => { - self.send_err(PassError::CannotUseNamed(head.range, *r)); - new_spine.push(self.desugar_expr(v)) - } - } + new_spine.push(desugared::AppBinding { + data: self.desugar_expr(&arg.data), + erased: arg.erased + }) } desugared::Expr::app(range, new_head, new_spine) } diff --git a/src/kind-pass/src/desugar/destruct.rs b/src/kind-pass/src/desugar/destruct.rs index 6b4a491d..d54a318c 100644 --- a/src/kind-pass/src/desugar/destruct.rs +++ b/src/kind-pass/src/desugar/destruct.rs @@ -223,7 +223,7 @@ impl<'a> DesugarState<'a> { let motive = if let Some(res) = &match_.motive { self.desugar_expr(res) } else { - let mut idx: Vec = sum.indices.iter().map(|x| x.name.clone()).collect(); + let mut idx: Vec = sum.parameters.extend(&sum.indices).iter().map(|x| x.name.clone()).collect(); idx.push(Ident::generate("_val")); idx.iter().rfold(self.gen_hole_expr(), |expr, l| { desugared::Expr::lambda(l.range, l.clone(), expr) diff --git a/src/kind-pass/src/erasure/mod.rs b/src/kind-pass/src/erasure/mod.rs index 7ec437a5..99994489 100644 --- a/src/kind-pass/src/erasure/mod.rs +++ b/src/kind-pass/src/erasure/mod.rs @@ -16,7 +16,7 @@ use fxhash::{FxHashMap, FxHashSet}; use kind_report::data::DiagnosticFrame; use kind_span::Range; -use kind_tree::desugared::{Book, Entry, Expr, ExprKind, Rule}; +use kind_tree::{desugared::{Book, Entry, Expr, ExprKind, Rule, self}, symbol::{QualifiedIdent}}; use crate::errors::PassError; @@ -211,41 +211,60 @@ impl<'a> ErasureState<'a> { self.unify_loop(range, left, right, &mut Default::default(), relevance_unify) } - pub fn erase_pat(&mut self, on: (Option, Relevance), pat: &Expr) { + pub fn erase_pat_spine(&mut self, on: (Option, Relevance), name: &QualifiedIdent, spine: &Vec>) -> Vec> { + let fun = match self.names.get(&name.to_string()) { + Some(res) => *res, + None => self.new_hole(name.range, name.to_string()), + }; + + if !self.unify(name.range, on, fun, true) { + self.err_irrelevant(None, name.range, None) + } + + let entry = self.book.entrs.get(name.to_string().as_str()).unwrap(); + let erased = entry.args.iter(); + + let irrelevances = erased.map(|arg| { + if on.1 == Relevance::Irrelevant { + on + } else if arg.erased { + (Some(arg.span), Relevance::Irrelevant) + } else { + (Some(arg.span), Relevance::Relevant) + } + }); + + spine + .iter() + .zip(irrelevances) + .map(|(arg, relev)| (self.erase_pat(relev, arg), relev.1.clone())) + .filter(|res| res.1 == Relevance::Relevant) + .map(|res| res.0) + .collect() + } + + pub fn erase_pat(&mut self, on: (Option, Relevance), pat: &Expr) -> Box { use kind_tree::desugared::ExprKind::*; match &pat.data { - Num(_) | Str(_) => (), + Num(_) | Str(_) => Box::new(pat.clone()), Var(name) => { self.ctx.insert(name.to_string(), (name.range, on)); + Box::new(pat.clone()) } - Fun(name, spine) | Ctr(name, spine) => { - let fun = match self.names.get(&name.to_string()) { - Some(res) => *res, - None => self.new_hole(name.range, name.to_string()), - }; - - if !self.unify(name.range, on, fun, true) { - self.err_irrelevant(None, name.range, None) - } - - let entry = self.book.entrs.get(name.to_string().as_str()).unwrap(); - let erased = entry.args.iter(); - - let irrelevances = erased.map(|arg| { - if on.1 == Relevance::Irrelevant { - on - } else if arg.erased { - (Some(arg.span), Relevance::Irrelevant) - } else { - (Some(arg.span), Relevance::Relevant) - } - }); - - spine - .iter() - .zip(irrelevances) - .for_each(|(arg, relev)| self.erase_pat(relev, arg)); + Fun(name, spine) => { + let spine = self.erase_pat_spine(on, &name, spine); + Box::new(Expr { + span: pat.span.clone(), + data: ExprKind::Fun(name.clone(), spine), + }) + } + Ctr(name, spine) => { + let spine = self.erase_pat_spine(on, &name, spine); + Box::new(Expr { + span: pat.span.clone(), + data: ExprKind::Ctr(name.clone(), spine), + }) } res => panic!("Internal Error: Not a pattern {:?}", res), } @@ -313,7 +332,17 @@ impl<'a> ErasureState<'a> { } App(head, spine) => { let head = self.erase_expr(on, head); - let spine = spine.iter().map(|x| self.erase_expr(on, x)).collect(); + let spine = spine.iter().map(|x| { + let on = if x.erased { + (x.data.span.to_range(), Relevance::Irrelevant) + } else { + on.clone() + }; + desugared::AppBinding { + data: self.erase_expr(&on, &x.data), + erased: x.erased + } + }).filter(|x| !x.erased).collect(); Box::new(Expr { span: expr.span, data: ExprKind::App(head, spine), @@ -414,26 +443,22 @@ impl<'a> ErasureState<'a> { ) -> Rule { let ctx = self.ctx.clone(); - args.iter() + let new_pats : Vec<_> = args.iter() .zip(rule.pats.iter()) - .for_each(|((range, erased), expr)| { - self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr) - }); + .map(|((range, erased), expr)| { + (erased, self.erase_pat((Some(*range), erasure_to_relevance(*erased)), expr)) + }) + .filter(|(erased, _)| !*erased) + .map(|res| res.1) + .collect(); let body = self.erase_expr(place, &rule.body); self.ctx = ctx; - let new_pats = args - .iter() - .zip(rule.pats.iter()) - .filter(|((_, erased), _)| !*erased) - .map(|res| res.1) - .cloned(); - Rule { name: rule.name.clone(), - pats: new_pats.collect(), + pats: new_pats, body, span: rule.span, } diff --git a/src/kind-pass/src/unbound/mod.rs b/src/kind-pass/src/unbound/mod.rs index a20677c7..8230ee63 100644 --- a/src/kind-pass/src/unbound/mod.rs +++ b/src/kind-pass/src/unbound/mod.rs @@ -372,7 +372,7 @@ impl Visitor for UnboundCollector { } ExprKind::App(head, spine) => { self.visit_expr(head); - visit_vec!(spine.iter_mut(), arg => self.visit_binding(arg)); + visit_vec!(spine.iter_mut(), arg => self.visit_expr(&mut arg.data)); } ExprKind::Ann(val, ty) => { self.visit_expr(val); diff --git a/src/kind-span/src/lib.rs b/src/kind-span/src/lib.rs index 364a45a6..40c91266 100644 --- a/src/kind-span/src/lib.rs +++ b/src/kind-span/src/lib.rs @@ -95,6 +95,13 @@ impl Span { Span::Generated } + pub fn to_range(&self) -> Option { + match self { + Span::Generated => None, + Span::Locatable(pos) => Some(pos.clone()), + } + } + /// Join two spans and keeps the syntax context of the /// first locatable range. If it's generated then it /// will be ignored and the other span will be the canonical diff --git a/src/kind-target-hvm/src/lib.rs b/src/kind-target-hvm/src/lib.rs index 577413eb..c1f0b336 100644 --- a/src/kind-target-hvm/src/lib.rs +++ b/src/kind-target-hvm/src/lib.rs @@ -16,7 +16,7 @@ pub fn compile_term(expr: &desugared::Expr) -> Box { App(head, spine) => spine.iter().fold(compile_term(head), |func, arg| { Box::new(Term::App { func, - argm: compile_term(arg), + argm: compile_term(&arg.data), }) }), Fun(head, spine) | Ctr(head, spine) => Box::new(Term::Ctr { diff --git a/src/kind-tree/src/concrete/expr.rs b/src/kind-tree/src/concrete/expr.rs index d01c3fdf..32ddf907 100644 --- a/src/kind-tree/src/concrete/expr.rs +++ b/src/kind-tree/src/concrete/expr.rs @@ -24,6 +24,21 @@ pub enum Binding { /// Vector of bindings pub type Spine = Vec; +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +pub struct AppBinding { + pub data: Box, + pub erased: bool +} + +impl AppBinding { + pub fn explicit(data: Box) -> AppBinding { + AppBinding { + data, + erased: false, + } + } +} + /// A case binding is a field or a rename of some field /// inside a match expression. #[derive(Clone, Debug, Hash, PartialEq, Eq)] @@ -121,7 +136,7 @@ pub enum ExprKind { /// A anonymous function that receives one argument Lambda(Ident, Option>, Box), /// Application of a expression to a spine of expressions - App(Box, Spine), + App(Box, Vec), /// Declaration of a local variable Let(Destruct, Box, Box), /// Type ascription (x : y) @@ -362,6 +377,16 @@ impl Display for Binding { } } +impl Display for AppBinding { + fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { + if self.erased { + write!(f, "{{{}}}", self.data) + } else { + write!(f, "{}", self.data) + } + } +} + impl Display for Expr { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { use ExprKind::*; diff --git a/src/kind-tree/src/concrete/visitor.rs b/src/kind-tree/src/concrete/visitor.rs index b35e995c..6fffb576 100644 --- a/src/kind-tree/src/concrete/visitor.rs +++ b/src/kind-tree/src/concrete/visitor.rs @@ -35,6 +35,7 @@ macro_rules! visit_opt { } use kind_span::{Range, SyntaxCtxIndex}; + pub(crate) use visit_opt; pub(crate) use visit_vec; @@ -71,6 +72,10 @@ pub trait Visitor: Sized { walk_ident(self, ident); } + fn visit_app_binding(&mut self, ident: &mut AppBinding) { + walk_app_binding(self, ident); + } + fn visit_destruct(&mut self, ident: &mut Destruct) { walk_destruct(self, ident); } @@ -186,6 +191,10 @@ pub fn walk_binding(ctx: &mut T, binding: &mut Binding) { } } +pub fn walk_app_binding(ctx: &mut T, binding: &mut AppBinding) { + ctx.visit_expr(&mut binding.data) +} + pub fn walk_case_binding(ctx: &mut T, binding: &mut CaseBinding) { match binding { CaseBinding::Field(ident) => ctx.visit_pat_ident(ident), @@ -413,7 +422,7 @@ pub fn walk_expr(ctx: &mut T, expr: &mut Expr) { ExprKind::App(expr, spine) => { ctx.visit_expr(expr); for arg in spine { - ctx.visit_binding(arg); + ctx.visit_app_binding(arg); } } ExprKind::List(spine) => { diff --git a/src/kind-tree/src/desugared/mod.rs b/src/kind-tree/src/desugared/mod.rs index bb649cbe..8bced2e4 100644 --- a/src/kind-tree/src/desugared/mod.rs +++ b/src/kind-tree/src/desugared/mod.rs @@ -17,6 +17,12 @@ use crate::{ /// as ((((a b) c) d) e) that looks like a spine. pub type Spine = Vec>; +#[derive(Clone, Debug, Hash, PartialEq, Eq)] +pub struct AppBinding { + pub data: Box, + pub erased: bool +} + #[derive(Clone, Debug, Hash, PartialEq, Eq)] pub enum ExprKind { /// Name of a variable @@ -26,7 +32,7 @@ pub enum ExprKind { /// A anonymous function that receives one argument Lambda(Ident, Box), /// Application of a expression to a spine of expressions - App(Box, Spine), + App(Box, Vec), /// Application of a function Fun(QualifiedIdent, Spine), /// Application of a Construtor @@ -113,7 +119,7 @@ impl Expr { .fold(body, |body, ident| Expr::lambda(range, ident.clone(), body)) } - pub fn app(range: Range, ident: Box, spine: Vec>) -> Box { + pub fn app(range: Range, ident: Box, spine: Vec) -> Box { Box::new(Expr { span: Span::Locatable(range), data: ExprKind::App(ident, spine), @@ -306,6 +312,16 @@ impl Expr { } } +impl Display for AppBinding { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + if self.erased { + write!(f, "{{{}}}", self.data) + } else { + write!(f, "{}", self.data) + } + } +} + impl Display for Expr { fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> { use ExprKind::*;