working in progress

parsing/forward_rules.ml

@@ -495,7 +495,9 @@ let rec resolveInnerTryCatches typ env (match_summary:tryCatchLemma option) (spe
             | _, RaisingEff (_pre, _post, _constr, ret) -> ret
             | _, HigherOrder (_pre, _post, _constr, ret) -> ret
             | _, TryCatch (_pre, _post, _constr, ret) -> ret
+            (*
             | _, RaisingEff (_, _, _, ret) | _, HigherOrder (_, _, _, ret) |  _, TryCatch (_, _, _, ret) -> failwith (Format.asprintf "ret not a variable: %s" (string_of_term ret))
+            *)
             | _ -> 
             (match retriveLastRes phi1_spec_body with 
             | Some t -> t

parsing/normalize.ml

@@ -1323,6 +1323,13 @@ let rec existControdictionSpec (spec : spec) : bool =
     | true ->  true
     | _ -> 
       existControdictionSpec xs)
+
+  | Require (pi1, _) ::xs ->
+    (match ProversEx.is_valid pi1 False with
+    | true ->  true
+    | _ -> 
+      existControdictionSpec xs)
+
   | NormalReturn (pi, _)::xs 
   | RaisingEff (pi, _, _, _) :: xs
   | HigherOrder (pi, _, _, _) ::xs -> 

src/demo/8_schduler.ml

@@ -35,19 +35,13 @@ ens  queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ re
 = let (front, back) = !queue in
   queue := (front, ele::back)
 
-(* ex mm mm' w inter; req any_queue(queue, mm); 
-  Norm(non_empty_queue(queue, mm') /\ effNo(ele)=w /\ w >0 /\ mm'=mm+w /\ res=inter /\ inter=()) *)
-let enqueue ele queue
-(*@
-ex m m' q q'; req queue->q /\ effNo(q) = m /\ m>=0; 
-ens  queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ res=() 
-@*)
-= queue_push ele queue
 
-(*
+
+(* ex inter; req empty_queue(queue); Norm(empty_queue(queue) /\ res=true /\ inter=true)
+\/ ex m inter; req non_empty_queue(queue, m);  Norm(non_empty_queue(queue, m) /\ res=false) *)
 let queue_is_empty queue 
-(*@ ex inter; req empty_queue(queue); Norm(empty_queue(queue) /\ res=true /\ inter=true)
-\/ ex m inter; req non_empty_queue(queue, m);  Norm(non_empty_queue(queue, m) /\ res=false) @*)
+(*@ ex q ; req queue->q /\ effNo(q)=0; ens queue->q /\ res=true 
+\/  ex q ; req queue->q /\ effNo(q)>0; ens queue->q /\ res=false @*)
 = let (front, back) = !queue in
   List.length front = 0 && List.length back = 0
 
@@ -58,9 +52,14 @@ let rev_list l =
   in
   rev_acc [] l
 
+(* ex m m' w f; req non_empty_queue(queue, m);  
+  Norm(any_queue(queue, m') /\ effNo(f) =w /\ w >0 /\ m'+w=m /\ res=f) *)
 let queue_pop queue 
-(*@ ex m m' w f; req non_empty_queue(queue, m);  
-  Norm(any_queue(queue, m') /\ effNo(f) =w /\ w >0 /\ m'+w=m /\ res=f) @*)
+(*@
+ex m m' q q' f w; 
+req queue->q /\ effNo(q) = m /\ m>0; 
+ens  queue->q' /\ effNo(q') = m' /\ m'>=0  /\ effNo(f) =w /\ w >0 /\ m'+w=m /\  res = f 
+@*)
 = let (front, back) = !queue in
   match front with
   | h::tl ->
@@ -73,32 +72,53 @@ let queue_pop queue
         queue := (newfront, []);
         h)
 
+(* ex f; queue_pop (run_q, f); Norm (res=f)*)
 let wrapPop run_q 
-(*@ ex f; queue_pop (run_q, f); Norm (res=f)@*)
+(*@
+ex m m' q q' f w; 
+req run_q->q /\ effNo(q) = m /\ m>0; 
+ens  run_q->q' /\ effNo(q') = m' /\ m'>=0  /\ effNo(f) =w /\ w >0 /\ m'+w=m /\  res = f 
+@*)
 =  queue_pop run_q
 
-let dequeue run_q
-(*@ queue_is_empty(run_q, true); Norm(res=())
+(* ex mm mm' w inter; req any_queue(queue, mm); 
+  Norm(non_empty_queue(queue, mm') /\ effNo(ele)=w /\ w >0 /\ mm'=mm+w /\ res=inter /\ inter=()) *)
+let enqueue ele queue
+(*@
+ex m m' q q'; req queue->q /\ effNo(q) = m /\ m>=0; 
+ens  queue->q' /\ effNo(q') = m' /\ m'>0 /\ effNo(ele)=w /\ w >0 /\ m'=m+w /\ res=() 
+@*)
+= queue_push ele queue
+
+(* queue_is_empty(run_q, true); Norm(res=())
 \/  queue_is_empty(run_q, false); 
     ex m m' w f cr; req non_empty_queue(run_q, m);  
     Norm(any_queue(run_q, m') /\ effNo(f) =w /\ w >0 /\ m'+w=m );
-    continue (f, (), cr); Norm(res=cr)
+    continue (f, (), cr); Norm(res=cr) *)
+let dequeue run_q
+(*@
+ex q; req run_q->q /\ effNo(q)=0; ens run_q->q  /\ res=()   
+\/ 
+ex m m' q q' f w;  
+req run_q->q /\ effNo(q)=m /\ m >0; 
+ens run_q->q' /\ effNo(q') = m' /\ m'>=0  /\ effNo(f) =w /\ w >0 /\ m'+w=m;
+ex cr; continue_syh (f, (), cr)
 @*)
 = if queue_is_empty run_q then ()
   else 
     let f = queue_pop run_q in 
-    continue f ()
-
+    continue_syh f ()
 
 (*@ predicate f(arg) = 
      ex r; Norm(effNo(f) = 0 /\ r = () /\ res=r)
    \/
- ex r r1 r2 n; Yield(effNo(f)=n/\n>0/\effNo(f2)=n-1, r1); f2(r2);
+   ex r r1 r2 n; Yield(effNo(f)=n/\n>0/\effNo(f2)=n-1, r1); f2(r2);
       Norm(res = r /\ r= ()) 
-\/ ex r r1 r2 n m1 m2; Fork(effNo(f)=n /\ n>0 /\ effNo(f1)= m1 /\ effNo(f2)=m2 /\ m1>0 /\ m2>0 /\ (m1+m2)=(n-1), f1, r1); f2(r2); 
+    \/ ex r r1 r2 n m1 m2; Fork(effNo(f)=n /\ n>0 /\ effNo(f1)= m1 /\ effNo(f2)=m2 /\ m1>0 /\ m2>0 /\ (m1+m2)=(n-1), f1, r1); f2(r2); 
       Norm(res =r /\ r= ())
 @*)
 
+(*
 let rec spawn f run_q 
 (*@ ex r; queue_is_empty(run_q, true) ; ens effNo(f)=0 /\ res =r /\ r= () 
 \/ ex m m' w w' ele cr; req non_empty_queue(run_q, m);