h$       !"#$%&'()*+,-./0123456 7 8 9 : ; < = > ? @ A B C D E F G H I J K L M N O P Q R S T U V W X Y Z [ \ ] ^ _ ` a b c d e f g h i j k l m n o p q r s t u v w x y z { | } ~                                                                                                                              ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " # # # # $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ) ) ) * * * * * * * * * * * * * * * + + + + + + , , , , , , , , , , , , , , - - - - - - - . . . . . . . . . . . . . . . . . . . . . . . . / / / / / / / / / / / / 0 0 0 0 0 0 0 0 01disco team and contributorsbyorgey@gmail.comNone&'(./238>? disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(+./8>?"disco$Return the next integer in sequence.discoDispatch a counter effect, starting the counter from the given Integer. disco:Dispatch a counter effect, starting the counter from zero.  disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?" disco8Run an input effect in terms of an ambient state effect.  disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(+./8>?% disco#Local fresh name generation effect.discoWrapper for a monadic action with phantom type parameter for reflection. Locally defined so that the instance we are going to build with reflection must be coherent, that is there cannot be orphans.disco Dispatch an   effect via a  4 effect to keep track of a set of in-scope names.discoOpen a binder, automatically freshening the names of the bound variables, and providing the opened pattern and term to the provided continuation. The bound variables are also added to the set of in-scope variables within in the continuation.    disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?&!disco#Run a QuickCheck generator using a   effect. !!disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(+./8>?'s"disco/Use a lens to zoom into a component of a state. "#$%"#%$$4%4disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(+./8>?(M5discoDispatch a store effect.&-,+*)'(./012345&-,+*)'(43210/.5 disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?*6disco,Enumeration of optional language extensions.7discoAllow primitives, i.e. $prim8disco3Don't automatically import standard library modules9disco/Allow randomness. This is not implemented yet.;discoThe default set of language extensions (currently, the empty set).<discoA set of all possible language extensions, provided for convenience.=disco7All possible language extensions in the form of a list.>disco%Add an extension to an extension set. 6789:;<=> 6789:;<=> disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?+c EJIHGFKLMNOPQ EJIHGFKLMNOPQ disco team and contributorsbyorgey@gmail.comNone&'(./38:>?7>6SdiscoAn OpInfo record contains information about an operator, such as the operator itself, its fixity, a list of concrete syntax representations, and a numeric precedence level.Xdisco%Operators together with their fixity.[discoFixity/associativity of infix binary operators (either left, right, or non-associative).\discoLeft-associative infix.]discoRight-associative infix.^discoInfix._disco5Fixities of unary operators (either pre- or postfix).`disco Unary prefix.adiscoUnary postfix.bdiscoType operators.cdiscoList all values of a typeddisco)Count how many values there are of a typeediscoBinary operators.fdisco Addition (+)gdisco Subtraction (-)hdiscoSaturating Subtraction (.- / D)idiscoMultiplication (*)jdisco Division (/)kdiscoExponentiation (^)ldiscoInteger division (//)mdiscoEquality test (==)ndisco Not-equal (/=)odisco Less than (<)pdiscoGreater than (>)qdiscoLess than or equal (<=)rdiscoGreater than or equal (>=)sdisco Minimum (min)tdisco Maximum (max)udisco Logical and (&& / and)vdisco Logical or (|| / or)wdiscoLogical implies (-> / implies)xdiscoLogical biconditional ( - / iff)ydiscoModulo (mod)zdiscoDivisibility test (|){disco'Binomial and multinomial coefficients (choose)|disco List cons (::)}discoCartesian product of sets (** / T)~discoUnion of two sets (union / D)discoIntersection of two sets ( intersect / D)disco Difference between two sets (@@)discoElement test (D)disco Subset test (E)discoEquality assertion (=!=)discoUnary operators.discoArithmetic negation (-)discoLogical negation (not)disco Factorial (!)discoThe opTable lists all the operators in the language, in order of precedence (highest precedence first). Operators in the same list have the same precedence. This table is used by both the parser and the pretty-printer.disco3A map from all unary operators to their associated S records.disco5A map from all binary operators to their associatied S records.discoA convenient function for looking up the precedence of a unary operator.discoA convenient function for looking up the precedence of a binary operator.discoLook up the "fixity" (i.e.% associativity) of a binary operator.discoThe precedence level of function application (higher than any other precedence level).?8M   disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?8disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./8<=>?A discoConvenience function combining  and , since we often want to simultaneously indicate what the precedence and associativity of a term is, and optionally surround it with parentheses depending on the precedence and associativity of its parent.discoLocally set the precedence and associativity within a subcomputation.discoMark a subcomputation as pretty-printing a term on the left of an operator (so parentheses can be inserted appropriately, depending on the associativity).discoMark a subcomputation as pretty-printing a term on the right of an operator (so parentheses can be inserted appropriately, depending on the associativity).discoOptionally surround a pretty-printed term with parentheses, depending on its precedence and associativity (given as the  argument) and that of its context (given by the ambient 'Reader PA' effect).discoPretty-print a rational number using its decimal expansion, in the format nnn.prefix[rep]...;, with any repeating digits enclosed in square brackets.discodigitalExpansion b n d takes the numerator and denominator of a fraction n/d between 0 and 1, and returns a pair of (1) a list of digits ds,, and (2) a nonnegative integer k such that splitAt k ds = (prefix, rep)5, where the infinite base-b expansion of n/d is 0.(prefix ++ cycle rep). For example, digitalExpansion 10 1 4 = ([2,5,0], 2) digitalExpansion 10 1 7 = ([1,4,2,8,5,7], 0) digitalExpansion 10 3 28 = ([1,0,7,1,4,2,8,5], 2) digitalExpansion 2 1 5 = ([0,0,1,1], 0)It works by performing the standard long division algorithm, and looking for the first time that the remainder repeats.discoPretty-print a binary operator, by looking up its concrete syntax in the .discoPretty-print a unary operator, by looking up its concrete syntax in the .1disco team and contributorsbyorgey@gmail.comNone &'(./8>?K discoA value of type Substitution a8 is a substitution which maps some set of names (the domain, see ) to values of type a. Substitutions can be applied to certain terms (see ), replacing any free occurrences of names in the domain with their corresponding values. Thus, substitutions can be thought of as functions of type  Term -> Term (for suitable Term3s that contain names and values of the right type).-Concretely, substitutions are stored using a Map. See also  Disco.Types, which defines S as an alias for substitutions on types (the most common kind in the disco codebase).discoThe domain of a substitution is the set of names for which the substitution is defined.discoThe identity substitution, i.e. the unique substitution with an empty domain, which acts as the identity function on terms.discoConstruct a singleton substitution, which maps the given name to the given value.disco%Compose two substitutions. Applying s1 @@ s2" is the same as applying first s2, then s1; that is, semantically, composition of substitutions corresponds exactly to function composition when they are considered as functions on terms.8As one would expect, composition is associative and has  as its identity.disco=Compose a whole container of substitutions. For example, %compose [s1, s2, s3] = s1 @@ s2 @@ s3.discoApply a substitution to a term, resulting in a new term in which any free variables in the domain of the substitution have been replaced by their corresponding values. Note this requires a  Subst b a< constraint, which intuitively means that values of type a contain variables of type b we can substitute for.discoCreate a substitution from an association list of names and values.disco0Convert a substitution into an association list.discoLook up the value a particular name maps to under the given substitution; or return Nothing5 if the name being looked up is not in the domain.  disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./58>?Kdisco team and contributorsbyorgey@gmail.comNone&'(./38:>?UdiscoAn info record for a single primitive name, containing the primitive itself, its concrete syntax, and whether it is "exposed", i.e. available to be used in the surface syntax of the basic language. Unexposed prims can only be referenced by enabling the Primitives language extension and prefixing their name by $.disco Primitives, i.e. built-in constants.discoA table containing a " record for every non-operator  recognized by the language.disco+Find any exposed prims with the given name.discoA convenient map from each  to its info record.%discoUnary operatordiscoBinary operatordiscoLeft injection into a sum type.disco Right injection into a sum type.discoInteger square root (sqrt)discoFloor of fractional type (floor)discoCeiling of fractional type (ceiling)discoAbsolute value (abs)discoPower set (XXX or bag?)discoContainer -> list conversiondiscoContainer -> bag conversiondiscoContainer -> set conversiondiscobag -> set of counts conversiondiscoset of counts -> bag conversiondiscounsafe set of counts -> bag conversion that assumes all distinctdiscoMap k v -> Set (k  v)discoSet (k  v) -> Map k vdiscoGet Adjacency list of GraphdiscoConstruct a graph Vertexdisco Empty graphdiscoOverlay two Graphsdisco,Connect Graph to another with directed edgesdiscoInsert into mapdisco$Get value associated with key in mapdiscoEach operation for containersdiscoReduce operation for containersdiscoFilter operation for containersdiscoMonadic join for containersdisco%Generic merge operation for bags/setsdiscoEfficient primality testdisco Factorizationdisco(Turn a rational into a pair (num, denom)discoCrashdisco [x, y, z .. e]disco Test whether a proposition holdsdiscoLookup OEIS sequencediscoExtend OEIS sequence..disco team and contributorsbyorgey@gmail.comNone &'(./8:>?\ discoA  represents a set of qualifiers, and also represents a set of types (in general, the intersection of the sets corresponding to the qualifiers).discoA "qualifier" is kind of like a type class in Haskell; but unlike Haskell, disco users cannot define their own. Rather, there is a finite fixed list of qualifiers supported by disco. For example, QSub denotes types which support a subtraction operation. Each qualifier corresponds to a set of types which satisfy it (see hasQual and  qualRules).These qualifiers generally arise from uses of various operations. For example, the expression  \x y. x - y% would be inferred to have a type a -> a -> a [subtractive a]!, that is, a function of type  a -> a -> a where a* is any type that supports subtraction.!These qualifiers can appear in a CQual constraint; see Disco.Typecheck.Constraint.disco+Numeric, i.e. a semiring supporting + and *discoSubtractive, i.e. supports -discoDivisive, i.e. supports /discoComparable, i.e. supports decidable ordering/comparison (see Note [QCmp])disco4Enumerable, i.e. supports ellipsis notation [x .. y]disco2Boolean, i.e. supports and, or, not (Bool or Prop)disco Things that do not involve Prop.disco7Things for which we can derive a *Haskell* Ord instancediscoA helper function that returns the appropriate qualifier for a binary arithmetic operation.discoThe special sort \top which includes all types.  disco team and contributorsbyorgey@gmail.comNone &'(./38:>?>disco;A type class for things whose type can be extracted or set.discoGet the type of a thing.discoSet the type of a thing, when that is possible; the default implementation is for  to do nothing.discoDefine S as a substitution on types (the most common kind) for convenience.disco Strictness represents the strictness (either strict or lazy) of a function application or let-expression.disco+ represents a polymorphic type of the form forall a1 a2 ... an. ty (note, however, that n may be 0, that is, we can have a "trivial" polytype which quantifies zero variables).discoA  is a mapping from type names to their corresponding definitions.disco/The definition of a user-defined type contains:The actual names of the type variable arguments used in the definition (we keep these around only to help with pretty-printing)A function representing the body of the definition. It takes a list of type arguments and returns the body of the definition with the type arguments substituted.We represent type definitions this way (using a function, as opposed to a chunk of abstract syntax) because it makes some things simpler, and we don't particularly need to do anything more complicated.discoThe main data type for representing types in the disco language. A type can be either an atomic type, or the application of a type constructor to one or more type arguments.Type"s are broken down into two cases (TyAtom and TyCon) for ease of implementation: there are many situations where all atoms can be handled generically in one way and all type constructors can be handled generically in another. However, using this representation to write down specific types is tedious; for example, to represent the type N -> a" one must write something like 2TyCon CArr [TyAtom (ABase N), TyAtom (AVar (U a))]0. For this reason, pattern synonyms such as ,  , and  are provided so that one can use them to construct and pattern-match on types when convenient. For example, using these synonyms the foregoing example can be written TyN :->: TyVar a.disco)Atomic types (variables and base types), e.g. N, Bool, etc.disco5Application of a type constructor to type arguments, e.g.  N -> Bool is the application of the arrow type constructor to the arguments N and Bool.discoCompound types, such as functions, product types, and sum types, are an application of a type constructor" to one or more argument types.discoFunction type constructor, T1 -> T2.discoProduct type constructor, T1 * T2.discoSum type constructor, T1 + T2.discoContainer type (list, bag, or set) constructor. Note this looks like it could contain any ?, but it will only ever contain either a type variable or a , , or . See also , , and .discoKey value maps, Map k vdiscoGraph constructor, Graph adisco.The name of a user defined algebraic datatype.disco Unifiable atomic types are the same as atomic types but without skolem variables. Hence, a unifiable atomic type is either a base type or a unification variable.Again, the reason this has its own type is that at some stage of the typechecking/constraint solving process, these should be the only things around; we can get rid of skolem variables because either they impose no constraints, or result in an error if they are related to something other than themselves. After checking these things, we can just focus on base types and unification variables.discoAn  atomic type is either a base type or a type variable. The alternative is a  compound type which is built out of type constructors. The reason we split out the concept of atomic types into its own data type  is because constraints involving compound types can always be simplified/translated into constraints involving only atomic types. After that simplification step, we want to be able to work with collections of constraints that are guaranteed to contain only atomic types.disco represents type variables2, that is, variables which stand for some type.disco represents type variables, that is, variables which stand for some type. There are two kinds of type variables:Unification variables stand for an unknown type, about which we might learn additional information during the typechecking process. For example, given a function of type List a -> List a, if we typecheck an application of the function to the list [1,2,3], we would learn that List a has to be List N, and hence that a has to be N.Skolem variables stand for a fixed generic type, and are used to typecheck universally quantified type signatures (i.e. type signatures which contain type variables). For example, if a function has the declared type  List a -> N, it amounts to a claim that the function will work no matter what type is substituted for a<. We check this by making up a new skolem variable for a. Skolem variables are equal to themselves, but nothing else. In contrast to a unification variable, "learning something" about a skolem variable is an error: it means that the function will only work for certain types, in contradiction to its claim to work for any type at all.discoBase types are the built-in types which form the basis of the disco type system, out of which more complex types can be built.disco#The void type, with no inhabitants.disco#The unit type, with one inhabitant.disco Booleans.disco Propositions.discoNatural numbers.disco Integers.disco)Fractionals (i.e. nonnegative rationals).disco Rationals.discoUnicode characters.discoSet container type. It's a bit odd putting these here since they have kind * -> * and all the other base types have kind *; but there's nothing fundamentally wrong with it and in particular this allows us to reuse all the existing constraint solving machinery for container subtyping.discoBag container type.discoList container type.disco&An application of a user-defined type.disco is provided for convenience; it represents a set type constructor (i.e. Set a).disco is provided for convenience; it represents a bag type constructor (i.e. Bag a).disco is provided for convenience; it represents a list type constructor (i.e. List a).discoTest whether a $ is a container (set, bag, or list).discoIs this atomic type a variable?disco Is this atomic type a base type?disco&Is this atomic type a skolem variable?disco7Is this unifiable atomic type a (unification) variable?disco;Convert a unifiable atomic type into a regular atomic type.disco/Convert a unifiable atomic type to an explicit Either type.discoIs this a type variable?discoConvert a monotype into a trivial polytype that does not quantify over any type variables. If the type can contain free type variables, use  instead.discoConvert a monotype into a polytype by quantifying over all its free type variables.disco.Compute the number of inhabitants of a type. Nothing) means the type is countably infinite.disco(Check whether a type is a numeric type (N, Z, F, Q, or Zn).disco Decide whether a type is empty, i.e. uninhabited.disco Decide whether a type is finite.discoDecide whether a type is searchable, i.e. effectively enumerable.disco*Numeric types are strict; others are lazy.discoDecompose a nested product T1 * (T2 * ( ... )) into a list of types.disco=Convert a substitution on atoms into a substitution on types.discoConvert a substitution on unifiable atoms into a substitution on types.disco;Return a set of all the free container variables in a type.discoPretty-print a type definition.discoPretty-print a polytype. Note that we never explicitly print forall,; quantification is implicit, as in Haskell.675disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?discoGiven a list of equations between types, return a substitution which makes all the equations satisfied (or fail if it is not possible).This is not the most efficient way to implement unification but it is simple.discoGiven a list of equations between types, return a substitution which makes all the equations equal *up to* identifying all base types. So, for example, Int = Nat weakly unifies but Int = (Int -> Int) does not. This is used to check whether subtyping constraints are structurally sound before doing constraint simplification/solving, to ensure termination.discoGiven a list of equations between types, return a substitution which makes all the equations satisfied (or fail if it is not possible), up to the given comparison on base types.disco team and contributorsbyorgey@gmail.comNone &'(./38:>?discoA QName, or qualified name, is a   paired with its .discoWhere did a name come from?discoThe name is locally bounddisco(The name is exported by the given modulediscoThe name of a module.discoThe special top-level "module" consisting of what has been entered at the REPL.disco-A named module, with its name and provenance.discoWhere did a module come from?disco-From a particular directory (relative to cwd)discoFrom the standard librarydisco-Does this name correspond to a free variable?disco&Create a locally bound qualified name.disco%Create a module-bound qualified name.discoThe unbound-generics library gives us free variables for free. But when dealing with typed and desugared ASTs, we want all the free s instead of just  s.disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(+./8>?1discoFresh name generation effect, supporting raw generation of fresh names, and opening binders with automatic freshening. Simply increments a global counter every time < is called and makes a variable with that numeric suffix.discoWrapper for a monadic action with phantom type parameter for reflection. Locally defined so that the instance we are going to build with reflection must be coherent, that is there cannot be orphans.discoDispatch the fresh name generation effect, starting at a given integer.discoRun a computation requiring fresh name generation, beginning with 0 for the initial freshly generated name.discoRun a computation requiring fresh name generation, beginning with 1 instead of 0 for the initial freshly generated name.discoOpen a binder, automatically creating fresh names for the bound variables.discoGenerate a fresh (local, free) qualified name based on a given string.discoRun a   computation requiring a   constraint (from the unbound-generics# library) in terms of an available  effect.disco team and contributorsbyorgey@gmail.comNone&'(./5678>?disco;A context maps qualified names to things. In particular a  Ctx a b maps qualified names for as to values of type b.discoThe empty context.disco9A singleton context, mapping a qualified name to a thing.disco>Create a context from a list of (qualified name, value) pairs.disco3Create a context for bindings from a single module.disco%Create a context with local bindings.discoInsert a new binding into a context. The new binding shadows any old binding for the same qualified name.discoRun a computation under a context extended with a new binding. The new binding shadows any old binding for the same name.discoRun a computation in a context extended with an additional context. Bindings in the additional context shadow any bindings with the same names in the existing context.discoCheck if a context is empty.disco/Look up a qualified name in an ambient context.disco&Look up a qualified name in a context.discoLook up all the non-local bindings of a name in an ambient context.disco:Look up all the non-local bindings of a name in a context.discoLook up all the bindings of an (unqualified) name in an ambient context.disco?Look up all the bindings of an (unqualified) name in a context.disco2Return a list of the names defined by the context.disco5Return a list of all the values bound by the context.discoReturn a list of the qualified name-value associations in the context.disco3Return a set of all qualified names in the context.disco8Coerce the type of the qualified name keys in a context.disco5Restrict a context to only the keys in the given set.disco Join two contexts (left-biased, i.e. if the same qualified name exists in both contexts, the result will use the value from the first context, and throw away the value from the second.).disco&Join a list of contexts (left-biased).disco#Filter a context using a predicate.disco team and contributorsbyorgey@gmail.comNone &'(-./235678:>?disco)A property is just a term (of type Prop).discoA quantifier: , D, or DdiscoA binder represents the stuff between the quantifier and the body of a lambda, D, or D abstraction, as in  x : N, r : F.discoA type family specifying what the binder in an abstraction can be. Should have at least variables in it, but how many variables and what other information is carried along may vary.disco Patterns.disco:Variable pattern: matches anything and binds the variable.discoWildcard pattern _: matches anything.discoType ascription pattern pat : ty.disco Unit pattern () : matches ().discoLiteral boolean pattern.discoTuple pattern (pat1, .. , patn).discoInjection pattern (inl pat or inr pat).discoLiteral natural number pattern.discoUnicode character patterndiscoString pattern.disco Cons pattern p1 :: p2.disco List pattern  [p1, .., pn].discoAddition pattern, p + t or t + pdiscoMultiplication pattern, p * t or t * pdiscoSubtraction pattern, p - tdiscoNegation pattern, -pdiscoFraction pattern, p1/p2discoExpansion slot.discoGuards in case expressions.discoBoolean guard (if test)discoPattern guard (when term = pat)discoLet ( let x = term)discoA branch of a case is a list of guards with an accompanying term. The guards scope over the term. Additionally, each guard scopes over subsequent guards.discoA binding is a name along with its definition, and optionally its type.discoA container comprehension consists of a head term and then a list of qualifiers. Each qualifier either binds a variable to some collection or consists of a boolean guard.discoA binding qualifier (i.e. x in t).discoA boolean guard qualfier (i.e.  x + y > 4).discoA "link" is a comparison operator and a term; a single term followed by a sequence of links makes up a comparison chain, such as 2 < x < y < 10.discoNote that although the type of  says it can hold any e2, it should really only hold comparison operators.discoThe base generic AST representing terms in the disco language. e is a type index indicating the kind of term, i.e. the phase (for example, surface, typed, or desugared). Type families like  and so on use the phase index to determine what extra information (if any) should be stored in each constructor. For example, in the typed phase many constructors store an extra type, giving the type of the term.discoA term variable.disco A primitive, i.e. a constant which is interpreted specially at runtime. See Disco.Syntax.Prims.disco"A (non-recursive) let expression, let x1 = t1, x2 = t2, ... in t.discoExplicit parentheses. We need to keep track of these in the surface syntax in order to syntactically distinguish multiplication and function application. However, note that these disappear after the surface syntax phase.disco!The unit value, (), of type Unit.discoA boolean value.discoA natural number.discoA nonnegative rational number, parsed as a decimal. (Note syntax like 3/5 does not parse as a rational, but rather as the application of a division operator to two natural numbers.)discoA literal unicode character, e.g. d.discoA string literal, e.g. "disco".disco#A binding abstraction, of the form  Q vars. expr where Q is a quantifier and vars is a list of bound variables and optional type annotations. In particular, this could be a lambda abstraction, i.e. an anonymous function (e.g. x, (y:N). 2x + y), a universal quantifier (forall x, (y:N). x^2 + y > 0!), or an existential quantifier ( exists x, (y:N). x^2 + y == 0).discoFunction application, t1 t2.disco An n-tuple,  (t1, ..., tn).discoA case expression.discoA chained comparison, consisting of a term followed by one or more "links", where each link is a comparison operator and another term.disco"An application of a type operator.disco)A containter literal (set, bag, or list).discoA container comprehension.discoType ascription, (Term_ e : type).discoA data constructor with an extension descriptor that a "concrete" implementation of a generic AST may use to carry extra information.discoAn ellipsis is an "omitted" part of a literal container (such as a list or set), of the form .. t. We don't have open-ended ellipses since everything is evaluated eagerly and hence containers must be finite.disco5 represents an ellipsis with a given endpoint, as in  [3 .. 20].discoAn enumeration of the different kinds of containers in disco: lists, bags, and sets.discoInjections into a sum type (inl or inr) have a "side" (L or R).discoA telescope is essentially a list, except that each item can bind names in the rest of the list.discoThe empty telescope.discoA binder of type b followed by zero or more b 's. This b) can bind variables in the subsequent b's.disco%Add a new item to the beginning of a .discoFold a telescope given a combining function and a value to use for the empty telescope. Analogous to   for lists.disco.Apply a function to every item in a telescope.discoTraverse over a telescope.discoConvert a list to a telescope.discoConvert a telescope to a list.discoUse a ; to select one of two arguments (the first argument for , and the second for ).disco Convert a  to a boolean.disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./28>?discoA declaration is either a type declaration, a term definition, or a type definition.disco,A user-defined type (potentially recursive).@type T arg1 arg2 ... = bodydisco*A group of definition clauses of the form name pat1 .. patn = term;. The patterns bind variables in the term. For example, f n (x,y) = n*x + y.discoA type declaration,  name : type.disco;A property is a universally quantified term of the form forall v1 : T1, v2 : T2. term.discoAn item of documentation.disco+A documentation string, i.e. a block of ||| text itemsdisco An exampledoctestproperty of the form "!!! forall (x1:ty1) ... . propertydisco!Convenient synonym for a list of s.discoA TopLevel is either documentation (a ) or a declaration ().discoA module contains all the information from one disco source file.discoEnabled extensionsdiscoModule importsdisco Declarationsdisco DocumentationdiscoTop-level (bare) termsdisco8The extension descriptor for Surface specific AST types.disco Pretty-print a type declaration.disco3Pretty-print a single qualifier in a comprehension.disco/Pretty-print the qualifiers in a comprehension.discoPretty-print a binding, i.e. a pairing of a name (with optional type annotation) and term.disco2Pretty-print a single branch in a case expression.discoPretty-print the guards in a single branch of a case expression.disco-Pretty-print a single clause in a definition.disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./38>?discoAn ATerm is a typechecked term where every node in the tree has been annotated with the type of the subterm rooted at that node.;;disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?discoA DTerm is a term which has been typechecked and desugared, so it has fewer constructors and complex features than ATerm*, but still retains typing information.discoA test frame, recording a collection of variables with their types and their original user-facing names. Used for legible reporting of test failures inside the enclosed term.!(c) 2016 disco team (see LICENSE)BSD-style (see LICENSE)byorgey@gmail.comNone&'(./8>?disco+Erase all the type annotations from a term.  disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./38:>?vdiscoOperators that can show up in the core language. Note that not all surface language operators show up here, since some are desugared into combinators of the operators here.disco Addition (+)discoArithmetic negation (-)discoInteger square root (sqrt)discoFloor of fractional type (floor)discoCeiling of fractional type (ceiling)discoAbsolute value (abs)discoMultiplication (*)disco Division (/)discoExponentiation (^)discoModulo (mod)discoDivisibility test (|)discoMultinomial coefficient (choose)disco Factorial (!)discoEquality test (==)disco Less than (<)discoEnumerate the values of a type.discoCount the values of a type.disco Power setbag of a given setbag (power).discoSet/bag element test.discoList element test.discoMap a function over a bag. Carries the output type of the function.discoMap a function over a set. Carries the output type of the function.disco Filter a bag.discoMerge two bags/sets.disco#Bag join, i.e. union a bag of bags.discoAdjacency List of given graphdisco Empty graphdisco#Construct a vertex with given valuedisco Graph overlaydisco Graph connectdisco Map insertdisco Map lookupdiscoContinue until end, [x, y, z .. e]disco&set -> list conversion (sorted order).disco*bag -> set conversion (forget duplicates).disco&bag -> list conversion (sorted order).disco2list -> set conversion (forget order, duplicates).disco&list -> bag conversion (forget order).discobag -> set of countsdiscoset of counts -> bagdisco5unsafe set of counts -> bag, assumes all are distinctdiscoMap k v -> Set (k  v)discoSet (k  v) -> Map k vdiscoPrimality testdisco Factorizationdisco(Turn a rational into a (num, denom) pairdisco2Universal quantification. Applied to a closure t1, ..., tn -> Prop it yields a Prop.disco4Existential quantification. Applied to a closure t1, ..., tn -> Prop it yields a Prop.disco+Convert Prop -> Bool via exhaustive search.disco$Flip success and failure for a prop.discoEquality assertion, =!=disco&Error for non-exhaustive pattern matchdisco"Crash with a user-supplied messagediscoNo-op/identity functiondiscoLookup OEIS sequencediscoExtend a List via OEISdisco-AST for the desugared, untyped core language.disco A variable.discoA rational number.discoA built-in constant.discoAn injection into a sum type, i.e. a value together with a tag indicating which element of a sum type we are in. For example, false is represented by  CSum L CUnit; right(v) is represented by CSum R v. Note we do not need to remember which type the constructor came from; if the program typechecked then we will never end up comparing constructors from different types.disco5A primitive case expression on a value of a sum type.discoThe unit value.discoA pair of values.disco'A projection from a product type, i.e. fst or snd.discoAn anonymous function.discoFunction application.discoA "test frame" under which a test case is run. Records the types and legible names of the variables that should be reported to the user if the test fails.discoA type.discoIntroduction form for a lazily evaluated value of type Lazy T for some type T. We can have multiple bindings to multiple terms to create a simple target for compiling mutual recursion.disco!Force evaluation of a lazy value.discoA type of flags specifying whether to display a rational number as a fraction or a decimal.discoGet the arity (desired number of arguments) of a function constant. A few constants have arity 0; everything else is uncurried and hence has arity 1.discoThe   instance for  corresponds to the idea that the result should be displayed as a decimal if any decimal literals are used in the input; otherwise, the default is to display as a fraction. So the identity element is  , and  always wins when combining.disco team and contributorsbyorgey@gmail.comNone&'(./8>?discoA "direction" for the subtyping relation (either subtype or supertype).discoA particular type argument can be either co- or contravariant with respect to subtyping.discoThe arity of a type constructor is a list of variances, expressing both how many type arguments the constructor takes, and the variance of each argument. This is used to decompose subtyping constraints. For example, arity CArr = [Contra, Co] since function arrow is contravariant in its first argument and covariant in its second. That is,  S1 -> T1  :S2 - T2 (<:, means "is a subtype of") if and only if S2 <: S1 and T1 <: T2.discoSwap directions.discoCheck whether one atomic type is a subtype of the other. Returns True< if either they are equal, or if they are base types and  returns true.disco4Check whether one base type is a subtype of another.disco>Check whether one base type is a sub- or supertype of another.disco-List all the supertypes of a given base type.disco+List all the subtypes of a given base type.disco5List all the sub- or supertypes of a given base type.disco6Check whether a given base type satisfies a qualifier.discoCheck whether a base type has a certain sort, which simply amounts to whether it satisfies every qualifier in the sort. discoGiven a constructor T and a qualifier we want to hold of a type T t1 t2 ..., return a list of qualifiers that need to hold of t1, t2, ... discosortRules T s = [s1, ..., sn] means that sort s holds of type  (T t1 ... tn) if and only if s1 t1  ...  sn tn0. For now this is just derived directly from  . This is the arity7 function described in section 4.1 of Traytel et al. discoPick a base type (generally the "simplest") that satisfies a given sort.  disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./8:>?ݙ discoConstraints are generated as a result of type inference and checking. These constraints are accumulated during the inference and checking phase and are subsequently solved by the constraint solver. disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?ި discoA synonym for pairing which makes convenient syntax for constructing literal maps via M.fromList.   1 disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./8>? disco+Directed graphs, with vertices labelled by a and unlabelled edges. discoCreate a graph with the given set of vertices and directed edges. If any edges refer to vertices that are not in the given vertex set, they will simply be dropped. disco.Return the set of vertices (nodes) of a graph. disco,Return the set of directed edges of a graph. disco2Map a function over all the vertices of a graph. Graph is not a Functor instance because of the Ord constraint on b. discoDelete a vertex. discoThe  condensation of a graph is the graph of its strongly connected components, i.e. each strongly connected component is compressed to a single node, labelled by the set of vertices in the component. There is an edge from component A to component B in the condensed graph iff there is an edge from any vertex in component A to any vertex in component B in the original graph. discoGet a list of the weakly connected components of a graph, providing the set of vertices in each. Equivalently, return the strongly connected components of the graph when considered as an undirected graph. discoDo a topological sort on a DAG. disco+A miscellaneous utility function to turn a  Graph Maybe into a  Maybe Graph: the result is Just0 iff all the vertices in the input graph are. discoGet a list of all the  successors" of a given node in the graph, i.e. all the nodes reachable from the given node by a directed path. Does not include the given node itself. discoGet a list of all the  predecessors" of a given node in the graph, i.e. all the nodes from which from the given node is reachable by a directed path. Does not include the given node itself. discoGiven a graph, return two mappings: the first maps each vertex to its set of successors; the second maps each vertex to its set of predecessors. Equivalent to (M.fromList *** M.fromList) . unzip . map (\a -> ((a, suc g a), (a, pre g a))) . nodes $ gbut much more efficient.  !disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./8:>? discoInformation about a particular type variable. More information may be added in the future (e.g. polarity). disco9The ilk (unification or skolem) of the variable, if known disco2The sort (set of qualifiers) of the type variable. discoType of errors which can be generated by the constraint solving process. discoRun a list of actions, and return the results from those which do not throw an error. If all of them throw an error, rethrow the first one. disco A variant of asum which picks the first action that succeeds, or re-throws the error of the last one if none of them do. Precondition: the list must not be empty. discoA   records what we know about each type variable; it is a mapping from type variable names to   records. disco Create a   given an  and a . disco!Utility function for acting on a   by acting on the underlying  . disco#Look up a given variable name in a  . discoRemove the mapping for a particular variable name (if it exists) from a  . disco y)  :(z - Int), then we can decompose it into two constraints, (z <: x) and (y <: Int); if we have a constraint v <: (a,b), then we substitute v C (x,y) (where x and y are fresh type variables) and continue; and so on.After this step, the remaining constraints will all be atomic constraints, that is, only of the form (v1 <: v2), (v <: b), or (b <: v), where v is a type variable and b is a base type. discoGiven a list of atoms and atomic subtype constraints (each pair (a1,a2) corresponds to the constraint a1 <: a2.) build the corresponding constraint graph. discoCheck for any weakly connected components containing more than one skolem, or a skolem and a base type, or a skolem and any variables with nontrivial sorts; such components are not allowed. If there are any WCCs with a single skolem, no base types, and only unsorted variables, just unify them all with the skolem and remove those components. discoEliminate cycles in the constraint set by collapsing each strongly connected component to a single node, (unifying all the types in the SCC). A strongly connected component is a maximal set of nodes where every node is reachable from every other by a directed path; since we are using directed edges to indicate a subtyping constraint, this means every node must be a subtype of every other, and the only way this can happen is if all are in fact equal.Of course, this step can fail if the types in a SCC are not unifiable. If it succeeds, it returns the collapsed graph (which is now guaranteed to be acyclic, i.e. a DAG) and a substitution. disco Modify a RelMap to record the fact that we have solved for a type variable. In particular, delete the variable from the RelMap as a key, and also update the relative sets of every other variable to remove this variable and add the base type we chose for it. discoEssentially dirtypesBySort vm rm dir t s x finds all the dir-types (sub- or super-) of t which have sort s, relative to the variables in x. This is overbar{T}_S^X (resp. underbar...) from Traytel et al. discoSort-aware infimum or supremum. discoFrom the constraint graph, build the sets of sub- and super- base types of each type variable, as well as the sets of sub- and supertype variables. For each type variable x in turn, try to find a common supertype of its base subtypes which is consistent with the sort of x and with the sorts of all its sub-variables, as well as symmetrically a common subtype of its supertypes, etc. Assign x one of the two: if it has only successors, assign it their inf; otherwise, assign it the sup of its predecessors. If it has both, we have a choice of whether to assign it the sup of predecessors or inf of successors; both lead to a sound & complete algorithm. We choose to assign it the sup of its predecessors in this case, since it seems nice to default to "simpler" types lower down in the subtyping chain.? ? "!(c) 2016 disco team (see LICENSE)BSD-style (see LICENSE)byorgey@gmail.comNone&'(./8>? ;! discoPotential typechecking errors. discoEncountered an unbound variable discoEncountered an ambiguous name. disco%No type is specified for a definition discoThe type of the term should have an outermost constructor matching Con, but it has type  instead discoCase analyses cannot be empty. discoThe given pattern should have the type, but it doesn't. instead it has a kind of type given by the Con. discoDuplicate declarations. discoDuplicate definitions. discoDuplicate type definitions. discoCyclic type definition. disco/# of patterns does not match type in definition discoType can't be quantified over. disco/The constraint solver couldn't find a solution. disco An undefined type name was used. disco#Wildcards are not allowed in terms. disco2Not enough arguments provided to type constructor. disco0Too many arguments provided to type constructor. discoUnbound type variable disco$Polymorphic recursion is not allowed disco&Not an error. The identity of the Monoid TCError instance. disco7A typing context is a mapping from term names to types. discoEmit a constraint. discoEmit a list of constraints. disco0Close over the current constraint with a forall. discoRun two constraint-generating actions and combine the constraints via disjunction. discoRun a computation that generates constraints, returning the generated   along with the output. Note that this locally dispatches the constraint writer effect.This function is somewhat low-level; typically you should use  6 instead, which also solves the generated constraints. discoRun a computation and solve its generated constraint, returning the resulting substitution (or failing with an error). Note that this locally dispatches the constraint writer effect. disco1Look up the definition of a named type. Throw a   error if it is not found. disco>Run a subcomputation with an extended type definition context. disco+Generate a type variable with a fresh name. disco%Generate a fresh variable as an atom. disco 5 is a monoid where we simply discard the first error. #disco team and contributorsbyorgey@gmail.comNone&'(./8>? J discoA map from some primitives to a short descriptive string, to be shown by the :doc command. discoA map from some primitives to their corresponding page in the Disco language reference (https:/disco-lang.readthedocs.ioenlatestreference/index.html).  1None&'(./8>?  $!(c) 2019 disco team (see LICENSE) BSD-3-Clausebyorgey@gmail.comNone&'(./238:>? discoType checking a module yields a value of type ModuleInfo which contains mapping from terms to their relavent documenation, a mapping from terms to properties, and a mapping from terms to their types. discoA clause in a definition consists of a list of patterns (the LHS of the =) and a term (the RHS). For example, given the concrete syntax f n (x,y) = n*x + y, the corresponding   would be something like [n, (x,y)] (n*x + y). discoA definition consists of a name being defined, the types of any pattern arguments (each clause must have the same number of patterns), the type of the body of each clause, and a list of clauses. For example, 1 f x (0,z) = 3*x + z > 5 f x (y,z) = z == 9 might look like .Defn f [Z, Z*Z] B [clause 1 ..., clause 2 ...] discoWhen loading a module, we could be loading it from code entered at the REPL, or from a standalone file. The two modes have slightly different behavior. discoA data type indicating where we should look for Disco modules to be loaded. disco>Load only from the stdlib (standard lib modules) disco/Load only from a specific directory (:load) disco8Load from current working dir or stdlib (import at REPL) disco8Load from specific dir or stdlib (import in file) disco3Get something from a module and its direct imports. discoGet the types of all names bound in a module and its direct imports. disco>Get all type definitions from a module and its direct imports. discoThe empty module info record. discoMerges a list of ModuleInfos into one ModuleInfo. Two ModuleInfos are merged by joining their doc, type, type definition, and term contexts. The property context of the new module is the one obtained from the second module. The name of the new module is taken from the first. Definitions from later modules override earlier ones. Note that this function should really only be used for the special top-level REPL module. discoAdd the possibility of loading imports from the stdlib. For example, this is what we want to do after a user loads a specific file using `:load` (for which we will NOT look in the stdlib), but then we need to recursively load modules which it imports (which may either be in the stdlib, or the same directory as the `:load`ed module). discoGiven a module resolution mode and a raw module name, relavent directories are searched for the file containing the provided module name. Returns Nothing if no module with the given name could be found.' ' %disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./8>?0_$ discoTypechecking can be in one of two modes: inference mode means we are trying to synthesize a valid type for a term; checking mode means we are trying to show that a term has a given type. discoInfer the type of a telescope, given a way to infer the type of each item along with a context of variables it binds; each such context is then added to the overall context when inferring subsequent items in the telescope. discoCheck all the types and extract all relevant info (docs, properties, types) from a module, returning a   record on success. This function does not handle imports at all; any imports should already be checked and passed in as the second argument. disco'Turn a list of type definitions into a , checking for duplicate names among the definitions and also any type definitions already in the context. disco(Check the validity of a type definition. disco(Check if a given type is cyclic. A type ty is cyclic if: ty$ is the name of a user-defined type.Repeated expansions of the type yield nothing but other user-defined types.An expansion of one of those types yields another type that has been previously encountered.In other words, repeatedly expanding the definition can get us back to exactly where we started.The function returns the set of TyDefs encountered during expansion if the TyDef is not cyclic. discoEnsure that a type definition does not use any unbound type variables or undefined types. discoCheck for polymorphic recursion: starting from a user-defined type, keep expanding its definition recursively, ensuring that any recursive references to the defined type have only type variables as arguments. disco-Keep only the duplicate elements from a list.filterDups [1,3,2,1,1,4,2][1,2] discoGiven a list of type declarations from a module, first check that there are no duplicate type declarations, and that the types are well-formed; then create a type context containing the given declarations. disco0Check that all the types in a context are valid. disco6Type check a top-level definition in the given module. discoGiven a context mapping names to documentation, extract the properties attached to each name and typecheck them. disco4Check the types of the terms embedded in a property. disco.Check that a sigma type is a valid type. See  . discoDisco doesn't need kinds per se, since all types must be fully applied. But we do need to check that every type is applied to the correct number of arguments. discoCheck that a term has the given type. Either throws an error, or returns the term annotated with types for all subterms.>This function is provided for convenience; it simply calls   with an appropriate  . disco1Check that a term has the given polymorphic type. discoInfer the type of a term. If it succeeds, it returns the term with all subterms annotated.>This function is provided for convenience; it simply calls   with an appropriate  . discoTop-level type inference algorithm: infer a (polymorphic) type for a term by running type inference, solving the resulting constraints, and quantifying over any remaining type variables. discoTop-level type checking algorithm: check that a term has a given polymorphic type by running type checking and solving the resulting constraints. discoThe main workhorse of the typechecker. Instead of having two functions, one for inference and one for checking,   takes a  . This cuts down on code duplication in many cases, and allows all the checking and inference code related to a given AST node to be placed together. discoCheck that a pattern has the given type, and return a context of pattern variables bound in the pattern along with their types. discoConstraints needed on a function type for it to be the type of the absolute value function. discoConstraints needed on a function type for it to be the type of the container size operation. discoGiven an input type ty, return a type which represents the output type of the absolute value function, and generate appropriate constraints. discoGiven an input type ty, return a type which represents the output type of the floor or ceiling functions, and generate appropriate constraints. discoGiven input types to the exponentiation operator, return a type which represents the output type, and generate appropriate constraints. discoGet the argument (element) type of a (known) container type. Returns a fresh variable with a suitable constraint if the given type is not literally a container type. discoEnsure that a type's outermost constructor matches the provided constructor, returning the types within the matched constructor or throwing a type error. If the type provided is a type variable, appropriate constraints are generated to guarantee the type variable's outermost constructor matches the provided constructor, and a list of fresh type variables is returned whose count matches the arity of the provided constructor. discoA variant of ensureConstr that expects to get exactly one argument type out, and throws an error if we get any other number. discoA variant of ensureConstr that expects to get exactly two argument types out, and throws an error if we get any other number. disco A variant of   that works on  s instead of s. Behaves similarly to   if the   is  ?; otherwise it generates an appropriate number of copies of  . disco A variant of  ! that expects to get a single  7 and throws an error if it encounters any other number. disco A variant of   that expects to get two  ;s and throws an error if it encounters any other number. discoEnsure that two types are equal: 1. Do nothing if they are literally equal 2. Generate an equality constraint otherwise) ) &disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?A ' discoA parser is a megaparsec parser of strings, with an extra layer of state to keep track of the current indentation level and language extensions, and some custom error messages. disco$Run a parser from the initial state. disco indented p is just like p, except that every token must not start in the first column. disco indented p is just like p, except that every token after the first must not start in the first column. disco6Locally set the enabled extensions within a subparser. disco3Generically consume whitespace, including comments. discoParse a lexeme, that is, a parser followed by consuming whitespace. disco!Parse a given string as a lexeme. discoParse a reserved operator. discoThe symbol that starts an anonymous function (either a backslash or a Greek ). discoParse a natural number. discoParse a reserved word. discoThe list of all reserved words. disco Parse an   and turn it into a  . discoParse the entire input as a module (with leading whitespace and no leftovers). discoParse an entire module (a list of declarations ended by semicolons). The   parameter tells us whether to include or replace any language extensions enabled at the top level. We include them when parsing a module entered at the REPL, and replace them when parsing a standalone module. disco:Parse the name of a language extension (case-insensitive). discoParse an import, of the form import modulename. discoParse the name of a module. discoParse a top level item (either documentation or a declaration), which must start at the left margin. discoParse a single top-level declaration (either a type declaration or single definition clause). discoParse the entire input as a term (with leading whitespace and no leftovers). discoParse a term, consisting of a  parseTerm') optionally followed by an ascription. disco&Parse a non-atomic, non-ascribed term. discoParse an atomic term. discoParse a container, like a literal list, set, bag, or a comprehension (not including the square or curly brackets).  container ::= '['  container-contents ']' | '{'  container-contents '}'  container-contents ::= empty |  nonempty-container  nonempty-container ::=  term [  ellipsis ] |  term  container-end  container-end ::= '|'  comprehension | ',' [  term (','  item)* ] [  ellipsis ]  comprehension ::=  qual [ ','  qual ]*  qual ::=  ident 'in'  term |  term  ellipsis ::= '..' [  term ] disco?Parse an ellipsis at the end of a literal list, of the form .. t4. Any number > 1 of dots may be used, just for fun. discoParse the part of a list comprehension after the | (without square brackets), i.e. a list of qualifiers. q [,q]* disco6Parse a qualifier in a comprehension: either a binder x in t or a guard t. discoParse a let expression (let x1 = t1, x2 = t2, ... in t). discoParse a case expression. disco&Parse one branch of a case expression. disco'Parse the list of guards in a branch.  otherwise= can be used interchangeably with an empty list of guards. discoParse a single guard (either if or when) discoParse an atomic pattern, by parsing a term and then attempting to convert it to a pattern. discoParse a pattern, by parsing a term and then attempting to convert it to a pattern. disco?D disco(Errors that can be generated at runtime. disco(An unbound name. This shouldn't happen. discoDivision by zero. discoOverflow, e.g. (2^66)! discoNon-exhaustive case analysis. disco&Infinite loop detected via black hole. discoUser-generated crash. discoTop-level error type for Disco. discoModule not found. discoCyclic import encountered. disco&Error encountered during typechecking. disco!Error encountered during parsing. discoError encountered at runtime. discoSomething that shouldn't happen; indicates the presence of a bug.  (disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./5678<>?Yl, disco ! represents a memory, containing  s disco1An environment is a mapping from names to values. discoA ValProp- is the normal form of a Disco value of type Prop. disco3A prop that has already either succeeded or failed. discoA pending search. disco'The possible outcomes of a proposition. discoThe possible outcomes of a property test, parametrized over the type of values. A  TestReason3 explains why a proposition succeeded or failed. disco The prop evaluated to a boolean. discoThe test was an equality test. Records the values being compared and also their type (which is needed for printing). disco4The search didn't find any examples/counterexamples. disco+The search found an example/counterexample. discoThe prop failed at runtime. This is always a failure, no matter which quantifiers or negations it's under. disco*A variable assignment found during a test. discoA collection of variables that might need to be reported for a test, along with their types and user-legible names. discoThe answer (success or failure) we're searching for, and the result (success or failure) we return when we find it. The motive (False, False) corresponds to a "forall" quantifier (look for a counterexample, fail if you find it) and the motive  (True, True) corresponds to "exists". The other values arise from negations. discoAll possibilities were checked. discoA number of small cases were checked exhaustively and then a number of additional cases were checked at random. discoValues which can be used as keys in a map, i.e. those for which a Haskell Ord instance can be easily created. These should always be of a type for which the QSimple qualifier can be constructed. At the moment these are always fully evaluated (containing no indirections) and thus don't need memory management. At some point in the future constructors for simple graphs and simple maps could be created, if the value type is also QSimple. The only reason for actually doing this would be constructing graphs of graphs or maps of maps, or the like. discoDifferent types of values which can result from the evaluation process. discoA numeric value, which also carries a flag saying how fractional values should be diplayed. discoA built-in function constant. discoAn injection into a sum type. discoThe unit value. discoA pair of values. discoA closure, i.e. a function body together with its environment. discoA disco type can be a value. For now, there are only a very limited number of places this could ever show up (in particular, as an argument to  enumerate or count). discoA reference, i.e. a pointer to a memory cell. This is used to implement (optional, user-requested) laziness as well as recursion. discoA literal function value. VFun is only used when enumerating function values in order to decide comparisons at higher-order function types. For example, in order to compare two values of type (Bool -> Bool) -> Bool= for equality, we have to enumerate all functions of type Bool -> Bool as VFun values.We assume that all VFun values are strict, that is, their arguments should be fully evaluated to RNF before being passed to the function. discoA proposition. discoA literal bag, containing a finite list of (perhaps only partially evaluated) values, each paired with a count. This is also used to represent sets (with the invariant that all counts are equal to 1). disco1A graph, stored using an algebraic repesentation. discoA map from keys to values. Differs from functions because we can actually construct the set of entries, while functions only have this property when the key type is finite. disco!Convenient pattern for list cons. disco&Convenient pattern for the empty list. disco.A convenience function for creating a default VNum value with a default ( Fractional) flag. disco.A convenience function for creating a default VNum value with a default ( Fractional) flag. discoTurn any instance of Enum into a Value, by creating a constructor with an index corresponding to the enum value. disco6Whether the property test resulted in a runtime error. disco.Whether the property test resulted in success. disco-The reason the property test had this result. discoAllocate a new memory cell containing an unevaluated expression with the current environment. Return the index of the allocated cell. discoAllocate new memory cells for a group of mutually recursive bindings, and return the indices of the allocate cells. disco"Look up the cell at a given index. discoSet the cell at a given index. )disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?]. discoToggles which outcome (finding or not finding the thing being searched for) qualifies as success, without changing the thing being searched for. disco)Flips the success or failure status of a  PropResult', leaving the explanation unchanged. discoSelect samples from an enumeration according to a search type. Also returns a  & describing the results, which may be   if the enumeration is no larger than the number of samples requested.  *disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?cL discoEnumerate all values of type Void (none). discoEnumerate all values of type Unit (the single value unit). discoEnumerate the values of type Bool as  [false, true]. discoEnumerate all values of type Nat (0, 1, 2, ...). discoEnumerate all values of type Integer (0, 1, -1, 2, -2, ...). discoEnumerate all values of type  Fractional" in the Calkin-Wilf order (1, 12, 2, 13, 32, 2 3, 3, ...). discoEnumerate all values of type Rational in the Calkin-Wilf order, with negatives interleaved (0, 1, -1, 12, -12, 2, -2, ...). disco!Enumerate all Unicode characters. discoEnumerate all *finite* sets over a certain element type, given an enumeration of the elements. If we think of each finite set as a binary string indicating which elements in the enumeration are members, the sets are enumerated in order of the binary strings. discoEnumerate all *finite* lists over a certain element type, given an enumeration of the elements. It is very difficult to describe the order in which the lists are generated. disco%Enumerate the values of a given type. disco$Enumerate a finite product of types. disco/Produce an actual list of the values of a type. discoProduce an actual list of values enumerated from a finite product of types.  +disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?f] discoRun a desugaring computation. discoDesugar a definition (consisting of a collection of pattern clauses with bodies) into a core language term. discoDesugar a typechecked term. discoDesugar a property by wrapping its corresponding term in a test frame to catch its exceptions & convert booleans to props. disco&Desugar a branch of a case expression. discoDesugar the list of guards in one branch of a case expression. Pattern guards essentially remain as they are; boolean guards get turned into pattern guards which match against true.   2 6 6 7 4 4 4,disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?s discoUtility function to desugar and compile a thing, given a desugaring function for it. discoCompile a typechecked term () directly to a + term, by desugaring and then compiling. disco Compile a typechecked property () directly to a , term, by desugaring and then compilling. disco.Compile a context of typechecked definitions ( ) to a sequence of compiled  bindings, such that the body of each binding depends only on previous ones in the list. First topologically sorts the definitions into mutually recursive groups, then compiles recursive definitions specially in terms of delay and force. disco9Compile a group of mutually recursive definitions, using delay8 to compile recursion via references to memory cells. disco!Compile a typechecked, desugared  to an untyped  term. discoCompile a natural number. A separate function is needed in case the number is of a finite type, in which case we must mod it by its type. compileNat :: Member Fresh r => Type -> Integer -> Sem r Core compileNat (TyFin n) x = return $ CNum Fraction ((x   n) % 1) compileNat _ x = return $ CNum Fraction (x % 1)Compile a primitive. Typically primitives turn into a corresponding function constant in the core language, but sometimes the particular constant it turns into may depend on the type. discoCompile a case expression of type  to a core language expression of type (Unit C ), in order to delay evaluation until explicitly applying it to the unit value. discoCompile a branch of a case expression of type  to a core language expression of type (Unit C ) C . The idea is that it takes a failure continuation representing the subsequent branches in the case expression. If the branch succeeds, it just returns the associated expression of type ; if it fails, it calls the continuation to proceed with the case analysis. disco  takes a list of guards, the name of the failure continuation of type (Unit C ), and a Core term of type  to return in the case of success, and compiles to an expression of type  which evaluates the guards in sequence, ultimately returning the given expression if all guards succeed, or calling the failure continuation at any point if a guard fails. disco  takes a pattern, the compiled scrutinee, the name of the failure continuation, and a Core term representing the compilation of any guards which come after this one, and returns a Core expression of type  that performs the match and either calls the failure continuation in the case of failure, or the rest of the guards in the case of success. discoCompile a unary operator. discoCompile a binary operator. This function needs to know the types of the arguments and result since some operators are overloaded and compile to different code depending on their type. /arg1 ty -> arg2 ty -> result ty -> op -> result discoType of the operator argument  -disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>?t disco/The CESK machine has two basic kinds of states. disco!Run a CESK machine to completion. disco%Advance the CESK machine by one step.  .disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./8>?~S discoA record of information about the current top-level environment. disco2All effects needed for the top level + evaluation. discoEffects needed for evaluation. discoRun a top-level computation. discoRun a computation that needs an input environment, grabbing the current top-level environment from the   records. discoParse a module from a file, re-throwing a parse error if it fails. discoRun a typechecking computation, providing it with local (initially empty) contexts for variable types and type definitions. discoRun a typechecking computation, providing it with local contexts (initialized to the provided arguments) for variable types and type definitions. discoRun a typechecking computation in the context of the top-level REPL module, re-throwing a wrapped error if it fails. discoRecursively loads a given module by first recursively loading and typechecking its imported modules, adding the obtained   records to a map from module names to info records, and then typechecking the parent module in an environment with access to this map. This is really just a depth-first search.The  : argument specifies where to look for imported modules. discoLike  #, but start with an already parsed  instead of loading a module from disk by name. Also, check it in a context that includes the current top-level context (unlike a module loaded from disk). Used for e.g. blocks/modules entered at the REPL prompt. discoTry loading the contents of a file from the filesystem, emitting an error if it's not found. discoAdd things from the given module to the set of currently loaded things. discoSet the given   record as the currently loaded module. This also includes updating the top-level state with new term definitions, documentation, types, and type definitions. Replaces any previously loaded module. discoPopulate various pieces of the top-level info record (docs, type context, type and term definitions) from the   record corresponding to the currently loaded module, and load all the definitions into the current top-level environment.  /disco team and contributors BSD-3-Clausebyorgey@gmail.comNone &'(./28>? discoGiven a list of REPL commands and something typed at the REPL, pick the first command with a matching type-level tag and run its associated action. discoThe list of all commands that can be used at the REPL. Resolution of REPL commands searches this list in order, which means ambiguous command prefixes (e.g. :t for :type) are resolved to the first matching command. discoGiven a list of available REPL commands and the currently enabled extensions, parse a string entered at the REPL prompt, returning either a parse error message or a parsed REPL expression.  0disco team and contributors BSD-3-Clausebyorgey@gmail.comNone&'(./8>? discoCommand-line options for disco. discoA single expression to evaluate disco$Execute the commands in a given file discoCheck a file and then exit 23456789:;<=>?@ABCCDDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefg h i j k l m n o p q r s t u v w x y z { | } ~                                                                                                                           ~        }             CCPQR                                               ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! ! " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " " # # # # $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % % & & & & & & & & & & & &&& && & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & & ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ' ( ( ( (( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ) ) ) * * * * * * * * * * * * * * * + + + + + + , , , , , , , , , , , , , , - - - - - - - . . . . . . . . . . . . . . . . . . . . . . . . / / / / / / / / / / / / 0 0 0 0 0 0 0 0 0                1 1 1 1 1 1 1 1 & + + + + + + + $disco-0.1.2.0-LRM3yB13Zi07a3347LVW4F Disco.Pretty Disco.DataDisco.Effects.CounterDisco.Effects.InputDisco.Effects.LFreshDisco.Effects.RandomDisco.Effects.StateDisco.Effects.StoreDisco.Extensions Disco.ReportDisco.Syntax.OperatorsDisco.Pretty.PrecDisco.Pretty.DSL Disco.SubstDisco.MessagesDisco.Syntax.PrimsDisco.Types.Qualifiers Disco.TypesDisco.Typecheck.Unify Disco.NamesDisco.Effects.Fresh Disco.ContextDisco.AST.GenericDisco.AST.SurfaceDisco.AST.TypedDisco.AST.DesugaredDisco.Typecheck.EraseDisco.AST.CoreDisco.Types.RulesDisco.Typecheck.Constraints Disco.UtilDisco.Typecheck.GraphDisco.Typecheck.SolveDisco.Typecheck.Util Disco.Doc Disco.ModuleDisco.Typecheck Disco.Parser Disco.Error Disco.ValueDisco.PropertyDisco.Enumerate Disco.Desugar Disco.CompileDisco.Interpret.CESK Disco.EvalDisco.Interactive.CommandsDisco.Interactive.CmdLine Paths_discopretty-1.1.3.6Text.PrettyPrint.HughesPJDoc $fDataName $fDataRebind $fDataEmbed $fDataBindCounterNextnext runCounter' runCounter inputToStateLFreshLfreshAvoid GetAvoidsAction LFreshDictlfresh_avoid_ getAvoids_lfreshavoid getAvoids runLFresh runLFresh'lunbind absorbLFresh$fLFreshAction$fFunctorAction$fApplicativeAction $fMonadActionrunGenzoomuse.=%=Store ClearStoreNew LookupStore InsertStoreMapStore AssocsStoreKeepKeys clearStorenew lookupStore insertStoremapStore assocsStorekeepKeysrunStoreExt PrimitivesNoStdLib RandomnessExtSet defaultExtsallExts allExtsList addExtension$fEqExt$fOrdExt $fShowExt $fReadExt $fEnumExt $fBoundedExtReportRTxtRSeqRVSeqRListRNesttexthcathsepvcatvseplistnest $fShowReportOpInfoopFixityopSynsopPrecOpFixityUOpFBOpFBFixityInLInRInUFixityPrePostTyOp EnumerateCountBOpAddSubSSubMulDivExpIDivEqNeqLtGtLeqGeqMinMaxAndOrImplIffModDividesChooseConsCartProdUnionInterDiffElemSubsetShouldEqUOpNegNotFactopTableuopMapbopMapuPrecbPrecassocfunPrec $fShowOpInfo $fEqOpFixity$fShowOpFixity$fGenericOpFixity $fEqBFixity $fOrdBFixity $fEnumBFixity$fBoundedBFixity $fShowBFixity$fGenericBFixity $fEqUFixity $fOrdUFixity $fEnumUFixity$fBoundedUFixity $fShowUFixity$fGenericUFixity $fShowTyOp$fEqTyOp $fOrdTyOp $fGenericTyOp $fDataTyOp $fAlphaTyOp $fSubsttTyOp $fShowBOp $fReadBOp$fEqBOp$fOrdBOp $fGenericBOp $fDataBOp $fAlphaBOp $fSubsttBOp $fShowUOp $fReadUOp$fEqUOp$fOrdUOp $fGenericUOp $fDataUOp $fAlphaUOp $fSubsttUOpPAPrecinitPAascrPAfunPArPAtarrPAtaddPAtmulPAtfunPAugetPAgetPA$fOrdPA$fShowPA$fEqPAparensbracketsbracesbagquotes doubleQuotesintegerhangempty<+><>$+$ punctuate intercalate bulletList renderDoc renderDoc' $fIsStringSemPrettyprettywithPAsetPAltrtmparens prettyStrpretty' prettyDecimalfindRepfindRep'digitalExpansion $fPrettyBOp $fPrettyUOp $fPrettyTyOp $fPrettyName $fPrettySet $fPrettyMap $fPretty[] SubstitutiongetSubstdomidS|->@@compose applySubstfromListtoListlookup$fPrettySubstitution$fFunctorSubstitution$fEqSubstitution$fOrdSubstitution$fShowSubstitutionMessage _messageType_message MessageTypeInfoWarningErrMsgDebug $fShowMessage$fShowMessageType$fReadMessageType$fEqMessageType$fOrdMessageType$fEnumMessageType$fBoundedMessageTypemessage messageType handleMsgprintMsgmsginfo infoPrettywarndebug debugPrettyerrPrimInfothePrim primSyntax primExposedPrimPrimUOpPrimBOpPrimLeft PrimRightPrimSqrt PrimFloorPrimCeilPrimAbs PrimPowerPrimListPrimBagPrimSetPrimB2CPrimC2BPrimUC2B PrimMapToSet PrimSetToMap PrimSummary PrimVertexPrimEmptyGraph PrimOverlay PrimConnect PrimInsert PrimLookupPrimEach PrimReduce PrimFilterPrimJoin PrimMerge PrimIsPrime PrimFactorPrimFrac PrimCrash PrimUntil PrimHolds PrimLookupSeq PrimExtendSeq primTabletoPrimprimMap $fShowPrim $fReadPrim$fEqPrim $fOrdPrim $fGenericPrim $fAlphaPrim $fSubsttPrim $fDataPrimSort QualifierQNumQSubQDivQCmpQEnumQBoolQBasicQSimplebopQualtopSort$fPrettyQualifier$fShowQualifier $fEqQualifier$fOrdQualifier$fGenericQualifier$fAlphaQualifierHasTypegetTypesetTypeS StrictnessStrictLazyPolyTypeForallTyDefCtx TyDefBodyTypeTyAtomTyConConCArrCProdCSum CContainerCMapCGraphCUserUAtomUBUVAtomAVarABaseVarVIlkSkolem UnificationBaseTyVoidUnitBPNZFQCCtrSetCtrBagCtrListTyStringTyUserTyMapTyGraph TyContainerTySetTyBagTyList:+::*::->:TyCTyQTyFTyZTyNTyPropTyBoolTyUnitTyVoidTySkolemTyVarCSetCBagCListUisCtrisVarisBaseisSkolemuisVar uatomToAtom uatomToEitherisTyVar toPolyType closeType countTypeisNumTy isEmptyTy isFiniteTy isSearchable strictnessunpairatomToTypeSubstuatomToTypeSubst containerVars $fSubsttMap $fSubsttSet$fSubstTypeType$fSubstTypeCon$fSubstTypeVoid$fSubstTypeRatio$fSubstTypeQualifier $fPrettyType $fPrettyCon $fPrettyUAtom$fSubstUAtomUAtom $fPrettyAtom$fSubstAtomAtom $fPrettyIlk$fPrettyBaseTy $fPretty(,)$fShowTyDefBody$fPrettyPolyType$fEqStrictness$fShowStrictness$fGenericStrictness$fAlphaStrictness$fShowPolyType$fGenericPolyType$fDataPolyType$fAlphaPolyType$fSubstTypePolyType $fShowType$fEqType $fOrdType $fGenericType $fDataType $fAlphaType $fShowCon$fEqCon$fOrdCon $fGenericCon $fDataCon $fAlphaCon $fShowAtom$fEqAtom $fOrdAtom $fGenericAtom $fDataAtom $fAlphaAtom$fSubstTypeAtom $fShowVar$fEqVar$fOrdVar $fGenericVar $fDataVar $fAlphaVar$fSubstAtomVar$fSubstTypeVar$fEqIlk$fOrdIlk $fReadIlk $fShowIlk $fGenericIlk $fDataIlk $fAlphaIlk$fSubstAtomIlk$fSubstTypeIlk $fShowBaseTy $fEqBaseTy $fOrdBaseTy$fGenericBaseTy $fDataBaseTy $fAlphaBaseTy$fSubstBaseTyBaseTy$fSubstAtomBaseTy$fSubstUAtomBaseTy$fSubstTypeBaseTy $fShowUAtom $fEqUAtom $fOrdUAtom$fGenericUAtom $fAlphaUAtom$fSubstBaseTyUAtomunify weakUnifyunify'equateoccurs unifyAtoms unifyUAtomsQNameqnameProvenanceqnameNameProvenance LocalName QualifiedName ModuleName REPLModuleNamedModuleProvenanceDirStdlibisFree localName.-fvQsubstQsubstsQ$fPrettyModuleName $fPrettyQName $fEqQName $fOrdQName $fShowQName$fGenericQName $fDataQName $fAlphaQName$fSubstTypeQName$fEqNameProvenance$fOrdNameProvenance$fShowNameProvenance$fGenericNameProvenance$fDataNameProvenance$fAlphaNameProvenance$fSubstTypeNameProvenance$fEqModuleName$fOrdModuleName$fShowModuleName$fGenericModuleName$fDataModuleName$fAlphaModuleName$fSubstTypeModuleName$fEqModuleProvenance$fOrdModuleProvenance$fShowModuleProvenance$fGenericModuleProvenance$fDataModuleProvenance$fAlphaModuleProvenance$fSubstTypeModuleProvenanceFresh FreshDictfresh_fresh runFresh'runFresh runFresh1unbindfreshQ absorbFresh $fFreshActionCtxemptyCtx singleCtx ctxForModulelocalCtxinsertextendextendsnulllookup'lookupNonLocallookupNonLocal' lookupAll lookupAll'nameselemsassocskeysSet coerceKeys restrictKeysjoinCtxjoinCtxsfilter $fMonoidCtx$fSemigroupCtx$fEqCtx $fShowCtx $fFunctorCtx $fFoldableCtx$fTraversableCtx Property_ QuantifierLamExAllBinder_X_Binder ForallPatternPattern_PVar_PWild_PAscr_PUnit_PBool_PTup_PInj_PNat_PChar_PString_PCons_PList_PAdd_PMul_PSub_PNeg_PFrac_ XPattern_ X_PatternX_PFracX_PNegX_PSubX_PMulX_PAddX_PListX_PCons X_PStringX_PCharX_PNatX_PInjX_PTupX_PBoolX_PUnitX_PAscrX_PWildX_PVar ForallGuardGuard_GBool_GPat_GLet_X_GLetX_GPatX_GBoolBranch_Binding_ ForallQualQual_QBind_QGuard_X_QGuardX_QBind ForallLinkLink_TLink_X_TLink ForallTermTerm_TVar_TPrim_TLet_TParens_TUnit_TBool_TNat_TRat_TChar_TString_TAbs_TApp_TTup_TCase_TChain_TTyOp_ TContainer_TContainerComp_TAscr_XTerm_X_TermX_TAscrX_TContainerComp X_TContainerX_TTyOpX_TChainX_TCaseX_TTupX_TAppX_TAbs X_TStringX_TCharX_TRatX_TNatX_TBoolX_TUnit X_TParensX_TLetX_TPrimX_TVarEllipsisUntil Container ListContainer BagContainer SetContainerSideLR TelescopeTelEmptyTelConstelCons foldTelescope mapTelescopetraverseTelescope toTelescope fromTelescope selectSidefromSide $fAlphaVoid $fPrettySide$fAlphaBinding_$fSubstTypeBinding_$fAlphaPattern_$fSubstTypePattern_ $fAlphaGuard_$fSubstTypeGuard_ $fAlphaQual_$fSubstTypeQual_ $fAlphaLink_$fSubstTypeLink_ $fPlatedTerm_ $fAlphaTerm_$fSubstTypeTerm_$fGenericTerm_$fGenericGuard_$fGenericPattern_$fGenericBinding_$fGenericQual_$fGenericLink_$fGenericQuantifier$fDataQuantifier$fEqQuantifier$fOrdQuantifier$fShowQuantifier$fAlphaQuantifier$fSubstTypeQuantifier$fShowEllipsis$fGenericEllipsis$fFunctorEllipsis$fFoldableEllipsis$fTraversableEllipsis$fAlphaEllipsis$fSubstaEllipsis$fDataEllipsis$fShowContainer $fEqContainer$fEnumContainer$fGenericContainer$fDataContainer$fAlphaContainer$fSubsttContainer $fShowSide$fEqSide $fOrdSide $fEnumSide $fBoundedSide $fGenericSide $fDataSide $fAlphaSide $fSubsttSide$fShowTelescope$fGenericTelescope$fAlphaTelescope$fSubsttTelescope$fDataTelescope$fDataPattern_$fShowPattern_ $fDataGuard_ $fShowGuard_$fDataBinding_$fShowBinding_ $fDataQual_ $fShowQual_ $fDataLink_ $fShowLink_ $fDataTerm_ $fShowTerm_PatternGuardBranchBindingQualLinkTermDeclDTypeDDefnDTyDefTypeDefnTermDefnTypeDeclPropertyDocThing DocString DocPropertyDocsTopLevelTLDocTLDeclTLExprModulemodExts modImportsmodDeclsmodDocsmodTermsUDPFracPNegPSubPMulPAddPListPConsPNatPInjPTupPStringPCharPBoolPUnitPAscrPWildPVarGLetGPatGBoolQGuardQBindTLink TListCompTListTWildTAscrTContainerComp TContainerTTyOpTChainTCaseTTupTAppTAbsTStringTCharTRatTNatTBoolTUnitTParensTLetTBinTUnTPrimTVarpartitionDecls prettyTyDecl $fPrettyTerm_ $fPrettyQual_$fPrettyTelescope$fPrettyBinding_ $fPrettyBind$fPrettyGuard_$fPrettyTelescope0$fPrettyPattern_ $fPrettyDecl$fShowTypeDefn $fShowDecl$fShowTermDefn$fShowTypeDecl$fShowDocThing$fShowTopLevel $fShowModuleAPatternAGuardABranchABindingAQualALinkATerm APropertyAPFracAPNegAPSubAPMulAPAddAPListAPConsAPNatAPInjAPTupAPStringAPCharAPBoolAPUnitAPWildAPVarAGLetAGPatAGBoolAQGuardAQBindATLink ATListCompATListATTestATContainerComp ATContainerATTyOpATChainATCaseATTupATAppATAbsATStringATCharATRatATNatATBoolATUnitATLetATPrimATVar varsBoundsubstQT$fHasTypeTerm_ $fHasTypeBind$fHasTypePattern_$fDataTYDPatternDGuardDBranchDBindingDTerm DPropertyDPInjDPPairDPUnitDPWildDPVarDGPatDTTestDTNilDTTyOpDTCaseDTPairDTAppDTAbsDTCharDTRatDTNatDTBoolDTUnitDTPrimDTVar$fAlphaX_DTerm$fSubstTypeX_DTerm $fShowX_DTerm$fGenericX_DTermerase eraseBinding erasePattern eraseBranch eraseGuard eraseLink eraseQual eraseProperty eraseDTerm eraseDBranch eraseDGuard eraseDPatternOpOAddONegOSqrtOFloorOCeilOAbsOMulODivOExpOModODivides OMultinomOFactOEqOLtOEnumOCountOPowerOBagElem OListElemOEachBagOEachSet OFilterBagOMerge OBagUnionsOSummary OEmptyGraphOVertexOOverlayOConnectOInsertOLookupOUntil OSetToList OBagToSet OBagToList OListToSet OListToBag OBagToCounts OCountsToBagOUnsafeCountsToBag OMapToSet OSetToMapOIsPrimeOFactorOFracOForallOExistsOHoldsONotProp OShouldEq OMatchErrOCrashOId OLookupSeq OExtendSeqCoreCVarCNumCConstCInjCCaseCUnitCPairCProjCAbsCAppCTestCTypeCDelayCForceRationalDisplayFractionDecimalopAritysubstQCsubstsQC$fMonoidRationalDisplay$fSemigroupRationalDisplay $fPrettyOp $fPrettyCore $fPlatedCore $fShowCore $fGenericCore $fDataCore $fAlphaCore$fShowOp $fGenericOp$fDataOp $fAlphaOp$fEqOp$fOrdOp$fEqRationalDisplay$fShowRationalDisplay$fGenericRationalDisplay$fDataRationalDisplay$fOrdRationalDisplay$fAlphaRationalDisplaySubTySuperTyVarianceCoContraarityotherisSubAisSubBisDirB supertypessubtypesdirtypeshasQualhasSort qualRules sortRulespickSortBaseTy$fEqDir$fOrdDir $fReadDir $fShowDir$fShowVariance$fReadVariance $fEqVariance $fOrdVariance ConstraintCSubCEqCQualCAndCTrueCOrCAllcAnd$fMonoidConstraint$fSemigroupConstraint$fPrettyConstraint$fShowConstraint$fGenericConstraint$fAlphaConstraint$fSubstTypeConstraint==>for!GraphGmkGraphnodesedgesmapdelete condensationwccwccIDstopsort sequenceGraphsucprecessors $fPrettyGraph $fShowGraph TyVarInfoTVI _tyVarIlk _tyVarSortSimpleConstraint:<::=: SolveError NoWeakUnifierNoUnify UnqualBaseUnqual QualSkolemrunSolve filterErrorsasum'$fSemigroupSolveError$fPrettySimpleConstraint$fShowTyVarInfo$fShowSimpleConstraint$fEqSimpleConstraint$fOrdSimpleConstraint$fGenericSimpleConstraint$fAlphaSimpleConstraint$fSubstTypeSimpleConstraint$fShowSolveError SimplifyStateSS _ssVarMap_ssConstraints_ssSubst_ssSeen TyVarInfoMapVMunVMtyVarIlk tyVarSortmkTVIonVMlookupVMdeleteVM addSkolemsgetSortgetIlk extendSort$fSemigroupTyVarInfo$fPrettyTyVarInfo$fMonoidTyVarInfoMap$fSemigroupTyVarInfoMap$fPrettyTyVarInfoMap$fShowTyVarInfoMapRelMapunRelMapRelsbaseRelsvarRels ssConstraintsssSeenssSubstssVarMaplkupsolveConstraintsolveConstraintChoicedecomposeConstraint decomposeQual checkQualsimplifymkConstraintGraph checkSkolems elimCycles elimCyclesGensubstReldirtypesBySort limBySort lubBySort glbBySort solveGraph$fPrettyRelMap $fShowRels$fEqRelsTCErrorUnbound AmbiguousNoTypeNotCon EmptyCase PatternTypeDuplicateDeclsDuplicateDefnsDuplicateTyDefns CyclicTyDef NumPatternsNoSearch UnsolvableNotTyDefNoTWild NotEnoughArgs TooManyArgs UnboundTyVar NoPolyRecNoErrorTyCtx constraint constraintsforAllcOrwithConstraintsolve lookupTyDefn withTyDefnsfreshTy freshAtom$fMonoidTCError$fSemigroupTCError $fShowTCErrorprimDoc primReferenceotherDocotherReference ModuleInfo_miName _miImports_miDocs_miProps_miTys _miTydefs _miTermdefs_miTerms_miExtsClauseDefn LoadingModeREPL Standalone eraseClause $fPrettyDefn$fShowModuleInfo $fShowDefn $fGenericDefn $fAlphaDefn $fDataDefn$fSubstTypeDefnResolver FromStdlibFromDirFromCwdOrStdlibFromDirOrStdlibmiDocsmiExts miImportsmiNamemiProps miTermdefsmiTermsmiTydefsmiTys withImportsallTys allTydefsemptyModuleInfocombineModuleInfo withStdlib resolveModuleModeInferCheck containerTycontainerToConinferTelescope checkModule makeTyDefnCtx checkTyDefn checkCyclicTycheckUnboundVars checkPolyRec filterDups makeTyCtxcheckCtx checkDefncheckProperties checkPropertycheckPolyTyValidcheckTypeValidconAritycheck checkPolyTyinferinferTopcheckTop typecheck checkPatterncAbscSizecPoscIntcExpgetEltTy ensureConstr ensureConstr1 ensureConstr2ensureConstrModeensureConstrMode1ensureConstrMode2ensureEq $fShowModeParserDiscoParseErrorReservedVarName runParserindented thenIndentedwithExtssclexemesymbol reservedOpanglessemicommacolondotpipelambdanaturalreserved reservedWordsident#$fShowErrorComponentDiscoParseError$fShowDiscoParseError$fEqDiscoParseError$fOrdDiscoParseError wholeModule parseModule parseExtName parseImportparseModuleName parseTopLevel parseDeclterm parseTerm parseTerm' parseAtomparseContainer parseEllipsisparseContainerComp parseQualparseLet parseCase parseBranch parseGuards parseGuardparseAtomicPattern parsePattern parseExprparseAtomicType parsePolyTy parseType parseTypeOp EvalError UnboundError DivByZeroOverflow NonExhaustive InfiniteLoopCrash DiscoErrorModuleNotFound CyclicImport TypeCheckErrParseErrEvalErrPanicpanicoutputDiscoErrors$fPrettyDiscoError$fShowDiscoError$fShowEvalErrorCell BlackholeEMemEnvValPropVPDoneVPSearch TestResult TestReason TestReason_TestBool TestEqual TestNotFound TestFoundTestRuntimeErrorTestEnvTestVars SearchMotive SearchType Exhaustive Randomized SimpleValueSNumSUnitSInjSPairSBagSTypeValueVNumVConstVInjVUnitVPairVCloVTypeVRefVFun_VPropVBagVGraphVMapSMExistsSMForallVFunVConsVNil toSimpleValuefromSimpleValueratvvratintvvintvcharcharvenumvpairvvpairlistvvlist emptyTestEnv getTestEnv testIsErrortestIsOk testReasontestEnv extendPropEnvextendResultEnvemptyMemallocate allocateRecset prettyValue' prettyValueprettyTestFailureprettyTestResult $fShowValFun $fShowMem $fShowCell $fShowValue $fShowValProp$fShowTestResult$fShowTestReason_$fFunctorTestReason_$fFoldableTestReason_$fTraversableTestReason_ $fShowTestEnv$fSemigroupTestEnv$fMonoidTestEnv$fShowTestVars$fSemigroupTestVars$fMonoidTestVars$fShowSearchMotive$fShowSearchType$fShowSimpleValue$fEqSimpleValue$fOrdSimpleValue invertMotiveinvertPropResultgenerateSamplesValueEnumerationenumVoidenumUnitenumBoolenumNenumZenumFenumQenumCenumSetenumListenumType enumTypes enumerateTypeenumerateTypes runDesugar desugarDefn desugarTermdesugarProperty desugarBranch desugarGuards compileThing compileTermcompileProperty compileDefnscompileDefnGroup compileDTerm compilePrimcompilePrimErr compileCase compileBranch compileGuards compileMatch compileUOp compileBOpCESKrunCESKsteprunTesteval $fShowCESK $fShowFrame DiscoConfigTopInfo debugModeinitDiscoConfig DiscoEffects EvalEffects discoConfiglastFile replModInfotopEnv topModMaprunDisco inputTopEnvparseDiscoModulerunTCM runTCMWith typecheckToploadDiscoModuleloadParsedDiscoModuleloadFileaddToREPLModule setREPLModule loadDefsFromloadDefdispatch discoCommands parseLine handleLoad$fShowDocInput $fShowCmdTag $fEqCmdTag$fEqREPLCommandType$fShowREPLCommandType$fEqREPLCommandCategory$fShowREPLCommandCategory$fShowREPLExpr DiscoOptsevaluatecmdFile checkFile debugFlag discoOpts discoInfo discoMain'polysemy-1.7.1.0-L6KUFCAfnWCEMExUQkTgRQPolysemy.Input runInputSem runInputList runInputConstinputsinputInputPolysemy.ReaderReader+polysemy-zoo-0.7.0.2-815TXwj5QN7Az0JNPh6WekPolysemy.RandomRandom runRandomIO runRandomrandomRrandomRandomRPolysemy.StatehoistStateIntoStateT stateToST runStateSTRef stateToIO runStateIORef execLazyState evalLazyState runLazyState execState evalStaterunStatemodify'modifygetsputgetStateGetPut-unbound-generics-0.4.1-2XChRStN8EW9S5NfZafGkB%Unbound.Generics.LocallyNameless.NameNamePolysemy.InternalSem&Unbound.Generics.LocallyNameless.Freshbase Data.FoldablefoldrGHC.BaseMonoidcontainers-0.6.2.1Data.Map.InternalMap Semigroupversion getBinDir getLibDir getDynLibDir getDataDir getLibexecDir getSysconfDirgetDataFileName identifier||.-.+./.<.>=.==.GHC.Realmod