summaryrefslogtreecommitdiff
path: root/src/parser.rs
blob: 917df662430b5025b04306353295bfe54ae156ce (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
use crate::ast::*;

// (λx:T.y): T z
pub fn parse(input: &str) -> Expression {
    return parse_str(input).expect("invalid expression");
}

/// 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 awful
    // 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
                    }
                }
            }
            // fucking awful but i don't know another way
            // k:("empty" / "unit" / etc) returns ()
            // and i can't seem to match and raise a parse error
            // so ¯\_(ツ)_/¯
            rule empty() -> Type = k:"empty" {Type::Empty}
            rule unit() -> Type = k:"unit" {Type::Unit}
            rule boolean() -> Type = k:"bool" {Type::Boolean}
            rule natural() -> Type = k:"nat" {Type::Natural}
            rule integer() -> Type = k:"int" {Type::Integer}
            rule kind() -> Type
             = k:(empty() / unit() / boolean() / natural() / integer()) {
                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)
                }
            }
            // fixme: more cases should parse, but how?
            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"+)
        }
    }
    // assert_eq!(lambda::expression("(λx:bool.x)").unwrap(), lambda::expression("(λx: bool . x)").unwrap());

    return lambda::expression(input.trim());
}

/// Parses a Nim-like language into an AST.
#[allow(unused_variables)]
pub fn parse_file(path: &str) -> Vec<Expression> {
    todo!();
}