also bidirectional typechecking and subtyping
ten slides, five minutes
pub type Value = u8;
pub struct Term {
pub val: Value,
pub kind: Type, // for casting
}
pub type Identifier = String;
pub type Context = HashMap<Identifier, Term>;
#[derive(Clone, PartialEq, Eq)]
pub enum Expression {
Annotation {
expr: Box<Expression>,
kind: Type
},
Constant {
term: Term
},
Variable {
id: Identifier
},
Abstraction {
param: Identifier,
func: Box<Expression>
},
Application {
func: Box<Expression>,
arg: Box<Expression>
},
Conditional {
if_cond: Box<Expression>,
if_then: Box<Expression>,
if_else: Box<Expression>
}
}
pegs are magic
very nice for simple stuff
/// Parses a lambda-calculus-like language into an AST.
pub fn parse_str(input: &str) -> Result<Expression, peg::error::ParseError<peg::str::LineCol>>{
// this is kinda gross
// i miss my nim pegs
peg::parser!{
grammar lambda() for str {
rule identifier() -> String
= i:['a'..='z' | 'A'..='Z' | '0'..='9']+ {
i.iter().collect::<String>()
}
rule constant() -> Expression
= p:"-"? c:['0'..='9']+ {
let value = c.iter().collect::<String>().parse::<Value>().unwrap();
Expression::Constant {
term: Term {
val: if let Some(_) = p {
value.wrapping_neg()
} else {
value
},
kind: Type::Empty
}
}
}
rule primitive() -> Type
= k:$("empty" / "unit" / "bool" / "nat" / "int") {
match k {
"empty" => Type::Empty,
"unit" => Type::Unit,
"bool" => Type::Boolean,
"nat" => Type::Natural,
"int" => Type::Integer,
_ => Type::Empty
}
}
rule function() -> Type = "(" f:kind() " "* "->" " "* t:kind() ")" {
Type::Function { from: Box::new(f), to: Box::new(t) }
}
rule kind() -> Type
= k:(function() / primitive()) {
k
}
rule annotation() -> Expression
= e:(conditional() / abstraction() / application() / constant() / variable()) " "* ":" " "* k:kind() {
Expression::Annotation {
expr: Box::new(e),
kind: k
}
}
rule variable() -> Expression
= v:identifier() {
Expression::Variable {
id: v
}
}
rule abstraction() -> Expression
= ("λ" / "lambda") " "* p:identifier() " "* "." " "* f:expression() {
Expression::Abstraction {
param: p,
func: Box::new(f)
}
}
rule application() -> Expression
= "(" f:(annotation() / abstraction()) ")" " "* a:expression() {
Expression::Application {
func: Box::new(f),
arg: Box::new(a)
}
}
rule conditional() -> Expression
= "if" " "+ c:expression() " "+ "then" " "+ t:expression() " "+ "else" " "+ e:expression() {
Expression::Conditional {
if_cond: Box::new(c),
if_then: Box::new(t),
if_else: Box::new(e)
}
}
pub rule expression() -> Expression
= e:(conditional() / annotation() / abstraction() / application() / constant() / variable()) {
e
}
pub rule ast() -> Vec<Expression>
= expression() ** ("\n"+)
}
}
return lambda::expression(input.trim());
}why did i decide to do this
/// Parses a simple language with bracket-based indentation and end-of-term semicolons.
#[allow(unused_variables)]
pub fn parse_lang(input: &str) -> Result<Vec<Expression>, peg::error::ParseError<peg::str::LineCol>> {
peg::parser! {
grammar puck() for str {
// whitespace
rule w() = ("\n" / " ")+
// todo: multiple parameters pls
rule abs() -> Expression
= "func" w() n:ident() w()? "(" p:ident() ")"
w()? ":" w()? k:function() w() "=" w() "{" w() f:expr() w() "}" {
Expression::Annotation {
expr: Box::new(Expression::Abstraction { param: p, func: Box::new(f) }),
kind: k
}
}
// fixme: this requires, uh, refactoring the ast...
rule app() -> Expression
= f:ident() "(" a:expr() ")" {
Expression::Application {
func: Box::new(Expression::Variable {
id: f
}),
arg: Box::new(a)
}
}
rule cond() -> Expression
= "if" w() c:expr() w() "=" w() "{" w() t:expr() w() "};" w()
"else" w() "=" w() "{" w() e:expr() w() "}" {
Expression::Conditional {
if_cond: Box::new(c),
if_then: Box::new(t),
if_else: Box::new(e)
}
}
// fixme: cannot say e:(expr()), left-recursion issue
rule ann() -> Expression
= e:(cond() / abs() / app() / cons() / var()) w()? ":" w() k:kind() {
Expression::Annotation {
expr: Box::new(e),
kind: k
}
}
// identifiers
rule ident() -> String = i:['a'..='z' | 'A'..='Z' | '0'..='9']+ {
i.iter().collect::<String>()
}
rule var() -> Expression
= v:ident() {
Expression::Variable {
id: v
}
}
// constants
rule cons() -> Expression = p:"-"? c:['0'..='9']+ {
let value = c.iter().collect::<String>().parse::<Value>().unwrap();
Expression::Constant {
term: Term {
val: if let Some(_) = p {
value.wrapping_neg()
} else {
value
},
kind: Type::Empty // fixme
}
}
}
// types
rule primitive() -> Type = k:$("empty" / "unit" / "bool" / "nat" / "int") {
match k {
"empty" => Type::Empty,
"unit" => Type::Unit,
"bool" => Type::Boolean,
"nat" => Type::Natural,
"int" => Type::Integer,
_ => Type::Empty // never happens
}
}
// fixme: parenthesis necessary, left-recursion issue
rule function() -> Type = "(" w()? f:kind() w()? "->" w()? t:kind() w()? ")" {
Type::Function { from: Box::new(f), to: Box::new(t) }
}
// todo: records, etc
rule kind() -> Type
= k:(function() / primitive()) {
k
}
pub rule expr() -> Expression
= e:(ann() / cond() / abs() / app() / cons() / var()) ";" {
e
}
pub rule file() -> Vec<Expression>
= expr() ++ "\n"
}
}
return puck::file(input);
}
func negate(x): (bool -> bool) =
if x: 0
else: 1
func fib(x): (int -> int) =
if eq(x, 0):
0
else:
if eq(x, 1):
1
else: # comment
add(fib(sub(x, 1)),
fib(sub(x, 2)))
negate(negate(1))
fib(5)
/// Converts a whitespace-indented language
/// into a bracketed language for PEG matching.
pub fn lex(input: &str) ->
Result<String, &'static str> {
#[derive(Eq, PartialEq)]
enum Previous {
Start,
Block,
Line,
}
struct State {
blank: bool, // entirely whitespace so far?
level: usize, // current indentation level
count: usize, // current whitespace count
previous: Previous,
comment: bool // current line a comment?
}
let indent_size: usize = 2;
let mut state = State {
blank: true,
level: 0,
count: 0,
previous: Previous::Start,
comment: false
};
let mut buffer = String::new();
let mut result = String::new();
// wow lexers are hard
for c in input.chars() {
match c {
'\n' => {
if !buffer.is_empty() {
if state.count == state.level {
if state.previous !=
Previous::Start {
result.push(';');
result.push('\n');
}
state.previous = Previous::Line;
} else if state.level + indent_size
== state.count {
result.push(' ');
result.push('{');
result.push('\n');
state.level = state.count;
state.previous = Previous::Line;
} else if state.count >
state.level + indent_size {
return Err("invalid indent jump");
} else if state.count % indent_size
!= 0 {
return Err("incorrect indent offset");
} else if state.level > state.count {
while state.level > state.count {
if state.previous ==
Previous::Line {
result.push(';');
}
state.level -= indent_size;
result.push('\n');
result.push_str(
&" ".repeat(state.level));
result.push('}');
result.push(';');
state.previous = Previous::Block;
}
result.push('\n');
} else {
return Err("unknown indentation");
}
result.push_str(
&" ".repeat(state.count));
result.push_str(&buffer);
state.count = 0;
state.comment = false;
buffer.clear();
}
state.blank = true;
},
' ' if state.blank => {
state.count += 1;
},
'#' => {
state.blank = false;
state.comment = true;
},
_ => {
if state.blank {
state.blank = false;
}
if !state.comment {
buffer.push(c);
}
},
}
}
if state.previous == Previous::Line {
result.push(';');
}
while state.level != 0 {
state.level -= 2;
result.push('\n');
result.push_str(&" ".repeat(state.level));
result.push('}');
result.push(';');
}
return Ok(result);
}i now fully appreciate the role of lexers, whitespace and PEGs do *not* mix
/// The subtyping relation between any two types.
pub fn subtype(is: &Type, of: &Type) -> bool {
match (is, of) {
(Type::Record(is_fields), Type::Record(of_fields)) => {
// width, depth, and permutation
for (key, of_value) in of_fields {
match is_fields.get(key) {
Some(is_value) => if !subtype(is_value, of_value) {
return false;
},
None => return false
}
}
return true;
},
(Type::Function { from: is_from, to: is_to },
Type::Function { from: of_from, to: of_to }) => {
subtype(of_from, is_from) && subtype(is_to, of_to)
}
(Type::Natural, Type::Integer) => true, // obviously not, but let's pretend
(_, Type::Empty) => true,
(Type::Error, _) => true,
(_, _) if is == of => true,
(_, _) => false,
}
}
pub type Identifier = String;
pub type Context =
HashMap<Identifier, Term>;
pub type Value = u64;
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Type {
Empty, // top
Error, // bottom
Unit,
Boolean,
Natural,
Integer,
// Float,
// String,
Enum(Vec<Type>),
Record(HashMap<Identifier, Type>),
Function{from: Box<Type>,
to: Box<Type>
},
}
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Term {
pub val: Value,
pub kind: Type,
}
no