#[test]
pub fn listing () { fgi_listing_test![
decls {
type OpNat = (+ Unit + Nat );
fn opnat_max:(
Thk[0] 0 OpNat -> 0 OpNat -> 0 F OpNat
) = {
#xo.#yo.
match (xo) {
_u => { ret yo }
x => { match (yo) {
_u => { ret yo }
y => {
if { x < y } {ret yo}
else {ret xo}
}
}}
}
}
type Lev = ( Nat )
type Seq = (
rec seq. foralli (X,Y):NmSet.
(+ (+ Unit + Nat)
+ (exists (X1,X2,X3) :NmSet | ((X1%X2%X3)=X:NmSet).
exists (Y1,Y2,Y3,Y4):NmSet | ((Y1%Y2%Y3%Y4)=Y:NmSet).
x Nm[X1] x Lev
x Ref[Y1](seq[X2][Y2])
x Ref[Y3](seq[X3][Y4]))
)
);
idxtm Seq_SR = ( #x:Nm.({x,@1})%({x,@2}) );
idxtm WS_Seq_SR = ( #x:NmSet.{@!}((Seq_SR) x) );
fn is_empty:(
Thk[0] foralli (X,Y):NmSet.
0 (Seq[X][Y]) -> { 0; Y } F Bool
) = { unimplemented }
}
let max:(
Thk[0] foralli (X,Y):NmSet.
0 Seq[X][Y] -> { {WS_Seq_SR} X; Y } F OpNat
) = {
ret thunk fix max. #seq. match seq {
on => { ret on }
bin => {
unpack (X1,X2,X3,Y1,Y2,Y3,Y4) bin = bin
let (n,lev,l,r) = {ret bin}
let (_rsl, ml) = { memo{n,(@1)}{ {force max}[X2][Y2]{!l} } }
let (_rsr, mr) = { memo{n,(@2)}{ {force max}[X3][Y4]{!r} } }
{{force opnat_max} ml mr}
}
}
}
ret 0
]}