Merge pull request #225 from HigherOrderCO/chore/sc-489/simplify-hvml…

…-passes-using-term-iterators

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

src/term/check/unbound_vars.rs

@@ -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);
@@ -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);
         }
       }

src/term/parser/parser.rs

@@ -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),

src/term/transform/desugar_implicit_match_binds.rs

@@ -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 {
@@ -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![];
@@ -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) }

src/term/transform/encode_adts.rs

@@ -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))
     }
   }
 }

src/term/transform/encode_pattern_matching.rs

@@ -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 {
@@ -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,
@@ -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)
@@ -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)

src/term/transform/linearize_matches.rs

@@ -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.
@@ -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

src/term/transform/resolve_refs.rs

@@ -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);
@@ -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);
         }
       }

src/term/transform/simplify_matches.rs

@@ -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),