[CakeML] translating mergesort

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Sat Apr 16 23:51:39 UTC 2016


Thanks Konrad.

Does your translation work with the latest version of the CakeML translator?

I tried following your approach and still run into a failed translation. (I
rewrote DIV2 away rather than translating it, but I don't think that should
be the cause of the problem..)

On 15 April 2016 at 13:42, Konrad Slind <konrad.slind at gmail.com> wrote:

> Looking a bit more at this ... the reason we take
> the last conjunct of mergesortN_def is because all
> the ones before that are subsumed in the last one.
> Maybe the redundancy is confusing the translator.
>
> Konrad.
>
>
> On Thu, Apr 14, 2016 at 10:34 PM, Konrad Slind <konrad.slind at gmail.com>
> wrote:
>
>> What is called in my development (this is used in the regexp compiler).
>>
>>  val thms =
>> List.map translate
>>   [mergesortTheory.sort2_def,
>>    mergesortTheory.sort3_def,
>>    mergesortTheory.merge_def,
>>    arithmeticTheory.DIV2_def,
>>    listTheory.DROP_def,
>>    last(CONJUNCTS mergesortTheory.mergesortN_def),
>>    mergesortTheory.mergesort_def];
>>
>>
>>
>>
>>
>> On Thu, Apr 14, 2016 at 10:13 PM, Konrad Slind <konrad.slind at gmail.com>
>> wrote:
>>
>>> This sounds familiar. I got mergesortN to translate.
>>> Might have had to fix the translator in order to make it go through.
>>>
>>> Konrad.
>>>
>>>
>>> On Thu, Apr 14, 2016 at 9:44 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk
>>> > wrote:
>>>
>>>> Hi,
>>>>
>>>> I am trying to use the CakeML translator to translate mergesort from
>>>> HOL's mergesortTheory. The main function to translate is mergesortN_def,
>>>> printed below. But the translator fails. Why? I translated sort2 and sort3
>>>> and DROP already, so I don't think they are the problem.
>>>>
>>>> val it =
>>>>    |- (∀l R. mergesortN R 0 l = []) ∧
>>>>    (∀x l R. mergesortN R 1 (x::l) = [x]) ∧
>>>>    (∀R. mergesortN R 1 [] = []) ∧
>>>>    (∀y x l R. mergesortN R 2 (x::y::l) = sort2 R x y) ∧
>>>>    (∀x R. mergesortN R 2 [x] = [x]) ∧ (∀R. mergesortN R 2 [] = []) ∧
>>>>    (∀z y x l R. mergesortN R 3 (x::y::z::l) = sort3 R x y z) ∧
>>>>    (∀y x R. mergesortN R 3 [x; y] = sort2 R x y) ∧
>>>>    (∀x R. mergesortN R 3 [x] = [x]) ∧ (∀R. mergesortN R 3 [] = []) ∧
>>>>    ∀v4 l R.
>>>>      mergesortN R v4 l =
>>>>      if v4 = 0 then []
>>>>      else if v4 = 1 then case l of [] => [] | x::l' => [x]
>>>>      else if v4 = 2 then
>>>>        case l of [] => [] | [x'] => [x'] | x'::y::l'' => sort2 R x' y
>>>>      else if v4 = 3 then
>>>>        case l of
>>>>          [] => []
>>>>        | [x''] => [x'']
>>>>        | [x''; y'] => sort2 R x'' y'
>>>>        | x''::y'::z::l''' => sort3 R x'' y' z
>>>>      else
>>>>        (let len1 = v4 DIV 2
>>>>         in
>>>>           merge R (mergesortN R (v4 DIV 2) l)
>>>>             (mergesortN R (v4 − len1) (DROP len1 l))):
>>>>    thm
>>>>
>>>> Translating mergesortn
>>>> metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+0+0+0+0!
>>>> metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+0+0+0+0!
>>>> metis: r[+0+14]+0+0+0+0+0+0+0+0+0+0+0+0+0+0!
>>>> Failed translation: mergesortN
>>>> Exception- HOL_ERR {message = "no solution found", origin_function =
>>>> "FOL_FIND", origin_structure = "folTools"} raised
>>>>
>>>> I to looks like there's a lot of pattern matching in the definition.
>>>> What is the status of HOL issue #285 (
>>>> https://github.com/HOL-Theorem-Prover/HOL/issues/285)? I think that
>>>> might be able to help.
>>>>
>>>> Looking forward to your reply,
>>>> Ramana
>>>>
>>>> _______________________________________________
>>>> Users mailing list
>>>> Users at cakeml.org
>>>> https://lists.cakeml.org/listinfo/users
>>>>
>>>>
>>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/users/attachments/20160417/c44330db/attachment.html>


More information about the Users mailing list