MiniAgda-0.2022.3.11: test/succeed/msort.golden
MiniAgda by Andreas Abel and Karl Mehltretter
--- opening "msort.ma" ---
--- scope checking ---
--- type checking ---
type Bool : Set
term Bool.tt : < Bool.tt : Bool >
term Bool.ff : < Bool.ff : Bool >
term ifthenelse : .[A : Set] -> Bool -> A -> A -> A
{ ifthenelse [A] Bool.tt x y = x
; ifthenelse [A] Bool.ff x y = y
}
type Pair : ++(A : Set) -> Set
term Pair.pair : .[A : Set] -> ^(y0 : A) -> ^(y1 : A) -> < Pair.pair y0 y1 : Pair A >
term pr1 : .[A : Set] -> Pair A -> A
{ pr1 [A] (Pair.pair a b) = a
}
term pr2 : .[A : Set] -> Pair A -> A
{ pr2 [A] (Pair.pair a b) = b
}
type SList : ++(A : Set) -> + Size -> Set
term SList.nil : .[A : Set] -> .[s!ze : Size] -> .[i < s!ze] -> SList A s!ze
term SList.nil : .[A : Set] -> .[i : Size] -> < SList.nil i : SList A $i >
term SList.cons : .[A : Set] -> .[s!ze : Size] -> .[i < s!ze] -> ^ A -> ^ SList A i -> SList A s!ze
term SList.cons : .[A : Set] -> .[i : Size] -> ^(y1 : A) -> ^(y2 : SList A i) -> < SList.cons i y1 y2 : SList A $i >
term split : .[A : Set] -> .[i : Size] -> SList A i -> Pair (SList A i)
{ split [A] [.$i] (SList.nil [i]) = Pair.pair (SList.nil [i]) (SList.nil [i])
; split [A] [.$$i] (SList.cons [.$i] a (SList.nil [i])) = Pair.pair (SList.cons [$i] a (SList.nil [i])) (SList.nil [$i])
; split [A] [.$$i] (SList.cons [.$i] a (SList.cons [i] b as)) = let rec : Pair (SList A i)
= split [A] [i] as
in let l1 : SList A i
= pr1 [SList A i] rec
in let l2 : SList A i
= pr2 [SList A i] rec
in Pair.pair (SList.cons [i] a l1) (SList.cons [i] b l2)
}
term merge : .[A : Set] -> (leq : A -> A -> Bool) -> SList A # -> SList A # -> SList A #
{ merge [A] leq (SList.nil [.#]) ys = ys
; merge [A] leq (SList.cons [.#] x xs) (SList.nil [.#]) = SList.cons [#] x xs
; merge [A] leq (SList.cons [.#] x xs) (SList.cons [.#] y ys) = ifthenelse [SList A #] (leq x y) (SList.cons [#] x (SList.cons [#] y (merge [A] leq xs ys))) (SList.cons [#] y (SList.cons [#] x (merge [A] leq xs ys)))
}
term msort : .[A : Set] -> (leq : A -> A -> Bool) -> .[i : Size] -> SList A i -> SList A #
{ msort [A] leq [.$j] (SList.nil [j]) = SList.nil [#]
; msort [A] leq [.$$i] (SList.cons [.$i] a (SList.nil [i])) = SList.cons [#] a (SList.nil [#])
; msort [A] leq [.$$i] (SList.cons [.$i] a (SList.cons [i] b l)) = let sl : Pair (SList A i)
= split [A] [i] l
in let l1 : SList A #
= msort [A] leq [$i] (SList.cons [i] a (pr1 [SList A i] sl))
in let l2 : SList A #
= msort [A] leq [$i] (SList.cons [i] b (pr2 [SList A i] sl))
in merge [A] leq l1 l2
}
term msort' : .[A : Set] -> (leq : A -> A -> Bool) -> (.[i : Size] -> SList A i -> Pair (SList A i)) -> .[i : Size] -> SList A i -> SList A #
{ msort' [A] leq splt [.$j] (SList.nil [j]) = SList.nil [#]
; msort' [A] leq splt [.$$i] (SList.cons [.$i] a (SList.nil [i])) = SList.cons [#] a (SList.nil [#])
; msort' [A] leq splt [.$$i] (SList.cons [.$i] a (SList.cons [i] b l)) = let sl : Pair (SList A i)
= splt [i] l
in let l1 : SList A #
= msort' [A] leq splt [$i] (SList.cons [i] a (pr1 [SList A i] sl))
in let l2 : SList A #
= msort' [A] leq splt [$i] (SList.cons [i] b (pr2 [SList A i] sl))
in merge [A] leq l1 l2
}
--- evaluating ---
--- closing "msort.ma" ---