Skip to content

Commit

Permalink
RichTerms can now have an optional position
Browse files Browse the repository at this point in the history
  • Loading branch information
teofr committed Sep 18, 2019
1 parent 5ed8118 commit 1e9a495
Show file tree
Hide file tree
Showing 5 changed files with 82 additions and 37 deletions.
5 changes: 4 additions & 1 deletion src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,10 @@ pub fn eval(t0: RichTerm) -> Result<Term, EvalError> {

loop {
let Closure {
body: RichTerm { term: boxed_term },
body: RichTerm {
term: boxed_term,
pos: _,
},
mut env,
} = clos;
let term = *boxed_term;
Expand Down
33 changes: 20 additions & 13 deletions src/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -6,32 +6,39 @@ use label::Label;

grammar;

pub Term: RichTerm = {
"fun" <p:Pattern> "=>" <t:Term> =>
pub Term: RichTerm = SpTerm<RichTerm>;

SpTerm<Rule>: RichTerm =
<l: @L> <t: Rule> <r: @R> => match t {
RichTerm {term: t, pos: _} => RichTerm {term: t, pos: Some((l, r))}
};

RichTerm: RichTerm = {
"fun" <p:Pattern> "=>" <t: SpTerm<Term>> =>
RichTerm::new(Term::Fun(p, t)),
"let" <id:Ident> "=" <t1:Term> "in" <t2:Term> =>
"let" <id:Ident> "=" <t1:SpTerm<Term>> "in" <t2:SpTerm<Term>> =>
RichTerm::new(Term::Let(id, t1, t2)),
"if" <b:Term> "then" <t:Term> "else" <e:Term> =>
"if" <b:SpTerm<Term>> "then" <t:SpTerm<Term>> "else" <e:SpTerm<Term>> =>
RichTerm::app(RichTerm::app(RichTerm::new(Term::Op1(UnaryOp::Ite(), b)), t), e),
Operation
SpTerm<Operation>
};

Operation: RichTerm = {
<t1: Applicative> <op: BOp> <t2: Operation> => RichTerm::new(Term::Op2(op, t1, t2)),
<op: UOp> <t: Operation> => RichTerm::new(Term::Op1(op, t)),
Applicative,
<t1: SpTerm< Applicative>> <op: BOp> <t2: SpTerm<Operation>> => RichTerm::new(Term::Op2(op, t1, t2)),
<op: UOp> <t: SpTerm<Operation>> => RichTerm::new(Term::Op1(op, t)),
SpTerm< Applicative>,
};

Applicative: RichTerm = {
<t1:Applicative> <t2:Atom> => RichTerm::new(Term::App(t1, t2)),
Atom,
<t1:SpTerm< Applicative>> <t2: SpTerm<Atom>> => RichTerm::new(Term::App(t1, t2)),
SpTerm<Atom>,
};

Atom: RichTerm = {
"(" <Term> ")",
<l:@L> "Promise(" <ty: Types> "," <t: Term> ")" <r:@R> =>
"(" <SpTerm<Term>> ")",
<l:@L> "Promise(" <ty: Types> "," <t: SpTerm<Term>> ")" <r:@R> =>
RichTerm::new(Term::Promise(ty, Label{tag: "A promise".to_string(), l: l, r: r}, t)),
<l:@L> "Assume(" <ty: Types> "," <t: Term> ")" <r:@R> =>
<l:@L> "Assume(" <ty: Types> "," <t: SpTerm<Term>> ")" <r:@R> =>
RichTerm::new(Term::Assume(ty, Label{tag: "An assume".to_string(), l: l, r: r}, t)),
Num => RichTerm::new(Term::Num(<>)),
Bool => RichTerm::new(Term::Bool(<>)),
Expand Down
6 changes: 3 additions & 3 deletions src/operation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ fn process_unary_operation(
stack: &mut Stack,
) -> Result<Closure, EvalError> {
let Closure {
body: RichTerm { term: t },
body: RichTerm { term: t, pos: _ },
env: _env,
} = clos;
match u_op {
Expand Down Expand Up @@ -100,11 +100,11 @@ fn process_binary_operation(
_stack: &mut Stack,
) -> Result<Closure, EvalError> {
let Closure {
body: RichTerm { term: t1 },
body: RichTerm { term: t1, pos: _ },
env: _env1,
} = fst_clos;
let Closure {
body: RichTerm { term: t2 },
body: RichTerm { term: t2, pos: _ },
env: _env2,
} = clos;
match b_op {
Expand Down
39 changes: 20 additions & 19 deletions src/parser/tests.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,25 +2,30 @@ use identifier::Ident;
use term::Term::*;
use term::{BinaryOp, RichTerm, UnaryOp};

fn parse_without_pos(s: &str) -> RichTerm {
let parser = super::grammar::TermParser::new();
let mut result = parser.parse(s).unwrap();
result.clean_pos();
result
}

#[test]
fn numbers() {
let parser = super::grammar::TermParser::new();
assert_eq!(parser.parse("22").unwrap(), Num(22.0).into());
assert_eq!(parser.parse("22.0").unwrap(), Num(22.0).into());
assert_eq!(parser.parse("22.22").unwrap(), Num(22.22).into());
assert_eq!(parser.parse("(22)").unwrap(), Num(22.0).into());
assert_eq!(parser.parse("((22))").unwrap(), Num(22.0).into());
assert_eq!(parse_without_pos("22"), Num(22.0).into());
assert_eq!(parse_without_pos("22.0"), Num(22.0).into());
assert_eq!(parse_without_pos("22.22"), Num(22.22).into());
assert_eq!(parse_without_pos("(22)"), Num(22.0).into());
assert_eq!(parse_without_pos("((22))"), Num(22.0).into());
}

#[test]
fn plus() {
let parser = super::grammar::TermParser::new();
assert_eq!(
parser.parse("3 + 4").unwrap(),
parse_without_pos("3 + 4"),
Op2(BinaryOp::Plus(), Num(3.0).into(), Num(4.).into()).into()
);
assert_eq!(
parser.parse("(true + false) + 4").unwrap(),
parse_without_pos("(true + false) + 4"),
Op2(
BinaryOp::Plus(),
Op2(BinaryOp::Plus(), Bool(true).into(), Bool(false).into()).into(),
Expand All @@ -32,16 +37,14 @@ fn plus() {

#[test]
fn booleans() {
let parser = super::grammar::TermParser::new();
assert_eq!(parser.parse("true").unwrap(), Bool(true).into());
assert_eq!(parser.parse("false").unwrap(), Bool(false).into());
assert_eq!(parse_without_pos("true"), Bool(true).into());
assert_eq!(parse_without_pos("false"), Bool(false).into());
}

#[test]
fn ite() {
let parser = super::grammar::TermParser::new();
assert_eq!(
parser.parse("if true then 3 else 4").unwrap(),
parse_without_pos("if true then 3 else 4"),
RichTerm::app(
RichTerm::app(
Op1(UnaryOp::Ite(), Bool(true).into()).into(),
Expand All @@ -54,16 +57,15 @@ fn ite() {

#[test]
fn applications() {
let parser = super::grammar::TermParser::new();
assert_eq!(
parser.parse("1 true 2").unwrap(),
parse_without_pos("1 true 2"),
RichTerm::app(
RichTerm::app(Num(1.0).into(), Bool(true).into()),
Num(2.0).into()
),
);
assert_eq!(
parser.parse("1 (2 3) 4").unwrap(),
parse_without_pos("1 (2 3) 4"),
RichTerm::app(
RichTerm::app(
Num(1.0).into(),
Expand All @@ -83,9 +85,8 @@ fn variables() {

#[test]
fn functions() {
let parser = super::grammar::TermParser::new();
assert_eq!(
parser.parse("fun x => x").unwrap(),
parse_without_pos("fun x => x"),
Fun(Ident("x".into()), RichTerm::var("x".into())).into(),
);
}
Expand Down
36 changes: 35 additions & 1 deletion src/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,30 @@ pub enum Term {
Assume(Types, Label, RichTerm),
}

impl Term {
pub fn apply_to_rich_terms<F>(&mut self, func: F)
where
F: Fn(&mut RichTerm),
{
use self::Term::*;
match self {
Bool(_) | Num(_) | Lbl(_) | Var(_) => {}
Fun(_, ref mut t)
| Op1(_, ref mut t)
| Promise(_, _, ref mut t)
| Assume(_, _, ref mut t) => {
func(t);
}
Let(_, ref mut t1, ref mut t2)
| App(ref mut t1, ref mut t2)
| Op2(_, ref mut t1, ref mut t2) => {
func(t1);
func(t2);
}
}
}
}

#[derive(Clone, Debug, PartialEq)]
pub enum UnaryOp {
Ite(),
Expand All @@ -39,11 +63,21 @@ pub enum BinaryOp {
#[derive(Debug, PartialEq, Clone)]
pub struct RichTerm {
pub term: Box<Term>,
pub pos: Option<(usize, usize)>,
}

impl RichTerm {
pub fn new(t: Term) -> RichTerm {
RichTerm { term: Box::new(t) }
RichTerm {
term: Box::new(t),
pos: None,
}
}

pub fn clean_pos(&mut self) {
self.pos = None;
self.term
.apply_to_rich_terms(|rt: &mut Self| rt.clean_pos());
}

pub fn app(rt1: RichTerm, rt2: RichTerm) -> RichTerm {
Expand Down

0 comments on commit 1e9a495

Please sign in to comment.