From 44d2fa9136c5bb9ab430f3962303a3907d956531 Mon Sep 17 00:00:00 2001 From: Hongwei Date: Sat, 31 Aug 2024 00:31:42 -0400 Subject: [PATCH] Updating: very very minorly --- prelude/DATS/gdbg000.dats | 85 ---------------------- prelude/DATS/gfun000.dats | 115 ++++++++++++++++++++++++++++++ prelude/SATS/gdbg000.sats | 62 ---------------- prelude/SATS/gfun000.sats | 100 ++++++++++++++++++++++++++ srcgen1/prelude/SATS/gfun000.sats | 26 +++++++ srcgen2/DATS/dynexp3_utils0.dats | 17 ++--- 6 files changed, 250 insertions(+), 155 deletions(-) diff --git a/prelude/DATS/gdbg000.dats b/prelude/DATS/gdbg000.dats index 4d59d6693..e67dcb2fb 100644 --- a/prelude/DATS/gdbg000.dats +++ b/prelude/DATS/gdbg000.dats @@ -211,91 +211,6 @@ g_ptype();pstrn":";g_psort()) (* ****** ****** *) (* ****** ****** *) // -(* -HX-2024-08-24: -Sat 24 Aug 2024 06:29:59 PM EDT -*) -// -#impltmp -< r0:vt > -f_trace_f0un - (msg, f00) = -lam((*0*)) => let -// -val () = -prints(msg, ":", "\n") -// -val r0 = f00( ) -// -val () = print1s -(msg, ": res0 = ", r0, "\n") in r0 end -// -(* ****** ****** *) -// -#impltmp -< a1:t0 > -< r0:vt > -f_trace_f1un - (msg, f00) = -lam(x1:a1) => let -// -val () = prints -(msg, ": arg1 = ", x1, "\n") -// -val r0 = f00( x1 ) -// -val () = print1s -(msg, ": res0 = ", r0, "\n") in r0 end -// -(* ****** ****** *) -// -#impltmp -< a1:t0 > -< a2:t0 > -< r0:vt > -f_trace_f2un - (msg, f00) = -lam -(x1:a1,x2:a2) => let -// -val () = prints -(msg, ": arg1 = ", x1, "\n") -val () = prints -(msg, ": arg2 = ", x2, "\n") -// -val r0 = f00( x1, x2 ) -// -val () = print1s -(msg, ": res0 = ", r0, "\n") in r0 end -// -(* ****** ****** *) -// -#impltmp -< a1:t0 > -< a2:t0 > -< a3:t0 > -< r0:vt > -f_trace_f3un - (msg, f00) = -lam -(x1:a1 -,x2:a2,x3:a3) => let -// -val () = prints -(msg, ": arg1 = ", x1, "\n") -val () = prints -(msg, ": arg2 = ", x2, "\n") -val () = prints -(msg, ": arg3 = ", x3, "\n") -// -val r0 = f00( x1, x2, x3 ) -// -val () = print1s -(msg, ": res0 = ", r0, "\n") in r0 end -// -(* ****** ****** *) -(* ****** ****** *) -// (* ****** ****** *)(* ****** ****** *) (* ****** ****** *)(* ****** ****** *) diff --git a/prelude/DATS/gfun000.dats b/prelude/DATS/gfun000.dats index f189b9546..3e5c5b628 100644 --- a/prelude/DATS/gfun000.dats +++ b/prelude/DATS/gfun000.dats @@ -100,6 +100,121 @@ foritm$work(_) = f0((*void*)) (* ****** ****** *) (* ****** ****** *) // +// +(* +HX-2024-08-24: +Sat 24 Aug 2024 06:29:59 PM EDT +*) +// +#impltmp +< r0:vt > +f_trace_f0un + (msg, f00) = +lam((*0*)) => let +// +val () = +prints(msg, ":", "\n") +// +val r0 = f00( ) +// +val () = print1s +(msg, ": res0 = ", r0, "\n") in r0 end +// +(* ****** ****** *) +// +#impltmp +< a1:t0 > +< r0:vt > +f_trace_f1un + (msg, f00) = +lam(x1:a1) => let +// +val () = prints +(msg, ": arg1 = ", x1, "\n") +// +val r0 = f00( x1 ) +// +val () = print1s +(msg, ": res0 = ", r0, "\n") in r0 end +// +(* ****** ****** *) +// +#impltmp +< a1:t0 > +< a2:t0 > +< r0:vt > +f_trace_f2un + (msg, f00) = +lam +(x1:a1,x2:a2) => let +// +val () = prints +(msg, ": arg1 = ", x1, "\n") +val () = prints +(msg, ": arg2 = ", x2, "\n") +// +val r0 = f00( x1, x2 ) +// +val () = print1s +(msg, ": res0 = ", r0, "\n") in r0 end +// +(* ****** ****** *) +// +#impltmp +< a1:t0 > +< a2:t0 > +< a3:t0 > +< r0:vt > +f_trace_f3un + (msg, f00) = +lam +(x1:a1 +,x2:a2,x3:a3) => let +// +val () = prints +(msg, ": arg1 = ", x1, "\n") +val () = prints +(msg, ": arg2 = ", x2, "\n") +val () = prints +(msg, ": arg3 = ", x3, "\n") +// +val r0 = f00( x1, x2, x3 ) +// +val () = print1s +(msg, ": res0 = ", r0, "\n") in r0 end +// +(* ****** ****** *) +// +#impltmp +< a1:t0 > +< a2:t0 > +< a3:t0 > +< a4:t0 > +< r0:vt > +f_trace_f4un + (msg, f00) = +lam +(x1:a1 +,x2:a2 +,x3:a3,x4:a4) => let +// +val () = prints +(msg, ": arg1 = ", x1, "\n") +val () = prints +(msg, ": arg2 = ", x2, "\n") +val () = prints +(msg, ": arg3 = ", x3, "\n") +val () = prints +(msg, ": arg4 = ", x3, "\n") +// +val r0 = f00(x1, x2, x3, x4) +// +val () = print1s +(msg, ": res0 = ", r0, "\n") in r0 end +// +(* ****** ****** *) +(* ****** ****** *) +// (* ****** ****** *)(* ****** ****** *) (* ****** ****** *)(* ****** ****** *) diff --git a/prelude/SATS/gdbg000.sats b/prelude/SATS/gdbg000.sats index ef9038fc7..9e2669c7d 100644 --- a/prelude/SATS/gdbg000.sats +++ b/prelude/SATS/gdbg000.sats @@ -104,68 +104,6 @@ g_ptype((*void*)): ( void ) (* ****** ****** *) (* ****** ****** *) // -(* -HX-2024-08-24: -Sat 24 Aug 2024 06:29:26 PM EDT -*) -// -#typedef -f0un(r0:vt) = () -> r0 -// -#typedef -f1un -(a1:t0,r0:vt) = (a1) -> r0 -// -#typedef -f2un -(a1:t0 -,a2:t0,r0:vt) = (a1,a2) -> r0 -// -#typedef -f3un -(a1:t0 -,a2:t0 -,a3:t0,r0:vt) = (a1,a2,a3) -> r0 -// -(* ****** ****** *) -// -fun - -f_trace_f0un -(msg: strn -,f00: f0un(r0)): f0un(r0) -fun - - -f_trace_f1un -(msg: strn -,f00: f1un(a1,r0)): f1un(a1,r0) -fun - - - -f_trace_f2un -(msg: strn -,f00: f2un(a1,a2,r0)): f2un(a1,a2,r0) -fun - - - - -f_trace_f3un -(msg: strn -,f00: f3un(a1,a2,a3,r0)): f3un(a1,a2,a3,r0) -// -(* ****** ****** *) -// -#symload trace with f_trace_f0un of 1000 -#symload trace with f_trace_f1un of 1000 -#symload trace with f_trace_f2un of 1000 -#symload trace with f_trace_f3un of 1000 -// -(* ****** ****** *) -(* ****** ****** *) -// (* ****** ****** *)(* ****** ****** *) (* ****** ****** *)(* ****** ****** *) diff --git a/prelude/SATS/gfun000.sats b/prelude/SATS/gfun000.sats index 06c62da38..4ad526270 100644 --- a/prelude/SATS/gfun000.sats +++ b/prelude/SATS/gfun000.sats @@ -73,6 +73,24 @@ f4un ,a3:t0 ,a4:t0,r0:vt) = (a1,a2,a3,a4)->r0 (* ****** ****** *) +#typedef +f5un +(a1:t0 +,a2:t0 +,a3:t0 +,a4:t0 +,a5:t0,r0:vt) = (a1,a2,a3,a4,a5)->r0 +(* ****** ****** *) +#typedef +f6un +(a1:t0 +,a2:t0 +,a3:t0 +,a4:t0 +,a5:t0 +,a6:t0,r0:vt) = (a1,a2,a3,a4,a5,a6)->r0 +(* ****** ****** *) +(* ****** ****** *) // fun @@ -83,6 +101,7 @@ f1un_not #symload not with f1un_not of 1000 // (* ****** ****** *) +(* ****** ****** *) // fun<> f0un_repeat_nint @@ -96,6 +115,7 @@ nint_repeat_f0un #symload repeat with nint_repeat_f0un // (* ****** ****** *) +(* ****** ****** *) // fun @@ -110,6 +130,7 @@ fun f1un_srch$make_gseq(xs): f1un(x0,bool) // (* ****** ****** *) +(* ****** ****** *) // (* HX: for run-time testing @@ -134,6 +155,85 @@ f1un_rand$equal (* ****** ****** *) (* ****** ****** *) // +fun + +f_trace_f0un +(msg: strn +,f00: f0un(r0)): f0un(r0) +fun + + +f_trace_f1un +(msg: strn +,f00: f1un(a1,r0)): f1un(a1,r0) +fun + + + +f_trace_f2un +(msg: strn +,f00: f2un(a1,a2,r0)): f2un(a1,a2,r0) +fun + + + + +f_trace_f3un +(msg: strn +,f00: f3un(a1,a2,a3,r0)): f3un(a1,a2,a3,r0) +// +(* ****** ****** *) +// +fun + + + + + +f_trace_f4un +(msg: strn +,f00: f4un(a1,a2,a3,a4,r0)): f4un(a1,a2,a3,a4,r0) +// +(* ****** ****** *) +// +fun + + + + + + +f_trace_f5un +(msg: strn +,f00: f5un(a1,a2,a3,a4,a5,r0)): f5un(a1,a2,a3,a4,a5,r0) +// +(* ****** ****** *) +// +fun + + + + + + + +f_trace_f6un +(msg: strn +,f00: f6un(a1,a2,a3,a4,a5,a6,r0)): f6un(a1,a2,a3,a4,a5,a6,r0) +// +(* ****** ****** *) +// +#symload trace with f_trace_f0un of 1000 +#symload trace with f_trace_f1un of 1000 +#symload trace with f_trace_f2un of 1000 +#symload trace with f_trace_f3un of 1000 +#symload trace with f_trace_f4un of 1000 +#symload trace with f_trace_f5un of 1000 +#symload trace with f_trace_f6un of 1000 +// +(* ****** ****** *) +(* ****** ****** *) +// (* ****** ****** *)(* ****** ****** *) (* ****** ****** *)(* ****** ****** *) diff --git a/srcgen1/prelude/SATS/gfun000.sats b/srcgen1/prelude/SATS/gfun000.sats index 9cf78710e..8b5ca0253 100644 --- a/srcgen1/prelude/SATS/gfun000.sats +++ b/srcgen1/prelude/SATS/gfun000.sats @@ -24,6 +24,32 @@ f3un ,a3:t0,r0:vt) = (a1,a2,a3) -> r0 // (* ****** ****** *) +// +#typedef +f4un +(a1:t0 +,a2:t0 +,a3:t0 +,a4:t0,r0:vt) = (a1,a2,a3,a4)->r0 +// +#typedef +f5un +(a1:t0 +,a2:t0 +,a3:t0 +,a4:t0 +,a5:t0,r0:vt) = (a1,a2,a3,a4,a5)->r0 +// +#typedef +f6un +(a1:t0 +,a2:t0 +,a3:t0 +,a4:t0 +,a5:t0 +,a6:t0,r0:vt) = (a1,a2,a3,a4,a5,a6)->r0 +// +(* ****** ****** *) (* ****** ****** *) // fun diff --git a/srcgen2/DATS/dynexp3_utils0.dats b/srcgen2/DATS/dynexp3_utils0.dats index c1bbec84e..a3f3eb2f2 100644 --- a/srcgen2/DATS/dynexp3_utils0.dats +++ b/srcgen2/DATS/dynexp3_utils0.dats @@ -715,6 +715,7 @@ tip1.node() of g2_trcd_tjp1(tip1, tjp1)) // |T2Pnone0((*0*)) => ( true ) +// |T2Pnone1(s2typ) => ( true ) |T2Ps2exp(s2exp) => ( true ) // @@ -905,11 +906,11 @@ end(*let*)//end of [g2_trcd_tjp1(...)] // (* val () = -prerrln -("f0_targequ:f2_tip1_tjp1: tip1 = ", tip1) +prerrln("\ +f0_targequ:f2_tip1_tjp1: tip1 = ", tip1) val () = -prerrln -("f0_targequ:f2_tip1_tjp1: tjp1 = ", tjp1) +prerrln("\ +f0_targequ:f2_tip1_tjp1: tjp1 = ", tjp1) *) // (* ****** ****** *) @@ -1546,11 +1547,11 @@ end(*let*)//end of [g2_trcd_tjp1(...)] // (* val () = -prerrln -("f0_targmat:f2_tip1_tjp1: tip1 = ", tip1) +prerrln("\ +f0_targmat:f2_tip1_tjp1: tip1 = ", tip1) val () = -prerrln -("f0_targmat:f2_tip1_tjp1: tjp1 = ", tjp1) +prerrln("\ +f0_targmat:f2_tip1_tjp1: tjp1 = ", tjp1) *) // (* ****** ****** *)