Message de test de la coloration du code Anubis.
Commençons par un petit dérivateur formel en Anubis :
// a simple formal derivator
// functions from R to R
public type RtoR :
x,
cst(Int),
~ RtoR,
RtoR + RtoR,
RtoR * RtoR,
sin(RtoR),
cos(RtoR),
exp(RtoR).
// automagically generated
public type RtoR_recu($T) :
recu
(
$T x,
$T cst,
($T) -> $T neg,
($T,$T) -> $T add,
(RtoR,$T,RtoR,$T) -> $T mul,
(RtoR,$T) -> $T sin,
(RtoR,$T) -> $T cos,
(RtoR,$T) -> $T exp
).
// automagically generated
public define $T recu (RtoR f,RtoR_recu($T) d)
=
if f is
{
x then x(d),
cst(z) then cst(d),
~ u then neg(d)(recu(u,d)),
u + v then add(d)(recu(u,d),recu(v,d)),
u * v then mul(d)(u,recu(u,d),v,recu(v,d)),
sin(u) then sin(d)(u,recu(u,d)),
cos(u) then cos(d)(u,recu(u,d)),
exp(u) then exp(d)(u,recu(u,d))
}.
public define RtoR deriv (RtoR f)
=
recu
(
f,
recu
(
cst(0),
cst(1),
(RtoR du) |-> ~ du,
(RtoR du,RtoR dv) |-> du + dv,
(RtoR u,RtoR du,RtoR v,RtoR dv) |-> du * v + u * dv,
(RtoR u,RtoR du) |-> du * cos(u),
(RtoR u,RtoR du) |-> ~ du * sin(u),
(RtoR u,RtoR du) |-> du * exp(u)
)
).
J'attire l'attention du lecteur sur le fait que la fonction deriv n'est pas directement récursive, nulle part dans son corps elle appelle la fonction deriv !
En effet, toute la récursion est encapsulée dans le récurseur recu.
Le second exemple, à savoir les ensembles totalement ordonnés, illustre un ensemble plus complet de récurseurs : accu, fold, cata, recu et para.
Spoiler (Sélectionnez le texte dans le cadre pointillé pour le faire apparaître)
// totally ordered set of integers
public type Ordered :
empty,
ordered(Ordered,Int,Ordered).
// automagically generated
public type Ordered_accu($T) :
accu
(
$T->$T empty,
(Int,$T) -> $T cons,
).
// automagically generated
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)
}.
// automagically generated
public type Ordered_fold($T) :
fold
(
$T empty,
($T,Int,$T) -> $T ordered
).
// automagically generated
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))
}.
// automagically generated
public type Ordered_cata($T) :
cata
(
$T empty,
(One->$T,Int,One->$T) -> $T ordered
).
// automagically generated
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))
}.
// automagically generated
public type Ordered_recu($T) :
recu
(
$T empty,
(Ordered,$T,Int,Ordered,$T) -> $T ordered
).
// automagically generated
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))
}.
// automagically generated
public type Ordered_para($T) :
para
(
$T empty,
(Ordered,One->$T,Int,Ordered,One->$T) -> $T ordered
).
// automagically generated
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
)
).
// an alternative cardinal using 'accu' instead of 'fold'
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
).
// concatenation of sa + sb where max(sa) < min(sb)
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
).
// returns (sa,b,sb) where max(sa) < n < min(sb) and b = member(s,n)
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]
)
).
fuse.
Spoiler (Sélectionnez le texte dans le cadre pointillé pour le faire apparaître)
// skew max-heap
public type Skew :
empty,
skew(Skew,Int,Skew).
// automagically generated
public type Skew_fuse :
fuse
(
(Skew,Skew,(Skew,Skew)->Skew,(Skew,Skew)->Skew) -> Skew both_not_empty
).
// automagically generated
public define Skew fuse(Skew sa,Skew sb,Skew_fuse d)
=
if sa is {
empty then sb
skew(_,_,_) then
if sb is
{
empty then sa
skew(_,_,_) then both_not_empty(d)
(sa,sb,(Skew u,Skew v)|->fuse(u,v,d),(Skew u,Skew v)|->fuse(u,v,d))
}
}.
public define Skew join(Skew s1,Skew s2)
=
fuse
(
s1,
s2,
fuse
(
(Skew sa,Skew sb,(Skew,Skew)->Skew fa,(Skew,Skew)->Skew fb) |->
if sa is {empty then alert,skew(la,na,ra) then
if sb is {empty then alert,skew(lb,nb,rb) then
if na > nb then skew(la,na,fa(ra,sb))
else skew(fb(sa,lb),nb,rb)}}
)
).
public define Skew insert(Skew s,Int n)
=
join(s,skew(empty,n,empty)).
public define Skew remove(Skew l,Skew r)
=
join(l,r).
Je laisse le soin au lecteur de vérifier que les fonctions (assez avancées) de ces deux derniers exemples ne font appel à aucune récursion ni aucune itération.
au talentueux webmaster qui a implémenté la coloration OCaml, Anubis, Coq ainsi que la citation de code dans le texte, sur ma simple demande.
Je comprends encore moins que le Coq, mais c'est très joli