<div dir="ltr">The normal version fails too due to some strange combination of mutual recursion + lem-exported definition (missing termination proof) + side conditions.<div>(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)<div><br></div><div>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)</div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Apr 8, 2017 at 12:34 PM, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">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.<br>
<span class="HOEnZb"><font color="#888888"><br>
Scott<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
> On 2017/04/08, at 17:30, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
><br>
> The translation of PMATCH is fragile. Do you have a version of these<br>
> functions with normal case statements? -- Magnus<br>
><br>
> On 8 April 2017 at 18:28, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk">S.A.Owens@kent.ac.uk</a>> wrote:<br>
>> No, they are equations. Do you have to do something special for mutual recursion? This is the definition:<br>
>><br>
>> |- (∀t.<br>
>> inf_type_to_string t =<br>
>> PMATCH t<br>
>> [PMATCH_ROW (λ_0. Infer_Tuvar _0) (λ_0. T)<br>
>> (λ_0. "<unification variable>");<br>
>> PMATCH_ROW (λn. Infer_Tvar_db n) (λn. T) (λn. toString n);<br>
>> PMATCH_ROW (λ(t1,t2). Infer_Tapp [t1; t2] TC_fn) (λ(t1,t2). T)<br>
>> (λ(t1,t2).<br>
>> STRCAT "("<br>
>> (STRCAT (inf_type_to_string t1)<br>
>> (STRCAT "->" (STRCAT (inf_type_to_string t2) ")"))));<br>
>> PMATCH_ROW (λ_0. Infer_Tapp _0 TC_fn) (λ_0. T)<br>
>> (λ_0. "<bad function type>");<br>
>> PMATCH_ROW (λts. Infer_Tapp ts TC_tup) (λts. T)<br>
>> (λts. STRCAT "(" (STRCAT (inf_types_to_string ts) ")"));<br>
>> PMATCH_ROW (λtc1. Infer_Tapp [] tc1) (λtc1. T)<br>
>> (λtc1. tc_to_string tc1);<br>
>> PMATCH_ROW (λ(ts,tc1). Infer_Tapp ts tc1) (λ(ts,tc1). T)<br>
>> (λ(ts,tc1).<br>
>> STRCAT "("<br>
>> (STRCAT (inf_types_to_string ts)<br>
>> (STRCAT ") " (tc_to_string tc1))))]) ∧<br>
>> ∀ts.<br>
>> inf_types_to_string ts =<br>
>> PMATCH ts<br>
>> [PMATCH_ROW (λ_. []) (λ_. T) (λ_. "");<br>
>> PMATCH_ROW (λt. [t]) (λt. T) (λt. inf_type_to_string t);<br>
>> PMATCH_ROW (λ(t,ts). t::ts) (λ(t,ts). T)<br>
>> (λ(t,ts).<br>
>> STRCAT (inf_type_to_string t)<br>
>> (STRCAT ", " (inf_types_to_string ts)))]:<br>
>><br>
>><br>
>> Scott<br>
>><br>
>>> On 2017/04/08, at 17:18, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
>>><br>
>>> Do you have a function that returns T? This might be cause by that,<br>
>>> because some simplification might have turned the function definition<br>
>>> `foo n = T` into `foo n` and the translator expects functions to be<br>
>>> defined using equations.<br>
>>><br>
>>> I debug the translator by starting the HOL session fresh in the file<br>
>>> you want to work in, then do all the opens at the top, then copy in<br>
>>> the code of the translator (this overshadows the opened<br>
>>> ml_translatorLib), then just feed file you want to debug in as usual.<br>
>>><br>
>>> Cheers,<br>
>>> Magnus<br>
>>><br>
>>> On 8 April 2017 at 18:12, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk">S.A.Owens@kent.ac.uk</a>> wrote:<br>
>>>> 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.<br>
>>>><br>
>>>> Improved induction theorem: inf_type_to_string_ind<br>
>>>> Failed translation: inf_type_to_string, inf_types_to_string<br>
>>>> Exception- HOL_ERR {message = "not an \"=\"", origin_function = "dest_eq(_ty)", origin_structure = "boolSyntax"} raised<br>
>>>><br>
>>>> Does anyone have any ideas what the problem might be, or tips on debugging translator failures?<br>
>>>><br>
>>>> Scott<br>
>>>> ______________________________<wbr>_________________<br>
>>>> Developers mailing list<br>
>>>> <a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
>>>> <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
>><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/developers</a><br>
</div></div></blockquote></div><br></div>