Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Updating: minor.

  • Loading branch information...
commit d5f0dc800d622b41fc0459847818251fee1875dc 1 parent b2478e0
Hongwei Xi authored
Showing with 33 additions and 12 deletions.
  1. +22 −12 prelude/DATS/dlist_vt.dats
  2. +11 −0 prelude/SATS/dlist_vt.sats
View
34 prelude/DATS/dlist_vt.dats
@@ -121,36 +121,46 @@ end // end of [dlist_vt_set]
(* ****** ****** *)
implement{a}
-dlist_vt_is_end
+dlist_vt_is_beg
{f,r} (xs) = let
- val+ DLISTcons
- (_, _, !p_xs1) = xs
- val next = dlist2ptr (!p_xs1)
+ val+ DLISTcons (_, prev, _) = xs
prval () = fold@ (xs)
val [b:bool] ans = (
- if next > null then false else true
+ if prev > null then false else true
) : Bool // end of [val]
prval () = __assert () where {
- extern praxi __assert (): [b==(r==1)] void
+ extern praxi __assert (): [b==(f==0)] void
} // end of [prval]
in
ans
-end // end of [dlist_vt_is_end]
+end // end of [dlist_vt_is_beg]
implement{a}
-rdlist_vt_is_end
+dlist_vt_is_end
{f,r} (xs) = let
- val+ DLISTcons (_, prev, _) = xs
+ val+ DLISTcons
+ (_, _, !p_xs1) = xs
+ val next = dlist2ptr (!p_xs1)
prval () = fold@ (xs)
val [b:bool] ans = (
- if prev > null then false else true
+ if next > null then false else true
) : Bool // end of [val]
prval () = __assert () where {
- extern praxi __assert (): [b==(f==0)] void
+ extern praxi __assert (): [b==(r==1)] void
} // end of [prval]
in
ans
-end // end of [rdlist_vt_is_end]
+end // end of [dlist_vt_is_end]
+
+implement{a}
+rdlist_vt_is_beg
+ {f,r} (xs) = dlist_vt_is_end {f,r} (xs)
+// end of [rdlist_vt_is_beg]
+
+implement{a}
+rdlist_vt_is_end
+ {f,r} (xs) = dlist_vt_is_beg {f,r} (xs)
+// end of [rdlist_vt_is_end]
(* ****** ****** *)
View
11 prelude/SATS/dlist_vt.sats
@@ -84,10 +84,21 @@ dlist_vt_snoc {f:int}
(* ****** ****** *)
fun{a:vt0p}
+dlist_vt_is_beg
+ {f,r:int | r > 0}
+ (xs: !dlist_vt (a, f, r)):<> bool (f==0)
+// end of [dlist_vt_is_beg]
+fun{a:vt0p}
dlist_vt_is_end
{f,r:int | r > 0}
(xs: !dlist_vt (a, f, r)):<> bool (r==1)
// end of [dlist_vt_is_end]
+
+fun{a:vt0p}
+rdlist_vt_is_beg
+ {f,r:int | r > 0}
+ (xs: !dlist_vt (a, f, r)):<> bool (r==1)
+// end of [rdlist_vt_is_end]
fun{a:vt0p}
rdlist_vt_is_end
{f,r:int | r > 0}
Please sign in to comment.
Something went wrong with that request. Please try again.