(** {1 Stacks} *) (** {2 Polymorphic mutable stacks} *) module Stack use import list.List use import list.Length as L type t 'a model {| mutable elts: list 'a |} val create: unit -> {} t 'a { result.elts = Nil } val push: x: 'a -> s: t 'a -> {} unit writes s { s.elts = Cons x (old s.elts) } exception Empty val pop: s: t 'a -> {} 'a writes s raises Empty { match old s.elts with Nil -> false | Cons x t -> result = x /\ s.elts = t end } | Empty -> { s.elts = old s.elts = Nil } val top: s: t 'a -> {} 'a reads s raises Empty { match s.elts with Nil -> false | Cons x _ -> result = x end } | Empty -> { s.elts = Nil } val clear: s: t 'a -> {} unit writes s { s.elts = Nil } val copy: s: t 'a -> {} t 'a { result = s } val is_empty: s: t 'a -> {} bool reads s { result=True <-> s.elts = Nil } (*** val length: s: t 'a -> {} int reads s { result = length s.elts } *) function length (s: t 'a) : int = L.length s.elts end module Test use import int.Int use import list.List use import module Stack let test0 () = let s = Stack.create () : Stack.t 'a in assert { s.elts = 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: *)