[CakeML-dev] Bootstrapped compiler preview

[Ramana Kumar]

Hi Konrad,

The source code for the grep program is in the file
characteristic/examples/grepProgScript.sml.

The HOL function that does the matching is here:
https://github.com/CakeML/cakeml/blob/master/characteristic/examples/grepProgScript.sml#L213

The main program, which is parsed to AST from source syntax inside the
logic, is here:
https://github.com/CakeML/cakeml/blob/master/characteristic/examples/grepProgScript.sml#L599
(it refers to some other functions that are either parsed or defined
in that file.)

The regexp parser, which is in
$HOLDIR/examples/formal-languages/regular/regexp_parserScript.sml,
currently supports concatenation, alternation (|), repetition (*),
digit set (\d), anything (.), and limited (no ranges, complements, or
escapes) charsets ([...]). The usage for cake_grep is

cake_grep <regexp_string> <filename> <filename>...

The regexep is applied, as is, to the whole of each line in each file
(not including the newline character). We might want to change it to
automatically surround it with ".*"s to allow matches anywhere inside
lines.

The intended semantics (against which the program is verified) is
defined in grepProg also:
https://github.com/CakeML/cakeml/blob/master/characteristic/examples/grepProgScript.sml#L630
(that function computes the string to be printed on stdout).

Cheers,
Ramana

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