public type Ordered :
empty,
ordered(Ordered,Int,Ordered).
public type Ordered_accu($T) :
accu
(
$T->$T empty,
(Int,$T) -> $T cons,
).
public define $T accu (Ordered t,$T acc,Ordered_accu($T) d)
=
if t is
{
empty then empty(d)(acc),
ordered(l,i,r) then accu(l,cons(d)(i,accu(r,acc,d)),d)
}.
public type Ordered_fold($T) :
fold
(
$T empty,
($T,Int,$T) -> $T ordered
).
public define $T fold (Ordered s,Ordered_fold($T) d)
=
if s is
{
empty then empty(d),
ordered(l,i,r) then ordered(d)(fold(l,d),i,fold(r,d))
}.
public type Ordered_cata($T) :
cata
(
$T empty,
(One->$T,Int,One->$T) -> $T ordered
).
public define $T cata (Ordered s,Ordered_cata($T) d,One _)
=
if s is
{
empty then empty(d),
ordered(l,i,r) then ordered(d)
((One u)|->cata(l,d,u),i,(One u)|->cata(r,d,u))
}.
public type Ordered_recu($T) :
recu
(
$T empty,
(Ordered,$T,Int,Ordered,$T) -> $T ordered
).
public define $T recu (Ordered s,Ordered_recu($T) d)
=
if s is
{
empty then empty(d),
ordered(l,i,r) then ordered(d)(l,recu(l,d),i,r,recu(r,d))
}.
public type Ordered_para($T) :
para
(
$T empty,
(Ordered,One->$T,Int,Ordered,One->$T) -> $T ordered
).
public define $T para (Ordered s,Ordered_para($T) d,One _)
=
if s is
{
empty then empty(d),
ordered(l,i,r) then ordered(d)
(l,(One u)|->para(l,d,u),i,r,(One u)|->para(r,d,u))
}.
public define Word32 cardinal (Ordered s)
=
fold
(
s,
fold
(
0,
(Word32 l,Int _,Word32 r) |-> l + 1 + r
)
).
public define Word32 cardinal (Ordered s)
=
accu
(
s,
0,
accu
(
(Word32 n) |-> n,
(Int _,Word32 n) |-> n + 1
)
).
public define Bool member (Ordered s,Int n)
=
cata
(
s,
cata
(
false,
(One->Bool l,Int i,One->Bool r) |->
if n < i then l(unique)
else if n > i then r(unique)
else true
),
unique
).
public define Bool forall (Ordered s,(Int)->Bool cond)
=
cata
(
s,
cata
(
true,
(One->Bool l,Int i,One->Bool r) |->
cond(i) & l(unique) & r(unique)
),
unique
).
public define Ordered insert (Ordered s,Int n)
=
para
(
s,
para
(
ordered(empty,n,empty),
(Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered dr) |->
if n < i then ordered(dl(unique),i,r)
else if n > i then ordered(l,i,dr(unique))
else s
),
unique
).
public define Ordered Ordered s + Int n
=
insert(s,n).
public define Int minimum (Ordered s,Int n)
=
para
(
s,
para
(
n,
(Ordered l,One->Int dl,Int i,Ordered r,One->Int _) |->
if l is empty then i else dl(unique)
),
unique
).
public define Ordered remove_minimum (Ordered sl,Int n,Ordered sr)
=
if sl is empty then
sr
else
ordered
(
para
(
sl,
para
(
empty,
(Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered _) |->
if l is empty then r
else ordered(dl(unique),i,r)
),
unique
),
n,
sr
).
public define Ordered concat (Ordered sa,Ordered sb)
=
if sa is empty then
sb
else if sb is
{
empty then sa
ordered(lb,nb,rb) then
ordered(sa,minimum(lb,nb),remove_minimum(lb,nb,rb))
}.
public define Ordered remove (Ordered s,Int n)
=
para
(
s,
para
(
empty,
(Ordered l,One->Ordered dl,Int i,Ordered r,One->Ordered dr) |->
if n < i then ordered(dl(unique),i,r)
else if n > i then ordered(l,i,dr(unique))
else concat(l,r)
),
unique
).
public define (Ordered,Bool,Ordered) split (Ordered s,Int n)
=
para
(
s,
para
(
(empty,false,empty),
(Ordered l,One->(Ordered,Bool,Ordered) dl,Int i,Ordered r,One->(Ordered,Bool,Ordered) dr) |->
if n < i then
(if dl(unique) is (a,b,c) then (a,b,ordered(c,i,r)))
else if n > i then
(if dr(unique) is (a,b,c) then (ordered(l,i,a),b,c))
else (l,true,r)
),
unique
).
public define Ordered filter (Ordered s,Int->Bool cond)
=
fold
(
s,
fold
(
empty,
(Ordered l,Int i,Ordered r) |->
if cond(i) then ordered(l,i,r)
else concat(l,r)
)
).
public define Ordered union (Ordered sa,Ordered sb)
=
fold
(
sa,
fold
(
(Ordered s) |-> s,
(Ordered->Ordered l,Int i,Ordered->Ordered r) |->
(Ordered s) |->
if s is
{
empty then empty,
ordered(sl,si,sr) then
if split(s,i) is (a,b,c) then ordered(l(a),i,r(c))
}
)
)
(sb).
public define Ordered Ordered sa + Ordered sb
=
union(sa,sb).
public define Ordered intersection (Ordered sa,Ordered sb)
=
fold
(
sa,
fold
(
(Ordered s) |-> empty,
(Ordered->Ordered l,Int i,Ordered->Ordered r) |->
(Ordered s) |->
if s is
{
empty then empty,
ordered(sl,si,sr) then
if split(s,i) is (a,b,c) then
if b then ordered(l(a),i,r(c))
else concat(l(a),r(c))
}
)
)
(sb).
public define Ordered difference (Ordered sa,Ordered sb)
=
recu
(
sa,
recu
(
(Ordered s) |-> empty,
(Ordered l,Ordered->Ordered dl,Int i,Ordered r,Ordered->Ordered dr) |->
(Ordered s) |->
if s is
{
empty then ordered(l,i,r),
ordered(sl,si,sr) then
if split(s,i) is (a,b,c) then
if b then concat(dl(a),dr(c))
else ordered(dl(a),i,dr(c))
}
)
)
(sb).
public define Ordered Ordered sa - Ordered sb
=
difference(sa,sb).
public define Bool subset (Ordered sa,Ordered sb)
=
fold
(
sa,
fold
(
(Ordered s) |-> true,
(Ordered->Bool l,Int i,Ordered->Bool r) |->
(Ordered s) |->
if s is
{
empty then true,
ordered(sl,si,sr) then
if i < si then l(sl) & member(sl,i) & r(s)
else if i > si then l(s) & member(sr,i) & r(sr)
else l(sl) & r(sr)
}
)
)
(sb).
public define Bool Ordered sa = Ordered sb
=
subset(sa,sb) & subset(sb,sa).
public define List(Int) to_ordered_list(Ordered t)
=
accu
(
t,
[],
accu
(
(List(Int) l) |-> l,
(Int i,List(Int) l) |-> [i . l]
)
).
Je comprends encore moins que le Coq, mais c'est très joli