From f5d2151d35942b957230c3081a928af3619d9400 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 31 Mar 2019 18:47:34 +0200
Subject: Make SubExpr a newtype

---
 dhall/src/typecheck.rs | 103 +++++++++++++++++++++++--------------------------
 1 file changed, 48 insertions(+), 55 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index f21721d..e769c7f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1,7 +1,6 @@
 #![allow(non_snake_case)]
 use std::collections::HashSet;
 use std::fmt;
-use std::rc::Rc;
 
 use crate::normalize::normalize;
 use dhall_core;
@@ -113,7 +112,7 @@ where
     go::<S, T>(&mut ctx, eL0, eR0)
 }
 
-fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
+fn type_of_builtin<S>(b: Builtin) -> SubExpr<S, X> {
     use dhall_core::Builtin::*;
     match b {
         Bool | Natural | Integer | Double | Text => dhall_expr!(Type),
@@ -184,16 +183,15 @@ fn type_of_builtin<S>(b: Builtin) -> Rc<Expr<S, X>> {
 /// is not necessary for just type-checking.  If you actually care about the
 /// returned type then you may want to `normalize` it afterwards.
 pub fn type_with<S>(
-    ctx: &Context<Label, Rc<Expr<S, X>>>,
-    e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+    ctx: &Context<Label, SubExpr<S, X>>,
+    e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>>
 where
     S: ::std::fmt::Debug,
 {
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
     use dhall_core::Const::*;
-    use dhall_core::Expr;
     use dhall_core::Expr::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
     let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
@@ -266,7 +264,7 @@ where
                     return Err(mkerr(NotAFunction(f.clone(), tf)));
                 }
             };
-            let tA = normalize(Rc::clone(tA));
+            let tA = normalize(SubExpr::clone(tA));
             let tA2 = normalized_type_with(ctx, a.clone())?;
             if prop_equal(tA.as_ref(), tA2.as_ref()) {
                 let vx0 = &V(x.clone(), 0);
@@ -280,9 +278,9 @@ where
         }
         Let(f, mt, r, b) => {
             let r = if let Some(t) = mt {
-                rc(Annot(Rc::clone(r), Rc::clone(t)))
+                rc(Annot(SubExpr::clone(r), SubExpr::clone(t)))
             } else {
-                Rc::clone(r)
+                SubExpr::clone(r)
             };
 
             let tR = type_with(ctx, r)?;
@@ -351,7 +349,7 @@ where
         EmptyListLit(t) => {
             let s = normalized_type_with(ctx, t.clone())?;
             ensure_is_type(s, InvalidListType(t.clone()))?;
-            let t = normalize(Rc::clone(t));
+            let t = normalize(SubExpr::clone(t));
             return Ok(dhall_expr!(List t));
         }
         NEListLit(xs) => {
@@ -377,7 +375,7 @@ where
             return Ok(dhall_expr!(Optional t));
         }
         NEOptionalLit(x) => {
-            let t: Rc<Expr<_, _>> = type_with(ctx, x.clone())?;
+            let t: SubExpr<_, _> = type_with(ctx, x.clone())?;
             let s = normalized_type_with(ctx, t.clone())?;
             ensure_is_type(s, InvalidOptionalType(t.clone()))?;
             let t = normalize(t);
@@ -451,9 +449,9 @@ where
 }
 
 pub fn normalized_type_with<S>(
-    ctx: &Context<Label, Rc<Expr<S, X>>>,
-    e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>>
+    ctx: &Context<Label, SubExpr<S, X>>,
+    e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>>
 where
     S: ::std::fmt::Debug,
 {
@@ -464,8 +462,8 @@ where
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
 pub fn type_of<S: ::std::fmt::Debug>(
-    e: Rc<Expr<S, X>>,
-) -> Result<Rc<Expr<S, X>>, TypeError<S>> {
+    e: SubExpr<S, X>,
+) -> Result<SubExpr<S, X>, TypeError<S>> {
     let ctx = Context::new();
     type_with(&ctx, e) //.map(|e| e.into_owned())
 }
@@ -474,63 +472,58 @@ pub fn type_of<S: ::std::fmt::Debug>(
 #[derive(Debug)]
 pub enum TypeMessage<S> {
     UnboundVariable,
-    InvalidInputType(Rc<Expr<S, X>>),
-    InvalidOutputType(Rc<Expr<S, X>>),
-    NotAFunction(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    TypeMismatch(
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-    ),
-    AnnotMismatch(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidInputType(SubExpr<S, X>),
+    InvalidOutputType(SubExpr<S, X>),
+    NotAFunction(SubExpr<S, X>, SubExpr<S, X>),
+    TypeMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    AnnotMismatch(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     Untyped,
-    InvalidListElement(usize, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    InvalidListType(Rc<Expr<S, X>>),
-    InvalidOptionalElement(Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidListElement(usize, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidListType(SubExpr<S, X>),
+    InvalidOptionalElement(SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
     InvalidOptionalLiteral(usize),
-    InvalidOptionalType(Rc<Expr<S, X>>),
-    InvalidPredicate(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    InvalidOptionalType(SubExpr<S, X>),
+    InvalidPredicate(SubExpr<S, X>, SubExpr<S, X>),
     IfBranchMismatch(
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
-        Rc<Expr<S, X>>,
+        SubExpr<S, X>,
+        SubExpr<S, X>,
+        SubExpr<S, X>,
+        SubExpr<S, X>,
     ),
-    IfBranchMustBeTerm(bool, Rc<Expr<S, X>>, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    InvalidField(Label, Rc<Expr<S, X>>),
-    InvalidFieldType(Label, Rc<Expr<S, X>>),
-    InvalidAlternative(Label, Rc<Expr<S, X>>),
-    InvalidAlternativeType(Label, Rc<Expr<S, X>>),
+    IfBranchMustBeTerm(bool, SubExpr<S, X>, SubExpr<S, X>, SubExpr<S, X>),
+    InvalidField(Label, SubExpr<S, X>),
+    InvalidFieldType(Label, SubExpr<S, X>),
+    InvalidAlternative(Label, SubExpr<S, X>),
+    InvalidAlternativeType(Label, SubExpr<S, X>),
     DuplicateAlternative(Label),
-    MustCombineARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    MustCombineARecord(SubExpr<S, X>, SubExpr<S, X>),
     FieldCollision(Label),
-    MustMergeARecord(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    MustMergeUnion(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    MustMergeARecord(SubExpr<S, X>, SubExpr<S, X>),
+    MustMergeUnion(SubExpr<S, X>, SubExpr<S, X>),
     UnusedHandler(HashSet<Label>),
     MissingHandler(HashSet<Label>),
-    HandlerInputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    HandlerOutputTypeMismatch(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    HandlerNotAFunction(Label, Rc<Expr<S, X>>),
-    NotARecord(Label, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    MissingField(Label, Rc<Expr<S, X>>),
-    BinOpTypeMismatch(BinOp, Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    NoDependentLet(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
-    NoDependentTypes(Rc<Expr<S, X>>, Rc<Expr<S, X>>),
+    HandlerInputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
+    HandlerOutputTypeMismatch(Label, SubExpr<S, X>, SubExpr<S, X>),
+    HandlerNotAFunction(Label, SubExpr<S, X>),
+    NotARecord(Label, SubExpr<S, X>, SubExpr<S, X>),
+    MissingField(Label, SubExpr<S, X>),
+    BinOpTypeMismatch(BinOp, SubExpr<S, X>, SubExpr<S, X>),
+    NoDependentLet(SubExpr<S, X>, SubExpr<S, X>),
+    NoDependentTypes(SubExpr<S, X>, SubExpr<S, X>),
 }
 
 /// A structured type error that includes context
 #[derive(Debug)]
 pub struct TypeError<S> {
-    pub context: Context<Label, Rc<Expr<S, X>>>,
-    pub current: Rc<Expr<S, X>>,
+    pub context: Context<Label, SubExpr<S, X>>,
+    pub current: SubExpr<S, X>,
     pub type_message: TypeMessage<S>,
 }
 
 impl<S> TypeError<S> {
     pub fn new(
-        context: &Context<Label, Rc<Expr<S, X>>>,
-        current: Rc<Expr<S, X>>,
+        context: &Context<Label, SubExpr<S, X>>,
+        current: SubExpr<S, X>,
         type_message: TypeMessage<S>,
     ) -> Self {
         TypeError {
-- 
cgit v1.2.3


From 7374d0524ccd53b256107667b213597c05720d2d Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 31 Mar 2019 19:08:08 +0200
Subject: Move recursion out of Expr

---
 dhall/src/typecheck.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index e769c7f..31702db 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -12,7 +12,7 @@ use self::TypeMessage::*;
 
 fn axiom<S>(c: Const) -> Result<Const, TypeError<S>> {
     use dhall_core::Const::*;
-    use dhall_core::Expr::*;
+    use dhall_core::ExprF::*;
     match c {
         Type => Ok(Kind),
         Kind => Err(TypeError::new(&Context::new(), rc(Const(Kind)), Untyped)),
@@ -53,7 +53,7 @@ where
     S: ::std::fmt::Debug,
     T: ::std::fmt::Debug,
 {
-    use dhall_core::Expr::*;
+    use dhall_core::ExprF::*;
     fn go<S, T>(
         ctx: &mut Vec<(Label, Label)>,
         el: &Expr<S, X>,
@@ -192,7 +192,7 @@ where
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
     use dhall_core::Const::*;
-    use dhall_core::Expr::*;
+    use dhall_core::ExprF::*;
     let mkerr = |msg: TypeMessage<_>| TypeError::new(ctx, e.clone(), msg);
     let ensure_const = |x: &SubExpr<_, _>, msg: TypeMessage<_>| match x.as_ref()
     {
-- 
cgit v1.2.3


From 62970fd2010b01260cf45a1f2a6a582c6a8c0c12 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sun, 31 Mar 2019 21:04:10 +0200
Subject: Make Expr generic in Label

---
 dhall/src/typecheck.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 31702db..da52ba8 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -28,7 +28,7 @@ fn rule(a: Const, b: Const) -> Result<Const, ()> {
     }
 }
 
-fn match_vars(vl: &V, vr: &V, ctx: &[(Label, Label)]) -> bool {
+fn match_vars(vl: &V<Label>, vr: &V<Label>, ctx: &[(Label, Label)]) -> bool {
     let mut vl = vl.clone();
     let mut vr = vr.clone();
     let mut ctx = ctx.to_vec();
-- 
cgit v1.2.3


From 627287185118482ceb7132f6dedad7111dccf972 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Sat, 6 Apr 2019 00:06:13 +0200
Subject: Give up on laziness and greatly simplify normalization

---
 dhall/src/typecheck.rs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dhall/src/typecheck.rs')

diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index da52ba8..75e6e1d 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -187,7 +187,7 @@ pub fn type_with<S>(
     e: SubExpr<S, X>,
 ) -> Result<SubExpr<S, X>, TypeError<S>>
 where
-    S: ::std::fmt::Debug,
+    S: ::std::fmt::Debug + Clone,
 {
     use dhall_core::BinOp::*;
     use dhall_core::Builtin::*;
@@ -453,7 +453,7 @@ pub fn normalized_type_with<S>(
     e: SubExpr<S, X>,
 ) -> Result<SubExpr<S, X>, TypeError<S>>
 where
-    S: ::std::fmt::Debug,
+    S: ::std::fmt::Debug + Clone,
 {
     Ok(normalize(type_with(ctx, e)?))
 }
@@ -461,7 +461,7 @@ where
 /// `typeOf` is the same as `type_with` with an empty context, meaning that the
 /// expression must be closed (i.e. no free variables), otherwise type-checking
 /// will fail.
-pub fn type_of<S: ::std::fmt::Debug>(
+pub fn type_of<S: ::std::fmt::Debug + Clone>(
     e: SubExpr<S, X>,
 ) -> Result<SubExpr<S, X>, TypeError<S>> {
     let ctx = Context::new();
-- 
cgit v1.2.3