[CakeML-dev] Translation failure

Magnus Myreen magnus.myreen at gmail.com
Sat Apr 8 16:18:01 UTC 2017

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.


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

More information about the Developers mailing list