[CakeML] Re-use CakeML's code to build toy languages?

[Chun Tian (binghe)]

Hi,

CakeML is really a great project in which I expect myself to learn almost
everything about programming languages (and HOL theorem prover).

I see the whole work consists of many small modules (as HOL theories) and
also depends on HOL's example theories "formal-language" and
"l3-machine-code"). I think most of these modules must be general
utilities, while the rest of them concern about the CakeML language itself.

Here is my question: if I want to build at least an interpreter for a toy
(not even turing complete) programming language which currently can be seen
as a strict sub-set of CakeML (but later I may add object-oriented features
to it), and if I want to benefit from existing framework and code of
CakeML, *which modules should I look into*, to achieve the following goals:

1. define the grammar for this language, and get ASTs from any input as
mini programs of the toy language.
2. writing code to do some basic semantic analysis (e.g. type checking,
detection of undefined/uninitialized variables).
3. static analysis: taking a mini program as input, output a theorem saying
something like "this program is semantically correct".
4. actually "run" any mini program in HOL interactive environment.

Above plan could be one of my exam project (in which other students use
Java and ANTLR to do the same thing). I hope in this way I could deeply
understand the design and structure of CakeML better, maybe one day I can
also make some useful contributions.

Best Regards,

-- 
Chun Tian (binghe)
University of Bologna (Italy)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170428/4f871571/attachment.html>