mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-08-15 19:30:41 +03:00
fix: a lot of bug fixes
This commit is contained in:
parent
ba3aff95d6
commit
56f5d88d4f
@ -129,7 +129,6 @@ fn codegen_all_expr(
|
||||
expr: &Expr,
|
||||
) -> Box<Term> {
|
||||
use kind_tree::desugared::ExprKind::*;
|
||||
|
||||
match &expr.data {
|
||||
Typ => mk_lifted_ctr(eval_ctr(quote, TermTag::Typ), vec![span_to_num(expr.span)]),
|
||||
NumType(kind_tree::NumType::U60) => {
|
||||
@ -251,8 +250,8 @@ fn codegen_all_expr(
|
||||
Binary(operator, left, right) => mk_lifted_ctr(
|
||||
eval_ctr(quote, TermTag::Binary),
|
||||
vec![
|
||||
mk_single_ctr(operator_to_constructor(*operator).to_owned()),
|
||||
span_to_num(expr.span),
|
||||
mk_single_ctr(operator_to_constructor(*operator).to_owned()),
|
||||
codegen_all_expr(lhs_rule, lhs, num, quote, left),
|
||||
codegen_all_expr(lhs_rule, lhs, num, quote, right),
|
||||
],
|
||||
@ -262,7 +261,7 @@ fn codegen_all_expr(
|
||||
vec![span_to_num(expr.span), mk_u60(*num)],
|
||||
),
|
||||
Hlp(_) => mk_lifted_ctr(eval_ctr(quote, TermTag::Hlp), vec![span_to_num(expr.span)]),
|
||||
Str(input) => codegen_str(input),
|
||||
Str(_) => todo!("Strings in codegen"),
|
||||
Err => panic!("Internal Error: Was not expecting an ERR node inside the HVM checker"),
|
||||
}
|
||||
}
|
||||
|
@ -8,7 +8,7 @@ license = "MIT"
|
||||
keywords = ["functional", "language", "type-theory", "proof-assistant"]
|
||||
|
||||
[[bin]]
|
||||
name = "kind2"
|
||||
name = "kind"
|
||||
path = "src/main.rs"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
@ -268,7 +268,6 @@ pub fn check_unbound_top_level(session: &mut Session, book: &mut Book) -> bool {
|
||||
for (_, unbound) in unbound_tops {
|
||||
let res: Vec<Ident> = unbound
|
||||
.iter()
|
||||
.filter(|x| !x.used_by_sugar)
|
||||
.map(|x| x.to_ident())
|
||||
.collect();
|
||||
if !res.is_empty() {
|
||||
|
@ -302,7 +302,7 @@ impl<'a> Parser<'a> {
|
||||
}));
|
||||
}
|
||||
|
||||
vec.push(*self.parse_expr(false)?);
|
||||
vec.push(*self.parse_atom()?);
|
||||
let mut initialized = false;
|
||||
let mut with_comma = false;
|
||||
|
||||
@ -572,7 +572,7 @@ impl<'a> Parser<'a> {
|
||||
if self.get().same_variant(&Token::RBrace) {
|
||||
let end = expr.range;
|
||||
Ok(Box::new(Sttm {
|
||||
data: SttmKind::Return(expr),
|
||||
data: SttmKind::RetExpr(expr),
|
||||
range: start.mix(end),
|
||||
}))
|
||||
} else {
|
||||
|
@ -241,9 +241,7 @@ impl<'a> DesugarState<'a> {
|
||||
let motive = if let Some(res) = &match_.motive {
|
||||
self.desugar_expr(res)
|
||||
} else {
|
||||
let mut idx: Vec<Ident> = sum
|
||||
.parameters
|
||||
.extend(&sum.indices)
|
||||
let mut idx: Vec<Ident> = sum.indices
|
||||
.iter()
|
||||
.map(|x| x.name.clone())
|
||||
.collect();
|
||||
|
@ -8,6 +8,21 @@ use crate::errors::{PassError, Sugar};
|
||||
use super::DesugarState;
|
||||
|
||||
impl<'a> DesugarState<'a> {
|
||||
|
||||
pub(crate) fn desugar_str(&self, range: Range, input: &str) -> Box<desugared::Expr> {
|
||||
let cons = QualifiedIdent::new_static("String.cons", None, range);
|
||||
input.chars().rfold(
|
||||
desugared::Expr::ctr(range, QualifiedIdent::new_static("String.nil", None, range), vec![]),
|
||||
|right, chr| {
|
||||
desugared::Expr::ctr(range, cons.clone(), vec![
|
||||
desugared::Expr::num60(range, chr as u64),
|
||||
right
|
||||
])
|
||||
},
|
||||
)
|
||||
}
|
||||
|
||||
|
||||
pub(crate) fn desugar_literal(
|
||||
&mut self,
|
||||
range: Range,
|
||||
@ -20,7 +35,7 @@ impl<'a> DesugarState<'a> {
|
||||
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.to_owned()),
|
||||
Literal::String(string) => self.desugar_str(range, string),
|
||||
Literal::Char(cht) => desugared::Expr::num60(range, *cht as u64),
|
||||
}
|
||||
}
|
||||
@ -191,9 +206,10 @@ impl<'a> DesugarState<'a> {
|
||||
if_: &expr::Expr,
|
||||
else_: &expr::Expr,
|
||||
) -> Box<desugared::Expr> {
|
||||
let bool_ident = QualifiedIdent::new_sugared("Bool", "if", range);
|
||||
let boolean = QualifiedIdent::new_static("Bool", None, range);
|
||||
let bool_if_ident = boolean.add_segment("if");
|
||||
|
||||
let bool_if = self.old_book.entries.get(bool_ident.to_string().as_str());
|
||||
let bool_if = self.old_book.entries.get(bool_if_ident.to_string().as_str());
|
||||
|
||||
if bool_if.is_none() {
|
||||
self.send_err(PassError::NeedToImplementMethods(range, Sugar::BoolIf));
|
||||
@ -206,7 +222,7 @@ impl<'a> DesugarState<'a> {
|
||||
self.desugar_expr(else_),
|
||||
];
|
||||
|
||||
self.mk_desugared_fun(range, bool_ident, spine, false)
|
||||
self.mk_desugared_fun(range, bool_if_ident, spine, false)
|
||||
}
|
||||
|
||||
pub(crate) fn desugar_pair(
|
||||
|
@ -393,7 +393,7 @@ impl Display for Expr {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
use ExprKind::*;
|
||||
match &self.data {
|
||||
Do(id, sttms) => write!(f, "do {} ({})", id, sttms),
|
||||
Do(id, sttms) => write!(f, "do {} {{{}}}", id, sttms),
|
||||
All(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
|
||||
Sigma(_, _, _) => write!(f, "({})", self.traverse_pi_types()),
|
||||
Lit(lit) => write!(f, "{}", lit),
|
||||
|
@ -80,10 +80,10 @@ impl QualifiedIdent {
|
||||
}
|
||||
}
|
||||
|
||||
pub fn new_sugared(root: &str, aux: &str, range: Range) -> QualifiedIdent {
|
||||
pub fn new_sugared(root: &str, extension: &str, range: Range) -> QualifiedIdent {
|
||||
QualifiedIdent {
|
||||
root: Symbol(root.to_string()),
|
||||
aux: Some(Symbol(aux.to_string())),
|
||||
root: Symbol(format!("{}.{}", root, extension)),
|
||||
aux: None,
|
||||
range,
|
||||
used_by_sugar: true,
|
||||
generated: true,
|
||||
|
Loading…
Reference in New Issue
Block a user