`Theory` syntax

[digama0]

I would like to implement a new syntax for the new_theory command and the prelude. This will ensure more consistent use of the header and also make it more introspectable by HOL tooling like IDEs. Proposal:

(*
  Module documentation
*)
Import fooLib barTheory
Import[open] bazTheory
Theory bla

Definition foo:
  foo = T
End

is equivalent to

(*
  Module documentation
*)
local open fooLib barTheory in end
open bazTheory
val _ = new_theory "bla";

Definition foo:
  foo = T
End

val _ = export_theory ();

Some points of interest:

• I'd like to remove the Theory suffix from the theory imports, since HOL itself tends to refer to theories without this suffix in e.g. qualified constant names, but I don't think it can be implemented as long as quote-filter is a preprocessor which runs without any filesystem context (unless we change the structure name itself to drop the Theory suffix).
• It is mandatory that there be no non-whitespace text between the beginning of the file and the Theory command, except for Import declarations. In particular, that means that all opens have to happen at the beginning of the file, and there cannot be additional commands before new_theory. This happens occasionally (e.g. temp_delsimps is often before new_theory), but it doesn't seem to make a difference.
• For now, holdep will continue to work as it does currently, but I would like to transition this to a warning and deprecate mid-file holdeps (e.g. using qualified identifiers for unimported files).
• The export_theory at the end of the file is implicit when using Theory syntax.

[xrchz]

I have a feeling this would make HOL exceptionally more welcoming/non-intimidating to newcomers.

[myreen]

This sounds great and I support it.

Here are a few requests from my side:

• The new syntax should also generate a set_grammar_ancestry by default. Note that the order is very important and often does not include all of the opened theory files. HOL scripts written with good style should have a set_grammar_ancestry. In the example below I mark files to exclude with [ignore_grammar].
• I would like the common case to be short. In particular opening a bunch of theories should be concise, while opening theories inside a local in ... end is less common and should be an opt out. In the example, below I mark the local in ... end opens with [no_bind] because they produce no ML-level bindings.
• I like the idea of dropping Theory suffixes. How about having different lines for theory files and other files? In the example below I write Import for theories and Use for all others.

(*
  Module documentation
*)
Import[no_bind] bar
Import[ignore_grammar] other
Import baz arithmetic list
Use fooLib listSyntax
Theory bla

Definition foo_def:
  foo = T
End

Would expand to:

(*
  Module documentation
*)
local in open barTheory end;
open otherTheory;
open bazTheory; open arithmeticTheory; open listTheory;
open fooLib; open listSyntax;
val _ = new_theory "bla"; val _ = set_grammar_ancentry ["bar","baz","arithmetic","list"];

Definition foo_def:
  foo = T
End

val _ = export_theory();

I intentionally made each open a top-level declaration of its own because I worry that multiple simultaneous opens can lead to some unpredictability.

[mn200]

I agree with Magnus about both the need to make the common case easy and to include support for set_grammar_ancestry.

I’d also prefer to have the Theory bla as the first line rather than buried.

I don’t mind dropping the Theory suffix though I wonder a bit about the way users will still need to remember it when they come to refer to the theorems (on the nobind imports).

Finally, is it going to be easy to have a version that works for pre-bossLib files?

[digama0]

I don’t mind dropping the Theory suffix though I wonder a bit about the way users will still need to remember it when they come to refer to the theorems (on the nobind imports).

I think we should drop the suffix on the structure name itself. But I think that can be done independently of this proposal, it's a pretty large breaking change.

[mn200]

Agreed that it can be deferred. It might at least be easy to implement (outside of Holmake) : s/(ident)Theory/\1/g

[dnezam]

To my understanding, open and thus by extension Import as suggested by @myreen would essentially "import" everything, i.e. instead of baz.foo, foo would be accessible directly via foo. I find that slightly disturbing, and it did lead to bit of confusion when I was working on the correctness proof for the Dafny compiler.

Is there anything that would speak against having separate syntax for the following:

• Import everything in a way that you don't need to mention where it is coming from (for example Import[all])
• Imports where we require mentioning where it comes from (for example Import)
• Imports where we require mentioning where it comes from, except for a subset of definitions which may be optionally be renamed. At the moment, I do such renaming myself (see for example exp in the Dafny correctness proof sketch).

[mn200]

I think you are conflating two namespace levels. This proposal is more about the SML level (the names visible in tactics for example). The renaming you did in your example file was to do with the HOL namespaces. Of course a more powerful syntax could do both!

[myreen]

Finally, is it going to be easy to have a version that works for pre-bossLib files?

Could one specify that with something like:

Theory[bare] pair

[digama0]

Notes from HOL meeting:

Theory thy[bare]
(*
  Module documentation
*)
Ancestors
  long_name[alias LN, qualified, ignore_grammar]
  other[ignore_grammar]
  baz
  arithmetic
  list
Libs
  preamble
  Theory
  fooLib
  listSyntax

val _ = bazTheory.bla;
Definition foo_def:
  foo = T
End