[CakeML-dev] Translation failure

[Yong Kiam]

The normal version fails too due to some strange combination of mutual
recursion + lem-exported definition (missing termination proof) + side
conditions.
(I think I've seen definitions that satisfy the first and last one go
through translation before, so it might be a lookup problem for the
termination proof)

I gave up trying to fix it, so I'm just giving a more translatable
alternative for it. (there needs to be an alternative definition anyway
because one of the side conditions is unprovable)

On Sat, Apr 8, 2017 at 12:34 PM, Scott Owens <S.A.Owens at kent.ac.uk> wrote:

> Yeah. Some kind of magic in the inferProgScript makes the PMATCH versions
> from the normal versions. I can try it with the normal versions. I haven’t
> yet had a chance to look at PMATCH.
>
> Scott
>
> > On 2017/04/08, at 17:30, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> >
> > The translation of PMATCH is fragile. Do you have a version of these
> > functions with normal case statements? -- Magnus
> >
> > On 8 April 2017 at 18:28, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> >> No, they are equations. Do you have to do something special for mutual
> recursion? This is the definition:
> >>
> >>   |- (∀t.
> >>      inf_type_to_string t =
> >>      PMATCH t
> >>        [PMATCH_ROW (λ_0. Infer_Tuvar _0) (λ_0. T)
> >>           (λ_0. "<unification variable>");
> >>         PMATCH_ROW (λn. Infer_Tvar_db n) (λn. T) (λn. toString n);
> >>         PMATCH_ROW (λ(t1,t2). Infer_Tapp [t1; t2] TC_fn) (λ(t1,t2). T)
> >>           (λ(t1,t2).
> >>              STRCAT "("
> >>                (STRCAT (inf_type_to_string t1)
> >>                   (STRCAT "->" (STRCAT (inf_type_to_string t2) ")"))));
> >>         PMATCH_ROW (λ_0. Infer_Tapp _0 TC_fn) (λ_0. T)
> >>           (λ_0. "<bad function type>");
> >>         PMATCH_ROW (λts. Infer_Tapp ts TC_tup) (λts. T)
> >>           (λts. STRCAT "(" (STRCAT (inf_types_to_string ts) ")"));
> >>         PMATCH_ROW (λtc1. Infer_Tapp [] tc1) (λtc1. T)
> >>           (λtc1. tc_to_string tc1);
> >>         PMATCH_ROW (λ(ts,tc1). Infer_Tapp ts tc1) (λ(ts,tc1). T)
> >>           (λ(ts,tc1).
> >>              STRCAT "("
> >>                (STRCAT (inf_types_to_string ts)
> >>                   (STRCAT ") " (tc_to_string tc1))))]) ∧
> >>   ∀ts.
> >>     inf_types_to_string ts =
> >>     PMATCH ts
> >>       [PMATCH_ROW (λ_. []) (λ_. T) (λ_. "");
> >>        PMATCH_ROW (λt. [t]) (λt. T) (λt. inf_type_to_string t);
> >>        PMATCH_ROW (λ(t,ts). t::ts) (λ(t,ts). T)
> >>          (λ(t,ts).
> >>             STRCAT (inf_type_to_string t)
> >>               (STRCAT ", " (inf_types_to_string ts)))]:
> >>
> >>
> >> Scott
> >>
> >>> On 2017/04/08, at 17:18, Magnus Myreen <magnus.myreen at gmail.com>
> wrote:
> >>>
> >>> Do you have a function that returns T? This might be cause by that,
> >>> because some simplification might have turned the function definition
> >>> `foo n = T` into `foo n` and the translator expects functions to be
> >>> defined using equations.
> >>>
> >>> I debug the translator by starting the HOL session fresh in the file
> >>> you want to work in, then do all the opens at the top, then copy in
> >>> the code of the translator (this overshadows the opened
> >>> ml_translatorLib), then just feed file you want to debug in as usual.
> >>>
> >>> Cheers,
> >>> Magnus
> >>>
> >>> On 8 April 2017 at 18:12, Scott Owens <S.A.Owens at kent.ac.uk> wrote:
> >>>> I’m seeing the translator fail on a pretty simple function that
> coverts inferencer types to strings in inferProgScript.sml on the
> type-error-loc branch. The error message is unhelpful.
> >>>>
> >>>> Improved induction theorem: inf_type_to_string_ind
> >>>> Failed translation: inf_type_to_string, inf_types_to_string
> >>>> Exception- HOL_ERR {message = "not an \"=\"", origin_function =
> "dest_eq(_ty)", origin_structure = "boolSyntax"} raised
> >>>>
> >>>> Does anyone have any ideas what the problem might be, or tips on
> debugging translator failures?
> >>>>
> >>>> Scott
> >>>> _______________________________________________
> >>>> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20170409/e843f374/attachment-0001.html>