Conjure.Prim

This module is part of Conjure.

The Prim type and utilities involving it.

You are probably better off importing Conjure.

Documentation

type Prim = (Expr, Reification)

A primitive expression (paired with instance reification). Create Prims with pr and prim.

prim :: Conjurable a => String -> a -> Prim

Provides a primitive value to Conjure. To be used on values that are not Show instances such as functions. (cf. pr)

conjure "fun" fun [ ...
                  , prim "&&" (&&)
                  , prim "||" (||)
                  , prim "+" ((+) :: Int -> Int -> Int)
                  , prim "*" ((*) :: Int -> Int -> Int)
                  , prim "-" ((-) :: Int -> Int -> Int)
                  , ...
                  ]

Argument types have to be monomorphized, so use type bindings when applicable.

pr :: (Conjurable a, Show a) => a -> Prim

Provides a primitive value to Conjure. To be used on Show instances. (cf. prim)

conjure "fun" fun [ pr False
                  , pr True
                  , pr (0 :: Int)
                  , pr (1 :: Int)
                  , ...
                  ]

Argument types have to be monomorphized, so use type bindings when applicable.

prif :: Conjurable a => a -> Prim

Provides an if condition bound to the given return type.

This should be used when one wants Conjure to consider if-expressions at all:

last' :: [Int] -> Int
last' [x]  =  x
last' [x,y]  =  y
last' [x,y,z]  =  z

> conjure "last" last' [ pr ([] :: [Int])
>                      , prim ":" ((:) :: Int -> [Int] -> [Int])
>                      , prim "null" (null :: [Int] -> Bool)
>                      , prif (undefined :: Int)
>                      , prim "undefined" (undefined :: Int)
>                      ]
last :: [Int] -> Int
-- 0.0s, testing 360 combinations of argument values
-- 0.0s, pruning with 5/5 rules
-- ...   ...   ...   ...   ...
-- 0.0s, 4 candidates of size 7
-- 0.0s, tested 2 candidates
last []  =  undefined
last (x:xs)  =  if null xs
                then x
                else last xs

primOrdCaseFor :: Conjurable a => a -> Prim

Provides a case condition bound to the given return type.

This should be used when one wants Conjure to consider ord-case expressions:

> conjure "mem" mem
>   [ pr False
>   , pr True
>   , prim "`compare`" (compare :: Int -> Int -> Ordering)
>   , primOrdCaseFor (undefined :: Bool)
>   ]
mem :: Int -> Tree -> Bool
-- ...   ...   ...   ...   ...
-- 0.0s, 384 candidates of size 12
-- 0.0s, tested 346 candidates
mem x Leaf  =  False
mem x (Node t1 y t2)  =  case x `compare` y of
                         LT -> mem x t1
                         EQ -> True
                         GT -> mem x t2

guard :: Prim

Provides an if condition bound to the conjured function's return type.

Guards are only alllowed at the root fo the RHS.

last' :: [Int] -> Int
last' [x]  =  x
last' [x,y]  =  y
last' [x,y,z]  =  z

> conjure "last" last'
>   [ pr ([] :: [Int])
>   , prim ":" ((:) :: Int -> [Int] -> [Int])
>   , prim "null" (null :: [Int] -> Bool)
>   , guard
>   , prim "undefined" (undefined :: Int)
>   ]
last :: [Int] -> Int
-- 0.0s, testing 360 combinations of argument values
-- 0.0s, pruning with 5/5 rules
-- 0.0s, 1 candidates of size 1
-- 0.0s, 0 candidates of size 2
-- 0.0s, 0 candidates of size 3
-- 0.0s, 0 candidates of size 4
-- 0.0s, 0 candidates of size 5
-- 0.0s, 0 candidates of size 6
-- 0.0s, 4 candidates of size 7
-- 0.0s, tested 2 candidates
last []  =  undefined
last (x:xs)
  | null xs  =  x
  | otherwise  =  last xs

cjHoles :: [Prim] -> [Expr]

Computes a list of holes encoded as Exprs from a list of Prims.

This function mirrors functionality from conjureHoles.

cjTiersFor :: [Prim] -> Expr -> [[Expr]]

Given a list of Prims, returns a function that given an Expr will return tiers of test Expr values.

This is used in cjAreEqual.

cjAreEqual :: [Prim] -> Int -> Expr -> Expr -> Bool

Given a list of Prims, computes a function that checks whether two Exprs are equal up to a given number of tests.

cjMkEquation :: [Prim] -> Expr -> Expr -> Expr

Computes a function that equates two Exprs from a list of Prims.

This function mirrors functionality from conjureMkEquation.