!?-      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ :(c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone%hobbits The type Closed a" represents a closed term of type a, i.e., an expression of type aj with no free (Haskell) variables. Since this cannot be checked directly in the Haskell type system, the Closedd data type is hidden, and the user can only create closed terms using Template Haskell, through the  operator. hobbitsExtract the value of a  objecthobbitsExtract the type of an Info objecthobbitsmkClosedJ is used with Template Haskell quotations to create closed terms of type O. A quoted expression is closed if all of the names occuring in it are either:L1) bound globally or 2) bound within the quotation or 3) also of type .NoneSXb:(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone (c) 2016 Edwin WestbrookBSD3westbrook@galois.com experimentalGHCSafe &'-.HSUVX>yhobbitsA type-class which ensures that ctx is a valid context, i.e., has | the form (RNil :> t1 :> ... :> tn) for some types t1 through tnhobbits{Heterogeneous type application, including a proof that the input kind of the function equals the kind of the type argumenthobbitsAn  RAssign f r an assignment of an f a for each a in the  r hobbitsAn Append ctx1 ctx2 ctx is a "proof" that  ctx = ctx1  ctx2.hobbitsA  Member ctx a is a "proof" that the type a is in the type list ctx, meaning that ctx equals # t0 ':>' a ':>' t1 ':>' ... ':>' tnfor some types  t0,t1,...,tn.hobbits Append two s at the type levelhobbitsIA form of lists where elements are added to the right instead of the lefthobbits Weaken a L proof by prepending another context to the context it proves membership inhobbitsMake an   proof from any / vector for the second argument of the append.hobbits A version of  that takes in a  argument.hobbitsThe inverse of , that builds an  from an  hobbitsCreate an empty  vector.hobbitsCreate a singleton  vector.hobbitsLook up an element of an  vector using a  proofhobbitsLook up an element of an  vector using a K proof at what GHC thinks might be a different kind, i.e., heterogeneouslyhobbitsModify an element of an  vector using a  proof.hobbitsSet an element of an  vector using a  proof.hobbitsTest if an object is in an , returning a  proof if it is hobbits%Map a function on all elements of an  vector.!hobbitsAn alternate name for  % that does not clash with the prelude"hobbits6Map a binary function on all pairs of elements of two  vectors.#hobbitsTake the tail of an $hobbitsConvert a monomorphic  to a list%hobbits6Map a function with monomorphic output type across an  to create a standard list: )mapToList f = toList . map (Constant . f)&hobbits Append two  vectors.'hobbitsPerform a right fold across an (hobbits Split an o vector into two pieces. The first argument is a phantom argument that gives the form of the first list piece.)hobbits,Create a vector of proofs that each type in c is a  of c.&  !"#$%&'()&   !"#$%&'()5:(c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3westbrook@kestrel.edu experimentalGHCNone &'-.2=?HSUVXMDhobbits1A name refresher gives new fresh indices to names/hobbitsA Name a. is a bound name that is associated with type a.0hobbits cmpName n m compares names n and m of types Name a and Name b', respectively. When they are equal, Some e is returned for e a proof of type a :~: b( that their types are equal. Otherwise, None is returned. For example: nu $ \n -> nu $ \m -> cmpName n n == nu $ \n -> nu $ \m -> Some Refl nu $ \n -> nu $ \m -> cmpName n m == nu $ \n -> nu $ \m -> None1hobbitsCHeterogeneous comparison of names, that could be at different kindshobbitsApply a  to a /hobbitsBuild a + that maps one sequence of names to anotherhobbits Extend a  with one more name mapping  / 01  :(c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3westbrook@kestrel.edu experimentalGHCNone %&'-.2HSXe2hobbitsdThis type states that it is possible to replace free names with fresh names in an object of type a.. This type essentially just captures a representation of the type a as either a Name type, a multi-binding, a function type, or a (G)ADT. In order to be sure that only the "right" proofs are used for (G)ADTs, however, this type is hidden from the user, and can only be constructed with  mkNuMatching.3hobbitsAn Mb ctx b; is a multi-binding that binds one name for each type in ctx, where ctx has the form   t1  ...  tnh. Internally, multi-bindings are represented either as "fresh functions", which are functions that quantify over all fresh names that have not been used before and map them to the body of the binding, or as "fresh pairs", which are pairs of a list of names that are guaranteed to be fresh along with a body. Note that fresh pairs must come with an 2a for the body type, to ensure that the names given in the pair can be relaced by fresher names.hobbits The call mapNamesPf data ns ns' a. replaces each occurrence of a free name in a which is listed in ns' by the corresponding name listed in ns'j. This is similar to the name-swapping of Nominal Logic, except that the swapping does not go both ways.hobbits3Ensures a multi-binding is in "fresh function" formhobbits/Ensures a multi-binding is in "fresh pair" form 23:(c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3westbrook@kestrel.edu experimentalGHCNone%&'-.=>?@AHSUVX34hobbitsTypeclass for lifting the 6d constraint to functors on arbitrary kinds that do not require any constraints on their input types6hobbitsInstances of the 6 aI class allow pattern-matching on multi-bindings whose bodies have type a$, i.e., on multi-bindings of type 3 ctx aD. The structure of this class is mostly hidden from the user; see :) to see how to create instances of the  NuMatching class.hobbits Just like $, except uses the NuMatching class. 8hobbits Build an 2 for type a= by using an isomorphism with an already-representable type b. This is useful for building 6 instances for, e.g.,  types, by mapping to and from B, without having to define instances for each one in this module.9hobbits Builds an 2 proof for use in a 6 instance. This proof is unsafe because it does no renaming of fresh names, so should only be used for types that are guaranteed not to contain any / or 3 values.:hobbitsTemplate Haskell function for creating NuMatching instances for (G)ADTs. Typical usage is to include the following line in the source file for (G)ADT T+ (here assumed to have two type arguments): )$(mkNuMatching [t| forall a b . T a b |])The :5 call here will create an instance declaration for 6 (T a b)_. It is also possible to include a context in the forall type; for example, if we define the ID data type as follows: data ID a = ID athen we can create a 6 instance for it like this: ,$( mkNuMatching [t| NuMatching a => ID a |])INote that, when a context is included, the Haskell parser will add the forall a for you.2456789:67:28945:(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone->Hp hobbitsA WrapKite specifies a transformation to be applied to variables | in a Template Haskell patterns, as follows:_varView gives an expression for a function to be applied, as a view pattern, to variables before matching them, including to variables bound by @ patterns;_asXform^ gives a function to transform the bodies of @ patterns, i.e., this function is applied to p in pattern x@p; _topXform; gives a function to transform the whole pattern after _varView and/or _asXform? have been applied to sub-patterns; as the first argument,  _topXform` also takes a flag indicating whether any transformations have been applied to sub-patterns. hobbits<Helper function to apply an expression to multiple arguments!hobbits8Helper function to apply the (.) operator on expressions"hobbits patQQ str pat builds a quasi-quoter named str that parses | patterns with pat#hobbits9Combine two WrapKits, composing the individual components$hobbitsApply a  to a pattern%hobbits%Parse a pattern from a string, using &hobbitsJA helper function used to ensure two multi-bindings have the same contexts'hobbits Builds a & for parsing patterns that match over 3(. | Takes two fresh names as arguments.Vhobbits*Quasi-quoter for patterns that match over 3(hobbits Builds a & for parsing patterns that match over Whobbits*Quasi-quoter for patterns that match over , built using (Xhobbits*Quasi-quoter for patterns that match over  (3 ctx a)VWXVWX:(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone %&'-.=?HSUVXYhobbitsA Binding. is simply a multi-binding that binds one nameZhobbitsnu f, creates a binding which binds a fresh name n# and whose body is the result of f n.[hobbitsThe expression  nuMulti p fU creates a multi-binding of zero or more names, one for each element of the vector p,. The bound names are passed the names to f?, which returns the body of the multi-binding. The argument p , of type  f ctxB, acts as a "phantom" argument, used to reify the list of types ctxD at the term level; thus it is unimportant what the type function f is.\hobbits  nus = nuMulti]hobbits<Extend the context of a name-binding by adding a single type^hobbits8Extend the context of a name-binding with multiple types_hobbits8Checks if a name is bound in a multi-binding, returning Left mem! when the name is bound, where memc is a proof that the type of the name is in the type list for the multi-binding, and returning Right n# when the name is not bound, where n is the name. For example: nu $ \n -> mbNameBoundP (nu $ \m -> m) == nu $ \n -> Left Member_Base nu $ \n -> mbNameBoundP (nu $ \m -> n) == nu $ \n -> Right n`hobbitscCompares two names inside bindings, taking alpha-equivalence into account; i.e., if both are the ith name, or both are the same name not bound in their respective multi-bindings, then they compare as equal. The return values are the same as for 0 , so that  Some Refl* is returned when the names are equal and Nothing! is returned when they are not.ahobbits,Creates an empty binding that binds 0 names.bhobbits=Eliminates an empty binding, returning its body. Note that  elimEmptyMb is the inverse of emptyMb.chobbits@Combines a binding inside another binding into a single binding.dhobbitsLSeparates a binding into two nested bindings. The first argument, of type  any c28, is a "phantom" argument to indicate how the context c should be split.ehobbits<Returns a proxy object that enumerates all the types in ctx.fhobbitsdTake a multi-binding inside another multi-binding and move the outer binding inside the ineer one.ghobbits"Put a value inside a multi-bindinghhobbitsxApplies a function in a multi-binding to an argument in a multi-binding that binds the same number and types of names.ihobbits#Lift a binary function function to 3sjhobbitsasdfasdfThe expression nuWithElimMulti args f takes a sequence argsp of one or more multi-bindings (it is a runtime error to pass an empty sequence of arguments), each of type  Mb ctx ai for the same type context ctx" of bound names, and a function f and does the following:)Creates a multi-binding that binds names  n1,...,nn , one name for each type in ctx;Substitutes the names  n1,...,nn1 for the names bound by each argument in the args& sequence, yielding the bodies of the args (using the new name n ); and thenPasses the sequence  n1,...,nn0 along with the result of substituting into args to the function fA, which then returns the value for the newly created binding.3For example, here is an alternate way to implement h: mbApply' :: Mb ctx (a -> b) -> Mb ctx a -> Mb ctx b mbApply' f a = nuWithElimMulti ('MNil' :>: f :>: a) (\_ ('MNil' :>: 'Identity' f' :>: 'Identity' a') -> f' a')khobbits Similar to jT but binds only one name. Note that the argument list here is allowed to be empty.lhobbits Similar to j but takes only one argumentmhobbits Similar to j8 but takes only one argument that binds a single name./013YZ[\]^_`abcdefghijklm/Y3Z[\a]^01_`bcdefghijklm(c) 2020 Edwin WestbrookBSD3westbrook@galois.com experimentalGHCNone%&'-.HSUVXG(c) 2019 Edwin WestbrookBSD3westbrook@galois.com experimentalGHCNone%&'-.HSUVXwhobbits A pair of a / of some type a along with an element of type f ayhobbitsA heterogeneous map from /s of arbitrary type a to elements of f a)hobbitsAn element of a y, where the name type a is existentially quantified*hobbits Coerce an ) f to an f a for a specific type aY. This assumes we know that this is the proper type to coerce it to, i.e., it is unsafe.+hobbits>Internal-only helper function for mapping a unary function on ,s to a y-hobbits?Internal-only helper function for mapping a binary function on ,s to yszhobbits The empty y{hobbitsThe singleton y with precisely one / and corresponding value|hobbitsBuild a y5 from a list of pairs of names and values they map to}hobbits Insert a / and a value it maps to into a y~hobbits Delete a /! and the value it maps to from a yhobbits-Apply a function to the value mapped to by a /hobbits Update the value mapped to by a /, possibly deleting ithobbits9Apply a function to the optional value associated with a / , where . represents the / not being present in the yhobbits$Look up the value associated with a / , returning . if there is nonehobbits Synonym for ! with the argument order reversedhobbits Test if a / has a value in a yhobbits Test if a y is emptyhobbitsReturn the number of /s in a yhobbits Union two yshobbits!Remove all bindings in the first y for /s in the secondhobbitsInfix synonym for hobbitsIntersect two yshobbits6Map a function across the values associated with each /hobbits,Perform a right fold across all values in a yhobbits+Perform a left fold across all values in a yhobbits Return all /s in a y with their associated valueshobbitsLift a y\ out of a name-binding using a "partial lifting function" that can lift some values in the y$ out of the binding. The resulting y contains those names and associated values where the names were not bound by the name-binding and the partial lifting function was able to lift their associated values.wxyz{|}~ywxz{|}~:(c) 2014 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone%&'-HE /hobbitsType functors f where f a is always  for any a0hobbits Object-level reification of the  typeclasshobbits%Typeclass for inherently closed typeshobbits noClosedNamesJ encodes the hobbits guarantee that no name can escape its multi-binding.hobbits2Closed terms are closed (sorry) under application.hobbits8Closed multi-bindings are also closed under application.hobbitsNWhen applying a closed function, the argument can be viewed as locally closed1hobbits$FIXME: this should not be possible!!hobbitsvMark an object as closed without actually traversing it. This is unsafe if the object does in fact contain any names.2hobbits-Helper function to use the proof returned by 3   (c) 2014 Edwin WestbrookBSD3 emw4@rice.edu experimentalGHCNone%&'-.=?HUV ohobbits The class  Liftable aE gives a "lifting function" for a, which can take any data of type a out of a multi-binding of type 3 ctx a.hobbits9Lift a list (but not its elements) out of a multi-binding (c) 2020 Edwin WestbrookBSD3westbrook@galois.com experimentalGHCNone%&'-.HSUVXhobbitsA / of some unknown type of kind khobbits A set of /s whose types all have kind khobbits The empty hobbitsThe singleton hobbitsConvert a list of names to a hobbits Convert a  to a listhobbitsInsert a name into a hobbitsDelete a name from a hobbitsTest if a name is in a hobbits Test if a  is emptyhobbitsCompute the cardinality of a hobbitsTake the union of two shobbitsTake the union of a list of shobbits*Take the set of all elements of the first  not in the secondhobbitsAnother name for hobbitsTake the intersection of two shobbits(Map a function across all elements of a hobbits<Perform a right fold of a function across all elements of a hobbits;Perform a left fold of a function across all elements of a hobbitsLift a ^ out of a name-binding by lifting all names not bound by the name-binding and then forming a  from those lifted names (c) 2020 Edwin WestbrookBSD3westbrook@galois.com experimentalGHCNone %-.HUV"4hobbits A monad whose effects are closed5hobbits.State types that can incorporate name-bindingshobbits A version of  that does not require a 6@ instance on the element type of the multi-binding in the monadhobbits The class of name-binding monads6hobbitshBind a name inside a computation and return the name-binding whose body was returned by the computation:(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNoneUV$|R789:;<=>?@ABCDEFGHI /0123456789:VWXYZ[\]^_`abcdefghijklm   :(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone %&'.HSX' :(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone*:(c) 2011 Edwin Westbrook, Nicolas Frisby, and Paul BraunerBSD3 emw4@rice.edu experimentalGHCNone %&'.HUV-YJhobbits Create a  object for the type list of a  vector.K !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~,-3:     , - 7 3 :                         !"#$%&'()*+,-./0123 4 5 6789:;;<=<><?<@<A<B<C<D<E<F<G<H<I<JKL"hobbits-1.3-B2K3O41sFpxICZDvSgiyV2Data.Binding.Hobbits.Closed"Data.Binding.Hobbits.PatternParserData.Type.RListData.Binding.Hobbits.MbData.Binding.Hobbits.NuMatchingData.Binding.Hobbits.QQ(Data.Binding.Hobbits.NuMatchingInstancesData.Binding.Hobbits.NameMapData.Binding.Hobbits.LiftableData.Binding.Hobbits.NameSetData.Binding.Hobbits.MonadBind1Data.Binding.Hobbits.Examples.LambdaLifting.Terms4Data.Binding.Hobbits.Examples.LambdaLifting.Examples+Data.Binding.Hobbits.Examples.LambdaLifting$Data.Binding.Hobbits.Internal.Closed'Data.Binding.Hobbits.Internal.Utilities"Data.Binding.Hobbits.Internal.Name Data.Binding.Hobbits.Internal.MbData.Binding.HobbitsClosedunClosedmkClosed parsePatternTypeCtxtypeCtxProxiesHApplyRAssignMNil:>:Append Append_Base Append_StepMember Member_Base Member_Step:++:RListRNil:> weakenMemberLmkAppend mkMonoAppendproxiesFromAppendempty singletongethgetmodifyset memberElemmap mapRAssignmap2tailtoList mapToListappendfoldrsplitmembers $fEqMember$fTestEqualitykMember $fShowMember $fTypeCtxk:>$fTypeCtxkRNilNamecmpNamehcmpName MbTypeReprMbNuMatchingAny1nuMatchingAny1Proof NuMatchingnuMatchingProof isoMbTypeReprunsafeMbTypeRepr mkNuMatching$fNuMatchingVector$fNuMatching[]$fNuMatching(,,,)$fNuMatching(,,)$fNuMatching(,)$fNuMatching()$fNuMatchingWord64$fNuMatchingWord32$fNuMatchingWord16$fNuMatchingWord8$fNuMatchingWord$fNuMatchingDouble$fNuMatchingFloat$fNuMatchingNatural$fNuMatchingChar$fNuMatchingInteger$fNuMatchingInt$fNuMatchingBool$fNuMatchingMb$fNuMatching->$fNuMatchingClosed$fNuMatchingName$fNuMatchingRAssign$fNuMatchingAny1kConstant$fNuMatchingAny1k:~:$fNuMatchingAny1kName $fNuMatchingfnuPclPclNuPBindingnunuMultinusextMb extMbMulti mbNameBoundP mbCmpNameemptyMb elimEmptyMb mbCombine mbSeparate mbToProxymbSwapmbPurembApplymbMap2nuMultiWithElim nuWithElimnuMultiWithElim1 nuWithElim1$fApplicativeMb $fFunctorMb$fShowMb$fNuMatchingMaybe$fNuMatchingEither$fNuMatchingMember$fNuMatchingProxy$fNuMatching:~:$fNuMatchingConstant NameAndElemNameMapfromListinsertdeleteadjustupdatealterlookup!membernullsizeunion difference\\ intersectionfoldlassocs liftNameMap$fNuMatchingNameAndElemClosabletoClosed noClosedNamesclApply clMbApply clApplyCl unsafeClose $fClosable[] $fClosableInt$fClosableChar$fClosableBool$fClosableClosed$fClosableProxy$fClosableMember$fClosableInteger$fClosableRAssign$fClosableAny1kMember$fClosableAny1kProxyLiftablembLiftmbList$fNuMatchingRatio$fEqMb$fLiftableProxy $fLiftable:~:$fLiftableEither$fLiftableMaybe$fLiftableBool $fLiftable(,) $fLiftable() $fLiftable[]$fLiftableRatio$fLiftableMember$fLiftableNatural$fLiftableClosed$fLiftableInteger $fLiftableInt$fLiftableCharSomeNameNameSetunions liftNameSet$fNuMatchingSomeNameMonadStrongBind strongMbM MonadBindmbM$fMonadBindReaderT$fMonadBindMaybe$fMonadBindIdentity$fMonadStrongBindReaderT$fMonadStrongBindIdentity$fMonadStrongBindStateT$fMonadBindStateT$fBindStateClosed$fMonadClosedStateT$fMonadClosedIdentityTermVarLamAppDLDecls Decls_Base Decls_ConsDeclDecl_One Decl_ConsDTermTVarTDVarTApplam $fShowTerm$fNuMatchingTerm$fNuMatchingDTerm$fNuMatchingDecl $fShowDecls $fShowDTerm$fNuMatchingDeclsex1ex2ex3ex4ex5ex6ex7exP lambdaLift mbLambdaLift reifyNameTypeeverywhereButMbase Data.ProxyProxy NameRefresher refreshName mkRefresher extRefresherExProxyExMemberunNameRefresherMkName memberFromLen unsafeLookupC proxyFromLencounter fresh_name mapNamesPfensureFreshFunensureFreshPairMbTypeReprDataMkMbTypeReprData MbTypeReprFun MbTypeReprMbMbTypeReprNameMkMbPairMkMbFunmapNamesGHC.RealIntegral integer-gmpGHC.Integer.TypeIntegerWrapKit appEMulticomposepatQQcombineWrapKitswrapVars parseHeresame_ctxnuKitclKitNMElem coerceNMElemmapNMap1containers-0.6.0.1Data.IntMap.InternalIntMapmapNMap2 GHC.MaybeNothing ClosableAny1 IsClosablecloseBug toClosedAny1 closableAny1 MonadClosed BindStatenuMghc-prim GHC.Types~~ asProxyTypeOfKProxyData.Type.Equalityouterinnerapply gcastWithcastWithtranssym:~:Refl:~~:HRefl TestEquality testEquality==proxyOfRAssign