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/20160414/b7e02175/attachment.html>