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