[CakeML] Low-level Compiler Explorer

[Tan Yong Kiam]

Hi Lars,

If you are just after the raw AST, you could use something like fullEval  
 from explorer/pp/allPP.sml without loading the pretty printers   
(allIntermediates should work too). e.g.:

open HolKernel boolLib bossLib Parse
open cakeml_computeLib

fun fullEval p =
   let val asts = eval ``get_all_asts ^(p)``
        val elab = eval ``elab_all_asts ^(asts |> concl |> rhs)``
   in
      rhs(concl elab) |>rand
   end;

I think this requires standalone/ to be built.

In the pretty printing modules (e.g. explorer/pp/astPP.sml), the pretty  
printers are loaded using temp_add_user_printer calls (you can selectively  
disable if you want partial pretty printing by calling  
temp_remove_user_printer or just don't load them)

Finally, explorer/examples.sml should contain several examples covering  
the concrete syntax (some of the comments might be out of date).

On Wed, 23 Jul 2014 21:20:09 +0800, Ramana Kumar  
<Ramana.Kumar at cl.cam.ac.uk> wrote:

> On Wed, Jul 23, 2014 at 1:59 PM, Lars Hupel <hupel at in.tum.de> wrote:
>> Right, exactly. I used Lem to generate Isabelle theories from the
>> "semantics" folder in the "vml" repository. I made some preliminary
>> experiments and was already able to prove some trivial lemmas for
>> evaluation of arithmetic expressions with no toplevel definitions  
>> involved.
>
> Cool!
>
>> My long-term goal is to write a compiler from Isabelle code equations to
>> CakeML ASTs (via a deeply-embedded term rewriting fragment of HOL as an
>> intermediate step).
>> (This is obviously inspired from the ICFP'12 paper by Myreen and Owens.)
>
> Apart from the ICFP'12 paper, there is an updated JFP paper available  
> from the authors' websites (Magnus, Scott, we should link to >this from  
> cakeml.org too, no?).
>
> And for the ground truth, there is the code (maybe even with some  
> limited comments and README) in the "translator" folder of the >CakeML  
> code repository.
>
> I imagine both the code and the journal paper will be useful in porting  
> the translator to Isabelle. I'd be very interested to see your >progress  
> on this, and of course am happy to help where I can.
>
>>> Yes it is possible. At the moment the numerous ways I can think of  
>>> getting
>>> such output involve running HOL4. If you are not opposed to that, I can
>>> spell them out. (Also, if it's a one-off thing, you can just send me  
>>> the
>>> code and I can send back the AST.)
>>
>> Yes, I'd appreciate that.
>
> I guess one place to start could be  
> translator/ml_translator_demoScript.sml, and also the  
> ml_translatorLib.hol2deep function.
>
>> I'm already in the process of trying to build a repository snapshot of
>> HOL4 with Poly/ML, but so far am struggling with some linker issues.
>> I'll report back if I can't get it to work.
>
> The people on (and archives of) the hol-info mailing list (see  
> http://hol.sf.net) may be of help.
>
>>
>> Cheers
>> Lars
>



-- 
Regards
-Yong Kiam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20140723/88585ee8/attachment-0001.html>