Skip to content

Commit

Permalink
Adapt to Coq 8.19 and the flocq/interval packages that go with it
Browse files Browse the repository at this point in the history
  • Loading branch information
andrew-appel committed Mar 20, 2024
1 parent a43370d commit 10caf1c
Show file tree
Hide file tree
Showing 2 changed files with 19 additions and 10 deletions.
14 changes: 8 additions & 6 deletions vcfloat/Prune.v
Original file line number Diff line number Diff line change
Expand Up @@ -1172,12 +1172,14 @@ apply (bconstexpr_correct' _ _ _ x vars Heqf H0).
apply Rabs_pos. eassumption. eassumption.
destruct (F.mul_UP_correct p52 t t0).
left. split.
split. apply F'.valid_ub_real; auto.
unfold F.toR in H5. rewrite F.real_correct in H4. destruct (F.toX t); try discriminate.
simpl in H5. pose proof (Rabs_pos (eval e1 vars)); lra.
split. apply F'.valid_ub_real; auto.
unfold F.toR in H7. rewrite F.real_correct in H6. destruct (F.toX t0); try discriminate.
simpl in H7. pose proof (Rabs_pos (eval e2 vars)); lra.
clear - H4 H5.
rewrite F.real_correct in H4. unfold F.is_non_neg'. unfold F.toR in H5.
destruct (F.toX t); try discriminate. simpl in H5.
pose proof (Rabs_pos (eval e1 vars)). lra.
clear - H6 H7.
rewrite F.real_correct in H6. unfold F.is_non_neg'. unfold F.toR in H7.
destruct (F.toX t0); try discriminate. simpl in H7.
pose proof (Rabs_pos (eval e2 vars)). lra.
unfold Xbind2 in H1.
red in H1. unfold F.toR. rewrite F.real_correct in H8.
destruct (F.toX (F.mul_UP p52 t t0)); try discriminate.
Expand Down
15 changes: 11 additions & 4 deletions vcfloat/compute_tactics_ltac2.v
Original file line number Diff line number Diff line change
Expand Up @@ -76,7 +76,9 @@ Ltac2 redflags_full () :=
(* zeta: expand let expressions by substitution *)
Std.rZeta := true;
(* Symbols to expand or not to expand (depending on rDelta) *)
Std.rConst := []
Std.rConst := [];
(* Just guessing that Norm is the right thing here: *)
Std.rStrength := Std.Norm
}.

(** ** Ltac2 functions for evaluation restricted reductions on a term *)
Expand Down Expand Up @@ -131,11 +133,13 @@ Ltac2 rec eval_cbv_uao_lr (head : constr) (rf : Std.red_flags) (term : constr) :
then (Constr.Unsafe.make (Constr.Unsafe.Cast value_r cast type), true)
else (term, false)

(* Commented this out for Coq 8.19
| Constr.Unsafe.Proj projection value =>
let (value_r, value_m) := eval_cbv_uao_lr head rf value in
if value_m
then (Constr.Unsafe.make (Constr.Unsafe.Proj projection value_r), true)
else (term, false)
*)

| Constr.Unsafe.Case case_a constr_return case_b constr_match case_funcs =>
let (match_r, match_m) := eval_cbv_uao_lr head rf constr_match in
Expand Down Expand Up @@ -190,18 +194,21 @@ Ltac2 rec eval_cbv_uao_afr (head : constr) (rf : Std.red_flags) (term : constr)
then (Constr.Unsafe.make (Constr.Unsafe.Cast value_r cast type_r), true)
else (term, false)


(* Commented this out for Coq 8.19
| Constr.Unsafe.Proj projection value =>
let (value_r, value_m) := eval_cbv_uao_afr head rf value in
if value_m
then (Constr.Unsafe.make (Constr.Unsafe.Proj projection value_r), true)
else (term, false)

| Constr.Unsafe.Case case_a constr_return case_b constr_match case_funcs =>
*)
| Constr.Unsafe.Case case_a constr_return_rel case_b constr_match case_funcs =>
let (constr_return, relev) := constr_return_rel in
let (return_r, return_m) := eval_cbv_uao_afr head rf constr_return in
let (match_r, match_m) := eval_cbv_uao_afr head rf constr_match in
let case_funcs_e := Array.map (eval_cbv_uao_afr head rf) case_funcs in
if return_m || match_m || (Array.exist pair_second case_funcs_e)
then (Constr.Unsafe.make (Constr.Unsafe.Case case_a return_r case_b match_r (Array.map pair_first case_funcs_e)), true)
then (Constr.Unsafe.make (Constr.Unsafe.Case case_a (return_r,relev) case_b match_r (Array.map pair_first case_funcs_e)), true)
else (term, false)

| Constr.Unsafe.Fix int_arr int binder_arr constr_arr =>
Expand Down

0 comments on commit 10caf1c

Please sign in to comment.