mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-15 18:20:26 +03:00
Initial commit
This commit is contained in:
Victor Maia
commit
469eb5976d
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
@ -0,0 +1 @@
|
||||
/target
|
||||
307
Cargo.lock
generated
Normal file
307
Cargo.lock
generated
Normal file
@ -0,0 +1,307 @@
|
||||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "aho-corasick"
|
||||
version = "0.7.18"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1e37cfd5e7657ada45f742d6e99ca5788580b5c529dc78faf11ece6dc702656f"
|
||||
dependencies = [
|
||||
"memchr",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "atty"
|
||||
version = "0.2.14"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa"
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "1.3.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
|
||||
|
||||
[[package]]
|
||||
name = "clap"
|
||||
version = "3.2.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "69c5a7f9997be616e47f0577ee38c91decb33392c5be4866494f34cdf329a9aa"
|
||||
dependencies = [
|
||||
"atty",
|
||||
"bitflags",
|
||||
"clap_derive",
|
||||
"clap_lex",
|
||||
"indexmap",
|
||||
"once_cell",
|
||||
"strsim",
|
||||
"termcolor",
|
||||
"textwrap",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_derive"
|
||||
version = "3.2.7"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "759bf187376e1afa7b85b959e6a664a3e7a95203415dba952ad19139e798f902"
|
||||
dependencies = [
|
||||
"heck",
|
||||
"proc-macro-error",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "clap_lex"
|
||||
version = "0.2.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2850f2f5a82cbf437dd5af4d49848fbdfc27c157c3d010345776f952765261c5"
|
||||
dependencies = [
|
||||
"os_str_bytes",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "either"
|
||||
version = "1.7.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3f107b87b6afc2a64fd13cac55fe06d6c8859f12d4b14cbcdd2c67d0976781be"
|
||||
|
||||
[[package]]
|
||||
name = "hashbrown"
|
||||
version = "0.12.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "607c8a29735385251a339424dd462993c0fed8fa09d378f259377df08c126022"
|
||||
|
||||
[[package]]
|
||||
name = "heck"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2540771e65fc8cb83cd6e8a237f70c319bd5c29f78ed1084ba5d50eeac86f7f9"
|
||||
|
||||
[[package]]
|
||||
name = "hermit-abi"
|
||||
version = "0.1.19"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33"
|
||||
dependencies = [
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "hvm"
|
||||
version = "0.1.31"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "361a02d7ed07086c16927712c1bf610e54c3a43bd5d78deab7708f56c33ee5fb"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"itertools",
|
||||
"num_cpus",
|
||||
"regex",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "indexmap"
|
||||
version = "1.9.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "10a35a97730320ffe8e2d410b5d3b69279b98d2c14bdb8b70ea89ecf7888d41e"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"hashbrown",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
version = "0.10.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a9a9d19fa1e79b6215ff29b9d6880b706147f16e9b1dbb1e4e5947b5b02bc5e3"
|
||||
dependencies = [
|
||||
"either",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind2-rs"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"hvm",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.126"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "349d5a591cd28b49e1d1037471617a32ddcda5731b99419008085f72d5a53836"
|
||||
|
||||
[[package]]
|
||||
name = "memchr"
|
||||
version = "2.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
|
||||
|
||||
[[package]]
|
||||
name = "num_cpus"
|
||||
version = "1.13.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "19e64526ebdee182341572e50e9ad03965aa510cd94427a4549448f285e957a1"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "once_cell"
|
||||
version = "1.13.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "18a6dbe30758c9f83eb00cbea4ac95966305f5a7772f3f42ebfc7fc7eddbd8e1"
|
||||
|
||||
[[package]]
|
||||
name = "os_str_bytes"
|
||||
version = "6.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "21326818e99cfe6ce1e524c2a805c189a99b5ae555a35d19f9a284b427d86afa"
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro-error"
|
||||
version = "1.0.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c"
|
||||
dependencies = [
|
||||
"proc-macro-error-attr",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"syn",
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro-error-attr"
|
||||
version = "1.0.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"version_check",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.40"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "dd96a1e8ed2596c337f8eae5f24924ec83f5ad5ab21ea8e455d3566c69fbcaf7"
|
||||
dependencies = [
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "quote"
|
||||
version = "1.0.20"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3bcdf212e9776fbcb2d23ab029360416bb1706b1aea2d1a5ba002727cbcab804"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex"
|
||||
version = "1.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4c4eb3267174b8c6c2f654116623910a0fef09c4753f8dd83db29c48a0df988b"
|
||||
dependencies = [
|
||||
"aho-corasick",
|
||||
"memchr",
|
||||
"regex-syntax",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex-syntax"
|
||||
version = "0.6.27"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a3f87b73ce11b1619a3c6332f45341e0047173771e8b8b73f87bfeefb7b56244"
|
||||
|
||||
[[package]]
|
||||
name = "strsim"
|
||||
version = "0.10.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "1.0.98"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c50aef8a904de4c23c788f104b7dddc7d6f79c647c7c8ce4cc8f73eb0ca773dd"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "termcolor"
|
||||
version = "1.1.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "bab24d30b911b2376f3a13cc2cd443142f0c81dda04c118693e35b3835757755"
|
||||
dependencies = [
|
||||
"winapi-util",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "textwrap"
|
||||
version = "0.15.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b1141d4d61095b28419e22cb0bbf02755f5e54e0526f97f1e3d1d160e60885fb"
|
||||
|
||||
[[package]]
|
||||
name = "unicode-ident"
|
||||
version = "1.0.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5bd2fe26506023ed7b5e1e315add59d6f584c621d037f9368fea9cfb988f368c"
|
||||
|
||||
[[package]]
|
||||
name = "version_check"
|
||||
version = "0.9.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f"
|
||||
|
||||
[[package]]
|
||||
name = "winapi"
|
||||
version = "0.3.9"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
|
||||
dependencies = [
|
||||
"winapi-i686-pc-windows-gnu",
|
||||
"winapi-x86_64-pc-windows-gnu",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi-i686-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
|
||||
|
||||
[[package]]
|
||||
name = "winapi-util"
|
||||
version = "0.1.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178"
|
||||
dependencies = [
|
||||
"winapi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "winapi-x86_64-pc-windows-gnu"
|
||||
version = "0.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
|
||||
9
Cargo.toml
Normal file
9
Cargo.toml
Normal file
@ -0,0 +1,9 @@
|
||||
[package]
|
||||
name = "kind2-rs"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
hvm = "0.1.31"
|
||||
417
src/main.rs
Normal file
417
src/main.rs
Normal file
@ -0,0 +1,417 @@
|
||||
#![allow(dead_code)]
|
||||
#![allow(unused_variables)]
|
||||
|
||||
// imports hashmap
|
||||
use std::collections::HashMap;
|
||||
|
||||
// type Bool {
|
||||
// {True}
|
||||
// {False}
|
||||
// }
|
||||
//
|
||||
// type List <T: Type> {
|
||||
// {Nil}
|
||||
// {Cons T (List <T>)}
|
||||
// }
|
||||
//
|
||||
// type Equal <T: Type> (a: T) ~ (b: T) {
|
||||
// {Refl} ~ (b = a)
|
||||
// }
|
||||
//
|
||||
// Add (a: Nat) (b: Nat) : Nat {
|
||||
// {Zero} b => b
|
||||
// {Succ a} b => {Succ (Add a b)}
|
||||
// }
|
||||
//
|
||||
// Add (a: Nat) (b: Nat) : Nat =
|
||||
// match a {
|
||||
// {Zero} => b
|
||||
// {Succ a} => {Succ (Add a b)}
|
||||
// }
|
||||
//
|
||||
// Map <A: Type> <B: Type> (f: A -> B) (xs: List A) : List B {
|
||||
// A B f {Cons x xs} => {Cons (f x) (map A B f xs)}
|
||||
// A B f {Nil} => {Nil}
|
||||
// }
|
||||
//
|
||||
// Main : (List Nat) =
|
||||
// let x = 50
|
||||
// let y = 60
|
||||
// if (== x y) {
|
||||
// (print "hi")
|
||||
// } else {
|
||||
// (print "bye")
|
||||
// }
|
||||
//
|
||||
// alice : Person =
|
||||
// {Person
|
||||
// age: 40
|
||||
// name: "Alice"
|
||||
// items: ["Foo", "Bar", "Tic", "Tac"]
|
||||
// }
|
||||
//
|
||||
// {Cons x xs}
|
||||
// {Cons head: x tail: xs }
|
||||
|
||||
use hvm::parser as parser;
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Term {
|
||||
Typ,
|
||||
Var { name: String },
|
||||
Let { name: String, expr: Box<Term>, body: Box<Term> },
|
||||
App { func: Box<Term>, argm: Box<Term> },
|
||||
Lam { name: String, body: Box<Term> },
|
||||
All { name: String, tipo: Box<Term>, body: Box<Term> },
|
||||
Ctr { name: String, args: Vec<Box<Term>> },
|
||||
Fun { name: String, args: Vec<Box<Term>> },
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Argument {
|
||||
eras: bool,
|
||||
name: String,
|
||||
tipo: Box<Term>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Rule {
|
||||
pats: Vec<Box<Term>>,
|
||||
body: Box<Term>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Entry {
|
||||
name: String,
|
||||
args: Vec<Box<Argument>>,
|
||||
tipo: Box<Term>,
|
||||
rules: Vec<Box<Rule>>
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct File {
|
||||
entries: HashMap<String, Box<Entry>>
|
||||
}
|
||||
|
||||
pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
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<Option<Box<Term>>> {
|
||||
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<Option<Box<Term>>> {
|
||||
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<Option<Box<Term>>> {
|
||||
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<Option<Box<Term>>> {
|
||||
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<Option<Box<Term>>> {
|
||||
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<Option<Box<Term>>> {
|
||||
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<Box<Term>> {
|
||||
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<Box<Entry>> {
|
||||
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::get_char(state)?;
|
||||
if head == '=' {
|
||||
let (state, body) = parse_term(state)?;
|
||||
let rules = vec![Box::new(Rule { pats: vec![], body })];
|
||||
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
|
||||
} else if head == '{' {
|
||||
let (state, rules) = parser::until(parser::text_parser("}"), Box::new(parse_rule), state)?;
|
||||
return Ok((state, Box::new(Entry { name, args, tipo, rules })));
|
||||
} else {
|
||||
parser::expected("'=' or '{'", 1, state)
|
||||
}
|
||||
}
|
||||
|
||||
pub fn parse_rule(state: parser::State) -> parser::Answer<Box<Rule>> {
|
||||
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 { pats, body })));
|
||||
}
|
||||
|
||||
pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
|
||||
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<Box<File>> {
|
||||
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::<Vec<String>>().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::<String>())
|
||||
}
|
||||
Term::Fun { name, args } => {
|
||||
format!("({}{})", name, args.iter().map(|x| format!(" {}",show_term(x))).collect::<String>())
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub fn show_rule(rule: &Rule) -> String {
|
||||
let mut pats = vec![];
|
||||
for pat in &rule.pats {
|
||||
pats.push(show_term(pat));
|
||||
}
|
||||
let body = show_term(&rule.body);
|
||||
format!("{} => {}", 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)));
|
||||
}
|
||||
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<Box<Term>, String> {
|
||||
parser::read(Box::new(parse_term), code)
|
||||
}
|
||||
|
||||
pub fn read_file(code: &str) -> Result<Box<File>, String> {
|
||||
parser::read(Box::new(parse_file), code)
|
||||
}
|
||||
|
||||
fn main() -> Result<(), String> {
|
||||
|
||||
//let term = read_term("{Foo @x(x) {Tic} {Tac}}")?;
|
||||
//println!("Parsed: {}", show_term(&*term));
|
||||
|
||||
let file = read_file("
|
||||
Bool : Type {}
|
||||
True : Bool {}
|
||||
False : Bool {}
|
||||
|
||||
Add (a: Nat) (b: Nat) : Nat {
|
||||
{Zero} b => b
|
||||
{Succ a} b => {Succ (Add a b)}
|
||||
}
|
||||
|
||||
Not (a: Bool) : Bool {
|
||||
{True} => {False}
|
||||
{False} => {True}
|
||||
}
|
||||
|
||||
Map (a: Type) (b: Type) (f: (x: a) a) (xs: (List a)) : (List b) {
|
||||
a b f {Cons x xs} => {Cons (f x) (Map a b f xs)}
|
||||
a b f Nil => {Nil}
|
||||
}
|
||||
")?;
|
||||
|
||||
println!("parsed:\n\n{}", show_file(&file));
|
||||
|
||||
return Ok(());
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
//Map (a: {Type}) (b: {Type}) (f: (x: a) a) (xs: ({List} a)) : ({List} b) {
|
||||
//a b f {Cons x xs} => {Cons (f x) ({Map} a b f xs)}
|
||||
//a b f {Nil} => {Nil}
|
||||
//}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user