mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-09-11 07:15:45 +03:00
feat: Update basic function names for Kindex update
This commit is contained in:
parent
b09fadd441
commit
e7c0371373
@ -44,7 +44,7 @@ fn lift_spine(spine: Vec<Box<Term>>) -> Vec<Box<Term>> {
|
|||||||
if spine.len() > 16 {
|
if spine.len() > 16 {
|
||||||
let mut start = spine[..2].to_vec();
|
let mut start = spine[..2].to_vec();
|
||||||
start.push(Box::new(Term::Ctr {
|
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(),
|
args: spine[2..].to_vec(),
|
||||||
}));
|
}));
|
||||||
start
|
start
|
||||||
@ -101,7 +101,7 @@ fn range_to_num(lhs: bool, range: Range) -> Box<Term> {
|
|||||||
|
|
||||||
fn set_origin(ident: &Ident) -> Box<Term> {
|
fn set_origin(ident: &Ident) -> Box<Term> {
|
||||||
mk_lifted_ctr(
|
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())],
|
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> {
|
fn desugar_str(input: &str, range: Range) -> Box<desugared::Expr> {
|
||||||
let nil = QualifiedIdent::new_static("String.nil", None, range);
|
let nil = QualifiedIdent::new_static("Data.String.nil", None, range);
|
||||||
let cons = QualifiedIdent::new_static("String.cons", None, range);
|
let cons = QualifiedIdent::new_static("Data.String.cons", None, range);
|
||||||
input
|
input
|
||||||
.chars()
|
.chars()
|
||||||
.rfold(desugared::Expr::ctr(range, nil, vec![]), |right, chr| {
|
.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> {
|
fn codegen_str(input: &str) -> Box<Term> {
|
||||||
input.chars().rfold(
|
input.chars().rfold(
|
||||||
Box::new(Term::Ctr {
|
Box::new(Term::Ctr {
|
||||||
name: "String.nil".to_string(),
|
name: "Data.String.nil".to_string(),
|
||||||
args: vec![],
|
args: vec![],
|
||||||
}),
|
}),
|
||||||
|right, chr| {
|
|right, chr| {
|
||||||
Box::new(Term::Ctr {
|
Box::new(Term::Ctr {
|
||||||
name: "String.cons".to_string(),
|
name: "Data.String.cons".to_string(),
|
||||||
args: vec![mk_u60(chr as u64), right],
|
args: vec![mk_u60(chr as u64), right],
|
||||||
})
|
})
|
||||||
},
|
},
|
||||||
@ -339,8 +339,8 @@ fn codegen_vec<T>(exprs: T) -> Box<Term>
|
|||||||
where
|
where
|
||||||
T: DoubleEndedIterator<Item = Box<Term>>,
|
T: DoubleEndedIterator<Item = Box<Term>>,
|
||||||
{
|
{
|
||||||
exprs.rfold(mk_ctr("List.nil".to_string(), vec![]), |left, right| {
|
exprs.rfold(mk_ctr("Data.List.nil".to_string(), vec![]), |left, right| {
|
||||||
mk_ctr("List.cons".to_string(), vec![right, left])
|
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),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
TermTag::HoasF(rule.name.to_string()).to_string(),
|
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(
|
rhs: mk_ctr(
|
||||||
"HVM.print".to_owned(),
|
"Apps.HVM.print".to_owned(),
|
||||||
vec![
|
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"),
|
mk_var("ret"),
|
||||||
],
|
],
|
||||||
),
|
),
|
||||||
@ -449,7 +449,7 @@ fn codegen_entry_rules(
|
|||||||
) -> Box<Term> {
|
) -> Box<Term> {
|
||||||
if pats.is_empty() {
|
if pats.is_empty() {
|
||||||
mk_ctr(
|
mk_ctr(
|
||||||
"Kind.Rule.rhs".to_owned(),
|
"Apps.Kind.Rule.rhs".to_owned(),
|
||||||
vec![mk_ctr(
|
vec![mk_ctr(
|
||||||
format!("QT{}", index),
|
format!("QT{}", index),
|
||||||
vec_preppend![
|
vec_preppend![
|
||||||
@ -464,7 +464,7 @@ fn codegen_entry_rules(
|
|||||||
let expr = codegen_all_expr(true, false, count, false, pat);
|
let expr = codegen_all_expr(true, false, count, false, pat);
|
||||||
args.push(expr.clone());
|
args.push(expr.clone());
|
||||||
mk_ctr(
|
mk_ctr(
|
||||||
"Kind.Rule.lhs".to_owned(),
|
"Apps.Kind.Rule.lhs".to_owned(),
|
||||||
vec![
|
vec![
|
||||||
expr,
|
expr,
|
||||||
codegen_entry_rules(count, index + 1, args, entry, &pats[1..]),
|
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) {
|
fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
|
||||||
file.rules.push(lang::Rule {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.NameOf".to_owned(),
|
"Apps.Kind.Axiom.NameOf".to_owned(),
|
||||||
vec![mk_ctr_name(&entry.name)],
|
vec![mk_ctr_name(&entry.name)],
|
||||||
),
|
),
|
||||||
rhs: codegen_str(entry.name.to_string().as_str()),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.OrigOf".to_owned(),
|
"Apps.Kind.Axiom.OrigOf".to_owned(),
|
||||||
vec![mk_ctr_name(&entry.name)],
|
vec![mk_ctr_name(&entry.name)],
|
||||||
),
|
),
|
||||||
rhs: range_to_num(false, entry.name.range),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.HashOf".to_owned(),
|
"Apps.Kind.Axiom.HashOf".to_owned(),
|
||||||
vec![mk_ctr_name(&entry.name)],
|
vec![mk_ctr_name(&entry.name)],
|
||||||
),
|
),
|
||||||
rhs: mk_u60(fxhash::hash64(entry.name.to_string().as_str())),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.TypeOf".to_owned(),
|
"Apps.Kind.Axiom.TypeOf".to_owned(),
|
||||||
vec![mk_ctr_name(&entry.name)],
|
vec![mk_ctr_name(&entry.name)],
|
||||||
),
|
),
|
||||||
rhs: codegen_type(&entry.args, &entry.typ),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_lifted_ctr(
|
lhs: mk_lifted_ctr(
|
||||||
format!("Kind.Term.FN{}", entry.args.len()),
|
format!("Apps.Kind.Term.FN{}", entry.args.len()),
|
||||||
vec_preppend![
|
vec_preppend![
|
||||||
mk_ctr_name(&entry.name),
|
mk_ctr_name(&entry.name),
|
||||||
mk_var("orig");
|
mk_var("orig");
|
||||||
@ -561,7 +561,7 @@ fn codegen_entry(file: &mut lang::File, entry: &desugared::Entry) {
|
|||||||
|
|
||||||
file.rules.push(lang::Rule {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.RuleOf".to_owned(),
|
"Apps.Kind.Axiom.RuleOf".to_owned(),
|
||||||
vec![mk_ctr_name(&entry.name)],
|
vec![mk_ctr_name(&entry.name)],
|
||||||
),
|
),
|
||||||
rhs: codegen_vec(rules),
|
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 {
|
if !entry.rules.is_empty() && !entry.rules[0].pats.is_empty() && !entry.attrs.partial && !entry.attrs.axiom {
|
||||||
file.rules.push(lang::Rule {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.CoverCheck".to_owned(),
|
"Apps.Kind.Axiom.CoverCheck".to_owned(),
|
||||||
vec![mk_ctr_name(&entry.name)],
|
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() {
|
for family in book.families.values() {
|
||||||
file.rules.push(lang::Rule {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.Family.Constructors".to_owned(),
|
"Apps.Kind.Axiom.Family.Constructors".to_owned(),
|
||||||
vec![mk_ctr_name(&family.name)],
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.Family.Params".to_owned(),
|
"Apps.Kind.Axiom.Family.Params".to_owned(),
|
||||||
vec![mk_ctr_name(&family.name)],
|
vec![mk_ctr_name(&family.name)],
|
||||||
),
|
),
|
||||||
rhs: mk_u60(family.parameters.len() as u64),
|
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 entry = book.entrs.get(constructor.to_str()).unwrap();
|
||||||
|
|
||||||
let mut maker = mk_ctr(
|
let mut maker = mk_ctr(
|
||||||
"Kind.Coverage.Maker.End".to_string(),
|
"Apps.Kind.Coverage.Maker.End".to_string(),
|
||||||
vec![codegen_expr(
|
vec![codegen_expr(
|
||||||
false,
|
false,
|
||||||
&kind_tree::desugared::Expr::ctr(
|
&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() {
|
for arg in entry.args[family.parameters.len()..].iter().rev() {
|
||||||
maker = mk_ctr(
|
maker = mk_ctr(
|
||||||
"Kind.Coverage.Maker.Cons".to_string(),
|
"Apps.Kind.Coverage.Maker.Cons".to_string(),
|
||||||
vec![
|
vec![
|
||||||
range_to_num(false, arg.range),
|
range_to_num(false, arg.range),
|
||||||
codegen_all_expr(false, false, &mut 0, false, &arg.typ),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Coverage.Maker.Mk".to_owned(),
|
"Apps.Kind.Coverage.Maker.Mk".to_owned(),
|
||||||
vec![
|
vec![
|
||||||
mk_ctr_name(constructor),
|
mk_ctr_name(constructor),
|
||||||
mk_var("orig"),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.Compare".to_owned(),
|
"Apps.Kind.Axiom.Compare".to_owned(),
|
||||||
vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.ArgsCount".to_owned(),
|
"Apps.Kind.Axiom.ArgsCount".to_owned(),
|
||||||
vec![mk_ctr_name(constructor)],
|
vec![mk_ctr_name(constructor)],
|
||||||
),
|
),
|
||||||
rhs: mk_u60(entry.args.len() as u64),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.Compare".to_owned(),
|
"Apps.Kind.Axiom.Compare".to_owned(),
|
||||||
vec![mk_ctr_name(constructor), mk_ctr_name(constructor)],
|
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 {
|
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))),
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr("Kind.Axiom.CoverCheck".to_owned(), vec![mk_var("_")]),
|
lhs: mk_ctr("Apps.Kind.Axiom.CoverCheck".to_owned(), vec![mk_var("_")]),
|
||||||
rhs: mk_single_ctr("Bool.false".to_string()),
|
rhs: mk_single_ctr("Data.Bool.false".to_string()),
|
||||||
});
|
});
|
||||||
|
|
||||||
if check_coverage {
|
if check_coverage {
|
||||||
file.rules.push(lang::Rule {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
lhs: mk_ctr(
|
||||||
"Kind.Axiom.Compare".to_owned(),
|
"Apps.Kind.Axiom.Compare".to_owned(),
|
||||||
vec![mk_var("a"), mk_var("b")],
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr(
|
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")],
|
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 {
|
file.rules.push(lang::Rule {
|
||||||
lhs: mk_ctr("Kind.Axiom.Family.Constructors".to_owned(), vec![mk_var("_")]),
|
lhs: mk_ctr("Apps.Kind.Axiom.Family.Constructors".to_owned(), vec![mk_var("_")]),
|
||||||
rhs: mk_single_ctr("Maybe.none".to_string()),
|
rhs: mk_single_ctr("Data.Maybe.none".to_string()),
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -46,21 +46,21 @@ pub enum EvalTag {
|
|||||||
impl fmt::Display for TermTag {
|
impl fmt::Display for TermTag {
|
||||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
TermTag::Var => write!(f, "Kind.Term.var"),
|
TermTag::Var => write!(f, "Apps.Kind.Term.var"),
|
||||||
TermTag::All => write!(f, "Kind.Term.all"),
|
TermTag::All => write!(f, "Apps.Kind.Term.all"),
|
||||||
TermTag::Lambda => write!(f, "Kind.Term.lam"),
|
TermTag::Lambda => write!(f, "Apps.Kind.Term.lam"),
|
||||||
TermTag::App => write!(f, "Kind.Term.app"),
|
TermTag::App => write!(f, "Apps.Kind.Term.app"),
|
||||||
TermTag::Fun(n) => write!(f, "Kind.Term.fn{}", n),
|
TermTag::Fun(n) => write!(f, "Apps.Kind.Term.fn{}", n),
|
||||||
TermTag::Ctr(n) => write!(f, "Kind.Term.ct{}", n),
|
TermTag::Ctr(n) => write!(f, "Apps.Kind.Term.ct{}", n),
|
||||||
TermTag::Let => write!(f, "Kind.Term.let"),
|
TermTag::Let => write!(f, "Apps.Kind.Term.let"),
|
||||||
TermTag::Ann => write!(f, "Kind.Term.ann"),
|
TermTag::Ann => write!(f, "Apps.Kind.Term.ann"),
|
||||||
TermTag::Sub => write!(f, "Kind.Term.sub"),
|
TermTag::Sub => write!(f, "Apps.Kind.Term.sub"),
|
||||||
TermTag::Typ => write!(f, "Kind.Term.typ"),
|
TermTag::Typ => write!(f, "Apps.Kind.Term.typ"),
|
||||||
TermTag::U60 => write!(f, "Kind.Term.U60"),
|
TermTag::U60 => write!(f, "Apps.Kind.Term.U60"),
|
||||||
TermTag::NUMU60 => write!(f, "Kind.Term.u60"),
|
TermTag::NUMU60 => write!(f, "Apps.Kind.Term.u60"),
|
||||||
TermTag::Binary => write!(f, "Kind.Term.op2"),
|
TermTag::Binary => write!(f, "Apps.Kind.Term.op2"),
|
||||||
TermTag::Hole => write!(f, "Kind.Term.hol"),
|
TermTag::Hole => write!(f, "Apps.Kind.Term.hol"),
|
||||||
TermTag::Hlp => write!(f, "Kind.Term.hlp"),
|
TermTag::Hlp => write!(f, "Apps.Kind.Term.hlp"),
|
||||||
TermTag::HoasF(name) => write!(f, "F${}", name),
|
TermTag::HoasF(name) => write!(f, "F${}", name),
|
||||||
TermTag::HoasQ(name) => write!(f, "Q${}", name),
|
TermTag::HoasQ(name) => write!(f, "Q${}", name),
|
||||||
}
|
}
|
||||||
@ -70,11 +70,11 @@ impl fmt::Display for TermTag {
|
|||||||
impl fmt::Display for EvalTag {
|
impl fmt::Display for EvalTag {
|
||||||
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
|
||||||
match self {
|
match self {
|
||||||
EvalTag::Op => write!(f, "Kind.Term.eval_op"),
|
EvalTag::Op => write!(f, "Apps.Kind.Term.eval_op"),
|
||||||
EvalTag::App => write!(f, "Kind.Term.eval_app"),
|
EvalTag::App => write!(f, "Apps.Kind.Term.eval_app"),
|
||||||
EvalTag::Let => write!(f, "Kind.Term.eval_let"),
|
EvalTag::Let => write!(f, "Apps.Kind.Term.eval_let"),
|
||||||
EvalTag::Ann => write!(f, "Kind.Term.eval_ann"),
|
EvalTag::Ann => write!(f, "Apps.Kind.Term.eval_ann"),
|
||||||
EvalTag::Sub => write!(f, "Kind.Term.eval_sub"),
|
EvalTag::Sub => write!(f, "Apps.Kind.Term.eval_sub"),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -83,21 +83,21 @@ impl fmt::Display for EvalTag {
|
|||||||
/// by the checker.
|
/// by the checker.
|
||||||
pub fn operator_to_constructor<'a>(operator: Operator) -> &'a str {
|
pub fn operator_to_constructor<'a>(operator: Operator) -> &'a str {
|
||||||
match operator {
|
match operator {
|
||||||
Operator::Add => "Kind.Operator.add",
|
Operator::Add => "Apps.Kind.Operator.add",
|
||||||
Operator::Sub => "Kind.Operator.sub",
|
Operator::Sub => "Apps.Kind.Operator.sub",
|
||||||
Operator::Mul => "Kind.Operator.mul",
|
Operator::Mul => "Apps.Kind.Operator.mul",
|
||||||
Operator::Div => "Kind.Operator.div",
|
Operator::Div => "Apps.Kind.Operator.div",
|
||||||
Operator::Mod => "Kind.Operator.mod",
|
Operator::Mod => "Apps.Kind.Operator.mod",
|
||||||
Operator::And => "Kind.Operator.and",
|
Operator::And => "Apps.Kind.Operator.and",
|
||||||
Operator::Xor => "Kind.Operator.xor",
|
Operator::Xor => "Apps.Kind.Operator.xor",
|
||||||
Operator::Shl => "Kind.Operator.shl",
|
Operator::Shl => "Apps.Kind.Operator.shl",
|
||||||
Operator::Shr => "Kind.Operator.shr",
|
Operator::Shr => "Apps.Kind.Operator.shr",
|
||||||
Operator::Ltn => "Kind.Operator.ltn",
|
Operator::Ltn => "Apps.Kind.Operator.ltn",
|
||||||
Operator::Lte => "Kind.Operator.lte",
|
Operator::Lte => "Apps.Kind.Operator.lte",
|
||||||
Operator::Eql => "Kind.Operator.eql",
|
Operator::Eql => "Apps.Kind.Operator.eql",
|
||||||
Operator::Gte => "Kind.Operator.gte",
|
Operator::Gte => "Apps.Kind.Operator.gte",
|
||||||
Operator::Gtn => "Kind.Operator.gtn",
|
Operator::Gtn => "Apps.Kind.Operator.gtn",
|
||||||
Operator::Neq => "Kind.Operator.neq",
|
Operator::Neq => "Apps.Kind.Operator.neq",
|
||||||
Operator::Or => "Kind.Operator.or",
|
Operator::Or => "Apps.Kind.Operator.or",
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -110,7 +110,7 @@ pub fn eval_api(book: &Book) -> (String, u64) {
|
|||||||
runtime::link(
|
runtime::link(
|
||||||
&heap,
|
&heap,
|
||||||
0,
|
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;
|
let host = 0;
|
||||||
|
|
||||||
|
@ -35,22 +35,22 @@ fn parse_num(term: &Term) -> Result<u64, String> {
|
|||||||
fn parse_op(term: &Term) -> Result<Operator, String> {
|
fn parse_op(term: &Term) -> Result<Operator, String> {
|
||||||
match term {
|
match term {
|
||||||
Term::Ctr { name, args: _ } => match name.as_str() {
|
Term::Ctr { name, args: _ } => match name.as_str() {
|
||||||
"Kind.Operator.add" => Ok(Operator::Add),
|
"Apps.Kind.Operator.add" => Ok(Operator::Add),
|
||||||
"Kind.Operator.sub" => Ok(Operator::Sub),
|
"Apps.Kind.Operator.sub" => Ok(Operator::Sub),
|
||||||
"Kind.Operator.mul" => Ok(Operator::Mul),
|
"Apps.Kind.Operator.mul" => Ok(Operator::Mul),
|
||||||
"Kind.Operator.div" => Ok(Operator::Div),
|
"Apps.Kind.Operator.div" => Ok(Operator::Div),
|
||||||
"Kind.Operator.mod" => Ok(Operator::Mod),
|
"Apps.Kind.Operator.mod" => Ok(Operator::Mod),
|
||||||
"Kind.Operator.and" => Ok(Operator::And),
|
"Apps.Kind.Operator.and" => Ok(Operator::And),
|
||||||
"Kind.Operator.or" => Ok(Operator::Or),
|
"Apps.Kind.Operator.or" => Ok(Operator::Or),
|
||||||
"Kind.Operator.xor" => Ok(Operator::Xor),
|
"Apps.Kind.Operator.xor" => Ok(Operator::Xor),
|
||||||
"Kind.Operator.shl" => Ok(Operator::Shl),
|
"Apps.Kind.Operator.shl" => Ok(Operator::Shl),
|
||||||
"Kind.Operator.shr" => Ok(Operator::Shr),
|
"Apps.Kind.Operator.shr" => Ok(Operator::Shr),
|
||||||
"Kind.Operator.ltn" => Ok(Operator::Ltn),
|
"Apps.Kind.Operator.ltn" => Ok(Operator::Ltn),
|
||||||
"Kind.Operator.lte" => Ok(Operator::Lte),
|
"Apps.Kind.Operator.lte" => Ok(Operator::Lte),
|
||||||
"Kind.Operator.eql" => Ok(Operator::Eql),
|
"Apps.Kind.Operator.eql" => Ok(Operator::Eql),
|
||||||
"Kind.Operator.gte" => Ok(Operator::Gte),
|
"Apps.Kind.Operator.gte" => Ok(Operator::Gte),
|
||||||
"Kind.Operator.gtn" => Ok(Operator::Gtn),
|
"Apps.Kind.Operator.gtn" => Ok(Operator::Gtn),
|
||||||
"Kind.Operator.neq" => Ok(Operator::Neq),
|
"Apps.Kind.Operator.neq" => Ok(Operator::Neq),
|
||||||
_ => Err("Cannot recognized operator".to_string()),
|
_ => Err("Cannot recognized operator".to_string()),
|
||||||
},
|
},
|
||||||
_ => Err("Error parsing operator".to_string()),
|
_ => Err("Error parsing operator".to_string()),
|
||||||
@ -91,44 +91,44 @@ fn parse_all_expr(
|
|||||||
) -> Result<Box<desugared::Expr>, String> {
|
) -> Result<Box<desugared::Expr>, String> {
|
||||||
match term {
|
match term {
|
||||||
Term::Ctr { name, args } => match name.as_str() {
|
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])?,
|
parse_orig(&args[0])?,
|
||||||
Ident::generate(&parse_name(&args[1])?),
|
Ident::generate(&parse_name(&args[1])?),
|
||||||
parse_all_expr(names.clone(), &args[2])?,
|
parse_all_expr(names.clone(), &args[2])?,
|
||||||
parse_all_expr(names, &args[3])?,
|
parse_all_expr(names, &args[3])?,
|
||||||
false, // TODO: Fix
|
false, // TODO: Fix
|
||||||
)),
|
)),
|
||||||
"Kind.Term.Quoted.lam" => Ok(Expr::lambda(
|
"Apps.Kind.Term.Quoted.lam" => Ok(Expr::lambda(
|
||||||
parse_orig(&args[0])?,
|
parse_orig(&args[0])?,
|
||||||
Ident::generate(&parse_name(&args[1])?),
|
Ident::generate(&parse_name(&args[1])?),
|
||||||
parse_all_expr(names, &args[2])?,
|
parse_all_expr(names, &args[2])?,
|
||||||
false, // TODO: Fix
|
false, // TODO: Fix
|
||||||
)),
|
)),
|
||||||
"Kind.Term.Quoted.let" => Ok(Expr::let_(
|
"Apps.Kind.Term.Quoted.let" => Ok(Expr::let_(
|
||||||
parse_orig(&args[0])?,
|
parse_orig(&args[0])?,
|
||||||
Ident::generate(&parse_name(&args[1])?),
|
Ident::generate(&parse_name(&args[1])?),
|
||||||
parse_all_expr(names.clone(), &args[2])?,
|
parse_all_expr(names.clone(), &args[2])?,
|
||||||
parse_all_expr(names, &args[3])?,
|
parse_all_expr(names, &args[3])?,
|
||||||
)),
|
)),
|
||||||
"Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
|
"Apps.Kind.Term.Quoted.typ" => Ok(Expr::typ(parse_orig(&args[0])?)),
|
||||||
"Kind.Term.Quoted.var" => Ok(Expr::var(Ident::new(
|
"Apps.Kind.Term.Quoted.var" => Ok(Expr::var(Ident::new(
|
||||||
parse_name(&args[1])?,
|
parse_name(&args[1])?,
|
||||||
parse_orig(&args[0])?,
|
parse_orig(&args[0])?,
|
||||||
))),
|
))),
|
||||||
"Kind.Term.Quoted.hol" => Ok(Expr::hole(parse_orig(&args[0])?, parse_num(&args[1])?)),
|
"Apps.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.ann" => Ok(Expr::ann(
|
||||||
parse_orig(&args[0])?,
|
parse_orig(&args[0])?,
|
||||||
parse_all_expr(names.clone(), &args[1])?,
|
parse_all_expr(names.clone(), &args[1])?,
|
||||||
parse_all_expr(names, &args[2])?,
|
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])?,
|
parse_orig(&args[0])?,
|
||||||
Ident::generate(&parse_name(&args[1])?),
|
Ident::generate(&parse_name(&args[1])?),
|
||||||
parse_num(&args[2])? as usize,
|
parse_num(&args[2])? as usize,
|
||||||
parse_num(&args[3])? as usize,
|
parse_num(&args[3])? as usize,
|
||||||
parse_all_expr(names, &args[4])?,
|
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_orig(&args[0])?,
|
||||||
parse_all_expr(names.clone(), &args[1])?,
|
parse_all_expr(names.clone(), &args[1])?,
|
||||||
vec![desugared::AppBinding {
|
vec![desugared::AppBinding {
|
||||||
@ -136,7 +136,7 @@ fn parse_all_expr(
|
|||||||
erased: false,
|
erased: false,
|
||||||
}],
|
}],
|
||||||
)),
|
)),
|
||||||
"Kind.Term.Quoted.ctr" => {
|
"Apps.Kind.Term.Quoted.ctr" => {
|
||||||
let name = parse_qualified(&args[0])?;
|
let name = parse_qualified(&args[0])?;
|
||||||
let orig = parse_orig(&args[1])?;
|
let orig = parse_orig(&args[1])?;
|
||||||
let mut res = Vec::new();
|
let mut res = Vec::new();
|
||||||
@ -145,7 +145,7 @@ fn parse_all_expr(
|
|||||||
}
|
}
|
||||||
Ok(Expr::ctr(orig, name, res))
|
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_orig(&args[1])?,
|
||||||
parse_qualified(&args[0])?,
|
parse_qualified(&args[0])?,
|
||||||
{
|
{
|
||||||
@ -156,11 +156,11 @@ fn parse_all_expr(
|
|||||||
res
|
res
|
||||||
},
|
},
|
||||||
)),
|
)),
|
||||||
"Kind.Term.Quoted.hlp" => Ok(Expr::hlp(parse_orig(&args[0])?, Ident::generate("?"))),
|
"Apps.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])?)),
|
"Apps.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.num" => Ok(Expr::num_u60(parse_orig(&args[0])?, parse_num(&args[1])?)),
|
||||||
// TODO: Change quoting to support floats
|
// 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_orig(&args[0])?,
|
||||||
parse_op(&args[1])?,
|
parse_op(&args[1])?,
|
||||||
parse_all_expr(names.clone(), &args[2])?,
|
parse_all_expr(names.clone(), &args[2])?,
|
||||||
@ -181,9 +181,9 @@ fn parse_list(term: &Term) -> Result<Vec<Box<Term>>, String> {
|
|||||||
loop {
|
loop {
|
||||||
match cur {
|
match cur {
|
||||||
Term::Ctr { name, args } => {
|
Term::Ctr { name, args } => {
|
||||||
if name == "List.nil" {
|
if name == "Data.List.nil" {
|
||||||
break;
|
break;
|
||||||
} else if name == "List.cons" {
|
} else if name == "Data.List.cons" {
|
||||||
vec.push(args[0].clone());
|
vec.push(args[0].clone());
|
||||||
cur = &args[1];
|
cur = &args[1];
|
||||||
} else {
|
} 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.
|
/// Transforms a HVM quoted entry into a easy to manipulate structure.
|
||||||
pub fn transform_entry(term: &Term) -> Result<Entry, String> {
|
pub fn transform_entry(term: &Term) -> Result<Entry, String> {
|
||||||
match term {
|
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])?;
|
let fst = parse_name(&args[0])?;
|
||||||
match &*args[1] {
|
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 snd = parse_expr(&args[0])?;
|
||||||
let trd = parse_list(&args[1])?;
|
let trd = parse_list(&args[1])?;
|
||||||
let trd = trd.iter().flat_map(|x| parse_expr(x)).collect();
|
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 ctx = Context(entries.collect());
|
||||||
let orig = match_opt!(*args[1], Term::U6O { numb } => EncodedRange(numb).to_range())?;
|
let orig = match_opt!(*args[1], Term::U6O { numb } => EncodedRange(numb).to_range())?;
|
||||||
match name.as_str() {
|
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 args = parse_list(&args[2])?;
|
||||||
let mut new_args = Vec::with_capacity(args.len());
|
let mut new_args = Vec::with_capacity(args.len());
|
||||||
for arg in &args {
|
for arg in &args {
|
||||||
@ -234,25 +234,25 @@ fn parse_type_error(expr: &Term) -> Result<TypeDiagnostic, String> {
|
|||||||
}
|
}
|
||||||
new_args
|
new_args
|
||||||
})),
|
})),
|
||||||
"Kind.Error.Quoted.unbound_variable" => Ok(TypeDiagnostic::UnboundVariable(ctx, orig)),
|
"Apps.Kind.Error.Quoted.unbound_variable" => Ok(TypeDiagnostic::UnboundVariable(ctx, orig)),
|
||||||
"Kind.Error.Quoted.cant_infer_hole" => Ok(TypeDiagnostic::CantInferHole(ctx, orig)),
|
"Apps.Kind.Error.Quoted.cant_infer_hole" => Ok(TypeDiagnostic::CantInferHole(ctx, orig)),
|
||||||
"Kind.Error.Quoted.cant_infer_lambda" => Ok(TypeDiagnostic::CantInferLambda(ctx, orig)),
|
"Apps.Kind.Error.Quoted.cant_infer_lambda" => Ok(TypeDiagnostic::CantInferLambda(ctx, orig)),
|
||||||
"Kind.Error.Quoted.invalid_call" => Ok(TypeDiagnostic::InvalidCall(ctx, orig)),
|
"Apps.Kind.Error.Quoted.invalid_call" => Ok(TypeDiagnostic::InvalidCall(ctx, orig)),
|
||||||
"Kind.Error.Quoted.impossible_case" => Ok(TypeDiagnostic::ImpossibleCase(
|
"Apps.Kind.Error.Quoted.impossible_case" => Ok(TypeDiagnostic::ImpossibleCase(
|
||||||
ctx,
|
ctx,
|
||||||
orig,
|
orig,
|
||||||
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
||||||
parse_all_expr(im_rc::HashMap::new(), &args[3])?,
|
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,
|
ctx,
|
||||||
orig,
|
orig,
|
||||||
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
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))
|
Ok(TypeDiagnostic::TooManyArguments(ctx, orig))
|
||||||
}
|
}
|
||||||
"Kind.Error.Quoted.type_mismatch" => Ok(TypeDiagnostic::TypeMismatch(
|
"Apps.Kind.Error.Quoted.type_mismatch" => Ok(TypeDiagnostic::TypeMismatch(
|
||||||
ctx,
|
ctx,
|
||||||
orig,
|
orig,
|
||||||
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
parse_all_expr(im_rc::HashMap::new(), &args[2])?,
|
||||||
|
@ -214,7 +214,7 @@ impl<'a> Visitor for Subst<'a> {
|
|||||||
snd,
|
snd,
|
||||||
} => {
|
} => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
|
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
|
||||||
"Sigma", None, expr.range,
|
"Data.Sigma", None, expr.range,
|
||||||
));
|
));
|
||||||
self.visit_expr(fst);
|
self.visit_expr(fst);
|
||||||
self.visit_expr(snd);
|
self.visit_expr(snd);
|
||||||
@ -225,7 +225,7 @@ impl<'a> Visitor for Subst<'a> {
|
|||||||
snd,
|
snd,
|
||||||
} => {
|
} => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
|
self.visit_qualified_ident(&mut QualifiedIdent::new_static(
|
||||||
"Sigma", None, expr.range,
|
"Data.Sigma", None, expr.range,
|
||||||
));
|
));
|
||||||
self.visit_expr(fst);
|
self.visit_expr(fst);
|
||||||
self.context_vars.push((ident.range, ident.to_string()));
|
self.context_vars.push((ident.range, ident.to_string()));
|
||||||
@ -257,7 +257,7 @@ impl<'a> Visitor for Subst<'a> {
|
|||||||
}
|
}
|
||||||
ExprKind::If { cond, then_, else_ } => {
|
ExprKind::If { cond, then_, else_ } => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||||
"Bool", "if", expr.range,
|
"Data.Bool", "if", expr.range,
|
||||||
));
|
));
|
||||||
self.visit_expr(cond);
|
self.visit_expr(cond);
|
||||||
self.visit_expr(then_);
|
self.visit_expr(then_);
|
||||||
@ -265,17 +265,17 @@ impl<'a> Visitor for Subst<'a> {
|
|||||||
}
|
}
|
||||||
ExprKind::Pair { fst, snd } => {
|
ExprKind::Pair { fst, snd } => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
||||||
"Pair", "new", expr.range,
|
"Data.Pair", "new", expr.range,
|
||||||
));
|
));
|
||||||
self.visit_expr(fst);
|
self.visit_expr(fst);
|
||||||
self.visit_expr(snd);
|
self.visit_expr(snd);
|
||||||
}
|
}
|
||||||
ExprKind::List { args } => {
|
ExprKind::List { args } => {
|
||||||
self.visit_qualified_ident(&mut QualifiedIdent::new_sugared(
|
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(
|
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));
|
visit_vec!(args.iter_mut(), arg => self.visit_expr(arg));
|
||||||
}
|
}
|
||||||
|
@ -241,10 +241,10 @@ impl<'a> Parser<'a> {
|
|||||||
let id = self.parse_upper_id()?;
|
let id = self.parse_upper_id()?;
|
||||||
let data = match id.to_string().as_str() {
|
let data = match id.to_string().as_str() {
|
||||||
"Type" => ExprKind::Lit { lit: Literal::Type },
|
"Type" => ExprKind::Lit { lit: Literal::Type },
|
||||||
"U60" => ExprKind::Lit {
|
"Data.U60" => ExprKind::Lit {
|
||||||
lit: Literal::NumTypeU60,
|
lit: Literal::NumTypeU60,
|
||||||
},
|
},
|
||||||
"F60" => ExprKind::Lit {
|
"Data.F60" => ExprKind::Lit {
|
||||||
lit: Literal::NumTypeF60,
|
lit: Literal::NumTypeF60,
|
||||||
},
|
},
|
||||||
_ => ExprKind::Constr {
|
_ => ExprKind::Constr {
|
||||||
@ -263,10 +263,10 @@ impl<'a> Parser<'a> {
|
|||||||
let mut range = id.range;
|
let mut range = id.range;
|
||||||
let data = match id.to_string().as_str() {
|
let data = match id.to_string().as_str() {
|
||||||
"Type" => ExprKind::Lit { lit: Literal::Type },
|
"Type" => ExprKind::Lit { lit: Literal::Type },
|
||||||
"U60" => ExprKind::Lit {
|
"Data.U60" => ExprKind::Lit {
|
||||||
lit: Literal::NumTypeU60,
|
lit: Literal::NumTypeU60,
|
||||||
},
|
},
|
||||||
"F60" => ExprKind::Lit {
|
"Data.F60" => ExprKind::Lit {
|
||||||
lit: Literal::NumTypeF60,
|
lit: Literal::NumTypeF60,
|
||||||
},
|
},
|
||||||
_ => {
|
_ => {
|
||||||
|
@ -24,8 +24,8 @@ impl<'a> DesugarState<'a> {
|
|||||||
) -> Box<desugared::Expr> {
|
) -> Box<desugared::Expr> {
|
||||||
match literal {
|
match literal {
|
||||||
Literal::String(string) => {
|
Literal::String(string) => {
|
||||||
if !self.check_implementation("String.cons", range, Sugar::String)
|
if !self.check_implementation("Data.String.cons", range, Sugar::String)
|
||||||
|| !self.check_implementation("String.nil", range, Sugar::String)
|
|| !self.check_implementation("Data.String.nil", range, Sugar::String)
|
||||||
{
|
{
|
||||||
return desugared::Expr::err(range);
|
return desugared::Expr::err(range);
|
||||||
}
|
}
|
||||||
@ -37,7 +37,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
Literal::NumTypeF60 => desugared::Expr::type_f60(range),
|
Literal::NumTypeF60 => desugared::Expr::type_f60(range),
|
||||||
Literal::NumU60(num) => desugared::Expr::num_u60(range, *num),
|
Literal::NumU60(num) => desugared::Expr::num_u60(range, *num),
|
||||||
Literal::Nat(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 cons_ident = list_ident.add_segment("succ");
|
||||||
let nil_ident = list_ident.add_segment("zero");
|
let nil_ident = list_ident.add_segment("zero");
|
||||||
|
|
||||||
@ -50,7 +50,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
res
|
res
|
||||||
}
|
}
|
||||||
Literal::NumU120(num) => {
|
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);
|
return desugared::Expr::err(range);
|
||||||
}
|
}
|
||||||
desugared::Expr::num_u120(range, *num)
|
desugared::Expr::num_u120(range, *num)
|
||||||
@ -292,7 +292,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
typ: &expr::Expr,
|
typ: &expr::Expr,
|
||||||
body: &expr::Expr,
|
body: &expr::Expr,
|
||||||
) -> Box<desugared::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) {
|
if !self.check_implementation(sigma.to_str(), range, Sugar::Sigma) {
|
||||||
return desugared::Expr::err(range);
|
return desugared::Expr::err(range);
|
||||||
@ -316,7 +316,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
range: Range,
|
range: Range,
|
||||||
expr: &[expr::Expr],
|
expr: &[expr::Expr],
|
||||||
) -> Box<desugared::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 cons_ident = list_ident.add_segment("cons");
|
||||||
let nil_ident = list_ident.add_segment("nil");
|
let nil_ident = list_ident.add_segment("nil");
|
||||||
|
|
||||||
@ -345,7 +345,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
if_: &expr::Expr,
|
if_: &expr::Expr,
|
||||||
else_: &expr::Expr,
|
else_: &expr::Expr,
|
||||||
) -> Box<desugared::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_ident = boolean.add_segment("if");
|
||||||
|
|
||||||
let bool_if = self.old_book.names.get(bool_if_ident.to_str());
|
let bool_if = self.old_book.names.get(bool_if_ident.to_str());
|
||||||
@ -419,7 +419,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
fst: &expr::Expr,
|
fst: &expr::Expr,
|
||||||
snd: &expr::Expr,
|
snd: &expr::Expr,
|
||||||
) -> Box<desugared::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) {
|
if !self.check_implementation(sigma_new.to_str(), range, Sugar::Pair) {
|
||||||
return desugared::Expr::err(range);
|
return desugared::Expr::err(range);
|
||||||
|
@ -223,7 +223,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
fst: &concrete::pat::Pat,
|
fst: &concrete::pat::Pat,
|
||||||
snd: &concrete::pat::Pat,
|
snd: &concrete::pat::Pat,
|
||||||
) -> Box<desugared::Expr> {
|
) -> 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());
|
let entry = self.old_book.entries.get(sigma_new.to_string().as_str());
|
||||||
if entry.is_none() {
|
if entry.is_none() {
|
||||||
@ -241,7 +241,7 @@ impl<'a> DesugarState<'a> {
|
|||||||
range: Range,
|
range: Range,
|
||||||
expr: &[concrete::pat::Pat],
|
expr: &[concrete::pat::Pat],
|
||||||
) -> Box<desugared::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 cons_ident = list_ident.add_segment("cons");
|
||||||
let nil_ident = list_ident.add_segment("nil");
|
let nil_ident = list_ident.add_segment("nil");
|
||||||
|
|
||||||
|
@ -218,12 +218,12 @@ impl Diagnostic for PassDiagnostic {
|
|||||||
subtitles: vec![],
|
subtitles: vec![],
|
||||||
hints: vec![match sugar {
|
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::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::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 'Sigma' in order to use the sigma notation.".to_string(),
|
Sugar::Sigma => "You must implement 'Data.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::Pair => "You must implement 'Data.Sigma' and 'Data.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::BoolIf => "You must implement 'Data.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::String => "You must implement 'Data.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::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::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::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)
|
Sugar::Getter(typ) => format!("You must derive 'getters' for '{}' in order to use this syntax", typ)
|
||||||
|
@ -348,8 +348,8 @@ impl<'a> ErasureState<'a> {
|
|||||||
NumU60 { numb } => untyped::Expr::u60(expr.range, *numb),
|
NumU60 { numb } => untyped::Expr::u60(expr.range, *numb),
|
||||||
NumF60 { numb } => untyped::Expr::f60(expr.range, *numb),
|
NumF60 { numb } => untyped::Expr::f60(expr.range, *numb),
|
||||||
Str { val } => {
|
Str { val } => {
|
||||||
let nil = QualifiedIdent::new_static("String.nil", None, expr.range);
|
let nil = QualifiedIdent::new_static("Data.String.nil", None, expr.range);
|
||||||
let cons = QualifiedIdent::new_static("String.cons", None, expr.range);
|
let cons = QualifiedIdent::new_static("Data.String.cons", None, expr.range);
|
||||||
|
|
||||||
self.connect_with(edge, &nil, relevance);
|
self.connect_with(edge, &nil, relevance);
|
||||||
self.connect_with(edge, &cons, relevance);
|
self.connect_with(edge, &cons, relevance);
|
||||||
@ -491,8 +491,8 @@ impl<'a> ErasureState<'a> {
|
|||||||
NumU60 { numb } => untyped::Expr::u60(expr.range, *numb),
|
NumU60 { numb } => untyped::Expr::u60(expr.range, *numb),
|
||||||
NumF60 { numb } => untyped::Expr::f60(expr.range, *numb),
|
NumF60 { numb } => untyped::Expr::f60(expr.range, *numb),
|
||||||
Str { val } => {
|
Str { val } => {
|
||||||
let nil = QualifiedIdent::new_static("String.nil", None, expr.range);
|
let nil = QualifiedIdent::new_static("Data.String.nil", None, expr.range);
|
||||||
let cons = QualifiedIdent::new_static("String.cons", None, expr.range);
|
let cons = QualifiedIdent::new_static("Data.String.cons", None, expr.range);
|
||||||
self.connect_with(edge, &nil, ambient);
|
self.connect_with(edge, &nil, ambient);
|
||||||
self.connect_with(edge, &cons, ambient);
|
self.connect_with(edge, &cons, ambient);
|
||||||
|
|
||||||
|
@ -376,7 +376,7 @@ impl Visitor for UnboundCollector {
|
|||||||
match &mut pat.data {
|
match &mut pat.data {
|
||||||
PatKind::Var(ident) => self.visit_pat_ident(ident),
|
PatKind::Var(ident) => self.visit_pat_ident(ident),
|
||||||
PatKind::Str(_) => {
|
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("cons").to_generated());
|
||||||
self.visit_qualified_ident(&mut string.add_segment("nil").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::*;
|
use kind_tree::concrete::Literal::*;
|
||||||
|
|
||||||
if let String(_) = lit {
|
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("cons").to_generated());
|
||||||
self.visit_qualified_ident(&mut string.add_segment("nil").to_generated());
|
self.visit_qualified_ident(&mut string.add_segment("nil").to_generated());
|
||||||
}
|
}
|
||||||
@ -545,7 +545,7 @@ impl Visitor for UnboundCollector {
|
|||||||
snd,
|
snd,
|
||||||
} => {
|
} => {
|
||||||
self.visit_qualified_ident(
|
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(fst);
|
||||||
self.visit_expr(snd);
|
self.visit_expr(snd);
|
||||||
@ -556,7 +556,7 @@ impl Visitor for UnboundCollector {
|
|||||||
snd,
|
snd,
|
||||||
} => {
|
} => {
|
||||||
self.visit_qualified_ident(
|
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(fst);
|
||||||
self.context_vars.push((ident.range, ident.to_string()));
|
self.context_vars.push((ident.range, ident.to_string()));
|
||||||
@ -587,20 +587,20 @@ impl Visitor for UnboundCollector {
|
|||||||
self.visit_sttm(sttm)
|
self.visit_sttm(sttm)
|
||||||
}
|
}
|
||||||
ExprKind::If { cond, then_, else_ } => {
|
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_qualified_ident(&mut typ.add_segment("if").to_generated());
|
||||||
self.visit_expr(cond);
|
self.visit_expr(cond);
|
||||||
self.visit_expr(then_);
|
self.visit_expr(then_);
|
||||||
self.visit_expr(else_);
|
self.visit_expr(else_);
|
||||||
}
|
}
|
||||||
ExprKind::Pair { fst, snd } => {
|
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_qualified_ident(&mut typ.add_segment("new").to_generated());
|
||||||
self.visit_expr(fst);
|
self.visit_expr(fst);
|
||||||
self.visit_expr(snd);
|
self.visit_expr(snd);
|
||||||
}
|
}
|
||||||
ExprKind::List { args } => {
|
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);
|
||||||
self.visit_qualified_ident(&mut typ.add_segment("nil").to_generated());
|
self.visit_qualified_ident(&mut typ.add_segment("nil").to_generated());
|
||||||
|
@ -17,13 +17,13 @@ pub fn compile_book(book: untyped::Book, trace: bool) -> File {
|
|||||||
|
|
||||||
pub fn compile_str(val: &str) -> Box<Term> {
|
pub fn compile_str(val: &str) -> Box<Term> {
|
||||||
let nil = Box::new(Term::Ctr {
|
let nil = Box::new(Term::Ctr {
|
||||||
name: String::from("String.nil"),
|
name: String::from("Data.String.nil"),
|
||||||
args: vec![],
|
args: vec![],
|
||||||
});
|
});
|
||||||
|
|
||||||
let cons = |numb, next| {
|
let cons = |numb, next| {
|
||||||
Box::new(Term::Ctr {
|
Box::new(Term::Ctr {
|
||||||
name: String::from("String.cons"),
|
name: String::from("Data.String.cons"),
|
||||||
args: vec![Box::new(Term::U6O { numb }), next],
|
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(),
|
args: args.clone(),
|
||||||
}),
|
}),
|
||||||
rhs: Box::new(Term::Ctr {
|
rhs: Box::new(Term::Ctr {
|
||||||
name: "HVM.log".to_string(),
|
name: "Apps.HVM.log".to_string(),
|
||||||
args: vec![
|
args: vec![
|
||||||
compile_str(entry.name.to_str()),
|
compile_str(entry.name.to_str()),
|
||||||
Box::new(Term::Ctr {
|
Box::new(Term::Ctr {
|
||||||
|
@ -326,7 +326,7 @@ pub fn compile_expr(ctx: &mut CompileCtx, expr: &untyped::Expr) -> kdl::Term {
|
|||||||
From::Ctr { name, args } => {
|
From::Ctr { name, args } => {
|
||||||
// Convert U120 numbers into the native kindelia representation
|
// Convert U120 numbers into the native kindelia representation
|
||||||
// Only possible if both U60s are U60 terms
|
// 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 }) =
|
if let (From::U60 { numb: hi }, From::U60 { numb: lo }) =
|
||||||
(&args[0].data, &args[1].data)
|
(&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
|
// some numeric function applications
|
||||||
|
|
||||||
// Add with no boundary check is just a normal add
|
// 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,
|
oper: kdl::Oper::Add,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
// U60s are already stored in 120 bits
|
// 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
|
// Truncate to 60 bits
|
||||||
"U120.to_u60" => To::Op2 {
|
"Data.U120.to_u60" => To::Op2 {
|
||||||
oper: kdl::Oper::And,
|
oper: kdl::Oper::And,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(To::Num { numb: U60_MAX }),
|
val1: Box::new(To::Num { numb: U60_MAX }),
|
||||||
},
|
},
|
||||||
// Compilation for U120 numeric operations
|
// Compilation for U120 numeric operations
|
||||||
"U120.add" => To::Op2 {
|
"Data.U120.add" => To::Op2 {
|
||||||
oper: kdl::Oper::Add,
|
oper: kdl::Oper::Add,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.sub" => To::Op2 {
|
"Data.U120.sub" => To::Op2 {
|
||||||
oper: kdl::Oper::Add,
|
oper: kdl::Oper::Add,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.mul" => To::Op2 {
|
"Data.U120.mul" => To::Op2 {
|
||||||
oper: kdl::Oper::Mul,
|
oper: kdl::Oper::Mul,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.div" => To::Op2 {
|
"Data.U120.div" => To::Op2 {
|
||||||
oper: kdl::Oper::Div,
|
oper: kdl::Oper::Div,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.mod" => To::Op2 {
|
"Data.U120.mod" => To::Op2 {
|
||||||
oper: kdl::Oper::Mod,
|
oper: kdl::Oper::Mod,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.num_equal" => To::Op2 {
|
"Data.U120.num_equal" => To::Op2 {
|
||||||
oper: kdl::Oper::Eql,
|
oper: kdl::Oper::Eql,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
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,
|
oper: kdl::Oper::Neq,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.shift_left" => To::Op2 {
|
"Data.U120.shift_left" => To::Op2 {
|
||||||
oper: kdl::Oper::Shl,
|
oper: kdl::Oper::Shl,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.shift_right" => To::Op2 {
|
"Data.U120.shift_right" => To::Op2 {
|
||||||
oper: kdl::Oper::Shr,
|
oper: kdl::Oper::Shr,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
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,
|
oper: kdl::Oper::Ltn,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
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,
|
oper: kdl::Oper::Lte,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
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,
|
oper: kdl::Oper::Gtn,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
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,
|
oper: kdl::Oper::Gte,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.bitwise_and" => To::Op2 {
|
"Data.U120.bitwise_and" => To::Op2 {
|
||||||
oper: kdl::Oper::And,
|
oper: kdl::Oper::And,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.bitwise_or" => To::Op2 {
|
"Data.U120.bitwise_or" => To::Op2 {
|
||||||
oper: kdl::Oper::Or,
|
oper: kdl::Oper::Or,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
val1: Box::new(compile_expr(ctx, &args[1])),
|
||||||
},
|
},
|
||||||
"U120.bitwise_xor" => To::Op2 {
|
"Data.U120.bitwise_xor" => To::Op2 {
|
||||||
oper: kdl::Oper::Xor,
|
oper: kdl::Oper::Xor,
|
||||||
val0: Box::new(compile_expr(ctx, &args[0])),
|
val0: Box::new(compile_expr(ctx, &args[0])),
|
||||||
val1: Box::new(compile_expr(ctx, &args[1])),
|
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 } => {
|
From::Str { val } => {
|
||||||
let nil = kdl::Term::Ctr {
|
let nil = kdl::Term::Ctr {
|
||||||
name: *ctx.kdl_names.get("String.nil").unwrap(),
|
name: *ctx.kdl_names.get("Data.String.nil").unwrap(),
|
||||||
args: vec![],
|
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 {
|
let cons = |numb: u128, next| kdl::Term::Ctr {
|
||||||
name: cons_name,
|
name: cons_name,
|
||||||
@ -494,7 +494,7 @@ pub fn compile_entry(ctx: &mut CompileCtx, entry: &untyped::Entry) {
|
|||||||
}
|
}
|
||||||
} else {
|
} else {
|
||||||
match entry.name.to_str() {
|
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),
|
_ => compile_common_function(ctx, entry),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
@ -397,8 +397,8 @@ impl Display for Literal {
|
|||||||
match self {
|
match self {
|
||||||
Literal::Help(s) => write!(f, "?{}", s),
|
Literal::Help(s) => write!(f, "?{}", s),
|
||||||
Literal::Type => write!(f, "Type"),
|
Literal::Type => write!(f, "Type"),
|
||||||
Literal::NumTypeU60 => write!(f, "U60"),
|
Literal::NumTypeU60 => write!(f, "Data.U60"),
|
||||||
Literal::NumTypeF60 => write!(f, "F60"),
|
Literal::NumTypeF60 => write!(f, "Data.F60"),
|
||||||
Literal::Char(c) => write!(f, "'{}'", c),
|
Literal::Char(c) => write!(f, "'{}'", c),
|
||||||
Literal::NumU60(numb) => write!(f, "{}", numb),
|
Literal::NumU60(numb) => write!(f, "{}", numb),
|
||||||
Literal::Nat(numb) => write!(f, "{}numb", numb),
|
Literal::Nat(numb) => write!(f, "{}numb", numb),
|
||||||
|
@ -249,7 +249,7 @@ impl Expr {
|
|||||||
}
|
}
|
||||||
|
|
||||||
pub fn num_u120(range: Range, numb: u128) -> Box<Expr> {
|
pub fn num_u120(range: Range, numb: u128) -> Box<Expr> {
|
||||||
let name = QualifiedIdent::new_static("U120.new", None, range);
|
let name = QualifiedIdent::new_static("Data.U120.new", None, range);
|
||||||
let lo = Expr::num_u60(range, (numb & 0xFFFFFFFFFFFFFFF) as u64);
|
let lo = Expr::num_u60(range, (numb & 0xFFFFFFFFFFFFFFF) as u64);
|
||||||
let hi = Expr::num_u60(range, (numb >> 60) as u64);
|
let hi = Expr::num_u60(range, (numb >> 60) as u64);
|
||||||
Box::new(Expr {
|
Box::new(Expr {
|
||||||
@ -402,8 +402,8 @@ impl Display for AppBinding {
|
|||||||
|
|
||||||
pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box<Expr>], acc: u128) -> Option<u128> {
|
pub fn try_desugar_to_nat(name: &QualifiedIdent, spine: &[Box<Expr>], acc: u128) -> Option<u128> {
|
||||||
match (name.to_str(), spine) {
|
match (name.to_str(), spine) {
|
||||||
("Nat.zero", []) => Some(acc),
|
("Data.Nat.zero", []) => Some(acc),
|
||||||
("Nat.succ", [spine]) => match &spine.data {
|
("Data.Nat.succ", [spine]) => match &spine.data {
|
||||||
ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1),
|
ExprKind::Ctr { name, args } => try_desugar_to_nat(name, args, acc + 1),
|
||||||
_ => None,
|
_ => None,
|
||||||
},
|
},
|
||||||
@ -416,8 +416,8 @@ impl Display for Expr {
|
|||||||
use ExprKind::*;
|
use ExprKind::*;
|
||||||
match &self.data {
|
match &self.data {
|
||||||
Typ => write!(f, "Type"),
|
Typ => write!(f, "Type"),
|
||||||
NumTypeU60 => write!(f, "U60"),
|
NumTypeU60 => write!(f, "Data.U60"),
|
||||||
NumTypeF60 => write!(f, "F60"),
|
NumTypeF60 => write!(f, "Data.F60"),
|
||||||
Str { val } => write!(f, "\"{}\"", val),
|
Str { val } => write!(f, "\"{}\"", val),
|
||||||
NumU60 { numb } => write!(f, "{}", numb),
|
NumU60 { numb } => write!(f, "{}", numb),
|
||||||
NumF60 { numb: _ } => todo!(),
|
NumF60 { numb: _ } => todo!(),
|
||||||
|
Loading…
Reference in New Issue
Block a user