code-conjure 0.1.0 → 0.1.2

raw patch · 24 files changed

+184/−53 lines, 24 filesdep ~expressPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: express

API changes (from Hackage documentation)

Files

• .gitignore +1/−0
• Makefile +1/−0
• TODO.md +0/−3
• bench/runtime/zero/bench/self.runtime +1/−0
• bench/runtime/zero/eg/arith.runtime +1/−1
• bench/runtime/zero/eg/bools.runtime +1/−1
• bench/runtime/zero/eg/factorial.runtime +1/−1
• bench/runtime/zero/eg/ints.runtime +1/−1
• bench/runtime/zero/versions +1/−1
• bench/self.hs +24/−0
• code-conjure.cabal +7/−4
• eg/bools.hs +31/−5
• eg/factorial.hs +4/−6
• eg/ints.hs +23/−7
• mk/depend.mk +10/−0
• src/Conjure/Conjurable.hs +16/−9
• src/Conjure/Engine.hs +9/−5
• src/Conjure/Utils.hs +4/−0
• stack.yaml +1/−1
• test/conjurable.hs +7/−0
• test/model/bench/self.out +16/−0
• test/model/eg/bools.out +10/−2
• test/model/eg/factorial.out +1/−1
• test/model/eg/ints.out +13/−5

@@ -32,6 +32,7 @@ eg/factorial eg/ints eg/list+bench/self proto/u-conjure test/expr test/conjurable

@@ -10,6 +10,7 @@   eg/factorial \   eg/ints \   eg/bools \+  bench/self \   proto/u-conjure  TESTS = \

@@ -7,9 +7,6 @@   We should only enumerate functions that were tested to be different.   We can limit the tests to the ones that are defined in the given function. -* use FitSpec's notation of `"factorial n"` to name the variables-  instead of just `"factorial"`- * use partially defined implementations?      partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)

@@ -0,0 +1,1 @@+0.01

@@ -1,1 +1,1 @@-3.72+4.55

@@ -1,1 +1,1 @@-2.78+3.29

@@ -1,1 +1,1 @@-2.18+2.31

@@ -1,1 +1,1 @@-7.00+1.95

@@ -1,4 +1,4 @@ GHC 8.10.4 leancheck-0.9.4-express-0.1.6+express-0.1.8 speculate-0.4.6

@@ -0,0 +1,24 @@+-- self.hs: conjuring functions through themselves+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++main :: IO ()+main = do+  cj "?" ((+) :: Int -> Int -> Int)   background+  cj "?" ((*) :: Int -> Int -> Int)   background+  cj "i" ((+1) :: Int -> Int)         background+  cj "d" ((subtract 1) :: Int -> Int) background+  where+  -- the monomorphism restriction strikes again+  cj :: Conjurable f => String -> f -> [Expr] -> IO ()+  cj  =  conjureWith args{maxSize=3,maxEquationSize=0}++background :: [Expr]+background =+  [ val (0::Int)+  , val (1::Int)+  , value "+" ((+) :: Int -> Int -> Int)+  , value "*" ((*) :: Int -> Int -> Int)+  ]

@@ -3,7 +3,7 @@ -- Copyright (C) 2021 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name:                code-conjure-version:             0.1.0+version:             0.1.2 synopsis:            conjure Haskell functions out of partial definitions description:   Conjure is a tool that produces Haskell functions out of partial definitions.@@ -27,8 +27,9 @@ extra-source-files: .gitignore                   , .github/workflows/build.yml                   , Makefile-                  , proto/*.hs+                  , bench/*.hs                   , eg/*.hs+                  , proto/*.hs                   , mk/All.hs                   , mk/Toplibs.hs                   , mk/depend.mk@@ -37,10 +38,12 @@                   , mk/haskell.mk                   , mk/install-on                   , stack.yaml+                  , bench/runtime/zero/bench/*.runtime                   , bench/runtime/zero/eg/*.runtime                   , bench/runtime/zero/proto/*.runtime                   , bench/runtime/zero/versions                   , bench/versions+                  , test/model/bench/*.out                   , test/model/eg/*.out                   , test/model/proto/*.out                   , test/sdist@@ -53,7 +56,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/conjure-  tag:             v0.1.0+  tag:             v0.1.2  library   exposed-modules: Conjure@@ -66,7 +69,7 @@                , leancheck >= 0.9.4                , template-haskell                , speculate >= 0.4.6-               , express >= 0.1.6+               , express >= 0.1.8   hs-source-dirs:      src   default-language:    Haskell2010 

@@ -4,16 +4,28 @@ -- Distributed under the 3-Clause BSD licence (see the file LICENSE). import Conjure +and' :: [Bool] -> Bool+and' [p]      =  p+and' [p,q]    =  p && q+and' [p,q,r]  =  p && q && r++or' :: [Bool] -> Bool+or' [p]      =  p+or' [p,q]    =  p || q+or' [p,q,r]  =  p || q || r+ main :: IO () main = do-  conjure "and" (and :: [Bool] -> Bool) background-  conjure "or"  (or  :: [Bool] -> Bool) background+  conjure "and" (and' :: [Bool] -> Bool) background+  conjure "or"  (or'  :: [Bool] -> Bool) background +  -- conjure can use fold as well+  conjureWithMaxSize 4 "and" (and' :: [Bool] -> Bool) backgroundWithFold+  conjureWithMaxSize 4 "or"  (or'  :: [Bool] -> Bool) backgroundWithFold+ background :: [Expr] background =-  [ val False-  , val True-  , value "not" not+  [ value "not" not   , value "||" (||)   , value "&&" (&&)   , value "null" (null :: [Bool] -> Bool)@@ -21,6 +33,11 @@   , value "tail" (tail :: [Bool] -> [Bool])   ] +backgroundWithFold :: [Expr]+backgroundWithFold  =+    value "foldr" (foldr :: (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool)+  : background+ -- target (for and):  -- and ps  =  if null ps then True else head ps && and (tail ps)@@ -28,3 +45,12 @@ -- or -- and ps  =  null ps || head ps && and (tail ps) --            1    2  3  4    5  6  7    8    9 symbols+--+--+-- for or, we only reach the solution at size 11:+--+-- or' ps  =  not (null ps || not (head ps || or' (tail ps)))+--+-- unfortunately this is an ill-case,+-- I think there are smaller expressions that rewrite to the above bigger+-- expression so it is only found at the bigger size.

@@ -14,7 +14,7 @@   main :: IO ()-main  =  conjure "factorial" factorial background+main  =  conjure "factorial n" factorial background   background :: [Expr]@@ -25,21 +25,19 @@   , value "*" ((*) :: Int -> Int -> Int)   , value "dec" (subtract 1 :: Int -> Int)   , value "isZero" ((==0) :: Int -> Bool)-  , val False-  , val True   ]   -- the actual factorial function:--- factorial x  =  if x == 0 then 1 else x * factorial (x - 1)+-- factorial n  =  if n == 0 then 1 else n * factorial (n - 1) --                 1  2 3  4      5      6 7 8         9 10 11 symbols -- -- OR ----- factorial x  =  if x == 0 then 1 else x * factorial (dec x)+-- factorial n  =  if n == 0 then 1 else n * factorial (dec n) --                 1  2 3  4      5      6 7 8          9  10 symbols -- -- OR ----- factorial x  =  if (isZero x) then 1 else (x * factorial (dec x))+-- factorial n  =  if (isZero n) then 1 else (n * factorial (dec n)) --                 1   2      3       4       5 6 7          8   9 symbols

@@ -13,18 +13,29 @@ third [x,y,z]  =  z third [x,y,z,w]  =  z +sum' :: [Int] -> Int+sum' [x]      =  x+sum' [x,y]    =  x+y+sum' [x,y,z]  =  x+y+z++product' :: [Int] -> Int+product' [x]      =  x+product' [x,y]    =  x*y+product' [x,y,z]  =  x*y*z+ main :: IO () main = do-  conjure "second"  (second  :: [Int] -> Int) background-  conjure "third"   (third   :: [Int] -> Int) background-  conjure "sum"     (sum     :: [Int] -> Int) background-  conjure "product" (product :: [Int] -> Int) background+  conjure "second"  (second   :: [Int] -> Int) background+  conjure "third"   (third    :: [Int] -> Int) background+  conjure "sum"     (sum'     :: [Int] -> Int) background+  conjure "product" (product' :: [Int] -> Int) background +  conjureWithMaxSize 4 "sum"     (sum'     :: [Int] -> Int) backgroundWithFold+  conjureWithMaxSize 4 "product" (product' :: [Int] -> Int) backgroundWithFold+ background :: [Expr] background =-  [ val False-  , val True-  , val (0 :: Int)+  [ val (0 :: Int)   , val (1 :: Int)   , value "+" ((+) :: Int -> Int -> Int)   , value "*" ((*) :: Int -> Int -> Int)@@ -32,6 +43,11 @@   , value "head" (head :: [Int] -> Int)   , value "tail" (tail :: [Int] -> [Int])   ]++backgroundWithFold :: [Expr]+backgroundWithFold  =+    value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+  : background  -- sum xs      =  if null xs then 0 else head xs + sum (tail xs) -- product xs  =  if null xs then 1 else head xs * product (tail xs)

@@ -1,3 +1,13 @@+bench/self: \+  bench/self.hs \+  mk/toplibs+bench/self.o: \+  src/Conjure/Utils.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Conjurable.hs \+  bench/self.hs eg/arith: \   eg/arith.hs \   mk/toplibs

@@ -19,6 +19,7 @@   , reifyEquality   , canonicalApplication   , canonicalVarApplication+  , conjureHoles   , conjureIfs   , conjureTiersFor   , conjureMkEquation@@ -112,10 +113,13 @@ conjureReification1 x  =  (hole x, ifFor x, conjureEquality x, conjureTiers x)  conjureReification :: Conjurable a => a -> [Reification1]-conjureReification x  =  conjureType x [conjureReification1 bool]+conjureReification x  =  nubOn (\(eh,_,_,_) -> eh)+                      $  conjureType x [conjureReification1 bool]   where   bool :: Bool   bool  =  error "conjureReification: evaluated proxy boolean value (definitely a bug)"+-- The use of nubOn above is O(n^2).+-- So long as there is not a huge number of subtypes of a, so we're fine.  -- | Reifies equality to be used in a conjurable type. --@@ -146,6 +150,9 @@ mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]] mkExprTiers a  =  mapT val (tiers -: [[a]]) +conjureHoles :: Conjurable f => f -> [Expr]+conjureHoles f  =  [eh | (eh,_,_,Just _) <- conjureReification f]+ conjureIfs :: Conjurable f => f -> [Expr] conjureIfs f  =  [eef | (_,eef,_,Just _) <- conjureReification f] @@ -287,17 +294,17 @@ resTy :: (a -> b) -> b resTy _  =  undefined -canonicalArgumentVariables :: Conjurable f => f -> [Expr]-canonicalArgumentVariables  =  unfoldApp-                            .  mostGeneralCanonicalVariation-                            .  foldApp-                            .  conjureArgumentHoles- canonicalApplication :: Conjurable f => String -> f -> Expr-canonicalApplication nm f  =  foldApp (value nm f : canonicalArgumentVariables f)+canonicalApplication  =  canonicalWhatApplication value  canonicalVarApplication :: Conjurable f => String -> f -> Expr-canonicalVarApplication nm f  =  foldApp (var nm f : canonicalArgumentVariables f)+canonicalVarApplication  =  canonicalWhatApplication var++canonicalWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr+canonicalWhatApplication what nm f  =  mostGeneralCanonicalVariation . foldApp+                                    $  what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f)+  where+  (nf:nas)  =  words nm ++ repeat ""   

@@ -91,10 +91,11 @@   candidates  =  filter (\e -> typ e == typ ffxx)               .  concat               .  take maxSize-              $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===) [es ++ conjureIfs f]+              $  candidateExprs nm f maxEquationSize maxRecursiveCalls (===)+                 [nub $ [val False, val True] ++ es ++ conjureIfs f]   ffxx   =  canonicalApplication nm f   vffxx  =  canonicalVarApplication nm f-  rrff   =  var nm f+  (rrff:_)   =  unfoldApp vffxx    (===), (?=?) :: Expr -> Expr -> Bool   e1 === e2  =  isReallyTrue      (e1 -==- e2)@@ -147,14 +148,17 @@ -- -- > conjureWithMaxSize 10 "function" function [...] conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()-conjureWithMaxSize sz  =  conjureWith args{maxSize = sz}+conjureWithMaxSize sz  =  conjureWith args+                       {  maxSize = sz+                       ,  maxEquationSize = min sz (maxEquationSize args)+                       }  -- | Like 'conjure' but allows setting options through 'Args'/'args'. -- -- > conjureWith args{maxSize = 11} "function" function [...] conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () conjureWith args nm f es  =  do-  print (var nm f)+  print (var (head $ words nm) f)   putStr $ "-- looking through " ++ show ncs ++ " candidates"   hFlush stdout   case rs of@@ -178,7 +182,7 @@ candidateExprs nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess   where   (ef:exs)  =  unfoldApp $ canonicalVarApplication nm f-  thy  =  theoryFromAtoms (===) sz $ [nub (b_:map holeAsTypeOf exs)] \/ ess+  thy  =  theoryFromAtoms (===) sz $ [conjureHoles f] \/ ess   expressionsT ds  =  filterT (\e -> count (== ef) (vars e) <= mc)                    $  filterT (isRootNormalE thy)                    $  ds \/ (delay $ productMaybeWith ($$) es es)

@@ -17,6 +17,7 @@   , module Data.Typeable    , count+  , nubOn   ) where @@ -29,3 +30,6 @@  count :: (a -> Bool) -> [a] -> Int count p  =  length . filter p++nubOn :: Eq b => (a -> b) -> [a] -> [a]+nubOn f  =  nubBy ((==) `on` f)

@@ -11,4 +11,4 @@ extra-deps: - leancheck-0.9.4 - speculate-0.4.6-- express-0.1.6+- express-0.1.8

@@ -21,6 +21,13 @@ tests n  =   [ True +  , canonicalApplication "not"   not  ==  not' pp+  , canonicalApplication "not q" not  ==  not' qq+  , canonicalApplication "negate"   (negate :: Int -> Int)  ==  negate' xx+  , canonicalApplication "negate i" (negate :: Int -> Int)  ==  negate' ii+  , canonicalApplication "+"     ((+) :: Int -> Int -> Int)  ==  xx -+- yy+  , canonicalApplication "+ i j" ((+) :: Int -> Int -> Int)  ==  ii -+- jj+   , holds n $ \x y -> (x <==> y)  ==  (x == (y :: ()))   , holds n $ \x y -> (x <==> y)  ==  (x == (y :: Int))   , holds n $ \p q -> (p <==> q)  ==  (p == (q :: Bool))

@@ -0,0 +1,16 @@+(?) :: Int -> Int -> Int+-- looking through 52 candidates, 100% match, 60/60 assignments+x ? y  =  x + y++(?) :: Int -> Int -> Int+-- looking through 52 candidates, 100% match, 60/60 assignments+x ? y  =  x * y++i :: Int -> Int+-- looking through 24 candidates, 100% match, 60/60 assignments+i x  =  x + 1++d :: Int -> Int+-- looking through 24 candidates+cannot conjure+

@@ -1,8 +1,16 @@ and :: [Bool] -> Bool--- looking through 1207 candidates, 100% match, 60/60 assignments+-- looking through 1207 candidates, 100% match, 14/14 assignments and ps  =  null ps || head ps && and (tail ps)  or :: [Bool] -> Bool--- looking through 1207 candidates, 90% match, 54/60 assignments+-- looking through 1207 candidates, 78% match, 11/14 assignments or ps  =  head ps || or (tail ps)++and :: [Bool] -> Bool+-- looking through 19 candidates, 100% match, 14/14 assignments+and ps  =  foldr (&&) True ps++or :: [Bool] -> Bool+-- looking through 19 candidates, 100% match, 14/14 assignments+or ps  =  foldr (||) False ps 

@@ -1,4 +1,4 @@ factorial :: Int -> Int -- looking through 8576 candidates, 100% match, 6/6 assignments-factorial x  =  if isZero x then 1 else x * factorial (dec x)+factorial n  =  if isZero n then 1 else n * factorial (dec n) 

@@ -1,16 +1,24 @@ second :: [Int] -> Int--- looking through 12955 candidates, 100% match, 47/47 assignments+-- looking through 636 candidates, 100% match, 47/47 assignments second xs  =  head (tail xs)  third :: [Int] -> Int--- looking through 12955 candidates, 100% match, 34/34 assignments+-- looking through 636 candidates, 100% match, 34/34 assignments third xs  =  head (tail (tail xs))  sum :: [Int] -> Int--- looking through 12955 candidates, 8% match, 5/60 assignments+-- looking through 636 candidates, 13% match, 5/37 assignments sum xs  =  if null (tail xs) then head xs else sum xs  product :: [Int] -> Int--- looking through 12955 candidates, 36% match, 22/60 assignments-product xs  =  0 * head (tail (tail (tail xs)))+-- looking through 636 candidates, 13% match, 5/37 assignments+product xs  =  if null (tail xs) then head xs else product xs++sum :: [Int] -> Int+-- looking through 15 candidates, 100% match, 37/37 assignments+sum xs  =  foldr (+) 0 xs++product :: [Int] -> Int+-- looking through 15 candidates, 100% match, 37/37 assignments+product xs  =  foldr (*) 1 xs