From 7ea6ce6322c8bc2e3712c02142dbe1cd11102c83 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Jun 2024 14:48:14 +0200 Subject: [PATCH 1/3] implement shortcut for more data types in Natural/fold --- dhall/src/Dhall/Eval.hs | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 0f3b64388..6e97ece6f 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -252,6 +252,26 @@ data Val a -- | For use with "Text.Show.Functions". deriving instance (Show a, Show (Val a -> Val a)) => Show (Val a) +valEq :: Val a -> Val a -> Bool +valEq (VConst x1) (VConst x2) = x1 == x2 +valEq (VVar t1 i1) (VVar t2 i2) = t1 == t2 && i1 == i2 +valEq VPrimVar VPrimVar = True +valEq (VApp f1 x1) (VApp f2 x2) = valEq f1 f2 && valEq x1 x2 +valEq VBool VBool = True +valEq (VBoolLit x1) (VBoolLit x2) = x1 == x2 +valEq (VBytesLit x1) (VBytesLit x2) = x1 == x2 +valEq (VNaturalLit x1) (VNaturalLit x2) = x1 == x2 +valEq (VNaturalFold t1 x1 y1 z1) (VNaturalFold t2 x2 y2 z2) = valEq t1 t2 && valEq x1 x2 && valEq y1 y2 && valEq z1 z2 +valEq (VNaturalIsZero x1) (VNaturalIsZero x2) = valEq x1 x2 +valEq (VIntegerLit x1) (VIntegerLit x2) = x1 == x2 +valEq (VDoubleLit x1) (VDoubleLit x2) = x1 == x2 +valEq (VList _) (VList _) = True +valEq (VListLit _ x1) (VListLit _ x2) = all (uncurry valEq) (zip (toList x1) (toList x2)) +valEq (VSome x1) (VSome x2) = valEq x1 x2 +valEq (VNone _) (VNone _) = True +valEq (VRecordLit x1) (VRecordLit x2) = (length x1 == length x2) && (all (uncurry valEq) (zip (Map.elems x1) (Map.elems x2))) +valEq _ _ = False + (~>) :: Val a -> Val a -> Val a (~>) a b = VHPi "_" a (\_ -> b) {-# INLINE (~>) #-} @@ -529,11 +549,9 @@ eval !env t0 = -- https://github.com/ghcjs/ghcjs/issues/782 go zero (fromIntegral n' :: Integer) where go !acc 0 = acc - go (VNaturalLit x) m = - case vApp succ (VNaturalLit x) of - VNaturalLit y | x == y -> VNaturalLit x - notNaturalLit -> go notNaturalLit (m - 1) - go acc m = go (vApp succ acc) (m - 1) + go acc m = + let next = vApp succ acc in + if valEq next acc then acc else go next (m - 1) _ -> inert NaturalBuild -> VPrim $ \case From 05372bc620debf2496db2c801b099ecd05c1029d Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Jun 2024 17:44:59 +0200 Subject: [PATCH 2/3] use conv --- dhall/src/Dhall/Eval.hs | 22 +--------------------- 1 file changed, 1 insertion(+), 21 deletions(-) diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 6e97ece6f..0e29b118a 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -252,26 +252,6 @@ data Val a -- | For use with "Text.Show.Functions". deriving instance (Show a, Show (Val a -> Val a)) => Show (Val a) -valEq :: Val a -> Val a -> Bool -valEq (VConst x1) (VConst x2) = x1 == x2 -valEq (VVar t1 i1) (VVar t2 i2) = t1 == t2 && i1 == i2 -valEq VPrimVar VPrimVar = True -valEq (VApp f1 x1) (VApp f2 x2) = valEq f1 f2 && valEq x1 x2 -valEq VBool VBool = True -valEq (VBoolLit x1) (VBoolLit x2) = x1 == x2 -valEq (VBytesLit x1) (VBytesLit x2) = x1 == x2 -valEq (VNaturalLit x1) (VNaturalLit x2) = x1 == x2 -valEq (VNaturalFold t1 x1 y1 z1) (VNaturalFold t2 x2 y2 z2) = valEq t1 t2 && valEq x1 x2 && valEq y1 y2 && valEq z1 z2 -valEq (VNaturalIsZero x1) (VNaturalIsZero x2) = valEq x1 x2 -valEq (VIntegerLit x1) (VIntegerLit x2) = x1 == x2 -valEq (VDoubleLit x1) (VDoubleLit x2) = x1 == x2 -valEq (VList _) (VList _) = True -valEq (VListLit _ x1) (VListLit _ x2) = all (uncurry valEq) (zip (toList x1) (toList x2)) -valEq (VSome x1) (VSome x2) = valEq x1 x2 -valEq (VNone _) (VNone _) = True -valEq (VRecordLit x1) (VRecordLit x2) = (length x1 == length x2) && (all (uncurry valEq) (zip (Map.elems x1) (Map.elems x2))) -valEq _ _ = False - (~>) :: Val a -> Val a -> Val a (~>) a b = VHPi "_" a (\_ -> b) {-# INLINE (~>) #-} @@ -551,7 +531,7 @@ eval !env t0 = go !acc 0 = acc go acc m = let next = vApp succ acc in - if valEq next acc then acc else go next (m - 1) + if conv env next acc then acc else go next (m - 1) _ -> inert NaturalBuild -> VPrim $ \case From d851f5b7bf3be8ad155a437d170582213ed09cb3 Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Wed, 12 Jun 2024 17:50:55 +0200 Subject: [PATCH 3/3] add a comment --- dhall/src/Dhall/Eval.hs | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/dhall/src/Dhall/Eval.hs b/dhall/src/Dhall/Eval.hs index 0e29b118a..8d9eef345 100644 --- a/dhall/src/Dhall/Eval.hs +++ b/dhall/src/Dhall/Eval.hs @@ -530,8 +530,9 @@ eval !env t0 = go zero (fromIntegral n' :: Integer) where go !acc 0 = acc go acc m = - let next = vApp succ acc in - if conv env next acc then acc else go next (m - 1) + -- Detect a shortcut: if succ acc == acc then return acc immediately. + let next = vApp succ acc + in if conv env next acc then acc else go next (m - 1) _ -> inert NaturalBuild -> VPrim $ \case