remove use

Author: bgregoir

examples/exception.ec

@@ -9,7 +9,6 @@ op p2: int -> bool.
 module M' ={
   proc truc (x:int) : int = {
   if (! p1 x \/ ! p2 x) else raise assume; 
-  ensure (! p1 x \/ ! p2 x) -> assume;
   if (!p1 x \/ !p2 x) { raise assert;}
   return x;
   }
@@ -54,7 +53,7 @@ exception e3.
 
 module M ={
   proc f1 (x:int) : int = {
-    ensure (x <> 3) -> e1;
+    if (x <> 3) else raise e1;
     x <- 5;
     return x;
   }
@@ -196,7 +195,7 @@ proof.
   proc. wp. skip => //.
 qed.
 
-exception return ['a] 
+
 
 
 

src/ecLexer.mll

@@ -36,7 +36,6 @@
     "admitted"    , ADMITTED   ;        (* KW: dangerous *)
 
     "forall"      , FORALL     ;        (* KW: prog *)
-    "ensure"      , ENSURE     ;        (* KW: prog *)
     "exists"      , EXIST      ;        (* KW: prog *)
     "fun"         , FUN        ;        (* KW: prog *)
     "glob"        , GLOB       ;        (* KW: prog *)
@@ -54,7 +53,6 @@
     "match"       , MATCH      ;        (* KW: prog *)
     "for"         , FOR        ;        (* KW: prog *)
     "while"       , WHILE      ;        (* KW: prog *)
-    "ensure"      , ENSURE     ;        (* KW: prog *)
     "raise"       , RAISE      ;        (* KW: prog *)
     "return"      , RETURN     ;        (* KW: prog *)
     "res"         , RES        ;        (* KW: prog *)

src/ecParser.mly

@@ -437,7 +437,6 @@
 %token ELIM
 %token ELSE
 %token END
-%token ENSURE
 %token EOF
 %token EQ
 %token EQUIV
@@ -1365,10 +1364,7 @@ base_instr:
     { PScall (None, f, es) }
 
 | RAISE ex=expr
-    { PSraise (ex, None) }
-
-| ENSURE e=expr RARROW ex=expr
-    { PSraise (ex, Some e) }
+    { PSraise ex }
 
 instr:
 | bi=base_instr SEMICOLON
@@ -1387,8 +1383,8 @@ instr:
    { PSmatch (e, `If ((c, b1), b2)) }
 
 %inline if_expr:
-| IF c=paren(expr) b=block el=if_else_expr
-   { PSif ((c, b), fst el, snd el) }
+| IF c=paren(expr) b=block? el=if_else_expr
+   { PSif ((c, odfl [] b), fst el, snd el) }
 
 if_else_expr:
 |  /* empty */ { ([], []) }

src/ecParsetree.ml

@@ -161,7 +161,7 @@ and pinstr_r =
   | PSif     of pscond * pscond list * pstmt
   | PSwhile  of pscond
   | PSmatch  of pexpr * psmatch
-  | PSraise  of pexpr * pexpr option
+  | PSraise  of pexpr
 
 and psmatch = [
   | `Full of (ppattern * pstmt) list

src/ecPrinting.ml

@@ -2679,7 +2679,6 @@ let pp_axiom ?(long=false) (ppe : PPEnv.t) fmt (x, ax) =
 type ppnode1 = [
   | `Asgn     of (EcModules.lvalue * EcTypes.expr)
   | `Raise    of EcTypes.expr
-  | `ERaise   of (EcTypes.expr * EcTypes.expr)
   | `Call     of (EcModules.lvalue option * P.xpath * EcTypes.expr list)
   | `Rnd      of (EcModules.lvalue * EcTypes.expr)
   | `Abstract of EcIdent.t
@@ -2708,10 +2707,6 @@ let at (ppe : PPEnv.t) n i =
   | Swhile (e, s), 0 -> Some (`While e, `P, s.s_node)
   | Swhile _     , 1 -> Some (`EBlk   , `B, [])
 
-  | Sif (e, {s_node=[{i_node=Sraise p}]}, {s_node= []}), 0 ->
-    Some (`ERaise (p,e), `P, [])
-  | Sif (_, {s_node=[{i_node=Sraise _}]}, {s_node= []}), 1 ->
-    None
   | Sif (e, s, _ ), 0 -> Some (`If e, `P, s.s_node)
   | Sif (_, _, s ), 1 -> begin
       match s.s_node with
@@ -2804,10 +2799,6 @@ let pp_i_asgn (ppe : PPEnv.t) fmt (lv, e) =
 let pp_i_raise (ppe : PPEnv.t) fmt (e : expr) =
   Format.fprintf fmt "raise %a" (pp_expr ppe) e
 
-let pp_i_eraise (ppe : PPEnv.t) fmt (p,e) =
-  Format.fprintf fmt "ensure %a -> %a"
-    (pp_expr ppe) (add_not e) (pp_expr ppe) p
-
 let pp_i_call (ppe : PPEnv.t) fmt (lv, xp, args) =
   match lv with
   | None ->
@@ -2854,7 +2845,6 @@ let c_ppnode1 ~width ppe (pp1 : ppnode1) =
   match pp1 with
   | `Asgn     x -> c_split ~width (pp_i_asgn     ppe) x
   | `Raise    x -> c_split ~width (pp_i_raise    ppe) x
-  | `ERaise   x -> c_split ~width (pp_i_eraise   ppe) x
   | `Call     x -> c_split ~width (pp_i_call     ppe) x
   | `Rnd      x -> c_split ~width (pp_i_rnd      ppe) x
   | `Abstract x -> c_split ~width (pp_i_abstract ppe) x
@@ -3481,19 +3471,18 @@ let rec pp_instr_r (ppe : PPEnv.t) fmt i =
     Format.fprintf fmt "@[<v>while (@[%a@])%a@]"
       (pp_expr ppe) e (pp_block ppe) s
 
-  | Sif (e, {s_node=[{i_node=Sraise p}]}, {s_node= []})->
-    Format.fprintf fmt "@[<hov 2>ensure@ @[%a@]@ ->@ %a@];"
-      (pp_expr ppe) (add_not e) (pp_expr ppe) p
-
   | Sif (e, s1, s2) ->
+    let pp_then ppe fmt s =
+      if s.s_node = [] then ()
+      else pp_block ppe fmt s in
     let pp_else ppe fmt s =
       match s.s_node with
       | []  -> ()
       | [_] -> Format.fprintf fmt "@,else %a" (pp_block ppe) s
       | _   -> Format.fprintf fmt "@ else %a" (pp_block ppe) s
     in
       Format.fprintf fmt "@[<v>if (@[%a@]) %a%a@]"
-      (pp_expr ppe) e (pp_block ppe) s1 (pp_else ppe) s2
+      (pp_expr ppe) e (pp_then ppe) s1 (pp_else ppe) s2
 
   | Smatch (e, ps) ->
     let p, tyd, typ = oget (EcEnv.Ty.get_top_decl e.e_ty ppe.PPEnv.ppe_env) in

src/ecTyping.ml

@@ -2822,15 +2822,10 @@ and transinstr
       [ i_match (e, branches) ]
     end
 
-  | PSraise (pex,pe) ->
+  | PSraise (pex) ->
     let ex, exty = transexp env `InProc ue pex in
     unify_or_fail env ue pex.pl_loc ~expct:texn exty;
-    match pe with
-    | None ->  [i_raise ex]
-    | Some pe ->
-      let e, ety = transexp env `InProc ue pe in
-      unify_or_fail env ue pe.pl_loc ~expct:tbool ety;
-      [i_if (e_not e, stmt [i_raise ex], stmt [])]
+    [i_raise ex]
 
 (* -------------------------------------------------------------------- *)
 and trans_pv env { pl_desc = x; pl_loc = loc } =