sc-reduced() ==
t,voters,clients.
<map(x.<x
, rec-dataflow(rec-dataflow(<<
, >, ff>;
s,a.let s1,s2 = s in
let _,_ = s1 in
let h,ty,v = a in
<<<, >
, if if if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;
)
then tt
else ff
fi
else ff
fi
then inl v
else ff
fi
then tt
if if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;_: 
_: )
then let a,b,_ = v in
if if a <z 0
then ff
else tt
fi
then if b <z 0
then ff
else tt
fi
else ff
fi
else ff
fi
else ff
fi
then inl v
else ff
fi
then tt
else ff
fi
then case if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;)
then tt
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(a) => inl if case s2
of inl(b) => ...
| inr(_) => tt
then <case s2
of inl(b) => ...
| inr(_) => <0
, []
, 1>
, case s2
of inl(b) => ...
| inr(_) => ...
>
else <case s2
of inl(b) => ...
| inr(_) => <0
, []
, 0>
, ff
>
fi
| inr(_) => case if if rec-case(h) of
[] => ff
b::bs' => _....
then if ...
then ...
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(b) => inl if ...
then <...
, ...
>
else <...
, ff
>
fi
| inr(_) => ff
else s2
fi
>
, case if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;)
then tt
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(a) => let _,y = if case s2
of inl(b) => ...
| inr(_) => tt
then <case s2
of inl(b) => ...
| inr(_) => <0, [], 1>
, case s2
of inl(b) => ...
| inr(_) => inl inl <0
, 0
, a>
>
else <case s2
of inl(b) => ...
| inr(_) => <0, [], 0>
, ff
>
fi in
case y
of inl(x) => x
| inr(_) => ff
| inr(_) => case if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _....
else ff
fi
then if eq_type(ty;_:
_:
)
then ...
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(b) => let _,y = if ...
then <...
, ...
>
else <...
, ff
>
fi in
case y
of inl(x) => x
| inr(_) => ff
| inr(_) => ff
>);s,m.let s',x = s m in
<s'
, case x
of inl(v) => map(x.<x, [], []>;
map(y.<y
, "msg"
, ``sc vote``
, _:
_:
, v>;voters))
| inr(_) => []
>)
>;voters)
@ map(x.<x
, rec-dataflow(rec-dataflow(<<, >, ff>;
s,a.let s1,s2 = s in
let _,_ = s1 in
let h,ty,v = a in
<<<, >
, if if if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;)
then tt
else ff
fi
else ff
fi
then inl v
else ff
fi
then tt
if if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;_: _: )
then let a,b,_ = v in
if if a <z 0
then ff
else tt
fi
then if b <z 0
then ff
else tt
fi
else ff
fi
else ff
fi
else ff
fi
then inl v
else ff
fi
then tt
else ff
fi
then case if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;)
then tt
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(a) => inl if case s2
of inl(b) => ...
| inr(_) => tt
then <case s2
of inl(b) => ...
| inr(_) => <0
, []
, 1>
, case s2
of inl(b) => ...
| inr(_) => ...
>
else <case s2
of inl(b) => ...
| inr(_) => <0
, []
, 0>
, ff
>
fi
| inr(_) => case if if ...
then if ...
then ...
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(b) => inl if ...
then <...
, ...
>
else <...
, ff
>
fi
| inr(_) => ff
else s2
fi
>
, case if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => ff
b::bs' => _.if ...
then rec-case(bs') of
[] => tt
_::_ => _.ff
else ff
fi
else ff
fi
then if eq_type(ty;)
then tt
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(a) => let _,y = if case s2
of inl(b) => ...
| inr(_) => tt
then <case s2
of inl(b) => ...
| inr(_) => <0, [], 1>
, case s2
of inl(b) => ...
| inr(_) => inl ...
>
else <case s2
of inl(b) => ...
| inr(_) => <0, [], 0>
, ff
>
fi in
case y
of inl(x) => case x
of inl(_) => ff
| inr(a) => ...
| inr(_) => ff
| inr(_) => case if if rec-case(h) of
[] => ff
b::bs' => _.if ...
then ...
else ff
fi
then if eq_type(ty;_:
_:
)
then ...
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(b) => let _,y = if ...
then <...
, ...
>
else <...
, ff
>
fi in
case y
of inl(x) => ...
| inr(_) => ff
| inr(_) => ff
>);
s,m.let s',x = s m in
<s'
, case x
of inl(v) => map(x.<x, [], []>;map(y.<y
, "msg"
, ``sc consensus``
, _:
, v>;clients))
| inr(_) => []
>)
>;voters)
, []
>
Definitions :
nil: [],
int: ,
product: x:A B[x],
pair: <a, b>,
token: "$token",
cons: [car / cdr],
lambda: x.A[x],
map: map(f;as),
decide: case b of inl(x) => s[x] | inr(y) => t[y],
apply: f a,
spread: spread def,
bfalse: ff,
inl: inl x ,
natural_number: $n,
minus: -n,
eq_int: (i =
j),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
spreadn: spread3,
subtract: n - m,
inr: inr x ,
btrue: tt,
list_accum: list_accum(x,a.f[x; a];y;l),
multiply: n * m,
length: ||as||,
add: n + m,
list_ind: list_ind def,
eq_type: eq_type(T;T'),
atom_eq: if a=b then c else d,
it: ,
rec-dataflow: rec-dataflow(s0;s,m.next[s; m]),
append: as @ bs
FDL editor aliases :
sc-reduced
sc-reduced() ==
\mlambda{}t,voters,clients.
<map(\mlambda{}x.<x
, rec-dataflow(rec-dataflow(<<\mcdot{}, \mcdot{}>, ff>
s,a.let s1,s2 = s in
let $_{}$,$_{}$ = s1 in
let h,ty,v = a in
<<<\mcdot{}, \mcdot{}>
, if if if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if "sc"=b the\000C
n tt else ff
then rec-case(bs') of
[] => ff
b::bs' => $_{}$.if if "inpu\000C
t"=b then tt else ff
then rec-case(bs') of
[] => tt
$_{}$::$_{\000C
}$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;\mBbbZ{}) then tt else ff fi
else ff
fi
then inl v
else ff
fi
then tt
if if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if "sc"=b the\000C
n tt else ff
then rec-case(bs') of
[] => ff
b::bs' => $_{}$.if if "vote\000C
"=b then tt else ff
then rec-case(bs') of
[] => tt
$_{}$::$_{\000C
}$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;$_{}$:\mBbbZ{} \mtimes{} $\mbackslash{}\000C
ff5f{}$:\mBbbZ{} \mtimes{} \mBbbZ{})
then let a,b,$_{}$ = v in
if if a <z 0 then ff else tt fi
then if b <z 0 then ff else tt fi
else ff
fi
else ff
fi
else ff
fi
then inl v
else ff
fi
then tt
else ff
fi
then case if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if "sc"=b\000C
then tt else ff
then rec-case(bs') of
[] => ff
b::bs' => $_{}$.if if "\000C
input"=b then tt else ff
then rec-case(bs') of
[] => tt
$_{}$::$_\mbackslash{}\000C
ff7b}$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;\mBbbZ{}) then tt else ff fi
else ff
fi
then inl v
else ff
fi
of inl(a) => inl if case s2
of inl(b) => let x,$_{}\000C
$ = b in
let $_{}\000C
$,$_{}$,i = x in
(i =\msubz{} 0)
| inr($_{}$) => tt
then <case s2
of inl(b) => let x,$_{}\mbackslash{}\000C
ff24 = b in
let n,$_{\mbackslash{}ff7\000C
d$,$_{}$ = x in
<n, [], 1>
| inr($_{}$) => ɘ,\000C
[], 1>
, case s2
of inl(b) => let x,$_{}\000C
$ = b in
let n,$_{\mbackslash{}ff\000C
7d$,$_{}$ = x in
inl inl <n, 0, a>
| inr($_{}$) => in\000C
l inl ɘ, 0, a>
>
else <case s2
of inl(b) => let x,$_{}\mbackslash{}\000C
ff24 = b in
let n,vs,i = x in
<n, vs, i>
| inr($_{}$) => ɘ,\000C
[], 0>
, ff
>
fi
| inr($_{}$) => case if if rec-case(h)\000C
of
[] => ff
b::bs' => $_{}$.\000C
if ...
then rec-case(bs') of
[] => ff
b::bs' => $_{}\mbackslash{}\000C
ff24.if ...
then rec-case(bs') of
[] => tt
$_{}$:\000C
:$_{}$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;$_{}\000C
$:\mBbbZ{} \mtimes{} $_{}$:\mBbbZ{} \mtimes{} \mBbbZ{})
then let a,b,$_{}\mbackslash{}\000C
ff24 = v in
if if a <z 0
then ff
else tt
fi
then if b <z 0
then ff
else tt
fi
else ff
fi
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(b) => inl if case s2
of inl(b1) => ...
| inr($_{}\000C
$) => ...
then <case s2
of inl(b1) => let x,$\mbackslash{}ff\000C
5f{}$ = b1 in
...
| inr($_{}\mbackslash{}\000C
ff24) => ...
, case s2
of inl(b1) => ...
| inr($_{}\000C
$) => ...
>
else <case s2
of inl(b1) => let x,$\mbackslash{}ff\000C
5f{}$ = b1 in
...
| inr($_{}\mbackslash{}\000C
ff24) => ...
, ff
>
fi
| inr($_{}$) => ff
else s2
fi
>
, case if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if "sc"=b then \000C
tt else ff
then rec-case(bs') of
[] => ff
b::bs' => $_{}$.if if "input"\000C
=b then tt else ff
then rec-case(bs') of
[] => tt
$_{}$::$_{\mbackslash{}f\000C
f7d$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;\mBbbZ{}) then tt else ff fi
else ff
fi
then inl v
else ff
fi
of inl(a) => let $_{}$,y = if case s2
of inl(b) => let x,$_{}\mbackslash{}\000C
ff24 = b in
let $_{}\mbackslash{}\000C
ff24,$_{}$,i = x in
(i =\msubz{} 0)
| inr($_{}$) => tt
then <case s2
of inl(b) => let x,$_{}$ \000C
= b in
let n,$_{}\mbackslash{}ff2\000C
4,$_{}$ = x in
<n, [], 1>
| inr($_{}$) => ɘ, [], \000C
1>
, case s2
of inl(b) => let x,$_{}$\000C
= b in
let n,$_{}\mbackslash{}ff\000C
24,$_{}$ = x in
inl inl <n, 0, a>
| inr($_{}$) => inl inl\000C
ɘ, 0, a>
>
else <case s2
of inl(b) => let x,$_{}$ \000C
= b in
let n,vs,i = x in
<n, vs, i>
| inr($_{}$) => ɘ, [], \000C
0>
, ff
>
fi in
case y of inl(x) => x | inr($_{}\mbackslash{}f\000C
f24) => ff
| inr($_{}$) => case if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if \000C
"sc"=b then tt else ff
then rec-case(bs') of
[] => ff
b::bs' => $_{}$.i\000C
f ...
then rec-case(bs') of
[] => tt
$_{}$::$\000C
_{}$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;$_{}$:\000C
\mBbbZ{} \mtimes{} $_{}$:\mBbbZ{} \mtimes{} \mBbbZ{})
then let a,b,$_{}$ =\000C
v in
if if a <z 0 then ff else tt fi
then if b <z 0 then ff else tt fi
else ff
fi
else ff
fi
else ff
fi
then inl v
else ff
fi
of inl(b) => let $_{}$,y = if cas\000C
e s2
of inl(b1) => let x,$\mbackslash{}ff\000C
5f{}$ = b1 in
...
| inr($_{}\mbackslash{}\000C
ff24) => let m,j,$_{}$ = b in
if 0 <z m
then tt
if (m =\msubz{} 0)
then if ...
then tt
...
else ff
fi
then <case s2
of inl(b1) => let x,$_\mbackslash{}ff\000C
7b}$ = b1 in
...
| inr($_{}$)\000C
=> let m,j,v = b in
if 0 <z m
then <m
, [v]
, j + 1>
if if j <z 0
then ff
else tt
fi
then ɘ
, [v]
, j + 1>
else ə, [], 0>
fi
, case s2
of inl(b1) => let x,$_\mbackslash{}f\000C
f7b}$ = b1 in
...
| inr($_{}$\000C
) => let m,j,v = b in
if 0 <z m
then inl inl <m
, j
, v>
if if j <z 0
then ff
else tt
fi
then inl inl <m
, j
, v>
else inl (inr ɘ
, v
> )
fi
>
else <case s2
of inl(b1) => let x,$_\mbackslash{}ff\000C
7b}$ = b1 in
...
| inr($_{}$)\000C
=> let m,j,v = b in
if m <z 0
then ɘ, [], 0>
if (j =\msubz{} -1)
then ɘ, [v], 0>
else ɘ, [], 0>
fi
, ff
>
fi in
case y of inl(x) => x | inr($_\000C
{}$) => ff
| inr($_{}$) => ff
>);s,m.let s',x = s m in
<s'
, case x
of inl(v) => map(\mlambda{}x.<x, [], []>map(\mlambda{}y.<y
, "msg"
, ``sc vote``
, $_{\mbackslash{}\000C
ff7d$:\mBbbZ{} \mtimes{} $_{}$:\mBbbZ{} \mtimes{} \mBbbZ{}
, v>voters))
| inr($_{}$) => []
>)
>voters)
@ map(\mlambda{}x.<x
, rec-dataflow(rec-dataflow(<<\mcdot{}, \mcdot{}>, ff>
s,a.let s1,s2 = s in
let $_{}$,$_{}$ = s1 in
let h,ty,v = a in
<<<\mcdot{}, \mcdot{}>
, if if if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if "sc"=b t\000C
hen tt else ff
then rec-case(bs') of
[] => ff
b::bs' => $_{}$.if if "in\000C
put"=b then tt else ff
then rec-case(bs') of
[] => tt
$_{}$::$_\mbackslash{}ff\000C
7b}$ => $_{}$.ff
else ff
fi
else ff
fi
then if eq\_type(ty;\mBbbZ{}) then tt else ff fi
else ff
fi
then inl v
else ff
fi
then tt
if if if rec-case(h) of
[] => ff
b::bs' => $_{}$.if if "sc"=b t\000C
hen tt else ...
then ...
else ...
fi
then ...
else ...
fi
then ...
else ...
fi
then ...
else ...
fi
then ...
else ...
fi
>
, ...
>);s,m....)
>...)
, ...
>
Date html generated:
2010_08_30-AM-12_59_26
Last ObjectModification:
2010_08_25-PM-07_09_48
Home
Index