Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Implement generalization #316

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Implement generalization #316

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion examples/infinite_recursion.g
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
f = x => f x
f = (x : bool) => f x
f true
2 changes: 1 addition & 1 deletion examples/infinite_type.g
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
t = int -> t
f : t = x => f
f : t = (x : int) => f
f 1 2 3
84 changes: 48 additions & 36 deletions src/de_bruijn.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,7 @@ use crate::term::{
Quotient, Sum, True, Type, Unifier, Variable,
},
};
use std::{
cmp::{min, Ordering},
convert::TryFrom,
rc::Rc,
};
use std::{cmp::Ordering, convert::TryFrom, rc::Rc};

// Shifting refers to adjusting the De Bruijn indices of free variables. A cutoff determines which
// variables are considered free. This function is used to raise or lower a term into a different
Expand All @@ -23,25 +19,27 @@ pub fn signed_shift<'a>(term: &Term<'a>, cutoff: usize, amount: isize) -> Option
// We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
let borrow = { subterm.borrow().clone() };

match borrow {
Ok(subterm) => {
signed_shift(
// The `unwrap` is safe due to [ref:unifier_shifts_valid].
&signed_shift(&subterm, 0, *subterm_shift).unwrap(),
cutoff,
amount,
)
}
Err(min_shift) => {
let new_shift = subterm_shift + amount;

*subterm.borrow_mut() = Err(min(min_shift, new_shift));
if let Some(subterm) = borrow {
signed_shift(&unsigned_shift(&subterm, 0, *subterm_shift), cutoff, amount)
} else if *subterm_shift >= cutoff {
// This `unwrap` is "virtually safe", unless the conversion overflows.
let signed_subterm_shift = isize::try_from(*subterm_shift).unwrap();

// Adjust the shift if it results in a non-negative quantity.
if signed_subterm_shift >= -amount {
Some(Term {
source_range: term.source_range,
variant: Unifier(subterm.clone(), new_shift),
variant: Unifier(
subterm.clone(),
// This `unwrap` is safe due to the check above.
usize::try_from(signed_subterm_shift + amount).unwrap(),
),
})
} else {
None
}
} else {
Some(term.clone())
}
}
Type | Integer | IntegerLiteral(_) | Boolean | True | False => Some(term.clone()),
Expand Down Expand Up @@ -189,8 +187,8 @@ pub fn signed_shift<'a>(term: &Term<'a>, cutoff: usize, amount: isize) -> Option
// is total.
pub fn unsigned_shift<'a>(term: &Term<'a>, cutoff: usize, amount: usize) -> Term<'a> {
// The inner `unwrap` is "essentially safe" in that it can only fail in the virtually
// impossible case of the conversion overflowing. The outer `unwrap` is safe due to
// [ref:unifier_shifts_valid].
// impossible case of the conversion overflowing. The outer `unwrap` is safe because `amount`
// is non-negative.
signed_shift(term, cutoff, isize::try_from(amount).unwrap()).unwrap()
}

Expand All @@ -211,16 +209,15 @@ pub fn open<'a>(
// We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
let borrow = { subterm.borrow().clone() };

if let Ok(subterm) = borrow {
if let Some(subterm) = borrow {
open(
// The `unwrap` is safe due to [ref:unifier_shifts_valid].
&signed_shift(&subterm, 0, *subterm_shift).unwrap(),
&unsigned_shift(&subterm, 0, *subterm_shift),
index_to_replace,
term_to_insert,
shift_amount,
)
} else {
// The `unwrap` is safe because shifting an unresolved unifier is always safe.
// The `unwrap` is NOT justified!
signed_shift(term_to_open, 0, -1).unwrap()
}
}
Expand Down Expand Up @@ -431,31 +428,46 @@ mod tests {
use std::{cell::RefCell, rc::Rc};

#[test]
fn signed_shift_unifier_none() {
fn signed_shift_unifier_none_valid() {
assert_same!(
signed_shift(
&Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(0))), 0),
variant: Unifier(Rc::new(RefCell::new(None)), 10),
},
0,
-42,
-4,
),
Some(Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(-42))), -42),
variant: Unifier(Rc::new(RefCell::new(None)), 6),
}),
);
}

#[test]
fn signed_shift_unifier_none_invalid() {
assert_same!(
signed_shift(
&Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(None)), 0),
},
0,
-42,
),
None,
);
}

#[test]
fn signed_shift_unifier_some() {
assert_same!(
signed_shift(
&Term {
source_range: None,
variant: Unifier(
Rc::new(RefCell::new(Ok(Term {
Rc::new(RefCell::new(Some(Term {
source_range: None,
variant: Variable("x", 10),
}))),
Expand Down Expand Up @@ -529,14 +541,14 @@ mod tests {
unsigned_shift(
&Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(0))), 0),
variant: Unifier(Rc::new(RefCell::new(None)), 0),
},
0,
42,
),
Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(0))), 42),
variant: Unifier(Rc::new(RefCell::new(None)), 42),
},
);
}
Expand All @@ -548,7 +560,7 @@ mod tests {
&Term {
source_range: None,
variant: Unifier(
Rc::new(RefCell::new(Ok(Term {
Rc::new(RefCell::new(Some(Term {
source_range: None,
variant: Variable("x", 0),
}))),
Expand Down Expand Up @@ -1299,7 +1311,7 @@ mod tests {
open(
&Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(0))), 0),
variant: Unifier(Rc::new(RefCell::new(None)), 10),
},
0,
&Term {
Expand All @@ -1310,7 +1322,7 @@ mod tests {
),
Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(-1))), -1),
variant: Unifier(Rc::new(RefCell::new(None)), 9),
},
);
}
Expand All @@ -1322,7 +1334,7 @@ mod tests {
&Term {
source_range: None,
variant: Unifier(
Rc::new(RefCell::new(Ok(Term {
Rc::new(RefCell::new(Some(Term {
source_range: None,
variant: Variable("x", 0),
}))),
Expand Down
38 changes: 11 additions & 27 deletions src/equality.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use crate::{
de_bruijn::signed_shift,
de_bruijn::unsigned_shift,
term::{
Term,
Variant::{
Expand All @@ -20,16 +20,8 @@ pub fn syntactically_equal<'a>(term1: &Term<'a>, term2: &Term<'a>) -> bool {
loop {
term1 = if let Unifier(subterm, subterm_shift) = &term1.variant {
// We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
let borrow = { subterm.borrow().clone() };

if let Ok(subterm) = borrow {
if let Some(shifted_term) = signed_shift(&subterm, 0, *subterm_shift) {
shifted_term
} else {
// The `signed_shift` failed. This means the term is malformed. The error will
// be reported during type checking.
return false;
}
if let Some(subterm) = { subterm.borrow().clone() } {
unsigned_shift(&subterm, 0, *subterm_shift)
} else {
break;
}
Expand All @@ -43,16 +35,8 @@ pub fn syntactically_equal<'a>(term1: &Term<'a>, term2: &Term<'a>) -> bool {
loop {
term2 = if let Unifier(subterm, subterm_shift) = &term2.variant {
// We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
let borrow = { subterm.borrow().clone() };

if let Ok(subterm) = borrow {
if let Some(shifted_term) = signed_shift(&subterm, 0, *subterm_shift) {
shifted_term
} else {
// The `signed_shift` failed. This means the term is malformed. The error will
// be reported during type checking.
return false;
}
if let Some(subterm) = { subterm.borrow().clone() } {
unsigned_shift(&subterm, 0, *subterm_shift)
} else {
break;
}
Expand Down Expand Up @@ -177,7 +161,7 @@ mod tests {
let term1 = Term {
source_range: None,
variant: Unifier(
Rc::new(RefCell::new(Ok(Term {
Rc::new(RefCell::new(Some(Term {
source_range: None,
variant: Variable("x", 0),
}))),
Expand All @@ -203,7 +187,7 @@ mod tests {
let term2 = Term {
source_range: None,
variant: Unifier(
Rc::new(RefCell::new(Ok(Term {
Rc::new(RefCell::new(Some(Term {
source_range: None,
variant: Variable("x", 0),
}))),
Expand All @@ -216,7 +200,7 @@ mod tests {

#[test]
fn syntactically_equal_unifier_same_pointer_same_shift() {
let rc = Rc::new(RefCell::new(Err(0)));
let rc = Rc::new(RefCell::new(None));

let term1 = Term {
source_range: None,
Expand All @@ -233,7 +217,7 @@ mod tests {

#[test]
fn syntactically_inequal_unifier_same_pointer_different_shift() {
let rc = Rc::new(RefCell::new(Err(0)));
let rc = Rc::new(RefCell::new(None));

let term1 = Term {
source_range: None,
Expand All @@ -252,12 +236,12 @@ mod tests {
fn syntactically_inequal_unifier_different_pointer_same_shift() {
let term1 = Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(0))), 5),
variant: Unifier(Rc::new(RefCell::new(None)), 5),
};

let term2 = Term {
source_range: None,
variant: Unifier(Rc::new(RefCell::new(Err(0))), 5),
variant: Unifier(Rc::new(RefCell::new(None)), 5),
};

assert!(!syntactically_equal(&term1, &term2));
Expand Down
12 changes: 4 additions & 8 deletions src/evaluator.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use crate::{
de_bruijn::{open, signed_shift, unsigned_shift},
de_bruijn::{open, unsigned_shift},
error::Error,
format::CodeStr,
term::{
Expand Down Expand Up @@ -48,13 +48,9 @@ pub fn step<'a>(term: &Term<'a>) -> Option<Term<'a>> {
| True
| False => None,
Unifier(subterm, subterm_shift) => {
// We `clone` the borrowed `subterm` to avoid holding the dynamic borrow for too long.
let borrow = { subterm.borrow().clone() };

// If the unifier points to something, step to it. Otherwise, we're stuck.
borrow
.ok()
.and_then(|subterm| signed_shift(&subterm, 0, *subterm_shift))
// If the unifier points to something, step to it. Otherwise, we're stuck. We `clone`
// the borrowed `subterm` to avoid holding the dynamic borrow for too long.
{ subterm.borrow().clone() }.map(|subterm| unsigned_shift(&subterm, 0, *subterm_shift))
}
Application(applicand, argument) => {
// Try to step the applicand.
Expand Down
17 changes: 13 additions & 4 deletions src/main.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,7 @@ fn run(source_path: &Path, check_only: bool) -> Result<(), Error> {
// Type check the term.
let mut typing_context = vec![];
let mut definitions_context = vec![];
let _ = type_check(
let (elaborated_term, elaborated_type) = type_check(
Some(source_path),
&source_contents,
&term,
Expand All @@ -170,9 +170,18 @@ fn run(source_path: &Path, check_only: bool) -> Result<(), Error> {
)
.map_err(collect_errors)?;

// Evaluate the term.
if !check_only {
let value = evaluate(&term)?;
// Evaluate the term if applicable.
if check_only {
println!(
"Elaborated term:\n\n{}",
elaborated_term.to_string().code_str(),
);
println!(
"\nElaborated type:\n\n{}",
elaborated_type.to_string().code_str(),
);
} else {
let value = evaluate(&elaborated_term)?;
println!("{}", value.to_string().code_str());
}

Expand Down
13 changes: 6 additions & 7 deletions src/normalizer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use crate::{
de_bruijn::{open, signed_shift, unsigned_shift},
de_bruijn::{open, unsigned_shift},
term::{
Term,
Variant::{
Expand Down Expand Up @@ -35,12 +35,11 @@ pub fn normalize_weak_head<'a>(
let borrow = { subterm.borrow().clone() };

// If the unifier points to something, normalize it. Otherwise, we're stuck.
if let Ok(subterm) = borrow {
if let Some(subterm) = signed_shift(&subterm, 0, *subterm_shift) {
normalize_weak_head(&subterm, definitions_context)
} else {
term.clone()
}
if let Some(subterm) = borrow {
normalize_weak_head(
&unsigned_shift(&subterm, 0, *subterm_shift),
definitions_context,
)
} else {
term.clone()
}
Expand Down
Loading