śĪ!ƒRzŠŽ      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~€‚ƒ„…†‡ˆ‰Š‹ŒNone3K6morte$Bound variable names and their types0Variable names may appear more than once in the . The Var x@n refers to the nth occurrence of x in the  (using 0-based numbering).morte(An empty context with no key-value pairs toList empty = []morteAdd a key-value pair to the morteLookup a key by name and index ilookup k 0 (insert k v0 ctx ) = Just v0 lookup k 1 (insert k v0 (insert k v1 ctx)) = Just v1morte+Return all key-value associations as a listNone 1345KQV?cmorte-A structured type error that includes context morteThe specific type errormorteSyntax tree for expressionsmorte Const c ~ cmorte )Var (V x 0) ~ x Var (V x n) ~ x@nmorte Lam x A b ~ »(x : A) !’ bmorte =Pi x A B ~ "(x : A) !’ B Pi unused A B ~ A !’ Bmorte App f a ~ f amorte Embed path ~ #pathmorteLike , except with an Ž0 instance in order to avoid orphan instancesmortePath to an external resource morte+Constants for the calculus of constructionsThe only axiom is: "¦ * : %”&... and all four rule pairs are valid: /"¦ * ! * : * "¦ %” ! * : * "¦ * ! %” : %” "¦ %” ! %” : %”#morteLabel 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: ’@ +-refers to-+ | | v | \(x : *) -> \(y : *) -> \(x : *) -> x@0 +-------------refers to-------------+ | | v | \(x : *) -> \(y : *) -> \(x : *) -> 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 : *) -> \(y : *) -> \(x : *) -> x.Zero indices are omitted when pretty-printing #6s and non-zero indices appear as a numeric suffix.%morte Pretty-print an expression as a ‘, using Unicode symbols&morte Pretty-print an expression as a ‘, using ASCII symbols'morte;Substitute all occurrences of a variable with an expression subst x n C B ~ B[x@n := C](morte shift n x adds n* to the index of all free variables named x within an )morteyType-check an expression and return the expression's type if type-checking suceeds 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 + it afterwards.*morte* 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.’morte-Reduce an expression to weak-head normal form“morte3Returns whether a variable is free in an expression+morte]Reduce an expression to its normal form, performing both beta reduction and eta reduction+Ā 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.,mortePretty-print a value:morte-Generates a syntactically valid Morte program'   "!#$%&'()*+,'#$ "!)*+(',%&  NoneDEłUmorte<Token type, used to communicate between the lexer and parserdmorteA U augmented with h informationhmorte+The cursor's location while lexing the textlmorteFConvert a text representation of an expression into a stream of tokenslT keeps track of position and returns the remainder of the input if lexing fails.U`c\Ya[Zb^VWX]_defghijkllU`c\Ya[Zb^VWX]_hijkdefgNone1LK0qmorte"Structured type for parsing errorsumorteThe specific parsing errorvmorte2Lexing failed, returning the remainder of the textwmorteCParsing failed, returning the invalid token and the expected tokensxmorte Parse an  from  or return a q if parsing failsqrstuvwxxqrstuvwNone1z> }morte6Extend another exception with the current import stackmorte)Imports resolved so far, in reverse order€morteThe nested exceptionmorteŠMorte 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 term this "static linking". Morte (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 Morte can still try to guard against common unintentional violations. To do this, Morte 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-localƒmorteThe offending opaque import„morte7An import failed because of a cycle in the import graph†morteThe offending cyclic import”morteaThis function computes the current path by taking the last absolute path (either an absolute • or 8) 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 –xs in the URL-handling cod 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 —$ at all is for consistency with the  http-client library.˜morte Remove all .'s and ..'s in the path™morteLoad a : as a "dynamic" expression (without resolving any imports)YThis also returns the true final path (i.e. explicit "/@" at the end for directories)šmorteLoad a 5 as a "static" expression (with all imports resolved)‡morte(Resolve all imports within an expressionšBy default the starting path is the current directory, but you can override the starting path with a file if you read in the expression from that file‡morte Starting pathmorteExpression to resolve }~€‚ƒ„…†‡ ‡„…†‚ƒ}~€NonezĢ›      !""#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^'(_`ab%&cddefghijklmnoppfqrstuvwxyzz{|}}~€‚ƒ„…†‡ˆ‰Š‹ŒŽ‹‘’“”•–—˜™š›™œžŸ ”#morte-1.6.20-38bZ0rt6aOp7ringjrj0q4 Morte.Context Morte.Core Morte.Lexer Morte.Parser Morte.Import Data.VoidVoidMorte.TutorialContextemptyinsertlookuptoList$fFunctorContext$fNFDataContext TypeErrorcontextcurrent typeMessage TypeMessageUnboundVariableInvalidInputTypeInvalidOutputType NotAFunction TypeMismatchUntypedExprConstVarLamPiAppEmbedXabsurdPathFileURLStarBoxV buildExprbuildExprASCIIsubstshifttypeWithtypeOf normalizepretty$fBuildableVar $fNFDataVar $fIsStringVar $fBinaryVar$fBuildableConst $fNFDataConst $fBinaryConst$fBuildablePath $fBinaryX $fBuildableX $fNFDataX$fShowX$fEqX$fBuildableExpr $fNFDataExpr$fIsStringExpr $fBinaryExpr$fEqExpr $fMonadExpr$fApplicativeExpr$fBuildableTypeMessage$fNFDataTypeMessage$fBuildableTypeError$fNFDataTypeError$fExceptionTypeError$fShowTypeError$fEqVar $fShowVar $fEqConst $fShowConst$fBoundedConst $fEnumConst$fEqPath $fOrdPath $fShowPath $fFunctorExpr$fFoldableExpr$fTraversableExpr $fShowExpr$fShowTypeMessageToken OpenParen CloseParenColonAtArrowLambdaLabelNumberEOF LocatedTokentokenpositionPositionPlineNocolumnNolexExpr$fShowPosition $fEqToken $fShowToken$fShowLocatedToken ParseError parseMessage ParseMessageLexingParsing exprFromText$fBuildableParseError$fExceptionParseError$fShowParseError$fShowParseMessageImported importStacknestedReferentiallyOpaque opaqueImportCycle cyclicImportload $fShowCycle$fExceptionCycle$fShowReferentiallyOpaque$fExceptionReferentiallyOpaque$fShowImported$fExceptionImporteddeepseq-1.4.3.0Control.DeepSeqNFData text-1.2.3.0Data.Text.Internal.LazyTextghc-prim GHC.TypesIntData.Text.Internal.BuilderBuilderwhnffreeIn canonicalize-system-filepath-0.4.14-9jYDOZRDoMqIkxdisSNvm4Filesystem.Path.InternalFilePathbaseGHC.ListreverseGHC.BaseStringclean loadDynamic loadStatic