ML documentation

[maxhaslbeck]

Peter comments:

 -- if only the Isabelle sources themselves would follow these ;)
    Here a few general structuring guidelines, that Isabelle seems to
adhere to:
  * No global functions or types. Everything declared by your
implementation goes into a structure with a speaking name. The
structure comes with an explicit signature. Structure_Name uses
underscores and first letter of word capitalized, signature name is
all-uppercase version of structure name.

e.g.

signature RAW_SIMPLIFIER =
sig ... end

structure Raw_Simplifier: RAW_SIMPLIFIER =
struct ... end

the signature only lists the functions that are meant to be used
publicly: care has to be taken to not unnecessarily bar access from
functions that might be required later, e.g., when building new tools
on top of this tool.
In Isabelle: Only very rarely is there some very brief documentation in
the signature. Sometimes, you might find some documentation in the
definition inside the structure. Lot's of documentation is decoupled
from the source-code, and maintained as latex in doc/ directory.

For this style-guide: ? My opinion: put documentation to be read by
user into signature. Do we have doxygen or something similar for
Isabelle-ML?


ML "Do Nots"

* declare global types or functions. Wrap your stuff in structures.
Perhaps add signatures when it has become "stable".

  BAD: ML {* fun my_fun x = ...    *}
  BETTER: structure My_Struct = struct fun my_fun x =...
  BEST: structure My_Struct: MY_STRUCT = struct ...

* open signatures, except perhaps very locally.

  Examples:

  structure Foo = struct
    open Conv
    ...

  tempting, but usually not OK

  Better:
  structure Foo = struct

    local open Conv in
      val my_conv = arg_conv (arg_conv (...)..)
    end

[wimmers]

I think these are all good.
I think the problem remains that the stub there just needs to be filled?

[kappelmann]

I do not have enough ML knowledge to contribute in a reasonable way, but my main question would be if we want to just put this in there already or wait for a complete set of rules we want for ML code? I would be fine with the former and just iterate and extend when needed.

[kappelmann]

Here is some feedback about ML standards as stated in #10

The 0th chapter of "The Isabelle/Isar Implementation" contains quite a number of style guidelines for the Isabelle/ML programming. My personal opinion is that the ML-part of the guidelines should merely reference the aforementioned document. Alternatively, it may be plausible to merely copy all matters concerned with style from "The Isabelle/Isar Implementation".

[kappelmann]

Some further discussion about invariants can be found here