Add README

Author: konrad-slind

examples/acl2/hol-to-acl2/README.md

@@ -0,0 +1,25 @@
+# HOL to ACL2 Translation
+
+This directory provides an automated translation from a subset of HOL
+to ACL(zfc), a formalization of Set Theory in the ACL2 system. Details
+of ACL2(zfc) can be found at
+```
+  https://github.com/acl2/acl2/tree/master/books/projects/set-theory
+```
+
+The modelling of the HOL logic in ACL2(zfc) is analogous to the
+"Pitts" semantics of the HOL4 Logic Manual. It can be found at
+```
+https://github.com/acl2/acl2/tree/master/books/projects/hol-in-acl2/acl2
+```
+
+The translator itself can be seen in action in the `examples` directory.
+Typing
+```
+  <holdir>/bin/Holmake cleanAll
+  <holdir>/bin/Holmake
+```
+will create, for each `<x>Script.sml`, a corresponding file
+`<x>.defhol`, comprising a list of so-called `defhol forms` which can
+then be used in ACL2(zfc) to "recreate" the selected definitions,
+theorems, and goals coming from the `<x>` formalization in HOL4.

examples/acl2/hol-to-acl2/src/HOL_to_ACL2.sig

@@ -2,11 +2,7 @@ signature HOL_to_ACL2 =
 sig
   include Abbrev
 
-  datatype t =
-      Cons of t * t
-    | Integer of int
-    | String of string
-    | Symbol of string
+  datatype t = datatype HOLsexp_dtype.t
 
   val basis_defs : thm list
   val builtin_const_map : (term * string) list
@@ -35,5 +31,4 @@ sig
      {fns: term list,
       defs: (term list * ((term * term list) * term)) list}
 
-
 end

examples/acl2/hol-to-acl2/src/HOL_to_ACL2.sml

@@ -366,14 +366,14 @@ fun pp_sexp t =
      | Integer i => add_string (if i < 0 then "-" ^ Int.toString (~i) else Int.toString i)
      | Cons _ =>
         let val (els, last) = break_sexp_list t
-         in block INCONSISTENT 1 (
-              add_string "(" ::
-              pr_list pp_sexp [add_break(1,0)] els @
-              (case last
-                of Symbol "nil" => [add_string ")"]
-                 | t => [add_string " .", add_break(1,0), printer t, add_string ")"])
-            )
-         end
+        in block INCONSISTENT 1 (
+             add_string "(" ::
+             pr_list pp_sexp [add_break(1,0)] els @
+             (case last
+               of Symbol "nil" => [add_string ")"]
+                | t => [add_string " .", add_break(1,0), pp_sexp t, add_string ")"])
+           )
+        end
  end
 
 (*---------------------------------------------------------------------------*)