Add more fixes

Author: lyonel2017

examples/exception.ec

@@ -8,7 +8,7 @@ op p2: int -> bool.
 
 module M' ={
   proc truc (x:int) : int = {
-  raise (! p1 x \/ ! p2 x) assume;
+  ensure (! p1 x \/ ! p2 x) assume;
   if (!p1 x \/ !p2 x) { raise assert;}
   return x;
   }
@@ -46,7 +46,7 @@ exception e3.
 
 module M ={
   proc f1 (x:int) : int = {
-    raise (x <> 3) e1;
+    ensure (x <> 3) e1;
     x <- 5;
     return x;
   }

src/ecLexer.mll

@@ -53,7 +53,8 @@
     "match"       , MATCH      ;        (* KW: prog *)
     "for"         , FOR        ;        (* KW: prog *)
     "while"       , WHILE      ;        (* KW: prog *)
-    "raise"       , RAISE     ;        (* KW: prog *)
+    "ensure"      , ENSURE     ;        (* KW: prog *)
+    "raise"       , RAISE      ;        (* KW: prog *)
     "return"      , RETURN     ;        (* KW: prog *)
     "res"         , RES        ;        (* KW: prog *)
     "equiv"       , EQUIV      ;        (* KW: prog *)

src/ecParser.mly

@@ -384,6 +384,7 @@
 %token AMP
 %token APPLY
 %token AS
+%token ENSURE
 %token RAISE
 %token ASSUMPTION
 %token ASYNC
@@ -1361,8 +1362,11 @@ base_instr:
 | f=loc(fident) LPAREN es=loc(plist0(expr, COMMA)) RPAREN
     { PScall (None, f, es) }
 
-| RAISE e=paren(expr)? x=qident
-     { PSraise (x, e) }
+| ENSURE e=paren(expr) x=qident
+     { PSraise (x, Some e) }
+
+| RAISE x=qident
+     { PSraise (x, None) }
 
 instr:
 | bi=base_instr SEMICOLON
@@ -2551,15 +2555,11 @@ conseq_xt:
 | UNDERSCORE COLON cmp=hoare_bd_cmp? bd=sform
     { (None, None, None), Some (CQI_bd (cmp, bd)) }
 
-call_epost:
-| empty             { ([],None) }
-| c=epostl_xt       { c }
-
 call_info:
-| f1=form LONGARROW f2=form poe=call_epost { CI_spec (f1, f2, poe) }
-| f=form                                   { CI_inv  (f) }
-| bad=form COMMA p=form                    { CI_upto (bad,p,None) }
-| bad=form COMMA p=form COMMA q=form       { CI_upto (bad,p,Some q) }
+| f1=form LONGARROW f2=form poe=conseq_epost { CI_spec (f1, f2, poe) }
+| f=form                                     { CI_inv  (f) }
+| bad=form COMMA p=form                      { CI_upto (bad,p,None) }
+| bad=form COMMA p=form COMMA q=form         { CI_upto (bad,p,Some q) }
 
 tac_dir:
 | BACKS { Backs }

src/ecParsetree.ml

@@ -544,7 +544,7 @@ and pspattern = unit
 type excep_spec_preds = ((pqsymbol * pformula) list * pformula option)
 
 type call_info =
-  | CI_spec of (pformula * pformula * excep_spec_preds)
+  | CI_spec of (pformula * pformula * excep_spec_preds option)
   | CI_inv of pformula
   | CI_upto of (pformula * pformula * pformula option)
 

src/phl/ecPhlCall.ml

@@ -422,6 +422,8 @@ let mk_inv_spec (_pf : proofenv) env inv fl fr =
       let post = map_ts_inv2 f_and eq_res inv in
         f_equivF pre fl fr post
 
+let ensure_none_poe tc poe =
+  if not (is_none poe) then tc_error !!tc "exception are not supported"
 
 let process_call side info tc =
   let process_spec_2 tc side pre post =
@@ -569,9 +571,11 @@ let process_call side info tc =
         let _, concl = FApi.tc1_flat tc in
         match concl.f_node with
         | FhoareS _ ->
+          let poe = odfl ([],None) poe in
           process_spec_1 tc side pre post poe
         | _ ->
-           process_spec_2 tc side pre post
+          ensure_none_poe tc poe;
+          process_spec_2 tc side pre post
       end
 
     | CI_inv inv ->
@@ -647,7 +651,8 @@ let process_call_concave (fc, info) tc =
 
   let process_cut tc info =
     match info with
-    | CI_spec (pre, post, ([],None)) ->
+    | CI_spec (pre, post, poe) ->
+      ensure_none_poe tc poe;
       let ty,fmake = process_spec tc in
       let _, pre = TTC.tc1_process_Xhl_form tc ty pre in
       let _, post = TTC.tc1_process_Xhl_form tc ty post in

src/phl/ecPhlEager.ml

@@ -603,7 +603,7 @@ let process_fun_abs info eqI tc =
 let process_call info tc =
   let process_cut info =
     match info with
-    | EcParsetree.CI_spec (fpre, fpost, ([],None)) ->
+    | EcParsetree.CI_spec (fpre, fpost, None) ->
         let env, hyps, _ = FApi.tc1_eflat tc in
         let es  = tc1_as_equivS tc in
 

src/phl/ecPhlUpto.ml

@@ -62,7 +62,7 @@ let rec check_bad_true env bad s =
     | Smatch(_,bs) ->
       let check_branch (_, s) = check_bad_true env bad s.s_node in
       List.iter (check_branch) bs
-    | Sraise _ -> assert false
+    | Sraise _ -> tacuerror "exception are not supported"
     | Sabstract _ -> ()
     end;
     check_bad_true env bad c
@@ -142,7 +142,7 @@ and i_upto env alpha bad i1 i2 =
     with E.NotConv -> false
   end
 
-  | Sraise e1, Sraise e2 -> EcPath.p_equal e1 e2
+  | Sraise _, Sraise _ -> tacuerror "exception are not supported"
 
   | Sabstract id1, Sabstract id2 ->
     EcIdent.id_equal id1 id2

src/phl/ecPhlWhile.ml

@@ -42,7 +42,7 @@ let while_info env e s =
         let f = EcEnv.NormMp.norm_xfun env f in
         (w, r, Sx.add f c)
 
-    | Sraise _ -> assert false
+    | Sraise _ -> tacuerror "exception are not supported";
 
     | Sabstract id ->
         let add_pv x (pv,ty) = PV.add env pv ty x in