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