mirror of
https://github.com/HigherOrderCO/Kind1.git
synced 2024-09-11 08:45:32 +03:00
Changed structure
This commit is contained in:
parent
1e8b0024e3
commit
b996312813
73
Cargo.lock
generated
73
Cargo.lock
generated
@ -230,6 +230,17 @@ dependencies = [
|
||||
"slab",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "getrandom"
|
||||
version = "0.2.7"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4eb1a864a501629691edf6c15a593b7a51eebaa1e8468e9ddc623de7c9b58ec6"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"libc",
|
||||
"wasi",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "h2"
|
||||
version = "0.3.14"
|
||||
@ -428,32 +439,16 @@ dependencies = [
|
||||
|
||||
[[package]]
|
||||
name = "kind2"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"kind2_log",
|
||||
"tracing",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind2_book"
|
||||
version = "0.1.0"
|
||||
|
||||
[[package]]
|
||||
name = "kind2_log"
|
||||
version = "0.1.0"
|
||||
version = "0.2.76"
|
||||
dependencies = [
|
||||
"clap",
|
||||
"highlight_error",
|
||||
"hvm",
|
||||
"rand",
|
||||
"tracing",
|
||||
"tracing-subscriber",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "kind2_parser"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"hvm",
|
||||
"kind2_book",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "lazy_static"
|
||||
version = "1.4.0"
|
||||
@ -617,6 +612,12 @@ version = "0.3.25"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1df8c4ec4b0627e53bdf214615ad287367e482558cf84b109250b37464dc03ae"
|
||||
|
||||
[[package]]
|
||||
name = "ppv-lite86"
|
||||
version = "0.2.16"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "eb9f9e6e233e5c4a35559a617bf40a4ec447db2e84c20b55a6f83167b7e57872"
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro-error"
|
||||
version = "1.0.4"
|
||||
@ -659,6 +660,36 @@ dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand"
|
||||
version = "0.8.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404"
|
||||
dependencies = [
|
||||
"libc",
|
||||
"rand_chacha",
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_chacha"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
|
||||
dependencies = [
|
||||
"ppv-lite86",
|
||||
"rand_core",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "rand_core"
|
||||
version = "0.6.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
|
||||
dependencies = [
|
||||
"getrandom",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "redox_syscall"
|
||||
version = "0.2.16"
|
||||
|
28
Cargo.toml
28
Cargo.toml
@ -1,11 +1,19 @@
|
||||
[workspace]
|
||||
members = [
|
||||
"compiler/kind2",
|
||||
"compiler/log",
|
||||
"compiler/book",
|
||||
#"compiler/driver",
|
||||
"compiler/parser",
|
||||
#"compiler/adjuster",
|
||||
]
|
||||
[package]
|
||||
name = "kind2"
|
||||
version = "0.2.76"
|
||||
edition = "2021"
|
||||
description = "A pure functional functional language that uses the HVM."
|
||||
repository = "https://github.com/Kindelia/Kind2"
|
||||
license = "MIT"
|
||||
keywords = ["functional", "language", "type-theory", "proof-assistant"]
|
||||
|
||||
[profile.release.package]
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
hvm = "0.1.81"
|
||||
#hvm = { path = "../hvm" }
|
||||
tracing = "0.1.36"
|
||||
tracing-subscriber = { version = "0.3.15", features = ["env-filter"] }
|
||||
highlight_error = "0.1.1"
|
||||
clap = { version = "3.1.8", features = ["derive"] }
|
||||
rand = "0.8.5"
|
@ -1,8 +0,0 @@
|
||||
[package]
|
||||
name = "kind2_book"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
@ -1,120 +0,0 @@
|
||||
// The location of things inside the source code
|
||||
pub mod span;
|
||||
|
||||
// Description of all the terms inside the language
|
||||
pub mod term;
|
||||
|
||||
// Types of names.
|
||||
pub mod name;
|
||||
|
||||
use crate::term::Term;
|
||||
use crate::span::Span;
|
||||
use crate::name::Qualified;
|
||||
|
||||
use std::collections::HashMap;
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
// A book is a collection of entries.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Book {
|
||||
pub names: Vec<String>,
|
||||
pub entrs: HashMap<Qualified, Box<Entry>>,
|
||||
pub holes: u64,
|
||||
}
|
||||
|
||||
// A entry describes a function that has
|
||||
// rules and a type.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Entry {
|
||||
pub name: Qualified,
|
||||
pub orig: Span,
|
||||
pub kdln: Option<String>,
|
||||
pub args: Vec<Box<Argument>>,
|
||||
pub tipo: Box<Term>,
|
||||
pub rules: Vec<Box<Rule>>
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Rule {
|
||||
pub orig: Span,
|
||||
pub name: Qualified,
|
||||
pub pats: Vec<Box<Term>>,
|
||||
pub body: Box<Term>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Argument {
|
||||
pub hide: bool,
|
||||
pub eras: bool,
|
||||
pub name: String,
|
||||
pub tipo: Box<Term>,
|
||||
}
|
||||
|
||||
impl Entry {
|
||||
pub fn count_implicits(&self) -> (usize, usize) {
|
||||
let mut hiddens = 0;
|
||||
let mut eraseds = 0;
|
||||
for arg in &self.args {
|
||||
if arg.hide {
|
||||
hiddens = hiddens + 1;
|
||||
}
|
||||
if arg.eras {
|
||||
eraseds = eraseds + 1;
|
||||
}
|
||||
}
|
||||
(hiddens, eraseds)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Rule {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "{}", self.name)?;
|
||||
for pat in &self.pats {
|
||||
write!(f, " {}", pat)?;
|
||||
}
|
||||
write!(f, " = {}", self.body)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Argument {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
let (open, close) = match (self.eras, self.hide) {
|
||||
(false, false) => ("(", ")"),
|
||||
(false, true ) => ("+<", ">"),
|
||||
(true , false) => ("-(", ")"),
|
||||
(true , true ) => ("<", ">"),
|
||||
};
|
||||
write!(f, "{}{}: {}{}", open, self.name, &self.tipo, close)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Entry {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
if let Some(kdln) = &self.kdln {
|
||||
write!(f, "{} #{}", self.name, kdln)?
|
||||
} else {
|
||||
write!(f, "{}", self.name.clone())?
|
||||
};
|
||||
|
||||
for arg in &self.args {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
|
||||
write!(f, " : {}", &self.tipo)?;
|
||||
|
||||
for rule in &self.rules {
|
||||
write!(f, "\n{}", rule)?
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Book {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
for name in &self.names {
|
||||
write!(f, "{}\n", self.entrs.get(&Qualified::from_str(name)).unwrap())?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
@ -1,105 +0,0 @@
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct EncodedName(u64);
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub struct Ident(pub String);
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub struct Qualified {
|
||||
pub path: Ident,
|
||||
pub name: Ident,
|
||||
}
|
||||
|
||||
impl EncodedName {
|
||||
pub fn u64_to_name(&self) -> String {
|
||||
let mut name = String::new();
|
||||
let mut num = self.0;
|
||||
while num > 0 {
|
||||
let chr = (num % 64) as u8;
|
||||
let chr =
|
||||
match chr {
|
||||
0 => '.',
|
||||
1 ..= 10 => (chr - 1 + b'0') as char,
|
||||
11 ..= 36 => (chr - 11 + b'A') as char,
|
||||
37 ..= 62 => (chr - 37 + b'a') as char,
|
||||
63 => '_',
|
||||
64 .. => panic!("impossible character value")
|
||||
};
|
||||
name.push(chr);
|
||||
num = num / 64;
|
||||
}
|
||||
name.chars().rev().collect()
|
||||
}
|
||||
|
||||
pub fn encode(name: &str) -> EncodedName {
|
||||
fn char_to_u64(chr: char) -> u64 {
|
||||
match chr {
|
||||
'.' => 0,
|
||||
'0'..='9' => 1 + chr as u64 - '0' as u64,
|
||||
'A'..='Z' => 11 + chr as u64 - 'A' as u64,
|
||||
'a'..='z' => 37 + chr as u64 - 'a' as u64,
|
||||
'_' => 63,
|
||||
_ => panic!("Invalid name character."),
|
||||
}
|
||||
}
|
||||
|
||||
let mut num: u64 = 0;
|
||||
for (i, chr) in name.chars().enumerate() {
|
||||
if i < 10 {
|
||||
num = (num << 6) + char_to_u64(chr);
|
||||
}
|
||||
}
|
||||
|
||||
return EncodedName(num);
|
||||
}
|
||||
}
|
||||
|
||||
impl Qualified {
|
||||
#[inline]
|
||||
pub fn new(path: String, name: String) -> Qualified {
|
||||
Qualified { path: Ident(path), name: Ident(name) }
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn new_raw(path: &str, name: &str) -> Qualified {
|
||||
Qualified { path: Ident(path.to_string()), name: Ident(name.to_string()) }
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn from_str(str: &str) -> Qualified {
|
||||
let mut path = str
|
||||
.split(".")
|
||||
.map(|x| x.to_string())
|
||||
.collect::<Vec<String>>();
|
||||
let name = path.pop().unwrap_or("".to_string());
|
||||
Qualified { path: Ident(path.join(".")), name: Ident(name) }
|
||||
}
|
||||
|
||||
pub fn to_string(&self) -> String {
|
||||
format!("{}.{}", self.path, self.name)
|
||||
}
|
||||
|
||||
pub fn encode(&self) -> EncodedName {
|
||||
EncodedName::encode(&self.to_string())
|
||||
}
|
||||
}
|
||||
|
||||
impl Ident {
|
||||
pub fn encode(&self) -> EncodedName {
|
||||
EncodedName::encode(&self.0)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Qualified {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "{}.{}", self.path, self.name)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Ident {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "{}", self.0)
|
||||
}
|
||||
}
|
@ -1,155 +0,0 @@
|
||||
// Module that describes terms and operators
|
||||
// of the language
|
||||
|
||||
use crate::name::{Ident, Qualified};
|
||||
use crate::span::Span;
|
||||
|
||||
use std::ascii;
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
#[derive(Copy, Clone, Debug)]
|
||||
pub enum Operator {
|
||||
Add,
|
||||
Sub,
|
||||
Mul,
|
||||
Div,
|
||||
Mod,
|
||||
And,
|
||||
Or,
|
||||
Xor,
|
||||
Shl,
|
||||
Shr,
|
||||
Ltn,
|
||||
Lte,
|
||||
Eql,
|
||||
Gte,
|
||||
Gtn,
|
||||
Neq,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Term {
|
||||
Typ { orig: Span },
|
||||
Var { orig: Span, name: Ident },
|
||||
All { orig: Span, name: Ident, tipo: Box<Term>, body: Box<Term> },
|
||||
Lam { orig: Span, name: Ident, body: Box<Term> },
|
||||
App { orig: Span, func: Box<Term>, argm: Box<Term> },
|
||||
Let { orig: Span, name: Ident, expr: Box<Term>, body: Box<Term> },
|
||||
Ann { orig: Span, expr: Box<Term>, tipo: Box<Term> },
|
||||
Sub { orig: Span, name: Ident, indx: u64, redx: u64, expr: Box<Term> },
|
||||
Ctr { orig: Span, name: Qualified, args: Vec<Box<Term>> },
|
||||
Fun { orig: Span, name: Qualified, args: Vec<Box<Term>> },
|
||||
Hlp { orig: Span },
|
||||
U60 { orig: Span },
|
||||
Num { orig: Span, numb: u64 },
|
||||
Op2 { orig: Span, oper: Operator, val0: Box<Term>, val1: Box<Term> },
|
||||
Hol { orig: Span, numb: u64 },
|
||||
Mat { orig: Span, tipo: Qualified, name: Ident, expr: Box<Term>, cses: Vec<(Ident,Box<Term>)>, moti: Box<Term> },
|
||||
}
|
||||
|
||||
impl Term {
|
||||
pub fn interpret_as_string(&self) -> Option<String> {
|
||||
let mut text = String::new();
|
||||
let mut term = self;
|
||||
|
||||
let string_nil = Qualified::from_str("String.nil");
|
||||
let string_cons = Qualified::from_str("String.cons");
|
||||
|
||||
loop {
|
||||
if let Term::Ctr { name, args, .. } = term {
|
||||
if *name == string_cons && args.len() == 2 {
|
||||
if let Term::Num { numb, .. } = *args[0] {
|
||||
if ascii::escape_default(numb as u8).count() > 1 {
|
||||
return None;
|
||||
} else {
|
||||
text.push(char::from_u32(numb as u32).unwrap_or('\0'));
|
||||
term = &*args[1];
|
||||
continue;
|
||||
}
|
||||
} else {
|
||||
return None;
|
||||
}
|
||||
} else if *name == string_nil && args.len() == 0 {
|
||||
return Some(text);
|
||||
}
|
||||
}
|
||||
return None;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Operator {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
use Operator::*;
|
||||
|
||||
match self {
|
||||
Add => write!(f, "*"),
|
||||
Sub => write!(f, "-"),
|
||||
Mul => write!(f, "*"),
|
||||
Div => write!(f, "/"),
|
||||
Mod => write!(f, "%"),
|
||||
And => write!(f, "&"),
|
||||
Or => write!(f, "|"),
|
||||
Xor => write!(f, "^"),
|
||||
Shl => write!(f, "<<"),
|
||||
Shr => write!(f, ">>"),
|
||||
Ltn => write!(f, "<"),
|
||||
Lte => write!(f, "<="),
|
||||
Eql => write!(f, "=="),
|
||||
Gte => write!(f, ">="),
|
||||
Gtn => write!(f, ">"),
|
||||
Neq => write!(f, "!="),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Term {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
if let Some(str) = self.interpret_as_string() {
|
||||
write!(f, "\"{}\"", str)
|
||||
} else {
|
||||
use Term::*;
|
||||
match self {
|
||||
Typ { orig: _ } =>
|
||||
write!(f, "Type"),
|
||||
Hlp { orig: _ } =>
|
||||
write!(f, "?"),
|
||||
U60 { orig: _ } =>
|
||||
write!(f, "U60"),
|
||||
Hol { orig: _, .. } =>
|
||||
write!(f, "_"),
|
||||
Var { orig: _, name } =>
|
||||
write!(f, "{}", name),
|
||||
Num { orig: _, numb } =>
|
||||
write!(f, "{}", numb),
|
||||
Lam { orig: _, name, body } =>
|
||||
write!(f, "({} => {})", name, body),
|
||||
Ann { orig: _, expr, tipo } =>
|
||||
write!(f, "({} :: {})", expr, tipo),
|
||||
Op2 { orig: _, oper, val0, val1 } =>
|
||||
write!(f, "({} {} {})", oper, val0, val1),
|
||||
All { orig: _, name, tipo, body } =>
|
||||
write!(f, "(({}: {}) {})", name, tipo, body),
|
||||
Let { orig: _, name, expr, body } =>
|
||||
write!(f, "(let {} = {}; {})", name, expr, body),
|
||||
Sub { orig: _, name, indx: _, redx, expr } =>
|
||||
write!(f, "({} ## {}/{})", expr, name, redx),
|
||||
Ctr { orig: _, name, args } =>
|
||||
write!(f, "({}{})", name, args.iter().map(|x| format!(" {}", x)).collect::<String>()),
|
||||
Fun { orig: _, name, args } =>
|
||||
write!(f, "({}{})", name, args.iter().map(|x| format!(" {}", x)).collect::<String>()),
|
||||
App { func, argm, .. } => {
|
||||
let mut args = vec![argm];
|
||||
let mut expr = func;
|
||||
while let App { func, argm, .. } = &**expr {
|
||||
args.push(argm);
|
||||
expr = func;
|
||||
}
|
||||
args.reverse();
|
||||
write!(f, "({} {})", expr, args.iter().map(|x| format!("{}", x)).collect::<Vec<String>>().join(" "))
|
||||
}
|
||||
Mat { .. } => panic!("Internal Error: Cannot display a Term::Mat because it's removed after adjust.")
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
@ -1,10 +0,0 @@
|
||||
[package]
|
||||
name = "kind2"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
tracing = "0.1.36"
|
||||
kind2_log = { path = "../log" }
|
@ -1,3 +0,0 @@
|
||||
# Kind2
|
||||
|
||||
The entire compiler executable.
|
@ -1,5 +0,0 @@
|
||||
use kind2_log::init_logger;
|
||||
|
||||
fn main() {
|
||||
init_logger("").unwrap();
|
||||
}
|
@ -1,10 +0,0 @@
|
||||
[package]
|
||||
name = "kind2_log"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
tracing = "0.1.36"
|
||||
tracing-subscriber = { version = "0.3.15", features = ["env-filter"] }
|
@ -1,3 +0,0 @@
|
||||
# kind2_log
|
||||
|
||||
Tiny crate to help while debugging the compiler.
|
@ -1,10 +0,0 @@
|
||||
[package]
|
||||
name = "kind2_parser"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
kind2_book = { path = "../book" }
|
||||
hvm = "0.1.81"
|
185
src/book/mod.rs
Normal file
185
src/book/mod.rs
Normal file
@ -0,0 +1,185 @@
|
||||
// The location of things inside the source code
|
||||
pub mod span;
|
||||
|
||||
// Description of all the terms inside the language
|
||||
pub mod term;
|
||||
|
||||
// Types of names.
|
||||
pub mod name;
|
||||
|
||||
// Types of names.
|
||||
pub mod new_type;
|
||||
|
||||
use crate::book::name::{Ident, Qualified};
|
||||
use crate::book::span::{FileOffset, Localized, Span};
|
||||
use crate::book::term::Term;
|
||||
|
||||
use std::collections::HashMap;
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
// A book is a collection of entries.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Book {
|
||||
pub names: Vec<String>,
|
||||
pub entrs: HashMap<Qualified, Box<Entry>>,
|
||||
pub holes: u64,
|
||||
}
|
||||
|
||||
// A entry describes a function that has
|
||||
// rules and a type.
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Entry {
|
||||
pub name: Qualified,
|
||||
pub orig: Span,
|
||||
pub kdln: Option<String>,
|
||||
pub args: Vec<Box<Argument>>,
|
||||
pub tipo: Box<Term>,
|
||||
pub rules: Vec<Box<Rule>>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Rule {
|
||||
pub orig: Span,
|
||||
pub name: Qualified,
|
||||
pub pats: Vec<Box<Term>>,
|
||||
pub body: Box<Term>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Argument {
|
||||
pub hide: bool,
|
||||
pub orig: Span,
|
||||
pub eras: bool,
|
||||
pub name: Ident,
|
||||
pub tipo: Box<Term>,
|
||||
}
|
||||
|
||||
impl Book {
|
||||
pub fn set_origin_file(book: &mut Book, file: FileOffset) {
|
||||
for entr in book.entrs.values_mut() {
|
||||
entr.set_origin_file(file);
|
||||
}
|
||||
}
|
||||
|
||||
pub fn new() -> Book {
|
||||
Book {
|
||||
names: vec![],
|
||||
entrs: HashMap::new(),
|
||||
holes: 0,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Entry {
|
||||
pub fn count_implicits(&self) -> (usize, usize) {
|
||||
let mut hiddens = 0;
|
||||
let mut eraseds = 0;
|
||||
for arg in &self.args {
|
||||
if arg.hide {
|
||||
hiddens = hiddens + 1;
|
||||
}
|
||||
if arg.eras {
|
||||
eraseds = eraseds + 1;
|
||||
}
|
||||
}
|
||||
(hiddens, eraseds)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Rule {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "{}", self.name)?;
|
||||
for pat in &self.pats {
|
||||
write!(f, " {}", pat)?;
|
||||
}
|
||||
write!(f, " = {}", self.body)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Argument {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
let (open, close) = match (self.eras, self.hide) {
|
||||
(false, false) => ("(", ")"),
|
||||
(false, true) => ("+<", ">"),
|
||||
(true, false) => ("-(", ")"),
|
||||
(true, true) => ("<", ">"),
|
||||
};
|
||||
write!(f, "{}{}: {}{}", open, self.name, &self.tipo, close)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Entry {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
if let Some(kdln) = &self.kdln {
|
||||
write!(f, "{} #{}", self.name, kdln)?
|
||||
} else {
|
||||
write!(f, "{}", self.name.clone())?
|
||||
};
|
||||
|
||||
for arg in &self.args {
|
||||
write!(f, " {}", arg)?;
|
||||
}
|
||||
|
||||
write!(f, " : {}", &self.tipo)?;
|
||||
|
||||
for rule in &self.rules {
|
||||
write!(f, "\n{}", rule)?
|
||||
}
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Book {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
for name in &self.names {
|
||||
write!(
|
||||
f,
|
||||
"{}\n",
|
||||
self.entrs.get(&Qualified::from_str(name)).unwrap()
|
||||
)?;
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
impl Localized for Rule {
|
||||
fn get_origin(&self) -> Span {
|
||||
self.orig
|
||||
}
|
||||
|
||||
fn set_origin_file(&mut self, file: FileOffset) {
|
||||
self.orig = self.orig.set_file(file);
|
||||
for pat in &mut self.pats {
|
||||
pat.set_origin_file(file);
|
||||
}
|
||||
self.body.set_origin_file(file);
|
||||
}
|
||||
}
|
||||
|
||||
impl Localized for Entry {
|
||||
fn get_origin(&self) -> Span {
|
||||
self.orig
|
||||
}
|
||||
|
||||
fn set_origin_file(&mut self, file: FileOffset) {
|
||||
self.orig = self.orig.set_file(file);
|
||||
for arg in &mut self.args {
|
||||
arg.set_origin_file(file);
|
||||
}
|
||||
for rule in &mut self.rules {
|
||||
rule.set_origin_file(file);
|
||||
}
|
||||
self.tipo.set_origin_file(file);
|
||||
}
|
||||
}
|
||||
|
||||
impl Localized for Argument {
|
||||
fn get_origin(&self) -> Span {
|
||||
self.orig
|
||||
}
|
||||
|
||||
fn set_origin_file(&mut self, file: FileOffset) {
|
||||
self.tipo.set_origin_file(file);
|
||||
}
|
||||
}
|
113
src/book/name.rs
Normal file
113
src/book/name.rs
Normal file
@ -0,0 +1,113 @@
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct EncodedName(u64);
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub struct Ident(pub String);
|
||||
|
||||
#[derive(Clone, PartialEq, Eq, Hash, Debug)]
|
||||
pub struct Qualified {
|
||||
pub path: Ident,
|
||||
pub name: Ident,
|
||||
}
|
||||
|
||||
impl EncodedName {
|
||||
pub fn u64_to_name(&self) -> String {
|
||||
let mut name = String::new();
|
||||
let mut num = self.0;
|
||||
while num > 0 {
|
||||
let chr = (num % 64) as u8;
|
||||
let chr = match chr {
|
||||
0 => '.',
|
||||
1..=10 => (chr - 1 + b'0') as char,
|
||||
11..=36 => (chr - 11 + b'A') as char,
|
||||
37..=62 => (chr - 37 + b'a') as char,
|
||||
63 => '_',
|
||||
64.. => panic!("impossible character value"),
|
||||
};
|
||||
name.push(chr);
|
||||
num = num / 64;
|
||||
}
|
||||
name.chars().rev().collect()
|
||||
}
|
||||
|
||||
pub fn encode(name: &str) -> EncodedName {
|
||||
fn char_to_u64(chr: char) -> u64 {
|
||||
match chr {
|
||||
'.' => 0,
|
||||
'0'..='9' => 1 + chr as u64 - '0' as u64,
|
||||
'A'..='Z' => 11 + chr as u64 - 'A' as u64,
|
||||
'a'..='z' => 37 + chr as u64 - 'a' as u64,
|
||||
'_' => 63,
|
||||
_ => panic!("Invalid name character."),
|
||||
}
|
||||
}
|
||||
|
||||
let mut num: u64 = 0;
|
||||
for (i, chr) in name.chars().enumerate() {
|
||||
if i < 10 {
|
||||
num = (num << 6) + char_to_u64(chr);
|
||||
}
|
||||
}
|
||||
|
||||
return EncodedName(num);
|
||||
}
|
||||
}
|
||||
|
||||
impl Qualified {
|
||||
#[inline]
|
||||
pub fn new(path: String, name: String) -> Qualified {
|
||||
Qualified {
|
||||
path: Ident(path),
|
||||
name: Ident(name),
|
||||
}
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn new_raw(path: &str, name: &str) -> Qualified {
|
||||
Qualified {
|
||||
path: Ident(path.to_string()),
|
||||
name: Ident(name.to_string()),
|
||||
}
|
||||
}
|
||||
|
||||
#[inline]
|
||||
pub fn from_str(str: &str) -> Qualified {
|
||||
let mut path = str
|
||||
.split(".")
|
||||
.map(|x| x.to_string())
|
||||
.collect::<Vec<String>>();
|
||||
let name = path.pop().unwrap_or("".to_string());
|
||||
Qualified {
|
||||
path: Ident(path.join(".")),
|
||||
name: Ident(name),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn to_string(&self) -> String {
|
||||
format!("{}.{}", self.path, self.name)
|
||||
}
|
||||
|
||||
pub fn encode(&self) -> EncodedName {
|
||||
EncodedName::encode(&self.to_string())
|
||||
}
|
||||
}
|
||||
|
||||
impl Ident {
|
||||
pub fn encode(&self) -> EncodedName {
|
||||
EncodedName::encode(&self.0)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Qualified {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "{}.{}", self.path, self.name)
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Ident {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
write!(f, "{}", self.0)
|
||||
}
|
||||
}
|
22
src/book/new_type.rs
Normal file
22
src/book/new_type.rs
Normal file
@ -0,0 +1,22 @@
|
||||
use crate::book::{Argument, Entry};
|
||||
use crate::book::name::Ident;
|
||||
|
||||
// TODO: indexed types
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct NewType {
|
||||
pub name: Ident,
|
||||
pub pars: Vec<Box<Argument>>,
|
||||
pub ctrs: Vec<Box<Constructor>>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Constructor {
|
||||
pub name: Ident,
|
||||
pub args: Vec<Box<Argument>>,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct Derived {
|
||||
pub path: Ident,
|
||||
pub entr: Entry,
|
||||
}
|
@ -26,9 +26,24 @@ impl Span {
|
||||
Span::Localized(SpanData { start, end, file })
|
||||
}
|
||||
|
||||
#[inline]
|
||||
#[inline]
|
||||
pub fn new_off(start: ByteOffset, end: ByteOffset) -> Span {
|
||||
Span::Localized(SpanData { start, end, file: FileOffset(0) })
|
||||
Span::Localized(SpanData {
|
||||
start,
|
||||
end,
|
||||
file: FileOffset(0),
|
||||
})
|
||||
}
|
||||
|
||||
pub fn set_file(&self, new_file: FileOffset) -> Span {
|
||||
match self {
|
||||
Span::Generated => Span::Generated,
|
||||
Span::Localized(SpanData { start, end, .. }) => Span::Localized(SpanData {
|
||||
start: *start,
|
||||
end: *end,
|
||||
file: new_file,
|
||||
}),
|
||||
}
|
||||
}
|
||||
|
||||
#[inline]
|
||||
@ -47,3 +62,8 @@ impl Span {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub trait Localized {
|
||||
fn get_origin(&self) -> Span;
|
||||
fn set_origin_file(&mut self, file: FileOffset);
|
||||
}
|
257
src/book/term.rs
Normal file
257
src/book/term.rs
Normal file
@ -0,0 +1,257 @@
|
||||
// Module that describes terms and operators
|
||||
// of the language
|
||||
|
||||
use crate::book::name::{Ident, Qualified};
|
||||
use crate::book::span::{Span, Localized, FileOffset};
|
||||
|
||||
use std::ascii;
|
||||
use std::fmt::{Display, Error, Formatter};
|
||||
|
||||
#[derive(Copy, Clone, Debug)]
|
||||
pub enum Operator {
|
||||
Add,
|
||||
Sub,
|
||||
Mul,
|
||||
Div,
|
||||
Mod,
|
||||
And,
|
||||
Or,
|
||||
Xor,
|
||||
Shl,
|
||||
Shr,
|
||||
Ltn,
|
||||
Lte,
|
||||
Eql,
|
||||
Gte,
|
||||
Gtn,
|
||||
Neq,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum Term {
|
||||
Typ { orig: Span },
|
||||
Var { orig: Span, name: Ident },
|
||||
All { orig: Span, name: Ident, tipo: Box<Term>, body: Box<Term> },
|
||||
Lam { orig: Span, name: Ident, body: Box<Term> },
|
||||
App { orig: Span, func: Box<Term>, argm: Box<Term> },
|
||||
Let { orig: Span, name: Ident, expr: Box<Term>, body: Box<Term> },
|
||||
Ann { orig: Span, expr: Box<Term>, tipo: Box<Term> },
|
||||
Sub { orig: Span, name: Ident, indx: u64, redx: u64, expr: Box<Term> },
|
||||
Ctr { orig: Span, name: Qualified, args: Vec<Box<Term>> },
|
||||
Fun { orig: Span, name: Qualified, args: Vec<Box<Term>> },
|
||||
Hlp { orig: Span },
|
||||
U60 { orig: Span },
|
||||
Num { orig: Span, numb: u64 },
|
||||
Op2 { orig: Span, oper: Operator, val0: Box<Term>, val1: Box<Term> },
|
||||
Hol { orig: Span, numb: u64 },
|
||||
Mat { orig: Span, tipo: Qualified, name: Ident, expr: Box<Term>, cses: Vec<(Ident,Box<Term>)>, moti: Box<Term> },
|
||||
}
|
||||
|
||||
impl Term {
|
||||
pub fn interpret_as_string(&self) -> Option<String> {
|
||||
let mut text = String::new();
|
||||
let mut term = self;
|
||||
|
||||
let string_nil = Qualified::from_str("String.nil");
|
||||
let string_cons = Qualified::from_str("String.cons");
|
||||
|
||||
loop {
|
||||
if let Term::Ctr { name, args, .. } = term {
|
||||
if *name == string_cons && args.len() == 2 {
|
||||
if let Term::Num { numb, .. } = *args[0] {
|
||||
if ascii::escape_default(numb as u8).count() > 1 {
|
||||
return None;
|
||||
} else {
|
||||
text.push(char::from_u32(numb as u32).unwrap_or('\0'));
|
||||
term = &*args[1];
|
||||
continue;
|
||||
}
|
||||
} else {
|
||||
return None;
|
||||
}
|
||||
} else if *name == string_nil && args.len() == 0 {
|
||||
return Some(text);
|
||||
}
|
||||
}
|
||||
return None;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Display for Operator {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
use Operator::*;
|
||||
|
||||
match self {
|
||||
Add => write!(f, "*"),
|
||||
Sub => write!(f, "-"),
|
||||
Mul => write!(f, "*"),
|
||||
Div => write!(f, "/"),
|
||||
Mod => write!(f, "%"),
|
||||
And => write!(f, "&"),
|
||||
Or => write!(f, "|"),
|
||||
Xor => write!(f, "^"),
|
||||
Shl => write!(f, "<<"),
|
||||
Shr => write!(f, ">>"),
|
||||
Ltn => write!(f, "<"),
|
||||
Lte => write!(f, "<="),
|
||||
Eql => write!(f, "=="),
|
||||
Gte => write!(f, ">="),
|
||||
Gtn => write!(f, ">"),
|
||||
Neq => write!(f, "!="),
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
impl Display for Term {
|
||||
fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error> {
|
||||
if let Some(str) = self.interpret_as_string() {
|
||||
write!(f, "\"{}\"", str)
|
||||
} else {
|
||||
use Term::*;
|
||||
match self {
|
||||
Typ { orig: _ } =>
|
||||
write!(f, "Type"),
|
||||
Hlp { orig: _ } =>
|
||||
write!(f, "?"),
|
||||
U60 { orig: _ } =>
|
||||
write!(f, "U60"),
|
||||
Hol { orig: _, .. } =>
|
||||
write!(f, "_"),
|
||||
Var { orig: _, name } =>
|
||||
write!(f, "{}", name),
|
||||
Num { orig: _, numb } =>
|
||||
write!(f, "{}", numb),
|
||||
Lam { orig: _, name, body } =>
|
||||
write!(f, "({} => {})", name, body),
|
||||
Ann { orig: _, expr, tipo } =>
|
||||
write!(f, "({} :: {})", expr, tipo),
|
||||
Op2 { orig: _, oper, val0, val1 } =>
|
||||
write!(f, "({} {} {})", oper, val0, val1),
|
||||
All { orig: _, name, tipo, body } =>
|
||||
write!(f, "(({}: {}) {})", name, tipo, body),
|
||||
Let { orig: _, name, expr, body } =>
|
||||
write!(f, "(let {} = {}; {})", name, expr, body),
|
||||
Sub { orig: _, name, indx: _, redx, expr } =>
|
||||
write!(f, "({} ## {}/{})", expr, name, redx),
|
||||
Ctr { orig: _, name, args } =>
|
||||
write!(f, "({}{})", name, args.iter().map(|x| format!(" {}", x)).collect::<String>()),
|
||||
Fun { orig: _, name, args } =>
|
||||
write!(f, "({}{})", name, args.iter().map(|x| format!(" {}", x)).collect::<String>()),
|
||||
App { func, argm, .. } => {
|
||||
let mut args = vec![argm];
|
||||
let mut expr = func;
|
||||
while let App { func, argm, .. } = &**expr {
|
||||
args.push(argm);
|
||||
expr = func;
|
||||
}
|
||||
args.reverse();
|
||||
write!(f, "({} {})", expr, args.iter().map(|x| format!("{}", x)).collect::<Vec<String>>().join(" "))
|
||||
}
|
||||
Mat { .. } => panic!("Internal Error: Cannot display a Term::Mat because it's removed after adjust.")
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl Localized for Term {
|
||||
fn get_origin(&self) -> Span {
|
||||
use Term::*;
|
||||
match self {
|
||||
Typ { orig } => *orig,
|
||||
Hlp { orig } => *orig,
|
||||
U60 { orig } => *orig,
|
||||
Hol { orig, .. } => *orig,
|
||||
Var { orig, .. } => *orig,
|
||||
Num { orig, .. } => *orig,
|
||||
Lam { orig, .. } => *orig,
|
||||
Ann { orig, .. } => *orig,
|
||||
Op2 { orig, .. } => *orig,
|
||||
All { orig, .. } => *orig,
|
||||
Let { orig, .. } => *orig,
|
||||
Sub { orig, .. } => *orig,
|
||||
Ctr { orig, .. } => *orig,
|
||||
Fun { orig, .. } => *orig,
|
||||
App { orig, .. } => *orig,
|
||||
Mat { orig, .. } => *orig
|
||||
}
|
||||
}
|
||||
|
||||
fn set_origin_file(&mut self, file: FileOffset) {
|
||||
use Term::*;
|
||||
match self {
|
||||
Typ { orig } => {
|
||||
*orig = orig.set_file(file);
|
||||
}
|
||||
Hlp { orig } => {
|
||||
*orig = orig.set_file(file);
|
||||
}
|
||||
U60 { orig } => {
|
||||
*orig = orig.set_file(file);
|
||||
}
|
||||
Hol { orig, .. } => {
|
||||
*orig = orig.set_file(file);
|
||||
}
|
||||
Var { orig, .. } => {
|
||||
*orig = orig.set_file(file);
|
||||
}
|
||||
Num { orig, .. } => {
|
||||
*orig = orig.set_file(file);
|
||||
}
|
||||
Lam { orig, body, .. } => {
|
||||
*orig = orig.set_file(file);
|
||||
body.set_origin_file(file);
|
||||
}
|
||||
Ann { orig, expr, tipo } => {
|
||||
*orig = orig.set_file(file);
|
||||
expr.set_origin_file(file);
|
||||
tipo.set_origin_file(file);
|
||||
}
|
||||
Op2 { orig, oper:_, val0, val1 } => {
|
||||
*orig = orig.set_file(file);
|
||||
val0.set_origin_file(file);
|
||||
val1.set_origin_file(file);
|
||||
}
|
||||
All { orig, name:_, tipo, body } => {
|
||||
*orig = orig.set_file(file);
|
||||
tipo.set_origin_file(file);
|
||||
body.set_origin_file(file);
|
||||
}
|
||||
Let { orig, name:_, expr, body } => {
|
||||
*orig = orig.set_file(file);
|
||||
expr.set_origin_file(file);
|
||||
body.set_origin_file(file);
|
||||
}
|
||||
Sub { orig, name:_, indx:_, redx:_, expr } => {
|
||||
*orig = orig.set_file(file);
|
||||
expr.set_origin_file(file);
|
||||
}
|
||||
Ctr { orig, name:_, args } => {
|
||||
*orig = orig.set_file(file);
|
||||
for arg in args {
|
||||
arg.set_origin_file(file);
|
||||
}
|
||||
}
|
||||
Fun { orig, name:_, args } => {
|
||||
*orig = orig.set_file(file);
|
||||
for arg in args {
|
||||
arg.set_origin_file(file);
|
||||
}
|
||||
}
|
||||
App { orig, func, argm } => {
|
||||
*orig = orig.set_file(file);
|
||||
func.set_origin_file(file);
|
||||
argm.set_origin_file(file);
|
||||
}
|
||||
Mat { orig, tipo:_, name:_, expr, cses, moti } => {
|
||||
*orig = orig.set_file(file);
|
||||
expr.set_origin_file(file);
|
||||
for cse in cses {
|
||||
cse.1.set_origin_file(file);
|
||||
}
|
||||
moti.set_origin_file(file);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
399
src/lowering/adjust.rs
Normal file
399
src/lowering/adjust.rs
Normal file
@ -0,0 +1,399 @@
|
||||
use crate::book::name::{Ident, Qualified};
|
||||
use crate::book::new_type::NewType;
|
||||
use crate::book::span::{Localized, Span};
|
||||
use crate::book::term::Term;
|
||||
use crate::book::Book;
|
||||
|
||||
use crate::parser::new_type::read_newtype;
|
||||
|
||||
use std::collections::HashMap;
|
||||
use std::rc::Rc;
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub struct AdjustError {
|
||||
pub orig: Span,
|
||||
pub kind: AdjustErrorKind,
|
||||
}
|
||||
|
||||
#[derive(Clone, Debug)]
|
||||
pub enum AdjustErrorKind {
|
||||
IncorrectArity,
|
||||
UnboundVariable { name: String },
|
||||
RepeatedVariable,
|
||||
CantLoadType,
|
||||
NoCoverage,
|
||||
}
|
||||
|
||||
// The state that adjusts uses and update a term, book, rule or entry.
|
||||
pub struct AdjustState<'a> {
|
||||
// The book that we are adjusting now.
|
||||
book: &'a Book,
|
||||
// If we are in the right hand side of a rule.
|
||||
rhs: bool,
|
||||
// TODO:
|
||||
eras: u64,
|
||||
// How much holes we created
|
||||
holes: u64,
|
||||
// All the vars that are bound in the context.
|
||||
vars: Vec<Ident>,
|
||||
// Definitions of types that are useful to the
|
||||
// "match" expression.
|
||||
types: HashMap<Qualified, Rc<NewType>>,
|
||||
}
|
||||
|
||||
trait Adjust {
|
||||
fn adjust<'a>(&self, state: &mut AdjustState<'a>) -> Result<Self, AdjustError>
|
||||
where
|
||||
Self: Sized;
|
||||
|
||||
fn adjust_with_book<'a>(&self, book: &'a Book) -> Result<Self, AdjustError>
|
||||
where
|
||||
Self: Sized,
|
||||
{
|
||||
self.adjust(&mut AdjustState {
|
||||
book,
|
||||
rhs: false,
|
||||
eras: 0,
|
||||
holes: 0,
|
||||
vars: Vec::new(),
|
||||
types: HashMap::new(),
|
||||
})
|
||||
}
|
||||
}
|
||||
|
||||
// TODO: Remove this from the adjust layer. I think that we need to move it
|
||||
// to the driver.
|
||||
fn load_newtype(name: &Qualified) -> Result<Box<NewType>, String> {
|
||||
let path = format!("{}/_.type", name.to_string().replace(".", "/"));
|
||||
let newcode = match std::fs::read_to_string(&path) {
|
||||
Err(_) => {
|
||||
return Err(format!("File not found: '{}'.", path));
|
||||
}
|
||||
Ok(code) => code,
|
||||
};
|
||||
let newtype = match read_newtype(&newcode) {
|
||||
Err(err) => {
|
||||
return Err(format!("\x1b[1m[{}]\x1b[0m\n{}", path, err));
|
||||
}
|
||||
Ok(book) => book,
|
||||
};
|
||||
return Ok(newtype);
|
||||
}
|
||||
|
||||
pub fn load_newtype_cached(
|
||||
cache: &mut HashMap<Qualified, Rc<NewType>>,
|
||||
name: &Qualified,
|
||||
) -> Result<Rc<NewType>, String> {
|
||||
if !cache.contains_key(name) {
|
||||
let newtype = Rc::new(*load_newtype(name)?);
|
||||
cache.insert(name.clone(), newtype);
|
||||
}
|
||||
return Ok(cache.get(name).unwrap().clone());
|
||||
}
|
||||
|
||||
impl Adjust for Term {
|
||||
fn adjust<'a>(&self, state: &mut AdjustState<'a>) -> Result<Self, AdjustError> {
|
||||
match *self {
|
||||
Term::Typ { orig } => Ok(Term::Typ { orig }),
|
||||
Term::Var { ref orig, ref name } => {
|
||||
let orig = *orig;
|
||||
if state.rhs && state.vars.iter().find(|&x| x == name).is_none() {
|
||||
return Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::UnboundVariable {
|
||||
name: name.to_string(),
|
||||
},
|
||||
});
|
||||
} else if !state.rhs && state.vars.iter().find(|&x| x == name).is_some() {
|
||||
return Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::RepeatedVariable,
|
||||
});
|
||||
} else if !state.rhs {
|
||||
state.vars.push(name.clone());
|
||||
}
|
||||
Ok(Term::Var {
|
||||
orig,
|
||||
name: name.clone(),
|
||||
})
|
||||
}
|
||||
Term::Let {
|
||||
ref orig,
|
||||
ref name,
|
||||
ref expr,
|
||||
ref body,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(expr.adjust(state)?);
|
||||
state.vars.push(name.clone());
|
||||
let body = Box::new(body.adjust(state)?);
|
||||
state.vars.pop();
|
||||
Ok(Term::Let {
|
||||
orig,
|
||||
name: name.clone(),
|
||||
expr,
|
||||
body,
|
||||
})
|
||||
}
|
||||
Term::Ann {
|
||||
ref orig,
|
||||
ref expr,
|
||||
ref tipo,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(expr.adjust(state)?);
|
||||
let tipo = Box::new(tipo.adjust(state)?);
|
||||
Ok(Term::Ann { orig, expr, tipo })
|
||||
}
|
||||
Term::Sub {
|
||||
ref orig,
|
||||
ref name,
|
||||
indx: _,
|
||||
ref redx,
|
||||
ref expr,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
let expr = Box::new(expr.adjust(state)?);
|
||||
match state.vars.iter().position(|x| x == name) {
|
||||
None => {
|
||||
return Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::UnboundVariable {
|
||||
name: name.to_string(),
|
||||
},
|
||||
});
|
||||
}
|
||||
Some(indx) => {
|
||||
let name = name.clone();
|
||||
let indx = indx as u64;
|
||||
let redx = *redx;
|
||||
Ok(Term::Sub {
|
||||
orig,
|
||||
name,
|
||||
indx,
|
||||
redx,
|
||||
expr,
|
||||
})
|
||||
}
|
||||
}
|
||||
}
|
||||
Term::All {
|
||||
ref orig,
|
||||
ref name,
|
||||
ref tipo,
|
||||
ref body,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
let tipo = Box::new(tipo.adjust(state)?);
|
||||
state.vars.push(name.clone());
|
||||
let body = Box::new(body.adjust(state)?);
|
||||
state.vars.pop();
|
||||
Ok(Term::All {
|
||||
orig,
|
||||
name: name.clone(),
|
||||
tipo,
|
||||
body,
|
||||
})
|
||||
}
|
||||
Term::Lam {
|
||||
ref orig,
|
||||
ref name,
|
||||
ref body,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
state.vars.push(name.clone());
|
||||
let body = Box::new(body.adjust(state)?);
|
||||
state.vars.pop();
|
||||
Ok(Term::Lam {
|
||||
orig,
|
||||
name: name.clone(),
|
||||
body,
|
||||
})
|
||||
}
|
||||
Term::App {
|
||||
ref orig,
|
||||
ref func,
|
||||
ref argm,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
let func = Box::new(func.adjust(state)?);
|
||||
let argm = Box::new(argm.adjust(state)?);
|
||||
Ok(Term::App { orig, func, argm })
|
||||
}
|
||||
Term::Ctr {
|
||||
ref orig,
|
||||
ref name,
|
||||
ref args,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
if let Some(entry) = state.book.entrs.get(name) {
|
||||
let mut new_args = Vec::new();
|
||||
for arg in args {
|
||||
// On lhs, switch holes for vars
|
||||
if let (false, Term::Hol { orig, numb: _ }) = (state.rhs, &**arg) {
|
||||
let name = format!("x{}_", state.eras);
|
||||
state.eras = state.eras + 1;
|
||||
let arg = Box::new(Term::Var {
|
||||
orig: *orig,
|
||||
name: Ident(name),
|
||||
});
|
||||
new_args.push(Box::new(arg.adjust(state)?));
|
||||
} else {
|
||||
new_args.push(Box::new(arg.adjust(state)?));
|
||||
}
|
||||
}
|
||||
let (hiddens, eraseds) = entry.count_implicits();
|
||||
// Fill implicit arguments (on rhs)
|
||||
if state.rhs && args.len() == entry.args.len() - hiddens {
|
||||
new_args.reverse();
|
||||
let mut aux_args = Vec::new();
|
||||
for arg in &entry.args {
|
||||
if arg.hide {
|
||||
let numb = state.holes;
|
||||
state.holes = state.holes + 1;
|
||||
aux_args.push(Box::new(Term::Hol { orig, numb }));
|
||||
} else {
|
||||
aux_args.push(new_args.pop().unwrap());
|
||||
}
|
||||
}
|
||||
new_args = aux_args;
|
||||
}
|
||||
// Fill erased arguments (on lhs)
|
||||
if !state.rhs && args.len() == entry.args.len() - eraseds {
|
||||
new_args.reverse();
|
||||
let mut aux_args = Vec::new();
|
||||
for arg in &entry.args {
|
||||
if arg.eras {
|
||||
let name = format!("{}{}_", arg.name, state.eras);
|
||||
state.eras = state.eras + 1;
|
||||
let arg = Term::Var {
|
||||
orig: orig,
|
||||
name: Ident(name),
|
||||
};
|
||||
aux_args.push(Box::new(arg.adjust(state)?));
|
||||
} else {
|
||||
aux_args.push(new_args.pop().unwrap());
|
||||
}
|
||||
}
|
||||
new_args = aux_args;
|
||||
}
|
||||
if new_args.len() != entry.args.len() {
|
||||
Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::IncorrectArity,
|
||||
})
|
||||
} else if entry.rules.len() > 0 {
|
||||
Ok(Term::Fun {
|
||||
orig,
|
||||
name: name.clone(),
|
||||
args: new_args,
|
||||
})
|
||||
} else {
|
||||
Ok(Term::Ctr {
|
||||
orig,
|
||||
name: name.clone(),
|
||||
args: new_args,
|
||||
})
|
||||
}
|
||||
} else {
|
||||
return Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::UnboundVariable {
|
||||
name: name.to_string(),
|
||||
},
|
||||
});
|
||||
}
|
||||
}
|
||||
Term::Fun { .. } => {
|
||||
panic!("Internal error."); // shouldn't happen since we can't parse Fun{}
|
||||
}
|
||||
Term::Hol { ref orig, numb: _ } => {
|
||||
let orig = *orig;
|
||||
let numb = state.holes;
|
||||
state.holes = state.holes + 1;
|
||||
Ok(Term::Hol { orig, numb })
|
||||
}
|
||||
Term::Hlp { ref orig } => {
|
||||
let orig = *orig;
|
||||
Ok(Term::Hlp { orig })
|
||||
}
|
||||
Term::U60 { ref orig } => {
|
||||
let orig = *orig;
|
||||
Ok(Term::U60 { orig })
|
||||
}
|
||||
Term::Num { ref orig, ref numb } => {
|
||||
let orig = *orig;
|
||||
let numb = *numb;
|
||||
Ok(Term::Num { orig, numb })
|
||||
}
|
||||
Term::Op2 {
|
||||
ref orig,
|
||||
ref oper,
|
||||
ref val0,
|
||||
ref val1,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
let oper = *oper;
|
||||
let val0 = Box::new(val0.adjust(state)?);
|
||||
let val1 = Box::new(val1.adjust(state)?);
|
||||
Ok(Term::Op2 {
|
||||
orig,
|
||||
oper,
|
||||
val0,
|
||||
val1,
|
||||
})
|
||||
}
|
||||
Term::Mat {
|
||||
ref orig,
|
||||
ref name,
|
||||
ref tipo,
|
||||
ref expr,
|
||||
ref cses,
|
||||
ref moti,
|
||||
} => {
|
||||
let orig = *orig;
|
||||
if let Ok(newtype) = load_newtype_cached(&mut state.types, tipo) {
|
||||
let mut args = vec![];
|
||||
args.push(expr.clone());
|
||||
args.push(Box::new(Term::Lam {
|
||||
orig: moti.get_origin(),
|
||||
name: name.clone(),
|
||||
body: moti.clone(),
|
||||
}));
|
||||
|
||||
if newtype.ctrs.len() != cses.len() {
|
||||
return Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::NoCoverage,
|
||||
});
|
||||
}
|
||||
|
||||
for ctr in &newtype.ctrs {
|
||||
if let Some(cse) = cses.iter().find(|x| x.0 == ctr.name) {
|
||||
let mut case_term = cse.1.clone();
|
||||
for arg in ctr.args.iter().rev() {
|
||||
case_term = Box::new(Term::Lam {
|
||||
orig: case_term.get_origin(),
|
||||
name: Ident(format!("{}.{}", name, arg.name)),
|
||||
body: case_term,
|
||||
});
|
||||
}
|
||||
args.push(case_term);
|
||||
} else {
|
||||
return Err(AdjustError {
|
||||
orig,
|
||||
kind: AdjustErrorKind::NoCoverage,
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
let result = Term::Ctr { orig, name: Qualified::new_raw(&tipo.to_string(), "match"), args };
|
||||
|
||||
result.adjust(state)
|
||||
} else {
|
||||
Err(AdjustError { orig, kind: AdjustErrorKind::CantLoadType })
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
1
src/lowering/mod.rs
Normal file
1
src/lowering/mod.rs
Normal file
@ -0,0 +1 @@
|
||||
pub mod adjust;
|
13
src/main.rs
Normal file
13
src/main.rs
Normal file
@ -0,0 +1,13 @@
|
||||
pub mod log;
|
||||
|
||||
pub mod book;
|
||||
|
||||
pub mod parser;
|
||||
|
||||
pub mod lowering;
|
||||
|
||||
use crate::log::init_logger;
|
||||
|
||||
fn main() {
|
||||
init_logger("").unwrap();
|
||||
}
|
@ -1,14 +1,18 @@
|
||||
use hvm::parser;
|
||||
use std::collections::HashMap;
|
||||
|
||||
use kind2_book::name::{Ident, Qualified};
|
||||
use kind2_book::span::{ByteOffset, Span};
|
||||
use kind2_book::term::Term;
|
||||
use kind2_book::{Argument, Book, Entry, Rule};
|
||||
|
||||
pub mod term;
|
||||
|
||||
use crate::term::*;
|
||||
pub mod new_type;
|
||||
|
||||
pub mod utils;
|
||||
|
||||
use crate::book::name::{Ident, Qualified};
|
||||
use crate::book::span::{ByteOffset, Span};
|
||||
use crate::book::term::Term;
|
||||
use crate::book::{Argument, Book, Entry, Rule};
|
||||
use crate::parser::term::{parse_apps, parse_term};
|
||||
use crate::parser::utils::{get_init_index, get_last_index};
|
||||
|
||||
use hvm::parser;
|
||||
use std::collections::HashMap;
|
||||
|
||||
pub fn parse_rule(
|
||||
state: parser::State,
|
||||
@ -72,7 +76,7 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
|
||||
for arg in &args {
|
||||
pats.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident(arg.name.clone()),
|
||||
name: arg.name.clone(),
|
||||
})); // TODO: set orig
|
||||
}
|
||||
let rules = vec![Box::new(Rule {
|
||||
@ -121,6 +125,7 @@ pub fn parse_entry(state: parser::State) -> parser::Answer<Box<Entry>> {
|
||||
}
|
||||
|
||||
pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
|
||||
let (state, init) = get_init_index(state)?;
|
||||
let (state, eras) = parser::text("-", state)?;
|
||||
let (state, keep) = parser::text("+", state)?;
|
||||
let (state, next) = parser::peek_char(state)?;
|
||||
@ -141,12 +146,15 @@ pub fn parse_argument(state: parser::State) -> parser::Answer<Box<Argument>> {
|
||||
let (state, _) = parser::consume(close, state)?;
|
||||
let hide = open == "<";
|
||||
let eras = if hide { !keep } else { eras };
|
||||
let (state, last) = get_last_index(state)?;
|
||||
let orig = Span::new_off(init, last);
|
||||
return Ok((
|
||||
state,
|
||||
Box::new(Argument {
|
||||
hide,
|
||||
orig,
|
||||
eras,
|
||||
name,
|
||||
name: Ident(name),
|
||||
tipo,
|
||||
}),
|
||||
));
|
311
src/parser/new_type.rs
Normal file
311
src/parser/new_type.rs
Normal file
@ -0,0 +1,311 @@
|
||||
use crate::book::name::Ident;
|
||||
use crate::book::name::Qualified;
|
||||
use crate::book::new_type::{Constructor, Derived, NewType};
|
||||
use crate::book::span::Span;
|
||||
use crate::book::term::Term;
|
||||
use crate::book::{Argument, Entry, Rule};
|
||||
use crate::parser::*;
|
||||
|
||||
pub fn derive_type(tipo: &NewType) -> Derived {
|
||||
let path = format!("{}/_.kind2", tipo.name.0.replace(".", "/"));
|
||||
let name = format!("{}", tipo.name);
|
||||
let kdln = None;
|
||||
let mut args = vec![];
|
||||
for par in &tipo.pars {
|
||||
args.push(Box::new(Argument {
|
||||
hide: false,
|
||||
orig: Span::Generated,
|
||||
eras: false,
|
||||
name: par.name.clone(),
|
||||
tipo: par.tipo.clone(),
|
||||
}));
|
||||
}
|
||||
let tipo = Box::new(Term::Typ {
|
||||
orig: Span::Generated,
|
||||
});
|
||||
let rules = vec![];
|
||||
let entr = Entry {
|
||||
name: Qualified::from_str(&name),
|
||||
orig: Span::Generated,
|
||||
kdln,
|
||||
args,
|
||||
tipo,
|
||||
rules,
|
||||
};
|
||||
return Derived { path: Ident(path), entr };
|
||||
}
|
||||
|
||||
pub fn derive_ctr(tipo: &NewType, index: usize) -> Derived {
|
||||
if let Some(ctr) = tipo.ctrs.get(index) {
|
||||
let path = format!("{}/{}.kind2", tipo.name.0.replace(".", "/"), ctr.name);
|
||||
let name = format!("{}.{}", tipo.name, ctr.name);
|
||||
let kdln = None;
|
||||
let mut args = vec![];
|
||||
for arg in &tipo.pars {
|
||||
args.push(arg.clone());
|
||||
}
|
||||
for arg in &ctr.args {
|
||||
args.push(arg.clone());
|
||||
}
|
||||
let tipo = Box::new(Term::Ctr {
|
||||
orig: Span::Generated,
|
||||
name: Qualified::from_str(&tipo.name.0),
|
||||
args: tipo
|
||||
.pars
|
||||
.iter()
|
||||
.map(|x| {
|
||||
Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: x.name.clone(),
|
||||
})
|
||||
})
|
||||
.collect(),
|
||||
});
|
||||
let rules = vec![];
|
||||
let entr = Entry {
|
||||
name: Qualified::from_str(&name),
|
||||
orig: Span::Generated,
|
||||
kdln,
|
||||
args,
|
||||
tipo,
|
||||
rules,
|
||||
};
|
||||
return Derived { path: Ident(path), entr };
|
||||
} else {
|
||||
panic!("Constructor out of bounds.");
|
||||
}
|
||||
}
|
||||
|
||||
pub fn derive_match(ntyp: &NewType) -> Derived {
|
||||
// type List <t: Type> { nil cons (head: t) (tail: (List t)) }
|
||||
// -----------------------------------------------------------
|
||||
// List.match <t: Type> (x: (List t)) -(p: (List t) -> Type) (nil: (p (List.nil t))) (cons: (head: t) (tail: (List t)) (p (List.cons t head tail))) : (p x)
|
||||
// List.match t (List.nil t) p nil cons = nil
|
||||
// List.match t (List.cons t head tail) p nil cons = (cons head tail)
|
||||
|
||||
let path = format!("{}/match.kind2", ntyp.name.0.replace(".", "/"));
|
||||
|
||||
fn gen_type_ctr(ntyp: &NewType) -> Box<Term> {
|
||||
Box::new(Term::Ctr {
|
||||
orig: Span::Generated,
|
||||
name: Qualified::from_str(&ntyp.name.0),
|
||||
args: ntyp
|
||||
.pars
|
||||
.iter()
|
||||
.map(|x| {
|
||||
Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: x.name.clone(),
|
||||
})
|
||||
})
|
||||
.collect(),
|
||||
})
|
||||
}
|
||||
|
||||
fn gen_ctr_value(ntyp: &NewType, ctr: &Box<Constructor>, _: usize, suffix: &str) -> Box<Term> {
|
||||
let mut ctr_value_args = vec![];
|
||||
for par in &ntyp.pars {
|
||||
ctr_value_args.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident(format!("{}{}", par.name, suffix)),
|
||||
}));
|
||||
}
|
||||
for fld in &ctr.args {
|
||||
ctr_value_args.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident(format!("{}{}", fld.name, suffix)),
|
||||
}));
|
||||
}
|
||||
let ctr_value = Box::new(Term::Ctr {
|
||||
orig: Span::Generated,
|
||||
name: Qualified::new_raw(&ntyp.name.0, &ctr.name.0),
|
||||
args: ctr_value_args,
|
||||
});
|
||||
return ctr_value;
|
||||
}
|
||||
|
||||
// List.match
|
||||
let name = Qualified::new_raw(&ntyp.name.0, "match");
|
||||
let kdln = None;
|
||||
|
||||
let mut args = vec![];
|
||||
|
||||
// <t: Type>
|
||||
for par in &ntyp.pars {
|
||||
args.push(Box::new(Argument {
|
||||
hide: true,
|
||||
orig: Span::Generated,
|
||||
eras: true,
|
||||
name: par.name.clone(),
|
||||
tipo: par.tipo.clone(),
|
||||
}));
|
||||
}
|
||||
|
||||
// (x: (List t))
|
||||
args.push(Box::new(Argument {
|
||||
eras: false,
|
||||
orig: Span::Generated,
|
||||
hide: false,
|
||||
name: Ident("x".to_string()),
|
||||
tipo: gen_type_ctr(ntyp),
|
||||
}));
|
||||
|
||||
// -(p: (List t) -> Type)
|
||||
args.push(Box::new(Argument {
|
||||
eras: true,
|
||||
orig: Span::Generated,
|
||||
hide: false,
|
||||
name: Ident("p".to_string()),
|
||||
tipo: Box::new(Term::All {
|
||||
orig: Span::Generated,
|
||||
name: Ident("x".to_string()),
|
||||
tipo: gen_type_ctr(ntyp),
|
||||
body: Box::new(Term::Typ {
|
||||
orig: Span::Generated,
|
||||
}),
|
||||
}),
|
||||
}));
|
||||
|
||||
// (nil: (p (List.nil t)))
|
||||
// (cons: (head t) (tail: (List t)) (p (List.cons t head tail)))
|
||||
for ctr in &ntyp.ctrs {
|
||||
fn ctr_case_type(ntyp: &NewType, ctr: &Box<Constructor>, index: usize) -> Box<Term> {
|
||||
if index < ctr.args.len() {
|
||||
// for nil = ...
|
||||
// for cons = (head: t) (tail: (List t))
|
||||
let arg = ctr.args.get(index).unwrap();
|
||||
return Box::new(Term::All {
|
||||
orig: Span::Generated,
|
||||
name: arg.name.clone(),
|
||||
tipo: arg.tipo.clone(),
|
||||
body: ctr_case_type(ntyp, ctr, index + 1),
|
||||
});
|
||||
} else {
|
||||
// for nil = (p (List.nil t))
|
||||
// for cons = (p (List.cons t head tail))
|
||||
return Box::new(Term::App {
|
||||
orig: Span::Generated,
|
||||
func: Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident("p".to_string()),
|
||||
}),
|
||||
argm: gen_ctr_value(ntyp, ctr, index, ""),
|
||||
});
|
||||
}
|
||||
}
|
||||
args.push(Box::new(Argument {
|
||||
eras: false,
|
||||
orig: Span::Generated,
|
||||
hide: false,
|
||||
name: ctr.name.clone(),
|
||||
tipo: ctr_case_type(ntyp, &ctr, 0),
|
||||
}));
|
||||
}
|
||||
|
||||
// : (p x)
|
||||
let tipo = Box::new(Term::App {
|
||||
orig: Span::Generated,
|
||||
func: Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident("p".to_string()),
|
||||
}),
|
||||
argm: Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident("x".to_string()),
|
||||
}),
|
||||
});
|
||||
|
||||
// List.match t (List.nil t) p nil cons = nil
|
||||
// List.match t (List.cons t head tail) p nil cons = (cons head tail)
|
||||
let mut rules = vec![];
|
||||
|
||||
for idx in 0..ntyp.ctrs.len() {
|
||||
let ctr = &ntyp.ctrs[idx];
|
||||
let orig = Span::Generated;
|
||||
let name = format!("{}.match", ntyp.name);
|
||||
let mut pats = vec![];
|
||||
for par in &ntyp.pars {
|
||||
pats.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: par.name.clone(),
|
||||
}));
|
||||
}
|
||||
pats.push(gen_ctr_value(ntyp, &ctr, idx, "_"));
|
||||
pats.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident("p".to_string()),
|
||||
}));
|
||||
for ctr in &ntyp.ctrs {
|
||||
pats.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: ctr.name.clone(),
|
||||
}));
|
||||
}
|
||||
let mut body_args = vec![];
|
||||
for arg in &ctr.args {
|
||||
body_args.push(Box::new(Term::Var {
|
||||
orig: Span::Generated,
|
||||
name: Ident(format!("{}_", arg.name)),
|
||||
}));
|
||||
}
|
||||
let body = Box::new(Term::Ctr {
|
||||
orig: Span::Generated,
|
||||
name: Qualified::from_str(&ctr.name.0),
|
||||
args: body_args,
|
||||
});
|
||||
rules.push(Box::new(Rule {
|
||||
orig,
|
||||
name: Qualified::from_str(&name),
|
||||
pats,
|
||||
body,
|
||||
}));
|
||||
}
|
||||
|
||||
let entr = Entry {
|
||||
name,
|
||||
orig: Span::Generated,
|
||||
kdln,
|
||||
args,
|
||||
tipo,
|
||||
rules,
|
||||
};
|
||||
|
||||
return Derived { path: Ident(path), entr };
|
||||
}
|
||||
|
||||
pub fn parse_newtype(state: parser::State) -> parser::Answer<Box<NewType>> {
|
||||
let (state, _) = parser::consume("type", state)?;
|
||||
let (state, name) = parser::name1(state)?;
|
||||
let (state, pars) = parser::until(parser::text_parser("{"), Box::new(parse_argument), state)?;
|
||||
let mut ctrs = vec![];
|
||||
let mut state = state;
|
||||
loop {
|
||||
let state_i = state;
|
||||
let (state_i, ctr_name) = parser::name(state_i)?;
|
||||
if ctr_name.len() == 0 {
|
||||
break;
|
||||
}
|
||||
let mut ctr_args = vec![];
|
||||
let mut state_i = state_i;
|
||||
loop {
|
||||
let state_j = state_i;
|
||||
let (state_j, head) = parser::peek_char(state_j)?;
|
||||
if head != '(' {
|
||||
break;
|
||||
}
|
||||
let (state_j, ctr_arg) = parse_argument(state_j)?;
|
||||
ctr_args.push(ctr_arg);
|
||||
state_i = state_j;
|
||||
}
|
||||
ctrs.push(Box::new(Constructor {
|
||||
name: Ident(ctr_name),
|
||||
args: ctr_args,
|
||||
}));
|
||||
state = state_i;
|
||||
}
|
||||
return Ok((state, Box::new(NewType { name: Ident(name), pars, ctrs })));
|
||||
}
|
||||
|
||||
pub fn read_newtype(code: &str) -> Result<Box<NewType>, String> {
|
||||
parser::read(Box::new(parse_newtype), code)
|
||||
}
|
@ -1,21 +1,9 @@
|
||||
use hvm::parser;
|
||||
|
||||
use kind2_book::name::{Ident, Qualified};
|
||||
use kind2_book::span::{ByteOffset, Span};
|
||||
use kind2_book::term::{Operator, Term};
|
||||
|
||||
pub fn is_ctr_head(head: char) -> bool {
|
||||
('A'..='Z').contains(&head)
|
||||
}
|
||||
|
||||
pub fn get_init_index(state: parser::State) -> parser::Answer<ByteOffset> {
|
||||
let (state, _) = parser::skip(state)?;
|
||||
Ok((state, ByteOffset(state.index as u32)))
|
||||
}
|
||||
|
||||
pub fn get_last_index(state: parser::State) -> parser::Answer<ByteOffset> {
|
||||
Ok((state, ByteOffset(state.index as u32)))
|
||||
}
|
||||
use crate::book::name::{Ident, Qualified};
|
||||
use crate::book::span::{ByteOffset, Span};
|
||||
use crate::book::term::{Operator, Term};
|
||||
use crate::parser::utils::{get_init_index, get_last_index, is_ctr_head};
|
||||
|
||||
pub fn parse_var(state: parser::State) -> parser::Answer<Option<Box<Term>>> {
|
||||
parser::guard(
|
16
src/parser/utils.rs
Normal file
16
src/parser/utils.rs
Normal file
@ -0,0 +1,16 @@
|
||||
use hvm::parser;
|
||||
|
||||
use crate::book::span::ByteOffset;
|
||||
|
||||
pub fn is_ctr_head(head: char) -> bool {
|
||||
('A'..='Z').contains(&head)
|
||||
}
|
||||
|
||||
pub fn get_init_index(state: parser::State) -> parser::Answer<ByteOffset> {
|
||||
let (state, _) = parser::skip(state)?;
|
||||
Ok((state, ByteOffset(state.index as u32)))
|
||||
}
|
||||
|
||||
pub fn get_last_index(state: parser::State) -> parser::Answer<ByteOffset> {
|
||||
Ok((state, ByteOffset(state.index as u32)))
|
||||
}
|
Loading…
Reference in New Issue
Block a user