h$Cz/2      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) 2017-2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela None(c) 2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela  Safe-Inferred0(c) 2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela Noneb code-conjureO(n)". Compares the simplicity of two s. An expression e1 is strictly simpler than another expression e2 if the first of the following conditions to distingish between them is: e1 is smaller in size/length than e2 , e.g.: x + y < x + (y + z);or, e1$ has less variable occurrences than e2,or, e1# has fewer distinct constants than e2 , e.g.:  1 + 1 < 0 + 1.9They're otherwise considered of equal complexity, e.g.: x + y and y + z. 9> (xx -+- yy) `compareComplexity` (xx -+- (yy -+- zz)) LT 0> (xx -+- yy) `compareComplexity` (xx -+- xx) EQ 1> (xx -+- xx) `compareComplexity` (one -+- xx) GT 5> (one -+- one) `compareComplexity` (zero -+- one) LT 0> (xx -+- yy) `compareComplexity` (yy -+- zz) EQ 6> (zero -+- one) `compareComplexity` (one -+- zero) EQ code-conjure/Makes the function in an application a variable code-conjureExpands recursive calls on an expression until the given size limit is reached. )> recursexpr 6 (ff xx) (ff xx) f x :: Int > recursexpr 6 (ff xx) (one -+- ff xx) 1 + (1 + (1 + (1 + f x))) :: Int > recursexpr 6 (ff xx) (if' pp one (xx -*- ff xx)) (if p then 1 else x * (if p then 1 else x * f x)) :: Int > recursexpr 6 (ff xx) (if' pp one (xx -*- ff (gg xx))) (if p then 1 else x * (if p then 1 else g x * f (g (g x)))) :: Int code-conjureChecks if the given recursive call apparently terminates. The first argument indicates the functional variable indicating the recursive call. (> apparentlyTerminates ffE (ff xx) False 5> apparentlyTerminates ffE (if' pp zero (ff xx)) True7This function only allows recursion in the else clause: 6> apparentlyTerminates ffE (if' pp (ff xx) zero) False apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero) False code-conjureChecks if the given functional expression may refrain from evaluating its next argument. +> mayNotEvaluateArgument (plus :$ xx) False *> mayNotEvaluateArgument (andE :$ pp) TrueThis returns false for non-funcional value even if it involves an application which may not evaluate its argument. 1> mayNotEvaluateArgument (andE :$ pp :$ qq) False;This currently works by checking if the function is an if,  or . code-conjureCreates an if  of the type of the given proxy. :> ifFor (undefined :: Int) if :: Bool -> Int -> Int -> Int > ifFor (undefined :: String) if :: Bool -> [Char] -> [Char] -> [Char]You need to provide this as part of your building blocks on the background if you want recursive functions to be considered and produced.  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) 2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela NoneN(c) 2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela None#$!  code-conjureArguments to be passed to  or  . See  for the defaults. code-conjuredefaults to 60 code-conjure0defaults to 9, keep greater than maxEquationSize code-conjure(defaults to 5, keep smaller than maxSize code-conjuredefaults to 60 code-conjureDefault arguments to conjure.60 testsfunctions of up to 9 symbols#pruning with equations up to size 5recursion up to 60 symbols. code-conjureLike  but in the pure world.Returns a triple whose: 4first element is the number of candidates consideredsecond element is the number of defined points in the given function6third element is a list of implementations encoded as 0s paired with the number of matching points. code-conjureLike $ but allows setting options through  and . code-conjure;Conjures an implementation of a partially defined function.Takes a  with the name of a function, a partially-defined function from a conjurable type, and a list of building blocks encoded as s.For example, given: square :: Int -> Int square 0 = 0 square 1 = 1 square 2 = 4 background :: [Expr] background = [ val (0::Int) , val (1::Int) , value "+" ((+) :: Int -> Int -> Int) , value "*" ((*) :: Int -> Int -> Int) , value "==" ((==) :: Int -> Int -> Bool) ](The conjure function does the following: > conjure "square" square background square :: Int -> Int -- looking through 815 candidates, 100% match, 3/3 assignments square x = x * xThe background is defined with ,  and . code-conjureLike $ but allows setting options through  and .  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~(c) 2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela None&.(c) 2021 Rudy Matela$3-Clause BSD (see the file LICENSE) Rudy Matela None+ code-conjureExtrapolate can generalize counter-examples of any types that are .! types must first be instances of/, so Extrapolate knows how to enumerate values;6, so Extrapolate can represent then manipulate values;-, so Extrapolate knows how to name variables.There are no required functions, so we can define instances with: instance Arguable OurType(However, it is desirable to define both  and .8The following example shows a datatype and its instance: (data Stack a = Stack a (Stack a) | Empty instance Arguable a => Arguable (Stack a) where subInstances s = instances (argTy1of1 s) To declare : it may be useful to use type binding operators such as: ,  and ..Instances can be automatically derived using  * which will also automatically derivate ,  and  when needed. code-conjureList of symbols allowed to appear in side-conditions. Defaults to []. See . code-conjure=Computes a list of reified subtype instances. Defaults to  . See . code-conjureUsed in the definition of  in  typeclass instances.  !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                   ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 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 wx wy wz w{ w| w} w~ w w w w w                                                                                                                             )code-conjure-0.0.2-LO1QJbBA6df6rl4EuP9Sg0 Conjure.ExprConjure.ArguableConjure.TypeBinding Conjure.UtilsConjure.ConjurableConjure.EngineConjureConjure.Arguable.DerivederiveArguable$express-0.1.6-GVboVqtCaOK6NW7flDzNwtData.Express.Fixturessixtuple quintuple quadrupletriplecommapair-|-justjustBooljustInt nothingBool nothingIntnothingcompare'if'-<--<=--/=--$-elem'insert'sort'length'null'tail'head'-++--:-unitconsCharconsBoolconsIntconsnilCharnilBoolnilInt emptyStringnilyysxxsis_ordEord' lineBreakspacedeeceebeeaeccsddccc_even'odd'absEabs'negateEnegate'const'idStringidBoolsidIntsidCharidBoolidIntidEid'times-*-plus-+-ggE-?-ggffEffminusTwominusOnethreetwoonezeroii'kkjjiixx'zzyyxxi_-||--&&-not'implies-==>-orEandEnotEtruefalsepp'rrqqppb_Data.Express.CanonfastMostSpecificVariationfastMostGeneralVariationfastCanonicalVariationsmostSpecificCanonicalVariationmostGeneralCanonicalVariationcanonicalVariations isCanonicalcanonicalization canonicalizeisCanonicalWithcanonicalizationWithcanonicalizeWithData.Express.InstancespreludeNameInstances findValidApp validApps listVarsWith lookupNames lookupNamemkComparisonLEmkComparisonLT mkEquation mkComparisonisEqOrdisOrdisEqisEqOrdTisOrdTisEqTlookupComparison mkNameWithmkNamemkOrdLessEqualmkOrdmkEq reifyName reifyEqOrdreifyOrdreifyEqData.Express.Match isSubexprOf hasInstanceOf isInstanceOf matchWithmatchData.Express.Express.DerivederiveExpressCascadingderiveExpressIfNeeded deriveExpressData.Express.ExpressexprExpressData.Express.Foldunfoldfold unfoldTriofoldTrio unfoldPairfoldPairfoldAppData.Express.HolefilllistVarsAsTypeOflistVarsnubHolesholesisHolehole holeAsTypeOf varAsTypeOfData.Express.Map renameVarsBy////- mapSubexprs mapConstsmapVars mapValuesData.Express.CoreheightdepthsizearitynubVarsvars nubConstsconsts nubValuesvalues nubSubexprssubexprsisAppisValueisVarisConstisGroundhasVar unfoldAppcompareQuicklycompareLexicographicallycompareComplexityshowExpr showPrecExpr showOpExpr toDynamicevlevalevaluateisFun isWellTyped isIllTypedmtypetyptypvar$$valvalue:$ValueExprData.Express.Name.DerivederiveNameCascadingderiveNameIfNeeded deriveNameData.Express.NamenamesnameNameData.Express.Utils.StringvariableNamesFromTemplate&leancheck-0.9.4-FE4c8WiMHKqIlWOgN0M2EhTest.LeanCheck.CorelisttiersListablearg1arg2arg3arg4arg5arg6==: argTy1of1 argTy1of2 argTy2of2 argTy1of3 argTy2of3 argTy3of3 argTy1of4 argTy2of4 argTy3of4 argTy4of4 argTy1of5 argTy2of5 argTy3of5 argTy4of5 argTy5of5 argTy1of6 argTy2of6 argTy3of6 argTy4of6 argTy5of6 argTy6of6countfromLeft fromRightelemBylistEqlistOrdmaybeEqmaybeOrdeitherEq eitherOrdpairEqpairOrdtripleEq tripleOrd quadrupleEq quadrupleOrdcompareSimplicityfunToVar recursexprapparentlyTerminatesmayNotEvaluateArgumentapplicationOldifFor ConjurablecanonicalApplicationcanonicalVarApplicationunifiedArgumentTiers mkExprTierstiersFor$fConjurable->$fConjurable(,,,,,)$fConjurable(,,,,)$fConjurable(,,,)$fConjurable(,,)$fConjurableOrdering$fConjurableDouble$fConjurableFloat$fConjurableEither$fConjurableMaybe$fConjurable(,)$fConjurable[]$fConjurableBool$fConjurableInteger$fConjurableInt$fConjurable()ArgsmaxTestsmaxSizemaxEquationSizemaxRecursionSizeargsconjpure conjpureWithconjure conjureWithcandidateExprsArguable background subInstancesmkEq1mkEq2mkEq3mkEq4mkOrd1mkOrd2mkOrd3mkOrd4 instances*==**/=**<=**<*$fArguable(,,,,,,,)$fArguable(,,,,,,)$fArguable(,,,,,)$fArguable(,,,,)$fArguableRatio$fArguableOrdering $fArguable[]$fArguable(,,,)$fArguable(,,) $fArguable(,)$fArguableEither$fArguableMaybe$fArguableChar$fArguableInteger $fArguableInt$fArguableBool $fArguable() Test.LeanCheck.Utils.TypeBindinguint4uint3uint2uint1word4word3word2word1int4int3int2int1natnaturaleithmayborderingstringcharboolrationaldoublefloatintegerintund>-->>>>>>>>>>>>:->>>>>>>>>>>:> ->>>>>>>>>>>: ->>>>>>>>>>:> ->>>>>>>>>>: ->>>>>>>>>:> ->>>>>>>>>: ->>>>>>>>:> ->>>>>>>>: ->>>>>>>:> ->>>>>>>: ->>>>>>:>->>>>>>:->>>>>:>->>>>>:->>>>:>->>>>:->>>:>->>>:->>:>->>:->:>->:-:>-:baseGHC.Base++GHC.Listfilterzip Data.Tuplefstsndmap$Data.Typeable.InternalTypeable Data.Foldableelemminimummaximumfoldr1productsumfoldl1foldl'nullfoldlfoldrlength<>Monoidmconcatmemptymappend GHC.MaybeMaybeNothingJustghc-prim GHC.TypesTyCon Data.ListisSubsequenceOfData.Traversable mapAccumR mapAccumL Data.TypeabletypeOf7typeOf6typeOf5typeOf4typeOf3typeOf2typeOf1 rnfTypeReptypeRepFingerprint typeRepTyCon typeRepArgs splitTyConAppmkFunTy funResultTygcast2gcast1gcasteqTcast showsTypeReptypeReptypeOfTypeReprnfTyContyConFingerprint tyConName tyConModule tyConPackagefindnotElem minimumBy maximumByallanyorand concatMapconcat Data.MonoidFirstgetFirstLastgetLastApgetApData.Semigroup.InternalDualgetDualEndoappEndoAllgetAllAnygetAnySumgetSumProduct getProductAltgetAlt Data.OldListunwordswordsunlineslinesunfoldrsortOnsortBysort permutations subsequencestailsinitsgroupBygroupdeleteFirstsByunzip7unzip6unzip5unzip4zipWith7zipWith6zipWith5zipWith4zip7zip6zip5zip4genericReplicate genericIndexgenericSplitAt genericDrop genericTake genericLengthinsertByinsert partition transpose intercalate intersperse intersectBy intersectunionByunion\\deleteBydeletenubBynub isInfixOf isSuffixOf isPrefixOf findIndices findIndex elemIndices elemIndex stripPrefix dropWhileEnd Data.ProxyProxyData.Type.Equality:~:Refl:~~:HReflunzip3unzipzipWith3zipWithzip3!!lookupreversebreakspansplitAtdroptake dropWhile takeWhilecycle replicaterepeatiterate'iteratescanr1scanrscanl'scanl1scanlfoldl1'initlasttailunconshead Data.MaybemapMaybe catMaybes listToMaybe maybeToList fromMaybefromJust isNothingisJustmaybe Data.Function&onfixswapuncurrycurryflip.constid GHC.Classes&&||StringData.Express.Utils.Typeable->:: typesInListtypesIn mkCompareTymkComparisonTyisFunTyfunTyCon orderingTyintTyboolTy elementTyresultTy argumentTyunFunTy finalResultTytyArity compareTy&speculate-0.4.6-3dvgZGQ91aaFMKTlywXRbGTest.Speculate.EnginepsortBysubConsequenceconditionalEquivalencesconditionalTheoryFromThyAndRepssemiTheoryFromThyAndRepsequivalencesBetweenclassesFromSchemasAndVariablesclassesFromSchemasdistinctFromSchemasconsider(theoryAndRepresentativesFromAtomsKeepingrepresentativesFromAtomsKeepingtheoryFromAtomsKeeping!theoryAndRepresentativesFromAtomsrepresentativesFromAtomstheoryFromAtoms expansionsexpansionsWithexpansionsOfTypeTest.Speculate.ReasondiscardRedundantEquations defaultKeep initialize theorizeBytheorizefinalizefinalEquationsshowThyprintThy canonicalRule canonicalEqncanonicalizeEqncollapsecomposesimplifyorientdeducecompleteappendequivalentInstance equivalent criticalPairsnormalizedCriticalPairs reductions1 isRootNormalE isRootNormalisNormal normalizeE normalize keepMaxOfkeepUpToLengthemptyThy|==|updateEquationsBy updateRulesByokThyThykeepE closureLimitcompareE canReduceTorules equationsTest.Speculate.Reason.OrderdwoBy|>Test.Speculate.Expr.GroundisFalseisTrue trueRatioinequalless lessOrEqual condEqualM condEqualequal groundBindsgroundsTest.Speculate.Expr.EquateunConditionalEquationmkConditionalEquation unComparison isEquation unEquationTest.Speculate.Expr.InstancepreludeInstances maybeHoleOfTyholeOfTy lookupTiersT lookupTiers isListableT isListable mkListable reifyListablereifyInstancesreifyInstances1 InstancesTest.Speculate.Expr.CorehasCanonInstanceOfisCanonInstanceOf unificationunifyisConstantNamed isAssignmentunrepeatedVarscompareComplexityThenIndexcompareLexicographicallyByBinds