==========   LoopW imperative proof inference and proof checking program   ==========

This tool contains two executables, namely loopW and loopWc.

I. loopW: imperative proof inference.

The loopW inference tool reads its input in a file with extension ".loop" and tries to infer a correct
and complete proof derivation that corresponds to the given source code.

usage: loopW [-version] [-v123] [-uprint] [-print] [-pprint] [-form] [-tex] [-ott] file.loop
  -version print version and exit
  -v       Verbosity level (1 : low, 2 : medium, 3 : high)
  -uprint  Erase all type information and pretty print (file.cs)
  -print   Pretty print (file.rev.loop)
  -pprint  Complete infered proof pretty printing (file.proof)
  -form    Display formula-like types instead of imperative types
  -tex     Tex output
  -ott     Ott/twelf complete infered proof pretty printing (file.loop.ott)

NOTES

- On Unix systems (including Mac OS X) you need to have mono (www.mono-project.com)
  installed and you can then run the command as:

  mono loopW.exe [-version] [-v123] [-uprint] [-print] [-pprint] [-form] [-tex] [-ott] file.loop

II. loopWc: imperative proof checking, functional translation and proof checking.

The loopWc proof checker and translater tool reads its input in a file with extension ".proof" (eventually
written by the loopW tool (see above)). It first checks the imperative proof derivation, then it
translate it into a functional proof derivation and check it.

usage: loopWc [-version] [-v123] [-uprint] [-fprint] file.proof
  -version print version and exit
  -v       Verbosity level (1 : low, 2 : medium, 3 : high)
  -uprint  Erase all type information and pretty print (file.pcs)
  -fprint  Functional translation (untyped) pretty print (file.sml)

NOTES

- On Unix systems (including Mac OS X) you need to have mono (www.mono-project.com)
  installed and you can then run the command as:

  mono loopWc.exe [-version] [-v123] [-uprint] [-fprint] file.proof

- The generated sml file can be tested with SML/NJ with the provided library file:

  sml lib.sml file.sml