search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
621 stars 140 forks source link

Theory namespaces #135

Open mn200 opened 10 years ago

mn200 commented 10 years ago

We currently have an entirely flat namespace for theories. These should be arranged in some sort of nested namespace kind of way to allow more control, mainly to prevent clashes.

(Needless to say, this may be hard to integrate with the (Moscow ML inspired) treatment of theories as SML structs.)

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

konrad-slind commented 10 years ago

A. I would use this kind of thing only to supply a tiny bit more organizational support, such as to prevent clashes.

B. Are you talking theories as on disk, or as what the manual calls theory segments? (Or something more semantic, ala OpenTheory?) If it's just those on disk, i.e., the contents of a structure, then can't the ML module system be used? For example, all the theories related to "num" could be made sub-structures of numLib. (Or is this not supported in MoscowML? I can't remember.)

Konrad.

On Wed, Nov 13, 2013 at 10:22 PM, Michael Norrish notifications@github.comwrote:

We currently have an entirely flat namespace for theories. These should be arranged in some sort of nested namespace kind of way to allow more control, mainly to prevent clashes.

(Needless to say, this may be hard to integrate with the (Moscow ML inspired) treatment of theories as SML structs.)

— Reply to this email directly or view it on GitHubhttps://github.com/mn200/HOL/issues/135 .

mn200 commented 10 years ago

I think the issue is how we'd map the namespaces to the files on disk. Also, SML doesn't allow you to extend a structure once it's defined. If I say that theory 1 should be in namespace Foo with name Bar, so that I can refer to it as Foo$Bar, I can't have structure Foo = struct structure Bar = ... end and then later come along with theory Baz that gets put into namespace Foo.