New lazy/eager logic.

examples/MEE-CBC/RCPA_CMA.ec

@@ -336,7 +336,7 @@ theory EtM.
     type leaks           <- leaks,
     op   leak            <- leak,
     op   dC    (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>)
-  proof * by smt.
+  proof * by smt(dC_ll dprod_ll dunit_ll).
 
   (** The black-box construction is as follows **)
   module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {

examples/PRG.ec

@@ -340,12 +340,9 @@ section.
     by wp; rnd; wp; rnd{2} predT; auto; rewrite dseed_ll.
   (* presampling ~ postsampling *)
   seq 2 2: (={glob A, glob F, glob Plog}); first by sim.
-  eager (H: Resample.resample(); ~ Resample.resample();
-    : ={glob Plog} ==> ={glob Plog})
-    : (={glob A, glob Plog, glob F})=> //;
-    first by sim.
-  eager proc H (={glob Plog, glob F})=> //.
-  + eager proc; inline Resample.resample.
+  eager call (: ={glob A, glob Plog, glob F}) => //. 
+  eager proc (={glob Plog, glob F}) => //; try by sim. 
+  - eager proc; inline Resample.resample.
     swap{1} 3 3. swap{2} [4..5] 2. swap{2} [6..8] 1.
     swap{1} 4 3. swap{1} 4 2. swap{2} 2 4.
     sim.
@@ -357,10 +354,8 @@ section.
       by wp; rnd{2}; auto=> />; smt (size_ge0).
     rcondt{2} 1; first by move=> &hr; auto=> /#.
     rcondf{2} 3; first by move=> &hr; auto=> /#.
-  + by sim.
-  + by sim.
-  + by eager proc; swap{1} 1 4; sim.
-  by sim.
+    by sim.
+  by eager proc; swap{1} 1 4; sim.
   qed.
 
   lemma P_PrgI &m:

examples/UC/RndO.ec

@@ -681,8 +681,7 @@ lemma eager_D :
          D(RRO).distinguish, RRO.resample(); :
          ={glob D, FRO.m} ==> ={FRO.m, glob D} /\ ={res}].
 proof.
-  eager proc (H_: RRO.resample(); ~ RRO.resample();: ={FRO.m} ==> ={FRO.m})
-             (={FRO.m}) =>//; try by sim.
+  eager proc (={FRO.m}) =>//; try by sim.
   + by apply eager_init. + by apply eager_get. + by apply eager_set. 
   + by apply eager_rem. + by apply eager_sample. 
   + by apply eager_in_dom. + by apply eager_restrK. 

src/ecEnv.ml

@@ -2351,7 +2351,7 @@ module NormMp = struct
     match item with
     | MI_Module me -> mod_use env rm fdone us (EcPath.mqname mp me.me_name)
     | MI_Variable v -> add_var env (xpath mp v.v_name) us
-    | MI_Function f -> fun_use_aux env rm fdone us (xpath mp f.f_name)
+    | MI_Function f -> gen_fun_use env fdone rm us (xpath mp f.f_name)
 
   and body_use env rm fdone mp us comps body =
     match body with
@@ -2363,9 +2363,6 @@ module NormMp = struct
     | ME_Structure ms ->
       List.fold_left (item_use env rm fdone mp) us ms.ms_body
 
-  and fun_use_aux env rm fdone us f =
-    gen_fun_use env fdone rm us f
-
   let mod_use_top env mp =
     let mp = norm_mpath env mp in
     let me, _ = Mod.by_mpath mp env in

src/ecHiTacticals.ml

@@ -222,9 +222,8 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Peager_if                 -> EcPhlEager.process_if
     | Peager_while info         -> EcPhlEager.process_while info
     | Peager_fun_def            -> EcPhlEager.process_fun_def
-    | Peager_fun_abs infos      -> curry EcPhlEager.process_fun_abs infos
+    | Peager_fun_abs infos      -> EcPhlEager.process_fun_abs infos
     | Peager_call info          -> EcPhlEager.process_call info
-    | Peager infos              -> curry EcPhlEager.process_eager infos
     | Pbd_equiv (nm, f1, f2)    -> EcPhlConseq.process_bd_equiv nm (f1, f2)
     | Pauto                     -> EcPhlAuto.t_auto ~conv:`Conv
     | Plossless                 -> EcPhlHiAuto.t_lossless

src/ecParser.mly

@@ -2844,35 +2844,25 @@ logtactic:
 | WLOG b=boption(SUFF) COLON ids=loc(ipcore_name)* SLASH f=form
    { Pwlog (ids, b, f) }
 
-eager_info:
-| h=ident
-    { LE_done h }
-
-| LPAREN h=ident COLON s1=stmt TILD s2=stmt COLON pr=form LONGARROW po=form RPAREN
-    { LE_todo (h, s1, s2, pr, po) }
-
 eager_tac:
-| SEQ n1=codepos1 n2=codepos1 i=eager_info COLON p=sform
-    { Peager_seq (i, (n1, n2), p) }
+| SEQ n1=codepos1 n2=codepos1 COLON s=stmt COLON p=form_or_double_form
+    { Peager_seq ((n1, n2), s, p) }
 
 | IF
     { Peager_if }
 
-| WHILE i=eager_info
+| WHILE i=sform
     { Peager_while i }
 
 | PROC
     { Peager_fun_def }
 
-| PROC i=eager_info f=sform
-    { Peager_fun_abs (i, f) }
+| PROC f=sform
+    { Peager_fun_abs f }
 
 | CALL info=gpterm(call_info)
     { Peager_call info }
 
-| info=eager_info COLON p=sform
-    { Peager (info, p) }
-
 form_or_double_form:
 | f=sform
     { Single f }

src/ecParsetree.ml

@@ -596,11 +596,6 @@ type trans_formula =
 type trans_info =
   trans_kind * trans_formula
 
-(* -------------------------------------------------------------------- *)
-type eager_info =
-  | LE_done of psymbol
-  | LE_todo of psymbol * pstmt * pstmt * pformula * pformula
-
 (* -------------------------------------------------------------------- *)
 type bdh_split =
   | BDH_split_bop     of pformula * pformula * pformula option
@@ -774,13 +769,12 @@ type phltactic =
   | Pprocrewrite   of side option * pcodepos * prrewrite
 
     (* Eager *)
-  | Peager_seq       of (eager_info * pcodepos1 pair * pformula)
+  | Peager_seq       of (pcodepos1 pair * pstmt * pformula doption)
   | Peager_if
-  | Peager_while     of (eager_info)
+  | Peager_while     of pformula
   | Peager_fun_def
-  | Peager_fun_abs   of (eager_info * pformula)
-  | Peager_call      of (call_info gppterm)
-  | Peager           of (eager_info * pformula)
+  | Peager_fun_abs   of pformula
+  | Peager_call      of call_info gppterm
 
     (* Relation between logic *)
   | Pbd_equiv of (side * pformula * pformula)