From a49bad9a5819c8e4932a0a99548299c0f4a7eebb Mon Sep 17 00:00:00 2001
From: Gabriel Gonzalez <Gabriel439@gmail.com>
Date: Tue, 11 Oct 2016 09:02:12 -0700
Subject: [PATCH] Add `absurd`

---
 src/Dhall/Core.hs  | 7 +++++++
 src/Dhall/Lexer.x  | 4 ++++
 src/Dhall/Parser.y | 3 +++
 3 files changed, 14 insertions(+)

diff --git a/src/Dhall/Core.hs b/src/Dhall/Core.hs
index 58ae0c9..248588a 100644
--- a/src/Dhall/Core.hs
+++ b/src/Dhall/Core.hs
@@ -265,6 +265,8 @@ data Expr a
     | RecordLit (Map Text (Expr a))
     -- | > Union     [(k1, t1), (k2, t2)]           ~  < k1 t1 | k2 t2 >
     | Union     (Map Text (Expr a))
+    -- | > Absurd                                   ~  absurd
+    | Absurd
     -- | > Field e x                                ~  e.x
     | Field (Expr a) Text
     -- | > Embed path                               ~  #path
@@ -330,6 +332,7 @@ instance Monad Expr where
     Record    kts    >>= k = Record    (fmap (>>= k) kts)
     RecordLit kvs    >>= k = RecordLit (fmap (>>= k) kvs)
     Union     kts    >>= k = Union     (fmap (>>= k) kts)
+    Absurd           >>= _ = Absurd
     Field r x        >>= k = Field (r >>= k) x
     Embed r          >>= k = k r
 
@@ -544,6 +547,8 @@ buildExpr6 (Record a) =
     buildRecord a
 buildExpr6 (Union a) =
     buildUnion a
+buildExpr6 Absurd =
+    "absurd"
 buildExpr6 (Embed a) =
     build a
 buildExpr6 (Field a b) =
@@ -1843,6 +1848,8 @@ typeWith ctx e@(Union     kts   ) = do
                 _          -> Left (TypeError ctx e (InvalidTagType k t))
     mapM_ process (Data.Map.toList kts)
     return (Const Type)
+typeWith _      Absurd            = do
+    return (Pi "_" (Union Data.Map.empty) (Pi "a" (Const Type) "a"))
 typeWith ctx e@(Field r x       ) = do
     t <- fmap normalize (typeWith ctx r)
     case t of
diff --git a/src/Dhall/Lexer.x b/src/Dhall/Lexer.x
index 2977f08..9094f8d 100644
--- a/src/Dhall/Lexer.x
+++ b/src/Dhall/Lexer.x
@@ -109,6 +109,7 @@ tokens :-
     "List/concat"                       { emit ListConcat       }
     "Maybe"                             { emit Maybe            }
     "Maybe/fold"                        { emit MaybeFold        }
+    "absurd"                            { emit Absurd           }
     \" ([^\"] | \\.)* \"                { capture (TextLit . str)        }
     $fst $labelchar* | "(" $opchar+ ")" { capture (Label . toText)       }
     \-? $digit+                         { capture (Number . toInt)       }
@@ -276,6 +277,7 @@ data Token
     | MaybeFold
     | TextLit Text
     | TextConcat
+    | Absurd
     | Label Text
     | Number Integer
     | File FilePath
@@ -402,6 +404,8 @@ instance Buildable Token where
         = "Maybe/fold"
     build (TextLit t)
         = Data.Text.Buildable.build (show t)
+    build  Absurd
+        = "absurd"
     build (Label t)
         = Data.Text.Buildable.build t
     build (Number n)
diff --git a/src/Dhall/Parser.y b/src/Dhall/Parser.y
index 40fbc0e..3f192c2 100644
--- a/src/Dhall/Parser.y
+++ b/src/Dhall/Parser.y
@@ -96,6 +96,7 @@ import qualified NeatInterpolation
     'List/concat'     { Dhall.Lexer.ListConcat     }
     'Maybe'           { Dhall.Lexer.Maybe          }
     'Maybe/fold'      { Dhall.Lexer.MaybeFold      }
+    'absurd'          { Dhall.Lexer.Absurd         }
     text              { Dhall.Lexer.TextLit    $$  }
     label             { Dhall.Lexer.Label      $$  }
     number            { Dhall.Lexer.Number     $$  }
@@ -248,6 +249,8 @@ Expr6
         { $1 }
     | Union
         { $1 }
+    | 'absurd'
+        { Absurd }
     | Import
         { Embed $1 }
     | Expr6 '.' label