Implementation of the distillation algorithm as described in the paper "Distillation: Extracting the Essence of Programs".
License: BSD 3-Clause "New" or "Revised" License
When I try to distill the following code I get the error:
Constructor application is not saturated: 1 v
CallStack (from HasCallStack):
error, called at src/Trans.hs:36:44 in distiller-0.1.0.0-HlUVpzbHjXb1UQKvCSDDcW:Trans
Code to distill:
import Bool
import Nat
main = map is_z_nut g (mAdd is_z_bool op m1 m2)
;
is_z_nut x = eqNat x (Zero)
;
is_z_bool x = eqBool x (False)
;
op x y = or x y
;
g x = (Succ(Zero))
;
map isZ g m =
case m of
Error -> Error
| None -> None
| Val (v) -> (mkNode isZ (g v))
| Node (q1, q2, q3, q4) -> (Node(
(map isZ g q1)
,(map isZ g q2)
,(map isZ g q3)
,(map isZ g q4)))
;
mAdd isZ g m1 m2 =
case m1 of
Error -> Error
| None -> (m2)
| Val (v1) -> (case m2 of
Error -> Error
| None -> m1
| Val (v) -> (mkNode isZ (g v1 v))
| Node (t1, t2, t3, t4) -> Error)
| Node (q1, q2, q3, q4) -> (case m2 of
Error -> Error
| None -> m1
| Val (v) -> Error
| Node (t1, t2, t3, t4) -> (Node(
(mAdd isZ g q1 t1)
,(mAdd isZ g q2 t2)
,(mAdd isZ g q3 t3)
,(mAdd isZ g q4 t4))))
The reason is fiction g x = (Succ(Zero)) which throws out the argument and always returns the constant 1. Looks like the body of the function substituted instead of the call and as a result, we try to apply 1 to a variable.
The distiller generates a big number of equal-modulo-renaming functions for the following example (elementwise addition of two matrices)
main = mAdd isZ g m1 (mAdd isZ h m2 m3);
mAdd isZ g m1 m2 =
case m1 of
Error -> Error
| None -> (m2)
| Val (v1) -> (case m2 of
Error -> Error
| None -> m1
| Val (v) -> (mkNode isZ (g v1 v))
| Node (t1, t2, t3, t4) -> Error)
| Node (q1, q2, q3, q4) -> (case m2 of
Error -> Error
| None -> m1
| Val (v) -> Error
| Node (t1, t2, t3, t4) -> (Node(
(mAdd isZ g q1 t1)
,(mAdd isZ g q2 t2)
,(mAdd isZ g q3 t3)
,(mAdd isZ g q4 t4))))
It may be not important for the formal correctness of transformation, but when we try to generate hardware for distillation result, each function requires additional LUTs in a target circuit.
The following code is a matrix-matrix multiplication (for matrices represented as quad-trees). Distillation of this code does not finish in a reasonable time (30 min).
main = mMult is_zero op_add op_mult mtx1 mtx2
;
mMult isZ f_add f_mul m1 m2 =
case m1 of
Error -> Error
| None -> None
| Val (v1) ->
(case m2 of
Error -> Error
| None -> None
| Val (v) -> (mkNode isZ (f_mul v1 v))
| Node (t1, t2, t3, t4) -> Error)
| Node (q1, q2, q3, q4) ->
(case m2 of
Error -> Error
| None -> None
| Val (v) -> Error
| Node (t1, t2, t3, t4) ->
(Node(
(mAdd isZ f_add (mMult isZ f_add f_mul q1 t1)(mMult isZ f_add f_mul q2 t3))
,(mAdd isZ f_add (mMult isZ f_add f_mul q1 t2)(mMult isZ f_add f_mul q2 t4))
,(mAdd isZ f_add (mMult isZ f_add f_mul q3 t1)(mMult isZ f_add f_mul q4 t3))
,(mAdd isZ f_add (mMult isZ f_add f_mul q3 t2)(mMult isZ f_add f_mul q4 t4))))
)
;
mAdd isZ f_add m1 m2 =
case m1 of
Error -> Error
| None -> (m2)
| Val (v1) -> (case m2 of
Error -> Error
| None -> m1
| Val (v) -> (mkNode isZ (f_add v1 v))
| Node (t1, t2, t3, t4) -> Error)
| Node (q1, q2, q3, q4) -> (case m2 of
Error -> Error
| None -> m1
| Val (v) -> Error
| Node (t1, t2, t3, t4) -> (Node(
(mAdd isZ f_add q1 t1)
,(mAdd isZ f_add q2 t2)
,(mAdd isZ f_add q3 t3)
,(mAdd isZ f_add q4 t4))))
Here is the file I used in my test:
main = root input;
root xs = map' (\x -> Succ(x)) (rev' xs Nil);
map' f xs = case xs of
Nil -> Nil
| Cons(x,xs) -> Cons(f x, map' f xs);
rev' xs acc = case xs of
Nil -> acc
| Cons(x,xs) -> rev' xs (Cons(x,acc))And here is the output, using the master branch (commit 3969101):
POT> :load test
Loading file: test.pot
POT> :prog
main = root input;
root xs = map' (\x.Succ(x)) (rev' xs []);
map' f xs = case xs of
Nil -> []
| Cons(x,xs) -> Cons(f x,map' f xs);
rev' xs acc = case xs of
Nil -> acc
| Cons(x,xs) -> (rev' xs Cons(x,acc))
POT> :distill
main = case input of
Nil -> []
| Cons(x,xs) -> (rev' xs [x]);
rev' xs acc = case xs of
Nil -> acc
| Cons(x,xs) -> (rev' xs Cons(x,acc))
It looks like the distilled result is equivalent to rev and does not take into account the map operation. How come?
Hello.
I try to use Distiller for tree-manipulation programs transformation, but I have the following problem.
Suppose I have the following function:
eWizeOp g s m =
case m of
Val (v1) -> (Val (g v1 s))
| Node (q1, q2) -> (Node ((eWizeOp g s q1), (eWizeOp g s q2)))
When I try to distill the following term
main = eWizeOp g s2 (eWizeOp g2 s m) ;
the result is correct, but when I try to distill the term
main = eWizeOp g s2 (eWizeOp g s m) ;
the distiller does not terminate.
The only difference between these two cases is that I use the same first parameter in both calls of the eWizeOp function in the second case.
Full tests.
-- OK
main = eWizeOp g s2 (eWizeOp g2 s m) ;
eWizeOp g s m =
case m of
Val (v1) -> (Val (g v1 s))
| Node (q1, q2) -> (Node ((eWizeOp g s q1), (eWizeOp g s q2)))
-- Fail
main = eWizeOp g s2 (eWizeOp g s m) ;
eWizeOp g s m =
case m of
Val (v1) -> (Val (g v1 s))
| Node (q1, q2) -> (Node ((eWizeOp g s q1), (eWizeOp g s q2)))
I wrote naïve reverse function that reverses by second end: moves last element to front and recursively reverses all elements but the last:
main = nrev2 xs;
nrev2 xs =
case xs of
Nil -> Nil
| Cons(a, as) -> Cons(last a as, nrev2 (cutlast a as));
last b bs =
case bs of
Nil -> b
| Cons(c, cs) -> last c cs;
cutlast d ds =
case ds of
Nil -> Nil
| Cons(e, es) -> Cons(d, cutlast e es)
Residual program is incorrect:
main = case xs of
Nil -> []
| Cons(a,as) -> Cons(f as a,f' as a);
f' as a = case as of
Nil -> []
| Cons(e,es) -> Cons(f'' es a,f' es a);
f'' es a = case es of
Nil -> a
| Cons(e,es) -> (f'' es e);
f as a = case as of
Nil -> a
| Cons(c,cs) -> (f cs c)
Function f' forgets e variable.
Distillation of the following example failed with
Main: Trans.hs:(13,1)-(43,72): Non-exhaustive patterns in function distill
An example:
main = trav2 f g t
;
trav1 f t =
case t of
Val (v) -> (f v)
| Node (t1, t2) -> Node ((trav1 f t1), (trav1 f t2))
;
trav2 f g t =
case t of
Val (v) -> (f v)
| Node (t1, t2) -> (trav1 g (Node ((trav2 f g t1), (trav2 f g t2))))
Hi Geoff,
the following example forces the distiller into an infinite loop:
main = (uequal (uadd x y) (uadd y x));
uadd x y = case x of
Z -> y
| S(xs) -> (uadd xs S(y));
uequal x y = case x of
Z -> (case y of
Z -> True
| S(ys) -> False)
| S(xs) -> (case y of
Z -> True
| S(ys) -> (uequal xs ys))
I try to distill the following code:
main = fold f2 s (map isZ f1 m1);
mkNode isZ x = case (isZ x) of True -> None | False -> Val(x);
reduceTree n1 n2 n3 n4 = Node (n1, n2, n3, n4);
map isZ g m =
case m of
Error -> Error
| None -> None
| Val (v) -> (mkNode isZ (g v))
| Node (q1, q2, q3, q4) -> (reduceTree
(map isZ g q1)
(map isZ g q2)
(map isZ g q3)
(map isZ g q4))
;
fold g s m =
case m of
None -> s
| Error -> s
| Val(v) -> (g s v)
| Node (n1, n2, n3, n4) -> (fold g (fold g (fold g (fold g s n1) n2) n3) n4)
But the distiller does not terminate.
But if I inline reduceTree manually, then distillation terminates successfully. So, the following code can be distilled.
main = fold f2 s (map isZ f1 m1);
mkNode isZ x = case (isZ x) of True -> None | False -> Val(x);
reduceTree n1 n2 n3 n4 = Node (n1, n2, n3, n4);
map isZ g m =
case m of
Error -> Error
| None -> None
| Val (v) -> (mkNode isZ (g v))
| Node (q1, q2, q3, q4) -> (Node(
(map isZ g q1)
,(map isZ g q2)
,(map isZ g q3)
,(map isZ g q4)))
;
fold g s m =
case m of
None -> s
| Error -> s
| Val(v) -> (g s v)
| Node (n1, n2, n3, n4) -> (fold g (fold g (fold g (fold g s n1) n2) n3) n4)
I wrote function map with accumulator filling by append:
main = map g xs;
map g xs = map1 Nil g xs;
map1 res g xs =
case xs of
Nil -> res
| Cons(x, xs1) -> map1 (push res (g x)) g xs1;
push xs c =
case xs of
Nil -> Cons(c, Nil)
| Cons(x, xs1) -> Cons(x, (push xs1 c))
(Instead append I used push as special case for one element list.)
Residual program don’t contain constructor Cons in right parts of clauses and call f x' g x is too strange:
main = f xs [] g;
f xs x' g = case xs of
Nil -> x'
| Cons(x,xs1) -> (f xs1 (f x' g x) g)
I simplified the program, changed g argument to G(•) constructor:
main = map xs;
map xs = map1 Nil xs;
map1 res xs =
case xs of
Nil -> res
| Cons(x, xs1) -> map1 (push res G(x)) xs1;
push xs c =
case xs of
Nil -> Cons(c, Nil)
| Cons(x, xs1) -> Cons(x, (push xs1 c))
Residual program don’t contain G(•) constructor:
main = f xs [];
f xs x' = case xs of
Nil -> x'
| Cons(x,xs1) -> (f xs1 (f x' x))
What I’m doing wrong? Maybe I have typos in source programs?
There is the source code:
main = myeq (mymul x S(Z)) (mymul Z x);
myeq x y = case x of
Z -> (case y of
Z -> True
| S(ys) -> False)
| S(xs) -> (case y of
Z -> True
| S(ys) -> myeq xs ys);
mymul x y = case x of
Z -> Z
| S(xs) -> myadd y (mymul xs y);
myadd x y = case x of
Z -> y
| S(xs) -> myadd xs S(y)
There is the residual program:
main = case x of
Z -> True
| S(xs) -> True
Expected result:
main = case x of
Z -> True
| S(xs) -> False
I've written a simple multiplication function:
main = multiply x y;
add x y = case y of
Zero -> x
| Succ(y') -> Succ(add x y');
multiply x y = case y of
Zero -> 0
| Succ(y') -> add (multiply x y') x
This produces:
main = case y of
Zero -> 0
| Succ(y') -> (f x y');
f x y' = case x of
Zero -> (case y' of
Zero -> 0
| Succ(y') -> (f' y'))
| Succ(y'') -> Succ(f y'' y');
f' y'' = case y'' of
Zero -> 0
| Succ(y') -> (f' y')
However this is incorrect. E.g:
POT> :eval
x = 3
y = 5
15
Reductions: 114
Allocations: 26
POT> :distill
...
POT> :eval
y = 5
x = 3
3
Reductions: 32
Allocations: 10
Am I doing something wrong?
I try to distill the fold-map composition over a boolean list.
map and fold implemented as follows
map f l =
case l of
Nil -> Nil
| Cons (hd, tl) -> (Cons ((f hd), (map f tl)))
;
fold f s l =
case l of
Nil -> s
| Cons (hd, tl) -> (fold f (f s hd) tl)
Distillation of fold g False (map not l) works fine, but the distillation of fold or False (map not l) fails with the following message:
POT> :distill
Main: No matching pattern in case for term:
case False(map not l) of
True -> True
| False -> hd
CallStack (from HasCallStack):
error, called at ./Trans.hs:34:62 in main:Trans
In the first case g is an abstract function, and in the second case I specify the first parameter of fold to be a not function from Boolean.pot (instead of g).
Full test:
import Bool
main =
-- OK
fold g False (map not l)
-- Fail
-- fold or False (map not l)
;
map f l =
case l of
Nil -> Nil
| Cons (hd, tl) -> (Cons ((f hd), (map f tl)))
;
fold f s l =
case l of
Nil -> s
| Cons (hd, tl) -> (fold f (f s hd) tl)
Distillation of the Example1 (see below) failed with the following message:
Main: Prelude.head: empty list
At the same time, a distillation of both Example2 and Example3 does not finish in a reasonable time. All three examples express the same thing but in a different manner.
Example1:
main = mOp op m
;
reduceTree n1 n2 =
let nd = (Node (n1, n2)) in
(case n1 of
None -> (case n2 of
None -> None
| Val (v1) -> nd
| Node (m1, m2) -> nd)
| Val (v2) -> nd
| Node (l1, l2) -> nd)
;
mOp g m =
case m of
None -> None
| Val (v1) -> (g v1)
| Node (q1, q2) -> (reduceTree (mOp g q1) (mOp g q2))
Example2:
main = mOp op m
;
reduceTree n1 n2 =
(case n1 of
None -> (case n2 of
None -> None
| Val (v1) -> (Node (n1, n2))
| Node (m1, m2) -> (Node (n1, n2)))
| Val (v2) -> (Node (n1, n2))
| Node (l1, l2) -> (Node (n1, n2)))
;
mOp g m =
case m of
None -> None
| Val (v1) -> (g v1)
| Node (q1, q2) -> (reduceTree (mOp g q1) (mOp g q2))
Example3:
main = mOp op m
;
reduceTree n1 n2 nd =
case n1 of
None -> (case n2 of
None -> None
| Val (v1) -> nd
| Node (m1, m2) -> nd)
| Val (v2) -> nd
| Node (l1, l2) -> nd
;
mOp g m =
case m of
None -> None
| Val (v1) -> (g v1)
| Node (q1, q2) -> (reduceTree (mOp g q1) (mOp g q2) (Node (q1, q2)))
Source program contains f variable in entry point:
main = map f xs;
map g xs =
case xs of
Nil -> Nil
| Cons(x, xs1) -> Cons(g x, map g xs1)
Residual program contains two f names: name of variable in source and name of generated function:
main = f xs f;
f xs f = case xs of
Nil -> []
| Cons(x,xs1) -> Cons(f x,f xs1 f)
For reducing confusion new generated functions should have names different from variables in entry point.
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
Django
The Web framework for perfectionists with deadlines.
Laravel
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft
Open source projects and samples from Microsoft.
Google
Google ❤️ Open Source for everyone.
Alibaba
Alibaba Open Source for everyone
D3
Data-Driven Documents codes.
Tencent
China tencent open source team.