8>      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~  *Utilities used by the Sequent Core librarymaurerl@cs.uoregon.edu experimentalNone!If debug output is on, show some  on the screen None  NoneSequent Core syntaxmaurerl@cs.uoregon.edu experimentalNoneJ^A class of types that contain an identifier. Useful so that we can compare, say, elements of  Command b for any b7 that wraps an identifier with additional information.Usual instance of  , with  s for binders Usual instance of , with  s for binders Usual instance of , with  s for binders Usual instance of , with  s for binders Usual instance of , with  s for binders A case alternative. Given by the head constructor (or literal), a list of bound variables (empty for a literal), and the body as a .A binding. Similar to the Bind` datatype from GHC. Can be either a single non-recursive binding or a mutually recursive block.WA general computation. A command brings together a list of bindings, some term, and a  continuation^ saying what to do with the value produced by the term. The term and continuation comprise a cut in the sequent calculus. Invariant: If )1 is a variable representing a constructor, then * must not begin with as many 0 frames as the constructor's arity. In other words, the command must not represent a saturated application of a constructor. Such an application should be represented by a 5$ value instead. When in doubt, use  to enforce this invariant.A continuation, representing a strict context of a Haskell expression. Computation in the sequent calculus is expressed as the interaction of a value with a continuation.|An expression producing a value. These include literals, lambdas, and variables, as well as types and coercions (see GHC's w for the reasoning). They also include computed values, which bind the current continuation in the body of a command.Constructs a command, given let& bindings, a term, and a continuation.kThis smart constructor enforces the invariant that a saturated constructor invocation is represented as a 5 value rather than using 0 frames.@The class of types that can be compared up to alpha-equivalence.MTrue if the two given terms are the same, up to renaming of bound variables.True if the two given terms are the same, up to renaming of bound variables and the specified equivalences between free variables.The type of the environment of an alpha-equivalence comparison. Only needed by user code if two terms need to be compared under some assumed correspondences between free variables. See GHC's  module for operations.%The identifier contained by the type a.Usual instance of , with  s for bindersUsual instance of , with  s for binders$Usual binders for Sequent Core termsAn entire program.jSome expression -- a term, a command, or a continuation. Useful for writing mutually recursive functions.%'A block of mutually recursive bindings.&A single non-recursive binding.(%Bindings surrounding the computation.)The term producing the value.*What to do with the value.+WThe identifier for a covariable, which is like a variable but it binds a continuation.,"Reference to a bound continuation.-2Annotate the enclosed frame. Used by the profiler..(Cast the value using the given coercion./#Perform case analysis on the value.0Apply the value to an argument.1A continuation. Allowed only! as the body of a non-recursive let.2+A coercion. Used to pass evidence for the cast operation to a lambda.3CA type. Used to pass a type as an argument to a type-level lambda.49A value produced by a computation. Binds a continuation.57A value formed by a saturated constructor application.6LA function. Binds some arguments and a continuation. The body is a command.7A term variable. Must not be a nullary constructor; use 5 for this.8A primitive literal value.9KWraps a command that returns to the given continuation id in a term using 4). If the command is a value command (see O), unwraps it instead.:;Adds the given bindings outside those in the given command.;hAdds the given binding outside the given command, possibly using a case binding rather than a let. See CoreSyn on the let/app invariant.=RDivide a continuation into a sequence of arguments and an outer continuation. If k+ is not an application continuation, then collectArgs k == ([], k).>WDivide a continuation into a sequence of type arguments and an outer continuation. If kN is not an application continuation or only applies non-type arguments, then collectTypeArgs k == ([], k).?Divide a continuation into a sequence of type arguments, then a sequence of non-type arguments, then an outer continuation. If k+ is not an application continuation, then (collectTypeAndOtherArgs k == ([], [], k).@/Divide a continuation into a sequence of up to n* arguments and an outer continuation. If k+ is not an application continuation, then collectArgsUpTo n k == ([], k).AQDivide a list of terms into an initial sublist of types and the remaining terms.BXTrue if the given command is a simple lambda, with no let bindings and no continuation.D&True if the given term is a type. See .E*True if the given term is a coercion. See .F-True if the given term is a type or coercion.GRTrue if the given term appears at runtime, i.e. is neither a type nor a coercion.HTrue if the given term can appear in an expression without restriction. Not true if the term is a type, coercion, or continuation; these can only appear on the RHS of a let or (except for continuations) as an argument in a function call.ITrue if the given command is so simple we can duplicate it freely. This means it has no bindings and its term and continuation are both trivial.JTrue if the given term is so simple we can duplicate it freely. Some literals are not trivial, and a lambda whose argument is not erased or whose body is non-trivial is also non-trivial.KTrue if the given continuation is so simple we can duplicate it freely. This is true of casts and of applications of erased arguments (types and coercions). Ticks are not considered trivial, since this would cause them to be inlined.L9True if the given continuation is a return continuation, Return _.MIf a command represents a saturated call to some function, splits it into the function, the arguments, and the remaining continuation after the arguments.NIf the given term is a function, and the given continuation would provide enough arguments to saturate it, returns the arguments and the remainder of the continuation.O`If a command does nothing but provide a value to the given continuation id, returns that value.TCompute the type of a term.U,Compute the type a continuation accepts. If  contType cont is Foo and cont is bound to k, then k's idType will be !Foo.V9Compute (a conservative estimate of) the arity of a term.W0Find whether an expression is definitely bottom.X6Find whether a command definitely evaluates to bottom.Y,Decide whether a term should be bound using case rather than let. See .f(Find whether an id is a continuation id.gTag an id as a continuation id.3An empty context for alpha-equivalence comparisons.iMTrue if the two given terms are the same, up to renaming of bound variables.If the given lists of bindings are alpha-equivalent, returns an augmented environment tracking the correspondences between the bound variables.If the given bindings are alpha-equivalent, returns an augmented environment tracking the correspondences between the bound variables.z  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghig  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghig876543210/.-,'()*&% $" #!+ 9:;<=>?@ABCDEFGHIJKLMNOPQRSVTUWXYZ\^[]_`bdacefghi] $&%'()*0/.-,87654321" #!+9:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghii%Pretty printing of Sequent Core termsmaurerl@cs.uoregon.edu experimentalNone=Print the given bindings as a sequence of top-level bindings.          Nonemn mnmnmn None !"#$%&'()*+,-./0123456789:;<=>?@'()*+123!&"#$%'()*+,-./0123456789:;<=>?@None#o$An environment for substituting for Asp,A substitution environment, containing both A and B substitutions.6Some invariants apply to how you use the substitution: in_scope_invariant* The in-scope set contains at least those As and Bs that will be in scope after applying the substitution to a term. Precisely, the in-scope set must be a superset of the free vars of the substitution range that might possibly clash with locally-bound variables in the thing being substituted in. apply_once% You may apply the substitution only oncecThere are various ways of setting up the in-scope set such that the first of these invariants hold:?Arrange that the in-scope set really is all the things in scope@Arrange that it's the free vars of the range of the substitutionoMake it empty, if you know that all the free vars of the substitution are fresh, and hence can't possibly clashvFind the in-scope set: see CoreSubst#in_scope_invariantwRemove all substitutions for As and Bs that might have been built up while preserving the in-scope setxAdd a substitution for an A to the p:: you must ensure that the in-scope set is such that the CoreSubst#in_scope_invariant3 is true after extending the substitution like thisyAdds multiple A substitutions to the p : see also xzAdd a substitution for a B to the p:: you must ensure that the in-scope set is such that the CoreSubst#in_scope_invariant3 is true after extending the substitution like this{Adds multiple B substitutions to the p : see also z|Add a substitution from a C to a  to the p:: you must ensure that the in-scope set is such that the CoreSubst#in_scope_invariant3 is true after extending the substitution like this}Adds multiple C ->  substitutions to the p : see also |~yAdd a substitution appropriate to the thing being substituted (whether an expression, type, or coercion). See also x, z, and |.Add a substitution as appropriate to each of the terms being substituted (whether expressions, types, or coercions). See also ~.Find the substitution for an A in the pFind the substitution for a B in the p%Find the coercion substitution for a C in the pSimultaneously substitute for a bunch of variables No left-right shadowing ie the substitution for (x y. e) a1 a2 so neither x nor y scope over a1 a2Add the J to the in-scope set, but do not remove any existing substitutions for itAdd the U to the in-scope set: as a side effect, and remove any existing substitutions for itAdd the  s to the in-scope set: see also Optimized version of F that can be used if you are certain all the things being added are As and hence none are Bs or Cs!Apply a substititon to an entire CoreBind$, additionally returning an updated p1 that should be used by subsequent substitutons.!Apply a substititon to an entire CoreBind$, additionally returning an updated p1 that should be used by subsequent substitutons.De-shadowing the program is sometimes a useful pre-pass. It can be done simply by running over the bindings with an empty substitution, because substitution returns a result that has no-shadowing guaranteed.(Actually, within a single type+ there might still be shadowing, because @ is a no-op for the empty substitution, but that's probably OK.) Aug 09xThis function is not used in GHC at the moment, but seems so short and simple that I'm going to leave it hereSubstitutes a " for another one according to the p- given, returning the result and an updated p2 that should be used by subsequent substitutons. DM is preserved by this process, although it is substituted into appropriately.Applies  to a number of s, accumulating a new p left-to-right,Substitute in a mutually recursive group of AsVery similar to  , but it always allocates a new EE for each variable in its output. It substitutes the IdInfo though.Applies  to a number of A8s, accumulating a final substitution from left to right$Clone a mutually recursive group of AsSee FSee GHSubstitute into some D! with regard to the supplied new A.Substitutes for the As within an unfoldingSubstitutes for the As within an unfoldingSubstitutes for the A s within the  WorkerInfo given the new function ADopqrstuvwxyz{|}~IJKLMNO"Substitution to use for the IdInfo Substitition and Id to transform-Transformed pair NB: unfolding may be zappedPQRSTUVHWX5opqrstuvwxyz{|}~5pqostuvrxyz{|}~wCopqrstuvwxyz{|}~IJKLMNOPQRSTUVHWXCore <-> Sequent Coremaurerl@cs.uoregon.edu experimentalNoneE jJTake an operation on Sequent Core terms and perform it on Core expressionskTranslates a term into Core.l;Translates a single Core expression as a Sequent Core term.5Translates a list of Core bindings into Sequent Core.Y/Translates a Core expression into Sequent Core.Z5Translates a Core case alternative into Sequent Core.[,Translates a Core binding into Sequent Core.Translates a command into Core.Translates a continuation into a function that will wrap a Core expression with a fragment of context (an argument to apply to, a case expression to run, etc.).\Translates a binding into Core.2Translates a list of top-level bindings into Core.JTake an operation on Core expressions and perform it on Sequent Core termsjkl]^_`aYbcdZ[ef\gjkllkjjkl]^_`aYbcdZ[ef\gGHC plugin librarymaurerl@cs.uoregon.edu experimentalNoneGiven a function that processes a module's bindings as Sequent Core terms, perform the same processing as a Core-to-Core pass usable from a GHC plugin. Intended to be passed to the CoreDoPluginPass' constructor as part of your plugin's installCoreToDos function. See Language.SequentCore.Dump5 for an example and the GHC manual for more details.~A processing function. May assume that there are no shadowed identifiers in the given binders (this is ensured by a call to h).Example pluginmaurerl@cs.uoregon.edu experimentalNoneAThe plugin. A GHC plugin is a module that exports a value called plugin with the type i.jkjkSequent Core information dumpermaurerl@cs.uoregon.edu experimentalNoneAThe plugin. A GHC plugin is a module that exports a value called plugin with the type i. lmnopqrstlmnopqrstNone{uvwxyz{|}~`y{|}~Yuxwvyz{|}~   .Simplifier reimplementation using Sequent Coremaurerl@cs.uoregon.edu experimentalNone?EaPlugin data. The initializer replaces all instances of the original simplifier with the new one.Divide a continuation into some (floated) bindings, a simplified continuation we'll happily copy into many case branches, and possibly an unsimplified continuation that we'll keep in a let binding and invoke from each branch.>The rules: 1. Duplicate returns. 2. Duplicate casts. 3. Don't duplicate ticks (because GHC doesn't). 4. Duplicate applications, but ANF-ize them first to share the arguments. 5. Don't duplicate cases (!) because, unlike with Simplify.mkDupableCont, we don't need to (see comment in Case clause).ITODO We could conceivably copy single-branch cases, since this would still limit bloat, but we would need polyadic continuations in most cases (just as GHC's join points can be polyadic). The simplest option would be to use regular continuations of unboxed tuples for this, though that could make inlining decisions trickier..     +      SpecConstr reimplementationmaurerl@cs.uoregon.edu experimentalNoneA generated specialization---the call pattern that gave rise to it, the identifier of the specialized function, and the function's definition.iPlugin data. The initialization code replaces the built-in SpecConstr pass in the Core-to-Core pipeline. The kernel of the SpecConstr pass. Takes the environment, data about how variables are used, and a let binding (part of a recursive block), and returns a new list of bindings---the original one (with specialization rules added) and also all specialized versions.* !"#$%&'()*+,-./0123456789:;<=>?@ABCDE !"#$%&(')*+,-./0123456789:;<=>?@ABCDE?.External interface to the Sequent Core librarymaurerl@cs.uoregon.edu experimentalNoneq  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklF  !"#$%&'()*+,-./0123456789:;&<=(>?@ABCDEF)GHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~        LLHGG      !"#$%&'()*+,-../01233456789:;<=>?@ABCDEFGHIJKLLLMLNOOPPHGQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvvwxtyz{|}~]_^                                                    ! " # $ % & ' ( ) ) * + , - .  / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ ABsequent-core-0.5.0.1Language.SequentCore.SyntaxLanguage.SequentCore.SubstLanguage.SequentCore.PrettyLanguage.SequentCore.TranslateLanguage.SequentCore.LintLanguage.SequentCore.PluginLanguage.SequentCore.DumpLanguage.SequentCore.InspectLanguage.SequentCore.SimplLanguage.SequentCore.SpecConstrLanguage.SequentCore.Util Language.SequentCore.Simpl.MonadLanguage.SequentCore.WiredInGHCExpr CoreUtilsneedsCaseBinding#Language.SequentCore.Simpl.ExprSizeLanguage.SequentCore.Simpl.EnvLanguage.SequentCore ghc-7.8.3CoreSynDataAltLitAltDEFAULTAltConTypeRep TvSubstEnvVarEnv InScopeSetmkContTyHasId SeqCoreAlt SeqCoreBindSeqCoreCommand SeqCoreCont SeqCoreTermAltBindCommandContTerm mkCommandpprTopLevelBindsAlphaEqaeqaeqInAlphaEnv identifierSeqCoreProgram SeqCoreExpr SeqCoreBndrProgramKunKCunCTunTRecNonReccmdLetcmdTermcmdContContIdReturnTickCastCaseAppCoercionTypeComputeConsLamVarLit mkComputeaddLets addNonReclambdas collectArgscollectTypeArgscollectTypeAndOtherArgscollectArgsUpTopartitionTypesisLambda isValueArg isTypeTermisCoTerm isErasedTerm isRuntimeTerm isProperTerm isTrivial isTrivialTerm isTrivialCont isReturnContcommandAsSaturatedCallasSaturatedCallasValueCommand flattenBind flattenBinds bindersOfbindersOfBindstermTypecontType termArity termIsBottomcommandIsBottomtermOkForSpeculationtermOkForSideEffectscommandOkForSpeculationcommandOkForSideEffectscontOkForSpeculationcontOkForSideEffects termIsCheaptermIsExpandable contIsCheapcontIsExpandablecommandIsCheapcommandIsExpandableisContIdasContId contTyArg=~= onCoreExprtermToCoreExprtermFromCoreExprlintCoreBindingslintTerm IdSubstEnvSubst isEmptySubst emptySubst mkEmptySubstmkSubst substInScope zapSubstEnv extendIdSubstextendIdSubstList extendTvSubstextendTvSubstList extendCvSubstextendCvSubstList extendSubstextendSubstWithVarextendSubstList lookupIdSubst lookupTvSubst lookupCvSubstdelBndrdelBndrs mkOpenSubst isInScope addInScopeSet extendInScopeextendInScopeListextendInScopeIds setInScope substTerm substBindSC substBind deShadowBinds substBndr substBndrs substRecBndrs cloneIdBndr cloneIdBndrs cloneBndrs cloneBndrcloneRecIdBndrssubstTysubstCosubstUnfoldingSCsubstUnfolding substIdOcc substSpecsubstRulesForImportedIds substVarSet substTickishfromCoreModulecommandToCoreExprcontToCoreExpr bindsToCoreonSequentCoreTerm sequentPassplugin pprTraceShort OutputableSDoc consMaybe pprAndThenMaybesorElseSimplGlobalEnvsg_modeSimplMunSimplM traceTicks runSimplM liftCoreMgetModetickfreeTick withZeroCount$fMonadUniqueSimplM$fMonadIOSimplM$fHasDynFlagsSimplM$fApplicativeSimplM$fFunctorSimplM $fMonadSimplMDynFlags getDynFlagssequentCoreTagsequentCoreWiredInTag contKindKey contTypeKeycontFunTypeKey lamContKey argContKey letContKey contArgKey lamContName argContName letContName contArgNamecontKindTyConName contTyConNamecontFunTyConName mkLamContId mkArgContId mkLetContId mkContArgId contKindTyCon contTyCon contFunTyCon mkContKindisContTyisContTy_maybe mkContFunTy isContFunTysplitContFunTy_maybe emptyAlphaEnv aeqBindsIn aeqBindIn CheapMeasuretermOkcommOkcutOkcontOkappOk termCheap contCheap commCheapcutCheap isCheapAppisExpandableApp $fAlphaEqBind $fAlphaEq[]$fAlphaEqCoercion $fAlphaEqType $fAlphaEqAlt$fAlphaEqCommand $fAlphaEqCont $fAlphaEqTerm $fHasIdVarppr_bind ppr_binds_top ppr_block ppr_bindsppr_binds_with ppr_bindingppr_commppr_termppr_cont_framesppr_cont pprCoreAlt ppr_case_pat pprCoreComm pprCoreTermnoParens$fOutputableAlt$fOutputableCont$fOutputableCommand$fOutputableTerm$fOutputableBindLintEnvLintM eitherToMaybe lintCoreBind lintCoreTermlintCoreCommand lintCoreCut lintCoreContextendTvInScopeSubsted substTyInIdextendTvInScopeListSubstedmkError checkRhsType checkingTypecontIdTyOrErrorBodySizebsBase bsArgDiscs bsResultDiscTooBigExprSizeesBase esArgDiscs esResultDisc body2ExprSizesizeZerosizeNmaxSize mkBodySizetermSize commandSizecontSizebodySizelitSize classOpSizefunSize primOpSize buildSize augmentSizeconSizelamScrutDiscount isRealWorldIdisRealWorldTerm$fOutputableExprSize$fOutputableBodySizeIdTyVarCoVarIdInfoUnique substIdInfotoCoreIdSubstEnv toCoreSubst subst_term subst_comm subst_cont subst_expr substIdBndrclone_idsubstTyVarBndrcloneTyVarBndrsubstCoVarBndr getTvSubst getCvSubst substIdType substRule$fOutputableSubst fromCoreExpr fromCoreAlt fromCoreBind bindToCore FromCoreM FromCoreEnv uniqSupply freshContId runFromCoreM fromCoreLamsfromCoreExprAsTermfromCoreLamAsCont fromCoreBinds contIdToCore altToCore CoreSubst CoreMonadPlugininstallshowSequentCoreOptions optShowSizesoptUnrecognizeddefaults parseOptioninspectSequentCoreshowBind FloatFlag FltCareful FltOkSpec FltLiftedFloatsOutCoVarOutTyVarOutVarOutIdOutBindOutAltOutContOutTerm OutCommandInCoVarInTyVarInVarInIdInBindInAltInContInTerm InCommandGuidance SometimesguSizeguArgDiscountsguResultDiscountUsually guEvenIfUnsatguEvenIfBoringNever DefinitionNotAmong BoundToDFun dfunBndrs dfunDataCondfunArgsBoundTodefTermdefLevel defGuidanceIdDefEnvSubstAnsSuspTermDoneIdDoneTerm SimplIdSubst StaticEnvSimplEnv se_idSubst se_tvSubst se_cvSubstse_retId se_inScopese_defs se_floats se_dflags mkBoundTo mkGuidance initialEnv mkSuspension enterScope enterScopes mkFreshVar mkFreshContIdsubstIdrefine substTyVar substCoVar zapSubstEnvs setSubstEnvsbindCont bindContAspushContzapContsetContretType staticPart setStaticPartinDynamicScope restoreEnvandFF classifyFFdoFloatFromRhs emptyFloats unitFloataddNonRecFloat mapFloats extendFloats addFloats wrapFloatsaddFlts zapFloats addRecFloats getFloatBinds floatBinds getFloats isEmptyFloatsfindDefunfoldingToDefunfGuidanceToGuidancesetDefdefToUnfoldingguidanceToUnfGuidance termIsHNF commandIsHNF$fOutputableFloatFlag$fOutputableFloats$fOutputableGuidance$fOutputableDefinition$fOutputableSubstAns$fOutputableStaticEnv$fOutputableSimplEnvsplitDupableCont ContSplittingDupeSomeDupeNoneDupeAlltracingdumpinglinting runSimplifier simplModulesimplCommandNoFloats simplCommandsimplTermNoFloats simplTerm simplBinds simplBind simplNonRec simplLazyBindwrapFloatsAroundContwrapFloatsAroundTermcompleteNonRec completeBindsimplRecsimplCut simplCut2 matchCasesimplContNoFloats simplCont simplContWith simplCoercionsimplVar simplContIdpreInlineUnconditionallypostInlineUnconditionallycallSiteInline shouldInline someBenefit whnfOrBot inlineMultinoSizeIncrease smallEnough inlineDFun makeTrivial contIsCasecontIsCase_maybeSpec specializespec_patspec_id spec_defnCallPat:->ArgUsageHowBoundSpecArgSpecFunCallCallsScUsageScEnvSCEsc_size sc_how_bound sc_dflags specModule initScEnv emptyScUsage specInTerm specInCont specInAlt specInBind specInCommand specInCut usageFromCutspecBind specToBindingsamePat$fOutputableSpec$fOutputableCallPat$fMonoidScUsage$fOutputableHowBound$fOutputableScUsage$fOutputableScEnv