PaI
: A System for Grammar-based Program InversionThis is an implementation of the paper "Grammar-based Approach to Invertible Programs" written by Kazutaka Matsuda et al.
The program takes a input program written in a original programming language, and produces a Haskell code of its inverse.
$ cat examples/snoc.txt
snoc(Nil,y) = Cons(y,Nil)
snoc(Cons(a,x),y) = Cons(a,snoc(x,y))
$ ./pai examples/snoc.txt -i MyData > test.hs
$ ghci test.hs
...
Ok, module loaded: MyData, InvSnoc, InvUtil.
*Invsnoc> :t snoc
snoc :: List x -> x -> List x
*Invsnoc> :t inv_Fsnoc
inv_Fsnoc :: List t -> (List t, t)
*Invsnoc> snoc (Cons 1 (Cons 2 Nil)) 3
Cons 1 (Cons 2 (Cons 3 Nil))
*Invsnoc> inv_Fsnoc (Cons 1 (Cons 2 (Cons 3 Nil)))
(Cons 1 (Cons 2 Nil),3)
For non-injective fucntion, the system can generate a right inverse that enumerates possible corresponding inputs.
$ cat examples/add.txt
-- Noninjective program but linear & treeless
-- Hence, the correct right inverse is obtained.
add(Z,y) = y
add(S(x),y) = S(add(x,y))
$ ./pai examples/add.txt -i MyData > test.hs
--- Ambiguity Info ------------------------------
System failed to prove the injectivity because of following reasons:
Possibly range-overlapping expressions:
at (3,12) -- (4,1)
y
at (4,15) -- (5,1)
S(add{9}(x{10},y{11}))
$ ghci test.hs
...
Ok, modules loaded: MyData, Invadd, InvUtil.
*Invadd> :t add
add :: Nat -> Nat -> Nat
*Invadd> :t inv_Fadd
inv_Fadd :: Nat -> [(Nat,Nat)]
*Invadd> add (S Z) (S (S Z))
S (S (S Z))
*Invadd> inv_Fadd (S (S (S Z)))
[(Z,S (S (S Z))),(S Z,S (S Z)),(S (S Z),S Z),(S (S (S Z)),Z)]
*Invadd> map (uncurry add) $ inv_Fadd (S (S (S Z)))
[S (S (S Z)),S (S (S Z)),S (S (S Z)),S (S (S Z))]
*Invadd> :m +Data.List
*Invadd Data.List> nub $ map (uncurry add) $ inv_Fadd (S (S (S Z)))
[S (S (S Z))]
You can run these generated inverses with InvUtil.hs
and MyData.hs
. The directory examples
contains more examples.
Description | Input Program | Generated Inverse | Suff-Left | Suff-Right |
---|---|---|---|---|
([1,2],3) -> [1,2,3] | snoc.txt | SNOC.hs | OK | OK |
2*x | double.txt | DOUBLE.hs | OK | OK |
[1,2] -> [1,1,2,2] | doubleList.txt | DOUBLELIST.hs | OK | OK |
Runlength Encoding | runlength.txt | RUNLENGTH.hs | OK | |
Printing S Expression | print_sexp.txt | PRINT_SEXP.hs | OK | |
IO-Swapped reverse |
taba_reverse.txt | TABA_REVERSE.hs | OK | |
Injective zip |
zipI.txt | ZIPI.hs | OK | |
x + y | add.txt | ADD.hs | OK | |
zip |
zip.txt | ZIP.hs | OK | |
reverse |
reverse.txt | REVERSE.hs | ||
x + x | dupdouble.txt | DUPDOUBLE.hs |
The system fails to invert programs that satisfy neither Suff-Left nor Suff-Right. There is no guaratee that the obtained program is really inverse.
tar zxvf PaI.tar.gz
cd PaI
make
pai
(or, pai.exe
in Windows) is the name of the program inverterexamples
contains some examples.MyData.hs
contains data declarations for the examples.InvUtil.hs
contains function defintions used in the generated inverses.pai
-i MODULE_NAME
It inserts "import MODULE_NAME" to a generated inverse program.
-f INPUT_FILE
It specifies input file.
-m MODULE_NAME
It specifies the module name of a generated inverse program.
-d
It turns on debugMode flag.
-h
Not implemented. (help)
-t
With this flag, pai
shows elapsed time of code generation.
<Prog> ::= <Decl> ... <Decl>
<Decl> ::= FunName(<Pat>,...,<Pat>) = <Exp>
<Pat> ::= ConName(<Pat>,...,<Pat>)
| VarName
<Exp> ::= FunName(<Exp>,...,<Exp>)
| ConName(<Exp>,...,<Exp>)
| VarName
| let <Pat> = <Exp> in <Exp>
FunName = [a-z] [a-zA-Z0-9_]*
VarName = [a-z] [a-zA-Z0-9_]*
ConName = [A-Z] [a-zA-Z0-9_]*