From d3f54e5536cc4d2ba46b6e4e88b7218da1b797ee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 8 Aug 2019 23:09:37 +0200
Subject: Remove dhall::expr!() macro

It's a lot of hassle for not a lot of benefit
---
 dhall/src/phase/typecheck.rs | 107 ++++++++++++++++++++++++++++++++-----------
 1 file changed, 81 insertions(+), 26 deletions(-)

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

diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 297a096..8f5ca8b 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1,6 +1,5 @@
 use std::collections::HashMap;
 
-use dhall_proc_macros as dhall;
 use dhall_syntax::{
     rc, Builtin, Const, Expr, ExprF, InterpolatedTextContents, Label, Span,
     SubExpr, X,
@@ -173,41 +172,97 @@ pub fn type_of_const(c: Const) -> Result<Type, TypeError> {
     }
 }
 
+// Ad-hoc macro to help construct the types of builtins
+macro_rules! make_type {
+    (Type) => { ExprF::Const(Const::Type) };
+    (Bool) => { ExprF::Builtin(Builtin::Bool) };
+    (Natural) => { ExprF::Builtin(Builtin::Natural) };
+    (Integer) => { ExprF::Builtin(Builtin::Integer) };
+    (Double) => { ExprF::Builtin(Builtin::Double) };
+    (Text) => { ExprF::Builtin(Builtin::Text) };
+    ($var:ident) => {
+        ExprF::Var(dhall_syntax::V(stringify!($var).into(), 0))
+    };
+    (Optional $ty:ident) => {
+        ExprF::App(
+            rc(ExprF::Builtin(Builtin::Optional)),
+            rc(make_type!($ty))
+        )
+    };
+    (List $($rest:tt)*) => {
+        ExprF::App(
+            rc(ExprF::Builtin(Builtin::List)),
+            rc(make_type!($($rest)*))
+        )
+    };
+    ({ $($label:ident : $ty:ident),* }) => {{
+        let mut kts = dhall_syntax::map::DupTreeMap::new();
+        $(
+            kts.insert(
+                Label::from(stringify!($label)),
+                rc(make_type!($ty)),
+            );
+        )*
+        ExprF::RecordType(kts)
+    }};
+    ($ty:ident -> $($rest:tt)*) => {
+        ExprF::Pi(
+            "_".into(),
+            rc(make_type!($ty)),
+            rc(make_type!($($rest)*))
+        )
+    };
+    (($($arg:tt)*) -> $($rest:tt)*) => {
+        ExprF::Pi(
+            "_".into(),
+            rc(make_type!($($arg)*)),
+            rc(make_type!($($rest)*))
+        )
+    };
+    (forall ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
+        ExprF::Pi(
+            stringify!($var).into(),
+            rc(make_type!($($ty)*)),
+            rc(make_type!($($rest)*))
+        )
+    };
+}
+
 fn type_of_builtin(b: Builtin) -> Expr<X, X> {
     use dhall_syntax::Builtin::*;
     match b {
-        Bool | Natural | Integer | Double | Text => dhall::expr!(Type),
-        List | Optional => dhall::expr!(
+        Bool | Natural | Integer | Double | Text => make_type!(Type),
+        List | Optional => make_type!(
             Type -> Type
         ),
 
-        NaturalFold => dhall::expr!(
+        NaturalFold => make_type!(
             Natural ->
             forall (natural: Type) ->
             forall (succ: natural -> natural) ->
             forall (zero: natural) ->
             natural
         ),
-        NaturalBuild => dhall::expr!(
+        NaturalBuild => make_type!(
             (forall (natural: Type) ->
                 forall (succ: natural -> natural) ->
                 forall (zero: natural) ->
                 natural) ->
             Natural
         ),
-        NaturalIsZero | NaturalEven | NaturalOdd => dhall::expr!(
+        NaturalIsZero | NaturalEven | NaturalOdd => make_type!(
             Natural -> Bool
         ),
-        NaturalToInteger => dhall::expr!(Natural -> Integer),
-        NaturalShow => dhall::expr!(Natural -> Text),
-        NaturalSubtract => dhall::expr!(Natural -> Natural -> Natural),
+        NaturalToInteger => make_type!(Natural -> Integer),
+        NaturalShow => make_type!(Natural -> Text),
+        NaturalSubtract => make_type!(Natural -> Natural -> Natural),
 
-        IntegerToDouble => dhall::expr!(Integer -> Double),
-        IntegerShow => dhall::expr!(Integer -> Text),
-        DoubleShow => dhall::expr!(Double -> Text),
-        TextShow => dhall::expr!(Text -> Text),
+        IntegerToDouble => make_type!(Integer -> Double),
+        IntegerShow => make_type!(Integer -> Text),
+        DoubleShow => make_type!(Double -> Text),
+        TextShow => make_type!(Text -> Text),
 
-        ListBuild => dhall::expr!(
+        ListBuild => make_type!(
             forall (a: Type) ->
             (forall (list: Type) ->
                 forall (cons: a -> list -> list) ->
@@ -215,28 +270,28 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> {
                 list) ->
             List a
         ),
-        ListFold => dhall::expr!(
+        ListFold => make_type!(
             forall (a: Type) ->
-            List a ->
+            (List a) ->
             forall (list: Type) ->
             forall (cons: a -> list -> list) ->
             forall (nil: list) ->
             list
         ),
-        ListLength => dhall::expr!(forall (a: Type) -> List a -> Natural),
+        ListLength => make_type!(forall (a: Type) -> (List a) -> Natural),
         ListHead | ListLast => {
-            dhall::expr!(forall (a: Type) -> List a -> Optional a)
+            make_type!(forall (a: Type) -> (List a) -> Optional a)
         }
-        ListIndexed => dhall::expr!(
+        ListIndexed => make_type!(
             forall (a: Type) ->
-            List a ->
+            (List a) ->
             List { index: Natural, value: a }
         ),
-        ListReverse => dhall::expr!(
-            forall (a: Type) -> List a -> List a
+        ListReverse => make_type!(
+            forall (a: Type) -> (List a) -> List a
         ),
 
-        OptionalBuild => dhall::expr!(
+        OptionalBuild => make_type!(
             forall (a: Type) ->
             (forall (optional: Type) ->
                 forall (just: a -> optional) ->
@@ -244,15 +299,15 @@ fn type_of_builtin(b: Builtin) -> Expr<X, X> {
                 optional) ->
             Optional a
         ),
-        OptionalFold => dhall::expr!(
+        OptionalFold => make_type!(
             forall (a: Type) ->
-            Optional a ->
+            (Optional a) ->
             forall (optional: Type) ->
             forall (just: a -> optional) ->
             forall (nothing: optional) ->
             optional
         ),
-        OptionalNone => dhall::expr!(
+        OptionalNone => make_type!(
             forall (a: Type) -> Optional a
         ),
     }
-- 
cgit v1.2.3