From 0b319fe7a34fb8c6729ea8e333f48eb4c0044f21 Mon Sep 17 00:00:00 2001 From: Hongwei Date: Sun, 8 Sep 2024 13:00:10 -0400 Subject: [PATCH] Updating: very very minorly --- prelude/DATS/gmap000.dats | 24 +++++++++++++++++++----- prelude/SATS/VT/optn000_vt.sats | 4 ++-- prelude/SATS/optn000.sats | 2 +- srcgen1/TEST/Makefile_prelude | 2 ++ 4 files changed, 24 insertions(+), 8 deletions(-) diff --git a/prelude/DATS/gmap000.dats b/prelude/DATS/gmap000.dats index b918e1d99..4b9d3d647 100644 --- a/prelude/DATS/gmap000.dats +++ b/prelude/DATS/gmap000.dats @@ -40,21 +40,35 @@ Authoremail: gmhwxiATgmailDOTcom (* ****** ****** *) // #impltmp -< xs:vt > +< m0:vt > +< k0:vt > < x0:vt > gmap_sep((*void*)) = "," #impltmp -< xs:vt > +< m0:vt > +< k0:vt > < x0:vt > -gseq_end((*void*)) = "}" +gmap_end((*void*)) = "}" #impltmp -< xs:vt > +< m0:vt > +< k0:vt > < x0:vt > -gseq_beg((*void*)) = "gmap{" +gmap_beg((*void*)) = "gmap{" // (* ****** ****** *) (* ****** ****** *) // +#impltmp +< m0:t0 > +< k0:t0 > +< x0:t0 > +gmap_search$tst + (map, k0) = +head$opt( +filter0_fun( +gseq_strmize +<(k0,x0)>(map), lam(kx) => g_equal(k0, kx.0))) +// (* ****** ****** *) (* ****** ****** *) // diff --git a/prelude/SATS/VT/optn000_vt.sats b/prelude/SATS/VT/optn000_vt.sats index 1cf1049f3..c7479dcf4 100644 --- a/prelude/SATS/VT/optn000_vt.sats +++ b/prelude/SATS/VT/optn000_vt.sats @@ -72,7 +72,7 @@ fun optn_vt_length0 {b0:b0} (xs: -~optn_vt(x0,n0)): sint(b2i(b0)) +~optn_vt(x0,b0)): sint(b2i(b0)) // (* HX-2024-09-07: @@ -83,7 +83,7 @@ fun optn_vt_length1 {b0:b0} (xs: -!optn_vt(x0,n0)): sint(b2i(b0)) +!optn_vt(x0,b0)): sint(b2i(b0)) // #symload length0 with optn_vt_length0 of 1000 #symload length1 with optn_vt_length1 of 1000 diff --git a/prelude/SATS/optn000.sats b/prelude/SATS/optn000.sats index e537b349a..607585699 100644 --- a/prelude/SATS/optn000.sats +++ b/prelude/SATS/optn000.sats @@ -51,7 +51,7 @@ optn_cons_ // fun<> optn_nilq -{a:t0}{b:i0} +{a:t0}{b:b0} (xs: optn(a,b)): bool(~b) // (* ****** ****** *) diff --git a/srcgen1/TEST/Makefile_prelude b/srcgen1/TEST/Makefile_prelude index 2ed396d26..faddd241d 100644 --- a/srcgen1/TEST/Makefile_prelude +++ b/srcgen1/TEST/Makefile_prelude @@ -80,6 +80,8 @@ $(XATSOPT) -s $(PRELUDE)/SATS/gasz001.sats all0_sats:: ; \ $(XATSOPT) -s $(PRELUDE)/SATS/gasz002.sats all0_sats:: ; \ +$(XATSOPT) -s $(PRELUDE)/SATS/gmap000.sats +all0_sats:: ; \ $(XATSOPT) -s $(PRELUDE)/SATS/gcls000.sats all0_sats:: ; \ $(XATSOPT) -s $(PRELUDE)/SATS/gsyn000.sats