Updating: very very minorly

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>(x0)
+)
+//
+#impltmp
+{ x0:vt }
+gseq_forall0
+<optn_vt(x0)><x0> = optn_vt_forall0<x0>(*void*)
+//
+(* ****** ****** *)
+//
+#impltmp
+< x0:vt >
+optn_vt_rforall0
+  ( xs ) = 
+(
+case+ xs of
+| ~
+optn_vt_nil() => true
+| ~
+optn_vt_cons(x0) => rforall$test0<x0>(x0)
+)
+//
+#impltmp
+{ x0:vt }
+gseq_rforall0
+<optn_vt(x0)><x0> = optn_vt_rforall0<x0>(*void*)
+//
+(* ****** ****** *)
+//
+#impltmp
+< x0:vt >
+optn_vt_iforall0
+  ( xs ) = 
+(
+case+ xs of
+| ~
+optn_vt_nil() => true
+| ~
+optn_vt_cons(x0) => iforall$test0<x0>(0, x0)
+)
+//
+#impltmp
+{ x0:vt }
+gseq_iforall0
+<optn_vt(x0)><x0> = optn_vt_iforall0<x0>(*void*)
+//
+(* ****** ****** *)
+//
+#impltmp
+< x0:vt >
+optn_vt_irforall0
+  ( xs ) = 
+(
+case+ xs of
+| ~
+optn_vt_nil() => true
+| ~
+optn_vt_cons(x0) => irforall$test0<x0>(0, x0)
+)
+//
+#impltmp
+{ x0:vt }
+gseq_irforall0
+<optn_vt(x0)><x0> = optn_vt_irforall0<x0>(*void*)
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
+
+(* end of [ATS3/XANADU_prelude_DATS_VT_optn001_vt.dats] *)

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
+<m0><k0><x0>(map)) where
+{
+#impltmp
+exists$test0<k0>(k1) = g_equal<k0>(k0, k1)
+}
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+#impltmp
+< m0:t0 >
+< k0:t0 >
 < x0:t0 >
 gmap_search$tst
  (map, k0) =

prelude/DATS/gmap001.dats

@@ -43,11 +43,31 @@ Authoremail: gmhwxiATgmailDOTcom
 <map:t0>
 <key:vt>
 <itm:vt>
-gmap_key$strmize(map) =
-strm_vt_map$fopr0<(key,val)>
+gmap_key$strmize
+  ( map ) =
+let
+//
+val kxs =
 (
 gmap_keyval$strmize
-<map><key><val>(map), lam(kx) => kx.0)
+< map >< key >< itm >(map))
+//
+in//let
+(
+strm_vt_map0<kx>(kxs)) where
+{
+#vwtpdef kx = (key,itm)
+#impltmp map$fopr0<kx>(kx) = kx.0}
+end//let//end(gmap_key$strmize(map))
+//
+(* ****** ****** *)
+//
+#impltmp
+<map:t0>
+<key:vt>
+<itm:vt>
+gmap_keyval$strmize =
+gseq_strmize1<map><(key,itm)>(*void*)
 //
 (* ****** ****** *)
 (* ****** ****** *)

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 () =

srcgen1/prelude/SATS/gmap000.sats

@@ -56,7 +56,7 @@ gmap_print$keyval
 fun
 <map:t0>
 <key:t0>
-<itm:t0>
+<itm:vt>
 gmap_keyq
 (kxs: map, key: key): bool
 //
@@ -65,7 +65,7 @@ gmap_keyq
 fun
 <map:t0>
 <key:t0>
-<itm:t0>
+<itm:vt>
 gmap_make_nil((*0*)): (map)
 //
 (* ****** ****** *)

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] *)