[CakeML-dev] Translation failure

[Scott Owens]

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