lw      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                  ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~                                                 portable experimental*Stephanie Weirich <sweirich@cis.upenn.edu> >Compose two permutations. The right-hand permutation will be  applied first. 'isid -- do all keys map to themselves? @Join two permutation. Fail if the two permutations map the same " name to two different variables.     non-portable experimentalsweirich@cis.upenn.edu0  A Class of representatble types A heterogeneous list Cons for a list of types An empty list of types ,Information about a datatype, including its , fully qualified name and representation of  its type arguments. %An embedding between a list of types l and  a datatype a*, based on a particular data constructor. 7 The to function is a wrapper for the constructor, the 3 from function pattern matches on the constructor.  !"#$1Representation of a data constructor includes an : embedding between the datatype and a list of other types < as well as the representation of that list of other types. %&A value of type R a is a representation of a type a. '()*+,-./0123456780  !"#$%&'()*+,-./0123456782&10/.-,+*)('$% !"#  23456780    !"# !"#$%%& 10/.-,+*)(''()*+,-./012345678 non-portable experimentalsweirich@cis.upenn.edu9:;<=>?@ABCDEFGHI'Access a representation, given a proxy J/Transform a parameterized rep to a vanilla rep KL9:;<=>?@ABCDEFGHIJKL=HGFEDCBA@?>;<9:IJKL9::;<<= HGFEDCBA@?>>?@ABCDEFGHIJKL non-portable experimentalsweirich@cis.upenn.edu*Given a type, produce its representation. MFGenerate representations (both basic and parameterized) for a list of  types. N7Generate abstract representations for a list of types. MNMNMN non-portable experimentalsweirich@cis.upenn.eduOPQRSTUVWXYZ[\]^_`OPQRSTUVWXYZ[\]^_``_^]\[ZYXWVUTSRQPOOPQRSTUVWXYZ[\]^_` non-portable experimentalsweirich@cis.upenn.edu)abcdefghiSYB style monadic map type jSYB style query type kA SYB style traversal l0A datastructure to store the results of findCon mn,Determine if two reps are for the same type o1The type-safe cast operation, explicit arguments p1The type-safe cast operation, implicit arguments q9Leibniz equality between types, explicit representations r9Leibniz equality between types, implicit representations sHeterogeneous Ordering t<Given a list of constructor representations for a datatype, 2 determine which constructor formed the datatype. uFA fold right operation for heterogeneous lists, that folds a function G expecting a type type representation across each element of the list. v$A fold left for heterogeneous lists wA map for heterogeneous lists x5Transform a heterogeneous list in to a standard list ymapM for heterogeneous lists z,Generate a heterogeneous list from metadata {8Generate a heterogeneous list from metadata, in a monad |&Generate a normal lists from metadata }4Map a traversal across the kids of a data structure ~$abcdefghijklmnopqrstuvwxyz{|}~$nporqstlmvuwxyz{|kji}~hgfdeacb$acbbcdeefghijklmmnopqrstuvwxyz{|}~ non-portable experimentalsweirich@cis.upenn.edu/!The type constructor for readers !The type constructor for queries )The type constructor for transformations )The type constructor for transformations 'Other first-class polymorphic wrappers Wrapped generic functions;  recall: [Generic c] would be legal but [Generic' c] not. 0The general scheme underlying generic functions 5 assumed by gfoldl; there are isomorphisms such as  GenericT = Generic T. 'Generic readers, say monadic builders,  i.e., produce an "a" with the help of a monad "m". Generic builders  i.e., produce an "a". !Generic monadic transformations,  i.e., take an "a" and compute an "a" Generic queries of type "r",  i.e., take any "a" and return an "r" Generic transformations,  i.e., take an "a" and return an "a" Make a generic transformation; $ start from a type-specific case;  preserve the term otherwise Make a generic query; $ start from a type-specific case;  return a constant otherwise 'Make a generic monadic transformation; $ start from a type-specific case;  resort to return otherwise 5Make a generic monadic transformation for MonadPlus;  use " const mzero"/ (i.e., failure) instead of return as default. Make a generic builder; # start from a type-specific ase; . resort to no build (i.e., mzero) otherwise Flexible type extension 8Extend a generic transformation by a type-specific case /Extend a generic query by a type-specific case @Extend a generic monadic transformation by a type-specific case BExtend a generic MonadPlus transformation by a type-specific case Extend a generic builder Extend a generic reader Left-biased choice on maybies #Choice for monadic transformations Choice for monadic queries ?Recover from the failure of monadic transformation by identity 8Recover from the failure of monadic query by a constant ### non-portable experimentalsweirich@cis.upenn.edu6Apply a transformation everywhere in bottom-up manner 5Apply a transformation everywhere in top-down manner 5Variation on everywhere with an extra stop condition  Monadic variation on everywhere 2Apply a monadic transformation at least somewhere 6 somewhere :: MonadPlus m => GenericM m -> GenericM m 5Summarise all nodes in top-down, left-to-right order 1Get a list of all entities that meet a predicate 3Look up a subterm by means of a maybe-typed filter )Bottom-up synthesis of a data structure; < 1st argument z is the initial element for the synthesis; = 2nd argument o is for reduction of results from subterms; K 3rd argument f updates the synthesised data according to the given term ,Compute size of an arbitrary data structure 9Count the number of immediate subterms of the given term "Determine depth of the given term ;Determine the number of all suitable nodes in a given term 2Determine the number of all nodes in a given term >Determine the number of nodes of a given type in a given term :Find (unambiguously) an immediate subterm of a given type   non-portable experimentalsweirich@cis.upenn.eduA7All of the functions below are defined using instances  of the following class 9A general version of fold left, use for Fold class below :A general version of fold right, use for Fold class below ;Given an element, return smaller elements of the same type G for example, to automatically find small counterexamples when testing 0enumerate the elements of a type, in DFS order. 2Generate elements of a type up to a certain depth  Create a zero element of a type   ' ( zero :: ((Int, Maybe Int), Float))  ((0, Nothing), 0.0)   Add together all of the Ints in a datastructure  For example:  gsum ( 1 , True, (a , Maybe 3, [] ) , Nothing)  4 <Produce all children of a datastructure with the same type. M Note that subtrees is available for all representable types. For those that > are not recursive datatypes, subtrees will always return the A empty list. But, these trivial instances are convenient to have ! for the Shrink operation below. .Recursively force the evaluation of the first  argument. For example,    deepSeq ( x , y ) z where  x = ...  y = ...    will evaluate both x and y then return z 4Force the evaluation of *datatypes* to their normal 3 forms. Other types are left alone and not forced. 3Fold a bindary operation left over a datastructure Multiply all elements together Ensure all booleans are true $Ensure at least one boolean is true Convert to list Count number of as that appear in the argument 4Compose all functions in the datastructure together 4Concatenate all lists in the datastructure together "Ensure property holds of all data &Ensure property holds of some element (Is an element stored in a datastructure <<< 1Polymorphic equality, given an R1 representation $Minimal completion of the Ord class To generate the Bounded class To generate the Bounded class %Minimal completion of the show class      <Generic unifyStep. almost identical to polymorphic equality !                     non-portable experimentalsweirich@cis.upenn.edu  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ non-portable (-XKitchenSink)  experimental +Stephanie Weirich <sweirich@cis.upenn.edu> >Rebinding is for telescopes --- i.e. to support patterns that ' also bind variables that appear later An annotation is a hole in a pattern where variables > can be used, but not bound. For example patterns may include A type annotations, and those annotations can reference variables  without binding them. D Annotations do nothing special when they appear elsewhere in terms 6A name with a hidden (existentially quantified) sort. 9Type of a binding. Morally, the type a should be in the  class Pattern' and the type b should be in the class 1. 7 The Pattern class contains the constructor and a safe  destructor for these types.  We can Bind an a object in a b object if we  can create fresh a objects, and Names can be  swapped in b objects. Often a is Name  but that need not be the case.  4Names are things that get bound. The usual protocol 8 is for names to get created by some automatic process, 5 that preserves alpha renaming under operations over  Binding instances. !"#$%&'()Locally fresh monad  This is the class of D monads that support freshness in an (implicit) local scope. Names D drawn are fresh for this particular scope, but not globally fresh. < This class has a basic instance based on the reader monad. *@pick a new name that is fresh for the current (implicit) scope. +9avoid these names when freshening in the subcomputation. ,A monad m supports the fresh operation if it " can generate a new unique names. -.A monad m* supports the nextInteger operation if it ! can generate new fresh integers /0 1:The Alpha class is for all terms that may contain binders  The 9) class constraint means that we can only 2 make instances of this class for types that have 5 generic representations. (Derive these using TH and  RepLib.) 234 The method swaps' applys a compound permutation. 5+calculate the free variables (aka support) 67Match'- compares two data structures and produces a 9 permutation of their free variables that will make them  alpha-equivalent to eachother. 8An object of type a can be freshened if a new  copy of a% can be produced where all old Names  in a, are replaced with new fresh Names, and the 9 permutation reports which names were swapped by others. 9See S :Many of the operations in the 1 class take an :: 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.     Get the integer index of an . Get the string part of an . ;<=>?@ABCDEFGGet the string part of a  . HIDetermine the sort of a  . JSmart constructor for binders K7A destructor for binders that does not guarantee fresh  names for the binders. L$Constructor for binding in patterns MHdestructor for binding patterns, the external names should have already  been freshen'4ed. We swap the internal names so that they use the  external names NO)calculate the free variables of the term P(List the binding variables in a pattern Q@Set of variables that occur freely in annotations (not binding) R The method swaps, applys a permutation to all free variables  in the term. ;Apply a permutation to the binding variables in a pattern. 0 Annotations are left alone by the permutation. =Apply a permutation to the annotations in a pattern. Binding * names are left alone by the permutation. SLocally freshen an object TAn object of type b can be freshened if a new  copy of b/ can be produced where all old *binding* Names  in b, are replaced with new fresh Names, and the 9 permutation reports which Names were swapped by others. >Match compares two data structures and produces a permutation 8 of their Names that will make them alpha-equivalent to C eachother. (Names that appear in annotations must match exactly.) > Also note that two terms are alpha-equivalent when the empty  permutation is returned. ACompare two patterns, ignoring the names of binders, and produce B a permutation of their annotations to make them alpha-equivalent  to eachother. Return " if no such renaming is possible. ?Compare two patterns for equality and produce a permutation of  their binding Names- to make them alpha-equivalent to each other  ( 9s that appear in annotations must match exactly). Return  " if no such renaming is possible.  !"#$U%&'()V7Unbind is the destructor of a binding. It ensures that ' the names in the binding b are fresh. W>Destruct two bindings simultanously, if they match, using the  same list of fresh names XY(Destruct a binding in the LFresh monad. Z[*@Capture-avoiding substitution, in a monad so that we can rename 2 variables at binding locations and avoid capture +,-.1Reader monad instance for local freshness class. /01234567@ !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[@ FHEGI;<=>?@ABCD123456789RPQONJK,-TVWX./0)*+SYZ[LM%&'(:U#$!"@ !"#$%&'(&'()*+*+,--./0/012345678923456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[ non-portable (-XKitchenSink)  experimental +Stephanie Weirich <sweirich@cis.upenn.edu> \\ supports " telescopes" --- that is, patterns where 0 bound variables appear in multiple subterms. 8]An annotation is a "hole"% in a pattern where variables can be ? used, but not bound. For example, patterns may include type > annotations, and those annotations can reference variables C without binding them. Annotations do nothing special when they  appear elsewhere in terms. ^9:_The type of a binding. We can _ an a object in a b  object if we can create "fresh" a objects, and a objects  can occur unbound in b objects. Often a is b but that  need not be the case. Like b, _+ is also abstract. You can create bindings  using  and take them apart with  and friends. ;`6A name with a hidden (existentially quantified) sort. abb9s are things that get bound. This type is intentionally  abstract; to create a b you can use  or  ". The type parameter is a tag, or sort, which tells B us what sorts of things this name may stand for. The sort must  be an instance of the   type class. <=>?c@dAeBfCDEFGHReified class dictionary for g. IJKLgThe g2 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 h. h>If the argument is a variable, return its name and a function + to generate a substituted term. Return  for  non-variable arguments. ii nm sub tm substitutes sub for nm in tm. j,Perform several simultaneous substitutions. k9This is the class of monads that support freshness in an D (implicit) local scope. Generated names are fresh for the current > local scope, but not globally fresh. This class has a basic % instance based on the reader monad. l@Pick a new name that is fresh for the current (implicit) scope. m=Avoid the given names when freshening in the subcomputation. n=Type class for monads which can generate new globally unique  bs based on a given b. op>Type class for contexts which can generate new globally fresh  integers. qGet a new, globally fresh /M. r,Reset the internal state, i.e. forget about Integers that  have already been generated. N=Class constraint hackery to allow us to override the default % definitions for certain classes. ON is essentially a  reified dictionary for the t class. OPQRSTUVWXY>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 Z; the function , ,  ,  and  do this by default. [ZsMatch returns a permutation ordering. Either the terms are known G to be LT or GT, or there is some permutation that can make them equal  to eachother 1 data POrdering = PLT | PEq (Perm AnyName) | PGT Many of the operations in the t class take an s: 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. \]^tThe t7 type class is for types which may contain names. The  9: 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 t" should never be called directly! @ Instead, use other methods provided by this module which are  defined in terms of t$ methods. (The only reason they are A exported is to make them available to automatically-generated  code.) @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 uSee . vSee . wSee . xSee . yz#Replace free names by bound names. {#Replace bound names by free names. || b n looks up the nth name in the pattern b B (zero-indexed), returning the number of names encountered if not  found. }@Find the (first) index of the name in the pattern if it exists;  if not found (_ = `), return the number of names  encountered instead. ab~cGet the integer index of a b. Get the string part of a b. Get the integer index of an a`. Get the string part of an a`. d Create a b from an /M.  Create a b from a e.  Create a b from a String and an Integer index. fDetermine the sort of a b. ghijklmnopqrstuvwx9A smart constructor for binders, also sometimes known as  "close". #A destructor for binders that does not guarantee fresh  names for the binders. %Constructor for binding in patterns. ?destructor for binding patterns, the names should have already  been freshened. Determine alpha-equivalence. *Determine (alpha-)equivalence of patterns GCalculate the free variables of a particular sort contained in a term. DList all the binding variables (of a particular sort) in a pattern. 9List variables of a particular sort that occur freely in  annotations (not bindings). Apply a permutation to a term. <Apply a permutation to the binding variables in a pattern. 0 Annotations are left alone by the permutation. =Apply a permutation to the annotations in a pattern. Binding * names are left alone by the permutation. "Locally"B freshen a term. TODO: explain this type signature a bit better. $Freshen a term by replacing all old binding b s with new  fresh bs, returning a new term and a  b  specifying how bs were replaced. ?Compare two data structures and produce a permutation of their  b6s that will make them alpha-equivalent to each other (bs 9 that appear in annotations must match exactly). Return  ; if no such renaming is possible. Note that two terms are 8 alpha-equivalent if the empty permutation is returned. ACompare two patterns, ignoring the names of binders, and produce C a permutation of their annotations to make them alpha-equivalent  to eachother. Return " if no such renaming is possible. ?Compare two patterns for equality and produce a permutation of  their binding Names- to make them alpha-equivalent to each other  (b9s that appear in annotations must match exactly). Return  $ if no such renaming is possible. yy 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. zAFind the (first) index of the name in the pattern, if it exists. Unbind (also known as "open") is the destructor for ? bindings. It ensures that the names in the binding are fresh. 9Unbind two terms with the same fresh names, provided the  binders match. Destruct a binding in an k monad. 9Unbind two terms with the same fresh names, provided the  binders match. ;Unbind three terms with the same fresh names, provided the  binders match. {|}~A monad instance for k which renames to the lowest " number not currently being used !Simple reader monad instance for k. A monad m supports the o operation if it " can generate a new unique names. Compare for alpha-equality. The  instance for _ compares bindings for  alpha-equality. S\]^_`abcdefghijklmnopqrstuvwxyz{|}~Sb`a_]^\~tuvwxyz{|}nopqrklmghijsefcdK\]^^_`aabcdefghijhijklmlmnoopqrqrst uvwxyz{|}uvwxyz{|}~  !!"#$%&'(()*+,-../0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuuvwxyz{|}~                                                                ! " #  $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y     Z Z   ! " #  $  [ ' ( ) * + , - . 8 / 2 3 7 6 5 \ ] ^ _ 9 : ; < = > ? @ A B C E ` a D F G S b c d e f g h i H I J K L j M N O P k l Q R m n o T U V W X Ypqrstuv"wxyz{|}~//                    / Z Z       w                        ` a    k l m n o                   [         q r   /          w          8                                                        q r   RepLib-0.3Generics.RepLib.Bind.PermMGenerics.RepLib.RGenerics.RepLib.R1Generics.RepLib.DeriveGenerics.RepLib.PreludeRepsGenerics.RepLib.RepAuxGenerics.RepLib.SYB.AliasesGenerics.RepLib.SYB.SchemesGenerics.RepLib.LibGenerics.RepLib.PreludeLibGenerics.RepLib.UnifyGenerics.RepLib.Bind.Nominal$Generics.RepLib.Bind.LocallyNamelessGenerics.RepLibPermapplysingleempty<>isidjoinsupportrestrictReprepMTupMEx:+:MNilEx:*:NilDTFixityInfixrInfixlInfixprecNonfixEmbtofromlabelsnamefixityConRAbstractDataArrowIOIOErrorRationalDoubleFloatIntegerCharIntrUnitEmbrUnitrTup2rPairEmbrListrNilEmbrConsEmbRep1rep1SatdictR1 Abstract1Data1Arrow1IO1IOError1 Rational1Double1Float1Integer1Char1Int1getRepCtoRrTup2_1rList1derivederive_abstractrTup7rTup7_1rTup6rTup6_1rTup5rTup5_1rTup4rTup4_1rTup3rTup3_1 rOrdering rOrdering1rEitherrEither1rMayberMaybe1rBoolrBool1Spine:<>ConstrTyped:::MapM1Query1 Traversal1MapMQuery TraversalValeqRcastRcastgcastRgcastcompareRfindConfoldr_lfoldl_lmap_lmapQ_lmapM_lfromTupfromTupMtoListgmapTgmapQgmapMgmapT1gmapQ1gmapM1toSpine fromSpine GenericM'GMunGM GenericQ'GQunGQ GenericT'GTunGTGeneric' unGeneric'GenericGenericRGenericBGenericMGenericQGenericTmkTmkQmkMmkMpmkRext0extTextQextMextMpextBextRorElsechoiceMpchoiceQ recoverMprecoverQ everywhere everywhere' everywhereBut everywhereM everythinglistify something synthesizegsizeglengthgdepthgcount gnodecount gtypecount gfindtypeFold foldRightfoldLeftLreducelreduceRreducerreduceLreduceDlreduceDRreduceDrreduceDShrinkshrinkShrinkDshrinkD Enumerate enumerate EnumerateD enumerateDGenerategenerate GenerateD generateDZeroDZDzeroDZerozeroGSumDgsumDGSumgsumsubtreesdeepSeqrnfrnfRdeepSeqRgsumR1zeroR1 generateR1 enumerateR1 lreduceR1 rreduceR1crushgproductgandgorflattencountcompgconcatgallganygelemShowDBoundedDOrdDEqDeqR1 compareR1 minBoundR1 maxBoundR1 showsPrecR1Occurs occursCheckSubstsubstHasVaris_varvarUnify unifyStepUnificationStateUState uConstraintsuSubst UConstraintUC UnifySubD unifyStepDsubstD occursCheckDUM UnifyErrorProxy unifyStepR1addConstraintsRL1dequeueConstraintqueueConstraintextendSubstitutionsolveUnificationsolveUnification'substR1 occursCheckR1RebindAnnotBindNamerRebindrAnnotrNamerBindisvarlsubstlsubstsLFreshlfreshavoidFreshfreshHasNext nextInteger resetNextAlphaaeq'swapall'swaps'fv'binders'match'freshen' lfreshen'AlphaCtxname1name2name3name4name5name6name7name8name9name10 name2Integer integer2Name name2String string2NamemakeNamebind unsafeUnBindrebindreopenaeqfvbinderspatfvswapslfreshenfreshenmatchR1unbindunbind2unbind3lunbindlunbind2lunbind3AnyNamesubstscloseopen nthpatrec findpatrecanyName2IntegeranyName2String abs_swapsabs_fv abs_freshen abs_match abs_nthpatrecabs_findpatrec abs_closeabs_open aeqBinders swapsBinders swapsAnnotsmatch matchAnnots matchBindersseteqassertdo_testsFlagConcAbsreptyrName1repconrfromrtorembrepDTreprreprs ctx_params lookupNamerepcon1repr1repr1s stringNametypeInfo simpleName tyVarBndrNameeqDTeqRTup compareMTuptoSpineR toSpineRlunRQunQMunMTunT deepSeq_lgenEnum enumerateCons showsPrecD minBoundD maxBoundDcompareDeqDeqRL1lexord compareTup getFixity unifyStepEqBNmrRrR1rRebind1rAnnot1rBind1ExpLAVSubstDsubstsDAlphaDaeqDswapallDswapsDfvDbindersDmatchDfreshenD lfreshenDPatTermrAnyName rAnyName1 toSortedNamename11getRbase Data.MaybeNothinginitialpattermmodeaeqR1aeq1swapsR1 swapallR1fvR1fv1 bindersR1binders1match1 freshenR1freshenL lfreshenR1 lfreshenLsubstsR1$fLFreshReaderTrExprExp1nameAnameBnameCemptyNEmkbigSBindSBBnisvarD integer-gmpGHC.Integer.TypecloseDopenDfindpatDnthpatDModeAClevelghc-primGHC.BoolBoolFalseGHC.BaseStringincrcloseR1openR1 findpatR1findpatLnthpatR1nthpatLnthpatfindpat substDefault$fLFreshReaderT0$fFreshm $fEqRebind $fReadBind GHC.ClassesEq