Skip to content

Commit

Permalink
Adapt to coq/coq#18590
Browse files Browse the repository at this point in the history 
For coq/coq#18590

Change made with
```bash
python -c "$(printf 'import re\nfs = {f:open(f, "r").read() for f in (%s)}\nfs2 = {f:[m for m in re.findall(r"%s", c, flags=re.MULTILINE|re.DOTALL) if not m.startswith("Existing") and ":>" in m and re.search(r"%s", m, flags=re.MULTILINE|re.DOTALL)] for f, c in fs.items()}\nfs3 = {f:m for f, m in fs2.items() if m}\nfs4 = {}\nfor f, m in fs3.items():\n    orig = rep = fs[f]\n    for val in m:\n        rep = rep.replace(val, val.replace(":>", "::"))\n    fs4[f] = rep\nfor f, c in fs4.items():\n    open(f, "w").write(c)' "$(printf '"%s", ' $(git grep --name-only 'Class '))" '(?:Existing\s+)?Class\s.*?\.\s' ':=\s*{')"
```
  • Loading branch information
@JasonGross
JasonGross committed Mar 12, 2024
1 parent 2be0970 commit b0e687c
Show file tree
Hide file tree
Showing 2 changed files with 69 additions and 69 deletions.
16 changes: 8 additions & 8 deletions src/Algebra/Group.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,10 +97,10 @@ Section GroupByIsomorphism.

Class isomorphic_groups :=
{
isomorphic_groups_group_G :> @group G EQ OP ID INV;
isomorphic_groups_group_H :> @group H eq op id inv;
isomorphic_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi';
isomorphic_groups_group_G :: @group G EQ OP ID INV;
isomorphic_groups_group_H :: @group H eq op id inv;
isomorphic_groups_hom_GH :: @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_groups_hom_HG :: @Monoid.is_homomorphism H eq op G EQ OP phi';
}.

Lemma group_by_isomorphism
Expand Down Expand Up @@ -144,10 +144,10 @@ Section CommutativeGroupByIsomorphism.

Class isomorphic_commutative_groups :=
{
isomorphic_commutative_groups_group_G :> @commutative_group G EQ OP ID INV;
isomorphic_commutative_groups_group_H :> @commutative_group H eq op id inv;
isomorphic_commutative_groups_hom_GH :> @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_commutative_groups_hom_HG :> @Monoid.is_homomorphism H eq op G EQ OP phi';
isomorphic_commutative_groups_group_G :: @commutative_group G EQ OP ID INV;
isomorphic_commutative_groups_group_H :: @commutative_group H eq op id inv;
isomorphic_commutative_groups_hom_GH :: @Monoid.is_homomorphism G EQ OP H eq op phi;
isomorphic_commutative_groups_hom_HG :: @Monoid.is_homomorphism H eq op G EQ OP phi';
}.

Lemma commutative_group_by_isomorphism
Expand Down
122 changes: 61 additions & 61 deletions src/LegacyArithmetic/Interface.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -163,16 +163,16 @@ Section InstructionGallery.

Class is_spread_left_immediate (sprl : spread_left_immediate) :=
{
decode_fst_spread_left_immediate :> forall r count,
decode_fst_spread_left_immediate :: forall r count,
0 <= count < n
-> decode (fst (sprl r count)) =~> (decode r << count) mod 2^n;
decode_snd_spread_left_immediate :> forall r count,
decode_snd_spread_left_immediate :: forall r count,
0 <= count < n
-> decode (snd (sprl r count)) =~> (decode r << count) >> n

}.

Class mask_keep_low := { mkl :> W -> imm -> W }.
Class mask_keep_low := { mkl :: W -> imm -> W }.
Global Coercion mkl : mask_keep_low >-> Funclass.

Class is_mask_keep_low (mkl : mask_keep_low) :=
Expand All @@ -184,7 +184,7 @@ Section InstructionGallery.

Class is_bitwise_and (and : bitwise_and) :=
{
decode_bitwise_and :> forall x y, decode (and x y) <~=~> Z.land (decode x) (decode y)
decode_bitwise_and :: forall x y, decode (and x y) <~=~> Z.land (decode x) (decode y)
}.

(** Quoting http://www.felixcloutier.com/x86/AND.html:
Expand All @@ -197,16 +197,16 @@ Section InstructionGallery.

Class is_bitwise_and_with_CF (andf : bitwise_and_with_CF) :=
{
decode_snd_bitwise_and_with_CF :> forall x y, decode (snd (andf x y)) <~=~> Z.land (decode x) (decode y);
fst_bitwise_and_with_CF :> forall x y, fst (andf x y) =~> false
decode_snd_bitwise_and_with_CF :: forall x y, decode (snd (andf x y)) <~=~> Z.land (decode x) (decode y);
fst_bitwise_and_with_CF :: forall x y, fst (andf x y) =~> false
}.

Class bitwise_or := { or : W -> W -> W }.
Global Coercion or : bitwise_or >-> Funclass.

Class is_bitwise_or (or : bitwise_or) :=
{
decode_bitwise_or :> forall x y, decode (or x y) <~=~> Z.lor (decode x) (decode y)
decode_bitwise_or :: forall x y, decode (or x y) <~=~> Z.lor (decode x) (decode y)
}.

(** Quoting http://www.felixcloutier.com/x86/OR.html:
Expand All @@ -219,8 +219,8 @@ Section InstructionGallery.

Class is_bitwise_or_with_CF (orf : bitwise_or_with_CF) :=
{
decode_snd_bitwise_or_with_CF :> forall x y, decode (snd (orf x y)) <~=~> Z.lor (decode x) (decode y);
fst_bitwise_or_with_CF :> forall x y, fst (orf x y) =~> false
decode_snd_bitwise_or_with_CF :: forall x y, decode (snd (orf x y)) <~=~> Z.lor (decode x) (decode y);
fst_bitwise_or_with_CF :: forall x y, fst (orf x y) =~> false
}.

Local Notation bit b := (if b then 1 else 0).
Expand All @@ -230,17 +230,17 @@ Section InstructionGallery.

Class is_add_with_carry (adc : add_with_carry) :=
{
bit_fst_add_with_carry :> forall x y c, bit (fst (adc x y c)) <~=~> (decode x + decode y + bit c) >> n;
decode_snd_add_with_carry :> forall x y c, decode (snd (adc x y c)) <~=~> (decode x + decode y + bit c) mod (2^n)
bit_fst_add_with_carry :: forall x y c, bit (fst (adc x y c)) <~=~> (decode x + decode y + bit c) >> n;
decode_snd_add_with_carry :: forall x y c, decode (snd (adc x y c)) <~=~> (decode x + decode y + bit c) mod (2^n)
}.

Class sub_with_carry := { subc : W -> W -> bool -> bool * W }.
Global Coercion subc : sub_with_carry >-> Funclass.

Class is_sub_with_carry (subc:W->W->bool->bool*W) :=
{
fst_sub_with_carry :> forall x y c, fst (subc x y c) <~=~> ((decode x - decode y - bit c) <? 0);
decode_snd_sub_with_carry :> forall x y c, decode (snd (subc x y c)) <~=~> (decode x - decode y - bit c) mod 2^n
fst_sub_with_carry :: forall x y c, fst (subc x y c) <~=~> ((decode x - decode y - bit c) <? 0);
decode_snd_sub_with_carry :: forall x y c, decode (snd (subc x y c)) <~=~> (decode x - decode y - bit c) mod 2^n
}.

Class multiply := { mul : W -> W -> W }.
Expand Down Expand Up @@ -279,17 +279,17 @@ Section InstructionGallery.
forall x y, decode (mulhwhh x y) <~=~> ((decode x >> w) * (decode y >> w)) mod 2^n.
Class is_mul_double (muldw : multiply_double) :=
{
decode_fst_mul_double :>
decode_fst_mul_double ::
forall x y, decode (fst (muldw x y)) =~> (decode x * decode y) mod 2^n;
decode_snd_mul_double :>
decode_snd_mul_double ::
forall x y, decode (snd (muldw x y)) =~> (decode x * decode y) >> n
}.

Class is_mul_double_with_CF (muldwf : multiply_double_with_CF) :=
{
decode_fst_mul_double_with_CF :>
decode_fst_mul_double_with_CF ::
forall x y, decode (fst (snd (muldwf x y))) =~> (decode x * decode y) mod 2^n;
decode_snd_mul_double_with_CF :>
decode_snd_mul_double_with_CF ::
forall x y, decode (snd (snd (muldwf x y))) =~> (decode x * decode y) >> n
}.

Expand Down Expand Up @@ -388,34 +388,34 @@ Module fancy_machine.
Class instructions (n : Z) :=
{
W : Type (* [n]-bit word *);
decode :> decoder n W;
ldi :> load_immediate W;
shrd :> shift_right_doubleword_immediate W;
shl :> shift_left_immediate W;
shr :> shift_right_immediate W;
adc :> add_with_carry W;
subc :> sub_with_carry W;
mulhwll :> multiply_low_low W;
mulhwhl :> multiply_high_low W;
mulhwhh :> multiply_high_high W;
selc :> select_conditional W;
addm :> add_modulo W
decode :: decoder n W;
ldi :: load_immediate W;
shrd :: shift_right_doubleword_immediate W;
shl :: shift_left_immediate W;
shr :: shift_right_immediate W;
adc :: add_with_carry W;
subc :: sub_with_carry W;
mulhwll :: multiply_low_low W;
mulhwhl :: multiply_high_low W;
mulhwhh :: multiply_high_high W;
selc :: select_conditional W;
addm :: add_modulo W
}.

Class arithmetic {n_over_two} (ops:instructions (2 * n_over_two)) :=
{
decode_range :> is_decode decode;
load_immediate :> is_load_immediate ldi;
shift_right_doubleword_immediate :> is_shift_right_doubleword_immediate shrd;
shift_left_immediate :> is_shift_left_immediate shl;
shift_right_immediate :> is_shift_right_immediate shr;
add_with_carry :> is_add_with_carry adc;
sub_with_carry :> is_sub_with_carry subc;
multiply_low_low :> is_mul_low_low n_over_two mulhwll;
multiply_high_low :> is_mul_high_low n_over_two mulhwhl;
multiply_high_high :> is_mul_high_high n_over_two mulhwhh;
select_conditional :> is_select_conditional selc;
add_modulo :> is_add_modulo addm
decode_range :: is_decode decode;
load_immediate :: is_load_immediate ldi;
shift_right_doubleword_immediate :: is_shift_right_doubleword_immediate shrd;
shift_left_immediate :: is_shift_left_immediate shl;
shift_right_immediate :: is_shift_right_immediate shr;
add_with_carry :: is_add_with_carry adc;
sub_with_carry :: is_sub_with_carry subc;
multiply_low_low :: is_mul_low_low n_over_two mulhwll;
multiply_high_low :: is_mul_high_low n_over_two mulhwhl;
multiply_high_high :: is_mul_high_high n_over_two mulhwhh;
select_conditional :: is_select_conditional selc;
add_modulo :: is_add_modulo addm
}.
End fancy_machine.

Expand All @@ -425,30 +425,30 @@ Module x86.
Class instructions (n : Z) :=
{
W : Type (* [n]-bit word *);
decode :> decoder n W;
ldi :> load_immediate W;
shrdf :> shift_right_doubleword_immediate_with_CF W;
shlf :> shift_left_immediate_with_CF W;
shrf :> shift_right_immediate_with_CF W;
adc :> add_with_carry W;
subc :> sub_with_carry W;
muldwf :> multiply_double_with_CF W;
selc :> select_conditional W;
orf :> bitwise_or_with_CF W
decode :: decoder n W;
ldi :: load_immediate W;
shrdf :: shift_right_doubleword_immediate_with_CF W;
shlf :: shift_left_immediate_with_CF W;
shrf :: shift_right_immediate_with_CF W;
adc :: add_with_carry W;
subc :: sub_with_carry W;
muldwf :: multiply_double_with_CF W;
selc :: select_conditional W;
orf :: bitwise_or_with_CF W
}.

Class arithmetic {n} (ops:instructions n) :=
{
decode_range :> is_decode decode;
load_immediate :> is_load_immediate ldi;
shift_right_doubleword_immediate_with_CF :> is_shift_right_doubleword_immediate_with_CF shrdf;
shift_left_immediate_with_CF :> is_shift_left_immediate_with_CF shlf;
shift_right_immediate_with_CF :> is_shift_right_immediate_with_CF shrf;
add_with_carry :> is_add_with_carry adc;
sub_with_carry :> is_sub_with_carry subc;
multiply_double_with_CF :> is_mul_double_with_CF muldwf;
select_conditional :> is_select_conditional selc;
bitwise_or_with_CF :> is_bitwise_or_with_CF orf
decode_range :: is_decode decode;
load_immediate :: is_load_immediate ldi;
shift_right_doubleword_immediate_with_CF :: is_shift_right_doubleword_immediate_with_CF shrdf;
shift_left_immediate_with_CF :: is_shift_left_immediate_with_CF shlf;
shift_right_immediate_with_CF :: is_shift_right_immediate_with_CF shrf;
add_with_carry :: is_add_with_carry adc;
sub_with_carry :: is_sub_with_carry subc;
multiply_double_with_CF :: is_mul_double_with_CF muldwf;
select_conditional :: is_select_conditional selc;
bitwise_or_with_CF :: is_bitwise_or_with_CF orf
}.
End x86.

Expand Down

0 comments on commit b0e687c

Please sign in to comment.