Updating: very very minorly

githwxi · Sep 14, 2024 · 092c84b · 092c84b
1 parent 25521e1
commit 092c84b
Show file tree

Hide file tree

Showing 8 changed files with 124 additions and 45 deletions.
diff --git a/prelude/DATS/optn000.dats b/prelude/DATS/optn000.dats
@@ -75,7 +75,7 @@ gseq_nil
 optn_nil_
  ((*0*)) = optn_nil()
 #impltmp
-< x0:t0 >
+< a: t0 >
 optn_cons_
  (  x0  ) = optn_cons(x0)
 //
@@ -111,7 +111,7 @@ case+ xs of
 #impltmp
 { x0:t0 }
 gseq_head
-<optn(x0)><x0> = optn_nilq<x0>
+<optn(x0)><x0> = optn_head<x0>
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -160,13 +160,20 @@ gseq_print<optn(x0)><x0>(xs))
 (* ****** ****** *)
 //
 #impltmp
+< a: t0 >
+optn_make_1val = optn_cons_<a>
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+#impltmp
 < x0:t0 >
 optn_length
   (xs) =
 (
 case+ xs of
-| optn_nil() => 0
-| optn_cons(_, _) => 1)//impl
+| optn_nil( ) => 0
+| optn_cons(_) => 1)//impltmp
 //
 #impltmp
 { x0:t0 }

diff --git a/prelude/SATS/VT/list000_vt.sats b/prelude/SATS/VT/list000_vt.sats
@@ -98,11 +98,31 @@ list_vt_make_3val
 (* ****** ****** *)
 //
 #symload
-llist_sing with list_vt_make_1val
+list_vt_sing with list_vt_make_1val
 #symload
-llist_pair with list_vt_make_2val
+list_vt_pair with list_vt_make_2val
+//
+#symload
+list_vt_1val with list_vt_make_1val
+#symload
+list_vt_2val with list_vt_make_2val
+#symload
+list_vt_3val with list_vt_make_2val
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+fun
+<a:vt>
+list_vt_make_nfun
+{n:nat}
+(n0: sint(n)
+,f0: nintlt(n)->(a)): list_vt(a, n)
+//
+#symload
+list_vt with list_vt_make_nfun
 #symload
-llist_triple with list_vt_make_3val
+list_vt_make with list_vt_make_nfun
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -138,9 +158,9 @@ list_vt_make0_lstrq
 (xs: strq_vt(x0,n0)): list_vt(x0,n0)
 //
 #symload
-llist_make0 with list_vt_make0_lstrm
+list_vt_make0 with list_vt_make0_lstrm
 #symload
-llist_make0 with list_vt_make0_lstrq
+list_vt_make0 with list_vt_make0_lstrq
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -185,6 +205,16 @@ list_vt_append10
 //
 (* ****** ****** *)
 //
+#symload
+append0 with list_vt_append0 of 1000
+#symload
+append00 with list_vt_append00 of 1000
+#symload
+append10 with list_vt_append10 of 1000
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
 fun
 <x0:vt>
 list_vt_reverse0
@@ -196,33 +226,44 @@ list_vt_reverse1
 {n0:i0}
 (xs: !list_vt(x0,n0)): list_vt(x0,n0)
 //
-#symload reverse0 with list_reverse0 of 1000
-#symload reverse1 with list_reverse1 of 1000
+#symload
+reverse0 with list_vt_reverse0 of 1000
+#symload
+reverse1 with list_vt_reverse1 of 1000
 //
 (* ****** ****** *)
 //
 fun
 <x0:vt>
 list_vt_rappend0
 {n1,n2:i0}
-( xs: ~list_vt(x0,n1)
-, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+( xs
+: ~list_vt(x0,n1)
+, ys
+: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 fun
 <x0:vt>
 list_vt_rappend00
 {n1,n2:i0}
-( xs: ~list_vt(x0,n1)
-, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+( xs
+: ~list_vt(x0,n1)
+, ys
+: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 fun
 <x0:vt>
 list_vt_rappend10
 {n1,n2:i0}
-( xs: !list_vt(x0,n1)
-, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+( xs
+: !list_vt(x0,n1)
+, ys
+: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 //
-#symload rappend0 with list_rappend0 of 1000
-#symload rappend00 with list_rappend00 of 1000
-#symload rappend10 with list_rappend10 of 1000
+#symload
+rappend0 with list_vt_rappend0 of 1000
+#symload
+rappend00 with list_vt_rappend00 of 1000
+#symload
+rappend10 with list_vt_rappend10 of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/SATS/axrf000.sats b/prelude/SATS/axrf000.sats
@@ -94,11 +94,12 @@ a2rf_vt(x0:vt) = [m:i0;n:i0] a2rf_vt(x0,m,n)
 //
 fun
 <a:vt>
-a0rf_make_1val
-  (elem: a): a0rf(a)
+a0rf_make_1val(x1: a): a0rf(a)
 //
 #symload
-a0rf with a0rf_make_1val of 1000
+a0rf with a0rf_make_1val// of 1000
+#symload
+a0rf_1val with a0rf_make_1val// of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -151,7 +152,7 @@ a1rf_make_list
 (xs: list(a, n)): a1rf(a, n)
 //
 #symload
-a1rf with a1rf_make_list of 1000
+a1rf with a1rf_make_list//of 1000
 //
 (* ****** ****** *)
 //
@@ -169,13 +170,13 @@ a1rf_make_nfun
 , f0: nint(n) -> a): a1rf(a, n)
 //
 #symload
-a1rf with a1rf_make_ncpy of 1000
+a1rf with a1rf_make_ncpy//of 1000
 #symload
-a1rf with a1rf_make_nfun of 1000
+a1rf with a1rf_make_nfun//of 1000
 #symload
-array with a1rf_make_ncpy of 1000
+array with a1rf_make_ncpy//of 1000
 #symload
-array with a1rf_make_nfun of 1000
+array with a1rf_make_nfun//of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/SATS/axsz000.sats b/prelude/SATS/axsz000.sats
@@ -94,7 +94,7 @@ a1sz_make_list
 (xs: list(a, n)): a1sz(a, n)
 //
 #symload
-a1sz with a1sz_make_list of 1000
+a1sz with a1sz_make_list//of 1000
 //
 (* ****** ****** *)
 //
@@ -112,13 +112,13 @@ a1sz_make_nfun
 , f: nint(n) -> a): a1sz(a, n)
 //
 #symload
-a1sz with a1sz_make_ncpy of 1000
+a1sz with a1sz_make_ncpy//of 1000
 #symload
-a1sz with a1sz_make_nfun of 1000
+a1sz with a1sz_make_nfun//of 1000
 #symload
-arrsz with a1sz_make_ncpy of 1000
+arrsz with a1sz_make_ncpy//of 1000
 #symload
-arrsz with a1sz_make_nfun of 1000
+arrsz with a1sz_make_nfun//of 1000
 //
 (* ****** ****** *)
 //
@@ -134,9 +134,9 @@ a1sz_make_lstrq
 (xs:strq_vt(a, n)): a1sz(a, n)
 //
 #symload
-a1sz with a1sz_make_lstrm of 1000
+a1sz with a1sz_make_lstrm//of 1000
 #symload
-a1sz with a1sz_make_lstrq of 1000
+a1sz with a1sz_make_lstrq//of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/SATS/list000.sats b/prelude/SATS/list000.sats
@@ -140,10 +140,11 @@ fun
 <a:t0>
 list_make_nfun
 {n:nat}
-( x0: (a)
-, f0: nintlt(n)->(a)): list(a, n)
+(n0: sint(n)
+,f0: nintlt(n)->(a)): list(a, n)
+//
 #symload
-list with list_make_nfun of 1000
+list with list_make_nfun//of 1000
 #symload
 list_nfun with list_make_nfun//of 1000
 //
@@ -156,7 +157,8 @@ list_length
 {n:i0}
 (xs: list(a, n)): sint(n)
 //
-#symload length with list_length of 1000
+#symload
+length with list_length of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/SATS/optn000.sats b/prelude/SATS/optn000.sats
@@ -40,12 +40,10 @@ Authoremail: gmhwxiATgmailDOTcom
 //
 fun<>
 optn_nil_
-{a:t0}
-((*0*)): optn(a,ff)
+{a:t0}((*0*)): optn(a,ff)
 fun
 <a:t0>
-optn_cons_
-(x0:(a)): optn(a,tt)
+optn_cons_(x0:(a)): optn(a,tt)
 //
 (* ****** ****** *)
 //
@@ -65,6 +63,19 @@ optn_head
 #symload head with optn_head of 1000
 //
 (* ****** ****** *)
+(* ****** ****** *)
+//
+fun
+<a:t0>
+optn_make_1val(a): optn(a,tt)
+//
+#symload
+optn with optn_make_1val// of 1000
+#symload
+optn_1val with optn_make_1val// of 1000
+//
+(* ****** ****** *)
+(* ****** ****** *)
 //
 (*
 HX-2024-09-07:

diff --git a/srcgen1/prelude/SATS/gseq000.sats b/srcgen1/prelude/SATS/gseq000.sats
@@ -113,6 +113,15 @@ gseq_copy(xs): (xs)
 fun
 <xs:t0>
 <x0:t0>
+gseq_head(xs): x0
+fun
+<xs:t0>
+<x0:t0>
+gseq_tail(xs): xs
+//
+fun
+<xs:t0>
+<x0:t0>
 gseq_head$exn(xs): x0
 fun
 <xs:t0>

diff --git a/srcgen1/prelude/SATS/optn000.sats b/srcgen1/prelude/SATS/optn000.sats
@@ -36,7 +36,8 @@
 // Authoremail: gmhwxiATgmailDOTcom
 //
 (* ****** ****** *)
-
+(* ****** ****** *)
+//
 fun<>
 optn_nil_
 {a:t0}
@@ -45,7 +46,14 @@ fun
 <a:t0>
 optn_cons_
 (x0: a): optn(a, tt)
-
+//
+(* ****** ****** *)
+//
+fun
+<a:t0>
+optn_make_1val
+(x0: a): optn(a, tt)
+//
 (* ****** ****** *)
 //
 fun<>