Updating: very very minorly

srcgen1/xatslib/githwxi/SATS/genv000.sats

@@ -68,7 +68,7 @@ forall$test_e1nv
 fun
 <x0:t0>
 <e1:vt>
-foreach$work_e1nv
+foritm$work_e1nv
 (x0: x0, e1: !e1): void
 *)
 //
@@ -123,7 +123,7 @@ fun
 <xs:t0>
 <x0:t0>
 <e1:vt>
-gseq_foreach_e1nv(xs, !e1): void
+gseq_foritm_e1nv(xs, !e1): void
 *)
 //
 (* ****** ****** *)

srcgen1/xatslib/libcats/SATS/libcats.sats

@@ -178,5 +178,9 @@ fun<>
 fputc_ptr(chr: sint, fp: !FILP1): ierr
 //
 (* ****** ****** *)
+(* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 
-(* end of [ATS3/XANADU_xatslib_libcats_libcats.sats] *)
+(* end of [ATS3/XANADU_srcgen1_xatslib_libcats_SATS_libcats.sats] *)

srcgen1/xatslib/libcats/SATS/synoug0.sats

@@ -1102,5 +1102,9 @@ gs_prerrln1_n10
 #symload prerrln1 with gs_prerrln1_n10
 //
 (* ****** ****** *)
+(* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 
-(* end of [ATS3/XANADU_xatslib_libcats_synoug0.sats] *)
+(* end of [ATS3/XANADU_srcgen1_xatslib_libcats_SATS_synoug0.sats] *)

srcgen2/HATS/xatsopt_sats.hats

@@ -6,23 +6,34 @@ For ATS3/XATSOPT
 *)
 (* ****** ****** *)
 (* ****** ****** *)
+//
 #staload
 "srcgen1\
 /xatslib/libcats/SATS/libcats.sats"
+//
 (* ****** ****** *)
+//
 #staload
 "srcgen1\
 /xatslib/libcats/SATS/synoug0.sats"
+//
 (* ****** ****** *)
 (* ****** ****** *)
+//
 #staload
 "srcgen1\
 /xatslib/githwxi/SATS/genv000.sats"
+//
 (* ****** ****** *)
+//
 #staload
 "srcgen1\
 /xatslib/githwxi/SATS/githwxi.sats"
+//
 (* ****** ****** *)
 (* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)
 
 (* end of [ATS3/XATSOPT_srcgen2_HATS_xatsopt_sats.hats] *)

srcgen2/Makefile_xatsopt

@@ -1,8 +1,10 @@
 ########################################################################
+########################################################################
 #
 # For typecking with xatsopt
 #
 ########################################################################
+########################################################################
 
 AR=ar
 CP=cp
@@ -924,4 +926,4 @@ clean:: ; rm -f */DATS/CATS/JS/*~
 cleanall:: clean
 ######
 
-######################## end of [Makefile] ##############################
+#################### end of [Makefile_xatsopt] ##########################

srcgen2/UTIL/Makefile

@@ -0,0 +1 @@
+Makefile_xats2js

srcgen2/UTIL/Makefile_xats2js

@@ -0,0 +1,58 @@
+########################################################################
+#
+# For compiling xatsopt_typing to JS
+#
+########################################################################
+#
+# HX-2024-03-25:
+# Mon 25 Mar 2024 06:06:29 PM EDT
+# The compiler is srcgen1/xats2js
+#
+########################################################################
+CAT=cat
+CPF=cp -f
+ECHO=echo
+NODE=node
+NODE=node \
+--stack-size=4096
+NODE=node \
+--stack-size=4096 \
+--max-old-space-size=4096
+########################################################################
+XSHARED=${XATSJSD}/xshared
+XATS2JS=${XATSJSD}/bin/xats2js
+########################################################################
+XATSJSD=\
+./../../srcgen1/xats2js/srcgenx
+########################################################################
+LIBXATSOPT_JS="./../lib/libxatsopt.js"
+########################################################################
+XATS2JS_PRELUDE="$(XSHARED)/runtime/xats2js_prelude.js"
+XATS2JS_PRELUDE_NODE="$(XSHARED)/runtime/xats2js_prelude_node.js"
+XATS2JS_XATSLIB_NODE="$(XSHARED)/runtime/xats2js_xatslib_node.js"
+########################################################################
+#
+all:: \
+xatsopt_typing
+xatsopt_typing:: \
+xatsopt_typing.dats ; \
+$(CAT) \
+$(XATS2JS_PRELUDE) > $@_dats.js && \
+$(CAT) \
+$(XATS2JS_PRELUDE_NODE) >> $@_dats.js && \
+$(CAT) \
+$(XATS2JS_XATSLIB_NODE) >> $@_dats.js && \
+$(CAT) $(LIBXATSOPT_JS) >> $@_dats.js && \
+$(XATS2JS) --output-a $@_dats.js --dynamic [email protected]
+#
+########################################################################
+#
+# HX: for cleaning up
+#
+clean:: ; rm -f *~
+#
+cleanall:: clean
+cleanall:: ; rm -f ./xatsopt_typing_dats.js
+#
+########################################################################
+###################### end of [Makefile_xats2js] #######################

srcgen2/UTIL/xatsopt_typing.dats

@@ -0,0 +1,65 @@
+(***********************************************************************)
+(*                                                                     *)
+(*                         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
+//
+Thu 29 Aug 2024 08:38:27 AM EDT
+//
+Authoremail: gmhwxiATgmailDOTcom
+*)
+(* ****** ****** *)
+(* ****** ****** *)
+#include
+"./../HATS/libxatsopt.hats"
+(* ****** ****** *)
+(* ****** ****** *)
+#include
+"./../HATS/xatsopt_sats.hats"
+#include
+"./../HATS/xatsopt_dats.hats"
+(* ****** ****** *)
+(* ****** ****** *)
+//
+val ret =
+the_fxtyenv_pvsload()
+val (  ) = prerrln
+("the_fxtyenv_pvsload() = ", ret)
+//
+val ret =
+the_tr12env_pvsload()
+val (  ) = prerrln
+("the_tr12env_pvsload() = ", ret)
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)
+
+(* end of [ATS3/XANADU_srcgen2_UTIL_xatstop_typing.dats] *)

srcgen2/xats2js/bin/xats2js.sh

@@ -0,0 +1,17 @@
+#!/bin/sh
+
+if [ ! "$XATSHOME" ] ; then
+  export \
+  XATSHOME=/home/hwxi/Research/ATS-Xanadu
+fi # end-if
+
+export NODE=node
+export XATS2JS_OUT=\
+"${XATSHOME}/srcgen2/xats2js/srcgenx/bin/xats2js.out"
+
+if [ -f "$XATS2JS_OUT" ] ; then
+  ${NODE} ${XATS2JS_OUT} "$@"
+else
+  # if build failed or "make cleanall" was executed
+  echo "please execute `make all` to build [xats2js.out]"
+fi # end-if

srcgen2/xats2js/srcgen1/HATS/libxatsopt.hats

@@ -25,9 +25,18 @@ Mon 19 Feb 2024 10:54:31 AM
 "./../../../SATS/xlabel0.sats"
 (* ****** ****** *)
 (* ****** ****** *)
-#staload
+#staload // LEX =
 "./../../../SATS/lexing0.sats"
 (* ****** ****** *)
+#staload // PAR =
+"./../../../SATS/parsing.sats"
+(* ****** ****** *)
+(* ****** ****** *)
+#staload
+"./../../../SATS/staexp0.sats"
+#staload
+"./../../../SATS/dynexp0.sats"
+(* ****** ****** *)
 #staload
 "./../../../SATS/staexp1.sats"
 #staload
@@ -37,12 +46,13 @@ Mon 19 Feb 2024 10:54:31 AM
 "./../../../SATS/staexp2.sats"
 #staload
 "./../../../SATS/statyp2.sats"
-(* ****** ****** *)
 #staload
 "./../../../SATS/dynexp2.sats"
+(* ****** ****** *)
 #staload
 "./../../../SATS/dynexp3.sats"
 (* ****** ****** *)
+(* ****** ****** *)
 #staload
 "./../../../SATS/trans01.sats"
 #staload
@@ -72,13 +82,13 @@ Mon 19 Feb 2024 10:54:31 AM
 "./../../../SATS/fperr30.sats"
 (* ****** ****** *)
 //
-#staload
-"./../../../SATS/xatsopt.sats"
+#staload "./../../../SATS/xatsopt.sats"
+#staload "./../../../SATS/xglobal.sats"
 //
 (* ****** ****** *)
-#staload(* GLO = *)
-"./../../../SATS/xglobal.sats"
-(* ****** ****** *)
 (* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 
 (* end of [ATS3/XANADU_srcgen2_xats2js_srcgen1_HATS_libxatsopt.hats] *)