https://github.com/EasyCrypt/easycrypt
Tip revision: a2c11f189da68d291d48547461aff2432662e9e8 authored by François Dupressoir on 05 September 2024, 14:37:36 UTC
[ci] diversified external CI selects a valid branch
[ci] diversified external CI selects a valid branch
Tip revision: a2c11f1
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