module QuickSort imports libstratego-lib signature constructors true : Bool false : Bool 'not : Bool -> Bool Zero : Nat OneZero : Nat s : Nat -> Nat st : Nat * Nat -> Bool get : Nat * Nat -> Bool nil : NatList cons : Nat * NatList -> NatList plus : Nat * Nat -> Nat times : Nat * Nat -> Nat rev : Nat -> NatList pair : NatList * NatList -> NatListPair split : Nat * NatList -> NatListPair qsort : NatList -> NatList append : NatList * NatList -> NatList strategies main = (( qsort(rev(OneZero())) ; (?cons( Zero() , cons( s(Zero()) , cons( s(s(Zero())) , cons( s(s(s(Zero()))) , cons( s( s(s(s(Zero()))) ) , cons( s( s( s(s(s(Zero()))) ) ) , cons( s( s( s( s(s(s(Zero()))) ) ) ) , cons( s( s( s( s( s(s(s(Zero()))) ) ) ) ) , cons( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) , cons( s( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) ) , cons( s( s( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) ) ) , nil() ) ) ) ) ) ) ) ) ) ) ) ; say(!"Evaluated as expected!") <+ fatal-err( | [ "Unexpected value returned (was expecting " , cons( Zero() , cons( s(Zero()) , cons( s(s(Zero())) , cons( s(s(s(Zero()))) , cons( s( s(s(s(Zero()))) ) , cons( s( s( s(s(s(Zero()))) ) ) , cons( s( s( s( s(s(s(Zero()))) ) ) ) , cons( s( s( s( s( s(s(s(Zero()))) ) ) ) ) , cons( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) , cons( s( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) ) , cons( s( s( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) ) ) , nil() ) ) ) ) ) ) ) ) ) ) ) , ")" ] ))) ; qsort( rev(times(OneZero(), OneZero())) ) ; qsort( rev( times( OneZero() , times(OneZero(), OneZero()) ) ) ) ; id) ; 0 rewrite = \ OneZero() -> s( s( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) ) ) \ <+ \ 'not(true()) -> false() \ <+ \ 'not(false()) -> true() \ <+ \ st(Zero(), s(N)) -> true() \ <+ \ st(s(N), Zero()) -> false() \ <+ \ st(N, N) -> false() \ <+ \ st(s(N), s(M)) -> st(N, M) \ <+ \ get(N, M) -> 'not(st(N, M)) \ <+ \ plus(Zero(), N) -> N \ <+ \ plus(s(N), M) -> s(plus(N, M)) \ <+ \ times(Zero(), N) -> Zero() \ <+ \ times(s(N), M) -> plus(M, times(N, M)) \ <+ \ rev(s(N)) -> cons(s(N), rev(N)) \ <+ \ rev(Zero()) -> cons(Zero(), nil()) \ <+ \ split(N, cons(M, L)) -> pair(LT, cons(M, GT)) where (!st(N, M) => true() <+ st(N, M) => true()) ; (!split(N, L) => pair(LT, GT) <+ split(N, L) => pair(LT, GT)) ; id \ <+ \ split(N, cons(M, L)) -> pair(cons(M, LT), GT) where (!get(N, M) => true() <+ get(N, M) => true()) ; (!split(N, L) => pair(LT, GT) <+ split(N, L) => pair(LT, GT)) ; id \ <+ \ split(N, nil()) -> pair(nil(), nil()) \ <+ \ append(cons(N, L), LT) -> cons(N, append(L, LT)) \ <+ \ append(nil(), L) -> L \ <+ \ qsort(nil()) -> nil() \ <+ \ qsort(cons(N, L)) -> append( qsort(LT) , cons(N, qsort(GT)) ) where (!split(N, L) => pair(LT, GT) <+ split(N, L) => pair(LT, GT)) ; id \ <+ fail rewrite-all = not(is-list) ; (flatten-subterms <+ ?input ; (![] ; try( ![<\ OneZero() -> s( s( s( s( s( s( s( s(s(s(Zero()))) ) ) ) ) ) ) ) \> input|] ) ; try( ![<\ 'not(true()) -> false() \> input|] ) ; try( ![<\ 'not(false()) -> true() \> input|] ) ; try( ![<\ st(Zero(), s(N)) -> true() \> input|] ) ; try( ![<\ st(s(N), Zero()) -> false() \> input|] ) ; try( ![<\ st(N, N) -> false() \> input|] ) ; try( ![<\ st(s(N), s(M)) -> st(N, M) \> input|] ) ; try( ![<\ get(N, M) -> 'not(st(N, M)) \> input|] ) ; try( ![<\ plus(Zero(), N) -> N \> input|] ) ; try( ![<\ plus(s(N), M) -> s(plus(N, M)) \> input|] ) ; try( ![<\ times(Zero(), N) -> Zero() \> input|] ) ; try( ![<\ times(s(N), M) -> plus(M, times(N, M)) \> input|] ) ; try( ![<\ rev(s(N)) -> cons(s(N), rev(N)) \> input|] ) ; try( ![<\ rev(Zero()) -> cons(Zero(), nil()) \> input|] ) ; try( ![<\ split(N, cons(M, L)) -> pair(LT, cons(M, GT)) where (!st(N, M) => true() <+ st(N, M) => true()) ; (!split(N, L) => pair(LT, GT) <+ split(N, L) => pair(LT, GT)) ; id \> input|] ) ; try( ![<\ split(N, cons(M, L)) -> pair(cons(M, LT), GT) where (!get(N, M) => true() <+ get(N, M) => true()) ; (!split(N, L) => pair(LT, GT) <+ split(N, L) => pair(LT, GT)) ; id \> input|] ) ; try( ![<\ split(N, nil()) -> pair(nil(), nil()) \> input|] ) ; try( ![<\ append(cons(N, L), LT) -> cons(N, append(L, LT)) \> input|] ) ; try( ![<\ append(nil(), L) -> L \> input|] ) ; try( ![<\ qsort(nil()) -> nil() \> input|] ) ; try( ![<\ qsort(cons(N, L)) -> append( qsort(LT) , cons(N, qsort(GT)) ) where (!split(N, L) => pair(LT, GT) <+ split(N, L) => pair(LT, GT)) ; id \> input|] ) ; id) ; make-set ; not([]) ; try(?[])) flatten-subterms = one(is-list) ; ?name#() ; rec rec ( {?[args|tail] ; all-tails := tail ; <(flatten-list ; make-set)> args ; mapconcat( {head: ?head ; ])> all-tails } ) <+ ?[arg1|tail] ; all-tails := tail ; map(![arg1|]) <+ \ [] -> [[]] \} ) ; map(!name#()) rec-normal-form-main = debug(!"Normal form of: ") ; rec-normal-form ; debug(!"is: ") rec-normal-form = memo(innermost(rewrite)) rec-all-normal-forms = debug(!"All normal forms of: ") ; innermost(rewrite-all) ; (is-list <+ ![]) ; flatten-list ; make-set ; debug(!"are: ") rec-rewrites-to = debug(!"Rewrites to: ") ; (rec-normal-form, id) ; if eq then rec-rewrites-yes else Fst ; rec-rewrites-no end rec-equals = debug(!"Equals: ") ; if eq then rec-rewrites-yes else (rec-normal-form, id) ; if eq then rec-rewrites-yes else (id, rec-normal-form) ; if eq then rec-rewrites-yes else rec-rewrites-no end end end rec-rewrites-yes = !"yes" ; say(id) rec-rewrites-no = debug(!"no: ") ; !"no" repeat-memo(the-s) : term -> term' where repeat(Memo1) ; the-s => term' ; rules ( Memo1 : term -> term' )