From 84ee3973d94168af01c55fcc85fb0636a8c55c6b Mon Sep 17 00:00:00 2001 From: Hongwei Xi Date: Thu, 26 Oct 2023 19:45:38 -0400 Subject: [PATCH] Updating: very very minorly --- prelude/DATS/gint000.dats | 45 ++++++++++++++++++++++++++++++++++++++- srcgen2/DATS/tread33.dats | 2 ++ 2 files changed, 46 insertions(+), 1 deletion(-) diff --git a/prelude/DATS/gint000.dats b/prelude/DATS/gint000.dats index e66e4fea0..183d0b4e9 100644 --- a/prelude/DATS/gint000.dats +++ b/prelude/DATS/gint000.dats @@ -141,6 +141,49 @@ gint_consq_uint<>(xs) = (xs >= 1u) *) // (* ****** ****** *) +// +#impltmp + +gint_foldl_sint +(xs , r0) = +loop(x0, r0) where +{ +// +val x0 = 0 +// +#typedef x0 = sint +// +fun +loop(x0: x0, r0: r0): r0 = +if +x0 >= xs then r0 else +loop(x0+1, foldl$fopr(r0, x0)) +// +} (*where*) // end-of-[gint_foldl_sint] +// +(* ****** ****** *) +// +#impltmp + +gint_foldr_sint +(xs , r0) = +loop(x0, r0) where +{ +// +val x0 = xs +// +#typedef x0 = sint +// +fun +loop(x0: x0, r0: r0): r0 = +if +(x0 <= 0) then r0 else +(loop + (x0-1, foldr$fopr(x0-1, r0))) +// +} (*where*) // end-of-[gint_foldr_sint] +// +(* ****** ****** *) #impltmp gint_forall_sint<> @@ -250,7 +293,7 @@ end // end of [gint_rlistize_nint] (* ****** ****** *) #impltmp - + gint_map_llist_nint {n}(xs) = let // diff --git a/srcgen2/DATS/tread33.dats b/srcgen2/DATS/tread33.dats index 22342aa16..9657ce46d 100644 --- a/srcgen2/DATS/tread33.dats +++ b/srcgen2/DATS/tread33.dats @@ -144,8 +144,10 @@ d3parsed_get_parsed(dpar) val parsed = tread33_d3eclistopt(parsed, nerror) // +(* val ( ) = prerrln ("d3parsed_of_tread33: t3penv = ", t3penv) +*) // in//let //