Skip to content

Commit

Permalink
Updating: very very minorly
Browse files Browse the repository at this point in the history
  • Loading branch information
githwxi committed Sep 9, 2024
1 parent df77cfb commit 704287b
Show file tree
Hide file tree
Showing 5 changed files with 122 additions and 15 deletions.
12 changes: 12 additions & 0 deletions prelude/SATS/gbas000.sats
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,9 @@ Authoremail: gmhwxiATgmailDOTcom
//
(* ****** ****** *)
(* ****** ****** *)
#typedef ni = nint
(* ****** ****** *)
(* ****** ****** *)
//
fun
<a:t0>
Expand Down Expand Up @@ -65,6 +68,15 @@ fun
<a:t0>
g_test(x : a): bool
//
fun
<a0:t0>
g_iwork
(i0:ni,x0:a0): void
fun
<a0:t0>
g_itest
(i0:ni,x0:a0): bool
//
(* ****** ****** *)
(* ****** ****** *)
//
Expand Down
25 changes: 23 additions & 2 deletions xatslib/DATS/CATS/JS/Hsmap00.dats
Original file line number Diff line number Diff line change
Expand Up @@ -235,8 +235,8 @@ jshsmap_search$tst
//
#extern
fun<>
jshsmap_search$cpy
{k:t0}{x:vt}
jshsmap_search$opt
{k:t0}{x:t0} // HX: not(x:vt)
(map: jsm0(k,x), key: k): optn_vt(x)
//
(* ****** ****** *)
Expand Down Expand Up @@ -518,6 +518,27 @@ XATS2JS_jshsmap_search$tst
}
//
(* ****** ****** *)
//
#impltmp
<(*tmp*)>
jshsmap_search$opt
(map, key) =
let
val
test =
jshsmap_search$tst<>(map, key)
in//let
if
test
then
optn_vt_cons
(
UN_jshsmap_get$at$raw<>(map, key))
else
(optn_vt_nil( (*void*) ))
end//let//end-of-[jshsmap_search$opt]
//
(* ****** ****** *)
(* ****** ****** *)
//
#impltmp
Expand Down
12 changes: 11 additions & 1 deletion xatslib/githwxi/DATS/CATS/JS/myobj00.dats
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,17 @@ hmap_make_nil
//
#impltmp
< a: t0 >
hmap_insert$obj
hmap_search$opt
(map, k0) =
(
jshsmap_search$opt<>(map, k0))
//
(* ****** ****** *)
(* ****** ****** *)
//
#impltmp
< a: t0 >
hmap_insert$opt
(map, k0, x0) =
(
jshsmap_insert$opt<>(map, k0, x0))
Expand Down
80 changes: 71 additions & 9 deletions xatslib/githwxi/DATS/myobj00.dats
Original file line number Diff line number Diff line change
Expand Up @@ -45,16 +45,22 @@ hmap_make_nil((*0*)): hmap(a)
#extern
fun
<a:t0>
hmap_insert$opt
hmap_search$opt
( map
: hmap(a)
, k0: strn, x0: a): optn_vt(a)
: hmap(a), k0: strn): optn_vt(a)
//
(* ****** ****** *)
//
#extern
fun
<a:t0>
hmap_insert$opt
( map
: hmap(a)
, k0: strn, x0: a): optn_vt(a)
#extern
fun
<a:t0>
hmap_insert$new
( map
: hmap(a), k0: strn, x0: a): void
Expand Down Expand Up @@ -184,18 +190,19 @@ g_print
< dtval >
( dtv ) =
(
praux(dtv)) where
auxpr(dtv)) where
{
//
fun
praux
auxpr
(dtv: dtval): void =
let
//
#impltmp
g_print<dtval> = praux
g_print<dtval> = auxpr
//
in//let
//
case+ dtv of
//
|DTVunit(ut) =>
Expand All @@ -218,9 +225,29 @@ case+ dtv of
(
prints("DTVstrn(", s0, ")"))
//
end//let//end-of-[praux(dtv)]
|DTVa1sz(a0) =>
(
prints("DTVa1sz(", a0, ")"))
|DTVhmap(hm) =>
(
prints("DTVhmap(", hm, ")"))
//
}
|DTVf1un(f1) =>
(
prints("DTVf1un(", f1, ")"))
|DTVf2un(f2) =>
(
prints("DTVf2un(", f2, ")"))
|DTVf3un(f3) =>
(
prints("DTVf3un(", f3, ")"))
|DTVfxun(fx) =>
(
prints("DTVfxun(", fx, ")"))
//
end//let//end-of-[ auxpr(dtv) ]
//
}//where//end(g_print<dtval>(dtv)]
//
(* ****** ****** *)
//
Expand Down Expand Up @@ -299,13 +326,48 @@ let val-DTVfxun(fx) = dtv in fx end
(* ****** ****** *)
(* ****** ****** *)
//
#typedef myobj(*void*) = hmap(dtval)
#typedef
myobj(*void*) = hmap(dtval)
//
(* ****** ****** *)
(* ****** ****** *)
//
#extern
fun<>
myobj_get$at
(obj
:myobj, k0: strn): dtval
#extern
fun<>
myobj_get$at$opt
(obj
:myobj, k0: strn): optn_vt(dtval)
//
#impltmp
<(*tmp*)>
myobj_get$at
(obj, k0) =
(
case+ opt of
| ~optn_vt_cons(dtv) => dtv
) where
{
val opt =
myobj_get$at$opt<>(obj, k0) }
//
#impltmp
<(*tmp*)>
myobj_get$at$opt
(obj, k0) =
(
hmap_search$opt<>(obj, k0))
//
#symload [] with myobj_get$at of 1000
//
(* ****** ****** *)
//
#extern
fun<>
myobj_make_nil(): myobj
//
#impltmp
Expand Down
8 changes: 5 additions & 3 deletions xatslib/githwxi/TEST/CATS/JS/test07_myobj00.dats
Original file line number Diff line number Diff line change
Expand Up @@ -54,17 +54,19 @@ prints
//
(* ****** ****** *)
(* ****** ****** *)

//
val
obj0 = myobj_make_nil()
val () = prints("obj0 = ", obj0, "\n")
//
val () =
hmap_insert$new(obj0, "a", DTVsint(0))
hmap_insert$new(obj0, "a", DTVsint(1))
val () =
hmap_insert$new(obj0, "b", DTVsint(1))
hmap_insert$new(obj0, "b", DTVsint(2))
val () = prints("obj0 = ", obj0, "\n")
//
val () = prints
("a+b = ", sint(obj0["a"])+sint(obj0["b"]))
//
(* ****** ****** *)
(* ****** ****** *)
Expand Down

0 comments on commit 704287b

Please sign in to comment.