[CakeML] translating mergesort

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Tue Apr 19 05:06:36 UTC 2016


I was able to work around this in the following way:

1. I defined a new version of mergesortN with a simpler definition and
induction theorem (just using the final conjunct of the original as the
whole definition).
2. I added the following theorem (temporarily) to the stateful rewriter:
``x + 1 = 2 <=> x = 1``

The theorem helps the translator's automation prove a lemma about the
induction. I suspect my step 1 was not necessary, but I like the simpler
definition.

On 17 April 2016 at 10:05, Konrad Slind <konrad.slind at gmail.com> wrote:

> 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/20160419/b74cdf8b/attachment.html>


More information about the Users mailing list