[ɓ      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz { | } ~  (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone!"'=JK 0More perspicuous synonym for operator precedenceLike !Precedence for top-level printing Convert a  to a  Convert a  to a  for further rendering Enclose a  in parens if the flag is  Synonym for  /(Inefficiently) strips whitespace from a string NPluck out the nth item from a list, or use a default if the list is too short      (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone !"'(24=HJKM Singleton for a typing context An implicit ", wrapped up in a class constraintSingleton for a glambda type Representation of a glambda typeA function type>Perhaps convert a string representation of a base type into a #The singleton for the empty context Convert a  into an . Convert an  into a  Compare two s for equality.      (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone!"(*E 0A lexed token with location information attached A lexed token00 ("unchecked 2%") is an existential package for an 22An  ArithOp ty; is an operator on numbers that produces a result of type tyG Compare two 2/s (potentially of different types) for equalityHPerhaps extract a 0IPerhaps extract an JPerhaps extract an KPerhaps extract a L$Remove location information from an ? !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKL0 !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKL02<;:987654301G=>?@ABCDEF/.-,+*)('&%$#"! LHIJK#/.-,+*)('&%$#"! 012 <;:9876543=>?@ABCDEFGHIJKL(C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone  !"24 M2A class for expressions that can be pretty-printedO;Information about coloring in de Bruijn indexes and bindersMa stream of remaining colors to use, and the colors used for bound variablesA function that changes a s color2Returns (overall, left, right) precedences for an 2PA O for an empty contextQConvenient implementation of RPrint a variableSPrint a lambda expressionTPrint an applicationUPrint an arithemtic expressionVPrint a conditionalWPrint a fixMNOPQRSTUVW MNOPQRSTUVW MNQOPRSTUVWMNOPQRSTUVW(C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone !"'(=JKMX:Classifies types that can be values of glambda expressionsYwWell-typed closed values. Encoded as a data family with newtype instances in order to avoid runtime checking of valuesZ6Convert a glambda value back into a glambda expression[ Exp ctx ty$ is a well-typed expression of type ty in context ctx. Note that a context is a list of types, where a type's index in the list indicates the de Bruijn index of the associated term-level variable.d Elem xs x is evidence that x is in the list xs. EZ :: Elem xs x is evidence that x is the first element of xs. ES ev :: Elem xs x is evidence that x is one position later in xs than is indicated in ev Convert an d to a proper de Bruijn indexg+Equality on expressions, needed for testinghPretty-prints a Y{. This needs type information to know how to print. Pattern matching gives GHC enough information to be able to find the X" instance needed to construct the M instance. XYZ[\]^_`abcdefghXYZ[\]^_`abcdefgh[cba`_^]\dfeXYZhgXYZ[cba`_^]\dfegh(C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone!"(3HMiKThe global variable environment maps variables to type-checked expressionsAn existential wrapper around [', storing the expression and its type.j$An empty global variable environmentk Extend a i with a new bindingl%Lookup a global variable. Fails with  if the variable is not bound.ijklijklijklijkl(C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone136B m"Class for the two glamorous monadsnPrint a  without a newline at the endoPrint a  with a newlinep Like the q/ monad, but also supporting error messages via sq5A monad giving Haskeline-like interaction, access to i!, and the ability to abort with .rGPrompt the user for input, returning a string if one is entered. Like .s Abort the q monadt#Abort the computation with an erroru Hoist an  into pvRun a q computationwRun a p computationmnopqrstuvw mnopqrstuvw qvrspwtumno mnopqrstuvw(C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone !"'(=JKM Length xs tells you how long a list xs is. LZ :: Length xs says that xs is empty. LS len :: Length xs tells you that xs has one more element than len says.xConvert an expression typed in one context to one typed in a larger context. Operationally, this amounts to de Bruijn index shifting. As a proposition, this is the weakening lemma.ycSubstitute the first expression into the second. As a proposition, this is the substitution lemma.xyxyxyxy (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNonezUnchecked expressionde Bruijn index for a variable z{|}~ z{|}~ z~}|{z ~}|{ (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNonemA statement can either be a bare expression, which will be evaluated, or an assignment to a global variable. (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNoneT XParse a sequence of semicolon-separated statements, aborting with an error upon failure2Parse a sequence of semicolon-separated statementsParse a %, aborting with an error upon failureParse a Parse a z%, aborting with an error upon failureParse a zBind a name over an expressionParse the given nullary tokenParse the given unary tokenParse one of a set of 2sposition of the current token current tokenremaining tokenslocation of the next token (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone %Lex some program text into a list of s, aborting upon failure%Lex some program text into a list of s Overall lexer'Lex either one token or some whitespaceLex some whitespaceLex a  {- ... -}O comment (perhaps nested); consumes no input if the target doesn't start with {-.-Lex a block comment, without the opening "{-"Lex a line comment Lex one tokenLex one non-alphanumeric tokenLex one arithmetic operator Lex one alphanumeric token  Lex one word        (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone !"'(=HJKM .Given a lambda and an expression, beta-reduce.+Apply an arithmetic operator to two values.,Conditionally choose between two expressions Unroll a fix one level8A well-typed variable in an empty context is impossible.1Evaluate an expression, using big-step semantics.?Step an expression, either to another expression or to a value.  (C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone !"'(3=HM/Abort with a type error in the given expressionCheck the given expression, aborting on type errors. The resulting type and checked expression is given to the provided continuation. This is parameterized over the choice of monad in order to support pure operation during testing. p( is the canonical choice for the monad.UTake a closed expression and shift its indices to make sense in a non-empty context.(C) 2015 Richard EisenbergBSD-style (see LICENSE)%Richard Eisenberg (eir@cis.upenn.edu) experimentalNone 24Q!The glamorous Glambda interpreterPrints welcome messageThe welcome messageThe current version of glambda@Run a sequence of statements, returning the new global variablesRun a E and then run another action with the global variables built in the )Interpret a command (missing the initial :). !"#$%&'()*+,-./01 !"#$%&'()*+,-./012 !"#$%&'()*+,-./0123456789:;<=>?@ABB;CDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~              :9_y                                    ! "#$%&'()*+,-./0123456789:;<=>?@ABC glambda-1.0.1Language.Glambda.UtilLanguage.Glambda.TypeLanguage.Glambda.TokenLanguage.Glambda.PrettyLanguage.Glambda.ExpLanguage.Glambda.GlobalsLanguage.Glambda.MonadLanguage.Glambda.ShiftLanguage.Glambda.UncheckedLanguage.Glambda.StatementLanguage.Glambda.ParseLanguage.Glambda.LexLanguage.Glambda.EvalLanguage.Glambda.CheckLanguage.Glambda.ReplbaseData.Type.EqualityRefl:~:PrecignoretopPrecrender toSimpleDoc maybeParens$$stripWhitespace nthDefaultSCtxSConsSNilITystySTySBoolTySIntTySArrTyBoolTyIntTyArr readTyCon emptyContextrefineTy unrefineTyeqSTyLTokenLTokenNameSemiAssignFixTElseThenIfBoolIntArithOpColonArrowDotLambdaRParenLParenUArithOpEqualsGreaterEGreaterLessELessModDivideTimesMinusPlusuPlusuMinusuTimesuDivideuModuLessuLessEuGreater uGreaterEuEquals eqArithOp unArithOpunIntunBoolunNameunLoc PrettyExp prettyExpColoringdefaultColoring defaultPretty prettyVar prettyLam prettyApp prettyArithprettyIf prettyFixGlamValValvalExpBoolEIntEFixCondArithAppLamVarElemESEZeqExp prettyValGlobals emptyGlobalsextend lookupGlobalGlamMprintDoc printLineGlamEGlampromptquit issueError eitherToGlamErunGlamrunGlamEshiftsubstUExpUBoolEUIntEUFixUCondUArithUAppULamUGlobalUVar Statement NewGlobalBareExp parseStmtsG parseStmts parseStmtG parseStmt parseExpGparseExplexGlexevalstepcheckmain Control.Monadvoidansi-wl-pprint-0.6.7.3Text.PrettyPrint.ANSI.LeijenDocGHC.BaseString SimpleDocghc-prim GHC.TypesTrue<$>$fPrettyParseError arrowLeftPrecarrowRightPrec arrowPrec pretty_ty $fPrettySTy$fShowTy $fPrettyTy $fITyBool$fITyInt $fITy(->) PrintingInfoalonegetDoc printingInfo printTogether $fShowLToken$fPrettyLToken $fShowToken $fPrettyToken$fShowUArithOp$fPrettyUArithOp $fShowArithOp$fPrettyArithOp $fEqUArithOp $fEqArithOp ApplyColorprecInfoprettylamPrecappPrec appLeftPrec appRightPrecifPrecopPrec opLeftPrec opRightPrec elemToIntLamValBoolValIntVal pretty_exp$fPrettyExpVal $fPrettyVal$fPrettyExpExp $fPrettyExpTFCo:R:Val(->) $fGlamVal(->)TFCo:R:ValBool $fGlamValBool TFCo:R:ValInt $fGlamValIntEExp mtl-2.1.3.1Control.Monad.Error.Class throwErrormzerohaskeline-0.7.1.2System.Console.Haskeline getInputLine Data.EitherEitherunGlamEunGlam $fGlamMGlamE $fGlamMGlam$fMonadReaderGlobalsGlamELength++LSLZ TFCo:R:++k:ysTFCo:R:++k[]ys$fPrettyExpUExp $fPrettyUExp$fPrettyStatementbindtoktok'arith_opParserparsenext_posstmtsstmtexprint_exptermappsfactorlamcondvartyarg_tytyconadd_opmul_opbool_opmk_oplexer lexer1_ws whitespace block_comment comment_body line_commentlexer1symbolic word_tokenwordLexerstring_applyarithunfix impossibleVar typeErrorshift_into_ctx check_var helloWorldlambdaversiondoStmtsdoStmt runCommand Reportablereport CommandTablelooprunStmtsdispatchCommandcmdTablequitCmd reportErrorsparseLex printWithTypeprintValWithTypelexCmdparseCmdevalCmdstepCmdtypeCmdallCmdloadCmd $fReportablea$fReportableGlobals$fReportable()$fReportableDoc