code-conjure (empty) → 0.0.2
raw patch · 44 files changed
+2681/−0 lines, 44 filesdep +basedep +code-conjuredep +expresssetup-changed
Dependencies added: base, code-conjure, express, leancheck, speculate, template-haskell
Files
- .gitignore +35/−0
- .travis.yml +90/−0
- LICENSE +30/−0
- Makefile +68/−0
- README.md +177/−0
- Setup.hs +5/−0
- TODO.md +33/−0
- code-conjure.cabal +81/−0
- doc/conjure.svg +118/−0
- eg/arith.hs +43/−0
- eg/bools.hs +32/−0
- eg/factorial.hs +47/−0
- eg/ints.hs +41/−0
- eg/runtime/zero/eg/arith.runtime +1/−0
- eg/runtime/zero/eg/bools.runtime +1/−0
- eg/runtime/zero/eg/factorial.runtime +1/−0
- eg/runtime/zero/eg/ints.runtime +1/−0
- eg/runtime/zero/proto/u-conjure.runtime +1/−0
- eg/runtime/zero/versions +4/−0
- eg/versions +19/−0
- mk/All.hs +6/−0
- mk/Toplibs.hs +4/−0
- mk/depend.mk +108/−0
- mk/ghcdeps +50/−0
- mk/haddock-i +36/−0
- mk/haskell.mk +140/−0
- mk/install-on +33/−0
- proto/u-conjure.hs +167/−0
- src/Conjure.hs +61/−0
- src/Conjure/Arguable.hs +331/−0
- src/Conjure/Conjurable.hs +100/−0
- src/Conjure/Engine.hs +188/−0
- src/Conjure/Expr.hs +174/−0
- src/Conjure/TypeBinding.hs +120/−0
- src/Conjure/Utils.hs +139/−0
- stack.yaml +14/−0
- test/Test.hs +43/−0
- test/expr.hs +37/−0
- test/model/eg/arith.out +16/−0
- test/model/eg/bools.out +8/−0
- test/model/eg/factorial.out +4/−0
- test/model/eg/ints.out +16/−0
- test/model/proto/u-conjure.out +18/−0
- test/sdist +40/−0
+ .gitignore view
@@ -0,0 +1,35 @@+# gitignore for Conjure+#+# Part of Conjure, Copyright 2020 Rudy Matela,+# distribued under the 3-clause BSD license.++# temporary files+*~+*.swp+mk/toplibs++# Haskell stuff+*.hi+*.o+dist-newstyle+dist++# Haskell docs+doc/*.html+doc/*.js+doc/*.json+doc/*.css+doc/*.png+doc/src++# Tag files+tags+TAGS++# benches, prototypes and test programs+eg/arith+eg/bools+eg/factorial+eg/ints+proto/u-conjure+test/expr
+ .travis.yml view
@@ -0,0 +1,90 @@+# .travis.yml file for Conjure+#+# Copyright: (c) 2017-2021 Rudy Matela+# License: 3-Clause BSD (see the file LICENSE)+# Maintainer: Rudy Matela <rudy@matela.com.br>++language: c # not really++notifications:+ email:+ on_failure: change++sudo: false++cache:+ directories:+ - $HOME/.ghc+ - $HOME/.cabal+ - $HOME/.stack++before_install:+- export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH+- ghc --version+- cabal --version+- haddock --version+- du -hd3 ~/.cabal ~/.ghc || true+- du -hd4 ~/.stack || true+- rm -f ~/.cabal/config && cabal update+# Download and unpack the stack executable+# "Once Travis whitelists the stack.dev files," simply include stack in the+# addons section. -- https://docs.haskellstack.org/en/stable/travis_ci/+- mkdir -p ~/.local/bin+- export PATH=$HOME/.local/bin:$PATH+- travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'+- stack config set system-ghc --global true+- stack --version+- cabal install leancheck express speculate || cabal install leancheck express speculate --lib++script:+- make && make test+- make haddock+- make test-sdist+- cabal test --ghc-option=-O0+- stack --resolver $STACKVER --no-terminal --skip-ghc-check test --ghc-options=-O0++matrix:+ allow_failures:+ - ghc: 'head'+ include:+ - ghc: 'head'+ env: GHCVER=head CABALVER=head STACKVER=nightly-2020-03-28+ addons: {apt: {packages: [ghc-head, cabal-install-head], sources: hvr-ghc}}+ - ghc: '8.10'+ env: GHCVER=8.10.1 CABALVER=3.2 STACKVER=nightly-2020-03-28+ addons: {apt: {packages: [ghc-8.10.1, cabal-install-3.2], sources: hvr-ghc}}+ - ghc: '8.8'+ env: GHCVER=8.8.3 CABALVER=3.0 STACKVER=lts-15.6+ addons: {apt: {packages: [ghc-8.8.3, cabal-install-3.0], sources: hvr-ghc}}+ - ghc: '8.6'+ env: GHCVER=8.6.5 CABALVER=2.4 STACKVER=lts-14.27+ addons: {apt: {packages: [ghc-8.6.5, cabal-install-2.4], sources: hvr-ghc}}+ - ghc: '8.4'+ env: GHCVER=8.4.4 CABALVER=2.2 STACKVER=lts-12.26+ addons: {apt: {packages: [ghc-8.4.4, cabal-install-2.2], sources: hvr-ghc}}+ - ghc: '8.2'+ env: GHCVER=8.2.2 CABALVER=2.0 STACKVER=lts-11.22+ addons: {apt: {packages: [ghc-8.2.2, cabal-install-2.0], sources: hvr-ghc}}+ - ghc: '8.0'+ env: GHCVER=8.0.2 CABALVER=1.24 STACKVER=lts-9.21+ addons: {apt: {packages: [ghc-8.0.2, cabal-install-1.24], sources: hvr-ghc}}+ - ghc: '7.10'+ env: GHCVER=7.10.3 CABALVER=1.22 STACKVER=lts-6.35+ addons: {apt: {packages: [ghc-7.10.3, cabal-install-1.22], sources: hvr-ghc}}+ # we only support stack with GHC >= 7.10+ - ghc: '7.8'+ env: GHCVER=7.8.4 CABALVER=1.18+ addons: {apt: {packages: [ghc-7.8.4, cabal-install-1.18], sources: hvr-ghc}}+ before_install:+ - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH+ - ghc --version+ - cabal --version+ - haddock --version+ - rm -f ~/.cabal/config && cabal update+ - cabal install Cabal==1.18.*+ - cabal install leancheck express speculate+ script:+ - make && make test+ - make haddock HADDOCKFLAGS=+ - make test-sdist+ - cabal test
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2021, Rudy Matela++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Rudy Matela nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Makefile view
@@ -0,0 +1,68 @@+GHCIMPORTDIRS = src:test+GHCFLAGS = -O2 \+ $(shell grep -q "Arch Linux" /etc/lsb-release && echo -dynamic)+HADDOCKFLAGS = --no-print-missing-docs \+ $(shell grep -q "Arch Linux" /etc/lsb-release && echo --optghc=-dynamic)++EG = \+ eg/arith \+ eg/factorial \+ eg/ints \+ eg/bools \+ proto/u-conjure++TESTS = \+ test/expr++all: mk/toplibs++all-all: all $(EG) $(TESTS)++test: $(patsubst %,%.run,$(TESTS)) diff-test test-sdist++.PHONY: bench+bench: $(patsubst %,%.bench,$(EG))+ @mkdir -p bench/runtime/$$HOSTNAME+ ./bench/versions | tee bench/runtime/$$HOSTNAME/versions++ghci: src/Conjure.ghci++%.bench: %+ @mkdir -p bench/runtime/$$HOSTNAME/`dirname $<`+ @printf "%-18s " $<+ @/usr/bin/time -f%e ./$< 2>&1 >/dev/null | tee bench/runtime/$$HOSTNAME/$<.runtime++diff-test: $(patsubst %,%.diff-test,$(EG))++update-diff-test: $(patsubst %,%.update-diff-test,$(EG))++test-sdist:+ ./test/sdist++clean: clean-hi-o clean-haddock+ rm -f $(EG) $(TESTS)++full-clean: clean clean-cabal clean-stack+ rm -f tags TAGS mk/toplibs++%.run: %+ ./$<++%.diff-test: %+ ./$< | diff -rud test/model/$<.out -++%.update-diff-test: %+ ./$< > test/model/$<.out++# lists files missing copyright notices+list-missing-copyright:+ grep -LRE '(Copyright|\(C\))' `git ls-tree -r master --name-only | grep -vE '(\.(runtime|out)|versions|toplibs|(Toplibs|All)\.hs|depend.mk)$$'` || true++# NOTE: (very hacky!) the following target allows parallel compilation (-jN) of+# eg and test programs so long as they don't share dependencies _not_ stored+# in src/ and test/. Runnable binaries should depend on mk/toplibs instead of+# actual Haskell source files+mk/toplibs: mk/Toplibs.o+ touch mk/toplibs++include mk/haskell.mk
+ README.md view
@@ -0,0 +1,177 @@+Conjure+=======++[![Conjure's Build Status][build-status]][build-log]+[![Conjure on Hackage][hackage-version]][code-conjure-on-hackage]+[![Conjure on Stackage LTS][stackage-lts-badge]][code-conjure-on-stackage-lts]+[![Conjure on Stackage Nightly][stackage-nightly-badge]][code-conjure-on-stackage-nightly]++![Conjure logo][conjure-logo]++Conjure is a tool that produces Haskell functions out of partial definitions.++This is currently an experimental tool in its early stages,+don't expect much from its current version.+It is just a piece of curiosity in its current state.+++Installing+----------++To install the [latest Conjure version from Hackage], just run:++ $ cabal update+ $ cabal install code-conjure++Starting from Cabal v3.0, you need to pass `--lib` as an argument to cabal+install:++ $ cabal install code-conjure --lib++Prerequisites are [express], [leancheck] and [speculate].+They should be automatically resolved and installed by [Cabal].++NOTE: the name of the Hackage package is __[`code-conjure`]__+-- not to be confused with [Conjure the BitTorrent client].+++Conjuring functions+-------------------++Given++ square :: Int -> Int+ square 0 = 0+ square 1 = 1+ square 2 = 4++and++ background :: [Expr]+ background =+ [ val (0::Int)+ , val (1::Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "==" ((==) :: Int -> Int -> Bool)+ ]++running++ > conjure "square" square background++yields++ square :: Int -> Int+ -- looking through 815 candidates, 100% match, 3/3 assignments+ square x = x * x++in less than a second.++See the `eg/arith.hs` example.+++Conjuring recursive functions+-----------------------------++Given++ factorial :: Int -> Int+ factorial 0 = 1+ factorial 1 = 1+ factorial 2 = 2+ factorial 3 = 6+ factorial 4 = 24+ factorial 5 = 120++and++ background :: [Expr]+ background =+ [ val (0::Int)+ , val (1::Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "dec" (subtract 1 :: Int -> Int)+ , value "isZero" ((==0) :: Int -> Bool)+ , val False+ , val True+ , ifFor (undefined :: Int)+ , value "==" ((==) :: Int -> Int -> Bool)+ ]++running++ > conjure "factorial" factorial background++yields++ factorial :: Int -> Int+ -- looking through 9266 candidates, 100% match, 6/6 assignments+ factorial x = if isZero x then 1 else x * factorial (dec x)++in about 3 seconds.++See the `eg/factorial.hs` example.++It is also possible to generate:++ factorial x = if x == 0 then 1 else x * factorial x - 1++in about 30s by changing the background and increasing the size limit.+++Related work+------------++[MagicHaskeller] (2007) is another tool+that is able to generate Haskell code automatically.+It supports recursion through+catamorphisms, paramorphisms and the [fix] function.+It is more mature than Conjure and is several orders of magnitude faster.++[Barliman] for Lisp is another tool that does program synthesis.++There are hundreds of others,+I'll add the most closely related here when I have the time.+++Further reading+---------------++For a detailed documentation of each function, see+[Conjure's Haddock documentation].+++Conjure, Copyright 2020 Rudy Matela,+distribued under the 3-clause BSD license.+++[Conjure's Haddock documentation]: https://hackage.haskell.org/package/code-conjure/docs/Conjure.html+[fix]: https://hackage.haskell.org/package/base/docs/Data-Function.html#v:fix++[symbol `>`]: https://www.haskell.org/haddock/doc/html/ch03s08.html#idm140354810780208+[Template Haskell]: https://wiki.haskell.org/Template_Haskell++[conjure-logo]: https://github.com/rudymatela/conjure/raw/master/doc/conjure.svg?sanitize=true++[`code-conjure`]: https://hackage.haskell.org/package/code-conjure+[Conjure the BitTorrent client]: https://hackage.haskell.org/package/conjure++[Cabal]: https://www.haskell.org/cabal+[Haskell]: https://www.haskell.org/+[leancheck]: https://hackage.haskell.org/package/leancheck+[express]: https://hackage.haskell.org/package/express+[speculate]: https://hackage.haskell.org/package/speculate+[MagicHaskeller]: https://hackage.haskell.org/package/MagicHaskeller+[Barliman]: https://github.com/webyrd/Barliman++[build-status]: https://travis-ci.org/rudymatela/conjure.svg?branch=master+[build-log]: https://travis-ci.org/rudymatela/conjure+[hackage-version]: https://img.shields.io/hackage/v/code-conjure.svg+[code-conjure-on-hackage]: https://hackage.haskell.org/package/code-conjure+[stackage-lts-badge]: https://stackage.org/package/code-conjure/badge/lts+[stackage-nightly-badge]: https://stackage.org/package/code-conjure/badge/nightly+[code-conjure-on-stackage]: https://stackage.org/package/code-conjure+[code-conjure-on-stackage-lts]: https://stackage.org/lts/package/code-conjure+[code-conjure-on-stackage-nightly]: https://stackage.org/nightly/package/code-conjure
+ Setup.hs view
@@ -0,0 +1,5 @@+-- Setup.hs for code-conjure / Conjure+-- Part of Conjure, Copyright 2020 Rudy Matela,+-- distribued under the 3-clause BSD license.+import Distribution.Simple+main = defaultMain
+ TODO.md view
@@ -0,0 +1,33 @@+TODO for Conjure+================++A non-exhaustive list of things TO DO for Conjure.++* reduce to unique `candidateExprs` through testing.+ 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"`++* Automatically include `if`s and `==`s.+ Minor problem: typeclass folding is not possible for result values.++* Automatically include background functions based on the argument types.+ The `Arguable` typeclass is a sketch of how to do that based on+ the `Generalizable` typeclass from the Extrapolate library.+ Though the implementation is quite crufty.++* use partially defined implementations?++ partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)+ partial impl = f+ where+ f n = if n == 0+ then 1+ else impl f n+++This file is part of Conjure,+(C) 2021 Rudy Matela,+Distribued under the 3-Clause BSD license.
+ code-conjure.cabal view
@@ -0,0 +1,81 @@+-- Cabal file for the Conjure program generation library.+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+name: code-conjure+version: 0.0.2+synopsis: conjure Haskell functions out of partial definitions+description:+ Conjure is a tool that produces Haskell functions out of partial definitions.+ .+ This is currently an experimental tool in its early stages,+ don't expect much from its current version.+ It is just a piece of curiosity in its current state.++homepage: https://github.com/rudymatela/conjure#readme+license: BSD3+license-file: LICENSE+author: Rudy Matela+maintainer: Rudy Matela <rudy@matela.com.br>+category: Haskell+build-type: Simple+cabal-version: 1.18++extra-doc-files: README.md+ , TODO.md+ , doc/conjure.svg+extra-source-files: .gitignore+ , .travis.yml+ , Makefile+ , proto/*.hs+ , eg/*.hs+ , mk/All.hs+ , mk/Toplibs.hs+ , mk/depend.mk+ , mk/ghcdeps+ , mk/haddock-i+ , mk/haskell.mk+ , mk/install-on+ , stack.yaml+ , eg/runtime/zero/eg/*.runtime+ , eg/runtime/zero/proto/*.runtime+ , eg/runtime/zero/versions+ , eg/versions+ , test/model/eg/*.out+ , test/model/proto/*.out+ , test/sdist+tested-with: GHC==8.10++source-repository head+ type: git+ location: https://github.com/rudymatela/extrapolate++source-repository this+ type: git+ location: https://github.com/rudymatela/extrapolate+ tag: v0.0.2++library+ exposed-modules: Conjure+ , Conjure.Arguable+ , Conjure.Conjurable+ , Conjure.Engine+ , Conjure.Expr+ , Conjure.TypeBinding+ , Conjure.Utils+ other-extensions: TemplateHaskell, CPP+ build-depends: base >= 4 && < 5+ , leancheck >= 0.9.4+ , template-haskell+ , speculate >= 0.4.6+ , express >= 0.1.6+ hs-source-dirs: src+ default-language: Haskell2010++test-suite expr+ type: exitcode-stdio-1.0+ main-is: expr.hs+ other-modules: Test+ hs-source-dirs: test+ build-depends: base >= 4 && < 5, leancheck, express, speculate, code-conjure+ default-language: Haskell2010
+ doc/conjure.svg view
@@ -0,0 +1,118 @@+<?xml version="1.0" encoding="UTF-8" standalone="no"?>+<svg+ xmlns:dc="http://purl.org/dc/elements/1.1/"+ xmlns:cc="http://creativecommons.org/ns#"+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"+ xmlns:svg="http://www.w3.org/2000/svg"+ xmlns="http://www.w3.org/2000/svg"+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"+ width="75mm"+ height="60mm"+ viewBox="0 0 75 60.000001"+ version="1.1"+ id="svg857"+ inkscape:version="1.0.2 (e86c870879, 2021-01-15)"+ sodipodi:docname="conjure.svg">+ <title+ id="title923">Conjure</title>+ <defs+ id="defs851" />+ <sodipodi:namedview+ id="base"+ pagecolor="#ffffff"+ bordercolor="#666666"+ borderopacity="1.0"+ inkscape:pageopacity="0"+ inkscape:pageshadow="2"+ inkscape:zoom="1.1616101"+ inkscape:cx="25.853601"+ inkscape:cy="77.774729"+ inkscape:document-units="mm"+ inkscape:current-layer="layer1"+ showgrid="false"+ fit-margin-top="0"+ fit-margin-left="0"+ fit-margin-right="0"+ fit-margin-bottom="0"+ inkscape:window-width="1342"+ inkscape:window-height="1063"+ inkscape:window-x="1366"+ inkscape:window-y="15"+ inkscape:window-maximized="0"+ units="mm"+ inkscape:document-rotation="0" />+ <metadata+ id="metadata854">+ <rdf:RDF>+ <cc:Work+ rdf:about="">+ <dc:format>image/svg+xml</dc:format>+ <dc:type+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />+ <dc:title>Conjure</dc:title>+ <cc:license+ rdf:resource="http://creativecommons.org/licenses/by-sa/4.0/" />+ <dc:date>2021-04-22</dc:date>+ <dc:creator>+ <cc:Agent>+ <dc:title>Rudy Matela</dc:title>+ </cc:Agent>+ </dc:creator>+ <dc:subject>+ <rdf:Bag>+ <rdf:li>Conjure</rdf:li>+ <rdf:li>logo</rdf:li>+ </rdf:Bag>+ </dc:subject>+ <dc:description>Conjure's logo. A check or tick (J) is seen in brown intersected with an opening angle bracket (C). Provisional++The proportions are based on the beautiful proportions of the Thompson-Wheeler Haskell logo (2009).</dc:description>+ <dc:source>https://github.com/rudymatela/conjure</dc:source>+ <dc:publisher>+ <cc:Agent>+ <dc:title />+ </cc:Agent>+ </dc:publisher>+ </cc:Work>+ <cc:License+ rdf:about="http://creativecommons.org/licenses/by-sa/4.0/">+ <cc:permits+ rdf:resource="http://creativecommons.org/ns#Reproduction" />+ <cc:permits+ rdf:resource="http://creativecommons.org/ns#Distribution" />+ <cc:requires+ rdf:resource="http://creativecommons.org/ns#Notice" />+ <cc:requires+ rdf:resource="http://creativecommons.org/ns#Attribution" />+ <cc:permits+ rdf:resource="http://creativecommons.org/ns#DerivativeWorks" />+ <cc:requires+ rdf:resource="http://creativecommons.org/ns#ShareAlike" />+ </cc:License>+ </rdf:RDF>+ </metadata>+ <g+ inkscape:label="Layer 1"+ inkscape:groupmode="layer"+ id="layer1"+ transform="translate(297.11803,-172.26764)">+ <path+ style="clip-rule:nonzero;fill:#b3997f;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.17638952"+ d="m -237.11837,172.26764 -32.49995,48.74992 -12.49979,-18.74983 h -14.99992 l 19.99989,29.99983 h 14.99992 l 39.99976,-59.99992 z"+ id="path9-3"+ inkscape:connector-curvature="0" />+ <path+ style="clip-rule:nonzero;fill:#80664c;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.176389"+ d="m -249.61892,191.01803 -27.49932,41.24961 h 14.99958 l 19.99979,-29.99967 z"+ id="path9-3-3"+ inkscape:connector-curvature="0"+ sodipodi:nodetypes="ccccc" />+ <path+ inkscape:connector-curvature="0"+ id="path9"+ d="m -242.11887,232.26764 -20.00013,-29.99985 20.00013,-29.99984 h -14.99992 l -19.99945,30.00002 19.99945,29.99967 z"+ style="clip-rule:nonzero;fill:#808080;fill-opacity:1;fill-rule:nonzero;stroke:none;stroke-width:0.176389"+ sodipodi:nodetypes="ccccccc" />+ </g>+</svg>
+ eg/arith.hs view
@@ -0,0 +1,43 @@+-- arith.hs: conjuring simple non-recursive numeric functions+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++double :: Int -> Int+double 0 = 0+double 1 = 2+double 2 = 4+double 3 = 6++add :: Int -> Int -> Int+add 0 0 = 0+add 0 1 = 1+add 1 0 = 1+add 1 1 = 2++square :: Int -> Int+square 0 = 0+square 1 = 1+square 2 = 4++tnpo :: Int -> Int+tnpo 0 = 1+tnpo 1 = 4+tnpo 2 = 7++main :: IO ()+main = do+ conjure "double" double background+ conjure "add" add background+ conjure "square" square background+ conjure "tnpo" tnpo background++background :: [Expr]+background =+ [ val (0::Int)+ , val (1::Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "==" ((==) :: Int -> Int -> Bool)+ ]
+ eg/bools.hs view
@@ -0,0 +1,32 @@+-- bools.hs: simple recursive functions over boolean lists+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++main :: IO ()+main = do+ conjure "and" (and :: [Bool] -> Bool) background+ conjure "or" (or :: [Bool] -> Bool) background++background :: [Expr]+background =+ [ val False+ , val True+ , value "not" not+ , value "||" (||)+ , value "&&" (&&)+ , value "null" (null :: [Bool] -> Bool)+ , value "head" (head :: [Bool] -> Bool)+ , value "tail" (tail :: [Bool] -> [Bool])+ , ifFor (undefined :: Bool)+ , value "==" ((==) :: [Bool] -> [Bool] -> Bool)+ ]++-- target (for and):++-- and ps = if null ps then True else head ps && and (tail ps)+-- 1 2 3 4 5 6 7 8 9 10 symbols+-- or+-- and ps = null ps || head ps && and (tail ps)+-- 1 2 3 4 5 6 7 8 9 symbols
+ eg/factorial.hs view
@@ -0,0 +1,47 @@+-- factorial.hs: conjuring a factorial function+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++factorial :: Int -> Int+factorial 0 = 1+factorial 1 = 1+factorial 2 = 2+factorial 3 = 6+factorial 4 = 24+factorial 5 = 120+++main :: IO ()+main = conjure "factorial" factorial background+++background :: [Expr]+background =+ [ val (0::Int)+ , val (1::Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "dec" (subtract 1 :: Int -> Int)+ , value "isZero" ((==0) :: Int -> Bool)+ , val False+ , val True+ , ifFor (undefined :: Int)+ , value "==" ((==) :: Int -> Int -> Bool)+ ]+++-- the actual factorial function:+-- factorial x = if x == 0 then 1 else x * factorial (x - 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)+-- 1 2 3 4 5 6 7 8 9 10 symbols+--+-- OR+--+-- factorial x = if (isZero x) then 1 else (x * factorial (dec x))+-- 1 2 3 4 5 6 7 8 9 symbols
+ eg/ints.hs view
@@ -0,0 +1,41 @@+-- ints.hs: conjuring functions over lists of ints+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++second :: [Int] -> Int+second [x,y] = y+second [x,y,z] = y+second [x,y,z,w] = y++third :: [Int] -> Int+third [x,y,z] = z+third [x,y,z,w] = 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++background :: [Expr]+background =+ [ val False+ , val True+ , val (0 :: Int)+ , val (1 :: Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "null" (null :: [Int] -> Bool)+ , value "head" (head :: [Int] -> Int)+ , value "tail" (tail :: [Int] -> [Int])+ , ifFor (undefined :: Int)+ , value "==" ((==) :: Int -> Int -> Bool)+ , value "==" ((==) :: [Int] -> [Int] -> Bool)+ ]++-- 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 2 3 4 5 6 7 8 9 10 symbols
+ eg/runtime/zero/eg/arith.runtime view
@@ -0,0 +1,1 @@+6.16
+ eg/runtime/zero/eg/bools.runtime view
@@ -0,0 +1,1 @@+3.33
+ eg/runtime/zero/eg/factorial.runtime view
@@ -0,0 +1,1 @@+2.70
+ eg/runtime/zero/eg/ints.runtime view
@@ -0,0 +1,1 @@+7.78
+ eg/runtime/zero/proto/u-conjure.runtime view
@@ -0,0 +1,1 @@+0.12
+ eg/runtime/zero/versions view
@@ -0,0 +1,4 @@+GHC 8.10.4+leancheck-0.9.4+express-0.1.6+speculate-0.4.5
+ eg/versions view
@@ -0,0 +1,19 @@+#!/bin/bash+#+# bench/versions: print versions of installed dependencies+#+# Copyright (C) 2021 Rudy Matela+# Distributed under the 3-Clause BSD licence (see the file LICENSE).+get-ghc-v() {+ ghc --version | sed -e "s/.* version/GHC/"+}+get-pkg-v() {+ ghc-pkg list $1 2>/dev/null |+ grep " $1-" |+ sed -e "s/^ *//" |+ tail -1+}+get-ghc-v+get-pkg-v leancheck+get-pkg-v express+get-pkg-v speculate
+ mk/All.hs view
@@ -0,0 +1,6 @@+module All+ ( module Conjure+ )+where++import Conjure
+ mk/Toplibs.hs view
@@ -0,0 +1,4 @@+-- Using ghc --make in this module triggers compilation of every library.+module Toplibs () where++import Conjure ()
+ mk/depend.mk view
@@ -0,0 +1,108 @@+eg/arith: \+ eg/arith.hs \+ mk/toplibs+eg/arith.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ eg/arith.hs+eg/bools: \+ eg/bools.hs \+ mk/toplibs+eg/bools.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ eg/bools.hs+eg/factorial: \+ eg/factorial.hs \+ mk/toplibs+eg/factorial.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ eg/factorial.hs+eg/ints: \+ eg/ints.hs \+ mk/toplibs+eg/ints.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ eg/ints.hs+mk/All.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ mk/All.hs+mk/Toplibs.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ mk/Toplibs.hs+proto/u-conjure.o: \+ proto/u-conjure.hs+proto/u-conjure: \+ proto/u-conjure.hs \+ mk/toplibs+src/Conjure/Arguable.o: \+ src/Conjure/Utils.hs \+ src/Conjure/TypeBinding.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Arguable.hs+src/Conjure/Conjurable.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Conjurable.hs+src/Conjure/Engine.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs+src/Conjure/Expr.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Expr.hs+src/Conjure.o: \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs+src/Conjure/TypeBinding.o: \+ src/Conjure/TypeBinding.hs+src/Conjure/Utils.o: \+ src/Conjure/Utils.hs+test/expr.o: \+ test/Test.hs \+ test/expr.hs \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs+test/expr: \+ test/Test.hs \+ test/expr.hs \+ mk/toplibs+test/Test.o: \+ test/Test.hs \+ src/Conjure/Utils.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs+test/Test: \+ test/Test.hs \+ mk/toplibs
+ mk/ghcdeps view
@@ -0,0 +1,50 @@+#!/bin/bash+#+# ghcdeps: generate Haskell make dependencies for compiling with GHC.+#+# Copyright (c) 2015-2021 Rudy Matela.+# Distributed under the 3-Clause BSD licence.+#+# From a list of files provided on standard input,+# generate flat make dependencies.+#+# Transitive relations are repeated.+#+# Usage:+# $ ghcdeps -isomedir:someother <<LIST+# program.hs+# Library.hs+# Path/To/Library.hs+# LIST+# program: ...+# Library.o: ...+# Path/To/Library.o: ...+#+# Or:+# $ find -name \*.hs -o -name \*.lhs | ghcdeps [GHCFLAGS]+# ...+#+# Note that when using find, you have to remember to exclude unecessary files,+# e.g.: dist, Setup.hs+#+# Yes, this is hacky. But hey, it works.+while read fn+do+ ghc "$@" -dep-suffix=. -dep-makefile=tmp.mk -M "$fn" ||+ exit 1+ deps="`cat tmp.mk |+ grep "hs$" |+ sort |+ sed -e "s/.*: //" |+ tac |+ tr '\n' ' ' |+ sed -e "s/ $//"`"+ obj=`echo $fn | sed -e 's,^\./,,;s/\.hs$/.o/'`+ bin=`echo $fn | sed -e 's,^\./,,;s/\.hs$//'`+ echo "$obj: $deps"+ grep -q "main" "$fn" && echo "$bin: `echo $deps | sed -e 's|[^ ]*src[^ ]*||g'` mk/toplibs"+ rm -f tmp.mk+done |+sort |+grep -v "^Loaded package environment from " |+sed -e 's, *, \\\n ,g'
+ mk/haddock-i view
@@ -0,0 +1,36 @@+#!/bin/bash+#+# haddock-i: list haddock's -i parameters.+#+# Copyright (c) 2015-2021 Rudy Matela.+# Distributed under the 3-Clause BSD licence.+#+# $ haddock-i <package1> <package2> ... <packageN>+#+# will print -i parameters necessary for haddock to link to Haddock+# documentation installed on your system, so you can:+#+# $ haddock-i base template-haskell | xargs haddock <files>+err() {+ echo "$@" > /dev/stderr+}++errxit() {+ err "$@"+ exit 1+}++iface-for() {+ ghc-pkg field $1 haddock-interfaces | sort -rV | head -1 | sed "s/.*: //"+}++html-for() {+ ghc-pkg field $1 haddock-html | sort -rV | head -1 | sed "s/.*: //"+}++for pkg in "$@"+do+ iface=$(iface-for $pkg)+ html=$(html-for $pkg)+ [ -d "$html" -a -f "$iface" ] && echo "-i$html,$iface" || err "haddock-i: warning: could not find interface file for $pkg"+done
+ mk/haskell.mk view
@@ -0,0 +1,140 @@+# Implicit rules for compiling Haskell code.+#+# Copyright (c) 2015-2021 Rudy Matela.+# Distributed under the 3-Clause BSD licence.+#+# You can optionally configure the "Configuration variables" below in your main+# makefile, e.g.:+#+# GHCIMPORTDIRS = path/to/dir:path/to/another/dir+# GHCFLAGS = -O2 -dynamic+# GHC = ghc-7.6+# include haskell.mk++++# Configuration variables++# GHC Parameters+GHCIMPORTDIRS ?=+GHCFLAGS ?=+GHC ?= ghc+GHCCMD = $(GHC) -i$(GHCIMPORTDIRS) $(GHCFLAGS)+HADDOCK ?= haddock++# Hugs Parameters+HUGSIMPORTDIRS ?= "/usr/lib/hugs/packages/*"+HUGSFLAGS ?=+CPPHS_HUGS ?= cpphs-hugs --noline -D__HUGS__+HUGS ?= hugs+RUNHUGS ?= runhugs+HUGSCMD = $(HUGS) -F"$(CPPHS_HUGS)" -P$(HUGSIMPORTDIRS) $(HUGSFLAGS)+RUNHUGSCMD = $(RUNHUGS) -F"$(CPPHS_HUGS)" -P$(HUGSIMPORTDIRS) $(HUGSFLAGS)+++# Makefile where to keep the dependencies+DEPMK ?= mk/depend.mk++# LIB_HSS: all library Haskell files+# ALL_HSS: all Haskell files+# You can override ALL/LIB_HSS in your main Makefile+LIST_LIB_HSS ?= find src -name "*.hs"+LIST_ALL_HSS ?= find \( -path "./dist*" -o -path "./.stack-work" -o -path "./Setup.hs" \) -prune \+ -o -name "*.*hs" -print+LIB_HSS ?= $(shell $(LIST_LIB_HSS))+ALL_HSS ?= $(shell $(LIST_ALL_HSS))++LIB_DEPS ?= base+ALL_DEPS ?= $(LIB_DEPS)++PKGNAME = $(shell cat *.cabal | grep "^name:" | sed -e "s/name: *//")+HADDOCK_VERSION = $(shell $(HADDOCK) --version | grep version | sed -e 's/.*version //;s/,.*//')+HADDOCK_MAJOR = $(shell echo $(HADDOCK_VERSION) | sed -e 's/\..*//')+HADDOCK_MINOR = $(shell echo $(HADDOCK_VERSION) | sed -e 's/[0-9]*\.\([0-9]*\).[0-9]*/\1/')+HADDOCK_PKG_NAME = $(shell [ $(HADDOCK_MAJOR) -gt 2 ] \+ || [ $(HADDOCK_MAJOR) -eq 2 -a $(HADDOCK_MINOR) -ge 20 ] \+ && echo "--package-name=$(PKGNAME)")+HADDOCK_HLNK_SRC = $(shell [ $(HADDOCK_MAJOR) -gt 2 ] \+ || [ $(HADDOCK_MAJOR) -eq 2 -a $(HADDOCK_MINOR) -ge 17 ] \+ && echo "--hyperlinked-source")+++# Implicit rules+%.hi %.o: %.hs+ $(GHCCMD) $< && touch $@++%: %.hs+ $(GHCCMD) $< && touch $@++.PHONY: %.ghci+%.ghci: %.hs+ $(GHCCMD) -O0 --interactive $<++.PHONY: %.hugs+%.hugs: %.hs+ $(HUGSCMD) $<++.PHONY: %.runhugs+%.runhugs: %.hs+ $(RUNHUGSCMD) $<+++# Cleaning rule (add as a clean dependency)+clean-hs: clean-hi-o clean-haddock clean-cabal clean-stack++clean-hi-o:+ find $(ALL_HSS) | sed -e 's/hs$$/o/' | xargs rm -f+ find $(ALL_HSS) | sed -e 's/hs$$/hi/' | xargs rm -f+ find $(ALL_HSS) | sed -e 's/hs$$/dyn_o/' | xargs rm -f+ find $(ALL_HSS) | sed -e 's/hs$$/dyn_hi/' | xargs rm -f+++# Update dependency file+.PHONY: depend+depend:+ find $(ALL_HSS) | ./mk/ghcdeps -i$(GHCIMPORTDIRS) $(GHCFLAGS) > $(DEPMK)++# haddock rules+haddock: doc/index.html++clean-haddock:+ rm -f doc/*.{html,css,js,png,gif,json} doc/src/* README.html++upload-haddock:+ @echo "use \`cabal upload -d' instead"+ @echo "(but 1st: cabal install --only-dependencies --enable-documentation)"+ @echo "(to just compile docs: cabal haddock --for-hackage)"+ @echo "(on Arch Linux, use: cabal haddock --for-hackage --haddock-options=--optghc=-dynamic)"++doc/index.html: $(LIB_HSS)+ ./mk/haddock-i $(LIB_DEPS) | xargs \+ $(HADDOCK) --html -odoc $(LIB_HSS) \+ --title=$(PKGNAME) \+ $(HADDOCK_PKG_NAME) \+ $(HADDOCK_HLNK_SRC) \+ $(HADDOCKFLAGS)++clean-cabal:+ rm -rf dist/ dist-newstyle/ cabal.project.local cabal.project.local~++clean-stack:+ rm -rf .stack-work/ stack.yaml.lock++# lists all Haskell source files+list-all-hss:+ @find $(ALL_HSS)++# lists library Haskell source files+list-lib-hss:+ @find $(LIB_HSS)++bootstrap-haskell-mk:+ @[ -d "$(DEST)" ] || (echo -e "error: no destination found\nusage: \`make bootstrap-haskell-mk DEST=path/to/prj'"; exit 1)+ mkdir -p mk+ cp mk/{haskell.mk,ghcdeps,haddock-i} $(DEST)/mk+ touch $(DEST)/mk/depend.mk++show-pkgname:+ @echo $(PKGNAME)++include $(DEPMK)
+ mk/install-on view
@@ -0,0 +1,33 @@+#!/bin/bash+#+# mk/install-on: install or updates the mk folder on a Haskell project+#+# Copyright (c) 2019-2021 Rudy Matela.+# Distributed under the 3-Clause BSD licence.+#+# usage: ./mk/install-on path/to/project+#+# This script assumes that:+#+# * tests are stored in a "test/" folder+# * sources are stored in a "src/" folder+set -e++errxit() {+ echo "$@" > /dev/stderr+ exit 1+}++src=`dirname $0`/..+dst="$1"++[ -n "$dst" ] || errxit "destination folder not provided"++mkdir -p $dst/mk+mkdir -p $dst/test++cp $src/mk/ghcdeps $dst/mk/ghcdeps+cp $src/mk/haddock-i $dst/mk/haddock-i+cp $src/mk/haskell.mk $dst/mk/haskell.mk+cp $src/mk/install-on $dst/mk/install-on+cp $src/test/sdist $dst/test/sdist
+ proto/u-conjure.hs view
@@ -0,0 +1,167 @@+-- 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 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++fact :: Int -> Int+fact 0 = 1+fact 1 = 1+fact 2 = 2+fact 3 = 6+fact 4 = 24++second :: [Int] -> Int+second [x,y] = y+second [x,y,z] = y+second [x,y,z,w] = y++main :: IO ()+main = do+ value "square" (square :: Int -> Int) `conjureFrom` intBackground+ value "add" (add :: Int -> Int -> Int) `conjureFrom` intBackground+ value "fact" (fact :: Int -> Int) `conjureFrom` intBackground++ value "==>" (==>) `conjureFrom`+ [ val False+ , val True+ , value "not" not+ , value "&&" (&&)+ , value "||" (||)+ ]++ value "second" (second :: [Int] -> Int) `conjureFrom` listBackground+ value "reverse" (reverse :: [Int] -> [Int]) `conjureFrom` listBackground+ where+ intBackground :: [Expr]+ intBackground =+ [ val (0 :: Int)+ , val (1 :: Int)+ , val (2 :: Int)+ , val (3 :: Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "-" ((-) :: Int -> Int -> Int)+ ]+ listBackground :: [Expr]+ listBackground =+ [ val (0 :: Int)+ , val (1 :: Int)+ , val ([] :: [Int])+ , value "head" (head :: [Int] -> Int)+ , value "tail" (tail :: [Int] -> [Int])+ , value ":" ((:) :: Int -> [Int] -> [Int])+ , value "++" ((++) :: [Int] -> [Int] -> [Int])+ ]+++conjureFrom :: Expr -> [Expr] -> IO ()+ff `conjureFrom` es = do+ print ff -- prints the type signature+ case rs of+ [] -> putStrLn $ "cannot conjure"+-- es -> putStrLn $ unlines $ map showEq es -- uncomment to show all found variations+ (e:_) -> putStrLn $ showEq e+ putStrLn ""+ where+ nm (Value s _) = s+ rrff = ('_':nm ff) `varAsTypeOf` ff+ rs = [ ffxx -==- e+ | e <- candidateExprsFrom $ [rrff] ++ xxs ++ filter isGround es+ , isWellTyped (ffxx -==- e)+ , isTrue (ffxx -==- e)+ , isDefined e+ ]+ ffxx = mostGeneralCanonicalVariation+ . fromJust+ $ application ff es+ (_:xxs) = unfoldApp ffxx+ showEq eq = showExpr (lhs eq) ++ " = " ++ showExpr (rhs eq)+++application :: Expr -> [Expr] -> Maybe Expr+application ff es = appn ff+ where+ appn ff+ | isFun ff = case [e | Just (_ :$ e) <- (map (ff $$)) es] of+ [] -> Nothing -- could not find type representative in es+ (e:_) -> appn (ff :$ holeAsTypeOf e)+ | otherwise = Just ff+++candidateExprsFrom :: [Expr] -> [Expr]+candidateExprsFrom = concat . take 6 . expressionsT+ where+ expressionsT ds = [ds] \/ (delay $ productMaybeWith ($$) es es)+ where+ es = expressionsT ds+++isTrue :: Expr -> Bool+isTrue = all (errorToTrue . eval False) . take 60 . grounds+++-- checks if a function is defined for at least one combination of argument values+isDefined :: Expr -> Bool+isDefined e = any (isJust . errorToNothing . eval False) . take 60 . grounds $ (e -==- e)+++(-==-) :: 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+++grounds :: Expr -> [Expr]+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]]])+ _ -> []
+ src/Conjure.hs view
@@ -0,0 +1,61 @@+-- |+-- Module : Conjure+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- A library for Conjuring function implementations+-- from tests or partial definitions.+-- (a.k.a.: functional inductive programming)+--+-- This is currently an experimental tool in its early stages,+-- don't expect much from its current version.+-- It is just a piece of curiosity in its current state.+--+-- Step 1: declare your partial function+--+-- > square :: Int -> Int+-- > square 0 = 0+-- > square 1 = 1+-- > square 2 = 4+--+-- Step 2: declare a list with the potential building blocks:+--+-- > background :: [Expr]+-- > background =+-- > [ val (0::Int)+-- > , val (1::Int)+-- > , value "+" ((+) :: Int -> Int -> Int)+-- > , value "*" ((*) :: Int -> Int -> Int)+-- > , value "==" ((==) :: Int -> Int -> Bool)+-- > ]+--+-- Including equality '==' over the given type is a good rule of thumb to+-- improve performance.+--+-- Step 3: call conjure and see your generated function:+--+-- > > conjure "square" square background+-- > square :: Int -> Int+-- > -- looking through 815 candidates, 100% match, 3/3 assignments+-- > square x = x * x+{-# LANGUAGE CPP #-}+module Conjure+ (+-- * Basic use+ conjure+ , val+ , value+ , ifFor+ , Expr++-- * Advanced use+ , conjpure+ , Args(..)+ , args+ , conjureWith+ , conjpureWith+ )+where++import Conjure.Engine
+ src/Conjure/Arguable.hs view
@@ -0,0 +1,331 @@+-- |+-- Module : Conjure.Arguable+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of 'Arguable'.+--+-- This defines the 'Arguable' typeclass+-- and utilities involving it.+--+-- You are probably better off importing "Conjure".+{-# LANGUAGE CPP #-}+module Conjure.Arguable+ ( Arguable (..)+ , instances++ , mkEq1+ , mkEq2+ , mkEq3+ , mkEq4+ , mkOrd1+ , mkOrd2+ , mkOrd3+ , mkOrd4++ , (*==*)+ , (*/=*)+ , (*<=*)+ , (*<*)++ , Listable (..)+ , module Conjure.Expr+ )+where++import Data.Maybe+import Data.Ratio++import Test.LeanCheck+import Test.LeanCheck.Utils++import Conjure.Expr hiding (application)+import Conjure.TypeBinding+import Test.Speculate.Expr+++-- |+-- Extrapolate can generalize counter-examples of any types that are+-- 'Arguable'.+--+-- 'Arguable' types must first be instances of+--+-- * 'Listable', so Extrapolate knows how to enumerate values;+-- * 'Express', so Extrapolate can represent then manipulate values;+-- * 'Name', 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 'background' and 'subInstances'.+--+-- The 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 'instances' it may be useful to use type binding+-- operators such as: 'argTy1of1', 'argTy1of2' and 'argTy2of2'.+--+-- Instances can be automatically derived using+-- 'Conjure.Arguable.Derive.deriveArguable'+-- which will also automatically derivate+-- 'Listable', 'Express' and 'Name' when needed.+class (Listable a, Express a, Name a, Show a) => Arguable a where+ -- | List of symbols allowed to appear in side-conditions.+ -- Defaults to @[]@. See 'value'.+ background :: a -> [Expr]+ background _ = []++ -- | Computes a list of reified subtype instances.+ -- Defaults to 'id'.+ -- See 'instances'.+ subInstances :: a -> Instances -> Instances+ subInstances _ = id+++instance Arguable ()++instance Arguable Bool where+ background p = reifyEq p+ ++ [ value "not" not + , value "&&" (&&)+ , value "||" (||)+ ]++instance Arguable Int where+ background x = reifyEqOrd x+ ++ [ value "+" ((+) -:> x)+ , value "*" ((*) -:> x)+ , value "-" ((-) -:> x)+ , value "if" (\b x y -> if b then x else y :: Int)+ ]++instance Arguable Integer where+ background x = reifyEqOrd x++instance Arguable Char where+ background c = reifyEqOrd c++instance Arguable a => Arguable (Maybe a) where+ background mx = mkEq1 (maybeEq ->:> mx)+ ++ mkOrd1 (maybeOrd ->:> mx)+ ++ [ value "Just" (Just ->: mx) ]+ subInstances mx = instances (fromJust mx)++-- TODO: move maybeEq and maybeOrd here, I'll have to change the tests++instance (Arguable a, Arguable b) => Arguable (Either a b) where+ background exy = mkEq2 (eitherEq ->>:> exy)+ ++ mkOrd2 (eitherOrd ->>:> exy)+ ++ [ value "Left" (Left ->: exy)+ , value "Right" (Right ->: exy) ]+ subInstances exy = instances (fromLeft exy)+ . instances (fromRight exy)++-- TODO: move eitherEq and eitherOrd here, I'll have to change the tests++instance (Arguable a, Arguable b) => Arguable (a,b) where+ background xy = mkEq2 (pairEq ->>:> xy)+ ++ mkOrd2 (pairOrd ->>:> xy)+ subInstances xy = instances (fst xy)+ . instances (snd xy)++instance (Arguable a, Arguable b, Arguable c)+ => Arguable (a,b,c) where+ background xyz = mkEq3 (tripleEq ->>>:> xyz)+ ++ mkOrd3 (tripleOrd ->>>:> xyz)+ subInstances xyz = instances x . instances y . instances z+ where (x,y,z) = xyz++instance (Arguable a, Arguable b, Arguable c, Arguable d)+ => Arguable (a,b,c,d) where+ background xyzw = mkEq4 (quadrupleEq ->>>>:> xyzw)+ ++ mkOrd4 (quadrupleOrd ->>>>:> xyzw)+ subInstances xyzw = instances x+ . instances y+ . instances z+ . instances w+ where (x,y,z,w) = xyzw++instance Arguable a => Arguable [a] where+ background xs = mkEq1 (listEq ->:> xs)+ ++ mkOrd1 (listOrd ->:> xs)+ ++ [ value "length" (length -:> xs) ]+ ++ [ value "elem" (elemBy (*==*) ->:> xs) | hasEq $ head xs ]+ subInstances xs = instances (head xs)++instance Arguable Ordering where+ background o = reifyEqOrd o++mkEq1 :: (Arguable a, Arguable b)+ => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]+mkEq1 m = takeWhile (\_ -> hasEq x) . mkEq $ m (*==*)+ where+ x = arg1 ==: m++mkEq2 :: (Arguable a, Arguable b, Arguable c)+ => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]+mkEq2 m = takeWhile (\_ -> hasEq x && hasEq y) . mkEq $ m (*==*) (*==*)+ where+ x = arg1 ==: m+ y = arg2 ==: m++mkEq3 :: (Arguable a, Arguable b, Arguable c, Arguable d)+ => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)+ -> [Expr]+mkEq3 m = takeWhile (\_ -> hasEq x && hasEq y && hasEq z) . mkEq+ $ m (*==*) (*==*) (*==*)+ where+ x = arg1 ==: m+ y = arg2 ==: m+ z = arg3 ==: m++mkEq4 :: (Arguable a, Arguable b, Arguable c, Arguable d, Arguable e)+ => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)+ -> [Expr]+mkEq4 m = takeWhile (\_ -> hasEq x && hasEq y && hasEq z && hasEq w) . mkEq+ $ m (*==*) (*==*) (*==*) (*==*)+ where+ x = arg1 ==: m+ y = arg2 ==: m+ z = arg3 ==: m+ w = arg4 ==: m++mkOrd1 :: (Arguable a, Arguable b)+ => ((b -> b -> Bool) -> a -> a -> Bool) -> [Expr]+mkOrd1 m = takeWhile (\_ -> hasOrd x) . mkOrdLessEqual+ $ m (*<=*)+ where+ x = arg1 ==: m++mkOrd2 :: (Arguable a, Arguable b, Arguable c)+ => ((b -> b -> Bool) -> (c -> c -> Bool) -> a -> a -> Bool) -> [Expr]+mkOrd2 m = takeWhile (\_ -> hasOrd x && hasOrd y) . mkOrdLessEqual+ $ m (*<=*) (*<=*)+ where+ x = arg1 ==: m+ y = arg2 ==: m++mkOrd3 :: (Arguable a, Arguable b, Arguable c, Arguable d)+ => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> a -> a -> Bool)+ -> [Expr]+mkOrd3 m = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z) . mkOrdLessEqual+ $ m (*<=*) (*<=*) (*<=*)+ where+ x = arg1 ==: m+ y = arg2 ==: m+ z = arg3 ==: m++mkOrd4 :: (Arguable a, Arguable b, Arguable c, Arguable d, Arguable e)+ => ((b->b->Bool) -> (c->c->Bool) -> (d->d->Bool) -> (e->e->Bool) -> a -> a -> Bool)+ -> [Expr]+mkOrd4 m = takeWhile (\_ -> hasOrd x && hasOrd y && hasOrd z && hasOrd w) . mkOrdLessEqual+ $ m (*<=*) (*<=*) (*<=*) (*<=*)+ where+ x = arg1 ==: m+ y = arg2 ==: m+ z = arg3 ==: m+ w = arg4 ==: m++-- | Usage: @ins "x" (undefined :: Type)@+ins :: Arguable a => a -> Instances+ins x = reifyListable x+ ++ reifyName x+ ++ reifyBackground x++-- | Used in the definition of 'subInstances'+-- in 'Arguable' typeclass instances.+instances :: Arguable a => a -> Instances -> Instances+instances x = this x (subInstances x)+ where+ this :: Arguable a+ => a -> (Instances -> Instances) -> Instances -> Instances+ this x f is =+ if isListableT is (typeOf x)+ then is+ else f (ins x ++ is)+ -- TODO: change type to a -> [Instances -> Instances] -> Instances -> Instances++reifyBackground :: Arguable a => a -> Instances+reifyBackground x = [value "background" (background x)]++fromBackgroundOf :: (Arguable a, Typeable b) => String -> a -> Maybe b+fromBackgroundOf nm = listToMaybe+ . mapMaybe evaluate+ . filter (`isConstantNamed` nm)+ . background++hasEq :: Arguable a => a -> Bool+hasEq x = isJust $ "==" `fromBackgroundOf` x -: mayb (x >- x >- bool)++hasOrd :: Arguable a => a -> Bool+hasOrd x = isJust $ "<=" `fromBackgroundOf` x -: mayb (x >- x >- bool)++(*==*) :: Arguable a => a -> a -> Bool+x *==* y = x == y+ where+ (==) = fromMaybe (error "(*==*): no (==) operator in background")+ $ "==" `fromBackgroundOf` x++(*/=*) :: Arguable a => a -> a -> Bool+x */=* y = x /= y+ where+ (/=) = fromMaybe (error "(*/=*): no (/=) operator in background")+ $ "/=" `fromBackgroundOf` x++(*<=*) :: Arguable a => a -> a -> Bool+x *<=* y = x <= y+ where+ (<=) = fromMaybe (error "(*<=*): no (<=) operator in background")+ $ "<=" `fromBackgroundOf` x++(*<*) :: Arguable a => a -> a -> Bool+x *<* y = x < y+ where+ (<) = fromMaybe (error "(*<*): no (<) operator in background")+ $ "<" `fromBackgroundOf` x++-- -- other Arguable instances -- --++instance (Integral a, Arguable a) => Arguable (Ratio a)++instance ( Arguable a, Arguable b, Arguable c, Arguable d+ , Arguable e )+ => Arguable (a,b,c,d,e) where+ subInstances xyzwv = instances x . instances y . instances z+ . instances w . instances v+ where (x,y,z,w,v) = xyzwv++instance ( Arguable a, Arguable b, Arguable c, Arguable d+ , Arguable e, Arguable f )+ => Arguable (a,b,c,d,e,f) where+ subInstances xyzwvu = instances x . instances y . instances z+ . instances w . instances v . instances u+ where (x,y,z,w,v,u) = xyzwvu++instance ( Arguable a, Arguable b, Arguable c, Arguable d+ , Arguable e, Arguable f, Arguable g )+ => Arguable (a,b,c,d,e,f,g) where+ subInstances xyzwvut = instances x . instances y . instances z . instances w+ . instances v . instances u . instances t+ where (x,y,z,w,v,u,t) = xyzwvut++#if __GLASGOW_HASKELL__ < 710+-- No 8-tuples for you:+-- On GHC 7.8, 8-tuples are not Typeable instances. We could add a standalone+-- deriving clause, but that may cause trouble if some other library does the+-- same. User should declare Generalizable 8-tuples manually when using GHC <=+-- 7.8.+#else+instance ( Arguable a, Arguable b, Arguable c, Arguable d+ , Arguable e, Arguable f, Arguable g, Arguable h )+ => Arguable (a,b,c,d,e,f,g,h) where+ subInstances xyzwvuts = instances x . instances y . instances z . instances w+ . instances v . instances u . instances t . instances s+ where (x,y,z,w,v,u,t,s) = xyzwvuts+#endif
+ src/Conjure/Conjurable.hs view
@@ -0,0 +1,100 @@+-- |+-- Module : Conjure.Conjurable+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of 'Conjure'.+--+-- This defines the 'Conjurable' typeclass+-- and utilities involving it.+--+-- You are probably better off importing "Conjure".+module Conjure.Conjurable+ ( Conjurable+ , canonicalApplication+ , canonicalVarApplication+ , unifiedArgumentTiers+ , tiersFor+ , mkExprTiers+ )+where++import Test.LeanCheck+import Test.LeanCheck.Utils+import Conjure.Expr hiding (application)+import Test.Speculate.Expr++class Typeable a => Conjurable a where+ argumentHoles :: a -> [Expr]+ argumentHoles _ = []+ argumentTiers :: a -> [ [[Expr]] ]+ argumentTiers _ = []++instance Conjurable ()+instance Conjurable Int+instance Conjurable Integer+instance Conjurable Bool+instance Typeable a => Conjurable [a]+instance (Typeable a, Typeable b) => Conjurable (a,b)+instance Typeable a => Conjurable (Maybe a)+instance (Typeable a, Typeable b) => Conjurable (Either a b)++instance Conjurable Float+instance Conjurable Double+instance Conjurable Ordering++instance (Typeable a, Typeable b, Typeable c) => Conjurable (a,b,c)+instance (Typeable a, Typeable b, Typeable c, Typeable d) => Conjurable (a,b,c,d)+instance (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => Conjurable (a,b,c,d,e)+instance (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) => Conjurable (a,b,c,d,e,f)++instance (Listable a, Name a, Show a, Typeable a, Conjurable b) => Conjurable (a -> b) where+ argumentHoles f = hole (arg1 f) : argumentHoles (f undefined)+ argumentTiers f = mkExprTiers (arg1 f) : argumentTiers (f undefined)++arg1 :: (a -> b) -> a+arg1 _ = undefined++canonicalArgumentVariables :: Conjurable f => f -> [Expr]+canonicalArgumentVariables = unfoldApp+ . mostGeneralCanonicalVariation+ . foldApp+ . argumentHoles++canonicalApplication :: Conjurable f => String -> f -> Expr+canonicalApplication nm f = foldApp (value nm f : canonicalArgumentVariables f)++canonicalVarApplication :: Conjurable f => String -> f -> Expr+canonicalVarApplication nm f = foldApp (var nm f : canonicalArgumentVariables f)++unifiedArgumentTiers :: Conjurable f => f -> [[Expr]]+unifiedArgumentTiers = foldr (\/) [] . nubArgumentTiers++nubArgumentTiers :: Conjurable f => f -> [[ [Expr] ]]+nubArgumentTiers = nubOn tierepr . argumentTiers+ where+ nubOn f = nubBy ((==) `on` f)+ -- NOTE: this is O(n*n),+ -- not much of a problem the number of arguments will hardly pass 6.++mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]]+mkExprTiers a = mapT val (tiers -: [[a]])++tiersFor :: Conjurable f => f -> Expr -> [[Expr]]+tiersFor f e = tf (mkExprTiers (undefined :: Bool) : argumentTiers f)+ where+ tf [] = [[e]] -- no tiers found, keep variable+ tf (etiers:etc) = case etiers of+ ((e':_):_) | typ e' == typ e -> etiers+ _ -> tf etc++-- | tries to extract a representative from the first 6 tiers+tierepr :: [[Expr]] -> Maybe Expr+tierepr ((e:_):_) = Just e+tierepr ([]:(e:_):_) = Just e+tierepr ([]:[]:(e:_):_) = Just e+tierepr ([]:[]:[]:(e:_):_) = Just e+tierepr ([]:[]:[]:[]:(e:_):_) = Just e+tierepr ([]:[]:[]:[]:[]:(e:_):_) = Just e+tierepr _ = Nothing
+ src/Conjure/Engine.hs view
@@ -0,0 +1,188 @@+-- |+-- Module : Conjure.Engine+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- An internal module of 'Conjure',+-- a library for Conjuring function implementations+-- from tests or partial definitions.+-- (a.k.a.: functional inductive programming)+{-# LANGUAGE CPP, RecordWildCards, TupleSections #-}+module Conjure.Engine+ ( module Data.Express+ , module Data.Express.Fixtures+ , module Test.Speculate.Engine+ , module Test.Speculate.Reason+ , Args(..)+ , args+ , conjure+ , conjureWith+ , conjpure+ , conjpureWith+ , candidateExprs+ , ifFor+ )+where++import Data.Express+import Data.Express.Fixtures hiding ((-==-))+import qualified Data.Ratio+import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)+import Test.Speculate hiding ((===), Args(..), args)+import Test.Speculate.Reason+import Test.Speculate.Engine+import Test.Speculate.Expr+import System.IO++import Conjure.Expr+import Conjure.Conjurable++-- | Arguments to be passed to 'conjureWith' or 'conjpureWith'.+-- See 'args' for the defaults.+data Args = Args+ { maxTests :: Int -- ^ defaults to 60+ , maxSize :: Int -- ^ defaults to 9, keep greater than maxEquationSize+ , maxEquationSize :: Int -- ^ defaults to 5, keep smaller than maxSize+ , maxRecursionSize :: Int -- ^ defaults to 60+ }++-- | Default arguments to conjure.+--+-- * 60 tests+-- * functions of up to 9 symbols+-- * pruning with equations up to size 5+-- * recursion up to 60 symbols.+args :: Args+args = Args+ { maxTests = 60+ , maxSize = 9+ , maxEquationSize = 5+ , maxRecursionSize = 60+ }++-- | Like 'conjure' but in the pure world.+--+-- Returns a triple whose:+--+-- 1. first element is the number of candidates considered+--+-- 2. second element is the number of defined points in the given function+--+-- 3. third element is a list of implementations encoded as 'Expr's+-- paired with the number of matching points.+conjpure :: Conjurable f => String -> f -> [Expr] -> (Int,Int,[(Int,Expr)])+conjpure = conjpureWith args++-- | Like 'conjpure' but allows setting options through 'Args' and 'args'.+conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> (Int,Int,[(Int,Expr)])+conjpureWith Args{..} nm f es = (length candidates,totalDefined,) $ sortBy compareResult+ [ (ffxx .=. re, ffxx -==- e)+ | e <- candidates+ , apparentlyTerminates rrff e+ , let re = recursexpr maxRecursionSize vffxx e+ , ffxx ?=? re+ ]+ where+ totalDefined = ffxx .=. ffxx+ candidates = filter (\e -> typ e == typ ffxx)+ . concat+ . take maxSize+ $ candidateExprs nm f maxEquationSize (===) [es]+ ffxx = canonicalApplication nm f+ vffxx = canonicalVarApplication nm f+ rrff = var nm f++ (===), (?=?) :: Expr -> Expr -> Bool+ e1 === e2 = isReallyTrue (e1 -==- e2)+ e1 ?=? e2 = isTrueWhenDefined (e1 -==- e2)++ e1 .=. e2 = countTrue (e1 -==- e2)+ (-==-) = mkEquation eqs+ where+ eqs = value "==" ((==) :: Bool -> Bool -> Bool)+ : es++ isTrueWhenDefined = all (errorToTrue . eval False) . gs+ isReallyTrue = all (errorToFalse . eval False) . gs+ countTrue = count (errorToFalse . eval False) . gs++ gs :: Expr -> [Expr]+ gs = take maxTests . grounds (tiersFor f)++-- | Conjures an implementation of a partially defined function.+--+-- Takes a 'String' with the name of a function,+-- a partially-defined function from a conjurable type,+-- and a list of building blocks encoded as 'Expr'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 * x+--+-- The background is defined with 'val', 'value' and 'ifFor'.+conjure :: Conjurable f => String -> f -> [Expr] -> IO ()+conjure = conjureWith args++-- | Like 'conjure' but allows setting options through 'Args' and 'args'.+conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()+conjureWith args nm f es = do+ print (var nm f)+ putStr $ "-- looking through " ++ show ncs ++ " candidates"+ hFlush stdout+ case rs of+ [] -> putStrLn $ "\ncannot conjure"+ ((n,e):_) -> do putStrLn $ ", " ++ showMatch n+ putStrLn $ showEq e+-- nes -> putStrLn . unlines $ "":[showEq e ++ " -- " ++ show n | (n,e) <- nes]+ putStrLn ""+ where+ (ncs,t,rs) = conjpureWith args nm f es+ showMatch n = show (n % t) ++ "% match, " ++ show n ++ "/" ++ show t ++ " assignments"+ showEq eq = showExpr (lhs eq) ++ " = " ++ showExpr (rhs eq)++candidateExprs :: Conjurable f+ => String -> f+ -> Int+ -> (Expr -> Expr -> Bool)+ -> [[Expr]]+ -> [[Expr]]+candidateExprs nm f sz (===) ess = expressionsT $ [ef:exs] \/ ess+ where+ (ef:exs) = unfoldApp $ canonicalVarApplication nm f+ thy = theoryFromAtoms (===) sz $ [nub (b_:map holeAsTypeOf exs)] \/ ess+ expressionsT ds = filterT (\e -> count (== ef) (vars e) <= 1)+ $ filterT (isRootNormalE thy)+ $ ds \/ (delay $ productMaybeWith ($$) es es)+ where+ es = expressionsT ds++lhs, rhs :: Expr -> Expr+lhs (((Value "==" _) :$ e) :$ _) = e+rhs (((Value "==" _) :$ _) :$ e) = e++compareResult :: (Int,Expr) -> (Int,Expr) -> Ordering+compareResult (n1,e1) (n2,e2) = n2 `compare` n1+ <> e1 `compareSimplicity` e2++(%) :: Int -> Int -> Int+x % y = x * 100 `div` y
+ src/Conjure/Expr.hs view
@@ -0,0 +1,174 @@+-- |+-- Module : Conjure.Expr+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- This internal module reexports 'Data.Express' along with a few other+-- utilities.+{-# LANGUAGE CPP #-}+module Conjure.Expr+ ( module Data.Express+ , module Data.Express.Fixtures++ , funToVar+ , recursexpr+ , apparentlyTerminates+ , mayNotEvaluateArgument+ , applicationOld+ , compareSimplicity+ , ifFor++ , module Conjure.Utils+ )+where++import Conjure.Utils++import Data.Express+import Data.Express.Fixtures hiding ((-==-))++-- | /O(n)/.+-- Compares the simplicity of two 'Expr's.+-- An expression /e1/ is /strictly simpler/ than another expression /e2/+-- if the first of the following conditions to distingish between them is:+--+-- 1. /e1/ is smaller in size\/length than /e2/,+-- e.g.: @x + y < x + (y + z)@;+--+-- 2. or, /e1/ has less variable occurrences than /e2/,+--+-- 3. or, /e1/ has fewer distinct constants than /e2/,+-- e.g.: @1 + 1 < 0 + 1@.+--+-- They're otherwise considered of equal complexity,+-- e.g.: @x + y@ and @y + z@.+--+-- > > (xx -+- yy) `compareComplexity` (xx -+- (yy -+- zz))+-- > LT+--+-- > > (xx -+- yy) `compareComplexity` (xx -+- xx)+-- > EQ+--+-- > > (xx -+- xx) `compareComplexity` (one -+- xx)+-- > GT+--+-- > > (one -+- one) `compareComplexity` (zero -+- one)+-- > LT+--+-- > > (xx -+- yy) `compareComplexity` (yy -+- zz)+-- > EQ+--+-- > > (zero -+- one) `compareComplexity` (one -+- zero)+-- > EQ+compareSimplicity :: Expr -> Expr -> Ordering+compareSimplicity = (compare `on` length . values)+ <> (compare `on` length . vars)+ <> (compare `on` length . nubConsts)++-- | Makes the function in an application a variable+funToVar :: Expr -> Expr+funToVar (ef :$ ex) = funToVar ef :$ ex+funToVar ef@(Value nm _) = nm `varAsTypeOf` ef++-- | Expands 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+recursexpr :: Int -> Expr -> Expr -> Expr+recursexpr sz epat = re+ where+ err = error "recursexpr: pattern must contain an application of variables"+ (erf:vs) = unfoldApp epat+ re e' | not (all isVar (erf:vs)) = err+ | e == e' || size e > sz = e+ | otherwise = re e+ where+ e = re1 e'+ re1 e = case unfoldApp e of+ [e] -> e+ (ef:exs) | ef == erf -> e' //- zip vs exs+ | otherwise -> foldApp (map re1 (ef:exs))++-- recursive call _only_ under an if+-- future-work: guess short-circuit operators++-- | Checks if the given recursive call apparently terminates.+-- The first argument indicates the functional variable indicating the+-- recursive call.+--+-- > > apparentlyTerminates ffE (ff xx)+-- > False+--+-- > > apparentlyTerminates ffE (if' pp zero (ff xx))+-- > True+--+-- This function only allows recursion in the else clause:+--+-- > > apparentlyTerminates ffE (if' pp (ff xx) zero)+-- > False+--+-- Of course, recursive calls as the condition are not allowed:+--+-- > > apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero)+-- > False+apparentlyTerminates :: Expr -> Expr -> Bool+apparentlyTerminates eRecursiveCall = at+ where+ at (e1 :$ e2) = (mayNotEvaluateArgument e1 || at e2) && at e1+ at e = e /= eRecursiveCall++-- | Checks if the given functional expression may refrain from evaluating its+-- next argument.+--+--+-- > > mayNotEvaluateArgument (plus :$ xx)+-- > False+--+-- > > mayNotEvaluateArgument (andE :$ pp)+-- > True+--+-- This returns false for non-funcional value even if it involves an+-- application which may not evaluate its argument.+--+-- > > mayNotEvaluateArgument (andE :$ pp :$ qq)+-- > False+--+-- This currently works by checking if the function is an if, '&&' or '||'.+mayNotEvaluateArgument :: Expr -> Bool+mayNotEvaluateArgument (Value "if" ce :$ _ :$ _) = True+mayNotEvaluateArgument (Value "&&" ce :$ _) = True+mayNotEvaluateArgument (Value "||" ce :$ _) = True+mayNotEvaluateArgument _ = False++applicationOld :: Expr -> [Expr] -> Maybe Expr+applicationOld ff es = appn ff+ where+ appn ff+ | isFun ff = case [e | Just (_ :$ e) <- (map (ff $$)) es] of+ [] -> Nothing -- could not find type representative in es+ (e:_) -> appn (ff :$ holeAsTypeOf e)+ | otherwise = Just ff++-- | Creates an if 'Expr' 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.+ifFor :: Typeable a => a -> Expr+ifFor a = value "if" (\p x y -> if p then x else y `asTypeOf` a)
+ src/Conjure/TypeBinding.hs view
@@ -0,0 +1,120 @@+-- |+-- Module : Conjure.TypeBinding+-- Copyright : (c) 2017-2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- Some type binding operators that are useful when defining 'Conjurable'+-- instances.+module Conjure.TypeBinding+ ( arg1+ , arg2+ , arg3+ , arg4+ , arg5+ , arg6+ , (==:)+ , argTy1of1+ , argTy1of2, argTy2of2+ , argTy1of3, argTy2of3, argTy3of3+ , argTy1of4, argTy2of4, argTy3of4, argTy4of4+ , argTy1of5, argTy2of5, argTy3of5, argTy4of5, argTy5of5+ , argTy1of6, argTy2of6, argTy3of6, argTy4of6, argTy5of6, argTy6of6+ , module Test.LeanCheck.Utils.TypeBinding+ )+where++import Test.LeanCheck.Utils.TypeBinding++-- TODO: reexport LeanCheck's typebinding operators+-- TODO: or maybe re-export Express's typebinding operators?++arg1 :: (a -> b) -> a+arg1 _ = undefined++arg2 :: (a -> b -> c) -> b+arg2 _ = undefined++arg3 :: (a -> b -> c -> d) -> c+arg3 _ = undefined++arg4 :: (a -> b -> c -> d -> e) -> d+arg4 _ = undefined++arg5 :: (a -> b -> c -> d -> e -> f) -> e+arg5 _ = undefined++arg6 :: (a -> b -> c -> d -> e -> f -> g) -> f+arg6 _ = undefined++(==:) :: (a -> (b -> c -> d)) -> a -> b+x ==: y = undefined+++argTy1of1 :: con a -> a+argTy1of1 _ = undefined+++argTy1of2 :: con a b -> a+argTy1of2 _ = undefined++argTy2of2 :: con a b -> b+argTy2of2 _ = undefined+++argTy1of3 :: con a b c -> a+argTy1of3 _ = undefined++argTy2of3 :: con a b c -> b+argTy2of3 _ = undefined++argTy3of3 :: con a b c -> c+argTy3of3 _ = undefined+++argTy1of4 :: con a b c d -> a+argTy1of4 _ = undefined++argTy2of4 :: con a b c d -> b+argTy2of4 _ = undefined++argTy3of4 :: con a b c d -> c+argTy3of4 _ = undefined++argTy4of4 :: con a b c d -> d+argTy4of4 _ = undefined+++argTy1of5 :: con a b c d e -> a+argTy1of5 _ = undefined++argTy2of5 :: con a b c d e -> b+argTy2of5 _ = undefined++argTy3of5 :: con a b c d e -> c+argTy3of5 _ = undefined++argTy4of5 :: con a b c d e -> d+argTy4of5 _ = undefined++argTy5of5 :: con a b c d e -> e+argTy5of5 _ = undefined+++argTy1of6 :: con a b c d e f -> a+argTy1of6 _ = undefined++argTy2of6 :: con a b c d e f -> b+argTy2of6 _ = undefined++argTy3of6 :: con a b c d e f -> c+argTy3of6 _ = undefined++argTy4of6 :: con a b c d e f -> d+argTy4of6 _ = undefined++argTy5of6 :: con a b c d e f -> e+argTy5of6 _ = undefined++argTy6of6 :: con a b c d e f -> f+argTy6of6 _ = undefined
+ src/Conjure/Utils.hs view
@@ -0,0 +1,139 @@+-- |+-- Module : Conjure.Utils+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- An internal module of 'Conjure'.+-- This exports 'Data.List', 'Data.Maybe', 'Data.Function'+-- and a few other simple utitilites.+{-# LANGUAGE CPP #-}+module Conjure.Utils+ ( module Data.List+ , module Data.Function+ , module Data.Maybe+ , module Data.Monoid+ , module Data.Tuple+ , module Data.Typeable++ , count++ , fromLeft+ , fromRight+ , elemBy+ , listEq+ , listOrd+ , maybeEq+ , maybeOrd+ , eitherEq+ , eitherOrd+ , pairEq+ , pairOrd+ , tripleEq+ , tripleOrd+ , quadrupleEq+ , quadrupleOrd+ )+where++import Data.List+import Data.Function+import Data.Maybe+import Data.Monoid+import Data.Tuple+import Data.Typeable++count :: (a -> Bool) -> [a] -> Int+count p = length . filter p++mapHead :: (a -> a) -> [a] -> [a]+mapHead f (x:xs) = f x : xs+mapHead _ [] = error "Conjure.Utils.mapHead: empty list"++-- note these versions of fromLeft and fromRight differ from the ones of+-- Data.Either since 4.10.0.0.+fromLeft :: Either a b -> a+fromLeft (Left x) = x+fromLeft _ = error "fromLeft: not a left"++fromRight :: Either a b -> b+fromRight (Right x) = x+fromRight _ = error "fromRight: not a right"++elemBy :: (a -> a -> Bool) -> a -> [a] -> Bool+elemBy (==) x = any (== x)++listEq :: (a -> a -> Bool) -> [a] -> [a] -> Bool+listEq (==) [] [] = True+listEq (==) (x:xs) [] = False+listEq (==) [] (y:ys) = False+listEq (==) (x:xs) (y:ys) = x == y && listEq (==) xs ys++listOrd :: (a -> a -> Bool) -> [a] -> [a] -> Bool+listOrd (<=) [] [] = True+listOrd (<=) (x:xs) [] = False+listOrd (<=) [] (y:ys) = True+listOrd (<=) (x:xs) (y:ys) = x < y+ || x == y && listOrd (<=) xs ys+ where+ x < y = x <= y && not (y <= x)+ x == y = x <= y && y <= x++maybeEq :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool+maybeEq (==) Nothing Nothing = True+maybeEq (==) Nothing (Just y) = False+maybeEq (==) (Just x) Nothing = False+maybeEq (==) (Just x) (Just y) = x == y++maybeOrd :: (a -> a -> Bool) -> Maybe a -> Maybe a -> Bool+maybeOrd (<=) Nothing Nothing = True+maybeOrd (<=) Nothing (Just y) = True+maybeOrd (<=) (Just x) Nothing = False+maybeOrd (<=) (Just x) (Just y) = x <= y++eitherEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool+eitherEq (==) _ (Left x) (Left y) = x == y+eitherEq _ (==) (Right x) (Right y) = x == y+eitherEq _ _ _ _ = False++eitherOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> Either a b -> Either a b -> Bool+eitherOrd (<=) _ (Left x) (Left y) = x <= y+eitherOrd _ (<=) (Right x) (Right y) = x <= y+eitherOrd _ _ (Left _) (Right _) = True+eitherOrd _ _ (Right _) (Left _) = False++pairEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a,b) -> (a,b) -> Bool+pairEq (==.) (.==) (x1,y1) (x2,y2) = x1 ==. x2 && y1 .== y2++pairOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (a,b) -> (a,b) -> Bool+pairOrd (<=.) (.<=) (x1,y1) (x2,y2) = x1 <. x2+ || x1 ==. x2 && y1 .<= y2+ where+ x <. y = x <=. y && not (y <=. x)+ x ==. y = x <=. y && y <=. x++tripleEq :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool)+ -> (a,b,c) -> (a,b,c) -> Bool+tripleEq (==..) (.==.) (..==) (x1,y1,z1) (x2,y2,z2) =+ x1 ==.. x2 && y1 .==. y2 && z1 ..== z2++tripleOrd :: (a -> a -> Bool) -> (b -> b -> Bool) -> (c -> c -> Bool)+ -> (a,b,c) -> (a,b,c) -> Bool+tripleOrd (<=..) (.<=.) (..<=) (x1,y1,z1) (x2,y2,z2) =+ x1 <.. x2 || x1 ==.. x2 && pairOrd (.<=.) (..<=) (y1,z1) (y2,z2)+ where+ x <.. y = x <=.. y && not (y <=.. x)+ x ==.. y = x <=.. y && y <=.. x++quadrupleEq :: (a->a->Bool) -> (b->b->Bool) -> (c->c->Bool) -> (d->d->Bool)+ -> (a,b,c,d) -> (a,b,c,d) -> Bool+quadrupleEq (==...) (.==..) (..==.) (...==) (x1,y1,z1,w1) (x2,y2,z2,w2) =+ x1 ==... x2 && y1 .==.. y2 && z1 ..==. z2 && w1 ...== w2++quadrupleOrd :: (a->a->Bool) -> (b->b->Bool) -> (c->c->Bool) -> (d->d->Bool)+ -> (a,b,c,d) -> (a,b,c,d) -> Bool+quadrupleOrd (<=...) (.<=..) (..<=.) (...<=) (x1,y1,z1,w1) (x2,y2,z2,w2) =+ x1 <... x2 || x1 ==... x2 && tripleOrd (.<=..) (..<=.) (...<=) (y1,z1,w1) (y2,z2,w2)+ where+ x <... y = x <=... y && not (y <=... x)+ x ==... y = x <=... y && y <=... x
+ stack.yaml view
@@ -0,0 +1,14 @@+# Stack file for the Conjure program generation library.+#+# Copyright (C) 2021 Rudy Matela+# Distributed under the 3-Clause BSD licence (see the file LICENSE).++resolver: lts-15.6 # or ghc-8.8.3++packages:+- .++extra-deps:+- leancheck-0.9.4+- speculate-0.4.6+- express-0.1.6
+ test/Test.hs view
@@ -0,0 +1,43 @@+-- |+-- Module : Test+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- Internal test module for Conjure,+-- intended to be imported from all test programs and only by them.+module Test+ ( module Conjure+ , module Conjure.Expr++ , mainTest+ )+where++import System.Exit (exitFailure)+import System.Environment (getArgs)++import Conjure+import Conjure.Expr hiding (delete, insert)++reportTests :: [Bool] -> IO ()+reportTests tests =+ case elemIndices False tests of+ [] -> putStrLn "Tests passed!"+ is -> do putStrLn ("Failed tests:" ++ show is)+ exitFailure++getMaxTestsFromArgs :: Int -> IO Int+getMaxTestsFromArgs n = do+ as <- getArgs+ return $ case as of+ (s:_) -> read s+ _ -> n++mainTest :: (Int -> [Bool]) -> Int -> IO ()+mainTest tests n' = do+ n <- getMaxTestsFromArgs n'+ reportTests (tests n)++printLines :: Show a => [a] -> IO ()+printLines = putStrLn . unlines . map show
+ test/expr.hs view
@@ -0,0 +1,37 @@+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).++import Test++main :: IO ()+main = mainTest tests 5040++tests :: Int -> [Bool]+tests n =+ [ True++ , recursexpr 6 (ff xx) (ff xx)+ == (ff xx)++ , recursexpr 6 (ff xx) (one -+- ff xx)+ == (one -+- (one -+- (one -+- (one -+- ff xx))))++ , recursexpr 6 (ff xx) (if' pp one (xx -*- ff xx))+ == (if' pp one (xx -*- (if' pp one (xx -*- ff xx))))++ , recursexpr 6 (ff xx) (if' pp one (xx -*- ff (gg xx)))+ == (if' pp one (xx -*- (if' pp one (gg xx -*- ff (gg (gg xx))))))++ , mayNotEvaluateArgument (plus :$ xx) == False+ , mayNotEvaluateArgument (andE :$ pp) == True+ , mayNotEvaluateArgument (orE :$ qq) == True++ , mayNotEvaluateArgument (if' pp xx yy) == False+ , mayNotEvaluateArgument (andE :$ pp :$ qq) == False+ , mayNotEvaluateArgument (orE :$ pp :$ qq) == False++ , apparentlyTerminates ffE (ff xx) == False+ , apparentlyTerminates ffE (if' pp zero (ff xx)) == True+ , apparentlyTerminates ffE (if' pp (ff xx) zero) == False+ , apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero) == False+ ]
+ test/model/eg/arith.out view
@@ -0,0 +1,16 @@+double :: Int -> Int+-- looking through 815 candidates, 100% match, 4/4 assignments+double x = x + x++add :: Int -> Int -> Int+-- looking through 28024 candidates, 100% match, 4/4 assignments+add x y = x + y++square :: Int -> Int+-- looking through 815 candidates, 100% match, 3/3 assignments+square x = x * x++tnpo :: Int -> Int+-- looking through 815 candidates, 100% match, 3/3 assignments+tnpo x = x + (x + (x + 1))+
+ test/model/eg/bools.out view
@@ -0,0 +1,8 @@+and :: [Bool] -> Bool+-- looking through 1110 candidates, 100% match, 60/60 assignments+and ps = null ps || head ps && and (tail ps)++or :: [Bool] -> Bool+-- looking through 1110 candidates, 90% match, 54/60 assignments+or ps = head ps || or (tail ps)+
+ test/model/eg/factorial.out view
@@ -0,0 +1,4 @@+factorial :: Int -> Int+-- looking through 9266 candidates, 100% match, 6/6 assignments+factorial x = if isZero x then 1 else x * factorial (dec x)+
+ test/model/eg/ints.out view
@@ -0,0 +1,16 @@+second :: [Int] -> Int+-- looking through 13460 candidates, 100% match, 47/47 assignments+second xs = head (tail xs)++third :: [Int] -> Int+-- looking through 13460 candidates, 100% match, 34/34 assignments+third xs = head (tail (tail xs))++sum :: [Int] -> Int+-- looking through 13460 candidates, 8% match, 5/60 assignments+sum xs = if null (tail xs) then head xs else sum xs++product :: [Int] -> Int+-- looking through 13460 candidates, 81% match, 49/60 assignments+product xs = if 0 == head xs then 0 else product (tail xs)+
+ test/model/proto/u-conjure.out view
@@ -0,0 +1,18 @@+square :: Int -> Int+square x = x * x++add :: Int -> Int -> Int+add x y = x + y++fact :: Int -> Int+cannot conjure++(==>) :: Bool -> Bool -> Bool+p ==> q = q || not p++second :: [Int] -> Int+second xs = head (tail xs)++reverse :: [Int] -> [Int]+cannot conjure+
+ test/sdist view
@@ -0,0 +1,40 @@+#!/bin/bash+#+# test/sdist: tests the package generated by "cabal sdist".+#+# Copyright (c) 2015-2021 Rudy Matela.+# Distributed under the 3-Clause BSD licence.++set -xe++export LC_ALL=C # consistent sort++pkgver=` cat *.cabal | grep "^version:" | sed -e "s/version: *//"`+pkgname=`cat *.cabal | grep "^name:" | sed -e "s/name: *//"`+pkgbase=$pkgname-$pkgver++cabal sdist++# Try to find the package generated by cabal.+pkg=`find dist* -name $pkgbase.tar.gz`+[ -f "$pkg" ]+# If the script fails here, either:+# * no package was generated+# * there are packages in both dist and dist-newstyle folders.++tmp=`mktemp -d /tmp/test-sdist-XXXXXXXXXX`++# Test if our file is compatible with case-insensitive filesystems.+tar -tf $pkg | sort --ignore-case > $tmp/ls-cabal-i+tar -tf $pkg | sort --ignore-case --unique > $tmp/ls-cabal-iu+diff -rud $tmp/ls-cabal-i $tmp/ls-cabal-iu++if [ -d .git ]+then+ # Test if files included by cabal are the same as files tracked in git.+ git ls-files | sort > $tmp/ls-git+ tar -tf $pkg | grep -v "/$" | sed -e "s,$pkgbase/,," | sort > $tmp/ls-cabal+ diff -rud $tmp/ls-git $tmp/ls-cabal+fi++rm -r $tmp