stack.mlw 1.44 KB
Newer Older
1 2 3 4 5 6 7 8

(* Polymorphic mutable stacks *)

module Stack

  use import list.List
  use import list.Length

9
  type t 'a model {| mutable contents: list 'a |}
10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71

  parameter create : unit -> {} t 'a { result = Nil }

  parameter push : x:'a -> s:t 'a -> {} unit writes s { s = Cons x (old s) }

  exception Empty

  parameter pop : 
    s:t 'a -> 
    {} 
    'a 
    writes s raises Empty
    { match old s with Nil -> false | Cons x t -> result = x and s = t end } 
    | Empty -> { s = old s = Nil }

  parameter top : 
    s:t 'a -> 
    {} 
    'a 
    reads s raises Empty
    { match s with Nil -> false | Cons x _ -> result = x end } 
    | Empty -> { s = Nil }

  parameter clear : s:t 'a -> {} unit writes s { s = Nil }

  parameter copy : s:t 'a -> {} t 'a { result = s }

  parameter is_empty : s:t 'a -> {} bool reads s { result=True <-> s = Nil }

  parameter length : s:t 'a -> {} int reads s { result = length s }

end

module Test

  use import int.Int
  use import list.List
  use module Stack

  let test0 () =
    let s = Stack.create () : Stack.t 'a in
    assert { s = Nil };
    let b = Stack.is_empty s in
    assert { b = True };
    let n = Stack.length s in
    assert { n = 0 }

  let test1 () =
    let s = Stack.create () in
    Stack.push 1 s;
    let x = Stack.top s in assert { x = 1 };
    Stack.push 2 s;
    let x = Stack.top s in assert { x = 2 };
    ()

end

(*
Local Variables: 
compile-command: "unset LANG; make -C .. modules/stack"
End: 
*)