add tactic weakmem

src/ecHiTacticals.ml

@@ -194,6 +194,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pkill info                -> EcPhlCodeTx.process_kill info
     | Palias info               -> EcPhlCodeTx.process_alias info
     | Pset info                 -> EcPhlCodeTx.process_set info
+    | Pweakmem info             -> EcPhlCodeTx.process_weakmem info
     | Prnd (side, pos, info)    -> EcPhlRnd.process_rnd side pos info
     | Prndsem (side, pos)       -> EcPhlRnd.process_rndsem side pos
     | Pconseq (opt, info)       -> EcPhlConseq.process_conseq_opt opt info

src/ecLexer.mll

@@ -156,6 +156,7 @@
     "inline"      , INLINE     ;        (* KW: tactic *)
     "interleave"  , INTERLEAVE ;        (* KW: tactic *)
     "alias"       , ALIAS      ;        (* KW: tactic *)
+    "weakmem"     , WEAKMEM    ;        (* KW: tactic *)
     "fission"     , FISSION    ;        (* KW: tactic *)
     "fusion"      , FUSION     ;        (* KW: tactic *)
     "unroll"      , UNROLL     ;        (* KW: tactic *)

src/ecParser.mly

@@ -600,6 +600,7 @@
 %token UNDO
 %token UNROLL
 %token VAR
+%token WEAKMEM
 %token WHILE
 %token WHY3
 %token WITH
@@ -3235,6 +3236,9 @@ phltactic:
 | ALIAS s=side? o=codepos x=lident EQ e=expr
     { Pset (s, o, false, x,e) }
 
+| WEAKMEM h=lident p=param_decl
+    { Pweakmem(h, p) }
+
 | FISSION s=side? o=codepos AT d1=word COMMA d2=word
     { Pfission (s, o, (1, (d1, d2))) }
 

src/ecParsetree.ml

@@ -736,6 +736,7 @@ type phltactic =
   | Prnd           of oside * semrndpos option * rnd_tac_info_f
   | Prndsem        of oside * codepos1
   | Palias         of (oside * codepos * osymbol_r)
+  | Pweakmem       of (psymbol * fun_params)
   | Pset           of (oside * codepos * bool * psymbol * pexpr)
   | Pconseq        of (pcqoptions * (conseq_ppterm option tuple3))
   | Pconseqauto    of crushmode

src/phl/ecPhlCodeTx.ml

@@ -232,3 +232,37 @@ let process_alias (side, cpos, id) tc =
 let process_set (side, cpos, fresh, id, e) tc =
   let e = TTC.tc1_process_Xhl_exp tc side None e in
   t_set side cpos (fresh, id) e tc
+
+
+(* -------------------------------------------------------------------- *)
+
+let process_weakmem (id, params) tc =
+  let open EcLocation in
+  let hyps = FApi.tc1_hyps tc in
+  let env = FApi.tc1_env tc in
+  let _, f =
+    try LDecl.hyp_by_name (unloc id) hyps
+    with LDecl.LdeclError _ ->
+      tc_lookup_error !!tc ~loc:id.pl_loc `Local ([], unloc id)
+  in
+
+  let process_decl (x, ty) =
+    let ty = EcTyping.transty EcTyping.tp_tydecl env (EcUnify.UniEnv.create None) ty in
+    let x = omap unloc (unloc x) in
+    { ov_name = x; ov_type = ty } in
+
+  let decls = List.map process_decl params in
+
+  let bind me =
+    try EcMemory.bindall decls me
+    with EcMemory.DuplicatedMemoryBinding x ->
+      tc_error ~loc:id.pl_loc !!tc "variable %s already declared" x in
+
+  match f.f_node with
+  | FbdHoareS hs ->
+      let me = bind hs.bhs_m in
+      let hs = { hs with bhs_m = me } in
+      let concl = f_imp (f_bdHoareS_r hs) (FApi.tc1_goal tc) in
+      FApi.xmutate1 tc `WeakenMem [concl]
+  | _ ->
+      tc_error ~loc:id.pl_loc !!tc "the hypothesis need to be a phoare"

src/phl/ecPhlCodeTx.mli

@@ -14,3 +14,6 @@ val process_kill  : oside * codepos * int option -> backward
 val process_alias : oside * codepos * psymbol option -> backward
 val process_set   : oside * codepos * bool * psymbol * pexpr -> backward
 val process_cfold : oside * codepos * int option -> backward
+
+(* -------------------------------------------------------------------- *)
+val process_weakmem : (psymbol * fun_params) -> backward

theories/distributions/Dexcepted.ec

@@ -300,6 +300,7 @@ while (i = x /\ test = X) (if test x r then 1 else 0) 1 (mu (dt x) (predC (X x))
 + smt().
 + smt().
 + move=> ih. alias 2 r0 = r.
+  weakmem ih (r0:t) => {ih} ih.
   (** TRANSITIVITY FOR PHOARE!! **)
   phoare split (mu (dt x) (predI P (predC (X x))))
                (mu (dt x) (X x) * mu (dt x \ X x) P)