[CakeML-dev] Translation failure

[Scott Owens]

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