Skip to content

Commit

Permalink
Add syntactic support for implicit arguments
Browse files Browse the repository at this point in the history
  • Loading branch information
Stephan Boyer committed Apr 17, 2020
1 parent 5dce53f commit a88dbba
Show file tree
Hide file tree
Showing 11 changed files with 596 additions and 65 deletions.
16 changes: 15 additions & 1 deletion grammar.y
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,11 +33,13 @@
%token IF
%token INTEGER
%token INTEGER_LITERAL
%token LEFT_CURLY
%token LEFT_PAREN
%token LESS_THAN
%token LESS_THAN_OR_EQUAL
%token MINUS
%token PLUS
%token RIGHT_CURLY
%token RIGHT_PAREN
%token SLASH
%token TERMINATOR
Expand All @@ -55,8 +57,11 @@ term: let | jumbo_term;
type: TYPE;
variable: IDENTIFIER;
lambda: IDENTIFIER THICK_ARROW term;
lambda_implicit: LEFT_CURLY IDENTIFIER RIGHT_CURLY THICK_ARROW term;
annotated_lambda: LEFT_PAREN IDENTIFIER COLON jumbo_term RIGHT_PAREN THICK_ARROW term;
annotated_lambda_implicit: LEFT_CURLY IDENTIFIER COLON jumbo_term RIGHT_CURLY THICK_ARROW term;
pi: LEFT_PAREN IDENTIFIER COLON jumbo_term RIGHT_PAREN THIN_ARROW term;
pi_implicit: LEFT_CURLY IDENTIFIER COLON jumbo_term RIGHT_CURLY THIN_ARROW term;
non_dependent_pi: small_term THIN_ARROW term;
application: atom small_term;
let: IDENTIFIER let_annotation EQUALS term TERMINATOR term;
Expand Down Expand Up @@ -90,4 +95,13 @@ giant_term:
greater_than |
greater_than_or_equal_to |
huge_term;
jumbo_term: lambda | annotated_lambda | pi | non_dependent_pi | if | giant_term;
jumbo_term:
lambda |
lambda_implicit |
annotated_lambda |
annotated_lambda_implicit |
pi |
pi_implicit |
non_dependent_pi |
if |
giant_term;
20 changes: 16 additions & 4 deletions src/de_bruijn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -63,18 +63,20 @@ pub fn signed_shift<'a>(term: &Term<'a>, cutoff: usize, amount: isize) -> Option
Some(term.clone())
}
}
Lambda(variable, domain, body) => Some(Term {
Lambda(variable, implicit, domain, body) => Some(Term {
source_range: term.source_range,
variant: Lambda(
variable,
*implicit,
Rc::new(signed_shift(domain, cutoff, amount)?),
Rc::new(signed_shift(body, cutoff + 1, amount)?),
),
}),
Pi(variable, domain, codomain) => Some(Term {
Pi(variable, implicit, domain, codomain) => Some(Term {
source_range: term.source_range,
variant: Pi(
variable,
*implicit,
Rc::new(signed_shift(domain, cutoff, amount)?),
Rc::new(signed_shift(codomain, cutoff + 1, amount)?),
),
Expand Down Expand Up @@ -231,10 +233,11 @@ pub fn open<'a>(
Ordering::Less => term_to_open.clone(),
Ordering::Equal => unsigned_shift(term_to_insert, 0, shift_amount),
},
Lambda(variable, domain, body) => Term {
Lambda(variable, implicit, domain, body) => Term {
source_range: term_to_open.source_range,
variant: Lambda(
variable,
*implicit,
Rc::new(open(domain, index_to_replace, term_to_insert, shift_amount)),
Rc::new(open(
body,
Expand All @@ -244,10 +247,11 @@ pub fn open<'a>(
)),
),
},
Pi(variable, domain, codomain) => Term {
Pi(variable, implicit, domain, codomain) => Term {
source_range: term_to_open.source_range,
variant: Pi(
variable,
*implicit,
Rc::new(open(domain, index_to_replace, term_to_insert, shift_amount)),
Rc::new(open(
codomain,
Expand Down Expand Up @@ -623,6 +627,7 @@ mod tests {
source_range: None,
variant: Lambda(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("b", 0),
Expand All @@ -640,6 +645,7 @@ mod tests {
source_range: None,
variant: Lambda(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("b", 42),
Expand All @@ -661,6 +667,7 @@ mod tests {
source_range: None,
variant: Pi(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("b", 0),
Expand All @@ -678,6 +685,7 @@ mod tests {
source_range: None,
variant: Pi(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("b", 42),
Expand Down Expand Up @@ -1431,6 +1439,7 @@ mod tests {
source_range: None,
variant: Lambda(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("b", 0),
Expand All @@ -1452,6 +1461,7 @@ mod tests {
source_range: None,
variant: Lambda(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("x", 4),
Expand All @@ -1473,6 +1483,7 @@ mod tests {
source_range: None,
variant: Pi(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("b", 0),
Expand All @@ -1494,6 +1505,7 @@ mod tests {
source_range: None,
variant: Pi(
"a",
false,
Rc::new(Term {
source_range: None,
variant: Variable("x", 4),
Expand Down
78 changes: 71 additions & 7 deletions src/equality.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -70,9 +70,13 @@ pub fn syntactically_equal<'a>(term1: &Term<'a>, term2: &Term<'a>) -> bool {
true
}
(Variable(_, index1), Variable(_, index2)) => index1 == index2,
(Lambda(_, _, body1), Lambda(_, _, body2)) => syntactically_equal(body1, body2),
(Pi(_, domain1, codomain1), Pi(_, domain2, codomain2)) => {
syntactically_equal(domain1, domain2) && syntactically_equal(codomain1, codomain2)
(Lambda(_, implicit1, _, body1), Lambda(_, implicit2, _, body2)) => {
implicit1 == implicit2 && syntactically_equal(body1, body2)
}
(Pi(_, implicit1, domain1, codomain1), Pi(_, implicit2, domain2, codomain2)) => {
implicit1 == implicit2
&& syntactically_equal(domain1, domain2)
&& syntactically_equal(codomain1, codomain2)
}
(Application(applicand1, argument1), Application(applicand2, argument2)) => {
syntactically_equal(applicand1, applicand2) && syntactically_equal(argument1, argument2)
Expand Down Expand Up @@ -112,10 +116,10 @@ pub fn syntactically_equal<'a>(term1: &Term<'a>, term2: &Term<'a>) -> bool {
| (_, Unifier(_, _))
| (Variable(_, _), _)
| (_, Variable(_, _))
| (Lambda(_, _, _), _)
| (_, Lambda(_, _, _))
| (Pi(_, _, _), _)
| (_, Pi(_, _, _))
| (Lambda(_, _, _, _), _)
| (_, Lambda(_, _, _, _))
| (Pi(_, _, _, _), _)
| (_, Pi(_, _, _, _))
| (Application(_, _), _)
| (_, Application(_, _))
| (Let(_, _), _)
Expand Down Expand Up @@ -334,6 +338,21 @@ mod tests {
assert!(syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_equal_lambda_implicit() {
let context = [];

let source1 = "{x : type} => x";
let tokens1 = tokenize(None, source1).unwrap();
let term1 = parse(None, source1, &tokens1[..], &context[..]).unwrap();

let source2 = "{x : type} => x";
let tokens2 = tokenize(None, source2).unwrap();
let term2 = parse(None, source2, &tokens2[..], &context[..]).unwrap();

assert!(syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_equal_lambda_inequal_domain() {
let context = [];
Expand All @@ -349,6 +368,21 @@ mod tests {
assert!(syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_inequal_lambda_explicit_implicit() {
let context = [];

let source1 = "{x : type} => x";
let tokens1 = tokenize(None, source1).unwrap();
let term1 = parse(None, source1, &tokens1[..], &context[..]).unwrap();

let source2 = "(x : type) => x";
let tokens2 = tokenize(None, source2).unwrap();
let term2 = parse(None, source2, &tokens2[..], &context[..]).unwrap();

assert!(!syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_inequal_lambda_body() {
let context = [];
Expand Down Expand Up @@ -379,6 +413,36 @@ mod tests {
assert!(syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_equal_pi_implicit() {
let context = [];

let source1 = "{x : type} -> x";
let tokens1 = tokenize(None, source1).unwrap();
let term1 = parse(None, source1, &tokens1[..], &context[..]).unwrap();

let source2 = "{x : type} -> x";
let tokens2 = tokenize(None, source2).unwrap();
let term2 = parse(None, source2, &tokens2[..], &context[..]).unwrap();

assert!(syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_inequal_pi_explicit_implicit() {
let context = [];

let source1 = "(x : type) -> x";
let tokens1 = tokenize(None, source1).unwrap();
let term1 = parse(None, source1, &tokens1[..], &context[..]).unwrap();

let source2 = "{x : type} -> x";
let tokens2 = tokenize(None, source2).unwrap();
let term2 = parse(None, source2, &tokens2[..], &context[..]).unwrap();

assert!(!syntactically_equal(&term1, &term2));
}

#[test]
fn syntactically_inequal_pi_domain() {
let context = [];
Expand Down
16 changes: 11 additions & 5 deletions src/evaluator.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,8 +39,8 @@ pub fn evaluate<'a>(term: &Term<'a>) -> Result<Term<'a>, Error> {
pub fn step<'a>(term: &Term<'a>) -> Option<Term<'a>> {
match &term.variant {
Type
| Lambda(_, _, _)
| Pi(_, _, _)
| Lambda(_, _, _, _)
| Pi(_, _, _, _)
| Variable(_, _)
| Integer
| IntegerLiteral(_)
Expand Down Expand Up @@ -84,7 +84,7 @@ pub fn step<'a>(term: &Term<'a>) -> Option<Term<'a>> {
}

// Check if the applicand is a lambda.
if let Lambda(_, _, body) = &applicand.variant {
if let Lambda(_, _, _, body) = &applicand.variant {
// We got a lambda. Perform beta reduction and continue evaluating.
Some(open(body, 0, argument, 0))
} else {
Expand Down Expand Up @@ -616,8 +616,8 @@ pub fn step<'a>(term: &Term<'a>) -> Option<Term<'a>> {
pub fn is_value<'a>(term: &Term<'a>) -> bool {
match term.variant {
Type
| Lambda(_, _, _)
| Pi(_, _, _)
| Lambda(_, _, _, _)
| Pi(_, _, _, _)
| Integer
| IntegerLiteral(_)
| Boolean
Expand Down Expand Up @@ -697,10 +697,12 @@ mod tests {
source_range: Some((0, 39)),
variant: Lambda(
"f",
false,
Rc::new(Term {
source_range: Some((5, 17)),
variant: Pi(
"_",
false,
Rc::new(Term {
source_range: Some((5, 9)),
variant: Type,
Expand All @@ -715,6 +717,7 @@ mod tests {
source_range: Some((22, 39)),
variant: Lambda(
"x",
false,
Rc::new(Term {
source_range: Some((27, 31)),
variant: Type,
Expand Down Expand Up @@ -751,10 +754,12 @@ mod tests {
source_range: Some((0, 39)),
variant: Pi(
"f",
false,
Rc::new(Term {
source_range: Some((5, 17)),
variant: Pi(
"_",
false,
Rc::new(Term {
source_range: Some((5, 9)),
variant: Type,
Expand All @@ -769,6 +774,7 @@ mod tests {
source_range: Some((22, 39)),
variant: Pi(
"x",
false,
Rc::new(Term {
source_range: Some((27, 31)),
variant: Type,
Expand Down
Loading

0 comments on commit a88dbba

Please sign in to comment.