Revision aab2ca46757051ae341e28a2d6e26c3a62c909ad authored by Pierre-Yves Strub on 27 April 2022, 12:46:45 UTC, committed by Pierre-Yves Strub on 27 April 2022, 12:46:45 UTC
1 parent dbdca26
ecPhlSym.ml
(*-------------------------------------------------------------------- *)
open EcFol
open EcCoreGoal
open EcLowPhlGoal
(*-------------------------------------------------------------------- *)
let build_sym ml mr pr po =
let s = Fsubst.f_subst_id in
let s = Fsubst.f_bind_mem s ml mr in
let s = Fsubst.f_bind_mem s mr ml in
let s = Fsubst.f_subst s in
(s pr, s po)
(*-------------------------------------------------------------------- *)
let t_equivF_sym tc =
let ef = tc1_as_equivF tc in
let pr,po = build_sym mleft mright ef.ef_pr ef.ef_po in
let cond = f_equivF pr ef.ef_fr ef.ef_fl po in
FApi.xmutate1 tc `EquivSym [cond]
(*-------------------------------------------------------------------- *)
let t_equivS_sym tc =
let es = tc1_as_equivS tc in
let pr,po = build_sym (fst es.es_ml) (fst es.es_mr) es.es_pr es.es_po in
let cond = f_equivS_r {
es_ml = fst es.es_ml, snd es.es_mr;
es_mr = fst es.es_mr, snd es.es_ml;
es_sl = es.es_sr;
es_sr = es.es_sl;
es_pr = pr;
es_po = po; } in
FApi.xmutate1 tc `EquivSym [cond]
(*-------------------------------------------------------------------- *)
let t_equiv_sym tc =
match (FApi.tc1_goal tc).f_node with
| FequivF _ -> t_equivF_sym tc
| FequivS _ -> t_equivS_sym tc
| _ -> tc_error_noXhl ~kinds:[`Equiv `Any] !!tc
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...