From b3a325b334a1f22d0080be81c28754847408c501 Mon Sep 17 00:00:00 2001 From: Hongwei Date: Sun, 8 Sep 2024 16:23:34 -0400 Subject: [PATCH] Updating: very very minorly --- prelude/DATS/VT/optn001_vt.dats | 122 ++++++++++++++++++++++++++++++ prelude/DATS/gmap000.dats | 17 +++++ prelude/DATS/gmap001.dats | 26 ++++++- srcgen1/DATS/xatsopt_utils0.dats | 6 ++ srcgen1/prelude/SATS/gmap000.sats | 4 +- srcgen1/prelude/SATS/gmap001.sats | 49 ++++++++++++ 6 files changed, 219 insertions(+), 5 deletions(-) create mode 100644 prelude/DATS/VT/optn001_vt.dats create mode 100644 srcgen1/prelude/SATS/gmap001.sats diff --git a/prelude/DATS/VT/optn001_vt.dats b/prelude/DATS/VT/optn001_vt.dats new file mode 100644 index 000000000..41c376f3c --- /dev/null +++ b/prelude/DATS/VT/optn001_vt.dats @@ -0,0 +1,122 @@ +(***********************************************************************) +(* *) +(* Applied Type System *) +(* *) +(***********************************************************************) + +(* +** ATS/Xanadu - Unleashing the Potential of Types! +** Copyright (C) 2024 Hongwei Xi, ATS Trustful Software, Inc. +** All rights reserved +** +** ATS is free software; you can redistribute it and/or modify it under +** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the +** Free Software Foundation; either version 3, or (at your option) any +** later version. +** +** ATS is distributed in the hope that it will be useful, but WITHOUT ANY +** WARRANTY; without even the implied warranty of MERCHANTABILITY or +** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +** for more details. +** +** You should have received a copy of the GNU General Public License +** along with ATS; see the file COPYING. If not, please write to the +** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA +** 02110-1301, USA. +*) + +(* ****** ****** *) +(* ****** ****** *) +// +(* +Author: Hongwei Xi +(* +Fri 06 Sep 2024 11:56:52 PM EDT +*) +Authoremail: gmhwxiATgmailDOTcom +*) +// +(* ****** ****** *) +(* ****** ****** *) +// +#impltmp +< x0:vt > +optn_vt_forall0 + ( xs ) = +( +case+ xs of +| ~ +optn_vt_nil() => true +| ~ +optn_vt_cons(x0) => forall$test0(x0) +) +// +#impltmp +{ x0:vt } +gseq_forall0 + = optn_vt_forall0(*void*) +// +(* ****** ****** *) +// +#impltmp +< x0:vt > +optn_vt_rforall0 + ( xs ) = +( +case+ xs of +| ~ +optn_vt_nil() => true +| ~ +optn_vt_cons(x0) => rforall$test0(x0) +) +// +#impltmp +{ x0:vt } +gseq_rforall0 + = optn_vt_rforall0(*void*) +// +(* ****** ****** *) +// +#impltmp +< x0:vt > +optn_vt_iforall0 + ( xs ) = +( +case+ xs of +| ~ +optn_vt_nil() => true +| ~ +optn_vt_cons(x0) => iforall$test0(0, x0) +) +// +#impltmp +{ x0:vt } +gseq_iforall0 + = optn_vt_iforall0(*void*) +// +(* ****** ****** *) +// +#impltmp +< x0:vt > +optn_vt_irforall0 + ( xs ) = +( +case+ xs of +| ~ +optn_vt_nil() => true +| ~ +optn_vt_cons(x0) => irforall$test0(0, x0) +) +// +#impltmp +{ x0:vt } +gseq_irforall0 + = optn_vt_irforall0(*void*) +// +(* ****** ****** *) +(* ****** ****** *) +// +(* ****** ****** *)(* ****** ****** *)(* ****** ****** *) +(* ****** ****** *)(* ****** ****** *)(* ****** ****** *) + +(* end of [ATS3/XANADU_prelude_DATS_VT_optn001_vt.dats] *) diff --git a/prelude/DATS/gmap000.dats b/prelude/DATS/gmap000.dats index bd8f7ae6a..23806f586 100644 --- a/prelude/DATS/gmap000.dats +++ b/prelude/DATS/gmap000.dats @@ -61,6 +61,23 @@ gmap_beg((*void*)) = "gmap{" #impltmp < m0:t0 > < k0:t0 > +< x0:vt > +gmap_keyq(map, k0) = +gseq_exists0 +( +gmap_key$strmize +(map)) where +{ +#impltmp +exists$test0(k1) = g_equal(k0, k1) +} +// +(* ****** ****** *) +(* ****** ****** *) +// +#impltmp +< m0:t0 > +< k0:t0 > < x0:t0 > gmap_search$tst (map, k0) = diff --git a/prelude/DATS/gmap001.dats b/prelude/DATS/gmap001.dats index 1585ab182..ed5c58b45 100644 --- a/prelude/DATS/gmap001.dats +++ b/prelude/DATS/gmap001.dats @@ -43,11 +43,31 @@ Authoremail: gmhwxiATgmailDOTcom -gmap_key$strmize(map) = -strm_vt_map$fopr0<(key,val)> +gmap_key$strmize + ( map ) = +let +// +val kxs = ( gmap_keyval$strmize -(map), lam(kx) => kx.0) +< map >< key >< itm >(map)) +// +in//let +( +strm_vt_map0(kxs)) where +{ +#vwtpdef kx = (key,itm) +#impltmp map$fopr0(kx) = kx.0} +end//let//end(gmap_key$strmize(map)) +// +(* ****** ****** *) +// +#impltmp + + + +gmap_keyval$strmize = +gseq_strmize1<(key,itm)>(*void*) // (* ****** ****** *) (* ****** ****** *) diff --git a/srcgen1/DATS/xatsopt_utils0.dats b/srcgen1/DATS/xatsopt_utils0.dats index c6735d688..5b2a226a4 100644 --- a/srcgen1/DATS/xatsopt_utils0.dats +++ b/srcgen1/DATS/xatsopt_utils0.dats @@ -648,6 +648,12 @@ val () = the_prelude_load ( XATSENV , 0(*static*) +, "srcgen1/prelude/SATS/gmap001.sats") +// +val () = +the_prelude_load +( XATSENV +, 0(*static*) , "srcgen1/prelude/SATS/gras000.sats") // val () = diff --git a/srcgen1/prelude/SATS/gmap000.sats b/srcgen1/prelude/SATS/gmap000.sats index 861c72510..b6ba7fa2d 100644 --- a/srcgen1/prelude/SATS/gmap000.sats +++ b/srcgen1/prelude/SATS/gmap000.sats @@ -56,7 +56,7 @@ gmap_print$keyval fun - + gmap_keyq (kxs: map, key: key): bool // @@ -65,7 +65,7 @@ gmap_keyq fun - + gmap_make_nil((*0*)): (map) // (* ****** ****** *) diff --git a/srcgen1/prelude/SATS/gmap001.sats b/srcgen1/prelude/SATS/gmap001.sats new file mode 100644 index 000000000..e353b7821 --- /dev/null +++ b/srcgen1/prelude/SATS/gmap001.sats @@ -0,0 +1,49 @@ +(***********************************************************************) +(* *) +(* Applied Type System *) +(* *) +(***********************************************************************) + +(* +** ATS/Xanadu - Unleashing the Potential of Types! +** Copyright (C) 2024 Hongwei Xi, ATS Trustful Software, Inc. +** All rights reserved +** +** ATS is free software; you can redistribute it and/or modify it under +** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the +** Free Software Foundation; either version 3, or (at your option) any +** later version. +** +** ATS is distributed in the hope that it will be useful, but WITHOUT ANY +** WARRANTY; without even the implied warranty of MERCHANTABILITY or +** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License +** for more details. +** +** You should have received a copy of the GNU General Public License +** along with ATS; see the file COPYING. If not, please write to the +** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA +** 02110-1301, USA. +*) + +(* ****** ****** *) +(* ****** ****** *) +// +(* +Author: Hongwei Xi +(* +Mon 29 Jul 2024 06:15:29 PM EDT +*) +Authoremail: gmhwxiATgmailDOTcom +*) +// +(* ****** ****** *) +(* ****** ****** *) +#include +"./../../../prelude/SATS/gmap001.sats" +(* ****** ****** *) +(* ****** ****** *) +// +(* ****** ****** *)(* ****** ****** *) +(* ****** ****** *)(* ****** ****** *) + +(* end of [ATS3/XANADU_srcgen1_prelude_SATS_gmap001.sats] *)