úÎAª<Ü     (c) Levent ErkokBSD3erkokl@gmail.com experimentalSafe+The actual annotation.›Plugin options. Note that we allow picking multiple solvers, which will all be run in parallel. If you want to run all available solvers, use the option m. The default is to error-out on failure, using the default-SMT solver picked by SBV, which is currently Z3.Continue even if proof failsVSkip the proof. Can be handy for properties that we currently do not want to focus on.*Produce verbose output, good for debuggingDProduce really verbose output, use only when things go really wrong!Perform quickCheck +Uninterpret this binding for proof purposes 9Use these names for the arguments; need not be exhaustive NIf a list-input is found, use this length. If not specified, we will complain! Use Z3  Use Yices Use BoolectorUse CVC4 Use MathSATUse ABCUse all installed solvers-A property annotation, using default options.)Synonym for sbv really, just looks cooler   (c) Levent ErkokBSD3erkokl@gmail.com experimentalNone+The values kept track of by the interpreterThe kinds used by the plugin'Configuration info as we run the pluginThe interpreter monadInterpreter environment2Certain "very-polymorphic" things are just special8Given the user options, determine which solver(s) to use:Structural lifting of a boolean function (eq/neq) over Val Symbolic equality over variablesMCompute the span given a Tick. Returns the old-span if the tick span useless. Compute the span for a binding.!&Show a GHC span in user-friendly form."Outputable instance for Val#Outputable instance for S.Kind$Outputable instance for SKind.%&'()*+,-./0123456789:;<=>?@ABC !"#$+%&'()*+,-./0123456789:;<=>?@ABC !%&'()*+,-./012 3456789:;<=>?@ABC !"#$(c) Levent ErkokBSD3erkokl@gmail.com experimentalNoneD#Dispatch the analyzer over bindingsEProve an SBVTheoremFgSafely execute an action, catching the exceptions, printing and returning False if something goes wrongGReturns True if proof went thruHÿ’Is this really a dictionary in disguise? This is a terrible hack, and the ice is thin here. But it seems to work. TODO: Figure out if there's a better way of doing this. Note that this function really does get applications, when those dictionaries are parameterized by others. Think of the case where "Eq [a]" dictionary depends on "Eq a", for instance. In these cases, GHC to produces applications.IUninterpret an expressionJBConvert a Core type to an SBV Type, retaining functions and tuplesDEFGHIKJDDEFGHIKJ(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone<LTWhat tuple-sizes we support? We go upto 15, but would be easy to change if necessaryM.Build the initial environment containing typesN2Build the initial environment containing functionsO#Basic conversions, only on one kindP?Symbolic functions supported by the plugin; those from a class.Q DestructorsRlThese types show up during uninterpretation, but are not really "interesting" as they are singly inhabited.STCertain things are just too special, as they uniformly apply to uninterpreted types.T$Lift a binary type, with result boolULift a unary typeVLift a binary typeW0Lift a binary type, where second argument is IntX/Lift a unary SBV function that via kind/integerY3Lift a unary SBV function to the plugin value spaceZ>Lift a two argument SBV function to our the plugin value space[DLifting an equality is special; since it acts uniformly over tuples.LMNOPQRSTUVWXYZ[\]MNQRSLMNOPQRSTUVWXYZ[\](c) Levent ErkokBSD3erkokl@gmail.com experimentalNoneEntry point to the plugin(c) Levent ErkokBSD3erkokl@gmail.com experimentalNone  ^      !"#$%&'()*+,-./012345678!9:;<=>?@ABCD"EFGHIJKLMNOPQRSTUVWXYZ[\]^_`absbvPl_EEkjMw3MOUSDmPfRNNOS1oData.SBV.PluginData.SBV.Plugin.DataData.SBV.Plugin.CommonData.SBV.Plugin.AnalyzeData.SBV.Plugin.EnvData.SBV.Plugin.Plugin SBVAnnotationSBVoptions SBVOption IgnoreFailureSkipVerboseDebug QuickCheck UninterpretNamesListSizeZ3Yices BoolectorCVC4MathSATABC AnySolversbvtheorempluginValSKindConfigEvalEnvSpecials pickSolvers liftEqValeqValtickSpanbindSpanshowSpan$fOutputableVal$fOutputableKind$fOutputableSKindBaseTypTupLstFuncKBaseKTupKLstKFunisGHCiopts sbvAnnotationcfgEnvcurLocflags machWordSize uninterestingrUninterpreted rUsedNamesrUITypesspecialstcMapenvMapdestMapcoreMap isEqualityisTupleisList analyzeBindprovesafelyproveItisReallyADictionary uninterpretgetType mkValidNamesupportTupleSizes buildTCEnv buildFunEnv basicFuncssymFuncs buildDestsuninterestingTypes buildSpecials tlift2Booltlift1tlift2 tlift2ShRotlift1Intlift1lift2liftEqthToGHCgrabTH