[CakeML-Dev] reusing a CF specification
Michael.Norrish at data61.csiro.au
Michael.Norrish at data61.csiro.au
Fri Oct 14 09:46:43 UTC 2016
I just copied the code out of basisProg; that has
- -
val _ = ml_prog_update (open_module "Word8");
val _ = append_dec ``Dtabbrev [] "word" (Tapp [] TC_word8)``;
val _ = trans "fromInt" `n2w:num->word8`
val _ = trans "toInt" `w2n:word8->num`
val _ = ml_prog_update (close_module NONE);
- -
Michael
On 14/10/16, 20:44, "Armaël Guéneau" <armael.gueneau at ens-lyon.fr> wrote:
Did you store the specification you proved?
On 14/10/2016 11:39, Michael.Norrish at data61.csiro.au wrote:
> I’ve got as far as something like
>
> 0. NUM n nv
> 1. n + 1 < LENGTH a
> ------------------------------------
> cf_app p (Var (Long "Word8" "fromInt")) [Lit (IntLit 0)] (…)
> (W8ARRAY av a) (POSTv zv. &WORD 0w zv)
>
>
> where Word8.fromInt has been declared and characterized by code identical to that in basisProgTheory, but I don’t know how to use the proved specification: xapp throws an exception.
>
> What am I doing wrong?
>
> Many thanks,
> Michael.
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
More information about the Developers
mailing list