I'm trying to read the source of Isabelle even though I'm a beginner of Standard ML.
I arrive at the structure Unsynchronized
in src/Pure/Concurrent/unsynchronized.ML, which seems for the multi-thread programming. It includes
...
structure Unsynchronized: UNSYNCHRONIZED =
struct
datatype ref = datatype ref;
...
end;
ML_Name_Space.forget_val "ref";
ML_Name_Space.forget_type "ref";
and I cannot understand datatype ref = datatype ref;
. It's not in the usual form of datatype declaration.
As an experiment, in the REPL of poly/ML, I got
> datatype ref = datatype ref;
datatype 'a ref = ref of 'a
and so this declaration seems doing nothing or giving a type constructor synonym Unsynchronized.ref
= ref
(also Unsynchronized.ref
seems not being distinguished from ref
at all).
So my questions are:
- What kind of syntax structure does
datatype ref = datatype ref;
have? - What is the semantics (or meaning?) of
datatype ref = datatype ref;
? - What is the usage of such a type constructor synonym declaration? (Just for the clarity in semantics?)
Addendum: The functions
ML_Name_Space.forget_val
ML_Name_Space.forget_type
are defined in src/Pure/ML/ml_name_space.ML as
val forget_val = PolyML.Compiler.forgetValue;
val forget_type = PolyML.Compiler.forgetType;
and so after loading (?) unsynchronized.ML
, the original type constructor ref
is not available anymore. Probably, this answers Q.3 partially.
means that we create a synonym for the SML builtin type ref. It has the same constructor (
ref
) as the original one.The commit does not provide any motivation why this was introduced, but I would not be surprised to hear that this comes from
(i) supporting the compilers PolyML and Moscow ML.
(ii) putting ref into a proper module for more clarity, making it possible to call other datypes
ref
(there is one insrc/Pure/facts.ML
)