Continued fraction/Arithmetic/G(matrix ng, continued fraction n1, continued fraction n2): Difference between revisions

Content added Content deleted
Line 432: Line 432:
extern fn cf_get_at_size : {i : int} (cf, size_t i) -> integer
extern fn cf_get_at_size : {i : int} (cf, size_t i) -> integer
extern fn cf_get_at_int : {i : nat} (cf, int i) -> integer
extern fn cf_get_at_int : {i : nat} (cf, int i) -> integer

extern fn cf2generator : cf -> cf_generator


(* The precedence of the overloads has to exceed that of ref[] *)
(* The precedence of the overloads has to exceed that of ref[] *)
Line 469: Line 471:


implement cf_get_at_int (cf, i) = cf_get_at_size (cf, g1i2u i)
implement cf_get_at_int (cf, i) = cf_get_at_size (cf, g1i2u i)

implement
cf2generator cf =
let
val i : ref Size_t = ref (i2sz 0)
in
lam () =>
let
val term = cf[!i]
in
!i := succ !i;
term
end
end


end (* local *)
end (* local *)
Line 781: Line 797:
cf_make
cf_make
let
let
typedef state = '(ng8,
val ng : ref ng8 = ref ng8
and xsource : ref cf_generator = ref (cf2generator x)
Size_t -<cloref1> integer,
and ysource : ref cf_generator = ref (cf2generator y)
Size_t -<cloref1> integer,
Size_t,
Size_t)

fn xsource (i : Size_t) :<cloref1> integer = x[i]
fn ysource (i : Size_t) :<cloref1> integer = y[i]

fn neginf_source (i : Size_t) :<cloref1> integer =
neginf<integerknd> ()


fn neginf_source () :<cloref1> integer = neginf<integerknd> ()
val state_ref : ref state =
ref '(ng8, xsource, ysource, i2sz 0, i2sz 0)
in
in
lam () =<cloref1>
lam () =<cloref1>
let
let
fnx
fnx
loop () : integer =
recurs () : integer =
let
let
val '(@(a12, a1, a2, a, b12, b1, b2, b),
val @(a12, a1, a2, a, b12, b1, b2, b) = !ng
xsource, ysource, i, j) = !state_ref
val bz = iseqz b
and b1z = iseqz b1
and b2z = iseqz b2
and b12z = iseqz b12
in
in
if iseqz b12 * iseqz b1 * iseqz b2 * iseqz b then
if b12z * b1z * b2z * bz then
neginf<integerknd> ()
neginf<integerknd> ()
else if iseqz b * iseqz b2 then
else if bz * b2z then
absorb_x_term ()
absorb_x_term ()
else if iseqz b + iseqz b2 then
else if bz + b2z then
absorb_y_term ()
absorb_y_term ()
else if iseqz b1 then
else if b1z then
absorb_x_term ()
absorb_x_term ()
else
else
Line 818: Line 828:
and @(q2, r2) = a2 divrem b2
and @(q2, r2) = a2 divrem b2
and @(q12, r12) =
and @(q12, r12) =
(if isneqz b12 then
(if ~b12z then
a12 divrem b12
a12 divrem b12
else
else
@(neginf (), neginf ())) : @(integer, integer)
@(neginf (), neginf ())) : @(integer, integer)
in
in
if (isneqz b12)
if (~b12z) * (q = q1) * (q = q2) * (q = q12) then
* (q = q1) * (q = q2) * (q = q12) then
begin (* Output a term. *)
begin (* Output a term. *)
!state_ref :=
!ng := @(b12, b1, b2, b, r12, r1, r2, r);
'(@(b12, b1, b2, b, r12, r1, r2, r),
xsource, ysource, i, j);
q
q
end
end
Line 849: Line 856:
absorb_x_term () : integer =
absorb_x_term () : integer =
let
let
val '(@(a12, a1, a2, a, b12, b1, b2, b),
val @(a12, a1, a2, a, b12, b1, b2, b) = !ng
xsource, ysource, i, j) = !state_ref
val term = (!xsource) ()
val term = xsource i
in
in
if term <> neginf<integerknd> () then
if term <> neginf<integerknd> () then
Line 857: Line 863:
try
try
let
let
val a12 = a2 +! (a12 *! term)
val a12_ = a2 +! (a12 *! term)
and a1 = a +! (a1 *! term)
and a1_ = a +! (a1 *! term)
and a2 = a12
and a2_ = a12
and a = a1
and a_ = a1
and b12 = b2 +! (b12 *! term)
and b12_ = b2 +! (b12 *! term)
and b1 = b +! (b1 *! term)
and b1_ = b +! (b1 *! term)
and b2 = b12
and b2_ = b12
and b = b1
and b_ = b1
in
in
!state_ref :=
!ng := @(a12_, a1_, a2_, a_,
'(@(a12, a1, a2, a, b12, b1, b2, b),
b12_, b1_, b2_, b_);
xsource, ysource, succ i, j);
(* Be aware: this is not a tail recursion! *)
(* Be aware: this is not a tail recursion! *)
loop ()
recurs ()
end
end
with
with
Line 877: Line 882:
(* Replace the sources with ones that return no
(* Replace the sources with ones that return no
terms. (You have to replace BOTH sources.) *)
terms. (You have to replace BOTH sources.) *)
!state_ref :=
!ng := @(a12, a1, a12, a1, b12, b1, b12, b1);
'(@(a12, a1, a12, a1, b12, b1, b12, b1),
!xsource := neginf_source;
neginf_source, neginf_source, succ i, j);
!ysource := neginf_source;
loop ()
recurs ()
end
end
end
end
else
else
begin
begin
!state_ref :=
!ng := @(a12, a1, a12, a1, b12, b1, b12, b1);
'(@(a12, a1, a12, a1, b12, b1, b12, b1),
recurs ()
xsource, ysource, succ i, j);
loop ()
end
end
end
end
Line 894: Line 897:
absorb_y_term () : integer =
absorb_y_term () : integer =
let
let
val '(@(a12, a1, a2, a, b12, b1, b2, b),
val @(a12, a1, a2, a, b12, b1, b2, b) = !ng
xsource, ysource, i, j) = !state_ref
val term = (!ysource) ()
val term = ysource j
in
in
if term <> neginf<integerknd> () then
if term <> neginf<integerknd> () then
Line 902: Line 904:
try
try
let
let
val a12 = a1 +! (a12 *! term)
val a12_ = a1 +! (a12 *! term)
and a1 = a12
and a1_ = a12
and a2 = a +! (a2 *! term)
and a2_ = a +! (a2 *! term)
and a = a2
and a_ = a2
and b12 = b1 +! (b12 *! term)
and b12_ = b1 +! (b12 *! term)
and b1 = b12
and b1_ = b12
and b2 = b +! (b2 *! term)
and b2_ = b +! (b2 *! term)
and b = b2
and b_ = b2
in
in
!state_ref :=
!ng := @(a12_, a1_, a2_, a_,
'(@(a12, a1, a2, a, b12, b1, b2, b),
b12_, b1_, b2_, b_);
xsource, ysource, i, succ j);
(* Be aware: this is not a tail recursion! *)
(* Be aware: this is not a tail recursion! *)
loop ()
recurs ()
end
end
with
with
Line 922: Line 923:
(* Replace the sources with ones that return no
(* Replace the sources with ones that return no
terms. (You have to replace BOTH sources.) *)
terms. (You have to replace BOTH sources.) *)
!state_ref :=
!ng := @(a12, a12, a2, a2, b12, b12, b2, b2);
'(@(a12, a12, a2, a2, b12, b12, b2, b2),
!xsource := neginf_source;
neginf_source, neginf_source, i, succ j);
!ysource := neginf_source;
loop ()
recurs ()
end
end
end
end
else
else
begin
begin
!state_ref :=
!ng := @(a12, a12, a2, a2, b12, b12, b2, b2);
'(@(a12, a12, a2, a2, b12, b12, b2, b2),
recurs ()
xsource, ysource, i, succ j);
loop ()
end
end
end
end
in
in
loop ()
recurs ()
end
end
end
end