h$vp      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                  Safe copilot-language(Report an error due to a bug in Copilot.copilot-languageReport an error due to an error detected by Copilot (e.g., user error).copilot-language5Name of the function in which the error was detected.copilot-language5Name of the package in which the function is located.copilot-languageDescription of the error.Safe !" #$% &'()  *+,-./01R 2trsxqwvy{zu3TVWU456FI789:?@GHANLMBCDEJKOPQSXYZ[\]^_`abcdefghijklmnop|}~!" #$% &'()  *+,-./01R 2trsxqwvy{zu3TVWU456FI789:?@GHANLMBCDEJKOPQSXYZ[\]^_`abcdefghijklmnop|}~Safe'( copilot-languageWrapper to use s as arguments to triggers.copilot-languageA stream in Copilot is an infinite succession of values of the same type.3Streams can be built using simple primities (e.g., !), by applying step-wise (e.g., %) or temporal transformations (e.g., , ) to streams, or by combining existing streams to form new streams (e.g., , ).copilot-languagePoint-wise application of ceiling to a stream.Unlike the Haskell variant of this function, this variant takes and returns two streams of the same type. Use a casting function to convert the result to an intergral type of your choice.Note that the result can be too big (or, if negative, too small) for that type (see the man page of ceil for details), so you must check that the value fits in the desired integral type before casting it.$This definition clashes with one in .) in Haskell's Prelude, re-exported from Language.Copilot, so you need to import this module qualified to use this function.copilot-languagePoint-wise application of floor to a stream.Unlike the Haskell variant of this function, this variant takes and returns two streams of the same type. Use a casting function to convert the result to an intergral type of your choice.Note that the result can be too big (or, if negative, too small) for that type (see the man page of floor for details), so you must check that the value fits in the desired integral type before casting it.$This definition clashes with one in .) in Haskell's Prelude, re-exported from Language.Copilot, so you need to import this module qualified to use this function.copilot-languagePoint-wise application of atan2 to the values of two streams.-For each pair of real floating-point samples x and y, one from each stream, atan2' computes the angle of the vector from (0, 0) to the point (x, y).$This definition clashes with one in -) in Haskell's Prelude, re-exported from Language.Copilot, so you need to import this module qualified to use this function.copilot-language9Streams carrying floating point numbers are instances of $!, and you can apply to them the $ functions, point-wise.copilot-language5Streams carrying fractional numbers are instances of %!, and you can apply to them the % functions, point-wise.copilot-language*Streams carrying numbers are instances of )!, and you can apply to them the ) functions, point-wise.copilot-language Dummy instance in order to make  an instance of ).copilot-language Dummy instance in order to make  an instance of ).Safe'(%copilot-languageA proposition, representing the quantification of a boolean streams over time.copilot-languageA property, representing a boolean stream that is existentially or universally quantified over time.copilot-languageA trigger, representing a function we execute when a boolean stream becomes true at a sample.copilot-languageAn observer, representing a stream that we observe during execution at every sample.copilot-language#An item of a Copilot specification.copilot-languageAn action in a specification (e.g., a declaration) that returns a value that can be used in subsequent actions.copilot-languageA specification is a list of declarations of triggers, observers, properties and theorems.Specifications are normally declared in monadic style, for example: monitor1 :: Stream Bool monitor1 = [False] ++ not monitor1 counter :: Stream Int32 counter = [0] ++ not counter spec :: Spec spec = do trigger "handler_1" monitor1 [] trigger "handler_2" (counter > 10) [arg counter] copilot-language2Return the complete list of declarations inside a  or .The word run in this function is unrelated to running the underlying specifications or monitors, and is merely related to the monad defined by a copilot-language7Filter a list of spec items to keep only the observers.copilot-language6Filter a list of spec items to keep only the triggers.copilot-language8Filter a list of spec items to keep only the properties.copilot-language6Filter a list of spec items to keep only the theorems.copilot-languageDefine a new observer as part of a specification. This allows someone to print the value at every iteration during interpretation. Observers do not have any functionality outside the interpreter.copilot-languageDefine a new trigger as part of a specification. A trigger declares which external function, or handler, will be called when a guard defined by a boolean stream becomes true.copilot-language6Universal quantification of boolean streams over time.copilot-language8Existential quantification of boolean streams over time.copilot-language (s >= 0 && s <= 10)  Safe4copilot-languageThis function allows you to label a stream with a tag, which can be used by different backends to provide additional information either in error messages or in the generated code (e.g., for traceability purposes).Semantically, a labelled stream is just the stream inside it. The use of label should not affect the observable behavior of the monitor, and how it is used in the code generated is a decision specific to each backend. SafeB copilot-language9Create a stream populated by an external global variable.The Copilot compiler does not check that the type is correct. If the list given as second argument does not constrain the type of the values carried by the stream, this primitive stream building function will match any stream of any type, which is potentially dangerous if the global variable mentioned has a different type. We rely on the compiler used with the generated code to detect type errors of this kind.copilot-languageCreate a stream carrying values of type Bool, populated by an external global variable.copilot-languageCreate a stream carrying values of type Word8, populated by an external global variable.copilot-languageCreate a stream carrying values of type Word16, populated by an external global variable.copilot-languageCreate a stream carrying values of type Word32, populated by an external global variable.copilot-languageCreate a stream carrying values of type Word64, populated by an external global variable.copilot-languageCreate a stream carrying values of type Int8, populated by an external global variable.copilot-languageCreate a stream carrying values of type Int16, populated by an external global variable.copilot-languageCreate a stream carrying values of type Int32, populated by an external global variable.copilot-languageCreate a stream carrying values of type Int64, populated by an external global variable.copilot-languageCreate a stream carrying values of type Float, populated by an external global variable.copilot-languageCreate a stream carrying values of type Double, populated by an external global variable. copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language6Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language8Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language6Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language6Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language6Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.copilot-language/Name of the global variable to make accessible.copilot-language5Values to be used exclusively for testing/simulation.   SafeDcopilot-language,Compare two streams point-wise for equality.The output stream contains the value True at a point in time if both argument streams contain the same value at that point in time.copilot-language.Compare two streams point-wise for inequality.The output stream contains the value True at a point in time if both argument streams contain different values at that point in time.SafeK& copilot-languageCreate a constant stream that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type 6< that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type < that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type < that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type < that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type < that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type ;< that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type << that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type =< that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type >< that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type 9< that is equal to the given argument, at any point in time.copilot-language1Create a constant stream carrying values of type 8< that is equal to the given argument, at any point in time.  Safe`ucopilot-languageClass to capture casting between types for which casting may be unsafe and/or result in a loss of precision or information.copilot-languagePerform an unsafe cast from Stream a to Stream b.copilot-languageClass to capture casting between types for which it can be performed safely.copilot-languagePerform a safe cast from Stream a to Stream b.copilot-languageIdentity casting.copilot-languageCast number to bigger type.copilot-languageIdentity casting.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageIdentity casting.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageIdentity casting.copilot-languageIdentity casting.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageIdentity casting.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageIdentity casting.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageCast number to bigger type.copilot-languageIdentity casting.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageCast a boolean stream to a stream of numbers, producing 1 if the value at a point in time is I, and 0 otherwise.copilot-languageIdentity casting.copilot-languageSigned to unsigned casting.copilot-languageSigned to unsigned casting.copilot-languageSigned to unsigned casting.copilot-languageSigned to unsigned casting.copilot-language-Cast from unsigned numbers to signed numbers.copilot-language-Cast from unsigned numbers to signed numbers.copilot-language-Cast from unsigned numbers to signed numbers.copilot-language-Cast from unsigned numbers to signed numbers.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language;Unsafe unsigned integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language9Unsafe signed integer promotion to floating point values.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.copilot-language$Unsafe downcasting to smaller sizes.Safebcopilot-language*A stream that contains the constant value I.copilot-language*A stream that contains the constant value F.copilot-languageApply the and (.) operator to two boolean streams, point-wise.copilot-languageApply the or (.) operator to two boolean streams, point-wise.copilot-language*Negate all the values in a boolean stream.copilot-languageApply the exclusive-or (/) operator to two boolean streams, point-wise.copilot-languageApply the implication (.) operator to two boolean streams, point-wise.44Safe'(>dcopilot-languageNegate a proposition.copilot-language1Negation of a universally quantified proposition.copilot-language4Negation of an existentially quantified proposition.Safeegcopilot-languageSee .copilot-language(Shifting values of a stream to the left.copilot-language)Shifting values of a stream to the right.copilot-languageInstance of the  class for s.Only the methods , ,  and  are defined.Safegcopilot-language Apply the & operation to two streams, point-wise.copilot-language Apply the & operation to two streams, point-wise.copilot-language(Apply a limited form of exponentiation (^) to two streams, point-wise.Either the first stream must be the constant 2, or the second must be a constant stream.Safehcopilot-languageCreate a stream that carries an element of an array in another stream.This function implements a projection of the element of an array at a given position, over time. For example, if s is a stream of type Stream (Array '5 Word8), then s .!! 3 has type  Stream Word8 and contains the 3rd element (starting from zero) of the arrays in s at any point in time. TrustworthyiSafel?copilot-languageO(log n). Insert with a function for combining the new value and old value.  f key value mp) will insert the pair (key, value) into mp if the key does not exist in the map. If the key does exist, the function will insert the pair (key, f new_value old_value)copilot-languageSame as 3, but with the combining function applied strictly.copilot-languageO(log n)'. Lookup the value at a key in the map.6The function will return the corresponding value as a (H value) or G if the key isn't in the map.copilot-languageO(log n). The expression ( def k map) returns the value at key k or returns the default value def! when the key is not in the map.Safe'(3nWcopilot-languageExceptions or kinds of errors in Copilot specifications that the analysis implemented is able to detect.copilot-language?Analyze a Copilot specification and report any errors detected.5This function can fail with one of the exceptions in .copilot-language$ instance so we can throw and catch AnalyzeExcetions.copilot-languageShow instance that prints a detailed message for each kind of exception. Safencopilot-languageTransform a Copilot Language specification into a Copilot Core specification.Safe'(>pcopilot-languageSimulate a number of steps of a given specification, printing the results in a table in comma-separated value (CSV) format.copilot-languageSimulate a number of steps of a given specification, printing the results in a table in readable format. Compared to ?, this function is slower but the output may be more readable.SafeqMcopilot-languageTransform a high-level Copilot Language specification into a low-level Copilot Core specification and pretty-print it to stdout.!" #$% &'()  *+,-./01R 2trsxqwvy{zu3TVWU456FI789:;<=>?@GHANLMBCDEJKOPQSXYZ[\]^_`abcdefghijklmnop|}~;<=>Safes!" #$% &'()  *+,-./01R 2trsxqwvy{zu3TVWU456FI789:;<=>?@GHANLMBCDEJKOPQSXYZ[\]^_`abcdefghijklmnop|}~ !"#!"$!%&!'(!')!*+!*,!*-!./!.0!12!34!35!36!37!.8!*9!*:!*;!*<!=>!1?!1@!1A!1B!*C!*D!*E!*F!*G!*H!*I!3J!3KLM!NO!1P!1Q!*R!*S!.TLU!VW!1X!NY!1Z![\!=]!*^!_`!ab!*c!*defegeheiej!kl!km!kn!kopqr!steu!1vewex!yze{!s|!s}e~!y!yeee!*!y!*!*!!a!a!a!a!%!%!%!%!%!%!%!%!%!%!%!%!!!!!_!_!_!_!_!_!_!_!_!_!_!_!_!_!_!_!_!_!_!_!!!!!!V!V!V!V!!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!N!!!!!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!1!3!3!3!3!3!3![![![![![![![![!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!"!!!'!'!.!.!.!.!.!*!*!*!*!*!*!!!L                  !!!!!!!!!!!!!onmlifh+copilot-language-3.7-4RgRPwdjEYu2UcYypaENZrCopilot.Language.PreludeCopilot.Language"Copilot.Language.Operators.BitWiseCopilot.Language.SpecCopilot.Language.Stream#Copilot.Language.Operators.Temporal!Copilot.Language.Operators.StructCopilot.Language.Operators.OrdCopilot.Language.Operators.Mux Copilot.Language.Operators.Local Copilot.Language.Operators.Label!Copilot.Language.Operators.ExternCopilot.Language.Operators.Eq#Copilot.Language.Operators.ConstantCopilot.Language.Operators.Cast"Copilot.Language.Operators.Boolean(Copilot.Language.Operators.Propositional#Copilot.Language.Operators.Integral Copilot.Language.Operators.ArrayCopilot.Language.ReifyCopilot.Language.ErrorPreludedivmodSystem.Mem.StableName.DynamicSystem.Mem.StableName.MapCopilot.Language.AnalyzeCopilot.Language.InterpretCopilotghc-primGHC.PrimseqbaseGHC.Listfilterzip System.IOprint Data.TuplefstsndGHC.Base otherwisemap$GHC.Num fromInteger-GHC.Real fromRationalGHC.EnumenumFrom enumFromThen enumFromToenumFromThenTonegate>>=>>fmapreturnControl.Monad.Failfail fromIntegral realToFrac toInteger toRational<>memptymappendmconcat<*>pure*>BoundedEnum GHC.ClassesEq GHC.FloatFloating FractionalIntegralMonadFunctorNumOrdGHC.ReadReadReal RealFloatRealFracGHC.ShowShow MonadFail Applicative Data.FoldableFoldableData.Traversable Traversable SemigroupMonoid GHC.TypesBoolCharDoubleFloatIntGHC.IntInt8Int16Int32Int64integer-wired-inGHC.Integer.TypeInteger GHC.MaybeMaybeOrderingRationalIOWord Data.EitherEitherFalseNothingJustTrueLeftRightLTEQGTideitherString<* Text.ReadreadsequencemapM sequenceAtraversereadIOreadLn appendFile writeFilereadFileinteract getContentsgetLinegetCharputStrLnputStrputCharGHC.IO.ExceptionioErrorGHC.IOFilePath userErrorIOErrornotElemallanyorand concatMapconcat sequence_mapM_productminimummaximumelemlengthnullfoldl1foldr1foldlfoldrfoldMap Data.OldListunwordswordsunlineslinesreadslex readParenreadList readsPrecText.ParserCombinators.ReadPReadSatanhacoshasinhtanhcoshsinhatanacosasintancossinlogBase**sqrtlogexppiatan2isIEEEisNegativeZeroisDenormalized isInfiniteisNaN scaleFloat significandexponent encodeFloat decodeFloat floatRange floatDigits floatRadix Data.Bits complement.|..&.Bitslcmgcd^^oddevendivModquotRemremquotrecip/floorceilingroundtruncateproperFractionmaxBoundminBoundfromEnumtoEnumpredsucc showParen showStringshowCharshowsShowSshowListshow showsPrecunzip3unzipzipWith3zipWithzip3lookupreversebreakspansplitAt dropWhile takeWhile replicaterepeatiteratescanr1scanrscanl1scanlinitlasttailhead Data.Maybemaybe Data.Functor<$>uncurrycurrysubtractsignumabs*+asTypeOf$!flip.=<<<$GHC.Err undefinederrorWithoutStackTraceerrorcompare'copilot-core-3.7-C09UhOaiw2jDxqqQ4oiNe8Copilot.Core.ExprNameCopilot.Core.TypeTyped*copilot-theorem-3.7-2TKwG9E8DKhJ3AniQzzXbqCopilot.Theorem.Prove Universal Existential impossiblebadUsage StructArgname_arg'ArgStreamAppendConstDropExternLocalVarOp1Op2Op3Label$fFloatingStream$fFractionalStream $fNumStream $fEqStream $fShowStreamPropForallExistsPropertyTriggerObserverSpecItemSpec'SpecrunSpec observerstriggers propertiestheoremsobservertriggerforallexists extractPropproptheoremarg++drop#<=>=<>mux ifThenElselocallabelexternexternBexternW8 externW16 externW32 externW64externI8 externI16 externI32 externI64externFexternD==/=constantconstBconstW8constW16constW32constW64constI8constI16constI32constI64constFconstD UnsafeCast unsafeCastCastcast$fCastInt64Int64$fCastInt32Int64$fCastInt32Int32$fCastInt16Int64$fCastInt16Int32$fCastInt16Int16$fCastInt8Int64$fCastInt8Int32$fCastInt8Int16$fCastInt8Int8$fCastWord64Word64$fCastWord32Int64$fCastWord32Word64$fCastWord32Word32$fCastWord16Int64$fCastWord16Int32$fCastWord16Word64$fCastWord16Word32$fCastWord16Word16$fCastWord8Int64$fCastWord8Int32$fCastWord8Int16$fCastWord8Word64$fCastWord8Word32$fCastWord8Word16$fCastWord8Word8$fCastBoolInt64$fCastBoolInt32$fCastBoolInt16$fCastBoolInt8$fCastBoolWord64$fCastBoolWord32$fCastBoolWord16$fCastBoolWord8$fCastBoolBool$fUnsafeCastInt8Word8$fUnsafeCastInt16Word16$fUnsafeCastInt32Word32$fUnsafeCastInt64Word64$fUnsafeCastWord8Int8$fUnsafeCastWord16Int16$fUnsafeCastWord32Int32$fUnsafeCastWord64Int64$fUnsafeCastWord8Double$fUnsafeCastWord16Double$fUnsafeCastWord32Double$fUnsafeCastWord64Double$fUnsafeCastWord8Float$fUnsafeCastWord16Float$fUnsafeCastWord32Float$fUnsafeCastWord64Float$fUnsafeCastInt8Double$fUnsafeCastInt16Double$fUnsafeCastInt32Double$fUnsafeCastInt64Double$fUnsafeCastInt8Float$fUnsafeCastInt16Float$fUnsafeCastInt32Float$fUnsafeCastInt64Float$fUnsafeCastInt16Int8$fUnsafeCastInt32Int8$fUnsafeCastInt32Int16$fUnsafeCastInt64Int8$fUnsafeCastInt64Int16$fUnsafeCastInt64Int32$fUnsafeCastWord16Word8$fUnsafeCastWord32Word8$fUnsafeCastWord32Word16$fUnsafeCastWord64Word8$fUnsafeCastWord64Word16$fUnsafeCastWord64Word32truefalse&&||notxor==>$fNegatablePropProp$fNegatablePropProp0.^..<<..>>. $fBitsStream^.!!reifycsv interpret prettyPrintGHC.WordWord8Word16Word32Word64 DynStableNamemakeDynStableNamehashDynStableName insertWith insertWith'findWithDefaultMapgetSizegetMapempty singletonmember notMemberinsertfindAnalyzeExceptionanalyze$fExceptionAnalyzeExceptionGHC.Exception.Type Exception$fShowAnalyzeExceptionDropAppliedToNonAppendDropIndexOverflowReferentialCycleDropMaxViolation NestedArrayTooMuchRecursion InvalidFieldDifferentTypes RedeclaredBadNumberOfArgsBadFunctionArgType bitReverse64 bitReverse32 bitReverse16 bitReverse8 byteSwap64 byteSwap32 byteSwap16tysizetylength accessorname fieldnameStructtypenametoValuesValueFieldTypeArray SimpleTypeSStructSArraySDoubleSFloatSWord64SWord32SWord16SWord8SInt64SInt32SInt16SBoolSInt8typeOf simpleTypeUType uTypeTypeCopilot.Core.Type.Array arrayelemssizearray InnerTypeFlattenflatten