Updating: very very minorly

githwxi · Feb 8, 2025 · 62da747 · 62da747
1 parent 6c10a03
commit 62da747
Show file tree

Hide file tree

Showing 17 changed files with 236 additions and 60 deletions.
diff --git a/prelude/basics0.sats b/prelude/basics0.sats
@@ -1104,11 +1104,14 @@ stropt1
 #typedef stropt(n:i0) = stropt1(n)
 //
 (* ****** ****** *)
+(* ****** ****** *)
 //
 #absvwtp
 string_i0_vx(n:i0) <= p0tr
 #absvwtp
 stropt_i0_vx(n:i0) <= p0tr
+#absvwtp
+strtmp_i0_vx(n:i0) <= p0tr
 //
 #vwtpdef
 string0_vt =
@@ -1124,6 +1127,13 @@ stropt0_vt =
 stropt1_vt
 (n:i0) = stropt_i0_vx( n )
 //
+#vwtpdef
+strtmp0_vt =
+[n: i0] strtmp_i0_vx(n)
+#vwtpdef
+strtmp1_vt
+(n: i0) = strtmp_i0_vx( n )
+//
 (* ****** ****** *)
 //
 #sexpdef lstrn = string0_vt
@@ -1144,6 +1154,12 @@ stropt1_vt
 #vwtpdef stropt_vt(n:i0) = stropt1_vt(n)
 //
 (* ****** ****** *)
+//
+#vwtpdef strtmp_vt = strtmp0_vt
+#vwtpdef strtmp_vt(n:i0) = strtmp1_vt(n)
+//
+(* ****** ****** *)
+(* ****** ****** *)
 (*
 //
 // HX:

diff --git a/srcgen1/prelude/DATS/VT/strn000_vt.dats b/srcgen1/prelude/DATS/VT/strn000_vt.dats
@@ -322,9 +322,10 @@ $UN.castlin01
 //
 (* ****** ****** *)
 
-#impltmp<>
+#impltmp
+<>(*tmp*)
 strn_vt_make_strn
-  {n}(cs) =
+  {n:int}(cs) =
 (
 UN_strn_vt_cast(p0)
 ) where
@@ -341,13 +342,13 @@ where
 //
 val n0 = strn_length<>(cs)
 //
-#sexpdef stmp = strtmp1_vt
-//
 fnx
 loop
 {i:nat
 |i<=n}.<n-i>.
-( p0: stmp(n)
+( p0:
+! strtmp_vt
+  (   n   )
 , i0: sint(i)
 , cs: strn(n)): void =
 (
@@ -365,7 +366,8 @@ loop(p0, suc(i0), cs)) where
 
 (* ****** ****** *)
 
-#impltmp<>
+#impltmp
+<>(*tmp*)
 strn_vt_make_list
   {n}(cs) =
 (
@@ -409,7 +411,8 @@ strtmp_vt_set$at<>(p0, i0, c0) } )
 
 (* ****** ****** *)
 
-#impltmp<>
+#impltmp
+<>(*tmp*)
 strn_vt_make0_llist
   {n}(cs) =
 (
@@ -493,6 +496,7 @@ strntrm_vt_concat0<>(list_vt_strmize0(css))
 //
 (* ****** ****** *)
 //
+(*
 #impltmp
 <n0:i0>(*tmp*)
 strn_vt_tabulate
@@ -536,9 +540,11 @@ strtmp_vt_set$at<>(p0, i0, c0)
 ) (* end-of-of[loop(p0, i0)] *)
 //
 } (*where*)//end-of-[strn_vt_tabulate]
-
+*)
+//
 (* ****** ****** *)
 //
+(*
 #impltmp
 <>(*tmp*)
 strn_vt_tabulate$f1un
@@ -550,6 +556,7 @@ strn_vt_tabulate<n>(n0)
 #impltmp
 tabulate$fopr<cgtz><n>(i0) = f0(i0)
 }
+*)
 //
 (* ****** ****** *)
 //

diff --git a/srcgen1/prelude/SATS/VT/list000_vt.sats b/srcgen1/prelude/SATS/VT/list000_vt.sats
@@ -620,5 +620,8 @@ rstrmize0 with list_vt_rstrmize0 of 1000
 #symload permutize0 with list_vt_permutize0 of 1000
 //
 (* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)
 
 (* end of [ATS3/XANADU_prelude_list000_vt.sats] *)
diff --git a/srcgen1/prelude/SATS/VT/strm000_vt.sats b/srcgen1/prelude/SATS/VT/strm000_vt.sats
@@ -629,5 +629,8 @@ rlistize0 with strm_vt_rlistize0 of 1000
 #symload foritm0 with strm_vt_foritm0 of 1000
 (* ****** ****** *)
 (* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)
 
 (* end of [ATS3/XANADU_prelude_strm000_vt.sats] *)
diff --git a/srcgen1/prelude/SATS/VT/strm001_vt.sats b/srcgen1/prelude/SATS/VT/strm001_vt.sats
@@ -237,4 +237,8 @@ rlistize0 with strq_vt_rlistize0 of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)
+
+(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)
+
 (* end of [ATS3/XANADU_prelude_strm001_vt.sats] *)
diff --git a/srcgen1/prelude/SATS/VT/strn000_vt.sats b/srcgen1/prelude/SATS/VT/strn000_vt.sats
@@ -91,33 +91,15 @@ stropt_vt2t
 //
 (*
 HX-2020-09-27:
+(Please see prelude/basics0.sats)
 Note that [strtmp_vt] and [string_vt] are
 assumed to be of the same representation.
-The former is actually a temporary of the
-latter:
-A string_vt construction is cemented with
-a call to the cast-function UN_string_vt_cast,
-which itself is just a no-op.
-*)
-//
-#absvwtp
-strtmp_i0_vx(n:int) <= p0tr
-//
-(* ****** ****** *)
 //
-#vwtpdef
-strtmp0_vt =
-[n: int] strtmp_i0_vx(n)
-#vwtpdef
-strtmp1_vt
-(n: int) = strtmp_i0_vx( n )
+The former is actually a temporary of the latter:
+A string_vt construction is cemented with a call to the
+cast-function UN_string_vt_cast, which itself is just a no-op.
 //
-(* ****** ****** *)
-//
-#vwtpdef
-strtmp_vt(*nil*) = strtmp0_vt
-#vwtpdef
-strtmp_vt(n:int) = strtmp1_vt(n)
+*)
 //
 (* ****** ****** *)
 //

diff --git a/srcgen1/prelude/basics0.sats b/srcgen1/prelude/basics0.sats
@@ -1095,20 +1095,32 @@ stropt1
 string_i0_vx(n:i0) <= p0tr
 #absvwtp
 stropt_i0_vx(n:i0) <= p0tr
+#absvwtp
+strtmp_i0_vx(n:i0) <= p0tr
+//
+(* ****** ****** *)
+(* ****** ****** *)
 //
 #vwtpdef
 string0_vt =
-[n:i0] string_i0_vx(n)
+[n: i0] string_i0_vx(n)
 #vwtpdef
 string1_vt
-(n:i0) = string_i0_vx( n )
+(n: i0) = string_i0_vx( n )
 //
 #vwtpdef
 stropt0_vt =
-[n:i0] stropt_i0_vx(n)
+[n: i0] stropt_i0_vx(n)
 #vwtpdef
 stropt1_vt
-(n:i0) = stropt_i0_vx( n )
+(n: i0) = stropt_i0_vx( n )
+//
+#vwtpdef
+strtmp0_vt =
+[n: i0] strtmp_i0_vx(n)
+#vwtpdef
+strtmp1_vt
+(n: i0) = strtmp_i0_vx( n )
 //
 (* ****** ****** *)
 //
@@ -1118,18 +1130,24 @@ stropt1_vt
 #sexpdef strn_vt = string0_vt
 #sexpdef strn_vt = string1_vt
 //
-#vwtpdef string_vt = string0_vt
+#vwtpdef string_vt(*0*) = string0_vt
 #vwtpdef string_vt(n:i0) = string1_vt(n)
 //
 (* ****** ****** *)
 //
-#vwtpdef lstropt = stropt0_vt
+#vwtpdef lstropt(*0*) = stropt0_vt
 #vwtpdef lstropt(n:i0) = stropt1_vt(n)
 //
-#vwtpdef stropt_vt = stropt0_vt
+#vwtpdef stropt_vt(*0*) = stropt0_vt
 #vwtpdef stropt_vt(n:i0) = stropt1_vt(n)
 //
 (* ****** ****** *)
+//
+#vwtpdef strtmp_vt(*0*) = strtmp0_vt
+#vwtpdef strtmp_vt(n:i0) = strtmp1_vt(n)
+//
+(* ****** ****** *)
+(* ****** ****** *)
 (*
 //
 // HX:

diff --git a/srcgen1/xatslib/githwxi/SATS/githwxi.sats b/srcgen1/xatslib/githwxi/SATS/githwxi.sats
@@ -124,5 +124,8 @@ strn_rand_length
 {n:nat}(ln: sint(n)): strn_vt( n )
 //
 (* ****** ****** *)
+//
+(* ****** ****** *)(* ****** ****** *)
+(* ****** ****** *)(* ****** ****** *)
 
 (* end of [srcgen1_xatslib_githwxi_SATS_githwxi.sats] *)
diff --git a/srcgen2/DATS/filpath_drpth0.dats b/srcgen2/DATS/filpath_drpth0.dats
@@ -34,13 +34,24 @@ Authoremail: gmhwxiATgmailDOTcom
 *)
 //
 (* ****** ****** *)
-#include
-"./../HATS/xatsopt_dats.hats"
 (* ****** ****** *)
 #define
 ATS_PACKNAME
 "ATS3.XANADU.xatsopt-20220500"
 (* ****** ****** *)
+(* ****** ****** *)
+//
+#include
+"./../HATS/xatsopt_sats.hats"
+(*
+#include
+"./../HATS/xatsopt_dats.hats"
+*)
+#include
+"./../HATS/xatsopt_dpre.hats"
+//
+(* ****** ****** *)
+(* ****** ****** *)
 #staload "./../SATS/filpath.sats"
 (* ****** ****** *)
 

diff --git a/srcgen2/DATS/filpath_search.dats b/srcgen2/DATS/filpath_search.dats
@@ -40,10 +40,20 @@ ATS_PACKNAME
 "ATS3.XANADU.xatsopt-20220500"
 (* ****** ****** *)
 (* ****** ****** *)
+//
 #include
 "./../HATS/xatsopt_sats.hats"
+(*
 #include
 "./../HATS/xatsopt_dats.hats"
+*)
+#include
+"./../HATS/xatsopt_dpre.hats"
+//
+#include
+"srcgen1/xatslib/githwxi\
+/DATS/CATS/JS/NODE/basics0.dats"
+//
 (* ****** ****** *)
 (* ****** ****** *)
 #staload "./../SATS/xsymbol.sats"

diff --git a/srcgen2/DATS/trans01_utils0.dats b/srcgen2/DATS/trans01_utils0.dats
@@ -43,10 +43,16 @@ ATS_PACKNAME
 "ATS3.XANADU.xatsopt-20220500"
 (* ****** ****** *)
 (* ****** ****** *)
+//
 #include
 "./../HATS/xatsopt_sats.hats"
+(*
 #include
 "./../HATS/xatsopt_dats.hats"
+*)
+#include
+"./../HATS/xatsopt_dpre.hats"
+//
 (* ****** ****** *)
 (* ****** ****** *)
 #staload

diff --git a/srcgen2/DATS/trans12_decl00.dats b/srcgen2/DATS/trans12_decl00.dats
@@ -36,18 +36,22 @@ Authoremail: gmhwxiATgmailDOTcom
 *)
 //
 (* ****** ****** *)
-#include
-"./../HATS/xatsopt_sats.hats"
-#include
-"./../HATS/xatsopt_dats.hats"
 (* ****** ****** *)
 #define
 ATS_PACKNAME
 "ATS3.XANADU.xatsopt-20220500"
 (* ****** ****** *)
 (* ****** ****** *)
-#staload
-_(*TRANS12*) = "./trans12.dats"
+//
+#include
+"./../HATS/xatsopt_sats.hats"
+(*
+#include
+"./../HATS/xatsopt_dats.hats"
+*)
+#include
+"./../HATS/xatsopt_dpre.hats"
+//
 (* ****** ****** *)
 (* ****** ****** *)
 #staload "./../SATS/xbasics.sats"
@@ -77,6 +81,10 @@ _(*TRANS12*) = "./trans12.dats"
 #staload "./../SATS/xatsmtp.sats"
 (* ****** ****** *)
 (* ****** ****** *)
+#staload
+_(* TRANS12 *) = "./trans12.dats"
+(* ****** ****** *)
+(* ****** ****** *)
 #symload name with symbl_get_name
 (* ****** ****** *)
 #symload lctn with token_get_lctn

diff --git a/srcgen2/DATS/trans12_dynexp.dats b/srcgen2/DATS/trans12_dynexp.dats
@@ -43,15 +43,18 @@ ATS_PACKNAME
 "ATS3.XANADU.xatsopt-20220500"
 (* ****** ****** *)
 (* ****** ****** *)
+//
 #include
 "./../HATS/xatsopt_sats.hats"
+(*
 #include
 "./../HATS/xatsopt_dats.hats"
+*)
+#include
+"./../HATS/xatsopt_dpre.hats"
+//
 (* ****** ****** *)
 (* ****** ****** *)
-#staload
-_(*TRANS12*) = "./trans12.dats"
-(* ****** ****** *)
 #staload "./../SATS/xbasics.sats"
 (* ****** ****** *)
 #staload "./../SATS/xsymbol.sats"
@@ -74,6 +77,10 @@ _(*TRANS12*) = "./trans12.dats"
 #staload "./../SATS/trans12.sats"
 (* ****** ****** *)
 (* ****** ****** *)
+#staload
+_(* TRANS12 *) = "./trans12.dats"
+(* ****** ****** *)
+(* ****** ****** *)
 #symload lctn with token_get_lctn
 #symload node with token_get_node
 (* ****** ****** *)