new library module Stack

.gitignore

@@ -155,4 +155,6 @@ why.conf
 /examples/programs/binary_search/
 /examples/programs/same_fringe/
 
+# modules
+/modules/stack/
 

drivers/tptp.drv

@@ -5,6 +5,7 @@ filename "%f-%t-%g.p"
 
 valid   "Proof found"
 invalid "Completion found"
+invalid "SZS status CounterSatisfiable"
 timeout "Ran out of time"
 timeout "Resource limit exceeded"
 timeout "CPU time limit exceeded"

modules/stack.mlw

+
+(* Polymorphic mutable stacks *)
+
+module Stack
+
+  use import list.List
+  use import list.Length
+
+  mutable type t 'a model list 'a
+
+  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: 
+*)

src/programs/pgm_typing.ml

@@ -1055,12 +1055,15 @@ let rec type_v env = function
       let env, bl = add_binders env bl in
       tarrow bl (type_c env c)
 
-and type_c env c = {
-  c_result_type = type_v env c.ic_result_type;
-  c_effect      = effect env c.ic_effect;
-  c_pre         = c.ic_pre;
-  c_post        = c.ic_post; 
-}
+and type_c env c = 
+  let ef = effect env c.ic_effect in
+  let q = c.ic_post in
+  (* saturate effect with exceptions appearing in q *)
+  let ef = List.fold_left (fun ef (e, _) -> E.add_raise e ef) ef (snd q) in
+  { c_result_type = type_v env c.ic_result_type;
+    c_effect      = ef;
+    c_pre         = c.ic_pre;
+    c_post        = q; }
 
 and add_binders env bl =
   map_fold_left add_binder env bl