From 5c33165e95eb264fa9d305c097b183f6622aad03 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Mon, 18 Mar 2019 05:02:28 +0100
Subject: tweaks

---
 dhall/src/normalize.rs | 18 ++++++++++++++----
 1 file changed, 14 insertions(+), 4 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 3c04b9e..bf1bff5 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -4,7 +4,7 @@ use dhall_generator::dhall_expr;
 use std::fmt;
 use std::rc::Rc;
 
-fn apply_builtin<S, A>(b: Builtin, args: Vec<SubExpr<S, A>>) -> SubExpr<S, A>
+fn apply_builtin<S, A>(b: Builtin, mut args: Vec<SubExpr<S, A>>) -> SubExpr<S, A>
 where
     S: fmt::Debug,
     A: fmt::Debug,
@@ -13,8 +13,8 @@ where
     use dhall_core::Builtin::*;
     use dhall_core::Expr::*;
     let f = rc(Builtin(b));
-    // How many arguments for each builtin, and which argument
-    // is the important one for pattern-matching
+    // How many arguments a builtin needs, and which argument
+    // should be normalized and pattern-matched
     let (len_consumption, arg_to_eval) = match b {
         OptionalSome => (1, None),
         OptionalNone => (1, None),
@@ -35,10 +35,11 @@ where
         NaturalFold => (1, Some(0)),
         _ => (0, None),
     };
-    let mut args = args.to_vec();
+    // Abort if not enough arguments present
     if len_consumption > args.len() {
         return rc(App(f, args));
     }
+    // Normalize the important argument
     if let Some(i) = arg_to_eval {
         args[i] = Rc::clone(&normalize_whnf(&args[i]));
     }
@@ -79,6 +80,7 @@ where
                 };
                 let a0 = Rc::clone(a0);
                 let a1 = shift(1, &V("a".into(), 0), &a0);
+                // TODO: use Embed to avoid reevaluating g
                 break dhall_expr!(g (List a0) (λ(a : a0) -> λ(as : List a1) -> [ a ] # as) ([] : List a0));
             }
         }
@@ -93,6 +95,7 @@ where
                     }
                 };
                 let a0 = Rc::clone(a0);
+                // TODO: use Embed to avoid reevaluating g
                 break dhall_expr!((g (Optional a0)) (λ(x: a0) -> [x] :  Optional a0) ([] :  Optional a0));
             }
         }
@@ -146,6 +149,9 @@ where
         }
         _ => return rc(App(f, args)),
     };
+    // Put the remaining arguments back and eval again. In most cases
+    // ret will not be of a form that can be applied, so this won't go very deep.
+    // In lots of cases, there are no remaining args so this cann will just return ret.
     normalize_whnf(&rc(Expr::App(ret, args.split_off(len_consumption))))
 }
 
@@ -165,7 +171,10 @@ where
         Let(f, _, r, b) => {
             let vf0 = &V(f.clone(), 0);
             let r2 = shift(1, vf0, r);
+            // TODO: use a context
             let b2 = subst(vf0, &r2, b);
+            // TODO: add tests sensitive to shift errors before
+            // trying anything
             let b3 = shift(-1, vf0, &b2);
             normalize_whnf(&b3)
         }
@@ -175,6 +184,7 @@ where
             let f = normalize_whnf(f);
             match (f.as_ref(), args.as_slice()) {
                 (_, []) => f,
+                // TODO: use Embed to avoid reevaluating f
                 (App(f, args1), args2) => normalize_whnf(&rc(App(
                     f.clone(),
                     args1.iter().chain(args2.iter()).cloned().collect(),
-- 
cgit v1.2.3