From e4293c0f755db29904a35e28b85978dc4353e6ec Mon Sep 17 00:00:00 2001
From: John Harrison <jargh@amazon.com>
Date: Mon, 23 Sep 2024 23:47:18 -0700
Subject: [PATCH] Enable more descriptive names for quantifiers and logical
 constants

The new functions "set_verbose_symbols" and "unset_verbose_symbols"
enable and disable, respectively, more verbose and descriptive names
for some logical symbols; these are now enabled by default:

        F -> false
        T -> true
        ! -> forall
        ? -> exists
        ?! -> existsunique

This is all done via interface maps. Not only is the underlying term
structure unchanged (the "actual" names are the symbolic ones) but
also the original syntax is accepted as an alternative:

  # `exists x. x = 1` = `?x. x = 1`;;
  val it : bool = true
---
 Help/set_verbose_symbols.hlp   | 61 ++++++++++++++++++++++++++++++++++
 Help/unset_verbose_symbols.hlp | 38 +++++++++++++++++++++
 bool.ml                        | 20 +++++++++++
 3 files changed, 119 insertions(+)
 create mode 100644 Help/set_verbose_symbols.hlp
 create mode 100644 Help/unset_verbose_symbols.hlp

diff --git a/Help/set_verbose_symbols.hlp b/Help/set_verbose_symbols.hlp
new file mode 100644
index 00000000..f7884a20
--- /dev/null
+++ b/Help/set_verbose_symbols.hlp
@@ -0,0 +1,61 @@
+\DOC set_verbose_symbols
+
+\TYPE {set_verbose_symbols : unit -> unit}
+
+\SYNOPSIS
+Enables more verbose descriptive names for quantifiers and logical constants
+
+\DESCRIBE
+A call to {set_verbose_symbols()} enables a more verbose syntax for the logical
+quantifiers and constants. These are all just interface mappings, the
+underlying constant names in the abstract syntax of the logic being unchanged.
+But the more descriptive names are applied by default when printing and
+are accepted when parsing terms as synonyms of the symbolic names. The new
+names are:
+
+\begin{{itemize}}
+
+\item The universal quantifier `{!}' is now parsed and printed as `{forall}'
+
+\item The existential quantifier `{?}' is now parsed and printed as `{exists}'
+
+\item The exists-unique quantifier `{?!}' is now parsed and printed as
+`{existsunique}'
+
+\item The logical constant `{T}' is now parsed and printed as `{true}'
+
+\item The logical constant `{F}' is now parsed and printed as `{false}'
+
+\end{{itemize}}
+
+The effect can be reverse by a call to the dual function
+{unset_verbose_symbols()}.
+
+\EXAMPLE
+Notice how the printing of theorems changes from using the symbolic names for
+quantifiers
+{
+  # unset_verbose_symbols();;
+  val it : unit = ()
+  # num_Axiom;;
+  val it : thm = |- !e f. ?!fn. fn 0 = e /\ (!n. fn (SUC n) = f (fn n) n)
+}
+\noindent to the more verbose and descriptive names:
+{
+  # set_verbose_symbols();;
+  val it : unit = ()
+  # num_Axiom;;
+  val it : thm =
+    |- forall e f.
+           existsunique fn. fn 0 = e /\ (forall n. fn (SUC n) = f (fn n) n)
+}
+
+\FAILURE
+Only fails if some of the names have already been used for incompatible
+constants.
+
+\SEEALSO
+overload_interface, override_interface, remove_interface,
+the_interface, unset_verbose_symbols.
+
+\ENDDOC
diff --git a/Help/unset_verbose_symbols.hlp b/Help/unset_verbose_symbols.hlp
new file mode 100644
index 00000000..9622ec0a
--- /dev/null
+++ b/Help/unset_verbose_symbols.hlp
@@ -0,0 +1,38 @@
+\DOC unset_verbose_symbols
+
+\TYPE {unset_verbose_symbols : unit -> unit}
+
+\SYNOPSIS
+Disables more verbose descriptive names for quantifiers and logical constants
+
+\DESCRIBE
+A call to {unset_verbose_symbols()} disables the more verbose syntax for the
+logical quantifiers and constants that is set up by default and can be
+explicitly enabled by the dual function {set_verbose_symbols()}.
+
+\EXAMPLE
+Notice how the printing of theorems changes from using the verbose descriptive
+names for quantifiers by default:
+{
+  # num_Axiom;;
+  val it : thm =
+    |- forall e f.
+           existsunique fn. fn 0 = e /\ (forall n. fn (SUC n) = f (fn n) n)
+}
+\noindent to using the more concise symbolic names
+{
+  # unset_verbose_symbols();;
+  val it : unit = ()
+  # num_Axiom;;
+  val it : thm = |- !e f. ?!fn. fn 0 = e /\ (!n. fn (SUC n) = f (fn n) n)
+}
+
+\FAILURE
+Only fails if some of the names have already been used for incompatible
+constants.
+
+\SEEALSO
+overload_interface, override_interface, remove_interface, set_verbose_symbols,
+the_interface.
+
+\ENDDOC
diff --git a/bool.ml b/bool.ml
index d21bb92e..8f8e27ca 100644
--- a/bool.ml
+++ b/bool.ml
@@ -482,3 +482,23 @@ let EXISTENCE =
         let ty = snd(dest_var(bndvar abs)) in
         MP (PINST [ty,aty] [abs,P] pth) th
     with Failure _ -> failwith "EXISTENCE";;
+
+(* ------------------------------------------------------------------------- *)
+(* Optionally select more verbose syntax for quantifiers, as well            *)
+(* as the logical constants T (true) and F (false). Enabled by default.      *)
+(* ------------------------------------------------------------------------- *)
+
+let set_verbose_symbols() =
+ (do_list parse_as_binder ["forall"; "exists"; "existsunique"];
+  override_interface("true",`T`);
+  override_interface("false",`F`);
+  override_interface("forall",`(!):(A->bool)->bool`);
+  override_interface("exists",`(?):(A->bool)->bool`);
+  override_interface("existsunique",`(?!):(A->bool)->bool`));;
+
+let unset_verbose_symbols() =
+ (do_list unparse_as_binder ["forall"; "exists"; "existsunique"];
+  do_list remove_interface
+    ["true"; "false"; "forall"; "exists"; "existsunique"]);;
+
+set_verbose_symbols();;