h&b=I      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[ \ ]^_`abcde f g h i j k l m n o p q r s t u v w x y z { | } ~                                                                                 !!!!!!!!&(c) Galois, Inc 2014-2021Unsafe0parameterized-utilsAssert a proof of equality between two types. This is unsafe if used improperly, so use this with caution!parameterized-utilsAssert a proof of heterogeneous equality between two types. This is unsafe if used improperly, so use this with caution!utilities for working with Data.Functor.Compose(c) Galois, Inc 2014-2019&Langston Barrett Safe )*0parameterized-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 Safe)*0<'fparameterized-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 Ixed class, but with the guarantee that indexes exist in the container.parameterized-utilsGiven 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-utilsGiven 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-utilsThe % class is a total ordering over parameterized types so that types with different parameters can be compared. Instances of %, are expected to satisfy the following laws:  Transitivityif leqF x y && leqF y z = , then  leqF x = z = True ReflexivityleqF x x = True Antisymmetryif leqF x y && leqF y x = , then testEquality x y =  Just ReflNote that the following operator interactions are expected to hold:geqF x y iff leqF y xltF x y iff &leqF x y && testEquality x y = NothinggtF x y iff ltF y xltF x y iff compareF x y == LTFgtF x y iff compareF x y == GTFisJust (testEquality x y) iff compareF x y == EQFFurthermore, when x and y both have type (k tp) , we expect:toOrdering (compareF x y) equals  compare x y when  Ord (k tp) has an instance.isJust (testEquality x y) equals x == y when  Eq (k tp) has an instance.$Minimal complete definition: either & or ' . Using &) can be more efficient for complex types.+parameterized-utils=Ordering over two distinct types with a proof they are equal./parameterized-utils1A polymorphic equality operator that generalizes .2parameterized-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.4parameterized-utilsAn instance of 4 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 rtp is a phantom type by giving an implementation in terms of Data.Coerce.coerce.7parameterized-utilsConvert + to standard ordering.8parameterized-utilsConvert standard ordering to +.9parameterized-utilsjoinOrderingF x y first compares on x., returning an equivalent value if it is not - . If it is - , it returns y.:parameterized-utilsCompare 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 23/01%&'()*:+,-.9678;!"#$<45  Type-level lists.(c) Galois, Inc 2015-2019!Joe Hendrix Safe /01-C Iparameterized-utilsFlatten a nested contextJparameterized-utilsUpdate the value in a context by number, from the left. If the index is out of range, the context is unchanged.Kparameterized-utilsLookup the value in a context by number, from the left. Produce a type error if the index is out of range.Lparameterized-utilsUpdate the value in a context by number, from the right. If the index is out of range, the context is unchanged.Mparameterized-utils7Lookup the value in a context by number, from the rightNparameterized-utilsS 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.Oparameterized-utils&A constraint that checks that the nat n& is a valid index into the context ctx!, and raises a type error if not.Pparameterized-utilsHelper type family used to generate descriptive error messages when an index is larger than the length of the S being indexed.Qparameterized-utils6This type family computes the number of elements in a SRparameterized-utilsAppend two type-level contexts.Sparameterized-utilsKind S k" comprises lists of types of kind k.IJKLMNOPQRSTUVWXSTUXVWRQKJMLIPON$type-level proofs involving contexts(c) Galois, Inc 2015-2019!Joe Hendrix  Safe-Inferred0-YZYZ Decideable equality (i.e. evidence of non-equality) on type families(c) Galois, Inc 2014-2019&Langston Barrett Safe 0.[parameterized-utilsDecidable equality.[\[\"(c) Galois, Inc 2014-2018!Joe Hendrix  Safe-Inferred)*0160]parameterized-utils Result of comparing two numbers.aparameterized-utils'A runtime presentation of a type-level .This can be used for performing dynamic checks on a type-level natural numbers.bparameterized-utils+The underlying natural value of the number.dparameterized-utils3This generates a NatRepr from a type-level context. ]`_^abcd A counter in the ST monad.(c) Galois, Inc 2014!Joe Hendrix  provisionalUnsafe03,eparameterized-utils"An index generated by the counter.gparameterized-utils4A simple type that for getting fresh indices in the  monad. The type parameter s is used for the  monad parameter.hparameterized-utilsCreate a new counter.iparameterized-utils,Get a fresh index and increment the counter.jparameterized-utilsReturn true if counter has reached the limit, and can't be incremented without risk of error.efghijghijef 8Template Haskell primitives for working with large GADTs(c) Galois, Inc 2013-2019!Joe Hendrix  Safe-Inferred )*Ysparameterized-utilsA type used to describe (and match) types appearing in generated pattern matches inside of the TH generators in this module (}, ~, , and )tparameterized-utilsThe application of a type.uparameterized-utilsMatch any type.vparameterized-utils;Match the i'th argument of the data type we are traversing.wparameterized-utilsMatch a ground type.zparameterized-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-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*.|parameterized-utilsFind 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-utilsGenerate a list of fresh names using the base name and numbered 1 to n* to make them useful in conjunction with -dsuppress-uniques.parameterized-utilsCompare 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  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  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.The second arguments is for generating user-defined patterns to replace   for specific types.parameterized-utilsThis 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.parameterized-utilsGenerate a "repr" or singleton type from a data kind. For nullary constructors, this works as follows: data T1 = A | B | C $(mkRepr ''T1) ======> data T1Repr (tp :: T1) where ARepr :: T1Repr 'A BRepr :: T1Repr 'B CRepr :: T1Repr 'C 8For constructors with fields, we assume each field type T( already has a corresponding repr type TRepr :: T -> *. data T2 = T2_1 T1 | T2_2 T1 $(mkRepr ''T2) ======> data T2Repr (tp :: T2) where T2_1Repr :: T1Repr tp -> T2Repr ('T2_1 tp) T2_2Repr :: T1Repr tp -> T2Repr ('T2_2 tp) 4Constructors with multiple fields work fine as well: data T3 = T3 T1 T2 $(mkRepr ''T3) ======> data T3Repr (tp :: T3) where T3Repr :: T1Repr tp1 -> T2Repr tp2 -> T3Repr ('T3 tp1 tp2) This is generally compatible with other "repr" types provided by parameterized-utils , such as NatRepr and  PeanoRepr: data T4 = T4_1 Nat | T4_2 Peano $(mkRepr ''T4) ======> data T4Repr (tp :: T4) where T4Repr :: NatRepr tp1 -> PeanoRepr tp2 -> T4Repr ('T4 tp1 tp2) The data kind must be "simple", i.e. it must be monomorphic and only contain user-defined data constructors (no lists, tuples, etc.). For example, the following will not work: data T5 a = T5 a $(mkRepr ''T5) ======> Foo.hs:1:1: error: Exception when trying to run compile-time code: mkRepr cannot be used on polymorphic data kinds. Similarly, this will not work: data T5 = T5 [Nat] $(mkRepr ''T5) ======> Foo.hs:1:1: error: Exception when trying to run compile-time code: mkRepr cannot be used on this data kind. Note that at a minimum, you will need the following extensions to use this macro: {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE TemplateHaskell #-} parameterized-utils Generate  KnownRepr instances for each constructor of a data kind. Given a data kind T, we assume a repr type TRepr (t :: T)4 is in scope with structure that perfectly matches T (using 1 to generate the repr type will guarantee this).Given data kinds T1, T2, and T3 from the documentation of !, and the associated repr types T1Repr, T2Repr, and T3Repr, we can use % to generate these instances like so: $(mkKnownReprs ''T1) ======> instance KnownRepr T1Repr 'A where knownRepr = ARepr instance KnownRepr T1Repr 'B where knownRepr = BRepr instance KnownRepr T1Repr 'C where knownRepr = CRepr  $(mkKnownReprs ''T2) ======> instance KnownRepr T1Repr tp => KnownRepr T2Repr ('T2_1 tp) where knownRepr = T2_1Repr knownRepr  $(mkKnownReprs ''T3) ======> instance (KnownRepr T1Repr tp1, KnownRepr T2Repr tp2) => KnownRepr T3Repr ('T3_1 tp1 tp2) where knownRepr = T3_1Repr knownRepr knownRepr $The same restrictions that apply to  also apply to . The data kind must be "simple", i.e. it must be monomorphic and only contain user-defined data constructors (no lists, tuples, etc.).Note that at a minimum, you will need the following extensions to use this macro: {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TemplateHaskell #-} Also,  must be used in the same module as the definition of the repr type (not necessarily for the data kind). zparameterized-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-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/01swtuvxyz{|}~}~/01xyzswtuv{|  Safe-Inferred )*015Y Traversing structures having a single parametric type followed by a fixed kind.(c) Galois, Inc 2014-2015!Joe Hendrix  Trustworthy0eparameterized-utils This is a generalization of the / class to structures over parameterized terms.parameterized-utilsMap 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-utilsRight-associative fold of a structure, but with strict application of the operator.parameterized-utilsLeft-associative fold of a parameterized structure with a strict accumulator.parameterized-utilsConvert structure to list.parameterized-utilsA parameterized class for types which can be tested for parameterized ordering, when given an comparison test for subterms.parameterized-utilsA parameterized class for types which can be tested for parameterized equality, when given an equality test for subterms.parameterized-utilsA parameterized class for types which can be hashed, when given functions to hash parameterized subterms.parameterized-utilsA parameterized class for types which can be shown, when given functions to show parameterized subterms.parameterized-utils8A parameterized type that is a functor on all instances.Laws: Identity  ==  Composition (f . g) ==  f .  gparameterized-utilsThis is a coercion used to avoid overhead associated with function composition.parameterized-utilsMonadic fold over the elements of a structure from left to right.parameterized-utilsMonadic strict fold over the elements of a structure from left to right.parameterized-utilsMonadic fold over the elements of a structure from right to left.parameterized-utilsMonadic 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-utilsMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsFlipped !!5Traversing structures having a single parametric type(c) Galois, Inc 2014-2019!Joe Hendrix  Trustworthy02nparameterized-utils This is a generalization of the / class to structures over parameterized terms.parameterized-utilsMap 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-utilsRight-associative fold of a structure, but with strict application of the operator.parameterized-utilsLeft-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-utilsThis is a coercion used to avoid overhead associated with function composition.parameterized-utilsMonadic fold over the elements of a structure from left to right.parameterized-utilsMonadic strict fold over the elements of a structure from left to right.parameterized-utilsMonadic fold over the elements of a structure from right to left.parameterized-utilsMonadic 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-utilsMap each element of a structure to an action, evaluate these actions from left to right, and ignore the results.parameterized-utilsMap 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."a GADT that hides a type parameter(c) Galois, Inc 2014-2019!Joe Hendrix  Safe-Inferred)*0qparameterized-utilsProject out of Some.parameterized-utilsApply function to inner value.parameterized-utilsModify the inner value.parameterized-utilsModify the inner value.parameterized-utilsA lens that is polymorphic in the index may be used on a value with an existentially-quantified index.a type family for representing a type-level string (AKA symbol) at runtime(c) Galois, Inc 2014-2019!Joe Hendrix  Trustworthy)*1tparameterized-utilsThe SomeSym hides a Symbol parameter but preserves a KnownSymbol constraint on the hidden parameter.parameterized-utils4A runtime representation of a GHC type-level symbol.parameterized-utils0The underlying text representation of the symbolparameterized-utilsGenerate 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.parameterized-utilsProjects a value out of a SomeSym into a function, re-ifying the Symbol type parameter to the called function, along with the KnownSymbol constraint on that Symbol value.   Index generator in the ST monad.(c) Galois, Inc 2014-2019!Joe Hendrix  Trustworthy )*0z parameterized-utils"An index generated by the counter.parameterized-utils8Provides a monadic action for getting fresh typed names.The first type parameter m is the monad used for generating names, and the second parameter s is used for the counter.parameterized-utilsThe 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  to create a nonce generator that shares the same phantom type parameter as the ST monad.This 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 an / computation with a new nonce generator in the  monad.parameterized-utilsRun an / computation with 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  Safe-Inferred0}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  Trustworthy)*168+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-utilsReturn minimum unsigned value for bitvector with given width (always 0).parameterized-utils=Return maximum unsigned value for bitvector with given width.parameterized-utilsReturn minimum value for bitvector in two's complement with given width.parameterized-utilsReturn 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 i 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 associative.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-utils.The strict order on the naturals is asymmetricparameterized-utilsx  y checks whether x is less than or equal to y.parameterized-utilsApply reflexivity to LeqProofparameterized-utilsApply transitivity to LeqProofparameterized-utils"Zero is less than or equal to any .parameterized-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-utilsProduce proof that adding a value to the larger element in an LeqProof is largerparameterized-utilsProduce proof that subtracting a value from the smaller element is smaller.parameterized-utilsApply a function to each element in a range; return the list of values obtained.parameterized-utilsApply 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-utils A version of  which doesn't require the type index of the result to be greater than 0- and provides a strict inequality constraint.parameterized-utilsUsed in Vectorparameterized-utils base case parameterized-utils base case parameterized-utilsinductive step  ]^_`abcdabd]^_`c (c) Galois, Inc 2021 Safe-Inferred )*1parameterized-utils The type  n has exactly n inhabitants.parameterized-utilsCount all of the numbers up to m that meet some condition.parameterized-utilsThe smallest element of  nparameterized-utils/Non-lawful instance, intended only for testing.  .a hash table for parameterized keys and values(c) Galois, Inc 2014-2019!Joe Hendrix  Trustworthy0parameterized-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  Trustworthy0^parameterized-utilsThis instance demonstrates where the above class is useful: namely, in types with existential quantification. Safe-Inferred)*/01vparameterized-utilsA Boolean flagparameterized-utils conditionalparameterized-utilsnegationparameterized-utils Conjunctionparameterized-utils Disjunction  321A 2-tuple with identically parameterized elements(c) Galois, Inc 2017-2019 Safe-Inferred)*0cparameterized-utilsLike a 2-tuple, but with an existentially quantified parameter that both of the elements share.parameterized-utils$Extract the first element of a pair.parameterized-utils%Extract the second element of a pair.parameterized-utilsProject out of Pair.'Universal quantification, in a datatype(c) Galois, Inc 2019&Langston Barrett  Safe-Inferred0 % Safe-Inferred?   !$"#%*)(&'+.,-/0123456789:; Safe-Inferred)*015parameterized-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-utils5Apply function to list to yield a parameterized list.parameterized-utils;Apply monadic action to list to yield a parameterized list.parameterized-utils"Map from list of Some to Some listparameterized-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-utilsProvides a lens for manipulating the element at the given index.parameterized-utilsMap over the elements in the list, and provide the index into each element along with the element itself.This is a specialization of .parameterized-utils#Left fold with an additional index.parameterized-utils$Right-fold with an additional index.This is a specialization of .parameterized-utilsZip up two lists with a zipper function, which can use the index.parameterized-utils"Traverse with an additional index.This is a specialization of .5& Trustworthy)*0125;parameterized-utilsRepresent 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.The first parameter is the height of the tree. The second is the parameterized value.parameterized-utils.This represents a contiguous range of indices.parameterized-utilsView of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.parameterized-utilsAn index is a reference to a position with a particular type in a context.parameterized-utilsA difference that can be automatically inferred at compile time.parameterized-utils Proof that r = l  + app for some appparameterized-utilsDifference 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 Convert a  into a a.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-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-utilsAdapts an index in the left hand context of an append operation.parameterized-utilsAdapts an index in the right hand context of an append operation.parameterized-utils Compute an  into a context r from an  into a sub-context l of r.parameterized-utils Compute an " into an appended context from an  into its suffix.parameterized-utils Given a size n , a function f, and an initial value v0, the expression forIndex n f v0 is equivalent to v0 when n is zero, and f (forIndex (n-1) f v0) n9 otherwise. Unlike the safe version, which starts from  0 and increments ! values, this version starts at  (n-1) and decrements  values to  0.parameterized-utilsGiven an index i, size n , a function f, and a value v, the expression forIndex i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n f v) otherwise.parameterized-utilsReturn 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 n 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*Extend an indexed vector with a new entry.parameterized-utils>Unexported index that returns an arbitrary type of expression.parameterized-utilsReturn value of assignment.parameterized-utilsReturn 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-utilsView 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 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 treeIJKLMNOPQRSTUVWX(c) Galois, Inc 2014-2019!Joe Hendrix  Trustworthy(/012"parameterized-utilsThis class implements two methods that witness the isomorphism between curried and uncurried functions.parameterized-utilsTransform a function that accepts an assignment into one with a separate variable for each element of the assignment.parameterized-utilsTransform 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 S.parameterized-utils'Constraint synonym used for getting an  into a S. 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-utilsGenerate an assignment with some context type that is not known.parameterized-utilsGenerate an assignment with some context type that is not known.parameterized-utils#Convert the assignment to a vector.parameterized-utils Utility function for testing if xs is an assignment with prefix as a prefix, and computing the tail of xs not in the prefix, if so.parameterized-utils8Unzip an assignment of pairs into a pair of assignments.This is the inverse of  .parameterized-utils8Flattens a nested assignment over a context of contexts ctxs :: Ctx (Ctx a)3 into a flat assignment over the flattened context CtxFlatten ctxs.parameterized-utils"Given the size of each context in ctxs, returns the size of CtxFlatten ctxs8. You can obtain the former from any nested assignment Assignment (Assignment f) ctxs , by calling  fmapFC size.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-utilsView an assignment as either empty or an assignment with one appended.parameterized-utils!Return the prefix of an appended parameterized-utils!Return the suffix of an appended parameterized-utilsProve that the prefix of an appended context is embeddable in itparameterized-utilsProve that the suffix of an appended context is embeddable in itparameterized-utils!Get a lens for an position in an  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 S. The TypeApplications 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  Assignment 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.parameterized-utilsInductive-stepparameterized-utils Base-caseparameterized-utilsAssignment to split parameterized-utilsExpected prefix parameterized-utilserror continuation parameterized-utilssuccess continuation IJKLMNOPQRSTUVWX 3Representations of a type-level natural at runtime.(c) Galois, Inc 2019 Safe-Inferred)*/01)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-utilsThe 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 plusparameterized-utils%We can reshuffle minus with less than1 1 '(c) Galois, Inc 2014-2015!Joe Hendrix  Safe-Inferred)*01250parameterized-utilsView 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-utilsView of indexes as pointing to the last element in the index range or pointing to an earlier element in a smaller range.parameterized-utilsAn index is a reference to a position with a particular type in a context.parameterized-utilsA difference that can be automatically inferred at compile time.parameterized-utils Proof that r = l  + app for some appparameterized-utilsDifference 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-utils Convert a  into a a.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  + appparameterized-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.parameterized-utilsAdapts an index in the left hand context of an append operation.parameterized-utilsAdapts an index in the right hand context of an append operation.parameterized-utils Compute an  into a context r from an  into a sub-context l of r.parameterized-utils Compute an " into an appended context from an  into its suffix.parameterized-utils Given a size n , a function f, and an initial value v0, the expression forIndex n f v0 calls f on each index less than n starting from 0 and v0, with the value v obtained from the last call.parameterized-utilsGiven an index i, size n , a function f, and a value v, the expression forIndexRange i n f v is equivalent to v when i >= sizeInt n, and f i (forIndexRange (i+1) n f v) otherwise.parameterized-utilsReturn index at given integer or nothing if integer is out of bounds.parameterized-utilsProject an indexparameterized-utils(Return number of elements in assignment.parameterized-utilsGenerate an assignmentparameterized-utilsGenerate an assignmentparameterized-utils replicate n make a context with different copies of the same polymorphic value.parameterized-utilsCreate empty indexed vector.parameterized-utils*Extend an indexed vector with a new entry.parameterized-utilsReturn value of assignment.parameterized-utilsReturn value of assignment, where the index is into an initial sequence of the assignment.parameterized-utilsMap assignmentparameterized-utilsConvert assignment to list.parameterized-utilsThis is a specialization of .parameterized-utilsRenders as integer literalparameterized-utilsImplemented with  and parameterized-utilsRenders as integer literalIJKLMNOPQRSTUVWX$Utilities for balanced binary trees.(c) Galois, Inc 2014-2019!Joe Hendrix Safe ()*/nparameterized-utils A Strict pairparameterized-utils Updated a 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-utilslink is called to insert a key and value between two disjoint subtrees.parameterized-utilsConcatenate two trees that are ordered with respect to each other.parameterized-utils insert p m inserts the binding into m. 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-utilsReturns 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-utilsInsert a new key and value in the map if it is not already present. Used by .parameterized-utilsUnion two setsparameterized-utilsHedge union where we only add elements in second map if key is strictly above a lower bound.parameterized-utilsHedge union where we only add elements in second map if key is strictly below a upper bound.parameterized-utilsHedge 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.2Finite maps with parameterized key and value types(c) Galois, Inc 2014-2019 Trustworthy)*02M4parameterized-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-utilsA 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  results.parameterized-utilsMap elements and collect  results.parameterized-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  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-utilsReturn 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.parameterized-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-utilsInsert a binding into the map, replacing the existing binding if needed.parameterized-utilsInsert 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 $ 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-utilsLog-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-utilsGenerate a map from a foldable collection of keys and a function from keys to values.parameterized-utilsGenerate a map from a foldable collection of keys and a monadic function from keys to values.parameterized-utilsScope a monadic function to a sub-section of the given vector.parameterized-utils6Scope a function to a sub-section of the given vector.parameterized-utilsMonadically unfold a vector, with access to the current index.c.f. Data.Vector.unfoldrExactNMparameterized-utils2Unfold a vector, with access to the current index.c.f. Data.Vector.unfoldrExactNparameterized-utils,Monadically construct a vector with exactly h + 1 elements by repeatedly applying a generator function to a seed value.c.f. Data.Vector.unfoldrExactNMparameterized-utils Construct a vector with exactly h + 1 elements by repeatedly applying a generator function to a seed value.c.f. Data.Vector.unfoldrExactNparameterized-utilsBuild a vector by repeatedly applying a monadic function to a seed value. Compare to .parameterized-utilsBuild a vector by repeatedly applying a function to a seed value. Compare to 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-utilsJoin 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  BigEndian, then less significant bits go into larger indexes. See the documentation for  for more details.parameterized-utilsAn applicative version of  splitWith.parameterized-utilsAppend the two bit vectors. The first argument is at the lower indexes of the resulting vector.parameterized-utilsSplit 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-utilsJoin a vector of vectors into a single vector. Assumes an append/ LittleEndian 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-utils Start index parameterized-utilsSection width parameterized-utilsmap for the sub-vector parameterized-utils Start index parameterized-utilsSection width parameterized-utilsmap for the sub-vector parameterized-utils Start index parameterized-utils 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 vector22(c) Galois, Inc 2022 Safe-Inferred)*01Aparameterized-utils n a is a map with  n keys and a values.parameterized-utilsO(1). Is the map empty?parameterized-utils O(min(n,W)).. Fetch the value at the given key in the map.parameterized-utilsUnsafely create a  n from an ! which is known to be less than n, for reasons not visible to the type system.parameterized-utilsO(1) . Number of elements in the map.parameterized-utilsO(1)!. Increase maximum key/size by 1.This does not alter the key-value pairs in the map, but rather increases the maximum number of key-value pairs that the map can hold. See Data.Parameterized.FinMap for more information. Requires n + 1 < (maxBound :: Int).parameterized-utilsO(1). Increase maximum key/size. Requires m < (maxBound :: Int).parameterized-utilsO(1). The empty map.parameterized-utilsO(1). A map with one element.parameterized-utils O(min(n,W)).parameterized-utils O(min(n,W)).parameterized-utils O(min(n,W)).parameterized-utils1Decrement the key/size, removing the item at key n + 1 if present.parameterized-utilsO(n+m).parameterized-utilsO(n+m).parameterized-utilsO(n+m). Left-biased union, i.e. ( ==  ).parameterized-utils)Non-lawful instance, provided for testing((c) Galois, Inc 2022 Safe-Inferred )*1B` (c) Galois, Inc 2022 Safe-Inferred )*1Hparameterized-utils n a is a map with  n keys and a values.parameterized-utilsO(1). Is the map empty?parameterized-utilsO(log n).. Fetch the value at the given key in the map.parameterized-utils O(nlog(n)) . Number of elements in the map.#This operation is much slower than ) because its implementation must provide significant evidence to the type-checker, and the easiest way to do that is fairly inefficient. If speed is a concern, use  Data.Parameterized.FinMap.Unsafe.parameterized-utils O(n log n)!. Increase maximum key/size by 1.This does not alter the key-value pairs in the map, but rather increases the maximum number of key-value pairs that the map can hold. See Data.Parameterized.FinMap for more information. Requires n + 1 < (maxBound :: Int).parameterized-utils O(n log n). Increase maximum key/size. Requires m < (maxBound :: Int).parameterized-utilsO(1). The empty map.parameterized-utilsO(1). A map with one element.parameterized-utilsO(log n).parameterized-utils O(min(n,W)).parameterized-utilsO(log n).parameterized-utils1Decrement the key/size, removing the item at key n + 1 if present.parameterized-utilsO(n+m).parameterized-utilsO(n+m).parameterized-utilsO(n+m). Left-biased union, i.e. ( ==  ).parameterized-utils)Non-lawful instance, provided for testing!(c) Galois, Inc 2019 Safe-Inferred )*0Iparameterized-utilsTurn an explicit Repr value into an implict KnownRepr constraint*+,-./-01*23*24*25*67*89*8:*8;*8<*=>?@A?@B?@CDEFGHIIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~  """"""""                                                                               &&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&&)&&&&&&&&&&&&&&&))    )                       !!!!!!!!**-0*2"*            **#* *-0******&-0&&&&&&&&*&&&&&&**''''''''''''''''''''''''''''''''''')''''''''''''''''''''''''''''''''''''***2parameterized-utils-2.1.7.0-E8NonuJyO68LOjiogZKbv7Data.Parameterized.SymbolReprData.Parameterized.HashTableData.Parameterized.NatReprData.Parameterized.ClassesData.Parameterized.AxiomData.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.FinData.Parameterized.ClassesCData.Parameterized.BoolReprData.Parameterized.PairData.Parameterized.All*Data.Parameterized.TraversableFC.WithIndexData.Parameterized.ListData.Parameterized.ContextData.Parameterized.Peano Data.Parameterized.Utils.BinTreeData.Parameterized.MapData.Parameterized.Utils.EndianData.Parameterized.Vector Data.Parameterized.FinMap.UnsafeData.Parameterized.FinMap.SafeData.Parameterized.WithRepr#Data.Parameterized.NatRepr.Internal Data.FoldablefoldMapData.Parameterized!Data.Parameterized.Context.UnsafeData.Parameterized.Context.SafeData.Parameterized.FinMapsizebase GHC.TypeLits KnownSymbolghc-primGHC.Prim RealWorld GHC.TypesSymbol GHC.TypeNats+*- Data.Type.Ord<=Data.Type.Equality testEquality TestEqualityRefl:~: Data.MaybeisJust'hashable-1.4.2.0-D6EOHOGayLdHLpjCLzeHpLData.Hashable.Classhash hashWithSaltHashable unsafeAxiomunsafeHeteroAxiomtestEqualityComposeBare KnownRepr knownReprTypeAp HashableF hashWithSaltFhashFAtFatFIxedF'ixF'IxedFixFIxValueFIndexFShowFwithShowshowF showsPrecFOrdFcompareFleqFltFgeqFgtF OrderingFLTFEQFGTFPolyEqpolyEqFpolyEqEqFeqF CoercibleFcoerceForderingF_refl toOrdering fromOrdering joinOrderingF lexCompareF ordFComposeshowsF$fCoercibleFkConst $fEqFkProxy $fEqFkConst$fOrdFkCompose $fShowFkProxy $fShowFkConst$fHashableFkConst$fHashableTypeAp $fShowTypeAp $fOrdTypeAp $fEqTypeAp$fKnownReprkProxyctx CtxFlatten CtxUpdate CtxLookupCtxUpdateRightCtxLookupRightFromLeftValidIxCheckIxCtxSize<+>CtxEmptyCtx::> SingleCtxleftIdassoc DecidableEqdecEq NatComparisonNatLTNatEQNatGTNatReprnatValue compareNatknownNatNonce indexValueNonceGeneratornewNonceGenerator freshNonceatLimit $fShowFkNonce$fHashableFkNonce $fOrdFkNonce$fTestEqualitykNonce $fEqNonce $fOrdNonce$fHashableNonce $fShowNonceTypePatTypeAppAnyTypeDataArgConTypeDataDlookupDataType'conPatdataParamTypes assocTypePatsstructuralEqualitystructuralTypeEqualitystructuralTypeOrdstructuralTraversal asTypeConstructuralHashstructuralHashWithSaltstructuralShowsPrecmkRepr mkKnownReprsSndFstPairReprfstsnd$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_someLens$fTraversableFkSome$fFoldableFkSome$fFunctorFkSome $fShowSome$fHashableSome $fOrdSome$fEqSomeSomeSym SymbolRepr symbolRepr someSymbol knownSymbol viewSomeSym$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 mkNatReprmaxNatplusComm plusAssocmulCommmul2PlusplusMinusCancelminusPlusCanceladdMulDistribRightwithAddMulDistribRightwithSubMulDistribRight decideLeq testStrictLeq testNatCaseslessThanIrreflexivelessThanAsymmetrictestLeqleqReflleqSuccleqTransleqZeroleqAdd2leqSub2leqProof withLeqProofisPosNat leqMulCongr leqMulPos leqMulMonoleqAdd leqAddPosleqSubaddIsLeqaddPrefixIsLeq dblPosIsPos addIsLeqLeft1withAddPrefixLeq withAddLeq natForEach natFromZeronatRec natRecStrong natRecBoundednatRecStrictlyBounded mulCancelRlemmaMulFinmkFinbuildFincountFinviewFinfinToNatembedtryEmbedminFinincFinfin0Voidfin1Unitfin2Bool $fShowFin $fBoundedFin$fOrdFin$fEqFin 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$fFunctorFkAllTraversableFCWithIndex itraverseFCFoldableFCWithIndex ifoldMapFCifoldrFCifoldlFC ifoldrFC' ifoldlFC' itoListFCFunctorFCWithIndeximapFC ifoldlMFC ifoldrMFCiallFCianyFC imapFCDefaultifoldMapFCDefaultIndex IndexHere IndexThereListNil:< fromListWith fromListWithM fromSomeListindex0index1index2index3!!updateindexedimapifoldlMifoldrizipWith itraverse$fKnownRepr[]List:$fKnownRepr[]List[] $fOrdF[]List$fTestEquality[]List$fTraversableFCWithIndexk[]List$fFoldableFCWithIndexk[]List$fFunctorFCWithIndexk[]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 knownSizeSizeViewZeroSizeIncSizeSizesizeIntzeroSizeincSizedecSizeviewSize sizeToNatReprnoDiffaddDiff extendRight appendDiffextSizeaddSize diffIsAppendviewDiff baseIndex skipIndex nextIndex lastIndex leftIndex rightIndex extendIndex extendIndex'extendIndexAppendLeftforIndex forIndexRangeintIndex viewIndexallRange indexOfRange dropTailRange dropHeadRange replicategenerate generateMemptyextend!!^adjustadjustM viewAssignzipWithzipWithMtraverseWithIndex<++>CurryAssignmentClasscurryAssignmentuncurryAssignmentCurryAssignmentIdxExtendContext'extendContext' ExtendContext extendContextApplyEmbedding'applyEmbedding'ApplyEmbeddingapplyEmbedding CtxEmbedding _ctxeSize_ctxeAssignment:>Empty singleton forIndexM generateSome generateSomeMtoVector dropPrefixunzipflattenAssignment flattenSizenull decomposeinitlastviewtakedropctxeSizectxeAssignmentidentityEmbeddingextendEmbeddingRightDiffextendEmbeddingRightappendEmbeddingappendEmbeddingLeftextendEmbeddingBothfieldnatIndex 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 mergeWithKeyintersectWithKeyMaybe $fShowMapF$fTraversableFkMapF$fFoldableFkMapF$fFunctorFkMapF$fEqMapF$fIsBinTreeMapFPair $fAtFaMapF $fIxedFaMapFEndian LittleEndian BigEndian $fEqEndian $fShowEndian $fOrdEndianVectorlength lengthIntelemAt elemAtMaybe elemAtUnsafe indicesUpTo indicesOfinsertAt insertAtMaybenonEmptyunconsunsnocfromAssignment toAssignmentslicemapAtMmapAtreplace zipWithM_ interleaveshufflereverserotateLrotateRshiftLshiftRappendconssnocunfoldrWithIndexMunfoldrWithIndexunfoldrMunfoldr iterateNMiterateN joinWithMjoinWith splitWith splitWithAsplitjoin$fTraversableVector$fFoldableVector$fFunctorVector$fTraversableWithIndexFinVector$fFoldableWithIndexFinVector$fFunctorWithIndexFinVector $fShowVector $fEqVectorFinMapincMax buildFinMap fromVectordecMax unionWithKey unionWith $fShowFinMap$fFoldableWithIndexFinFinMap$fFunctorWithIndexFinFinMap$fTraversableFinMap$fFoldableFinMap$fFunctorFinMap$fMonoidFinMap$fSemigroupFinMap $fEqFinMapIsReprwithRepr$fIsReprCtxAssignment$fIsRepr[]List$fIsReprBoolBoolRepr$fIsReprPeanoPeanoRepr$fIsReprSymbolSymbolRepr$fIsReprNaturalNatReprGHC.ShowShow showsPrecTrue defaultSaltNatGHC.STSTconExprtemplate-haskellLanguage.Haskell.TH.SyntaxSigTVarTStarTmkEqFnewNamesjoinCompareToOrdFmatchOrdArgumentsmkOrdFgenTraverseOfTypetraverseAppMatch matchHashCtormatchEqArguments mkSimpleEqF mkSimpleOrdFData.TraversabletraverseFoldableGHC.Baseid#.runSTIOGHC.RealmodData.Type.Bool||NotIf&&const BalancedTreeIntunsafe_bal_indexunsafe_bal_adjust bal_zipWithMfmap_binbal_dropunsafe_bin_indexunsafe_bin_adjust Applicative unsafeIndex$fCategoryCtxDiffunsafe_bal_generateunsafe_bal_generateMunsafe_bin_generateunsafe_bin_generateMIdx'Data.Functor.ProductGHC.WordWord64 $fShowSize GHC.MaybeMaybe insertMax insertMininsertR hedgeUnion_LB hedgeUnion_UBhedgeUnion_LB_UBJustshowMapinsertWithImpl filterMiddleatKey'Vector'Nothing&vector-0.13.0.0-JKrBPPZBIK2JBM2KZEUb7Z Data.VectorvAppend unsafeFin