express 0.1.8 → 0.1.10

raw patch · 26 files changed

+546/−63 lines, 26 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• .gitignore +1/−0
• Makefile +1/−0
• README.md +78/−4
• bench/runtime/zero/bench/compare.runtime +1/−1
• bench/runtime/zero/bench/pairs.runtime +1/−1
• bench/runtime/zero/bench/sort.runtime +1/−0
• bench/runtime/zero/bench/tiers.runtime +1/−1
• bench/runtime/zero/eg/u-conjure.runtime +1/−0
• bench/runtime/zero/eg/u-extrapolate.runtime +1/−1
• bench/runtime/zero/eg/u-speculate.runtime +1/−1
• changelog.md +49/−0
• eg/u-conjure.hs +194/−0
• eg/u-extrapolate.hs +30/−21
• eg/u-speculate.hs +11/−15
• express.cabal +13/−3
• mk/depend.mk +22/−0
• src/Data/Express.hs +3/−0
• src/Data/Express/Express.hs +5/−6
• src/Data/Express/Fixtures.hs +4/−0
• src/Data/Express/Hole.hs +38/−0
• src/Data/Express/Match.hs +17/−1
• test/express.hs +6/−1
• test/hole.hs +4/−0
• test/match.hs +27/−0
• test/model/eg/u-conjure.out +24/−0
• test/model/eg/u-extrapolate.out +12/−7

@@ -17,6 +17,7 @@ tags eg/u-extrapolate eg/u-speculate+eg/u-conjure bench/compare bench/pairs bench/sort

@@ -25,6 +25,7 @@ BENCHS = \   eg/u-extrapolate \   eg/u-speculate \+  eg/u-conjure \   bench/compare \   bench/pairs \   bench/sort \

@@ -182,10 +182,10 @@  	tiersFor :: Expr -> [[Expr]] 	tiersFor e  =  case show (typ e) of-	  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])-	  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])-	  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])-	  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])+	  "Int"    ->  mapT val (tiers :: [[Int]])+	  "Bool"   ->  mapT val (tiers :: [[Bool]])+	  "[Int]"  ->  mapT val (tiers :: [[ [Int] ]])+	  "[Bool]" ->  mapT val (tiers :: [[ [Bool] ]]) 	  _        ->  []  Above, we restrict ourselves to `Int`, `Bool`, `[Int]` and `[Bool]` as test@@ -337,6 +337,78 @@ limitations.  +Example 5: u-Conjure+--------------------++Using Express, it takes less than 70 lines of code to define a function+`conjure` that generates a function from a partial function definition+and a list of primitives.++__Example 5.1.__ Given:++	factorial :: Int -> Int+	factorial 0  =  1+	factorial 1  =  1+	factorial 2  =  2+	factorial 3  =  6+	factorial 4  =  24++Running:++	conjure "factorial" factorial+	  [ val (0 :: Int)+	  , val (1 :: Int)+	  , value "+" ((+) :: Int -> Int -> Int)+	  , value "*" ((*) :: Int -> Int -> Int)+	  , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+	  , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])+	  ]++Prints:++	  factorial :: Int -> Int+	  factorial x  =  foldr (*) 1 (enumFromTo 1 x)++__Example 5.2.__ Given:++	(+++) :: [Int] -> [Int] -> [Int]+	[x] +++ [y]  =  [x,y]+	[x,y] +++ [z,w]  =  [x,y,z,w]++Running:++	conjure "++" (+++)+      [ val (0 :: Int)+      , val (1 :: Int)+      , val ([] :: [Int])+      , value "head" (head :: [Int] -> Int)+      , value "tail" (tail :: [Int] -> [Int])+      , value ":" ((:) :: Int -> [Int] -> [Int])+      , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])+      ]++Prints:++	(++) :: [Int] -> [Int] -> [Int]+	xs ++ ys  =  foldr (:) ys xs++Please see the [u-Conjure] example in the [eg](eg) folder for the full code.++[u-Conjure] has some limitations:++* the maximum function size (7) or number of tests (60) are not configurable;+* the maximum function size has to be kept small (<=7)+  for a reasonable runtime.+  Due to this, several simple functions are simply out-of-reach;+* the number of primitive functions given has to be kept small (<12)+  for a reasonable runtime;+* there is no support for explicitly recursive functions+  thought it is possible to pass `foldr` and similar functions as primitives.++Please see [Conjure] library for an experimental version that addresses+some the above limitations.++ Further reading --------------- @@ -360,9 +432,11 @@ [LeanCheck]:   https://hackage.haskell.org/package/leancheck [Extrapolate]: https://hackage.haskell.org/package/extrapolate [Speculate]:   https://hackage.haskell.org/package/speculate+[Conjure]:     https://hackage.haskell.org/package/conjure  [u-Speculate]:   eg/u-speculate.hs [u-Extrapolate]: eg/u-extrapolate.hs+[u-Conjure]:     eg/u-conjure.hs  [express-logo]: https://github.com/rudymatela/express/raw/master/doc/express.svg?sanitize=true 

@@ -1,1 +1,1 @@-0.01+0.02

@@ -1,1 +1,1 @@-0.00+0.01

@@ -0,0 +1,1 @@+0.19

@@ -1,1 +1,1 @@-0.18+0.20

@@ -0,0 +1,1 @@+0.34

@@ -1,1 +1,1 @@-0.00+0.01

@@ -1,1 +1,1 @@-0.30+0.32

@@ -0,0 +1,49 @@+Changelog for Express+=====================+++v0.1.10+-------++* add the `hasHole` and `isComplete` functions+* add the `encompasses` function+* add `appendInt` to `Data.Express.Fixtures`+* add the `u-conjure` example+* the `Express` typeclass now requires `Show`+* improve examples in the `eg/` folder+* improve tests of `hasInstanceOf` and `isInstanceOf`+* improve tests+* add this changelog+++v0.1.8+------++* slightly change behaviour of `canonicalVariations` and related functions.+* add more fixtures and improve fixtures' documentation+* improve Makefile and test scripts+* use GitHub actions as CI+++v0.1.6+------++* add `compareLexicographically` and `compareQuickly`+* define behaviour of `canonicalVariations` for some undefined cases+* improve haddock documentation+* improve tests+++v0.1.4+------++* add the `fill` and `isFun` functions+* `Data.Express.Fixtures`: more fixtures, define fixity+* add fixity for some fixtures+* improve documentation, tests and lint+++v0.1.3+------++See the git commit log for v0.1.3 and previous versions.

@@ -0,0 +1,194 @@+-- u-conjure.hs -- u-Conjure+--+-- This is a prototype for Conjure, a library for conjuring code+-- out of partially implemented functions.+--+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+--+--+-- To run this you need to have both LeanCheck and Express installed:+--+-- $ cabal install leancheck+-- $ cabal install express+--+-- If installation fails, use v1-install:+--+-- $ cabal v1-install leancheck+-- $ cabal v1-install express+import Data.List+import Data.Maybe+import Data.Express+import Data.Typeable+import Test.LeanCheck.Error+++square :: Int -> Int+square 0  =  0+square 1  =  1+square 2  =  4+square 3  =  9+square 4  =  16++add :: Int -> Int -> Int+add 0 0  =  0+add 0 1  =  1+add 1 0  =  1+add 1 1  =  2++factorial :: Int -> Int+factorial 0  =  1+factorial 1  =  1+factorial 2  =  2+factorial 3  =  6+factorial 4  =  24++second :: [Int] -> Int+second [x,y]  =  y+second [x,y,z]  =  y+second [x,y,z,w]  =  y++-- reverse+reverse' :: [Int] -> [Int]+reverse' [x,y]  =  [y,x]+reverse' [x,y,z]  =  [z,y,x]++-- +++(+++) :: [Int] -> [Int] -> [Int]+[x] +++ [y]  =  [x,y]+[x,y] +++ [z,w]  =  [x,y,z,w]+++main :: IO ()+main  =  do+  conjure "square"    square    primitives+  conjure "add"       add       primitives+  conjure "factorial" factorial primitives++  conjure "factorial"   factorial+    [ val (0 :: Int)+    , val (1 :: Int)+    , value "+" ((+) :: Int -> Int -> Int)+    , value "*" ((*) :: Int -> Int -> Int)+    , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+    , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])+    ]++  conjure "second"  second   listPrimitives+  conjure "++"      (+++)    listPrimitives+  conjure "reverse" reverse' listPrimitives++  -- even by using fold and some cheating,+  -- this function is out of reach+  --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs+  --  reverse xs  =  foldr (flip (++) . unit) [] xs+  conjure "reverse" reverse' $ listPrimitives +++    [ value "unit" ((:[]) :: Int -> [Int])+    , value "++" ((++) :: [Int] -> [Int] -> [Int])+    -- these last two are cheats:+    , value "flip" (flip :: ([Int]->[Int]->[Int]) -> [Int] -> [Int] -> [Int])+    , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])+    ]++  where++  primitives :: [Expr]+  primitives =+    [ val (0 :: Int)+    , val (1 :: Int)+    , val (2 :: Int)+    , val (3 :: Int)+    , value "+" ((+) :: Int -> Int -> Int)+    , value "*" ((*) :: Int -> Int -> Int)+    , value "-" ((-) :: Int -> Int -> Int)+    ]++  listPrimitives :: [Expr]+  listPrimitives =+    [ val (0 :: Int)+    , val (1 :: Int)+    , val ([] :: [Int])+    , value "head" (head :: [Int] -> Int)+    , value "tail" (tail :: [Int] -> [Int])+    , value ":" ((:) :: Int -> [Int] -> [Int])+    , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])+    ]+++conjure :: Typeable f => String -> f -> [Expr] -> IO ()+conjure nm f primitives  =  do+  print (value nm f) -- prints the type signature+  case conjureImplementations nm f primitives of+    []    -> putStrLn $ "cannot conjure"+--  es    -> putStrLn $ unlines $ map showEq es  -- uncomment to show all found variations+    (e:_) -> putStrLn $ showEq e+  putStrLn ""+  where+  showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)+++conjureImplementations :: Typeable f => String -> f -> [Expr] -> [Expr]+conjureImplementations nm f primitives  =+  [ appn -==- e+  | e <- candidateExprsFrom $ exs ++ primitives+  , isTrue (appn -==- e)+  ]+  where+  appn  =  application nm f primitives+  (ef:exs)  =  unfoldApp appn+  isTrue e  =  all (errorToFalse . eval False) . map (e //-) $ definedBinds appn+++definedBinds :: Expr -> [[(Expr,Expr)]]+definedBinds ffxx  =  [bs | bs <- bss, errorToFalse . eval False $ e //- bs]+  where+  e  =  ffxx -==- ffxx+  bss  =  take 360 $ groundBinds ffxx+++application :: Typeable f => String -> f -> [Expr] -> Expr+application nm f es  =  mostGeneralCanonicalVariation $ appn (value nm f)+  where+  appn ff | isFun ff   =  case [e | Just (_ :$ e) <- (map (ff $$)) es] of+                          [] -> error "application: could not find type representative"+                          (e:_) -> appn (ff :$ holeAsTypeOf e)+          | otherwise  =  ff+++candidateExprsFrom :: [Expr] -> [Expr]+candidateExprsFrom  =  concat . take 7 . expressionsT+  where+  expressionsT ds  =  [ds] \/ (delay $ productMaybeWith ($$) es es)+    where+    es = expressionsT ds+++(-==-) :: Expr -> Expr -> Expr+ex -==- ey  =  headOr (val False) . map (:$ ey) $ mapMaybe ($$ ex)+  [ value "==" ((==) :: Int -> Int -> Bool)+  , value "==" ((==) :: Bool -> Bool -> Bool)+  , value "==" ((==) :: [Int] -> [Int] -> Bool)+  , value "==" ((==) :: [Bool] -> [Bool] -> Bool)+  ]+  where+  headOr x []     =  x+  headOr _ (x:_)  =  x+++lhs, rhs :: Expr -> Expr+lhs (((Value "==" _) :$ e) :$ _)  =  e+rhs (((Value "==" _) :$ _) :$ e)  =  e+++groundBinds :: Expr -> [[(Expr,Expr)]]+groundBinds e  =  concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e]+++tiersFor :: Expr -> [[Expr]]+tiersFor e  =  case show (typ e) of+  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])+  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])+  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])+  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])+  _        ->  []

@@ -29,7 +29,7 @@ import Data.List import Data.Maybe import Data.Express-import Test.LeanCheck hiding (counterExample, check)+import Test.LeanCheck hiding (counterExamples, check)  main :: IO () main  =  do@@ -39,6 +39,9 @@   putStrLn "length . nub = length  (incorrect when there are repeated elements)"   check $ \xs -> length (nub xs :: [Int]) == length xs +  putStrLn "xs `union` ys == ys `union` xs  (incorrect for repeated elements)"+  check $ \(xs,ys) -> xs `union` ys == ys `union` (xs :: [Int])+   putStrLn "\\(x,y) -> x + y == y + x"   check $ \(x,y) -> x + y == y + (x :: Int) @@ -53,24 +56,23 @@   check :: (Listable a, Express a) => (a -> Bool) -> IO ()-check prop  =  putStrLn $ case counterExample 500 prop of-  Nothing -> "+++ Tests passed.\n"-  Just ce -> "*** Falsified, counterexample:  " ++ show ce-          ++ case counterExampleGeneralization 500 prop ce of-             Nothing -> ""-             Just g -> "\n               generalization:  " ++ show g-          ++ "\n"---counterExample :: (Listable a, Express a) => Int -> (a -> Bool) -> Maybe Expr-counterExample maxTests prop  =  listToMaybe-  [expr x | x <- take maxTests list, not (prop x)]+check prop  =  putStrLn $ case counterExampleAndGeneralizations 500 prop of+  []      ->  "+++ Tests passed.\n"+  (ce:gs) -> unlines+           $ ("*** Falsified, counterexample:  " ++ showExpr ce)+           : ["               generalization:  " ++ showExpr g | g <- gs ] -counterExampleGeneralization :: Express a => Int -> (a -> Bool) -> Expr -> Maybe Expr-counterExampleGeneralization maxTests prop e  =  listToMaybe-  [g | g <- candidateGeneralizations e-     , all (not . prop . evl) (take maxTests $ grounds g)]+counterExamples :: (Listable a, Express a) => Int -> (a -> Bool) -> [Expr]+counterExamples maxTests prop  =  [expr x | x <- take maxTests list, not (prop x)] +counterExampleAndGeneralizations :: (Listable a, Express a)+                                 => Int -> (a -> Bool) -> [Expr]+counterExampleAndGeneralizations maxTests prop  =+  case counterExamples maxTests prop of+  [] -> []+  (ce:_) -> ce : discardLater isInstanceOf+                   [ g | g <- candidateGeneralizations ce+                       , all (not . prop . evl) (take maxTests $ grounds g) ]  candidateGeneralizations :: Expr -> [Expr] candidateGeneralizations  =  map canonicalize@@ -94,8 +96,15 @@  tiersFor :: Expr -> [[Expr]] tiersFor e  =  case show (typ e) of-  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])-  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])-  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])-  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])+  "Int"    ->  mapT val (tiers :: [[Int]])+  "Bool"   ->  mapT val (tiers :: [[Bool]])+  "[Int]"  ->  mapT val (tiers :: [[ [Int] ]])+  "[Bool]" ->  mapT val (tiers :: [[ [Bool] ]])   _        ->  []++discardLater :: (a -> a -> Bool) -> [a] -> [a]+discardLater (?)  =  d+  where+  d []      =  []+  d (x:xs)  =  x : d (discard (? x) xs)+  discard p  =  filter (not . p)

@@ -13,7 +13,7 @@ -- -- Limitations: ----- * even with pruning, this program still prints some redundant rules;+-- * this program prints redundant equations; -- * there is no way to configure maximum number of tests to consider an --   equation true; -- * runtime is exponential as you add more symbols to speculate about.@@ -71,25 +71,22 @@   showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)  speculateAbout :: [Expr] -> [Expr]-speculateAbout  =  discardLater hasRewrite-                .  discardLaterInstances+speculateAbout  =  discardLater canBeSimplifiedBy+                .  discardLater isInstanceOf                 .  concatMap trueCanonicalVariations-                .  discardLaterInstances+                .  discardLater (\e1 e2 -> isntIdentity e2 && e2 `isInstanceOf` e1)                 .  sort                 .  filter isTrue                 .  candidateEquationsFrom   where-  hasRewrite e1 e2  =  isRule e2 && e1 `hasInstanceOf` lhs e2+  e1 `canBeSimplifiedBy` e2  =  isRule e2 && e1 `hasInstanceOf` lhs e2  trueCanonicalVariations :: Expr -> [Expr]-trueCanonicalVariations  =  discardLaterInstances+trueCanonicalVariations  =  discardLater isInstanceOf                          .  filter isTrue                          .  filter isntIdentity                          .  canonicalVariations -discardLaterInstances :: [Expr] -> [Expr]-discardLaterInstances =  discardLater (\e1 e2 -> isntIdentity e2 && e1 `isInstanceOf` e2)- candidateEquationsFrom :: [Expr] -> [Expr] candidateEquationsFrom es'  =  [e1 -==- e2 | e1 <- es, e2 <- es, e1 >= e2]   where@@ -106,15 +103,14 @@ isTrue  =  all (eval False) . take 60 . grounds  grounds :: Expr -> [Expr]-grounds e  =  map (e //-)  .  concat-           $  products [mapT ((,) v) (tiersFor v) | v <- nubVars e]+grounds e  =  map (e //-) . concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e]  tiersFor :: Expr -> [[Expr]] tiersFor e  =  case show (typ e) of-  "Int"    ->  mapT val (tiers `asTypeOf` [[undefined :: Int]])-  "Bool"   ->  mapT val (tiers `asTypeOf` [[undefined :: Bool]])-  "[Int]"  ->  mapT val (tiers `asTypeOf` [[undefined :: [Int]]])-  "[Bool]" ->  mapT val (tiers `asTypeOf` [[undefined :: [Bool]]])+  "Int"    ->  mapT val (tiers :: [[Int]])+  "Bool"   ->  mapT val (tiers :: [[Bool]])+  "[Int]"  ->  mapT val (tiers :: [[ [Int] ]])+  "[Bool]" ->  mapT val (tiers :: [[ [Bool] ]])   _        ->  []  (-==-) :: Expr -> Expr -> Expr

@@ -1,6 +1,6 @@ -- Cabal file for express name: express-version: 0.1.8+version: 0.1.10 synopsis: Dynamically-typed expressions involving applications and variables. description:   Express is a library for manipulating dynamically typed Haskell expressions.@@ -23,6 +23,7 @@  extra-doc-files: README.md                , TODO.md+               , changelog.md                , doc/express.svg extra-source-files: .gitignore                   , .travis.yml@@ -43,7 +44,9 @@                   , bench/runtime/zero/versions                   , bench/runtime/zero/bench/*.runtime                   , bench/runtime/zero/eg/*.runtime-tested-with: GHC==8.8+tested-with: GHC==9.0+           , GHC==8.10+           , GHC==8.8            , GHC==8.6            , GHC==8.4            , GHC==8.2@@ -59,7 +62,7 @@ source-repository this   type:           git   location:       https://github.com/rudymatela/express-  tag:            v0.1.8+  tag:            v0.1.10  library   exposed-modules:     Data.Express@@ -262,6 +265,13 @@ benchmark u-speculate   type:                exitcode-stdio-1.0   main-is:             u-speculate.hs+  hs-source-dirs:      eg+  build-depends:       base >= 4 && < 5, express, leancheck >= 0.9.4+  default-language:    Haskell2010++benchmark u-conjure+  type:                exitcode-stdio-1.0+  main-is:             u-conjure.hs   hs-source-dirs:      eg   build-depends:       base >= 4 && < 5, express, leancheck >= 0.9.4   default-language:    Haskell2010

@@ -106,6 +106,28 @@   test/Test/ListableExpr.hs \   bench/tiers.hs \   mk/toplibs+eg/u-conjure: \+  eg/u-conjure.hs \+  mk/toplibs+eg/u-conjure.o: \+  src/Data/Express/Utils/Typeable.hs \+  src/Data/Express/Utils/TH.hs \+  src/Data/Express/Utils/String.hs \+  src/Data/Express/Utils/List.hs \+  src/Data/Express.hs \+  src/Data/Express/Name.hs \+  src/Data/Express/Name/Derive.hs \+  src/Data/Express/Match.hs \+  src/Data/Express/Map.hs \+  src/Data/Express/Instances.hs \+  src/Data/Express/Hole.hs \+  src/Data/Express/Fold.hs \+  src/Data/Express/Express.hs \+  src/Data/Express/Express/Derive.hs \+  src/Data/Express/Core.hs \+  src/Data/Express/Canon.hs \+  src/Data/Express/Basic.hs \+  eg/u-conjure.hs eg/u-extrapolate: \   eg/u-extrapolate.hs \   mk/toplibs

@@ -142,7 +142,9 @@   , isWellTyped   , isFun   , hasVar+  , hasHole   , isGround+  , isComplete    -- ** Comparing Exprs   , compareComplexity@@ -239,6 +241,7 @@   , isInstanceOf   , hasInstanceOf   , isSubexprOf+  , encompasses    -- -- -- Data.Express.Express exports -- -- -- 

@@ -60,7 +60,7 @@ -- '-:', '->:', '->>:', '->>>:', '->>>>:', '->>>>>:', ... -- -- For types with atomic values, just declare @ expr = val @-class Typeable a => Express a where+class (Show a, Typeable a) => Express a where   expr :: a -> Expr  instance Express ()        where  expr  =  val@@ -91,15 +91,14 @@                   :$ expr x :$ expr y :$ expr z :$ expr w  instance Express a => Express [a] where-  expr xs@[]-    | typeOf xs == typeOf ""  =  value "\"\"" ([] -: xs)-    | otherwise               =  value "[]" ([] -: xs)-  expr xs@(y:ys)              =  value ":"  ((:) ->>: xs) :$ expr y :$ expr ys+  expr xs  =  case xs of+              [] -> val xs+              (y:ys) -> value ":" ((:) ->>: xs) :$ expr y :$ expr ys   -- instances of further types and arities -- -instance (Integral a, Show a, Express a) => Express (Ratio a) where+instance (Integral a, Express a) => Express (Ratio a) where   expr  =  val -- The following would allow zero denominators -- expr (n % d) = constant "%" ((%) -:> n) :$ expr n :$ expr d

@@ -168,6 +168,7 @@   , bs_, pps, qqs   , and', or'   , sum', product'+  , appendInt    -- ** Maybes   , nothing@@ -834,6 +835,9 @@   where   err  =  error $ "(-:-): unhandled type " ++ show (typ e1) infixr 5 -:-++appendInt :: Expr+appendInt  =  value "++" ((++) :: [Int] -> [Int] -> [Int])  -- | List concatenation lifted over the 'Expr' type. --   Works for the element types 'Int', 'Char' and 'Bool'.

@@ -16,6 +16,8 @@   -- * Typed holes   , hole   , isHole+  , hasHole+  , isComplete   , holes   , nubHoles   , holeAsTypeOf@@ -130,6 +132,42 @@ -- such as @f (g (h (f (g (h x)))))@. nubHoles :: Expr -> [Expr] nubHoles  =  nubSort . holes++-- | /O(n)/.+-- Returns whether an expression contains a hole+--+-- > > hasHole $ hole (undefined :: Bool)+-- > True+--+-- > > hasHole $ value "not" not :$ val True+-- > False+--+-- > > hasHole $ value "not" not :$ hole (undefined :: Bool)+-- > True+hasHole :: Expr -> Bool+hasHole  =  any isHole . values++-- | /O(n)/.+-- Returns whether an expression is complete.+-- A complete expression is one without holes.+--+-- > > isComplete $ hole (undefined :: Bool)+-- > False+--+-- > > isComplete $ value "not" not :$ val True+-- > True+--+-- > > isComplete $ value "not" not :$ hole (undefined :: Bool)+-- > False+--+-- 'isComplete' is the negation of 'hasHole'.+--+-- > isComplete  =  not . hasHole+--+-- 'isComplete' is to 'hasHole' what+-- 'isGround' is to 'hasVar'.+isComplete :: Expr -> Bool+isComplete  =  not . hasHole  -- | -- Generate an infinite list of variables

@@ -11,6 +11,7 @@   , isInstanceOf   , hasInstanceOf   , isSubexprOf+  , encompasses   ) where @@ -76,7 +77,7 @@ -- checks if the first expression -- is an instance of the second -- in terms of variables.--- (cf. 'hasInstanceOf')+-- (cf. 'encompasses', 'hasInstanceOf') -- -- > > let zero = val (0::Int) -- > > let one  = val (1::Int)@@ -96,6 +97,21 @@ -- >  (one -+- (yy -+- xx)) `isInstanceOf` (zero -+- yy)  =  False isInstanceOf :: Expr -> Expr -> Bool e1 `isInstanceOf` e2 = isJust $ e1 `match` e2+++-- |+-- Given two 'Expr's,+-- checks if the first expression+-- encompasses the second expression+-- in terms of variables.+--+-- This is equivalent to flipping the arguments of 'isInstanceOf'.+--+-- > zero `encompasses` xx    =  False+-- >   xx `encompasses` zero  =  True+encompasses :: Expr -> Expr -> Bool+encompasses  =  flip isInstanceOf+  -- | -- Checks if any of the subexpressions of the first argument 'Expr'

@@ -72,6 +72,10 @@   , expr ([0::Int,1])  == zero -:- one -:- nil   , holds n $ \xs -> expr xs == foldr (-:-) nil (map expr (xs :: [Int]))   , holds n $ \ps -> expr ps == foldr (-:-) nilBool (map expr (ps :: [Bool]))+  , expr (""::String) == value "\"\"" ""+  , expr (""::String) == val ""+  , expr ("a"::String) == unit (val 'a')+  , expr ("abc"::String) == val 'a' -:- val 'b' -:- unit (val 'c')    -- Transforming Maybes into Exprs   , expr (Nothing    :: Maybe Int)   ==  nothing@@ -81,7 +85,7 @@   , holds n $ \x -> expr (Just x) == just (expr (x :: Int))   , holds n $ \p -> expr (Just p) == just (expr (p :: Bool)) -  -- Transforming Tuples into Exprs+  -- Transforming tuples into Exprs   , expr ((0,False) :: (Int,Bool))  ==  pair zero false   , expr ((True,1)  :: (Bool,Int))  ==  pair true one @@ -89,6 +93,7 @@   , holds n $ \x -> show (expr x) == show (x :: ()) ++ " :: ()"   , holds n $ \x -> show (expr x) == show (x :: Int) ++ " :: Int"   , holds n $ \p -> show (expr p) == show (p :: Bool) ++ " :: Bool"+  , holds n $ \s -> show (expr s) == show (s :: String) ++ " :: [Char]"   , holds n $ \x -> show (expr x) == show (x :: ((),Maybe Int,[Bool]))                                         ++ " :: ((),(Maybe Int),[Bool])"   ]

@@ -18,6 +18,10 @@    , holds n $ \e -> isHole e ==> isVar e   , holds n $ \e1 e2 -> isHole (e1 :$ e2) == False+  , holds n $ \e -> isHole e ==> hasHole e+  , holds n $ \e1 e2 -> (hasHole e1 || hasHole e2) == hasHole (e1 :$ e2)+  , holds n $ \e -> hasHole e == (not . null . holes) e+  , holds n $ \e -> isComplete e == not (hasHole e)    , holds n $ \e -> holes e `isSubsequenceOf` vars e   , holds n $ \e -> nubHoles e `isSubsetOf` holes e

@@ -15,6 +15,7 @@   , holds n $ \(IntE e1) (IntE e2) -> (e1 -+- e2) `isInstanceOf` (xx -+- yy)   , holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> not ((e1 -+- e2) `isInstanceOf` (xx -+- xx))   , holds n $ \e                   -> e /= zero ==> not (e `isInstanceOf` zero)+  , holds n $ \e1 e2 -> e1 `encompasses` e2 == e2 `isInstanceOf` e1    ,       (zero -+- one)       `isInstanceOf` (xx -+- yy)   ,       (zero -+- zero)      `isInstanceOf` (xx -+- yy)@@ -54,4 +55,30 @@                        == ((ef :$ ex) `isInstanceOf` e || ef `hasInstanceOf` e                                                        || ex `hasInstanceOf` e)   , holds n $ \e1 e2 -> e1 `hasInstanceOf` e2 == any (`isInstanceOf` e2) (subexprs e1)++  -- isInstanceOf is reflexive and transitive+  -- but not antisymmetric nor asymmetric+  -- so is no order+  , holds n $ isReflexive     isInstanceOf+  , holds n $ isTransitive    isInstanceOf+  , fails n $ isAntisymmetric isInstanceOf -- structural equality+  , fails n $ isAsymmetric    isInstanceOf+  , fails n $ isTotalOrder    isInstanceOf+  , fails n $ isPartialOrder  isInstanceOf++  -- the same goes for hasInstanceOf+  , holds n $ isReflexive     hasInstanceOf+  , holds n $ isTransitive    hasInstanceOf+  , fails n $ isAntisymmetric hasInstanceOf+  , fails n $ isAsymmetric    hasInstanceOf+  , fails n $ isTotalOrder    hasInstanceOf+  , fails n $ isPartialOrder  hasInstanceOf++  -- one can construct the following equivalence+  , holds n $ isEquivalence (isInstanceOf &&&& flip isInstanceOf)++  -- the following is not an equivalence+  , fails n $ isEquivalence (isInstanceOf |||| flip isInstanceOf)+  -- so it cannot be used as an argument to nubBy+  -- which requires equivalence according to the Haskell 2010 Report.   ]

@@ -0,0 +1,24 @@+square :: Int -> Int+square x  =  x * x++add :: Int -> Int -> Int+add x y  =  x + y++factorial :: Int -> Int+cannot conjure++factorial :: Int -> Int+factorial x  =  foldr (*) 1 (enumFromTo 1 x)++second :: [Int] -> Int+second xs  =  head (tail xs)++(++) :: [Int] -> [Int] -> [Int]+xs ++ ys  =  foldr (:) ys xs++reverse :: [Int] -> [Int]+cannot conjure++reverse :: [Int] -> [Int]+reverse xs  =  foldr (foldr (:) . unit) [] xs+

@@ -2,20 +2,25 @@ +++ Tests passed.  length . nub = length  (incorrect when there are repeated elements)-*** Falsified, counterexample:  [0,0] :: [Int]-               generalization:  x:x:xs :: [Int]+*** Falsified, counterexample:  [0,0]+               generalization:  x:x:xs +xs `union` ys == ys `union` xs  (incorrect for repeated elements)+*** Falsified, counterexample:  ([],[0,0])+               generalization:  (xs,x:x:xs)+               generalization:  ([],x:x:xs)+ \(x,y) -> x + y == y + x +++ Tests passed.  \x -> x == x + 1  (always incorrect)-*** Falsified, counterexample:  0 :: Int-               generalization:  x :: Int+*** Falsified, counterexample:  0+               generalization:  x  \(x,y) -> x + y == x + x  (incorrect)-*** Falsified, counterexample:  (0,1) :: (Int,Int)+*** Falsified, counterexample:  (0,1)  \(x,y) -> x /= y  (incorrect whenever x and y are equal)-*** Falsified, counterexample:  (0,0) :: (Int,Int)-               generalization:  (x,x) :: (Int,Int)+*** Falsified, counterexample:  (0,0)+               generalization:  (x,x)