[CakeML] Basis library

[Ramana Kumar]

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/5a134515/attachment.html>