diff --git a/.gitignore b/.gitignore
new file mode 100644
--- /dev/null
+++ b/.gitignore
@@ -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
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
--- /dev/null
+++ b/.travis.yml
@@ -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
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Makefile b/Makefile
new file mode 100644
--- /dev/null
+++ b/Makefile
@@ -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
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -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
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -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
diff --git a/TODO.md b/TODO.md
new file mode 100644
--- /dev/null
+++ b/TODO.md
@@ -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.
diff --git a/code-conjure.cabal b/code-conjure.cabal
new file mode 100644
--- /dev/null
+++ b/code-conjure.cabal
@@ -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
diff --git a/doc/conjure.svg b/doc/conjure.svg
new file mode 100644
--- /dev/null
+++ b/doc/conjure.svg
@@ -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>
diff --git a/eg/arith.hs b/eg/arith.hs
new file mode 100644
--- /dev/null
+++ b/eg/arith.hs
@@ -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)
+  ]
diff --git a/eg/bools.hs b/eg/bools.hs
new file mode 100644
--- /dev/null
+++ b/eg/bools.hs
@@ -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
diff --git a/eg/factorial.hs b/eg/factorial.hs
new file mode 100644
--- /dev/null
+++ b/eg/factorial.hs
@@ -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
diff --git a/eg/ints.hs b/eg/ints.hs
new file mode 100644
--- /dev/null
+++ b/eg/ints.hs
@@ -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
diff --git a/eg/runtime/zero/eg/arith.runtime b/eg/runtime/zero/eg/arith.runtime
new file mode 100644
--- /dev/null
+++ b/eg/runtime/zero/eg/arith.runtime
@@ -0,0 +1,1 @@
+6.16
diff --git a/eg/runtime/zero/eg/bools.runtime b/eg/runtime/zero/eg/bools.runtime
new file mode 100644
--- /dev/null
+++ b/eg/runtime/zero/eg/bools.runtime
@@ -0,0 +1,1 @@
+3.33
diff --git a/eg/runtime/zero/eg/factorial.runtime b/eg/runtime/zero/eg/factorial.runtime
new file mode 100644
--- /dev/null
+++ b/eg/runtime/zero/eg/factorial.runtime
@@ -0,0 +1,1 @@
+2.70
diff --git a/eg/runtime/zero/eg/ints.runtime b/eg/runtime/zero/eg/ints.runtime
new file mode 100644
--- /dev/null
+++ b/eg/runtime/zero/eg/ints.runtime
@@ -0,0 +1,1 @@
+7.78
diff --git a/eg/runtime/zero/proto/u-conjure.runtime b/eg/runtime/zero/proto/u-conjure.runtime
new file mode 100644
--- /dev/null
+++ b/eg/runtime/zero/proto/u-conjure.runtime
@@ -0,0 +1,1 @@
+0.12
diff --git a/eg/runtime/zero/versions b/eg/runtime/zero/versions
new file mode 100644
--- /dev/null
+++ b/eg/runtime/zero/versions
@@ -0,0 +1,4 @@
+GHC 8.10.4
+leancheck-0.9.4
+express-0.1.6
+speculate-0.4.5
diff --git a/eg/versions b/eg/versions
new file mode 100644
--- /dev/null
+++ b/eg/versions
@@ -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
diff --git a/mk/All.hs b/mk/All.hs
new file mode 100644
--- /dev/null
+++ b/mk/All.hs
@@ -0,0 +1,6 @@
+module All
+  ( module Conjure
+  )
+where
+
+import Conjure
diff --git a/mk/Toplibs.hs b/mk/Toplibs.hs
new file mode 100644
--- /dev/null
+++ b/mk/Toplibs.hs
@@ -0,0 +1,4 @@
+-- Using ghc --make in this module triggers compilation of every library.
+module Toplibs () where
+
+import Conjure ()
diff --git a/mk/depend.mk b/mk/depend.mk
new file mode 100644
--- /dev/null
+++ b/mk/depend.mk
@@ -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
diff --git a/mk/ghcdeps b/mk/ghcdeps
new file mode 100644
--- /dev/null
+++ b/mk/ghcdeps
@@ -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'
diff --git a/mk/haddock-i b/mk/haddock-i
new file mode 100644
--- /dev/null
+++ b/mk/haddock-i
@@ -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
diff --git a/mk/haskell.mk b/mk/haskell.mk
new file mode 100644
--- /dev/null
+++ b/mk/haskell.mk
@@ -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)
diff --git a/mk/install-on b/mk/install-on
new file mode 100644
--- /dev/null
+++ b/mk/install-on
@@ -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
diff --git a/proto/u-conjure.hs b/proto/u-conjure.hs
new file mode 100644
--- /dev/null
+++ b/proto/u-conjure.hs
@@ -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]]])
+  _        ->  []
diff --git a/src/Conjure.hs b/src/Conjure.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure.hs
@@ -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
diff --git a/src/Conjure/Arguable.hs b/src/Conjure/Arguable.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Arguable.hs
@@ -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
diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Conjurable.hs
@@ -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
diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Engine.hs
@@ -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
diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Expr.hs
@@ -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)
diff --git a/src/Conjure/TypeBinding.hs b/src/Conjure/TypeBinding.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/TypeBinding.hs
@@ -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
diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Conjure/Utils.hs
@@ -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
diff --git a/stack.yaml b/stack.yaml
new file mode 100644
--- /dev/null
+++ b/stack.yaml
@@ -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
diff --git a/test/Test.hs b/test/Test.hs
new file mode 100644
--- /dev/null
+++ b/test/Test.hs
@@ -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
diff --git a/test/expr.hs b/test/expr.hs
new file mode 100644
--- /dev/null
+++ b/test/expr.hs
@@ -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
+  ]
diff --git a/test/model/eg/arith.out b/test/model/eg/arith.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/arith.out
@@ -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))
+
diff --git a/test/model/eg/bools.out b/test/model/eg/bools.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/bools.out
@@ -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)
+
diff --git a/test/model/eg/factorial.out b/test/model/eg/factorial.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/factorial.out
@@ -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)
+
diff --git a/test/model/eg/ints.out b/test/model/eg/ints.out
new file mode 100644
--- /dev/null
+++ b/test/model/eg/ints.out
@@ -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)
+
diff --git a/test/model/proto/u-conjure.out b/test/model/proto/u-conjure.out
new file mode 100644
--- /dev/null
+++ b/test/model/proto/u-conjure.out
@@ -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
+
diff --git a/test/sdist b/test/sdist
new file mode 100644
--- /dev/null
+++ b/test/sdist
@@ -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