h&      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe )*1w copilot-coreImplementation of an array that uses type literals to store length. copilot-coreSmart array constructor that only type checks if the length of the given list matches the length of the array at type level. copilot-core Return the elements of an array. copilot-coreReturn the elemts of an array.Typing for Core.7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe)*1  copilot-core!A untyped type (no phantom type). copilot-coreA typed expression, from which we can obtain the two type representations used by Copilot:  and  .  copilot-coreA simple, monomorphic representation of types that facilitates putting variables in heterogeneous lists and environments in spite of their types being different. copilot-coreA Type representing the types of expressions or values handled by Copilot Core.Note that both arrays and structs use dependently typed features. In the former, the length of the array is part of the type. In the latter, the names of the fields are part of the type.' copilot-coreA field in a struct. The name of the field is a literal at the type level.) copilot-coreThe field of a struct, together with a representation of its type.+ copilot-coreThe value of that is a product or struct, defined as a constructor with several fields., copilot-core2Returns the name of struct in the target language.- copilot-core2Returns the name of struct in the target language.. copilot-core9Transforms all the struct's fields into a list of values./ copilot-coreExtract the name of a field.0 copilot-coreExtract the name of a field.1 copilot-coreExtract the name of an accessor (a function that returns a field of a struct).2 copilot-coreExtract the name of an accessor (a function that returns a field of a struct).3 copilot-core+Return the length of an array from its type4 copilot-core+Return the length of an array from its type5 copilot-core8Return the total (nested) size of an array from its type6 copilot-core8Return the total (nested) size of an array from its typeD copilot-core+Type equality, used to help type inference.2  !"$#%&'()*+-.,/01234562 !"$#%&  5634)*.'(,-+/012-Internal representation of Copilot operators.7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe)* H copilot-coreTernary operators.J copilot-coreBinary operators.b copilot-coreUnary operators.a copilot-core,Array access/projection of an array element.y copilot-coreCasting operator.z copilot-coreProjection of a struct field.3HIJVQPKLMNORSTUWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz3bcdefghijklmnopqrstuvwxyzJVQPKLMNORSTUWXYZ[\]^_`aHI6Internal representation of Copilot stream expressions.7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe)*9{ copilot-coreA untyped expression that carries the information about the type of the expression as a value, as opposed to exposing it at type level (using an existential). copilot-core6Internal representation of Copilot stream expressions.The Core representation mimics the high-level Copilot stream, but the Core representation contains information about the types of elements in the stream. copilot-coreAn index for the drop operator. copilot-coreA name of a trigger, an external variable, or an external function. copilot-coreA stream identifier.{|}~{|}~7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe)* copilot-coreA Copilot specification is a list of streams, together with monitors on these streams implemented as observers, triggers or properties. copilot-coreA property, representing a boolean stream that is existentially or universally quantified over time. copilot-coreA trigger, representing a function we execute when a boolean stream becomes true at a sample. copilot-coreAn observer, representing a stream that we observe during interpretation at every sample. copilot-core>A stream in an infinite succession of values of the same type.Stream can carry different types of data. Boolean streams play a special role: they are used by other parts (e.g., >) to detect when the properties being monitored are violated.7Intermediate representation for Copilot specifications.7(c) 2011 National Institute of Aerospace / Galois, Inc.Safe  &%#$"! '()*+-.,/0123456HIJa`_^]\[ZYXWUTSRONMLKPVQbzyxwvutsrqponmlkjihgfecd{~|}       !"#$%&'()*+,,--+./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}}~dLJ!"#$%&'((copilot-core-3.17-JdEoqXfJH59DXYObsTWNdVCopilot.Core.Type.ArrayCopilot.Core.TypeCopilot.Core.OperatorsCopilot.Core.ExprCopilot.Core.Spec Copilot.CoreArrayarray arrayElems arrayelems $fShowArrayUType uTypeTypeTypedtypeOf simpleType SimpleTypeSBoolSInt8SInt16SInt32SInt64SWord8SWord16SWord32SWord64SFloatSDoubleSArraySStructTypeBoolInt8Int16Int32Int64Word8Word16Word32Word64FloatDoubleStructFieldValuetypeNametypenametoValues fieldName fieldname accessorName accessorname typeLengthtylengthtypeSizetysize $fShowField $fTypedArray $fTypedDouble $fTypedFloat $fTypedWord64 $fTypedWord32 $fTypedWord16 $fTypedWord8 $fTypedInt64 $fTypedInt32 $fTypedInt16 $fTypedInt8 $fTypedBool$fEqSimpleType$fTestEqualityTYPEType$fShowt $fEqUTypeOp3MuxOp2AndOrAddSubMulModDivFdivPowLogbAtan2EqNeLeGeLtGtBwAndBwOrBwXorBwShiftLBwShiftRIndexOp1NotAbsSignRecipExpSqrtLogSinTanCosAsinAtanAcosSinhTanhCoshAsinhAtanhAcoshCeilingFloorBwNotCastGetFieldUExpr uExprType uExprExprExprConstDropLocalVar ExternVarLabelDropIdxNameIdSpec specStreams specObservers specTriggersspecPropertiesProperty propertyName propertyExprTrigger triggerName triggerGuard triggerArgsObserver observerName observerExprobserverExprTypeStreamstreamId streamBuffer streamExprstreamExprTypeghc-prim GHC.TypesIntbaseGHC.IntWordGHC.Word byteSwap64 byteSwap32 byteSwap16 bitReverse8 bitReverse64 bitReverse32 bitReverse16