diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 1dc8c50e76..9f50fa85c9 100644 --- a/src/ecHiTacticals.ml +++ b/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 diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml index 4c28479463..7a9ce5f0f1 100644 --- a/src/ecProofTyping.ml +++ b/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 = diff --git a/src/ecProofTyping.mli b/src/ecProofTyping.mli index b9ead3fa4c..6588c0d171 100644 --- a/src/ecProofTyping.mli +++ b/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 diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlApp.ml index 91a2987528..a4c0de7218 100644 --- a/src/phl/ecPhlApp.ml +++ b/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,12 +239,12 @@ 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 -> @@ -251,8 +252,9 @@ let process_app (side, dir, k, phi, bd_info) tc = 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 diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml index 8e858faf5e..78f715fc47 100644 --- a/src/phl/ecPhlHiCond.ml +++ b/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 diff --git a/src/phl/ecPhlRCond.ml b/src/phl/ecPhlRCond.ml index ee4a643177..110e0a04a5 100644 --- a/src/phl/ecPhlRCond.ml +++ b/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 diff --git a/src/phl/ecPhlRnd.ml b/src/phl/ecPhlRnd.ml index 8742fa0afc..df3c54fe8e 100644 --- a/src/phl/ecPhlRnd.ml +++ b/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" diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index 64e8b89213..f8c44ae20c 100644 --- a/src/phl/ecPhlWhile.ml +++ b/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 "@[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" diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml index 82101101d1..99ddee53ee 100644 --- a/src/phl/ecPhlWp.ml +++ b/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