[CakeML-Dev] reusing a CF specification
Armaël Guéneau
armael.gueneau at ens-lyon.fr
Fri Oct 14 12:23:33 UTC 2016
Ah! That means no value could be found in the environment for Long
"Word8" "fromInt".
Something must be wrong with how the states from ml_progLib are handled.
(the environment you start from is the one bundled in the closure that
is fetched by fetch_v in the goal).
On 14/10/2016 12:14, Michael.Norrish at data61.csiro.au wrote:
> xapp_prepare_goal turns the goal into F :-|
>
> Michael
>
> On 14/10/16, 21:02, "Armaël Guéneau" <armael.gueneau at ens-lyon.fr> wrote:
>
> Right. Humm, I don't see an obvious reason why it wouldn't work.
>
> To debug, run xapp_prepare_goal; the goal becomes something of the form:
>
> app p word8_fromint_v ...
>
> then xapp will search the environment for a theorem of the form ``(Arrow
> _ _) _ word8_from_int_v``
>
>
> On 14/10/2016 11:46, Michael.Norrish at data61.csiro.au wrote:
> > 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
> >
> >
> >
> >
>
>
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
More information about the Developers
mailing list