# `PaI`: A System for Grammar-based Program Inversion

## What is this?

This 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.
\$ ./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)
\$ ghci test.hs
...
add :: Nat -> Nat -> Nat
inv_Fadd :: Nat -> [(Nat,Nat)]
*Invadd> add (S Z) (S (S Z))
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 Data.List> nub \$ map (uncurry add) \$ inv_Fadd (S (S (S Z)))
[S (S (S Z))]
``````

## Examples

You can run these generated inverses with `InvUtil.hs` and `MyData.hs`. The directory `examples` contains more examples.

Description Input ProgramGenerated InverseSuff-LeftSuff-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
`zip` zip.txt ZIP.hs OK
`reverse` reverse.txt REVERSE.hs
x + x dupdouble.txt DUPDOUBLE.hs
• Suff-Left: Program is non-erasing and generated grammar is unambiguous.
• Suff-Right: Program is affine and treeless.

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.

## How to build

1. Install GHC over 6.8.2.
3. Unpack the tar file: `tar zxvf PaI.tar.gz`
4. Move to the generated directory: `cd PaI`
5. `make`
• In case of trouble, please edit make file to fix the problem.
• `pai` (or, `pai.exe` in Windows) is the name of the program inverter
• Directory `examples` contains some examples.
• `MyData.hs` contains data declarations for the examples.
• `InvUtil.hs` contains function defintions used in the generated inverses.

## Options of `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.

## Syntax of Input Program

``````<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_]*
``````

## Limitations & Known Issues

• The derived code may not accept a value in the range of original function if the ambiguity test does not succeed.