Copyright | (c) 2021 Rudy Matela |
---|---|
License | 3-Clause BSD (see the file LICENSE) |
Maintainer | Rudy Matela <rudy@matela.com.br> |
Safe Haskell | None |
Language | Haskell2010 |
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:
primitives :: [Prim] primitives = [ pr (0::Int) , pr (1::Int) , prim "+" ((+) :: Int -> Int -> Int) , prim "*" ((*) :: Int -> Int -> Int) ]
Step 3: call conjure and see your generated function:
> conjure "square" square primitives square :: Int -> Int -- testing 3 combinations of argument values -- pruning with 14/25 rules -- looking through 3 candidates of size 1 -- looking through 4 candidates of size 2 -- looking through 9 candidates of size 3 square x = x * x
Synopsis
- conjure :: Conjurable f => String -> f -> [Prim] -> IO ()
- type Prim = (Expr, Reification)
- pr :: (Conjurable a, Show a) => a -> Prim
- prim :: Conjurable a => String -> a -> Prim
- prif :: Conjurable a => a -> Prim
- conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()
- conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()
- data Args = Args {
- maxTests :: Int
- maxSize :: Int
- maxEvalRecursions :: Int
- maxEquationSize :: Int
- maxSearchTests :: Int
- requireDescent :: Bool
- usePatterns :: Bool
- showTheory :: Bool
- forceTests :: [[Expr]]
- args :: Args
- data Expr
- val :: (Typeable a, Show a) => a -> Expr
- value :: Typeable a => String -> a -> Expr
- type Spec1 a b = [(a, b)]
- type Spec2 a b c = [((a, b), c)]
- type Spec3 a b c d = [((a, b, c), d)]
- (-=) :: a -> b -> (a, b)
- conjure1 :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Prim] -> IO ()
- conjure2 :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c) => String -> Spec2 a b c -> [Prim] -> IO ()
- conjure3 :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c, Show c, Express c, Conjurable d, Eq d) => String -> Spec3 a b c d -> [Prim] -> IO ()
- conjure1With :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Prim] -> IO ()
- conjure2With :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c) => Args -> String -> Spec2 a b c -> [Prim] -> IO ()
- conjure3With :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c, Show c, Express c, Conjurable d, Eq d) => Args -> String -> Spec3 a b c d -> [Prim] -> IO ()
- class (Typeable a, Name a) => Conjurable a where
- conjureEquality :: a -> Maybe Expr
- conjureTiers :: a -> Maybe [[Expr]]
- conjureSubTypes :: a -> Reification
- conjureCases :: a -> [Expr]
- conjureExpress :: a -> Expr -> Expr
- reifyExpress :: (Express a, Show a) => a -> Expr -> Expr
- reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr
- reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]]
- conjureType :: Conjurable a => a -> Reification
- conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)
- data A
- data B
- data C
- data D
- data E
- data F
Basic use
conjure :: Conjurable f => String -> f -> [Prim] -> IO () Source #
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 primitives :: [Prim] primitives = [ pr (0::Int) , pr (1::Int) , prim "+" ((+) :: Int -> Int -> Int) , prim "*" ((*) :: Int -> Int -> Int) ]
The conjure function does the following:
> conjure "square" square primitives square :: Int -> Int -- testing 3 combinations of argument values -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 5 candidates of size 3 square x = x * x
type Prim = (Expr, Reification) Source #
A primtive expression (paired with instance reification).
prif :: Conjurable a => a -> Prim Source #
Provides an if condition bound to the given return type.
Advanced use
conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO () Source #
Like conjure
but allows setting the maximum size of considered expressions
instead of the default value of 12.
conjureWithMaxSize 10 "function" function [...]
conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO () Source #
Arguments to be passed to conjureWith
or conjpureWith
.
See args
for the defaults.
Args | |
|
Default arguments to conjure.
- 60 tests
- functions of up to 12 symbols
- maximum of one recursive call allowed in candidate bodies
- maximum evaluation of up to 60 recursions
- pruning with equations up to size 5
- search for defined applications for up to 100000 combinations
- require recursive calls to deconstruct arguments
- don't show the theory used in pruning
Values of type Expr
represent objects or applications between objects.
Each object is encapsulated together with its type and string representation.
Values encoded in Expr
s are always monomorphic.
An Expr
can be constructed using:
val
, for values that areShow
instances;value
, for values that are notShow
instances, like functions;:$
, for applications betweenExpr
s.
> val False False :: Bool
> value "not" not :$ val False not False :: Bool
An Expr
can be evaluated using evaluate
, eval
or evl
.
> evl $ val (1 :: Int) :: Int 1
> evaluate $ val (1 :: Int) :: Maybe Bool Nothing
> eval 'a' (val 'b') 'b'
Show
ing a value of type Expr
will return a pretty-printed representation
of the expression together with its type.
> show (value "not" not :$ val False) "not False :: Bool"
Expr
is like Dynamic
but has support for applications and variables
(:$
, var
).
The var
underscore convention:
Functions that manipulate Expr
s usually follow the convention
where a value
whose String
representation starts with '_'
represents a var
iable.
Instances
Eq Expr | O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types. This instance works for ill-typed expressions. |
Ord Expr | O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types. This instance works for ill-typed expressions. Expressions come first
when they have smaller complexity ( |
Show Expr | Shows > show (value "not" not :$ val False) "not False :: Bool" |
value :: Typeable a => String -> a -> Expr #
O(1).
It takes a string representation of a value and a value, returning an
Expr
with that terminal value.
For instances of Show
, it is preferable to use val
.
> value "0" (0 :: Integer) 0 :: Integer
> value "'a'" 'a' 'a' :: Char
> value "True" True True :: Bool
> value "id" (id :: Int -> Int) id :: Int -> Int
> value "(+)" ((+) :: Int -> Int -> Int) (+) :: Int -> Int -> Int
> value "sort" (sort :: [Bool] -> [Bool]) sort :: [Bool] -> [Bool]
Conjuring from a specification
type Spec1 a b = [(a, b)] Source #
A partial specification of a function with one argument:
sumSpec :: Spec1 [Int] Int sumSpec = [ [] -= 0 , [1,2] -= 3 , [3,4,5] -= 12 ]
To be passed as one of the arguments to conjure1
.
type Spec2 a b c = [((a, b), c)] Source #
A partial specification of a function with two arguments:
appSpec :: Spec2 [Int] [Int] [Int] appSpec = [ (,) [] [0,1] -= [0,1] , (,) [2,3] [] -= [2,3] , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9] ]
To be passed as one of the arguments to conjure2
.
type Spec3 a b c d = [((a, b, c), d)] Source #
A partial specification of a function with three arguments.
To be passed as one of the arguments to conjure3
conjure1 :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Prim] -> IO () Source #
Conjures a one argument function from a specification.
Given:
sumSpec :: Spec1 [Int] Int sumSpec = [ [] -= 0 , [1,2] -= 3 , [3,4,5] -= 12 ]
sumPrimitives :: [Prim] sumPrimitives = [ prim "null" (null :: [Int] -> Bool) , pr (0::Int) , prim "+" ((+) :: Int -> Int -> Int) , prim "head" (head :: [Int] -> Int) , prim "tail" (tail :: [Int] -> [Int]) ]
Then:
> conjure1 "sum" sumSpec sumPrimitives sum :: [Int] -> Int -- testing 3 combinations of argument values -- ... -- looking through 189/465 candidates of size 10 xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)
(cf. Spec1
, conjure1With
)
conjure2 :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c) => String -> Spec2 a b c -> [Prim] -> IO () Source #
Conjures a two argument function from a specification.
Given:
appSpec :: Spec2 [Int] [Int] [Int] appSpec = [ (,) [] [0,1] -= [0,1] , (,) [2,3] [] -= [2,3] , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9] ]
appPrimitives :: [Expr] appPrimitives = [ prim "null" (null :: [Int] -> Bool) , prim ":" ((:) :: Int -> [Int] -> [Int]) , prim "head" (head :: [Int] -> Int) , prim "tail" (tail :: [Int] -> [Int]) ]
Then:
> conjure2 "++" appSpec appPrimitives (++) :: [Int] -> [Int] -> [Int] -- testing 3 combinations of argument values -- ... -- looking through 26166/57090 candidates of size 11 xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)
(cf. Spec2
, conjure2With
)
conjure3 :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c, Show c, Express c, Conjurable d, Eq d) => String -> Spec3 a b c d -> [Prim] -> IO () Source #
Conjures a three argument function from a specification.
(cf. Spec3
, conjure3With
)
conjure1With :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Prim] -> IO () Source #
conjure2With :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c) => Args -> String -> Spec2 a b c -> [Prim] -> IO () Source #
conjure3With :: (Conjurable a, Eq a, Show a, Express a, Conjurable b, Eq b, Show b, Express b, Conjurable c, Eq c, Show c, Express c, Conjurable d, Eq d) => Args -> String -> Spec3 a b c d -> [Prim] -> IO () Source #
When using custom types
class (Typeable a, Name a) => Conjurable a where Source #
Class of Conjurable
types.
Functions are Conjurable
if all their arguments are Conjurable
, Listable
and Show
able.
For atomic types that are Listable
,
instances are defined as:
instance Conjurable Atomic where conjureTiers = reifyTiers
For atomic types that are both Listable
and Eq
,
instances are defined as:
instance Conjurable Atomic where conjureTiers = reifyTiers conjureEquality = reifyEquality
For types with subtypes, instances are defined as:
instance Conjurable Composite where conjureTiers = reifyTiers conjureEquality = reifyEquality conjureSubTypes x = conjureType y . conjureType z . conjureType w where (Composite ... y ... z ... w ...) = x
Above x
, y
, z
and w
are just proxies.
The Proxy
type was avoided for backwards compatibility.
Please see the source code of Conjure.Conjurable for more examples.
(cf. reifyTiers
, reifyEquality
, conjureType
)
conjureEquality :: a -> Maybe Expr Source #
conjureTiers :: a -> Maybe [[Expr]] Source #
conjureSubTypes :: a -> Reification Source #
conjureCases :: a -> [Expr] Source #
conjureExpress :: a -> Expr -> Expr Source #
Instances
reifyEquality :: (Eq a, Typeable a) => a -> Maybe Expr Source #
Reifies equality to be used in a conjurable type.
This is to be used
in the definition of conjureEquality
of Conjurable
typeclass instances:
instance ... => Conjurable <Type> where ... conjureEquality = reifyEquality ...
reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]] Source #
Reifies equality to be used in a conjurable type.
This is to be used
in the definition of conjureTiers
of Conjurable
typeclass instances:
instance ... => Conjurable <Type> where ... conjureTiers = reifyTiers ...
conjureType :: Conjurable a => a -> Reification Source #
Pure interfaces
conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
Like conjure
but in the pure world.
Returns a triple with:
- tiers of implementations
- tiers of candidate bodies (right type)
- tiers of candidate expressions (any type)
- a list of tests
conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) Source #
Helper test types
Generic type A
.
Can be used to test polymorphic functions with a type variable
such as take
or sort
:
take :: Int -> [a] -> [a] sort :: Ord a => [a] -> [a]
by binding them to the following types:
take :: Int -> [A] -> [A] sort :: [A] -> [A]
This type is homomorphic to Nat6
, B
, C
, D
, E
and F
.
It is instance to several typeclasses so that it can be used to test functions with type contexts.
Instances
Bounded A | |
Enum A | |
Eq A | |
Integral A | |
Num A | |
Ord A | |
Read A | |
Real A | |
Defined in Test.LeanCheck.Utils.Types toRational :: A -> Rational # | |
Show A | |
Ix A | |
Express A Source # | |
Defined in Conjure.Expr | |
Name A Source # | |
Defined in Conjure.Conjurable | |
Listable A | |
Conjurable A Source # | |
Defined in Conjure.Conjurable conjureArgumentHoles :: A -> [Expr] Source # conjureEquality :: A -> Maybe Expr Source # conjureTiers :: A -> Maybe [[Expr]] Source # conjureSubTypes :: A -> Reification Source # conjureIf :: A -> Expr Source # conjureCases :: A -> [Expr] Source # conjureArgumentCases :: A -> [[Expr]] Source # conjureSize :: A -> Int Source # conjureExpress :: A -> Expr -> Expr Source # conjureEvaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe A Source # |
Generic type B
.
Can be used to test polymorphic functions with two type variables
such as map
or foldr
:
map :: (a -> b) -> [a] -> [b] foldr :: (a -> b -> b) -> b -> [a] -> b
by binding them to the following types:
map :: (A -> B) -> [A] -> [B] foldr :: (A -> B -> B) -> B -> [A] -> B
Instances
Bounded B | |
Enum B | |
Eq B | |
Integral B | |
Num B | |
Ord B | |
Read B | |
Real B | |
Defined in Test.LeanCheck.Utils.Types toRational :: B -> Rational # | |
Show B | |
Ix B | |
Express B Source # | |
Defined in Conjure.Expr | |
Name B Source # | |
Defined in Conjure.Conjurable | |
Listable B | |
Conjurable B Source # | |
Defined in Conjure.Conjurable conjureArgumentHoles :: B -> [Expr] Source # conjureEquality :: B -> Maybe Expr Source # conjureTiers :: B -> Maybe [[Expr]] Source # conjureSubTypes :: B -> Reification Source # conjureIf :: B -> Expr Source # conjureCases :: B -> [Expr] Source # conjureArgumentCases :: B -> [[Expr]] Source # conjureSize :: B -> Int Source # conjureExpress :: B -> Expr -> Expr Source # conjureEvaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe B Source # |
Generic type C
.
Can be used to test polymorphic functions with three type variables
such as uncurry
or zipWith
:
uncurry :: (a -> b -> c) -> (a, b) -> c zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
by binding them to the following types:
uncurry :: (A -> B -> C) -> (A, B) -> C zipWith :: (A -> B -> C) -> [A] -> [B] -> [C]
Instances
Bounded C | |
Enum C | |
Eq C | |
Integral C | |
Num C | |
Ord C | |
Read C | |
Real C | |
Defined in Test.LeanCheck.Utils.Types toRational :: C -> Rational # | |
Show C | |
Ix C | |
Express C Source # | |
Defined in Conjure.Expr | |
Name C Source # | |
Defined in Conjure.Conjurable | |
Listable C | |
Conjurable C Source # | |
Defined in Conjure.Conjurable conjureArgumentHoles :: C -> [Expr] Source # conjureEquality :: C -> Maybe Expr Source # conjureTiers :: C -> Maybe [[Expr]] Source # conjureSubTypes :: C -> Reification Source # conjureIf :: C -> Expr Source # conjureCases :: C -> [Expr] Source # conjureArgumentCases :: C -> [[Expr]] Source # conjureSize :: C -> Int Source # conjureExpress :: C -> Expr -> Expr Source # conjureEvaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe C Source # |
Generic type D
.
Can be used to test polymorphic functions with four type variables.
Instances
Bounded D | |
Enum D | |
Eq D | |
Integral D | |
Num D | |
Ord D | |
Read D | |
Real D | |
Defined in Test.LeanCheck.Utils.Types toRational :: D -> Rational # | |
Show D | |
Ix D | |
Express D Source # | |
Defined in Conjure.Expr | |
Name D Source # | |
Defined in Conjure.Conjurable | |
Listable D | |
Conjurable D Source # | |
Defined in Conjure.Conjurable conjureArgumentHoles :: D -> [Expr] Source # conjureEquality :: D -> Maybe Expr Source # conjureTiers :: D -> Maybe [[Expr]] Source # conjureSubTypes :: D -> Reification Source # conjureIf :: D -> Expr Source # conjureCases :: D -> [Expr] Source # conjureArgumentCases :: D -> [[Expr]] Source # conjureSize :: D -> Int Source # conjureExpress :: D -> Expr -> Expr Source # conjureEvaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe D Source # |
Generic type E
.
Can be used to test polymorphic functions with five type variables.
Instances
Bounded E | |
Enum E | |
Eq E | |
Integral E | |
Num E | |
Ord E | |
Read E | |
Real E | |
Defined in Test.LeanCheck.Utils.Types toRational :: E -> Rational # | |
Show E | |
Ix E | |
Express E Source # | |
Defined in Conjure.Expr | |
Name E Source # | |
Defined in Conjure.Conjurable | |
Listable E | |
Conjurable E Source # | |
Defined in Conjure.Conjurable conjureArgumentHoles :: E -> [Expr] Source # conjureEquality :: E -> Maybe Expr Source # conjureTiers :: E -> Maybe [[Expr]] Source # conjureSubTypes :: E -> Reification Source # conjureIf :: E -> Expr Source # conjureCases :: E -> [Expr] Source # conjureArgumentCases :: E -> [[Expr]] Source # conjureSize :: E -> Int Source # conjureExpress :: E -> Expr -> Expr Source # conjureEvaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe E Source # |
Generic type F
.
Can be used to test polymorphic functions with five type variables.
Instances
Bounded F | |
Enum F | |
Eq F | |
Integral F | |
Num F | |
Ord F | |
Read F | |
Real F | |
Defined in Test.LeanCheck.Utils.Types toRational :: F -> Rational # | |
Show F | |
Ix F | |
Express F Source # | |
Defined in Conjure.Expr | |
Name F Source # | |
Defined in Conjure.Conjurable | |
Listable F | |
Conjurable F Source # | |
Defined in Conjure.Conjurable conjureArgumentHoles :: F -> [Expr] Source # conjureEquality :: F -> Maybe Expr Source # conjureTiers :: F -> Maybe [[Expr]] Source # conjureSubTypes :: F -> Reification Source # conjureIf :: F -> Expr Source # conjureCases :: F -> [Expr] Source # conjureArgumentCases :: F -> [[Expr]] Source # conjureSize :: F -> Int Source # conjureExpress :: F -> Expr -> Expr Source # conjureEvaluate :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe F Source # |