o>Z      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~     None !"234OTeSyntax tree for expressions -Const c ~ c ]Var (V x 0) ~ x Var (V x n) ~ x@n 9Lam x A b ~ (x : A) -> b sPi "_" A B ~ A -> B Pi x A B ~ "(x : A) -> B /App f a ~ f a }Let x Nothing r e ~ let x = r in e Let x (Just t) r e ~ let x : t = r in e 1Annot x t ~ x : t 0Bool ~ Bool -BoolLit b ~ b 2BoolAnd x y ~ x && y 2BoolOr x y ~ x || y 2BoolEQ x y ~ x == y 2BoolNE x y ~ x != y >BoolIf x y z ~ if x then y else z 3Natural ~ Natural .NaturalLit n ~ +n 8NaturalFold ~ Natural/fold 9NaturalBuild ~ Natural/build :NaturalIsZero ~ Natural/isZero 8NaturalEven ~ Natural/even 7NaturalOdd ~ Natural/odd 1NaturalPlus x y ~ x + y 1NaturalTimes x y ~ x * y 3Integer ~ Integer -IntegerLit n ~ n 2Double ~ Double -DoubleLit n ~ n 0Text ~ Text! -TextLit t ~ t" 2TextAppend x y ~ x ++ y# 0List ~ List$ tListLit (Just t ) [x, y, z] ~ [x, y, z] : List t ListLit Nothing [x, y, z] ~ [x, y, z]% 6ListBuild ~ List/build& 5ListFold ~ List/fold' 7ListLength ~ List/length( 5ListHead ~ List/head) 5ListLast ~ List/last* 8ListIndexed ~ List/indexed+ 8ListReverse ~ List/reverse, 4Optional ~ Optional- yOptionalLit t [e] ~ [e] : Optional t OptionalLit t [] ~ [] : Optional t. 9OptionalFold ~ Optional/fold/ @Record [(k1, t1), (k2, t2)] ~ { k1 : t1, k2 : t1 }0 @RecordLit [(k1, v1), (k2, v2)] ~ { k1 = v1, k2 = v2 }1 AUnion [(k1, t1), (k2, t2)] ~ < k1 : t1 | k2 : t2 >2 LUnionLit (k1, v1) [(k2, t2), (k3, t3)] ~ < k1 = t1 | k2 : t2 | k3 : t3 > 3 1Combine x y ~ x "' y4 9Merge x y t ~ merge x y : t5 /Field e x ~ e.x6 -Note s x ~ e7 0Embed path ~ path8Label for a bound variableThe % field is the variable's name (i.e. "x").The ! field disambiguates variables with the same name if there are multiple bound variables of the same name in scope. Zero refers to the nearest bound variable and the index increases by one for each bound variable of the same name going outward. The following diagram may help: p % %%refers to%%% % % v % (x : Type) ! (y : Type) ! (x : Type) ! x@0 % %%%%%%%%%%%%%%%%%refers to%%%%%%%%%%%%%%%%%% % % v % (x : Type) ! (y : Type) ! (x : Type) ! x@1This _ behaves like a De Bruijn index in the special case where all variables have the same name.+You can optionally omit the index if it is 0:  % %refers to%% % % v % (x : Type) ! (y : Type) ! (x : Type) ! x.Zero indices are omitted when pretty-printing 86s and non-zero indices appear as a numeric suffix.:Path to an external resource>EHow to interpret the path's contents (i.e. as Dhall code or raw text)ABThe type of path to import (i.e. local vs. remote vs. environment)B Local pathCRemote resourceDEnvironment variableE>Whether or not a path is relative to the user's home directoryH Constants for a pure type systemThe only axiom is:  " Type : Kind!... and the valid rule pairs are: " Type ! Type : Type -- Functions from terms to terms (ordinary functions) " Kind ! Type : Type -- Functions from types to terms (polymorphic functions) " Kind ! Kind : Kind -- Functions from types to types (type constructors)*These are the same rule pairs as System FzNote that Dhall does not support functions from terms to types and therefore Dhall is not a dependently typed languageKPretty-print a valueBuilder corresponding to the label token in  Dhall.ParserBuilder corresponding to the number token in  Dhall.ParserBuilder corresponding to the natural token in  Dhall.ParserBuilder corresponding to the double token in  Dhall.ParserBuilder corresponding to the text token in  Dhall.ParserBuilder corresponding to the expr parser in  Dhall.ParserBuilder corresponding to the exprA parser in  Dhall.ParserBuilder corresponding to the exprB parser in  Dhall.ParserBuilder corresponding to the exprC parser in  Dhall.ParserBuilder corresponding to the exprC0 parser in  Dhall.ParserBuilder corresponding to the exprC1 parser in  Dhall.Parser Builder corresponding to the exprC2 parser in  Dhall.Parser!Builder corresponding to the exprC3 parser in  Dhall.Parser"Builder corresponding to the exprC4 parser in  Dhall.Parser#Builder corresponding to the exprC5 parser in  Dhall.Parser$Builder corresponding to the exprC6 parser in  Dhall.Parser%Builder corresponding to the exprC7 parser in  Dhall.Parser&Builder corresponding to the exprD parser in  Dhall.Parser'Builder corresponding to the exprE parser in  Dhall.Parser(Builder corresponding to the exprF parser in  Dhall.Parser)Builder corresponding to the const parser in  Dhall.Parser*Builder corresponding to the var parser in  Dhall.Parser+Builder corresponding to the elems parser in  Dhall.Parser,Builder corresponding to the  recordLit parser in  Dhall.Parser-Builder corresponding to the  fieldValues parser in  Dhall.Parser.Builder corresponding to the  fieldValue parser in  Dhall.Parser/Builder corresponding to the record parser in  Dhall.Parser0Builder corresponding to the  fieldTypes parser in  Dhall.Parser1Builder corresponding to the  fieldType parser in  Dhall.Parser2Builder corresponding to the union parser in  Dhall.Parser3Builder corresponding to the alternativeTypes parser in  Dhall.Parser4Builder corresponding to the alternativeType parser in  Dhall.Parser5Builder corresponding to the unionLit parser in  Dhall.ParserLLk is used by both normalization and type-checking to avoid variable capture by shifting variable indicesIFor example, suppose that you were to normalize the following expression: 4(a : Type) ! (x : a) ! ((y : a) ! (x : a) ! y) xIf you were to substitute y with x^ without shifting any variable indices, then you would get the following incorrect result: C(a : Type) ! (x : a) ! (x : a) ! x -- Incorrect normalized formIn order to substitute x in place of y we need to L x by 13 in order to avoid being misinterpreted as the x8 bound by the innermost lambda. If we perform that L then we get the correct result: '(a : Type) ! (x : a) ! (x : a) ! x@1ZAs a more worked example, suppose that you were to normalize the following expression: [ (a : Type) ! (f : a ! a ! a) ! (x : a) ! (x : a) ! ((x : a) ! f x x@1) x@1'The correct normalized result would be: J (a : Type) ! (f : a ! a ! a) ! (x : a) ! (x : a) ! f x@1 xuThe above example illustrates how we need to both increase and decrease variable indices as part of substitution:+We need to increase the index of the outer x@1 to x@2 before we substitute it into the body of the innermost lambda expression in order to avoid variable capture. This substitution changes the body of the lambda expression to  (f x@2 x@1)UWe then remove the innermost lambda and therefore decrease the indices of both xs in  (f x@2 x@1) to  (f x@1 x)) in order to reflect that one less x( variable is now bound within that scope Formally, (shift d (V x n) e) modifies the expression e by adding d+ to the indices of all variables named x$ whose indices are greater than (n + m), where mH is the number of bound variables of the same name within that scope In practice, d is always 1 or -1 because we either:increment variables by 1. to avoid variable capture during substitutiondecrement variables by 1) when deleting lambdas after substitutionn starts off at 0 when substitution begins and increments every time we descend into a lambda or let expression that binds a variable of the same name in order to avoid shifting the bound variables by mistake.M;Substitute all occurrences of a variable with an expression subst x C B ~ B[x := C]NBReduce an expression to its normal form, performing beta reductionN does not type-check the expression. You may want to type-check expressions before normalizing them since normalization can convert an ill-typed expression into a well-typed expression. However, Ng will not fail if the expression is ill-typed and will leave ill-typed sub-expressions unevaluated.O0Quickly check if an expression is in normal formPUtility function used to throw internal errors that should never happen (in theory) but that are not enforced by the type systemQ-Generates a syntactically valid Dhall programz  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJK !"#$%&'()*+,-./012345LMNO6P7QRSTUVWXYZM  1# / !"$%&'()*+,-.023456789:;<=>?@ADBCEFGHJIKLMNOPMHIJEFGABCD>?@:;<=89  !"#$%&'()*+,-./01234567NMLOKP:3  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJK !"#$%&'()*+,-./012345LMNO6P7QRSTUVWXYZNone!"0IpA parsing errorrA r! that is almost identical to  Text.Trifecta.89 except treating Haskell-style comments as whitespaceuSource code extractw'Parser for a top-level Dhall expressionxParser for a top-level Dhall expression. The expression is parameterized over any parseable type, allowing the language to be extended as needed.yParse an expression from  containing a Dhall program4pqrstuv9:;<=>?@ABCDEFwxGHIJKLMNOPQRSTUVWXYZ[\]^yz{|} pqrstuvwxy ywxuvpqrst0pqrstuv9:;<=>?@ABCDEFwxGHIJKLMNOPQRSTUVWXYZ[\]^yz{|}None2IA  (Context a) associates  labels with values of type a . Each 1 label can correspond to multiple values of type aThe  is used for type-checking when  (a = Expr X) You create a  using  and You transform a  using _You consume a  using  and The difference between a  and a  is that a ^ lets you have multiple ordered occurrences of the same key and you can query for the nth occurrence of a given key.(An empty context with no key-value pairsAdd a key-value pair to the Look up a key by name and index lookup _ _ empty = Nothing lookup k 0 (insert k v c) = Just v lookup k n (insert k v c) = lookup k (n - 1) c lookup k n (insert j v c) = lookup k n c -- k /= j+Return all key-value associations as a list JtoList empty = [] toList (insert k v ctx) = (k, v) : toList ctx`a`aNone!"0OToNewtype used to wrap error messages so that they render with a more detailed explanation of what went wrong-A structured type error that includes contextb6Default succinct 1-line explanation of what went wrongc1Longer and more detailed explanation of the errorThe specific type errorLike   %, except with a shorter inferred typezType-check an expression and return the expression's type if type-checking succeeds or an error if type-checking fails does not necessarily normalize the type since full normalization is not necessary for just type-checking. If you actually care about the returned type then you may want to N it afterwards. is the same as  with an empty context, meaning that the expression must be closed (i.e. no free variables), otherwise type-checking will fail.Mdebcfghijklmno77debc*fghijklmnoNone!"0p8Exception thrown when an environment variable is missing1Exception thrown when an imported file is missingNewtype used to wrap qs with a prettier r instance6Extend another exception with the current import stack)Imports resolved so far, in reverse orderThe nested exceptionDhall tries to ensure that all expressions hosted on network endpoints are weakly referentially transparent, meaning roughly that any two clients will compile the exact same result given the same URL.To be precise, a strong interpretaton of referential transparency means that if you compiled a URL you could replace the expression hosted at that URL with the compiled result. Let's call this "static linking". Dhall (very intentionally) does not satisfy this stronger interpretation of referential transparency since "statically linking" an expression (i.e. permanently resolving all imports) means that the expression will no longer update if its dependencies change.`In general, either interpretation of referential transparency is not enforceable in a networked context since one can easily violate referential transparency with a custom DNS, but Dhall can still try to guard against common unintentional violations. To do this, Dhall enforces that a non-local import may not reference a local import.Local imports are defined as:A fileA URL with a host of  localhost or  127.0.0.1-All other imports are defined to be non-localThe offending opaque import7An import failed because of a cycle in the import graphThe offending cyclic importsaThis function computes the current path by taking the last absolute path (either an absolute t or C8) and combining it with all following relative pathsFor example, if the file  `./foo/bar` imports `./baz`, that will resolve to  `./foo/baz`a. Relative imports are relative to a file's parent directory. This also works for URLs, too.This code is full of all sorts of edge cases so it wouldn't surprise me at all if you find something broken in here. Most of the ugliness is due to:Handling paths ending with /@ by stripping the /@J suffix if and only if you navigate to any downstream relative pathsRemoving spurious .s and ..s from the pathAlso, there are way too many uxs in the URL-handling code For now I don't mind, but if were to really do this correctly we'd store the URLs as G for O(1) access to the end of the string. The only reason we use v$ at all is for consistency with the  http-client library.w Remove all .'s and ..'s in the pathParse an expression from a : containing a Dhall programxLoad a :: as a "dynamic" expression (without resolving any imports)YThis also returns the true final path (i.e. explicit "/@" at the end for directories)yLoad a :5 as a "static" expression (with all imports resolved)(Resolve all imports within an expression2z{|}~pswxy#z{|}~pswxyNone !"269:;QRT-This is the underlying class that powers the H class's support for automatically deriving a generic implementationMUse these options to tweak how Dhall derives a generic implementation of \Function used to transform Haskell field names into their corresponding Dhall field nameshFunction used to transform Haskell constructor names into their corresponding Dhall alternative namesAny value that implements G can be automatically decoded based on the inferred return type of -input auto "[1, 2, 3]" :: IO (Vector Integer)[1,2,3]RThis class auto-generates a default implementation for records that implement C. This does not auto-generate an instance for recursive types.A (Type a)- represents a way to marshal a value of type 'a' from Dhall into HaskellYou can produce s either explicitly: 3example :: Type (Vector Text) example = vector text... or implicitly using : ,example :: Type (Vector Text) example = autoYou can consume  s using the  function: input :: Type a -> Text -> IO aEvery I must obey the contract that if an expression's type matches the the  type then the B function must succeed. If not, then this exception is thrown)This exception indicates that an invalid  was provided to the  functionIType-check and evaluate a Dhall program, decoding the result into Haskell@The first argument determines the type of value that you decode:input integer "2"2"input (vector double) "[1.0, 2.0]" [1.0,2.0]Use T to automatically select which type to decode based on the inferred return type:input auto "True" :: IO BoolTrue0Use this to provide more detailed error messages }> input auto "True" :: IO Integer *** Exception: Error: Expression doesn't match annotation True : Integer (input):1:1  G> detailed (input auto "True") :: IO Integer *** Exception: Error: Expression doesn't match annotation Explanation: You can annotate an expression with its type or kind using the 'p:'q symbol, like this: % %%%%%%%% % x : t % 'px'q is an expression and 'pt'q is the annotated type or kind of 'px'q %%%%%%%%% The type checker verifies that the expression's type or kind matches the provided annotation For example, all of the following are valid annotations that the type checker accepts: % %%%%%%%%%%%%%% % 1 : Integer % 'p1'q is an expression that has type 'pInteger'q, so the type %%%%%%%%%%%%%%% checker accepts the annotation % %%%%%%%%%%%%%%%%%%%%%%%%% % Natural/even +2 : Bool % 'pNatural/even +2'q has type 'pBool'q, so the type %%%%%%%%%%%%%%%%%%%%%%%%%% checker accepts the annotation % %%%%%%%%%%%%%%%%%%%%% % List : Type ! Type % 'pList'q is an expression that has kind 'pType ! Type'q, %%%%%%%%%%%%%%%%%%%%%% so the type checker accepts the annotation % %%%%%%%%%%%%%%%%%%% % List Text : Type % 'pList Text'q is an expression that has kind 'pType'q, so %%%%%%%%%%%%%%%%%%%% the type checker accepts the annotation However, the following annotations are not valid and the type checker will reject them: % %%%%%%%%%%% % 1 : Text % The type checker rejects this because 'p1'q does not have type %%%%%%%%%%%% 'pText'q % %%%%%%%%%%%%%% % List : Type % 'pList'q does not have kind 'pType'q %%%%%%%%%%%%%%% You or the interpreter annotated this expression: ! True ... with this type or kind: ! Integer ... but the inferred type or kind of the expression is actually: ! Bool Some common reasons why you might get this error: % The Haskell Dhall interpreter implicitly inserts a top-level annotation matching the expected type For example, if you run the following Haskell code: % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % >>> input auto "1" :: IO Text % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ... then the interpreter will actually type check the following annotated expression: % %%%%%%%%%%% % 1 : Text % %%%%%%%%%%%% ... and then type-checking will fail %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% True : Integer (input):1:1 Decode a input bool "True"True Decode a input natural "+42"42 Decode an input integer "42"42 Decode a input double "42.0"42.0Decode input text "\"Test\"""Test" Decode a .input (maybe integer) "[1] : Optional Integer"Just 1 Decode a "input (vector integer) "[1, 2, 3]"[1,2,3]=Use the default options for interpreting a configuration file 'auto = autoWith defaultInterpretOptionsFDefault interpret options, which you can tweak or override, like this: \autoWith (defaultInterpretOptions { fieldModifier = Data.Text.Lazy.dropWhile (== '_') }).1The type of value to decode from Dhall to HaskellThe Dhall programThe decoded value in Haskell     %      None   !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~~W      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`a bcdefgghijklmnopqrstu vwxyz{ |} b~r.0 bW8"dhall-1.2.0-I1pG4NnuwrcHJ5oplzmMt5Dhall Dhall.Core Dhall.Parser Dhall.ContextDhall.TypeCheck Dhall.ImportData.MapMap Data.VoidVoidDhall.Tutorialbase GHC.GenericsGeneric#text-1.2.2.1-9Yh8rJoh8fO2JMLWffT3QsData.Text.Internal.LazyText GHC.NaturalNatural&vector-0.11.0.0-6uB77qGCxR6GPLxI2sqsX3 Data.VectorVectorExprConstVarLamPiAppLetAnnotBoolBoolLitBoolAndBoolOrBoolEQBoolNEBoolIf NaturalLit NaturalFold NaturalBuild NaturalIsZero NaturalEven NaturalOdd NaturalPlus NaturalTimesInteger IntegerLitDouble DoubleLitTextLit TextAppendListListLit ListBuildListFold ListLengthListHeadListLast ListIndexed ListReverseOptional OptionalLit OptionalFoldRecord RecordLitUnionUnionLitCombineMergeFieldNoteEmbedVPathpathTypepathModePathModeCodeRawTextPathTypeFileURLEnvHasHomeHomeHomelessTypeKindprettyshiftsubst normalize isNormalized internalError$fBuildableExpr$fIsStringExpr$fBifunctorExpr $fMonadExpr$fApplicativeExpr$fBuildableVar $fIsStringVar$fBuildablePath$fBuildablePathType$fBuildableConst $fShowConst$fBoundedConst $fEnumConst $fEqHasHome $fOrdHasHome $fShowHasHome $fEqPathType $fOrdPathType$fShowPathType $fEqPathMode $fOrdPathMode$fShowPathMode$fEqPath $fOrdPath $fShowPath$fEqVar $fShowVar $fFunctorExpr$fFoldableExpr$fTraversableExpr $fShowExpr ParseErrorParserunParserSrcexprexprA exprFromText$fExceptionParseError$fShowParseError$fTokenParsingParser$fBuildableSrc $fShowSrc$fFunctorParser$fApplicativeParser $fMonadParser$fAlternativeParser$fMonadPlusParser$fParsingParser$fCharParsingParser$fDeltaParsingParser$fMarkParsingParserContextemptyinsertlookuptoList$fFunctorContextDetailedTypeError TypeErrorcontextcurrent typeMessage TypeMessageUnboundVariableInvalidInputTypeInvalidOutputType NotAFunction TypeMismatch AnnotMismatchUntypedMissingListTypeMismatchedListElementsInvalidListElementInvalidListTypeInvalidOptionalElementInvalidOptionalLiteralInvalidOptionalTypeInvalidPredicateIfBranchMismatchIfBranchMustBeTerm InvalidFieldInvalidFieldTypeInvalidAlternativeInvalidAlternativeTypeDuplicateAlternativeMustCombineARecordFieldCollisionMustMergeARecordMustMergeUnion UnusedHandlerMissingHandlerHandlerInputTypeMismatchHandlerOutputTypeMismatchHandlerNotAFunction NotARecord MissingFieldCantAndCantOrCantEQCantNECantTextAppendCantAdd CantMultiplyNoDependentLetNoDependentTypesXabsurdtypeWithtypeOf$fBuildableDetailedTypeError$fExceptionDetailedTypeError$fShowDetailedTypeError$fBuildableTypeError$fExceptionTypeError$fShowTypeError $fBuildableX$fShowX$fShowTypeMessage MissingFilePrettyHttpExceptionImported importStacknestedReferentiallyOpaque opaqueImportCycle cyclicImport exprFromPathload $fShowMissingEnvironmentVariable%$fExceptionMissingEnvironmentVariable$fShowMissingFile$fExceptionMissingFile$fShowPrettyHttpException$fExceptionPrettyHttpException$fShowImported$fExceptionImported$fShowReferentiallyOpaque$fExceptionReferentiallyOpaque $fShowCycle$fExceptionCycleGenericInterpretgenericAutoWithInterpretOptions fieldModifierconstructorModifier InterpretautoWith InvalidTypeinputdetailedboolnaturalintegerdoubletextmaybevectorautodefaultInterpretOptions$fGenericInterpretM1$fGenericInterpret:*:$fGenericInterpretU1$fGenericInterpretM10$fGenericInterpret:+:$fGenericInterpret:+:0$fGenericInterpret:+:1$fGenericInterpret:+:2$fGenericInterpretV1$fGenericInterpretM11$fInterpretVector$fInterpretMaybe$fInterpretText$fInterpretDouble$fInterpretInteger$fInterpretNatural$fInterpretBool$fExceptionInvalidType$fShowInvalidType $fFunctorTypeghc-prim GHC.TypesInt buildLabel buildNumber buildNatural buildDouble buildText buildExpr buildExprA buildExprB buildExprC buildExprC0 buildExprC1 buildExprC2 buildExprC3 buildExprC4 buildExprC5 buildExprC6 buildExprC7 buildExprD buildExprE buildExprF buildConstbuildVar buildElemsbuildRecordLitbuildFieldValuesbuildFieldValue buildRecordbuildFieldTypesbuildFieldType buildUnionbuildAlternativeTypesbuildAlternativeType buildUnionLit_ERROR buildVector'trifecta-1.6.2.1-3QMcPRc8HsXDUKDnGXdYujText.Trifecta.ParseridentifierStylenotedtoMapreservesymbolsepBysepBy1 stringLiteraldoubleSingleQuoteStringlambdapiarrowcombinelabelexprBlistLikeexprCexprDexprEexprFconstvarelems recordLit fieldValues fieldValuerecord fieldTypes fieldTypeunionalternativeTypesalternativeTypeunionLitlistLitimport_fileurlenvGHC.Basefmap getContextshortlong ErrorMessagesaxiomrulematch propEqualshortTypeMessagelongTypeMessage_NOTprettyTypeMessagebuildBooleanOperatorbuildNaturalOperatorMissingEnvironmentVariable*http-client-0.5.6.1-IktGbVskunsLmiEIjZFcLLNetwork.HTTP.Client.Types HttpExceptionGHC.ShowShow canonicalize/system-filepath-0.4.13.4-2KYE6gPfKoHGyXJ6d0451GFilesystem.Path.InternalFilePathGHC.ListreverseStringclean loadDynamic loadStaticStatus_stack_cache_managernamebuilderToStringcanonicalizeAllstackcachemanager needManagercanonicalizePath parentURLremoveAtFromURLremoveAtFromFileexpectedextract integer-gmpGHC.Integer.TypeMaybethrows