Updating: very very minorly

githwxi · Sep 15, 2024 · ac8d18a · ac8d18a
1 parent a0452f2
commit ac8d18a
Show file tree

Hide file tree

Showing 10 changed files with 99 additions and 18 deletions.
diff --git a/prelude/DATS/axrf001.dats b/prelude/DATS/axrf001.dats
@@ -116,6 +116,13 @@ owed_vt_return0(pf, x0) in btf end
 (* ****** ****** *)
 //
 #impltmp
+< x0:vt >
+a1rf_strmize =
+gasz_strmize<a1rf(x0)><x0>(*void*)
+//
+(* ****** ****** *)
+//
+#impltmp
 { x0:t0 }
 gseq_strmize
 <a1rf(x0)><x0> =

diff --git a/prelude/DATS/axsz001.dats b/prelude/DATS/axsz001.dats
@@ -42,6 +42,27 @@ Authoremail: gmhwxiATgmailDOTcom
 (* ****** ****** *)
 //
 #impltmp
+< x0:vt >
+a1sz_strmize =
+gasz_strmize<a1sz(x0)><x0>(*void*)
+//
+(* ****** ****** *)
+//
+#impltmp
+{ x0:t0 }
+gseq_strmize
+<a1sz(x0)><x0> =
+gasz_strmize<a1sz(x0)><x0>(*void*)
+#impltmp
+{ x0:vt }
+gseq_strmize1
+<a1sz(x0)><x0> =
+gasz_strmize<a1sz(x0)><x0>(*void*)
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+#impltmp
 { a: vt }
 g_forall<a1sz(a)> =
 gasz_forall<a1sz(a)><a>

diff --git a/prelude/SATS/axrf001.sats b/prelude/SATS/axrf001.sats
@@ -39,6 +39,16 @@ Authoremail: gmhwxiATgmailDOTcom
 //
 fun
 <a:vt>
+a1rf_strmize
+  (A: a1rf(a)): strm_vt(a)
+//
+#symload strmize with a1rf_strmize of 1000
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+fun
+<a:vt>
 a1rf_forall_size
 {n:nat}
 (A:a1rf(a,n), n:sint(n)): bool

diff --git a/prelude/SATS/axsz001.sats b/prelude/SATS/axsz001.sats
@@ -42,6 +42,16 @@ Authoremail: gmhwxiATgmailDOTcom
 //
 fun
 <a:vt>
+a1sz_strmize
+  (A: a1sz(a)): strm_vt(a)
+//
+#symload strmize with a1sz_strmize of 1000
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+fun
+<a:vt>
 a1sz_forall(A: a1sz(a)): bool
 fun
 <a:vt>

diff --git a/prelude/SATS/gcls000.sats b/prelude/SATS/gcls000.sats
@@ -196,8 +196,8 @@ GSEQ_irforall
 //
 #symload forall with GSEQ_forall of 1000
 #symload rforall with GSEQ_rforall of 1000
-#symload iforall with GSEQ_rforall of 1000
-#symload irforall with GSEQ_rforall of 1000
+#symload iforall with GSEQ_iforall of 1000
+#symload irforall with GSEQ_irforall of 1000
 //
 (* ****** ****** *)
 //
@@ -297,8 +297,8 @@ GSEQ_irforitm
 //
 #symload foritm with GSEQ_foritm of 1000
 #symload rforitm with GSEQ_rforitm of 1000
-#symload iforitm with GSEQ_rforitm of 1000
-#symload irforitm with GSEQ_rforitm of 1000
+#symload iforitm with GSEQ_iforitm of 1000
+#symload irforitm with GSEQ_irforitm of 1000
 //
 (* ****** ****** *)
 //
@@ -386,8 +386,8 @@ GSEQ(xs,x0), r0: r0): (r0)
 //
 #symload folditm with GSEQ_folditm of 1000
 #symload rfolditm with GSEQ_rfolditm of 1000
-#symload ifolditm with GSEQ_rfolditm of 1000
-#symload irfolditm with GSEQ_rfolditm of 1000
+#symload ifolditm with GSEQ_ifolditm of 1000
+#symload irfolditm with GSEQ_irfolditm of 1000
 //
 (* ****** ****** *)
 //

diff --git a/prelude/SATS/gseq001.sats b/prelude/SATS/gseq001.sats
@@ -99,13 +99,23 @@ gseq_istrqize
 (*
 HX: for [gs_forall]
 HX: for [gs_exists]
+HX: for [gs_iforall]
+HX: for [gs_iexists]
 *)
 fun
 <xs:t0>
 g_forall(xs: xs): bool
 fun
 <xs:t0>
 g_exists(xs: xs): bool
+fun
+<xs:t0>
+g_iforall(xs: xs): bool
+fun
+<xs:t0>
+g_iexists(xs: xs): bool
+//
+(* ****** ****** *)
 //
 fun
 <xs:t0>
@@ -248,6 +258,11 @@ HX: for [gs_foritm]
 fun
 <xs:t0>
 g_foritm(xs: xs): void
+fun
+<xs:t0>
+g_iforitm(xs: xs): void
+//
+(* ****** ****** *)
 //
 fun
 <xs:t0>

diff --git a/srcgen1/prelude/DATS/VT/list000_vt.dats b/srcgen1/prelude/DATS/VT/list000_vt.dats
@@ -180,7 +180,7 @@ list_vt_cons(_, xs) => loop(xs, ln+1)
 
 #impltmp
 <a>(*tmp*)
-list_vt_make_nval
+list_vt_make_ncpy
   (n0, x0) = let
 //
 fnx
@@ -207,7 +207,7 @@ in
 let
 var r0: list_vt(a) in loop(n0, r0); r0
 end
-end (* end of [list_vt_make_nval] *)
+end (* end of [list_vt_make_ncpy] *)
 
 (* ****** ****** *)
 

diff --git a/srcgen1/prelude/SATS/VT/list000_vt.sats b/srcgen1/prelude/SATS/VT/list000_vt.sats
@@ -156,13 +156,11 @@ list_vt_make_3val
 (x1: a
 ,x2: a, x3: a): list_vt(a,3)
 //
-(*
 fun
 <a:vt>
 list_vt_make_ncpy
 {n:nat}
 (n0:sint(n), x0:a): list_vt(a,n)
-*)
 //
 fun
 <a:vt>

diff --git a/srcgen2/DATS/trsym2b_dynexp.dats b/srcgen2/DATS/trsym2b_dynexp.dats
@@ -727,17 +727,29 @@ endlet // end of [D2Etapp(...)]
 |
 D2Edapp
 (d2f0,npf1,d2es) =>
-(*
-HX-2023-07-07:
-Handling arguments first!
-*)
 let
-  val () =
-  trsym2b_d2exp(env0, d2f0)
+//
+val () =
+trsym2b_d2exp(env0, d2f0)
+//
 end where
 {
-  val () =
-  trsym2b_d2explst(env0, d2es)
+//
+(*
+val () =
+(
+ trsym2b_d2exp(env0, d2f0))
+*)
+//
+(*
+HX-2023-07-07:
+Handling the arguments first!
+*)
+//
+val () =
+(
+ trsym2b_d2explst(env0, d2es))
+//
 } (*where*) // end of [D2Edapp]
 //
 |

diff --git a/xatslib/githwxi/DATS/myfil00.dats b/xatslib/githwxi/DATS/myfil00.dats
@@ -50,6 +50,14 @@ end//let
 (* ****** ****** *)
 (* ****** ****** *)
 //
+#extern
+fun<>
+myfil00$myfil_make$opt_stdout
+  ( fpath: strn ): bool(*succ/fail*)
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)