mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-19 04:37:28 +03:00
Style changes suggested by Clippy
This commit is contained in:
parent
c6b88bb16e
commit
ff00aa79ad
105
src/checker.rs
105
src/checker.rs
@ -341,7 +341,8 @@ fn to_checker_rule_end(name: &Ident, size: u64) -> String {
|
||||
let mut text = String::new();
|
||||
|
||||
if size >= 15 {
|
||||
writeln!(text,
|
||||
writeln!(
|
||||
text,
|
||||
"(Q${} orig{}) = (Kind.Term.fn{} {}. orig (Kind.Term.args{}{}))",
|
||||
name,
|
||||
vars.join(""),
|
||||
@ -349,8 +350,10 @@ fn to_checker_rule_end(name: &Ident, size: u64) -> String {
|
||||
name,
|
||||
size,
|
||||
vars.join("")
|
||||
).ok();
|
||||
writeln!(text,
|
||||
)
|
||||
.ok();
|
||||
writeln!(
|
||||
text,
|
||||
"(F${} orig{}) = (Kind.Term.fn{} {}. orig (Kind.Term.args{}{}))",
|
||||
name,
|
||||
vars.join(""),
|
||||
@ -358,24 +361,29 @@ fn to_checker_rule_end(name: &Ident, size: u64) -> String {
|
||||
name,
|
||||
size,
|
||||
vars.join("")
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
} else {
|
||||
writeln!(text,
|
||||
writeln!(
|
||||
text,
|
||||
"(Q${} orig{}) = (Kind.Term.fn{} {}. orig{})",
|
||||
name,
|
||||
vars.join(""),
|
||||
size,
|
||||
name,
|
||||
vars.join("")
|
||||
).ok();
|
||||
writeln!(text,
|
||||
)
|
||||
.ok();
|
||||
writeln!(
|
||||
text,
|
||||
"(F${} orig{}) = (Kind.Term.fn{} {}. orig{})",
|
||||
name,
|
||||
vars.join(""),
|
||||
size,
|
||||
name,
|
||||
vars.join("")
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
}
|
||||
|
||||
text
|
||||
@ -405,21 +413,29 @@ fn to_checker_rule(rule: &Rule) -> String {
|
||||
let body_rhs = to_checker_term(&rule.body, true, false);
|
||||
let rule_rhs = to_checker_term(&rule.body, false, false);
|
||||
let mut text = String::new();
|
||||
writeln!(text,
|
||||
writeln!(
|
||||
text,
|
||||
"(Q${} orig{}) = {}",
|
||||
rule.name,
|
||||
pats.join(""),
|
||||
body_rhs
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
if rule.name.0 == "HVM.log" {
|
||||
write!(text,"(F$HVM.log orig a r log ret) = (HVM.put (Kind.Term.show log) ret)").ok();
|
||||
write!(
|
||||
text,
|
||||
"(F$HVM.log orig a r log ret) = (HVM.put (Kind.Term.show log) ret)"
|
||||
)
|
||||
.ok();
|
||||
} else {
|
||||
writeln!(text,
|
||||
writeln!(
|
||||
text,
|
||||
"(F${} orig{}) = {}",
|
||||
rule.name,
|
||||
pats.join(""),
|
||||
rule_rhs
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
}
|
||||
|
||||
//for size in 0 .. 9 {
|
||||
@ -436,13 +452,15 @@ fn to_checker_rule(rule: &Rule) -> String {
|
||||
|
||||
pub fn to_checker_entry(entry: &Entry) -> String {
|
||||
let mut result = String::new();
|
||||
writeln!(result,"(NameOf {}.) = \"{}\"", entry.name, entry.name).ok();
|
||||
writeln!(result,"(HashOf {}.) = %{}", entry.name, entry.name).ok();
|
||||
writeln!(result,
|
||||
writeln!(result, "(NameOf {}.) = \"{}\"", entry.name, entry.name).ok();
|
||||
writeln!(result, "(HashOf {}.) = %{}", entry.name, entry.name).ok();
|
||||
writeln!(
|
||||
result,
|
||||
"(TypeOf {}.) = {}",
|
||||
entry.name,
|
||||
to_checker_type(&entry.args, &entry.tipo, 0)
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
|
||||
let base_vars = (0..entry.args.len())
|
||||
.map(|x| format!(" x{}", x))
|
||||
@ -450,7 +468,8 @@ pub fn to_checker_entry(entry: &Entry) -> String {
|
||||
.join("");
|
||||
|
||||
if entry.args.len() >= 15 {
|
||||
writeln!(result,
|
||||
writeln!(
|
||||
result,
|
||||
"(Kind.Term.FN{} {}. orig (Kind.Term.args{}{})) = (F${} orig{})",
|
||||
entry.args.len(),
|
||||
entry.name,
|
||||
@ -458,58 +477,74 @@ pub fn to_checker_entry(entry: &Entry) -> String {
|
||||
base_vars,
|
||||
entry.name,
|
||||
base_vars
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
} else {
|
||||
writeln!(result,
|
||||
writeln!(
|
||||
result,
|
||||
"(Kind.Term.FN{} {}. orig{}) = (F${} orig{})",
|
||||
entry.args.len(),
|
||||
entry.name,
|
||||
base_vars,
|
||||
entry.name,
|
||||
base_vars
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
}
|
||||
|
||||
writeln!(result,
|
||||
writeln!(
|
||||
result,
|
||||
"(QT{} {}. orig{}) = (Q${} orig{})",
|
||||
entry.args.len(),
|
||||
entry.name,
|
||||
base_vars,
|
||||
entry.name,
|
||||
base_vars
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
|
||||
for rule in &entry.rules {
|
||||
write!(result, "{}", &to_checker_rule(rule)).ok();
|
||||
}
|
||||
if !entry.rules.is_empty() {
|
||||
write!(result, "{}", &to_checker_rule_end(
|
||||
&entry.name,
|
||||
entry.rules[0].pats.len() as u64,
|
||||
)).ok();
|
||||
write!(
|
||||
result,
|
||||
"{}",
|
||||
&to_checker_rule_end(&entry.name, entry.rules[0].pats.len() as u64,)
|
||||
)
|
||||
.ok();
|
||||
}
|
||||
write!(result,"(RuleOf {}.) =", entry.name).ok();
|
||||
write!(result, "(RuleOf {}.) =", entry.name).ok();
|
||||
for rule in &entry.rules {
|
||||
write!(result,
|
||||
write!(
|
||||
result,
|
||||
" (List.cons {}",
|
||||
to_checker_rule_chk(rule, 0, &mut 0, &mut vec![])
|
||||
).ok();
|
||||
)
|
||||
.ok();
|
||||
}
|
||||
write!(result," List.nil{}", ")".repeat(entry.rules.len())).ok();
|
||||
write!(result, " List.nil{}", ")".repeat(entry.rules.len())).ok();
|
||||
result
|
||||
}
|
||||
|
||||
|
||||
// Vendo oq da pra fazer pra
|
||||
pub fn to_checker_book(book: &Book) -> String {
|
||||
let mut result = String::new();
|
||||
writeln!(result, "// NOTE: functions with names starting with 'F$' are evaluated differently by the").ok();
|
||||
writeln!(result, "// HVM, as a specific optimization targetting Kind2. See 'HOAS_OPT' on HVM's code.\n").ok();
|
||||
writeln!(
|
||||
result,
|
||||
"// NOTE: functions with names starting with 'F$' are evaluated differently by the"
|
||||
)
|
||||
.ok();
|
||||
writeln!(
|
||||
result,
|
||||
"// HVM, as a specific optimization targetting Kind2. See 'HOAS_OPT' on HVM's code.\n"
|
||||
)
|
||||
.ok();
|
||||
writeln!(result, "Functions =").ok();
|
||||
writeln!(result, " let fns = List.nil").ok();
|
||||
for name in &book.names {
|
||||
let entry = book.entrs.get(&Ident(name.to_string())).unwrap();
|
||||
writeln!(result," let fns = (List.cons {}. fns)", entry.name).ok();
|
||||
writeln!(result, " let fns = (List.cons {}. fns)", entry.name).ok();
|
||||
}
|
||||
result.push_str(" fns\n\n");
|
||||
for name in &book.names {
|
||||
|
@ -9,12 +9,8 @@ pub fn to_hvm_term(book: &Book, term: &Term) -> String {
|
||||
return format!("\"{}\"", as_string);
|
||||
}
|
||||
match term {
|
||||
Term::Typ { .. } => {
|
||||
"Type".to_string()
|
||||
}
|
||||
Term::Var { orig: _, name } => {
|
||||
name.to_string()
|
||||
}
|
||||
Term::Typ { .. } => "Type".to_string(),
|
||||
Term::Var { orig: _, name } => name.to_string(),
|
||||
Term::Lam {
|
||||
orig: _,
|
||||
name,
|
||||
@ -55,18 +51,14 @@ pub fn to_hvm_term(book: &Book, term: &Term) -> String {
|
||||
orig: _,
|
||||
expr,
|
||||
tipo: _,
|
||||
} => {
|
||||
to_hvm_term(book, expr)
|
||||
}
|
||||
} => to_hvm_term(book, expr),
|
||||
Term::Sub {
|
||||
orig: _,
|
||||
expr,
|
||||
name: _,
|
||||
indx: _,
|
||||
redx: _,
|
||||
} => {
|
||||
to_hvm_term(book, expr)
|
||||
}
|
||||
} => to_hvm_term(book, expr),
|
||||
Term::Ctr {
|
||||
orig: _,
|
||||
name,
|
||||
@ -107,12 +99,8 @@ pub fn to_hvm_term(book: &Book, term: &Term) -> String {
|
||||
.collect::<String>()
|
||||
)
|
||||
}
|
||||
Term::Hlp { orig: _ } => {
|
||||
"0".to_string()
|
||||
}
|
||||
Term::U60 { orig: _ } => {
|
||||
"0".to_string()
|
||||
}
|
||||
Term::Hlp { orig: _ } => "0".to_string(),
|
||||
Term::U60 { orig: _ } => "0".to_string(),
|
||||
Term::Num { orig: _, numb } => {
|
||||
format!("{}", numb)
|
||||
}
|
||||
@ -126,9 +114,7 @@ pub fn to_hvm_term(book: &Book, term: &Term) -> String {
|
||||
let val1 = to_hvm_term(book, val1);
|
||||
format!("({} {} {})", oper, val0, val1)
|
||||
}
|
||||
Term::Hol { orig: _, numb: _ } => {
|
||||
"_".to_string()
|
||||
}
|
||||
Term::Hol { orig: _, numb: _ } => "_".to_string(),
|
||||
Term::Mat { .. } => {
|
||||
panic!("Internal error."); // removed after adjust()
|
||||
}
|
||||
@ -143,7 +129,7 @@ pub fn to_hvm_oper(oper: &Operator) -> String {
|
||||
Operator::Div => "/".to_string(),
|
||||
Operator::Mod => "%".to_string(),
|
||||
Operator::And => "&".to_string(),
|
||||
Operator::Or => "|".to_string(),
|
||||
Operator::Or => "|".to_string(),
|
||||
Operator::Xor => "^".to_string(),
|
||||
Operator::Shl => "<<".to_string(),
|
||||
Operator::Shr => ">>".to_string(),
|
||||
|
@ -11,9 +11,7 @@ pub const KDL_NAME_LEN: usize = 12;
|
||||
|
||||
pub fn to_kdl_term(kdl_names: &HashMap<String, String>, term: &CompTerm) -> Result<String, String> {
|
||||
let term = match term {
|
||||
CompTerm::Var { name } => {
|
||||
name.clone()
|
||||
}
|
||||
CompTerm::Var { name } => name.clone(),
|
||||
CompTerm::Lam { name, body } => {
|
||||
let body = to_kdl_term(kdl_names, body)?;
|
||||
format!("@{} {}", name, body)
|
||||
|
@ -11,46 +11,18 @@ use std::collections::HashSet;
|
||||
// Returns true if a ctor's argument is erased
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum CompTerm {
|
||||
Var {
|
||||
name: String,
|
||||
},
|
||||
Lam {
|
||||
name: String,
|
||||
body: Box<CompTerm>,
|
||||
},
|
||||
App {
|
||||
func: Box<CompTerm>,
|
||||
argm: Box<CompTerm>,
|
||||
},
|
||||
Dup {
|
||||
nam0: String,
|
||||
nam1: String,
|
||||
expr: Box<CompTerm>,
|
||||
body: Box<CompTerm>,
|
||||
},
|
||||
Let {
|
||||
name: String,
|
||||
expr: Box<CompTerm>,
|
||||
body: Box<CompTerm>,
|
||||
},
|
||||
Ctr {
|
||||
name: String,
|
||||
args: Vec<Box<CompTerm>>,
|
||||
},
|
||||
Fun {
|
||||
name: String,
|
||||
args: Vec<Box<CompTerm>>,
|
||||
},
|
||||
Num {
|
||||
numb: u128,
|
||||
},
|
||||
Op2 {
|
||||
oper: Operator,
|
||||
val0: Box<CompTerm>,
|
||||
val1: Box<CompTerm>,
|
||||
},
|
||||
Nil,
|
||||
}
|
||||
Var { name: String },
|
||||
Lam { name: String, body: Box<CompTerm> },
|
||||
App { func: Box<CompTerm>, argm: Box<CompTerm> },
|
||||
Dup { nam0: String, nam1: String, expr: Box<CompTerm>, body: Box<CompTerm> },
|
||||
Let { name: String, expr: Box<CompTerm>, body: Box<CompTerm> },
|
||||
Ctr { name: String, args: Vec<Box<CompTerm>> },
|
||||
Fun { name: String, args: Vec<Box<CompTerm>> },
|
||||
Num { numb: u128 },
|
||||
Op2 { oper: Oper, val0: Box<CompTerm>, val1: Box<CompTerm> },
|
||||
Nil
|
||||
}
|
||||
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct CompRule {
|
||||
@ -316,10 +288,7 @@ pub fn flatten(entry: CompEntry) -> Vec<CompEntry> {
|
||||
// The old rule is rewritten to be flat and call the new entry
|
||||
let n = post_inc(&mut name_count);
|
||||
let new_entry_name = format!("{}{}_", entry.name, n);
|
||||
let new_entry_kdln = entry
|
||||
.kdln
|
||||
.clone()
|
||||
.map(|kdln| format!("{}{}_", kdln, n));
|
||||
let new_entry_kdln = entry.kdln.clone().map(|kdln| format!("{}{}_", kdln, n));
|
||||
let mut new_entry_rules: Vec<CompRule> = Vec::new();
|
||||
// Rewrite the old rule to be flat and point to the new entry
|
||||
let mut old_rule_pats: Vec<Box<CompTerm>> = Vec::new();
|
||||
@ -571,9 +540,7 @@ pub fn subst(term: &mut CompTerm, sub_name: &str, value: &CompTerm) {
|
||||
// Removes proof-irrelevant parts of the term
|
||||
pub fn erase(book: &Book, term: &Term) -> Box<CompTerm> {
|
||||
match term {
|
||||
Term::Typ { .. } => {
|
||||
Box::new(CompTerm::Nil)
|
||||
}
|
||||
Term::Typ { .. } => Box::new(CompTerm::Nil),
|
||||
Term::Var { orig: _, name } => {
|
||||
let name = name.0.clone();
|
||||
Box::new(CompTerm::Var { name })
|
||||
@ -601,9 +568,7 @@ pub fn erase(book: &Book, term: &Term) -> Box<CompTerm> {
|
||||
name: _,
|
||||
tipo: _,
|
||||
body: _,
|
||||
} => {
|
||||
Box::new(CompTerm::Nil)
|
||||
}
|
||||
} => Box::new(CompTerm::Nil),
|
||||
Term::Let {
|
||||
orig: _,
|
||||
name,
|
||||
@ -619,18 +584,14 @@ pub fn erase(book: &Book, term: &Term) -> Box<CompTerm> {
|
||||
orig: _,
|
||||
expr,
|
||||
tipo: _,
|
||||
} => {
|
||||
erase(book, expr)
|
||||
}
|
||||
} => erase(book, expr),
|
||||
Term::Sub {
|
||||
orig: _,
|
||||
expr,
|
||||
name: _,
|
||||
indx: _,
|
||||
redx: _,
|
||||
} => {
|
||||
erase(book, expr)
|
||||
}
|
||||
} => erase(book, expr),
|
||||
Term::Ctr {
|
||||
orig: _,
|
||||
name,
|
||||
@ -661,12 +622,8 @@ pub fn erase(book: &Book, term: &Term) -> Box<CompTerm> {
|
||||
}
|
||||
Box::new(CompTerm::Fun { name, args })
|
||||
}
|
||||
Term::Hlp { orig: _ } => {
|
||||
Box::new(CompTerm::Nil)
|
||||
}
|
||||
Term::U60 { orig: _ } => {
|
||||
Box::new(CompTerm::Nil)
|
||||
}
|
||||
Term::Hlp { orig: _ } => Box::new(CompTerm::Nil),
|
||||
Term::U60 { orig: _ } => Box::new(CompTerm::Nil),
|
||||
Term::Num { orig: _, numb } => {
|
||||
let numb = *numb as u128;
|
||||
Box::new(CompTerm::Num { numb })
|
||||
@ -682,12 +639,8 @@ pub fn erase(book: &Book, term: &Term) -> Box<CompTerm> {
|
||||
let val1 = erase(book, val1);
|
||||
Box::new(CompTerm::Op2 { oper, val0, val1 })
|
||||
}
|
||||
Term::Hol { orig: _, numb: _ } => {
|
||||
Box::new(CompTerm::Nil)
|
||||
}
|
||||
Term::Mat { .. } => {
|
||||
Box::new(CompTerm::Nil)
|
||||
}
|
||||
Term::Hol { orig: _, numb: _ } => Box::new(CompTerm::Nil),
|
||||
Term::Mat { .. } => Box::new(CompTerm::Nil),
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -187,14 +187,12 @@ impl Adjust for Term {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(expr.adjust(rhs, state)?);
|
||||
match state.vars.iter().position(|x| x == name) {
|
||||
None => {
|
||||
Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::UnboundVariable {
|
||||
name: name.to_string(),
|
||||
},
|
||||
})
|
||||
}
|
||||
None => Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::UnboundVariable {
|
||||
name: name.to_string(),
|
||||
},
|
||||
}),
|
||||
Some(indx) => {
|
||||
let name = name.clone();
|
||||
let indx = indx as u64;
|
||||
|
Loading…
Reference in New Issue
Block a user