mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-16 10:40:42 +03:00
feat: add basic specialize function
This commit is contained in:
Gabrielle Guimarães de Oliveira
parent
3809f7217d
commit
d46739a9a5
254
Cargo.lock
generated
254
Cargo.lock
generated
@ -2,12 +2,111 @@
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "aho-corasick"
|
||||
version = "0.7.20"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "cc936419f96fa211c1b9166887b38e5e40b19958e5b895be7c1f93adec7071ac"
|
||||
dependencies = [
|
||||
"memchr",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "ariadne"
|
||||
version = "0.2.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "367fd0ad87307588d087544707bc5fbf4805ded96c7db922b70d368fa1cb5702"
|
||||
dependencies = [
|
||||
"concolor",
|
||||
"unicode-width",
|
||||
"yansi",
|
||||
]
|
||||
|
||||
[[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 = "cc"
|
||||
version = "1.0.79"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f"
|
||||
|
||||
[[package]]
|
||||
name = "concolor"
|
||||
version = "0.0.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "318d6c16e73b3a900eb212ad6a82fc7d298c5ab8184c7a9998646455bc474a16"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"concolor-query",
|
||||
"is-terminal",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "concolor-query"
|
||||
version = "0.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "82a90734b3d5dcf656e7624cca6bce9c3a90ee11f900e80141a7427ccfb3d317"
|
||||
|
||||
[[package]]
|
||||
name = "errno"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a"
|
||||
dependencies = [
|
||||
"errno-dragonfly",
|
||||
"libc",
|
||||
"windows-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "errno-dragonfly"
|
||||
version = "0.1.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "aa68f1b12764fab894d2755d2518754e71b4fd80ecfb822714a1206c2aab39bf"
|
||||
dependencies = [
|
||||
"cc",
|
||||
"libc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "hermit-abi"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "fed44880c466736ef9a5c5b5facefb5ed0785676d0c02d612db14e54f0d84286"
|
||||
|
||||
[[package]]
|
||||
name = "io-lifetimes"
|
||||
version = "1.0.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9c66c74d2ae7e79a5a8f7ac924adbe38ee42a859c6539ad869eb51f0b52dc220"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"libc",
|
||||
"windows-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "is-terminal"
|
||||
version = "0.4.7"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "adcf93614601c8129ddf72e2d5633df827ba6551541c6d8c59520a371475be1f"
|
||||
dependencies = [
|
||||
"hermit-abi",
|
||||
"io-lifetimes",
|
||||
"rustix",
|
||||
"windows-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind-cli"
|
||||
version = "0.1.3"
|
||||
@ -19,6 +118,13 @@ dependencies = [
|
||||
[[package]]
|
||||
name = "kind-fmt"
|
||||
version = "0.1.3"
|
||||
dependencies = [
|
||||
"ariadne",
|
||||
"kind-syntax",
|
||||
"thin-vec",
|
||||
"tree-sitter",
|
||||
"tree-sitter-kind",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind-syntax"
|
||||
@ -26,8 +132,27 @@ version = "0.1.3"
|
||||
dependencies = [
|
||||
"num-bigint",
|
||||
"thin-vec",
|
||||
"tree-sitter",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.141"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "3304a64d199bb964be99741b7a14d26972741915b3649639149b2479bb46f4b5"
|
||||
|
||||
[[package]]
|
||||
name = "linux-raw-sys"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d59d8c75012853d2e872fb56bc8a2e53718e2cafe1a4c823143141c6d90c322f"
|
||||
|
||||
[[package]]
|
||||
name = "memchr"
|
||||
version = "2.5.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d"
|
||||
|
||||
[[package]]
|
||||
name = "num-bigint"
|
||||
version = "0.4.3"
|
||||
@ -58,8 +183,137 @@ dependencies = [
|
||||
"autocfg",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex"
|
||||
version = "1.7.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8b1f693b24f6ac912f4893ef08244d70b6067480d2f1a46e950c9691e6749d1d"
|
||||
dependencies = [
|
||||
"aho-corasick",
|
||||
"memchr",
|
||||
"regex-syntax",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex-syntax"
|
||||
version = "0.6.29"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f162c6dd7b008981e4d40210aca20b4bd0f9b60ca9271061b07f78537722f2e1"
|
||||
|
||||
[[package]]
|
||||
name = "rustix"
|
||||
version = "0.37.11"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "85597d61f83914ddeba6a47b3b8ffe7365107221c2e557ed94426489fefb5f77"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"errno",
|
||||
"io-lifetimes",
|
||||
"libc",
|
||||
"linux-raw-sys",
|
||||
"windows-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "thin-vec"
|
||||
version = "0.2.12"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "aac81b6fd6beb5884b0cf3321b8117e6e5d47ecb6fc89f414cfdcca8b2fe2dd8"
|
||||
|
||||
[[package]]
|
||||
name = "tree-sitter"
|
||||
version = "0.20.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e747b1f9b7b931ed39a548c1fae149101497de3c1fc8d9e18c62c1a66c683d3d"
|
||||
dependencies = [
|
||||
"cc",
|
||||
"regex",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "tree-sitter-kind"
|
||||
version = "0.0.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a8e5976c200f9600e09c479038477e73b839ce56f621d2213d406afc848180e9"
|
||||
dependencies = [
|
||||
"cc",
|
||||
"tree-sitter",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "unicode-width"
|
||||
version = "0.1.10"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b"
|
||||
|
||||
[[package]]
|
||||
name = "windows-sys"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9"
|
||||
dependencies = [
|
||||
"windows-targets",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "windows-targets"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7b1eb6f0cd7c80c79759c929114ef071b87354ce476d9d94271031c0497adfd5"
|
||||
dependencies = [
|
||||
"windows_aarch64_gnullvm",
|
||||
"windows_aarch64_msvc",
|
||||
"windows_i686_gnu",
|
||||
"windows_i686_msvc",
|
||||
"windows_x86_64_gnu",
|
||||
"windows_x86_64_gnullvm",
|
||||
"windows_x86_64_msvc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_gnullvm"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "91ae572e1b79dba883e0d315474df7305d12f569b400fcf90581b06062f7e1bc"
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_msvc"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b2ef27e0d7bdfcfc7b868b317c1d32c641a6fe4629c171b8928c7b08d98d7cf3"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_gnu"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "622a1962a7db830d6fd0a69683c80a18fda201879f0f447f065a3b7467daa241"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_msvc"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4542c6e364ce21bf45d69fdd2a8e455fa38d316158cfd43b3ac1c5b1b19f8e00"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnu"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ca2b8a661f7628cbd23440e50b05d705db3686f894fc9580820623656af974b1"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnullvm"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7896dbc1f41e08872e9d5e8f8baa8fdd2677f29468c4e156210174edc7f7b953"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_msvc"
|
||||
version = "0.48.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a"
|
||||
|
||||
[[package]]
|
||||
name = "yansi"
|
||||
version = "0.5.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "09041cd90cf85f7f8b2df60c646f853b7f535ce68f85244eb6731cf89fa498ec"
|
||||
|
||||
@ -6,3 +6,8 @@ version = "0.1.3"
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
thin-vec = "0.2.12"
|
||||
ariadne = {version = "0.2.0", features = ["auto-color"]}
|
||||
kind-syntax = {path = "../kind-syntax", version = "0.1.3"}
|
||||
tree-sitter = "0.20.10"
|
||||
tree-sitter-kind = "0.0.1"
|
||||
|
||||
@ -1,3 +1,183 @@
|
||||
fn fmt() {
|
||||
println!("Hello, world!");
|
||||
use std::path::PathBuf;
|
||||
|
||||
use thin_vec::{thin_vec, ThinVec};
|
||||
use tree_sitter::{Parser, Tree, TreeCursor};
|
||||
|
||||
use kind_syntax::concrete::{Block, ConstructorExpr, Expr, ExprKind, LocalExpr, Module, Pat, PatKind, Rule, Signature, Stmt, TopLevel, TopLevelKind};
|
||||
use kind_syntax::lexemes::{Brace, Colon, Equal, Ident, Item, Name, Span, Token, Tokenized};
|
||||
|
||||
#[derive(Debug)]
|
||||
pub enum FmtError {
|
||||
IoError(std::io::Error),
|
||||
TreeSitterLanguageError(tree_sitter::LanguageError),
|
||||
TreeSitterQueryError(tree_sitter::QueryError),
|
||||
UnknownParseError,
|
||||
}
|
||||
|
||||
pub type Result<T> = std::result::Result<T, FmtError>;
|
||||
|
||||
pub fn run_fmt(string: String) -> Result<Module> {
|
||||
let mut parser = Parser::new();
|
||||
parser
|
||||
.set_language(tree_sitter_kind::language())
|
||||
.map_err(FmtError::TreeSitterLanguageError)?;
|
||||
let tree = parser
|
||||
.parse(string.as_bytes(), None)
|
||||
.ok_or(FmtError::UnknownParseError)?;
|
||||
|
||||
println!("{:?}", tree.root_node().to_sexp());
|
||||
|
||||
let mut cursor = tree.root_node().walk();
|
||||
|
||||
let declarations = tree.root_node().children(&mut cursor)
|
||||
.map(|node| {
|
||||
specialize_top_level(&string, &tree, &mut node.walk())
|
||||
})
|
||||
.collect::<Result<ThinVec<_>>>()?;
|
||||
|
||||
Ok(Module {
|
||||
shebang: None,
|
||||
items: declarations,
|
||||
eof: Token::default(),
|
||||
})
|
||||
}
|
||||
|
||||
fn specialize_top_level(file: &String, tree: &Tree, cursor: &mut TreeCursor) -> Result<TopLevel> {
|
||||
let node = cursor.node();
|
||||
match node.kind() {
|
||||
"val_declaration" => {
|
||||
let name = node.child_by_field_name("name").unwrap();
|
||||
let return_type = node.child_by_field_name("return_type");
|
||||
let value = node.child_by_field_name("value");
|
||||
|
||||
Ok(TopLevel {
|
||||
data: Item::new(
|
||||
Span::default(),
|
||||
TopLevelKind::Signature(Signature {
|
||||
name: specialize_name(file, tree, &mut name.walk())?,
|
||||
arguments: thin_vec![],
|
||||
return_type: return_type.map_or(Ok(None), |node| {
|
||||
let expr = specialize_expr(file, tree, &mut node.walk())?;
|
||||
Ok(Some(Colon(Token::default(), expr)))
|
||||
})?,
|
||||
value: value.map_or(Ok(None), |node| {
|
||||
let block = specialize_statements(file, tree, &mut node.walk())?;
|
||||
Ok(Some(block))
|
||||
})?,
|
||||
}),
|
||||
),
|
||||
attributes: thin_vec![],
|
||||
})
|
||||
}
|
||||
_ => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
fn specialize_pattern(file: &String, tree: &Tree, cursor: &mut TreeCursor) -> Result<Pat> {
|
||||
let node = cursor.node();
|
||||
match node.kind() {
|
||||
"identifier" => {
|
||||
specialize_name(file, tree, cursor)
|
||||
.map(|name| Pat::new(
|
||||
Span::default(),
|
||||
PatKind::Name(name),
|
||||
))
|
||||
}
|
||||
"constructor_identifier" => {
|
||||
specialize_name(file, tree, cursor)
|
||||
.map(|name| Pat::new(
|
||||
Span::default(),
|
||||
PatKind::Name(name),
|
||||
))
|
||||
}
|
||||
kind => todo!("{}", kind),
|
||||
}
|
||||
}
|
||||
|
||||
fn specialize_expr(file: &String, tree: &Tree, cursor: &mut TreeCursor) -> Result<Expr> {
|
||||
let node = cursor.node();
|
||||
match node.kind() {
|
||||
"call" => {
|
||||
let callee = node
|
||||
.child_by_field_name("callee")
|
||||
.unwrap();
|
||||
|
||||
specialize_primary(file, tree, &mut callee.walk())
|
||||
},
|
||||
kind => todo!("{}", kind),
|
||||
}
|
||||
}
|
||||
|
||||
fn specialize_name(file: &String, _tree: &Tree, cursor: &mut TreeCursor) -> Result<Name> {
|
||||
let node = cursor.node();
|
||||
match node.kind() {
|
||||
"identifier" => {
|
||||
let name = node.utf8_text(file.as_bytes()).unwrap().to_string();
|
||||
|
||||
Ok(Name::Ident(Ident(Item::new(
|
||||
Span::default(),
|
||||
Tokenized(Token::default(), name),
|
||||
))))
|
||||
}
|
||||
kind => todo!("{}", kind),
|
||||
}
|
||||
}
|
||||
|
||||
fn specialize_statements(file: &String, tree: &Tree, cursor: &mut TreeCursor) -> Result<Block> {
|
||||
let node = cursor.node();
|
||||
match node.kind() {
|
||||
"statements" => {
|
||||
let statements = node.named_children(cursor)
|
||||
.map(|node| {
|
||||
specialize_expr(file, tree, &mut node.walk())
|
||||
})
|
||||
.collect::<Result<ThinVec<_>>>()?;
|
||||
|
||||
Ok(Brace(
|
||||
Token::default(),
|
||||
statements.iter().map(|expr| Stmt {
|
||||
value: expr.clone(),
|
||||
semi: None,
|
||||
}).collect(),
|
||||
Token::default(),
|
||||
))
|
||||
}
|
||||
kind => todo!("{}", kind),
|
||||
}
|
||||
}
|
||||
|
||||
fn specialize_primary(file: &String, tree: &Tree, cursor: &mut TreeCursor) -> Result<Expr> {
|
||||
let node = cursor.node();
|
||||
match node.kind() {
|
||||
"constructor_identifier" => {
|
||||
specialize_name(file, tree, cursor)
|
||||
.map(|name| Expr::new(
|
||||
Span::default(),
|
||||
ExprKind::Constructor(Box::new(ConstructorExpr {
|
||||
name,
|
||||
})),
|
||||
))
|
||||
}
|
||||
"identifier" => {
|
||||
specialize_name(file, tree, cursor)
|
||||
.map(|name| Expr::new(
|
||||
Span::default(),
|
||||
ExprKind::Local(Box::new(LocalExpr {
|
||||
name,
|
||||
})),
|
||||
))
|
||||
}
|
||||
_ => todo!(),
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
|
||||
#[test]
|
||||
fn it_works() {
|
||||
let expr = run_fmt("bao:pao{a}".into()).unwrap();
|
||||
println!("{:#?}", expr);
|
||||
}
|
||||
}
|
||||
|
||||
@ -9,3 +9,5 @@ version = "0.1.3"
|
||||
[dependencies]
|
||||
num-bigint = "0.4.3"
|
||||
thin-vec = "0.2.12"
|
||||
tree-sitter = "0.20.10"
|
||||
|
||||
|
||||
@ -7,12 +7,9 @@ use num_bigint::BigUint;
|
||||
use thin_vec::ThinVec;
|
||||
|
||||
use crate::lexemes;
|
||||
use crate::lexemes::{
|
||||
AngleBracket, Brace, Bracket, Colon, Either, Equal, Ident, Item, Paren, QualifiedIdent, Token,
|
||||
Tokenized,
|
||||
};
|
||||
use crate::lexemes::{AngleBracket, Brace, Bracket, Colon, Either, Equal, Ident, Item, Name, Paren, QualifiedIdent, Token, Tokenized};
|
||||
|
||||
#[derive(Debug)]
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum AttributeStyleKind {
|
||||
String(Tokenized<String>),
|
||||
Number(Tokenized<u64>),
|
||||
@ -30,7 +27,7 @@ pub enum AttributeStyleKind {
|
||||
///
|
||||
pub type AttributeStyle = Item<AttributeStyleKind>;
|
||||
|
||||
#[derive(Debug)]
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct AttributeKind {
|
||||
pub r#hash: lexemes::Hash,
|
||||
pub name: Ident,
|
||||
@ -42,14 +39,20 @@ pub struct AttributeKind {
|
||||
pub type Attribute = Item<AttributeKind>;
|
||||
|
||||
/// A type binding is a type annotation for a variable.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct TypeBinding {
|
||||
pub name: Ident,
|
||||
pub typ: Colon<Box<Expr>>,
|
||||
}
|
||||
|
||||
pub type ArgumentBinding = Either<AngleBracket<Param>, Paren<Param>>;
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum ArgumentBinding {
|
||||
Implicit(AngleBracket<Param>),
|
||||
Explicit(Paren<Param>),
|
||||
}
|
||||
|
||||
/// An argument of a type signature.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Argument {
|
||||
pub minus: Option<lexemes::Minus>,
|
||||
pub plus: Option<lexemes::Plus>,
|
||||
@ -58,14 +61,16 @@ pub struct Argument {
|
||||
|
||||
/// A local expression is a reference atom to a local declaration.
|
||||
/// * Always starts with a lower case letter.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct LocalExpr {
|
||||
pub name: Ident,
|
||||
pub name: Name,
|
||||
}
|
||||
|
||||
/// A constructor expression is a reference atom to a top level declaration.
|
||||
/// * Always starts with an upper case letter.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct ConstructorExpr {
|
||||
pub name: QualifiedIdent,
|
||||
pub name: Name,
|
||||
}
|
||||
|
||||
/// A param is a variable or a type binding.
|
||||
@ -75,12 +80,14 @@ pub struct ConstructorExpr {
|
||||
/// // or
|
||||
/// x
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum Param {
|
||||
Named(Paren<TypeBinding>),
|
||||
Expr(Box<Expr>),
|
||||
}
|
||||
|
||||
/// A all node is a dependent function type.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct PiExpr {
|
||||
pub r#tilde: lexemes::Tilde,
|
||||
pub param: Param,
|
||||
@ -91,6 +98,7 @@ pub struct PiExpr {
|
||||
/// A sigma node is a dependent pair type. It express
|
||||
/// the dependency of the type of the second element
|
||||
/// of the pair on the first one.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct SigmaExpr {
|
||||
pub param: Bracket<TypeBinding>,
|
||||
pub r#arrow: lexemes::RightArrow,
|
||||
@ -98,6 +106,7 @@ pub struct SigmaExpr {
|
||||
}
|
||||
|
||||
/// A lambda expression (an anonymous function).
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct LambdaExpr {
|
||||
pub r#tilde: Option<lexemes::Tilde>,
|
||||
pub param: Param,
|
||||
@ -105,34 +114,30 @@ pub struct LambdaExpr {
|
||||
pub body: Box<Expr>,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Rename(pub Ident, pub Equal<Box<Expr>>);
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum NamedBinding {
|
||||
Named(Paren<Rename>),
|
||||
Expr(Box<Expr>),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Binding {
|
||||
pub r#tilde: Option<lexemes::Tilde>,
|
||||
pub value: NamedBinding,
|
||||
}
|
||||
|
||||
/// Application of a function to a sequence of arguments.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct AppExpr {
|
||||
pub fun: Box<Expr>,
|
||||
pub arg: ThinVec<Binding>,
|
||||
}
|
||||
|
||||
/// Let binding expression.
|
||||
pub struct LetExpr {
|
||||
pub r#let: lexemes::Let,
|
||||
pub name: Ident,
|
||||
pub value: Equal<Box<Expr>>,
|
||||
pub r#semi: Option<lexemes::Semi>,
|
||||
pub next: Box<Expr>,
|
||||
}
|
||||
|
||||
/// A type annotation.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct AnnExpr {
|
||||
pub value: Box<Expr>,
|
||||
pub r#colon: lexemes::ColonColon,
|
||||
@ -140,6 +145,7 @@ pub struct AnnExpr {
|
||||
}
|
||||
|
||||
/// A literal is a constant value that can be used in the program.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum Literal {
|
||||
U60(Tokenized<u64>),
|
||||
F60(Tokenized<f64>),
|
||||
@ -150,6 +156,7 @@ pub enum Literal {
|
||||
}
|
||||
|
||||
// TODO: Rename
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum TypeExpr {
|
||||
Help(Tokenized<String>),
|
||||
Type(lexemes::Type),
|
||||
@ -158,6 +165,7 @@ pub enum TypeExpr {
|
||||
TypeF60(Token),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum Operation {
|
||||
Add,
|
||||
Sub,
|
||||
@ -179,73 +187,46 @@ pub enum Operation {
|
||||
}
|
||||
|
||||
/// A binary operation.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct BinaryExpr {
|
||||
pub left: Box<Expr>,
|
||||
pub op: Tokenized<Operation>,
|
||||
pub right: Box<Expr>,
|
||||
}
|
||||
|
||||
/// Monadic binding without a variable name.
|
||||
pub struct NextStmt {
|
||||
pub left: Box<Expr>,
|
||||
pub r#semi: Option<lexemes::Semi>,
|
||||
pub next: Box<Stmt>,
|
||||
}
|
||||
|
||||
/// An ask statement is a monadic binding inside the `do` notation
|
||||
/// with a name.
|
||||
pub struct AskStmt {
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct AskExpr {
|
||||
pub r#ask: lexemes::Ask,
|
||||
pub name: Ident,
|
||||
pub value: Equal<Box<Expr>>,
|
||||
pub next: Box<Stmt>,
|
||||
}
|
||||
|
||||
/// A let binding inside the `do` notation.
|
||||
pub struct LetStmt {
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct LetExpr {
|
||||
pub r#let: lexemes::Let,
|
||||
pub name: Ident,
|
||||
pub value: Equal<Box<Expr>>,
|
||||
pub next: Box<Stmt>,
|
||||
pub r#semi: Option<lexemes::Semi>,
|
||||
pub next: Box<Expr>,
|
||||
}
|
||||
|
||||
/// The "pure" function of the `A` monad.
|
||||
pub struct ReturnStmt {
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct ReturnExpr {
|
||||
pub r#return: lexemes::Return,
|
||||
pub value: Box<Expr>,
|
||||
}
|
||||
|
||||
/// An expression without the "pure" function.
|
||||
pub struct ReturnExprStmt {
|
||||
pub value: Box<Expr>,
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Stmt {
|
||||
pub value: Expr,
|
||||
pub r#semi: Option<lexemes::Semi>,
|
||||
}
|
||||
|
||||
/// An statement is a "single line" of code inside the
|
||||
/// do notation. It can be either an expression, a let
|
||||
/// binding, a return statement or a return expression.
|
||||
/// i.e.
|
||||
///
|
||||
/// ```kind
|
||||
/// do A {
|
||||
/// ask a = 2 // Monadic binding of the `A` monad
|
||||
/// let a = 2 // A simple let expression
|
||||
/// return a + 2 // The "pure" functoin of the `A` monad
|
||||
/// }
|
||||
/// ```
|
||||
pub enum StmtKind {
|
||||
/// Monadic binding without a variable name.
|
||||
Next(NextStmt),
|
||||
/// Monadic binding with a variable name.
|
||||
Ask(AskStmt),
|
||||
/// A simple let expression.
|
||||
Let(LetStmt),
|
||||
/// The "pure" function of the `A` monad.
|
||||
Return(ReturnStmt),
|
||||
/// An expression without the "pure" function.
|
||||
ReturnExpr(ReturnExprStmt),
|
||||
}
|
||||
|
||||
pub type Stmt = Item<StmtKind>;
|
||||
pub type Block = Brace<ThinVec<Stmt>>;
|
||||
|
||||
/// A DoNode is similar to the haskell do notation.
|
||||
/// i.e.
|
||||
@ -257,13 +238,15 @@ pub type Stmt = Item<StmtKind>;
|
||||
/// return a + b;
|
||||
/// }
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct DoNode {
|
||||
pub r#do: lexemes::Do,
|
||||
pub typ: Option<Ident>,
|
||||
pub value: Brace<Stmt>,
|
||||
pub value: Block,
|
||||
}
|
||||
|
||||
/// Conditional expression.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct IfExpr {
|
||||
pub cond: Tokenized<Box<Expr>>,
|
||||
pub then: Brace<Box<Expr>>,
|
||||
@ -275,6 +258,7 @@ pub struct IfExpr {
|
||||
/// ```kind
|
||||
/// $ a b
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct PairNode<T> {
|
||||
pub r#sign: lexemes::Sign,
|
||||
pub left: Box<T>,
|
||||
@ -287,6 +271,7 @@ pub struct PairNode<T> {
|
||||
/// ```kind
|
||||
/// specialize a into #0 in a
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct SubstExpr {
|
||||
pub r#specialize: lexemes::Specialize,
|
||||
pub name: Ident,
|
||||
@ -298,11 +283,13 @@ pub struct SubstExpr {
|
||||
}
|
||||
|
||||
/// A List expression represents a list of values.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct ListNode<T> {
|
||||
pub bracket: Bracket<ThinVec<T>>,
|
||||
}
|
||||
|
||||
/// A Case is a single case in a match node.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct CaseNode {
|
||||
pub name: Ident,
|
||||
pub r#arrow: lexemes::FatArrow,
|
||||
@ -318,6 +305,7 @@ pub struct CaseNode {
|
||||
/// cons => a.head
|
||||
/// }
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct MatchExpr {
|
||||
pub r#match: lexemes::Match,
|
||||
pub typ: Option<Ident>,
|
||||
@ -336,6 +324,7 @@ pub struct MatchExpr {
|
||||
/// a.head
|
||||
/// ```
|
||||
///
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct OpenExpr {
|
||||
pub r#open: lexemes::Open,
|
||||
pub typ: Ident,
|
||||
@ -350,6 +339,7 @@ pub struct OpenExpr {
|
||||
|
||||
/// A node that express the operation after accessing fields
|
||||
/// of a record.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum AccessOperation {
|
||||
Set(Token, Box<Expr>),
|
||||
Mut(Token, Box<Expr>),
|
||||
@ -357,6 +347,7 @@ pub enum AccessOperation {
|
||||
}
|
||||
|
||||
/// A node for accessing and modifying fields of a record.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct AccessExpr {
|
||||
pub typ: Box<Expr>,
|
||||
pub expr: Box<Expr>,
|
||||
@ -365,6 +356,7 @@ pub struct AccessExpr {
|
||||
}
|
||||
|
||||
/// An expression is a piece of code that can be evaluated.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum ExprKind {
|
||||
Local(Box<LocalExpr>),
|
||||
Pi(Box<PiExpr>),
|
||||
@ -392,14 +384,16 @@ pub enum ExprKind {
|
||||
pub type Expr = Item<ExprKind>;
|
||||
|
||||
/// A constructor node is the name of a global function.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct ConstructorPat {
|
||||
pub name: QualifiedIdent,
|
||||
pub args: ThinVec<Argument>,
|
||||
}
|
||||
|
||||
/// A pattern is part of a rule. It is a structure that matches an expression.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum PatKind {
|
||||
Ident(Ident),
|
||||
Name(Name),
|
||||
Pair(PairNode<Pat>),
|
||||
Constructor(ConstructorPat),
|
||||
List(ListNode<Pat>),
|
||||
@ -414,10 +408,12 @@ pub type Pat = Item<PatKind>;
|
||||
/// ```kind
|
||||
/// Add (n: Nat) (m: Nat) : Nat
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Signature {
|
||||
pub name: Ident,
|
||||
pub name: Name,
|
||||
pub arguments: ThinVec<Argument>,
|
||||
pub colon: Colon<ThinVec<Expr>>,
|
||||
pub return_type: Option<Colon<Expr>>,
|
||||
pub value: Option<Block>,
|
||||
}
|
||||
|
||||
/// A rule is a top-level structure that have pattern match rules. It does
|
||||
@ -426,6 +422,7 @@ pub struct Signature {
|
||||
/// ```kind
|
||||
/// Add Nat.zero m = m
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Rule {
|
||||
pub name: Ident,
|
||||
pub patterns: ThinVec<Pat>,
|
||||
@ -440,6 +437,7 @@ pub struct Rule {
|
||||
/// n + m
|
||||
/// }
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Function {
|
||||
pub name: Ident,
|
||||
pub arguments: ThinVec<Argument>,
|
||||
@ -454,6 +452,7 @@ pub struct Function {
|
||||
/// ```kind
|
||||
/// @eval (+ 1 1)
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Command {
|
||||
pub at: Token,
|
||||
pub name: Ident,
|
||||
@ -466,6 +465,7 @@ pub struct Command {
|
||||
/// ```kind
|
||||
/// some (value: a) : Maybe a
|
||||
/// ```
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Constructor {
|
||||
pub name: Ident,
|
||||
pub arguments: ThinVec<Argument>,
|
||||
@ -474,6 +474,7 @@ pub struct Constructor {
|
||||
|
||||
/// A type definition is a top-level structure that defines a type family
|
||||
/// with multiple constructors that named fields, indices and parameters.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct TypeDef {
|
||||
pub name: QualifiedIdent,
|
||||
pub constructors: ThinVec<Constructor>,
|
||||
@ -483,6 +484,7 @@ pub struct TypeDef {
|
||||
|
||||
/// A record definition is a top-level structure that defines a type with
|
||||
/// a single constructor that has named fields with named fields.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct RecordDef {
|
||||
pub name: QualifiedIdent,
|
||||
pub fields: ThinVec<TypeBinding>,
|
||||
@ -492,6 +494,7 @@ pub struct RecordDef {
|
||||
|
||||
/// A top-level item is a item that is on the outermost level of a
|
||||
/// program. It includes functions, commands, signatures and rules.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub enum TopLevelKind {
|
||||
Function(Function),
|
||||
Commmand(Command),
|
||||
@ -501,6 +504,7 @@ pub enum TopLevelKind {
|
||||
Rule(Rule),
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Attributed<T> {
|
||||
pub attributes: ThinVec<Attribute>,
|
||||
pub data: T,
|
||||
@ -511,6 +515,7 @@ pub type TopLevel = Attributed<Item<TopLevelKind>>;
|
||||
|
||||
/// A collection of top-level items. This is the root of the CST and
|
||||
/// is the result of parsing a module.
|
||||
#[derive(Debug, Clone, PartialEq)]
|
||||
pub struct Module {
|
||||
pub shebang: Option<String>,
|
||||
pub items: ThinVec<TopLevel>,
|
||||
|
||||
@ -1,12 +1,31 @@
|
||||
#[derive(Debug, Clone)]
|
||||
use std::fmt::Debug;
|
||||
use tree_sitter::Point;
|
||||
|
||||
#[derive(Default, Clone, PartialEq)]
|
||||
pub struct Token {
|
||||
pub span: Span,
|
||||
}
|
||||
|
||||
#[derive(Debug, Clone)]
|
||||
pub struct Span;
|
||||
impl Debug for Token {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Token({:?})", self.span)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Default, Clone, PartialEq)]
|
||||
pub struct Span(pub Point, pub Point);
|
||||
|
||||
impl Debug for Span {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Span({:?}:{:?}..{:?}:{:?})", self.0.row, self.0.column, self.1.row, self.1.column)
|
||||
}
|
||||
}
|
||||
|
||||
impl Span {
|
||||
pub fn new(start: Point, end: Point) -> Span {
|
||||
Span(start, end)
|
||||
}
|
||||
|
||||
pub fn mix(&self, _other: &Span) -> Span {
|
||||
self.clone()
|
||||
}
|
||||
@ -34,49 +53,134 @@ pub type Open = Token;
|
||||
pub type Do = Token;
|
||||
pub type Dot = Token;
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub enum Either<A, B> {
|
||||
Left(A),
|
||||
Right(B),
|
||||
}
|
||||
|
||||
impl<A: Debug, B: Debug> Debug for Either<A, B> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
Either::Left(a) => write!(f, "Left({:?})", a),
|
||||
Either::Right(b) => write!(f, "Right({:?})", b),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// Compounds
|
||||
#[derive(Debug)]
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Paren<T>(pub Token, pub T, pub Token);
|
||||
|
||||
#[derive(Debug)]
|
||||
impl<A: Debug> Debug for Paren<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Paren({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Bracket<T>(pub Token, pub T, pub Token);
|
||||
|
||||
#[derive(Debug)]
|
||||
impl<A: Debug> Debug for Bracket<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Bracket({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Brace<T>(pub Token, pub T, pub Token);
|
||||
|
||||
#[derive(Debug)]
|
||||
impl<A: Debug> Debug for Brace<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Brace({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct AngleBracket<T>(pub Token, pub T, pub Token);
|
||||
|
||||
#[derive(Debug)]
|
||||
impl<A: Debug> Debug for AngleBracket<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "AngleBracket({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Equal<T>(pub Token, pub T);
|
||||
|
||||
#[derive(Debug)]
|
||||
impl<A: Debug> Debug for Equal<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Equal({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Colon<T>(pub Token, pub T);
|
||||
|
||||
#[derive(Debug)]
|
||||
impl<A: Debug> Debug for Colon<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Colon({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Tokenized<T>(pub Token, pub T);
|
||||
|
||||
impl<A: Debug> Debug for Tokenized<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Tokenized({:?}, {:?})", self.0, self.1)
|
||||
}
|
||||
}
|
||||
|
||||
// Concrete syntax tree
|
||||
|
||||
#[derive(Debug)]
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Ident(pub Item<Tokenized<String>>);
|
||||
|
||||
#[derive(Debug)]
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub enum Name {
|
||||
Ident(Ident),
|
||||
QualifiedIdent(QualifiedIdent),
|
||||
}
|
||||
|
||||
impl Debug for Name {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
match self {
|
||||
Name::Ident(ident) => write!(f, "{ident:?}"),
|
||||
Name::QualifiedIdent(ident) => write!(f, "{ident:?}"),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Debug for Ident {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Ident({:?})", self.0.data.1)
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct QualifiedIdent(pub Item<Tokenized<String>>);
|
||||
|
||||
impl Debug for QualifiedIdent {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "QualifiedIdent({:?})", self.0.data.1)
|
||||
}
|
||||
}
|
||||
|
||||
/// A localized data structure, it's useful to keep track of source code
|
||||
/// location.
|
||||
#[derive(Debug)]
|
||||
#[derive(Clone, PartialEq)]
|
||||
pub struct Item<T> {
|
||||
pub data: T,
|
||||
pub span: Span,
|
||||
}
|
||||
|
||||
impl<A: Debug> Debug for Item<A> {
|
||||
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
|
||||
write!(f, "Item({:?}, {:?})", self.span, self.data)
|
||||
}
|
||||
}
|
||||
|
||||
impl<T> Paren<T> {
|
||||
pub fn span(&self) -> Span {
|
||||
self.0.span.mix(&self.2.span)
|
||||
|
||||
1
example/example.kind
Normal file
1
example/example.kind
Normal file
@ -0,0 +1 @@
|
||||
bao
|
||||
@ -1,181 +0,0 @@
|
||||
// U60
|
||||
// ---
|
||||
|
||||
U60.to_nat (x: U60) : Nat
|
||||
U60.to_nat 0 = Nat.zero
|
||||
U60.to_nat n = (Nat.succ (U60.to_nat (- n 1)))
|
||||
|
||||
// Empty
|
||||
// -----
|
||||
|
||||
Empty : Type
|
||||
|
||||
// Unit
|
||||
// ----
|
||||
|
||||
Unit : Type
|
||||
Unit.new : Unit
|
||||
|
||||
// Bool
|
||||
// ----
|
||||
|
||||
type Bool {
|
||||
true : Bool
|
||||
false : Bool
|
||||
}
|
||||
|
||||
Bool.not (a: Bool) : Bool
|
||||
Bool.not Bool.true = Bool.false
|
||||
Bool.not Bool.false = Bool.true
|
||||
|
||||
Bool.and (a: Bool) (b: Bool) : Bool
|
||||
Bool.and Bool.true Bool.true = Bool.true
|
||||
Bool.and Bool.true Bool.false = Bool.false
|
||||
Bool.and Bool.false Bool.true = Bool.false
|
||||
Bool.and Bool.false Bool.false = Bool.false
|
||||
|
||||
Bool.if <r: Type> (b: Bool) (if_t: r) (if_f: r) : r
|
||||
Bool.if r Bool.true if_t if_f = if_t
|
||||
Bool.if r Bool.false if_t if_f = if_f
|
||||
|
||||
Bool.not_not_theorem (a: Bool) : (Equal Bool a (Bool.not (Bool.not a)))
|
||||
Bool.not_not_theorem Bool.true = (Equal.refl Bool Bool.true)
|
||||
Bool.not_not_theorem Bool.false = (Equal.refl Bool Bool.false)
|
||||
|
||||
Bool.true_not_false (e: (Equal Bool Bool.true Bool.false)) : Empty
|
||||
Bool.true_not_false e = (Equal.rewrite e (x => (Bool.if Type x Unit Empty)) Unit.new)
|
||||
|
||||
// Nat
|
||||
// ---
|
||||
|
||||
type Nat {
|
||||
zero : Nat
|
||||
succ (pred: Nat) : Nat
|
||||
}
|
||||
|
||||
Nat.double (x: Nat) : Nat
|
||||
Nat.double (Nat.succ x) = (Nat.succ (Nat.succ (Nat.double x)))
|
||||
Nat.double (Nat.zero) = (Nat.zero)
|
||||
|
||||
Nat.add (a: Nat) (b: Nat) : Nat
|
||||
Nat.add (Nat.succ a) b = (Nat.succ (Nat.add a b))
|
||||
Nat.add Nat.zero b = b
|
||||
|
||||
Nat.comm.a (a: Nat) : (Equal Nat a (Nat.add a Nat.zero))
|
||||
Nat.comm.a Nat.zero = Equal.refl
|
||||
Nat.comm.a (Nat.succ a) = (Equal.apply (x => (Nat.succ x)) (Nat.comm.a a))
|
||||
|
||||
Nat.comm.b (a: Nat) (b: Nat): (Equal Nat (Nat.add a (Nat.succ b)) (Nat.succ (Nat.add a b)))
|
||||
Nat.comm.b Nat.zero b = Equal.refl
|
||||
Nat.comm.b (Nat.succ a) b = (Equal.apply (x => (Nat.succ x)) (Nat.comm.b a b))
|
||||
|
||||
Nat.comm (a: Nat) (b: Nat) : (Equal Nat (Nat.add a b) (Nat.add b a))
|
||||
Nat.comm Nat.zero b = (Nat.comm.a b)
|
||||
Nat.comm (Nat.succ a) b =
|
||||
let e0 = (Equal.apply (x => (Nat.succ x)) (Nat.comm a b))
|
||||
let e1 = (Equal.mirror (Nat.comm.b b a))
|
||||
(Equal.chain e0 e1)
|
||||
|
||||
Nat.to_u60 (n: Nat) : U60
|
||||
Nat.to_u60 Nat.zero = 0
|
||||
Nat.to_u60 (Nat.succ n) = (+ 1 (Nat.to_u60 n))
|
||||
|
||||
Nat.mul (a: Nat) (b: Nat) : Nat
|
||||
Nat.mul (Nat.succ a) b = (Nat.add (Nat.mul a b) b) // (a + 1) * b = a*b + b
|
||||
Nat.mul Nat.zero b = Nat.zero // 0b = 0
|
||||
|
||||
Nat.mul.comm.a (x: Nat): (Equal (Nat.mul x Nat.zero) Nat.zero)
|
||||
Nat.mul.comm.a Nat.zero = Equal.refl
|
||||
Nat.mul.comm.a (Nat.succ x) =
|
||||
let e0 = (Nat.mul.comm.a x)
|
||||
let e1 = (Equal.apply (y => (Nat.add y Nat.zero)) e0)
|
||||
e1
|
||||
|
||||
// List
|
||||
// ----
|
||||
|
||||
List (a: Type) : Type
|
||||
List.nil <a> : (List a)
|
||||
List.cons <a> (x: a) (xs: (List a)) : (List a)
|
||||
|
||||
List.negate (xs: (List Bool)) : (List Bool)
|
||||
List.negate (List.cons Bool x xs) = (List.cons Bool (Bool.not x) (List.negate xs))
|
||||
List.negate (List.nil Bool) = (List.nil Bool)
|
||||
|
||||
List.tail <a> (xs: (List a)) : (List a)
|
||||
List.tail a (List.cons t x xs) = xs
|
||||
|
||||
List.map <a> <b> (x: (List a)) (f: (x: a) -> b) : (List b)
|
||||
List.map a b (List.nil t) f = List.nil
|
||||
List.map a b (List.cons t x xs) f = (List.cons (f x) (List.map xs f))
|
||||
|
||||
List.concat <a> (xs: (List a)) (ys: (List a)) : (List a)
|
||||
List.concat a (List.cons u x xs) ys = (List.cons u x (List.concat a xs ys))
|
||||
List.concat a (List.nil u) ys = ys
|
||||
|
||||
List.flatten <a> (xs: (List (List a))) : (List a)
|
||||
List.flatten a (List.cons u x xs) = (List.concat x (List.flatten xs))
|
||||
List.flatten a (List.nil u) = List.nil
|
||||
|
||||
List.bind <a: Type> <b: Type> (xs: (List a)) (f: a -> (List b)) : (List b)
|
||||
List.bind a b xs f = (List.flatten b (List.map xs f))
|
||||
|
||||
List.pure <t: Type> (x: t) : (List t)
|
||||
List.pure t x = (List.cons t x (List.nil t))
|
||||
|
||||
List.range.go (lim: Nat) (res: (List Nat)) : (List Nat)
|
||||
List.range.go Nat.zero res = res
|
||||
List.range.go (Nat.succ n) res = (List.range.go n (List.cons n res))
|
||||
|
||||
List.sum (xs: (List Nat)) : Nat
|
||||
List.sum (List.nil t) = Nat.zero
|
||||
List.sum (List.cons t x xs) = (Nat.add x (List.sum xs))
|
||||
|
||||
// Equal
|
||||
// -----
|
||||
|
||||
Equal <t> (a: t) (b: t) : Type
|
||||
Equal.refl <t> <a: t> : (Equal t a a)
|
||||
|
||||
Equal.mirror <t> <a: t> <b: t> (e: (Equal t a b)) : (Equal t b a)
|
||||
Equal.mirror t a b (Equal.refl u k) = (Equal.refl u k)
|
||||
|
||||
Equal.apply <t> <u> <a: t> <b: t> (f: t -> t) (e: (Equal t a b)) : (Equal t (f a) (f b))
|
||||
Equal.apply t u a b f (Equal.refl v k) = (Equal.refl v (f k))
|
||||
|
||||
Equal.rewrite <t> <a: t> <b: t> (e: (Equal t a b)) (p: t -> Type) (x: (p a)) : (p b)
|
||||
Equal.rewrite t a b (Equal.refl u k) p x = (x :: (p k))
|
||||
|
||||
Equal.chain <t> <a: t> <b: t> <c: t> (e0: (Equal t a b)) (e1: (Equal t b c)) : (Equal t a c)
|
||||
Equal.chain t a b c e0 (Equal.refl u x) = (e0 :: (Equal t a x))
|
||||
|
||||
// Monad
|
||||
// -----
|
||||
|
||||
Monad (f: Type -> Type) : Type
|
||||
Monad.new (f: Type -> Type)
|
||||
(pure: (a: Type) -> (x: a) -> (f a))
|
||||
(bind: (a: Type) -> (b: Type) -> (x: (f a)) -> (y: a -> (f b)) -> (f b))
|
||||
: (Monad f)
|
||||
|
||||
// Variadic
|
||||
// --------
|
||||
|
||||
Variadic (r: Type) (n: Nat) : Type
|
||||
Variadic r Nat.zero = r
|
||||
Variadic r (Nat.succ n) = r -> (Variadic r n)
|
||||
|
||||
// Examples
|
||||
// --------
|
||||
|
||||
SNat : Type
|
||||
SNat = (p: Type) -> ((SNat) -> p) -> p -> p
|
||||
|
||||
SZ : SNat
|
||||
SZ = p => s => z => z
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user