[CakeML-dev] Translation failure

[Magnus Myreen]

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
>