Add absurd
This commit is contained in:
parent
718fdeb171
commit
a49bad9a58
|
@ -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
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue
Block a user