Internal API: process_Xhl_*

This family of functions type-check a formula w.r.t. a memory that
is infered from the program logic goal.

The commit changes two things:

 - for prhl, its uses the same memory name as the one used
   in the program logic goal. (Previously, it was using `mhr`)

 - its returns the memory that has been used for the type-checking

src/ecHiTacticals.ml

@@ -80,7 +80,7 @@ and process1_case (_ : ttenv) (doeq, opts, gp) (tc : tcenv1) =
   in
     match (FApi.tc1_goal tc).f_node with
     | FbdHoareS _ | FcHoareS _ | FhoareS _ | FeHoareS _ when not opts.cod_ambient ->
-        let fp = TTC.tc1_process_Xhl_formula tc (form_of_gp ()) in
+        let _, fp = TTC.tc1_process_Xhl_formula tc (form_of_gp ()) in
         EcPhlCase.t_hl_case fp tc
 
     | FequivS _ when not opts.cod_ambient ->
@@ -224,6 +224,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pauto                     -> EcPhlAuto.t_auto ~conv:`Conv
     | Plossless                 -> EcPhlHiAuto.t_lossless
     | Prepl_stmt infos          -> EcPhlTrans.process_equiv_trans infos
+    | Pprocchange (s, p, f)     -> EcPhlRewrite.process_change s p f
   in
 
   try  tx tc

src/ecProofTyping.ml

@@ -163,24 +163,26 @@ let tc1_process_Xhl_exp tc side ty e =
 (* ------------------------------------------------------------------ *)
 let tc1_process_Xhl_form ?side tc ty pf =
   let hyps, concl = FApi.tc1_flat tc in
+  let m = fst (EcFol.destr_programS side concl) in
 
-  let memory, mv =
-    match concl.f_node, side with
-    | FhoareS  hs, None         -> (hs.hs_m, Some (hs.hs_pr, hs.hs_po ))
-    | FeHoareS  hs, None        -> (hs.ehs_m , Some (hs.ehs_pr , hs.ehs_po))
-    | FcHoareS  hs, None        -> (hs.chs_m, Some (hs.chs_pr, hs.chs_po ))
-    | FbdHoareS hs, None        -> (hs.bhs_m, Some (hs.bhs_pr, hs.bhs_po))
-    | FequivS   es, Some `Left  -> ((mhr, snd es.es_ml), None)
-    | FequivS   es, Some `Right -> ((mhr, snd es.es_mr), None)
-
-    | _, _ -> raise (DestrError "destr_programS")
+  let mv =
+    match concl.f_node with
+    | FhoareS   hs -> Some (hs.hs_pr , hs.hs_po )
+    | FeHoareS  hs -> Some (hs.ehs_pr, hs.ehs_po)
+    | FcHoareS  hs -> Some (hs.chs_pr, hs.chs_po)
+    | FbdHoareS hs -> Some (hs.bhs_pr, hs.bhs_po)
+    | _            -> None
   in
 
-  let hyps = LDecl.push_active memory hyps in
-  let mv = mv |> omap
-   (fun (pr, po) -> Msym.of_list [("pre", pr); ("post", po)]) in
+  let hyps = LDecl.push_active m hyps in
+
+  let mv =
+    Option.map
+      (fun (pr, po) -> Msym.of_list [("pre", pr); ("post", po)])
+      mv
+  in
 
-  pf_process_form ?mv !!tc hyps ty pf
+  (m, pf_process_form ?mv !!tc hyps ty pf)
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_Xhl_formula ?side tc pf =

src/ecProofTyping.mli

@@ -7,6 +7,7 @@ open EcDecl
 open EcModules
 open EcEnv
 open EcCoreGoal
+open EcMemory
 
 (* -------------------------------------------------------------------- *)
 type ptnenv = ty Mid.t * EcUnify.unienv
@@ -47,9 +48,9 @@ val tc1_process_exp      : tcenv1 -> [`InProc|`InOp] -> ty option -> pexpr -> ex
 val tc1_process_pattern  : tcenv1 -> pformula -> ptnenv * form
 
 (* Same as previous functions, but for *HL contexts *)
-val tc1_process_Xhl_form     : ?side:side -> tcenv1 -> ty -> pformula -> form
-val tc1_process_Xhl_formula  : ?side:side -> tcenv1 -> pformula -> form
-val tc1_process_Xhl_formula_xreal : tcenv1 -> pformula -> form
+val tc1_process_Xhl_form     : ?side:side -> tcenv1 -> ty -> pformula -> memenv * form
+val tc1_process_Xhl_formula  : ?side:side -> tcenv1 -> pformula -> memenv * form
+val tc1_process_Xhl_formula_xreal : tcenv1 -> pformula -> memenv * form
 
 val tc1_process_Xhl_exp      : tcenv1 -> oside -> ty option -> pexpr -> expr
 

src/phl/ecPhlApp.ml

@@ -179,7 +179,7 @@ let process_phl_bd_info dir bd_info tc =
 
   | PAppSingle f ->
       let hs = tc1_as_bdhoareS tc in
-      let f  = TTC.tc1_process_Xhl_form tc treal f in
+      let f  = snd (TTC.tc1_process_Xhl_form tc treal f) in
       let f1, f2 =
         match dir with
         | Backs  -> (f_real_div hs.bhs_bd f, f)
@@ -189,7 +189,7 @@ let process_phl_bd_info dir bd_info tc =
 
   | PAppMult (phi, f1, f2, g1, g2) ->
       let phi =
-        phi |> omap (TTC.tc1_process_Xhl_formula tc)
+        phi |> omap (fun f -> snd (TTC.tc1_process_Xhl_formula tc f))
             |> odfl f_true in
 
       let check_0 f =
@@ -201,16 +201,17 @@ let process_phl_bd_info dir bd_info tc =
         | None, None -> assert false
 
         | Some fp, None ->
-            let f = TTC.tc1_process_Xhl_form tc treal fp in
+            let _, f = TTC.tc1_process_Xhl_form tc treal fp in
             reloc fp.pl_loc check_0 f; (f, f_r1)
 
         | None, Some fp ->
-            let f = TTC.tc1_process_Xhl_form tc treal fp in
+            let _, f = TTC.tc1_process_Xhl_form tc treal fp in
             reloc fp.pl_loc check_0 f; (f_r1, f)
 
         | Some f1, Some f2 ->
-            (TTC.tc1_process_Xhl_form tc treal f1,
-             TTC.tc1_process_Xhl_form tc treal f2)
+            let _, f1 = TTC.tc1_process_Xhl_form tc treal f1 in
+            let _, f2 = TTC.tc1_process_Xhl_form tc treal f2 in
+            (f1, f2)
       in
 
       let f1, f2 = process_f (f1, f2) in
@@ -238,21 +239,22 @@ let process_app (side, dir, k, phi, bd_info) tc =
   match k, bd_info with
   | Single i, PAppNone when is_hoareS concl ->
     check_side side;
-    let phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
+    let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
     t_hoare_app i phi tc
 
   | Single i, PAppNone when is_eHoareS concl ->
     check_side side;
-    let phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in
+    let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in
     t_ehoare_app i phi tc
 
   | Single i, PAppNone when is_equivS concl ->
     let pre, post =
       match phi with
       | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected"
       | Double (pre, post) ->
-        TTC.tc1_process_Xhl_formula ?side tc pre,
-        TTC.tc1_process_Xhl_formula ?side tc post in
+        let _, pre  = TTC.tc1_process_Xhl_formula ?side tc pre in
+        let _, post = TTC.tc1_process_Xhl_formula ?side tc post in
+        (pre, post) in
     let side =
       match side with
       | None -> tc_error !!tc "seq onsided: side information expected"
@@ -261,12 +263,12 @@ let process_app (side, dir, k, phi, bd_info) tc =
 
   | Single i, _ when is_cHoareS concl ->
     check_side side;
-    let phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
+    let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
     let cost = process_phl_c_info bd_info tc in
     t_choare_app i phi cost tc
 
   | Single i, _ when is_bdHoareS concl ->
-      let pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in
+      let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in
       let (ra, f1, f2, f3, f4) = process_phl_bd_info dir bd_info tc in
       t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc
 

src/phl/ecPhlHiCond.ml

@@ -26,7 +26,7 @@ let process_cond info tc =
       if side <> None || i1 <> None || i2 <> None then
         tc_error !!tc "cannot supply side or code position when goal is a choare"
       else
-        let f = EcProofTyping.tc1_process_Xhl_formula tc f in
+        let _, f = EcProofTyping.tc1_process_Xhl_formula tc f in
         t_choare_cond (Some f) tc
     else
       let es = tc1_as_equivS tc in
@@ -39,8 +39,8 @@ let process_cond info tc =
   | `SeqOne (s, i, f1, f2) ->
     let es = tc1_as_equivS tc in
     let n = default_if i (match s with `Left -> es.es_sl | `Right -> es.es_sr) in
-    let f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
-    let f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
+    let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in
+    let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in
     FApi.t_seqsub
       (EcPhlApp.t_equiv_app_onesided s n f1 f2)
       [ t_id; t_bdhoare_cond] tc

src/phl/ecPhlRCond.ml

@@ -128,8 +128,11 @@ let t_rcond side b at_pos c tc =
     check_none (); Low.t_equiv_rcond side b at_pos tc
 
 let process_rcond side b at_pos c tc =
-  let c = EcUtils.omap (fun c ->
-      EcProofTyping.tc1_process_Xhl_formula tc c) c in
+  let c =
+    EcUtils.omap
+      (fun c ->
+         snd (EcProofTyping.tc1_process_Xhl_formula tc c))
+      c in
 
   t_rcond side b at_pos c tc
 

src/phl/ecPhlRnd.ml

@@ -647,8 +647,8 @@ let process_rnd side pos tac_info tc =
         PNoRndParams
 
       | PSingleRndParam fp ->
-        PSingleRndParam
-          (TTC.tc1_process_Xhl_form tc tbool fp)
+        let _, fp = TTC.tc1_process_Xhl_form tc tbool fp in
+        PSingleRndParam fp
 
       | _ -> tc_error !!tc "invalid arguments" in
 
@@ -664,15 +664,15 @@ let process_rnd side pos tac_info tc =
 
       | PSingleRndParam fp ->
           PSingleRndParam
-            (fun t -> TTC.tc1_process_Xhl_form tc (tfun t tbool) fp)
+            (fun t -> snd (TTC.tc1_process_Xhl_form tc (tfun t tbool) fp))
 
       | PMultRndParams ((phi, d1, d2, d3, d4), p) ->
-          let p t = p |> omap (TTC.tc1_process_Xhl_form tc (tfun t tbool)) in
-          let phi = TTC.tc1_process_Xhl_form tc tbool phi in
-          let d1  = TTC.tc1_process_Xhl_form tc treal d1 in
-          let d2  = TTC.tc1_process_Xhl_form tc treal d2 in
-          let d3  = TTC.tc1_process_Xhl_form tc treal d3 in
-          let d4  = TTC.tc1_process_Xhl_form tc treal d4 in
+          let p t = p |> omap (fun p -> snd (TTC.tc1_process_Xhl_form tc (tfun t tbool) p)) in
+          let _, phi = TTC.tc1_process_Xhl_form tc tbool phi in
+          let _, d1  = TTC.tc1_process_Xhl_form tc treal d1 in
+          let _, d2  = TTC.tc1_process_Xhl_form tc treal d2 in
+          let _, d3  = TTC.tc1_process_Xhl_form tc treal d3 in
+          let _, d4  = TTC.tc1_process_Xhl_form tc treal d4 in
           PMultRndParams ((phi, d1, d2, d3, d4), p)
 
       | _ -> tc_error !!tc "invalid arguments"

src/phl/ecPhlWhile.ml

@@ -444,24 +444,24 @@ let process_while side winfos tc =
       match vrnt with
       | None ->
         t_hoare_while
-          (TTC.tc1_process_Xhl_formula tc phi)
+          (snd (TTC.tc1_process_Xhl_formula tc phi))
           tc
       | _    -> tc_error !!tc "invalid arguments"
     end
 
   | FeHoareS _ ->
-      let inv = TTC.tc1_process_Xhl_formula_xreal tc phi in
+      let _, inv = TTC.tc1_process_Xhl_formula_xreal tc phi in
       t_ehoare_while inv tc
 
   | FcHoareS _ -> begin
       match vrnt, bds with
       | Some vrnt, Some (`Cost (n, cost)) ->
-        t_choare_while
-          (TTC.tc1_process_Xhl_formula tc         phi)
-          (TTC.tc1_process_Xhl_form    tc tint    vrnt)
-          (TTC.tc1_process_Xhl_form    tc tint    n)
-          (TTC.tc1_process_cost        tc [tint]  cost)
-          tc
+        let _, phi = TTC.tc1_process_Xhl_formula tc phi in
+        let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in
+        let _, n = TTC.tc1_process_Xhl_form tc tint n in
+        let cost = TTC.tc1_process_cost tc [tint] cost in
+
+        t_choare_while phi vrnt n cost tc
 
       | _    -> tc_error !!tc "@[<v 2>invalid arguments, you must supply :@;\
                                I (invariant),@ \
@@ -473,21 +473,22 @@ let process_while side winfos tc =
   | FbdHoareS _ -> begin
       match vrnt, bds with
       | Some vrnt, None ->
-          t_bdhoare_while
-            (TTC.tc1_process_Xhl_formula tc phi)
-            (TTC.tc1_process_Xhl_form tc tint vrnt)
-            tc
+          let _, phi = TTC.tc1_process_Xhl_formula tc phi in
+          let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in
+
+          t_bdhoare_while phi vrnt tc
 
       | Some vrnt, Some (`Bd (k, eps)) ->
-        t_bdhoare_while_rev_geq
-          (TTC.tc1_process_Xhl_formula tc phi)
-          (TTC.tc1_process_Xhl_form    tc tint vrnt)
-          (TTC.tc1_process_Xhl_form    tc tint k)
-          (TTC.tc1_process_Xhl_form    tc treal eps)
-          tc
+        let _, phi = TTC.tc1_process_Xhl_formula tc phi in
+        let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in
+        let _, k = TTC.tc1_process_Xhl_form tc tint k in
+        let _, eps = TTC.tc1_process_Xhl_form tc treal eps in
+
+        t_bdhoare_while_rev_geq phi vrnt k eps tc
 
       | None, None ->
-          t_bdhoare_while_rev (TTC.tc1_process_Xhl_formula tc phi) tc
+          let _, phi = TTC.tc1_process_Xhl_formula tc phi in
+          t_bdhoare_while_rev phi tc
 
       | Some _, Some (`Cost _) | None, Some _ ->
         tc_error !!tc "invalid arguments"

src/phl/ecPhlWp.ml

@@ -261,7 +261,7 @@ let () = EcTyping.wp := Some typing_wp
 (* -------------------------------------------------------------------- *)
 let process_wp k cost_pre tc =
   let cost_pre  = match cost_pre with
-    | Some pre -> Some (EcProofTyping.tc1_process_Xhl_formula tc pre)
+    | Some pre -> Some (snd (EcProofTyping.tc1_process_Xhl_formula tc pre))
     | None -> None in
   let t_after =
     match (FApi.tc1_goal tc).f_node with