{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
module Dhall.Normalize (
alphaNormalize
, normalize
, normalizeWith
, normalizeWithM
, Normalizer
, NormalizerM
, ReifiedNormalizer (..)
, judgmentallyEqual
, subst
, shift
, isNormalized
, isNormalizedWith
, freeIn
) where
import Control.Applicative (empty)
import Data.Foldable
import Data.Functor.Identity (Identity(..))
import Data.Semigroup (Semigroup(..))
import Data.Sequence (ViewL(..), ViewR(..))
import Data.Traversable
import Dhall.Syntax (Expr(..), Var(..), Binding(Binding), Chunks(..), DhallDouble(..), Const(..))
import Instances.TH.Lift ()
import Prelude hiding (succ)
import qualified Data.Sequence
import qualified Data.Set
import qualified Data.Text
import qualified Dhall.Eval as Eval
import qualified Dhall.Map
import qualified Dhall.Set
import qualified Dhall.Syntax as Syntax
judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
judgmentallyEqual = Eval.judgmentallyEqual
{-# INLINE judgmentallyEqual #-}
shift :: Int -> Var -> Expr s a -> Expr s a
shift _ _ (Const a) = Const a
shift d (V x n) (Var (V x' n')) = Var (V x' n'')
where
n'' = if x == x' && n <= n' then n' + d else n'
shift d (V x n) (Lam x' _A b) = Lam x' _A' b'
where
_A' = shift d (V x n ) _A
b' = shift d (V x n') b
where
n' = if x == x' then n + 1 else n
shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'
where
_A' = shift d (V x n ) _A
_B' = shift d (V x n') _B
where
n' = if x == x' then n + 1 else n
shift d v (App f a) = App f' a'
where
f' = shift d v f
a' = shift d v a
shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) =
Let (Binding src0 f src1 mt' src2 r') e'
where
e' = shift d (V x n') e
where
n' = if x == f then n + 1 else n
mt' = fmap (fmap (shift d (V x n))) mt
r' = shift d (V x n) r
shift d v (Annot a b) = Annot a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ Bool = Bool
shift _ _ (BoolLit a) = BoolLit a
shift d v (BoolAnd a b) = BoolAnd a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolOr a b) = BoolOr a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolEQ a b) = BoolEQ a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolNE a b) = BoolNE a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolIf a b c) = BoolIf a' b' c'
where
a' = shift d v a
b' = shift d v b
c' = shift d v c
shift _ _ Natural = Natural
shift _ _ (NaturalLit a) = NaturalLit a
shift _ _ NaturalFold = NaturalFold
shift _ _ NaturalBuild = NaturalBuild
shift _ _ NaturalIsZero = NaturalIsZero
shift _ _ NaturalEven = NaturalEven
shift _ _ NaturalOdd = NaturalOdd
shift _ _ NaturalToInteger = NaturalToInteger
shift _ _ NaturalShow = NaturalShow
shift _ _ NaturalSubtract = NaturalSubtract
shift d v (NaturalPlus a b) = NaturalPlus a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (NaturalTimes a b) = NaturalTimes a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ Integer = Integer
shift _ _ (IntegerLit a) = IntegerLit a
shift _ _ IntegerClamp = IntegerClamp
shift _ _ IntegerNegate = IntegerNegate
shift _ _ IntegerShow = IntegerShow
shift _ _ IntegerToDouble = IntegerToDouble
shift _ _ Double = Double
shift _ _ (DoubleLit a) = DoubleLit a
shift _ _ DoubleShow = DoubleShow
shift _ _ Text = Text
shift d v (TextLit (Chunks a b)) = TextLit (Chunks a' b)
where
a' = fmap (fmap (shift d v)) a
shift d v (TextAppend a b) = TextAppend a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ TextShow = TextShow
shift _ _ List = List
shift d v (ListLit a b) = ListLit a' b'
where
a' = fmap (shift d v) a
b' = fmap (shift d v) b
shift _ _ ListBuild = ListBuild
shift d v (ListAppend a b) = ListAppend a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ ListFold = ListFold
shift _ _ ListLength = ListLength
shift _ _ ListHead = ListHead
shift _ _ ListLast = ListLast
shift _ _ ListIndexed = ListIndexed
shift _ _ ListReverse = ListReverse
shift _ _ Optional = Optional
shift d v (Some a) = Some a'
where
a' = shift d v a
shift _ _ None = None
shift _ _ OptionalFold = OptionalFold
shift _ _ OptionalBuild = OptionalBuild
shift d v (Record a) = Record a'
where
a' = fmap (shift d v) a
shift d v (RecordLit a) = RecordLit a'
where
a' = fmap (shift d v) a
shift d v (Union a) = Union a'
where
a' = fmap (fmap (shift d v)) a
shift d v (Combine a b) = Combine a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (CombineTypes a b) = CombineTypes a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (Prefer a b) = Prefer a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (RecordCompletion a b) = RecordCompletion a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (Merge a b c) = Merge a' b' c'
where
a' = shift d v a
b' = shift d v b
c' = fmap (shift d v) c
shift d v (ToMap a b) = ToMap a' b'
where
a' = shift d v a
b' = fmap (shift d v) b
shift d v (Field a b) = Field a' b
where
a' = shift d v a
shift d v (Assert a) = Assert a'
where
a' = shift d v a
shift d v (Equivalent a b) = Equivalent a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (Project a b) = Project a' b'
where
a' = shift d v a
b' = fmap (shift d v) b
shift d v (Note a b) = Note a b'
where
b' = shift d v b
shift d v (ImportAlt a b) = ImportAlt a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ (Embed p) = Embed p
subst :: Var -> Expr s a -> Expr s a -> Expr s a
subst _ _ (Const a) = Const a
subst (V x n) e (Lam y _A b) = Lam y _A' b'
where
_A' = subst (V x n ) e _A
b' = subst (V x n') (shift 1 (V y 0) e) b
n' = if x == y then n + 1 else n
subst (V x n) e (Pi y _A _B) = Pi y _A' _B'
where
_A' = subst (V x n ) e _A
_B' = subst (V x n') (shift 1 (V y 0) e) _B
n' = if x == y then n + 1 else n
subst v e (App f a) = App f' a'
where
f' = subst v e f
a' = subst v e a
subst v e (Var v') = if v == v' then e else Var v'
subst (V x n) e (Let (Binding src0 f src1 mt src2 r) b) =
Let (Binding src0 f src1 mt' src2 r') b'
where
b' = subst (V x n') (shift 1 (V f 0) e) b
where
n' = if x == f then n + 1 else n
mt' = fmap (fmap (subst (V x n) e)) mt
r' = subst (V x n) e r
subst x e (Annot a b) = Annot a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ Bool = Bool
subst _ _ (BoolLit a) = BoolLit a
subst x e (BoolAnd a b) = BoolAnd a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolOr a b) = BoolOr a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolEQ a b) = BoolEQ a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolNE a b) = BoolNE a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolIf a b c) = BoolIf a' b' c'
where
a' = subst x e a
b' = subst x e b
c' = subst x e c
subst _ _ Natural = Natural
subst _ _ (NaturalLit a) = NaturalLit a
subst _ _ NaturalFold = NaturalFold
subst _ _ NaturalBuild = NaturalBuild
subst _ _ NaturalIsZero = NaturalIsZero
subst _ _ NaturalEven = NaturalEven
subst _ _ NaturalOdd = NaturalOdd
subst _ _ NaturalToInteger = NaturalToInteger
subst _ _ NaturalShow = NaturalShow
subst _ _ NaturalSubtract = NaturalSubtract
subst x e (NaturalPlus a b) = NaturalPlus a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (NaturalTimes a b) = NaturalTimes a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ Integer = Integer
subst _ _ (IntegerLit a) = IntegerLit a
subst _ _ IntegerClamp = IntegerClamp
subst _ _ IntegerNegate = IntegerNegate
subst _ _ IntegerShow = IntegerShow
subst _ _ IntegerToDouble = IntegerToDouble
subst _ _ Double = Double
subst _ _ (DoubleLit a) = DoubleLit a
subst _ _ DoubleShow = DoubleShow
subst _ _ Text = Text
subst x e (TextLit (Chunks a b)) = TextLit (Chunks a' b)
where
a' = fmap (fmap (subst x e)) a
subst x e (TextAppend a b) = TextAppend a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ TextShow = TextShow
subst _ _ List = List
subst x e (ListLit a b) = ListLit a' b'
where
a' = fmap (subst x e) a
b' = fmap (subst x e) b
subst x e (ListAppend a b) = ListAppend a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ ListBuild = ListBuild
subst _ _ ListFold = ListFold
subst _ _ ListLength = ListLength
subst _ _ ListHead = ListHead
subst _ _ ListLast = ListLast
subst _ _ ListIndexed = ListIndexed
subst _ _ ListReverse = ListReverse
subst _ _ Optional = Optional
subst x e (Some a) = Some a'
where
a' = subst x e a
subst _ _ None = None
subst _ _ OptionalFold = OptionalFold
subst _ _ OptionalBuild = OptionalBuild
subst x e (Record kts) = Record kts'
where
kts' = fmap (subst x e) kts
subst x e (RecordLit kvs) = RecordLit kvs'
where
kvs' = fmap (subst x e) kvs
subst x e (Union kts) = Union kts'
where
kts' = fmap (fmap (subst x e)) kts
subst x e (Combine a b) = Combine a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (CombineTypes a b) = CombineTypes a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (Prefer a b) = Prefer a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (RecordCompletion a b) = RecordCompletion a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (Merge a b c) = Merge a' b' c'
where
a' = subst x e a
b' = subst x e b
c' = fmap (subst x e) c
subst x e (ToMap a b) = ToMap a' b'
where
a' = subst x e a
b' = fmap (subst x e) b
subst x e (Field a b) = Field a' b
where
a' = subst x e a
subst x e (Project a b) = Project a' b'
where
a' = subst x e a
b' = fmap (subst x e) b
subst x e (Assert a) = Assert a'
where
a' = subst x e a
subst x e (Equivalent a b) = Equivalent a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (Note a b) = Note a b'
where
b' = subst x e b
subst x e (ImportAlt a b) = ImportAlt a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ (Embed p) = Embed p
boundedType :: Expr s a -> Bool
boundedType Bool = True
boundedType Natural = True
boundedType Integer = True
boundedType Double = True
boundedType Text = True
boundedType (App List _) = False
boundedType (App Optional t) = boundedType t
boundedType (Record kvs) = all boundedType kvs
boundedType (Union kvs) = all (all boundedType) kvs
boundedType _ = False
alphaNormalize :: Expr s a -> Expr s a
alphaNormalize = Eval.alphaNormalize
{-# INLINE alphaNormalize #-}
normalize :: Eq a => Expr s a -> Expr t a
normalize = Eval.normalize
{-# INLINE normalize #-}
normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
normalizeWith (Just ctx) t = runIdentity (normalizeWithM (getReifiedNormalizer ctx) t)
normalizeWith _ t = Eval.normalize t
normalizeWithM
:: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
normalizeWithM ctx e0 = loop (Syntax.denote e0)
where
loop e = case e of
Const k -> pure (Const k)
Var v -> pure (Var v)
Lam x _A b -> Lam x <$> _A' <*> b'
where
_A' = loop _A
b' = loop b
Pi x _A _B -> Pi x <$> _A' <*> _B'
where
_A' = loop _A
_B' = loop _B
App f a -> do
res <- ctx (App f a)
case res of
Just e1 -> loop e1
Nothing -> do
f' <- loop f
a' <- loop a
case f' of
Lam x _A b₀ -> do
let a₂ = shift 1 (V x 0) a'
let b₁ = subst (V x 0) a₂ b₀
let b₂ = shift (-1) (V x 0) b₁
loop b₂
_ -> do
case App f' a' of
App NaturalFold (NaturalLit n) -> do
let natural = Var (V "natural" 0)
let go 0 x = x
go n' x = go (n'-1) (App (Var (V "succ" 0)) x)
let n' = go n (Var (V "zero" 0))
pure
(Lam "natural"
(Const Type)
(Lam "succ"
(Pi "_" natural natural)
(Lam "zero"
natural
n')))
App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do
t' <- loop t
if boundedType t' then strict else lazy
where
strict = strictLoop (fromIntegral n0 :: Integer)
lazy = loop ( lazyLoop (fromIntegral n0 :: Integer))
strictLoop !0 = loop zero
strictLoop !n = App succ' <$> strictLoop (n - 1) >>= loop
lazyLoop !0 = zero
lazyLoop !n = App succ' (lazyLoop (n - 1))
App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)
where
succ = Lam "n" Natural (NaturalPlus "n" (NaturalLit 1))
zero = NaturalLit 0
App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0))
App NaturalEven (NaturalLit n) -> pure (BoolLit (even n))
App NaturalOdd (NaturalLit n) -> pure (BoolLit (odd n))
App NaturalToInteger (NaturalLit n) -> pure (IntegerLit (toInteger n))
App NaturalShow (NaturalLit n) ->
pure (TextLit (Chunks [] (Data.Text.pack (show n))))
App (App NaturalSubtract (NaturalLit x)) (NaturalLit y)
| y >= x -> pure (NaturalLit (subtract x y))
| otherwise -> pure (NaturalLit 0)
App (App NaturalSubtract (NaturalLit 0)) y -> pure y
App (App NaturalSubtract _) (NaturalLit 0) -> pure (NaturalLit 0)
App (App NaturalSubtract x) y | Eval.judgmentallyEqual x y -> pure (NaturalLit 0)
App IntegerClamp (IntegerLit n)
| 0 <= n -> pure (NaturalLit (fromInteger n))
| otherwise -> pure (NaturalLit 0)
App IntegerNegate (IntegerLit n) ->
pure (IntegerLit (negate n))
App IntegerShow (IntegerLit n)
| 0 <= n -> pure (TextLit (Chunks [] ("+" <> Data.Text.pack (show n))))
| otherwise -> pure (TextLit (Chunks [] (Data.Text.pack (show n))))
App IntegerToDouble (IntegerLit n) -> pure (DoubleLit ((DhallDouble . read . show) n))
App DoubleShow (DoubleLit (DhallDouble n)) ->
pure (TextLit (Chunks [] (Data.Text.pack (show n))))
App (App OptionalBuild _A₀) g ->
loop (App (App (App g optional) just) nothing)
where
optional = App Optional _A₀
just = Lam "a" _A₀ (Some "a")
nothing = App None _A₀
App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)
where
_A₁ = shift 1 "a" _A₀
list = App List _A₀
cons =
Lam "a" _A₀
(Lam "as"
(App List _A₁)
(ListAppend (ListLit Nothing (pure "a")) "as")
)
nil = ListLit (Just (App List _A₀)) empty
App (App ListFold t) (ListLit _ xs) -> do
t' <- loop t
let list = Var (V "list" 0)
let lam term =
Lam "list" (Const Type)
(Lam "cons" (Pi "_" t' (Pi "_" list list))
(Lam "nil" list term))
term <- foldrM
(\x acc -> do
x' <- loop x
pure (App (App (Var (V "cons" 0)) x') acc))
(Var (V "nil" 0))
xs
pure (lam term)
App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do
t' <- loop t
if boundedType t' then strict else lazy
where
strict = foldr strictCons strictNil xs
lazy = loop (foldr lazyCons lazyNil xs)
strictNil = loop nil
lazyNil = nil
strictCons y ys = do
App (App cons y) <$> ys >>= loop
lazyCons y ys = App (App cons y) ys
App (App ListLength _) (ListLit _ ys) ->
pure (NaturalLit (fromIntegral (Data.Sequence.length ys)))
App (App ListHead t) (ListLit _ ys) -> loop o
where
o = case Data.Sequence.viewl ys of
y :< _ -> Some y
_ -> App None t
App (App ListLast t) (ListLit _ ys) -> loop o
where
o = case Data.Sequence.viewr ys of
_ :> y -> Some y
_ -> App None t
App (App ListIndexed _A₀) (ListLit _ as₀) -> loop (ListLit t as₁)
where
as₁ = Data.Sequence.mapWithIndex adapt as₀
_A₂ = Record (Dhall.Map.fromList kts)
where
kts = [ ("index", Natural)
, ("value", _A₀)
]
t | null as₀ = Just (App List _A₂)
| otherwise = Nothing
adapt n a_ =
RecordLit (Dhall.Map.fromList kvs)
where
kvs = [ ("index", NaturalLit (fromIntegral n))
, ("value", a_)
]
App (App ListReverse _) (ListLit t xs) ->
loop (ListLit t (Data.Sequence.reverse xs))
App (App OptionalFold t0) x0 -> do
t1 <- loop t0
let optional = Var (V "optional" 0)
let lam term = (Lam "optional"
(Const Type)
(Lam "some"
(Pi "_" t1 optional)
(Lam "none" optional term)))
x1 <- loop x0
pure $ case x1 of
App None _ -> lam (Var (V "none" 0))
Some x' -> lam (App (Var (V "some" 0)) x')
_ -> App (App OptionalFold t1) x1
App TextShow (TextLit (Chunks [] oldText)) ->
loop (TextLit (Chunks [] newText))
where
newText = Eval.textShow oldText
_ -> do
res2 <- ctx (App f' a')
case res2 of
Nothing -> pure (App f' a')
Just app' -> loop app'
Let (Binding _ f _ _ _ r) b -> loop b''
where
r' = shift 1 (V f 0) r
b' = subst (V f 0) r' b
b'' = shift (-1) (V f 0) b'
Annot x _ -> loop x
Bool -> pure Bool
BoolLit b -> pure (BoolLit b)
BoolAnd x y -> decide <$> loop x <*> loop y
where
decide (BoolLit True ) r = r
decide (BoolLit False) _ = BoolLit False
decide l (BoolLit True ) = l
decide _ (BoolLit False) = BoolLit False
decide l r
| Eval.judgmentallyEqual l r = l
| otherwise = BoolAnd l r
BoolOr x y -> decide <$> loop x <*> loop y
where
decide (BoolLit False) r = r
decide (BoolLit True ) _ = BoolLit True
decide l (BoolLit False) = l
decide _ (BoolLit True ) = BoolLit True
decide l r
| Eval.judgmentallyEqual l r = l
| otherwise = BoolOr l r
BoolEQ x y -> decide <$> loop x <*> loop y
where
decide (BoolLit True ) r = r
decide l (BoolLit True ) = l
decide l r
| Eval.judgmentallyEqual l r = BoolLit True
| otherwise = BoolEQ l r
BoolNE x y -> decide <$> loop x <*> loop y
where
decide (BoolLit False) r = r
decide l (BoolLit False) = l
decide l r
| Eval.judgmentallyEqual l r = BoolLit False
| otherwise = BoolNE l r
BoolIf bool true false -> decide <$> loop bool <*> loop true <*> loop false
where
decide (BoolLit True ) l _ = l
decide (BoolLit False) _ r = r
decide b (BoolLit True) (BoolLit False) = b
decide b l r
| Eval.judgmentallyEqual l r = l
| otherwise = BoolIf b l r
Natural -> pure Natural
NaturalLit n -> pure (NaturalLit n)
NaturalFold -> pure NaturalFold
NaturalBuild -> pure NaturalBuild
NaturalIsZero -> pure NaturalIsZero
NaturalEven -> pure NaturalEven
NaturalOdd -> pure NaturalOdd
NaturalToInteger -> pure NaturalToInteger
NaturalShow -> pure NaturalShow
NaturalSubtract -> pure NaturalSubtract
NaturalPlus x y -> decide <$> loop x <*> loop y
where
decide (NaturalLit 0) r = r
decide l (NaturalLit 0) = l
decide (NaturalLit m) (NaturalLit n) = NaturalLit (m + n)
decide l r = NaturalPlus l r
NaturalTimes x y -> decide <$> loop x <*> loop y
where
decide (NaturalLit 1) r = r
decide l (NaturalLit 1) = l
decide (NaturalLit 0) _ = NaturalLit 0
decide _ (NaturalLit 0) = NaturalLit 0
decide (NaturalLit m) (NaturalLit n) = NaturalLit (m * n)
decide l r = NaturalTimes l r
Integer -> pure Integer
IntegerLit n -> pure (IntegerLit n)
IntegerClamp -> pure IntegerClamp
IntegerNegate -> pure IntegerNegate
IntegerShow -> pure IntegerShow
IntegerToDouble -> pure IntegerToDouble
Double -> pure Double
DoubleLit n -> pure (DoubleLit n)
DoubleShow -> pure DoubleShow
Text -> pure Text
TextLit (Chunks xys z) -> do
chunks' <- mconcat <$> chunks
case chunks' of
Chunks [("", x)] "" -> pure x
c -> pure (TextLit c)
where
chunks =
((++ [Chunks [] z]) . concat) <$> traverse process xys
process (x, y) = do
y' <- loop y
case y' of
TextLit c -> pure [Chunks [] x, c]
_ -> pure [Chunks [(x, y')] mempty]
TextAppend x y -> loop (TextLit (Chunks [("", x), ("", y)] ""))
TextShow -> pure TextShow
List -> pure List
ListLit t es
| Data.Sequence.null es -> ListLit <$> t' <*> pure Data.Sequence.empty
| otherwise -> ListLit Nothing <$> es'
where
t' = traverse loop t
es' = traverse loop es
ListAppend x y -> decide <$> loop x <*> loop y
where
decide (ListLit _ m) r | Data.Sequence.null m = r
decide l (ListLit _ n) | Data.Sequence.null n = l
decide (ListLit t m) (ListLit _ n) = ListLit t (m <> n)
decide l r = ListAppend l r
ListBuild -> pure ListBuild
ListFold -> pure ListFold
ListLength -> pure ListLength
ListHead -> pure ListHead
ListLast -> pure ListLast
ListIndexed -> pure ListIndexed
ListReverse -> pure ListReverse
Optional -> pure Optional
Some a -> Some <$> a'
where
a' = loop a
None -> pure None
OptionalFold -> pure OptionalFold
OptionalBuild -> pure OptionalBuild
Record kts -> Record . Dhall.Map.sort <$> kts'
where
kts' = traverse loop kts
RecordLit kvs -> RecordLit . Dhall.Map.sort <$> kvs'
where
kvs' = traverse loop kvs
Union kts -> Union . Dhall.Map.sort <$> kts'
where
kts' = traverse (traverse loop) kts
Combine x y -> decide <$> loop x <*> loop y
where
decide (RecordLit m) r | Data.Foldable.null m =
r
decide l (RecordLit n) | Data.Foldable.null n =
l
decide (RecordLit m) (RecordLit n) =
RecordLit (Dhall.Map.unionWith decide m n)
decide l r =
Combine l r
CombineTypes x y -> decide <$> loop x <*> loop y
where
decide (Record m) r | Data.Foldable.null m =
r
decide l (Record n) | Data.Foldable.null n =
l
decide (Record m) (Record n) =
Record (Dhall.Map.unionWith decide m n)
decide l r =
CombineTypes l r
Prefer x y -> decide <$> loop x <*> loop y
where
decide (RecordLit m) r | Data.Foldable.null m =
r
decide l (RecordLit n) | Data.Foldable.null n =
l
decide (RecordLit m) (RecordLit n) =
RecordLit (Dhall.Map.union n m)
decide l r | Eval.judgmentallyEqual l r =
l
decide l r =
Prefer l r
RecordCompletion x y -> do
loop (Annot (Prefer (Field x "default") y) (Field x "Type"))
Merge x y t -> do
x' <- loop x
y' <- loop y
case x' of
RecordLit kvsX ->
case y' of
Field (Union ktsY) kY ->
case Dhall.Map.lookup kY ktsY of
Just Nothing ->
case Dhall.Map.lookup kY kvsX of
Just vX -> return vX
Nothing -> Merge x' y' <$> t'
_ ->
Merge x' y' <$> t'
App (Field (Union ktsY) kY) vY ->
case Dhall.Map.lookup kY ktsY of
Just (Just _) ->
case Dhall.Map.lookup kY kvsX of
Just vX -> loop (App vX vY)
Nothing -> Merge x' y' <$> t'
_ ->
Merge x' y' <$> t'
_ -> Merge x' y' <$> t'
_ -> Merge x' y' <$> t'
where
t' = traverse loop t
ToMap x t -> do
x' <- loop x
t' <- traverse loop t
case x' of
RecordLit kvsX -> do
let entry (key, value) =
RecordLit
(Dhall.Map.fromList
[ ("mapKey" , TextLit (Chunks [] key))
, ("mapValue", value )
]
)
let keyValues = Data.Sequence.fromList (map entry (Dhall.Map.toList kvsX))
let listType = case t' of
Just _ | null keyValues ->
t'
_ ->
Nothing
return (ListLit listType keyValues)
_ -> do
return (ToMap x' t')
Field r x -> do
let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v)
r' <- loop r
case r' of
RecordLit kvs ->
case Dhall.Map.lookup x kvs of
Just v -> pure v
Nothing -> Field <$> (RecordLit <$> traverse loop kvs) <*> pure x
Project r_ _ -> loop (Field r_ x)
Prefer (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Prefer (singletonRecordLit v) r_) x)
Nothing -> loop (Field r_ x)
Prefer l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
Just v -> pure v
Nothing -> loop (Field l x)
Combine (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Combine (singletonRecordLit v) r_) x)
Nothing -> loop (Field r_ x)
Combine l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Combine l (singletonRecordLit v)) x)
Nothing -> loop (Field l x)
_ -> pure (Field r' x)
Project x (Left fields)-> do
x' <- loop x
let fieldsSet = Dhall.Set.toSet fields
case x' of
RecordLit kvs ->
pure (RecordLit (Dhall.Map.restrictKeys kvs fieldsSet))
Project y _ ->
loop (Project y (Left fields))
Prefer l (RecordLit rKvs) -> do
let rKs = Dhall.Map.keysSet rKvs
let l' = Project l (Left (Dhall.Set.fromSet (Data.Set.difference fieldsSet rKs)))
let r' = RecordLit (Dhall.Map.restrictKeys rKvs fieldsSet)
loop (Prefer l' r')
_ | null fields -> pure (RecordLit mempty)
| otherwise -> pure (Project x' (Left (Dhall.Set.sort fields)))
Project r (Right e1) -> do
e2 <- loop e1
case e2 of
Record kts -> do
loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))
_ -> do
r' <- loop r
pure (Project r' (Right e2))
Assert t -> do
t' <- loop t
pure (Assert t')
Equivalent l r -> do
l' <- loop l
r' <- loop r
pure (Equivalent l' r')
Note _ e' -> loop e'
ImportAlt l _r -> loop l
Embed a -> pure (Embed a)
type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))
type Normalizer a = NormalizerM Identity a
newtype ReifiedNormalizer a = ReifiedNormalizer
{ getReifiedNormalizer :: Normalizer a }
isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e
isNormalized :: Eq a => Expr s a -> Bool
isNormalized e0 = loop (Syntax.denote e0)
where
loop e = case e of
Const _ -> True
Var _ -> True
Lam _ a b -> loop a && loop b
Pi _ a b -> loop a && loop b
App f a -> loop f && loop a && case App f a of
App (Lam _ _ _) _ -> False
App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
App NaturalFold (NaturalLit _) -> False
App NaturalBuild _ -> False
App NaturalIsZero (NaturalLit _) -> False
App NaturalEven (NaturalLit _) -> False
App NaturalOdd (NaturalLit _) -> False
App NaturalShow (NaturalLit _) -> False
App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False
App (App NaturalSubtract (NaturalLit 0)) _ -> False
App (App NaturalSubtract _) (NaturalLit 0) -> False
App (App NaturalSubtract x) y -> not (Eval.judgmentallyEqual x y)
App NaturalToInteger (NaturalLit _) -> False
App IntegerNegate (IntegerLit _) -> False
App IntegerClamp (IntegerLit _) -> False
App IntegerShow (IntegerLit _) -> False
App IntegerToDouble (IntegerLit _) -> False
App DoubleShow (DoubleLit _) -> False
App (App OptionalBuild _) _ -> False
App (App ListBuild _) _ -> False
App (App ListFold _) (ListLit _ _) -> False
App (App ListLength _) (ListLit _ _) -> False
App (App ListHead _) (ListLit _ _) -> False
App (App ListLast _) (ListLit _ _) -> False
App (App ListIndexed _) (ListLit _ _) -> False
App (App ListReverse _) (ListLit _ _) -> False
App (App OptionalFold _) (Some _) -> False
App (App OptionalFold _) (App None _) -> False
App TextShow (TextLit (Chunks [] _)) ->
False
_ -> True
Let _ _ -> False
Annot _ _ -> False
Bool -> True
BoolLit _ -> True
BoolAnd x y -> loop x && loop y && decide x y
where
decide (BoolLit _) _ = False
decide _ (BoolLit _) = False
decide l r = not (Eval.judgmentallyEqual l r)
BoolOr x y -> loop x && loop y && decide x y
where
decide (BoolLit _) _ = False
decide _ (BoolLit _) = False
decide l r = not (Eval.judgmentallyEqual l r)
BoolEQ x y -> loop x && loop y && decide x y
where
decide (BoolLit True) _ = False
decide _ (BoolLit True) = False
decide l r = not (Eval.judgmentallyEqual l r)
BoolNE x y -> loop x && loop y && decide x y
where
decide (BoolLit False) _ = False
decide _ (BoolLit False ) = False
decide l r = not (Eval.judgmentallyEqual l r)
BoolIf x y z ->
loop x && loop y && loop z && decide x y z
where
decide (BoolLit _) _ _ = False
decide _ (BoolLit True) (BoolLit False) = False
decide _ l r = not (Eval.judgmentallyEqual l r)
Natural -> True
NaturalLit _ -> True
NaturalFold -> True
NaturalBuild -> True
NaturalIsZero -> True
NaturalEven -> True
NaturalOdd -> True
NaturalShow -> True
NaturalSubtract -> True
NaturalToInteger -> True
NaturalPlus x y -> loop x && loop y && decide x y
where
decide (NaturalLit 0) _ = False
decide _ (NaturalLit 0) = False
decide (NaturalLit _) (NaturalLit _) = False
decide _ _ = True
NaturalTimes x y -> loop x && loop y && decide x y
where
decide (NaturalLit 0) _ = False
decide _ (NaturalLit 0) = False
decide (NaturalLit 1) _ = False
decide _ (NaturalLit 1) = False
decide (NaturalLit _) (NaturalLit _) = False
decide _ _ = True
Integer -> True
IntegerLit _ -> True
IntegerClamp -> True
IntegerNegate -> True
IntegerShow -> True
IntegerToDouble -> True
Double -> True
DoubleLit _ -> True
DoubleShow -> True
Text -> True
TextLit (Chunks [("", _)] "") -> False
TextLit (Chunks xys _) -> all (all check) xys
where
check y = loop y && case y of
TextLit _ -> False
_ -> True
TextAppend _ _ -> False
TextShow -> True
List -> True
ListLit t es -> all loop t && all loop es
ListAppend x y -> loop x && loop y && decide x y
where
decide (ListLit _ m) _ | Data.Sequence.null m = False
decide _ (ListLit _ n) | Data.Sequence.null n = False
decide (ListLit _ _) (ListLit _ _) = False
decide _ _ = True
ListBuild -> True
ListFold -> True
ListLength -> True
ListHead -> True
ListLast -> True
ListIndexed -> True
ListReverse -> True
Optional -> True
Some a -> loop a
None -> True
OptionalFold -> True
OptionalBuild -> True
Record kts -> Dhall.Map.isSorted kts && all loop kts
RecordLit kvs -> Dhall.Map.isSorted kvs && all loop kvs
Union kts -> Dhall.Map.isSorted kts && all (all loop) kts
Combine x y -> loop x && loop y && decide x y
where
decide (RecordLit m) _ | Data.Foldable.null m = False
decide _ (RecordLit n) | Data.Foldable.null n = False
decide (RecordLit _) (RecordLit _) = False
decide _ _ = True
CombineTypes x y -> loop x && loop y && decide x y
where
decide (Record m) _ | Data.Foldable.null m = False
decide _ (Record n) | Data.Foldable.null n = False
decide (Record _) (Record _) = False
decide _ _ = True
Prefer x y -> loop x && loop y && decide x y
where
decide (RecordLit m) _ | Data.Foldable.null m = False
decide _ (RecordLit n) | Data.Foldable.null n = False
decide (RecordLit _) (RecordLit _) = False
decide l r = not (Eval.judgmentallyEqual l r)
RecordCompletion _ _ -> False
Merge x y t -> loop x && loop y && all loop t
ToMap x t -> case x of
RecordLit _ -> False
_ -> loop x && all loop t
Field r k -> case r of
RecordLit _ -> False
Project _ _ -> False
Prefer (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
Prefer _ (RecordLit _) -> False
Combine (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
Combine _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r
_ -> loop r
Project r p -> loop r &&
case p of
Left s -> case r of
RecordLit _ -> False
Project _ _ -> False
Prefer _ (RecordLit _) -> False
_ -> not (Dhall.Set.null s) && Dhall.Set.isSorted s
Right e' -> case e' of
Record _ -> False
_ -> loop e'
Assert t -> loop t
Equivalent l r -> loop l && loop r
Note _ e' -> loop e'
ImportAlt _ _ -> False
Embed _ -> True
freeIn :: Eq a => Var -> Expr s a -> Bool
variable@(V var i) `freeIn` expression =
subst variable (Var (V var (i + 1))) strippedExpression
/= strippedExpression
where
denote' :: Expr t b -> Expr () b
denote' = Syntax.denote
strippedExpression = denote' expression