Skip to content

Instantly share code, notes, and snippets.

@doublec
Created October 3, 2012 11:26
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save doublec/3826469 to your computer and use it in GitHub Desktop.
ATS stack example
all: stack1 stack2 stack3 stack4 stack5
stack1: stack1.dats
atscc -o stack1 stack1.dats
stack2: stack2.dats
atscc -o stack2 stack2.dats
stack3: stack3.dats
atscc -tc stack3.dats
stack4: stack4.dats
atscc -o stack4 stack4.dats
stack5: stack5.dats
atscc -o stack5 stack5.dats
datatype stack =
| stack_nil
| stack_cons of (int, stack)
extern fun stack_new (): stack
extern fun stack_is_empty (s: stack): bool
extern fun stack_top (s: stack): int
extern fun stack_pop (s: &stack): void
extern fun stack_push (s: &stack, x: int): void
implement stack_new () = stack_nil ()
implement stack_is_empty (s) =
case+ s of
| stack_nil () => true
| stack_cons _ => false
implement stack_push (s, x) = (s := stack_cons (x, s))
implement stack_top (s) =
case+ s of
| stack_nil () => (assertloc (false); 0)
| stack_cons (x,_) => x
implement stack_pop (s) =
case+ s of
| stack_nil () => assertloc (false)
| stack_cons (_, xs) => s := xs
implement main () = {
var s1 = stack_new ()
val a = stack_is_empty (s1)
val () = stack_push (s1, 10)
val b = stack_is_empty (s1)
val c = stack_top (s1)
val () = stack_pop (s1)
val d = stack_is_empty (s1)
val () = printf("a=%s b=%s c=%d d=%s\n", @(if a then "true" else "false",
if b then "true" else "false",
c,
if d then "true" else "false"))
}
datatype stack (bool) =
| stack_nil (true)
| {b:bool} stack_cons (false) of (int, stack b)
extern fun stack_new (): stack true
extern fun stack_is_empty {b:bool} (s: stack b): bool b
extern fun stack_top {b:bool} (s: stack false): int
extern fun stack_pop (s: &stack false >> stack b): #[b:bool] void
extern fun stack_push {b:bool} (s: &stack b >> stack false, x: int): void
implement stack_new () = stack_nil ()
implement stack_is_empty (s) =
case+ s of
| stack_nil () => true
| stack_cons _ => false
implement stack_push (s, x) = (s := stack_cons (x, s))
implement stack_top (s) = let
val+ stack_cons (x,_) = s
in
x
end
implement stack_pop (s) = let
val+ stack_cons (_, xs) = s
in
s := xs
end
fun mustcheck {b:bool} (s: stack b): void = {
val () = assertloc (not (stack_is_empty (s)))
val c = stack_top (s)
}
fun nocheck {b:bool} (s: &stack b >> stack false): void = {
val () = stack_push (s, 42)
val c = stack_top (s)
}
implement main () = {
var s1 = stack_new ()
val a = stack_is_empty (s1)
val () = stack_push (s1, 10)
val b = stack_is_empty (s1)
val c = stack_top (s1)
val () = stack_pop (s1)
val d = stack_is_empty (s1)
val () = printf("a=%s b=%s c=%d d=%s\n", @(if a then "true" else "false",
if b then "true" else "false",
c,
if d then "true" else "false"))
}
datasort ilist =
| inil
| icons of (int, ilist)
dataprop EMPTY (ilist) =
| EMPTY (inil)
dataprop IS_EMPTY (ilist, bool) =
| IS_EMPTY_true (inil, true)
| {x:int} {xs:ilist} IS_EMPTY_false (icons (x,xs), false)
dataprop TOP (ilist, int) =
| {x:int} {xs:ilist} TOP (icons (x,xs), x)
dataprop PUSH (ilist, int, ilist) =
| {x:int} {xs,ys:ilist} PUSH (xs, x, icons (x, xs))
dataprop POP (ilist, ilist) =
| {x:int} {xs:ilist} POP (icons (x,xs), xs)
prfun stack_push_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> TOP (ys, x) = let
prval PUSH () = pf
in
TOP ()
end
prfun stack_pop_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> POP (ys, xs) = let
prval PUSH () = pf
in
POP ()
end
prfun stack_empty_check {xs:ilist} .<>. (pf: EMPTY xs):<> IS_EMPTY (xs, true) = let
prval EMPTY () = pf
in
IS_EMPTY_true ()
end
datasort ilist =
| inil
| icons of (int, ilist)
dataprop EMPTY (ilist) =
| EMPTY (inil)
dataprop IS_EMPTY (ilist, bool) =
| IS_EMPTY_true (inil, true)
| {x:int} {xs:ilist} IS_EMPTY_false (icons (x,xs), false)
dataprop TOP (ilist, int) =
| {x:int} {xs:ilist} TOP (icons (x,xs), x)
dataprop PUSH (ilist, int, ilist) =
| {x:int} {xs,ys:ilist} PUSH (xs, x, icons (x, xs))
dataprop POP (ilist, ilist) =
| {x:int} {xs:ilist} POP (icons (x,xs), xs)
prfun stack_push_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> TOP (ys, x) = let
prval PUSH () = pf
in
TOP ()
end
prfun stack_pop_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> POP (ys, xs) = let
prval PUSH () = pf
in
POP ()
end
prfun stack_empty_check {xs:ilist} .<>. (pf: EMPTY xs):<> IS_EMPTY (xs, true) = let
prval EMPTY () = pf
in
IS_EMPTY_true ()
end
datatype stack (ilist) =
| stack_nil (inil)
| {x:int} {xs:ilist} stack_cons (icons (x,xs)) of (int x, stack xs)
extern fun stack_new (): [xs:ilist] (EMPTY xs | stack xs)
extern fun stack_is_empty {xs:ilist} (s: stack xs): [b:bool] (IS_EMPTY (xs, b) | bool b)
extern fun stack_top {xs:ilist} (pf: IS_EMPTY (xs, false) | s: stack xs): [x:int] (TOP (xs, x) | int x)
extern fun stack_pop {x:int} {xs:ilist} (pf: IS_EMPTY (xs, false) | s: &stack xs >> stack ys): #[ys:ilist] (POP (xs, ys) | void)
extern fun stack_push {x:int} {xs:ilist} (s: &stack xs >> stack ys, x: int x): #[ys:ilist] (PUSH (xs, x, ys) | void)
implement stack_new () = (EMPTY () | stack_nil ())
implement stack_is_empty (s) =
case+ s of
| stack_nil () => (IS_EMPTY_true | true)
| stack_cons _ => (IS_EMPTY_false | false)
implement stack_push {x} {xs} (s, x) = (PUSH () | (s := stack_cons (x, s)))
implement stack_top (pf | s) = let
prval IS_EMPTY_false () = pf
val+ stack_cons (x,_) = s
in
(TOP () | x)
end
implement stack_pop (pf | s) = let
prval IS_EMPTY_false () = pf
val+ stack_cons (_, xs) = s
in
(POP () | s := xs)
end
fun mustcheck {xs:ilist} (s: stack xs): void = {
val (pf | e) = stack_is_empty (s)
val () = assertloc (not e)
val (_ | c) = stack_top (pf | s)
}
fun nocheck {xs:ilist} (s: &stack xs >> stack ys): #[ys:ilist] void = {
val (pf | ()) = stack_push (s, 42)
prval PUSH () = pf
val (_ | c) = stack_top (IS_EMPTY_false () | s)
}
implement main () = {
val (_ | s) = stack_new ()
var s1 = s
val (_ | a) = stack_is_empty (s1)
val (pf | ()) = stack_push (s1, 10)
prval PUSH () = pf
val (_ | b) = stack_is_empty (s1)
val (_ | c) = stack_top (IS_EMPTY_false () | s1)
val (pf | ()) = stack_pop (IS_EMPTY_false () | s1)
prval POP () = pf
val (_ | d) = stack_is_empty (s1)
val () = printf("a=%s b=%s c=%d d=%s\n", @(if a then "true" else "false",
if b then "true" else "false",
c,
if d then "true" else "false"))
}
datasort ilist =
| inil
| icons of (int, ilist)
dataprop EMPTY (ilist) =
| EMPTY (inil)
dataprop IS_EMPTY (ilist, bool) =
| IS_EMPTY_true (inil, true)
| {x:int} {xs:ilist} IS_EMPTY_false (icons (x,xs), false)
dataprop TOP (ilist, int) =
| {x:int} {xs:ilist} TOP (icons (x,xs), x)
dataprop PUSH (ilist, int, ilist) =
| {x:int} {xs,ys:ilist} PUSH (xs, x, icons (x, xs))
dataprop POP (ilist, ilist) =
| {x:int} {xs:ilist} POP (icons (x,xs), xs)
prfun stack_push_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> TOP (ys, x) = let
prval PUSH () = pf
in
TOP ()
end
prfun stack_pop_check {x:int} {xs,ys:ilist} .<>. (pf: PUSH (xs, x, ys)):<> POP (ys, xs) = let
prval PUSH () = pf
in
POP ()
end
prfun stack_empty_check {xs:ilist} .<>. (pf: EMPTY xs):<> IS_EMPTY (xs, true) = let
prval EMPTY () = pf
in
IS_EMPTY_true ()
end
abst@ype E (a:t@ype, x:int) = a
extern castfn encode (x: double):<> [x:int] E (double, x)
extern castfn decode {i:int} (x: E (double, i)):<> double
datatype stack (ilist) =
| stack_nil (inil)
| {x:int} {xs:ilist} stack_cons (icons (x,xs)) of (E (double, x), stack xs)
extern fun stack_new (): [xs:ilist] (EMPTY xs | stack xs)
extern fun stack_is_empty {xs:ilist} (s: stack xs): [b:bool] (IS_EMPTY (xs, b) | bool b)
extern fun stack_top {xs:ilist} (pf: IS_EMPTY (xs, false) | s: stack xs): [x:int] (TOP (xs, x) | E (double, x))
extern fun stack_pop {x:int} {xs:ilist} (pf: IS_EMPTY (xs, false) | s: &stack xs >> stack ys): #[ys:ilist] (POP (xs, ys) | void)
extern fun stack_push {x:int} {xs:ilist} (s: &stack xs >> stack ys, x: E (double, x)): #[ys:ilist] (PUSH (xs, x, ys) | void)
implement stack_new () = (EMPTY () | stack_nil ())
implement stack_is_empty (s) =
case+ s of
| stack_nil () => (IS_EMPTY_true | true)
| stack_cons _ => (IS_EMPTY_false | false)
implement stack_push {x} {xs} (s, x) = (PUSH () | (s := stack_cons (x, s)))
implement stack_top (pf | s) = let
prval IS_EMPTY_false () = pf
val+ stack_cons (x,_) = s
in
(TOP () | x)
end
implement stack_pop (pf | s) = let
prval IS_EMPTY_false () = pf
val+ stack_cons (_, xs) = s
in
(POP () | s := xs)
end
fun mustcheck {xs:ilist} (s: stack xs): void = {
val (pf | e) = stack_is_empty (s)
val () = assertloc (not e)
val (_ | c) = stack_top (pf | s)
}
fun nocheck {xs:ilist} (s: &stack xs >> stack ys): #[ys:ilist] void = {
val (pf | ()) = stack_push (s, encode 42.0)
prval PUSH () = pf
val (_ | c) = stack_top (IS_EMPTY_false () | s)
}
implement main () = {
val (_ | s) = stack_new ()
var s1 = s
val (_ | a) = stack_is_empty (s1)
val (pf | ()) = stack_push (s1, encode 10.0)
prval PUSH () = pf
val (_ | b) = stack_is_empty (s1)
val (_ | c) = stack_top (IS_EMPTY_false () | s1)
val (pf | ()) = stack_pop (IS_EMPTY_false () | s1)
prval POP () = pf
val (_ | d) = stack_is_empty (s1)
val c = decode (c)
val () = printf("a=%s b=%s c=%f d=%s\n", @(if a then "true" else "false",
if b then "true" else "false",
c,
if d then "true" else "false"))
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment