[CakeML] Basis library

[Ramana Kumar]

Hi again Lars,

Here's another simpler method to obtain the names of the basis library
functions. (Magnus suggested it to me off list.) It retrieves the names,
which are suggestive, but not the types (which would be even more so).

I put the result of running the following code at
https://cakeml.org/basis-names.txt for now. (But don't expect that link to
be kept up to date, or even alive.)

val _ = translation_extends"basisProg"
val () = Globals.max_print_depth := 20;

val get_dec_names_def = Define`
  get_dec_names (Dlet _ p _) = pat_bindings p [] ∧
  get_dec_names (Dletrec _ funs) = MAP FST funs ∧
  get_dec_names _ = []`;

val get_top_names_def = Define`
  get_top_names (Tdec d) = get_dec_names d ∧
  get_top_names (Tmod mn _ ds) = MAP ((++) (mn++".")) (FLAT (MAP
get_dec_names ds))`;

val get_prog_names_def = Define`
  get_prog_names prog = FLAT (MAP get_top_names prog)`;

val prog_tm =
  get_ml_prog_state() |> remove_snocs |> clean_state |> get_thm
  |> concl |> strip_comb |> #2 |> el 3

val names =
  EVAL``get_prog_names ^prog_tm`` |> rconc
  |> listSyntax.dest_list |> #1
  |> map stringSyntax.fromHOLstring

app (fn x => (print x; print"\n")) names

Cheers,
Ramana

On 20 July 2017 at 18:55, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:

> Hi Lars,
>
> I don't think there's a list of the basis contents, and it's not trivial
> (off the top of my head) to generate one unfortunately.
> Here's one way you could try: print the entire basis program in concrete
> syntax then try (maybe using some existing SML processing tools?) to get
> the function names from that.
> You can get the basis program in a hacky way with something like this:
>
> open preamble basisProgTheory ml_translatorLib ml_progLib astPP
> val _ = translation_extends"basisProg"
> val () = astPP.enable_astPP();
> val () = Globals.max_print_depth := 20;
> val prog_tm =
>   get_ml_prog_state() |> remove_snocs |> clean_state |> get_thm
>   |> concl |> strip_comb |> #2 |> el 3
>
> There is no 'a -> string function. I know there is Int.toString, but for
> most other types you need to define your own show functions.
>
> Cheers,
> Ramana
>
>
> On 20 July 2017 at 18:41, Lars Hupel <hupel at in.tum.de> wrote:
>
>> Dear CakeML developers,
>>
>> is there any list of predefined functions/modules in CakeML? I found
>> some using trial and error, but I'm having a hard time reading the HOL4
>> scripts in 'basis/'.
>>
>> And on the off chance: Is there a function 'a -> string? Otherwise I'll
>> have to resort to generating "show" functions myself.
>>
>> Cheers
>> Lars
>>
>> _______________________________________________
>> Users mailing list
>> Users at cakeml.org
>> https://lists.cakeml.org/listinfo/users
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20170720/27cb26fb/attachment.html>