Skip to content

address TODOs from memory softcoding PR #817

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

address TODOs from memory softcoding PR #817

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 0 additions & 15 deletions src/ecAst.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -466,7 +466,6 @@ type inv =
| Inv_ss of ss_inv
| Inv_ts of ts_inv

(* TODO: Get rid of this after refactor *)
let inv_of_inv (inv: inv) : form =
match inv with
| Inv_ss ss -> ss.inv
Expand Down Expand Up @@ -502,20 +501,6 @@ let lift_ts_inv2 (f: ts_inv -> ts_inv -> 'a) : inv -> inv -> 'a =
| _ -> failwith "expected only two sided invariants" in
f

(* TODO: This should be removed after refactor is done *)
let lift_inv_adapter (f: form -> 'a) : inv -> 'a =
let f inv = match inv with
| Inv_ss ss -> f ss.inv
| Inv_ts ts -> f ts.inv in
f

let lift_inv_adapter2 (f: form -> form -> 'a) : inv -> inv -> 'a =
let f inv1 inv2 = match inv1, inv2 with
| Inv_ss ss1, Inv_ss ss2 -> f ss1.inv ss2.inv
| Inv_ts ts1, Inv_ts ts2 -> f ts1.inv ts2.inv
| _ -> failwith "expected compatible invariants" in
f

let ss_inv_generalize_left (inv: ss_inv) (m: memory) : ts_inv =
{ ml = m; mr = inv.m; inv = inv.inv }

Expand Down
2 changes: 0 additions & 2 deletions src/ecAst.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -373,8 +373,6 @@ val lift_ss_inv2 : (ss_inv -> ss_inv -> 'a) -> inv -> inv -> 'a
val lift_ss_inv3 : (ss_inv -> ss_inv -> ss_inv -> 'a) -> inv -> inv -> inv -> 'a
val lift_ts_inv : (ts_inv -> 'a) -> inv -> 'a
val lift_ts_inv2 : (ts_inv -> ts_inv -> 'a) -> inv -> inv -> 'a
val lift_inv_adapter : (form -> 'a) -> inv -> 'a
val lift_inv_adapter2 : (form -> form -> 'a) -> inv -> inv -> 'a

val ss_inv_generalize_left : ss_inv -> memory -> ts_inv
val ss_inv_generalize_right : ss_inv -> memory -> ts_inv
Expand Down
1 change: 0 additions & 1 deletion src/phl/ecPhlConseq.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1024,7 +1024,6 @@ let rec t_hi_conseq notmod f1 f2 f3 tc =
let m,hi,hh, h0 =
as_seq4 (LDecl.fresh_ids (FApi.tc1_hyps tc) ["&m";"_";"_";"_"]) in
let pre = map_ss_inv2 f_and (bhs_pr hs) (hs_pr hs2) in
(* TODO: dubious *)
let mpre = Fsubst.f_subst_mem pre.m m pre.inv in
let post1 = (bhs_po hs0) in
let post = (bhs_po hs) in
Expand Down
1 change: 0 additions & 1 deletion src/phl/ecPhlPr.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,6 @@ let process_ppr info tc =
let ef = tc1_as_equivF tc in
let qenvl = snd (LDecl.hoareF ef.ef_ml ef.ef_fl hyps) in
let qenvr = snd (LDecl.hoareF ef.ef_mr ef.ef_fr hyps) in
(* TODO: These should be one-sided *)
let phi1 = TTC.pf_process_form_opt !!tc qenvl None phi1 in
let phi2 = TTC.pf_process_form_opt !!tc qenvr None phi2 in
if not (EcReduction.EqTest.for_type (LDecl.toenv hyps) phi1.f_ty phi2.f_ty) then
Expand Down