staload "libats/SATS/ilistp.sats"
stadef nil = ilist_nil
stadef cons = ilist_cons
sortdef nats = nat
dataprop MSET (ilist, int) =
| {x:nat} {xs:ilist} {n:nats}
MSETcons (cons (x, xs), x + n) of MSET (xs, n)
| MSETnil (nil, 0)
extern praxi MSET_istot {xs:ilist} (): [n:nats] MSET (xs, n)
dataprop LB (int, ilist) =
| {l:nat} {x:nat | l <= x} {xs:ilist} LBcons (l, cons (x, xs)) of LB (l, xs)
| {l:nat} LBnil (l, nil)
dataprop UB (ilist, int) =
| {u:nat} {x:nat | x <= u} {xs:ilist} UBcons (cons (x, xs), u) of UB (xs, u)
| {u:nat} UBnil (nil, u)
extern praxi LB_MSET_lemma {x:nat} {xs1,xs2:ilist} {n:nats}
(_: MSET (xs1, n), _: MSET (xs2, n), _lb: LB (x, xs1)):<prf> LB (x, xs2)
extern praxi UB_MSET_lemma {x:nat} {xs1,xs2:ilist} {n:nats}
(_: MSET (xs1, n), _: MSET (xs2, n), _ub: UB (xs1, x)):<prf> UB (xs2, x)
extern prfun LB_lemma_monotone
{l1,l2:nat | l1 <= l2} {xs: ilist} (pf: LB (l2, xs)):<prf> LB (l1, xs)
extern prfun UB_lemma_monotone
{u1,u2:nat | u1 >= u2} {xs: ilist} (pf: UB (xs, u2)):<prf> UB (xs, u1)
absprop ISORD (ilist)
extern prfun isord_nil (): ISORD (nil)
extern prfun isord_cons {x:int} {xs:ilist}
(pf1: LB (x, xs), pf2: ISORD (xs)): ISORD (cons (x, xs))
extern
prfun APPEND_MSET_lemma {xs,ys,zs:ilist} {n1,n2:nats}
(pf1: MSET (xs, n1), pf2: MSET (ys, n2), pf3: APPEND (xs, ys, zs))
:<prf> MSET (zs, n1 + n2)
extern
prfun APPEND_ISORD_lemma
{xs1,xs2,xs:ilist} {x:nat} (
pf1: ISORD xs1
, pf2: ISORD xs2
, pf3: UB (xs1, x)
, pf4: LB (x, xs2)
, pf5: APPEND (xs1, xs2, xs)
) :<prf> ISORD (xs)
abst@ype E (a: t@ype, x:int) = a
extern castfn eltencode {a:t@ype} (x: a):<> [x:pos] E (a, x)
extern castfn eltdecode {a:t@ype} {x:int} (x: E (a, x)):<> a
extern
fun{a:t@ype}
lte_elt_elt {x,y:nat} (x: E(a, x), y: E (a, y)):<> bool (x <= y)
overload <= with lte_elt_elt
datatype list (a:t@ype, ilist) =
| nil (a, nil) of ()
| {x:pos} {xs: ilist} cons (a, cons (x, xs)) of (E (a, x), list (a, xs))
typedef list (a:t@ype) = [xs:ilist] list (a, xs)
extern fun{a:t@ype} append {xs,ys:ilist}
(xs: list (a, xs), ys: list (a, ys)):<> [zs:ilist] (APPEND (xs, ys, zs) | list (a, zs))
implement{a}
append (xs, ys) = let
fun aux {xs,ys:ilist} .<xs>.
(xs: list (a, xs), ys: list (a, ys))
:<> [zs:ilist] (APPEND (xs, ys, zs) | list (a, zs)) = begin
case+ xs of
| cons (x, xs) => let
val (pf | zs) = aux (xs, ys) in (APPENDcons pf | cons (x, zs))
end
| nil () => (APPENDnil () | ys)
end in
aux (xs, ys)
end
fun{a:t@ype}
qsrt {xs:ilist} {n:nats} .<n,0>.
(pf: MSET (xs, n) | xs: list (a, xs))
:<> [xs: ilist] (MSET (xs, n), ISORD (xs) | list (a, xs)) = begin
case+ xs of
| cons (x, xs) => let
prval MSETcons pf = pf in part (
pf, MSETnil (), MSETnil (), UBnil (), LBnil () | x, xs, nil (), nil ()
) end
| nil () => let
prval MSETnil () = pf in (MSETnil (), isord_nil () | nil ())
end
end
and part {x:pos} {xs0,xs1,xs2:ilist} {n0,n1,n2:nats} .<n0+n1+n2,n0+1>. (
pf0: MSET (xs0, n0)
, pf1: MSET (xs1, n1)
, pf2: MSET (xs2, n2)
, pf_ub: UB (xs1, x)
, pf_lb: LB (x, xs2)
| x: E (a, x), xs0: list (a, xs0), xs1: list (a, xs1), xs2: list (a, xs2)
) :<> [xs: ilist] (MSET (xs, x+n0+n1+n2), ISORD (xs) | list (a, xs)) = begin
case+ xs0 of
| cons (x0, xs0) => let
prval MSETcons (pf0) = pf0
in
if x0 <= x then part (
pf0, MSETcons pf1, pf2, UBcons (pf_ub), pf_lb
| x, xs0, cons (x0, xs1), xs2
) else part (
pf0, pf1, MSETcons pf2, pf_ub, LBcons (pf_lb)
| x, xs0, xs1, cons (x0, xs2)
)
end | nil () => let
prval MSETnil () = pf0
val (pf1_set, pf1_ord | xs1) = qsrt (pf1 | xs1)
val (pf2_set, pf2_ord | xs2) = qsrt (pf2 | xs2)
prval pf_ub = UB_MSET_lemma (pf1, pf1_set, pf_ub)
prval pf_lb = LB_MSET_lemma (pf2, pf2_set, pf_lb)
prval pf2_ord1 = isord_cons (pf_lb, pf2_ord)
val (pf_app | xs) = append (xs1, cons (x, xs2))
prval pf_set = APPEND_MSET_lemma (pf1_set, MSETcons pf2_set, pf_app)
prval pf_ord = APPEND_ISORD_lemma (
pf1_ord, pf2_ord1, pf_ub, LBcons {x} (pf_lb), pf_app
)
in
(pf_set, pf_ord | xs)
end
end
extern fun{a:t@ype}
quicksort {xs:ilist} {n:nats}
(pf: MSET (xs, n) | xs: list (a, xs))
:<> [xs: ilist] (MSET (xs, n), ISORD (xs) | list (a, xs))
implement{a} quicksort (pf | xs) = qsrt<a> (pf | xs)
staload "libc/SATS/random.sats"
implement
lte_elt_elt<double>
{x,y} (x, y) = let
val x = eltdecode (x) and y = eltdecode(y)
extern castfn __cast (_: bool):<> bool (x <= y)
in
__cast (lte_double_double (x, y))
end
fn print_list (
xs: list (double)
) : void = let
fun aux (
xs: list (double), i: int
) : void = begin
case+ xs of
| cons (x, xs) => let
val x = eltdecode (x)
in
if i > 0 then print ", "; printf ("%.2f", @(x)); aux (xs, i+1)
end | nil () => ()
end in
aux (xs, 0)
end
fun randgen_list
{n:nat} .<n>.
(n: int n): list (double) =
if n > 0 then let
val x = drand48 ()
val x = eltencode (x)
in
cons {double} (x, randgen_list (n-1))
end else nil ()
implement main () = let
val () = srand48_with_time ()
val xs = randgen_list (20)
val () = (print "xs = "; print_list xs; print_newline ())
prval pfmset = MSET_istot ()
val (pford, pfmset | ys) = quicksort (pfmset | xs)
val () = (print "ys = "; print_list ys; print_newline ())
in
end