<div dir="ltr">What about the source HOL functions for the matcher? (If that's how the AST was obtained.)<div><br></div><div>Also, I haven't been able to (on a cursory effort) get a match, probably because I don't know</div><div>the expected syntax of a call to this grep. Any clues?</div><div><br></div><div>Thanks,</div><div>Konrad.</div><div><br></div><div><div><br></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Mar 12, 2017 at 12:32 PM, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Konrad,<br>
<br>
The sources only exist in AST format at the moment. At some point, we<br>
had a way of pretty printing AST into concrete syntax, but I'm not<br>
sure where that machinery lives nowadays or whether it produces<br>
readable concrete syntax for large programs.<br>
<br>
I believe the full AST for the bootstrapped compiler is in the<br>
constant called `entire_program` which is defined in the following<br>
script:<br>
<br>
<a href="https://github.com/CakeML/cakeml/blob/master/compiler/bootstrap/translation/compiler_x64ProgScript.sml#L176" rel="noreferrer" target="_blank">https://github.com/CakeML/<wbr>cakeml/blob/master/compiler/<wbr>bootstrap/translation/<wbr>compiler_x64ProgScript.sml#<wbr>L176</a><br>
<br>
Unfortunately, this term is not shown in the script and it's not easy<br>
to explore interactively either.<br>
<br>
Cheers,<br>
Magnus<br>
<div class="HOEnZb"><div class="h5"><br>
On 12 March 2017 at 18:22, Konrad Slind <<a href="mailto:konrad.slind@gmail.com">konrad.slind@gmail.com</a>> wrote:<br>
> Nice! Is it possible to see the source from which this is generated?<br>
><br>
> Thanks,<br>
> Konrad.<br>
><br>
><br>
> On Fri, Mar 10, 2017 at 12:31 AM, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>><br>
> wrote:<br>
>><br>
>> I've also put up the .S file for a version of grep in CakeML:<br>
>> <a href="https://cakeml.org/grep-b75523fe.tar.gz" rel="noreferrer" target="_blank">https://cakeml.org/grep-<wbr>b75523fe.tar.gz</a><br>
>><br>
>> You can compile it the same way as the others:<br>
>> gcc -o cake_grep basis_ffi.c grep.S<br>
>><br>
>> It works, but it's pretty slow compared to the GNU version in C... and<br>
>> of course has fewer features too... apart from the theorem (actually,<br>
>> I still need to produce the theorem about the machine code, as opposed<br>
>> to just about the source code).<br>
>><br>
>> On 5 March 2017 at 11:26, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk">S.A.Owens@kent.ac.uk</a>> wrote:<br>
>> > Thanks for this. I tried it out on the quicksort algorithm that I’ve<br>
>> > been working on verifying. It runs about 1/3 faster than with the more naive<br>
>> > partitioning algorithm from our benchmarks. It also takes about 10 seconds<br>
>> > to compile, which isn’t great, but not shameful either. With a little more<br>
>> > packaging, we could make this a beta release of v2 and put it on the web<br>
>> > page.<br>
>> ><br>
>> > Scott<br>
>> ><br>
>> >> On 2017/03/04, at 23:12, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk">Ramana.Kumar@cl.cam.ac.uk</a>><br>
>> >> wrote:<br>
>> >><br>
>> >> Hi CakeML developers,<br>
>> >><br>
>> >> I've put the result you could obtain by running the compiler bootstrap<br>
>> >> on a recent commit (389d340f) online here:<br>
>> >> <a href="https://cakeml.org/cake-389d340f.S.tar.gz" rel="noreferrer" target="_blank">https://cakeml.org/cake-<wbr>389d340f.S.tar.gz</a>, so you can try it without<br>
>> >> having to build it if you want.<br>
>> >><br>
>> >> This version contains basis library modules including FileIO (actually<br>
>> >> only read-only) and CharIO, whose contents you can glean by looking at<br>
>> >> basis/mlfileioProgScript.sml and basis/mlcharioProgScript.sml etc.<br>
>> >><br>
>> >> Here's an example of how to use it. You need the basis_ffi.c file<br>
>> >> available from basis/basis_ffi.c in the repo (preferably the one at<br>
>> >> commit 389d340f, but I think it hasn't changed on master since then).<br>
>> >><br>
>> >> $ tar -xvzf cake-389d340f.S.tar.gz<br>
>> >> $ gcc -o cake basis_ffi.c cake-389d340f.S<br>
>> >> # Example: a CakeML program that prints the first char in the .S file<br>
>> >> $ ./cake > result.S<br>
>> >> val f = FileIO.openIn("cake-389d340f.<wbr>S");<br>
>> >> val SOME c = FileIO.fgetc f;<br>
>> >> CharIO.write c;<br>
>> >> <CTRL-D><br>
>> >> $ gcc -o result basis_ffi.c result.S<br>
>> >> $ ./result<br>
>> >> # prints '#'<br>
>> >><br>
>> >> Have fun!<br>
>> >> Ramana<br>
>> >><br>
>> >> ______________________________<wbr>_________________<br>
>> >> Developers mailing list<br>
>> >> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>> >> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
>> ><br>
>> > ______________________________<wbr>_________________<br>
>> > Developers mailing list<br>
>> > <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>> > <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
>><br>
>> ______________________________<wbr>_________________<br>
>> Developers mailing list<br>
>> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
><br>
><br>
> ______________________________<wbr>_________________<br>
> Developers mailing list<br>
> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
><br>
</div></div></blockquote></div><br></div>