Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-10-05 20:07:27 +03:00
Code Issues Projects Releases Wiki Activity

merge: pull request #575 from HigherOrderCO/572-update-basic-function-names-for-kindex-update

Browse Source 
Update basic function names for kindex update
This commit is contained in:
Sofia Rodrigues 2023-05-11 08:30:26 -03:00 committed by GitHub
commit 678bcf4353
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
134 changed files with 1638 additions and 1638 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
crates/kind-checker/Cargo.toml
View File

@ -3,16 +3,16 @@ description = "Type checker for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-checker"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
hvm = "1.0.6"
hvm = "1.0.8"
fxhash = "0.2.1"
im-rc = "15.1.0"

1694
crates/kind-checker/src/checker.hvm
View File

File diff suppressed because it is too large Load Diff

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

@ -44,7 +44,7 @@ fn lift_spine(spine: Vec<Box<Term>>) -> Vec<Box<Term>> {
if spine.len() > 16 {
let mut start = spine[..2].to_vec();
start.push(Box::new(Term::Ctr {
name: format!("Kind.Term.args{}", spine.len() - 2),
name: format!("Apps.Kind.Term.args{}", spine.len() - 2),
args: spine[2..].to_vec(),
}));
start
@ -101,7 +101,7 @@ fn range_to_num(lhs: bool, range: Range) -> Box<Term> {
fn set_origin(ident: &Ident) -> Box<Term> {
mk_lifted_ctr(
"Kind.Term.set_origin".to_owned(),
"Apps.Kind.Term.set_origin".to_owned(),
vec![range_to_num(false, ident.range), mk_var(ident.to_str())],
)
}
@ -114,8 +114,8 @@ fn lam(name: &Ident, body: Box<Term>) -> Box<Term> {
}
fn desugar_str(input: &str, range: Range) -> Box<desugared::Expr> {
let nil = QualifiedIdent::new_static("String.nil", None, range);
let cons = QualifiedIdent::new_static("String.cons", None, range);
let nil = QualifiedIdent::new_static("Data.String.nil", None, range);
let cons = QualifiedIdent::new_static("Data.String.cons", None, range);
input
.chars()
.rfold(desugared::Expr::ctr(range, nil, vec![]), |right, chr| {
@ -132,12 +132,12 @@ fn desugar_str(input: &str, range: Range) -> Box<desugared::Expr> {
fn codegen_str(input: &str) -> Box<Term> {
input.chars().rfold(
Box::new(Term::Ctr {
name: "String.nil".to_string(),
name: "Data.String.nil".to_string(),
args: vec![],
}),
|right, chr| {
Box::new(Term::Ctr {
name: "String.cons".to_string(),
name: "Data.String.cons".to_string(),
args: vec![mk_u60(chr as u64), right],
})
},
@ -339,8 +339,8 @@ fn codegen_vec<T>(exprs: T) -> Box<Term>
where
T: DoubleEndedIterator<Item = Box<Term>>,
{
exprs.rfold(mk_ctr("List.nil".to_string(), vec![]), |left, right| {
mk_ctr("List.cons".to_string(), vec![right, left])
exprs.rfold(mk_ctr("Data.List.nil".to_string(), vec![]), |left, right| {
mk_ctr("Data.List.cons".to_string(), vec![right, left])
})
}
@ -406,7 +406,7 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) {
rhs: codegen_expr(true, &rule.body),
});
if rule.name.to_string().as_str() == "HVM.log" {
if rule.name.to_string().as_str() == "Apps.HVM.log" {
file.rules.push(lang::Rule {
lhs: mk_ctr(
TermTag::HoasF(rule.name.to_string()).to_string(),
@ -419,9 +419,9 @@ fn codegen_rule(file: &mut lang::File, rule: &desugared::Rule) {
],
),
rhs: mk_ctr(
"HVM.print".to_owned(),
"Apps.HVM.print".to_owned(),
vec![
mk_ctr("Kind.Term.show".to_owned(), vec![mk_var("log")]),
mk_ctr("Apps.Kind.Term.show".to_owned(), vec![mk_var("log")]),
mk_var("ret"),
],
),
@ -449,7 +449,7 @@ fn codegen_entry_rules(
) -> Box<Term> {
if pats.is_empty() {
mk_ctr(
"Kind.Rule.rhs".to_owned(),
"Apps.Kind.Rule.rhs".to_owned(),
vec![mk_ctr(
format!("QT{}", index),
vec_preppend![
@ -464,7 +464,7 @@ fn codegen_entry_rules(
let expr = codegen_all_expr(true, false, count, false, pat);
args.push(expr.clone());
mk_ctr(
"Kind.Rule.lhs".to_owned(),
"Apps.Kind.Rule.lhs".to_owned(),
vec![
expr,
codegen_entry_rules(count, index + 1, args, entry, &pats[1..]),
@ -476,7 +476,7 @@ fn codegen_entry_rules(
fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.NameOf".to_owned(),
"Apps.Kind.Axiom.NameOf".to_owned(),
vec![mk_ctr_name(&entry.name)],
),
rhs: codegen_str(entry.name.to_string().as_str()),
@ -484,7 +484,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.OrigOf".to_owned(),
"Apps.Kind.Axiom.OrigOf".to_owned(),
vec![mk_ctr_name(&entry.name)],
),
rhs: range_to_num(false, entry.name.range),
@ -492,7 +492,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.HashOf".to_owned(),
"Apps.Kind.Axiom.HashOf".to_owned(),
vec![mk_ctr_name(&entry.name)],
),
rhs: mk_u60(fxhash::hash64(entry.name.to_string().as_str())),
@ -500,7 +500,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.TypeOf".to_owned(),
"Apps.Kind.Axiom.TypeOf".to_owned(),
vec![mk_ctr_name(&entry.name)],
),
rhs: codegen_type(&entry.args, &entry.typ),
@ -512,7 +512,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
file.rules.push(lang::Rule {
lhs: mk_lifted_ctr(
format!("Kind.Term.FN{}", entry.args.len()),
format!("Apps.Kind.Term.FN{}", entry.args.len()),
vec_preppend![
mk_ctr_name(&entry.name),
mk_var("orig");
@ -561,7 +561,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.RuleOf".to_owned(),
"Apps.Kind.Axiom.RuleOf".to_owned(),
vec![mk_ctr_name(&entry.name)],
),
rhs: codegen_vec(rules),
@ -573,10 +573,10 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
if !entry.rules.is_empty() && !entry.rules[0].pats.is_empty() && !entry.attrs.partial && !entry.attrs.axiom {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.CoverCheck".to_owned(),
"Apps.Kind.Axiom.CoverCheck".to_owned(),
vec![mk_ctr_name(&entry.name)],
),
rhs: mk_single_ctr("Bool.true".to_string()),
rhs: mk_single_ctr("Data.Bool.true".to_string()),
});
}
}
@ -584,15 +584,15 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
for family in book.families.values() {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Family.Constructors".to_owned(),
"Apps.Kind.Axiom.Family.Constructors".to_owned(),
vec![mk_ctr_name(&family.name)],
),
rhs: mk_ctr("Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(mk_ctr_name))]),
rhs: mk_ctr("Data.Maybe.some".to_string(), vec![codegen_vec(family.constructors.iter().map(mk_ctr_name))]),
});
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Family.Params".to_owned(),
"Apps.Kind.Axiom.Family.Params".to_owned(),
vec![mk_ctr_name(&family.name)],
),
rhs: mk_u60(family.parameters.len() as u64),
@ -613,7 +613,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
let entry = book.entrs.get(constructor.to_str()).unwrap();
let mut maker = mk_ctr(
"Kind.Coverage.Maker.End".to_string(),
"Apps.Kind.Coverage.Maker.End".to_string(),
vec![codegen_expr(
false,
&kind_tree::desugared::Expr::ctr(
@ -630,7 +630,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
for arg in entry.args[family.parameters.len()..].iter().rev() {
maker = mk_ctr(
"Kind.Coverage.Maker.Cons".to_string(),
"Apps.Kind.Coverage.Maker.Cons".to_string(),
vec![
range_to_num(false, arg.range),
codegen_all_expr(false, false, &mut 0, false, &arg.typ),
@ -641,7 +641,7 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Coverage.Maker.Mk".to_owned(),
"Apps.Kind.Coverage.Maker.Mk".to_owned(),
vec![
mk_ctr_name(constructor),
mk_var("orig"),
@ -655,20 +655,20 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
),
],
),
rhs: mk_ctr("Maybe.some".to_string(), vec![maker]),
rhs: mk_ctr("Data.Maybe.some".to_string(), vec![maker]),
});
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Compare".to_owned(),
"Apps.Kind.Axiom.Compare".to_owned(),
vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
),
rhs: mk_single_ctr("Bool.true".to_string()),
rhs: mk_single_ctr("Data.Bool.true".to_string()),
});
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.ArgsCount".to_owned(),
"Apps.Kind.Axiom.ArgsCount".to_owned(),
vec![mk_ctr_name(constructor)],
),
rhs: mk_u60(entry.args.len() as u64),
@ -676,10 +676,10 @@ pub fn codegen_coverage(file: &mut lang::File, book: &Book) {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Compare".to_owned(),
"Apps.Kind.Axiom.Compare".to_owned(),
vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
),
rhs: mk_single_ctr("Bool.true".to_string()),
rhs: mk_single_ctr("Data.Bool.true".to_string()),
});
}
}
@ -694,7 +694,7 @@ pub fn codegen_book(book: &Book, check_coverage: bool, functions_to_check: Vec<S
};
let functions_entry = lang::Rule {
lhs: mk_ctr("Kind.Axiom.Functions".to_owned(), vec![]),
lhs: mk_ctr("Apps.Kind.Axiom.Functions".to_owned(), vec![]),
rhs: codegen_vec(functions_to_check.iter().map(|x| mk_ctr_name_from_str(x))),
};
@ -723,30 +723,30 @@ pub fn codegen_book(book: &Book, check_coverage: bool, functions_to_check: Vec<S
}
file.rules.push(lang::Rule {
lhs: mk_ctr("Kind.Axiom.CoverCheck".to_owned(), vec![mk_var("_")]),
rhs: mk_single_ctr("Bool.false".to_string()),
lhs: mk_ctr("Apps.Kind.Axiom.CoverCheck".to_owned(), vec![mk_var("_")]),
rhs: mk_single_ctr("Data.Bool.false".to_string()),
});
if check_coverage {
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Axiom.Compare".to_owned(),
"Apps.Kind.Axiom.Compare".to_owned(),
vec![mk_var("a"), mk_var("b")],
),
rhs: mk_single_ctr("Bool.false".to_string()),
rhs: mk_single_ctr("Data.Bool.false".to_string()),
});
file.rules.push(lang::Rule {
lhs: mk_ctr(
"Kind.Coverage.Maker.Mk".to_owned(),
"Apps.Kind.Coverage.Maker.Mk".to_owned(),
vec![mk_var("cons"), mk_var("a"), mk_var("b")],
),
rhs: mk_single_ctr("Maybe.none".to_string()),
rhs: mk_single_ctr("Data.Maybe.none".to_string()),
});
file.rules.push(lang::Rule {
lhs: mk_ctr("Kind.Axiom.Family.Constructors".to_owned(), vec![mk_var("_")]),
rhs: mk_single_ctr("Maybe.none".to_string()),
lhs: mk_ctr("Apps.Kind.Axiom.Family.Constructors".to_owned(), vec![mk_var("_")]),
rhs: mk_single_ctr("Data.Maybe.none".to_string()),
});
}

72
crates/kind-checker/src/compiler/tags.rs
View File

@ -46,21 +46,21 @@ pub enum EvalTag {
impl fmt::Display for TermTag {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
TermTag::Var => write!(f, "Kind.Term.var"),
TermTag::All => write!(f, "Kind.Term.all"),
TermTag::Lambda => write!(f, "Kind.Term.lam"),
TermTag::App => write!(f, "Kind.Term.app"),
TermTag::Fun(n) => write!(f, "Kind.Term.fn{}", n),
TermTag::Ctr(n) => write!(f, "Kind.Term.ct{}", n),
TermTag::Let => write!(f, "Kind.Term.let"),
TermTag::Ann => write!(f, "Kind.Term.ann"),
TermTag::Sub => write!(f, "Kind.Term.sub"),
TermTag::Typ => write!(f, "Kind.Term.typ"),
TermTag::U60 => write!(f, "Kind.Term.U60"),
TermTag::NUMU60 => write!(f, "Kind.Term.u60"),
TermTag::Binary => write!(f, "Kind.Term.op2"),
TermTag::Hole => write!(f, "Kind.Term.hol"),
TermTag::Hlp => write!(f, "Kind.Term.hlp"),
TermTag::Var => write!(f, "Apps.Kind.Term.var"),
TermTag::All => write!(f, "Apps.Kind.Term.all"),
TermTag::Lambda => write!(f, "Apps.Kind.Term.lam"),
TermTag::App => write!(f, "Apps.Kind.Term.app"),
TermTag::Fun(n) => write!(f, "Apps.Kind.Term.fn{}", n),
TermTag::Ctr(n) => write!(f, "Apps.Kind.Term.ct{}", n),
TermTag::Let => write!(f, "Apps.Kind.Term.let"),
TermTag::Ann => write!(f, "Apps.Kind.Term.ann"),
TermTag::Sub => write!(f, "Apps.Kind.Term.sub"),
TermTag::Typ => write!(f, "Apps.Kind.Term.typ"),
TermTag::U60 => write!(f, "Apps.Kind.Term.U60"),
TermTag::NUMU60 => write!(f, "Apps.Kind.Term.u60"),
TermTag::Binary => write!(f, "Apps.Kind.Term.op2"),
TermTag::Hole => write!(f, "Apps.Kind.Term.hol"),
TermTag::Hlp => write!(f, "Apps.Kind.Term.hlp"),
TermTag::HoasF(name) => write!(f, "F${}", name),
TermTag::HoasQ(name) => write!(f, "Q${}", name),
}
@ -70,11 +70,11 @@ impl fmt::Display for TermTag {
impl fmt::Display for EvalTag {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
EvalTag::Op => write!(f, "Kind.Term.eval_op"),
EvalTag::App => write!(f, "Kind.Term.eval_app"),
EvalTag::Let => write!(f, "Kind.Term.eval_let"),
EvalTag::Ann => write!(f, "Kind.Term.eval_ann"),
EvalTag::Sub => write!(f, "Kind.Term.eval_sub"),
EvalTag::Op => write!(f, "Apps.Kind.Term.eval_op"),
EvalTag::App => write!(f, "Apps.Kind.Term.eval_app"),
EvalTag::Let => write!(f, "Apps.Kind.Term.eval_let"),
EvalTag::Ann => write!(f, "Apps.Kind.Term.eval_ann"),
EvalTag::Sub => write!(f, "Apps.Kind.Term.eval_sub"),
}
}
}
@ -83,21 +83,21 @@ impl fmt::Display for EvalTag {
/// by the checker.
pub fn operator_to_constructor<'a>(operator: Operator) -> &'a str {
match operator {
Operator::Add => "Kind.Operator.add",
Operator::Sub => "Kind.Operator.sub",
Operator::Mul => "Kind.Operator.mul",
Operator::Div => "Kind.Operator.div",
Operator::Mod => "Kind.Operator.mod",
Operator::And => "Kind.Operator.and",
Operator::Xor => "Kind.Operator.xor",
Operator::Shl => "Kind.Operator.shl",
Operator::Shr => "Kind.Operator.shr",
Operator::Ltn => "Kind.Operator.ltn",
Operator::Lte => "Kind.Operator.lte",
Operator::Eql => "Kind.Operator.eql",
Operator::Gte => "Kind.Operator.gte",
Operator::Gtn => "Kind.Operator.gtn",
Operator::Neq => "Kind.Operator.neq",
Operator::Or => "Kind.Operator.or",
Operator::Add => "Apps.Kind.Operator.add",
Operator::Sub => "Apps.Kind.Operator.sub",
Operator::Mul => "Apps.Kind.Operator.mul",
Operator::Div => "Apps.Kind.Operator.div",
Operator::Mod => "Apps.Kind.Operator.mod",
Operator::And => "Apps.Kind.Operator.and",
Operator::Xor => "Apps.Kind.Operator.xor",
Operator::Shl => "Apps.Kind.Operator.shl",
Operator::Shr => "Apps.Kind.Operator.shr",
Operator::Ltn => "Apps.Kind.Operator.ltn",
Operator::Lte => "Apps.Kind.Operator.lte",
Operator::Eql => "Apps.Kind.Operator.eql",
Operator::Gte => "Apps.Kind.Operator.gte",
Operator::Gtn => "Apps.Kind.Operator.gtn",
Operator::Neq => "Apps.Kind.Operator.neq",
Operator::Or => "Apps.Kind.Operator.or",
}
}

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

@ -110,7 +110,7 @@ pub fn eval_api(book: &Book) -> (String, u64) {
runtime::link(
&heap,
0,
runtime::Fun(*book.name_to_id.get("Kind.API.eval_main").unwrap(), 0),
runtime::Fun(*book.name_to_id.get("Apps.Kind.API.eval_main").unwrap(), 0),
);
let host = 0;

88
crates/kind-checker/src/report.rs
View File

@ -35,22 +35,22 @@ fn parse_num(term: &Term) -> Result<u64, String> {
fn parse_op(term: &Term) -> Result<Operator, String> {
match term {
Term::Ctr { name, args: _ } => match name.as_str() {
"Kind.Operator.add" => Ok(Operator::Add),
"Kind.Operator.sub" => Ok(Operator::Sub),
"Kind.Operator.mul" => Ok(Operator::Mul),
"Kind.Operator.div" => Ok(Operator::Div),
"Kind.Operator.mod" => Ok(Operator::Mod),
"Kind.Operator.and" => Ok(Operator::And),
"Kind.Operator.or" => Ok(Operator::Or),
"Kind.Operator.xor" => Ok(Operator::Xor),
"Kind.Operator.shl" => Ok(Operator::Shl),
"Kind.Operator.shr" => Ok(Operator::Shr),
"Kind.Operator.ltn" => Ok(Operator::Ltn),
"Kind.Operator.lte" => Ok(Operator::Lte),
"Kind.Operator.eql" => Ok(Operator::Eql),
"Kind.Operator.gte" => Ok(Operator::Gte),
"Kind.Operator.gtn" => Ok(Operator::Gtn),
"Kind.Operator.neq" => Ok(Operator::Neq),
"Apps.Kind.Operator.add" => Ok(Operator::Add),
"Apps.Kind.Operator.sub" => Ok(Operator::Sub),
"Apps.Kind.Operator.mul" => Ok(Operator::Mul),
"Apps.Kind.Operator.div" => Ok(Operator::Div),
"Apps.Kind.Operator.mod" => Ok(Operator::Mod),
"Apps.Kind.Operator.and" => Ok(Operator::And),
"Apps.Kind.Operator.or" => Ok(Operator::Or),
"Apps.Kind.Operator.xor" => Ok(Operator::Xor),
"Apps.Kind.Operator.shl" => Ok(Operator::Shl),
"Apps.Kind.Operator.shr" => Ok(Operator::Shr),
"Apps.Kind.Operator.ltn" => Ok(Operator::Ltn),
"Apps.Kind.Operator.lte" => Ok(Operator::Lte),
"Apps.Kind.Operator.eql" => Ok(Operator::Eql),
"Apps.Kind.Operator.gte" => Ok(Operator::Gte),
"Apps.Kind.Operator.gtn" => Ok(Operator::Gtn),
"Apps.Kind.Operator.neq" => Ok(Operator::Neq),
_ => Err("Cannot recognized operator".to_string()),
},
_ => Err("Error parsing operator".to_string()),
@ -91,44 +91,44 @@ fn parse_all_expr(
) -> Result<Box<desugared::Expr>, String> {
match term {
Term::Ctr { name, args } => match name.as_str() {
"Kind.Term.Quoted.all" => Ok(Expr::all(
"Apps.Kind.Term.Quoted.all" => Ok(Expr::all(
parse_orig(&args[0])?,
Ident::generate(&parse_name(&args[1])?),
parse_all_expr(names.clone(), &args[2])?,
parse_all_expr(names, &args[3])?,
false, // TODO: Fix
)),
"Kind.Term.Quoted.lam" => Ok(Expr::lambda(
"Apps.Kind.Term.Quoted.lam" => Ok(Expr::lambda(
parse_orig(&args[0])?,
Ident::generate(&parse_name(&args[1])?),
parse_all_expr(names, &args[2])?,
false, // TODO: Fix
)),
"Kind.Term.Quoted.let" => Ok(Expr::let_(
"Apps.Kind.Term.Quoted.let" => Ok(Expr::let_(
parse_orig(&args[0])?,
Ident::generate(&parse_name(&args[1])?),
parse_all_expr(names.clone(), &args[2])?,
parse_all_expr(names, &args[3])?,
)),
"Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
"Kind.Term.Quoted.var" => Ok(Expr::var(Ident::new(
"Apps.Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
"Apps.Kind.Term.Quoted.var" => Ok(Expr::var(Ident::new(
parse_name(&args[1])?,
parse_orig(&args[0])?,
))),
"Kind.Term.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)),
"Kind.Term.Quoted.ann" => Ok(Expr::ann(
"Apps.Kind.Term.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)),
"Apps.Kind.Term.Quoted.ann" => Ok(Expr::ann(
parse_orig(&args[0])?,
parse_all_expr(names.clone(), &args[1])?,
parse_all_expr(names, &args[2])?,
)),
"Kind.Term.Quoted.sub" => Ok(Expr::sub(
"Apps.Kind.Term.Quoted.sub" => Ok(Expr::sub(
parse_orig(&args[0])?,
Ident::generate(&parse_name(&args[1])?),
parse_num(&args[2])? as usize,
parse_num(&args[3])? as usize,
parse_all_expr(names, &args[4])?,
)),
"Kind.Term.Quoted.app" => Ok(Expr::app(
"Apps.Kind.Term.Quoted.app" => Ok(Expr::app(
parse_orig(&args[0])?,
parse_all_expr(names.clone(), &args[1])?,
vec![desugared::AppBinding {
@ -136,7 +136,7 @@ fn parse_all_expr(
erased: false,
}],
)),
"Kind.Term.Quoted.ctr" => {
"Apps.Kind.Term.Quoted.ctr" => {
let name = parse_qualified(&args[0])?;
let orig = parse_orig(&args[1])?;
let mut res = Vec::new();
@ -145,7 +145,7 @@ fn parse_all_expr(
}
Ok(Expr::ctr(orig, name, res))
}
"Kind.Term.Quoted.fun" => Ok(Expr::fun(
"Apps.Kind.Term.Quoted.fun" => Ok(Expr::fun(
parse_orig(&args[1])?,
parse_qualified(&args[0])?,
{
@ -156,11 +156,11 @@ fn parse_all_expr(
res
},
)),
"Kind.Term.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
"Kind.Term.Quoted.u60" => Ok(Expr::type_u60(parse_orig(&args[0])?)),
"Kind.Term.Quoted.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)),
"Apps.Kind.Term.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
"Apps.Kind.Term.Quoted.u60" => Ok(Expr::type_u60(parse_orig(&args[0])?)),
"Apps.Kind.Term.Quoted.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)),
// TODO: Change quoting to support floats
"Kind.Term.Quoted.op2" => Ok(Expr::binary(
"Apps.Kind.Term.Quoted.op2" => Ok(Expr::binary(
parse_orig(&args[0])?,
parse_op(&args[1])?,
parse_all_expr(names.clone(), &args[2])?,
@ -181,9 +181,9 @@ fn parse_list(term: &Term) -> Result<Vec<Box<Term>>, String> {
loop {
match cur {
Term::Ctr { name, args } => {
if name == "List.nil" {
if name == "Data.List.nil" {
break;
} else if name == "List.cons" {
} else if name == "Data.List.cons" {
vec.push(args[0].clone());
cur = &args[1];
} else {
@ -199,10 +199,10 @@ fn parse_list(term: &Term) -> Result<Vec<Box<Term>>, String> {
/// Transforms a HVM quoted entry into a easy to manipulate structure.
pub fn transform_entry(term: &Term) -> Result<Entry, String> {
match term {
Term::Ctr { name, args } if name == "Pair.new" => {
Term::Ctr { name, args } if name == "Data.Pair.new" => {
let fst = parse_name(&args[0])?;
match &*args[1] {
Term::Ctr { name, args } if name == "Pair.new" => {
Term::Ctr { name, args } if name == "Data.Pair.new" => {
let snd = parse_expr(&args[0])?;
let trd = parse_list(&args[1])?;
let trd = trd.iter().flat_map(|x| parse_expr(x)).collect();
@ -226,7 +226,7 @@ fn parse_type_error(expr: &Term) -> Result<TypeDiagnostic, String> {
let ctx = Context(entries.collect());
let orig = match_opt!(*args[1], Term::U6O { numb } => EncodedRange(numb).to_range())?;
match name.as_str() {
"Kind.Error.Quoted.uncovered_pattern" => Ok(TypeDiagnostic::UncoveredPattern(ctx, orig, {
"Apps.Kind.Error.Quoted.uncovered_pattern" => Ok(TypeDiagnostic::UncoveredPattern(ctx, orig, {
let args = parse_list(&args[2])?;
let mut new_args = Vec::with_capacity(args.len());
for arg in &args {
@ -234,25 +234,25 @@ fn parse_type_error(expr: &Term) -> Result<TypeDiagnostic, String> {
}
new_args
})),
"Kind.Error.Quoted.unbound_variable" => Ok(TypeDiagnostic::UnboundVariable(ctx, orig)),
"Kind.Error.Quoted.cant_infer_hole" => Ok(TypeDiagnostic::CantInferHole(ctx, orig)),
"Kind.Error.Quoted.cant_infer_lambda" => Ok(TypeDiagnostic::CantInferLambda(ctx, orig)),
"Kind.Error.Quoted.invalid_call" => Ok(TypeDiagnostic::InvalidCall(ctx, orig)),
"Kind.Error.Quoted.impossible_case" => Ok(TypeDiagnostic::ImpossibleCase(
"Apps.Kind.Error.Quoted.unbound_variable" => Ok(TypeDiagnostic::UnboundVariable(ctx, orig)),
"Apps.Kind.Error.Quoted.cant_infer_hole" => Ok(TypeDiagnostic::CantInferHole(ctx, orig)),
"Apps.Kind.Error.Quoted.cant_infer_lambda" => Ok(TypeDiagnostic::CantInferLambda(ctx, orig)),
"Apps.Kind.Error.Quoted.invalid_call" => Ok(TypeDiagnostic::InvalidCall(ctx, orig)),
"Apps.Kind.Error.Quoted.impossible_case" => Ok(TypeDiagnostic::ImpossibleCase(
ctx,
orig,
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
parse_all_expr(im_rc::HashMap::new(), &args[3])?,
)),
"Kind.Error.Quoted.inspection" => Ok(TypeDiagnostic::Inspection(
"Apps.Kind.Error.Quoted.inspection" => Ok(TypeDiagnostic::Inspection(
ctx,
orig,
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
)),
"Kind.Error.Quoted.too_many_arguments" => {
"Apps.Kind.Error.Quoted.too_many_arguments" => {
Ok(TypeDiagnostic::TooManyArguments(ctx, orig))
}
"Kind.Error.Quoted.type_mismatch" => Ok(TypeDiagnostic::TypeMismatch(
"Apps.Kind.Error.Quoted.type_mismatch" => Ok(TypeDiagnostic::TypeMismatch(
ctx,
orig,
parse_all_expr(im_rc::HashMap::new(), &args[2])?,

8
crates/kind-cli/Cargo.toml
View File

@ -14,10 +14,10 @@ path = "src/main.rs"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-checker = {path = "../kind-checker", version = "0.1.2"}
kind-driver = {path = "../kind-driver", version = "0.1.2"}
kind-query = {path = "../kind-query", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-checker = {path = "../kind-checker", version = "0.1.3"}
kind-driver = {path = "../kind-driver", version = "0.1.3"}
kind-query = {path = "../kind-query", version = "0.1.3"}
kind-report = {path = "../kind-report", version = "0.1.3"}
anyhow = "1.0.66"
clap = {version = "4.0.10", features = ["derive"]}

8
crates/kind-derive/Cargo.toml
View File

@ -3,13 +3,13 @@ description = "Derive generator the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-derive"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
fxhash = "0.2.1"
im-rc = "15.1.0"
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}

12
crates/kind-derive/src/subst.rs
View File

@ -214,7 +214,7 @@ impl<'a> Visitor for Subst<'a> {
snd,
} => {
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
"Sigma", None, expr.range,
"Data.Sigma", None, expr.range,
));
self.visit_expr(fst);
self.visit_expr(snd);
@ -225,7 +225,7 @@ impl<'a> Visitor for Subst<'a> {
snd,
} => {
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
"Sigma", None, expr.range,
"Data.Sigma", None, expr.range,
));
self.visit_expr(fst);
self.context_vars.push((ident.range, ident.to_string()));
@ -257,7 +257,7 @@ impl<'a> Visitor for Subst<'a> {
}
ExprKind::If { cond, then_, else_ } => {
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
"Bool", "if", expr.range,
"Data.Bool", "if", expr.range,
));
self.visit_expr(cond);
self.visit_expr(then_);
@ -265,17 +265,17 @@ impl<'a> Visitor for Subst<'a> {
}
ExprKind::Pair { fst, snd } => {
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
"Pair", "new", expr.range,
"Data.Pair", "new", expr.range,
));
self.visit_expr(fst);
self.visit_expr(snd);
}
ExprKind::List { args } => {
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
"List", "nil", expr.range,
"Data.List", "nil", expr.range,
));
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
"List", "cons", expr.range,
"Data.List", "cons", expr.range,
));
visit_vec!(args.iter_mut(), arg => self.visit_expr(arg));
}

16
crates/kind-driver/Cargo.toml
View File

@ -3,22 +3,22 @@ description = "Driver for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-driver"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-checker = {path = "../kind-checker", version = "0.1.2"}
kind-parser = {path = "../kind-parser", version = "0.1.2"}
kind-pass = {path = "../kind-pass", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-checker = {path = "../kind-checker", version = "0.1.3"}
kind-parser = {path = "../kind-parser", version = "0.1.3"}
kind-pass = {path = "../kind-pass", version = "0.1.3"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
kind-target-hvm = {path = "../kind-target-hvm", version = "0.1.0"}
kind-target-kdl = {path = "../kind-target-kdl", version = "0.1.0"}
hvm = "1.0.6"
hvm = "1.0.8"
anyhow = "1.0.66"
dashmap = "5.4.0"

8
crates/kind-parser/Cargo.toml
View File

@ -3,13 +3,13 @@ description = "Parser for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-parser"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
fxhash = "0.2.1"

8
crates/kind-parser/src/expr.rs
View File

@ -241,10 +241,10 @@ impl<'a> Parser<'a> {
let id = self.parse_upper_id()?;
let data = match id.to_string().as_str() {
"Type" => ExprKind::Lit { lit: Literal::Type },
"U60" => ExprKind::Lit {
"Data.U60" => ExprKind::Lit {
lit: Literal::NumTypeU60,
},
"F60" => ExprKind::Lit {
"Data.F60" => ExprKind::Lit {
lit: Literal::NumTypeF60,
},
_ => ExprKind::Constr {
@ -263,10 +263,10 @@ impl<'a> Parser<'a> {
let mut range = id.range;
let data = match id.to_string().as_str() {
"Type" => ExprKind::Lit { lit: Literal::Type },
"U60" => ExprKind::Lit {
"Data.U60" => ExprKind::Lit {
lit: Literal::NumTypeU60,
},
"F60" => ExprKind::Lit {
"Data.F60" => ExprKind::Lit {
lit: Literal::NumTypeF60,
},
_ => {

10
crates/kind-pass/Cargo.toml
View File

@ -3,15 +3,15 @@ description = "A lot of compiler passes for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-pass"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-derive = {path = "../kind-derive", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-derive = {path = "../kind-derive", version = "0.1.3"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
anyhow = "1.0.66"
fxhash = "0.2.1"

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

@ -24,8 +24,8 @@ impl<'a> DesugarState<'a> {
) -> Box<desugared::Expr> {
match literal {
Literal::String(string) => {
if !self.check_implementation("String.cons", range, Sugar::String)
|| !self.check_implementation("String.nil", range, Sugar::String)
if !self.check_implementation("Data.String.cons", range, Sugar::String)
|| !self.check_implementation("Data.String.nil", range, Sugar::String)
{
return desugared::Expr::err(range);
}
@ -37,7 +37,7 @@ impl<'a> DesugarState<'a> {
Literal::NumTypeF60 => desugared::Expr::type_f60(range),
Literal::NumU60(num) => desugared::Expr::num_u60(range, *num),
Literal::Nat(num) => {
let list_ident = QualifiedIdent::new_static("Nat", None, range);
let list_ident = QualifiedIdent::new_static("Data.Nat", None, range);
let cons_ident = list_ident.add_segment("succ");
let nil_ident = list_ident.add_segment("zero");
@ -50,7 +50,7 @@ impl<'a> DesugarState<'a> {
res
}
Literal::NumU120(num) => {
if !self.check_implementation("U120.new", range, Sugar::U120) {
if !self.check_implementation("Data.U120.new", range, Sugar::U120) {
return desugared::Expr::err(range);
}
desugared::Expr::num_u120(range, *num)
@ -292,7 +292,7 @@ impl<'a> DesugarState<'a> {
typ: &expr::Expr,
body: &expr::Expr,
) -> Box<desugared::Expr> {
let sigma = QualifiedIdent::new_static("Sigma", None, range);
let sigma = QualifiedIdent::new_static("Data.Sigma", None, range);
if !self.check_implementation(sigma.to_str(), range, Sugar::Sigma) {
return desugared::Expr::err(range);
@ -316,7 +316,7 @@ impl<'a> DesugarState<'a> {
range: Range,
expr: &[expr::Expr],
) -> Box<desugared::Expr> {
let list_ident = QualifiedIdent::new_static("List", None, range);
let list_ident = QualifiedIdent::new_static("Data.List", None, range);
let cons_ident = list_ident.add_segment("cons");
let nil_ident = list_ident.add_segment("nil");
@ -345,7 +345,7 @@ impl<'a> DesugarState<'a> {
if_: &expr::Expr,
else_: &expr::Expr,
) -> Box<desugared::Expr> {
let boolean = QualifiedIdent::new_static("Bool", None, range);
let boolean = QualifiedIdent::new_static("Data.Bool", None, range);
let bool_if_ident = boolean.add_segment("if");
let bool_if = self.old_book.names.get(bool_if_ident.to_str());
@ -419,7 +419,7 @@ impl<'a> DesugarState<'a> {
fst: &expr::Expr,
snd: &expr::Expr,
) -> Box<desugared::Expr> {
let sigma_new = QualifiedIdent::new_sugared("Sigma", "new", range);
let sigma_new = QualifiedIdent::new_sugared("Data.Sigma", "new", range);
if !self.check_implementation(sigma_new.to_str(), range, Sugar::Pair) {
return desugared::Expr::err(range);

4
crates/kind-pass/src/desugar/top_level.rs
View File

@ -223,7 +223,7 @@ impl<'a> DesugarState<'a> {
fst: &concrete::pat::Pat,
snd: &concrete::pat::Pat,
) -> Box<desugared::Expr> {
let sigma_new = QualifiedIdent::new_static("Sigma", Some("new".to_string()), range);
let sigma_new = QualifiedIdent::new_static("Data.Sigma", Some("new".to_string()), range);
let entry = self.old_book.entries.get(sigma_new.to_string().as_str());
if entry.is_none() {
@ -241,7 +241,7 @@ impl<'a> DesugarState<'a> {
range: Range,
expr: &[concrete::pat::Pat],
) -> Box<desugared::Expr> {
let list_ident = QualifiedIdent::new_static("List", None, range);
let list_ident = QualifiedIdent::new_static("Data.List", None, range);
let cons_ident = list_ident.add_segment("cons");
let nil_ident = list_ident.add_segment("nil");

12
crates/kind-pass/src/diagnostic.rs
View File

@ -218,12 +218,12 @@ impl Diagnostic for PassDiagnostic {
subtitles: vec![],
hints: vec![match sugar {
Sugar::DoNotation => "You must implement 'bind' and 'pure' for this type in order to use the do notation.".to_string(),
Sugar::List => "You must implement 'List', 'List.cons' and 'List.nil' for this type in order to use the list notation.".to_string(),
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::List => "You must implement 'Data.List', 'Data.List.cons' and 'Data.List.nil' for this type in order to use the list notation.".to_string(),
Sugar::Sigma => "You must implement 'Data.Sigma' in order to use the sigma notation.".to_string(),
Sugar::Pair => "You must implement 'Data.Sigma' and 'Data.Sigma.new' in order to use the sigma notation.".to_string(),
Sugar::BoolIf => "You must implement 'Data.Bool.if' in order to use the if notation.".to_string(),
Sugar::String => "You must implement 'Data.String.cons' in order to use the string notation.".to_string(),
Sugar::U120 => "You must implement 'Data.U120.new' in order to use the u120 notation.".to_string(),
Sugar::Match(_) => "You must implement 'match' in order to use the match notation (or derive match with #derive[match]).".to_string(),
Sugar::Mutter(typ) => format!("You must derive 'mutters' for '{}' in order to use this syntax", typ),
Sugar::Getter(typ) => format!("You must derive 'getters' for '{}' in order to use this syntax", typ)

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

@ -348,8 +348,8 @@ impl<'a> ErasureState<'a> {
NumU60 { numb } => untyped::Expr::u60(expr.range, *numb),
NumF60 { numb } => untyped::Expr::f60(expr.range, *numb),
Str { val } => {
let nil = QualifiedIdent::new_static("String.nil", None, expr.range);
let cons = QualifiedIdent::new_static("String.cons", None, expr.range);
let nil = QualifiedIdent::new_static("Data.String.nil", None, expr.range);
let cons = QualifiedIdent::new_static("Data.String.cons", None, expr.range);
self.connect_with(edge, &nil, relevance);
self.connect_with(edge, &cons, relevance);
@ -491,8 +491,8 @@ impl<'a> ErasureState<'a> {
NumU60 { numb } => untyped::Expr::u60(expr.range, *numb),
NumF60 { numb } => untyped::Expr::f60(expr.range, *numb),
Str { val } => {
let nil = QualifiedIdent::new_static("String.nil", None, expr.range);
let cons = QualifiedIdent::new_static("String.cons", None, expr.range);
let nil = QualifiedIdent::new_static("Data.String.nil", None, expr.range);
let cons = QualifiedIdent::new_static("Data.String.cons", None, expr.range);
self.connect_with(edge, &nil, ambient);
self.connect_with(edge, &cons, ambient);

14
crates/kind-pass/src/unbound/mod.rs
View File

@ -376,7 +376,7 @@ impl Visitor for UnboundCollector {
match &mut pat.data {
PatKind::Var(ident) => self.visit_pat_ident(ident),
PatKind::Str(_) => {
let string = &mut QualifiedIdent::new_static("String", None, pat.range);
let string = &mut QualifiedIdent::new_static("Data.String", None, pat.range);
self.visit_qualified_ident(&mut string.add_segment("cons").to_generated());
self.visit_qualified_ident(&mut string.add_segment("nil").to_generated());
}
@ -475,7 +475,7 @@ impl Visitor for UnboundCollector {
use kind_tree::concrete::Literal::*;
if let String(_) = lit {
let string = &mut QualifiedIdent::new_static("String", None, range);
let string = &mut QualifiedIdent::new_static("Data.String", None, range);
self.visit_qualified_ident(&mut string.add_segment("cons").to_generated());
self.visit_qualified_ident(&mut string.add_segment("nil").to_generated());
}
@ -545,7 +545,7 @@ impl Visitor for UnboundCollector {
snd,
} => {
self.visit_qualified_ident(
&mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(),
&mut QualifiedIdent::new_static("Data.Sigma", None, expr.range).to_generated(),
);
self.visit_expr(fst);
self.visit_expr(snd);
@ -556,7 +556,7 @@ impl Visitor for UnboundCollector {
snd,
} => {
self.visit_qualified_ident(
&mut QualifiedIdent::new_static("Sigma", None, expr.range).to_generated(),
&mut QualifiedIdent::new_static("Data.Sigma", None, expr.range).to_generated(),
);
self.visit_expr(fst);
self.context_vars.push((ident.range, ident.to_string()));
@ -587,20 +587,20 @@ impl Visitor for UnboundCollector {
self.visit_sttm(sttm)
}
ExprKind::If { cond, then_, else_ } => {
let typ = QualifiedIdent::new_static("Bool", None, expr.range);
let typ = QualifiedIdent::new_static("Data.Bool", None, expr.range);
self.visit_qualified_ident(&mut typ.add_segment("if").to_generated());
self.visit_expr(cond);
self.visit_expr(then_);
self.visit_expr(else_);
}
ExprKind::Pair { fst, snd } => {
let typ = QualifiedIdent::new_static("Pair", None, expr.range);
let typ = QualifiedIdent::new_static("Data.Pair", None, expr.range);
self.visit_qualified_ident(&mut typ.add_segment("new").to_generated());
self.visit_expr(fst);
self.visit_expr(snd);
}
ExprKind::List { args } => {
let mut typ = QualifiedIdent::new_static("List", None, expr.range);
let mut typ = QualifiedIdent::new_static("Data.List", None, expr.range);
self.visit_qualified_ident(&mut typ);
self.visit_qualified_ident(&mut typ.add_segment("nil").to_generated());

16
crates/kind-query/Cargo.toml
View File

@ -3,18 +3,18 @@ description = "Query module for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-query"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-checker = {path = "../kind-checker", version = "0.1.2"}
kind-parser = {path = "../kind-parser", version = "0.1.2"}
kind-pass = {path = "../kind-pass", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-target-hvm = {path = "../kind-target-hvm", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-checker = {path = "../kind-checker", version = "0.1.3"}
kind-parser = {path = "../kind-parser", version = "0.1.3"}
kind-pass = {path = "../kind-pass", version = "0.1.3"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-target-hvm = {path = "../kind-target-hvm", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
fxhash = "0.2.1"
pathdiff = "0.2.1"

4
crates/kind-report/Cargo.toml
View File

@ -3,12 +3,12 @@ description = "Report module for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-report"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.3"}
fxhash = "0.2.1"
pathdiff = "0.2.1"

2
crates/kind-span/Cargo.toml
View File

@ -3,7 +3,7 @@ description = "Describes locations for the Kind compiler"
edition = "2021"
license = "MIT"
name = "kind-span"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

12
crates/kind-target-hvm/Cargo.toml
View File

@ -3,14 +3,14 @@ description = "HVM Code generator for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-target-hvm"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-derive = {path = "../kind-derive", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-derive = {path = "../kind-derive", version = "0.1.3"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
hvm = "1.0.6"
hvm = "1.0.8"

6
crates/kind-target-hvm/src/lib.rs
View File

@ -17,13 +17,13 @@ pub fn compile_book(book: untyped::Book, trace: bool) -> File {
pub fn compile_str(val: &str) -> Box<Term> {
let nil = Box::new(Term::Ctr {
name: String::from("String.nil"),
name: String::from("Data.String.nil"),
args: vec![],
});
let cons = |numb, next| {
Box::new(Term::Ctr {
name: String::from("String.cons"),
name: String::from("Data.String.cons"),
args: vec![Box::new(Term::U6O { numb }), next],
})
};
@ -105,7 +105,7 @@ fn compile_entry(file: &mut File, entry: Box<untyped::Entry>, trace: bool) {
args: args.clone(),
}),
rhs: Box::new(Term::Ctr {
name: "HVM.log".to_string(),
name: "Apps.HVM.log".to_string(),
args: vec![
compile_str(entry.name.to_str()),
Box::new(Term::Ctr {

10
crates/kind-target-kdl/Cargo.toml
View File

@ -3,15 +3,15 @@ description = "KDL target for the kind compiler"
edition = "2021"
license = "MIT"
name = "kind-target-kdl"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
kind-derive = {path = "../kind-derive", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-derive = {path = "../kind-derive", version = "0.1.3"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
fxhash = "0.2.1"
im-rc = "15.1.0"

46
crates/kind-target-kdl/src/compile.rs
View File

@ -326,7 +326,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
From::Ctr { name, args } => {
// Convert U120 numbers into the native kindelia representation
// Only possible if both U60s are U60 terms
if name.to_str() == "U120.new" {
if name.to_str() == "Data.U120.new" {
if let (From::U60 { numb: hi }, From::U60 { numb: lo }) =
(&args[0].data, &args[1].data)
{
@ -344,97 +344,97 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
// some numeric function applications
// Add with no boundary check is just a normal add
"U60.add_unsafe" => To::Op2 {
"Data.U60.add_unsafe" => To::Op2 {
oper: kdl::Oper::Add,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
// U60s are already stored in 120 bits
"U60.to_u120" => compile_expr(ctx, &args[0]),
"Data.U60.to_u120" => compile_expr(ctx, &args[0]),
// Truncate to 60 bits
"U120.to_u60" => To::Op2 {
"Data.U120.to_u60" => To::Op2 {
oper: kdl::Oper::And,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(To::Num { numb: U60_MAX }),
},
// Compilation for U120 numeric operations
"U120.add" => To::Op2 {
"Data.U120.add" => To::Op2 {
oper: kdl::Oper::Add,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.sub" => To::Op2 {
"Data.U120.sub" => To::Op2 {
oper: kdl::Oper::Add,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.mul" => To::Op2 {
"Data.U120.mul" => To::Op2 {
oper: kdl::Oper::Mul,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.div" => To::Op2 {
"Data.U120.div" => To::Op2 {
oper: kdl::Oper::Div,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.mod" => To::Op2 {
"Data.U120.mod" => To::Op2 {
oper: kdl::Oper::Mod,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.num_equal" => To::Op2 {
"Data.U120.num_equal" => To::Op2 {
oper: kdl::Oper::Eql,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.num_not_equal" => To::Op2 {
"Data.U120.num_not_equal" => To::Op2 {
oper: kdl::Oper::Neq,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.shift_left" => To::Op2 {
"Data.U120.shift_left" => To::Op2 {
oper: kdl::Oper::Shl,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.shift_right" => To::Op2 {
"Data.U120.shift_right" => To::Op2 {
oper: kdl::Oper::Shr,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.num_less_than" => To::Op2 {
"Data.U120.num_less_than" => To::Op2 {
oper: kdl::Oper::Ltn,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.num_less_equal" => To::Op2 {
"Data.U120.num_less_equal" => To::Op2 {
oper: kdl::Oper::Lte,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.num_greater_than" => To::Op2 {
"Data.U120.num_greater_than" => To::Op2 {
oper: kdl::Oper::Gtn,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.num_greater_equal" => To::Op2 {
"Data.U120.num_greater_equal" => To::Op2 {
oper: kdl::Oper::Gte,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.bitwise_and" => To::Op2 {
"Data.U120.bitwise_and" => To::Op2 {
oper: kdl::Oper::And,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.bitwise_or" => To::Op2 {
"Data.U120.bitwise_or" => To::Op2 {
oper: kdl::Oper::Or,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
},
"U120.bitwise_xor" => To::Op2 {
"Data.U120.bitwise_xor" => To::Op2 {
oper: kdl::Oper::Xor,
val0: Box::new(compile_expr(ctx, &args[0])),
val1: Box::new(compile_expr(ctx, &args[1])),
@ -455,11 +455,11 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
}
From::Str { val } => {
let nil = kdl::Term::Ctr {
name: *ctx.kdl_names.get("String.nil").unwrap(),
name: *ctx.kdl_names.get("Data.String.nil").unwrap(),
args: vec![],
};
let cons_name = *ctx.kdl_names.get("String.cons").unwrap();
let cons_name = *ctx.kdl_names.get("Data.String.cons").unwrap();
let cons = |numb: u128, next| kdl::Term::Ctr {
name: cons_name,
@ -494,7 +494,7 @@ pub fn compile_entry(ctx: &mut CompileCtx, entry: &untyped::Entry) {
}
} else {
match entry.name.to_str() {
"U120.new" => compile_u120_new(ctx, entry),
"Data.U120.new" => compile_u120_new(ctx, entry),
_ => compile_common_function(ctx, entry),
}
}

10
crates/kind-tests/Cargo.toml
View File

@ -2,18 +2,18 @@
edition = "2021"
license = "MIT"
name = "kind-tests"
version = "0.1.2"
version = "0.1.3"
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dev-dependencies]
kind-checker = {path = "../kind-checker"}
kind-driver = {path = "../kind-driver"}
kind-parser = {path = "../kind-parser", version = "0.1.2"}
kind-parser = {path = "../kind-parser", version = "0.1.3"}
kind-pass = {path = "../kind-pass"}
kind-report = {path = "../kind-report", version = "0.1.2"}
kind-span = {path = "../kind-span", version = "0.1.2"}
kind-tree = {path = "../kind-tree", version = "0.1.2"}
kind-report = {path = "../kind-report", version = "0.1.3"}
kind-span = {path = "../kind-span", version = "0.1.3"}
kind-tree = {path = "../kind-tree", version = "0.1.3"}
kind-target-hvm = {path = "../kind-target-hvm"}
kind-target-kdl = {path = "../kind-target-kdl"}

2
crates/kind-tests/suite/checker/Inspection.golden
View File

@ -1,6 +1,6 @@
INFO Inspection
* Hole: U60
* Hole: Data.U60
/--[suite/checker/Inspection.kind2:3:3]

2
crates/kind-tests/suite/checker/Inspection.kind2
View File

@ -1,3 +1,3 @@
Main : U60
Main : Data.U60
Main =
?

10
crates/kind-tests/suite/checker/Nat.kind2
View File

@ -1,8 +1,8 @@
type Nat {
succ (pred: Nat)
type Data.Nat {
succ (pred: Data.Nat)
zero
}
Nat.pred (n: Nat) : Nat
Nat.pred Nat.zero = Nat.zero
Nat.pred (Nat.succ n) = n
Data.Nat.pred (n: Data.Nat) : Data.Nat
Data.Nat.pred Data.Nat.zero = Data.Nat.zero
Data.Nat.pred (Data.Nat.succ n) = n

36
crates/kind-tests/suite/checker/Quicksort.kind2
View File

@ -1,7 +1,7 @@
// From: https://github.com/Kindelia/Functional-Benchmarks/blob/master/Runtime/quicksort.kind2
type List (t: Type) {
Cons (head: t) (tail: List t)
type Data.List (t: Type) {
Cons (head: t) (tail: Data.List t)
Nil
}
@ -12,44 +12,44 @@ type Tree (t: Type) {
}
// Generates a random list
Randoms (s: U60) (n: U60) : List U60
Randoms s 0 = List.Nil
Randoms s l = List.Cons s (Randoms (% (+ (* s 1664525) 1013904223) 4294967296) (- l 1))
Randoms (s: Data.U60) (n: Data.U60) : Data.List Data.U60
Randoms s 0 = Data.List.Nil
Randoms s l = Data.List.Cons s (Randoms (% (+ (* s 1664525) 1013904223) 4294967296) (- l 1))
// Sums all elements in a concatenation tree
Sum (tree: Tree U60) : U60
Sum (tree: Tree Data.U60) : Data.U60
Sum (Tree.Empty t) = 0
Sum (Tree.Single t a) = a
Sum (Tree.Concat t a b) = (+ (Sum a) (Sum b))
//// The initial pivot
Pivot : U60
Pivot : Data.U60
Pivot = 2147483648
QSort (p: U60) (s: U60) (l: List U60): Tree U60
QSort p s List.Nil = Tree.Empty
QSort p s (List.Cons x List.Nil) = Tree.Single x
QSort p s (List.Cons x xs) = Split p s (List.Cons x xs) List.Nil List.Nil
QSort (p: Data.U60) (s: Data.U60) (l: Data.List Data.U60): Tree Data.U60
QSort p s Data.List.Nil = Tree.Empty
QSort p s (Data.List.Cons x Data.List.Nil) = Tree.Single x
QSort p s (Data.List.Cons x xs) = Split p s (Data.List.Cons x xs) Data.List.Nil Data.List.Nil
//// Splits list in two partitions
Split (p: U60) (s: U60) (l: List U60) (min: List U60) (max: List U60) : Tree U60
Split p s List.Nil min max =
Split (p: Data.U60) (s: Data.U60) (l: Data.List Data.U60) (min: Data.List Data.U60) (max: Data.List Data.U60) : Tree Data.U60
Split p s Data.List.Nil min max =
let s = (>> s 1)
let min = (QSort (- p s) s min)
let max = (QSort (+ p s) s max)
Tree.Concat min max
Split p s (List.Cons x xs) min max =
Split p s (Data.List.Cons x xs) min max =
Place p s (< p x) x xs min max
//// Moves element to its partition
Place (p: U60) (s: U60) (y: U60) (x: U60) (xs: List U60) (min: List U60) (max: List U60) : Tree U60
Place p s 0 x xs min max = Split p s xs (List.Cons x min) max
Place p s _ x xs min max = Split p s xs min (List.Cons x max)
Place (p: Data.U60) (s: Data.U60) (y: Data.U60) (x: Data.U60) (xs: Data.List Data.U60) (min: Data.List Data.U60) (max: Data.List Data.U60) : Tree Data.U60
Place p s 0 x xs min max = Split p s xs (Data.List.Cons x min) max
Place p s _ x xs min max = Split p s xs min (Data.List.Cons x max)
//// Sorts and sums n random numbers
Main : U60
Main : Data.U60
Main =
let list = Randoms 1 254
Sum (QSort Pivot Pivot list)

6
crates/kind-tests/suite/checker/SimpleOpen.kind2
View File

@ -1,11 +1,11 @@
#derive[match]
record Pudim {
owo : U60
uwu : U60
owo : Data.U60
uwu : Data.U60
}
#keep
Ok (n: Pudim) : U60
Ok (n: Pudim) : Data.U60
Ok n =
open Pudim n
n.owo

8
crates/kind-tests/suite/checker/SimpleOpenWithMotive.kind2
View File

@ -1,14 +1,14 @@
#derive[match]
record Pudim {
owo : U60
uwu : U60
owo : Data.U60
uwu : Data.U60
}
#keep
Ok (n: Pudim) : U60
Ok (n: Pudim) : Data.U60
Ok n =
open Pudim n : _;
(+ n.owo n.uwu)
Main : U60
Main : Data.U60
Main = Ok (Pudim.new 10 20)

10
crates/kind-tests/suite/checker/Subst.golden
View File

@ -1,13 +1,13 @@
INFO Inspection
* Hole: U60
* Hole: Data.U60
* Context
* awoo : Type
* awoo = U60
* uuuhuuul : (List awoo)
* uuuhuuul = (List.nil awoo)
* ooooooo : (List U60)
* awoo = Data.U60
* uuuhuuul : (Data.List awoo)
* uuuhuuul = (Data.List.nil awoo)
* ooooooo : (Data.List Data.U60)
* ooooooo = uuuhuuul
/--[suite/checker/Subst.kind2:11:5]

10
crates/kind-tests/suite/checker/Subst.kind2
View File

@ -1,11 +1,11 @@
type List (a: Type) {
cons (x: a) (xs: List a)
type Data.List (a: Type) {
cons (x: a) (xs: Data.List a)
nil
}
Rei : U60
Rei : Data.U60
Rei =
let awoo = U60
let uuuhuuul = ([] :: List awoo)
let awoo = Data.U60
let uuuhuuul = ([] :: Data.List awoo)
let ooooooo = specialize awoo into #0 in uuuhuuul
?

38
crates/kind-tests/suite/checker/SubstUnbound.kind2
View File

@ -1,7 +1,7 @@
// A lot of thing here is just to test the substition
type List (t: Type) {
Cons (head: t) (tail: List t)
type Data.List (t: Type) {
Cons (head: t) (tail: Data.List t)
Nil
}
@ -17,49 +17,49 @@ record JustATest (t: Type) {
}
// Generates a random list
Randoms (s: U60) (n: U60) : List U60
Randoms s 0 = List.Nil
Randoms s l = List.Cons s (Randoms (% (+ (* s 1664525) 1013904223) 4294967296) (- l 1))
Randoms (s: Data.U60) (n: Data.U60) : Data.List Data.U60
Randoms s 0 = Data.List.Nil
Randoms s l = Data.List.Cons s (Randoms (% (+ (* s 1664525) 1013904223) 4294967296) (- l 1))
// Sums all elements in a concatenation tree
Sum (tree: Tree U60) : U60
Sum (tree: Tree Data.U60) : Data.U60
Sum (Tree.Empty t) = 0
Sum (Tree.Single t a) = a
Sum (Tree.Concat t a b) = (+ (Sum a) (Sum b))
//// The initial pivot
Pivot : U60
Pivot : Data.U60
Pivot = 2147483648
QSort (p: U60) (s: U60) (l: List U60): Tree U60
QSort p s List.Nil = Tree.Empty
QSort p s (List.Cons x List.Nil) = Tree.Single x
QSort p s (List.Cons x xs) = Split p s (List.Cons x xs) List.Nil List.Nil
QSort (p: Data.U60) (s: Data.U60) (l: Data.List Data.U60): Tree Data.U60
QSort p s Data.List.Nil = Tree.Empty
QSort p s (Data.List.Cons x Data.List.Nil) = Tree.Single x
QSort p s (Data.List.Cons x xs) = Split p s (Data.List.Cons x xs) Data.List.Nil Data.List.Nil
//// Splits list in two partitions
Split (p: U60) (s: U60) (l: List U60) (min: List U60) (max: List U60) : Tree U60
Split p s List.Nil min max =
Split (p: Data.U60) (s: Data.U60) (l: Data.List Data.U60) (min: Data.List Data.U60) (max: Data.List Data.U60) : Tree Data.U60
Split p s Data.List.Nil min max =
let s = (>> s 1)
let min = (QSort (- p s) s min)
let max = (QSort (+ p s) s max)
Tree.Concat min max
Split p s (List.Cons x xs) min max =
Split p s (Data.List.Cons x xs) min max =
Place p s (< p x) x xs min max
//// Moves element to its partition
Place (p: U60) (s: U60) (y: U60) (x: U60) (xs: List U60) (min: List U60) (max: List U60) : Tree U60
Place p s 0 x xs min max = Split p s xs (List.Cons x min) max
Place p s _ x xs min max = Split p s xs min (List.Cons x max)
Place (p: Data.U60) (s: Data.U60) (y: Data.U60) (x: Data.U60) (xs: Data.List Data.U60) (min: Data.List Data.U60) (max: Data.List Data.U60) : Tree Data.U60
Place p s 0 x xs min max = Split p s xs (Data.List.Cons x min) max
Place p s _ x xs min max = Split p s xs min (Data.List.Cons x max)
//// Sorts and sums n random numbers
Main : U60
Main : Data.U60
Main =
let list = Randoms 1 254
Sum (QSort Pivot Pivot list)
Entry : U60
Entry : Data.U60
Entry =
let a = 2
let b = 4

18
crates/kind-tests/suite/checker/TestWith.kind2
View File

@ -1,19 +1,19 @@
#derive[match]
type Nat {
succ (pred: Nat)
type Data.Nat {
succ (pred: Data.Nat)
zero
}
Run (n: Nat) : Type
Run (Nat.succ n) = U60
Run (Nat.zero) = U60
Run (n: Data.Nat) : Type
Run (Data.Nat.succ n) = Data.U60
Run (Data.Nat.zero) = Data.U60
Lero <t> (n: Nat) (f: Run n) : U60
Lero <t> (n: Data.Nat) (f: Run n) : Data.U60
Lero t1 n f =
match Nat n with (f : Run n) {
match Data.Nat n with (f : Run n) {
succ => (+ f 2)
zero => (+ f 1)
}
Main : U60
Main = Lero (Nat.succ Nat.zero) 1
Main : Data.U60
Main = Lero (Data.Nat.succ Data.Nat.zero) 1

18
crates/kind-tests/suite/checker/derive/DoNotation.kind2
View File

@ -1,12 +1,12 @@
Main : Maybe U60
Main : Data.Maybe Data.U60
Main =
do Maybe {
Maybe.some 3
Maybe.pure 2
ask res = Maybe.pure 2
ask res2 = Maybe.pure 3
match Maybe t = (Maybe.some 4) {
some val => Maybe.pure (+ 1000 (+ val (+ res res2)))
none => Maybe.none
do Data.Maybe {
Data.Maybe.some 3
Data.Maybe.pure 2
ask res = Data.Maybe.pure 2
ask res2 = Data.Maybe.pure 3
match Data.Maybe t = (Data.Maybe.some 4) {
some val => Data.Maybe.pure (+ 1000 (+ val (+ res res2)))
none => Data.Maybe.none
}
}

8
crates/kind-tests/suite/checker/derive/User.kind2
View File

@ -1,12 +1,12 @@
#derive[match]
record User {
constructor new
name : U60
ttt : U60
e : U60
name : Data.U60
ttt : Data.U60
e : Data.U60
}
Main : U60
Main : Data.U60
Main =
let User.new (ttt = e) e .. = User.new 2 4 1
let User.new (ttt = f) .. = User.new 6 7 3

10
crates/kind-tests/suite/checker/derive/Vec.kind2
View File

@ -1,9 +1,9 @@
type Nat {
succ (pred : Nat)
type Data.Nat {
succ (pred : Data.Nat)
zero
}
type Vec (t: Type) ~ (n: Nat) {
cons <size : Nat> (x : t) (xs : Vec t size) : Vec t (Nat.succ size)
nil : Vec t Nat.zero
type Vec (t: Type) ~ (n: Data.Nat) {
cons <size : Data.Nat> (x : t) (xs : Vec t size) : Vec t (Data.Nat.succ size)
nil : Vec t Data.Nat.zero
}

8
crates/kind-tests/suite/checker/derive/fail/IncompleteCase.kind2
View File

@ -1,12 +1,12 @@
#derive[match]
record User {
constructor new
name : U60
ttt : U60
e : U60
name : Data.U60
ttt : Data.U60
e : Data.U60
}
Main : U60
Main : Data.U60
Main =
let User.new (ttt = e) e .. = User.new 2 4 1
let User.new (ttt = f) name = User.new 6 7 3

8
crates/kind-tests/suite/checker/derive/fail/Repeated.kind2
View File

@ -1,12 +1,12 @@
#derive[match]
record User {
constructor new
name : U60
ttt : U60
e : U60
name : Data.U60
ttt : Data.U60
e : Data.U60
}
Main : U60
Main : Data.U60
Main =
let User.new (ttt = e) e .. = User.new 2 4 1
let User.new (ttt = f) ttt = User.new 6 7 3

6
crates/kind-tests/suite/checker/derive/fail/RepeatedDef.golden
View File

@ -2,14 +2,14 @@
/--[suite/checker/derive/fail/RepeatedDef.kind2:2:5]
|
1 | type Nat {
1 | type Data.Nat {
2 | zero
| v---
| \The first ocorrence
3 | succ
:
6 | Nat.zero : U60
| v-------
6 | Data.Nat.zero : Data.U60
| v------------
| \Second occorrence here!
Hint: Rename one of the definitions or remove and look at how names work in Kind at https://github.com/Kindelia/Kind2/blob/master/guide/naming.md

6
crates/kind-tests/suite/checker/derive/fail/RepeatedDef.kind2
View File

@ -1,7 +1,7 @@
type Nat {
type Data.Nat {
zero
succ
}
Nat.zero : U60
Nat.zero = 2
Data.Nat.zero : Data.U60
Data.Nat.zero = 2

4
crates/kind-tests/suite/checker/derive/fail/WrongU120Eq.golden
View File

@ -1,7 +1,7 @@
ERROR Type mismatch
* Got : (Eq _ (U120.new 0 123) (U120.new 0 123))
* Expected : (Eq _ (U120.new 0 123) (U120.new 0 124))
* Got : (Eq _ (Data.U120.new 0 123) (Data.U120.new 0 123))
* Expected : (Eq _ (Data.U120.new 0 123) (Data.U120.new 0 124))
/--[suite/checker/derive/fail/WrongU120Eq.kind2:12:9]

6
crates/kind-tests/suite/checker/derive/fail/WrongU120Eq.kind2
View File

@ -2,10 +2,10 @@ type Eq <t: Type> (a: t) ~ (b: t) {
rfl: Eq t a a
}
record U120 {
record Data.U120 {
constructor new
low : U60
high : U60
low : Data.U60
high : Data.U60
}
Teste : Eq 123u120 124u120

6
crates/kind-tests/suite/checker/fail/MismatchTwo.golden
View File

@ -1,14 +1,14 @@
ERROR Type mismatch
* Got : Type
* Expected : U60
* Expected : Data.U60
* Context
* a : U60
* a : Data.U60
/--[suite/checker/fail/MismatchTwo.kind2:2:10]
|
1 | Main (a: U60): U60
1 | Main (a: Data.U60): Data.U60
2 | Main a = Type
| v---
| \Here!

2
crates/kind-tests/suite/checker/fail/MismatchTwo.kind2
View File

@ -1,2 +1,2 @@
Main (a: U60): U60
Main (a: Data.U60): Data.U60
Main a = Type

6
crates/kind-tests/suite/checker/fail/SimpleOpenNoDerive.kind2
View File

@ -1,10 +1,10 @@
record Pudim {
owo : U60
uwu : U60
owo : Data.U60
uwu : Data.U60
}
#keep
Ok (n: Pudim) : U60
Ok (n: Pudim) : Data.U60
Ok n =
open Pudim n
n.owo

2
crates/kind-tests/suite/checker/fail/Unbound.golden
View File

@ -2,7 +2,7 @@
/--[suite/checker/fail/Unbound.kind2:2:7]
|
1 | Tew : U60
1 | Tew : Data.U60
2 | Tew = owo
| v--
| \Here!

2
crates/kind-tests/suite/checker/fail/Unbound.kind2
View File

@ -1,2 +1,2 @@
Tew : U60
Tew : Data.U60
Tew = owo

4
crates/kind-tests/suite/erasure/Ignores.kind2
View File

@ -1,5 +1,5 @@
Kek <a: U60> : U60
Kek <a: Data.U60> : Data.U60
Kek a = a
Main : U60
Main : Data.U60
Main = 3

6
crates/kind-tests/suite/erasure/Removes.kind2
View File

@ -1,8 +1,8 @@
Kek (a: U60) : U60
Kek (a: Data.U60) : Data.U60
Kek a = a
Main : U60
Main : Data.U60
Main = (Kuk) ~(20)
Kuk : ~(a : U60) -> U60
Kuk : ~(a : Data.U60) -> Data.U60
Kuk = ~x => Kek 3

2
crates/kind-tests/suite/erasure/fail/ShouldErr.golden
View File

@ -2,7 +2,7 @@
/--[suite/erasure/fail/ShouldErr.kind2:2:9]
|
1 | Kek <a: U60> : U60
1 | Kek <a: Data.U60> : Data.U60
2 | Kek a = a
| v
| \It's in relevant position!

6
crates/kind-tests/suite/erasure/fail/ShouldErr.kind2
View File

@ -1,8 +1,8 @@
Kek <a: U60> : U60
Kek <a: Data.U60> : Data.U60
Kek a = a
Main : U60
Main : Data.U60
Main = (Kuk) ~(20)
Kuk : ~(a : U60) -> U60
Kuk : ~(a : Data.U60) -> Data.U60
Kuk = ~x => Kek 3

6
crates/kind-tests/suite/eval/AllFieldsDestruct.kind2
View File

@ -1,10 +1,10 @@
#derive[match]
record Pudim {
owo : U60
uwu : U60
owo : Data.U60
uwu : Data.U60
}
Main : U60
Main : Data.U60
Main =
let Pudim.new owo uwu .. = Pudim.new (uwu = 300) (owo = 200)
(+ owo uwu)

2
crates/kind-tests/suite/eval/DoNotation.golden
View File

@ -1,2 +1,2 @@
(Maybe.some _ 1009)
(Data.Maybe.some _ 1009)

18
crates/kind-tests/suite/eval/DoNotation.kind2
View File

@ -1,12 +1,12 @@
Main : Maybe U60
Main : Data.Maybe Data.U60
Main =
do Maybe {
Maybe.some 3
Maybe.pure 2
ask res = Maybe.pure 2
ask res2 = Maybe.pure 3
match Maybe t = (Maybe.some 4) {
some val => Maybe.pure (+ 1000 (+ val (+ res res2)))
none => Maybe.none
do Data.Maybe {
Data.Maybe.some 3
Data.Maybe.pure 2
ask res = Data.Maybe.pure 2
ask res2 = Data.Maybe.pure 3
match Data.Maybe t = (Data.Maybe.some 4) {
some val => Data.Maybe.pure (+ 1000 (+ val (+ res res2)))
none => Data.Maybe.none
}
}

8
crates/kind-tests/suite/eval/Getters.kind2
View File

@ -1,10 +1,10 @@
#derive[getters]
record Pair (a: Type) (b: Type) {
record Data.Pair (a: Type) (b: Type) {
fst : a
snd : b
}
Main : U60
Main : Data.U60
Main =
let a = (Pair.new 100 200 :: Pair U60 U60)
(+ (Pair.fst.get a) (Pair.snd.get a))
let a = (Data.Pair.new 100 200 :: Data.Pair Data.U60 Data.U60)
(+ (Data.Pair.fst.get a) (Data.Pair.snd.get a))

12
crates/kind-tests/suite/eval/MatchMotive.kind2
View File

@ -1,5 +1,5 @@
#derive[match]
type Maybe (a: Type) {
type Data.Maybe (a: Type) {
some (val: a)
none
}
@ -7,13 +7,13 @@ type Maybe (a: Type) {
Str : Type
Str.nil : Str
MotiveGen (n: Maybe U60) : Type
MotiveGen (Maybe.some _) = U60
MotiveGen Maybe.none = Str
MotiveGen (n: Data.Maybe Data.U60) : Type
MotiveGen (Data.Maybe.some _) = Data.U60
MotiveGen Data.Maybe.none = Str
Main : U60
Main : Data.U60
Main =
match Maybe t = Maybe.some 3 {
match Data.Maybe t = Data.Maybe.some 3 {
some => t.val
none => Str.nil
} : (x => MotiveGen x)

4
crates/kind-tests/suite/eval/PatChar.kind2
View File

@ -1,6 +1,6 @@
Lol (n: U60) : U60
Lol (n: Data.U60) : Data.U60
Lol 'A' = 'A'
Lol _ = 0
Main : U60
Main : Data.U60
Main = (Lol 'A')

12
crates/kind-tests/suite/eval/Setters.kind2
View File

@ -1,12 +1,12 @@
#derive[getters, setters]
record Pair (a: Type) (b: Type) {
record Data.Pair (a: Type) (b: Type) {
fst : a
snd : b
}
Main : U60
Main : Data.U60
Main =
let a = (Pair.new 100 200 :: Pair U60 U60)
let b = Pair.fst.set a 500
let c = Pair.snd.set a (+ (Pair.fst.get b) (Pair.snd.get b))
Pair.snd.get c
let a = (Data.Pair.new 100 200 :: Data.Pair Data.U60 Data.U60)
let b = Data.Pair.fst.set a 500
let c = Data.Pair.snd.set a (+ (Data.Pair.fst.get b) (Data.Pair.snd.get b))
Data.Pair.snd.get c

8
crates/kind-tests/suite/eval/SimpleOpen.kind2
View File

@ -1,16 +1,16 @@
#derive[match]
record Pudim {
owo : U60
uwu : U60
owo : Data.U60
uwu : Data.U60
}
#keep
Ok (n: Pudim) : U60
Ok (n: Pudim) : Data.U60
Ok n =
open Pudim n
(+ n.owo n.uwu)
Main : U60
Main : Data.U60
Main =
let Pudim.new owo .. = Pudim.new (uwu = 300) (owo = 200)
2

18
crates/kind-tests/suite/eval/TestWith.kind2
View File

@ -1,19 +1,19 @@
#derive[match]
type Nat {
succ (pred: Nat)
type Data.Nat {
succ (pred: Data.Nat)
zero
}
Run (n: Nat) : Type
Run (Nat.succ n) = U60
Run (Nat.zero) = U60
Run (n: Data.Nat) : Type
Run (Data.Nat.succ n) = Data.U60
Run (Data.Nat.zero) = Data.U60
Lero <t> (n: Nat) (f: Run n) : U60
Lero <t> (n: Data.Nat) (f: Run n) : Data.U60
Lero t1 n f =
match Nat n with (f : Run n) {
match Data.Nat n with (f : Run n) {
succ => (+ f 2)
zero => (+ f 1)
}
Main : U60
Main = Lero (Nat.succ Nat.zero) 1
Main : Data.U60
Main = Lero (Data.Nat.succ Data.Nat.zero) 1

2
crates/kind-tests/suite/eval/User.golden
View File

@ -1,2 +1,2 @@
(Teste (List.nil _))
(Teste (Data.List.nil _))

12
crates/kind-tests/suite/eval/User.kind2
View File

@ -1,12 +1,12 @@
#kdl_run
Main : U60
Main = Teste List.nil
Main : Data.U60
Main = Teste Data.List.nil
type List (t: Type) {
cons (x: t) (xs: List t)
type Data.List (t: Type) {
cons (x: t) (xs: Data.List t)
nil
}
Teste (n: List U60) : U60
Teste (List.cons 2 xs) = 2
Teste (n: Data.List Data.U60) : Data.U60
Teste (Data.List.cons 2 xs) = 2

14
crates/kind-tests/suite/eval/VecMatch.kind2
View File

@ -1,20 +1,20 @@
type Nat {
succ (pred : Nat)
type Data.Nat {
succ (pred : Data.Nat)
zero
}
#derive[match]
type Vec (t: Type) ~ (n: Nat) {
cons <size : Nat> (x : t) (xs : Vec t size) : Vec t (Nat.succ size)
nil : Vec t Nat.zero
type Vec (t: Type) ~ (n: Data.Nat) {
cons <size : Data.Nat> (x : t) (xs : Vec t size) : Vec t (Data.Nat.succ size)
nil : Vec t Data.Nat.zero
}
Vec.count <t> <n: Nat> (v: Vec t n) : U60
Vec.count <t> <n: Data.Nat> (v: Vec t n) : Data.U60
Vec.count vec =
match Vec vec {
cons xs .. => (+ 1 (Vec.count xs))
nil => 0
}
Main : U60
Main : Data.U60
Main = Vec.count (Vec.cons 10 (Vec.cons 20 (Vec.cons 30 Vec.nil)))

8
crates/kind-tests/suite/eval/With.kind2
View File

@ -1,15 +1,15 @@
#derive[match]
type Maybe (t: Type) {
type Data.Maybe (t: Type) {
some (val: t)
none
}
Main : U60
Main : Data.U60
Main =
let t = Maybe.some 3
let t = Data.Maybe.some 3
let e = 4
let f = 10
match Maybe t with e f {
match Data.Maybe t with e f {
some val => (+ val (+ e f))
none => (* e f)
}

4
crates/kind-tests/suite/issues/checker/ArityOnLet.kind2
View File

@ -1,7 +1,7 @@
A (n : U60) : U60
A (n : Data.U60) : Data.U60
A n = n
ArityOnLet : U60
ArityOnLet : Data.U60
ArityOnLet =
let a = A
2

14
crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.golden
View File

@ -1,15 +1,15 @@
INFO Inspection
* Hole: (Assert (Nat.count_layers n 1))
* Hole: (Assert (Data.Nat.count_layers n 1))
* Context
* n : Nat
* n : Data.Nat
/--[suite/issues/checker/HvmReducesTooMuch.kind2:14:29]
/--[suite/issues/checker/HvmReducesTooMuch.kind2:14:34]
|
13 | Beq_nat_refl (n: Nat) : Assert (Nat.count_layers n 0)
14 | Beq_nat_refl (Nat.succ n) = ?
| v
| \Here!
13 | Beq_nat_refl (n: Data.Nat) : Assert (Data.Nat.count_layers n 0)
14 | Beq_nat_refl (Data.Nat.succ n) = ?
| v
| \Here!

16
crates/kind-tests/suite/issues/checker/HvmReducesTooMuch.kind2
View File

@ -1,14 +1,14 @@
type Nat {
succ (pred: Nat)
type Data.Nat {
succ (pred: Data.Nat)
zero
}
Nat.count_layers (n: Nat) (m: U60) : U60
Nat.count_layers (Nat.succ n) m = Nat.count_layers n (+ m 1)
Nat.count_layers n m = (+ m 1)
Data.Nat.count_layers (n: Data.Nat) (m: Data.U60) : Data.U60
Data.Nat.count_layers (Data.Nat.succ n) m = Data.Nat.count_layers n (+ m 1)
Data.Nat.count_layers n m = (+ m 1)
Assert (num: U60) : Type
Assert (num: Data.U60) : Type
#partial
Beq_nat_refl (n: Nat) : Assert (Nat.count_layers n 0)
Beq_nat_refl (Nat.succ n) = ?
Beq_nat_refl (n: Data.Nat) : Assert (Data.Nat.count_layers n 0)
Beq_nat_refl (Data.Nat.succ n) = ?

30
crates/kind-tests/suite/issues/checker/ISSUE-457.golden
View File

@ -1,15 +1,15 @@
INFO Inspection
* Hole: U60
* Hole: Data.U60
* Context
* n : (Pair U60 U60)
* n.fst : U60
* n.snd : U60
* n : (Data.Pair Data.U60 Data.U60)
* n.fst : Data.U60
* n.snd : Data.U60
/--[suite/issues/checker/ISSUE-457.kind2:10:16]
|
9 | match Pair n {
9 | match Data.Pair n {
10 | new => ?
| v
| \Here!
@ -18,16 +18,16 @@
INFO Inspection
* Hole: U60
* Hole: Data.U60
* Context
* n : (Pair U60 U60)
* n.fst : U60
* n.snd : U60
* n : (Data.Pair Data.U60 Data.U60)
* n.fst : Data.U60
* n.snd : Data.U60
/--[suite/issues/checker/ISSUE-457.kind2:17:5]
|
16 | open Pair n
16 | open Data.Pair n
17 | ?
| v
| \Here!
@ -36,16 +36,16 @@
INFO Inspection
* Hole: U60
* Hole: Data.U60
* Context
* n : (Pair U60 U60)
* fst : U60
* snd : U60
* n : (Data.Pair Data.U60 Data.U60)
* fst : Data.U60
* snd : Data.U60
/--[suite/issues/checker/ISSUE-457.kind2:22:5]
|
21 | let Pair.new fst snd = n
21 | let Data.Pair.new fst snd = n
22 | ?
| v
| \Here!

14
crates/kind-tests/suite/issues/checker/ISSUE-457.kind2
View File

@ -1,24 +1,24 @@
#derive[match]
record Pair (a: Type) (b: Type) {
record Data.Pair (a: Type) (b: Type) {
fst : a
snd : b
}
A (n: Pair U60 U60) : U60
A (n: Data.Pair Data.U60 Data.U60) : Data.U60
A n =
match Pair n {
match Data.Pair n {
new => ?
}
B (n: Pair U60 U60) : U60
B (n: Data.Pair Data.U60 Data.U60) : Data.U60
B n =
open Pair n
open Data.Pair n
?
C (n: Pair U60 U60) : U60
C (n: Data.Pair Data.U60 Data.U60) : Data.U60
C n =
let Pair.new fst snd = n
let Data.Pair.new fst snd = n
?

10
crates/kind-tests/suite/issues/checker/ISSUE-461.golden
View File

@ -1,13 +1,13 @@
INFO Inspection
* Hole: U60
* Hole: Data.U60
* Context
* awoo : Type
* awoo = U60
* uuuhuuul : (List awoo)
* uuuhuuul = (List.nil awoo)
* ooooooo : (List U60)
* awoo = Data.U60
* uuuhuuul : (Data.List awoo)
* uuuhuuul = (Data.List.nil awoo)
* ooooooo : (Data.List Data.U60)
* ooooooo = uuuhuuul
/--[suite/issues/checker/ISSUE-461.kind2:11:5]

10
crates/kind-tests/suite/issues/checker/ISSUE-461.kind2
View File

@ -1,11 +1,11 @@
type List (a: Type) {
cons (x: a) (xs: List a)
type Data.List (a: Type) {
cons (x: a) (xs: Data.List a)
nil
}
Rei : U60
Rei : Data.U60
Rei =
let awoo = U60
let uuuhuuul = ([] :: List awoo)
let awoo = Data.U60
let uuuhuuul = ([] :: Data.List awoo)
let ooooooo = specialize awoo into #0 in uuuhuuul
?

8
crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.golden
View File

@ -3,8 +3,8 @@
/--[suite/issues/checker/MatchDerivationWithAll.kind2:3:10]
|
2 | type WithCtx (a: Type) {
3 | new: U60 -> (WithCtx a)
| v-----------------
3 | new: Data.U60 -> (WithCtx a)
| v----------------------
| \Here!
4 | }
@ -18,8 +18,8 @@
| v------
| \This is the type that should be used instead
:
3 | new: U60 -> (WithCtx a)
| v-----------------
3 | new: Data.U60 -> (WithCtx a)
| v----------------------
| \This is not the type that is being declared
4 | }

2
crates/kind-tests/suite/issues/checker/MatchDerivationWithAll.kind2
View File

@ -1,4 +1,4 @@
#derive[match]
type WithCtx (a: Type) {
new: U60 -> (WithCtx a)
new: Data.U60 -> (WithCtx a)
}

12
crates/kind-tests/suite/issues/checker/TestWith.golden
View File

@ -1,19 +1,19 @@
ERROR Type mismatch
* Got : (Run n)
* Expected : U60
* Expected : Data.U60
* Context
* t1 : Type
* n : Nat
* n : Data.Nat
* f : (Run n)
/--[suite/issues/checker/TestWith.kind2:14:22]
/--[suite/issues/checker/TestWith.kind2:14:27]
|
13 | Lero t1 n f =
14 | match Nat n with f {
| v
| \Here!
14 | match Data.Nat n with f {
| v
| \Here!
15 | succ => (+ f 2)

18
crates/kind-tests/suite/issues/checker/TestWith.kind2
View File

@ -1,20 +1,20 @@
#derive[match]
type Nat {
succ (pred: Nat)
type Data.Nat {
succ (pred: Data.Nat)
zero
}
Run (n: Nat) : Type
Run (Nat.succ n) = U60
Run (Nat.zero) = U60
Run (n: Data.Nat) : Type
Run (Data.Nat.succ n) = Data.U60
Run (Data.Nat.zero) = Data.U60
// Without type specification
Lero <t> (n: Nat) (f: Run n) : U60
Lero <t> (n: Data.Nat) (f: Run n) : Data.U60
Lero t1 n f =
match Nat n with f {
match Data.Nat n with f {
succ => (+ f 2)
zero => (+ f 1)
}
Main : U60
Main = Lero (Nat.succ Nat.zero) 1
Main : Data.U60
Main = Lero (Data.Nat.succ Data.Nat.zero) 1

2
crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.golden
View File

@ -5,7 +5,7 @@
/--[suite/issues/checker/U60ToNatDoesNotReduce.kind2:30:17]
|
29 | Test_anon_fun : (Equal (Nat.succ (Nat.succ (Nat.zero))) (U60.to_nat 5))
29 | Test_anon_fun : (Equal (Data.Nat.succ (Data.Nat.succ (Data.Nat.zero))) (Data.U60.to_nat 5))
30 | Test_anon_fun = ?
| v
| \Here!

28
crates/kind-tests/suite/issues/checker/U60ToNatDoesNotReduce.kind2
View File

@ -2,31 +2,31 @@ Doit3times <x> (f: (x -> x)) (n: x) : x
Doit3times f n = (f (f (f n)))
#partial
Nat.zero : (Nat)
Data.Nat.zero : (Data.Nat)
U60.to_nat (x: U60) : (Nat)
U60.to_nat 0 = (Nat.zero)
U60.to_nat n = (Nat.succ (U60.to_nat (- n 1)))
Data.U60.to_nat (x: Data.U60) : (Data.Nat)
Data.U60.to_nat 0 = (Data.Nat.zero)
Data.U60.to_nat n = (Data.Nat.succ (Data.U60.to_nat (- n 1)))
#partial
Nat.add (a: (Nat)) (b: (Nat)) : (Nat)
Nat.add (Nat.succ a) b = (Nat.succ (Nat.add a b))
Nat.add (Nat.zero) b = b
Data.Nat.add (a: (Data.Nat)) (b: (Data.Nat)) : (Data.Nat)
Data.Nat.add (Data.Nat.succ a) b = (Data.Nat.succ (Data.Nat.add a b))
Data.Nat.add (Data.Nat.zero) b = b
#partial
Nat.succ (pred: (Nat)) : (Nat)
Data.Nat.succ (pred: (Data.Nat)) : (Data.Nat)
Nat : Type
Data.Nat : Type
Main : _
Main = (let a = (Doit3times ((x => (Nat.mul x x)) :: Nat -> Nat) (U60.to_nat 2)); a)
Main = (let a = (Doit3times ((x => (Data.Nat.mul x x)) :: Data.Nat -> Data.Nat) (Data.U60.to_nat 2)); a)
#partial
Nat.mul (a: (Nat)) (b: (Nat)) : (Nat)
Nat.mul (Nat.succ a) b = (Nat.add (Nat.mul a b) b)
Nat.mul (Nat.zero) b = (Nat.zero)
Data.Nat.mul (a: (Data.Nat)) (b: (Data.Nat)) : (Data.Nat)
Data.Nat.mul (Data.Nat.succ a) b = (Data.Nat.add (Data.Nat.mul a b) b)
Data.Nat.mul (Data.Nat.zero) b = (Data.Nat.zero)
Test_anon_fun : (Equal (Nat.succ (Nat.succ (Nat.zero))) (U60.to_nat 5))
Test_anon_fun : (Equal (Data.Nat.succ (Data.Nat.succ (Data.Nat.zero))) (Data.U60.to_nat 5))
Test_anon_fun = ?
Equal <t> (a: t) (b: t) : Type

10
crates/kind-tests/suite/issues/coverage/Bool.kind2
View File

@ -1,9 +1,9 @@
type Bool {
type Data.Bool {
true
false
}
Or (b: Bool) (bo: Bool) : Bool
Or Bool.true _ = Bool.true
Or _ Bool.true = Bool.true
Or Bool.false Bool.false = Bool.false
Or (b: Data.Bool) (bo: Data.Bool) : Data.Bool
Or Data.Bool.true _ = Data.Bool.true
Or _ Data.Bool.true = Data.Bool.true
Or Data.Bool.false Data.Bool.false = Data.Bool.false

6
crates/kind-tests/suite/issues/coverage/ISSUE-463.golden
View File

@ -1,13 +1,13 @@
WARN This function does not cover all the possibilities!
* Missing case : (String.cons _ _)
* Missing case : (Data.String.cons _ _)
/--[suite/issues/coverage/ISSUE-463.kind2:8:1]
|
7 |
8 | Bits.from_hex (x: String) : U60
8 | Bits.from_hex (x: Data.String) : Data.U60
| v------------
| \Here!
9 | Bits.from_hex (String.cons '0' xs) = 2
9 | Bits.from_hex (Data.String.cons '0' xs) = 2

12
crates/kind-tests/suite/issues/coverage/ISSUE-463.kind2
View File

@ -1,10 +1,10 @@
//The coverage check, Native type U60 --bug
//The coverage check, Native type Data.U60 --bug
type String {
cons (x: U60) (xs: String)
type Data.String {
cons (x: Data.U60) (xs: Data.String)
nil
}
Bits.from_hex (x: String) : U60
Bits.from_hex (String.cons '0' xs) = 2
Bits.from_hex (String.cons '1' xs) = 2
Bits.from_hex (x: Data.String) : Data.U60
Bits.from_hex (Data.String.cons '0' xs) = 2
Bits.from_hex (Data.String.cons '1' xs) = 2

6
crates/kind-tests/suite/issues/coverage/IncompleteBool.golden
View File

@ -1,13 +1,13 @@
WARN This function does not cover all the possibilities!
* Missing case : Bool.false Bool.true
* Missing case : Data.Bool.false Data.Bool.true
/--[suite/issues/coverage/IncompleteBool.kind2:6:1]
|
5 |
6 | Or (b: Bool) (bo: Bool) : Bool
6 | Or (b: Data.Bool) (bo: Data.Bool) : Data.Bool
| v-
| \Here!
7 | Or Bool.true _ = Bool.true
7 | Or Data.Bool.true _ = Data.Bool.true

8
crates/kind-tests/suite/issues/coverage/IncompleteBool.kind2
View File

@ -1,8 +1,8 @@
type Bool {
type Data.Bool {
true
false
}
Or (b: Bool) (bo: Bool) : Bool
Or Bool.true _ = Bool.true
Or Bool.false Bool.false = Bool.false
Or (b: Data.Bool) (bo: Data.Bool) : Data.Bool
Or Data.Bool.true _ = Data.Bool.true
Or Data.Bool.false Data.Bool.false = Data.Bool.false

2
crates/kind-tests/suite/issues/eval/CallStr.kind2
View File

@ -1,3 +1,3 @@
Main : U60 {
Main : Data.U60 {
"ata"
}

22
crates/kind-tests/suite/issues/eval/ISSUE-472.kind2
View File

@ -1,23 +1,23 @@
Char : Type
Char = U60
Data.Char : Type
Data.Char = Data.U60
#inline
String.new_line : (String)
String.new_line = (String.pure (Char.newline))
Data.String.new_line : (Data.String)
Data.String.new_line = (Data.String.pure (Data.Char.newline))
Main : _
Main = String.new_line
Main = Data.String.new_line
#inline
Char.newline : (Char)
Char.newline = 10
Data.Char.newline : (Data.Char)
Data.Char.newline = 10
#derive[match]
type String {
type Data.String {
nil
cons (head: (Char)) (tail: (String))
cons (head: (Data.Char)) (tail: (Data.String))
}
#inline
String.pure (x: (Char)) : (String)
String.pure x = (String.cons x (String.nil))
Data.String.pure (x: (Data.Char)) : (Data.String)
Data.String.pure x = (Data.String.cons x (Data.String.nil))

2
crates/kind-tests/suite/issues/run/CallStr.kind2
View File

@ -1,3 +1,3 @@
Main : U60 {
Main : Data.U60 {
"ata"
}

22
crates/kind-tests/suite/issues/run/ISSUE-472.kind2
View File

@ -1,23 +1,23 @@
Char : Type
Char = U60
Data.Char : Type
Data.Char = Data.U60
#inline
String.new_line : (String)
String.new_line = (String.pure (Char.newline))
Data.String.new_line : (Data.String)
Data.String.new_line = (Data.String.pure (Data.Char.newline))
Main : _
Main = String.new_line
Main = Data.String.new_line
#inline
Char.newline : (Char)
Char.newline = 10
Data.Char.newline : (Data.Char)
Data.Char.newline = 10
#derive[match]
type String {
type Data.String {
nil
cons (head: (Char)) (tail: (String))
cons (head: (Data.Char)) (tail: (Data.String))
}
#inline
String.pure (x: (Char)) : (String)
String.pure x = (String.cons x (String.nil))
Data.String.pure (x: (Data.Char)) : (Data.String)
Data.String.pure x = (Data.String.cons x (Data.String.nil))

2
crates/kind-tests/suite/kdl/ChangeName.kind2
View File

@ -1,4 +1,4 @@
#kdl_name = JOJO
#keep
Jonathan.Joestar : U60
Jonathan.Joestar : Data.U60
Jonathan.Joestar = 42

2
crates/kind-tests/suite/kdl/Constructor.golden
View File

@ -1,3 +1,3 @@
ctr {Ata}
ctr {Kek}
ctr {Bee}
ctr {Ata}

2
crates/kind-tests/suite/kdl/Constructor.kind2
View File

@ -1,6 +1,6 @@
#kdl_name = Kek
#keep
type Bool {
type Data.Bool {
#kdl_name = Ata
#keep

18
crates/kind-tests/suite/kdl/ISSUE-491-2.golden
View File

@ -1,17 +1,17 @@
ctr {String.nil}
ctr {Pair.new fst snd}
ctr {String.cons head tail}
ctr {USaeFJLF9ugE head tail}
ctr {elNhOG2o_j4N fst snd}
ctr {QfIbR9TgcoZc}
fun (Test n) {
(Test ~) = (!@x1 (!@x1.0 (Pair.match x1.0 @x2 (!@x2.0 @~ (String.match x2.0 #1 @~ @~ #2) x2)) x1) {Pair.new {String.cons #84 {String.cons #101 {String.cons #115 {String.cons #116 {String.cons #101 {String.nil}}}}}} #0})
(Test ~) = (!@x1 (!@x1.0 (T0Fu9pW_avGi x1.0 @x2 (!@x2.0 @~ (xNjG8UGUAGaO x2.0 #1 @~ @~ #2) x2)) x1) {elNhOG2o_j4N {USaeFJLF9ugE #84 {USaeFJLF9ugE #101 {USaeFJLF9ugE #115 {USaeFJLF9ugE #116 {USaeFJLF9ugE #101 {QfIbR9TgcoZc}}}}}} #0})
}
fun (Pair.match scrutinee new_) {
(Pair.match {Pair.new x0 x1} x2) = (!@x2.0 (!@x1.0 (!@x0.0 (!(!x2.0 x0.0) x1.0) x0) x1) x2)
fun (T0Fu9pW_avGi scrutinee new_) {
(T0Fu9pW_avGi {elNhOG2o_j4N x0 x1} x2) = (!@x2.0 (!@x1.0 (!@x0.0 (!(!x2.0 x0.0) x1.0) x0) x1) x2)
}
fun (String.match scrutinee nil_ cons_) {
(String.match {String.nil} x0 ~) = (!@x0.0 x0.0 x0)
(String.match {String.cons x0 x1} ~ x3) = (!@x3.0 (!@x1.0 (!@x0.0 (!(!x3.0 x0.0) x1.0) x0) x1) x3)
fun (xNjG8UGUAGaO scrutinee nil_ cons_) {
(xNjG8UGUAGaO {QfIbR9TgcoZc} x0 ~) = (!@x0.0 x0.0 x0)
(xNjG8UGUAGaO {USaeFJLF9ugE x0 x1} ~ x3) = (!@x3.0 (!@x1.0 (!@x0.0 (!(!x3.0 x0.0) x1.0) x0) x1) x3)
}

18
crates/kind-tests/suite/kdl/ISSUE-491-2.kind2
View File

@ -1,28 +1,28 @@
Char : Type
Char = U60
Data.Char : Type
Data.Char = Data.U60
#kdl_name = T2
#kdl_erase
#derive[match]
record Pair (a) (b) {
record Data.Pair (a) (b) {
constructor new
fst : a
snd : b
}
#derive[match]
type String {
type Data.String {
nil
cons (head: (Char)) (tail: (String))
cons (head: (Data.Char)) (tail: (Data.String))
}
#keep
Test (n: U60) : U60
Test (n: Data.U60) : Data.U60
Test n =
let state = Pair.new "Teste" 0
match Pair state {
let state = Data.Pair.new "Teste" 0
match Data.Pair state {
new =>
match String state.fst {
match Data.String state.fst {
nil =>
1
cons =>

8
crates/kind-tests/suite/kdl/Lambda.kind2
View File

@ -1,10 +1,10 @@
#keep
CoolFn : U60 -> U60 {
(x: U60) => (* 2 x)
CoolFn : Data.U60 -> Data.U60 {
(x: Data.U60) => (* 2 x)
}
#keep
CoolFnApp (n: U60) : U60 {
let lam = (x: U60) => ((CoolFn) x)
CoolFnApp (n: Data.U60) : Data.U60 {
let lam = (x: Data.U60) => ((CoolFn) x)
(lam n)
}

8
crates/kind-tests/suite/kdl/LinearizeVars.golden
View File

@ -1,10 +1,10 @@
ctr {List.cons h t}
ctr {zsfQr6_MzW7G h t}
fun (U120.new hi lo) {
(U120.new x0 x1) = (!@x1.0 (!@x0.0 (| (<< x0.0 #60) x1.0) x0) x1)
fun (9rVKCpdXApqm hi lo) {
(9rVKCpdXApqm x0 x1) = (!@x1.0 (!@x0.0 (| (<< x0.0 #60) x1.0) x0) x1)
}
fun (TestFunc xs) {
(TestFunc {List.cons ~ x1}) = (!@x1.0 (!@x2 dup c.0 x2.0 = x2; dup x2.1 x2.2 = c.0; (!@x3 (!@x3.0 (!@~ {List.cons {U120.add x2.0 x3.0} x1.0} #4) x3) {U120.add x2.1 x2.2}) #2) x1)
(TestFunc {zsfQr6_MzW7G ~ x1}) = (!@x1.0 (!@x2 dup c.0 x2.0 = x2; dup x2.1 x2.2 = c.0; (!@x3 (!@x3.0 (!@~ {zsfQr6_MzW7G {w4Xd4rma6YBa x2.0 x3.0} x1.0} #4) x3) {w4Xd4rma6YBa x2.1 x2.2}) #2) x1)
}

20
crates/kind-tests/suite/kdl/LinearizeVars.kind2
View File

@ -1,17 +1,17 @@
U120 : Type
U120.new (a: U60) (b: U60) : U120
Data.U120 : Type
Data.U120.new (a: Data.U60) (b: Data.U60) : Data.U120
#kdl_erase
U120.add (a: U120) (b: U120) : U120
Data.U120.add (a: Data.U120) (b: Data.U120) : Data.U120
List : Type
List.nil : List
List.cons (h: U120) (t: List) : Type
Data.List : Type
Data.List.nil : Data.List
Data.List.cons (h: Data.U120) (t: Data.List) : Type
#keep
TestFunc (xs: List) : List
TestFunc (List.cons h t) =
TestFunc (xs: Data.List) : Data.List
TestFunc (Data.List.cons h t) =
let aa = 2u120
let bb = (U120.add aa aa)
let bb = (Data.U120.add aa aa)
let cc = 4u120
List.cons (U120.add aa bb) t
Data.List.cons (Data.U120.add aa bb) t

2
crates/kind-tests/suite/kdl/LongNameChange.kind2
View File

@ -1,4 +1,4 @@
#kdl_name = JOJO
#keep
Jonathan.Joestar.PUdim.Pudim.Pudim : U60
Jonathan.Joestar.PUdim.Pudim.Pudim : Data.U60
Jonathan.Joestar.PUdim.Pudim.Pudim = 42

2
crates/kind-tests/suite/kdl/LongNameHash.kind2
View File

@ -1,3 +1,3 @@
#keep
Jonathan.Joestar.PUdim.Pudim.Pudim : U60
Jonathan.Joestar.PUdim.Pudim.Pudim : Data.U60
Jonathan.Joestar.PUdim.Pudim.Pudim = 42

4
crates/kind-tests/suite/kdl/NonInlineState.golden
View File

@ -3,8 +3,8 @@
/--[suite/kdl/NonInlineState.kind2:7:1]
|
6 |
7 | MyFn.state : U60
| v---------------
7 | MyFn.state : Data.U60
| v--------------------
| \Here!

Some files were not shown because too many files have changed in this diff Show More