[CakeML-Dev] reusing a CF specification

[Michael.Norrish at data61.csiro.au]

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
    >      
    >      
    >      
    >