Updating: very very minorly

githwxi · Sep 5, 2024 · 966a4c5 · 966a4c5
1 parent 7650045
commit 966a4c5
Show file tree

Hide file tree

Showing 15 changed files with 289 additions and 87 deletions.
diff --git a/prelude/DATS/CATS/JS/char000.cats b/prelude/DATS/CATS/JS/char000.cats
@@ -92,6 +92,16 @@ XATS2JS_char_sub_char
 }
 //
 ////////////////////////////////////////////////////////////////////////.
+//
+function
+XATS2JS_char_print
+  ( c0 )
+{
+  let cs = String.fromCharCode(c0)
+  XATS2JS_the_print_store.push(cs); return
+}
+//
+////////////////////////////////////////////////////////////////////////.
 ////////////////////////////////////////////////////////////////////////.
 // end of [ATS3/XANADU_prelude_DATS_CATS_JS_char000.cats]
 ////////////////////////////////////////////////////////////////////////.

diff --git a/prelude/DATS/list000.dats b/prelude/DATS/list000.dats
@@ -353,6 +353,38 @@ list_cons(x3, list_nil(*0*))))
 (* ****** ****** *)
 //
 (*
+HX-2024-09-05:
+Thu 05 Sep 2024 05:21:51 PM EDT
+*)
+//
+#impltmp
+< x0:t0 >
+list_make_t0up1(xs) =
+(
+  list_make_1val<x0>(xs.0))
+//
+#impltmp
+< x0:t0 >
+list_make_t0up2(xs) =
+(
+  list_make_2val<x0>(x0, x1))
+where
+{
+  val x0 = xs.0 and x1 = xs.1 }
+//
+#impltmp
+< x0:t0 >
+list_make_t0up3(xs) =
+let
+val @(x0, x1, x2) = xs in//let
+(
+  list_make_3val<x0>(x0, x1, x1))
+end//let//end-of-[list_make_t0up3]
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+(*
 HX-2024-09-01:
 Mon 02 Sep 2024 06:16:45 PM EDT
 *)

diff --git a/prelude/SATS/list000.sats b/prelude/SATS/list000.sats
@@ -72,20 +72,43 @@ list_make_3val
 (x1: a
 ,x2: a, x3: a): list(a, 3)
 //
-(* ****** ****** *)
-//
 #symload
-list_sing with list_make_1val of 1000
+list_sing with list_make_1val
 #symload
-list_1val with list_make_1val of 1000
+list_pair with list_make_2val
 //
 #symload
-list_pair with list_make_2val of 1000
+list_1val with list_make_1val
+#symload
+list_2val with list_make_2val
 #symload
-list_2val with list_make_2val of 1000
+list_3val with list_make_3val
+//
+(* ****** ****** *)
+(* ****** ****** *)
 //
+fun
+<a:t0>
+list_make_t0up1
+(tup: t0up(a)): list(a, 1)
+fun
+<a:t0>
+list_make_t0up2
+(tup: t0up(a, a)): list(a, 2)
+fun
+<a:t0>
+list_make_t0up3
+(tup: t0up(a, a, a)): list(a, 3)
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+#symload
+list with list_make_t0up1 of 1000
+#symload
+list with list_make_t0up2 of 1000
 #symload
-list_3val with list_make_3val of 1000
+list with list_make_t0up3 of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/TEST/CATS/JS/Makefile_jsemit b/prelude/TEST/CATS/JS/Makefile_jsemit
@@ -92,12 +92,14 @@ $(CAT) $(SRCGEN2_XSHARED)/xats2js_js1emit.js >> $@_out.js
 test03:: ; \
 $(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude.js >> $@_out.js
 ############
-test03:: ; \
-$(CAT) $(XATSHOME)/prelude/DATS/CATS/JS/NODE/node000.cats >> $@_out.js
-############
 test03:: \
 test03_a1sz000.dats; \
 $(NODE) --stack-size=4096 $(SRCGEN2_XATS2JS) $< >> $@_out.js
+############
+test03:: ; \
+npx google-closure-compiler -W QUIET \
+  --compilation_level ADVANCED --js=$@_out.js --js_output_file=$@_out2.js
+########################################################################
 ########################################################################
 test04:: ; \
 echo "//" `date` > $@_out.js
@@ -114,6 +116,7 @@ test04:: \
 test04_strn000.dats; \
 $(NODE) --stack-size=4096 $(SRCGEN2_XATS2JS) $< >> $@_out.js
 ########################################################################
+########################################################################
 test05:: ; \
 echo "//" `date` > $@_out.js
 ############
@@ -138,23 +141,17 @@ $(CAT) $(SRCGEN2_XSHARED)/xats2js_js1emit.js >> $@_out.js
 test06:: ; \
 $(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude.js >> $@_out.js
 ############
-test06:: ; \
-$(CAT) $(XATSHOME)/prelude/DATS/CATS/JS/NODE/node000.cats >> $@_out.js
-############
 test06:: \
 test06_list000.dats; \
 $(NODE) --stack-size=4096 $(SRCGEN2_XATS2JS) $< >> $@_out.js
 ############
 test06:: ; \
 npx google-closure-compiler -W QUIET \
   --compilation_level SIMPLE --js=$@_out.js --js_output_file=$@_out1.js
-#
-# HX-2024-09-05:
-# It seems that 'node' stuff cannot be properly handled!
-# test06:: ; \
-# npx google-closure-compiler -W QUIET \
-#   --compilation_level ADVANCED --js=$@_out.js --js_output_file=$@_out2.js
-#
+############
+test06:: ; \
+npx google-closure-compiler -W QUIET \
+  --compilation_level ADVANCED --js=$@_out.js --js_output_file=$@_out2.js
 ########################################################################
 ########################################################################
 test99:: ; \

diff --git a/prelude/TEST/CATS/JS/test03_a1sz000.dats b/prelude/TEST/CATS/JS/test03_a1sz000.dats
@@ -17,9 +17,11 @@ For testing prelude/JS!
 "srcgen2\
 /prelude/HATS/prelude_JS_dats.hats"
 (* ****** ****** *)
+(*
 #include
 "srcgen2\
 /prelude/HATS/prelude_NODE_dats.hats"
+*)
 (* ****** ****** *)
 (* ****** ****** *)
 //
@@ -55,6 +57,11 @@ prints("fact(10) = ", fact(10), "\n")
 (* ****** ****** *)
 (* ****** ****** *)
 //
+val () = console_log(the_print_store_flush())
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 

diff --git a/prelude/TEST/CATS/JS/test06_list000.dats b/prelude/TEST/CATS/JS/test06_list000.dats
@@ -17,9 +17,11 @@ For testing prelude/JS!
 "srcgen2\
 /prelude/HATS/prelude_JS_dats.hats"
 (* ****** ****** *)
+(*
 #include
 "srcgen2\
 /prelude/HATS/prelude_NODE_dats.hats"
+*)
 (* ****** ****** *)
 (* ****** ****** *)
 //
@@ -81,6 +83,11 @@ val ( ) = prints("list_fmake_fwork(...) = ", xs2, "\n")
 (* ****** ****** *)
 (* ****** ****** *)
 //
+val () = console_log(the_print_store_flush( (*void*) ))
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 

diff --git a/prelude/TEST/CATS/JS/test99_mydiary.dats b/prelude/TEST/CATS/JS/test99_mydiary.dats
@@ -23,8 +23,7 @@ For testing prelude/JS!
 (* ****** ****** *)
 (* ****** ****** *)
 //
-val () =
-prints
+val () = prints
 ("Hello from [test99_mydiary]!", "\n")
 //
 (* ****** ****** *)

diff --git a/prelude/basics0.sats b/prelude/basics0.sats
@@ -808,6 +808,8 @@ optn_vt2t
 {a:t0}{b:b0}
 (xs: optn_vt(a, b)): optn(a, b)
 //
+#symload vt2t with optn_vt2t of 1000
+//
 (* ****** ****** *)
 //
 (*
@@ -912,6 +914,8 @@ list_vt2t
 {a:t0}{n:i0}
 (xs: list_vt(a, n)): list(a, n)
 //
+#symload vt2t with list_vt2t of 1000
+//
 (* ****** ****** *)
 //
 (*

diff --git a/srcgen2/xats2js/srcgen1/xshared/runtime/xats2js_prelude.js b/srcgen2/xats2js/srcgen1/xshared/runtime/xats2js_prelude.js
@@ -1,4 +1,4 @@
-// Thu 05 Sep 2024 12:28:11 PM EDT
+// Thu 05 Sep 2024 01:48:28 PM EDT
 ////////////////////////////////////////////////////////////////////////
 ////////////////////////////////////////////////////////////////////////
 /*
@@ -412,6 +412,16 @@ XATS2JS_char_sub_char
 }
 //
 ////////////////////////////////////////////////////////////////////////.
+//
+function
+XATS2JS_char_print
+  ( c0 )
+{
+  let cs = String.fromCharCode(c0)
+  XATS2JS_the_print_store.push(cs); return
+}
+//
+////////////////////////////////////////////////////////////////////////.
 ////////////////////////////////////////////////////////////////////////.
 // end of [ATS3/XANADU_prelude_DATS_CATS_JS_char000.cats]
 ////////////////////////////////////////////////////////////////////////.

diff --git a/srcgen2/xats2js/srcgen1/xshared/runtime/xats2js_xatslib.js b/srcgen2/xats2js/srcgen1/xshared/runtime/xats2js_xatslib.js
@@ -1,4 +1,4 @@
-// Thu 05 Sep 2024 12:28:11 PM EDT
+// Thu 05 Sep 2024 01:48:28 PM EDT
 ////////////////////////////////////////////////////////////////////////
 ////////////////////////////////////////////////////////////////////////
 /*

diff --git a/xatslib/githwxi/DATS/range00.dats b/xatslib/githwxi/DATS/range00.dats
@@ -176,7 +176,7 @@ auxloop
 ( lb: si
 , ub: si): bool = // lb <= ub
 if
-forall$test<si>(ub)
+rforall$test<si>(ub)
 then
 (
 if
@@ -275,13 +275,13 @@ end(*let*)//end-of-[range_ibtw_inter(r1,r2)]
 fcast // fun
 GSEQ_make_range_ibtw
 (xs: range_ibtw): GSEQ(range_ibtw, sint)
-#symload GSEQ with GSEQ_make_range_ibtw//of(0)
+#symload GSEQ with GSEQ_make_range_ibtw of 1000
 //
 #extern
 fcast // fun
 GASZ_make_range_ibtw
 (xs: range_ibtw): GASZ(range_ibtw, sint)
-#symload GASZ with GASZ_make_range_ibtw//of(0)
+#symload GASZ with GASZ_make_range_ibtw of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/xatslib/githwxi/HATS/githwxi_dats.hats b/xatslib/githwxi/HATS/githwxi_dats.hats
@@ -29,5 +29,5 @@ HX: for linearly typed interfaces
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 
-(* end of [ATS3_XANADU/xatslib/HATS/xatslib_JS_dats.hats] *)
+(* end of [ATS3_XANADU/xatslib/githwxi/HATS/githwxi_JS_dats.hats] *)
 
diff --git a/xatslib/githwxi/TEST/CATS/JS/Makefile_jsemit b/xatslib/githwxi/TEST/CATS/JS/Makefile_jsemit
@@ -0,0 +1,68 @@
+########################################################################
+########################################################################
+# Makefile for JS-emission
+########################################################################
+########################################################################
+CAT=cat
+ECHO=echo
+NODE=node
+########################################################################
+########################################################################
+all:: test01
+all:: test99
+########################################################################
+########################################################################
+testall:: test00; $(NODE) $<_out.js
+testall:: test01; $(NODE) $<_out.js
+testall:: test02; $(NODE) $<_out.js
+########################################################################
+########################################################################
+SRCGEN2_SRCGENX=\
+$(XATSHOME)/srcgen2/xats2js/srcgenx
+SRCGEN2_XSHARED=\
+$(XATSHOME)/srcgen2/xats2js/srcgenx/xshared/runtime
+SRCGEN2_XATS2JS=\
+$(XATSHOME)/srcgen2/xats2js/srcgenx/UTIL/xats2js_jsemit_dats.js
+########################################################################
+########################################################################
+test01:: ; \
+echo "//" `date` > $@_out.js
+############
+test01:: ; \
+$(CAT) $(SRCGEN2_XSHARED)/xats2js_js1emit.js >> $@_out.js
+test01:: ; \
+$(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude.js >> $@_out.js
+test01:: ; \
+$(CAT) $(SRCGEN2_XSHARED)/xats2js_xatslib.js >> $@_out.js
+############
+test01:: ; \
+$(CAT) $(XATSHOME)/prelude/DATS/CATS/JS/NODE/node000.cats >> $@_out.js
+############
+test01:: \
+test01_range00.dats; \
+$(NODE) --stack-size=4096 $(SRCGEN2_XATS2JS) $< >> $@_out.js
+########################################################################
+########################################################################
+test99:: ; \
+echo "//" `date` > $@_out.js
+############
+test99:: ; \
+$(CAT) $(SRCGEN2_XSHARED)/xats2js_js1emit.js >> $@_out.js
+test99:: ; \
+$(CAT) $(SRCGEN2_XSHARED)/xats2js_prelude.js >> $@_out.js
+test99:: ; \
+$(CAT) $(SRCGEN2_XSHARED)/xats2js_xatslib.js >> $@_out.js
+############
+test99:: ; \
+$(CAT) $(XATSHOME)/prelude/DATS/CATS/JS/NODE/node000.cats >> $@_out.js
+############
+test99:: \
+test99_mydiary.dats; \
+$(NODE) --stack-size=4096 $(SRCGEN2_XATS2JS) $< >> $@_out.js
+########################################################################
+########################################################################
+clean:: ; rm -f *~
+cleanall:: ; rm -f *~
+cleanall:: ; rm -f test??_out.js
+########################################################################
+###################### end of [Makefile_jsemit] ########################