Skip to content

Commit

Permalink
Updating: very very minorly
Browse files Browse the repository at this point in the history
  • Loading branch information
githwxi committed Sep 6, 2024
1 parent a8045bc commit a36f7cf
Show file tree
Hide file tree
Showing 8 changed files with 186 additions and 26 deletions.
46 changes: 43 additions & 3 deletions prelude/DATS/VT/strm000_vt.dats
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,14 @@ Authoremail: gmhwxiATgmailDOTcom
(* ****** ****** *)
(* ****** ****** *)
//
#impltmp
{ x0:vt }
g_free//~xs
<strm_vt(x0)>(xs) = $free(xs)
//
(* ****** ****** *)
(* ****** ****** *)
//
(*
HX-2024-07-17:
Wed 17 Jul 2024 10:27:26 PM EDT
Expand Down Expand Up @@ -237,11 +245,43 @@ It is not harm to keep it here as a reference.
#impltmp
{ x0:vt }
gseq_filter0_lstrm
<strm_vt(x0)><x0> = strm_vt_filter0<x0>(*void*)
<strm_vt(x0)><x0> = strm_vt_filter0<x0>
//
(* ****** ****** *)
(* ****** ****** *)
//
(*
HX-2024-09-05:
Thu 05 Sep 2024 07:59:10 PM EDT
*)
#impltmp
<a>(*tmp*)
strm_vt_concat0
( xss ) =
(
auxmain(xss)) where
{
fun auxmain(xss) = $llazy
(
case+ !xss of
| ~
strmcon_vt_nil() =>
strmcon_vt_nil()
| ~
strmcon_vt_cons(xs1, xss) => !
(
strm_vt_append00<a>(xs1, auxmain(xss)))
)
}(*where*)//end-of-[strm_vt_concat0(xss)]
//
(* ****** ****** *)
(* ****** ****** *)
//
#impltmp
<a>(*tmp*)
strm_vt_append0 =
strm_vt_append00<a>(*void*)
//
#impltmp
<a>(*tmp*)
strm_vt_append00
Expand All @@ -263,8 +303,8 @@ strmcon_vt_nil() => !ys
| ~
strmcon_vt_cons(x0, xs) =>
strmcon_vt_cons(x0, auxmain(xs, ys))
) (*case+*)
} (*where*)//end-of(strm_vt_append00(xs,ys))
)(*case+*)
}(*where*)//end-of(strm_vt_append00(xs,ys))
//
(* ****** ****** *)
(* ****** ****** *)
Expand Down
46 changes: 44 additions & 2 deletions prelude/DATS/gseq002.dats
Original file line number Diff line number Diff line change
Expand Up @@ -216,6 +216,46 @@ x2rforall$test<x0><y0>(x0, y0) = rforall$test@(x0, y0)
(* ****** ****** *)
//
(*
HX-2024-09-05:
Thu 05 Sep 2024 08:13:20 PM EDT
*)
#impltmp
{ xs:t0
, x0:t0
, ys:t0
, y0:t0 }
gseq_strmize
<
gx2seq
(xs,x0,ys,y0)><(x0,y0)>
(xsys) =
let
//
#typedef
xy = @(x0, y0)
//
val
@(xs, ys) =
x2tup_unmk(xsys)
val xs = GSEQ_unmk(xs)
and ys = GSEQ_unmk(ys)
//
in//let
strm_vt_concat0<xy>
(
gseq_map_f1un_lstrm
<xs><x0><strm_vt(xy)>
(
xs,
lam(x0) =>
gseq_map_f1un_lstrm<ys><y0><xy>(ys,lam(y0)=>(x0,y0)))
)
end//let//end-of-[gseq_strmize<gx2seq(...)><...>]
//
(* ****** ****** *)
(* ****** ****** *)
//
(*
HX-2024-08-05:
Mon 05 Aug 2024 06:21:53 PM EDT
*)
Expand Down Expand Up @@ -555,7 +595,7 @@ Sun 04 Aug 2024 07:26:14 AM EDT
(*
HX-2024-08-04:
This one is BUGGY!!!
Can you spot the cause :)
Can you spot the SUBTLE cause :)
#impltmp
< xs:t0 >
< x0:t0 >
Expand All @@ -572,7 +612,9 @@ forall$test<x0>(x0) =
gseq_forall<ys><y0>(ys)) where
{
#impltmp
forall$test<y0>(y0) = x2forall$test<x0><y0>(x0, y0)
forall$test<y0>(y0) =
(
x2forall$test<x0><y0>(x0, y0))
}(*where*)
}(*where*)//end-of-[gseq_x2forall(xs, ys)]
*)
Expand Down
49 changes: 47 additions & 2 deletions prelude/DATS/list000.dats
Original file line number Diff line number Diff line change
Expand Up @@ -473,25 +473,70 @@ where
< x0:t0 >
list_make_t0up3(xs) =
let
val @(x0, x1, x2) = xs in//let
val @(x0, x1, x2) = xs in
(
list_make_3val<x0>(x0, x1, x2))
end//let//end-of-[list_make_t0up3]
//
(* ****** ****** *)
//
(*
#impltmp
< x0:t0 >
list_make_t0up4 =
list_make_gseq<t0up(x0,x0,x0,x0)><x0>
*)
#impltmp
< x0:t0 >
list_make_t0up4(xs) =
let
val
@(x0, x1, x2, x3) = xs in
(
list_cons(x0,
list_make_3val<x0>(x1, x2, x3)))
end//let//end-of-[list_make_t0up4(xs)]
//
(*
#impltmp
< x0:t0 >
list_make_t0up5 =
list_make_gseq<t0up(x0,x0,x0,x0,x0)><x0>
*)
#impltmp
< x0:t0 >
list_make_t0up5 =
list_make_t0up5(xs) =
let
//
val
@(x0, x1, x2, x3, x4) = xs in
(
list_cons(x0,
list_cons(x1,
list_make_3val<x0>(x2, x3, x4))))
end//let//end-of-[list_make_t0up5(xs)]
//
(*
#impltmp
< x0:t0 >
list_make_t0up6 =
list_make_gseq<t0up(x0,x0,x0,x0,x0,x0)><x0>
*)
#impltmp
< x0:t0 >
list_make_t0up6(xs) =
let
//
val
@(x0, x1, x2, x3, x4, x5) = xs
//
in//let
(
list_cons(x0,
list_cons(x1,
list_cons(x2,
list_make_3val<x0>(x3, x4, x5)))))
end//let//end-of-[list_make_t0up6(xs)]
//
(* ****** ****** *)
(* ****** ****** *)
Expand Down
15 changes: 15 additions & 0 deletions prelude/SATS/VT/strm000_vt.sats
Original file line number Diff line number Diff line change
Expand Up @@ -77,6 +77,21 @@ strq_vt_length0
//
fun
<x0:vt>
strm_vt_concat0
( xss
: strm_vt
( strm_vt(x0) )): strm_vt(x0)
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
<x0:vt>
strm_vt_append0
( xs: strm_vt(x0)
, ys: strm_vt(x0)): strm_vt(x0)
fun
<x0:vt>
strm_vt_append00
( xs: strm_vt(x0)
, ys: strm_vt(x0)): strm_vt(x0)
Expand Down
2 changes: 1 addition & 1 deletion prelude/TEST/CATS/JS/Makefile_jsemit
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ test07:: ; \
$(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude.js >> $@_out.js
############
test07:: \
test07_gcls000.dats; \
test07_gseq000.dats; \
$(NODE) --stack-size=4096 $(SRCGEN2_XATS2JS) $< >> $@_out.js
########################################################################
########################################################################
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,10 @@ For testing prelude/JS!
(* ****** ****** *)
(* ****** ****** *)
//
(*
HX-2024-09-05:
Already defined in gseq002
*)
#define
GZ2SEQ(xs, ys) =
GSEQ_z2make(GSEQ(xs), GSEQ(ys))
Expand All @@ -36,18 +40,32 @@ GSEQ_x2make(GSEQ(xs), GSEQ(ys))
(* ****** ****** *)
//
val xs = list@(1, 2, 3)
val ys = list@(10,20,30)
val ys = list@(10,20,30,40)
val () = prints("xs = ", xs, "\n")
val () = prints("ys = ", ys, "\n")
//
(* ****** ****** *)
//
val ztup = GZ2SEQ(xs, ys)
val zxys = rlistize(ztup)
///
val ztup =
GZ2SEQ(xs, ys)
val ( ) =
prints("ztup = ", ztup, "\n")
//
val zxys = listize(ztup)
val ( ) =
print1s("rlistize(ztup) = ", zxys, "\n")
print1s("listize(ztup) = ", zxys, "\n")
//
(* ****** ****** *)
//
val xztup =
GSEQ_x2make
(GSEQ(xs), ztup)
val ( ) =
prints("xztup = ", xztup, "\n")
//
val xzxys = listize(xztup)
val ( ) =
print1s("listize(xztup) = ", xzxys, "\n")
//
(* ****** ****** *)
(* ****** ****** *)
Expand Down
13 changes: 13 additions & 0 deletions srcgen1/prelude/SATS/xunimpl.sats
Original file line number Diff line number Diff line change
Expand Up @@ -1592,6 +1592,19 @@ fun
list_make_t0up3
(tup: t0up(x0,x0,x0)): list(x0,3)
//
fun
<x0:t0>
list_make_t0up4
(tup: t0up(x0,x0,x0,x0)): list(x0,4)
fun
<x0:t0>
list_make_t0up5
(tup: t0up(x0,x0,x0,x0,x0)): list(x0,5)
fun
<x0:t0>
list_make_t0up6
(tup: t0up(x0,x0,x0,x0,x0,x0)): list(x0,6)
//
(* ****** ****** *)
(* ****** ****** *)
//
Expand Down
13 changes: 0 additions & 13 deletions xatslib/githwxi/TEST/CATS/JS/test99_mydiary.dats
Original file line number Diff line number Diff line change
Expand Up @@ -232,19 +232,6 @@ val () = prints("\n")
val rys = rlistize(GSEQ(ys))
val ( ) = print1s("rys = ", rys, "\n")
////
val rxys =
rlistize(GZ2SEQ(xs, ys))
val ( ) =
print1s("rlistize(GSEQ_z2make(GSEQ(xs), GSEQ(ys))) = ", rxys, "\n")
//
val xys =
listize(GX2SEQ(xs, ys))
val ( ) =
print1s("listize(GSEQ_x2make(GSEQ(xs), GSEQ(ys))) = ", xys, "\n")
val rxys =
rlistize(GX2SEQ(xs, ys))
val ( ) =
print1s("rlistize(GSEQ_x2make(GSEQ(xs), GSEQ(ys))) = ", rxys, "\n")
//
(* ****** ****** *)
(* ****** ****** *)
Expand Down

0 comments on commit a36f7cf

Please sign in to comment.