Initial revision

[helm.git] / helm / interface / README

diff --git a/helm/interface/README b/helm/interface/README
new file mode 100644 (file)
index 0000000..89265ca
--- /dev/null
+++ b/helm/interface/README
@@ -0,0 +1,44 @@
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A tactic to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 22/11/1999                                 *)
+(******************************************************************************)
+
+This is the main directory of the coq-like pretty printer for cic terms exported
+in xml from Coq. Once compiled four different executables are made:
+
+ experiment            a command-line pretty-printer (interpreted)
+ experiment.opt        same as experiment (compiled)
+ gtkInterface          a gtk-based pretty-printer (interpreted)
+ gtkInterface.opt      a gtk-based pretty-printer (compiled)
+
+To use one of the previous pretty-printer the syntax is 
+
+        pretty_printer_name file1 ... filen
+
+where filei is an xml cic object
+
+Code files:
+
+ cic.ml            the internal definition of cic objects and terms
+ getter.ml         converts uris to filenames retrieving the correspondent file
+ cache.ml          a cache for cic objects (actually a simple hash-table)
+ cicParser.ml      a parser from xml to internal definition: top level
+ cicParser2.ml     a parser from xml to internal definition: objects level
+ cicParser3.ml     a parser from xml to internal definition: terms level
+ cicPp.ml          a pretty-printer for the internal definition of cic objects
+ experiment.ml     a textual interface to cicPp
+ gtkInterface.ml   a gtk interface to cicPp
+
+Interface files:
+ cache.mli getter.mli cicPp.mli cicParser.mli cicParser2.mli cicParser3.mli
+
+Other files:
+
+ Makefile     the targets are "all" "opt" "depend" "clean"
+ .depend      dependencies file used by make
+ examples     symbolic link to the root of the exported library