rndsem: new version that only computes the distribution for used vari…

…ables This version was already available internally. This commits only add the needed syntax for accessing it. The syntax is: `rndsem* <options>`. closes #415
EasyCrypt · Dec 6, 2023 · d248e73 · d248e73
1 parent 7c0adea
commit d248e73
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 12 deletions.
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
@@ -195,7 +195,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Palias info               -> EcPhlCodeTx.process_alias info
     | Pset info                 -> EcPhlCodeTx.process_set info
     | Prnd (side, pos, info)    -> EcPhlRnd.process_rnd side pos info
-    | Prndsem (side, pos)       -> EcPhlRnd.process_rndsem side pos
+    | Prndsem (red, side, pos)  -> EcPhlRnd.process_rndsem ~reduce:red side pos
     | Pconseq (opt, info)       -> EcPhlConseq.process_conseq_opt opt info
     | Pconseqauto cm            -> process_conseqauto cm
     | Pconcave info             -> EcPhlConseq.process_concave info

diff --git a/src/ecParser.mly b/src/ecParser.mly
@@ -3205,8 +3205,8 @@ phltactic:
 | RND s=side? info=rnd_info c=prefix(COLON, semrndpos)?
     { Prnd (s, c, info) }
 
-| RNDSEM s=side? c=codepos1
-    { Prndsem (s, c) }
+| RNDSEM red=boption(STAR) s=side? c=codepos1
+    { Prndsem (red, s, c) }
 
 | INLINE s=side? u=inlineopt? o=occurences?
   { Pinline (`ByName(s, u, ([], o))) }

diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
@@ -734,7 +734,7 @@ type phltactic =
   | Pinterleave    of interleave_info located
   | Pkill          of (oside * codepos * int option)
   | Prnd           of oside * semrndpos option * rnd_tac_info_f
-  | Prndsem        of oside * codepos1
+  | Prndsem        of bool * oside * codepos1
   | Palias         of (oside * codepos * osymbol_r)
   | Pset           of (oside * codepos * bool * psymbol * pexpr)
   | Pconseq        of (pcqoptions * (conseq_ppterm option tuple3))

diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml
@@ -696,19 +696,19 @@ let process_rnd side pos tac_info tc =
   | _ -> tc_error !!tc "invalid arguments"
 
 (* -------------------------------------------------------------------- *)
-let t_hoare_rndsem   = FApi.t_low1 "hoare-rndsem"   (Core.t_hoare_rndsem_r   false)
-let t_bdhoare_rndsem = FApi.t_low1 "bdhoare-rndsem" (Core.t_bdhoare_rndsem_r false)
-let t_equiv_rndsem   = FApi.t_low2 "equiv-rndsem"   (Core.t_equiv_rndsem_r   false)
+let t_hoare_rndsem   = FApi.t_low2 "hoare-rndsem"   Core.t_hoare_rndsem_r
+let t_bdhoare_rndsem = FApi.t_low2 "bdhoare-rndsem" Core.t_bdhoare_rndsem_r
+let t_equiv_rndsem   = FApi.t_low3 "equiv-rndsem"   Core.t_equiv_rndsem_r
 
 (* -------------------------------------------------------------------- *)
-let process_rndsem side pos tc =
+let process_rndsem ~reduce side pos tc =
   let concl = FApi.tc1_goal tc in
 
   match side with
   | None when is_hoareS concl ->
-     t_hoare_rndsem pos tc
+     t_hoare_rndsem reduce pos tc
   | None when is_bdHoareS concl ->
-     t_bdhoare_rndsem pos tc
+     t_bdhoare_rndsem reduce pos tc
   | Some side when is_equivS concl ->
-     t_equiv_rndsem side pos tc
+     t_equiv_rndsem reduce side pos tc
   | _ -> tc_error !!tc "invalid arguments"
diff --git a/src/phl/ecPhlRnd.mli b/src/phl/ecPhlRnd.mli
@@ -25,4 +25,4 @@ val t_equiv_rnd   : ?pos:semrndpos -> oside -> (mkbij_t option) pair -> backward
 val process_rnd : oside -> semrndpos option -> rnd_infos_t -> backward
 
 (* -------------------------------------------------------------------- *)
-val process_rndsem : oside -> codepos1 -> backward
+val process_rndsem : reduce:bool -> oside -> codepos1 -> backward