Maude-help mailing list

["Francesco Bongiovanni" <bongiovanni AT gmail.com>]

Hi everyone,

I found what I consider a beautiful one-line piece of code that does sorting
by term rewriting on Helene Kirchner slides
(https://wiki.bordeaux.inria.fr/Helene-Kirchner/lib/exe/fetch.php?media=wiki:rcdlecture.pdf)
(on slide 15)

fmod SORT is
   inc LIST{Nat} .

   vars NL1 NL2 NL3 : List{Nat} .
   vars M N : Nat .

    op  sort : List{Nat} -> List{Nat} .
    eq sort(nil) = nil .

   ceq sort(NL1 M NL2 N NL3) = sort(NL1 N NL2 M NL3) if N < M .

endfm

*** red in SORT : sort(11 12 55 3 2 1) .
*** result List{Nat}: sort(1 2 3 11 12 55)

What I would like is to have a proper List{Nat} as a result without the `sort`
before as I would like to do operation on the result list; e.g head( sort(11
12 55 3 2 1)) would result in result [List{Nat}]: head(sort(1 3 5 22 26 44))
instead of 1 as I would like.

Do you think its possible ?

Thanks a lot for your insights !

- Francesco

ps: in order to pre-answer some remarks, yes I know there are plenty of
materials around sorting and many quicksort/mergesort example in Maude, but I
wish to keep this one line :D