ATS stack example

Makefile

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

stack1.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"))
}

stack2.dats

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"))
}

stack3.dats

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

stack4.dats

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"))
}

stack5.dats

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"))
}