Skip to content

Commit f27a007

Browse files
lyonel2017strub
lyonel2017
authored and
strub
committed
Some refactoring
1 parent 7e3db4a commit f27a007

File tree

1 file changed

+40
-124
lines changed

1 file changed

+40
-124
lines changed

‎src/phl/ecPhlWhile.ml

Lines changed: 40 additions & 124 deletions
Original file line numberDiff line numberDiff line change
@@ -340,8 +340,7 @@ let t_equiv_while_disj_r side vrnt inv tc =
340340
FApi.xmutate1 tc `While [b_concl; concl]
341341

342342
(* -------------------------------------------------------------------- *)
343-
344-
module Truc = struct
343+
module LossLess = struct
345344
exception CannotTranslate
346345

347346
let form_of_expr env mother mh =
@@ -406,8 +405,28 @@ module Truc = struct
406405
| _ -> raise CannotTranslate
407406

408407
in fun f -> let e = aux f in (e, !map)
408+
409+
let xhyps evs =
410+
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in
411+
412+
fun m fp ->
413+
let fp =
414+
Mid.fold (fun mh pvs fp ->
415+
let mty = Mid.find_opt mh mtypes in
416+
let fp =
417+
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
418+
f_let1 x (f_pvar pv ty mh) fp)
419+
(EcPV.PVMap.raw pvs) fp
420+
in f_forall_mems [mh, oget mty] fp)
421+
m fp
422+
and cnt =
423+
Mid.fold
424+
(fun _ pvs i -> i + 1 + EcPV.Mnpv.cardinal (EcPV.PVMap.raw pvs))
425+
m 0
426+
in (cnt, fp)
409427
end
410428

429+
(* -------------------------------------------------------------------- *)
411430
let t_equiv_ll_while_disj_r side inv tc =
412431
let env = FApi.tc1_env tc in
413432
let es = tc1_as_equivS tc in
@@ -418,33 +437,19 @@ let t_equiv_ll_while_disj_r side inv tc =
418437
let (e, c), s = tc1_last_while tc s in
419438
let e = form_of_expr (EcMemory.memory m_side) e in
420439

421-
let ll =
422-
let evs = tc1_as_equivS tc in
423-
424-
let xhyps =
425-
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in
426-
427-
fun m fp ->
428-
let fp =
429-
Mid.fold (fun mh pvs fp ->
430-
let mty = Mid.find_opt mh mtypes in
431-
let fp =
432-
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
433-
f_let1 x (f_pvar pv ty mh) fp)
434-
(EcPV.PVMap.raw pvs) fp
435-
in f_forall_mems [mh, oget mty] fp)
436-
m fp
437-
in fp
438-
in
439-
440-
let ml = EcMemory.memory evs.es_ml in
441-
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
442-
let inv = Fsubst.f_subst subst inv in
443-
let e, m = Truc.form_of_expr env (EcMemory.memory evs.es_mr) ml e in
444-
let c = s_while (e, c) in
445-
xhyps m
446-
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
447-
in
440+
let (_,ll) =
441+
try
442+
let evs = tc1_as_equivS tc in
443+
let ml = EcMemory.memory evs.es_ml in
444+
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
445+
let inv = Fsubst.f_subst subst inv in
446+
let e, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml e in
447+
let c = s_while (e, c) in
448+
LossLess.xhyps evs m
449+
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
450+
with LossLess.CannotTranslate ->
451+
tc_error !!tc
452+
"while linking predicates cannot be converted to expressions" in
448453

449454
(* 1. The body preserves the invariant and the loop is lossless. *)
450455

@@ -577,74 +582,6 @@ let process_while side winfos tc =
577582

578583
| _ -> tc_error !!tc "expecting a hoare[...]/equiv[...]"
579584

580-
(* -------------------------------------------------------------------- *)
581-
module ASyncWhile = struct
582-
exception CannotTranslate
583-
584-
let form_of_expr env mother mh =
585-
let map = ref (Mid.add mother (EcPV.PVMap.create env) Mid.empty) in
586-
587-
let rec aux fp =
588-
match fp.f_node with
589-
| Fint z -> e_int z
590-
| Flocal x -> e_local x fp.f_ty
591-
592-
| Fop (p, tys) -> e_op p tys fp.f_ty
593-
| Fapp (f, fs) -> e_app (aux f) (List.map aux fs) fp.f_ty
594-
| Ftuple fs -> e_tuple (List.map aux fs)
595-
| Fproj (f, i) -> e_proj (aux f) i fp.f_ty
596-
597-
| Fif (c, f1, f2) ->
598-
e_if (aux c) (aux f1) (aux f2)
599-
600-
| Fmatch (c, bs, ty) ->
601-
e_match (aux c) (List.map aux bs) ty
602-
603-
| Flet (lp, f1, f2) ->
604-
e_let lp (aux f1) (aux f2)
605-
606-
| Fquant (kd, bds, f) ->
607-
e_quantif (auxkd kd) (List.map auxbd bds) (aux f)
608-
609-
| Fpvar (pv, m) ->
610-
if EcIdent.id_equal m mh then
611-
e_var pv fp.f_ty
612-
else
613-
let bds = odfl (EcPV.PVMap.create env) (Mid.find_opt m !map) in
614-
let idx =
615-
match EcPV.PVMap.find pv bds with
616-
| None ->
617-
let pfx = EcIdent.name m in
618-
let pfx = String.sub pfx 1 (String.length pfx - 1) in
619-
let x = symbol_of_pv pv in
620-
let x = EcIdent.create (x ^ "_" ^ pfx) in
621-
let bds = EcPV.PVMap.add pv (x, fp.f_ty) bds in
622-
map := Mid.add m bds !map; x
623-
| Some (x, _) -> x
624-
625-
in e_local idx fp.f_ty
626-
627-
| Fglob _
628-
| FhoareF _ | FhoareS _
629-
| FeHoareF _ | FeHoareS _
630-
| FbdHoareF _ | FbdHoareS _
631-
| FequivF _ | FequivS _
632-
| FeagerF _ | Fpr _ -> raise CannotTranslate
633-
634-
and auxkd (kd : quantif) : equantif =
635-
match kd with
636-
| Lforall -> `EForall
637-
| Lexists -> `EExists
638-
| Llambda -> `ELambda
639-
640-
and auxbd ((x, bd) : binding) =
641-
match bd with
642-
| GTty ty -> (x, ty)
643-
| _ -> raise CannotTranslate
644-
645-
in fun f -> let e = aux f in (e, !map)
646-
end
647-
648585
(* -------------------------------------------------------------------- *)
649586
let process_async_while (winfos : EP.async_while_info) tc =
650587
let e_and e1 e2 =
@@ -729,52 +666,31 @@ let process_async_while (winfos : EP.async_while_info) tc =
729666
in (hr1, hr2)
730667
in
731668

732-
let xhyps =
733-
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in
734-
735-
fun m fp ->
736-
let fp =
737-
Mid.fold (fun mh pvs fp ->
738-
let mty = Mid.find_opt mh mtypes in
739-
let fp =
740-
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
741-
f_let1 x (f_pvar pv ty mh) fp)
742-
(EcPV.PVMap.raw pvs) fp
743-
in f_forall_mems [mh, oget mty] fp)
744-
m fp
745-
and cnt =
746-
Mid.fold
747-
(fun _ pvs i -> i + 1 + EcPV.Mnpv.cardinal (EcPV.PVMap.raw pvs))
748-
m 0
749-
in (cnt, fp)
750-
in
751-
752669
let (c1, ll1), (c2, ll2) =
753670
try
754671
let ll1 =
755672
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
756673
let inv = Fsubst.f_subst subst inv in
757674
let test = f_ands [fe1; f_not p0; p1] in
758-
let test, m = ASyncWhile.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
675+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
759676
let c = s_while (test, cl) in
760-
xhyps m
677+
LossLess.xhyps evs m
761678
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
762679

763680
and ll2 =
764681
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id mr mhr in
765682
let inv = Fsubst.f_subst subst inv in
766683
let test = f_ands [fe1; f_not p0; f_not p1] in
767-
let test, m = ASyncWhile.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
684+
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
768685
let c = s_while (test, cr) in
769-
xhyps m
686+
LossLess.xhyps evs m
770687
(f_bdHoareS (mhr, EcMemory.memtype evs.es_mr) inv c f_true FHeq f_r1)
771688

772689
in (ll1, ll2)
773690

774-
with ASyncWhile.CannotTranslate ->
691+
with LossLess.CannotTranslate ->
775692
tc_error !!tc
776-
"async-while linking predicates cannot be converted to expressions"
777-
in
693+
"async-while linking predicates cannot be converted to expressions" in
778694

779695
let concl =
780696
let post = f_imps [f_not fe1; f_not fe2; inv] evs.es_po in

0 commit comments

Comments
 (0)