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 Oct 5, 2024
1 parent 76eceeb commit 0461518
Showing 1 changed file with 35 additions and 7 deletions.
42 changes: 35 additions & 7 deletions srcgen2/DATS/statyp2_tmplib.dats
Original file line number Diff line number Diff line change
Expand Up @@ -1316,6 +1316,8 @@ s2typ_subst0
s2typ_subst0_e1nv<e1nv>(e1nv,t2p0,svts)
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
s2typ_exi0_abst
( e1nv: !e1nv
Expand All @@ -1324,6 +1326,8 @@ fun
s2typ_uni0_abst
( e1nv: !e1nv
, t2p0: s2typ): s2typ = t2p0
//
(* ****** ****** *)
(* ****** ****** *)
//
local
Expand All @@ -1349,7 +1353,7 @@ map$fopr
<x0><y0>(s2v1) =
@(s2v1, s2typ_xtv(x2t2p_make()))
//
}(*where*)//end of [f0_inst_s2vs]
}(*where*)//end of [f0_inst_s2vs(s2vs)]
//
in//local
//
Expand All @@ -1372,7 +1376,9 @@ e1nv,
s2typ_subst0(e1nv,t2p1,svts) )
endlet // end of [T2Pexi0(...)]
| _(* non-T2Pexi0 *) => ( t2p0 )
)(*case+*)//end-of-[s2typ_exi0_inst]
)(*case+*)//end-of-[s2typ_exi0_inst(...)]
//
(* ****** ****** *)
//
fun
s2typ_uni0_inst
Expand All @@ -1393,11 +1399,12 @@ e1nv,
s2typ_subst0(e1nv,t2p1,svts) )
endlet // end of [T2Puni0(...)]
| _(* non-T2Puni0 *) => ( t2p0 )
)(*case+*)//end-of-[s2typ_uni0_inst]
)(*case+*)//end-of-[s2typ_uni0_inst(...)]
//
endloc // end-of-[s2typ_exi0/uni0_inst]
endloc // end-of-[s2typ_exi0/uni0_inst(...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
unify00_s2typ
Expand Down Expand Up @@ -1512,6 +1519,7 @@ t2p2.node() of
{
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f1_xset
Expand All @@ -1531,29 +1539,34 @@ unify00_s2typ$xset<>(xtp1, t2p2)
end (*let*) // end of [f1_xset(...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f0_xtv1
( e1nv: !e1nv
, t2p1: s2typ
, t2p2: s2typ): (bool) =
let
//
val-
T2Pxtv(xtp1) = t2p1.node()
//
in//let
//
case+
t2p2.node() of
|T2Pxtv(xtp2) =>
if
(xtp1 = xtp2)
then true else
(f1_xset(xtp1, t2p2); true)
(f1_xset(xtp1, t2p2); true)//endof(IF)
|_(*non-T2Pxtv*) =>
if
s2typ_xtpck0
( t2p2, xtp1 )
then false else
(f1_xset(xtp1, t2p2); true)
(f1_xset(xtp1, t2p2); true)//endof(IF)
//
end (*let*) // end of [f0_xtv1(e1nv,...)]
//
(* ****** ****** *)
Expand All @@ -1564,17 +1577,22 @@ f0_xtv2
, t2p1: s2typ
, t2p2: s2typ): (bool) =
let
//
val-
T2Pxtv(xtp2) = t2p2.node()
//
in//let
//
if
s2typ_xtpck0
( t2p1, xtp2 )
then false else
(f1_xset(xtp2, t2p1); true)
(f1_xset(xtp2, t2p1); true)//endof(IF)
//
end (*let*) // end of [f0_xtv2(e1nv,...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f0_top0
Expand All @@ -1595,6 +1613,8 @@ unify00_s2typ(e1nv, tp11, tp21)
//
end (*let*) // end of [f0_top0(e1nv,...)]
//
(* ****** ****** *)
//
fun
f0_top1
( e1nv: !e1nv
Expand All @@ -1615,6 +1635,7 @@ unify00_s2typ(e1nv, tp11, tp21)
end (*let*) // end of [f0_top1(e1nv,...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f0_apps
Expand Down Expand Up @@ -1647,6 +1668,7 @@ end (*let*) // end of [T2Papps(...)]
end (*let*) // end of [f0_apps(e1nv,...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f0_fun1
Expand Down Expand Up @@ -1681,6 +1703,7 @@ end (*let*) // end of [T2Pfun1(...)]
end (*let*) // end of [f0_fun1(e1nv,...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f0_text
Expand Down Expand Up @@ -1709,6 +1732,7 @@ unify00_s2typlst
end (*let*) // end of [f0_text(e1nv,...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
fun
f0_trcd
Expand Down Expand Up @@ -1740,6 +1764,7 @@ unify00_l2t2plst
end (*let*) // end of [f0_trcd(e1nv,...)]
//
(* ****** ****** *)
(* ****** ****** *)
//
val
t2p1 =
Expand All @@ -1749,13 +1774,15 @@ t2p2 =
unify00_s2typ$hnfz(e1nv, t2p2)
//
(* ****** ****** *)
(* ****** ****** *)
//
val
t2p1 = s2typ_uni0_inst(e1nv, t2p1)
val
t2p2 = s2typ_exi0_inst(e1nv, t2p2)
//
(* ****** ****** *)
(* ****** ****** *)
//
(*
val ( ) =
Expand All @@ -1765,6 +1792,7 @@ prerrsln("unify00_s2typ: t2p2 = ", t2p2)
*)
//
(* ****** ****** *)
(* ****** ****** *)
//
} (*where*) // end of [unify00_s2typ(e1nv,...)]
//
Expand Down

0 comments on commit 0461518

Please sign in to comment.