{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
module Dhall.Normalize (
alphaNormalize
, normalize
, normalizeWith
, normalizeWithM
, Normalizer
, NormalizerM
, ReifiedNormalizer (..)
, judgmentallyEqual
, subst
, shift
, isNormalized
, isNormalizedWith
, freeIn
) where
import Control.Applicative (empty)
import Data.Foldable
import Data.Functor.Identity (Identity(..))
import Data.Semigroup (Semigroup(..))
import Data.Sequence (ViewL(..), ViewR(..))
import Data.Traversable
import Dhall.Syntax (Expr(..), Var(..), Binding(Binding), Chunks(..), DhallDouble(..), Const(..))
import Instances.TH.Lift ()
import Prelude hiding (succ)
import qualified Data.Sequence
import qualified Data.Set
import qualified Data.Text
import qualified Dhall.Eval as Eval
import qualified Dhall.Map
import qualified Dhall.Set
import qualified Dhall.Syntax as Syntax
judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
judgmentallyEqual :: 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 _ _ (Const a :: Const
a) = Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
a
shift d :: Int
d (V x :: Text
x n :: Int
n) (Var (V x' :: Text
x' n' :: 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 d :: Int
d (V x :: Text
x n :: Int
n) (Lam x' :: Text
x' _A :: Expr s a
_A b :: 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
+ 1 else Int
n
shift d :: Int
d (V x :: Text
x n :: Int
n) (Pi x' :: Text
x' _A :: Expr s a
_A _B :: 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
+ 1 else Int
n
shift d :: Int
d v :: Var
v (App f :: Expr s a
f a :: 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
App Expr s a
f' Expr s a
a'
where
f' :: Expr s a
f' = 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
f
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 Var
v Expr s a
a
shift d :: Int
d (V x :: Text
x n :: Int
n) (Let (Binding src0 :: Maybe s
src0 f :: Text
f src1 :: Maybe s
src1 mt :: Maybe (Maybe s, Expr s a)
mt src2 :: Maybe s
src2 r :: Expr s a
r) e :: 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
+ 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 d :: Int
d v :: Var
v (Annot a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Annot 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 Var
v 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 Var
v Expr s a
b
shift _ _ Bool = Expr s a
forall s a. Expr s a
Bool
shift _ _ (BoolLit a :: Bool
a) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
a
shift d :: Int
d v :: Var
v (BoolAnd a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (BoolOr a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (BoolEQ a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (BoolNE a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (BoolIf a :: Expr s a
a b :: Expr s a
b c :: Expr s a
c) = 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
a' Expr s a
b' Expr s a
c'
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 Var
v 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 Var
v Expr s a
b
c' :: Expr s a
c' = 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
c
shift _ _ Natural = Expr s a
forall s a. Expr s a
Natural
shift _ _ (NaturalLit a :: Natural
a) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
a
shift _ _ NaturalFold = Expr s a
forall s a. Expr s a
NaturalFold
shift _ _ NaturalBuild = Expr s a
forall s a. Expr s a
NaturalBuild
shift _ _ NaturalIsZero = Expr s a
forall s a. Expr s a
NaturalIsZero
shift _ _ NaturalEven = Expr s a
forall s a. Expr s a
NaturalEven
shift _ _ NaturalOdd = Expr s a
forall s a. Expr s a
NaturalOdd
shift _ _ NaturalToInteger = Expr s a
forall s a. Expr s a
NaturalToInteger
shift _ _ NaturalShow = Expr s a
forall s a. Expr s a
NaturalShow
shift _ _ NaturalSubtract = Expr s a
forall s a. Expr s a
NaturalSubtract
shift d :: Int
d v :: Var
v (NaturalPlus a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (NaturalTimes a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift _ _ Integer = Expr s a
forall s a. Expr s a
Integer
shift _ _ (IntegerLit a :: Integer
a) = Integer -> Expr s a
forall s a. Integer -> Expr s a
IntegerLit Integer
a
shift _ _ IntegerClamp = Expr s a
forall s a. Expr s a
IntegerClamp
shift _ _ IntegerNegate = Expr s a
forall s a. Expr s a
IntegerNegate
shift _ _ IntegerShow = Expr s a
forall s a. Expr s a
IntegerShow
shift _ _ IntegerToDouble = Expr s a
forall s a. Expr s a
IntegerToDouble
shift _ _ Double = Expr s a
forall s a. Expr s a
Double
shift _ _ (DoubleLit a :: DhallDouble
a) = DhallDouble -> Expr s a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
a
shift _ _ DoubleShow = Expr s a
forall s a. Expr s a
DoubleShow
shift _ _ Text = Expr s a
forall s a. Expr s a
Text
shift d :: Int
d v :: Var
v (TextLit (Chunks a :: [(Text, Expr s a)]
a b :: Text
b)) = 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)]
a' Text
b)
where
a' :: [(Text, Expr s a)]
a' = ((Text, Expr s a) -> (Text, Expr s a))
-> [(Text, Expr s a)] -> [(Text, Expr s a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr s a -> Expr s a) -> (Text, Expr s a) -> (Text, 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 Var
v)) [(Text, Expr s a)]
a
shift d :: Int
d v :: Var
v (TextAppend a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend 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 Var
v 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 Var
v Expr s a
b
shift _ _ TextShow = Expr s a
forall s a. Expr s a
TextShow
shift _ _ List = Expr s a
forall s a. Expr s a
List
shift d :: Int
d v :: Var
v (ListLit a :: Maybe (Expr s a)
a b :: Seq (Expr s a)
b) = 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)
a' Seq (Expr s a)
b'
where
a' :: Maybe (Expr s a)
a' = (Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
v) Maybe (Expr s a)
a
b' :: Seq (Expr s a)
b' = (Expr s a -> Expr s a) -> Seq (Expr s a) -> Seq (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 Var
v) Seq (Expr s a)
b
shift _ _ ListBuild = Expr s a
forall s a. Expr s a
ListBuild
shift d :: Int
d v :: Var
v (ListAppend a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift _ _ ListFold = Expr s a
forall s a. Expr s a
ListFold
shift _ _ ListLength = Expr s a
forall s a. Expr s a
ListLength
shift _ _ ListHead = Expr s a
forall s a. Expr s a
ListHead
shift _ _ ListLast = Expr s a
forall s a. Expr s a
ListLast
shift _ _ ListIndexed = Expr s a
forall s a. Expr s a
ListIndexed
shift _ _ ListReverse = Expr s a
forall s a. Expr s a
ListReverse
shift _ _ Optional = Expr s a
forall s a. Expr s a
Optional
shift d :: Int
d v :: Var
v (Some a :: Expr s a
a) = Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some Expr s a
a'
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 Var
v Expr s a
a
shift _ _ None = Expr s a
forall s a. Expr s a
None
shift _ _ OptionalFold = Expr s a
forall s a. Expr s a
OptionalFold
shift _ _ OptionalBuild = Expr s a
forall s a. Expr s a
OptionalBuild
shift d :: Int
d v :: Var
v (Record a :: Map Text (Expr s a)
a) = 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)
a'
where
a' :: Map Text (Expr s a)
a' = (Expr s a -> Expr s a)
-> Map Text (Expr s a) -> Map Text (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 Var
v) Map Text (Expr s a)
a
shift d :: Int
d v :: Var
v (RecordLit a :: Map Text (Expr s a)
a) = 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)
a'
where
a' :: Map Text (Expr s a)
a' = (Expr s a -> Expr s a)
-> Map Text (Expr s a) -> Map Text (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 Var
v) Map Text (Expr s a)
a
shift d :: Int
d v :: Var
v (Union a :: Map Text (Maybe (Expr s a))
a) = 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))
a'
where
a' :: Map Text (Maybe (Expr s a))
a' = (Maybe (Expr s a) -> Maybe (Expr s a))
-> Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
v)) Map Text (Maybe (Expr s a))
a
shift d :: Int
d v :: Var
v (Combine a :: Maybe Text
a b :: Expr s a
b c :: Expr s a
c) = 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
a Expr s a
b' Expr s a
c'
where
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 Var
v Expr s a
b
c' :: Expr s a
c' = 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
c
shift d :: Int
d v :: Var
v (CombineTypes a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (Prefer a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer 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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (RecordCompletion a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
RecordCompletion 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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (Merge a :: Expr s a
a b :: Expr s a
b c :: Maybe (Expr s a)
c) = 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
a' Expr s a
b' Maybe (Expr s a)
c'
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 Var
v 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 Var
v Expr s a
b
c' :: Maybe (Expr s a)
c' = (Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
v) Maybe (Expr s a)
c
shift d :: Int
d v :: Var
v (ToMap a :: Expr s a
a b :: Maybe (Expr s a)
b) = 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
a' Maybe (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 Var
v Expr s a
a
b' :: Maybe (Expr s a)
b' = (Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
v) Maybe (Expr s a)
b
shift d :: Int
d v :: Var
v (Field a :: Expr s a
a b :: Text
b) = Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
a' Text
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 Var
v Expr s a
a
shift d :: Int
d v :: Var
v (Assert a :: Expr s a
a) = Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Assert Expr s a
a'
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 Var
v Expr s a
a
shift d :: Int
d v :: Var
v (Equivalent a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
v 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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (Project a :: Expr s a
a b :: Either (Set Text) (Expr s a)
b) = 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
a' Either (Set Text) (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 Var
v Expr s a
a
b' :: Either (Set Text) (Expr s a)
b' = (Expr s a -> Expr s a)
-> Either (Set Text) (Expr s a) -> Either (Set Text) (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 Var
v) Either (Set Text) (Expr s a)
b
shift d :: Int
d v :: Var
v (Note a :: s
a b :: Expr s a
b) = s -> Expr s a -> Expr s a
forall s a. s -> Expr s a -> Expr s a
Note s
a Expr s a
b'
where
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 Var
v Expr s a
b
shift d :: Int
d v :: Var
v (ImportAlt a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
ImportAlt 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 Var
v 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 Var
v Expr s a
b
shift _ _ (Embed p :: a
p) = a -> Expr s a
forall s a. a -> Expr s a
Embed a
p
subst :: Var -> Expr s a -> Expr s a -> Expr s a
subst :: Var -> Expr s a -> Expr s a -> Expr s a
subst _ _ (Const a :: Const
a) = Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
a
subst (V x :: Text
x n :: Int
n) e :: Expr s a
e (Lam y :: Text
y _A :: Expr s a
_A b :: 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 1 (Text -> Int -> Var
V Text
y 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
+ 1 else Int
n
subst (V x :: Text
x n :: Int
n) e :: Expr s a
e (Pi y :: Text
y _A :: Expr s a
_A _B :: 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 1 (Text -> Int -> Var
V Text
y 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
+ 1 else Int
n
subst v :: Var
v e :: Expr s a
e (App f :: Expr s a
f a :: 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
App Expr s a
f' Expr s a
a'
where
f' :: Expr s a
f' = 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
v Expr s a
e Expr s a
f
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 Var
v Expr s a
e Expr s a
a
subst v :: Var
v e :: Expr s a
e (Var v' :: 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 x :: Text
x n :: Int
n) e :: Expr s a
e (Let (Binding src0 :: Maybe s
src0 f :: Text
f src1 :: Maybe s
src1 mt :: Maybe (Maybe s, Expr s a)
mt src2 :: Maybe s
src2 r :: Expr s a
r) b :: 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 1 (Text -> Int -> Var
V Text
f 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
+ 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 x :: Var
x e :: Expr s a
e (Annot a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Annot 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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst _ _ Bool = Expr s a
forall s a. Expr s a
Bool
subst _ _ (BoolLit a :: Bool
a) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
a
subst x :: Var
x e :: Expr s a
e (BoolAnd a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (BoolOr a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (BoolEQ a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (BoolNE a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (BoolIf a :: Expr s a
a b :: Expr s a
b c :: Expr s a
c) = 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
a' Expr s a
b' Expr s a
c'
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 Var
x 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 Var
x Expr s a
e Expr s a
b
c' :: Expr s a
c' = 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
c
subst _ _ Natural = Expr s a
forall s a. Expr s a
Natural
subst _ _ (NaturalLit a :: Natural
a) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit Natural
a
subst _ _ NaturalFold = Expr s a
forall s a. Expr s a
NaturalFold
subst _ _ NaturalBuild = Expr s a
forall s a. Expr s a
NaturalBuild
subst _ _ NaturalIsZero = Expr s a
forall s a. Expr s a
NaturalIsZero
subst _ _ NaturalEven = Expr s a
forall s a. Expr s a
NaturalEven
subst _ _ NaturalOdd = Expr s a
forall s a. Expr s a
NaturalOdd
subst _ _ NaturalToInteger = Expr s a
forall s a. Expr s a
NaturalToInteger
subst _ _ NaturalShow = Expr s a
forall s a. Expr s a
NaturalShow
subst _ _ NaturalSubtract = Expr s a
forall s a. Expr s a
NaturalSubtract
subst x :: Var
x e :: Expr s a
e (NaturalPlus a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (NaturalTimes a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst _ _ Integer = Expr s a
forall s a. Expr s a
Integer
subst _ _ (IntegerLit a :: Integer
a) = Integer -> Expr s a
forall s a. Integer -> Expr s a
IntegerLit Integer
a
subst _ _ IntegerClamp = Expr s a
forall s a. Expr s a
IntegerClamp
subst _ _ IntegerNegate = Expr s a
forall s a. Expr s a
IntegerNegate
subst _ _ IntegerShow = Expr s a
forall s a. Expr s a
IntegerShow
subst _ _ IntegerToDouble = Expr s a
forall s a. Expr s a
IntegerToDouble
subst _ _ Double = Expr s a
forall s a. Expr s a
Double
subst _ _ (DoubleLit a :: DhallDouble
a) = DhallDouble -> Expr s a
forall s a. DhallDouble -> Expr s a
DoubleLit DhallDouble
a
subst _ _ DoubleShow = Expr s a
forall s a. Expr s a
DoubleShow
subst _ _ Text = Expr s a
forall s a. Expr s a
Text
subst x :: Var
x e :: Expr s a
e (TextLit (Chunks a :: [(Text, Expr s a)]
a b :: Text
b)) = 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)]
a' Text
b)
where
a' :: [(Text, Expr s a)]
a' = ((Text, Expr s a) -> (Text, Expr s a))
-> [(Text, Expr s a)] -> [(Text, Expr s a)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr s a -> Expr s a) -> (Text, Expr s a) -> (Text, 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 Var
x Expr s a
e)) [(Text, Expr s a)]
a
subst x :: Var
x e :: Expr s a
e (TextAppend a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
TextAppend 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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst _ _ TextShow = Expr s a
forall s a. Expr s a
TextShow
subst _ _ List = Expr s a
forall s a. Expr s a
List
subst x :: Var
x e :: Expr s a
e (ListLit a :: Maybe (Expr s a)
a b :: Seq (Expr s a)
b) = 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)
a' Seq (Expr s a)
b'
where
a' :: Maybe (Expr s a)
a' = (Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
x Expr s a
e) Maybe (Expr s a)
a
b' :: Seq (Expr s a)
b' = (Expr s a -> Expr s a) -> Seq (Expr s a) -> Seq (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 Var
x Expr s a
e) Seq (Expr s a)
b
subst x :: Var
x e :: Expr s a
e (ListAppend a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst _ _ ListBuild = Expr s a
forall s a. Expr s a
ListBuild
subst _ _ ListFold = Expr s a
forall s a. Expr s a
ListFold
subst _ _ ListLength = Expr s a
forall s a. Expr s a
ListLength
subst _ _ ListHead = Expr s a
forall s a. Expr s a
ListHead
subst _ _ ListLast = Expr s a
forall s a. Expr s a
ListLast
subst _ _ ListIndexed = Expr s a
forall s a. Expr s a
ListIndexed
subst _ _ ListReverse = Expr s a
forall s a. Expr s a
ListReverse
subst _ _ Optional = Expr s a
forall s a. Expr s a
Optional
subst x :: Var
x e :: Expr s a
e (Some a :: Expr s a
a) = Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some Expr s a
a'
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 Var
x Expr s a
e Expr s a
a
subst _ _ None = Expr s a
forall s a. Expr s a
None
subst _ _ OptionalFold = Expr s a
forall s a. Expr s a
OptionalFold
subst _ _ OptionalBuild = Expr s a
forall s a. Expr s a
OptionalBuild
subst x :: Var
x e :: Expr s a
e (Record kts :: 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)
kts'
where
kts' :: Map Text (Expr s a)
kts' = (Expr s a -> Expr s a)
-> Map Text (Expr s a) -> Map Text (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 Var
x Expr s a
e) Map Text (Expr s a)
kts
subst x :: Var
x e :: Expr s a
e (RecordLit kvs :: 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)
kvs'
where
kvs' :: Map Text (Expr s a)
kvs' = (Expr s a -> Expr s a)
-> Map Text (Expr s a) -> Map Text (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 Var
x Expr s a
e) Map Text (Expr s a)
kvs
subst x :: Var
x e :: Expr s a
e (Union kts :: 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))
kts'
where
kts' :: Map Text (Maybe (Expr s a))
kts' = (Maybe (Expr s a) -> Maybe (Expr s a))
-> Map Text (Maybe (Expr s a)) -> Map Text (Maybe (Expr s a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
x Expr s a
e)) Map Text (Maybe (Expr s a))
kts
subst x :: Var
x e :: Expr s a
e (Combine a :: Maybe Text
a b :: Expr s a
b c :: Expr s a
c) = 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
a Expr s a
b' Expr s a
c'
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 Var
x Expr s a
e Expr s a
b
c' :: Expr s a
c' = 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
c
subst x :: Var
x e :: Expr s a
e (CombineTypes a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (Prefer a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer 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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (RecordCompletion a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
RecordCompletion 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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (Merge a :: Expr s a
a b :: Expr s a
b c :: Maybe (Expr s a)
c) = 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
a' Expr s a
b' Maybe (Expr s a)
c'
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 Var
x 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 Var
x Expr s a
e Expr s a
b
c' :: Maybe (Expr s a)
c' = (Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
x Expr s a
e) Maybe (Expr s a)
c
subst x :: Var
x e :: Expr s a
e (ToMap a :: Expr s a
a b :: Maybe (Expr s a)
b) = 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
a' Maybe (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 Var
x Expr s a
e Expr s a
a
b' :: Maybe (Expr s a)
b' = (Expr s a -> Expr s a) -> Maybe (Expr s a) -> Maybe (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 Var
x Expr s a
e) Maybe (Expr s a)
b
subst x :: Var
x e :: Expr s a
e (Field a :: Expr s a
a b :: Text
b) = Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
a' Text
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 Var
x Expr s a
e Expr s a
a
subst x :: Var
x e :: Expr s a
e (Project a :: Expr s a
a b :: Either (Set Text) (Expr s a)
b) = 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
a' Either (Set Text) (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 Var
x Expr s a
e Expr s a
a
b' :: Either (Set Text) (Expr s a)
b' = (Expr s a -> Expr s a)
-> Either (Set Text) (Expr s a) -> Either (Set Text) (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 Var
x Expr s a
e) Either (Set Text) (Expr s a)
b
subst x :: Var
x e :: Expr s a
e (Assert a :: Expr s a
a) = Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Assert Expr s a
a'
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 Var
x Expr s a
e Expr s a
a
subst x :: Var
x e :: Expr s a
e (Equivalent a :: Expr s a
a b :: Expr s a
b) = 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
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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (Note a :: s
a b :: Expr s a
b) = s -> Expr s a -> Expr s a
forall s a. s -> Expr s a -> Expr s a
Note s
a 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 Var
x Expr s a
e Expr s a
b
subst x :: Var
x e :: Expr s a
e (ImportAlt a :: Expr s a
a b :: Expr s a
b) = Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
ImportAlt 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 Var
x 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 Var
x Expr s a
e Expr s a
b
subst _ _ (Embed p :: a
p) = a -> Expr s a
forall s a. a -> Expr s a
Embed a
p
boundedType :: Expr s a -> Bool
boundedType :: Expr s a -> Bool
boundedType Bool = Bool
True
boundedType Natural = Bool
True
boundedType Integer = Bool
True
boundedType Double = Bool
True
boundedType Text = Bool
True
boundedType (App List _) = Bool
False
boundedType (App Optional t :: Expr s a
t) = Expr s a -> Bool
forall s a. Expr s a -> Bool
boundedType Expr s a
t
boundedType (Record kvs :: 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 kvs :: 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 _ = 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 ctx :: ReifiedNormalizer a
ctx) t :: 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 _ t :: 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 ctx :: NormalizerM m a
ctx e0 :: 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 e :: Expr s a
e = case Expr s a
e of
Const k :: 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 v :: 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 x :: Text
x _A :: Expr s a
_A b :: 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 x :: Text
x _A :: Expr s a
_A _B :: 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 f :: Expr s a
f a :: 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 e1 :: Expr s a
e1 -> Expr s a -> m (Expr s a)
loop Expr s a
e1
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 x :: Text
x _A :: Expr s a
_A b₀ :: 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 1 (Text -> Int -> Var
V Text
x 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 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 (-1) (Text -> Int -> Var
V Text
x 0) Expr s a
b₁
Expr s a -> m (Expr s a)
loop Expr s a
b₂
_ -> 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 NaturalFold (NaturalLit n :: Natural
n) -> do
let natural :: Expr s a
natural = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "natural" 0)
let go :: t -> Expr s a -> Expr s a
go 0 x :: Expr s a
x = Expr s a
x
go n' :: t
n' x :: Expr s a
x = t -> Expr s a -> Expr s a
go (t
n't -> t -> t
forall a. Num a => a -> a -> a
-1) (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "succ" 0)) Expr s a
x)
let n' :: Expr s a
n' = Natural -> Expr s a -> Expr s a
forall t s a. (Eq t, Num t) => t -> Expr s a -> Expr s a
go Natural
n (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "zero" 0))
Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "natural"
(Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
Type)
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "succ"
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi "_" Expr s a
forall s a. Expr s a
natural Expr s a
forall s a. Expr s a
natural)
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "zero"
Expr s a
forall s a. Expr s a
natural
Expr s a
forall s a. Expr s a
n')))
App (App (App (App NaturalFold (NaturalLit n0 :: Natural
n0)) t :: Expr s a
t) succ' :: Expr s a
succ') zero :: 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
- 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
- 1))
App NaturalBuild g :: 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 "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 "n" (Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 1))
zero :: Expr s a
zero = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 0
App NaturalIsZero (NaturalLit n :: 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
== 0))
App NaturalEven (NaturalLit n :: 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 NaturalOdd (NaturalLit n :: 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 NaturalToInteger (NaturalLit n :: 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 NaturalShow (NaturalLit n :: 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 NaturalSubtract (NaturalLit x :: Natural
x)) (NaturalLit y :: 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 (Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
subtract Natural
x Natural
y))
| 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 0)
App (App NaturalSubtract (NaturalLit 0)) y :: 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 NaturalSubtract _) (NaturalLit 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 0)
App (App NaturalSubtract x :: Expr s a
x) y :: 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 0)
App IntegerClamp (IntegerLit n :: Integer
n)
| 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 0)
App IntegerNegate (IntegerLit n :: 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 IntegerShow (IntegerLit n :: Integer
n)
| 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
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 IntegerToDouble (IntegerLit n :: 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 DoubleShow (DoubleLit (DhallDouble n :: 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 OptionalBuild _A₀ :: Expr s a
_A₀) g :: 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
optional) Expr s a
just) Expr s a
nothing)
where
optional :: Expr s a
optional = 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
Optional Expr s a
_A₀
just :: Expr s a
just = Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "a" Expr s a
_A₀ (Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some "a")
nothing :: Expr s a
nothing = 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
_A₀
App (App ListBuild _A₀ :: Expr s a
_A₀) g :: 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 1 "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 "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 "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 "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 ListFold t :: Expr s a
t) (ListLit _ xs :: Seq (Expr s a)
xs) -> do
Expr s a
t' <- Expr s a -> m (Expr s a)
loop Expr s a
t
let list :: Expr s a
list = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "list" 0)
let lam :: Expr s a -> Expr s a
lam term :: Expr s a
term =
Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "list" (Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
Type)
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "cons" (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi "_" Expr s a
t' (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi "_" Expr s a
forall s a. Expr s a
list Expr s a
forall s a. Expr s a
list))
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "nil" Expr s a
forall s a. Expr s a
list Expr s a
term))
Expr s a
term <- (Expr s a -> Expr s a -> m (Expr s a))
-> Expr s a -> Seq (Expr s a) -> m (Expr s a)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> b -> m b) -> b -> t a -> m b
foldrM
(\x :: Expr s a
x acc :: Expr s a
acc -> do
Expr s a
x' <- Expr s a -> m (Expr s a)
loop Expr s a
x
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 -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "cons" 0)) Expr s a
x') Expr s a
acc))
(Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "nil" 0))
Seq (Expr s a)
xs
Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> Expr s a
lam Expr s a
term)
App (App (App (App (App ListFold _) (ListLit _ xs :: Seq (Expr s a)
xs)) t :: Expr s a
t) cons :: Expr s a
cons) nil :: 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 y :: Expr s a
y ys :: 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 y :: Expr s a
y ys :: 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 ListLength _) (ListLit _ ys :: 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 ListHead t :: Expr s a
t) (ListLit _ ys :: 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
y :: Expr s a
y :< _ -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some 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
App Expr s a
forall s a. Expr s a
None Expr s a
t
App (App ListLast t :: Expr s a
t) (ListLit _ ys :: 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
_ :> y :: Expr s a
y -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a
Some 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
App Expr s a
forall s a. Expr s a
None Expr s a
t
App (App ListIndexed _A₀ :: Expr s a
_A₀) (ListLit _ as₀ :: 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 = [ ("index", Expr s a
forall s a. Expr s a
Natural)
, ("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 n :: a
n a_ :: 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 = [ ("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))
, ("value", Expr s a
a_)
]
App (App ListReverse _) (ListLit t :: Maybe (Expr s a)
t xs :: 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 (App OptionalFold t0 :: Expr s a
t0) x0 :: Expr s a
x0 -> do
Expr s a
t1 <- Expr s a -> m (Expr s a)
loop Expr s a
t0
let optional :: Expr s a
optional = Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "optional" 0)
let lam :: Expr s a -> Expr s a
lam term :: Expr s a
term = (Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "optional"
(Const -> Expr s a
forall s a. Const -> Expr s a
Const Const
Type)
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "some"
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Pi "_" Expr s a
t1 Expr s a
forall s a. Expr s a
optional)
(Text -> Expr s a -> Expr s a -> Expr s a
forall s a. Text -> Expr s a -> Expr s a -> Expr s a
Lam "none" Expr s a
forall s a. Expr s a
optional Expr s a
term)))
Expr s a
x1 <- Expr s a -> m (Expr s a)
loop Expr s a
x0
Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Expr s a -> m (Expr s a)) -> Expr s a -> m (Expr s a)
forall a b. (a -> b) -> a -> b
$ case Expr s a
x1 of
App None _ -> Expr s a -> Expr s a
lam (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "none" 0))
Some x' :: Expr s a
x' -> Expr s a -> Expr s a
lam (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
App (Var -> Expr s a
forall s a. Var -> Expr s a
Var (Text -> Int -> Var
V "some" 0)) Expr s a
x')
_ -> 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
forall s a. Expr s a
OptionalFold Expr s a
t1) Expr s a
x1
App TextShow (TextLit (Chunks [] oldText :: 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
_ -> 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
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 app' :: Expr s a
app' -> Expr s a -> m (Expr s a)
loop Expr s a
app'
Let (Binding _ f :: Text
f _ _ _ r :: Expr s a
r) b :: 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 1 (Text -> Int -> Var
V Text
f 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 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 (-1) (Text -> Int -> Var
V Text
f 0) Expr s a
b'
Annot x :: Expr s a
x _ -> Expr s a -> m (Expr s a)
loop Expr s a
x
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 b :: 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 x :: Expr s a
x y :: 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 True ) r :: Expr s a
r = Expr s a
r
decide (BoolLit False) _ = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
decide l :: Expr s a
l (BoolLit True ) = Expr s a
l
decide _ (BoolLit False) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
False
decide l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 False) r :: Expr s a
r = Expr s a
r
decide (BoolLit True ) _ = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
decide l :: Expr s a
l (BoolLit False) = Expr s a
l
decide _ (BoolLit True ) = Bool -> Expr s a
forall s a. Bool -> Expr s a
BoolLit Bool
True
decide l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 True ) r :: Expr s a
r = Expr s a
r
decide l :: Expr s a
l (BoolLit True ) = Expr s a
l
decide l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 False) r :: Expr s a
r = Expr s a
r
decide l :: Expr s a
l (BoolLit False) = Expr s a
l
decide l :: Expr s a
l r :: 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 bool :: Expr s a
bool true :: Expr s a
true false :: 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 True ) l :: Expr s a
l _ = Expr s a
l
decide (BoolLit False) _ r :: Expr s a
r = Expr s a
r
decide b :: Expr s a
b (BoolLit True) (BoolLit False) = Expr s a
b
decide b :: Expr s a
b l :: Expr s a
l r :: 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
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 n :: 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)
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
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
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
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
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
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
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
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 x :: Expr s a
x y :: 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 0) r :: Expr s a
r = Expr s a
r
decide l :: Expr s a
l (NaturalLit 0) = Expr s a
l
decide (NaturalLit m :: Natural
m) (NaturalLit n :: 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 l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 1) r :: Expr s a
r = Expr s a
r
decide l :: Expr s a
l (NaturalLit 1) = Expr s a
l
decide (NaturalLit 0) _ = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 0
decide _ (NaturalLit 0) = Natural -> Expr s a
forall s a. Natural -> Expr s a
NaturalLit 0
decide (NaturalLit m :: Natural
m) (NaturalLit n :: 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 l :: Expr s a
l r :: 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
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 n :: 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)
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
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
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
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
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 n :: 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)
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
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 xys :: [(Text, Expr s a)]
xys z :: 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 [("", x :: Expr s a
x)] "" -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
x
c :: 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 (x :: Text
x, y :: 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 c :: 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]
_ -> [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 x :: Expr s a
x y :: 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 [("", Expr s a
x), ("", Expr s a
y)] ""))
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
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 t :: Maybe (Expr s a)
t es :: 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 x :: Expr s a
x y :: 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 _ m :: Seq (Expr s a)
m) r :: 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 l :: Expr s a
l (ListLit _ n :: 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 t :: Maybe (Expr s a)
t m :: Seq (Expr s a)
m) (ListLit _ n :: 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 l :: Expr s a
l r :: 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
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
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
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
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
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
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
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
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 a :: 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
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
OptionalFold -> 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
OptionalFold
OptionalBuild -> 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
OptionalBuild
Record kts :: 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 kvs :: 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 kts :: 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 mk :: Maybe Text
mk x :: Expr s a
x y :: 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 m :: Map Text (Expr s a)
m) r :: 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 l :: Expr s a
l (RecordLit n :: 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 m :: Map Text (Expr s a)
m) (RecordLit n :: 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 l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 m :: Map Text (Expr s a)
m) r :: 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 l :: Expr s a
l (Record n :: 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 m :: Map Text (Expr s a)
m) (Record n :: 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 l :: Expr s a
l r :: 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 x :: Expr s a
x y :: 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 m :: Map Text (Expr s a)
m) r :: 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 l :: Expr s a
l (RecordLit n :: 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 m :: Map Text (Expr s a)
m) (RecordLit n :: 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 l :: Expr s a
l r :: 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 l :: Expr s a
l r :: 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
Prefer Expr s a
l Expr s a
r
RecordCompletion x :: Expr s a
x y :: 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 (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer (Expr s a -> Text -> Expr s a
forall s a. Expr s a -> Text -> Expr s a
Field Expr s a
x "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 "Type"))
Merge x :: Expr s a
x y :: Expr s a
y t :: 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 kvsX :: Map Text (Expr s a)
kvsX ->
case Expr s a
y' of
Field (Union ktsY :: Map Text (Maybe (Expr s a))
ktsY) kY :: 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 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 vX :: Expr s a
vX -> Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
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 -> 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 ktsY :: Map Text (Maybe (Expr s a))
ktsY) kY :: Text
kY) vY :: 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 _) ->
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 vX :: 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)
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 -> 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 a :: 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 "Some" Map Text (Expr s a)
kvsX of
Just vX :: 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)
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 None _ ->
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 "None" Map Text (Expr s a)
kvsX of
Just vX :: Expr s a
vX -> Expr s a -> m (Expr s a)
forall (m :: * -> *) a. Monad m => a -> m a
return Expr s a
vX
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 -> 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 -> 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 x :: Expr s a
x t :: 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 kvsX :: Map Text (Expr s a)
kvsX -> do
let entry :: (Text, Expr s a) -> Expr s a
entry (key :: Text
key, value :: 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
[ ("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))
, ("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 _ | 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)
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)
_ -> 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 r :: Expr s a
r x :: Text
x -> do
let singletonRecordLit :: Expr s a -> Expr s a
singletonRecordLit v :: 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 kvs :: 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 v :: Expr s a
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
v
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 r_ :: Expr s a
r_ _ -> 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 (RecordLit kvs :: Map Text (Expr s a)
kvs) r_ :: 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 v :: 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 (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer (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)
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 l :: Expr s a
l (RecordLit kvs :: 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 v :: Expr s a
v -> Expr s a -> m (Expr s a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Expr s a
v
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 m :: Maybe Text
m (RecordLit kvs :: Map Text (Expr s a)
kvs) r_ :: 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 v :: 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)
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 m :: Maybe Text
m l :: Expr s a
l (RecordLit kvs :: 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 v :: 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)
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 -> 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 x :: Expr s a
x (Left fields :: 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 kvs :: 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 y :: Expr s a
y _ ->
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 l :: Expr s a
l (RecordLit rKvs :: 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 (Expr s a -> Expr s a -> Expr s a
forall s a. Expr s a -> Expr s a -> Expr s a
Prefer Expr s a
l' Expr s a
r')
_ | 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 r :: Expr s a
r (Right e1 :: 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 kts :: 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))))
_ -> 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 t :: 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 l :: Expr s a
l r :: 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')
Note _ e' :: Expr s a
e' -> Expr s a -> m (Expr s a)
loop Expr s a
e'
ImportAlt l :: Expr s a
l _r :: Expr s a
_r -> Expr s a -> m (Expr s a)
loop Expr s a
l
Embed a :: 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 ctx :: Normalizer a
ctx e :: 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 e0 :: 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 e :: Expr t a
e = case Expr t a
e of
Const _ -> Bool
True
Var _ -> Bool
True
Lam _ a :: Expr t a
a b :: 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 _ a :: Expr t a
a b :: 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 f :: Expr t a
f a :: 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 _ _ _) _ -> Bool
False
App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> Bool
False
App NaturalFold (NaturalLit _) -> Bool
False
App NaturalBuild _ -> Bool
False
App NaturalIsZero (NaturalLit _) -> Bool
False
App NaturalEven (NaturalLit _) -> Bool
False
App NaturalOdd (NaturalLit _) -> Bool
False
App NaturalShow (NaturalLit _) -> Bool
False
App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> Bool
False
App (App NaturalSubtract (NaturalLit 0)) _ -> Bool
False
App (App NaturalSubtract _) (NaturalLit 0) -> Bool
False
App (App NaturalSubtract x :: Expr t a
x) y :: 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 NaturalToInteger (NaturalLit _) -> Bool
False
App IntegerNegate (IntegerLit _) -> Bool
False
App IntegerClamp (IntegerLit _) -> Bool
False
App IntegerShow (IntegerLit _) -> Bool
False
App IntegerToDouble (IntegerLit _) -> Bool
False
App DoubleShow (DoubleLit _) -> Bool
False
App (App OptionalBuild _) _ -> Bool
False
App (App ListBuild _) _ -> Bool
False
App (App ListFold _) (ListLit _ _) -> Bool
False
App (App ListLength _) (ListLit _ _) -> Bool
False
App (App ListHead _) (ListLit _ _) -> Bool
False
App (App ListLast _) (ListLit _ _) -> Bool
False
App (App ListIndexed _) (ListLit _ _) -> Bool
False
App (App ListReverse _) (ListLit _ _) -> Bool
False
App (App OptionalFold _) (Some _) -> Bool
False
App (App OptionalFold _) (App None _) -> Bool
False
App TextShow (TextLit (Chunks [] _)) ->
Bool
False
_ -> Bool
True
Let _ _ -> Bool
False
Annot _ _ -> Bool
False
Bool -> Bool
True
BoolLit _ -> Bool
True
BoolAnd x :: Expr t a
x y :: 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
decide _ (BoolLit _) = Bool
False
decide l :: Expr s a
l r :: 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 x :: Expr t a
x y :: 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
decide _ (BoolLit _) = Bool
False
decide l :: Expr s a
l r :: 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 x :: Expr t a
x y :: 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 True) _ = Bool
False
decide _ (BoolLit True) = Bool
False
decide l :: Expr s a
l r :: 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 x :: Expr t a
x y :: 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 False) _ = Bool
False
decide _ (BoolLit False ) = Bool
False
decide l :: Expr s a
l r :: 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 x :: Expr t a
x y :: Expr t a
y z :: 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
False
decide _ (BoolLit True) (BoolLit False) = Bool
False
decide _ l :: Expr s a
l r :: 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)
Natural -> Bool
True
NaturalLit _ -> Bool
True
NaturalFold -> Bool
True
NaturalBuild -> Bool
True
NaturalIsZero -> Bool
True
NaturalEven -> Bool
True
NaturalOdd -> Bool
True
NaturalShow -> Bool
True
NaturalSubtract -> Bool
True
NaturalToInteger -> Bool
True
NaturalPlus x :: Expr t a
x y :: 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 0) _ = Bool
False
decide _ (NaturalLit 0) = Bool
False
decide (NaturalLit _) (NaturalLit _) = Bool
False
decide _ _ = Bool
True
NaturalTimes x :: Expr t a
x y :: 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 0) _ = Bool
False
decide _ (NaturalLit 0) = Bool
False
decide (NaturalLit 1) _ = Bool
False
decide _ (NaturalLit 1) = Bool
False
decide (NaturalLit _) (NaturalLit _) = Bool
False
decide _ _ = Bool
True
Integer -> Bool
True
IntegerLit _ -> Bool
True
IntegerClamp -> Bool
True
IntegerNegate -> Bool
True
IntegerShow -> Bool
True
IntegerToDouble -> Bool
True
Double -> Bool
True
DoubleLit _ -> Bool
True
DoubleShow -> Bool
True
Text -> Bool
True
TextLit (Chunks [("", _)] "") -> Bool
False
TextLit (Chunks xys :: [(Text, Expr t a)]
xys _) -> ((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 y :: Expr t a
y = Expr t a -> Bool
loop Expr t a
y Bool -> Bool -> Bool
&& case Expr t a
y of
TextLit _ -> Bool
False
_ -> Bool
True
TextAppend _ _ -> Bool
False
TextShow -> Bool
True
List -> Bool
True
ListLit t :: Maybe (Expr t a)
t es :: 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 x :: Expr t a
x y :: 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 _ m :: Seq (Expr s a)
m) _ | Seq (Expr s a) -> Bool
forall a. Seq a -> Bool
Data.Sequence.null Seq (Expr s a)
m = Bool
False
decide _ (ListLit _ n :: 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 _ _) (ListLit _ _) = Bool
False
decide _ _ = Bool
True
ListBuild -> Bool
True
ListFold -> Bool
True
ListLength -> Bool
True
ListHead -> Bool
True
ListLast -> Bool
True
ListIndexed -> Bool
True
ListReverse -> Bool
True
Optional -> Bool
True
Some a :: Expr t a
a -> Expr t a -> Bool
loop Expr t a
a
None -> Bool
True
OptionalFold -> Bool
True
OptionalBuild -> Bool
True
Record kts :: 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 kvs :: 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 kts :: 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 _ x :: Expr t a
x y :: 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 m :: Map Text (Expr s a)
m) _ | 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 _ (RecordLit n :: 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 _) (RecordLit _) = Bool
False
decide _ _ = Bool
True
CombineTypes x :: Expr t a
x y :: 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 m :: Map Text (Expr s a)
m) _ | 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 _ (Record n :: 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 _) (Record _) = Bool
False
decide _ _ = Bool
True
Prefer x :: Expr t a
x y :: 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 m :: Map Text (Expr s a)
m) _ | 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 _ (RecordLit n :: 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 _) (RecordLit _) = Bool
False
decide l :: Expr s a
l r :: 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 _ _ -> Bool
False
Merge x :: Expr t a
x y :: Expr t a
y t :: 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 _ -> case Expr t a
y of
Field (Union _) _ -> Bool
False
App (Field (Union _) _) _ -> Bool
False
Some _ -> Bool
False
App None _ -> Bool
False
_ -> Bool
True
_ -> Bool
True
ToMap x :: Expr t a
x t :: Maybe (Expr t a)
t -> case Expr t a
x of
RecordLit _ -> Bool
False
_ -> 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 r :: Expr t a
r k :: Text
k -> case Expr t a
r of
RecordLit _ -> Bool
False
Project _ _ -> Bool
False
Prefer (RecordLit m :: 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
Prefer _ (RecordLit _) -> Bool
False
Combine _ (RecordLit m :: 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
Combine _ _ (RecordLit m :: 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 -> Bool
loop Expr t a
r
Project r :: Expr t a
r p :: 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 s :: Set Text
s -> case Expr t a
r of
RecordLit _ -> Bool
False
Project _ _ -> Bool
False
Prefer _ (RecordLit _) -> Bool
False
_ -> 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 e' :: Expr t a
e' -> case Expr t a
e' of
Record _ -> Bool
False
_ -> Expr t a -> Bool
loop Expr t a
e'
Assert t :: Expr t a
t -> Expr t a -> Bool
loop Expr t a
t
Equivalent l :: Expr t a
l r :: 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
Note _ e' :: Expr t a
e' -> Expr t a -> Bool
loop Expr t a
e'
ImportAlt _ _ -> Bool
False
Embed _ -> Bool
True
freeIn :: Eq a => Var -> Expr s a -> Bool
variable :: Var
variable@(V var :: Text
var i :: Int
i) freeIn :: Var -> Expr s a -> Bool
`freeIn` expression :: 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
+ 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