# [CakeML] translating mergesort

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Fri Apr 15 02:44:35 UTC 2016

```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.