qsapp.golden

--- opening "qsapp.ma" ---
--- scope checking ---
--- type checking ---
type  Bool : Set
term  Bool.true : < Bool.true : Bool >
term  Bool.false : < Bool.false : Bool >
term  if : .[A : Set] -> Bool -> A -> A -> A
{ if [A] Bool.true t e = t
; if [A] Bool.false t e = e
}
type  Nat : Set
term  Nat.zero : < Nat.zero : Nat >
term  Nat.succ : ^(y0 : Nat) -> < Nat.succ y0 : Nat >
term  leq : Nat -> Nat -> Bool
{ leq Nat.zero n = Bool.true
; leq (Nat.succ m) Nat.zero = Bool.false
; leq (Nat.succ m) (Nat.succ n) = leq m n
}
type  List : + Size -> Set
term  List.nil : .[s!ze : Size] -> .[i < s!ze] -> List s!ze
term  List.nil : .[i : Size] -> < List.nil i : List $i >
term  List.cons : .[s!ze : Size] -> .[i < s!ze] -> ^ Nat -> ^ List i -> List s!ze
term  List.cons : .[i : Size] -> ^(y1 : Nat) -> ^(y2 : List i) -> < List.cons i y1 y2 : List $i >
term  partition : (Nat -> Bool) -> .[i : Size] -> List i -> .[A : Set] -> (List i -> List i -> A) -> A
{ partition p [i] (List.nil [j < i]) [A] k = k (List.nil [j]) (List.nil [j])
; partition p [i] (List.cons [j < i] n l) [A] k = if [A] (p n) (partition p [j] l [A] (\ l1 -> \ l2 -> k (List.cons [j] n l1) l2)) (partition p [j] l [A] (\ l1 -> \ l2 -> k l1 (List.cons [j] n l2)))
}
term  qsapp : .[i : Size] -> List i -> List # -> List #
{ qsapp [i] (List.nil [j < i]) acc = acc
; qsapp [i] (List.cons [j < i] n l) acc = partition (\ m -> leq m n) [j] l [List #] (\ l1 -> \ l2 -> qsapp [j] l1 (List.cons [#] n (qsapp [j] l2 acc)))
}
term  quicksort : List # -> List #
term  quicksort = \ l -> qsapp [#] l (List.nil [#])
term  n0 : Nat
term  n0 = Nat.zero
term  n1 : Nat
term  n1 = Nat.succ n0
term  n2 : Nat
term  n2 = Nat.succ n1
term  n3 : Nat
term  n3 = Nat.succ n2
term  n4 : Nat
term  n4 = Nat.succ n3
term  n5 : Nat
term  n5 = Nat.succ n4
term  n6 : Nat
term  n6 = Nat.succ n5
term  n7 : Nat
term  n7 = Nat.succ n6
term  n8 : Nat
term  n8 = Nat.succ n7
term  n9 : Nat
term  n9 = Nat.succ n8
term  l : List #
term  l = List.cons [#] n4 (List.cons [#] n9 (List.cons [#] n1 (List.cons [#] n7 (List.cons [#] n6 (List.cons [#] n4 (List.cons [#] n0 (List.cons [#] n0 (List.cons [#] n3 (List.cons [#] n3 (List.cons [#] n3 (List.cons [#] n2 (List.cons [#] n3 (List.nil [#])))))))))))))
term  l' : List #
term  l' = quicksort l
--- evaluating ---
--- closing "qsapp.ma" ---