Read OpenTheory package files

Author: gilith

README.md

@@ -21,6 +21,29 @@ Use [cabal][] to run the test suite:
 
     cabal test
 
+Run
+----
+
+Use hol-package contains an executable called hol-pkg, which is run as follows:
+
+    Usage: hol-pkg INPUT
+    where INPUT is one of the following forms:
+      FILE.art     : a proof article file
+      FILE.thy     : a theory package file
+      NAME-VERSION : a specific version of an installed theory package
+      NAME ...     : the latest version of a list of packages
+
+The hol-pkg program reads the INPUT to generate a set of theorems, which are pretty-printed to standard output together with the symbols they contain. For example, the command hol-pkg unit generates the following output:
+
+    3 type operators: (->) bool unit
+    6 constants: (=) (!) (==>) (?) (?!) ()
+    5 theorems:
+      |- !v. v = ()
+      |- !f g. f = g
+      |- !e. ?fn. fn () = e
+      |- !e. ?!fn. fn () = e
+      |- !p. p () ==> !x. p x
+
 Profile
 -------
 

hol.cabal

@@ -6,7 +6,7 @@ license: MIT
 license-file: LICENSE
 cabal-version: >= 1.8.0.2
 build-type: Simple
-extra-source-files: README.md doc/axioms.txt doc/bool.txt test/bool.art test/bool.int test/bool.thy
+extra-source-files: README.md doc/axioms.txt doc/bool.txt test/bool.art test/bool.int test/bool.thy test/bool-def.art
 extra-tmp-files: hol-profile.aux hol-profile.hp hol-profile.pdf hol-profile.prof hol-profile.ps
 author: Joe Leslie-Hurd <[email protected]>
 maintainer: Joe Leslie-Hurd <[email protected]>
@@ -18,6 +18,7 @@ Library
     base >= 4.0 && < 5.0,
     bytestring >= 0.9 && < 0.10,
     containers >= 0.5 && < 0.6,
+    filepath >= 1.3 && < 1.4,
     parsec >= 3.1 && < 3.2,
     pretty >= 1.1 && < 1.2,
     process >= 1.2 && < 1.3,
@@ -31,6 +32,9 @@ Library
     HOL.Data
     HOL.Name
     HOL.OpenTheory
+    HOL.OpenTheory.Article
+    HOL.OpenTheory.Interpret
+    HOL.OpenTheory.Package
     HOL.Parse
     HOL.Print
     HOL.Rule
@@ -48,12 +52,29 @@ Library
     HOL.TypeVar
     HOL.Var
 
+executable hol-pkg
+  build-depends:
+    base >= 4.0 && < 5.0,
+    bytestring >= 0.9 && < 0.10,
+    containers >= 0.5 && < 0.6,
+    filepath >= 1.3 && < 1.4,
+    parsec >= 3.1 && < 3.2,
+    pretty >= 1.1 && < 1.2,
+    process >= 1.2 && < 1.3,
+    QuickCheck >= 2.4 && < 2.5,
+    text >= 0.11 && < 0.12,
+    transformers >= 0.3 && < 0.4
+  hs-source-dirs: src
+  ghc-options: -Wall -threaded "-with-rtsopts=-N" -rtsopts
+  main-is: Main.hs
+
 test-suite hol-test
   type: exitcode-stdio-1.0
   build-depends:
     base >= 4.0 && < 5.0,
     bytestring >= 0.9 && < 0.10,
     containers >= 0.5 && < 0.6,
+    filepath >= 1.3 && < 1.4,
     parsec >= 3.1 && < 3.2,
     pretty >= 1.1 && < 1.2,
     process >= 1.2 && < 1.3,
@@ -70,13 +91,15 @@ benchmark hol-profile
     base >= 4.0 && < 5.0,
     bytestring >= 0.9 && < 0.10,
     containers >= 0.5 && < 0.6,
+    filepath >= 1.3 && < 1.4,
     parsec >= 3.1 && < 3.2,
     pretty >= 1.1 && < 1.2,
     process >= 1.2 && < 1.3,
     text >= 0.11 && < 0.12,
     transformers >= 0.3 && < 0.4
   hs-source-dirs: src
   ghc-options:
+    -Wall
     -fprof-auto-top
     "-with-rtsopts=-p -s -h -i0.1"
   main-is: Profile.hs