{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE UnicodeSyntax #-}
{-# OPTIONS_GHC -Wall #-}
module Dhall.Core (
Const(..)
, Directory(..)
, File(..)
, FilePrefix(..)
, Import(..)
, ImportHashed(..)
, ImportMode(..)
, ImportType(..)
, URL(..)
, Scheme(..)
, Var(..)
, Chunks(..)
, Expr(..)
, Dhall.Core.alphaNormalize
, normalize
, normalizeWith
, normalizeWithM
, Normalizer
, NormalizerM
, ReifiedNormalizer (..)
, judgmentallyEqual
, subst
, shift
, isNormalized
, isNormalizedWith
, denote
, shallowDenote
, freeIn
, pretty
, subExpressions
, chunkExprs
, bindingExprs
, multiLet
, wrapInLets
, MultiLet(..)
, Binding(..)
, makeBinding
, internalError
, reservedIdentifiers
, escapeText
, pathCharacter
, throws
) where
#if MIN_VERSION_base(4,8,0)
#else
import Control.Applicative (Applicative(..), (<$>))
#endif
import Control.Applicative (empty)
import Control.DeepSeq (NFData)
import Control.Exception (Exception)
import Control.Monad.IO.Class (MonadIO(..))
import Crypto.Hash (SHA256)
import Data.Bifunctor (Bifunctor(..))
import Data.Data (Data)
import Data.Foldable
import Data.Functor.Identity (Identity(..))
import Data.HashSet (HashSet)
import Data.List.NonEmpty (NonEmpty(..))
import Data.String (IsString(..))
import Data.Semigroup (Semigroup(..))
import Data.Sequence (Seq, ViewL(..), ViewR(..))
import Data.Text (Text)
import Data.Text.Prettyprint.Doc (Doc, Pretty)
import Data.Traversable
import Dhall.Map (Map)
import Dhall.Set (Set)
import Dhall.Src (Src)
import {-# SOURCE #-} Dhall.Pretty.Internal
import GHC.Generics (Generic)
import Instances.TH.Lift ()
import Language.Haskell.TH.Syntax (Lift)
import Numeric.Natural (Natural)
import Prelude hiding (succ)
import qualified Control.Exception
import qualified Control.Monad
import qualified Crypto.Hash
import qualified Data.Char
import {-# SOURCE #-} qualified Dhall.Eval
import qualified Data.HashSet
import qualified Data.List.NonEmpty
import qualified Data.Sequence
import qualified Data.Text
import qualified Data.Text.Prettyprint.Doc as Pretty
import qualified Dhall.Map
import qualified Dhall.Set
import qualified Network.URI as URI
import qualified Text.Printf
data Const = Type | Kind | Sort
deriving (Show, Eq, Ord, Data, Bounded, Enum, Generic, NFData)
instance Lift Const
instance Pretty Const where
pretty = Pretty.unAnnotate . prettyConst
newtype Directory = Directory { components :: [Text] }
deriving (Eq, Generic, Ord, Show, NFData)
instance Semigroup Directory where
Directory components₀ <> Directory components₁ =
Directory (components₁ <> components₀)
instance Pretty Directory where
pretty (Directory {..}) = foldMap prettyPathComponent (reverse components)
data File = File
{ directory :: Directory
, file :: Text
} deriving (Eq, Generic, Ord, Show, NFData)
instance Pretty File where
pretty (File {..}) =
Pretty.pretty directory
<> prettyPathComponent file
instance Semigroup File where
File directory₀ _ <> File directory₁ file =
File (directory₀ <> directory₁) file
data FilePrefix
= Absolute
| Here
| Parent
| Home
deriving (Eq, Generic, Ord, Show, NFData)
instance Pretty FilePrefix where
pretty Absolute = ""
pretty Here = "."
pretty Parent = ".."
pretty Home = "~"
data Scheme = HTTP | HTTPS deriving (Eq, Generic, Ord, Show, NFData)
data URL = URL
{ scheme :: Scheme
, authority :: Text
, path :: File
, query :: Maybe Text
, headers :: Maybe (Expr Src Import)
} deriving (Eq, Generic, Ord, Show, NFData)
instance Pretty URL where
pretty (URL {..}) =
schemeDoc
<> "://"
<> Pretty.pretty authority
<> pathDoc
<> queryDoc
<> foldMap prettyHeaders headers
where
prettyHeaders h = " using " <> Pretty.pretty h
File {..} = path
Directory {..} = directory
pathDoc =
foldMap prettyURIComponent (reverse components)
<> prettyURIComponent file
schemeDoc = case scheme of
HTTP -> "http"
HTTPS -> "https"
queryDoc = case query of
Nothing -> ""
Just q -> "?" <> Pretty.pretty q
data ImportType
= Local FilePrefix File
| Remote URL
| Env Text
| Missing
deriving (Eq, Generic, Ord, Show, NFData)
parent :: File
parent = File { directory = Directory { components = [ ".." ] }, file = "" }
instance Semigroup ImportType where
Local prefix file₀ <> Local Here file₁ = Local prefix (file₀ <> file₁)
Remote (URL { path = path₀, ..}) <> Local Here path₁ =
Remote (URL { path = path₀ <> path₁, ..})
Local prefix file₀ <> Local Parent file₁ =
Local prefix (file₀ <> parent <> file₁)
Remote (URL { path = path₀, .. }) <> Local Parent path₁ =
Remote (URL { path = path₀ <> parent <> path₁, .. })
import₀ <> Remote (URL { headers = headers₀, .. }) =
Remote (URL { headers = headers₁, .. })
where
importHashed₀ = Import (ImportHashed Nothing import₀) Code
headers₁ = fmap (fmap (importHashed₀ <>)) headers₀
_ <> import₁ =
import₁
instance Pretty ImportType where
pretty (Local prefix file) =
Pretty.pretty prefix <> Pretty.pretty file
pretty (Remote url) = Pretty.pretty url
pretty (Env env) = "env:" <> Pretty.pretty env
pretty Missing = "missing"
data ImportMode = Code | RawText | Location
deriving (Eq, Generic, Ord, Show, NFData)
data ImportHashed = ImportHashed
{ hash :: Maybe (Crypto.Hash.Digest SHA256)
, importType :: ImportType
} deriving (Eq, Generic, Ord, Show, NFData)
instance Semigroup ImportHashed where
ImportHashed _ importType₀ <> ImportHashed hash importType₁ =
ImportHashed hash (importType₀ <> importType₁)
instance Pretty ImportHashed where
pretty (ImportHashed Nothing p) =
Pretty.pretty p
pretty (ImportHashed (Just h) p) =
Pretty.pretty p <> " sha256:" <> Pretty.pretty (show h)
data Import = Import
{ importHashed :: ImportHashed
, importMode :: ImportMode
} deriving (Eq, Generic, Ord, Show, NFData)
instance Semigroup Import where
Import importHashed₀ _ <> Import importHashed₁ code =
Import (importHashed₀ <> importHashed₁) code
instance Pretty Import where
pretty (Import {..}) = Pretty.pretty importHashed <> Pretty.pretty suffix
where
suffix :: Text
suffix = case importMode of
RawText -> " as Text"
Location -> " as Location"
Code -> ""
data Var = V Text !Int
deriving (Data, Generic, Eq, Ord, Show, NFData)
instance Lift Var
instance IsString Var where
fromString str = V (fromString str) 0
instance Pretty Var where
pretty = Pretty.unAnnotate . prettyVar
data Expr s a
= Const Const
| Var Var
| Lam Text (Expr s a) (Expr s a)
| Pi Text (Expr s a) (Expr s a)
| App (Expr s a) (Expr s a)
| Let (Binding s a) (Expr s a)
| Annot (Expr s a) (Expr s a)
| Bool
| BoolLit Bool
| BoolAnd (Expr s a) (Expr s a)
| BoolOr (Expr s a) (Expr s a)
| BoolEQ (Expr s a) (Expr s a)
| BoolNE (Expr s a) (Expr s a)
| BoolIf (Expr s a) (Expr s a) (Expr s a)
| Natural
| NaturalLit Natural
| NaturalFold
| NaturalBuild
| NaturalIsZero
| NaturalEven
| NaturalOdd
| NaturalToInteger
| NaturalShow
| NaturalSubtract
| NaturalPlus (Expr s a) (Expr s a)
| NaturalTimes (Expr s a) (Expr s a)
| Integer
| IntegerLit Integer
| IntegerShow
| IntegerToDouble
| Double
| DoubleLit Double
| DoubleShow
| Text
| TextLit (Chunks s a)
| TextAppend (Expr s a) (Expr s a)
| TextShow
| List
| ListLit (Maybe (Expr s a)) (Seq (Expr s a))
| ListAppend (Expr s a) (Expr s a)
| ListBuild
| ListFold
| ListLength
| ListHead
| ListLast
| ListIndexed
| ListReverse
| Optional
| Some (Expr s a)
| None
| OptionalFold
| OptionalBuild
| Record (Map Text (Expr s a))
| RecordLit (Map Text (Expr s a))
| Union (Map Text (Maybe (Expr s a)))
| Combine (Expr s a) (Expr s a)
| CombineTypes (Expr s a) (Expr s a)
| Prefer (Expr s a) (Expr s a)
| Merge (Expr s a) (Expr s a) (Maybe (Expr s a))
| ToMap (Expr s a) (Maybe (Expr s a))
| Field (Expr s a) Text
| Project (Expr s a) (Either (Set Text) (Expr s a))
| Assert (Expr s a)
| Equivalent (Expr s a) (Expr s a)
| Note s (Expr s a)
| ImportAlt (Expr s a) (Expr s a)
| Embed a
deriving (Foldable, Generic, Traversable, Show, Data, NFData)
deriving instance (Eq s, Eq a) => Eq (Expr s a)
deriving instance (Ord s, Ord a) => Ord (Expr s a)
instance (Lift s, Lift a, Data s, Data a) => Lift (Expr s a)
instance Functor (Expr s) where
fmap _ (Const c) = Const c
fmap _ (Var v) = Var v
fmap f (Lam v e1 e2) = Lam v (fmap f e1) (fmap f e2)
fmap f (Pi v e1 e2) = Pi v (fmap f e1) (fmap f e2)
fmap f (App e1 e2) = App (fmap f e1) (fmap f e2)
fmap f (Let b e2) = Let (fmap f b) (fmap f e2)
fmap f (Annot e1 e2) = Annot (fmap f e1) (fmap f e2)
fmap _ Bool = Bool
fmap _ (BoolLit b) = BoolLit b
fmap f (BoolAnd e1 e2) = BoolAnd (fmap f e1) (fmap f e2)
fmap f (BoolOr e1 e2) = BoolOr (fmap f e1) (fmap f e2)
fmap f (BoolEQ e1 e2) = BoolEQ (fmap f e1) (fmap f e2)
fmap f (BoolNE e1 e2) = BoolNE (fmap f e1) (fmap f e2)
fmap f (BoolIf e1 e2 e3) = BoolIf (fmap f e1) (fmap f e2) (fmap f e3)
fmap _ Natural = Natural
fmap _ (NaturalLit n) = NaturalLit n
fmap _ NaturalFold = NaturalFold
fmap _ NaturalBuild = NaturalBuild
fmap _ NaturalIsZero = NaturalIsZero
fmap _ NaturalEven = NaturalEven
fmap _ NaturalOdd = NaturalOdd
fmap _ NaturalToInteger = NaturalToInteger
fmap _ NaturalShow = NaturalShow
fmap _ NaturalSubtract = NaturalSubtract
fmap f (NaturalPlus e1 e2) = NaturalPlus (fmap f e1) (fmap f e2)
fmap f (NaturalTimes e1 e2) = NaturalTimes (fmap f e1) (fmap f e2)
fmap _ Integer = Integer
fmap _ (IntegerLit i) = IntegerLit i
fmap _ IntegerShow = IntegerShow
fmap _ IntegerToDouble = IntegerToDouble
fmap _ Double = Double
fmap _ (DoubleLit d) = DoubleLit d
fmap _ DoubleShow = DoubleShow
fmap _ Text = Text
fmap f (TextLit cs) = TextLit (fmap f cs)
fmap f (TextAppend e1 e2) = TextAppend (fmap f e1) (fmap f e2)
fmap _ TextShow = TextShow
fmap _ List = List
fmap f (ListLit maybeE seqE) = ListLit (fmap (fmap f) maybeE) (fmap (fmap f) seqE)
fmap f (ListAppend e1 e2) = ListAppend (fmap f e1) (fmap f e2)
fmap _ ListBuild = ListBuild
fmap _ ListFold = ListFold
fmap _ ListLength = ListLength
fmap _ ListHead = ListHead
fmap _ ListLast = ListLast
fmap _ ListIndexed = ListIndexed
fmap _ ListReverse = ListReverse
fmap _ Optional = Optional
fmap f (Some e) = Some (fmap f e)
fmap _ None = None
fmap _ OptionalFold = OptionalFold
fmap _ OptionalBuild = OptionalBuild
fmap f (Record r) = Record (fmap (fmap f) r)
fmap f (RecordLit r) = RecordLit (fmap (fmap f) r)
fmap f (Union u) = Union (fmap (fmap (fmap f)) u)
fmap f (Combine e1 e2) = Combine (fmap f e1) (fmap f e2)
fmap f (CombineTypes e1 e2) = CombineTypes (fmap f e1) (fmap f e2)
fmap f (Prefer e1 e2) = Prefer (fmap f e1) (fmap f e2)
fmap f (Merge e1 e2 maybeE) = Merge (fmap f e1) (fmap f e2) (fmap (fmap f) maybeE)
fmap f (ToMap e maybeE) = ToMap (fmap f e) (fmap (fmap f) maybeE)
fmap f (Field e1 v) = Field (fmap f e1) v
fmap f (Project e1 vs) = Project (fmap f e1) (fmap (fmap f) vs)
fmap f (Assert t) = Assert (fmap f t)
fmap f (Equivalent e1 e2) = Equivalent (fmap f e1) (fmap f e2)
fmap f (Note s e1) = Note s (fmap f e1)
fmap f (ImportAlt e1 e2) = ImportAlt (fmap f e1) (fmap f e2)
fmap f (Embed a) = Embed (f a)
{-# INLINABLE fmap #-}
instance Applicative (Expr s) where
pure = Embed
(<*>) = Control.Monad.ap
instance Monad (Expr s) where
return = pure
Const a >>= _ = Const a
Var a >>= _ = Var a
Lam a b c >>= k = Lam a (b >>= k) (c >>= k)
Pi a b c >>= k = Pi a (b >>= k) (c >>= k)
App a b >>= k = App (a >>= k) (b >>= k)
Let a b >>= k = Let (adapt0 a) (b >>= k)
where
adapt0 (Binding src0 c src1 d src2 e) =
Binding src0 c src1 (fmap adapt1 d) src2 (e >>= k)
adapt1 (src3, f) = (src3, f >>= k)
Annot a b >>= k = Annot (a >>= k) (b >>= k)
Bool >>= _ = Bool
BoolLit a >>= _ = BoolLit a
BoolAnd a b >>= k = BoolAnd (a >>= k) (b >>= k)
BoolOr a b >>= k = BoolOr (a >>= k) (b >>= k)
BoolEQ a b >>= k = BoolEQ (a >>= k) (b >>= k)
BoolNE a b >>= k = BoolNE (a >>= k) (b >>= k)
BoolIf a b c >>= k = BoolIf (a >>= k) (b >>= k) (c >>= k)
Natural >>= _ = Natural
NaturalLit a >>= _ = NaturalLit a
NaturalFold >>= _ = NaturalFold
NaturalBuild >>= _ = NaturalBuild
NaturalIsZero >>= _ = NaturalIsZero
NaturalEven >>= _ = NaturalEven
NaturalOdd >>= _ = NaturalOdd
NaturalToInteger >>= _ = NaturalToInteger
NaturalShow >>= _ = NaturalShow
NaturalSubtract >>= _ = NaturalSubtract
NaturalPlus a b >>= k = NaturalPlus (a >>= k) (b >>= k)
NaturalTimes a b >>= k = NaturalTimes (a >>= k) (b >>= k)
Integer >>= _ = Integer
IntegerLit a >>= _ = IntegerLit a
IntegerShow >>= _ = IntegerShow
IntegerToDouble >>= _ = IntegerToDouble
Double >>= _ = Double
DoubleLit a >>= _ = DoubleLit a
DoubleShow >>= _ = DoubleShow
Text >>= _ = Text
TextLit (Chunks a b) >>= k = TextLit (Chunks (fmap (fmap (>>= k)) a) b)
TextAppend a b >>= k = TextAppend (a >>= k) (b >>= k)
TextShow >>= _ = TextShow
List >>= _ = List
ListLit a b >>= k = ListLit (fmap (>>= k) a) (fmap (>>= k) b)
ListAppend a b >>= k = ListAppend (a >>= k) (b >>= k)
ListBuild >>= _ = ListBuild
ListFold >>= _ = ListFold
ListLength >>= _ = ListLength
ListHead >>= _ = ListHead
ListLast >>= _ = ListLast
ListIndexed >>= _ = ListIndexed
ListReverse >>= _ = ListReverse
Optional >>= _ = Optional
Some a >>= k = Some (a >>= k)
None >>= _ = None
OptionalFold >>= _ = OptionalFold
OptionalBuild >>= _ = OptionalBuild
Record a >>= k = Record (fmap (>>= k) a)
RecordLit a >>= k = RecordLit (fmap (>>= k) a)
Union a >>= k = Union (fmap (fmap (>>= k)) a)
Combine a b >>= k = Combine (a >>= k) (b >>= k)
CombineTypes a b >>= k = CombineTypes (a >>= k) (b >>= k)
Prefer a b >>= k = Prefer (a >>= k) (b >>= k)
Merge a b c >>= k = Merge (a >>= k) (b >>= k) (fmap (>>= k) c)
ToMap a b >>= k = ToMap (a >>= k) (fmap (>>= k) b)
Field a b >>= k = Field (a >>= k) b
Project a b >>= k = Project (a >>= k) (fmap (>>= k) b)
Assert a >>= k = Assert (a >>= k)
Equivalent a b >>= k = Equivalent (a >>= k) (b >>= k)
Note a b >>= k = Note a (b >>= k)
ImportAlt a b >>= k = ImportAlt (a >>= k) (b >>= k)
Embed a >>= k = k a
instance Bifunctor Expr where
first _ (Const a ) = Const a
first _ (Var a ) = Var a
first k (Lam a b c ) = Lam a (first k b) (first k c)
first k (Pi a b c ) = Pi a (first k b) (first k c)
first k (App a b ) = App (first k a) (first k b)
first k (Let a b ) = Let (first k a) (first k b)
first k (Annot a b ) = Annot (first k a) (first k b)
first _ Bool = Bool
first _ (BoolLit a ) = BoolLit a
first k (BoolAnd a b ) = BoolAnd (first k a) (first k b)
first k (BoolOr a b ) = BoolOr (first k a) (first k b)
first k (BoolEQ a b ) = BoolEQ (first k a) (first k b)
first k (BoolNE a b ) = BoolNE (first k a) (first k b)
first k (BoolIf a b c ) = BoolIf (first k a) (first k b) (first k c)
first _ Natural = Natural
first _ (NaturalLit a ) = NaturalLit a
first _ NaturalFold = NaturalFold
first _ NaturalBuild = NaturalBuild
first _ NaturalIsZero = NaturalIsZero
first _ NaturalEven = NaturalEven
first _ NaturalOdd = NaturalOdd
first _ NaturalToInteger = NaturalToInteger
first _ NaturalShow = NaturalShow
first _ NaturalSubtract = NaturalSubtract
first k (NaturalPlus a b ) = NaturalPlus (first k a) (first k b)
first k (NaturalTimes a b ) = NaturalTimes (first k a) (first k b)
first _ Integer = Integer
first _ (IntegerLit a ) = IntegerLit a
first _ IntegerShow = IntegerShow
first _ IntegerToDouble = IntegerToDouble
first _ Double = Double
first _ (DoubleLit a ) = DoubleLit a
first _ DoubleShow = DoubleShow
first _ Text = Text
first k (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap (first k)) a) b)
first k (TextAppend a b ) = TextAppend (first k a) (first k b)
first _ TextShow = TextShow
first _ List = List
first k (ListLit a b ) = ListLit (fmap (first k) a) (fmap (first k) b)
first k (ListAppend a b ) = ListAppend (first k a) (first k b)
first _ ListBuild = ListBuild
first _ ListFold = ListFold
first _ ListLength = ListLength
first _ ListHead = ListHead
first _ ListLast = ListLast
first _ ListIndexed = ListIndexed
first _ ListReverse = ListReverse
first _ Optional = Optional
first k (Some a ) = Some (first k a)
first _ None = None
first _ OptionalFold = OptionalFold
first _ OptionalBuild = OptionalBuild
first k (Record a ) = Record (fmap (first k) a)
first k (RecordLit a ) = RecordLit (fmap (first k) a)
first k (Union a ) = Union (fmap (fmap (first k)) a)
first k (Combine a b ) = Combine (first k a) (first k b)
first k (CombineTypes a b ) = CombineTypes (first k a) (first k b)
first k (Prefer a b ) = Prefer (first k a) (first k b)
first k (Merge a b c ) = Merge (first k a) (first k b) (fmap (first k) c)
first k (ToMap a b ) = ToMap (first k a) (fmap (first k) b)
first k (Field a b ) = Field (first k a) b
first k (Assert a ) = Assert (first k a)
first k (Equivalent a b ) = Equivalent (first k a) (first k b)
first k (Project a b ) = Project (first k a) (fmap (first k) b)
first k (Note a b ) = Note (k a) (first k b)
first k (ImportAlt a b ) = ImportAlt (first k a) (first k b)
first _ (Embed a ) = Embed a
second = fmap
instance IsString (Expr s a) where
fromString str = Var (fromString str)
data Chunks s a = Chunks [(Text, Expr s a)] Text
deriving (Functor, Foldable, Generic, Traversable, Show, Eq, Ord, Data, NFData)
instance (Lift s, Lift a, Data s, Data a) => Lift (Chunks s a)
instance Data.Semigroup.Semigroup (Chunks s a) where
Chunks xysL zL <> Chunks [] zR =
Chunks xysL (zL <> zR)
Chunks xysL zL <> Chunks ((x, y):xysR) zR =
Chunks (xysL ++ (zL <> x, y):xysR) zR
instance Monoid (Chunks s a) where
mempty = Chunks [] mempty
#if !(MIN_VERSION_base(4,11,0))
mappend = (<>)
#endif
instance IsString (Chunks s a) where
fromString str = Chunks [] (fromString str)
instance Pretty a => Pretty (Expr s a) where
pretty = Pretty.unAnnotate . prettyExpr
shift :: Int -> Var -> Expr s a -> Expr s a
shift _ _ (Const a) = Const a
shift d (V x n) (Var (V x' n')) = Var (V x' n'')
where
n'' = if x == x' && n <= n' then n' + d else n'
shift d (V x n) (Lam x' _A b) = Lam x' _A' b'
where
_A' = shift d (V x n ) _A
b' = shift d (V x n') b
where
n' = if x == x' then n + 1 else n
shift d (V x n) (Pi x' _A _B) = Pi x' _A' _B'
where
_A' = shift d (V x n ) _A
_B' = shift d (V x n') _B
where
n' = if x == x' then n + 1 else n
shift d v (App f a) = App f' a'
where
f' = shift d v f
a' = shift d v a
shift d (V x n) (Let (Binding src0 f src1 mt src2 r) e) =
Let (Binding src0 f src1 mt' src2 r') e'
where
e' = shift d (V x n') e
where
n' = if x == f then n + 1 else n
mt' = fmap (fmap (shift d (V x n))) mt
r' = shift d (V x n) r
shift d v (Annot a b) = Annot a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ Bool = Bool
shift _ _ (BoolLit a) = BoolLit a
shift d v (BoolAnd a b) = BoolAnd a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolOr a b) = BoolOr a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolEQ a b) = BoolEQ a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolNE a b) = BoolNE a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (BoolIf a b c) = BoolIf a' b' c'
where
a' = shift d v a
b' = shift d v b
c' = shift d v c
shift _ _ Natural = Natural
shift _ _ (NaturalLit a) = NaturalLit a
shift _ _ NaturalFold = NaturalFold
shift _ _ NaturalBuild = NaturalBuild
shift _ _ NaturalIsZero = NaturalIsZero
shift _ _ NaturalEven = NaturalEven
shift _ _ NaturalOdd = NaturalOdd
shift _ _ NaturalToInteger = NaturalToInteger
shift _ _ NaturalShow = NaturalShow
shift _ _ NaturalSubtract = NaturalSubtract
shift d v (NaturalPlus a b) = NaturalPlus a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (NaturalTimes a b) = NaturalTimes a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ Integer = Integer
shift _ _ (IntegerLit a) = IntegerLit a
shift _ _ IntegerShow = IntegerShow
shift _ _ IntegerToDouble = IntegerToDouble
shift _ _ Double = Double
shift _ _ (DoubleLit a) = DoubleLit a
shift _ _ DoubleShow = DoubleShow
shift _ _ Text = Text
shift d v (TextLit (Chunks a b)) = TextLit (Chunks a' b)
where
a' = fmap (fmap (shift d v)) a
shift d v (TextAppend a b) = TextAppend a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ TextShow = TextShow
shift _ _ List = List
shift d v (ListLit a b) = ListLit a' b'
where
a' = fmap (shift d v) a
b' = fmap (shift d v) b
shift _ _ ListBuild = ListBuild
shift d v (ListAppend a b) = ListAppend a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ ListFold = ListFold
shift _ _ ListLength = ListLength
shift _ _ ListHead = ListHead
shift _ _ ListLast = ListLast
shift _ _ ListIndexed = ListIndexed
shift _ _ ListReverse = ListReverse
shift _ _ Optional = Optional
shift d v (Some a) = Some a'
where
a' = shift d v a
shift _ _ None = None
shift _ _ OptionalFold = OptionalFold
shift _ _ OptionalBuild = OptionalBuild
shift d v (Record a) = Record a'
where
a' = fmap (shift d v) a
shift d v (RecordLit a) = RecordLit a'
where
a' = fmap (shift d v) a
shift d v (Union a) = Union a'
where
a' = fmap (fmap (shift d v)) a
shift d v (Combine a b) = Combine a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (CombineTypes a b) = CombineTypes a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (Prefer a b) = Prefer a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (Merge a b c) = Merge a' b' c'
where
a' = shift d v a
b' = shift d v b
c' = fmap (shift d v) c
shift d v (ToMap a b) = ToMap a' b'
where
a' = shift d v a
b' = fmap (shift d v) b
shift d v (Field a b) = Field a' b
where
a' = shift d v a
shift d v (Assert a) = Assert a'
where
a' = shift d v a
shift d v (Equivalent a b) = Equivalent a' b'
where
a' = shift d v a
b' = shift d v b
shift d v (Project a b) = Project a' b'
where
a' = shift d v a
b' = fmap (shift d v) b
shift d v (Note a b) = Note a b'
where
b' = shift d v b
shift d v (ImportAlt a b) = ImportAlt a' b'
where
a' = shift d v a
b' = shift d v b
shift _ _ (Embed p) = Embed p
subst :: Var -> Expr s a -> Expr s a -> Expr s a
subst _ _ (Const a) = Const a
subst (V x n) e (Lam y _A b) = Lam y _A' b'
where
_A' = subst (V x n ) e _A
b' = subst (V x n') (shift 1 (V y 0) e) b
n' = if x == y then n + 1 else n
subst (V x n) e (Pi y _A _B) = Pi y _A' _B'
where
_A' = subst (V x n ) e _A
_B' = subst (V x n') (shift 1 (V y 0) e) _B
n' = if x == y then n + 1 else n
subst v e (App f a) = App f' a'
where
f' = subst v e f
a' = subst v e a
subst v e (Var v') = if v == v' then e else Var v'
subst (V x n) e (Let (Binding src0 f src1 mt src2 r) b) =
Let (Binding src0 f src1 mt' src2 r') b'
where
b' = subst (V x n') (shift 1 (V f 0) e) b
where
n' = if x == f then n + 1 else n
mt' = fmap (fmap (subst (V x n) e)) mt
r' = subst (V x n) e r
subst x e (Annot a b) = Annot a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ Bool = Bool
subst _ _ (BoolLit a) = BoolLit a
subst x e (BoolAnd a b) = BoolAnd a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolOr a b) = BoolOr a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolEQ a b) = BoolEQ a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolNE a b) = BoolNE a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (BoolIf a b c) = BoolIf a' b' c'
where
a' = subst x e a
b' = subst x e b
c' = subst x e c
subst _ _ Natural = Natural
subst _ _ (NaturalLit a) = NaturalLit a
subst _ _ NaturalFold = NaturalFold
subst _ _ NaturalBuild = NaturalBuild
subst _ _ NaturalIsZero = NaturalIsZero
subst _ _ NaturalEven = NaturalEven
subst _ _ NaturalOdd = NaturalOdd
subst _ _ NaturalToInteger = NaturalToInteger
subst _ _ NaturalShow = NaturalShow
subst _ _ NaturalSubtract = NaturalSubtract
subst x e (NaturalPlus a b) = NaturalPlus a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (NaturalTimes a b) = NaturalTimes a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ Integer = Integer
subst _ _ (IntegerLit a) = IntegerLit a
subst _ _ IntegerShow = IntegerShow
subst _ _ IntegerToDouble = IntegerToDouble
subst _ _ Double = Double
subst _ _ (DoubleLit a) = DoubleLit a
subst _ _ DoubleShow = DoubleShow
subst _ _ Text = Text
subst x e (TextLit (Chunks a b)) = TextLit (Chunks a' b)
where
a' = fmap (fmap (subst x e)) a
subst x e (TextAppend a b) = TextAppend a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ TextShow = TextShow
subst _ _ List = List
subst x e (ListLit a b) = ListLit a' b'
where
a' = fmap (subst x e) a
b' = fmap (subst x e) b
subst x e (ListAppend a b) = ListAppend a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ ListBuild = ListBuild
subst _ _ ListFold = ListFold
subst _ _ ListLength = ListLength
subst _ _ ListHead = ListHead
subst _ _ ListLast = ListLast
subst _ _ ListIndexed = ListIndexed
subst _ _ ListReverse = ListReverse
subst _ _ Optional = Optional
subst x e (Some a) = Some a'
where
a' = subst x e a
subst _ _ None = None
subst _ _ OptionalFold = OptionalFold
subst _ _ OptionalBuild = OptionalBuild
subst x e (Record kts) = Record kts'
where
kts' = fmap (subst x e) kts
subst x e (RecordLit kvs) = RecordLit kvs'
where
kvs' = fmap (subst x e) kvs
subst x e (Union kts) = Union kts'
where
kts' = fmap (fmap (subst x e)) kts
subst x e (Combine a b) = Combine a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (CombineTypes a b) = CombineTypes a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (Prefer a b) = Prefer a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (Merge a b c) = Merge a' b' c'
where
a' = subst x e a
b' = subst x e b
c' = fmap (subst x e) c
subst x e (ToMap a b) = ToMap a' b'
where
a' = subst x e a
b' = fmap (subst x e) b
subst x e (Field a b) = Field a' b
where
a' = subst x e a
subst x e (Project a b) = Project a' b'
where
a' = subst x e a
b' = fmap (subst x e) b
subst x e (Assert a) = Assert a'
where
a' = subst x e a
subst x e (Equivalent a b) = Equivalent a' b'
where
a' = subst x e a
b' = subst x e b
subst x e (Note a b) = Note a b'
where
b' = subst x e b
subst x e (ImportAlt a b) = ImportAlt a' b'
where
a' = subst x e a
b' = subst x e b
subst _ _ (Embed p) = Embed p
alphaNormalize :: Expr s a -> Expr s a
alphaNormalize = Dhall.Eval.alphaNormalize
normalize :: Eq a => Expr s a -> Expr t a
normalize = Dhall.Eval.nfEmpty
boundedType :: Expr s a -> Bool
boundedType Bool = True
boundedType Natural = True
boundedType Integer = True
boundedType Double = True
boundedType Text = True
boundedType (App List _) = False
boundedType (App Optional t) = boundedType t
boundedType (Record kvs) = all boundedType kvs
boundedType (Union kvs) = all (all boundedType) kvs
boundedType _ = False
denote :: Expr s a -> Expr t a
denote (Note _ b ) = denote b
denote (Const a ) = Const a
denote (Var a ) = Var a
denote (Lam a b c ) = Lam a (denote b) (denote c)
denote (Pi a b c ) = Pi a (denote b) (denote c)
denote (App a b ) = App (denote a) (denote b)
denote (Let a b ) = Let (adapt0 a) (denote b)
where
adapt0 (Binding _ c _ d _ e) =
Binding Nothing c Nothing (fmap adapt1 d) Nothing (denote e)
adapt1 (_, f) = (Nothing, denote f)
denote (Annot a b ) = Annot (denote a) (denote b)
denote Bool = Bool
denote (BoolLit a ) = BoolLit a
denote (BoolAnd a b ) = BoolAnd (denote a) (denote b)
denote (BoolOr a b ) = BoolOr (denote a) (denote b)
denote (BoolEQ a b ) = BoolEQ (denote a) (denote b)
denote (BoolNE a b ) = BoolNE (denote a) (denote b)
denote (BoolIf a b c ) = BoolIf (denote a) (denote b) (denote c)
denote Natural = Natural
denote (NaturalLit a ) = NaturalLit a
denote NaturalFold = NaturalFold
denote NaturalBuild = NaturalBuild
denote NaturalIsZero = NaturalIsZero
denote NaturalEven = NaturalEven
denote NaturalOdd = NaturalOdd
denote NaturalToInteger = NaturalToInteger
denote NaturalShow = NaturalShow
denote NaturalSubtract = NaturalSubtract
denote (NaturalPlus a b ) = NaturalPlus (denote a) (denote b)
denote (NaturalTimes a b ) = NaturalTimes (denote a) (denote b)
denote Integer = Integer
denote (IntegerLit a ) = IntegerLit a
denote IntegerShow = IntegerShow
denote IntegerToDouble = IntegerToDouble
denote Double = Double
denote (DoubleLit a ) = DoubleLit a
denote DoubleShow = DoubleShow
denote Text = Text
denote (TextLit (Chunks a b)) = TextLit (Chunks (fmap (fmap denote) a) b)
denote (TextAppend a b ) = TextAppend (denote a) (denote b)
denote TextShow = TextShow
denote List = List
denote (ListLit a b ) = ListLit (fmap denote a) (fmap denote b)
denote (ListAppend a b ) = ListAppend (denote a) (denote b)
denote ListBuild = ListBuild
denote ListFold = ListFold
denote ListLength = ListLength
denote ListHead = ListHead
denote ListLast = ListLast
denote ListIndexed = ListIndexed
denote ListReverse = ListReverse
denote Optional = Optional
denote (Some a ) = Some (denote a)
denote None = None
denote OptionalFold = OptionalFold
denote OptionalBuild = OptionalBuild
denote (Record a ) = Record (fmap denote a)
denote (RecordLit a ) = RecordLit (fmap denote a)
denote (Union a ) = Union (fmap (fmap denote) a)
denote (Combine a b ) = Combine (denote a) (denote b)
denote (CombineTypes a b ) = CombineTypes (denote a) (denote b)
denote (Prefer a b ) = Prefer (denote a) (denote b)
denote (Merge a b c ) = Merge (denote a) (denote b) (fmap denote c)
denote (ToMap a b ) = ToMap (denote a) (fmap denote b)
denote (Field a b ) = Field (denote a) b
denote (Project a b ) = Project (denote a) (fmap denote b)
denote (Assert a ) = Assert (denote a)
denote (Equivalent a b ) = Equivalent (denote a) (denote b)
denote (ImportAlt a b ) = ImportAlt (denote a) (denote b)
denote (Embed a ) = Embed a
shallowDenote :: Expr s a -> Expr s a
shallowDenote (Note _ e) = shallowDenote e
shallowDenote e = e
normalizeWith :: Eq a => Maybe (ReifiedNormalizer a) -> Expr s a -> Expr t a
normalizeWith (Just ctx) t = runIdentity (normalizeWithM (getReifiedNormalizer ctx) t)
normalizeWith _ t = Dhall.Eval.nfEmpty t
normalizeWithM
:: (Monad m, Eq a) => NormalizerM m a -> Expr s a -> m (Expr t a)
normalizeWithM ctx e0 = loop (denote e0)
where
loop e = case e of
Const k -> pure (Const k)
Var v -> pure (Var v)
Lam x _A b -> Lam x <$> _A' <*> b'
where
_A' = loop _A
b' = loop b
Pi x _A _B -> Pi x <$> _A' <*> _B'
where
_A' = loop _A
_B' = loop _B
App f a -> do
res <- ctx (App f a)
case res of
Just e1 -> loop e1
Nothing -> do
f' <- loop f
a' <- loop a
case f' of
Lam x _A b₀ -> do
let a₂ = shift 1 (V x 0) a'
let b₁ = subst (V x 0) a₂ b₀
let b₂ = shift (-1) (V x 0) b₁
loop b₂
_ -> do
case App f' a' of
App (App ListBuild _) (App (App ListFold _) e') -> loop e'
App NaturalFold (NaturalLit n) -> do
let natural = Var (V "natural" 0)
let go 0 x = x
go n' x = go (n'-1) (App (Var (V "succ" 0)) x)
let n' = go n (Var (V "zero" 0))
pure
(Lam "natural"
(Const Type)
(Lam "succ"
(Pi "_" natural natural)
(Lam "zero"
natural
n')))
App NaturalBuild (App NaturalFold e') -> loop e'
App (App OptionalBuild _) (App (App OptionalFold _) e') -> loop e'
App (App (App (App NaturalFold (NaturalLit n0)) t) succ') zero -> do
t' <- loop t
if boundedType t' then strict else lazy
where
strict = strictLoop (fromIntegral n0 :: Integer)
lazy = loop ( lazyLoop (fromIntegral n0 :: Integer))
strictLoop !0 = loop zero
strictLoop !n = App succ' <$> strictLoop (n - 1) >>= loop
lazyLoop !0 = zero
lazyLoop !n = App succ' (lazyLoop (n - 1))
App NaturalBuild g -> loop (App (App (App g Natural) succ) zero)
where
succ = Lam "n" Natural (NaturalPlus "n" (NaturalLit 1))
zero = NaturalLit 0
App NaturalIsZero (NaturalLit n) -> pure (BoolLit (n == 0))
App NaturalEven (NaturalLit n) -> pure (BoolLit (even n))
App NaturalOdd (NaturalLit n) -> pure (BoolLit (odd n))
App NaturalToInteger (NaturalLit n) -> pure (IntegerLit (toInteger n))
App NaturalShow (NaturalLit n) ->
pure (TextLit (Chunks [] (Data.Text.pack (show n))))
App (App NaturalSubtract (NaturalLit x)) (NaturalLit y)
| y >= x -> pure (NaturalLit (subtract x y))
| otherwise -> pure (NaturalLit 0)
App (App NaturalSubtract (NaturalLit 0)) y -> pure y
App (App NaturalSubtract _) (NaturalLit 0) -> pure (NaturalLit 0)
App (App NaturalSubtract x) y | judgmentallyEqual x y -> pure (NaturalLit 0)
App IntegerShow (IntegerLit n)
| 0 <= n -> pure (TextLit (Chunks [] ("+" <> Data.Text.pack (show n))))
| otherwise -> pure (TextLit (Chunks [] (Data.Text.pack (show n))))
App IntegerToDouble (IntegerLit n) -> pure (DoubleLit ((read . show) n))
App DoubleShow (DoubleLit n) ->
pure (TextLit (Chunks [] (Data.Text.pack (show n))))
App (App OptionalBuild _A₀) g ->
loop (App (App (App g optional) just) nothing)
where
optional = App Optional _A₀
just = Lam "a" _A₀ (Some "a")
nothing = App None _A₀
App (App ListBuild _A₀) g -> loop (App (App (App g list) cons) nil)
where
_A₁ = shift 1 "a" _A₀
list = App List _A₀
cons =
Lam "a" _A₀
(Lam "as"
(App List _A₁)
(ListAppend (ListLit Nothing (pure "a")) "as")
)
nil = ListLit (Just (App List _A₀)) empty
App (App ListFold t) (ListLit _ xs) -> do
t' <- loop t
let list = Var (V "list" 0)
let lam term =
Lam "list" (Const Type)
(Lam "cons" (Pi "_" t' (Pi "_" list list))
(Lam "nil" list term))
term <- foldrM
(\x acc -> do
x' <- loop x
pure (App (App (Var (V "cons" 0)) x') acc))
(Var (V "nil" 0))
xs
pure (lam term)
App (App (App (App (App ListFold _) (ListLit _ xs)) t) cons) nil -> do
t' <- loop t
if boundedType t' then strict else lazy
where
strict = foldr strictCons strictNil xs
lazy = loop (foldr lazyCons lazyNil xs)
strictNil = loop nil
lazyNil = nil
strictCons y ys = do
App (App cons y) <$> ys >>= loop
lazyCons y ys = App (App cons y) ys
App (App ListLength _) (ListLit _ ys) ->
pure (NaturalLit (fromIntegral (Data.Sequence.length ys)))
App (App ListHead t) (ListLit _ ys) -> loop o
where
o = case Data.Sequence.viewl ys of
y :< _ -> Some y
_ -> App None t
App (App ListLast t) (ListLit _ ys) -> loop o
where
o = case Data.Sequence.viewr ys of
_ :> y -> Some y
_ -> App None t
App (App ListIndexed _A₀) (ListLit _ as₀) -> loop (ListLit t as₁)
where
as₁ = Data.Sequence.mapWithIndex adapt as₀
_A₂ = Record (Dhall.Map.fromList kts)
where
kts = [ ("index", Natural)
, ("value", _A₀)
]
t | null as₀ = Just (App List _A₂)
| otherwise = Nothing
adapt n a_ =
RecordLit (Dhall.Map.fromList kvs)
where
kvs = [ ("index", NaturalLit (fromIntegral n))
, ("value", a_)
]
App (App ListReverse _) (ListLit t xs) ->
loop (ListLit t (Data.Sequence.reverse xs))
App (App OptionalFold t0) x0 -> do
t1 <- loop t0
let optional = Var (V "optional" 0)
let lam term = (Lam "optional"
(Const Type)
(Lam "some"
(Pi "_" t1 optional)
(Lam "none" optional term)))
x1 <- loop x0
pure $ case x1 of
App None _ -> lam (Var (V "none" 0))
Some x' -> lam (App (Var (V "some" 0)) x')
_ -> App (App OptionalFold t1) x1
App TextShow (TextLit (Chunks [] oldText)) ->
loop (TextLit (Chunks [] newText))
where
newText = textShow oldText
_ -> do
res2 <- ctx (App f' a')
case res2 of
Nothing -> pure (App f' a')
Just app' -> loop app'
Let (Binding _ f _ _ _ r) b -> loop b''
where
r' = shift 1 (V f 0) r
b' = subst (V f 0) r' b
b'' = shift (-1) (V f 0) b'
Annot x _ -> loop x
Bool -> pure Bool
BoolLit b -> pure (BoolLit b)
BoolAnd x y -> decide <$> loop x <*> loop y
where
decide (BoolLit True ) r = r
decide (BoolLit False) _ = BoolLit False
decide l (BoolLit True ) = l
decide _ (BoolLit False) = BoolLit False
decide l r
| judgmentallyEqual l r = l
| otherwise = BoolAnd l r
BoolOr x y -> decide <$> loop x <*> loop y
where
decide (BoolLit False) r = r
decide (BoolLit True ) _ = BoolLit True
decide l (BoolLit False) = l
decide _ (BoolLit True ) = BoolLit True
decide l r
| judgmentallyEqual l r = l
| otherwise = BoolOr l r
BoolEQ x y -> decide <$> loop x <*> loop y
where
decide (BoolLit True ) r = r
decide l (BoolLit True ) = l
decide l r
| judgmentallyEqual l r = BoolLit True
| otherwise = BoolEQ l r
BoolNE x y -> decide <$> loop x <*> loop y
where
decide (BoolLit False) r = r
decide l (BoolLit False) = l
decide l r
| judgmentallyEqual l r = BoolLit False
| otherwise = BoolNE l r
BoolIf bool true false -> decide <$> loop bool <*> loop true <*> loop false
where
decide (BoolLit True ) l _ = l
decide (BoolLit False) _ r = r
decide b (BoolLit True) (BoolLit False) = b
decide b l r
| judgmentallyEqual l r = l
| otherwise = BoolIf b l r
Natural -> pure Natural
NaturalLit n -> pure (NaturalLit n)
NaturalFold -> pure NaturalFold
NaturalBuild -> pure NaturalBuild
NaturalIsZero -> pure NaturalIsZero
NaturalEven -> pure NaturalEven
NaturalOdd -> pure NaturalOdd
NaturalToInteger -> pure NaturalToInteger
NaturalShow -> pure NaturalShow
NaturalSubtract -> pure NaturalSubtract
NaturalPlus x y -> decide <$> loop x <*> loop y
where
decide (NaturalLit 0) r = r
decide l (NaturalLit 0) = l
decide (NaturalLit m) (NaturalLit n) = NaturalLit (m + n)
decide l r = NaturalPlus l r
NaturalTimes x y -> decide <$> loop x <*> loop y
where
decide (NaturalLit 1) r = r
decide l (NaturalLit 1) = l
decide (NaturalLit 0) _ = NaturalLit 0
decide _ (NaturalLit 0) = NaturalLit 0
decide (NaturalLit m) (NaturalLit n) = NaturalLit (m * n)
decide l r = NaturalTimes l r
Integer -> pure Integer
IntegerLit n -> pure (IntegerLit n)
IntegerShow -> pure IntegerShow
IntegerToDouble -> pure IntegerToDouble
Double -> pure Double
DoubleLit n -> pure (DoubleLit n)
DoubleShow -> pure DoubleShow
Text -> pure Text
TextLit (Chunks xys z) -> do
chunks' <- mconcat <$> chunks
case chunks' of
Chunks [("", x)] "" -> pure x
c -> pure (TextLit c)
where
chunks =
((++ [Chunks [] z]) . concat) <$> traverse process xys
process (x, y) = do
y' <- loop y
case y' of
TextLit c -> pure [Chunks [] x, c]
_ -> pure [Chunks [(x, y')] mempty]
TextAppend x y -> loop (TextLit (Chunks [("", x), ("", y)] ""))
TextShow -> pure TextShow
List -> pure List
ListLit t es
| Data.Sequence.null es -> ListLit <$> t' <*> es'
| otherwise -> ListLit Nothing <$> es'
where
t' = traverse loop t
es' = traverse loop es
ListAppend x y -> decide <$> loop x <*> loop y
where
decide (ListLit _ m) r | Data.Sequence.null m = r
decide l (ListLit _ n) | Data.Sequence.null n = l
decide (ListLit t m) (ListLit _ n) = ListLit t (m <> n)
decide l r = ListAppend l r
ListBuild -> pure ListBuild
ListFold -> pure ListFold
ListLength -> pure ListLength
ListHead -> pure ListHead
ListLast -> pure ListLast
ListIndexed -> pure ListIndexed
ListReverse -> pure ListReverse
Optional -> pure Optional
Some a -> Some <$> a'
where
a' = loop a
None -> pure None
OptionalFold -> pure OptionalFold
OptionalBuild -> pure OptionalBuild
Record kts -> Record . Dhall.Map.sort <$> kts'
where
kts' = traverse loop kts
RecordLit kvs -> RecordLit . Dhall.Map.sort <$> kvs'
where
kvs' = traverse loop kvs
Union kts -> Union . Dhall.Map.sort <$> kts'
where
kts' = traverse (traverse loop) kts
Combine x y -> decide <$> loop x <*> loop y
where
decide (RecordLit m) r | Data.Foldable.null m =
r
decide l (RecordLit n) | Data.Foldable.null n =
l
decide (RecordLit m) (RecordLit n) =
RecordLit (Dhall.Map.unionWith decide m n)
decide l r =
Combine l r
CombineTypes x y -> decide <$> loop x <*> loop y
where
decide (Record m) r | Data.Foldable.null m =
r
decide l (Record n) | Data.Foldable.null n =
l
decide (Record m) (Record n) =
Record (Dhall.Map.unionWith decide m n)
decide l r =
CombineTypes l r
Prefer x y -> decide <$> loop x <*> loop y
where
decide (RecordLit m) r | Data.Foldable.null m =
r
decide l (RecordLit n) | Data.Foldable.null n =
l
decide (RecordLit m) (RecordLit n) =
RecordLit (Dhall.Map.union n m)
decide l r | judgmentallyEqual l r =
l
decide l r =
Prefer l r
Merge x y t -> do
x' <- loop x
y' <- loop y
case x' of
RecordLit kvsX ->
case y' of
Field (Union ktsY) kY ->
case Dhall.Map.lookup kY ktsY of
Just Nothing ->
case Dhall.Map.lookup kY kvsX of
Just vX -> return vX
Nothing -> Merge x' y' <$> t'
_ ->
Merge x' y' <$> t'
App (Field (Union ktsY) kY) vY ->
case Dhall.Map.lookup kY ktsY of
Just (Just _) ->
case Dhall.Map.lookup kY kvsX of
Just vX -> loop (App vX vY)
Nothing -> Merge x' y' <$> t'
_ ->
Merge x' y' <$> t'
_ -> Merge x' y' <$> t'
_ -> Merge x' y' <$> t'
where
t' = traverse loop t
ToMap x t -> do
x' <- loop x
t' <- traverse loop t
case x' of
RecordLit kvsX -> do
let entry (key, value) =
RecordLit
(Dhall.Map.fromList
[ ("mapKey" , TextLit (Chunks [] key))
, ("mapValue", value )
]
)
let keyValues = Data.Sequence.fromList (map entry (Dhall.Map.toList kvsX))
let listType = case t' of
Just _ | null keyValues ->
t'
_ ->
Nothing
return (ListLit listType keyValues)
_ -> do
return (ToMap x' t')
Field r x -> do
let singletonRecordLit v = RecordLit (Dhall.Map.singleton x v)
r' <- loop r
case r' of
RecordLit kvs ->
case Dhall.Map.lookup x kvs of
Just v -> pure v
Nothing -> Field <$> (RecordLit <$> traverse loop kvs) <*> pure x
Project r_ _ -> loop (Field r_ x)
Prefer (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Prefer (singletonRecordLit v) r_) x)
Nothing -> loop (Field r_ x)
Prefer l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
Just v -> pure v
Nothing -> loop (Field l x)
Combine (RecordLit kvs) r_ -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Combine (singletonRecordLit v) r_) x)
Nothing -> loop (Field r_ x)
Combine l (RecordLit kvs) -> case Dhall.Map.lookup x kvs of
Just v -> pure (Field (Combine l (singletonRecordLit v)) x)
Nothing -> loop (Field l x)
_ -> pure (Field r' x)
Project r (Left xs)-> do
r' <- loop r
case r' of
RecordLit kvs ->
pure (RecordLit (Dhall.Map.restrictKeys kvs (Dhall.Set.toSet xs)))
_ | null xs -> pure (RecordLit mempty)
| otherwise -> pure (Project r' (Left (Dhall.Set.sort xs)))
Project r (Right e1) -> do
e2 <- loop e1
case e2 of
Record kts -> do
loop (Project r (Left (Dhall.Set.fromSet (Dhall.Map.keysSet kts))))
_ -> do
r' <- loop r
pure (Project r' (Right e2))
Assert t -> do
t' <- loop t
pure (Assert t')
Equivalent l r -> do
l' <- loop l
r' <- loop r
pure (Equivalent l' r')
Note _ e' -> loop e'
ImportAlt l _r -> loop l
Embed a -> pure (Embed a)
textShow :: Text -> Text
textShow text = "\"" <> Data.Text.concatMap f text <> "\""
where
f '"' = "\\\""
f '$' = "\\u0024"
f '\\' = "\\\\"
f '\b' = "\\b"
f '\n' = "\\n"
f '\r' = "\\r"
f '\t' = "\\t"
f '\f' = "\\f"
f c | c <= '\x1F' = Data.Text.pack (Text.Printf.printf "\\u%04x" (Data.Char.ord c))
| otherwise = Data.Text.singleton c
judgmentallyEqual :: Eq a => Expr s a -> Expr t a -> Bool
judgmentallyEqual = Dhall.Eval.convEmpty
type NormalizerM m a = forall s. Expr s a -> m (Maybe (Expr s a))
type Normalizer a = NormalizerM Identity a
newtype ReifiedNormalizer a = ReifiedNormalizer
{ getReifiedNormalizer :: Normalizer a }
isNormalizedWith :: (Eq s, Eq a) => Normalizer a -> Expr s a -> Bool
isNormalizedWith ctx e = e == normalizeWith (Just (ReifiedNormalizer ctx)) e
isNormalized :: Eq a => Expr s a -> Bool
isNormalized e0 = loop (denote e0)
where
loop e = case e of
Const _ -> True
Var _ -> True
Lam _ a b -> loop a && loop b
Pi _ a b -> loop a && loop b
App f a -> loop f && loop a && case App f a of
App (Lam _ _ _) _ -> False
App (App ListBuild _) (App (App ListFold _) _) -> False
App NaturalBuild (App NaturalFold _) -> False
App (App OptionalBuild _) (App (App OptionalFold _) _) -> False
App (App (App (App NaturalFold (NaturalLit _)) _) _) _ -> False
App NaturalFold (NaturalLit _) -> False
App NaturalBuild _ -> False
App NaturalIsZero (NaturalLit _) -> False
App NaturalEven (NaturalLit _) -> False
App NaturalOdd (NaturalLit _) -> False
App NaturalShow (NaturalLit _) -> False
App (App NaturalSubtract (NaturalLit _)) (NaturalLit _) -> False
App (App NaturalSubtract (NaturalLit 0)) _ -> False
App (App NaturalSubtract _) (NaturalLit 0) -> False
App (App NaturalSubtract x) y -> not (judgmentallyEqual x y)
App NaturalToInteger (NaturalLit _) -> False
App IntegerShow (IntegerLit _) -> False
App IntegerToDouble (IntegerLit _) -> False
App DoubleShow (DoubleLit _) -> False
App (App OptionalBuild _) _ -> False
App (App ListBuild _) _ -> False
App (App ListFold _) (ListLit _ _) -> False
App (App ListLength _) (ListLit _ _) -> False
App (App ListHead _) (ListLit _ _) -> False
App (App ListLast _) (ListLit _ _) -> False
App (App ListIndexed _) (ListLit _ _) -> False
App (App ListReverse _) (ListLit _ _) -> False
App (App OptionalFold _) (Some _) -> False
App (App OptionalFold _) (App None _) -> False
App TextShow (TextLit (Chunks [] _)) ->
False
_ -> True
Let _ _ -> False
Annot _ _ -> False
Bool -> True
BoolLit _ -> True
BoolAnd x y -> loop x && loop y && decide x y
where
decide (BoolLit _) _ = False
decide _ (BoolLit _) = False
decide l r = not (judgmentallyEqual l r)
BoolOr x y -> loop x && loop y && decide x y
where
decide (BoolLit _) _ = False
decide _ (BoolLit _) = False
decide l r = not (judgmentallyEqual l r)
BoolEQ x y -> loop x && loop y && decide x y
where
decide (BoolLit True) _ = False
decide _ (BoolLit True) = False
decide l r = not (judgmentallyEqual l r)
BoolNE x y -> loop x && loop y && decide x y
where
decide (BoolLit False) _ = False
decide _ (BoolLit False ) = False
decide l r = not (judgmentallyEqual l r)
BoolIf x y z ->
loop x && loop y && loop z && decide x y z
where
decide (BoolLit _) _ _ = False
decide _ (BoolLit True) (BoolLit False) = False
decide _ l r = not (judgmentallyEqual l r)
Natural -> True
NaturalLit _ -> True
NaturalFold -> True
NaturalBuild -> True
NaturalIsZero -> True
NaturalEven -> True
NaturalOdd -> True
NaturalShow -> True
NaturalSubtract -> True
NaturalToInteger -> True
NaturalPlus x y -> loop x && loop y && decide x y
where
decide (NaturalLit 0) _ = False
decide _ (NaturalLit 0) = False
decide (NaturalLit _) (NaturalLit _) = False
decide _ _ = True
NaturalTimes x y -> loop x && loop y && decide x y
where
decide (NaturalLit 0) _ = False
decide _ (NaturalLit 0) = False
decide (NaturalLit 1) _ = False
decide _ (NaturalLit 1) = False
decide (NaturalLit _) (NaturalLit _) = False
decide _ _ = True
Integer -> True
IntegerLit _ -> True
IntegerShow -> True
IntegerToDouble -> True
Double -> True
DoubleLit _ -> True
DoubleShow -> True
Text -> True
TextLit (Chunks [("", _)] "") -> False
TextLit (Chunks xys _) -> all (all check) xys
where
check y = loop y && case y of
TextLit _ -> False
_ -> True
TextAppend _ _ -> False
TextShow -> True
List -> True
ListLit t es -> all loop t && all loop es
ListAppend x y -> loop x && loop y && decide x y
where
decide (ListLit _ m) _ | Data.Sequence.null m = False
decide _ (ListLit _ n) | Data.Sequence.null n = False
decide (ListLit _ _) (ListLit _ _) = False
decide _ _ = True
ListBuild -> True
ListFold -> True
ListLength -> True
ListHead -> True
ListLast -> True
ListIndexed -> True
ListReverse -> True
Optional -> True
Some a -> loop a
None -> True
OptionalFold -> True
OptionalBuild -> True
Record kts -> Dhall.Map.isSorted kts && all loop kts
RecordLit kvs -> Dhall.Map.isSorted kvs && all loop kvs
Union kts -> Dhall.Map.isSorted kts && all (all loop) kts
Combine x y -> loop x && loop y && decide x y
where
decide (RecordLit m) _ | Data.Foldable.null m = False
decide _ (RecordLit n) | Data.Foldable.null n = False
decide (RecordLit _) (RecordLit _) = False
decide _ _ = True
CombineTypes x y -> loop x && loop y && decide x y
where
decide (Record m) _ | Data.Foldable.null m = False
decide _ (Record n) | Data.Foldable.null n = False
decide (Record _) (Record _) = False
decide _ _ = True
Prefer x y -> loop x && loop y && decide x y
where
decide (RecordLit m) _ | Data.Foldable.null m = False
decide _ (RecordLit n) | Data.Foldable.null n = False
decide (RecordLit _) (RecordLit _) = False
decide l r = not (judgmentallyEqual l r)
Merge x y t -> loop x && loop y && all loop t
ToMap x t -> case x of
RecordLit _ -> False
_ -> loop x && all loop t
Field r k -> case r of
RecordLit _ -> False
Project _ _ -> False
Prefer (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
Prefer _ (RecordLit _) -> False
Combine (RecordLit m) _ -> Dhall.Map.keys m == [k] && loop r
Combine _ (RecordLit m) -> Dhall.Map.keys m == [k] && loop r
_ -> loop r
Project r p -> loop r &&
case p of
Left s -> case r of
RecordLit _ -> False
_ -> not (Dhall.Set.null s) && Dhall.Set.isSorted s
Right e' -> case e' of
Record _ -> False
_ -> loop e'
Assert t -> loop t
Equivalent l r -> loop l && loop r
Note _ e' -> loop e'
ImportAlt _ _ -> False
Embed _ -> True
freeIn :: Eq a => Var -> Expr s a -> Bool
variable@(V var i) `freeIn` expression =
Dhall.Core.subst variable (Var (V var (i + 1))) strippedExpression
/= strippedExpression
where
denote' :: Expr t b -> Expr () b
denote' = denote
strippedExpression = denote' expression
_ERROR :: String
_ERROR = "\ESC[1;31mError\ESC[0m"
internalError :: Data.Text.Text -> forall b . b
internalError text = error (unlines
[ _ERROR <> ": Compiler bug "
, " "
, "Explanation: This error message means that there is a bug in the Dhall compiler."
, "You didn't do anything wrong, but if you would like to see this problem fixed "
, "then you should report the bug at: "
, " "
, "https://github.com/dhall-lang/dhall-haskell/issues "
, " "
, "Please include the following text in your bug report: "
, " "
, "``` "
, Data.Text.unpack text <> " "
, "``` "
] )
reservedIdentifiers :: HashSet Text
reservedIdentifiers =
Data.HashSet.fromList
[ "let"
, "in"
, "Type"
, "Kind"
, "Sort"
, "forall"
, "Bool"
, "True"
, "False"
, "merge"
, "toMap"
, "if"
, "then"
, "else"
, "as"
, "using"
, "Natural"
, "Natural/fold"
, "Natural/build"
, "Natural/isZero"
, "Natural/even"
, "Natural/odd"
, "Natural/toInteger"
, "Natural/show"
, "Natural/subtract"
, "Integer"
, "Integer/show"
, "Integer/toDouble"
, "Double"
, "Double/show"
, "Text"
, "Text/show"
, "List"
, "List/build"
, "List/fold"
, "List/length"
, "List/head"
, "List/last"
, "List/indexed"
, "List/reverse"
, "Optional"
, "Some"
, "None"
, "Optional/build"
, "Optional/fold"
, "NaN"
, "Infinity"
]
subExpressions :: Applicative f => (Expr s a -> f (Expr s a)) -> Expr s a -> f (Expr s a)
subExpressions _ (Const c) = pure (Const c)
subExpressions _ (Var v) = pure (Var v)
subExpressions f (Lam a b c) = Lam a <$> f b <*> f c
subExpressions f (Pi a b c) = Pi a <$> f b <*> f c
subExpressions f (App a b) = App <$> f a <*> f b
subExpressions f (Let a b) = Let <$> bindingExprs f a <*> f b
subExpressions f (Annot a b) = Annot <$> f a <*> f b
subExpressions _ Bool = pure Bool
subExpressions _ (BoolLit b) = pure (BoolLit b)
subExpressions f (BoolAnd a b) = BoolAnd <$> f a <*> f b
subExpressions f (BoolOr a b) = BoolOr <$> f a <*> f b
subExpressions f (BoolEQ a b) = BoolEQ <$> f a <*> f b
subExpressions f (BoolNE a b) = BoolNE <$> f a <*> f b
subExpressions f (BoolIf a b c) = BoolIf <$> f a <*> f b <*> f c
subExpressions _ Natural = pure Natural
subExpressions _ (NaturalLit n) = pure (NaturalLit n)
subExpressions _ NaturalFold = pure NaturalFold
subExpressions _ NaturalBuild = pure NaturalBuild
subExpressions _ NaturalIsZero = pure NaturalIsZero
subExpressions _ NaturalEven = pure NaturalEven
subExpressions _ NaturalOdd = pure NaturalOdd
subExpressions _ NaturalToInteger = pure NaturalToInteger
subExpressions _ NaturalShow = pure NaturalShow
subExpressions _ NaturalSubtract = pure NaturalSubtract
subExpressions f (NaturalPlus a b) = NaturalPlus <$> f a <*> f b
subExpressions f (NaturalTimes a b) = NaturalTimes <$> f a <*> f b
subExpressions _ Integer = pure Integer
subExpressions _ (IntegerLit n) = pure (IntegerLit n)
subExpressions _ IntegerShow = pure IntegerShow
subExpressions _ IntegerToDouble = pure IntegerToDouble
subExpressions _ Double = pure Double
subExpressions _ (DoubleLit n) = pure (DoubleLit n)
subExpressions _ DoubleShow = pure DoubleShow
subExpressions _ Text = pure Text
subExpressions f (TextLit chunks) =
TextLit <$> chunkExprs f chunks
subExpressions f (TextAppend a b) = TextAppend <$> f a <*> f b
subExpressions _ TextShow = pure TextShow
subExpressions _ List = pure List
subExpressions f (ListLit a b) = ListLit <$> traverse f a <*> traverse f b
subExpressions f (ListAppend a b) = ListAppend <$> f a <*> f b
subExpressions _ ListBuild = pure ListBuild
subExpressions _ ListFold = pure ListFold
subExpressions _ ListLength = pure ListLength
subExpressions _ ListHead = pure ListHead
subExpressions _ ListLast = pure ListLast
subExpressions _ ListIndexed = pure ListIndexed
subExpressions _ ListReverse = pure ListReverse
subExpressions _ Optional = pure Optional
subExpressions f (Some a) = Some <$> f a
subExpressions _ None = pure None
subExpressions _ OptionalFold = pure OptionalFold
subExpressions _ OptionalBuild = pure OptionalBuild
subExpressions f (Record a) = Record <$> traverse f a
subExpressions f ( RecordLit a ) = RecordLit <$> traverse f a
subExpressions f (Union a) = Union <$> traverse (traverse f) a
subExpressions f (Combine a b) = Combine <$> f a <*> f b
subExpressions f (CombineTypes a b) = CombineTypes <$> f a <*> f b
subExpressions f (Prefer a b) = Prefer <$> f a <*> f b
subExpressions f (Merge a b t) = Merge <$> f a <*> f b <*> traverse f t
subExpressions f (ToMap a t) = ToMap <$> f a <*> traverse f t
subExpressions f (Field a b) = Field <$> f a <*> pure b
subExpressions f (Project a b) = Project <$> f a <*> traverse f b
subExpressions f (Assert a) = Assert <$> f a
subExpressions f (Equivalent a b) = Equivalent <$> f a <*> f b
subExpressions f (Note a b) = Note a <$> f b
subExpressions f (ImportAlt l r) = ImportAlt <$> f l <*> f r
subExpressions _ (Embed a) = pure (Embed a)
chunkExprs
:: Applicative f
=> (Expr s a -> f (Expr t b))
-> Chunks s a -> f (Chunks t b)
chunkExprs f (Chunks chunks final) =
flip Chunks final <$> traverse (traverse f) chunks
pathCharacter :: Char -> Bool
pathCharacter c =
'\x21' == c
|| ('\x24' <= c && c <= '\x27')
|| ('\x2A' <= c && c <= '\x2B')
|| ('\x2D' <= c && c <= '\x2E')
|| ('\x30' <= c && c <= '\x3B')
|| c == '\x3D'
|| ('\x40' <= c && c <= '\x5A')
|| ('\x5E' <= c && c <= '\x7A')
|| c == '\x7C'
|| c == '\x7E'
prettyPathComponent :: Text -> Doc ann
prettyPathComponent text
| Data.Text.all pathCharacter text =
"/" <> Pretty.pretty text
| otherwise =
"/\"" <> Pretty.pretty text <> "\""
prettyURIComponent :: Text -> Doc ann
prettyURIComponent text =
Pretty.pretty $ URI.normalizeCase $ URI.normalizeEscape $ "/" <> Data.Text.unpack text
throws :: (Exception e, MonadIO io) => Either e a -> io a
throws (Left e) = liftIO (Control.Exception.throwIO e)
throws (Right r) = return r
multiLet :: Binding s a -> Expr s a -> MultiLet s a
multiLet b0 = \case
Let b1 e1 ->
let MultiLet bs e = multiLet b1 e1
in MultiLet (Data.List.NonEmpty.cons b0 bs) e
e -> MultiLet (b0 :| []) e
wrapInLets :: Foldable f => f (Binding s a) -> Expr s a -> Expr s a
wrapInLets bs e = foldr Let e bs
data MultiLet s a = MultiLet (NonEmpty (Binding s a)) (Expr s a)
data Binding s a = Binding
{ bindingSrc0 :: Maybe s
, variable :: Text
, bindingSrc1 :: Maybe s
, annotation :: Maybe (Maybe s, Expr s a)
, bindingSrc2 :: Maybe s
, value :: Expr s a
} deriving (Data, Eq, Foldable, Functor, Generic, NFData, Ord, Show, Traversable)
instance Bifunctor Binding where
first k (Binding src0 a src1 b src2 c) =
Binding (fmap k src0) a (fmap k src1) (fmap adapt0 b) (fmap k src2) (first k c)
where
adapt0 (src3, d) = (fmap k src3, first k d)
second = fmap
bindingExprs
:: (Applicative f)
=> (Expr s a -> f (Expr s b))
-> Binding s a -> f (Binding s b)
bindingExprs f (Binding s0 n s1 t s2 v) =
Binding
<$> pure s0
<*> pure n
<*> pure s1
<*> traverse (traverse f) t
<*> pure s2
<*> f v
makeBinding :: Text -> Expr s a -> Binding s a
makeBinding name = Binding Nothing name Nothing Nothing Nothing