!^,      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_` 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 { | } ~        !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ utilities for working with Data.Functor.Compose(c) Galois, Inc 2014-2019&Langston Barrett <langston@galois.com>Safe &'-HSUVX+fparameterized-utils)The deduction (via generativity) that if  g x :~: g y then x :~: y.See  5https://gitlab.haskell.org/ghc/ghc/merge_requests/273.&Classes for working with type of kind k -> *(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com>Safe&'-8>@AHSUVXkeparameterized-utils&This class is parameterized by a kind k. (typically a data kind), a type constructor f of kind k -> *2 (typically a GADT of singleton types indexed by k), and an index parameter ctx of kind k.parameterized-utilsCaptures the value obtained from applying a type to a function so that we can use parameterized class instance to provide unparameterized instances for specific types.This is the same as Ap from Control.Applicative?, but we introduce our own new type to avoid orphan instances.parameterized-utils7A parameterized type that is hashable on all instances.parameterized-utilsHash with default salt.parameterized-utils)Parameterized generalization of the lens At class.parameterized-utilsGiven an index into a container, build a lens that points into the given position in the container, whether or not it currently exists. Setting values of atF to a Just= value will insert the value if it does not already exist.parameterized-utils)Parameterized generalization of the lens IxedF class, but with the guarantee that indexes exist in the container.parameterized-utilseGiven an index into a container, build a lens that points into the given element in the container.parameterized-utils)Parameterized generalization of the lens Ixed class.parameterized-utilssGiven an index into a container, build a traversal that visits the given element in the container, if it exists. parameterized-utils8A parameterized type that can be shown on all instances. To implement   g#, one should implement an instance  (g tp) for all argument types tp , then write an empty instance  instance   g.!parameterized-utils'Provides a show instance for each type.#parameterized-utilsLike , the precedence argument is one more/ than the precedence of the enclosing context.$parameterized-utils@A parameterized type that can be compared on distinct instances.%parameterized-utilscompareF compares two keys with different type parameters. Instances must ensure that keys are only equal if the type parameters are equal.*parameterized-utils=Ordering over two distinct types with a proof they are equal..parameterized-utils1A polymorphic equality operator that generalizes  .1parameterized-utilsEqF provides a method eqF8 for testing whether two parameterized types are equal.Unlike  , this only works when the type arguments are the same, and does not provide a proof that the types have the same type when they are equal. Thus this can be implemented over parameterized types that are unable to provide evidence that their type arguments are equal.3parameterized-utilsAn instance of 3 gives a way to coerce between all the types of a family. We generally use this to witness the fact that the type parameter to rtpQ is a phantom type by giving an implementation in terms of Data.Coerce.coerce.6parameterized-utilsConvert * to standard ordering.7parameterized-utilsConvert standard ordering to *.8parameterized-utilsjoinOrderingF x y first compares on x., returning an equivalent value if it is not , . If it is , , it returns y.9parameterized-utils_Compare two values, and if they are equal compare the next values, otherwise return LTF or GTF:parameterized-utilsIf the "outer" functor has an $ instance, then one can be generated for the "inner" functor. The type-level evidence of equality is deduced via generativity of g, e.g. the inference  g x ~ g y implies x ~ y.parameterized-utils-A default salt used in the implementation of  .3   !"#$%&'()*+,-./0123456789:;3 12./0$%&'()9*+,-8567: !"#;34 Type-level lists.(c) Galois, Inc 2015-2019!Joe Hendrix <jhendrix@galois.com>Safe ,-.HUVz Eparameterized-utilssUpdate the value in a context by number, from the left. If the index is out of range, the context is unchanged.Fparameterized-utilsmLookup the value in a context by number, from the left. Produce a type error if the index is out of range.Gparameterized-utilstUpdate the value in a context by number, from the right. If the index is out of range, the context is unchanged.Hparameterized-utils7Lookup the value in a context by number, from the rightIparameterized-utilsN is a snoc-list. In order to use the more intuitive left-to-right ordering of elements the desired index is subtracted from the total number of elements.Jparameterized-utils&A constraint that checks that the nat n& is a valid index into the context ctx!, and raises a type error if not.Kparameterized-utilsoHelper type family used to generate descriptive error messages when an index is larger than the length of the N being indexed.Lparameterized-utils6This type family computes the number of elements in a NMparameterized-utilsAppend two type-level contexts.Nparameterized-utilsKind N k" comprises lists of types of kind k.EFGHIJKLMNOPQRSNOPSQRMLFEHGKJI$type-level proofs involving contexts(c) Galois, Inc 2015-2019!Joe Hendrix <jhendrix@galois.com>None-HUV}TUTUDDecideable equality (i.e. evidence of non-equality) on type families(c) Galois, Inc 2014-2019&Langston Barrett <langston@galois.com>Safe -.=>?@AHSUVXsVparameterized-utilsDecidable equality.VWVW(c) Galois, Inc 2014-2018!Joe Hendrix <jhendrix@galois.com>None&'-.2=?@AHIMSUVXkxXparameterized-utils Result of comparing two numbers.\parameterized-utils'A runtime presentation of a type-level .PThis can be used for performing dynamic checks on a type-level natural numbers.]parameterized-utils+The underlying natural value of the number._parameterized-utils3This generates a NatRepr from a type-level context. X[ZY\]^_ A counter in the ST monad.(c) Galois, Inc 2014!Joe Hendrix <jhendrix@galois.com> provisionalUnsafe-HIM`parameterized-utils"An index generated by the counter.bparameterized-utils4A simple type that for getting fresh indices in the  monad. The type parameter s is used for the  monad parameter.cparameterized-utilsCreate a new counter.dparameterized-utils,Get a fresh index and increment the counter.eparameterized-utils^Return true if counter has reached the limit, and can't be incremented without risk of error.`abcdebcde`a (c) Galois, Inc 2013-2019!Joe Hendrix <jhendrix@galois.com>None &')@AUVfnparameterized-utils~A type used to describe (and match) types appearing in generated pattern matches inside of the TH generators in this module (x, y, z, and {)oparameterized-utilsThe application of a type.pparameterized-utilsMatch any type.qparameterized-utils;Match the i'th argument of the data type we are traversing.rparameterized-utilsMatch a ground type.uparameterized-utilsGiven a constructor and string, this generates a pattern for matching the expression, and the names of variables bound by pattern in order they appear in constructor.parameterized-utilsReturn an expression corresponding to the constructor. Note that this will have the type of a function expecting the argumetns given.vparameterized-utilsThe dataParamTypes function returns the list of Type arguments for the constructor. For example, if passed the DatatypeInfo for a newtype Id a = MkId a then this would return [ ( a) ]{. Note that there may be type *variables* not referenced in the returned array; this simply returns the type *arguments*.wparameterized-utilsGFind value associated with first pattern that matches given pat if any.xparameterized-utilsstructuralEquality* declares a structural equality predicate.parameterized-utilsMatch equational form.yparameterized-utilsstructuralTypeEquality f& returns a function with the type: 4 forall x y . f x -> f y -> Maybe (x :~: y) zparameterized-utilsstructuralTypeOrd f& returns a function with the type: 2 forall x y . f x -> f y -> OrderingF x y %This implementation avoids matching on both the first and second parameters in a simple case expression in order to avoid stressing GHC's coverage checker. In the case that the first and second parameters have unique constructors, a simple numeric comparison is done to compute the result.parameterized-utilsFGenerate a list of fresh names using the base name and numbered 1 to n* to make them useful in conjunction with -dsuppress-uniques.parameterized-utilsFCompare two variables, returning the third argument if they are equal.This returns an $ instance.parameterized-utils-Match expression with given type to variablesparameterized-utilsMatch equational form. parameterized-utilsgenTraverseOfType f var tp applies f to var where var has type tp. parameterized-utilstraverseAppMatch patMatch cexp C builds a case statement that matches a term with the constructor c and applies f to each argument.{parameterized-utilsstructuralTraversal tp0 generates a function that applies a traversal f( to the subterms with free variables in tp.}parameterized-utilsstructuralHash tp% generates a function with the type Int -> tp -> Int that hashes type.All arguments use hashable, and ~Y can be used instead as it allows user-definable patterns to be used at specific types.~parameterized-utilsstructuralHashWithSalt tp% generates a function with the type Int -> tp -> Int that hashes type.IThe second arguments is for generating user-defined patterns to replace   for specific types. parameterized-utilsFThis matches one of the constructors in a datatype when generating a   function.parameterized-utilsstructuralShow tp% generates a function with the type  tp -> ShowS that shows the constructor. uparameterized-utilsconstructor information parameterized-utilsgenerated name prefix parameterized-utilspattern and bound names  parameterized-utilsTypes bound by data arguments.parameterized-utilsPatterns for matching argumentsparameterized-utilsName of constructor. parameterized-utilsData declaration typesparameterized-utilsPatterns for matching argumentsparameterized-utilswildcard case requiredparameterized-utilsData declaration.parameterized-utilswildcard case requiredzparameterized-utils List of type patterns to match. parameterized-utilsbase name parameterized-utilsquantity parameterized-utilslist of names: base1, base2, ... parameterized-utilsTypes bound by data argumentsparameterized-utilsPatterns for matching argumentsparameterized-utilsName of constructor.parameterized-utilsNames bound in data declarationparameterized-utilsTypes for constructorsparameterized-utils Variables bound in first patternparameterized-utils!Variables bound in second patternparameterized-utilsData declaration typesparameterized-utilsPatterns for matching argumentsparameterized-utils(Information about the second constructorparameterized-utilsFirst constructor's indexparameterized-utils#Optional second constructor's indexparameterized-utilsName from first patternparameterized-utilsData declaration.parameterized-utilsPatterns for matching argumentsparameterized-utilsoptional right constructr index parameterized-utils(Argument types for the data declaration.parameterized-utils7Patterrns the user provided for overriding type lookup.parameterized-utilsFunction to applyparameterized-utils4Expression denoting value of this constructor field.parameterized-utils&Type bound for this constructor field. parameterized-utils(Argument types for the data declaration.parameterized-utils7Patterrns the user provided for overriding type lookup.parameterized-utils Function f given to parameterized-utilsConstructor to match. parameterized-utils(Data declaration of type we are hashing.parameterized-utilsUser provide type patternsparameterized-utilsInitial salt expressionparameterized-utilsIndex of constructorparameterized-utilsConstructor information./0nropqstuvwxyz{|}~xyz{}~./0st|unropqvw None &'-.1=?HV1 (c) Galois, Inc 2014-2015!Joe Hendrix <jhendrix@galois.com> Trustworthy-HSUVXWparameterized-utils This is a generalization of the / class to structures over parameterized terms.parameterized-utilsHMap each element of the structure to a monoid, and combine the results.parameterized-utils&Right-associative fold of a structure.parameterized-utils%Left-associative fold of a structure.parameterized-utilsTRight-associative fold of a structure, but with strict application of the operator.parameterized-utilsNLeft-associative fold of a parameterized structure with a strict accumulator.parameterized-utilsConvert structure to list.parameterized-utils~A parameterized class for types which can be tested for parameterized ordering, when given an comparison test for subterms.parameterized-utils|A parameterized class for types which can be tested for parameterized equality, when given an equality test for subterms.parameterized-utilslA parameterized class for types which can be hashed, when given functions to hash parameterized subterms.parameterized-utilskA parameterized class for types which can be shown, when given functions to show parameterized subterms.parameterized-utils9A parameterized type that is a function on all instances.parameterized-utilsPThis is a coercion used to avoid overhead associated with function composition.parameterized-utilsAMonadic fold over the elements of a structure from left to right.parameterized-utilsHMonadic strict fold over the elements of a structure from left to right.parameterized-utilsAMonadic fold over the elements of a structure from right to left.parameterized-utilsHMonadic strict fold over the elements of a structure from right to left.parameterized-utilsReturn ! if all values satisfy predicate.parameterized-utilsReturn ! if any values satisfy predicate.parameterized-utils,Return number of elements that we fold over.parameterized-utils)This function may be used as a value for fmapF in a FunctorF instance.parameterized-utils)This function may be used as a value for  in a  instance.parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsFlipped !! (c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy-/HSX2parameterized-utils This is a generalization of the / class to structures over parameterized terms.parameterized-utilsHMap each element of the structure to a monoid, and combine the results.parameterized-utils&Right-associative fold of a structure.parameterized-utils%Left-associative fold of a structure.parameterized-utilsTRight-associative fold of a structure, but with strict application of the operator.parameterized-utilsNLeft-associative fold of a parameterized structure with a strict accumulator.parameterized-utilsConvert structure to list.parameterized-utils8A parameterized type that is a functor on all instances.parameterized-utilsPThis is a coercion used to avoid overhead associated with function composition.parameterized-utilsAMonadic fold over the elements of a structure from left to right.parameterized-utilsHMonadic strict fold over the elements of a structure from left to right.parameterized-utilsAMonadic fold over the elements of a structure from right to left.parameterized-utilsHMonadic strict fold over the elements of a structure from right to left.parameterized-utilsReturn % if all values satisfy the predicate.parameterized-utilsReturn % if any values satisfy the predicate.parameterized-utils,Return number of elements that we fold over.parameterized-utilsFlipped parameterized-utils)This function may be used as a value for  in a  instance.parameterized-utils)This function may be used as a value for  in a  instance.parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utils"Traverse twice over: go under the t , under the s and lift m out.(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com>Safe&'-HSX7parameterized-utilsProject out of Some.parameterized-utilsApply function to inner value.parameterized-utilsModify the inner value.parameterized-utilsModify the inner value.(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy&'.=?@AHSUVX?parameterized-utils4A runtime representation of a GHC type-level symbol.parameterized-utils0The underlying text representation of the symbolparameterized-utilspGenerate a symbol representative at runtime. The type-level symbol will be abstract, as it is hidden by the  constructor.parameterized-utils:Generate a value representative for the type level symbol. Index generator in the ST monad.(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy&'-.EGHIMSXQ parameterized-utils"An index generated by the counter.parameterized-utils8Provides a monadic action for getting fresh typed names.The first type parameter mC is the monad used for generating names, and the second parameter s is used for the counter.parameterized-utils\The number of nonces generated so far by this generator. Only really useful for profiling.parameterized-utils$Create a new nonce generator in the  monad.parameterized-utilsThis combines  and Q to create a nonce generator that shares the same phantom type parameter as the ST monad.lThis can be used to reduce the number of type parameters when we know a ST computation only needs a single .parameterized-utils$Create a new nonce generator in the  monad.parameterized-utilsRun a / computation with a new nonce generator in the  monad.parameterized-utils$Create a new nonce generator in the  monad.parameterized-utils7A nonce generator that uses a globally-defined counter.parameterized-utilsCreate a new counter. 9A typeclass and monad transformers for generating nonces.(c) Galois, Inc 2014-2019%Eddy Westbrook <westbrook@galois.com>None-HMSVX]parameterized-utilsHelper type to build a  from the  monad.parameterized-utilsHelper type to build a  from the  monad.parameterized-utils9This transformer adds a nonce generator to a given monad.parameterized-utilsA $ is a monad that can generate fresh ?s in a given set (where we view the phantom type parameter of & as a designator of the set that the  came from).parameterized-utilsReturn the actual  used in an  computation.parameterized-utilsRun a  computation with a fresh .parameterized-utilsRun a  computation with a fresh  inside . 3Type level natural number representation at runtime(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy&'.2=>?@AGHIMQSUVXfk(parameterized-utils LeqProof m n0 is a type whose values are only inhabited when m is less than or equal to n.parameterized-utils+Return the value of the nat representation.parameterized-utils!Every nat is either zero or >= 1.parameterized-utils Decrement a NatReprparameterized-utilsGet the predecessor of a natparameterized-utils Increment a NatRepr!parameterized-utilsHReturn minimum unsigned value for bitvector with given width (always 0)."parameterized-utils=Return maximum unsigned value for bitvector with given width.#parameterized-utilsHReturn minimum value for bitvector in two's complement with given width.$parameterized-utilsHReturn maximum value for bitvector in two's complement with given width.%parameterized-utilstoUnsigned w i maps i to a i  2^w.&parameterized-utils toSigned w i" interprets the least-significant w bits in iI as a signed number in two's complement notation and returns that value.'parameterized-utilsunsignedClamp w i rounds i to the nearest value between 0 and 2^w-1 (inclusive).(parameterized-utilssignedClamp w i rounds i to the nearest value between -2^(w-1) and  2^(w-1)-1 (inclusive).)parameterized-utilsTurn an Integral value into a NatRepr . Returns Nothing# if the given value is negative.*parameterized-utilsTurn a Natural into the corresponding NatRepr+parameterized-utils.Return the maximum of two nat representations.,parameterized-utilsProduce evidence that + is commutative.-parameterized-utilsProduce evidence that * is commutative./parameterized-utils$Cancel an add followed by a subtract4parameterized-utils%(<=) is a decidable relation on nats.7parameterized-utilsThe strict order ( ),defined by n < m <- n + 1 <= m, is irreflexive.8parameterized-utils0The strict order on the naturals is irreflexive.9parameterized-utilsx 9 y checks whether x is less than or equal to y.:parameterized-utilsApply reflexivity to LeqProof;parameterized-utilsApply transitivity to LeqProof<parameterized-utils"Add both sides of two inequalities=parameterized-utils#Subtract sides of two inequalities.>parameterized-utils#Create a leqProof using two proxies@parameterized-utils(Test whether natural number is positive.Aparameterized-utils"Congruence rule for multiplicationBparameterized-utils>Multiplying two positive numbers results in a positive number.Dparameterized-utilsQProduce proof that adding a value to the larger element in an LeqProof is largerFparameterized-utilsKProduce proof that subtracting a value from the smaller element is smaller.Mparameterized-utilsQApply a function to each element in a range; return the list of values obtained.Nparameterized-utilsbApply a function to each element in a range starting at zero; return the list of values obtained.Oparameterized-utilsRecursor for natural numbeers.Pparameterized-utils)Strong induction variant of the recursor.Qparameterized-utils%Bounded recursor for natural numbers.If you can prove: - Base case: f 0 - Inductive step: if n <= h and (f n) then (f (n + 1)) You can conclude: for all n <= h, (f (n + 1)).Sparameterized-utilsUsed in VectorOparameterized-utils base case Pparameterized-utils base case parameterized-utilsinductive step [ XYZ[\]^_     !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRS[\]_XYZ[^ )*+OPQMN    678!"#$%&'(495:;<=A>?@DFBEGLHKJIC,-/0123R.S .a hash table for parameterized keys and values(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy-H~Tparameterized-utils&A hash table mapping nonces to values.Uparameterized-utilsCreate a new empty table.Vparameterized-utils!Create a new empty table to hold n elements.Wparameterized-utils6Create a hash table that is a copy of the current one.Xparameterized-utilsLookup value of key in table.Yparameterized-utils,Insert new key and value mapping into table.Zparameterized-utils,Return true if the key is in the hash table.[parameterized-utils&Delete an element from the hash table. TUVWXYZ[\ TUVWXYZ[\&Classes for working with type of kind  (k -> *) -> *(c) Galois, Inc 2014-2019&Langston Barrett <langston@galois.com>Safe-HSUVX*aparameterized-utilsnThis instance demonstrates where the above class is useful: namely, in types with existential quantification.]^_`_`]^Safe&',-.=>?@AHIQSUVX_fdparameterized-utilsA Boolean flaggparameterized-utils conditionalhparameterized-utilsnegationiparameterized-utils Conjunctionjparameterized-utils Disjunction cdefghijkdefghijck i3j21A 2-tuple with identically parameterized elements(c) Galois, Inc 2017-2019Safe&'-HSXUwparameterized-utils`Like a 2-tuple, but with an existentially quantified parameter that both of the elements share.yparameterized-utils$Extract the first element of a pair.zparameterized-utils%Extract the second element of a pair.{parameterized-utilsProject out of Pair.wxyz{wxyz{(c) Galois, Inc 2019&Langston Barrett <langston@galois.com>Safe-HSX!A type-indexed parameterized list(c) Galois, Inc 2017-2019!Joe Hendrix <jhendrix@galois.com>None&'-.1>@AHSUVXparameterized-utilsRepresents an index into a type-level list. Used in place of integers to 1. ensure that the given index *does* exist in the list 2. guarantee that it has the given kindparameterized-utilsParameterized list of elements.parameterized-utilsReturn the index as an integer.parameterized-utilsIndex 0parameterized-utilsIndex 1parameterized-utilsIndex 2parameterized-utilsIndex 3parameterized-utils+Return the value in a list at a given indexparameterized-utils Update the  at an indexparameterized-utils@Provides a lens for manipulating the element at the given index.parameterized-utilsjMap over the elements in the list, and provide the index into each element along with the element itself.parameterized-utils$Right-fold with an additional index.parameterized-utilsAZip up two lists with a zipper function, which can use the index.parameterized-utils"Traverse with an additional index.5  Trustworthy&'-./1=?@AHISUVX5parameterized-utilsKRepresent an assignment as either empty or an assignment with one appended.parameterized-utils;An assignment is a sequence that maps each index with type tp to a value of type f tp.This assignment implementation uses a binomial tree implementation that offers lookups and updates in time and space logarithmic with respect to the number of elements in the context.parameterized-utils8A balanced tree where all leaves are at the same height.VThe first parameter is the height of the tree. The second is the parameterized value.parameterized-utils.This represents a contiguous range of indices.parameterized-utilszView of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.parameterized-utilsKAn index is a reference to a position with a particular type in a context.parameterized-utils@A difference that can be automatically inferred at compile time.parameterized-utils Proof that r = l  + app for some appparameterized-utilsmDifference in number of elements between two contexts. The first context must be a sub-context of the other.parameterized-utils=A context that can be determined statically at compiler time.parameterized-utilsAllows interpreting a size.parameterized-utils!Represents the size of a context.parameterized-utilsConvert a context size to an .parameterized-utilsThe size of an empty context.parameterized-utils%Increment the size to the next value.parameterized-utilsProject a sizeparameterized-utils-The identity difference. Identity element of Category instance.parameterized-utils:The addition of differences. Flipped binary operation of Category instance.parameterized-utils9Extend the difference to a sub-context of the right side.parameterized-utils&Extend the size by a given difference.parameterized-utils,The total size of two concatenated contexts.parameterized-utilsIf l is a sub-context of r< then extract out their "contextual difference", i.e., the app such that r = l  + appparameterized-utils#Index for first element in context.parameterized-utils-Increase context while staying at same index.parameterized-utils0Return the index of a element one past the size.parameterized-utils#Return the last index of a element.parameterized-utils Given a size n, an initial value v0, and a function f, the expression forIndex n v0 f is equivalent to v0 when n is zero, and f (forIndex (n-1) v0) (n-1) otherwise.parameterized-utilsGiven an index i, size n , a function f, value v, and a function f, the expression forIndex i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.parameterized-utilsEReturn index at given integer or nothing if integer is out of bounds.parameterized-utilsProject an indexparameterized-utils5Return a range containing all indices in the context.parameterized-utils# returns the only index in a range.parameterized-utilsdropTailRange r n drops the last n elements in r.parameterized-utilsdropHeadRange r n drops the first n elements in r.parameterized-utilsLookup index in tree.parameterized-utilsUpdate value at index in tree.parameterized-utils Zip two balanced trees together. parameterized-utils0Concatenate a binomial tree and a balanced tree.!parameterized-utilsMap over a binary tree."parameterized-utils bal_drop x y returns the tree formed append x (init y)#parameterized-utilsLookup value in tree.$parameterized-utilsLookup value in tree.parameterized-utils(Return number of elements in assignment.parameterized-utils replicate nE make a context with different copies of the same polymorphic value.parameterized-utilsGenerate an assignmentparameterized-utilsGenerate an assignment in an % contextparameterized-utilsReturn empty assignment&parameterized-utils>Unexported index that returns an arbitrary type of expression.parameterized-utilsReturn value of assignment.parameterized-utils]Return value of assignment, where the index is into an initial sequence of the assignment.parameterized-utils8Modify the value of an assignment at a particular index.parameterized-utilsFView an assignment as either empty or an assignment with one appended.'parameterized-utilsImplemented with  and  (parameterized-utilsHeight of tree to generateparameterized-utilsStarting offset for entries.)parameterized-utilsHeight of tree to generateparameterized-utilsStarting offset for entries.parameterized-utilsTree to lookup.parameterized-utilsIndex to lookup.parameterized-utilsHeight of treeparameterized-utilsTree to updateparameterized-utilsIndex to lookup.parameterized-utilsHeight of tree*parameterized-utilsSize of tree to generateparameterized-utilsHeight of each element.+parameterized-utilsSize of tree to generateparameterized-utilsHeight of each element."parameterized-utilsBina#parameterized-utilsTree to lookup in.parameterized-utils Size of tree$parameterized-utilsTree to lookup in.parameterized-utils Size of treeREFGHIJKLMNOPQRS!(c) Galois, Inc 2014-2015!Joe Hendrix <jhendrix@galois.com>None&'-./1=>?@AEHISUVXJ),parameterized-utilsFView an assignment as either empty or an assignment with one appended.-parameterized-utils;An assignment is a sequence that maps each index with type tp to a value of type 'f tp'..parameterized-utilszView of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range./parameterized-utilsKAn index is a reference to a position with a particular type in a context.0parameterized-utils@A difference that can be automatically inferred at compile time.1parameterized-utils Proof that r = l  + app for some app2parameterized-utilsmDifference in number of elements between two contexts. The first context must be a sub-context of the other.3parameterized-utils=A context that can be determined statically at compiler time.4parameterized-utilsAllows interpreting a size.5parameterized-utils=An indexed singleton type representing the size of a context.6parameterized-utilsConvert a context size to an .7parameterized-utilsThe size of an empty context.8parameterized-utils%Increment the size to the next value.9parameterized-utils,The total size of two concatenated contexts.:parameterized-utils6View a size as either zero or a smaller size plus one.;parameterized-utils-The identity difference. Identity element of Category instance.<parameterized-utils:The addition of differences. Flipped binary operation of Category instance.=parameterized-utils9Extend the difference to a sub-context of the right side.>parameterized-utils&Extend the size by a given difference.?parameterized-utilsIf l is a sub-context of r< then extract out their "contextual difference", i.e., the app such that r = l  + app@parameterized-utilsConvert an index to an <, where the index of the left-most type in the context is 0.Aparameterized-utils#Index for first element in context.Bparameterized-utils-Increase context while staying at same index.Cparameterized-utils1Return the index of an element one past the size.Dparameterized-utils#Return the last index of a element.Eparameterized-utils Given a size n, an initial value v0, and a function f, the expression forIndex n v0 f calls f on each index less than n starting from 0 and v0, with the value v obtained from the last call.Fparameterized-utilsGiven an index i, size n , a function f, value v, and a function f, the expression forIndexRange i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n v) otherwise.Gparameterized-utilsEReturn index at given integer or nothing if integer is out of bounds.Hparameterized-utilsProject an indexIparameterized-utils(Return number of elements in assignment.Jparameterized-utilsGenerate an assignmentKparameterized-utilsGenerate an assignmentLparameterized-utils replicate nE make a context with different copies of the same polymorphic value.Mparameterized-utilsCreate empty indexed vector.Nparameterized-utilsReturn value of assignment.Oparameterized-utils]Return value of assignment, where the index is into an initial sequence of the assignment.Pparameterized-utilsMap assignmentQparameterized-utilsConvert assignment to list.Rparameterized-utilsRenders as integer literalSparameterized-utilsImplemented with ; and <Tparameterized-utilsRenders as integer literalMEFGHIJKLMNOPQRS,UV-.WX/0YZ[\1]23^4_`5678a9:;<=b>?c@ABCDdeEFGHfIJKLMghijNOklmn(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy%,-./=>?@ACHSUVXgkyparameterized-utilsjThis class implements two methods that witness the isomorphism between curried and uncurried functions.parameterized-utilsxTransform a function that accepts an assignment into one with a separate variable for each element of the assignment.parameterized-utilsGTransform a curried function into one that accepts an assignment value.parameterized-utilsThis type family is used to define currying/uncurrying operations on assignments. It is best understood by seeing its evaluation on several examples: CurryAssignment EmptyCtx f x = x CurryAssignment (EmptyCtx ::> a) f x = f a -> x CurryAssignment (EmptyCtx ::> a ::> b) f x = f a -> f b -> x CurryAssignment (EmptyCtx ::> a ::> b ::> c) f x = f a -> f b -> f c -> xoparameterized-utilsClass for computing  values for positions in a N.parameterized-utils'Constraint synonym used for getting an  into a N. n? is the zero-based, left-counted index into the list of types ctx which has the type r.parameterized-utilsThis datastructure contains a proof that the first context is embeddable in the second. This is useful if we want to add extend an existing term under a larger context.parameterized-utils8Pattern synonym for extending an assignment on the rightparameterized-utils(Pattern synonym for the empty assignmentparameterized-utils Create a single element context.parameterized-utils'forIndexM sz f' calls f on indices '[0..sz-1]'.parameterized-utils@Generate an assignment with some context type that is not known.parameterized-utils@Generate an assignment with some context type that is not known.parameterized-utils#Convert the assignment to a vector.parameterized-utils#Return true if assignment is empty.parameterized-utils.Return assignment with all but the last block.parameterized-utils*Return the last element in the assignment.parameterized-utilsFView an assignment as either empty or an assignment with one appended.parameterized-utils!Get a lens for an position in an N by zero-based, left-to-right position. The position must be specified using TypeApplications for the n parameter.parameterized-utils Compute an & value for a particular position in a N. The TypeApplicationsB extension will be needed to disambiguate the choice of the type n.parameterized-utilsThis version of ! is suitable for use without the TypeApplications extension.parameterized-utils+Create an assignment from a list of values.parameterized-utils!Visit each of the elements in an  AssignmentK in order from left to right and collect the results using the provided Monoid.parameterized-utils!Visit each of the elements in an  Assignment? in order from left to right, executing an action with each.3parameterized-utilsInductive-step4parameterized-utils Base-caseEFGHIJKLMNOPQRS      !"#$%&'()*+,-./0      !"#$%&'()*+,-./0 3Representations of a type-level natural at runtime.(c) Galois, Inc 2019None&',-.=>?@AHIQSUVX_f)9parameterized-utilsImplicit runtime representation:parameterized-utilsWhen we have optimized the runtime representation, we need to have a "view" that decomposes the representation into the standard form.=parameterized-utilscThe run time value, stored as an Word64 As these are unary numbers, we don't worry about overflow.?parameterized-utilsCalculate the size of a context@parameterized-utilsApply a constructor f n-times to an argument sAparameterized-utilsMinimumBparameterized-utilsMaximumCparameterized-utilsGreater-than-or-equalDparameterized-utils Greater-thanEparameterized-utils Less-thanFparameterized-utilsLess-than-or-equalGparameterized-utilsMultiplicationHparameterized-utils SubtractionIparameterized-utilsAdditionJparameterized-utilsPeano successorKparameterized-utils Peano zeroLparameterized-utils(Unary representation for natural numbersMparameterized-utils*Test whether a number is Zero or SuccessorNparameterized-utils3convert the view back to the runtime representationOparameterized-utilsZeroPparameterized-utilsSuccessor, IncrementQparameterized-utilsGet the predecessor (decrement)Rparameterized-utilsAdditionSparameterized-utils SubtractionTparameterized-utilsMultiplicationUparameterized-utilsMaximumVparameterized-utilsMinimumWparameterized-utilsLess-than-or-equal-toXparameterized-utils Less-thanYparameterized-utilsGreater-than-or-equal-toZparameterized-utils Greater-than[parameterized-utilsApply a constructor f n-times to an argument s\parameterized-utilsCalculate the size of a context]parameterized-utils Convert a p to a =^parameterized-utilsTurn an Integral value into a = . Returns Nothing# if the given value is negative._parameterized-utils*Return the maximum of two representations.`parameterized-utils*Return the minimum of two representations.aparameterized-utilsList length as a Peano numberbparameterized-utils)Context size commutes with context appendcparameterized-utilsMinus distributes over plusdparameterized-utils%We can reshuffle minus with less than1 9:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcd1LKJIHGBARSTUVOPQ@?[\FEDCWXZY9=:;<MN]>^_`abcd "Safe   !"#$%&'()*+,-./0123456789:;EFGHIJKLMNOPQRSXYZ[\]^_     !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSwxyz{$Utilities for balanced binary trees.(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com>Safe %&',>@ACXipparameterized-utils A Strict pairzparameterized-utils Updated aT contains a value that has been flagged on whether it was modified by an operation.}parameterized-utilsA strict version of qparameterized-utilsbalanceL p l r* returns a balanced tree for the sequence  l ++ [p] ++ r.It assumes that l and r- are close to being balanced, and that only l may contain too many elements.parameterized-utilsbalanceR p l r* returns a balanced tree for the sequence  l ++ [p] ++ r.It assumes that l and r- are close to being balanced, and that only r may contain too many elements.rparameterized-utilsInsert a new maximal element.sparameterized-utilsInsert a new minimal element.parameterized-utilslinkC is called to insert a key and value between two disjoint subtrees.parameterized-utilsBConcatenate two trees that are ordered with respect to each other.parameterized-utils insert p m inserts the binding into ms. It returns an Unchanged value if the map stays the same size and an updated value if a new entry was inserted.parameterized-utilsglue l r concatenates l and r.It assumes that l and r1 are already balanced with respect to each other.parameterized-utilsyReturns only entries that are less than predicate with respect to the ordering and Nothing if no elements are discarded.parameterized-utils filterLt k m returns submap of m3 that only contains entries that are smaller than k1. If no entries are deleted then return Nothing.tparameterized-utilsMInsert a new key and value in the map if it is not already present. Used by .parameterized-utilsUnion two setsuparameterized-utils]Hedge union where we only add elements in second map if key is strictly above a lower bound.vparameterized-utils]Hedge union where we only add elements in second map if key is strictly below a upper bound.wparameterized-utilsiHedge union where we only add elements in second map if key is strictly between a lower and upper bound.parameterized-utilsPredicate that returns whether the entry is less than, greater than, or equal to the key we are entry that we are looking for.pqrvustwxyz{|}~}~z{|wxyrvustpq2Finite maps with parameterized key and value types(c) Galois, Inc 2014-2019 Trustworthy&'-./=?@AHSUVXr2parameterized-utils$ tells what to do with a found valueparameterized-utilsKeep the current value.parameterized-utilsSet the value to a new value.parameterized-utilsDelete a value.parameterized-utilsEA map from parameterized keys to values with the same parameter type.parameterized-utilsReturn empty mapparameterized-utilsReturn true if map is emptyparameterized-utils&Return map containing a single elementparameterized-utils&Apply function to all elements in map.parameterized-utilsModify elements in a mapparameterized-utils"Map keys and elements and collect x results.parameterized-utilsMap elements and collect x results.yparameterized-utilsTraverse elements in a mapparameterized-utilsTraverse elements in a mapparameterized-utils4Traverse elements in a map without returning result.parameterized-utils%Traverse keys/values and collect the x results.parameterized-utilsLookup value in map.parameterized-utilsfindWithDefault d k m returns the value bound to k in the map m, or d if k is not bound in the map.parameterized-utils#Return true if key is bound in map.parameterized-utils'Return true if key is not bound in map.parameterized-utils.Return all keys of the map in ascending order.parameterized-utilsDReturn all elements of the map in the ascending order of their keys.parameterized-utils/Perform a left fold with the key also provided.parameterized-utils6Perform a strict left fold with the key also provided.parameterized-utils0Perform a right fold with the key also provided.parameterized-utils7Perform a strict right fold with the key also provided.parameterized-utils0Fold the keys and values using the given monoid.parameterized-utils=A monadic left-to-right fold over keys and values in the map.parameterized-utils=A monadic right-to-left fold over keys and values in the map.zparameterized-utils$Pretty print keys and values in map.parameterized-utils4Return entries with values that satisfy a predicate.parameterized-utils0Return key-value pairs that satisfy a predicate.parameterized-utils filterGt k m returns submap of m2 that only contains entries that are larger than k.parameterized-utils filterLt k m returns submap of m3 that only contains entries that are smaller than k.parameterized-utilsHInsert a binding into the map, replacing the existing binding if needed.{parameterized-utilsHInsert a binding into the map, replacing the existing binding if needed.parameterized-utilsinsertWith f new m inserts the binding into m. It inserts  f new old if m' already contains an equivalent value old, and new otherwise. It returns an |. value if the map stays the same size and an z$ value if a new entry was inserted.parameterized-utils'Delete a value from the map if present.parameterized-utilsLeft-biased union of two maps. The resulting map will contain the union of the keys of the two arguments. When a key is contained in both maps the value from the first map will be preserved.parameterized-utils\Log-time algorithm that allows a value at a specific key to be added, replaced, or deleted.parameterized-utils"Create a Map from a list of pairs.parameterized-utils:Return list of key-values pairs in map in ascending order.parameterized-utils;Return list of key-values pairs in map in descending order.parameterized-utils'Return list of key-values pairs in map.parameterized-utilsVGenerate a map from a foldable collection of keys and a function from keys to values.parameterized-utils^Generate a map from a foldable collection of keys and a monadic function from keys to values.parameterized-utils*Merge bindings in two maps to get a third.The first function is used to merge elements that occur under the same key in both maps. Return Just to add an entry into the resulting map under this key or Nothing to remove this key from the resulting map.aThe second function will be applied to submaps of the first map argument where no keys overlap with the second map argument. The result of this function must be a map with a subset of the keys of its argument. This means the function can alter the values of its argument and it can remove key-value pairs from it, but it must not introduce new keys.iThird function is analogous to the second function except that it applies to the second map argument of  instead of the first.-Common examples of the two functions include | when constructing a union or } # when constructing an intersection.~parameterized-utils<Returns only entries that are strictly between the two keys.parameterized-utilsNTurn a map key into a lens that points into the indicated position in the map.parameterized-utils[Turn a map key into a traversal that visits the indicated element in the map, if it exists.parameterized-utils(Function to call if no element is found.parameterized-utils Key to updateparameterized-utils"Action to call if nothing is foundparameterized-utils!Action to call if value is found.parameterized-utils Map to updateparameterized-utils)Function for evaluating a register value.parameterized-utilsSet of X86 registersparameterized-utilsFFunction for evaluating an input value to store the result in the map.parameterized-utils+Set of input values (traversed via folding)f   !"#$%&'()*+,-./0123456789:;wxvz{|3vz{|wx9A common location for defining multi-byte value ordering.(c) Galois, Inc 2019Safe(parameterized-utilsHDetermines the composition of smaller numeric values into larger values.BigEndian = most significant values in the lowest index location / first LittleEndian = least significant values in the lowest index location / firstiValue: 0x01020304 BigEndian = [ 0x01, 0x02, 0x03, 0x04 ] LittleEndian = [ 0x04, 0x03, 0x02, 0x01 ](c) Galois, Inc 2014-2019None&'.IQSUVXk#parameterized-utilsBThis newtype wraps Vector so that we can curry it in the call to  natRecBounded6. It adds 1 to the length so that the base case is a Vector of non-zero length.parameterized-utilsFixed-size non-empty vectors.parameterized-utils=Get the elements of the vector as a list, lowest index first.parameterized-utilsLength of the vector. O(1)parameterized-utilsThe length of the vector as an Int.parameterized-utils%Get the element at the given index. O(1)parameterized-utilshGet the element at the given index. Raises an exception if the element is not in the vector's domain. O(1)parameterized-utils'Insert an element at the given index. O(n).parameterized-utils.Insert an element at the given index. Return / if the element is outside the vector bounds. O(n).parameterized-utils.Proof that the length of this vector is not 0.parameterized-utilsDRemove the first element of the vector, and return the rest, if any.parameterized-utils=Make a vector of the given length and element type. Returns NothingA if the input list does not have the right number of elements. O(n).parameterized-utils(Extract a subvector of the given vector.parameterized-utils2Take the front (lower-indexes) part of the vector.parameterized-utils.Zip two vectors, potentially changing types. O(n)parameterized-utilsInterleave two vectors. The elements of the first vector are at even indexes in the result, the elements of the second are at odd indexes. parameterized-utils Move the elements around, as specified by the given function. * Note: the reindexing function says where each of the elements in the new vector come from. * Note: it is OK for the same input element to end up in mulitple places in the result. O(n)parameterized-utilsReverse the vector.parameterized-utilsRotate "left". The first element of the vector is on the "left", so rotate left moves all elemnts toward the corresponding smaller index. Elements that fall off the beginning end up at the end.parameterized-utilsRotate "right". The first element of the vector is on the "left", so rotate right moves all elemnts toward the corresponding larger index. Elements that fall off the end, end up at the beginning.parameterized-utilsMove all elements towards smaller indexes. Elements that fall off the front are ignored. Empty slots are filled in with the given element. O(n). parameterized-utilsMove all elements towards the larger indexes. Elements that "fall" off the end are ignored. Empty slots are filled in with the given element. O(n). parameterized-utilsDAppend two vectors. The first one is at lower indexes in the result.parameterized-utilsVector with exactly one elementparameterized-utils&Add an element to the head of a vectorparameterized-utils&Add an element to the tail of a vectorparameterized-utilsqApply a function to each element in a range starting at zero; return the a vector of values obtained. cf. both  natFromZero and Data.Vector.generateparameterized-utilsSince Vector3 is traversable, we can pretty trivially sequence natFromZeroVec inside a monad.parameterized-utilsMonadically join a vector of values, using the given function. This functionality can sometimes be reproduced by creating a newtype wrapper and using joinWith3, this implementation is provided for convenience.parameterized-utilsOJoin a vector of vectors, using the given function to combine the sub-vectors.parameterized-utils(Split a vector into a vector of vectors.The Endian> parameter determines the ordering of the inner vectors. If  LittleEndian;, then less significant bits go into smaller indexes. If  BigEndianQ, then less significant bits go into larger indexes. See the documentation for  for more details.parameterized-utilsAn applicative version of  splitWith.parameterized-utilsaAppend the two bit vectors. The first argument is at the lower indexes of the resulting vector.parameterized-utils^Split a vector into a vector of vectors. The default ordering of the outer result vector is  LittleEndian.For example: / let wordsize = knownNat :: NatRepr 3 vecsize = knownNat :: NatRepr 12 numwords = knownNat :: NatRepr 4 (12 / 3) Just inpvec = fromList vecsize [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ] in show (split numwords wordsize inpvec) == "[ [1,2,3], [4,5,6], [7,8,9], [10,11,12] ]" . whereas a BigEndian result would have been 2 [ [10,11,12], [7,8,9], [4,5,6], [1,2,3] ] parameterized-utilsCJoin a vector of vectors into a single vector. Assumes an append/ LittleEndianR join strategy: the order of the inner vectors is preserved in the result vector.  let innersize = knownNat :: NatRepr 4 Just inner1 = fromList innersize [ 1, 2, 3, 4 ] Just inner2 = fromList innersize [ 5, 6, 7, 8 ] Just inner3 = fromList innersize [ 9, 10, 11, 12 ] outersize = knownNat :: NatRepr 3 Just outer = fromList outersize [ inner1, inner2, inner3 ] in show (join innersize outer) = [ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12 ]  a prepend/ BigEndian' join strategy would have the result: / [ 9, 10, 11, 12, 5, 6, 7, 8, 1, 2, 3, 4 ] parameterized-utils Start index parameterized-utilsWidth of sub-vector parameterized-utilsA function for joining contained elements. The first argument is the size of the accumulated third term, and the second argument is the element to join to the accumulated term. The function can use any join strategy desired (prepending/ BigEndian, appending/ LittleEndian , etc.). parameterized-utilsA function for joining contained elements. The first argument is the size of the accumulated third term, and the second argument is the element to join to the accumulated term. The function can use any join strategy desired (prepending/ BigEndian, appending/ LittleEndian , etc.). parameterized-utils-A function for slicing out a chunk of length w, starting at i parameterized-utils-f function for slicing out f chunk of length w, starting at i parameterized-utilsInner vector sizeparameterized-utilsOuter vector sizeparameterized-utils Input vector$$(c) Galois, Inc 2019None &'-=HSXparameterized-utils@Turn an explicit Repr value into an implict KnownRepr constraint#$%&'(&)*#+,#+-#+.#+/#01#02#03#04#5678978:78;<=>?@@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}|{~                             !"#$%&'())*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                                                          !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~surtsu''##&)#             # # &) #&)##### &)      ! " ##$% & ' ( ) * +!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!,!'!!!!!!!!!!!!!!!!!!!!!!!!!!!-#./#01234567#089:#$;#$<=>?#0@AB2parameterized-utils-2.0.1.0-IOwKQvugsW6Dm8QBaH9DZcData.Parameterized.SymbolReprData.Parameterized.HashTableData.Parameterized.NatReprData.Parameterized.ClassesData.Parameterized.ComposeData.Parameterized.CtxData.Parameterized.Ctx.ProofsData.Parameterized.DecidableEqData.Parameterized.Nonce.UnsafeData.Parameterized.TH.GADTData.Parameterized.DataKind Data.Parameterized.TraversableFCData.Parameterized.TraversableFData.Parameterized.SomeData.Parameterized.Nonce%Data.Parameterized.Nonce.TransformersData.Parameterized.ClassesCData.Parameterized.BoolReprData.Parameterized.PairData.Parameterized.AllData.Parameterized.ListData.Parameterized.ContextData.Parameterized.Peano Data.Parameterized.Utils.BinTreeData.Parameterized.MapData.Parameterized.Utils.EndianData.Parameterized.VectorData.Parameterized.WithRepr#Data.Parameterized.NatRepr.Internal Data.FoldablefoldMap!Data.Parameterized.Context.UnsafeData.Parameterized.Context.SafeData.Parameterizedbase GHC.TypeLits KnownSymbolghc-primGHC.Prim RealWorld GHC.TypesSymbol GHC.TypeNats+*-<=Data.Type.EqualityRefl:~: testEquality TestEquality Data.MaybeisJust'hashable-1.3.0.0-1RsrIcitxVDKffGN1TuMlmData.Hashable.Classhash hashWithSaltHashabletestEqualityComposeBare$fTestEqualitykCompose KnownRepr knownReprTypeAp HashableF hashWithSaltFhashFAtFatFIxedF'ixF'IxedFixFIxValueFIndexFShowFwithShowshowF showsPrecFOrdFcompareFleqFltFgeqFgtF OrderingFLTFEQFGTFPolyEqpolyEqFpolyEqEqFeqF CoercibleFcoerceForderingF_refl toOrdering fromOrdering joinOrderingF lexCompareF ordFComposeshowsF$fCoercibleFkConst $fEqFkConst$fOrdFkCompose $fShowFkConst$fHashableFkConst$fHashableTypeAp $fShowTypeAp $fOrdTypeAp $fEqTypeAp CtxUpdate CtxLookupCtxUpdateRightCtxLookupRightFromLeftValidIxCheckIxCtxSize<+>CtxEmptyCtx::> SingleCtxleftIdassoc DecidableEqdecEq NatComparisonNatLTNatEQNatGTNatReprnatValue compareNatknownNatNonce indexValueNonceGeneratornewNonceGenerator freshNonceatLimit $fShowFkNonce$fHashableFkNonce $fOrdFkNonce$fTestEqualitykNonce $fEqNonce $fOrdNonce$fHashableNonce $fShowNonceTypePatTypeAppAnyTypeDataArgConTypeDataDlookupDataType'conPatdataParamTypes assocTypePatsstructuralEqualitystructuralTypeEqualitystructuralTypeOrdstructuralTraversal asTypeConstructuralHashstructuralHashWithSaltstructuralShowsPrecSndFstPairReprfstsnd$fOrdF(,)PairRepr$fTestEquality(,)PairRepr$fShowF(,)PairRepr$fShowPairRepr $fOrdPairRepr $fEqPairRepr TraversableFC traverseFC FoldableFC foldMapFCfoldrFCfoldlFCfoldrFC'foldlFC'toListFCOrdFC compareFCTestEqualityFCtestEqualityFC HashableFChashWithSaltFCShowFCshowFC showsPrecFC FunctorFCfmapFCfoldlMFC foldlMFC'foldrMFC foldrMFC'allFCanyFClengthFC fmapFCDefaultfoldMapFCDefault traverseFC_forMFC_forFC_forFC TraversableF traverseF FoldableFfoldMapFfoldrFfoldlFfoldrF'foldlF'toListFFunctorFfmapFfoldlMFfoldlMF'foldrMFfoldrMF'allFanyFlengthFforF fmapFDefaultfoldMapFDefault traverseF_forF_$fFunctorFlCompose$fFunctorFkConst$fFoldableFkConst$fTraversableFlCompose$fFoldableFlCompose$fTraversableFkConstSomeviewSomemapSome traverseSome traverseSome_$fTraversableFkSome$fFoldableFkSome$fFunctorFkSome $fShowSome$fHashableSome $fOrdSome$fEqSome SymbolRepr symbolRepr someSymbol knownSymbol$fShowFSymbolSymbolRepr$fShowSymbolRepr$fHashableSymbolRepr$fHashableFSymbolSymbolRepr$fOrdSymbolRepr$fEqSymbolRepr$fOrdFSymbolSymbolRepr$fTestEqualitySymbolSymbolRepr$fKnownReprSymbolSymbolReprsGlobalNonceGeneratorcountNoncesGeneratednewSTNonceGeneratorrunSTNonceGeneratornewIONonceGeneratorwithSTNonceGeneratorwithIONonceGeneratorglobalNonceGeneratorwithGlobalSTNonceGeneratorNonceIONonceSTNonceT runNonceT MonadNonceNonceSet freshNonceM getNonceSTGen runNonceST runNonceIO$fMonadNonceStateT$fMonadNonceNonceT$fMonadTransNonceT$fFunctorNonceT$fApplicativeNonceT $fMonadNonceTNatCases NatCaseLT NatCaseEQ NatCaseGTLeqProof IsZeroNatZeroNat NonZeroNatintValuewidthVal withKnownNat isZeroNat isZeroOrGT1decNatpredNatincNathalfNataddNatsubNatdivNat withDivModNat natMultiply minUnsigned maxUnsigned minSigned maxSigned toUnsignedtoSigned unsignedClamp signedClampsomeNat mkNatReprmaxNatplusCommmulCommmul2PlusplusMinusCancelminusPlusCanceladdMulDistribRightwithAddMulDistribRightwithSubMulDistribRight decideLeq testStrictLeq testNatCaseslessThanIrreflexivelessThanAsymmetrictestLeqleqReflleqTransleqAdd2leqSub2leqProof withLeqProofisPosNat leqMulCongr leqMulPos leqMulMonoleqAdd leqAddPosleqSubaddIsLeqaddPrefixIsLeq dblPosIsPos addIsLeqLeft1withAddPrefixLeq withAddLeq natForEach natFromZeronatRec natRecStrong natRecBounded mulCancelRlemmaMul HashTablenewnewSizedclonelookupinsertmemberdeleteclearOrdCcompareC TestEqualityC testEqualityC$fTestEqualityCkSome $fOrdCkSome KnownBoolBoolRepr FalseReprTrueReprifReprnotRepr%&&%||someBool$fKnownReprBoolBoolReprFalse$fKnownReprBoolBoolReprTrue$fHashableFBoolBoolRepr$fShowFBoolBoolRepr$fShowBoolRepr$fPolyEqBoolReprBoolRepr$fOrdFBoolBoolRepr$fDecidableEqBoolBoolRepr$fTestEqualityBoolBoolRepr $fEqBoolRepr$fHashableBoolReprPairfstPairsndPairviewPair$fFoldableFkPair$fFunctorFkPair$fEqPairAllgetAllallConst$fEqAll $fShowAll$fFoldableFkAll$fFunctorFkAllIndex IndexHere IndexThereListNil:<index0index1index2index3!!updateindexedimapifoldrizipWith itraverse$fKnownRepr[]List:$fKnownRepr[]List[] $fOrdF[]List$fTestEquality[]List$fTraversableFCk[]List$fFoldableFCk[]List$fFunctorFCk[]List $fShowF[]List $fShowList$fHashableIndex $fOrdIndex $fOrdFkIndex$fTestEqualitykIndex $fShowFkIndex $fShowIndex $fEqIndex AssignView AssignEmpty AssignExtend Assignment IndexRange IndexView IndexViewLast IndexViewInitindexVal KnownDiff knownDiffDiffViewNoDiffExtendRightDiffIsAppendDiff KnownContext knownSizeSizeViewZeroSizeIncSizeSizesizeIntzeroSizeincSizedecSizeviewSizenoDiffaddDiff extendRight appendDiffextSizeaddSize diffIsAppendviewDiff baseIndex skipIndex nextIndex lastIndex extendIndex extendIndex'forIndex forIndexRangeintIndex viewIndexallRange indexOfRange dropTailRange dropHeadRangesize replicategenerate generateMemptyextend!!^adjustadjustM viewAssignzipWithzipWithMtraverseWithIndex<++>CurryAssignmentClasscurryAssignmentuncurryAssignmentCurryAssignmentIdxExtendContext'extendContext' ExtendContext extendContextApplyEmbedding'applyEmbedding'ApplyEmbeddingapplyEmbedding CtxEmbedding _ctxeSize_ctxeAssignment:>Empty singleton forIndexM generateSome generateSomeMtoVectornull decomposeinitlastviewtakectxeSizectxeAssignmentidentityEmbeddingextendEmbeddingRightDiffextendEmbeddingRightappendEmbeddingextendEmbeddingBothfieldnatIndex natIndexProxyfromListtraverseAndCollecttraverseWithIndex_size1size2size3size4size5size6i1of2i2of2i1of3i2of3i3of3i1of4i2of4i3of4i4of4i1of5i2of5i3of5i4of5i5of5i1of6i2of6i3of6i4of6i5of6i6of6$fApplyEmbedding'k'k'Index$fExtendContext'k'k'Index $fIdx'kn::>r $fIdx'k0::>x$fCurryAssignmentClassk::>$fCurryAssignmentClasskEmptyCtx$fApplicativeCollector$fFunctorCollector KnownPeano PeanoViewZReprSRepr PeanoRepr peanoValueCtxSizePRepeatMinMaxGeGtLtLeMulMinusPlusSZPeano peanoViewviewReprzeroPsuccPpredPplusPminusPmulPmaxPminPlePltPgePgtPrepeatPctxSizeP mkPeanoRepr somePeanomaxPeanominPeano peanoLengthplusCtxSizeAxiomminusPlusAxiomltMinusPlusAxiom$fHashableFPeanoPeanoRepr$fShowFPeanoPeanoRepr$fShowPeanoRepr$fPolyEqPeanoReprPeanoRepr$fOrdFPeanoPeanoRepr$fDecidableEqPeanoPeanoRepr$fTestEqualityPeanoPeanoRepr $fEqPeanoRepr$fHashablePeanoRepr$fKnownReprPeanoPeanoReprS$fKnownReprPeanoPeanoReprZPairS IsBinTreeasBintipbinTreeAppBinTreeTipTreeUpdated UnchangedMaybeSJustSNothingS fromMaybeS updatedValuebalanceLbalanceRlinkmergegluefilterGtfilterLtunion$fApplicativeMaybeS$fAlternativeMaybeS$fFunctorMaybeS UpdateRequestKeepSetDeleteMapF mapWithKeymapmapMaybeWithKeymapMaybetraverseWithKeytraverseWithKey_traverseMaybeWithKeyfindWithDefault notMemberkeyselems foldlWithKey foldlWithKey' foldrWithKey foldrWithKey'foldMapWithKey foldlMWithKey foldrMWithKeyfilter filterWithKey insertWith updateAtKey toAscList toDescListtoListfromKeys fromKeysM mergeWithKeyM $fShowMapF$fTraversableFkMapF$fFoldableFkMapF$fFunctorFkMapF$fEqMapF$fIsBinTreeMapFPair $fAtFaMapF $fIxedFaMapFEndian LittleEndian BigEndian $fEqEndian $fShowEndian $fOrdEndianVectorlength lengthIntelemAt elemAtMaybe elemAtUnsafeinsertAt insertAtMaybenonEmptyunconsslice zipWithM_ interleaveshufflereverserotateLrotateRshiftLshiftRappendconssnoc joinWithMjoinWith splitWith splitWithAsplitjoin$fTraversableVector$fFoldableVector$fFunctorVector $fShowVector $fEqVectorIsReprwithRepr$fIsReprCtxAssignment$fIsRepr[]List$fIsReprBoolBoolRepr$fIsReprPeanoPeanoRepr$fIsReprSymbolSymbolRepr$fIsReprNatNatReprGHC.ShowShow showsPrec defaultSaltNatGHC.STSTconExprtemplate-haskellLanguage.Haskell.TH.SyntaxSigTVarTStarTmkEqFnewNamesjoinCompareToOrdFmatchOrdArgumentsmkOrdFgenTraverseOfTypetraverseAppMatch matchHashCtormatchEqArguments mkSimpleEqF mkSimpleOrdFData.TraversabletraverseFoldable#.TruerunSTIOGHC.RealmodData.Type.BoolIf&&||Not BalancedTreeIntunsafe_bal_indexunsafe_bal_adjust bal_zipWithMfmap_binbal_dropunsafe_bin_indexunsafe_bin_adjustGHC.Base Applicative unsafeIndex$fCategoryCtxDiffunsafe_bal_generateunsafe_bal_generateMunsafe_bin_generateunsafe_bin_generateM $fShowSizeIdx'GHC.WordWord64 GHC.MaybeMaybe insertMax insertMininsertR hedgeUnion_LB hedgeUnion_UBhedgeUnion_LB_UBJustshowMapinsertWithImplidconst filterMiddleatKey'Vector'NothingvAppend