From 9981cfbabced718ee764a89d78370fe33501db54 Mon Sep 17 00:00:00 2001 From: Samuel Durante Date: Thu, 14 Jul 2022 14:07:04 -0300 Subject: [PATCH 1/2] Add clap cli --- Cargo.lock | 1 + Cargo.toml | 1 + src/cli.rs | 20 ++++++++++++++++++ src/main.rs | 60 +++++++++++++++++++++++++++++++++-------------------- 4 files changed, 59 insertions(+), 23 deletions(-) create mode 100644 src/cli.rs diff --git a/Cargo.lock b/Cargo.lock index 94a30715..91d29c76 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -135,6 +135,7 @@ dependencies = [ name = "kind2" version = "0.1.0" dependencies = [ + "clap", "hvm", ] diff --git a/Cargo.toml b/Cargo.toml index 980128a0..4355dc89 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -7,3 +7,4 @@ edition = "2021" [dependencies] hvm = "0.1.38" +clap = { version = "3.1.8", features = ["derive"] } diff --git a/src/cli.rs b/src/cli.rs new file mode 100644 index 00000000..1d5f5dac --- /dev/null +++ b/src/cli.rs @@ -0,0 +1,20 @@ +pub use clap::{Parser, Subcommand}; + +#[derive(Parser)] +#[clap(author, version, about, long_about = None)] +#[clap(propagate_version = true)] +pub struct Cli { + #[clap(subcommand)] + pub command: Command, +} + +#[derive(Subcommand)] +pub enum Command { + /// Run a file interpreted + #[clap(aliases = &["r"])] + Run { file: String, params: Vec }, + + /// Check a file + #[clap(aliases = &["c"])] + Check { file: String, params: Vec }, +} diff --git a/src/main.rs b/src/main.rs index f3ad291c..d91f9daf 100644 --- a/src/main.rs +++ b/src/main.rs @@ -3,23 +3,47 @@ // TODO: type{} syntax +mod cli; + use std::collections::HashMap; +use cli::{Cli, Command, Parser}; use hvm::parser as parser; -fn main() -> Result<(), String> { - gen(); +fn main() { + match run_cli() { + Ok(..) => {} + Err(err) => { + eprintln!("{}", err); + } + }; +} - let args: Vec = std::env::args().collect(); +fn gen() { + let file = read_file(&DEMO_CODE).unwrap(); + let code = compile_file(&file); + let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string(); + checker.push_str(&code); + std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file +} - if args.len() <= 2 || args[1] != "check" && args[1] != "run" { - println!("Usage:"); - println!("$ kind2 check file.kind"); - println!("$ kind2 run file.kind"); - return Ok(()); +const CHECKER_HVM: &str = include_str!("checker.hvm"); + +fn run_cli() -> Result<(), String> { + let cli_matches = Cli::parse(); + + match cli_matches.command { + Command::Run { file: path, params } => { + kind2(&path, "Api.run_main") + } + + Command::Check { file: path, params } => { + kind2(&path, "Api.check_all") + } } +} - let path = &args[2]; - let file = match std::fs::read_to_string(path) { +fn kind2(path: &str, main_function: &str) -> Result<(), String> { + let file = match std::fs::read_to_string(&path) { Ok(code) => read_file(&code), Err(msg) => read_file(&DEMO_CODE), }; @@ -39,25 +63,15 @@ fn main() -> Result<(), String> { std::fs::write(format!("{}.hvm", path), checker.clone()).ok(); // writes checker to the checker.hvm file let mut rt = hvm::Runtime::from_code(&checker)?; - let main = rt.alloc_code(if args[1] == "check" { "Api.check_all" } else { "Api.run_main" })?; + let main = rt.alloc_code(main_function)?; rt.normalize(main); println!("{}", readback_string(&rt, main)); // TODO: optimize by deserializing term into text directly - println!("Rewrites: {}", rt.get_rewrites()); + eprintln!("Rewrites: {}", rt.get_rewrites()); - return Ok(()); + Ok(()) } -fn gen() { - let file = read_file(&DEMO_CODE).unwrap(); - let code = compile_file(&file); - let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string(); - checker.push_str(&code); - std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file -} - -const CHECKER_HVM: &str = include_str!("checker.hvm"); - #[derive(Clone, Debug)] pub enum Term { Typ, From ebaff0ee8a6e5284b539c7d3494637dba2a5bd4b Mon Sep 17 00:00:00 2001 From: Samuel Durante Date: Thu, 14 Jul 2022 20:52:37 -0300 Subject: [PATCH 2/2] Resolving conflicts --- Cargo.lock | 13 +- Cargo.toml | 2 +- bench/README.md | 7 + bench/nat_exp.kind2 | 45 ++-- bench/nat_exp.lean | 25 ++ example.kind2 | 48 ---- src/language.rs | 618 ++++++++++++++++++++++++++++++++++++++++++++ src/main.rs | 598 ++++-------------------------------------- 8 files changed, 733 insertions(+), 623 deletions(-) create mode 100644 bench/nat_exp.lean delete mode 100644 example.kind2 create mode 100644 src/language.rs diff --git a/Cargo.lock b/Cargo.lock index 91d29c76..6a984ff9 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -101,12 +101,19 @@ dependencies = [ ] [[package]] -name = "hvm" -version = "0.1.38" +name = "highlight_error" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1e25cb7dd4f63d4640709b13cc1f330189e2195318eaf3ab372d732d12df3aa" +checksum = "809e18805660d7b6b2e2b9f316a5099521b5998d5cba4dda11b5157a21aaef03" + +[[package]] +name = "hvm" +version = "0.1.40" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f73a95e6ba27736390f1cdebea112de3740beebac40102291dc09917bd7e721" dependencies = [ "clap", + "highlight_error", "itertools", "num_cpus", "regex", diff --git a/Cargo.toml b/Cargo.toml index 4355dc89..9db1ef1b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -6,5 +6,5 @@ edition = "2021" # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html [dependencies] -hvm = "0.1.38" +hvm = "0.1.40" clap = { version = "3.1.8", features = ["derive"] } diff --git a/bench/README.md b/bench/README.md index 3855ec44..9055b632 100644 --- a/bench/README.md +++ b/bench/README.md @@ -16,6 +16,12 @@ time agda -i src file.agda time idris2 --check file.idr ``` +### Lean + +``` +time lean file.lean +``` + ### Kind2 ``` @@ -45,4 +51,5 @@ Kind2-C | 0.17 s Kind2 | 0.58 s Agda | 15.55 s Idris2 | 67.40 s +Lean | timeout ``` diff --git a/bench/nat_exp.kind2 b/bench/nat_exp.kind2 index b3d05b3e..626cfa6b 100644 --- a/bench/nat_exp.kind2 +++ b/bench/nat_exp.kind2 @@ -1,29 +1,26 @@ Nat : Type - Z : Nat - S (pred: Nat) : Nat +Z : Nat +S (pred: Nat) : Nat The (x: Nat) : Type - Val (x: Nat) : {The x} +Val (x: Nat) : (The x) -Add (a: Nat) (b: Nat) : Nat { - Add a {S b} = {S (Add a b)} - Add a {Z} = a +Add (a: Nat) (b: Nat) : Nat +Add a (S b) = (S (Add a b)) +Add a (Z) = a + +Mul (a: Nat) (b: Nat) : Nat +Mul a (S b) = (Add a (Mul a b)) +Mul a (Z) = (Z) + +Exp (a: Nat) (b: Nat) : Nat +Exp a (S b) = (Mul a (Exp a b)) +Exp a (Z) = (S Z) + +Nul (n: Nat) : Nat +Nul (S a) = (Nul a) +Nul (Z) = (Z) + +Work : (The (Nul (Exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))) { + (Val Z) } - -Mul (a: Nat) (b: Nat) : Nat { - Mul a {S b} = (Add a (Mul a b)) - Mul a {Z} = {Z} -} - -Exp (a: Nat) (b: Nat) : Nat { - Exp a {S b} = (Mul a (Exp a b)) - Exp a {Z} = {S Z} -} - -Nul (n: Nat) : Nat { - Nul {S a} = (Nul a) - Nul {Z} = {Z} -} - -Work : {The (Nul (Exp {S {S {S Z}}} {S {S {S {S {S {S {S {S Z}}}}}}}}))} = - {Val Z} diff --git a/bench/nat_exp.lean b/bench/nat_exp.lean new file mode 100644 index 00000000..cf98a958 --- /dev/null +++ b/bench/nat_exp.lean @@ -0,0 +1,25 @@ +inductive NAT where + | Z : NAT + | S : NAT -> NAT + +inductive The : NAT -> Type where + | val : (x : NAT) -> The x + +def add : NAT -> NAT -> NAT + | a, NAT.S b => NAT.S (add a b) + | a, NAT.Z => a + +def mul : NAT -> NAT -> NAT + | a, NAT.S b => add a (mul a b) + | _, NAT.Z => NAT.Z + +def exp : NAT -> NAT -> NAT + | a, NAT.S b => mul a (exp a b) + | _, NAT.Z => NAT.S NAT.Z + +def nul : NAT -> NAT + | NAT.S a => nul a + | NAT.Z => NAT.Z + +def work : The (nul (exp (NAT.S (NAT.S (NAT.S NAT.Z))) (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S NAT.Z)))))))))) + := @The.val NAT.Z diff --git a/example.kind2 b/example.kind2 deleted file mode 100644 index dfa59612..00000000 --- a/example.kind2 +++ /dev/null @@ -1,48 +0,0 @@ -Bool : Type - True : Bool - False : Bool - -Nat : Type - Zero : Nat - Succ (pred: Nat) : Nat - -List (a: Type) : Type - Nil (a: Type) : {List a} - Cons (a: Type) (x: a) (xs: {List a}) : {List a} - -Not (a: Bool) : Bool { - Not True = False - Not False = True -} - -And (a: Bool) (b: Bool) : Bool { - And True True = True - And True False = False - And False True = False - And False False = False -} - -Negate (xs: {List Bool}) : {List Bool} { - Negate {Cons Bool x xs} = {Cons Bool (Not x) (Negate xs)} - Negate {Nil Bool} = {Nil Bool} -} - -Double (x: Nat) : Nat { - Double {Succ x} = {Succ {Succ (Double x)}} - Double {Zero} = {Zero} -} - -// FIXME: shouldn't type-check, but does due to Inp treatment -Tail (a: Type) (xs: {List a}) : {List a} { - Tail a {Cons t x xs} = x -} - -Main : Nat = (Double {Succ {Succ Zero}}) - - - - - - - - diff --git a/src/language.rs b/src/language.rs new file mode 100644 index 00000000..61579674 --- /dev/null +++ b/src/language.rs @@ -0,0 +1,618 @@ +use std::collections::HashMap; +use hvm::parser as parser; + +#[derive(Clone, Debug)] +pub struct File { + entries: HashMap> +} + +#[derive(Clone, Debug)] +pub struct Entry { + name: String, + args: Vec>, + tipo: Box, + rules: Vec> +} + +#[derive(Clone, Debug)] +pub struct Argument { + eras: bool, + name: String, + tipo: Box, +} + +#[derive(Clone, Debug)] +pub struct Rule { + name: String, + pats: Vec>, + body: Box, +} + +#[derive(Clone, Debug)] +pub enum Term { + Typ, + Var { name: String }, + Let { name: String, expr: Box, body: Box }, + All { name: String, tipo: Box, body: Box }, + Lam { name: String, body: Box }, + App { func: Box, argm: Box }, + Ctr { name: String, args: Vec> }, + Fun { name: String, args: Vec> }, +} + +// Adjuster +// ======== + +pub fn adjust_file(file: &File) -> File { + let mut entries = HashMap::new(); + for (name, entry) in &file.entries { + entries.insert(name.clone(), Box::new(adjust_entry(file, &*entry))); + } + return File { entries }; +} + +pub fn adjust_entry(file: &File, entry: &Entry) -> Entry { + let name = entry.name.clone(); + let mut args = Vec::new(); + for arg in &entry.args { + args.push(Box::new(adjust_argument(file, arg))); + } + let tipo = Box::new(adjust_term(file, &*entry.tipo)); + let mut rules = Vec::new(); + for rule in &entry.rules { + rules.push(Box::new(adjust_rule(file, &*rule))); + } + return Entry { name, args, tipo, rules }; +} + +pub fn adjust_argument(file: &File, arg: &Argument) -> Argument { + let eras = arg.eras; + let name = arg.name.clone(); + let tipo = Box::new(adjust_term(file, &*arg.tipo)); + return Argument { eras, name, tipo }; +} + +pub fn adjust_rule(file: &File, rule: &Rule) -> Rule { + let name = rule.name.clone(); + let mut pats = Vec::new(); + for pat in &rule.pats { + pats.push(Box::new(adjust_term(file, &*pat))); + } + let body = Box::new(adjust_term(file, &*rule.body)); + return Rule { name, pats, body }; +} + +pub fn adjust_term(file: &File, term: &Term) -> Term { + match *term { + Term::Typ => { + Term::Typ + }, + Term::Var { ref name } => { + Term::Var { name: name.clone() } + }, + Term::Let { ref name, ref expr, ref body } => { + let expr = Box::new(adjust_term(file, &*expr)); + let body = Box::new(adjust_term(file, &*body)); + Term::Let { name: name.clone(), expr, body } + }, + Term::All { ref name, ref tipo, ref body } => { + let tipo = Box::new(adjust_term(file, &*tipo)); + let body = Box::new(adjust_term(file, &*body)); + Term::All { name: name.clone(), tipo, body } + }, + Term::Lam { ref name, ref body } => { + let body = Box::new(adjust_term(file, &*body)); + Term::Lam { name: name.clone(), body } + }, + Term::App { ref func, ref argm } => { + let func = Box::new(adjust_term(file, &*func)); + let argm = Box::new(adjust_term(file, &*argm)); + Term::App { func, argm } + }, + Term::Ctr { ref name, ref args } => { + if let Some(entry) = file.entries.get(name) { + let mut new_args = Vec::new(); + for arg in args { + new_args.push(Box::new(adjust_term(file, &*arg))); + } + if entry.rules.len() > 0 { + Term::Fun { name: name.clone(), args: new_args } + } else { + Term::Ctr { name: name.clone(), args: new_args } + } + } else { + panic!("Missing declaration for: '{}'.", name); + } + }, + Term::Fun { ref name, ref args } => { + panic!("Internal error."); // shouldn't happen since we can't parse Fun{} + }, + } +} + +// Parser +// ====== + +pub fn is_var_head(head: char) -> bool { + ('a'..='z').contains(&head) || head == '_' || head == '$' +} + +pub fn is_ctr_head(head: char) -> bool { + ('A'..='Z').contains(&head) +} + +pub fn parse_var_name(state: parser::State) -> parser::Answer { + let (state, name) = parser::name1(state)?; + if !is_var_head(name.chars().nth(0).unwrap_or(' ')) { + let state = parser::State { index: state.index - name.len(), code: state.code }; // TODO: improve? + return parser::expected("lowercase name", name.len(), state); + } else { + return Ok((state, name)); + } +} + +pub fn parse_ctr_name(state: parser::State) -> parser::Answer { + let (state, name) = parser::name1(state)?; + if !is_ctr_head(name.chars().nth(0).unwrap_or(' ')) { + let state = parser::State { index: state.index - name.len(), code: state.code }; // TODO: improve? + return parser::expected("uppercase name", name.len(), state); + } else { + return Ok((state, name)); + } +} + +pub fn parse_var(state: parser::State) -> parser::Answer>> { + parser::guard( + Box::new(|state| { + let (state, head) = parser::get_char(state)?; + Ok((state, is_var_head(head))) + }), + Box::new(|state| { + let (state, name) = parse_var_name(state)?; + Ok((state, Box::new(Term::Var { name }))) + }), + state, + ) +} + +pub fn parse_lam(state: parser::State) -> parser::Answer>> { + parser::guard( + parser::text_parser("@"), + Box::new(move |state| { + let (state, _) = parser::consume("@", state)?; + let (state, name) = parse_var_name(state)?; + let (state, body) = parse_term(state)?; + Ok((state, Box::new(Term::Lam { name, body }))) + }), + state, + ) +} + +pub fn parse_all(state: parser::State) -> parser::Answer>> { + parser::guard( + Box::new(|state| { + let (state, all0) = parser::text("(", state)?; + let (state, name) = parser::name(state)?; + let (state, all1) = parser::text(":", state)?; + Ok((state, all0 && all1 && name.len() > 0 && is_var_head(name.chars().nth(0).unwrap_or(' ')))) + }), + Box::new(|state| { + let (state, _) = parser::consume("(", state)?; + let (state, name) = parse_var_name(state)?; + let (state, _) = parser::consume(":", state)?; + let (state, tipo) = parse_term(state)?; + let (state, _) = parser::consume(")", state)?; + let (state, body) = parse_term(state)?; + Ok((state, Box::new(Term::All { name, tipo, body }))) + }), + state, + ) +} + +pub fn parse_app(state: parser::State) -> parser::Answer>> { + return parser::guard( + parser::text_parser("("), + Box::new(|state| { + parser::list( + parser::text_parser("("), + parser::text_parser(""), + parser::text_parser(")"), + Box::new(parse_term), + Box::new(|args| { + if !args.is_empty() { + args.into_iter().reduce(|a, b| Box::new(Term::App { func: a, argm: b })).unwrap() + } else { + Box::new(Term::Var { name: "?".to_string() }) + } + }), + state, + ) + }), + state, + ); +} + +pub fn parse_let(state: parser::State) -> parser::Answer>> { + return parser::guard( + parser::text_parser("let "), + Box::new(|state| { + let (state, _) = parser::consume("let ", state)?; + let (state, name) = parse_var_name(state)?; + let (state, _) = parser::consume("=", state)?; + let (state, expr) = parse_term(state)?; + let (state, _) = parser::text(";", state)?; + let (state, body) = parse_term(state)?; + Ok((state, Box::new(Term::Let { name, expr, body }))) + }), + state, + ); +} + +pub fn parse_ctr(state: parser::State) -> parser::Answer>> { + parser::guard( + Box::new(|state| { + let (state, _) = parser::text("(", state)?; + let (state, head) = parser::get_char(state)?; + Ok((state, is_ctr_head(head))) + }), + Box::new(|state| { + let (state, open) = parser::text("(", state)?; + let (state, name) = parse_ctr_name(state)?; + if name == "Type" { + Ok((state, Box::new(Term::Typ))) + } else { + let (state, args) = if open { + parser::until(parser::text_parser(")"), Box::new(parse_term), state)? + } else { + (state, Vec::new()) + }; + Ok((state, Box::new(Term::Ctr { name, args }))) + } + }), + state, + ) +} + +pub fn parse_term(state: parser::State) -> parser::Answer> { + parser::grammar( + "Term", + &[ + Box::new(parse_let), // `let ` + Box::new(parse_all), // `(name:` + Box::new(parse_ctr), // `(Name` + Box::new(parse_app), // `(` + Box::new(parse_lam), // `@` + Box::new(parse_var), // + Box::new(|state| Ok((state, None))), + ], + state, + ) +} + +pub fn parse_entry(state: parser::State) -> parser::Answer> { + let (state, name) = parse_ctr_name(state)?; + 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)?; + return Ok((state, end_0 || end_1)); + }), Box::new(parse_argument), state)?; + let (state, next) = parser::peek_char(state)?; + let (state, tipo) = if next == ':' { + let (state, anno) = parser::consume(":", state)?; + parse_term(state)? + } else { + (state, Box::new(Term::Typ)) // TODO: return a hole + }; + let (state, head) = parser::peek_char(state)?; + if head == '{' { + let (state, _) = parser::consume("{", state)?; + let (state, body) = parse_term(state)?; + let (state, _) = parser::consume("}", state)?; + let mut pats = vec![]; + for arg in &args { + pats.push(Box::new(Term::Var { name: arg.name.clone() })); + } + let rules = vec![Box::new(Rule { name: name.clone(), pats, body })]; + return Ok((state, Box::new(Entry { name, args, tipo, rules }))); + } else { + let mut rules = Vec::new(); + let rule_prefix = &format!("{} ", name); + let mut state = state; + loop { + let loop_state = state; + let (loop_state, cont) = parser::text(&rule_prefix, loop_state)?; + if cont { + let (loop_state, rule) = parse_rule(loop_state, name.clone())?; + rules.push(rule); + state = loop_state; + } else { + state = loop_state; + break; + } + } + return Ok((state, Box::new(Entry { name, args, tipo, rules }))); + } +} + +pub fn parse_rule(state: parser::State, name: String) -> parser::Answer> { + let (state, pats) = parser::until(parser::text_parser("="), Box::new(parse_term), state)?; + let (state, body) = parse_term(state)?; + return Ok((state, Box::new(Rule { name, pats, body }))); +} + +pub fn parse_argument(state: parser::State) -> parser::Answer> { + let (state, _) = parser::consume("(", state)?; + let (state, name) = parse_var_name(state)?; + let (state, _) = parser::consume(":", state)?; + let (state, tipo) = parse_term(state)?; + let (state, _) = parser::consume(")", state)?; + return Ok((state, Box::new(Argument { eras: false, name, tipo }))); +} + +pub fn parse_file(state: parser::State) -> parser::Answer> { + let (state, entry_vec) = parser::until(Box::new(parser::done), Box::new(parse_entry), state)?; + let mut entries = HashMap::new(); + for entry in entry_vec { + entries.insert(entry.name.clone(), entry); + } + return Ok((state, Box::new(File { entries }))); +} + +pub fn show_term(term: &Term) -> String { + match term { + Term::Typ => { + format!("Type") + } + Term::Var { name } => { + format!("{}", name) + } + Term::Let { name, expr, body } => { + let expr = show_term(expr); + let body = show_term(body); + format!("let {} = {}; {}", name, expr, body) + } + Term::Lam { name, body } => { + let body = show_term(body); + format!("@{}({})", name, body) + } + Term::App { func, argm } => { + let mut args = vec![argm]; + let mut expr = func; + while let Term::App { func, argm } = &**expr { + args.push(argm); + expr = func; + } + args.reverse(); + format!("({} {})", show_term(expr), args.iter().map(|x| show_term(x)).collect::>().join(" ")) + } + Term::All { name, tipo, body } => { + let body = show_term(body); + format!("({}: {}) {}", name, show_term(tipo), body) + } + Term::Ctr { name, args } => { + format!("{{{}{}}}", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::()) + } + Term::Fun { name, args } => { + format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::()) + } + } +} + +pub fn show_rule(rule: &Rule) -> String { + let name = &rule.name; + let mut pats = vec![]; + for pat in &rule.pats { + pats.push(show_term(pat)); + } + let body = show_term(&rule.body); + format!("{} {} => {}", name, pats.join(" "), body) +} + +pub fn show_entry(entry: &Entry) -> String { + let name = &entry.name; + let mut args = vec![]; + for arg in &entry.args { + args.push(format!(" ({}: {})", arg.name, show_term(&arg.tipo))); + } + if entry.rules.len() == 0 { + format!("{}{} : {}", name, args.join(""), show_term(&entry.tipo)) + } else { + let mut rules = vec![]; + for rule in &entry.rules { + rules.push(format!("\n {}", show_rule(rule))); + } + format!("{}{} : {} {{{}\n}}", name, args.join(""), show_term(&entry.tipo), rules.join("")) + } +} + +pub fn show_file(file: &File) -> String { + let mut entries = vec![]; + for entry in file.entries.values() { + entries.push(show_entry(entry)); + } + entries.join("\n") +} + +pub fn read_term(code: &str) -> Result, String> { + parser::read(Box::new(parse_term), code) +} + +pub fn read_file(code: &str) -> Result, String> { + parser::read(Box::new(parse_file), code) +} + +// Compiler +// ======== + +//pub enum Term { + //Typ, + //Var { name: String }, + //Let { name: String, expr: Box, body: Box }, + //App { func: Box, argm: Box }, + //Lam { name: String, body: Box }, + //All { name: String, tipo: Box, body: Box }, + //Ctr { name: String, args: Vec> }, + //Fun { name: String, args: Vec> }, +//} +pub fn compile_term(term: &Term, quote: bool) -> String { + match term { + Term::Typ => { + format!("Typ") + } + Term::Var { name } => { + name.clone() + } + Term::Let { name, expr, body } => { + todo!() + } + Term::All { name, tipo, body } => { + format!("(All {} λ{} {})", compile_term(tipo, quote), name, compile_term(body, quote)) + } + Term::Lam { name, body } => { + format!("(Lam λ{} {})", name, compile_term(body, quote)) + } + Term::App { func, argm } => { + format!("({} {} {})", if quote { "App" } else { "Apply" }, compile_term(func, quote), compile_term(argm, quote)) + } + Term::Ctr { name, args } => { + let mut args_strs : Vec = Vec::new(); + for arg in args { + args_strs.push(format!(" {}", compile_term(arg, quote))); + } + format!("(Ct{} {}.{})", args.len(), name, args_strs.join("")) + } + Term::Fun { name, args } => { + let mut args_strs : Vec = Vec::new(); + for arg in args { + args_strs.push(format!(" {}", compile_term(arg, quote))); + } + format!("({}{} {}.{})", if quote { "NewFn" } else { "Rule_" }, args.len(), name, args_strs.join("")) + } + } +} + +pub fn compile_entry(entry: &Entry) -> String { + fn compile_type(args: &Vec>, tipo: &Box, index: usize) -> String { + if index < args.len() { + let arg = &args[index]; + format!("(All {} λ{} {})", compile_term(&arg.tipo, false), arg.name, compile_type(args, tipo, index + 1)) + } else { + compile_term(tipo, false) + } + } + + fn compile_rule(rule: &Rule) -> String { + let mut pats = vec![]; + for pat in &rule.pats { + pats.push(format!(" {}", compile_term(pat, false))); + } + let mut vars = vec![]; + for idx in 0 .. pats.len() { + vars.push(format!(" x{}", idx)); + } + let body_rhs = compile_term(&rule.body, true); + let rule_rhs = compile_term(&rule.body, false); + let mut text = String::new(); + //text.push_str(&format!(" (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body)); + text.push_str(&format!(" (Body_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_rhs)); + //text.push_str(&format!(" (Body_{} {}.{}) = (NewFn{} {}.{})\n", rule.pats.len(), rule.name, vars.join(""), rule.pats.len(), rule.name, vars.join(""))); + text.push_str(&format!(" (Rule_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), rule_rhs)); + return text; + } + + fn compile_rule_chk(rule: &Rule, index: usize, vars: &mut u64, args: &mut Vec) -> String { + if index < rule.pats.len() { + let (inp_patt_str, var_patt_str) = compile_patt_chk(&rule.pats[index], vars); + args.push(var_patt_str); + let head = inp_patt_str; + let tail = compile_rule_chk(rule, index + 1, vars, args); + return format!("(LHS {} {})", head, tail); + } else { + return format!("(RHS (Body_{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::>().join("")); + } + } + + fn compile_patt_chk(patt: &Term, vars: &mut u64) -> (String, String) { + match patt { + Term::Var { .. } => { + let inp = format!("(Inp {})", vars); + let var = format!("(Var {})", vars); + *vars += 1; + return (inp, var); + } + Term::Ctr { name, args } => { + let mut inp_args_str = String::new(); + let mut var_args_str = String::new(); + for arg in args { + let (inp_arg_str, var_arg_str) = compile_patt_chk(arg, vars); + inp_args_str.push_str(&format!(" {}", inp_arg_str)); + var_args_str.push_str(&format!(" {}", var_arg_str)); + } + let inp_str = format!("(Ct{} {}.{})", args.len(), name, inp_args_str); + let var_str = format!("(Ct{} {}.{})", args.len(), name, var_args_str); + return (inp_str, var_str); + } + _ => { + panic!("Invalid left-hand side pattern: {}", show_term(patt)); + } + } + } + + let mut result = String::new(); + result.push_str(&format!(" (NameOf {}.) = \"{}\"\n", entry.name, entry.name)); + result.push_str(&format!(" (HashOf {}.) = %{}\n", entry.name, entry.name)); + result.push_str(&format!(" (TypeOf {}.) = {}\n", entry.name, compile_type(&entry.args, &entry.tipo, 0))); + for rule in &entry.rules { + result.push_str(&compile_rule(&rule)); + } + result.push_str(&format!(" (Verify {}.) =\n", entry.name)); + for rule in &entry.rules { + result.push_str(&format!(" (Cons {}\n", compile_rule_chk(&rule, 0, &mut 0, &mut vec![]))); + } + result.push_str(&format!(" Nil{}\n", ")".repeat(entry.rules.len()))); + return result; +} + +pub fn compile_file(file: &File) -> String { + let mut result = String::new(); + result.push_str(&format!("\n Functions =\n")); + result.push_str(&format!(" let fns = Nil\n")); + for entry in file.entries.values() { + result.push_str(&format!(" let fns = (Cons {}. fns)\n", entry. name)); + } + result.push_str(&format!(" fns\n\n")); + for entry in file.entries.values() { + result.push_str(&format!(" // {}\n", entry.name)); + result.push_str(&format!(" // {}\n", "-".repeat(entry.name.len()))); + result.push_str(&format!("\n")); + result.push_str(&compile_entry(&entry)); + result.push_str(&format!("\n")); + } + return result; +} + +pub fn readback_string(rt: &hvm::Runtime, host: u64) -> String { + let str_cons = rt.get_id("String.cons"); + let str_nil = rt.get_id("String.nil"); + let mut term = rt.ptr(host); + let mut text = String::new(); + loop { + if hvm::get_tag(term) == hvm::CTR { + let fid = hvm::get_ext(term); + if fid == str_cons { + let head = rt.ptr(hvm::get_loc(term, 0)); + let tail = rt.ptr(hvm::get_loc(term, 1)); + if hvm::get_tag(head) == hvm::NUM { + text.push(std::char::from_u32(hvm::get_num(head) as u32).unwrap_or('?')); + term = tail; + continue; + } + } + if fid == str_nil { + break; + } + } + panic!("Invalid output: {} {}", hvm::get_tag(term), rt.show(host)); + } + return text; +} diff --git a/src/main.rs b/src/main.rs index d91f9daf..30e67ddf 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,14 +1,15 @@ #![allow(dead_code)] #![allow(unused_variables)] -// TODO: type{} syntax - mod cli; +mod language; -use std::collections::HashMap; -use cli::{Cli, Command, Parser}; +use cli::{Cli, Parser, Command}; +use language::{*}; use hvm::parser as parser; +const CHECKER_HVM: &str = include_str!("checker.hvm"); + fn main() { match run_cli() { Ok(..) => {} @@ -18,15 +19,9 @@ fn main() { }; } -fn gen() { - let file = read_file(&DEMO_CODE).unwrap(); - let code = compile_file(&file); - let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string(); - checker.push_str(&code); - std::fs::write("tmp.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file -} - -const CHECKER_HVM: &str = include_str!("checker.hvm"); +// ------------------------------------------------------------ +// ------------------------------------------------------------ +// ------------------------------------------------------------ fn run_cli() -> Result<(), String> { let cli_matches = Cli::parse(); @@ -43,10 +38,15 @@ fn run_cli() -> Result<(), String> { } fn kind2(path: &str, main_function: &str) -> Result<(), String> { - let file = match std::fs::read_to_string(&path) { + let file = match std::fs::read_to_string(path) { Ok(code) => read_file(&code), - Err(msg) => read_file(&DEMO_CODE), + Err(msg) => { + println!("File not found: {}", path); + return Ok(()); + }, }; + + // Prints errors if parsing failed let file = match file { Ok(file) => file, Err(msg) => { @@ -55,559 +55,63 @@ fn kind2(path: &str, main_function: &str) -> Result<(), String> { } }; - let code = compile_file(&file); + // Adjusts the file + let file = adjust_file(&file); + //for (name, entry) in &file.entries { + //println!("[{}]\n{}\n", name, show_entry(entry)); + //} + + let code = compile_file(&file); let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string(); checker.push_str(&code); - std::fs::write(format!("{}.hvm", path), checker.clone()).ok(); // writes checker to the checker.hvm file + // Writes the checker file.kind2.hvm + std::fs::write(format!("{}.hvm", path), checker.clone()).ok(); + // Runs with the interpreter let mut rt = hvm::Runtime::from_code(&checker)?; let main = rt.alloc_code(main_function)?; rt.normalize(main); println!("{}", readback_string(&rt, main)); // TODO: optimize by deserializing term into text directly - eprintln!("Rewrites: {}", rt.get_rewrites()); + // Display stats + println!("Rewrites: {}", rt.get_rewrites()); Ok(()) } -#[derive(Clone, Debug)] -pub enum Term { - Typ, - Var { name: String }, - Let { name: String, expr: Box, body: Box }, - All { name: String, tipo: Box, body: Box }, - Lam { name: String, body: Box }, - App { func: Box, argm: Box }, - Ctr { name: String, args: Vec> }, - Fun { name: String, args: Vec> }, +fn debug_print_parser_state(txt: &str, state: &parser::State) { + println!("{} ||{}", txt, &state.code[state.index..state.index+32].replace("\n"," || ")); } -#[derive(Clone, Debug)] -pub struct Argument { - eras: bool, - name: String, - tipo: Box, -} - -#[derive(Clone, Debug)] -pub struct Rule { - name: String, - pats: Vec>, - body: Box, -} - -#[derive(Clone, Debug)] -pub struct Entry { - name: String, - args: Vec>, - tipo: Box, - rules: Vec> -} - -#[derive(Clone, Debug)] -pub struct File { - entries: HashMap> -} - -// Parser -// ====== - -pub fn parse_var(state: parser::State) -> parser::Answer>> { - parser::guard( - Box::new(|state| { - let (state, head) = parser::get_char(state)?; - Ok((state, ('a'..='z').contains(&head) || head == '_' || head == '$')) - }), - Box::new(|state| { - let (state, name) = parser::name(state)?; - Ok((state, Box::new(Term::Var { name }))) - }), - state, - ) -} - -pub fn parse_lam(state: parser::State) -> parser::Answer>> { - parser::guard( - parser::text_parser("@"), - Box::new(move |state| { - let (state, _) = parser::consume("@", state)?; - let (state, name) = parser::name(state)?; - let (state, body) = parse_term(state)?; - Ok((state, Box::new(Term::Lam { name, body }))) - }), - state, - ) -} - -pub fn parse_all(state: parser::State) -> parser::Answer>> { - parser::guard( - Box::new(|state| { - let (state, all0) = parser::text("(", state)?; - let (state, name) = parser::name(state)?; - let (state, all1) = parser::text(":", state)?; - Ok((state, all0 && all1 && name.len() > 0)) - }), - Box::new(|state| { - let (state, _) = parser::consume("(", state)?; - let (state, name) = parser::name(state)?; - let (state, _) = parser::consume(":", state)?; - let (state, tipo) = parse_term(state)?; - let (state, _) = parser::consume(")", state)?; - let (state, body) = parse_term(state)?; - Ok((state, Box::new(Term::All { name, tipo, body }))) - }), - state, - ) -} - -pub fn parse_app(state: parser::State) -> parser::Answer>> { - return parser::guard( - parser::text_parser("("), - Box::new(|state| { - parser::list( - parser::text_parser("("), - parser::text_parser(""), - parser::text_parser(")"), - Box::new(parse_term), - Box::new(|args| { - if !args.is_empty() { - args.into_iter().reduce(|a, b| Box::new(Term::App { func: a, argm: b })).unwrap() - } else { - Box::new(Term::Var { name: "?".to_string() }) - } - }), - state, - ) - }), - state, - ); -} - -pub fn parse_let(state: parser::State) -> parser::Answer>> { - return parser::guard( - parser::text_parser("let "), - Box::new(|state| { - let (state, _) = parser::consume("let ", state)?; - let (state, name) = parser::name1(state)?; - let (state, _) = parser::consume("=", state)?; - let (state, expr) = parse_term(state)?; - let (state, _) = parser::text(";", state)?; - let (state, body) = parse_term(state)?; - Ok((state, Box::new(Term::Let { name, expr, body }))) - }), - state, - ); -} - -pub fn parse_ctr(state: parser::State) -> parser::Answer>> { - parser::guard( - Box::new(|state| { - let (state, _) = parser::text("{", state)?; - let (state, head) = parser::get_char(state)?; - Ok((state, ('A'..='Z').contains(&head))) - }), - Box::new(|state| { - let (state, open) = parser::text("{", state)?; - let (state, name) = parser::name1(state)?; - if name == "Type" { - Ok((state, Box::new(Term::Typ))) - } else { - let (state, args) = if open { - parser::until(parser::text_parser("}"), Box::new(parse_term), state)? - } else { - (state, Vec::new()) - }; - Ok((state, Box::new(Term::Ctr { name, args }))) - } - }), - state, - ) -} - -pub fn parse_fun(state: parser::State) -> parser::Answer>> { - parser::guard( - Box::new(|state| { - let (state, _) = parser::text("(", state)?; - let (state, head) = parser::get_char(state)?; - Ok((state, ('A'..='Z').contains(&head))) - }), - Box::new(|state| { - let (state, open) = parser::text("(", state)?; - let (state, name) = parser::name1(state)?; - let (state, args) = if open { - parser::until(parser::text_parser(")"), Box::new(parse_term), state)? - } else { - (state, Vec::new()) - }; - Ok((state, Box::new(Term::Fun { name, args }))) - }), - state, - ) -} - -pub fn parse_term(state: parser::State) -> parser::Answer> { - parser::grammar( - "Term", - &[ - Box::new(parse_let), // `let ` - Box::new(parse_all), // `(name:` - Box::new(parse_ctr), // `{Name` - Box::new(parse_fun), // `(Name` - Box::new(parse_app), // `(` - Box::new(parse_lam), // `@` - Box::new(parse_var), // - Box::new(|state| Ok((state, None))), - ], - state, - ) -} - -pub fn parse_entry(state: parser::State) -> parser::Answer> { - let (state, name) = parser::name1(state)?; - let (state, args) = parser::until(parser::text_parser(":"), Box::new(parse_argument), state)?; - let (state, tipo) = parse_term(state)?; - let (state, head) = parser::peek_char(state)?; - if head == '=' { - let (state, _) = parser::consume("=", state)?; - let (state, body) = parse_term(state)?; - let mut pats = vec![]; - for arg in &args { - pats.push(Box::new(Term::Var { name: arg.name.clone() })); +fn gen_debug_file() { + let file = match read_file(&DEBUG_CODE) { + Ok(file) => file, + Err(msg) => { + println!("{}", msg); + return; } - let rules = vec![Box::new(Rule { name: name.clone(), pats, body })]; - return Ok((state, Box::new(Entry { name, args, tipo, rules }))); - } else if head == '{' { - let (state, _) = parser::consume("{", state)?; - let name_clone = name.clone(); - let (state, rules) = parser::until(parser::text_parser("}"), Box::new(move |state| parse_rule(state, name_clone.clone())), state)?; - return Ok((state, Box::new(Entry { name, args, tipo, rules }))); - } else { - return Ok((state, Box::new(Entry { name, args, tipo, rules: vec![] }))); - } + }; + let code = compile_file(&file); + let mut checker = (&CHECKER_HVM[0 .. CHECKER_HVM.find("////INJECT////").unwrap()]).to_string(); + checker.push_str(&code); + std::fs::write("debug.hvm", checker.clone()).ok(); // writes checker to the checker.hvm file } -pub fn parse_rule(state: parser::State, name: String) -> parser::Answer> { - let (state, _) = parser::consume(&name, state)?; - let (state, pats) = parser::until(parser::text_parser("="), Box::new(parse_term), state)?; - let (state, body) = parse_term(state)?; - return Ok((state, Box::new(Rule { name, pats, body }))); -} +const DEBUG_CODE: &str = " +Bool : Type +True : Bool +False : Bool -pub fn parse_argument(state: parser::State) -> parser::Answer> { - let (state, _) = parser::consume("(", state)?; - let (state, name) = parser::name1(state)?; - let (state, _) = parser::consume(":", state)?; - let (state, tipo) = parse_term(state)?; - let (state, _) = parser::consume(")", state)?; - return Ok((state, Box::new(Argument { eras: false, name, tipo }))); -} - -pub fn parse_file(state: parser::State) -> parser::Answer> { - let (state, entry_vec) = parser::until(Box::new(parser::done), Box::new(parse_entry), state)?; - let mut entries = HashMap::new(); - for entry in entry_vec { - entries.insert(entry.name.clone(), entry); - } - return Ok((state, Box::new(File { entries }))); -} - -pub fn show_term(term: &Term) -> String { - match term { - Term::Typ => { - format!("Type") - } - Term::Var { name } => { - format!("{}", name) - } - Term::Let { name, expr, body } => { - let expr = show_term(expr); - let body = show_term(body); - format!("let {} = {}; {}", name, expr, body) - } - Term::Lam { name, body } => { - let body = show_term(body); - format!("@{}({})", name, body) - } - Term::App { func, argm } => { - let mut args = vec![argm]; - let mut expr = func; - while let Term::App { func, argm } = &**expr { - args.push(argm); - expr = func; - } - args.reverse(); - format!("({} {})", show_term(expr), args.iter().map(|x| show_term(x)).collect::>().join(" ")) - } - Term::All { name, tipo, body } => { - let body = show_term(body); - format!("({}: {}) {}", name, show_term(tipo), body) - } - Term::Ctr { name, args } => { - format!("{{{}{}}}", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::()) - } - Term::Fun { name, args } => { - format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::()) - } - } -} - -pub fn show_rule(rule: &Rule) -> String { - let name = &rule.name; - let mut pats = vec![]; - for pat in &rule.pats { - pats.push(show_term(pat)); - } - let body = show_term(&rule.body); - format!("{} {} => {}", name, pats.join(" "), body) -} - -pub fn show_entry(entry: &Entry) -> String { - let name = &entry.name; - let mut args = vec![]; - for arg in &entry.args { - args.push(format!(" ({}: {})", arg.name, show_term(&arg.tipo))); - } - if entry.rules.len() == 0 { - format!("{}{} : {}", name, args.join(""), show_term(&entry.tipo)) - } else { - let mut rules = vec![]; - for rule in &entry.rules { - rules.push(format!("\n {}", show_rule(rule))); - } - format!("{}{} : {} {{{}\n}}", name, args.join(""), show_term(&entry.tipo), rules.join("")) - } -} - -pub fn show_file(file: &File) -> String { - let mut entries = vec![]; - for entry in file.entries.values() { - entries.push(show_entry(entry)); - } - entries.join("\n") -} - -pub fn read_term(code: &str) -> Result, String> { - parser::read(Box::new(parse_term), code) -} - -pub fn read_file(code: &str) -> Result, String> { - parser::read(Box::new(parse_file), code) -} - -// Compiler -// ======== - -//pub enum Term { - //Typ, - //Var { name: String }, - //Let { name: String, expr: Box, body: Box }, - //App { func: Box, argm: Box }, - //Lam { name: String, body: Box }, - //All { name: String, tipo: Box, body: Box }, - //Ctr { name: String, args: Vec> }, - //Fun { name: String, args: Vec> }, -//} -pub fn compile_term(term: &Term, quote: bool) -> String { - match term { - Term::Typ => { - format!("Typ") - } - Term::Var { name } => { - name.clone() - } - Term::Let { name, expr, body } => { - todo!() - } - Term::All { name, tipo, body } => { - format!("(All {} λ{} {})", compile_term(tipo, quote), name, compile_term(body, quote)) - } - Term::Lam { name, body } => { - format!("(Lam λ{} {})", name, compile_term(body, quote)) - } - Term::App { func, argm } => { - format!("({} {} {})", if quote { "App" } else { "Apply" }, compile_term(func, quote), compile_term(argm, quote)) - } - Term::Ctr { name, args } => { - let mut args_strs : Vec = Vec::new(); - for arg in args { - args_strs.push(format!(" {}", compile_term(arg, quote))); - } - format!("(Ct{} {}.{})", args.len(), name, args_strs.join("")) - } - Term::Fun { name, args } => { - let mut args_strs : Vec = Vec::new(); - for arg in args { - args_strs.push(format!(" {}", compile_term(arg, quote))); - } - format!("({}{} {}.{})", if quote { "NewFn" } else { "Rule_" }, args.len(), name, args_strs.join("")) - } - } -} - -pub fn compile_entry(entry: &Entry) -> String { - fn compile_type(args: &Vec>, tipo: &Box, index: usize) -> String { - if index < args.len() { - let arg = &args[index]; - format!("(All {} λ{} {})", compile_term(&arg.tipo, false), arg.name, compile_type(args, tipo, index + 1)) - } else { - compile_term(tipo, false) - } - } - - fn compile_rule(rule: &Rule) -> String { - let mut pats = vec![]; - for pat in &rule.pats { - pats.push(format!(" {}", compile_term(pat, false))); - } - let body_quot = compile_term(&rule.body, true); - let body_exec = compile_term(&rule.body, false); - let mut text = String::new(); - //text.push_str(&format!(" (Rule{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body)); - text.push_str(&format!(" (Body_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_quot)); - text.push_str(&format!(" (Rule_{} {}.{}) = {}\n", rule.pats.len(), rule.name, pats.join(""), body_exec)); - return text; - } - - fn compile_rule_chk(rule: &Rule, index: usize, vars: &mut u64, args: &mut Vec) -> String { - if index < rule.pats.len() { - let (inp_patt_str, var_patt_str) = compile_patt_chk(&rule.pats[index], vars); - args.push(var_patt_str); - let head = inp_patt_str; - let tail = compile_rule_chk(rule, index + 1, vars, args); - return format!("(LHS {} {})", head, tail); - } else { - return format!("(RHS (Body_{} {}.{}))", index, rule.name, args.iter().map(|x| format!(" {}", x)).collect::>().join("")); - } - } - - fn compile_patt_chk(patt: &Term, vars: &mut u64) -> (String, String) { - match patt { - Term::Var { .. } => { - let inp = format!("(Inp {})", vars); - let var = format!("(Var {})", vars); - *vars += 1; - return (inp, var); - } - Term::Ctr { name, args } => { - let mut inp_args_str = String::new(); - let mut var_args_str = String::new(); - for arg in args { - let (inp_arg_str, var_arg_str) = compile_patt_chk(arg, vars); - inp_args_str.push_str(&format!(" {}", inp_arg_str)); - var_args_str.push_str(&format!(" {}", var_arg_str)); - } - let inp_str = format!("(Ct{} {}.{})", args.len(), name, inp_args_str); - let var_str = format!("(Ct{} {}.{})", args.len(), name, var_args_str); - return (inp_str, var_str); - } - _ => { - panic!("Invalid left-hand side pattern: {}", show_term(patt)); - } - } - } - - let mut result = String::new(); - result.push_str(&format!(" (NameOf {}.) = \"{}\"\n", entry.name, entry.name)); - result.push_str(&format!(" (HashOf {}.) = %{}\n", entry.name, entry.name)); - result.push_str(&format!(" (TypeOf {}.) = {}\n", entry.name, compile_type(&entry.args, &entry.tipo, 0))); - for rule in &entry.rules { - result.push_str(&compile_rule(&rule)); - } - result.push_str(&format!(" (Verify {}.) =\n", entry.name)); - for rule in &entry.rules { - result.push_str(&format!(" (Cons {}\n", compile_rule_chk(&rule, 0, &mut 0, &mut vec![]))); - } - result.push_str(&format!(" Nil{}\n", ")".repeat(entry.rules.len()))); - return result; -} - -pub fn compile_file(file: &File) -> String { - let mut result = String::new(); - result.push_str(&format!("\n Functions =\n")); - result.push_str(&format!(" let fns = Nil\n")); - for entry in file.entries.values() { - result.push_str(&format!(" let fns = (Cons {}. fns)\n", entry. name)); - } - result.push_str(&format!(" fns\n\n")); - for entry in file.entries.values() { - result.push_str(&format!(" // {}\n", entry.name)); - result.push_str(&format!(" // {}\n", "-".repeat(entry.name.len()))); - result.push_str(&format!("\n")); - result.push_str(&compile_entry(&entry)); - result.push_str(&format!("\n")); - } - return result; -} - -fn readback_string(rt: &hvm::Runtime, host: u64) -> String { - let str_cons = rt.get_id("String.cons"); - let str_nil = rt.get_id("String.nil"); - let mut term = rt.ptr(host); - let mut text = String::new(); - //let str_cons = rt. - loop { - if hvm::get_tag(term) == hvm::CTR { - let fid = hvm::get_ext(term); - if fid == str_cons { - let head = rt.ptr(hvm::get_loc(term, 0)); - let tail = rt.ptr(hvm::get_loc(term, 1)); - if hvm::get_tag(head) == hvm::NUM { - text.push(std::char::from_u32(hvm::get_num(head) as u32).unwrap_or('?')); - term = tail; - continue; - } - } - if fid == str_nil { - break; - } - } - panic!("Invalid output: {} {}", hvm::get_tag(term), rt.show(host)); - } - return text; -} - -const DEMO_CODE: &str = " Nat : Type - Zero : Nat - Succ (pred: Nat) : Nat +Zero : Nat +Succ (pred: Nat) : Nat -The (x: Nat) : Type - Val (x: Nat) : {The x} +List (a: Type) : Type +Nil (a: Type) : (List a) +Cons (a: Type) (x: a) (xs: (List a)) : (List a) -Double (x: Nat) : Nat { - Double {Succ x} = {Succ {Succ (Double x)}} - Double {Zero} = {Zero} -} - -Pow2 (x: Nat) : Nat { - Pow2 {Succ x} = (Double (Pow2 x)) - Pow2 {Zero} = {Succ Zero} -} - -Destroy (x: Nat) : Nat { - Destroy {Succ n} = (Destroy n) - Destroy {Zero} = {Zero} -} - -SlowNumber : Nat = - (Destroy (Pow2 - {Succ {Succ {Succ {Succ - {Succ {Succ {Succ {Succ - {Succ {Succ {Succ {Succ - {Succ {Succ {Succ {Succ - {Succ {Succ {Succ {Succ - {Succ {Succ {Succ {Succ - Zero - }}}} - }}}} - }}}} - }}}} - }}}} - }}}} - )) - -// Proof that SlowNumber is 0 -Main : {The (SlowNumber)} = {Val Zero} +Not (a: Bool) : Bool +Not True = False ";