Updating: very very minorly

githwxi · Jul 30, 2023 · 9034f35 · 9034f35
1 parent db45f22
commit 9034f35
Show file tree

Hide file tree

Showing 10 changed files with 129 additions and 32 deletions.
diff --git a/srcgen2/DATS/trans3a_decl00.dats b/srcgen2/DATS/trans3a_decl00.dats
@@ -345,6 +345,9 @@ prerrln("f0_implmnt0(3a): d3cl = ", d3cl)
 //
 } (*where*) //end of [trans3a_d3ecl(env0,d3cl)]
 
+(* ****** ****** *)
+
+
 (* ****** ****** *)
 
 #implfun
@@ -362,11 +365,8 @@ d3valdcl_get_wsxp(dval)
 //
 val dpat =
 trans3a_d3pat(env0, dpat)
-//
-(*
-val tdxp = ...
-(*handled in trans3a_d3valdclist*)
-*)
+val tdxp =
+trans3a_teqd3exp(env0, tdxp)
 //
 in//let
 d3valdcl_make_args(loc0,dpat,tdxp,wsxp)

diff --git a/srcgen2/DATS/trans3a_dynexp.dats b/srcgen2/DATS/trans3a_dynexp.dats
@@ -311,6 +311,23 @@ end where
 //
 } (*where*)//end of [trans3a_f3arg(env0,farg)]
 
+(* ****** ****** *)
+//
+#implfun
+trans3a_teqd3exp
+  (env0, tdxp) =
+(
+case+ tdxp of
+|
+TEQD3EXPnone() =>
+TEQD3EXPnone((*void*))
+|
+TEQD3EXPsome(teq1, d3e2) =>
+TEQD3EXPsome(teq1, d3e2) where
+{ val
+  d3e2 = trans3a_d3exp(env0, d3e2) }
+) (*case+*)//end-of(trans3a_teqd3exp(...))
+//
 (* ****** ****** *)
 //
 #implfun

diff --git a/srcgen2/DATS/tread23_dynexp.dats b/srcgen2/DATS/tread23_dynexp.dats
@@ -1429,6 +1429,8 @@ d3e0.node() of
 |D3Et2pck _ => f0_t2pck(d3e0, err)
 //
 |D3Enone0 _ => f0_none0(d3e0, err)
+|D3Enone1 _ => f0_none1(d3e0, err)
+|D3Enone2 _ => f0_none2(d3e0, err)
 //
 | _(*otherwise*) =>
 let
@@ -2338,8 +2340,35 @@ fun
 f0_none0
 (d3e: d3exp
 ,err: &sint >> _): d3exp =
+let // HX: this is non-error
+val-D3Enone0() = d3e.node() in (d3e)
+end (*let*) // end of [f0_none0(d3e,err)]
+//
+(* ****** ****** *)
+//
+fun
+f0_none1
+(d3e: d3exp
+,err: &sint >> _): d3exp =
 let
-val-D3Enone0() = d3e.node() in (d3e) end
+val-
+D3Enone1(d2e1) = d3e.node()
+val lvl = 1 // HX: treated as error
+val d3e = d3exp_errck(lvl, d3e) in (d3e)
+end (*let*) // end of [f0_none1(d3e,err)]
+//
+(* ****** ****** *)
+//
+fun
+f0_none2
+(d3e: d3exp
+,err: &sint >> _): d3exp =
+let
+val-
+D3Enone2(d3e1) = d3e.node()
+val lvl = 1 // HX: treated as error
+val d3e = d3exp_errck(lvl, d3e) in (d3e)
+end (*let*) // end of [f0_none2(d3e,err)]
 //
 (* ****** ****** *)
 //

diff --git a/srcgen2/DATS/tread33_dynexp.dats b/srcgen2/DATS/tread33_dynexp.dats
@@ -146,6 +146,8 @@ f0_var(d3p0, err)
 |D3Pflt _ => d3p0
 |D3Pstr _ => d3p0
 //
+|D3Pcon _ => d3p0
+//
 | _(*otherwise*) =>
 let
 val lvl0 = 1
@@ -214,6 +216,8 @@ f0_var(d3e0, err)
 |D3Ef00 _ => d3e0
 |D3Es00 _ => d3e0
 //
+|D3Econ _ => d3e0
+|D3Ecst _ => d3e0
 |
 _(* otherwise *) =>
 let

diff --git a/srcgen2/SATS/trans3a.sats b/srcgen2/SATS/trans3a.sats
@@ -100,6 +100,9 @@ MAP = "./xsymmap.sats"
 #typedef
  s2typlst  =  $S2E.s2typlst
 (* ****** ****** *)
+#typedef
+ teqd3exp  =  $D3E.teqd3exp
+(* ****** ****** *)
 #typedef
  d3patlst  =  $D3E.d3patlst
 #typedef
@@ -123,16 +126,16 @@ MAP = "./xsymmap.sats"
 #typedef
  d3eclist  =  $D3E.d3eclist
 (* ****** ****** *)
-#typedef
- d3parsed  =  $D3E.d3parsed
-(* ****** ****** *)
 #typedef
  d3valdcl  =  $D3E.d3valdcl
 #typedef
  d3vardcl  =  $D3E.d3vardcl
 #typedef
  d3fundcl  =  $D3E.d3fundcl
 (* ****** ****** *)
+#typedef
+ d3parsed  =  $D3E.d3parsed
+(* ****** ****** *)
 #typedef
 d3valdclist = $D3E.d3valdclist
 #typedef
@@ -331,6 +334,13 @@ trans3a_d3ecl
 (* ****** ****** *)
 //
 fun
+trans3a_teqd3exp
+( env0:
+! tr3aenv,tdxp:teqd3exp):teqd3exp
+//
+(* ****** ****** *)
+//
+fun
 trans3a_d3eclist
 ( env0:
 ! tr3aenv,dcls:d3eclist):d3eclist

diff --git a/srcgen2/TEST/JS/DATA/QueenPuzzle.dats b/srcgen2/TEST/JS/DATA/QueenPuzzle.dats
@@ -16,14 +16,16 @@
 (* ****** ****** *)
 val N = 8
 (* ****** ****** *)
-////
 (* ****** ****** *)
-
 #abstype
 board_tbox <= p0tr
 #typedef
 board = board_tbox
-
+(* ****** ****** *)
+#staload
+"prelude/SATS/gseq000.sats"
+#staload
+"prelude/SATS/synoug0.sats"
 (* ****** ****** *)
 #extval
 fun
@@ -36,11 +38,6 @@ board_cons
 #symload nil with board_nil
 #symload cons with board_cons
 (* ****** ****** *)
-#staload
-"prelude/SATS/gseq000.sats"
-#staload
-"prelude/SATS/synoug0.sats"
-(* ****** ****** *)
 
 local
 

diff --git a/srcgen2/TEST/JS/test32_xatsopt.dats b/srcgen2/TEST/JS/test32_xatsopt.dats
@@ -327,18 +327,29 @@
 #include
 "./../../DATS/trans3a_myenv0.dats"
 #include
+"./../../DATS/trans3a_staexp.dats"
+#include
 "./../../DATS/trans3a_dynexp.dats"
 #include
 "./../../DATS/trans3a_decl00.dats"
 (* ****** ****** *)
 #include
 "./../../DATS/tread33.dats"
 #include
+"./../../DATS/tread33_staexp.dats"
+#include
 "./../../DATS/tread33_dynexp.dats"
 #include
 "./../../DATS/tread33_decl00.dats"
 (* ****** ****** *)
 #include
+"./../../DATS/fperr33.dats"
+#include
+"./../../DATS/fperr33_dynexp.dats"
+#include
+"./../../DATS/fperr33_decl00.dats"
+(* ****** ****** *)
+#include
 "./../../DATS/xatsopt.dats"
 #include
 "./../../DATS/xatsopt_utils0.dats"
@@ -360,39 +371,39 @@ val dpar =
 d3parsed_of_filsats
 ("./DATA/mysats.sats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 (* ****** ****** *)
 val dpar =
 d3parsed_of_fildats
 ("./DATA/mydats.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 (* ****** ****** *)
 ////
 (* ****** ****** *)
 val dpar =
 d3parsed_of_filsats
 ("./../../../prelude/SATS/arrn000.sats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 val dpar =
 d3parsed_of_filsats
 ("./../../../prelude/SATS/bool000.sats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 val dpar =
 d3parsed_of_filsats
 ("./../../../prelude/SATS/char000.sats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 val dpar =
 d3parsed_of_filsats
 ("./../../../prelude/SATS/gint000.sats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 ////
@@ -402,31 +413,31 @@ val dpar =
 d3parsed_of_fildats
 ("./../../../prelude/DATS/bool000.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 //
 val dpar =
 d3parsed_of_fildats
 ("./../../../prelude/DATS/char000.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 //
 val dpar =
 d3parsed_of_fildats
 ("./../../../prelude/DATS/gint000.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 //
 val dpar =
 d3parsed_of_fildats
 ("./../../../prelude/DATS/strn000.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 ////
@@ -436,15 +447,15 @@ val dpar =
 d3parsed_of_fildats
 ("./../../../prelude/DATS/optn000.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 //
 val dpar =
 d3parsed_of_fildats
 ("./../../../prelude/DATS/list000.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 //
 (* ****** ****** *)
 

diff --git a/srcgen2/TEST/JS/test33_xatsopt.dats b/srcgen2/TEST/JS/test33_xatsopt.dats
@@ -327,18 +327,29 @@
 #include
 "./../../DATS/trans3a_myenv0.dats"
 #include
+"./../../DATS/trans3a_staexp.dats"
+#include
 "./../../DATS/trans3a_dynexp.dats"
 #include
 "./../../DATS/trans3a_decl00.dats"
 (* ****** ****** *)
 #include
 "./../../DATS/tread33.dats"
 #include
+"./../../DATS/tread33_staexp.dats"
+#include
 "./../../DATS/tread33_dynexp.dats"
 #include
 "./../../DATS/tread33_decl00.dats"
 (* ****** ****** *)
 #include
+"./../../DATS/fperr33.dats"
+#include
+"./../../DATS/fperr33_dynexp.dats"
+#include
+"./../../DATS/fperr33_decl00.dats"
+(* ****** ****** *)
+#include
 "./../../DATS/xatsopt.dats"
 #include
 "./../../DATS/xatsopt_utils0.dats"
@@ -360,7 +371,7 @@ val dpar =
 d3parsed_of_fildats
 ("./DATA/mygseq.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 (* ****** ****** *)
 
 (* end of [ATS3/XATSOPT_TEST_JS_test33_xatsopt.dats] *)
diff --git a/srcgen2/TEST/JS/test34_xatsopt.dats b/srcgen2/TEST/JS/test34_xatsopt.dats
@@ -327,18 +327,29 @@
 #include
 "./../../DATS/trans3a_myenv0.dats"
 #include
+"./../../DATS/trans3a_staexp.dats"
+#include
 "./../../DATS/trans3a_dynexp.dats"
 #include
 "./../../DATS/trans3a_decl00.dats"
 (* ****** ****** *)
 #include
 "./../../DATS/tread33.dats"
 #include
+"./../../DATS/tread33_staexp.dats"
+#include
 "./../../DATS/tread33_dynexp.dats"
 #include
 "./../../DATS/tread33_decl00.dats"
 (* ****** ****** *)
 #include
+"./../../DATS/fperr33.dats"
+#include
+"./../../DATS/fperr33_dynexp.dats"
+#include
+"./../../DATS/fperr33_decl00.dats"
+(* ****** ****** *)
+#include
 "./../../DATS/xatsopt.dats"
 #include
 "./../../DATS/xatsopt_utils0.dats"
@@ -360,7 +371,7 @@ val dpar =
 d3parsed_of_fildats
 ("./DATA/mygflt.dats")
 val (  ) =
-d3parsed_fpemsg(g_stderr((*tmp*)), dpar)
+fperr33_d3parsed(g_stderr((*tmp*)), dpar)
 (* ****** ****** *)
 
 (* end of [ATS3/XATSOPT_TEST_JS_test34_xatsopt.dats] *)