[CakeML] translating mergesort

[Konrad Slind]

Probably it only works for me because of mods I made to the translator.
I will try to incorporate those changes into the current translator
after the weekend.

  The use of variables named starting with "v" and (I think) "x" is fragile
in definitions
sent through the translator. So for now, maybe change the variable names
throughout mergesortN and see if that makes a difference.

Konrad.


On Sat, Apr 16, 2016 at 6:51 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> 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/20160416/8cff224a/attachment.html>