ehmry/dhall-haskell
ehmry/dhall-haskell
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Prevent "Natural/subtract 0" from causing a panic (#1208)

Browse Source 
Previously, normalizing `Natural/subtract 0` would result in this
error:

    ⊢ Natural/subtract 0

    Error: Compiler bug

    An ill-typed expression was encountered during normalization.
    Explanation: This error message means that there is a bug in the Dhall compiler.
    You didn't do anything wrong, but if you would like to see this problem fixed
    then you should report the bug at:

    https://github.com/dhall-lang/dhall-haskell/issues

    CallStack (from HasCallStack):
      error, called at src/Dhall/Eval.hs:865:38 in dhall-1.25.0-FCOZ7uxqivz8dkVwuN7aED:Dhall.Eval

This updates the dhall-lang submodule to include a new testcase added
in https://github.com/dhall-lang/dhall-lang/pull/692.
This commit is contained in:
Simon Jakobi 2019-08-07 04:38:56 +02:00 committed by mergify[bot]
parent 4559a27bf3
commit 0871fcd857
2 changed files with 16 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
dhall/dhall-lang

@ -1 +1 @@
Subproject commit 1ed98c33ce5078161109885f0b16b3828958f4e2
Subproject commit b08bfa062e2373d1cafaadfb75661e30f4caa91e

23
dhall/src/Dhall/Eval.hs
View File

@ -138,6 +138,7 @@ data HLamInfo a
| NaturalFoldCl (Val a)
| ListFoldCl (Val a)
| OptionalFoldCl (Val a)
| NaturalSubtractZero
pattern VPrim :: (Val a -> Val a) -> Val a
pattern VPrim f = VHLam Prim f
@ -414,14 +415,19 @@ eval !env t =
n -> VNaturalToInteger n
NaturalShow -> VPrim $ \case VNaturalLit n -> VTextLit (VChunks [] (Data.Text.pack (show n)))
n -> VNaturalShow n
NaturalSubtract -> VPrim $ \x -> VPrim $ \y ->
case (x,y) of
(VNaturalLit x, VNaturalLit y)
| y >= x -> VNaturalLit (subtract x y)
| otherwise -> VNaturalLit 0
(VNaturalLit 0, y) -> y
(x, VNaturalLit 0) -> VNaturalLit 0
(x, y) -> VNaturalSubtract x y
NaturalSubtract -> VPrim $ \case
VNaturalLit 0 ->
VHLam NaturalSubtractZero id
x@(VNaturalLit m) ->
VPrim $ \case
VNaturalLit n
| n >= m -> VNaturalLit (subtract m n)
| otherwise -> VNaturalLit 0
y -> VNaturalSubtract x y
x ->
VPrim $ \case
VNaturalLit 0 -> VNaturalLit 0
y -> VNaturalSubtract x y
NaturalPlus t u -> vNaturalPlus (evalE t) (evalE u)
NaturalTimes t u -> case (evalE t, evalE u) of
(VNaturalLit 1, u ) -> u
@ -798,6 +804,7 @@ quote !env !t =
NaturalFoldCl{} -> quote env (t VPrimVar)
ListFoldCl{} -> quote env (t VPrimVar)
OptionalFoldCl{} -> quote env (t VPrimVar)
NaturalSubtractZero -> App NaturalSubtract (NaturalLit 0)
VPi a (freshCl -> (x, v, b)) -> Pi x (quoteE a) (quoteBind x (inst b v))
VHPi (fresh -> (x, v)) a b -> Pi x (quoteE a) (quoteBind x (b v))