HigherOrderCO/Kind1
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind1.git synced 2024-09-11 08:45:32 +03:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'master' of github.com:kindelia/kind2

Browse Source
This commit is contained in:
Victor Maia 2022-09-06 15:08:34 -03:00
commit eae62b40e2
5 changed files with 179 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
Cargo.toml
View File

@ -1,6 +1,6 @@
[package]
name = "kind2"
version = "0.2.72"
version = "0.2.73"
edition = "2021"
description = "A pure functional functional language that uses the HVM."
repository = "https://github.com/Kindelia/Kind2"
@ -10,7 +10,8 @@ keywords = ["functional", "language", "type-theory", "proof-assistant"]
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
[dependencies]
hvm = "0.1.82"
hvm = "0.1.81"
#hvm = { path = "../hvm" }
highlight_error = "0.1.1"
clap = { version = "3.1.8", features = ["derive"] }
rand = "0.8.5"

42
src/language.rs
View File

@ -14,6 +14,7 @@ pub struct Book {
#[derive(Clone, Debug)]
pub struct Entry {
pub name: String,
pub kdln: Option<String>,
pub args: Vec<Box<Argument>>,
pub tipo: Box<Term>,
pub rules: Vec<Box<Rule>>
@ -136,6 +137,7 @@ pub fn adjust_book(book: &Book) -> Result<Book, AdjustError> {
pub fn adjust_entry(book: &Book, entry: &Entry, holes: &mut u64, types: &mut HashMap<String, Rc<NewType>>) -> Result<Entry, AdjustError> {
let name = entry.name.clone();
let kdln = entry.kdln.clone();
let mut args = Vec::new();
// Adjust the type arguments, return type
let mut vars = Vec::new();
@ -150,7 +152,7 @@ pub fn adjust_entry(book: &Book, entry: &Entry, holes: &mut u64, types: &mut Has
let mut vars = Vec::new();
rules.push(Box::new(adjust_rule(book, &*rule, holes, &mut vars, types)?));
}
return Ok(Entry { name, args, tipo, rules });
return Ok(Entry { name, kdln, args, tipo, rules });
}
pub fn adjust_argument(book: &Book, arg: &Argument, holes: &mut u64, vars: &mut Vec<String>, types: &mut HashMap<String, Rc<NewType>>) -> Result<Argument, AdjustError> {
@ -509,8 +511,12 @@ pub fn term_get_unbounds(book: &Book, term: &Term, rhs: bool, vars: &mut Vec<Str
if ('A'..='Z').contains(&name.chars().nth(0).unwrap_or(' ')) {
unbound.insert(name.clone());
// Is unbound variable
} else if rhs && vars.iter().find(|&x| x == name).is_none() {
unbound.insert(name.clone());
} else if vars.iter().find(|&x| x == name).is_none() {
if rhs {
unbound.insert(name.clone());
} else {
vars.push(name.clone());
}
}
},
Term::Let { ref name, ref expr, ref body, .. } => {
@ -1576,6 +1582,13 @@ pub fn parse_apps(state: parser::State) -> parser::Answer<Box<Term>> {
pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
let (state, name) = parser::name1(state)?;
let (state, kdl) = parser::text("#", state)?;
let (state, kdln) = if kdl {
let (state, name) = parser::name1(state)?;
(state, Some(name))
} else {
(state, None)
};
let (state, args) = parser::until(Box::new(|state| {
let (state, end_0) = parser::dry(Box::new(|state| parser::text(":", state)), state)?;
let (state, end_1) = parser::dry(Box::new(|state| parser::text("{", state)), state)?;
@ -1598,7 +1611,7 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
pats.push(Box::new(Term::Var { orig: 0, name: arg.name.clone() })); // TODO: set orig
}
let rules = vec![Box::new(Rule { orig: 0, name: name.clone(), pats, body })];
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
return Ok((state, Box::new(Entry { name, kdln, args, tipo, rules })));
} else {
let mut rules = Vec::new();
let rule_prefix = &format!("{} ", name);
@ -1616,7 +1629,7 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
break;
}
}
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
return Ok((state, Box::new(Entry { name, kdln, args, tipo, rules })));
}
}
@ -2140,7 +2153,11 @@ pub fn show_rule(rule: &Rule) -> String {
}
pub fn show_entry(entry: &Entry) -> String {
let name = &entry.name;
let name = if let Some(kdln) = &entry.kdln {
format!("{} #{}", entry.name, kdln)
} else {
entry.name.clone()
};
let mut args = vec![];
for arg in &entry.args {
let (open, close) = match (arg.eras, arg.hide) {
@ -2301,7 +2318,7 @@ pub fn erase(book: &Book, term: &Term) -> Box<Comp> {
args.push(erase(book, arg));
}
}
return Box::new(Comp::Ctr { name, args });
return Box::new(Comp::Fun { name, args });
}
Term::Hlp { orig: _ } => {
return Box::new(Comp::Nil);
@ -2518,6 +2535,7 @@ pub fn linearize(term: &mut Comp, fresh: &mut u64) {
pub fn derive_type(tipo: &NewType) -> Derived {
let path = format!("{}/_.kind2", tipo.name.replace(".","/"));
let name = format!("{}", tipo.name);
let kdln = None;
let mut args = vec![];
for par in &tipo.pars {
args.push(Box::new(Argument {
@ -2529,7 +2547,7 @@ pub fn derive_type(tipo: &NewType) -> Derived {
}
let tipo = Box::new(Term::Typ { orig: 0 });
let rules = vec![];
let entr = Entry { name, args, tipo, rules };
let entr = Entry { name, kdln, args, tipo, rules };
return Derived { path, entr };
}
@ -2537,6 +2555,7 @@ pub fn derive_ctr(tipo: &NewType, index: usize) -> Derived {
if let Some(ctr) = tipo.ctrs.get(index) {
let path = format!("{}/{}.kind2", tipo.name.replace(".","/"), ctr.name);
let name = format!("{}.{}", tipo.name, ctr.name);
let kdln = None;
let mut args = vec![];
for arg in &tipo.pars {
args.push(arg.clone());
@ -2550,7 +2569,7 @@ pub fn derive_ctr(tipo: &NewType, index: usize) -> Derived {
args: tipo.pars.iter().map(|x| Box::new(Term::Var { orig: 0, name: x.name.clone() })).collect(),
});
let rules = vec![];
let entr = Entry { name, args, tipo, rules };
let entr = Entry { name, kdln, args, tipo, rules };
return Derived { path, entr };
} else {
panic!("Constructor out of bounds.");
@ -2592,6 +2611,7 @@ pub fn derive_match(ntyp: &NewType) -> Derived {
// List.match
let name = format!("{}.match", ntyp.name);
let kdln = None;
let mut args = vec![];
@ -2694,7 +2714,7 @@ pub fn derive_match(ntyp: &NewType) -> Derived {
rules.push(Box::new(Rule { orig, name, pats, body }));
}
let entr = Entry { name, args, tipo, rules };
let entr = Entry { name, kdln, args, tipo, rules };
return Derived { path, entr };
}
@ -2702,7 +2722,7 @@ pub fn derive_match(ntyp: &NewType) -> Derived {
//type List <t: Type> { nil cons (head: t) (tail: (List t)) }
//pub struct Type { name: String, pars: Vec<Argument>, ctrs: Vec<Constructor> }
//pub struct Constructor { name: String, args: Vec<Argument> }
//pub struct Entry { pub name: String, pub args: Vec<Box<Argument>>, pub tipo: Box<Term>, pub rules: Vec<Box<Rule>> }
//pub struct Entry { pub name: String, pub kdln: Option<String>, pub args: Vec<Box<Argument>>, pub tipo: Box<Term>, pub rules: Vec<Box<Rule>> }
//pub struct Argument { pub hide: bool, pub eras: bool, pub name: String, pub tipo: Box<Term> }
//pub struct Rule { pub orig: u64, pub name: String, pub pats: Vec<Box<Term>>, pub body: Box<Term> }
// List (t: Type) : Type

5
src/main.rs
View File

@ -160,8 +160,9 @@ fn cmd_show(path: &str) -> Result<(), String> {
// Compiles a file to Kindelia (.kdl)
fn cmd_to_kdl(path: &str) -> Result<(), String> {
let loaded = load(path)?;
let result = to_kdl::to_kdl_book(&loaded.book);
let loaded = load(path)?;
let kdl_names = to_kdl::get_kdl_names(&loaded.book)?;
let result = to_kdl::to_kdl_book(&loaded.book, &kdl_names)?;
print!("{}", result);
Ok(())
}

11
src/to_hvm.rs
View File

@ -109,8 +109,13 @@ pub fn to_hvm_rule(book: &Book, rule: &Rule) -> String {
}
pub fn to_hvm_entry(book: &Book, entry: &Entry) -> String {
let name = &entry.name;
if name == "HVM.log" {
let kind_name = if let Some(kdln) = &entry.kdln {
format!("{} #{}", entry.name, kdln)
} else {
entry.name.clone()
};
let hvm_name = &entry.name;
if hvm_name == "HVM.log" {
return "".to_string();
}
let mut args = vec![];
@ -122,7 +127,7 @@ pub fn to_hvm_entry(book: &Book, entry: &Entry) -> String {
for rule in &entry.rules {
rules.push(format!("\n{}", to_hvm_rule(book, rule)));
}
return format!("// {}{} : {}{}\n\n", name, args.join(""), show_term(&entry.tipo), rules.join(""))
return format!("// {}{} : {}{}\n\n", kind_name, args.join(""), show_term(&entry.tipo), rules.join(""))
}
return "".to_string();
}

166
src/to_kdl.rs
View File

@ -2,51 +2,61 @@
// TODO: U120?
use crate::language::{*};
use std::collections::HashSet;
use std::collections::{HashSet, HashMap};
use rand::Rng;
pub fn to_kdl_term(term: &Comp) -> String {
match term {
pub const KDL_NAME_LEN: usize = 12;
pub fn to_kdl_term(kdl_names: &HashMap<String, String>, term: &Comp) -> Result<String, String> {
let term = match term {
Comp::Var { name } => {
format!("{}", name)
}
Comp::Lam { name, body } => {
let body = to_kdl_term(body);
let body = to_kdl_term(kdl_names, body)?;
format!("@{} {}", name, body)
}
Comp::App { func, argm } => {
let func = to_kdl_term(func);
let argm = to_kdl_term(argm);
let func = to_kdl_term(kdl_names, func)?;
let argm = to_kdl_term(kdl_names, argm)?;
format!("({} {})", func, argm)
}
Comp::Dup { nam0, nam1, expr, body } => {
let expr = to_kdl_term(expr);
let body = to_kdl_term(body);
let expr = to_kdl_term(kdl_names, expr)?;
let body = to_kdl_term(kdl_names, body)?;
format!("dup {} {} = {}; {}", nam0, nam1, expr, body)
}
Comp::Let { name, expr, body } => {
let expr = to_kdl_term(expr);
let body = to_kdl_term(body);
let expr = to_kdl_term(kdl_names, expr)?;
let body = to_kdl_term(kdl_names, body)?;
format!("let {} = {}; {}", name, expr, body)
}
Comp::Ctr { name, args } => {
format!("{{{}{}}}", name, args.iter().map(|x| format!(" {}", to_kdl_term(x))).collect::<String>())
let kdl_name = kdl_names.get(name).unwrap();
let args = args.iter().map(|x| to_kdl_term(kdl_names, x)).collect::<Result<Vec<String>, String>>()?;
let args = args.iter().map(|x| format!(" {}", x)).collect::<String>();
format!("{{{}{}}}", kdl_name, args)
}
Comp::Fun { name, args } => {
format!("({}{})", name, args.iter().map(|x| format!(" {}", to_kdl_term(x))).collect::<String>())
let kdl_name = kdl_names.get(name).unwrap();
let args = args.iter().map(|x| to_kdl_term(kdl_names, x)).collect::<Result<Vec<String>, String>>()?;
let args = args.iter().map(|x| format!(" {}", x)).collect::<String>();
format!("{{{}{}}}", kdl_name, args)
}
Comp::Num { numb } => {
format!("#{}", numb)
}
Comp::Op2 { oper, val0, val1 } => {
let oper = show_oper(&oper);
let val0 = to_kdl_term(val0);
let val1 = to_kdl_term(val1);
let val0 = to_kdl_term(kdl_names, val0)?;
let val1 = to_kdl_term(kdl_names, val1)?;
format!("({} {} {})", oper, val0, val1)
}
Comp::Nil => {
format!("#0")
return Err("Found invalid Nil term".to_string());
}
}
};
Ok(term)
}
pub fn to_kdl_oper(oper: &Oper) -> String {
@ -70,17 +80,26 @@ pub fn to_kdl_oper(oper: &Oper) -> String {
}
}
pub fn to_kdl_rule(book: &Book, rule: &Rule) -> String {
pub fn to_kdl_rule(book: &Book, kdl_names: &HashMap<String, String>, rule: &Rule) -> Result<String, String> {
let name = &rule.name;
let kdl_name = kdl_names.get(name).unwrap();
let entry = book.entrs.get(name).unwrap();
let mut pats = vec![]; // stringified pattern args
let mut vars = HashSet::new(); // rule pattern vars
for (arg, pat) in entry.args.iter().zip(rule.pats.iter()) {
if !arg.eras {
let pat = erase(book, pat);
let comp_pat = erase(book, pat);
let pat = match to_kdl_term(kdl_names, &comp_pat) {
Ok(term) => term,
Err(_) => {
let pats = rule.pats.iter().map(|pat| format!(" {}", show_term(pat))).collect::<String>();
let err = format!("Found invalid term in pattern \"{}\" of rule \"{}{}\"", show_term(&*pat), name, pats);
return Err(err);
},
};
pats.push(" ".to_string());
pats.push(to_kdl_term(&pat));
collect_lhs_vars(&pat, &mut vars);
pats.push(pat);
collect_lhs_vars(&comp_pat, &mut vars);
}
}
let mut body = erase(book, &rule.body);
@ -109,38 +128,121 @@ pub fn to_kdl_rule(book: &Book, rule: &Rule) -> String {
// lambdas. (@x0 #0 should be linearized to @~ #0)
}
linearize(&mut body, &mut fresh); // linearizes internal bound vars
format!("({}{}) = {}", name, pats.join(""), to_kdl_term(&body))
let body = match to_kdl_term(kdl_names, &body) {
Ok(body) => body,
Err(_) => {
let pats = rule.pats.iter().map(|pat| format!(" {}", show_term(pat))).collect::<String>();
let err = format!("Found invalid term in body of rule \"{}{}\"", name, pats);
return Err(err);
},
};
let rule = format!("({}{}) = {}", kdl_name, pats.join(""), body);
Ok(rule)
}
pub fn to_kdl_entry(book: &Book, entry: &Entry) -> String {
let name = &entry.name;
pub fn to_kdl_entry(book: &Book, kdl_names: &HashMap<String, String>, entry: &Entry) -> Result<String, String> {
let kdl_name = kdl_names.get(&entry.name).unwrap();
let kind_name = format!("{} #{}", entry.name, kdl_name);
let mut args_typed = vec![];
let mut args_names = vec![];
for arg in &entry.args {
args_typed.push(format!(" {}({}: {})", if arg.eras { "-" } else { "" }, arg.name, show_term(&arg.tipo)));
args_names.push(format!(" {}", arg.name));
if !arg.eras {
args_names.push(format!(" {}", arg.name));
}
}
if entry.rules.len() > 0 {
// Entries with no rules become constructors
let entry = if entry.rules.is_empty() {
let cmnt = format!("// {}{} : {}\n", kind_name, args_typed.join(""), show_term(&entry.tipo));
let ctr = format!("ctr {{{}{}}}\n\n", kdl_name, args_names.join(""));
cmnt + &ctr
// Entries with rules become functions
} else {
let mut rules = vec![];
for rule in &entry.rules {
rules.push(format!("\n {}", to_kdl_rule(book, rule)));
rules.push(format!("\n {}", to_kdl_rule(book, kdl_names, rule)?));
}
return format!("// {}{} : {}\nfun ({}{}) {{{}\n}}\n\n", name, args_typed.join(""), show_term(&entry.tipo), name, args_names.join(""), rules.join(""));
}
return "".to_string();
let cmnt = format!("// {}{} : {}\n", kind_name, args_typed.join(""), show_term(&entry.tipo));
let func = format!("fun ({}{}) {{{}\n}}\n\n", kdl_name, args_names.join(""), rules.join(""));
cmnt + &func
};
Ok(entry)
}
pub fn to_kdl_book(book: &Book) -> String {
pub fn to_kdl_book(book: &Book, kdl_names: &HashMap<String, String>) -> Result<String, String> {
let mut lines = vec![];
for name in &book.names {
lines.push(to_kdl_entry(book, book.entrs.get(name).unwrap()));
let entry = book.entrs.get(name).unwrap();
// Skip over useless entries
// TODO: This doesn't cover all cases. We need something like `erase` but for a Book.
// Also maybe there are functions of type Type that should be compiled?
if let Term::Typ {orig: _} = &*entry.tipo {
continue;
} else {
lines.push(to_kdl_entry(book, kdl_names, entry)?);
}
}
lines.join("")
Ok(lines.join(""))
}
// Utils
// -----
// Returns a map of kind names to kindelia names
// Returns an err if any of the names can't be converted
pub fn get_kdl_names(book: &Book) -> Result<HashMap<String, String>, String> {
fn get_kdl_name(entry: &Entry) -> Result<String, String> {
let kind_name = &entry.name;
// If the entry uses a kindelia name, use it
if let Some(kdln) = &entry.kdln {
// If the name has no ., put one at the start to make it part of the root namespace
if kdln.len() > KDL_NAME_LEN {
let err = format!("Kindelia name \"{}\" for \"{}\" has more than {} characters.", kdln, kind_name, KDL_NAME_LEN - 1);
return Err(err);
}
Ok(kdln.clone())
// Otherwise, try to fit the normal kind name in the max allowed len
} else {
let (ns, fun) = kind_name.rsplit_once('.').unwrap_or(("", kind_name));
let ns = if !ns.is_empty() { format!("{}.", ns) } else { ns.to_string() };
if ns.len() > KDL_NAME_LEN - 1 {
let err = format!("Namespace for \"{}\" has more than {} characters.", kind_name, KDL_NAME_LEN - 1);
return Err(err);
}
let max_fn_name = KDL_NAME_LEN - ns.len();
// If the name doesn't fit, truncate and insert some random characters at the end
let fun = if fun.len() > max_fn_name {
let n_rnd_chrs = usize::min(3, max_fn_name);
let fun_cut = fun[..max_fn_name - n_rnd_chrs].to_string();
let mut rng = rand::thread_rng();
let rnd_chrs = (0..n_rnd_chrs)
.map(|_| rng.gen_range(0..63))
.map(|n| encode_base64(n))
.collect::<String>();
format!("{}{}",fun_cut, rnd_chrs)
} else {
fun.to_string()
};
Ok(format!("{}{}", ns, fun))
}
}
let mut kdl_names = HashMap::new();
for name in &book.names {
let kdln = get_kdl_name(book.entrs.get(name).unwrap())?;
kdl_names.insert(name.clone(), kdln);
}
Ok(kdl_names)
}
pub fn encode_base64(num: u8) -> char {
match num {
0 ..= 9 => (num + b'0') as char,
10 ..= 35 => (num - 10 + b'A') as char,
36 ..= 61 => (num - 36 + b'a') as char,
62 .. => '_',
}
}
// Returns left-hand side variables
pub fn collect_lhs_vars(term: &Comp, vars: &mut HashSet<String>) {
match term {