gJ#      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ portable*Stephanie Weirich <sweirich@cis.upenn.edu> Safe-Infered A  permutation- is a bijective function from names to names A which is the identity on all but a finite set of names. They = form the basis for nominal approaches to binding, but can  also be useful in general. 1Apply a permutation to an element of the domain. /Create a permutation which swaps two elements. "The empty (identity) permutation. >Compose two permutations. The right-hand permutation will be  applied first. "Is this the identity permutation? Join8 two permutations by taking the union of their relation D graphs. Fail if they are inconsistent, i.e. map the same element  to two different elements. The support3 of a permutation is the set of elements which are  not fixed. ,Restrict a permutation to a certain domain.  mkPerm l1 l2" creates a permutation that sends l1 to l2. B Fail if there is no such permutation, either because the lists B have different lengths or because they are inconsistent (which  can only happen if l1 or l2 have repeated elements). .Permutations form a monoid under composition.      GHC only (-XKitchenSink)$Brent Yorgey <byorgey@cis.upenn.edu> Safe-Infered &A simple representation of multisets. >Collections are foldable types that support empty, singleton, = union, and map operations. The result of a free variable B calculation may be any collection. Instances are provided for  lists, sets, and multisets. .An empty collection. Must be the identity for union. Create a singleton collection. )An associative combining operation. The Ord constraint is in  order to accommodate sets. ,Collections must be functorial. The normal Functor class  won't do because of the Ord constraint on sets. 'Combine a list of containers into one. -Create a collection from a list of elements.  Remove the Nothings from a collection. ASets are containers under union, which preserve only occurrence, ! not multiplicity or ordering. =Multisets are containers which preserve multiplicity but not  ordering. :Lists are containers under concatenation. Lists preserve * ordering and multiplicity of elements.        GHC only %Brent Yorgey <byorgey@cis.upenn.edu> None9s are things that get bound. This type is intentionally  abstract; to create a  you can use * or  )". The type parameter is a tag, or sort, which C tells us what sorts of things this name may stand for. The sort  must be a  representable type, i.e. an instance of the   type class from the RepLib generic programming framework.  To hide the sort of a name, use . ?A name with a hidden (existentially quantified) sort. To hide  the sort of a name, use the  constructor directly; to * extract a name with a hidden sort, use (. BTest whether a name is a bound variable (i.e. a reference to some E binding site, represented as a de Bruijn index). Normal users of E the library should not need this function, as it is impossible to E encounter a bound name when using the abstract interface provided  by Unbound.LocallyNameless. !<Test whether a name is a free variable. Normal users of the ; library should not need this function, as all the names > encountered will be free variables when using the abstract  interface provided by Unbound.LocallyNameless. $Get the integer index of a . %Get the string part of a . &Get the integer index of an . 'Get the string part of an . (?Cast a name with an existentially hidden sort to an explicitly  sorted name. )Create a free  from an . *Create a free  from a . +Convenient synonym for *. ,Create a free  from a String and an Integer index. -Determine the sort of a . .Change the sort of a name.  !"#$%&'()*+,-. !"#$%&'()*+,-.)*+,$%&'(.- !"# !"#$%&'()*+,-.unportable (GHC 7 only)  experimental %Brent Yorgey <byorgey@cis.upenn.edu> None/+A convenient monad which is an instance of 3 . It keeps D track of a set of names to avoid, and when asked for a fresh one 0 will choose the first unused numerical name. 0@The LFresh monad transformer. Keeps track of a set of names to E avoid, and when asked for a fresh one will choose the first numeric 5 prefix of the given name which is currently unused. 39This is the class of monads that support freshness in an F (implicit) local scope. Generated names are fresh for the current 0 local scope, not necessarily globally fresh. 4@Pick a new name that is fresh for the current (implicit) scope. 5=Avoid the given names when freshening in the subcomputation, 5 that is, add the given names to the in-scope set. 6.Get the set of names currently being avoided. 7+A convenient monad which is an instance of ; . It keeps E track of a global index used for generating fresh names, which is  incremented every time < is called. 8The FreshM5 monad transformer. Keeps track of the lowest index D still globally unused, and increments the index every time it is  asked for a fresh name. ;The Fresh2 type class governs monads which can generate new  globally unique s based on a given . <<Generate a new globally unique name based on the given one. =Run a 87 computation (with the global index starting at zero). >Run a 83 computation given a starting index for fresh name  generation. ?CRun a FreshM computation (with the global index starting at zero). @1Run a FreshM computation given a starting index. ARun an 0" computation in an empty context. BRun an 0, computation given a set of names to avoid. C/Run a LFreshM computation in an empty context. D9Run a LFreshM computation given a set of names to avoid. 8/0123456789:;<=>?@ABCD     /0123456789:;<=>?@ABCD;<7?@89:=>3456/CD012AB0/0123456789:;<=>?@ABCD     GHC only experimental$Brent Yorgey <byorgey@cis.upenn.edu>NoneE8Shift the scope of an embedded term one level outwards. GEmbed allows for terms to be embedded within patterns. Such ? embedded terms do not bind names along with the rest of the E pattern. For examples, see the tutorial or examples directories. If t is a  term type, then Embed t is a  pattern type. Embed9 is not abstract since it involves no binding, and hence > it is safe to manipulate directly. To create and destruct  Embed terms, you may use the Embed constructor directly. # (You may also use the functions embed and unembed, which B additionally can construct or destruct any number of enclosing  Es at the same time.) ITRec is a standalone variant of K: the only difference is  that whereas K p is a pattern type, TRec p  is a  term type. It is isomorphic to Q (K p) ().  Note that TRec corresponds to Pottier's  abstraction construct & from alpha-Caml. In this context, G t corresponds to  alpha-Caml's inner t, and E (G t) corresponds to  alpha-Caml's outer t. KIf p is a pattern type, then Rec p is also a pattern type,  which is  recursive in the sense that p may bind names in terms ? embedded within itself. Useful for encoding e.g. lectrec and  Agda's dot notation. MRebind allows for nested bindings. If p1 and p2 are  pattern types, then  Rebind p1 p2 is also a pattern type,  similar to the pattern type (p1,p2) except that p1   scopes over p2+. That is, names within terms embedded in p2  may refer to binders in p1. RAThe most fundamental combinator for expressing binding structure  is Q. The  term type Bind p t represents a pattern p  paired with a term t, where names in p are bound within t. Like , Q+ is also abstract. You can create bindings  using bind and take them apart with unbind and friends. EFGHIJKLMNOPQRSTUVWX, !"#$%&'()*+,-.EFGHIJKLMNOPQRSTUVWXRSQPOMNKLIJGHEFTVUWXEFGHIJKLMNOPQRSTUVWXGHC only (-XKitchenSink) %Brent Yorgey <byorgey@cis.upenn.edu>  Safe-Infered$Y=Class constraint hackery to allow us to override the default % definitions for certain classes. Y is essentially a  reified dictionary for the | class. h>A mode is basically a flag that tells us whether we should be C looking at the names in the term, or if we are in a pattern and  should only1 be looking at the names in the annotations. The  standard mode is to use j%; many functions do this by default. kMany of the operations in the | class take an k: D stored information about the iteration as it progresses. This type I is abstract, as classes that override these operations should just pass  the context on. o@A continuation which takes the remaining index and searches for D that location in a pattern, yielding a name or a remaining index 3 if the end of the pattern was reached too soon. rThe result of an  operation. sWe haven't yet reached the  required index; this is the # index into the remainder of the " pattern (which decreases as we  traverse the pattern). tThe name found at the given  index. uThe result of a  operation. vWe haven't found the name " (yet), but have seen this many  others while looking for it w!The (first) index of the name we  sought x&Type class for embedded terms (either Embed or Shift). z4Construct an embedded term, which is an instance of G  with any number of enclosing E s. That is, embed can have  any of the types   t -> Embed t t -> Shift (Embed t) t -> Shift (Shift (Embed t)) and so on. {Destruct an embedded term. unembed can have any of the types   Embed t -> t Shift (Embed t) -> t and so on. |The Alpha7 type class is for types which may contain names. The  : constraint means that we can only make instances of this C class for types that have generic representations (which can be % automatically derived by RepLib.) Note that the methods of Alpha should almost never be called A directly. Instead, use other methods provided by this module ! which are defined in terms of Alpha methods. @Most of the time, the default definitions of these methods will E suffice, so you can make an instance for your data type by simply  declaring   instance Alpha MyType @Occasionally, however, it may be useful to override the default " implementations of one or more Alpha methods for a particular , type. For example, consider a type like   data Term = ... # | Annotation Stuff Term  where the  Annotation constructor of Term associates some sort B of annotation with a term --- say, information obtained from a A parser about where in an input file the term came from. This D information is needed to produce good error messages, but should < not be taken into consideration when, say, comparing two Terms , for alpha-equivalence. In order to make aeq ignore 7 annotations, you can override the implementation of aeq' like  so:   instance Alpha Term where . aeq' c (Annotation _ t1) t2 = aeq' c t1 t2 . aeq' c t1 (Annotation _ t2) = aeq' c t1 t2 # aeq' c t1 t2 = aeqR1 rep1 t1 t2 Note how the call to * handles all the other cases generically. }See swaps. ~See fv. See lfreshen. See freshen. See aeq. See acompare. #Replace free names by bound names. #Replace bound names by free names. isPat x dynamically checks whether x can be used as a valid * pattern. The default instance returns Just if at all B possible. If successful, returns a list of names bound by the  pattern. isTerm x dynamically checks whether x can be used as a , valid term. The default instance returns True if at all  possible. isEmbed0 is needed internally for the implementation of  isPat. isEmbed is true for terms wrapped in Embed and zero  or more occurrences of Shift. The default implementation  simply returns False.  p n looks up the nth name in the pattern p B (zero-indexed), returning the number of names encountered if not  found. 9Find the (first) index of the name in the pattern if one = exists; otherwise, return the number of names encountered  instead. AFind the (first) index of the name in the pattern, if it exists. <If we see a name, check whether the index is 0: if it is, we've  found the name we'*re looking for, otherwise continue with a  decremented index.  b n looks up up the nth name in the pattern b C (zero-indexed). PRECONDITION: the number of names in the pattern  must be at least n. %Open a term using the given pattern.  openP p1 p2 opens the pattern p2 using the pattern p1. &Close a term using the given pattern.  closeP p1 p2 closes the pattern p2 using the pattern p1. NthCont, forms a monoid: function composition which * short-circuits once a result is found.  FindResult0 forms a monoid which combines information from  several  operations. mappend takes the leftmost  w:, and combines the number of names seen to the left of it 1 so we can correctly compute its global index. lYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ !"#$%&'()*+,-./01234QYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~Q|}~xyz{uwvrtsopqklmnhjiYZ[\]^_`abcdefgCYZ[\]^_`abcdefghjiklmnopqrtsuwvxyz{| }~ !"#$%&'()*+,-./01234GHC only (-XKitchenSink)$Brent Yorgey <byorgey@cis.upenn.edu> Safe-InferedReified class dictionary for . The Subst2 class governs capture-avoiding substitution. To D derive this class, you only need to indicate where the variables 2 are in the data type, by overriding the method . ?This is the only method which normally needs to be implemented ? explicitly. If the argument is a variable, return its name  wrapped in the  constructor. Return 5 for > non-variable arguments. The default implementation always  returns 5. "This is an alternative version to , useable in the case & that the substituted argument doesn't have *exactly* the same type . as the term it should be substituted into. - The default implementation always returns 5.  nm sub tm substitutes sub for nm in tm . It has 0 a default generic implementation in terms of isvar. >Perform several simultaneous substitutions. This method also 4 has a default generic implementation in terms of isvar. See  See . '6789:;<=>?@ABCDEFGHIJK6789:;<=>?@ABCDEFGHIJKGHC only (-XKitchenSink)$Brent Yorgey <byorgey@cis.upenn.edu> Safe-Infered!?A smart constructor for binders, also sometimes referred to as  "close"9. Free variables in the term are taken to be references @ to matching binders in the pattern. (Free variables with no ' matching binders will remain free.) #A destructor for binders that does not guarantee fresh  names for the binders. Bind the pattern in the term "up to permutation" of bound variables. * For example, the following 4 terms are all alpha-equivalent:   permbind [a,b] (a,b)  permbind [a,b] (b,a)  permbind [b,a] (a,b)  permbind [b,a] (b,a) =Note that none of these terms is equivalent to a term with a  redundant pattern such as   permbind [a,b,c] (a,b) For binding constructors which do render these equivalent,  see  and . BBind the list of names in the term up to permutation and dropping  of unused variables. 'For example, the following 5 terms are all alpha-equivalent:   setbind [a,b] (a,b)  setbind [a,b] (b,a)  setbind [b,a] (a,b)  setbind [b,a] (b,a)  setbind [a,b,c] (a,b) There is also a variant, , which ignores name sorts. BBind the list of (any-sorted) names in the term up to permutation * and dropping of unused variables. See . $Constructor for rebinding patterns. ?Destructor for rebinding patterns. It does not need a monadic - context for generating fresh names, since Rebind can only occur  in the pattern of a Q; hence a previous call to  (or D something similar) must have already freshened the names at this  point. $Constructor for recursive patterns. #Destructor for recursive patterns. (Constructor for recursive abstractions. ADestructor for recursive abstractions which picks globally fresh  names for the binders. 2Destructor for recursive abstractions which picks locally fresh  names for binders (see 3). .Determine the alpha-equivalence of two terms. BDetermine (alpha-)equivalence of patterns. Do they bind the same < variables in the same patterns and have alpha-equivalent & annotations in matching positions? <An alpha-respecting total order on terms involving binders. @Calculate the free variables (of any sort) contained in a term. ACalculate the free variables of a particular sort contained in a  term. ACalculate the variables (of any sort) that occur freely in terms A embedded within a pattern (but are not bound by the pattern). BCalculate the variables of a particular sort that occur freely in G terms embedded within a pattern (but are not bound by the pattern). <Calculate the binding variables (of any sort) in a pattern. <Calculate the binding variables (of a particular sort) in a  pattern. Apply a permutation to a term. ;Apply a permutation to the binding variables in a pattern. 5 Embedded terms are left alone by the permutation. @Apply a permutation to the embedded terms in a pattern. Binding , names are left alone by the permutation. "Locally"5 freshen a pattern, replacing all binding names with " new names that are not already "in scope". The second argument E is a continuation, which takes the renamed term and a permutation C that specifies how the pattern has been renamed. The resulting A computation will be run with the in-scope set extended by the  names just generated. /Freshen a pattern by replacing all old binding  s with new  fresh !s, returning a new pattern and a    specifying how s were replaced. Unbind (also known as "open"!) is the simplest destructor for C bindings. It ensures that the names in the binding are globally 4 fresh, using a monad which is an instance of the ; type  class. Unbind two terms with the same fresh names, provided the > binders have the same number of binding variables. If the @ patterns have different numbers of binding variables, return  Nothing2. Otherwise, return the renamed patterns and the  associated terms. ;Unbind three terms with the same fresh names, provided the ? binders have the same number of binding variables. See the  documentation for  for more details. lunbind opens a binding in an 3 monad, ensuring that the $ names chosen for the binders are locally fresh. The components " of the binding are passed to a  continuation, and the resulting E monadic action is run in a context extended to avoid choosing new A names which are the same as the ones chosen for this binding. 4For more information, see the documentation for the 3 type  class. AUnbind two terms with the same locally fresh names, provided the @ patterns have the same number of binding variables. See the  documentation for  and  for more details. ?Unbind three terms with the same locally fresh names, provided C the binders have the same number of binding variables. See the  documentation for  and  for more details. LCompare for alpha-equality. %LM##%LM GHC only (-XKitchenSink)  experimental %Brent Yorgey <byorgey@cis.upenn.edu>  Safe-InferedfNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@A $%&'()*+,./0345678;<=?ACEFGHIKMQTUVWXz{|}~p)*+,$%&'.(QGHz{MKIEF   ;<7?8=3456/C0A|}~TVUWXB      !"#$$%&'()*+,-./01234567789:;<=>>?@ABCDEFGHIJJKKLLMMNOPQRSTUVWXYZZ[\]^_`abcdefghijklmnoopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSRTRURVRWRXRYRZR[R\R]R^R_R`RaRbRcRdReRfRgRhRiRjRkRlRlRmRnRoRpRqRrRsRsRtRuRvRwRwRxRyRzR{R{R|R}R~RRRRRRRRRRRR      !"#$%O&&'()*+,,-./0123344556789:;<:;=:;>:;?@ unbound-0.4 Unbound.PermM Unbound.UtilUnbound.LocallyNameless.NameUnbound.LocallyNameless.FreshUnbound.LocallyNameless.TypesUnbound.LocallyNameless.AlphaUnbound.LocallyNameless.SubstUnbound.LocallyNameless.OpsUnbound.LocallyNamelessPerm permValidapplysingleemptycomposeisidjoinsupportrestrictmkPermMultiset CollectionemptyC singletonunioncmapunionsfromListfilterCdisjointNameBnNmrRrR1AnyNamerNamerName1isBoundisFreerAnyName rAnyName1 name2Integer name2StringanyName2IntegeranyName2String toSortedName integer2Name string2Names2nmakeNamegetR translateLFreshMLFreshMT unLFreshMTLFreshlfreshavoid getAvoidsFreshMFreshMT unFreshMTFreshfresh runFreshMT contFreshMT runFreshM contFreshM runLFreshMT contLFreshMT runLFreshM contLFreshMShiftEmbedTRecRecRebindR SetPlusBindSetBindBindGenBindBrGenBindrEmbedrRebindrRecrShiftAlphaDisPatDisTermDisEmbedDswapsDfvDfreshenD lfreshenDaeqD acompareDcloseDopenDfindpatDnthpatDModePatTermAlphaCtxACmodelevelNthCont runNthCont NthResultCurIndexFound FindResult NamesSeenIndexIsEmbedEmbeddedembedunembedAlphaswaps'fv' lfreshen'freshen'aeq' acompare'closeopenisPatisTermisEmbed nthpatrec findpatrecfindpatnthNamenthpatinitialincrdecrpattermopenTopenPcloseTclosePcloseR1openR1swapsR1fvR1fv1aeqR1aeq1 freshenR1freshenL lfreshenR1 lfreshenL findpatR1findpatLnthpatR1nthpatLcombineisPatR1isTermR1 acompareR1 compareTupMSubstDisvarDsubstDsubstsDSubstisvar isCoerceVarsubstsubsts SubstCoerce SubstName substDefaultsubstR1substsR1bind unsafeUnbind permCloseAnystrength permClosepermbindsetbind setbindAnyrebindunrebindrecunrectrecuntrecluntrecaeq aeqBindersacomparefvAnyfvpatfvAnypatfv bindersAnybindersswaps swapsBinders swapsEmbedslfreshenfreshenunbindunbind2unbind3lunbindlunbind2lunbind3 $fMonoidPerm $fShowPerm$fEqPerm$fCollectionSet$fCollectionMultiset$fCollection[]$fFoldableMultiset RepLib-0.5.2Generics.RepLib.RRep integer-gmpGHC.Integer.TypeIntegerbaseGHC.BaseString$fRepR $fRepName $fShowName $fOrdAnyName $fEqAnyName $fShowAnyName $fRepAnyName$fMonadWriterwLFreshMT$fMonadReaderrLFreshMT$fMonadStatesLFreshMT$fMonadErroreLFreshMT$fMonadContLFreshMT$fMonadTransLFreshMT$fLFreshWriterT$fLFreshWriterT0$fLFreshStateT$fLFreshStateT0$fLFreshReaderT$fLFreshMaybeT $fLFreshListT$fLFreshIdentityT$fLFreshErrorT $fLFreshContT$fLFreshLFreshMT$fMonadWriterwFreshMT$fMonadReaderrFreshMT$fMonadStatesFreshMT$fMonadErroreFreshMT$fMonadContFreshMT$fMonadTransFreshMT$fFreshWriterT$fFreshWriterT0 $fFreshStateT$fFreshStateT0$fFreshReaderT $fFreshMaybeT $fFreshListT$fFreshIdentityT $fFreshErrorT $fFreshContT$fFreshFreshMT $fShowShift $fShowEmbed $fShowTRec $fShowRec $fShowRebind $fShowGenBind $fRepGenBind$fRepRelaxedOrderGenerics.RepLib.R1Rep1$fMonoidNthCont$fMonoidFindResult$fAlphaR $fAlpha(,,,,) $fAlpha(,,,) $fAlpha(,,) $fAlpha(,) $fAlphaEither $fAlphaMaybe $fAlphaChar $fAlphaDouble$fAlphaInteger $fAlphaInt $fAlpha[] $fAlpha() $fAlphaFloat $fAlphaBool$fIsEmbedShift $fAlphaShift$fIsEmbedEmbed $fAlphaEmbed $fAlphaRec $fAlphaRebind$fAlphaGenBind$fAlphaAnyName $fAlphaName $fSatAlphaD Data.MaybeNothing $fSubstcRec $fSubstcEmbed$fSubstcRebind$fSubstcGenBind$fSubstcEither $fSubstcMaybe $fSubstc[]$fSubstc(,,,,) $fSubstc(,,,) $fSubstc(,,) $fSubstc(,) $fSubstbName $fSubstbR$fSubstbAnyName$fSubstbDouble $fSubstbFloat$fSubstbInteger $fSubstbChar $fSubstb() $fSubstbBool $fSubstbInt $fSatSubstD $fEqRebind $fReadGenBindGenerics.RepLib.Libgelemganygallgconcatcompcountflattengorgandgproductcrush rreduceR1 lreduceR1 enumerateR1 generateR1zeroR1gsumR1deepSeqRrnfRrnfdeepSeqsubtreesgsumGSumgsumDGSumDzeroZerozeroDZDZeroD generateD GenerateDgenerateGenerate enumerateD EnumerateD enumerate EnumerateshrinkDShrinkDshrinkShrinkrreduceDRreduceDlreduceDLreduceDrreduceRreducelreduceLreducefoldLeft foldRightFoldGenerics.RepLib.PreludeLib showsPrecR1 maxBoundR1 minBoundR1 compareR1eqR1EqDOrdDBoundedDShowDGenerics.RepLib.SYB.Schemes gfindtype gtypecount gnodecountgcountgdepthglengthgsize synthesize somethinglistify everything everywhereM everywhereBut everywhere' everywhereGenerics.RepLib.SYB.AliasesrecoverQ recoverMpchoiceQchoiceMporElseextRextBextMpextMextQextText0mkRmkMpmkMmkQmkTGenericTGenericQGenericMGenericBGenericRGeneric unGeneric'Generic'unGTGT GenericT'unGQGQ GenericQ'unGMGM GenericM'Generics.RepLib.RepAux fromSpinetoSpinegmapM1gmapQ1gmapT1gmapMgmapQgmapTtoListfromTupMfromTupmapM_lmapQ_lmap_lfoldl_lfoldr_lfindConcompareRgcastgcastRcastcastReqRVal TraversalQueryMapM Traversal1Query1MapM1:::TypedConstr:<>SpineGenerics.RepLib.PreludeRepsrTup7_1rTup7rTup6_1rTup6rTup5_1rTup5rTup4_1rTup4rTup3_1rTup3 rOrdering1 rOrderingrEither1rEitherrMaybe1rMayberBool1rBoolGenerics.RepLib.Derivederive_abstractderiverList1rTup2_1toRgetRepCInt1Char1Integer1Float1Double1 Rational1IOError1IO1Arrow1Data1 Abstract1Equal1R1dictSatrep1rConsEmbrNilEmbrListrPairEmbrTup2rUnitrUnitEmbIntCharFloatDoubleRationalIOErrorIOArrowDataAbstractEqualConfixitynamelabelsfromtoEmbNonfixprecInfixInfixlInfixrFixityDTNil:*:MNil:+:MTupreptype-equality-0.1.0.2Data.Type.EqualityEqTeqT:=:Refl