mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-17 00:20:32 +03:00
stuff
This commit is contained in:
parent
0a48196422
commit
7bd588f9b6
@ -0,0 +1,22 @@
|
||||
/// Multiplies two natural numbers.
|
||||
///
|
||||
/// # Inputs
|
||||
///
|
||||
/// * `a` - The first natural number.
|
||||
/// * `b` - The second natural number.
|
||||
///
|
||||
/// # Output
|
||||
///
|
||||
/// The product of `a` and `b`.
|
||||
|
||||
use Nat/{succ,zero}
|
||||
|
||||
mul
|
||||
- a: Nat
|
||||
- b: Nat
|
||||
: Nat
|
||||
|
||||
match a {
|
||||
succ: (Nat/add b (mul a.pred b))
|
||||
zero: zero
|
||||
}
|
@ -17,4 +17,12 @@ impl Book {
|
||||
}
|
||||
code
|
||||
}
|
||||
|
||||
pub fn to_js(&self) -> String {
|
||||
let mut code = String::new();
|
||||
for (name, term) in &self.defs {
|
||||
code.push_str(&format!("const {} = {};\n", Term::to_js_name(name), term.to_js()));
|
||||
}
|
||||
code
|
||||
}
|
||||
}
|
||||
|
43
src/main.rs
43
src/main.rs
@ -1,3 +1,6 @@
|
||||
//./book/compile.rs//
|
||||
//./term/compile.rs//
|
||||
|
||||
use clap::{Arg, ArgAction, Command};
|
||||
use std::fs;
|
||||
use std::io::Write;
|
||||
@ -20,6 +23,7 @@ use TSPL::Parser;
|
||||
|
||||
TSPL::new_parser!(KindParser);
|
||||
|
||||
// FIXME: not necessary, already on book
|
||||
fn generate_kindc(book: &Book, arg: &str) -> String {
|
||||
let book_kindc = book.to_kindc();
|
||||
let main_kindc = format!("MAIN = {};\n", Term::to_kindc_name(arg));
|
||||
@ -68,12 +72,6 @@ fn auto_format(file_name: &str) {
|
||||
std::fs::write(&file, form).expect(&format!("failed to write to file '{}'", file_name));
|
||||
}
|
||||
|
||||
fn compile(name: &str) {
|
||||
let book = load_book(name);
|
||||
let code = generate_kindc(&book, name);
|
||||
println!("{code}");
|
||||
}
|
||||
|
||||
fn load_book(name: &str) -> Book {
|
||||
let cwd = std::env::current_dir().expect("failed to get current directory");
|
||||
Book::boot(cwd.to_str().unwrap(), name).unwrap_or_else(|e| {
|
||||
@ -94,6 +92,18 @@ fn deps(name: &str) {
|
||||
}
|
||||
}
|
||||
|
||||
fn compile_to_kindc(name: &str) {
|
||||
let book = load_book(name);
|
||||
let code = generate_kindc(&book, name);
|
||||
println!("{code}");
|
||||
}
|
||||
|
||||
fn compile_to_js(name: &str) {
|
||||
let book = load_book(name);
|
||||
let code = book.to_js();
|
||||
println!("{}", code);
|
||||
}
|
||||
|
||||
fn main() {
|
||||
let matches = Command::new("kind2")
|
||||
.about("The Kind2 Programming Language")
|
||||
@ -113,12 +123,15 @@ fn main() {
|
||||
.subcommand(Command::new("format")
|
||||
.about("Auto-formats a file")
|
||||
.arg(Arg::new("name").required(true)))
|
||||
.subcommand(Command::new("compile")
|
||||
.about("Compiles to KINDC")
|
||||
.arg(Arg::new("name").required(true)))
|
||||
.subcommand(Command::new("deps")
|
||||
.about("Lists all dependencies of a symbol")
|
||||
.arg(Arg::new("name").required(true)))
|
||||
.subcommand(Command::new("to-kindc")
|
||||
.about("Compiles to KINDC")
|
||||
.arg(Arg::new("name").required(true)))
|
||||
.subcommand(Command::new("to-js")
|
||||
.about("Compiles to JavaScript")
|
||||
.arg(Arg::new("name").required(true)))
|
||||
.get_matches();
|
||||
|
||||
match matches.subcommand() {
|
||||
@ -135,14 +148,18 @@ fn main() {
|
||||
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||
auto_format(name);
|
||||
}
|
||||
Some(("compile", sub_matches)) => {
|
||||
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||
compile(name);
|
||||
}
|
||||
Some(("deps", sub_matches)) => {
|
||||
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||
deps(name);
|
||||
}
|
||||
Some(("to-kindc", sub_matches)) => {
|
||||
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||
compile_to_kindc(name);
|
||||
}
|
||||
Some(("to-js", sub_matches)) => {
|
||||
let name = sub_matches.get_one::<String>("name").expect("required");
|
||||
compile_to_js(name);
|
||||
}
|
||||
_ => unreachable!(),
|
||||
}
|
||||
}
|
||||
|
@ -1,28 +1,11 @@
|
||||
use crate::{*};
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
// Kind -> HVM2
|
||||
// ------------
|
||||
|
||||
impl Oper {
|
||||
pub fn to_ctr(&self) -> &'static str {
|
||||
match self {
|
||||
Oper::Add => "ADD",
|
||||
Oper::Sub => "SUB",
|
||||
Oper::Mul => "MUL",
|
||||
Oper::Div => "DIV",
|
||||
Oper::Mod => "MOD",
|
||||
Oper::Eq => "EQ",
|
||||
Oper::Ne => "NE",
|
||||
Oper::Lt => "LT",
|
||||
Oper::Gt => "GT",
|
||||
Oper::Lte => "LTE",
|
||||
Oper::Gte => "GTE",
|
||||
Oper::And => "AND",
|
||||
Oper::Or => "OR",
|
||||
Oper::Xor => "XOR",
|
||||
Oper::Lsh => "LSH",
|
||||
Oper::Rsh => "RSH",
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_sym(&self) -> &'static str {
|
||||
pub fn to_hvm2(&self) -> &'static str {
|
||||
match self {
|
||||
Oper::Add => "+",
|
||||
Oper::Sub => "-",
|
||||
@ -89,7 +72,7 @@ impl Term {
|
||||
Term::Op2 { opr, fst, snd } => {
|
||||
let fst = fst.to_hvm2();
|
||||
let snd = snd.to_hvm2();
|
||||
format!("({} {} {})", opr.to_sym(), fst, snd)
|
||||
format!("({} {} {})", opr.to_hvm2(), fst, snd)
|
||||
},
|
||||
Term::Swi { nam, x, z, s, p: _ } => {
|
||||
let x = x.to_hvm2();
|
||||
@ -138,8 +121,10 @@ impl Term {
|
||||
}
|
||||
}
|
||||
|
||||
impl Term {
|
||||
// Kind -> KindCore
|
||||
// ----------------
|
||||
|
||||
impl Term {
|
||||
pub fn to_kindc(&self, env: im::Vector<String>, met: &mut usize) -> String {
|
||||
match self {
|
||||
Term::All { era: _, nam, inp, bod } => {
|
||||
@ -190,7 +175,6 @@ impl Term {
|
||||
Term::Txt { txt } => format!("\"{}\"", txt.replace("\n", "\\n")),
|
||||
Term::Mch { .. } => unreachable!(),
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
pub fn to_kindc_name(name: &str) -> String {
|
||||
@ -220,3 +204,113 @@ impl Oper {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Kind -> JavaScript
|
||||
// ------------------
|
||||
|
||||
impl Term {
|
||||
|
||||
pub fn to_js(&self) -> String {
|
||||
let mut term = self.clone();
|
||||
term.sanitize(&mut BTreeMap::new(), &mut 0);
|
||||
//term.desugar();
|
||||
//term.expand_implicits(im::Vector::new(), &BTreeMap::new());
|
||||
term.to_js_go()
|
||||
}
|
||||
|
||||
pub fn to_js_go(&self) -> String {
|
||||
match self {
|
||||
Term::All { era: _, nam: _, inp: _, bod: _ } => {
|
||||
"null".to_string()
|
||||
},
|
||||
Term::Lam { era: _, nam, bod } => {
|
||||
format!("({}) => {}", Term::to_js_name(nam), bod.to_js_go())
|
||||
},
|
||||
Term::App { era: _, fun, arg } => {
|
||||
format!("{}({})", fun.to_js_go(), arg.to_js_go())
|
||||
},
|
||||
Term::Ann { chk: _, val, typ: _ } => {
|
||||
val.to_js_go()
|
||||
},
|
||||
Term::Slf { nam: _, typ: _, bod: _ } => {
|
||||
"null".to_string()
|
||||
},
|
||||
Term::Ins { val } => {
|
||||
val.to_js_go()
|
||||
},
|
||||
Term::Set => {
|
||||
"null".to_string()
|
||||
},
|
||||
Term::U48 => {
|
||||
"null".to_string()
|
||||
},
|
||||
Term::Num { val } => {
|
||||
val.to_string()
|
||||
},
|
||||
Term::Op2 { opr, fst, snd } => {
|
||||
format!("Math.floor({} {} {})", fst.to_js_go(), opr.to_js(), snd.to_js_go())
|
||||
},
|
||||
Term::Swi { nam, x, z, s, p: _ } => {
|
||||
format!("(() => {{ const {} = {}; switch ({}) {{ case 0: return {}; default: return (({} => {})(({}) - 1)); }} }})()",
|
||||
Term::to_js_name(nam), x.to_js_go(), Term::to_js_name(nam), z.to_js_go(), Term::to_js_name(nam), s.to_js_go(), Term::to_js_name(nam))
|
||||
},
|
||||
Term::Let { nam, val, bod } => {
|
||||
format!("(() => {{ const {} = {}; return {}; }})()", Term::to_js_name(nam), val.to_js_go(), bod.to_js_go())
|
||||
},
|
||||
Term::Use { nam, val, bod } => {
|
||||
format!("(() => {{ const {} = {}; return {}; }})()", Term::to_js_name(nam), val.to_js_go(), bod.to_js_go())
|
||||
},
|
||||
Term::Hol { nam: _ } => {
|
||||
"null".to_string()
|
||||
},
|
||||
Term::Met {} => {
|
||||
//println!("WARNING: unsolved metas.");
|
||||
"null".to_string()
|
||||
},
|
||||
Term::Var { nam } => {
|
||||
Term::to_js_name(nam)
|
||||
},
|
||||
Term::Src { src: _, val } => {
|
||||
val.to_js_go()
|
||||
},
|
||||
Term::Nat { nat } => {
|
||||
format!("{}", nat)
|
||||
},
|
||||
Term::Txt { txt } => {
|
||||
format!("\"{}\"", txt.replace("\n", "\\n"))
|
||||
},
|
||||
Term::Mch { .. } => {
|
||||
unreachable!()
|
||||
},
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_js_name(name: &str) -> String {
|
||||
name.replace("/", "_").replace(".","_")
|
||||
}
|
||||
}
|
||||
|
||||
impl Oper {
|
||||
pub fn to_js(&self) -> &'static str {
|
||||
match self {
|
||||
Oper::Add => "+",
|
||||
Oper::Sub => "-",
|
||||
Oper::Mul => "*",
|
||||
Oper::Div => "/",
|
||||
Oper::Mod => "%",
|
||||
Oper::Eq => "===",
|
||||
Oper::Ne => "!==",
|
||||
Oper::Lt => "<",
|
||||
Oper::Gt => ">",
|
||||
Oper::Lte => "<=",
|
||||
Oper::Gte => ">=",
|
||||
Oper::And => "&&",
|
||||
Oper::Or => "||",
|
||||
Oper::Xor => "^",
|
||||
Oper::Lsh => "<<",
|
||||
Oper::Rsh => ">>",
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
@ -164,6 +164,97 @@ impl Term {
|
||||
}
|
||||
}
|
||||
|
||||
// FIXME: remove this comment \/
|
||||
// Implement a function that renames shadowed variable to have unique names
|
||||
// Have an immutable map from name to new name
|
||||
// Have a depth counter
|
||||
// On binders, add a mapping: name => name_{depth}
|
||||
// On variables, just retrieve
|
||||
// Receive a mutable term
|
||||
pub fn sanitize(&mut self, name_map: &mut BTreeMap<String, String>, depth: &mut u64) {
|
||||
match self {
|
||||
Term::All { era: _, nam, inp, bod } => {
|
||||
inp.sanitize(name_map, depth);
|
||||
*depth += 1;
|
||||
let new_name = format!("{}_{}", nam, depth);
|
||||
name_map.insert(nam.clone(), new_name.clone());
|
||||
*nam = new_name;
|
||||
bod.sanitize(name_map, depth);
|
||||
*depth -= 1;
|
||||
},
|
||||
Term::Lam { era: _, nam, bod } => {
|
||||
*depth += 1;
|
||||
let new_name = format!("{}_{}", nam, depth);
|
||||
name_map.insert(nam.clone(), new_name.clone());
|
||||
*nam = new_name;
|
||||
bod.sanitize(name_map, depth);
|
||||
*depth -= 1;
|
||||
},
|
||||
Term::App { era: _, fun, arg } => {
|
||||
fun.sanitize(name_map, depth);
|
||||
arg.sanitize(name_map, depth);
|
||||
},
|
||||
Term::Ann { chk: _, val, typ } => {
|
||||
val.sanitize(name_map, depth);
|
||||
typ.sanitize(name_map, depth);
|
||||
},
|
||||
Term::Slf { nam, typ, bod } => {
|
||||
typ.sanitize(name_map, depth);
|
||||
*depth += 1;
|
||||
let new_name = format!("{}_{}", nam, depth);
|
||||
name_map.insert(nam.clone(), new_name.clone());
|
||||
*nam = new_name;
|
||||
bod.sanitize(name_map, depth);
|
||||
*depth -= 1;
|
||||
},
|
||||
Term::Ins { val } => {
|
||||
val.sanitize(name_map, depth);
|
||||
},
|
||||
Term::Op2 { opr: _, fst, snd } => {
|
||||
fst.sanitize(name_map, depth);
|
||||
snd.sanitize(name_map, depth);
|
||||
},
|
||||
Term::Swi { nam, x, z, s, p } => {
|
||||
x.sanitize(name_map, depth);
|
||||
z.sanitize(name_map, depth);
|
||||
*depth += 1;
|
||||
let new_name = format!("{}_{}", nam, depth);
|
||||
name_map.insert(nam.clone(), new_name.clone());
|
||||
*nam = new_name;
|
||||
s.sanitize(name_map, depth);
|
||||
p.sanitize(name_map, depth);
|
||||
*depth -= 1;
|
||||
},
|
||||
Term::Let { nam, val, bod } => {
|
||||
val.sanitize(name_map, depth);
|
||||
*depth += 1;
|
||||
let new_name = format!("{}_{}", nam, depth);
|
||||
name_map.insert(nam.clone(), new_name.clone());
|
||||
*nam = new_name;
|
||||
bod.sanitize(name_map, depth);
|
||||
*depth -= 1;
|
||||
},
|
||||
Term::Use { nam, val, bod } => {
|
||||
val.sanitize(name_map, depth);
|
||||
*depth += 1;
|
||||
let new_name = format!("{}_{}", nam, depth);
|
||||
name_map.insert(nam.clone(), new_name.clone());
|
||||
*nam = new_name;
|
||||
bod.sanitize(name_map, depth);
|
||||
*depth -= 1;
|
||||
},
|
||||
Term::Var { nam } => {
|
||||
if let Some(new_name) = name_map.get(nam) {
|
||||
*nam = new_name.clone();
|
||||
}
|
||||
},
|
||||
Term::Src { src: _, val } => {
|
||||
val.sanitize(name_map, depth);
|
||||
},
|
||||
_ => {}
|
||||
}
|
||||
}
|
||||
|
||||
// Removes Src's
|
||||
pub fn clean(&self) -> Term {
|
||||
match self {
|
||||
|
Loading…
Reference in New Issue
Block a user