code-conjure-0.5.8: synthesize Haskell functions out of partial definitions
Copyright(c) 2021 Rudy Matela
License3-Clause BSD (see the file LICENSE)
MaintainerRudy Matela <rudy@matela.com.br>
Safe HaskellSafe-Inferred
LanguageHaskell2010

Conjure.Defn

Description

This module is part of Conjure.

This module exports the Defn type synonym and utilities involving it.

You are probably better off importing Conjure.

Synopsis

Documentation

type Defn = [Bndn] Source #

A function definition as a list of top-level case bindings (Bndn).

Here is an example using the notation from Data.Express.Fixtures:

sumV :: Expr
sumV  =  var "sum" (undefined :: [Int] -> Int)

(=-) = (,)
infixr 0 =-

sumDefn :: Defn
sumDefn  =  [ sum' nil           =-  zero
            , sum' (xx -:- xxs)  =-  xx -+- (sumV :$ xxs)
            ]  where  sum' e  =  sumV :$ e

type Bndn = (Expr, Expr) Source #

A single binding in a definition (Defn).

toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic Source #

Evaluates an Expr to a Dynamic value using the given Defn as definition when a recursive call is found.

Arguments:

  1. a function that deeply reencodes an expression (cf. expr)
  2. the maximum number of recursive evaluations
  3. a Defn to be used when evaluating the given Expr
  4. an Expr to be evaluated

This function cannot be used to evaluate a functional value for the given Defn and can only be used when occurrences of the given Defn are fully applied.

The function the deeply reencodes an Expr can be defined using functionality present in Conjure.Conjurable. Here's a quick-and-dirty version that is able to reencode Bools, Ints and their lists:

exprExpr :: Expr -> Expr
exprExpr  =  conjureExpress (undefined :: Bool -> [Bool] -> Int -> [Int] -> ())

The maximum number of recursive evaluations counts in two ways:

  1. the maximum number of entries in the recursive-evaluation memo table;
  2. the maximum number of terminal values considered (but in this case the limit is multiplied by the _size_ of the given Defn.

These could be divided into two separate parameters but then there would be an extra _dial_ to care about...

(cf. devaluate, deval, devl)

devaluate :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a Source #

Evaluates an Expr expression into Just a regular Haskell value using a Defn definition when it is found. If there's a type-mismatch, this function returns Nothing.

This function requires a Expr-deep-reencoding function and a limit to the number of recursive evaluations.

(cf. toDynamicWithDefn, deval, devl)

deval :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a Source #

Evaluates an Expr expression into a regular Haskell value using a Defn definition when it is found in the given expression. If there's a type-mismatch, this function return a default value.

This function requires a Expr-deep-reencoding function and a limit to the number of recursive evaluations.

(cf. toDynamicWithDefn, devaluate, devl')

devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a Source #

Evaluates an Expr expression into a regular Haskell value using a Defn definition when it is found in the given expression. If there's a type-mismatch, this raises an error.

This function requires a Expr-deep-reencoding function and a limit to the number of recursive evaluations.

(cf. toDynamicWithDefn, devaluate, deval')

devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a Source #

Like deval but only works for when the given Defn definition has no case breakdowns.

In other words, this only works when the given Defn is a singleton list whose first value of the only element is a simple application without constructors.

showDefn :: Defn -> String Source #

Pretty-prints a Defn as a String:

> putStr $ showDefn sumDefn
sum []  =  0
sum (x:xs)  =  x + sum xs

printDefn :: Defn -> IO () Source #

Pretty-prints a Defn to the screen.

> printDefn sumDefn
sum []  =  0
sum (x:xs)  =  x + sum xs

defnApparentlyTerminates :: Defn -> Bool Source #

Returns whether the given definition apparentlyTerminates.

isRedundantDefn :: Defn -> Bool Source #

Returns whether the given Defn is redundant with regards to repetitions on RHSs.

Here is an example of a redundant Defn:

0 ? 0  =  1
0 ? x  =  1
x ? 0  =  x
x ? y  =  x

It is redundant because it is equivalent to:

0 ? _  =  1
x ? _  =  x

This function safely handles holes on the RHSs by being conservative in cases these are found: nothing can be said before their fillings.

isRedundantBySubsumption :: Defn -> Bool Source #

Returns whether the given Defn is redundant with regards to subsumption by latter patterns

Here is an example of a redundant Defn by this criterium:

foo 0  =  0
foo x  =  x

isRedundantByRepetition :: Defn -> Bool Source #

Returns whether the given Defn is redundant with regards to repetitions on RHSs.

Here is an example of a redundant Defn:

0 ? 0  =  1
0 ? x  =  1
x ? 0  =  x
x ? y  =  x

It is redundant because it is equivalent to:

0 ? _  =  1
x ? _  =  x

1 and x are repeated in the results for when the first arguments are 0 and x.

isRedundantByIntroduction :: Defn -> Bool Source #

Returns whether the given Defn is redundant with regards to case elimination

The following is redundant according to this criterium:

foo []  =  []
foo (x:xs)  =  x:xs

It is equivalent to:

foo xs = xs

The following is also redundant:

[] ?? xs  =  []
(x:xs) ?? ys  =  x:xs

as it is equivalent to:

xs ?? ys == xs

This function is not used as one of the criteria in isRedundantDefn because it does not pay-off in terms of runtime vs number of pruned candidates.

hasRedundantRecursion :: Defn -> Bool Source #

Returns whether the given Defn is redundant with regards to recursions

The following is redundant:

xs ?? []  =  []
xs ?? (x:ys)  =  xs ?? []

The LHS of a base-case pattern, matches the RHS of a recursive pattern. The second RHS may be replaced by simply [] which makes it redundant.

isCompleteDefn :: Defn -> Bool Source #

Returns whether the definition is complete, i.e., whether it does not have any holes in the RHS.

isCompleteBndn :: Bndn -> Bool Source #

Returns whether the binding is complete, i.e., whether it does not have any holes in the RHS.

simplifyDefn :: Defn -> Defn Source #

Simplifies a definition by removing redundant patterns

This may be useful in the following case:

0 ^^^ 0  =  0
0 ^^^ x  =  x
x ^^^ 0  =  x
_ ^^^ _  =  0

The first pattern is subsumed by the last pattern.

hasUnbound :: Bndn -> Bool Source #

Returns whether a binding has undefined variables, i.e., there are variables in the RHS that are not declared in the LHS.

> hasUnbound (xx -:- xxs, xxs)
False
> hasUnbound (xx -:- xxs, yys)
True

For Defns, use isUndefined.

isUndefined :: Defn -> Bool Source #

Returns whether a Defn has undefined variables, i.e., there are variables in the RHSs that are not declared in the LHSs.

> isUndefined [(nil, nil), (xx -:- xxs, xxs)]
False
> isUndefined [(nil, xxs), (xx -:- xxs, yys)]
True

For single Bndns, use hasUnbound.

introduceVariableAt :: Int -> Bndn -> Bndn Source #

Introduces a hole at a given position in the binding:

> introduceVariableAt 1 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
(xs ? (y:ys) :: [Int],(y:ys) ++ (y:ys) :: [Int])
> introduceVariableAt 2 (xxs -?- (yy -:- yys), (yy -:- yys) -++- (yy -:- yys))
(xs ? x :: [Int],x ++ x :: [Int])

Relevant occurrences are replaced.

isBaseCase :: Bndn -> Bool Source #

Returns whether a binding is a base case.

> isBaseCase (ff (xx -:- nil), xx)
True
> isBaseCase (ff (xx -:- xxs), ff xxs)
False

(cf. isRecursiveCase)

isRecursiveCase :: Bndn -> Bool Source #

Returns whether a binding is a base case.

> isRecursiveCase (ff (xx -:- nil), xx)
False
> isRecursiveCase (ff (xx -:- xxs), ff xxs)
True

(cf. isBaseCase)

isRecursiveDefn :: Defn -> Bool Source #

Returns whether a definition is recursive