stack.mlw 1.57 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3 4
(** {1 Stacks} *)

(** {2 Polymorphic mutable stacks} *)
5 6 7 8

module Stack

  use import list.List
9
  use import list.Length as L
10

11
  type t 'a model {| mutable elts: list 'a |}
12

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
13
  val create: unit -> {} t 'a { result.elts = Nil }
14

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
15 16
  val push:
    x: 'a -> s: t 'a -> {} unit writes s { s.elts = Cons x (old s.elts) }
17 18 19

  exception Empty

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
20 21
  val pop:
    s: t 'a ->
22 23
    {}
    'a
24
    writes s raises Empty
25
    { match old s.elts with Nil -> false
Andrei Paskevich's avatar
Andrei Paskevich committed
26
                          | Cons x t -> result = x /\ s.elts = t end }
27 28
    | Empty -> { s.elts = old s.elts = Nil }

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
29 30
  val top:
    s: t 'a ->
31 32
    {}
    'a
33
    reads s raises Empty
34 35
    { match s.elts with Nil -> false | Cons x _ -> result = x end }
    | Empty -> { s.elts = Nil }
36

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
37
  val clear: s: t 'a -> {} unit writes s { s.elts = Nil }
38

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
39
  val copy: s: t 'a -> {} t 'a { result = s }
40

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
41 42
  val is_empty:
    s: t 'a -> {} bool reads s { result=True <-> s.elts = Nil }
43

MARCHE Claude's avatar
MARCHE Claude committed
44
  (***
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
45
  val length: s: t 'a -> {} int reads s { result = length s.elts }
46 47
  *)
  function length (s: t 'a) : int = L.length s.elts
48 49 50 51 52 53 54

end

module Test

  use import int.Int
  use import list.List
55
  use import module Stack
56 57 58

  let test0 () =
    let s = Stack.create () : Stack.t 'a in
59
    assert { s.elts = Nil };
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74
    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

MARCHE Claude's avatar
MARCHE Claude committed
75
(***
76
Local Variables:
77
compile-command: "unset LANG; make -C .. modules/stack"
78
End:
79
*)