A System for Bidirectionalizing View Function

What is This

This system automatically generates backward transformation programs based on derivation of view complement functions.

System Requirements

The system requires the following programs at least.

• GHC 6.4.2
• Happy 1.13
• Alex 2.0.1

How to Build

1. Download either one of the following archives.
   • generate_cmpl_0.1.tar.gz
   • generate_cmpl_0.1.tar.bz2
2. Unpack the archive.
3. Run make.

Then the program generate_cmpl is generated at the directory. The directory sample_inputs/ contains sample program files of view definition.

How to Use

Invoke the system by running the following command with view definition files.

> generate_cmpl VIEW_DEFINITION_FILES

Then, the system parses the input files and generates complement functions, the tupled functions and their inverse functions. the system prints a prompt “bt> ” to wait the next command.

For example, try a view definition file sample_inputs/test.txt. You can evaluate any expressions in FORWARD program from the prompt.

bt> add(S(Z),Z)
[S(Z)]

You can invoke backward transformation function by the command “:reflect” with a function call expression. Then, the system calculates the expressions and prints transitions of updatability checking automaton.

bt> :reflect add(S(Z),Z)
Current View: S(Z)
(S(0) ===> 0
S(1) ===> 0
Z    ===> 1
,[0])

Update To? 

The prompt asks how you want to update from the current value to. For example, if you input put S(S(S(S(S(Z))))) as a updated view,

Update To? S(S(S(S(S(Z)))))
Update Succeeded:
  #(S(Z),S(S(S(S(Z)))))

That output means updated arguments of the first function call.

You can quit the system by typing “:quit”.

Sample of View Definitions.

Addition of two natural numbers

Input (view definition)

add(S(x),y) = S(add(x,y))
add(Z,y)    = y

Output (complement function and backward transformation)

== Original Source =============================================================
add(S(x),y) = S(add(x,y))
add(Z,y)    = y

== Derived Complement ==========================================================
_add(S(x),y) = _B_add_0(_add(x,y))
_add(Z,y)    = _B_add_1

== Tupled Functions ============================================================
#add(S(x),y) = #(S(*a0),_B_add_0(*b0))
  where
    #(*a0,*b0) = #add(x,y)
#add(Z,y)    = #(y,_B_add_1)

== Inverted Tupled Functions ===================================================
#add#Inv(S(*a0),_B_add_0(*b0)) = #(S(x),y)
  where
    #(x,y) = #add#Inv(*a0,*b0)
#add#Inv(y,_B_add_1)           = #(Z,y)

bt> add(S(S(Z)),Z)
[S(S(Z))]
bt> :reflect add(S(S(Z)),Z)
Current View: S(S(Z))
(S(0) ===> 0
S(1) ===> 0
S(2) ===> 1
Z    ===> 2
,[0])

Update To?  S(S(S(S(S(Z)))))
Update Succeeded:
  #(S(S(Z)),S(S(S(Z))))
bt> :quit