!p:      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVW 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 { | } ~         !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~utilities for working with Data.Functor.Compose(c) Galois, Inc 2014-2019&Langston Barrett <langston@galois.com>Safe &'-HSUVX3y parameterized-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>@AHSUVXhparameterized-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-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  .,parameterized-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..parameterized-utilsAn instance of . 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.1parameterized-utilsConvert % to standard ordering.2parameterized-utilsConvert standard ordering to %.3parameterized-utilsjoinOrderingF x y first compares on x., returning an equivalent value if it is not ' . If it is ' , it returns y.4parameterized-utils_Compare two values, and if they are equal compare the next values, otherwise return LTF or GTF5parameterized-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 ..  !"#$%&'()*+,-./0123456. ,-)*+ !"#$4%&'(301256./ Type-level lists.(c) Galois, Inc 2015-2019!Joe Hendrix <jhendrix@galois.com>Safe ,-.HUV} <parameterized-utilssUpdate the value in a context by number, from the left. If the index is out of range, the context is unchanged.=parameterized-utilsmLookup the value in a context by number, from the left. Produce a type error if the index is out of range.>parameterized-utilstUpdate the value in a context by number, from the right. If the index is out of range, the context is unchanged.?parameterized-utils7Lookup the value in a context by number, from the right@parameterized-utilsE 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.Aparameterized-utils&A constraint that checks that the nat n& is a valid index into the context ctx!, and raises a type error if not.Bparameterized-utilsoHelper type family used to generate descriptive error messages when an index is larger than the length of the E being indexed.Cparameterized-utils6This type family computes the number of elements in a EDparameterized-utilsAppend two type-level contexts.Eparameterized-utilsKind E k" comprises lists of types of kind k.<=>?@ABCDEFGHIJEFGJHIDC=<?>BA@$type-level proofs involving contexts(c) Galois, Inc 2015-2019!Joe Hendrix <jhendrix@galois.com>None-HUV*KLKLDDecideable equality (i.e. evidence of non-equality) on type families(c) Galois, Inc 2014-2019&Langston Barrett <langston@galois.com>Safe -.=>?@AHSUVXMparameterized-utilsDecidable equality.MNMN(c) Galois, Inc 2014-2018!Joe Hendrix <jhendrix@galois.com>None&'-.2=?@AHIMSUVXkOparameterized-utils Result of comparing two numbers.Sparameterized-utils'A runtime presentation of a type-level .PThis can be used for performing dynamic checks on a type-level natural numbers.Tparameterized-utils+The underlying natural value of the number.Vparameterized-utils3This generates a NatRepr from a type-level context. ORQPSTUV A counter in the ST monad.(c) Galois, Inc 2014!Joe Hendrix <jhendrix@galois.com> provisionalUnsafe-HIMWparameterized-utils"An index generated by the counter.Yparameterized-utils4A simple type that for getting fresh indices in the  monad. The type parameter s is used for the  monad parameter.Zparameterized-utilsCreate a new counter.[parameterized-utils,Get a fresh index and increment the counter.\parameterized-utils^Return true if counter has reached the limit, and can't be incremented without risk of error.WXYZ[\YZ[\WX (c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com>Safe&'-HSXvgparameterized-utilsProject out of Some.hparameterized-utilsApply function to inner value.iparameterized-utilsModify the inner value.jparameterized-utilsModify the inner value.efghijefghij  Index generator in the ST monad.(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy&'-.EGHIMSX pparameterized-utils"An index generated by the counter.rparameterized-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.tparameterized-utils\The number of nonces generated so far by this generator. Only really useful for profiling.uparameterized-utils$Create a new nonce generator in the  monad.vparameterized-utils$Create a new nonce generator in the  monad.wparameterized-utilsRun a / computation with a new nonce generator in the  monad.xparameterized-utils$Create a new nonce generator in the  monad.yparameterized-utils7A nonce generator that uses a globally-defined counter.zparameterized-utilsCreate a new counter. opqrstuvwxyz rstpquvxwzoy 9A typeclass and monad transformers for generating nonces.(c) Galois, Inc 2014-2019%Eddy Westbrook <westbrook@galois.com>None-HMSVXparameterized-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 p?s in a given set (where we view the phantom type parameter of p& as a designator of the set that the p came from).parameterized-utilsReturn the actual r used in an  computation.parameterized-utilsRun a  computation with a fresh r.parameterized-utilsRun a  computation with a fresh r inside .opqrstuvwxyz 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 NatReprparameterized-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 NatReprparameterized-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 subtractparameterized-utils%(<=) is a decidable relation on nats.parameterized-utilsThe strict order ( ),defined by n < m <- n + 1 <= m, is irreflexive.parameterized-utils0The strict order on the naturals is irreflexive.parameterized-utilsx  y checks whether x is less than or equal to y.parameterized-utilsApply reflexivity to LeqProofparameterized-utilsApply transitivity to LeqProofparameterized-utils"Add both sides of two inequalitiesparameterized-utils#Subtract sides of two inequalities.parameterized-utils#Create a leqProof using two proxiesparameterized-utils(Test whether natural number is positive.parameterized-utils"Congruence rule for multiplicationparameterized-utils>Multiplying two positive numbers results in a positive number.parameterized-utilsQProduce proof that adding a value to the larger element in an LeqProof is largerparameterized-utilsKProduce proof that subtracting a value from the smaller element is smaller.parameterized-utilsQApply a function to each element in a range; return the list of values obtained.parameterized-utilsbApply a function to each element in a range starting at zero; return the list of values obtained.parameterized-utilsRecursor for natural numbeers.parameterized-utils)Strong induction variant of the recursor.parameterized-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)).parameterized-utilsUsed in Vectorparameterized-utils base case parameterized-utils base case parameterized-utilsinductive step [ OPQRSTUVe[STVOPQRU e.a hash table for parameterized keys and values(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy-H}parameterized-utils&A hash table mapping nonces to values.parameterized-utilsCreate a new empty table.parameterized-utils!Create a new empty table to hold n elements.parameterized-utils6Create a hash table that is a copy of the current one.parameterized-utilsLookup value of key in table.parameterized-utils,Insert new key and value mapping into table.parameterized-utils,Return true if the key is in the hash table.parameterized-utils&Delete an element from the hash table.   &Classes for working with type of kind  (k -> *) -> *(c) Galois, Inc 2014-2019&Langston Barrett <langston@galois.com>Safe-HSUVX)parameterized-utilsnThis instance demonstrates where the above class is useful: namely, in types with existential quantification.Safe&',-.=>?@AHIQSUVX_fparameterized-utilsparameterized-utils conditional parameterized-utilsnegationparameterized-utils Conjunction parameterized-utils Disjunction  e e32(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy&'.=?@AHSUVXparameterized-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 e constructor.parameterized-utils:Generate a value representative for the type level symbol.(c) Galois, Inc 2013-2019!Joe Hendrix <jhendrix@galois.com>None &')@AUVfIzparameterized-utils~A type used to describe (and match) types appearing in generated pattern matches inside of the TH generators in this module (, , , and )parameterized-utilsThe application of a type.parameterized-utilsMatch any type.parameterized-utils;Match the i'th argument of the data type we are traversing.parameterized-utilsMatch a ground type.parameterized-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.parameterized-utilsGFind value associated with first pattern that matches given pat if any.parameterized-utilsstructuralEquality* declares a structural equality predicate.parameterized-utilsMatch equational form.parameterized-utilsstructuralTypeEquality f& returns a function with the type: 4 forall x y . f x -> f y -> Maybe (x :~: y) parameterized-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-utilsrecurseArg f var tp applies f to var where var has type tp.parameterized-utilstraverseAppMatch f cC 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.parameterized-utilsstructuralShow tp% generates a function with the type  tp -> ShowS that shows the constructor. parameterized-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 requiredparameterized-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 indexparameterized-utilsFunction to applyparameterized-utilsPattern match functionparameterized-utils/Function to apply to each argument recursively.parameterized-utilsConstructor to match.parameterized-utilsMatch expression that)*+)*+(c) Galois, Inc 2014-2015!Joe Hendrix <jhendrix@galois.com> Trustworthy-HSUVXi!parameterized-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.1parameterized-utils9A parameterized type that is a function on all instances.parameterized-utilsPThis is a coercion used to avoid overhead associated with function composition.3parameterized-utilsReturn ! if all values satisfy predicate.4parameterized-utilsReturn ! if any values satisfy predicate.5parameterized-utils"Return number of elements in list.6parameterized-utils)This function may be used as a value for fmapF in a FunctorF instance.7parameterized-utils)This function may be used as a value for  in a  instance.8parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.9parameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results. !"#$%&'()*+,-./0123456789*+()./0,-12!"#$%&' 8967345(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy-/HSX<parameterized-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.Aparameterized-utilsNLeft-associative fold of a parameterized structure with a strict accumulator.Bparameterized-utilsConvert structure to list.Cparameterized-utils8A parameterized type that is a functor on all instances.parameterized-utilsPThis is a coercion used to avoid overhead associated with function composition.Eparameterized-utilsReturn % if all values satisfy the predicate.Fparameterized-utilsReturn % if any values satisfy the predicate.Gparameterized-utils)This function may be used as a value for D in a C instance.Hparameterized-utils)This function may be used as a value for  in a  instance.Iparameterized-utilsqMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.Mparameterized-utils"Traverse twice over: go under the t , under the s and lift m out.:;<=>?@ABCDEFGHICD<=>?@AB:;IGHEFSafe&'-HSXPparameterized-utils`Like a 2-tuple, but with an existentially quantified parameter that both of the elements share.Rparameterized-utils$Extract the first element of a pair.Sparameterized-utils%Extract the second element of a pair.Tparameterized-utilsProject out of Pair.PQRSTPQRST!A type-indexed parameterized list(c) Galois, Inc 2017-2019!Joe Hendrix <jhendrix@galois.com>Safe&'-.1>@AHSUVXXparameterized-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 kind[parameterized-utilsParameterized list of elements.^parameterized-utilsReturn the index as an integer._parameterized-utilsIndex 0`parameterized-utilsIndex 1aparameterized-utilsIndex 2bparameterized-utilsIndex 3cparameterized-utils+Return the value in a list at a given indexdparameterized-utils Update the [ at an indexeparameterized-utils@Provides a lens for manipulating the element at the given index.fparameterized-utilsjMap over the elements in the list, and provide the index into each element along with the element itself.gparameterized-utils$Right-fold with an additional index.hparameterized-utilsAZip up two lists with a zipper function, which can use the index.iparameterized-utils"Traverse with an additional index.XYZ[\]^_`abcdefghi[\]XYZ^cdefghi_`ab]5 Trustworthy&'-./=?@AHISUVX 1yparameterized-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-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-utilsThe identity difference.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-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 assignmentparameterized-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-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 treeparameterized-utilsSize of tree to generateparameterized-utilsHeight of each element.parameterized-utilsSize of tree to generateparameterized-utilsHeight of each element.parameterized-utilsBinaparameterized-utilsTree to lookup in.parameterized-utils Size of treeparameterized-utilsTree to lookup in.parameterized-utils Size of treeM<=>?@ABCDEFGHIJyz{|}~>~}|yz{(c) Galois, Inc 2014-2015!Joe Hendrix <jhendrix@galois.com>Safe&'-./=>?@AEHISUVX# 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-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=An indexed singleton type representing 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-utils,The total size of two concatenated contexts.$parameterized-utils6View a size as either zero or a smaller size plus one.%parameterized-utilsThe identity difference.&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.,parameterized-utils#Index for first element in context.-parameterized-utils-Increase context while staying at same index..parameterized-utils1Return the index of an element one past the size./parameterized-utils#Return the last index of a element.2parameterized-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.3parameterized-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.4parameterized-utilsEReturn index at given integer or nothing if integer is out of bounds.6parameterized-utils(Return number of elements in assignment.7parameterized-utilsGenerate an assignment8parameterized-utilsGenerate an assignment9parameterized-utils replicate nE make a context with different copies of the same polymorphic value.:parameterized-utilsCreate empty indexed vector.?parameterized-utilsReturn value of assignment.@parameterized-utils]Return value of assignment, where the index is into an initial sequence of the assignment.parameterized-utilsMap assignmentparameterized-utilsConvert assignment to list.H<=>?@ABCDEFGHIJ   !"#$%&'()*+,-./0123456789:;<=>?@ABCD9 !"(#$%&'*)+,-/.012346978:;<=>  5?@BADC(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com> Trustworthy%,-./=>?@ACHSUVXgk@parameterized-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 -> xparameterized-utilsClass for computing ~ values for positions in a E.parameterized-utils'Constraint synonym used for getting an ~ into a E. 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 E. 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-utilsInductive-stepparameterized-utils Base-case<=>?@ABCDEFGHIJyz{|}~D 3Representations of a type-level natural at runtime.(c) Galois, Inc 2019None&',-.=>?@AHIQSUVX_ff)parameterized-utilsImplicit runtime representationparameterized-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 contextparameterized-utilsApply a constructor f n-times to an argument sparameterized-utilsMinimumparameterized-utilsMaximumparameterized-utilsGreater-than-or-equalparameterized-utils Greater-thanparameterized-utils Less-thanparameterized-utilsLess-than-or-equalparameterized-utilsMultiplicationparameterized-utils Subtractionparameterized-utilsAdditionparameterized-utilsPeano successorparameterized-utils Peano zeroparameterized-utils(Unary representation for natural numbersparameterized-utils*Test whether a number is Zero or Successorparameterized-utils3convert the view back to the runtime representationparameterized-utilsZeroparameterized-utilsSuccessor, Incrementparameterized-utilsGet the predecessor (decrement)parameterized-utilsAdditionparameterized-utils Subtractionparameterized-utilsMultiplicationparameterized-utilsMaximumparameterized-utilsMinimumparameterized-utilsLess-than-or-equal-toparameterized-utils Less-thanparameterized-utilsGreater-than-or-equal-toparameterized-utils Greater-thanparameterized-utilsApply a constructor f n-times to an argument sparameterized-utilsCalculate the size of a contextparameterized-utils Convert a  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.parameterized-utilsList length as a Peano numberparameterized-utils)Context size commutes with context appendparameterized-utilsMinus distributes over plus parameterized-utils%We can reshuffle minus with less than1 e 1 e Safehu  !"#$%&'()*+,-./0123456<=>?@ABCDEFGHIJOPQRSTUVefghij !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIPQRST$Utilities for balanced binary trees.(c) Galois, Inc 2014-2019!Joe Hendrix <jhendrix@galois.com>Safe %&',>@ACXparameterized-utils A Strict pairparameterized-utils Updated aT contains a value that has been flagged on whether it was modified by an operation."parameterized-utilsA strict version of 'parameterized-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.parameterized-utilsInsert a new maximal element.parameterized-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.parameterized-utilsMInsert a new key and value in the map if it is not already present. Used by 0.0parameterized-utilsUnion two setsparameterized-utils]Hedge union where we only add elements in second map if key is strictly above a lower bound.parameterized-utils]Hedge union where we only add elements in second map if key is strictly below a upper bound.parameterized-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. !"$#%&'()*+,-./0"$#% !&'(,*./+-0)2Finite maps with parameterized key and value types(c) Galois, Inc 2014-2019 Trustworthy&'-./=?@AHSUVXr*4parameterized-utils4$ tells what to do with a found value5parameterized-utilsKeep the current value.6parameterized-utilsSet the value to a new value.7parameterized-utilsDelete a value.8parameterized-utilsEA map from parameterized keys to values with the same parameter type.9parameterized-utilsReturn empty map:parameterized-utilsReturn true if map is empty;parameterized-utils&Return map containing a single element<parameterized-utils&Apply function to all elements in map.=parameterized-utilsModify elements in a map>parameterized-utils"Map keys and elements and collect  results.?parameterized-utilsMap elements and collect  results.parameterized-utilsTraverse elements in a map@parameterized-utilsTraverse elements in a mapAparameterized-utils4Traverse elements in a map without returning result.Bparameterized-utilsLookup value in map.Cparameterized-utils#Return true if key is bound in map.Dparameterized-utils'Return true if key is not bound in map.Eparameterized-utils.Return all keys of the map in ascending order.Fparameterized-utilsDReturn all elements of the map in the ascending order of their keys.Gparameterized-utils/Perform a left fold with the key also provided.Hparameterized-utils6Perform a strict left fold with the key also provided.Iparameterized-utils0Perform a right fold with the key also provided.Jparameterized-utils7Perform a strict right fold with the key also provided.Kparameterized-utils0Fold the keys and values using the given monoid.Lparameterized-utils4Return entries with values that satisfy a predicate.Mparameterized-utils0Return key-value pairs that satisfy a predicate.Nparameterized-utils filterGt k m returns submap of m2 that only contains entries that are larger than k.Oparameterized-utils filterLt k m returns submap of m3 that only contains entries that are smaller than k.Pparameterized-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.Qparameterized-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 $ value if a new entry was inserted.Rparameterized-utils'Delete a value from the map if present.Sparameterized-utilsUnion two setsTparameterized-utils\Log-time algorithm that allows a value at a specific key to be added, replaced, or deleted.Uparameterized-utils"Create a Map from a list of pairs.Wparameterized-utilsVGenerate a map from a foldable collection of keys and a function from keys to values.Xparameterized-utils^Generate a map from a foldable collection of keys and a monadic function from keys to values.Yparameterized-utils*Merge bindings in two maps to get a third.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.aparameterized-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.Tparameterized-utils Key to updateparameterized-utils"Action to call if nothing is foundparameterized-utils!Action to call if value is found.parameterized-utils Map to updateWparameterized-utils)Function for evaluating a register value.parameterized-utilsSet of X86 registersXparameterized-utilsFFunction for evaluating an input value to store the result in the map.parameterized-utils+Set of input values (traversed via folding)[  !"#$%&'()*+,-./0123456PQ !&467589:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXY-89;PQRS:BCDEFUVWXLMNOGHIJK=<?>@A4675 !&TYPQ9A common location for defining multi-byte value ordering.(c) Galois, Inc 2019Safe}bparameterized-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 ]bcdbcd(c) Galois, Inc 2014-2019None&'.IQSUVXk7#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.hparameterized-utilsFixed-size non-empty vectors.iparameterized-utils=Get the elements of the vector as a list, lowest index first.jparameterized-utilsLength of the vector. O(1)kparameterized-utilsThe length of the vector as an Int.mparameterized-utils%Get the element at the given index. O(1)nparameterized-utilshGet the element at the given index. Raises an exception if the element is not in the vector's domain. O(1)oparameterized-utils'Insert an element at the given index. O(n).pparameterized-utils.Insert an element at the given index. Return / if the element is outside the vector bounds. O(n).qparameterized-utils.Proof that the length of this vector is not 0.rparameterized-utilsDRemove the first element of the vector, and return the rest, if any.sparameterized-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).tparameterized-utils(Extract a subvector of the given vector.uparameterized-utils2Take the front (lower-indexes) part of the vector.vparameterized-utils.Zip two vectors, potentially changing types. O(n)yparameterized-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. zparameterized-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 ] tparameterized-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$hijklmnopqrstuvwxyz{|}~$hsijqklmnoprtuvwxyz{|}~(c) Galois, Inc 2019None &'-=HSX:parameterized-utils@Turn an explicit Repr value into an implict KnownRepr constraint!"#$%&$'(!)*!)+!),!)-!./!.0!.1!.2!3456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqporstuvwxyz{|} ~      ~                     !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghhijklmnopqrstuvwxyz{|}~oz     oz      !"#$%&''()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~1,AA6,! !    $'z!$'!!!!! !"#$!%&$''&($')*+,-./0!12345678!9:!;<=>?@AB!;CDEFGH!;IJK.parameterized-utils-2.0-5EcWvL4VBZEIQmbRZzaRMZData.Parameterized.SymbolReprData.Parameterized.HashTableData.Parameterized.NatReprData.Parameterized.ClassesData.Parameterized.ComposeData.Parameterized.CtxData.Parameterized.Ctx.ProofsData.Parameterized.DecidableEqData.Parameterized.Nonce.UnsafeData.Parameterized.SomeData.Parameterized.Nonce%Data.Parameterized.Nonce.TransformersData.Parameterized.ClassesCData.Parameterized.BoolReprData.Parameterized.TH.GADT Data.Parameterized.TraversableFCData.Parameterized.TraversableFData.Parameterized.PairData.Parameterized.List!Data.Parameterized.Context.UnsafeData.Parameterized.Context.SafeData.Parameterized.ContextData.Parameterized.Peano Data.Parameterized.Utils.BinTreeData.Parameterized.MapData.Parameterized.Utils.EndianData.Parameterized.VectorData.Parameterized.WithRepr#Data.Parameterized.NatRepr.Internal Data.FoldablefoldMapData.Parameterizedbase GHC.TypeLits KnownSymbolghc-primGHC.Prim RealWorld GHC.TypesSymbol GHC.TypeNats+*-<=Data.Type.EqualityRefl:~: testEquality TestEquality Data.MaybeisJusttestEqualityComposeBare$fTestEqualitykCompose KnownRepr knownRepr HashableF hashWithSaltFhashFAtFatFIxedF'ixF'IxedFixFIxValueFIndexFShowFwithShowshowF showsPrecFOrdFcompareFleqFltFgeqFgtF OrderingFLTFEQFGTFPolyEqpolyEqFpolyEqEqFeqF CoercibleFcoerceForderingF_refl toOrdering fromOrdering joinOrderingF lexCompareF ordFComposeshowsF$fCoercibleFkConst $fEqFkConst$fOrdFkCompose $fShowFkConst$fHashableFkConst CtxUpdate CtxLookupCtxUpdateRightCtxLookupRightFromLeftValidIxCheckIxCtxSize<+>CtxEmptyCtx::> SingleCtxleftIdassoc DecidableEqdecEq NatComparisonNatLTNatEQNatGTNatReprnatValue compareNatknownNatNonce indexValueNonceGeneratornewNonceGenerator freshNonceatLimit $fShowFkNonce$fHashableFkNonce $fOrdFkNonce$fTestEqualitykNonce $fEqNonce $fOrdNonce$fHashableNonce $fShowNonceSomeviewSomemapSome traverseSome traverseSome_ $fShowSome$fHashableSome $fOrdSome$fEqSomeGlobalNonceGeneratorcountNoncesGeneratednewSTNonceGeneratornewIONonceGeneratorwithSTNonceGeneratorwithIONonceGeneratorglobalNonceGeneratorwithGlobalSTNonceGeneratorNonceIONonceSTNonceT 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$fHashableBoolRepr SymbolRepr symbolRepr someSymbol knownSymbol$fShowFSymbolSymbolRepr$fShowSymbolRepr$fHashableSymbolRepr$fHashableFSymbolSymbolRepr$fOrdSymbolRepr$fEqSymbolRepr$fOrdFSymbolSymbolRepr$fTestEqualitySymbolSymbolRepr$fKnownReprSymbolSymbolReprsTypePatTypeAppAnyTypeDataArgConTypeDataDlookupDataType'conPatdataParamTypes assocTypePatsstructuralEqualitystructuralTypeEqualitystructuralTypeOrdstructuralTraversal asTypeConstructuralHashstructuralShowsPrec TraversableFC traverseFC FoldableFC foldMapFCfoldrFCfoldlFCfoldrFC'foldlFC'toListFCOrdFC compareFCTestEqualityFCtestEqualityFC HashableFChashWithSaltFCShowFCshowFC showsPrecFC FunctorFCfmapFCallFCanyFClengthFC fmapFCDefaultfoldMapFCDefault traverseFC_forMFC_ TraversableF traverseF FoldableFfoldMapFfoldrFfoldlFfoldrF'foldlF'toListFFunctorFfmapFallFanyF fmapFDefaultfoldMapFDefault traverseF_$fFunctorFlCompose$fFunctorFkConst$fFoldableFkConst$fTraversableFlCompose$fFoldableFlCompose$fTraversableFkConstPairfstPairsndPairviewPair$fFoldableFkPair$fFunctorFkPair$fEqPairIndex IndexHere IndexThereListNil:<index0index1index2index3!!updateindexedimapifoldrizipWith itraverse$fKnownRepr[]List:$fKnownRepr[]List[] $fOrdF[]List$fTestEquality[]List$fTraversableFCk[]List$fFoldableFCk[]List$fFunctorFCk[]List $fShowF[]List $fShowList $fOrdIndex $fOrdFkIndex$fTestEqualitykIndex $fShowFkIndex $fShowIndex $fEqIndex AssignView AssignEmpty AssignExtend Assignment IndexRangeindexVal KnownDiff knownDiffDiffViewNoDiffExtendRightDiffIsAppendDiff KnownContext knownSizeSizeViewZeroSizeIncSizeSizesizeIntzeroSizeincSizedecSizeviewSizenoDiff extendRight appendDiffextSizeaddSize diffIsAppendviewDiff baseIndex skipIndex nextIndex lastIndex extendIndex extendIndex'forIndex forIndexRangeintIndexallRange indexOfRange dropTailRange dropHeadRangesize replicategenerate generateMemptyextend!!^adjustadjustM viewAssignzipWithzipWithMtraverseWithIndex<++> $fShowSize$fKnownContextk::>$fKnownContextkEmptyCtx$fCategoryCtxDiff$fKnownDiffkl::>$fKnownDiffkll$fHashableIndex$fHashableFkIndex$fShowFCtxBalancedTree$fShowBalancedTree$fHashableFCtxBalancedTree$fOrdFCkCtxBalancedTree $fTestEqualityFCkCtxBalancedTree$fHashableFCtxBinomialTree$fOrdFCkCtxBinomialTree $fTestEqualityFCkCtxBinomialTree $fKnownReprCtxAssignmentEmptyCtx$fKnownReprCtxAssignment::>$fTraversableFCkCtxAssignment$fFoldableFCkCtxAssignment$fFunctorFCkCtxAssignment$fIxedFkAssignment$fIxedF'kAssignment$fShowFCtxAssignment$fShowAssignment$fHashableFCtxAssignment$fHashableAssignment$fOrdAssignment$fOrdFCtxAssignment$fOrdFCkCtxAssignment$fEqAssignment$fTestEqualityCtxAssignment$fTestEqualityFCkCtxAssignment$fNFDataAssignment$fField1AssignmentAssignmentff$fField2AssignmentAssignmentff$fField1AssignmentAssignmentff0$fField3AssignmentAssignmentff$fField2AssignmentAssignmentff0$fField1AssignmentAssignmentff1$fField4AssignmentAssignmentff$fField3AssignmentAssignmentff0$fField2AssignmentAssignmentff1$fField1AssignmentAssignmentff2$fField5AssignmentAssignmentff$fField4AssignmentAssignmentff0$fField3AssignmentAssignmentff1$fField2AssignmentAssignmentff2$fField1AssignmentAssignmentff3$fField6AssignmentAssignmentff$fField5AssignmentAssignmentff0$fField4AssignmentAssignmentff1$fField3AssignmentAssignmentff2$fField2AssignmentAssignmentff3$fField1AssignmentAssignmentff4$fField7AssignmentAssignmentff$fField6AssignmentAssignmentff0$fField5AssignmentAssignmentff1$fField4AssignmentAssignmentff2$fField3AssignmentAssignmentff3$fField2AssignmentAssignmentff4$fField1AssignmentAssignmentff5$fField8AssignmentAssignmentff$fField7AssignmentAssignmentff0$fField6AssignmentAssignmentff1$fField5AssignmentAssignmentff2$fField4AssignmentAssignmentff3$fField3AssignmentAssignmentff4$fField2AssignmentAssignmentff5$fField1AssignmentAssignmentff6$fField9AssignmentAssignmentff$fField8AssignmentAssignmentff0$fField7AssignmentAssignmentff1$fField6AssignmentAssignmentff2$fField5AssignmentAssignmentff3$fField4AssignmentAssignmentff4$fField3AssignmentAssignmentff5$fField2AssignmentAssignmentff6$fField1AssignmentAssignmentff7$fPolyEqAssignmentAssignmentCurryAssignmentClasscurryAssignmentuncurryAssignmentCurryAssignmentIdxExtendContext'extendContext' ExtendContext extendContextApplyEmbedding'applyEmbedding'ApplyEmbeddingapplyEmbedding CtxEmbedding _ctxeSize_ctxeAssignment:>Empty singleton forIndexM generateSome generateSomeMtoVectornull decomposeinitlastviewtakectxeSizectxeAssignmentidentityEmbeddingextendEmbeddingRightDiffextendEmbeddingRightappendEmbeddingextendEmbeddingBothfieldnatIndex natIndexProxyfromListtraverseAndCollectsize1size2size3size4size5size6i1of2i2of2i1of3i2of3i3of3i1of4i2of4i3of4i4of4i1of5i2of5i3of5i4of5i5of5i1of6i2of6i3of6i4of6i5of6i6of6$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_ notMemberkeyselems foldlWithKey foldlWithKey' foldrWithKey foldrWithKey'foldMapWithKeyfilter filterWithKey insertWith updateAtKeytoListfromKeys 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 defaultSalt'hashable-1.2.7.0-2SI038axTEd7AEZJ275kpiData.Hashable.ClasshashNatGHC.STSTIOGHC.RealmodData.Type.BoolIf&&||NotconExprmkEqFnewNamesjoinCompareToOrdFmatchOrdArgumentsmkOrdF recurseArgtraverseAppMatchmatchEqArguments mkSimpleEqF mkSimpleOrdFFoldable#.True BalancedTreeIntunsafe_bal_indexunsafe_bal_adjust bal_zipWithMfmap_binbal_dropunsafe_bin_indexunsafe_bin_adjustGHC.Base Applicative unsafeIndexunsafe_bal_generateunsafe_bal_generateMunsafe_bin_generateunsafe_bin_generateMIdx'GHC.WordWord64 GHC.MaybeMaybe insertMax insertMininsertR hedgeUnion_LB hedgeUnion_UBhedgeUnion_LB_UBJusttraverseinsertWithImpl filterMiddleatKey'Vector'NothingvAppend