Skip to content

reduce when needed in proc and call rules #849

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

Merged
bgregoir merged 8 commits into from
Dec 18, 2025
Merged

reduce when needed in proc and call rules #849

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
2f007bd
remove dependancy between ecLowPhlGoal and ecProofTyping
bgregoir Dec 17, 2025
dd71ffb
reduce in t_hF_or_bhF_or_eF
bgregoir Dec 17, 2025
5a13662
add test file
bgregoir Dec 17, 2025
05010df
remove warning
bgregoir Dec 17, 2025
1ff243f
add reduction in call tactic
bgregoir Dec 17, 2025
f902937
add test
bgregoir Dec 17, 2025
e1795e0
optional argument in h_red_until
bgregoir Dec 17, 2025
9dc4381
fix default for h_red_until
bgregoir Dec 17, 2025
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
9 changes: 5 additions & 4 deletions src/ecLowGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -406,7 +406,8 @@ let t_hred_with_info ?target (ri : reduction_info) (tc : tcenv1) =
FApi.tcenv_of_tcenv1 (t_change_r ~fail:true ?target action tc)

(* -------------------------------------------------------------------- *)
let rec t_lazy_match ?(reduce = `Full) (tx : form -> FApi.backward)
let rec t_lazy_match ?(reduce = `Full) ?(texn = fun _ -> raise InvalidGoalShape)
(tx : form -> FApi.backward)
(tc : tcenv1) =
let concl = FApi.tc1_goal tc in
try tx concl tc
Expand All @@ -416,7 +417,7 @@ let rec t_lazy_match ?(reduce = `Full) (tx : form -> FApi.backward)
| `None -> raise InvalidGoalShape
| `Full -> EcReduction.full_red
| `NoDelta -> EcReduction.nodelta in
FApi.t_seq (t_hred_with_info strategy) (t_lazy_match ~reduce tx) tc
FApi.t_seq (FApi.t_or (t_hred_with_info strategy) texn) (t_lazy_match ~reduce tx) tc

(* -------------------------------------------------------------------- *)
type smode = [ `Cbv | `Cbn ]
Expand Down Expand Up @@ -2598,8 +2599,8 @@ let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(
let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) p in
try
Apply.t_apply_bwd_r ~ri ~mode ~canview:false pt tc
with Apply.NoInstance _ ->
t_fail tc
with Apply.NoInstance _ ->
t_fail tc
in

let rec t_apply ctn ip tc =
Expand Down
4 changes: 2 additions & 2 deletions src/ecLowGoal.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ val t_change : ?ri:EcReduction.reduction_info -> ?target:ident -> form -> FApi.

(* -------------------------------------------------------------------- *)
val t_lazy_match:
?reduce:lazyred -> (form -> FApi.backward)-> FApi.backward
?reduce:lazyred -> ?texn:EcCoreGoal.FApi.backward -> (form -> FApi.backward)-> FApi.backward

(* -------------------------------------------------------------------- *)
val t_reflex : ?mode:[`Alpha | `Conv] -> ?reduce:lazyred -> FApi.backward
Expand Down Expand Up @@ -362,4 +362,4 @@ val pp_tc :tcenv -> unit
[@@ocaml.alert debug "Debug function, remove uses before merging"]

val pp_tc1 :tcenv1 -> unit
[@@ocaml.alert debug "Debug function, remove uses before merging"]
[@@ocaml.alert debug "Debug function, remove uses before merging"]
67 changes: 44 additions & 23 deletions src/ecLowPhlGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,27 @@ let tc1_get_stmt side tc =
| _ ->
tc_error_noXhl ~kinds:(hlkinds_Xhl_r `Stmt) !!tc

(* ------------------------------------------------------------------ *)
let tc1_process_codepos_range tc (side, cpr) =
let me, _ = tc1_get_stmt side tc in
let env = FApi.tc1_env tc in
let env = EcEnv.Memory.push_active_ss me env in
EcTyping.trans_codepos_range env cpr

(* ------------------------------------------------------------------ *)
let tc1_process_codepos tc (side, cpos) =
let me, _ = tc1_get_stmt side tc in
let env = FApi.tc1_env tc in
let env = EcEnv.Memory.push_active_ss me env in
EcTyping.trans_codepos env cpos

(* ------------------------------------------------------------------ *)
let tc1_process_codepos1 tc (side, cpos) =
let me, _ = tc1_get_stmt side tc in
let env = FApi.tc1_env tc in
let env = EcEnv.Memory.push_active_ss me env in
EcTyping.trans_codepos1 env cpos

(* -------------------------------------------------------------------- *)
let hl_set_stmt (side : side option) (f : form) (s : stmt) =
match side, f.f_node with
Expand Down Expand Up @@ -256,28 +277,28 @@ let tc1_get_post tc =
(* -------------------------------------------------------------------- *)
let set_pre ~pre f =
match f.f_node, pre with
| FhoareF hf, Inv_ss pre ->
| FhoareF hf, Inv_ss pre ->
let pre = ss_inv_rebind pre hf.hf_m in
f_hoareF pre hf.hf_f (hf_po hf)
| FhoareS hs, Inv_ss pre ->
| FhoareS hs, Inv_ss pre ->
let pre = ss_inv_rebind pre (fst hs.hs_m) in
f_hoareS (snd hs.hs_m) pre hs.hs_s (hs_po hs)
| FeHoareF hf, Inv_ss pre ->
| FeHoareF hf, Inv_ss pre ->
let pre = ss_inv_rebind pre hf.ehf_m in
f_eHoareF pre hf.ehf_f (ehf_po hf)
| FeHoareS hs, Inv_ss pre ->
| FeHoareS hs, Inv_ss pre ->
let pre = ss_inv_rebind pre (fst hs.ehs_m) in
f_eHoareS (snd hs.ehs_m) pre hs.ehs_s (ehs_po hs)
| FbdHoareF hf, Inv_ss pre ->
let pre = ss_inv_rebind pre hf.bhf_m in
f_bdHoareF pre hf.bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf)
| FbdHoareS hs, Inv_ss pre ->
| FbdHoareS hs, Inv_ss pre ->
let pre = ss_inv_rebind pre (fst hs.bhs_m) in
f_bdHoareS (snd hs.bhs_m) pre hs.bhs_s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
| FequivF ef, Inv_ts pre ->
| FequivF ef, Inv_ts pre ->
let pre = ts_inv_rebind pre ef.ef_ml ef.ef_mr in
f_equivF pre ef.ef_fl ef.ef_fr (ef_po ef)
| FequivS es, Inv_ts pre ->
| FequivS es, Inv_ts pre ->
let pre = ts_inv_rebind pre (fst es.es_ml) (fst es.es_mr) in
f_equivS (snd es.es_ml) (snd es.es_mr) pre es.es_sl es.es_sr (es_po es)
| _ -> assert false
Expand Down Expand Up @@ -307,33 +328,33 @@ let t_hS_or_bhS_or_eS ?th ?teh ?tbh ?te tc =
| FeHoareS _ when EcUtils.is_some teh -> (oget teh) tc
| FbdHoareS _ when EcUtils.is_some tbh -> (oget tbh) tc
| FequivS _ when EcUtils.is_some te -> (oget te ) tc

| _ ->
let kinds = List.flatten [
if EcUtils.is_some th then [`Hoare `Stmt] else [];
if EcUtils.is_some teh then [`EHoare `Stmt] else [];
if EcUtils.is_some tbh then [`PHoare `Stmt] else [];
if EcUtils.is_some te then [`Equiv `Stmt] else []]

if EcUtils.is_some th then [`Hoare `Stmt] else [];
if EcUtils.is_some teh then [`EHoare `Stmt] else [];
if EcUtils.is_some tbh then [`PHoare `Stmt] else [];
if EcUtils.is_some te then [`Equiv `Stmt] else []]
in tc_error_noXhl ~kinds !!tc

let t_hF_or_bhF_or_eF ?th ?teh ?tbh ?te ?teg tc =
match (FApi.tc1_goal tc).f_node with
| FhoareF _ when EcUtils.is_some th -> (oget th ) tc
| FeHoareF _ when EcUtils.is_some teh -> (oget teh) tc
| FbdHoareF _ when EcUtils.is_some tbh -> (oget tbh) tc
| FequivF _ when EcUtils.is_some te -> (oget te ) tc
| FeagerF _ when EcUtils.is_some teg -> (oget teg) tc

| _ ->
let texn tc =
let kinds = List.flatten [
if EcUtils.is_some th then [`Hoare `Pred] else [];
if EcUtils.is_some teh then [`EHoare `Pred] else [];
if EcUtils.is_some tbh then [`PHoare `Pred] else [];
if EcUtils.is_some te then [`Equiv `Pred] else [];
if EcUtils.is_some teg then [`Eager ] else []]
in tc_error_noXhl ~kinds !!tc in
let tx f tc =
match f.f_node with
| FhoareF _ when EcUtils.is_some th -> (oget th ) tc
| FeHoareF _ when EcUtils.is_some teh -> (oget teh) tc
| FbdHoareF _ when EcUtils.is_some tbh -> (oget tbh) tc
| FequivF _ when EcUtils.is_some te -> (oget te ) tc
| FeagerF _ when EcUtils.is_some teg -> (oget teg) tc
| _ -> raise EcProofTyping.NoMatch in
EcLowGoal.t_lazy_match ~texn tx tc

in tc_error_noXhl ~kinds !!tc

(* -------------------------------------------------------------------- *)
let tag_sym_with_side ?mc name m =
Expand Down Expand Up @@ -672,7 +693,7 @@ let t_code_transform (side : oside) ?(bdhoare = false) cpos tr tx tc =
let pr, po = bhs_pr bhs, bhs_po bhs in
let (me, stmt, cs) =
tx (pf, hyps) cpos (pr.inv, po.inv) (bhs.bhs_m, bhs.bhs_s) in
let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs)
let concl = f_bdHoareS (snd me) (bhs_pr bhs) stmt (bhs_po bhs)
bhs.bhs_cmp (bhs_bd bhs) in
FApi.xmutate1 tc (tr None) (cs @ [concl])

Expand Down
23 changes: 1 addition & 22 deletions src/ecProofTyping.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ let tc1_process_stmt ?map hyps tc c =

let tc1_process_prhl_stmt ?map tc side c =
let concl = FApi.tc1_goal tc in
let ml, mr = match concl.f_node with
let ml, mr = match concl.f_node with
| FequivS {es_ml=ml; es_mr=mr} -> (ml, mr)
| FeagerF {eg_ml=ml; eg_mr=mr} ->
EcMemory.abstract ml, EcMemory.abstract mr
Expand Down Expand Up @@ -188,27 +188,6 @@ let tc1_process_Xhl_formula ?side tc pf =
let tc1_process_Xhl_formula_xreal tc pf =
tc1_process_Xhl_form tc txreal pf

(* ------------------------------------------------------------------ *)
let tc1_process_codepos_range tc (side, cpr) =
let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
let env = FApi.tc1_env tc in
let env = EcEnv.Memory.push_active_ss me env in
EcTyping.trans_codepos_range env cpr

(* ------------------------------------------------------------------ *)
let tc1_process_codepos tc (side, cpos) =
let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
let env = FApi.tc1_env tc in
let env = EcEnv.Memory.push_active_ss me env in
EcTyping.trans_codepos env cpos

(* ------------------------------------------------------------------ *)
let tc1_process_codepos1 tc (side, cpos) =
let me, _ = EcLowPhlGoal.tc1_get_stmt side tc in
let env = FApi.tc1_env tc in
let env = EcEnv.Memory.push_active_ss me env in
EcTyping.trans_codepos1 env cpos

(* ------------------------------------------------------------------ *)
(* FIXME: factor out to typing module *)
(* FIXME: TC HOOK - check parameter constraints *)
Expand Down
5 changes: 0 additions & 5 deletions src/ecProofTyping.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ open EcIdent
open EcDecl
open EcEnv
open EcCoreGoal
open EcMatching.Position
open EcAst

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -59,10 +58,6 @@ val tc1_process_prhl_stmt :
val tc1_process_Xhl_stmt :
?map:EcTyping.ismap -> tcenv1 -> pstmt -> stmt

val tc1_process_codepos_range : tcenv1 -> oside * pcodepos_range -> codepos_range
val tc1_process_codepos : tcenv1 -> oside * pcodepos -> codepos
val tc1_process_codepos1 : tcenv1 -> oside * pcodepos1 -> codepos1

(* -------------------------------------------------------------------- *)
exception NoMatch

Expand Down
14 changes: 10 additions & 4 deletions src/ecReduction.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1258,23 +1258,23 @@ let rec simplify ri env f =
match f.f_node with
| FhoareF hf when ri.ri.modpath ->
let hf_f = EcEnv.NormMp.norm_xfun env hf.hf_f in
f_map (fun ty -> ty) (simplify ri env)
f_map (fun ty -> ty) (simplify ri env)
(f_hoareF (hf_pr hf) hf_f (hf_po hf))

| FeHoareF hf when ri.ri.modpath ->
let ehf_f = EcEnv.NormMp.norm_xfun env hf.ehf_f in
f_map (fun ty -> ty) (simplify ri env)
f_map (fun ty -> ty) (simplify ri env)
(f_eHoareF (ehf_pr hf) ehf_f (ehf_po hf))

| FbdHoareF hf when ri.ri.modpath ->
let bhf_f = EcEnv.NormMp.norm_xfun env hf.bhf_f in
f_map (fun ty -> ty) (simplify ri env)
f_map (fun ty -> ty) (simplify ri env)
(f_bdHoareF (bhf_pr hf) bhf_f (bhf_po hf) hf.bhf_cmp (bhf_bd hf))

| FequivF ef when ri.ri.modpath ->
let ef_fl = EcEnv.NormMp.norm_xfun env ef.ef_fl in
let ef_fr = EcEnv.NormMp.norm_xfun env ef.ef_fr in
f_map (fun ty -> ty) (simplify ri env)
f_map (fun ty -> ty) (simplify ri env)
(f_equivF (ef_pr ef) ef_fl ef_fr (ef_po ef))

| FeagerF eg when ri.ri.modpath ->
Expand Down Expand Up @@ -1666,6 +1666,12 @@ let h_red_opt ri hyps f =
try Some (h_red ri hyps f)
with NotReducible -> None

let rec h_red_until ?(until = fun _ -> false) ri hyps f =
if until f then f
else match h_red ri hyps f with
| f -> h_red_until ~until ri hyps f
| exception NotReducible -> f

(* -------------------------------------------------------------------- *)
type xconv = [`Eq | `AlphaEq | `Conv]

Expand Down
10 changes: 9 additions & 1 deletion src/ecReduction.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,6 +88,14 @@ val reduce_logic : reduction_info -> env -> LDecl.hyps -> form -> form
val h_red_opt : reduction_info -> LDecl.hyps -> form -> form option
val h_red : reduction_info -> LDecl.hyps -> form -> form

(* [hred_until ~until ri hyps f] performs head reduction on [f]
until [test f] is true or that no more head reduction is possible.
If no [until] argument is provided then head reduction is performed
until it is possible.
*)
val h_red_until :
?until:(form -> bool) -> reduction_info -> LDecl.hyps -> form -> form

val reduce_user_gen :
(EcFol.form -> EcFol.form) ->
reduction_info ->
Expand All @@ -109,4 +117,4 @@ type xconv = [`Eq | `AlphaEq | `Conv]
val xconv : xconv -> LDecl.hyps -> form -> form -> bool

val ss_inv_alpha_eq : LDecl.hyps -> ss_inv -> ss_inv -> bool
val ts_inv_alpha_eq : LDecl.hyps -> ts_inv -> ts_inv -> bool
val ts_inv_alpha_eq : LDecl.hyps -> ts_inv -> ts_inv -> bool
18 changes: 9 additions & 9 deletions src/phl/ecPhlApp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
let (ir1, ir2) = EcIdent.create "r", EcIdent.create "r" in
let (r1 , r2 ) = f_local ir1 treal, f_local ir2 treal in
let condnm =
let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2)
let eqs = map_ss_inv2 f_and (map_ss_inv1 ((EcUtils.flip f_eq) r1) f2)
(map_ss_inv1 ((EcUtils.flip f_eq) r2) g2) in
f_forall
[(ir1, GTty treal); (ir2, GTty treal)]
Expand Down Expand Up @@ -124,11 +124,11 @@ let t_equiv_app_onesided side i pre post tc =
let (ml, mr) = fst es.es_ml, fst es.es_mr in
let s, s', p', q' =
match side with
| `Left ->
| `Left ->
let p' = ss_inv_generalize_right (EcSubst.ss_inv_rebind pre ml) mr in
let q' = ss_inv_generalize_right (EcSubst.ss_inv_rebind post ml) mr in
es.es_sl, es.es_sr, p', q'
| `Right ->
| `Right ->
let p' = ss_inv_generalize_left (EcSubst.ss_inv_rebind pre mr) ml in
let q' = ss_inv_generalize_left (EcSubst.ss_inv_rebind post mr) ml in
es.es_sr, es.es_sl, p', q'
Expand Down Expand Up @@ -227,13 +227,13 @@ let process_app (side, dir, k, phi, bd_info) tc =
| Single i, PAppNone when is_hoareS concl ->
check_side side;
let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) 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 i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
t_ehoare_app i phi tc

| Single i, PAppNone when is_equivS concl ->
Expand All @@ -248,21 +248,21 @@ let process_app (side, dir, k, phi, bd_info) tc =
match side with
| None -> tc_error !!tc "seq onsided: side information expected"
| Some side -> side in
let i = EcProofTyping.tc1_process_codepos1 tc (Some side, i) in
let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some side, i) in
t_equiv_app_onesided side i pre post tc

| Single i, _ when is_bdHoareS concl ->
check_side side;
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
let i = EcProofTyping.tc1_process_codepos1 tc (side, i) in
let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in
t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc

| Double (i, j), PAppNone when is_equivS concl ->
check_side side;
let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in
let i = EcProofTyping.tc1_process_codepos1 tc (Some `Left, i) in
let j = EcProofTyping.tc1_process_codepos1 tc (Some `Left, j) in
let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, i) in
let j = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, j) in
t_equiv_app (i, j) phi tc

| Single _, PAppNone
Expand Down
Loading