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.

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

[sc-489] Implement Clone for AST iterators, refactor iterator uses. #225

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
8 changes: 3 additions & 5 deletions src/term/check/unbound_vars.rs
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ impl Ctx<'_> {
for rule in &mut def.rules {
let mut scope = HashMap::new();
for pat in &rule.pats {
pat.named_binds().for_each(|nam| push_scope(Some(nam), &mut scope));
pat.binds().for_each(|nam| push_scope(nam.as_ref(), &mut scope));
}

rule.body.check_unbound_vars(&mut scope, &mut errs);
Expand Down Expand Up @@ -101,13 +101,11 @@ pub fn check_uses<'a>(

_ => {
for (child, binds) in term.children_mut_with_binds() {
let binds: Vec<_> = binds.collect();

for bind in binds.iter() {
for bind in binds.clone() {
push_scope(bind.as_ref(), scope);
}
check_uses(child, scope, globals, errs);
for bind in binds.iter().rev() {
for bind in binds.rev() {
pop_scope(bind.as_ref(), scope);
}
}
Expand Down
344 changes: 186 additions & 158 deletions src/term/mod.rs

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion src/term/parser/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -298,7 +298,7 @@ where
}
}
let mat = Term::Mat { args: args_no_bind, rules };
binds.into_iter().rev().fold(mat, |acc, (bind, arg)| Term::Let {
binds.into_iter().rfold(mat, |acc, (bind, arg)| Term::Let {
pat: Pattern::Var(Some(bind)),
val: Box::new(arg),
nxt: Box::new(acc),
Expand Down
26 changes: 25 additions & 1 deletion src/term/transform/desugar_implicit_match_binds.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,29 @@
use crate::term::{Adts, Book, Constructors, Name, NumCtr, Pattern, Term};

impl Book {
/// Converts implicit match binds into explicit ones, using the
/// field names specified in the ADT declaration or the default
/// names for builtin constructors.
///
/// Example:
/// ```hvm
/// data MyList = (Cons h t) | Nil
/// match x y {
/// 0 Nil: (A)
/// 0 Cons: (B y.h y.t)
/// 1+ Nil: (C x-1)
/// 1+p (Cons x xs): (D p x xs)
/// }
/// ```
/// becomes
/// ```hvm
/// match x y {
/// 0 Nil: (A)
/// 0 (Cons y.h y.t): (B y.h y.t)
/// 1+x-1 Nil: (C x-1)
/// 1+p (Cons x xs): (D p x xs)
/// }
/// ```
pub fn desugar_implicit_match_binds(&mut self) {
for def in self.defs.values_mut() {
for rule in &mut def.rules {
Expand All @@ -16,6 +39,7 @@ impl Term {
for child in self.children_mut() {
child.desugar_implicit_match_binds(ctrs, adts);
}

if let Term::Mat { args, rules } = self {
// Make all the matched terms variables
let mut match_args = vec![];
Expand Down Expand Up @@ -59,7 +83,7 @@ impl Term {
}

// Add the binds to the extracted term vars.
*self = match_args.into_iter().rev().fold(std::mem::take(self), |nxt, (nam, val)| {
*self = match_args.into_iter().rfold(std::mem::take(self), |nxt, (nam, val)| {
if let Some(val) = val {
// Non-Var term that was extracted.
Term::Let { pat: Pattern::Var(Some(nam)), val: Box::new(val), nxt: Box::new(nxt) }
Expand Down
20 changes: 9 additions & 11 deletions src/term/transform/encode_adts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -30,21 +30,19 @@ fn encode_ctr(
AdtEncoding::Scott => {
let ctr = Term::Var { nam: ctr_name.clone() };
let app = ctr_args.iter().cloned().fold(ctr, Term::arg_call);
let lam = ctrs.into_iter().rev().fold(app, |acc, arg| Term::named_lam(arg.clone(), acc));
ctr_args.into_iter().rev().fold(lam, |acc, arg| Term::named_lam(arg, acc))
let lam = ctrs.into_iter().rfold(app, |acc, arg| Term::named_lam(arg, acc));
ctr_args.into_iter().rfold(lam, |acc, arg| Term::named_lam(arg, acc))
}
// λarg1 λarg2 #type λctr1 #type λctr2 #type.ctr2.arg2(#type.ctr2.arg1(ctr2 arg1) arg2)
AdtEncoding::TaggedScott => {
let ctr = Term::Var { nam: ctr_name.clone() };
let app = ctr_args.iter().cloned().fold(ctr, |acc, nam| {
let tag = Tag::adt_name(adt_name);
Term::tagged_app(tag, acc, Term::Var { nam })
});
let lam = ctrs
.into_iter()
.rev()
.fold(app, |acc, arg| Term::tagged_lam(Tag::adt_name(adt_name), arg.clone(), acc));
ctr_args.into_iter().rev().fold(lam, |acc, arg| Term::named_lam(arg, acc))
let app = ctr_args
.iter()
.cloned()
.fold(ctr, |acc, nam| Term::tagged_app(Tag::adt_name(adt_name), acc, Term::Var { nam }));
let lam =
ctrs.into_iter().rfold(app, |acc, arg| Term::tagged_lam(Tag::adt_name(adt_name), Some(arg), acc));
ctr_args.into_iter().rfold(lam, |acc, arg| Term::named_lam(arg, acc))
}
}
}
22 changes: 15 additions & 7 deletions src/term/transform/encode_pattern_matching.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,16 @@ use crate::{
};

impl Book {
/// Encodes pattern matching expressions in the book functions according to the adt_encoding.
/// Encodes simple pattern matching expressions in the book into
/// their native/core form.
/// See [`super::simplify_matches::simplify_match_expression`] for
/// the meaning of "simple" used here.
///
/// ADT matches are encoded based on `adt_encoding`.
///
/// Num matches are encoded as a sequence of native num matches (on 0 and 1+).
///
/// Var and pair matches become a let expression.
pub fn encode_simple_matches(&mut self, adt_encoding: AdtEncoding) {
for def in self.defs.values_mut() {
for rule in &mut def.rules {
Expand Down Expand Up @@ -72,7 +81,7 @@ fn encode_num_succ(arg: Term, mut rules: Vec<Rule>) -> Term {
};
let last_arm = Term::lam(last_var, last_rule.body);

rules.into_iter().rev().fold(last_arm, |term, rule| {
rules.into_iter().rfold(last_arm, |term, rule| {
let rules = vec![Rule { pats: vec![Pattern::Num(NumCtr::Num(0))], body: rule.body }, Rule {
pats: vec![Pattern::Num(NumCtr::Succ(1, None))],
body: term,
Expand Down Expand Up @@ -152,8 +161,7 @@ fn encode_adt(arg: Term, rules: Vec<Rule>, adt: Name, adt_encoding: AdtEncoding)
AdtEncoding::Scott => {
let mut arms = vec![];
for rule in rules {
let body = rule.body;
let body = rule.pats[0].named_binds().rev().fold(body, |bod, nam| Term::named_lam(nam.clone(), bod));
let body = rule.pats[0].binds().cloned().rfold(rule.body, |bod, nam| Term::lam(nam, bod));
arms.push(body);
}
Term::call(arg, arms)
Expand All @@ -163,9 +171,9 @@ fn encode_adt(arg: Term, rules: Vec<Rule>, adt: Name, adt_encoding: AdtEncoding)
let mut arms = vec![];
for rule in rules.into_iter() {
let body = rule.pats[0]
.named_binds()
.rev()
.fold(rule.body, |bod, var| Term::tagged_lam(Tag::adt_name(&adt), var.clone(), bod));
.binds()
.cloned()
.rfold(rule.body, |bod, nam| Term::tagged_lam(Tag::adt_name(&adt), nam, bod));
arms.push(body);
}
Term::tagged_call(Tag::adt_name(&adt), arg, arms)
Expand Down
4 changes: 2 additions & 2 deletions src/term/transform/linearize_matches.rs
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ pub fn lift_match_vars(match_term: &mut Term, lift_all_vars: bool) -> &mut Term
.body
.free_vars()
.into_iter()
.filter(|(name, _)| !rule.pats.iter().any(|p| p.named_binds().contains(name)))
.filter(|(name, _)| !rule.pats.iter().any(|p| p.binds().flatten().contains(name)))
});

// Collect the vars.
Expand All @@ -75,7 +75,7 @@ pub fn lift_match_vars(match_term: &mut Term, lift_all_vars: bool) -> &mut Term
// Add lambdas to the arms
for rule in rules {
let old_body = std::mem::take(&mut rule.body);
rule.body = free_vars.iter().rev().fold(old_body, |body, var| Term::named_lam(var.clone(), body));
rule.body = free_vars.iter().cloned().rfold(old_body, |body, nam| Term::named_lam(nam, body));
}

// Add apps to the match
Expand Down
9 changes: 4 additions & 5 deletions src/term/transform/resolve_refs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -34,8 +34,8 @@ impl Ctx<'_> {
for rule in def.rules.iter_mut() {
let mut scope = HashMap::new();

for name in rule.pats.iter().flat_map(Pattern::named_binds) {
push_scope(Some(name), &mut scope);
for name in rule.pats.iter().flat_map(Pattern::binds) {
push_scope(name.as_ref(), &mut scope);
}

let res = rule.body.resolve_refs(&def_names, self.book.entrypoint.as_ref(), &mut scope);
Expand Down Expand Up @@ -72,12 +72,11 @@ impl Term {
}

for (child, binds) in self.children_mut_with_binds() {
let binds: Vec<_> = binds.collect();
for bind in binds.iter() {
for bind in binds.clone() {
push_scope(bind.as_ref(), scope);
}
child.resolve_refs(def_names, main, scope)?;
for bind in binds.iter() {
for bind in binds.rev() {
pop_scope(bind.as_ref(), scope);
}
}
Expand Down
2 changes: 1 addition & 1 deletion src/term/transform/simplify_matches.rs
Original file line number Diff line number Diff line change
Expand Up @@ -378,7 +378,7 @@ fn extract_args(args: &mut [Term]) -> Vec<(Name, Term)> {
///
/// `vec![(%match_arg0, arg)]` + `term` => `let %match_arg0 = arg; term`
fn bind_extracted_args(extracted: Vec<(Name, Term)>, term: Term) -> Term {
extracted.into_iter().rev().fold(term, |term, (nam, val)| Term::Let {
extracted.into_iter().rfold(term, |term, (nam, val)| Term::Let {
pat: Pattern::Var(Some(nam)),
val: Box::new(val),
nxt: Box::new(term),
Expand Down
56 changes: 0 additions & 56 deletions src/term/util.rs

This file was deleted.

Loading