| Some : A → option A.
ndefinition eq_option ≝
-λT.λop1,op2:option T.λf:T → T → bool.
+λT.λf:T → T → bool.λop1,op2:option T.
match op1 with
[ None ⇒ match op2 with [ None ⇒ true | Some _ ⇒ false ]
| Some x1 ⇒ match op2 with [ None ⇒ false | Some x2 ⇒ f x1 x2 ]
nqed.
nlemma symmetric_eqoption :
-∀T:Type.∀op1,op2:option T.∀f:T → T → bool.
+∀T:Type.∀f:T → T → bool.∀op1,op2:option T.
(symmetricT T bool f) →
- (eq_option T op1 op2 f = eq_option T op2 op1 f).
- #T; #op1; #op2; #f; #H;
+ (eq_option T f op1 op2 = eq_option T f op2 op1).
+ #T; #f; #op1; #op2; #H;
nelim op1;
nelim op2;
nnormalize;
nqed.
nlemma eq_to_eqoption :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.∀op1,op2:option T.
(∀x1,x2:T.x1 = x2 → f x1 x2 = true) →
- (op1 = op2 → eq_option T op1 op2 f = true).
- #T; #op1; #op2; #f; #H;
+ (op1 = op2 → eq_option T f op1 op2 = true).
+ #T; #f; #op1; #op2; #H;
nelim op1;
nelim op2;
nnormalize;
nqed.
nlemma eqoption_to_eq :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.∀op1,op2:option T.
(∀x1,x2:T.f x1 x2 = true → x1 = x2) →
- (eq_option T op1 op2 f = true → op1 = op2).
- #T; #op1; #op2; #f; #H;
+ (eq_option T f op1 op2 = true → op1 = op2).
+ #T; #f; #op1; #op2; #H;
nelim op1;
nelim op2;
nnormalize;
nqed.
nlemma neq_to_neqoption :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.∀op1,op2:option T.
(∀x1,x2:T.x1 ≠ x2 → f x1 x2 = false) →
- (op1 ≠ op2 → eq_option T op1 op2 f = false).
- #T; #op1; nelim op1;
+ (op1 ≠ op2 → eq_option T f op1 op2 = false).
+ #T; #f; #op1; nelim op1;
##[ ##1: #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1; nelim (H1 (refl_eq …))
- ##| ##2: #yy; #f; #H; nnormalize; #H1; napply refl_eq
+ ##[ ##1: nnormalize; #H; #H1; nelim (H1 (refl_eq …))
+ ##| ##2: #yy; #H; nnormalize; #H1; napply refl_eq
##]
##| ##2: #xx; #op2; ncases op2;
- ##[ ##1: #f; #H; nnormalize; #H1; napply refl_eq
- ##| ##2: #yy; #f; #H; nnormalize; #H1; napply (H xx yy …);
+ ##[ ##1: #H; nnormalize; #H1; napply refl_eq
+ ##| ##2: #yy; #H; nnormalize; #H1; napply (H xx yy …);
nnormalize; #H2; nrewrite > H2 in H1:(%); #H1;
napply (H1 (refl_eq …))
##]
nqed.
nlemma neqoption_to_neq :
-∀T.∀op1,op2:option T.∀f:T → T → bool.
+∀T.∀f:T → T → bool.∀op1,op2:option T.
(∀x1,x2:T.f x1 x2 = false → x1 ≠ x2) →
- (eq_option T op1 op2 f = false → op1 ≠ op2).
- #T; #op1; nelim op1;
+ (eq_option T f op1 op2 = false → op1 ≠ op2).
+ #T; #f; #op1; nelim op1;
##[ ##1: #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1;
+ ##[ ##1: nnormalize; #H; #H1;
ndestruct (*napply (bool_destruct … H1)*)
- ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2;
+ ##| ##2: #yy; #H; nnormalize; #H1; #H2;
(* !!! ndestruct: assert false *)
napply (option_destruct_none_some T … H2)
##]
##| ##2: #xx; #op2; ncases op2;
- ##[ ##1: nnormalize; #f; #H; #H1; #H2;
+ ##[ ##1: nnormalize; #H; #H1; #H2;
(* !!! ndestruct: assert false *)
napply (option_destruct_some_none T … H2)
- ##| ##2: #yy; #f; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
+ ##| ##2: #yy; #H; nnormalize; #H1; #H2; napply (H xx yy H1 ?);
napply (option_destruct_some_some T … H2)
##]
##]
λT1,T2:Type.λp:ProdT T1 T2.match p with [ pair _ x ⇒ x ].
ndefinition eq_pair ≝
-λT1,T2:Type.λp1,p2:ProdT T1 T2.
+λT1,T2:Type.
λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.
+λp1,p2:ProdT T1 T2.
(f1 (fst … p1) (fst … p2)) ⊗
(f2 (snd … p1) (snd … p2)).
λT1.λT2.λT3.λp:Prod3T T1 T2 T3.match p with [ triple _ _ x ⇒ x ].
ndefinition eq_triple ≝
-λT1,T2,T3:Type.λp1,p2:Prod3T T1 T2 T3.
+λT1,T2,T3:Type.
λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.
+λp1,p2:Prod3T T1 T2 T3.
(f1 (fst3T … p1) (fst3T … p2)) ⊗
(f2 (snd3T … p1) (snd3T … p2)) ⊗
(f3 (thd3T … p1) (thd3T … p2)).
λT1.λT2.λT3.λT4.λp:Prod4T T1 T2 T3 T4.match p with [ quadruple _ _ _ x ⇒ x ].
ndefinition eq_quadruple ≝
-λT1,T2,T3,T4:Type.λp1,p2:Prod4T T1 T2 T3 T4.
+λT1,T2,T3,T4:Type.
λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.
+λp1,p2:Prod4T T1 T2 T3 T4.
(f1 (fst4T … p1) (fst4T … p2)) ⊗
(f2 (snd4T … p1) (snd4T … p2)) ⊗
(f3 (thd4T … p1) (thd4T … p2)) ⊗
λT1.λT2.λT3.λT4.λT5.λp:Prod5T T1 T2 T3 T4 T5.match p with [ quintuple _ _ _ _ x ⇒ x ].
ndefinition eq_quintuple ≝
-λT1,T2,T3,T4,T5:Type.λp1,p2:Prod5T T1 T2 T3 T4 T5.
+λT1,T2,T3,T4,T5:Type.
λf1:T1 → T1 → bool.λf2:T2 → T2 → bool.λf3:T3 → T3 → bool.λf4:T4 → T4 → bool.λf5:T5 → T5 → bool.
+λp1,p2:Prod5T T1 T2 T3 T4 T5.
(f1 (fst5T … p1) (fst5T … p2)) ⊗
(f2 (snd5T … p1) (snd5T … p2)) ⊗
(f3 (thd5T … p1) (thd5T … p2)) ⊗
nqed.
nlemma symmetric_eqpair :
-∀T1,T2:Type.∀p1,p2:ProdT T1 T2.
+∀T1,T2:Type.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀p1,p2:ProdT T1 T2.
(symmetricT T1 bool f1) →
(symmetricT T2 bool f2) →
- (eq_pair T1 T2 p1 p2 f1 f2 = eq_pair T1 T2 p2 p1 f1 f2).
- #T1; #T2; #p1; #p2; #f1; #f2; #H; #H1;
+ (eq_pair T1 T2 f1 f2 p1 p2 = eq_pair T1 T2 f1 f2 p1 p2).
+ #T1; #T2; #f1; #f2; #p1; #p2; #H; #H1;
nelim p1;
#x1; #y1;
nelim p2;
nqed.
nlemma eq_to_eqpair :
-∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀T1,T2.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀p1,p2:ProdT T1 T2.
(∀x,y:T1.x = y → f1 x y = true) →
(∀x,y:T2.x = y → f2 x y = true) →
- (p1 = p2 → eq_pair T1 T2 p1 p2 f1 f2 = true).
- #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ (p1 = p2 → eq_pair T1 T2 f1 f2 p1 p2 = true).
+ #T1; #T2; #f1; #f2; #p1; #p2; #H1; #H2;
nelim p1;
#x1; #y1;
nelim p2;
nqed.
nlemma eqpair_to_eq :
-∀T1,T2.∀p1,p2:ProdT T1 T2.
+∀T1,T2.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀p1,p2:ProdT T1 T2.
(∀x,y:T1.f1 x y = true → x = y) →
(∀x,y:T2.f2 x y = true → x = y) →
- (eq_pair T1 T2 p1 p2 f1 f2 = true → p1 = p2).
- #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ (eq_pair T1 T2 f1 f2 p1 p2 = true → p1 = p2).
+ #T1; #T2; #f1; #f2; #p1; #p2; #H1; #H2;
nelim p1;
#x1; #y1;
nelim p2;
nqed.
nlemma neqpair_to_neq :
- ∀T1,T2.∀p1,p2:ProdT T1 T2.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀T1,T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀p1,p2:ProdT T1 T2.
(∀x,y:T1.f1 x y = false → x ≠ y) →
(∀x,y:T2.f2 x y = false → x ≠ y) →
- (eq_pair T1 T2 p1 p2 f1 f2 = false → p1 ≠ p2).
- #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2;
+ (eq_pair T1 T2 f1 f2 p1 p2 = false → p1 ≠ p2).
+ #T1; #T2; #f1; #f2; #p1; #p2; #H1; #H2;
nelim p1;
#x1; #y1;
nelim p2;
nqed.
nlemma neq_to_neqpair :
- ∀T1,T2.∀p1,p2:ProdT T1 T2.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀T1,T2.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.
+∀p1,p2:ProdT T1 T2.
(∀x,y:T1.decidable (x = y)) →
(∀x,y:T2.decidable (x = y)) →
(∀x,y:T1.x ≠ y → f1 x y = false) →
(∀x,y:T2.x ≠ y → f2 x y = false) →
- (p1 ≠ p2 → eq_pair T1 T2 p1 p2 f1 f2 = false).
- #T1; #T2; #p1; #p2; #f1; #f2; #H1; #H2; #H3; #H4;
+ (p1 ≠ p2 → eq_pair T1 T2 f1 f2 p1 p2 = false).
+ #T1; #T2; #f1; #f2; #p1; #p2; #H1; #H2; #H3; #H4;
nelim p1;
#x1; #y1;
nelim p2;
nqed.
nlemma symmetric_eqtriple :
-∀T1,T2,T3:Type.∀p1,p2:Prod3T T1 T2 T3.
+∀T1,T2,T3:Type.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀p1,p2:Prod3T T1 T2 T3.
(symmetricT T1 bool f1) →
(symmetricT T2 bool f2) →
(symmetricT T3 bool f3) →
- (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = eq_triple T1 T2 T3 p2 p1 f1 f2 f3).
- #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H; #H1; #H2;
+ (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = eq_triple T1 T2 T3 f1 f2 f3 p2 p1).
+ #T1; #T2; #T3; #f1; #f2; #f3; #p1; #p2; #H; #H1; #H2;
nelim p1;
#x1; #y1; #z1;
nelim p2;
nqed.
nlemma eq_to_eqtriple :
-∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀T1,T2,T3.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀p1,p2:Prod3T T1 T2 T3.
(∀x1,x2:T1.x1 = x2 → f1 x1 x2 = true) →
(∀y1,y2:T2.y1 = y2 → f2 y1 y2 = true) →
(∀z1,z2:T3.z1 = z2 → f3 z1 z2 = true) →
- (p1 = p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true).
- #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ (p1 = p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true).
+ #T1; #T2; #T3; #f1; #f2; #f3; #p1; #p2; #H1; #H2; #H3;
nelim p1;
#x1; #y1; #z1;
nelim p2;
nqed.
nlemma eqtriple_to_eq :
-∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
+∀T1,T2,T3.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀p1,p2:Prod3T T1 T2 T3.
(∀x1,x2:T1.f1 x1 x2 = true → x1 = x2) →
(∀y1,y2:T2.f2 y1 y2 = true → y1 = y2) →
(∀z1,z2:T3.f3 z1 z2 = true → z1 = z2) →
- (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = true → p1 = p2).
- #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = true → p1 = p2).
+ #T1; #T2; #T3; #f1; #f2; #f3; #p1; #p2; #H1; #H2; #H3;
nelim p1;
#x1; #y1; #z1;
nelim p2;
nqed.
nlemma neqtriple_to_neq :
- ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀T1,T2,T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀p1,p2:Prod3T T1 T2 T3.
(∀x,y:T1.f1 x y = false → x ≠ y) →
(∀x,y:T2.f2 x y = false → x ≠ y) →
(∀x,y:T3.f3 x y = false → x ≠ y) →
- (eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false → p1 ≠ p2).
- #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3;
+ (eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #f1; #f2; #f3; #p1; #p2; #H1; #H2; #H3;
nelim p1;
#x1; #y1; #z1;
nelim p2;
nqed.
nlemma neq_to_neqtriple :
- ∀T1,T2,T3.∀p1,p2:Prod3T T1 T2 T3.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀T1,T2,T3.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.
+∀p1,p2:Prod3T T1 T2 T3.
(∀x,y:T1.decidable (x = y)) →
(∀x,y:T2.decidable (x = y)) →
(∀x,y:T3.decidable (x = y)) →
(∀x,y:T1.x ≠ y → f1 x y = false) →
(∀x,y:T2.x ≠ y → f2 x y = false) →
(∀x,y:T3.x ≠ y → f3 x y = false) →
- (p1 ≠ p2 → eq_triple T1 T2 T3 p1 p2 f1 f2 f3 = false).
- #T1; #T2; #T3; #p1; #p2; #f1; #f2; #f3; #H1; #H2; #H3; #H4; #H5; #H6;
+ (p1 ≠ p2 → eq_triple T1 T2 T3 f1 f2 f3 p1 p2 = false).
+ #T1; #T2; #T3; #f1; #f2; #f3; #p1; #p2; #H1; #H2; #H3; #H4; #H5; #H6;
nelim p1;
#x1; #y1; #z1;
nelim p2;
nqed.
nlemma symmetric_eqquadruple :
-∀T1,T2,T3,T4:Type.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀T1,T2,T3,T4:Type.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀p1,p2:Prod4T T1 T2 T3 T4.
(symmetricT T1 bool f1) →
(symmetricT T2 bool f2) →
(symmetricT T3 bool f3) →
(symmetricT T4 bool f4) →
- (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = eq_quadruple T1 T2 T3 T4 p2 p1 f1 f2 f3 f4).
- #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H; #H1; #H2; #H3;
+ (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p2 p1).
+ #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #p1; #p2; #H; #H1; #H2; #H3;
nelim p1;
#x1; #y1; #z1; #v1;
nelim p2;
nqed.
nlemma eq_to_eqquadruple :
-∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀T1,T2,T3,T4.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀p1,p2:Prod4T T1 T2 T3 T4.
(∀x,y:T1.x = y → f1 x y = true) →
(∀x,y:T2.x = y → f2 x y = true) →
(∀x,y:T3.x = y → f3 x y = true) →
(∀x,y:T4.x = y → f4 x y = true) →
- (p1 = p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true).
- #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ (p1 = p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true).
+ #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #p1; #p2; #H1; #H2; #H3; #H4;
nelim p1;
#x1; #y1; #z1; #v1;
nelim p2;
nqed.
nlemma eqquadruple_to_eq :
-∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
+∀T1,T2,T3,T4.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀p1,p2:Prod4T T1 T2 T3 T4.
(∀x,y:T1.f1 x y = true → x = y) →
(∀x,y:T2.f2 x y = true → x = y) →
(∀x,y:T3.f3 x y = true → x = y) →
(∀x,y:T4.f4 x y = true → x = y) →
- (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = true → p1 = p2).
- #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #p1; #p2; #H1; #H2; #H3; #H4;
nelim p1;
#x1; #y1; #z1; #v1;
nelim p2;
nqed.
nlemma neqquadruple_to_neq :
- ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀T1,T2,T3,T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀p1,p2:Prod4T T1 T2 T3 T4.
(∀x,y:T1.f1 x y = false → x ≠ y) →
(∀x,y:T2.f2 x y = false → x ≠ y) →
(∀x,y:T3.f3 x y = false → x ≠ y) →
(∀x,y:T4.f4 x y = false → x ≠ y) →
- (eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false → p1 ≠ p2).
- #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4;
+ (eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #p1; #p2; #H1; #H2; #H3; #H4;
nelim p1;
#x1; #y1; #z1; #v1;
nelim p2;
nqed.
nlemma neq_to_neqquadruple :
- ∀T1,T2,T3,T4.∀p1,p2:Prod4T T1 T2 T3 T4.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀T1,T2,T3,T4.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.
+∀p1,p2:Prod4T T1 T2 T3 T4.
(∀x,y:T1.decidable (x = y)) →
(∀x,y:T2.decidable (x = y)) →
(∀x,y:T3.decidable (x = y)) →
(∀x,y:T2.x ≠ y → f2 x y = false) →
(∀x,y:T3.x ≠ y → f3 x y = false) →
(∀x,y:T4.x ≠ y → f4 x y = false) →
- (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 p1 p2 f1 f2 f3 f4 = false).
- #T1; #T2; #T3; #T4; #p1; #p2; #f1; #f2; #f3; #f4; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
+ (p1 ≠ p2 → eq_quadruple T1 T2 T3 T4 f1 f2 f3 f4 p1 p2 = false).
+ #T1; #T2; #T3; #T4; #f1; #f2; #f3; #f4; #p1; #p2; #H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8;
nelim p1;
#x1; #y1; #z1; #v1;
nelim p2;
nqed.
nlemma symmetric_eqquintuple :
-∀T1,T2,T3,T4,T5:Type.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀T1,T2,T3,T4,T5:Type.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀p1,p2:Prod5T T1 T2 T3 T4 T5.
(symmetricT T1 bool f1) →
(symmetricT T2 bool f2) →
(symmetricT T3 bool f3) →
(symmetricT T4 bool f4) →
(symmetricT T5 bool f5) →
- (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = eq_quintuple T1 T2 T3 T4 T5 p2 p1 f1 f2 f3 f4 f5).
- #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H; #H1; #H2; #H3; #H4;
+ (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p2 p1).
+ #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #p1; #p2; #H; #H1; #H2; #H3; #H4;
nelim p1;
#x1; #y1; #z1; #v1; #w1;
nelim p2;
nqed.
nlemma eq_to_eqquintuple :
-∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀T1,T2,T3,T4,T5.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀p1,p2:Prod5T T1 T2 T3 T4 T5.
(∀x,y:T1.x = y → f1 x y = true) →
(∀x,y:T2.x = y → f2 x y = true) →
(∀x,y:T3.x = y → f3 x y = true) →
(∀x,y:T4.x = y → f4 x y = true) →
(∀x,y:T5.x = y → f5 x y = true) →
- (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true).
- #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ (p1 = p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true).
+ #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #p1; #p2; #H1; #H2; #H3; #H4; #H5;
nelim p1;
#x1; #y1; #z1; #v1; #w1;
nelim p2;
nqed.
nlemma eqquintuple_to_eq :
-∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
+∀T1,T2,T3,T4,T5.
∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀p1,p2:Prod5T T1 T2 T3 T4 T5.
(∀x,y:T1.f1 x y = true → x = y) →
(∀x,y:T2.f2 x y = true → x = y) →
(∀x,y:T3.f3 x y = true → x = y) →
(∀x,y:T4.f4 x y = true → x = y) →
(∀x,y:T5.f5 x y = true → x = y) →
- (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = true → p1 = p2).
- #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = true → p1 = p2).
+ #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #p1; #p2; #H1; #H2; #H3; #H4; #H5;
nelim p1;
#x1; #y1; #z1; #v1; #w1;
nelim p2;
nqed.
nlemma neqquintuple_to_neq :
- ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀T1,T2,T3,T4,T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀p1,p2:Prod5T T1 T2 T3 T4 T5.
(∀x,y:T1.f1 x y = false → x ≠ y) →
(∀x,y:T2.f2 x y = false → x ≠ y) →
(∀x,y:T3.f3 x y = false → x ≠ y) →
(∀x,y:T4.f4 x y = false → x ≠ y) →
(∀x,y:T5.f5 x y = false → x ≠ y) →
- (eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false → p1 ≠ p2).
- #T1; #T2; #T3; #T4; #T5; #p1; #p2; #f1; #f2; #f3; #f4; #f5; #H1; #H2; #H3; #H4; #H5;
+ (eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false → p1 ≠ p2).
+ #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #p1; #p2; #H1; #H2; #H3; #H4; #H5;
nelim p1;
#x1; #y1; #z1; #v1; #w1;
nelim p2;
nqed.
nlemma neq_to_neqquintuple :
- ∀T1,T2,T3,T4,T5.∀p1,p2:Prod5T T1 T2 T3 T4 T5.
- ∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀T1,T2,T3,T4,T5.
+∀f1:T1 → T1 → bool.∀f2:T2 → T2 → bool.∀f3:T3 → T3 → bool.∀f4:T4 → T4 → bool.∀f5:T5 → T5 → bool.
+∀p1,p2:Prod5T T1 T2 T3 T4 T5.
(∀x,y:T1.decidable (x = y)) →
(∀x,y:T2.decidable (x = y)) →
(∀x,y:T3.decidable (x = y)) →
(∀x,y:T3.x ≠ y → f3 x y = false) →
(∀x,y:T4.x ≠ y → f4 x y = false) →
(∀x,y:T5.x ≠ y → f5 x y = false) →
- (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 p1 p2 f1 f2 f3 f4 f5 = false).
- #T1; #T2; #T3; #T4; #T5; #p1; #p2;
- #f1; #f2; #f3; #f4; #f5;
+ (p1 ≠ p2 → eq_quintuple T1 T2 T3 T4 T5 f1 f2 f3 f4 f5 p1 p2 = false).
+ #T1; #T2; #T3; #T4; #T5; #f1; #f2; #f3; #f4; #f5; #p1; #p2;
#H1; #H2; #H3; #H4; #H5; #H6; #H7; #H8; #H9; #H10;
nelim p1;
#x1; #y1; #z1; #v1; #w1;
num/quatern.ma num/bool.ma
num/exadecim.ma common/nat.ma common/prod.ma num/bool.ma num/oct.ma num/quatern.ma
num/bitrigesim_lemmas.ma num/bitrigesim.ma num/bool_lemmas.ma
-emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/opcode.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/RS08_status.ma
+emulator/status/status.ma emulator/memory/memory_abs.ma emulator/opcodes/opcode.ma emulator/status/HC05_status.ma emulator/status/HC08_status.ma emulator/status/IP2022_status.ma emulator/status/RS08_status.ma
num/byte8.ma num/bitrigesim.ma num/exadecim.ma
emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/HC08_instr_mode.ma emulator/opcodes/HC08_opcode.ma emulator/opcodes/byte_or_word.ma
common/nat_lemmas.ma common/nat.ma num/bool_lemmas.ma
emulator/opcodes/RS08_table_tests.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma
test_errori.ma
compiler/environment.ma common/string.ma compiler/ast_type.ma
-emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma
common/ascii_lemmas.ma common/ascii.ma num/bool_lemmas.ma
+emulator/translation/translation_base.ma common/option.ma emulator/opcodes/HC05_table.ma emulator/opcodes/HC08_table.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/RS08_table.ma emulator/opcodes/opcode.ma
emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_opcode.ma emulator/opcodes/byte_or_word.ma
emulator/status/HC05_status.ma num/word16.ma
emulator/memory/memory_bits.ma emulator/memory/memory_trees.ma
emulator/opcodes/HC08_opcode.ma num/bool.ma
num/exadecim_lemmas.ma num/bool_lemmas.ma num/exadecim.ma
num/word16_lemmas.ma num/byte8_lemmas.ma num/word16.ma
-emulator/status/status_getter.ma emulator/status/status.ma
+emulator/status/status_getter.ma emulator/status/status_setter.ma
+num/word24.ma num/byte8.ma
num/bool_lemmas.ma num/bool.ma
emulator/memory/memory_abs.ma emulator/memory/memory_bits.ma emulator/memory/memory_func.ma emulator/memory/memory_trees.ma
emulator/opcodes/RS08_opcode.ma num/bool.ma
emulator/opcodes/HCS08_table_tests.ma emulator/opcodes/HCS08_table.ma emulator/opcodes/opcode.ma
emulator/opcodes/HC05_instr_mode.ma num/word16.ma
emulator/opcodes/IP2022_table_tests.ma emulator/opcodes/IP2022_table.ma emulator/opcodes/opcode.ma
+emulator/status/IP2022_status.ma emulator/memory/memory_struct.ma num/word16.ma num/word24.ma
num/quatern_lemmas.ma num/bool_lemmas.ma num/quatern.ma
emulator/memory/memory_func.ma common/list.ma common/option.ma emulator/memory/memory_struct.ma num/word32.ma
emulator/opcodes/RS08_instr_mode.ma num/word16.ma
; a16_9 : T ; a16_10 : T ; a16_11 : T ; a16_12 : T
; a16_13 : T ; a16_14 : T ; a16_15 : T ; a16_16 : T }.
+(* operatore uguaglianza *)
+ndefinition eq_ar16 ≝
+λT.λf:T → T → bool.λa1,a2:Array16T T.
+ (f (a16_1 ? a1) (a16_1 ? a2)) ⊗ (f (a16_2 ? a1) (a16_2 ? a2)) ⊗
+ (f (a16_3 ? a1) (a16_3 ? a2)) ⊗ (f (a16_4 ? a1) (a16_4 ? a2)) ⊗
+ (f (a16_5 ? a1) (a16_5 ? a2)) ⊗ (f (a16_6 ? a1) (a16_6 ? a2)) ⊗
+ (f (a16_7 ? a1) (a16_7 ? a2)) ⊗ (f (a16_8 ? a1) (a16_8 ? a2)) ⊗
+ (f (a16_9 ? a1) (a16_9 ? a2)) ⊗ (f (a16_10 ? a1) (a16_10 ? a2)) ⊗
+ (f (a16_11 ? a1) (a16_11 ? a2)) ⊗ (f (a16_12 ? a1) (a16_12 ? a2)) ⊗
+ (f (a16_13 ? a1) (a16_13 ? a2)) ⊗ (f (a16_14 ? a1) (a16_14 ? a2)) ⊗
+ (f (a16_15 ? a1) (a16_15 ? a2)) ⊗ (f (a16_16 ? a1) (a16_16 ? a2)).
+
(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *)
(* posso definire un getter a matrice sull'array *)
{ a8_1 : T ; a8_2 : T ; a8_3 : T ; a8_4 : T
; a8_5 : T ; a8_6 : T ; a8_7 : T ; a8_8 : T }.
+(* operatore uguaglianza *)
+ndefinition eq_ar8 ≝
+λT.λf:T → T → bool.λa1,a2:Array8T T.
+ (f (a8_1 ? a1) (a8_1 ? a2)) ⊗ (f (a8_2 ? a1) (a8_2 ? a2)) ⊗
+ (f (a8_3 ? a1) (a8_3 ? a2)) ⊗ (f (a8_4 ? a1) (a8_4 ? a2)) ⊗
+ (f (a8_5 ? a1) (a8_5 ? a2)) ⊗ (f (a8_6 ? a1) (a8_6 ? a2)) ⊗
+ (f (a8_7 ? a1) (a8_7 ? a2)) ⊗ (f (a8_8 ? a1) (a8_8 ? a2)).
+
(* abbiamo gia' gli ottali come tipo induttivo quindi: *)
(* posso definire un getter a matrice sull'array *)
ndefinition getn_array8T ≝
let e06 ≝ (a8_7 T p) in
let e07 ≝ (a8_8 T p) in
match n with
- [ o0 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 e01 v
- | o1 ⇒ mk_Array8T T e07 e06 e05 e04 e03 e02 v e00
- | o2 ⇒ mk_Array8T T e07 e06 e05 e04 e03 v e01 e00
- | o3 ⇒ mk_Array8T T e07 e06 e05 e04 v e02 e01 e00
- | o4 ⇒ mk_Array8T T e07 e06 e05 v e03 e02 e01 e00
- | o5 ⇒ mk_Array8T T e07 e06 v e04 e03 e02 e01 e00
- | o6 ⇒ mk_Array8T T e07 v e05 e04 e03 e02 e01 e00
- | o7 ⇒ mk_Array8T T v e06 e05 e04 e03 e02 e01 e00
+ [ o0 ⇒ mk_Array8T T v e01 e02 e03 e04 e05 e06 e07
+ | o1 ⇒ mk_Array8T T e00 v e02 e03 e04 e05 e06 e07
+ | o2 ⇒ mk_Array8T T e00 e01 v e03 e04 e05 e06 e07
+ | o3 ⇒ mk_Array8T T e00 e01 e02 v e04 e05 e06 e07
+ | o4 ⇒ mk_Array8T T e00 e01 e02 e03 v e05 e06 e07
+ | o5 ⇒ mk_Array8T T e00 e01 e02 e03 e04 v e06 e07
+ | o6 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 v e07
+ | o7 ⇒ mk_Array8T T e00 e01 e02 e03 e04 e05 e06 v
].
(* lettura byte *)
ndefinition byte8_of_bits ≝
λp:Array8T bool.
mk_byte8
- (or_ex (match a8_8 ? p with [ true ⇒ x8 | false ⇒ x0 ])
- (or_ex (match a8_7 ? p with [ true ⇒ x4 | false ⇒ x0 ])
- (or_ex (match a8_6 ? p with [ true ⇒ x2 | false ⇒ x0 ])
- (match a8_5 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
- (or_ex (match a8_4 ? p with [ true ⇒ x8 | false ⇒ x0 ])
- (or_ex (match a8_3 ? p with [ true ⇒ x4 | false ⇒ x0 ])
- (or_ex (match a8_2 ? p with [ true ⇒ x2 | false ⇒ x0 ])
- (match a8_1 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
+ (or_ex (match a8_1 ? p with [ true ⇒ x8 | false ⇒ x0 ])
+ (or_ex (match a8_2 ? p with [ true ⇒ x4 | false ⇒ x0 ])
+ (or_ex (match a8_3 ? p with [ true ⇒ x2 | false ⇒ x0 ])
+ (match a8_4 ? p with [ true ⇒ x1 | false ⇒ x0 ]))))
+ (or_ex (match a8_5 ? p with [ true ⇒ x8 | false ⇒ x0 ])
+ (or_ex (match a8_6 ? p with [ true ⇒ x4 | false ⇒ x0 ])
+ (or_ex (match a8_7 ? p with [ true ⇒ x2 | false ⇒ x0 ])
+ (match a8_8 ? p with [ true ⇒ x1 | false ⇒ x0 ])))).
(* scrittura byte *)
+ndefinition bits_of_exadecim ≝
+λe:exadecim.match e with
+ [ x0 ⇒ quadruple … false false false false
+ | x1 ⇒ quadruple … false false false true
+ | x2 ⇒ quadruple … false false true false
+ | x3 ⇒ quadruple … false false true true
+ | x4 ⇒ quadruple … false true false false
+ | x5 ⇒ quadruple … false true false true
+ | x6 ⇒ quadruple … false true true false
+ | x7 ⇒ quadruple … false true true true
+ | x8 ⇒ quadruple … true false false false
+ | x9 ⇒ quadruple … true false false true
+ | xA ⇒ quadruple … true false true false
+ | xB ⇒ quadruple … true false true true
+ | xC ⇒ quadruple … true true false false
+ | xD ⇒ quadruple … true true false true
+ | xE ⇒ quadruple … true true true false
+ | xF ⇒ quadruple … true true true true
+ ].
ndefinition bits_of_byte8 ≝
-λp:byte8.
- match b8h p with
- [ x0 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false false false false false false false
- | x1 ⇒ mk_Array8T bool false false false false false false false true
- | x2 ⇒ mk_Array8T bool false false false false false false true false
- | x3 ⇒ mk_Array8T bool false false false false false false true true
- | x4 ⇒ mk_Array8T bool false false false false false true false false
- | x5 ⇒ mk_Array8T bool false false false false false true false true
- | x6 ⇒ mk_Array8T bool false false false false false true true false
- | x7 ⇒ mk_Array8T bool false false false false false true true true
- | x8 ⇒ mk_Array8T bool false false false false true false false false
- | x9 ⇒ mk_Array8T bool false false false false true false false true
- | xA ⇒ mk_Array8T bool false false false false true false true false
- | xB ⇒ mk_Array8T bool false false false false true false true true
- | xC ⇒ mk_Array8T bool false false false false true true false false
- | xD ⇒ mk_Array8T bool false false false false true true false true
- | xE ⇒ mk_Array8T bool false false false false true true true false
- | xF ⇒ mk_Array8T bool false false false false true true true true ]
- | x1 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false false true false false false false
- | x1 ⇒ mk_Array8T bool false false false true false false false true
- | x2 ⇒ mk_Array8T bool false false false true false false true false
- | x3 ⇒ mk_Array8T bool false false false true false false true true
- | x4 ⇒ mk_Array8T bool false false false true false true false false
- | x5 ⇒ mk_Array8T bool false false false true false true false true
- | x6 ⇒ mk_Array8T bool false false false true false true true false
- | x7 ⇒ mk_Array8T bool false false false true false true true true
- | x8 ⇒ mk_Array8T bool false false false true true false false false
- | x9 ⇒ mk_Array8T bool false false false true true false false true
- | xA ⇒ mk_Array8T bool false false false true true false true false
- | xB ⇒ mk_Array8T bool false false false true true false true true
- | xC ⇒ mk_Array8T bool false false false true true true false false
- | xD ⇒ mk_Array8T bool false false false true true true false true
- | xE ⇒ mk_Array8T bool false false false true true true true false
- | xF ⇒ mk_Array8T bool false false false true true true true true ]
- | x2 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false true false false false false false
- | x1 ⇒ mk_Array8T bool false false true false false false false true
- | x2 ⇒ mk_Array8T bool false false true false false false true false
- | x3 ⇒ mk_Array8T bool false false true false false false true true
- | x4 ⇒ mk_Array8T bool false false true false false true false false
- | x5 ⇒ mk_Array8T bool false false true false false true false true
- | x6 ⇒ mk_Array8T bool false false true false false true true false
- | x7 ⇒ mk_Array8T bool false false true false false true true true
- | x8 ⇒ mk_Array8T bool false false true false true false false false
- | x9 ⇒ mk_Array8T bool false false true false true false false true
- | xA ⇒ mk_Array8T bool false false true false true false true false
- | xB ⇒ mk_Array8T bool false false true false true false true true
- | xC ⇒ mk_Array8T bool false false true false true true false false
- | xD ⇒ mk_Array8T bool false false true false true true false true
- | xE ⇒ mk_Array8T bool false false true false true true true false
- | xF ⇒ mk_Array8T bool false false true false true true true true ]
- | x3 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false false true true false false false false
- | x1 ⇒ mk_Array8T bool false false true true false false false true
- | x2 ⇒ mk_Array8T bool false false true true false false true false
- | x3 ⇒ mk_Array8T bool false false true true false false true true
- | x4 ⇒ mk_Array8T bool false false true true false true false false
- | x5 ⇒ mk_Array8T bool false false true true false true false true
- | x6 ⇒ mk_Array8T bool false false true true false true true false
- | x7 ⇒ mk_Array8T bool false false true true false true true true
- | x8 ⇒ mk_Array8T bool false false true true true false false false
- | x9 ⇒ mk_Array8T bool false false true true true false false true
- | xA ⇒ mk_Array8T bool false false true true true false true false
- | xB ⇒ mk_Array8T bool false false true true true false true true
- | xC ⇒ mk_Array8T bool false false true true true true false false
- | xD ⇒ mk_Array8T bool false false true true true true false true
- | xE ⇒ mk_Array8T bool false false true true true true true false
- | xF ⇒ mk_Array8T bool false false true true true true true true ]
- | x4 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true false false false false false false
- | x1 ⇒ mk_Array8T bool false true false false false false false true
- | x2 ⇒ mk_Array8T bool false true false false false false true false
- | x3 ⇒ mk_Array8T bool false true false false false false true true
- | x4 ⇒ mk_Array8T bool false true false false false true false false
- | x5 ⇒ mk_Array8T bool false true false false false true false true
- | x6 ⇒ mk_Array8T bool false true false false false true true false
- | x7 ⇒ mk_Array8T bool false true false false false true true true
- | x8 ⇒ mk_Array8T bool false true false false true false false false
- | x9 ⇒ mk_Array8T bool false true false false true false false true
- | xA ⇒ mk_Array8T bool false true false false true false true false
- | xB ⇒ mk_Array8T bool false true false false true false true true
- | xC ⇒ mk_Array8T bool false true false false true true false false
- | xD ⇒ mk_Array8T bool false true false false true true false true
- | xE ⇒ mk_Array8T bool false true false false true true true false
- | xF ⇒ mk_Array8T bool false true false false true true true true ]
- | x5 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true false true false false false false
- | x1 ⇒ mk_Array8T bool false true false true false false false true
- | x2 ⇒ mk_Array8T bool false true false true false false true false
- | x3 ⇒ mk_Array8T bool false true false true false false true true
- | x4 ⇒ mk_Array8T bool false true false true false true false false
- | x5 ⇒ mk_Array8T bool false true false true false true false true
- | x6 ⇒ mk_Array8T bool false true false true false true true false
- | x7 ⇒ mk_Array8T bool false true false true false true true true
- | x8 ⇒ mk_Array8T bool false true false true true false false false
- | x9 ⇒ mk_Array8T bool false true false true true false false true
- | xA ⇒ mk_Array8T bool false true false true true false true false
- | xB ⇒ mk_Array8T bool false true false true true false true true
- | xC ⇒ mk_Array8T bool false true false true true true false false
- | xD ⇒ mk_Array8T bool false true false true true true false true
- | xE ⇒ mk_Array8T bool false true false true true true true false
- | xF ⇒ mk_Array8T bool false true false true true true true true ]
- | x6 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true true false false false false false
- | x1 ⇒ mk_Array8T bool false true true false false false false true
- | x2 ⇒ mk_Array8T bool false true true false false false true false
- | x3 ⇒ mk_Array8T bool false true true false false false true true
- | x4 ⇒ mk_Array8T bool false true true false false true false false
- | x5 ⇒ mk_Array8T bool false true true false false true false true
- | x6 ⇒ mk_Array8T bool false true true false false true true false
- | x7 ⇒ mk_Array8T bool false true true false false true true true
- | x8 ⇒ mk_Array8T bool false true true false true false false false
- | x9 ⇒ mk_Array8T bool false true true false true false false true
- | xA ⇒ mk_Array8T bool false true true false true false true false
- | xB ⇒ mk_Array8T bool false true true false true false true true
- | xC ⇒ mk_Array8T bool false true true false true true false false
- | xD ⇒ mk_Array8T bool false true true false true true false true
- | xE ⇒ mk_Array8T bool false true true false true true true false
- | xF ⇒ mk_Array8T bool false true true false true true true true ]
- | x7 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool false true true true false false false false
- | x1 ⇒ mk_Array8T bool false true true true false false false true
- | x2 ⇒ mk_Array8T bool false true true true false false true false
- | x3 ⇒ mk_Array8T bool false true true true false false true true
- | x4 ⇒ mk_Array8T bool false true true true false true false false
- | x5 ⇒ mk_Array8T bool false true true true false true false true
- | x6 ⇒ mk_Array8T bool false true true true false true true false
- | x7 ⇒ mk_Array8T bool false true true true false true true true
- | x8 ⇒ mk_Array8T bool false true true true true false false false
- | x9 ⇒ mk_Array8T bool false true true true true false false true
- | xA ⇒ mk_Array8T bool false true true true true false true false
- | xB ⇒ mk_Array8T bool false true true true true false true true
- | xC ⇒ mk_Array8T bool false true true true true true false false
- | xD ⇒ mk_Array8T bool false true true true true true false true
- | xE ⇒ mk_Array8T bool false true true true true true true false
- | xF ⇒ mk_Array8T bool false true true true true true true true ]
- | x8 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false false false false false false false
- | x1 ⇒ mk_Array8T bool true false false false false false false true
- | x2 ⇒ mk_Array8T bool true false false false false false true false
- | x3 ⇒ mk_Array8T bool true false false false false false true true
- | x4 ⇒ mk_Array8T bool true false false false false true false false
- | x5 ⇒ mk_Array8T bool true false false false false true false true
- | x6 ⇒ mk_Array8T bool true false false false false true true false
- | x7 ⇒ mk_Array8T bool true false false false false true true true
- | x8 ⇒ mk_Array8T bool true false false false true false false false
- | x9 ⇒ mk_Array8T bool true false false false true false false true
- | xA ⇒ mk_Array8T bool true false false false true false true false
- | xB ⇒ mk_Array8T bool true false false false true false true true
- | xC ⇒ mk_Array8T bool true false false false true true false false
- | xD ⇒ mk_Array8T bool true false false false true true false true
- | xE ⇒ mk_Array8T bool true false false false true true true false
- | xF ⇒ mk_Array8T bool true false false false true true true true ]
- | x9 ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false false true false false false false
- | x1 ⇒ mk_Array8T bool true false false true false false false true
- | x2 ⇒ mk_Array8T bool true false false true false false true false
- | x3 ⇒ mk_Array8T bool true false false true false false true true
- | x4 ⇒ mk_Array8T bool true false false true false true false false
- | x5 ⇒ mk_Array8T bool true false false true false true false true
- | x6 ⇒ mk_Array8T bool true false false true false true true false
- | x7 ⇒ mk_Array8T bool true false false true false true true true
- | x8 ⇒ mk_Array8T bool true false false true true false false false
- | x9 ⇒ mk_Array8T bool true false false true true false false true
- | xA ⇒ mk_Array8T bool true false false true true false true false
- | xB ⇒ mk_Array8T bool true false false true true false true true
- | xC ⇒ mk_Array8T bool true false false true true true false false
- | xD ⇒ mk_Array8T bool true false false true true true false true
- | xE ⇒ mk_Array8T bool true false false true true true true false
- | xF ⇒ mk_Array8T bool true false false true true true true true ]
- | xA ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false true false false false false false
- | x1 ⇒ mk_Array8T bool true false true false false false false true
- | x2 ⇒ mk_Array8T bool true false true false false false true false
- | x3 ⇒ mk_Array8T bool true false true false false false true true
- | x4 ⇒ mk_Array8T bool true false true false false true false false
- | x5 ⇒ mk_Array8T bool true false true false false true false true
- | x6 ⇒ mk_Array8T bool true false true false false true true false
- | x7 ⇒ mk_Array8T bool true false true false false true true true
- | x8 ⇒ mk_Array8T bool true false true false true false false false
- | x9 ⇒ mk_Array8T bool true false true false true false false true
- | xA ⇒ mk_Array8T bool true false true false true false true false
- | xB ⇒ mk_Array8T bool true false true false true false true true
- | xC ⇒ mk_Array8T bool true false true false true true false false
- | xD ⇒ mk_Array8T bool true false true false true true false true
- | xE ⇒ mk_Array8T bool true false true false true true true false
- | xF ⇒ mk_Array8T bool true false true false true true true true ]
- | xB ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true false true true false false false false
- | x1 ⇒ mk_Array8T bool true false true true false false false true
- | x2 ⇒ mk_Array8T bool true false true true false false true false
- | x3 ⇒ mk_Array8T bool true false true true false false true true
- | x4 ⇒ mk_Array8T bool true false true true false true false false
- | x5 ⇒ mk_Array8T bool true false true true false true false true
- | x6 ⇒ mk_Array8T bool true false true true false true true false
- | x7 ⇒ mk_Array8T bool true false true true false true true true
- | x8 ⇒ mk_Array8T bool true false true true true false false false
- | x9 ⇒ mk_Array8T bool true false true true true false false true
- | xA ⇒ mk_Array8T bool true false true true true false true false
- | xB ⇒ mk_Array8T bool true false true true true false true true
- | xC ⇒ mk_Array8T bool true false true true true true false false
- | xD ⇒ mk_Array8T bool true false true true true true false true
- | xE ⇒ mk_Array8T bool true false true true true true true false
- | xF ⇒ mk_Array8T bool true false true true true true true true ]
- | xC ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true false false false false false false
- | x1 ⇒ mk_Array8T bool true true false false false false false true
- | x2 ⇒ mk_Array8T bool true true false false false false true false
- | x3 ⇒ mk_Array8T bool true true false false false false true true
- | x4 ⇒ mk_Array8T bool true true false false false true false false
- | x5 ⇒ mk_Array8T bool true true false false false true false true
- | x6 ⇒ mk_Array8T bool true true false false false true true false
- | x7 ⇒ mk_Array8T bool true true false false false true true true
- | x8 ⇒ mk_Array8T bool true true false false true false false false
- | x9 ⇒ mk_Array8T bool true true false false true false false true
- | xA ⇒ mk_Array8T bool true true false false true false true false
- | xB ⇒ mk_Array8T bool true true false false true false true true
- | xC ⇒ mk_Array8T bool true true false false true true false false
- | xD ⇒ mk_Array8T bool true true false false true true false true
- | xE ⇒ mk_Array8T bool true true false false true true true false
- | xF ⇒ mk_Array8T bool true true false false true true true true ]
- | xD ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true false true false false false false
- | x1 ⇒ mk_Array8T bool true true false true false false false true
- | x2 ⇒ mk_Array8T bool true true false true false false true false
- | x3 ⇒ mk_Array8T bool true true false true false false true true
- | x4 ⇒ mk_Array8T bool true true false true false true false false
- | x5 ⇒ mk_Array8T bool true true false true false true false true
- | x6 ⇒ mk_Array8T bool true true false true false true true false
- | x7 ⇒ mk_Array8T bool true true false true false true true true
- | x8 ⇒ mk_Array8T bool true true false true true false false false
- | x9 ⇒ mk_Array8T bool true true false true true false false true
- | xA ⇒ mk_Array8T bool true true false true true false true false
- | xB ⇒ mk_Array8T bool true true false true true false true true
- | xC ⇒ mk_Array8T bool true true false true true true false false
- | xD ⇒ mk_Array8T bool true true false true true true false true
- | xE ⇒ mk_Array8T bool true true false true true true true false
- | xF ⇒ mk_Array8T bool true true false true true true true true ]
- | xE ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true true false false false false false
- | x1 ⇒ mk_Array8T bool true true true false false false false true
- | x2 ⇒ mk_Array8T bool true true true false false false true false
- | x3 ⇒ mk_Array8T bool true true true false false false true true
- | x4 ⇒ mk_Array8T bool true true true false false true false false
- | x5 ⇒ mk_Array8T bool true true true false false true false true
- | x6 ⇒ mk_Array8T bool true true true false false true true false
- | x7 ⇒ mk_Array8T bool true true true false false true true true
- | x8 ⇒ mk_Array8T bool true true true false true false false false
- | x9 ⇒ mk_Array8T bool true true true false true false false true
- | xA ⇒ mk_Array8T bool true true true false true false true false
- | xB ⇒ mk_Array8T bool true true true false true false true true
- | xC ⇒ mk_Array8T bool true true true false true true false false
- | xD ⇒ mk_Array8T bool true true true false true true false true
- | xE ⇒ mk_Array8T bool true true true false true true true false
- | xF ⇒ mk_Array8T bool true true true false true true true true ]
- | xF ⇒ match b8l p with
- [ x0 ⇒ mk_Array8T bool true true true true false false false false
- | x1 ⇒ mk_Array8T bool true true true true false false false true
- | x2 ⇒ mk_Array8T bool true true true true false false true false
- | x3 ⇒ mk_Array8T bool true true true true false false true true
- | x4 ⇒ mk_Array8T bool true true true true false true false false
- | x5 ⇒ mk_Array8T bool true true true true false true false true
- | x6 ⇒ mk_Array8T bool true true true true false true true false
- | x7 ⇒ mk_Array8T bool true true true true false true true true
- | x8 ⇒ mk_Array8T bool true true true true true false false false
- | x9 ⇒ mk_Array8T bool true true true true true false false true
- | xA ⇒ mk_Array8T bool true true true true true false true false
- | xB ⇒ mk_Array8T bool true true true true true false true true
- | xC ⇒ mk_Array8T bool true true true true true true false false
- | xD ⇒ mk_Array8T bool true true true true true true false true
- | xE ⇒ mk_Array8T bool true true true true true true true false
- | xF ⇒ mk_Array8T bool true true true true true true true true ]
- ].
+λb:byte8.
+ mk_Array8T ? (fst4T … (bits_of_exadecim (b8h b)))
+ (snd4T … (bits_of_exadecim (b8h b)))
+ (thd4T … (bits_of_exadecim (b8h b)))
+ (fth4T … (bits_of_exadecim (b8h b)))
+ (fst4T … (bits_of_exadecim (b8l b)))
+ (snd4T … (bits_of_exadecim (b8l b)))
+ (thd4T … (bits_of_exadecim (b8l b)))
+ (fth4T … (bits_of_exadecim (b8l b))).
interpretation "mk_alu_HC05" 'mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl =
(mk_alu_HC05 acclow indxlow sp spm spf pc pcm hfl ifl nfl zfl cfl irqfl).
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* setter specifico HC05 di A *)
+ndefinition set_acc_8_low_reg_HC05 ≝
+λalu.λacclow':byte8.
+ mk_alu_HC05
+ acclow'
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di X *)
+ndefinition set_indX_8_low_reg_HC05 ≝
+λalu.λindxlow':byte8.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ indxlow'
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
+ndefinition set_sp_reg_HC05 ≝
+λalu.λsp':word16.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di PC, effettua PC∧mask *)
+ndefinition set_pc_reg_HC05 ≝
+λalu.λpc':word16.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (and_w16 pc' (pc_mask_HC05 alu))
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di H *)
+ndefinition set_h_flag_HC05 ≝
+λalu.λhfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ hfl'
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di I *)
+ndefinition set_i_flag_HC05 ≝
+λalu.λifl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ ifl'
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di N *)
+ndefinition set_n_flag_HC05 ≝
+λalu.λnfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ nfl'
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di Z *)
+ndefinition set_z_flag_HC05 ≝
+λalu.λzfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ zfl'
+ (c_flag_HC05 alu)
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di C *)
+ndefinition set_c_flag_HC05 ≝
+λalu.λcfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ cfl'
+ (irq_flag_HC05 alu).
+
+(* setter specifico HC05 di IRQ *)
+ndefinition set_irq_flag_HC05 ≝
+λalu.λirqfl':bool.
+ mk_alu_HC05
+ (acc_low_reg_HC05 alu)
+ (indX_low_reg_HC05 alu)
+ (sp_reg_HC05 alu)
+ (sp_mask_HC05 alu)
+ (sp_fix_HC05 alu)
+ (pc_reg_HC05 alu)
+ (pc_mask_HC05 alu)
+ (h_flag_HC05 alu)
+ (i_flag_HC05 alu)
+ (n_flag_HC05 alu)
+ (z_flag_HC05 alu)
+ (c_flag_HC05 alu)
+ irqfl'.
+
(* ***************** *)
(* CONFRONTO FRA ALU *)
(* ***************** *)
interpretation "mk_alu_HC08" 'mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl =
(mk_alu_HC08 acclow indxlow indxhigh sp pc vfl hfl ifl nfl zfl cfl irqfl).
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* setter specifico HC08/HCS08 di A *)
+ndefinition set_acc_8_low_reg_HC08 ≝
+λalu.λacclow':byte8.
+ mk_alu_HC08
+ acclow'
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di X *)
+ndefinition set_indX_8_low_reg_HC08 ≝
+λalu.λindxlow':byte8.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ indxlow'
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di H *)
+ndefinition set_indX_8_high_reg_HC08 ≝
+λalu.λindxhigh':byte8.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ indxhigh'
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di H:X *)
+ndefinition set_indX_16_reg_HC08 ≝
+λalu.λindx16:word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (w16l indx16)
+ (w16h indx16)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di SP *)
+ndefinition set_sp_reg_HC08 ≝
+λalu.λsp':word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ sp'
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di PC *)
+ndefinition set_pc_reg_HC08 ≝
+λalu.λpc':word16.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ pc'
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di V *)
+ndefinition set_v_flag_HC08 ≝
+λalu.λvfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ vfl'
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di H *)
+ndefinition set_h_flag_HC08 ≝
+λalu.λhfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ hfl'
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di I *)
+ndefinition set_i_flag_HC08 ≝
+λalu.λifl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ ifl'
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di N *)
+ndefinition set_n_flag_HC08 ≝
+λalu.λnfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ nfl'
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di Z *)
+ndefinition set_z_flag_HC08 ≝
+λalu.λzfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ zfl'
+ (c_flag_HC08 alu)
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di C *)
+ndefinition set_c_flag_HC08 ≝
+λalu.λcfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ cfl'
+ (irq_flag_HC08 alu).
+
+(* setter specifico HC08/HCS08 di IRQ *)
+ndefinition set_irq_flag_HC08 ≝
+λalu.λirqfl':bool.
+ mk_alu_HC08
+ (acc_low_reg_HC08 alu)
+ (indX_low_reg_HC08 alu)
+ (indX_high_reg_HC08 alu)
+ (sp_reg_HC08 alu)
+ (pc_reg_HC08 alu)
+ (v_flag_HC08 alu)
+ (h_flag_HC08 alu)
+ (i_flag_HC08 alu)
+ (n_flag_HC08 alu)
+ (z_flag_HC08 alu)
+ (c_flag_HC08 alu)
+ irqfl'.
+
(* ***************** *)
(* CONFRONTO FRA ALU *)
(* ***************** *)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/memory/memory_struct.ma".
+include "num/word16.ma".
+include "num/word24.ma".
+
+(* ******************************** *)
+(* IP2022 REGISTER SPECIAL HARDWARE *)
+(* ******************************** *)
+
+(* (Top Of Stack) : CALLH/CALL ↑ CALLH/CALL ↓ *)
+(* Pos2-15 : ... ↑ ... ↓ *)
+(* Pos16 : 0xFFFF ↑ ... ↓ *)
+ndefinition aux_callstack_type ≝ Array16T word16.
+
+(* Top Of Stack : 0xFFFF on reset *)
+ndefinition new_callstack ≝
+ mk_Array16T ? (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
+ (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
+ (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉)
+ (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉) (〈〈xF,xF〉:〈xF,xF〉〉).
+
+ndefinition pop_callstack ≝
+λcs:aux_callstack_type.
+ pair ?? (a16_1 ? cs)
+ (mk_Array16T ? (a16_2 ? cs) (a16_3 ? cs) (a16_4 ? cs) (a16_5 ? cs)
+ (a16_6 ? cs) (a16_7 ? cs) (a16_8 ? cs) (a16_9 ? cs)
+ (a16_10 ? cs) (a16_11 ? cs) (a16_12 ? cs) (a16_13 ? cs)
+ (a16_14 ? cs) (a16_15 ? cs) (a16_16 ? cs) 〈〈xF,xF〉:〈xF,xF〉〉).
+
+ndefinition push_callstack ≝
+λcs:aux_callstack_type.λtop.
+ mk_Array16T ? top (a16_1 ? cs) (a16_2 ? cs) (a16_3 ? cs)
+ (a16_4 ? cs) (a16_5 ? cs) (a16_6 ? cs) (a16_7 ? cs)
+ (a16_8 ? cs) (a16_9 ? cs) (a16_10 ? cs) (a16_11 ? cs)
+ (a16_12 ? cs) (a16_13 ? cs) (a16_14 ? cs) (a16_15 ? cs).
+
+(* array ad accesso diretto di 8 registri ADDR a 24bit *)
+(* selezione con registro ADDRSEL, solo i primi 3bit validi *)
+ndefinition aux_addrarray_type ≝ Array8T word24.
+
+(* tutti a 0x000000 on reset *)
+ndefinition new_addrarray ≝
+ mk_Array8T ? (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
+ (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
+ (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
+ (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
+
+ndefinition get_low3bits ≝
+λaddrsel:byte8.
+ match b8l addrsel with
+ [ x0 ⇒ o0 | x1 ⇒ o1 | x2 ⇒ o2 | x3 ⇒ o3 | x4 ⇒ o4 | x5 ⇒ o5 | x6 ⇒ o6 | x7 ⇒ o7
+ | x8 ⇒ o0 | x9 ⇒ o1 | xA ⇒ o2 | xB ⇒ o3 | xC ⇒ o4 | xD ⇒ o5 | xE ⇒ o6 | xF ⇒ o7 ].
+
+ndefinition get_addrarray ≝
+λaddrsel:byte8.λaa:aux_addrarray_type.
+ getn_array8T (get_low3bits addrsel) ? aa.
+
+ndefinition set_addrarray ≝
+λaddrsel:byte8.λaa:aux_addrarray_type.λv.
+ setn_array8T (get_low3bits addrsel) ? aa v.
+
+(* *********************************** *)
+(* STATUS INTERNO DEL PROCESSORE (ALU) *)
+(* *********************************** *)
+
+(* ALU dell'IP2022 *)
+nrecord alu_IP2022: Type ≝
+ {
+ (* W: accumulatore *)
+ acc_low_reg_IP2022 : byte8;
+ (* MULH: parte alta moltiplicazione *)
+ mulh_reg_IP2022 : byte8;
+
+ (* ADDRSEL: selettore di indirizzo *)
+ addrsel_reg_IP2022 : byte8;
+ (* ADDR [ADDRX|ADDRH|ADDRL] : array indirizzi indicizzati da ADDRSEL *)
+ addr_array_IP2022 : aux_addrarray_type;
+
+ (* CALL [CALLH|CALLL] : stack indirizzi di ritorno *)
+ call_stack_IP2022 : aux_callstack_type;
+
+ (* IP [IPH|IPL] : indirect pointer *)
+ ip_reg_IP2022 : word16;
+ (* DP [DPH|DPL] : data pointer *)
+ dp_reg_IP2022 : word16;
+ (* DATA [DATAH|DATAL] : data value *)
+ data_reg_IP2022 : word16;
+ (* SP [SPH|SPL] : stack pointer *)
+ sp_reg_IP2022 : word16;
+ (* PC [PCH|PCL] : program counter *)
+ pc_reg_IP2022 : word16;
+
+ (* SPEED[xxxxSSSS] : divisore del clock *)
+ speed_reg_IP2022 : exadecim;
+ (* PAGE [PPPxxxxx] : selettore pagina *)
+ page_reg_IP2022 : oct;
+
+ (* H: flag semi-carry (somma nibble basso) *)
+ h_flag_IP2022 : bool;
+ (* Z: flag zero *)
+ z_flag_IP2022 : bool;
+ (* C: flag carry *)
+ c_flag_IP2022 : bool;
+
+ (* skip mode : effettua fetch-decode, no execute *)
+ skip_mode_IP2022 : bool
+ }.
+
+notation "{hvbox('W_Reg' ≝ w ; break 'MulH_Reg' ≝ mulh ; break 'Addrsel_Reg' ≝ addrsel ; break 'Addr_Array' ≝ addr ; break 'Call_Stack' ≝ call ; break 'Ip_Reg' ≝ ip ; break 'Dp_Reg' ≝ dp ; break 'Data_Reg' ≝ data ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'Speed_Reg' ≝ speed ; break 'Page_Reg' ≝ page ; break 'H_Flag' ≝ hfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'Skip_Mode' ≝ skipmode)}"
+ non associative with precedence 80 for
+ @{ 'mk_alu_IP2022 $w $mulh $addrsel $addr $call $ip $dp $data $sp $pc $speed $page $hfl $zfl $cfl $skipmode }.
+interpretation "mk_alu_IP2022" 'mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode =
+ (mk_alu_IP2022 w mulh addrsel addr call ip dp data sp pc speed page hfl zfl cfl skipmode).
+
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* setter specifico IP2022 di A *)
+ndefinition set_acc_8_low_reg_IP2022 ≝
+λalu.λacclow':byte8.
+ mk_alu_IP2022
+ acclow'
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di MULH *)
+ndefinition set_mulh_reg_IP2022 ≝
+λalu.λmulh':byte8.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ mulh'
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di ADDRSEL *)
+ndefinition set_addrsel_reg_IP2022 ≝
+λalu.λaddrsel':byte8.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ addrsel'
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di ADDR *)
+ndefinition set_addr_reg_IP2022 ≝
+λalu.λaddr':word24.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (set_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu) addr')
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di CALL *)
+ndefinition set_call_reg_IP2022 ≝
+λalu.λcall':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (setn_array16T x0 ? (call_stack_IP2022 alu) call')
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+ndefinition push_call_reg_IP2022 ≝
+λalu.λcall':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (push_callstack (call_stack_IP2022 alu) call')
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di IP *)
+ndefinition set_ip_reg_IP2022 ≝
+λalu.λip':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ ip'
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di DP *)
+ndefinition set_dp_reg_IP2022 ≝
+λalu.λdp':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ dp'
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di DATA *)
+ndefinition set_data_reg_IP2022 ≝
+λalu.λdata':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ data'
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di SP *)
+ndefinition set_sp_reg_IP2022 ≝
+λalu.λsp':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ sp'
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di PC *)
+ndefinition set_pc_reg_IP2022 ≝
+λalu.λpc':word16.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ pc'
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di SPEED *)
+ndefinition set_speed_reg_IP2022 ≝
+λalu.λspeed':exadecim.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ speed'
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di PAGE *)
+ndefinition set_page_reg_IP2022 ≝
+λalu.λpage':oct.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ page'
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di H *)
+ndefinition set_h_flag_IP2022 ≝
+λalu.λhfl':bool.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ hfl'
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di Z *)
+ndefinition set_z_flag_IP2022 ≝
+λalu.λzfl':bool.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ zfl'
+ (c_flag_IP2022 alu)
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di C *)
+ndefinition set_c_flag_IP2022 ≝
+λalu.λcfl':bool.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ cfl'
+ (skip_mode_IP2022 alu).
+
+(* setter specifico IP2022 di SKIP *)
+ndefinition set_skip_mode_IP2022 ≝
+λalu.λskipmode':bool.
+ mk_alu_IP2022
+ (acc_low_reg_IP2022 alu)
+ (mulh_reg_IP2022 alu)
+ (addrsel_reg_IP2022 alu)
+ (addr_array_IP2022 alu)
+ (call_stack_IP2022 alu)
+ (ip_reg_IP2022 alu)
+ (dp_reg_IP2022 alu)
+ (data_reg_IP2022 alu)
+ (sp_reg_IP2022 alu)
+ (pc_reg_IP2022 alu)
+ (speed_reg_IP2022 alu)
+ (page_reg_IP2022 alu)
+ (h_flag_IP2022 alu)
+ (z_flag_IP2022 alu)
+ (c_flag_IP2022 alu)
+ skipmode'.
+
+(* ***************** *)
+(* CONFRONTO FRA ALU *)
+(* ***************** *)
+
+(* confronto registro per registro dell'IP2022 *)
+ndefinition eq_IP2022_alu ≝
+λalu1,alu2:alu_IP2022.
+ (eq_b8 (acc_low_reg_IP2022 alu1) (acc_low_reg_IP2022 alu2)) ⊗
+ (eq_b8 (mulh_reg_IP2022 alu1) (mulh_reg_IP2022 alu2)) ⊗
+ (eq_b8 (addrsel_reg_IP2022 alu1) (addrsel_reg_IP2022 alu2)) ⊗
+ (eq_ar8 ? eq_w24 (addr_array_IP2022 alu1) (addr_array_IP2022 alu2)) ⊗
+ (eq_ar16 ? eq_w16 (call_stack_IP2022 alu1) (call_stack_IP2022 alu2)) ⊗
+ (eq_w16 (ip_reg_IP2022 alu1) (ip_reg_IP2022 alu2)) ⊗
+ (eq_w16 (dp_reg_IP2022 alu1) (dp_reg_IP2022 alu2)) ⊗
+ (eq_w16 (data_reg_IP2022 alu1) (data_reg_IP2022 alu2)) ⊗
+ (eq_w16 (sp_reg_IP2022 alu1) (sp_reg_IP2022 alu2)) ⊗
+ (eq_w16 (pc_reg_IP2022 alu1) (pc_reg_IP2022 alu2)) ⊗
+ (eq_ex (speed_reg_IP2022 alu1) (speed_reg_IP2022 alu2)) ⊗
+ (eq_oct (page_reg_IP2022 alu1) (page_reg_IP2022 alu2)) ⊗
+ (eq_bool (h_flag_IP2022 alu1) (h_flag_IP2022 alu2)) ⊗
+ (eq_bool (z_flag_IP2022 alu1) (z_flag_IP2022 alu2)) ⊗
+ (eq_bool (c_flag_IP2022 alu1) (c_flag_IP2022 alu2)) ⊗
+ (eq_bool (skip_mode_IP2022 alu1) (skip_mode_IP2022 alu2)).
interpretation "mk_alu_RS08" 'mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl =
(mk_alu_RS08 acclow pc pcm spc xm psm zfl cfl).
+(* ****** *)
+(* SETTER *)
+(* ****** *)
+
+(* setter specifico RS08 di A *)
+ndefinition set_acc_8_low_reg_RS08 ≝
+λalu.λacclow':byte8.
+ mk_alu_RS08
+ acclow'
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
+
+(* setter specifico RS08 di PC, effettua PC∧mask *)
+ndefinition set_pc_reg_RS08 ≝
+λalu.λpc':word16.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (and_w16 pc' (pc_mask_RS08 alu))
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
+
+(* setter specifico RS08 di SPC, effettua SPC∧mask *)
+ndefinition set_spc_reg_RS08 ≝
+λalu.λspc':word16.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (and_w16 spc' (pc_mask_RS08 alu))
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
+
+(* setter specifico RS08 di memory mapped X *)
+ndefinition set_x_map_RS08 ≝
+λalu.λxm':byte8.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ xm'
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
+
+(* setter specifico RS08 di memory mapped PS *)
+ndefinition set_ps_map_RS08 ≝
+λalu.λpsm':byte8.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ psm'
+ (z_flag_RS08 alu)
+ (c_flag_RS08 alu).
+
+(* setter sprcifico RS08 di Z *)
+ndefinition set_z_flag_RS08 ≝
+λalu.λzfl':bool.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ zfl'
+ (c_flag_RS08 alu).
+
+(* setter specifico RS08 di C *)
+ndefinition set_c_flag_RS08 ≝
+λalu.λcfl':bool.
+ mk_alu_RS08
+ (acc_low_reg_RS08 alu)
+ (pc_reg_RS08 alu)
+ (pc_mask_RS08 alu)
+ (spc_reg_RS08 alu)
+ (x_map_RS08 alu)
+ (ps_map_RS08 alu)
+ (z_flag_RS08 alu)
+ cfl'.
+
(* ***************** *)
(* CONFRONTO FRA ALU *)
(* ***************** *)
include "emulator/status/HC05_status.ma".
include "emulator/status/HC08_status.ma".
include "emulator/status/RS08_status.ma".
+include "emulator/status/IP2022_status.ma".
include "emulator/opcodes/opcode.ma".
(* *********************************** *)
nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
{
alu : match mcu with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ];
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ];
(* descritore della memoria *)
mem_desc : aux_mem_type t;
match m
return λm.
match m with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ] →
match m with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] →
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ] →
bool
with
[ HC05 ⇒ eq_HC05_alu
| HC08 ⇒ eq_HC08_alu
| HCS08 ⇒ eq_HC08_alu
| RS08 ⇒ eq_RS08_alu
+ | IP2022 ⇒ eq_IP2022_alu
].
(* confronto di una regione di memoria [addr1 ; ... ; addrn] *)
(addrl:list word32) on addrl ≝
match addrl return λ_.bool with
[ nil ⇒ true
- | cons hd tl ⇒ (eq_option byte8 (mem_read t mem1 chk1 hd)
- (mem_read t mem2 chk2 hd) eq_b8) ⊗
+ | cons hd tl ⇒ (eq_option byte8 eq_b8 (mem_read t mem1 chk1 hd)
+ (mem_read t mem2 chk2 hd)) ⊗
(forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
].
(* *)
(* ********************************************************************** *)
-include "emulator/status/status.ma".
+include "emulator/status/status_setter.ma".
(* **************** *)
(* GETTER SPECIFICI *)
(* funzione ausiliaria per il tipaggio dei getter *)
ndefinition aux_get_type ≝ λx:Type.λm:mcu_type.match m with
- [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ] → x.
+ [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ] → x.
(* REGISTRI *)
[ HC05 ⇒ acc_low_reg_HC05
| HC08 ⇒ acc_low_reg_HC08
| HCS08 ⇒ acc_low_reg_HC08
- | RS08 ⇒ acc_low_reg_RS08 ]
+ | RS08 ⇒ acc_low_reg_RS08
+ | IP2022 ⇒ acc_low_reg_IP2022 ]
(alu m t s).
(* getter di X, non esiste sempre *)
[ HC05 ⇒ λalu.Some ? (indX_low_reg_HC05 alu)
| HC08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
| HCS08 ⇒ λalu.Some ? (indX_low_reg_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di H, non esiste sempre *)
[ HC05 ⇒ λalu.None ?
| HC08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
| HCS08 ⇒ λalu.Some ? (indX_high_reg_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di H:X, non esiste sempre *)
[ HC05 ⇒ λalu.None ?
| HC08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
| HCS08 ⇒ λalu.Some ? (mk_word16 (indX_high_reg_HC08 alu) (indX_low_reg_HC08 alu))
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di SP, non esiste sempre *)
[ HC05 ⇒ λalu.Some ? (sp_reg_HC05 alu)
| HC08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
| HCS08 ⇒ λalu.Some ? (sp_reg_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (sp_reg_IP2022 alu) ]
(alu m t s).
(* getter di PC, esiste sempre *)
[ HC05 ⇒ pc_reg_HC05
| HC08 ⇒ pc_reg_HC08
| HCS08 ⇒ pc_reg_HC08
- | RS08 ⇒ pc_reg_RS08 ]
+ | RS08 ⇒ pc_reg_RS08
+ | IP2022 ⇒ pc_reg_IP2022 ]
(alu m t s).
(* getter di SPC, non esiste sempre *)
[ HC05 ⇒ λalu.None ?
| HC08 ⇒ λalu.None ?
| HCS08 ⇒ λalu.None ?
- | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu) ]
+ | RS08 ⇒ λalu.Some ? (spc_reg_RS08 alu)
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
-(* REGISTRI MEMORY MAPPED *)
+(* getter di MULH, non esiste sempre *)
+ndefinition get_mulh_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option byte8) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (mulh_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* getter di ADDRSEL, non esiste sempre *)
+ndefinition get_addrsel_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option byte8) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (addrsel_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* getter di ADDR, non esiste sempre *)
+ndefinition get_addr_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option word24) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (get_addrarray (addrsel_reg_IP2022 alu) (addr_array_IP2022 alu)) ]
+ (alu m t s).
+
+(* getter di CALL, non esiste sempre *)
+ndefinition get_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option word16) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (getn_array16T x0 ? (call_stack_IP2022 alu)) ]
+ (alu m t s).
+
+ndefinition pop_call_reg ≝
+λm:mcu_type.
+ match m
+ return λm.Πt.any_status m t → (option (ProdT word16 (any_status m t))) with
+ [ HC05 ⇒ λt:memory_impl.λs:any_status HC05 t.None ?
+ | HC08 ⇒ λt:memory_impl.λs:any_status HC08 t.None ?
+ | HCS08 ⇒ λt:memory_impl.λs:any_status HCS08 t.None ?
+ | RS08 ⇒ λt:memory_impl.λs:any_status RS08 t.None ?
+ | IP2022 ⇒ λt:memory_impl.λs:any_status IP2022 t.
+ match pop_callstack (call_stack_IP2022 (alu IP2022 t s)) with
+ [ pair val call' ⇒ Some ? (pair … val
+ (set_alu IP2022 t s
+ (mk_alu_IP2022
+ (acc_low_reg_IP2022 (alu IP2022 t s))
+ (mulh_reg_IP2022 (alu IP2022 t s))
+ (addrsel_reg_IP2022 (alu IP2022 t s))
+ (addr_array_IP2022 (alu IP2022 t s))
+ call'
+ (ip_reg_IP2022 (alu IP2022 t s))
+ (dp_reg_IP2022 (alu IP2022 t s))
+ (data_reg_IP2022 (alu IP2022 t s))
+ (sp_reg_IP2022 (alu IP2022 t s))
+ (pc_reg_IP2022 (alu IP2022 t s))
+ (speed_reg_IP2022 (alu IP2022 t s))
+ (page_reg_IP2022 (alu IP2022 t s))
+ (h_flag_IP2022 (alu IP2022 t s))
+ (z_flag_IP2022 (alu IP2022 t s))
+ (c_flag_IP2022 (alu IP2022 t s))
+ (skip_mode_IP2022 (alu IP2022 t s))))) ]].
+
+(* getter di IP, non esiste sempre *)
+ndefinition get_ip_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option word16) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (ip_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* getter di DP, non esiste sempre *)
+ndefinition get_dp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option word16) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (dp_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* getter di DATA, non esiste sempre *)
+ndefinition get_data_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option word16) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (data_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* getter di SPEED, non esiste sempre *)
+ndefinition get_speed_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option exadecim) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (speed_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* getter di PAGE, non esiste sempre *)
+ndefinition get_page_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option oct) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (page_reg_IP2022 alu) ]
+ (alu m t s).
+
+(* REGISTRI SPECIALI *)
(* getter di memory mapped X, non esiste sempre *)
ndefinition get_x_map ≝
[ HC05 ⇒ λalu.None ?
| HC08 ⇒ λalu.None ?
| HCS08 ⇒ λalu.None ?
- | RS08 ⇒ λalu.Some ? (x_map_RS08 alu) ]
+ | RS08 ⇒ λalu.Some ? (x_map_RS08 alu)
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di memory mapped PS, non esiste sempre *)
[ HC05 ⇒ λalu.None ?
| HC08 ⇒ λalu.None ?
| HCS08 ⇒ λalu.None ?
- | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu) ]
+ | RS08 ⇒ λalu.Some ? (ps_map_RS08 alu)
+ | IP2022 ⇒ λalu.None ? ]
+ (alu m t s).
+
+(* getter di skip mode, non esiste sempre *)
+ndefinition get_skip_mode ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.
+ match m
+ return aux_get_type (option bool) with
+ [ HC05 ⇒ λalu.None ?
+ | HC08 ⇒ λalu.None ?
+ | HCS08 ⇒ λalu.None ?
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (skip_mode_IP2022 alu) ]
(alu m t s).
(* FLAG *)
[ HC05 ⇒ λalu.None ?
| HC08 ⇒ λalu.Some ? (v_flag_HC08 alu)
| HCS08 ⇒ λalu.Some ? (v_flag_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di H, non esiste sempre *)
[ HC05 ⇒ λalu.Some ? (h_flag_HC05 alu)
| HC08 ⇒ λalu.Some ? (h_flag_HC08 alu)
| HCS08 ⇒ λalu.Some ? (h_flag_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.Some ? (h_flag_IP2022 alu) ]
(alu m t s).
(* getter di I, non esiste sempre *)
[ HC05 ⇒ λalu.Some ? (i_flag_HC05 alu)
| HC08 ⇒ λalu.Some ? (i_flag_HC08 alu)
| HCS08 ⇒ λalu.Some ? (i_flag_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di N, non esiste sempre *)
[ HC05 ⇒ λalu.Some ? (n_flag_HC05 alu)
| HC08 ⇒ λalu.Some ? (n_flag_HC08 alu)
| HCS08 ⇒ λalu.Some ? (n_flag_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* getter di Z, esiste sempre *)
[ HC05 ⇒ z_flag_HC05
| HC08 ⇒ z_flag_HC08
| HCS08 ⇒ z_flag_HC08
- | RS08 ⇒ z_flag_RS08 ]
+ | RS08 ⇒ z_flag_RS08
+ | IP2022 ⇒ z_flag_IP2022 ]
(alu m t s).
(* getter di C, esiste sempre *)
[ HC05 ⇒ c_flag_HC05
| HC08 ⇒ c_flag_HC08
| HCS08 ⇒ c_flag_HC08
- | RS08 ⇒ c_flag_RS08 ]
+ | RS08 ⇒ c_flag_RS08
+ | IP2022 ⇒ c_flag_IP2022 ]
(alu m t s).
(* getter di IRQ, non esiste sempre *)
[ HC05 ⇒ λalu.Some ? (irq_flag_HC05 alu)
| HC08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
| HCS08 ⇒ λalu.Some ? (irq_flag_HC08 alu)
- | RS08 ⇒ λalu.None ? ]
+ | RS08 ⇒ λalu.None ?
+ | IP2022 ⇒ λalu.None ? ]
(alu m t s).
(* funzione ausiliaria per il tipaggio dei setter forti *)
ndefinition aux_set_type ≝ λx:Type.λm:mcu_type.
- match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ]
→ x →
- match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ].
(* funzione ausiliaria per il tipaggio dei setter deboli *)
ndefinition aux_set_type_opt ≝ λx:Type.λm:mcu_type.option
- (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]
+ (match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ]
→ x →
- match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]).
+ match m with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08
+ | IP2022 ⇒ alu_IP2022 ]).
(* DESCRITTORI ESTERNI ALLA ALU *)
(* REGISTRO A *)
-(* setter specifico HC05 di A *)
-ndefinition set_acc_8_low_reg_HC05 ≝
-λalu.λacclow':byte8.
- mk_alu_HC05
- acclow'
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di A *)
-ndefinition set_acc_8_low_reg_HC08 ≝
-λalu.λacclow':byte8.
- mk_alu_HC08
- acclow'
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
-(* setter specifico RS08 di A *)
-ndefinition set_acc_8_low_reg_RS08 ≝
-λalu.λacclow':byte8.
- mk_alu_RS08
- acclow'
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
-
(* setter forte di A *)
ndefinition set_acc_8_low_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λacclow':byte8.
| HC08 ⇒ set_acc_8_low_reg_HC08
| HCS08 ⇒ set_acc_8_low_reg_HC08
| RS08 ⇒ set_acc_8_low_reg_RS08
+ | IP2022 ⇒ set_acc_8_low_reg_IP2022
] (alu m t s) acclow').
(* REGISTRO X *)
-(* setter specifico HC05 di X *)
-ndefinition set_indX_8_low_reg_HC05 ≝
-λalu.λindxlow':byte8.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- indxlow'
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di X *)
-ndefinition set_indX_8_low_reg_HC08 ≝
-λalu.λindxlow':byte8.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- indxlow'
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di X *)
ndefinition set_indX_8_low_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxlow':byte8.
[ HC05 ⇒ Some ? set_indX_8_low_reg_HC05
| HC08 ⇒ Some ? set_indX_8_low_reg_HC08
| HCS08 ⇒ Some ? set_indX_8_low_reg_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) indxlow'))).
(* setter debole di X *)
(* REGISTRO H *)
-(* setter specifico HC08/HCS08 di H *)
-ndefinition set_indX_8_high_reg_HC08 ≝
-λalu.λindxhigh':byte8.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- indxhigh'
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di H *)
ndefinition set_indX_8_high_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λindxhigh':byte8.
[ HC05 ⇒ None ?
| HC08 ⇒ Some ? set_indX_8_high_reg_HC08
| HCS08 ⇒ Some ? set_indX_8_high_reg_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) indxhigh'))).
(* setter debole di H *)
(* REGISTRO H:X *)
-(* setter specifico HC08/HCS08 di H:X *)
-ndefinition set_indX_16_reg_HC08 ≝
-λalu.λindx16:word16.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (w16l indx16)
- (w16h indx16)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di H:X *)
ndefinition set_indX_16_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λindx16:word16.
[ HC05 ⇒ None ?
| HC08 ⇒ Some ? set_indX_16_reg_HC08
| HCS08 ⇒ Some ? set_indX_16_reg_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) indx16))).
(* setter debole di H:X *)
(* REGISTRO SP *)
-(* setter specifico HC05 di SP, effettua (SP∧mask)∨fix *)
-ndefinition set_sp_reg_HC05 ≝
-λalu.λsp':word16.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (or_w16 (and_w16 sp' (sp_mask_HC05 alu)) (sp_fix_HC05 alu))
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di SP *)
-ndefinition set_sp_reg_HC08 ≝
-λalu.λsp':word16.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- sp'
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di SP *)
ndefinition set_sp_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λsp':word16.
[ HC05 ⇒ Some ? set_sp_reg_HC05
| HC08 ⇒ Some ? set_sp_reg_HC08
| HCS08 ⇒ Some ? set_sp_reg_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_sp_reg_IP2022 ])
(λf.Some ? (set_alu m t s (f (alu m t s) sp'))).
(* setter debole di SP *)
(* REGISTRO PC *)
-(* setter specifico HC05 di PC, effettua PC∧mask *)
-ndefinition set_pc_reg_HC05 ≝
-λalu.λpc':word16.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (and_w16 pc' (pc_mask_HC05 alu))
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di PC *)
-ndefinition set_pc_reg_HC08 ≝
-λalu.λpc':word16.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- pc'
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
-(* setter specifico RS08 di PC, effettua PC∧mask *)
-ndefinition set_pc_reg_RS08 ≝
-λalu.λpc':word16.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (and_w16 pc' (pc_mask_RS08 alu))
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
-
(* setter forte di PC *)
ndefinition set_pc_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λpc':word16.
| HC08 ⇒ set_pc_reg_HC08
| HCS08 ⇒ set_pc_reg_HC08
| RS08 ⇒ set_pc_reg_RS08
+ | IP2022 ⇒ set_pc_reg_IP2022
] (alu m t s) pc').
(* REGISTRO SPC *)
-(* setter specifico RS08 di SPC, effettua SPC∧mask *)
-ndefinition set_spc_reg_RS08 ≝
-λalu.λspc':word16.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (and_w16 spc' (pc_mask_RS08 alu))
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
-
(* setter forte di SPC *)
ndefinition set_spc_reg ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λspc':word16.
[ HC05 ⇒ None ?
| HC08 ⇒ None ?
| HCS08 ⇒ None ?
- | RS08 ⇒ Some ? set_spc_reg_RS08 ])
+ | RS08 ⇒ Some ? set_spc_reg_RS08
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) spc'))).
(* setter debole di SPC *)
match set_spc_reg m t s spc' with
[ None ⇒ s | Some s' ⇒ s' ].
-(* REGISTRO MEMORY MAPPED X *)
+(* REGISTRO MULH *)
-(* setter specifico RS08 di memory mapped X *)
-ndefinition set_x_map_RS08 ≝
-λalu.λxm':byte8.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- xm'
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
+(* setter forte di MULH *)
+ndefinition set_mulh_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_mulh_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) mulh'))).
+
+(* setter debole di MULH *)
+ndefinition setweak_mulh_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λmulh':byte8.
+ match set_mulh_reg m t s mulh' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO ADDRSEL *)
+
+(* setter forte di ADDRSEL *)
+ndefinition set_addrsel_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
+ opt_map … (match m return aux_set_type_opt byte8 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_addrsel_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) addrsel'))).
+
+(* setter debole di ADDRSEL *)
+ndefinition setweak_addrsel_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddrsel':byte8.
+ match set_addrsel_reg m t s addrsel' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO ADDR *)
+
+(* setter forte di ADDR *)
+ndefinition set_addr_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
+ opt_map … (match m return aux_set_type_opt word24 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_addr_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) addr'))).
+
+(* setter debole di ADDR *)
+ndefinition setweak_addr_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr':word24.
+ match set_addr_reg m t s addr' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO CALL *)
+
+(* setter forte di CALL *)
+ndefinition set_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_call_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
+
+(* setter debole di CALL *)
+ndefinition setweak_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ match set_call_reg m t s call' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* push forte di CALL *)
+ndefinition push_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? push_call_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) call'))).
+
+(* push debole di CALL *)
+ndefinition pushweak_call_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λcall':word16.
+ match push_call_reg m t s call' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO IP *)
+
+(* setter forte di IP *)
+ndefinition set_ip_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_ip_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) ip'))).
+
+(* setter debole di IP *)
+ndefinition setweak_ip_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λip':word16.
+ match set_ip_reg m t s ip' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO DP *)
+
+(* setter forte di DP *)
+ndefinition set_dp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_dp_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) dp'))).
+
+(* setter debole di DP *)
+ndefinition setweak_dp_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdp':word16.
+ match set_dp_reg m t s dp' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO DATA *)
+
+(* setter forte di DATA *)
+ndefinition set_data_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
+ opt_map … (match m return aux_set_type_opt word16 with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_data_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) data'))).
+
+(* setter debole di DATA *)
+ndefinition setweak_data_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λdata':word16.
+ match set_data_reg m t s data' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO SPEED *)
+
+(* setter forte di SPEED *)
+ndefinition set_speed_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
+ opt_map … (match m return aux_set_type_opt exadecim with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_speed_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) speed'))).
+
+(* setter debole di SPEED *)
+ndefinition setweak_speed_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λspeed':exadecim.
+ match set_speed_reg m t s speed' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO PAGE *)
+
+(* setter forte di PAGE *)
+ndefinition set_page_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
+ opt_map … (match m return aux_set_type_opt oct with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_page_reg_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) page'))).
+
+(* setter debole di PAGE *)
+ndefinition setweak_page_reg ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λpage':oct.
+ match set_page_reg m t s page' with
+ [ None ⇒ s | Some s' ⇒ s' ].
+
+(* REGISTRO MEMORY MAPPED X *)
(* setter forte di memory mapped X *)
ndefinition set_x_map ≝
[ HC05 ⇒ None ?
| HC08 ⇒ None ?
| HCS08 ⇒ None ?
- | RS08 ⇒ Some ? set_x_map_RS08 ])
+ | RS08 ⇒ Some ? set_x_map_RS08
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) xm'))).
(* setter debole di memory mapped X *)
(* REGISTRO MEMORY MAPPED PS *)
-(* setter specifico RS08 di memory mapped PS *)
-ndefinition set_ps_map_RS08 ≝
-λalu.λpsm':byte8.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- psm'
- (z_flag_RS08 alu)
- (c_flag_RS08 alu).
-
(* setter forte di memory mapped PS *)
ndefinition set_ps_map ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λpsm':byte8.
[ HC05 ⇒ None ?
| HC08 ⇒ None ?
| HCS08 ⇒ None ?
- | RS08 ⇒ Some ? set_ps_map_RS08 ])
+ | RS08 ⇒ Some ? set_ps_map_RS08
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) psm'))).
(* setter debole di memory mapped PS *)
match set_ps_map m t s psm' with
[ None ⇒ s | Some s' ⇒ s' ].
-(* FLAG V *)
+(* MODALITA SKIP *)
+
+(* setter forte di SKIP *)
+ndefinition set_skip_mode ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
+ opt_map … (match m return aux_set_type_opt bool with
+ [ HC05 ⇒ None ?
+ | HC08 ⇒ None ?
+ | HCS08 ⇒ None ?
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_skip_mode_IP2022 ])
+ (λf.Some ? (set_alu m t s (f (alu m t s) skipmode'))).
+
+(* setter debole di SKIP *)
+ndefinition setweak_skip_mode ≝
+λm:mcu_type.λt:memory_impl.λs:any_status m t.λskipmode':bool.
+ match set_skip_mode m t s skipmode' with
+ [ None ⇒ s | Some s' ⇒ s' ].
-(* setter specifico HC08/HCS08 di V *)
-ndefinition set_v_flag_HC08 ≝
-λalu.λvfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- vfl'
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
+(* FLAG V *)
(* setter forte di V *)
ndefinition set_v_flag ≝
[ HC05 ⇒ None ?
| HC08 ⇒ Some ? set_v_flag_HC08
| HCS08 ⇒ Some ? set_v_flag_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) vfl'))).
(* setter debole di V *)
(* FLAG H *)
-(* setter specifico HC05 di H *)
-ndefinition set_h_flag_HC05 ≝
-λalu.λhfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- hfl'
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di H *)
-ndefinition set_h_flag_HC08 ≝
-λalu.λhfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- hfl'
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di H *)
ndefinition set_h_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λhfl':bool.
[ HC05 ⇒ Some ? set_h_flag_HC05
| HC08 ⇒ Some ? set_h_flag_HC08
| HCS08 ⇒ Some ? set_h_flag_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ Some ? set_h_flag_IP2022 ])
(λf.Some ? (set_alu m t s (f (alu m t s) hfl'))).
(* setter debole di H *)
(* FLAG I *)
-(* setter specifico HC05 di I *)
-ndefinition set_i_flag_HC05 ≝
-λalu.λifl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- ifl'
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di I *)
-ndefinition set_i_flag_HC08 ≝
-λalu.λifl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- ifl'
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di I *)
ndefinition set_i_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λifl':bool.
[ HC05 ⇒ Some ? set_i_flag_HC05
| HC08 ⇒ Some ? set_i_flag_HC08
| HCS08 ⇒ Some ? set_i_flag_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) ifl'))).
(* setter debole di I *)
(* FLAG N *)
-(* setter specifico HC05 di N *)
-ndefinition set_n_flag_HC05 ≝
-λalu.λnfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- nfl'
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di N *)
-ndefinition set_n_flag_HC08 ≝
-λalu.λnfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- nfl'
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
(* setter forte di N *)
ndefinition set_n_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λnfl':bool.
[ HC05 ⇒ Some ? set_n_flag_HC05
| HC08 ⇒ Some ? set_n_flag_HC08
| HCS08 ⇒ Some ? set_n_flag_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) nfl'))).
(* setter debole di N *)
(* FLAG Z *)
-(* setter specifico HC05 di Z *)
-ndefinition set_z_flag_HC05 ≝
-λalu.λzfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- zfl'
- (c_flag_HC05 alu)
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di Z *)
-ndefinition set_z_flag_HC08 ≝
-λalu.λzfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- zfl'
- (c_flag_HC08 alu)
- (irq_flag_HC08 alu).
-
-(* setter sprcifico RS08 di Z *)
-ndefinition set_z_flag_RS08 ≝
-λalu.λzfl':bool.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- zfl'
- (c_flag_RS08 alu).
-
(* setter forte di Z *)
ndefinition set_z_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λzfl':bool.
| HC08 ⇒ set_z_flag_HC08
| HCS08 ⇒ set_z_flag_HC08
| RS08 ⇒ set_z_flag_RS08
+ | IP2022 ⇒ set_z_flag_IP2022
] (alu m t s) zfl').
(* FLAG C *)
-(* setter specifico HC05 di C *)
-ndefinition set_c_flag_HC05 ≝
-λalu.λcfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- cfl'
- (irq_flag_HC05 alu).
-
-(* setter specifico HC08/HCS08 di C *)
-ndefinition set_c_flag_HC08 ≝
-λalu.λcfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- cfl'
- (irq_flag_HC08 alu).
-
-(* setter specifico RS08 di C *)
-ndefinition set_c_flag_RS08 ≝
-λalu.λcfl':bool.
- mk_alu_RS08
- (acc_low_reg_RS08 alu)
- (pc_reg_RS08 alu)
- (pc_mask_RS08 alu)
- (spc_reg_RS08 alu)
- (x_map_RS08 alu)
- (ps_map_RS08 alu)
- (z_flag_RS08 alu)
- cfl'.
-
(* setter forte di C *)
ndefinition set_c_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λcfl':bool.
| HC08 ⇒ set_c_flag_HC08
| HCS08 ⇒ set_c_flag_HC08
| RS08 ⇒ set_c_flag_RS08
+ | IP2022 ⇒ set_c_flag_IP2022
] (alu m t s) cfl').
(* FLAG IRQ *)
-(* setter specifico HC05 di IRQ *)
-ndefinition set_irq_flag_HC05 ≝
-λalu.λirqfl':bool.
- mk_alu_HC05
- (acc_low_reg_HC05 alu)
- (indX_low_reg_HC05 alu)
- (sp_reg_HC05 alu)
- (sp_mask_HC05 alu)
- (sp_fix_HC05 alu)
- (pc_reg_HC05 alu)
- (pc_mask_HC05 alu)
- (h_flag_HC05 alu)
- (i_flag_HC05 alu)
- (n_flag_HC05 alu)
- (z_flag_HC05 alu)
- (c_flag_HC05 alu)
- irqfl'.
-
-(* setter specifico HC08/HCS08 di IRQ *)
-ndefinition set_irq_flag_HC08 ≝
-λalu.λirqfl':bool.
- mk_alu_HC08
- (acc_low_reg_HC08 alu)
- (indX_low_reg_HC08 alu)
- (indX_high_reg_HC08 alu)
- (sp_reg_HC08 alu)
- (pc_reg_HC08 alu)
- (v_flag_HC08 alu)
- (h_flag_HC08 alu)
- (i_flag_HC08 alu)
- (n_flag_HC08 alu)
- (z_flag_HC08 alu)
- (c_flag_HC08 alu)
- irqfl'.
-
(* setter forte di IRQ *)
ndefinition set_irq_flag ≝
λm:mcu_type.λt:memory_impl.λs:any_status m t.λirqfl':bool.
[ HC05 ⇒ Some ? set_irq_flag_HC05
| HC08 ⇒ Some ? set_irq_flag_HC08
| HCS08 ⇒ Some ? set_irq_flag_HC08
- | RS08 ⇒ None ? ])
+ | RS08 ⇒ None ?
+ | IP2022 ⇒ None ? ])
(λf.Some ? (set_alu m t s (f (alu m t s) irqfl'))).
(* setter debole di IRQ *)
(* operatore shift destro *)
ndefinition shr_b8 ≝
-λb:byte8.match rcr_ex (b8h b) false with
+λb:byte8.match shr_ex (b8h b) with
[ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
[ pair bl' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
(* operatore rotazione destra *)
ndefinition ror_b8 ≝
-λb:byte8.match rcr_ex (b8h b) false with
+λb:byte8.match shr_ex (b8h b) with
[ pair bh' c' ⇒ match rcr_ex (b8l b) c' with
[ pair bl' c'' ⇒ match c'' with
[ true ⇒ mk_byte8 (or_ex x8 bh') bl'
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_b8_n (b:byte8) (n:nat) on n ≝
- match n with
- [ O ⇒ b
- | S n' ⇒ ror_b8_n (ror_b8 b) n' ].
+nlet rec ror_b8_n (b:byte8) (o:oct) (ro:rec_oct o) on ro ≝
+ match ro with
+ [ oc_O ⇒ b
+ | oc_S o' n' ⇒ ror_b8_n (ror_b8 b) o' n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_b8 ≝
(* operatore shift sinistro *)
ndefinition shl_b8 ≝
-λb:byte8.match rcl_ex (b8l b) false with
+λb:byte8.match shl_ex (b8l b) with
[ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
[ pair bh' c'' ⇒ pair … (mk_byte8 bh' bl') c'' ]].
(* operatore rotazione sinistra *)
ndefinition rol_b8 ≝
-λb:byte8.match rcl_ex (b8l b) false with
+λb:byte8.match shl_ex (b8l b) with
[ pair bl' c' ⇒ match rcl_ex (b8h b) c' with
[ pair bh' c'' ⇒ match c'' with
[ true ⇒ mk_byte8 bh' (or_ex x1 bl')
| false ⇒ mk_byte8 bh' bl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_b8_n (b:byte8) (n:nat) on n ≝
- match n with
- [ O ⇒ b
- | S n' ⇒ rol_b8_n (rol_b8 b) n' ].
+nlet rec rol_b8_n (b:byte8) (o:oct) (ro:rec_oct o) on ro ≝
+ match ro with
+ [ oc_O ⇒ b
+ | oc_S o' n' ⇒ rol_b8_n (rol_b8 b) o' n' ].
(* operatore not/complemento a 1 *)
ndefinition not_b8 ≝
ndefinition plus_b8_dc_dc ≝
λb1,b2:byte8.λc:bool.
match plus_ex_dc_dc (b8l b1) (b8l b2) c with
- [ pair l c ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c with
- [ pair h c' ⇒ pair … 〈h,l〉 c' ]].
+ [ pair l c' ⇒ match plus_ex_dc_dc (b8h b1) (b8h b2) c' with
+ [ pair h c'' ⇒ pair … 〈h,l〉 c'' ]].
(* operatore somma con data+carry → data *)
ndefinition plus_b8_dc_d ≝
λb1,b2:byte8.λc:bool.
match plus_ex_dc_dc (b8l b1) (b8l b2) c with
- [ pair l c ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c,l〉 ].
+ [ pair l c' ⇒ 〈plus_ex_dc_d (b8h b1) (b8h b2) c',l〉 ].
(* operatore somma con data+carry → c *)
ndefinition plus_b8_dc_c ≝
pair … X'' true
].
+(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
+nlet rec div_b8_ex_aux (divd:byte8) (divs:byte8) (molt:exadecim) (q:exadecim) (qu:quatern) (rqu:rec_quatern qu) on rqu ≝
+ let w' ≝ plus_b8_d_d divd (compl_b8 divs) in
+ match rqu with
+ [ qu_O ⇒ match le_b8 divs divd with
+ [ true ⇒ triple … (or_ex molt q) (b8l w') (⊖ (eq_ex (b8h w') x0))
+ | false ⇒ triple … q (b8l divd) (⊖ (eq_ex (b8h divd) x0)) ]
+ | qu_S qu' rqu' ⇒ match le_b8 divs divd with
+ [ true ⇒ div_b8_ex_aux w' (ror_b8 divs) (ror_ex molt) (or_ex molt q) qu' rqu'
+ | false ⇒ div_b8_ex_aux divd (ror_b8 divs) (ror_ex molt) q qu' rqu' ]].
+
+ndefinition div_b8_ex ≝
+λb:byte8.λe:exadecim.match eq_ex e x0 with
+(*
+ la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
+*)
+ [ true ⇒ triple … xF (b8l b) true
+ | false ⇒ match eq_b8 b 〈x0,x0〉 with
+(* 0 diviso qualsiasi cosa diverso da 0 da' q=0 r=0 o=false *)
+ [ true ⇒ triple … x0 x0 false
+(* 1) e' una divisione sensata che produrra' overflow/risultato *)
+(* 2) parametri: dividendo, divisore, moltiplicatore, quoziente, contatore *)
+(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
+(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
+(* puo' essere sottratto al dividendo *)
+ | false ⇒ div_b8_ex_aux b (rol_b8_n 〈x0,e〉 ? (oct_to_recoct o3)) x8 x0 ? (qu_to_recqu q3) ]].
+
(* operatore x in [inf,sup] o in sup],[inf *)
ndefinition inrange_b8 ≝
λx,inf,sup:byte8.
| xC ⇒ x6 | xD ⇒ xE | xE ⇒ x7 | xF ⇒ xF ].
(* operatore rotazione destra n-volte *)
-nlet rec ror_ex_n (e:exadecim) (n:nat) on n ≝
- match n with
- [ O ⇒ e
- | S n' ⇒ ror_ex_n (ror_ex e) n' ].
+nlet rec ror_ex_n (e:exadecim) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+ [ qu_O ⇒ e
+ | qu_S q' n' ⇒ ror_ex_n (ror_ex e) q' n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_ex ≝
| xC ⇒ x9 | xD ⇒ xB | xE ⇒ xD | xF ⇒ xF ].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_ex_n (e:exadecim) (n:nat) on n ≝
- match n with
- [ O ⇒ e
- | S n' ⇒ rol_ex_n (rol_ex e) n' ].
+nlet rec rol_ex_n (e:exadecim) (q:quatern) (rq:rec_quatern q) on rq ≝
+ match rq with
+ [ qu_O ⇒ e
+ | qu_S q' n' ⇒ rol_ex_n (rol_ex e) q' n' ].
(* operatore not/complemento a 1 *)
ndefinition not_ex ≝
ndefinition rcr_w16 ≝
λw:word16.λc:bool.match rcr_b8 (w16h w) c with
[ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
- [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
+ [ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
(* operatore shift destro *)
ndefinition shr_w16 ≝
-λw:word16.match rcr_b8 (w16h w) false with
+λw:word16.match shr_b8 (w16h w) with
[ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
[ pair wl' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
(* operatore rotazione destra *)
ndefinition ror_w16 ≝
-λw:word16.match rcr_b8 (w16h w) false with
+λw:word16.match shr_b8 (w16h w) with
[ pair wh' c' ⇒ match rcr_b8 (w16l w) c' with
[ pair wl' c'' ⇒ match c'' with
[ true ⇒ mk_word16 (or_b8 (mk_byte8 x8 x0) wh') wl'
| false ⇒ mk_word16 wh' wl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_w16_n (w:word16) (n:nat) on n ≝
- match n with
- [ O ⇒ w
- | S n' ⇒ ror_w16_n (ror_w16 w) n' ].
+nlet rec ror_w16_n (w:word16) (e:exadecim) (re:rec_exadecim e) on re ≝
+ match re with
+ [ ex_O ⇒ w
+ | ex_S e' n' ⇒ ror_w16_n (ror_w16 w) e' n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_w16 ≝
(* operatore shift sinistro *)
ndefinition shl_w16 ≝
-λw:word16.match rcl_b8 (w16l w) false with
+λw:word16.match shl_b8 (w16l w) with
[ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
[ pair wh' c'' ⇒ pair … (mk_word16 wh' wl') c'' ]].
(* operatore rotazione sinistra *)
ndefinition rol_w16 ≝
-λw:word16.match rcl_b8 (w16l w) false with
+λw:word16.match shl_b8 (w16l w) with
[ pair wl' c' ⇒ match rcl_b8 (w16h w) c' with
[ pair wh' c'' ⇒ match c'' with
[ true ⇒ mk_word16 wh' (or_b8 (mk_byte8 x0 x1) wl')
| false ⇒ mk_word16 wh' wl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_w16_n (w:word16) (n:nat) on n ≝
- match n with
- [ O ⇒ w
- | S n' ⇒ rol_w16_n (rol_w16 w) n' ].
+nlet rec rol_w16_n (w:word16) (e:exadecim) (re:rec_exadecim e) on re ≝
+ match re with
+ [ ex_O ⇒ w
+ | ex_S e' n' ⇒ rol_w16_n (rol_w16 w) e' n' ].
(* operatore not/complemento a 1 *)
ndefinition not_w16 ≝
ndefinition plus_w16_dc_dc ≝
λw1,w2:word16.λc:bool.
match plus_b8_dc_dc (w16l w1) (w16l w2) c with
- [ pair l c ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c with
- [ pair h c' ⇒ pair … 〈h:l〉 c' ]].
+ [ pair l c' ⇒ match plus_b8_dc_dc (w16h w1) (w16h w2) c' with
+ [ pair h c'' ⇒ pair … 〈h:l〉 c'' ]].
(* operatore somma con data+carry → data *)
ndefinition plus_w16_dc_d ≝
λw1,w2:word16.λc:bool.
match plus_b8_dc_dc (w16l w1) (w16l w2) c with
- [ pair l c ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c:l〉 ].
+ [ pair l c' ⇒ 〈plus_b8_dc_d (w16h w1) (w16h w2) c':l〉 ].
(* operatore somma con data+carry → c *)
ndefinition plus_w16_dc_c ≝
]]]]]].
(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (c:nat) on c ≝
+nlet rec div_w16_b8_aux (divd:word16) (divs:word16) (molt:byte8) (q:byte8) (o:oct) (ro:rec_oct o) on ro ≝
let w' ≝ plus_w16_d_d divd (compl_w16 divs) in
- match c with
- [ O ⇒ match le_w16 divs divd with
+ match ro with
+ [ oc_O ⇒ match le_w16 divs divd with
[ true ⇒ triple … (or_b8 molt q) (w16l w') (⊖ (eq_b8 (w16h w') 〈x0,x0〉))
| false ⇒ triple … q (w16l divd) (⊖ (eq_b8 (w16h divd) 〈x0,x0〉)) ]
- | S c' ⇒ match le_w16 divs divd with
- [ true ⇒ div_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) c'
- | false ⇒ div_b8_aux divd (ror_w16 divs) (ror_b8 molt) q c' ]].
+ | oc_S o' ro' ⇒ match le_w16 divs divd with
+ [ true ⇒ div_w16_b8_aux w' (ror_w16 divs) (ror_b8 molt) (or_b8 molt q) o' ro'
+ | false ⇒ div_w16_b8_aux divd (ror_w16 divs) (ror_b8 molt) q o' ro' ]].
-ndefinition div_b8 ≝
+ndefinition div_w16_b8 ≝
λw:word16.λb:byte8.match eq_b8 b 〈x0,x0〉 with
(*
la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
(* puo' essere sottratto al dividendo *)
- | false ⇒ div_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 nat7) 〈x8,x0〉 〈x0,x0〉 nat7 ]].
+ | false ⇒ div_w16_b8_aux w (rol_w16_n 〈〈x0,x0〉:b〉 ? (ex_to_recex x7)) 〈x8,x0〉 〈x0,x0〉 ? (oct_to_recoct o7) ]].
(* operatore x in [inf,sup] o in sup],[inf *)
ndefinition inrange_w16 ≝
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/byte8.ma".
+
+(* ********* *)
+(* BYTE+WORD *)
+(* ********* *)
+
+nrecord word24 : Type ≝
+ {
+ w24x: byte8;
+ w24h: byte8;
+ w24l: byte8
+ }.
+
+(* \langle \rangle *)
+notation "〈x;y;z〉" non associative with precedence 80
+ for @{ 'mk_word24 $x $y $z }.
+interpretation "mk_word24" 'mk_word24 x y z = (mk_word24 x y z).
+
+(* operatore = *)
+ndefinition eq_w24 ≝
+λw1,w2.(eq_b8 (w24x w1) (w24x w2)) ⊗
+ (eq_b8 (w24h w1) (w24h w2)) ⊗
+ (eq_b8 (w24l w1) (w24l w2)).
+
+(* operatore < *)
+ndefinition lt_w24 ≝
+λw1,w2:word24.
+ (lt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (lt_b8 (w24l w1) (w24l w2))))).
+
+(* operatore ≤ *)
+ndefinition le_w24 ≝
+λw1,w2:word24.
+ (lt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((lt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (le_b8 (w24l w1) (w24l w2))))).
+
+(* operatore > *)
+ndefinition gt_w24 ≝
+λw1,w2:word24.
+ (gt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (gt_b8 (w24l w1) (w24l w2))))).
+
+(* operatore ≥ *)
+ndefinition ge_w24 ≝
+λw1,w2:word24.
+ (gt_b8 (w24x w1) (w24x w2)) ⊕
+ ((eq_b8 (w24x w1) (w24x w2)) ⊗ ((gt_b8 (w24h w1) (w24h w2)) ⊕
+ ((eq_b8 (w24h w1) (w24h w2)) ⊗ (ge_b8 (w24l w1) (w24l w2))))).
+
+(* operatore and *)
+ndefinition and_w24 ≝
+λw1,w2:word24.
+ mk_word24 (and_b8 (w24x w1) (w24x w2))
+ (and_b8 (w24h w1) (w24h w2))
+ (and_b8 (w24l w1) (w24l w2)).
+
+(* operatore or *)
+ndefinition or_w24 ≝
+λw1,w2:word24.
+ mk_word24 (or_b8 (w24x w1) (w24x w2))
+ (or_b8 (w24h w1) (w24h w2))
+ (or_b8 (w24l w1) (w24l w2)).
+
+(* operatore xor *)
+ndefinition xor_w24 ≝
+λw1,w2:word24.
+ mk_word24 (xor_b8 (w24x w1) (w24x w2))
+ (xor_b8 (w24h w1) (w24h w2))
+ (xor_b8 (w24l w1) (w24l w2)).
+
+(* operatore rotazione destra con carry *)
+ndefinition rcr_w24 ≝
+λw:word24.λc:bool.match rcr_b8 (w24x w) c with
+ [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
+ [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore shift destro *)
+ndefinition shr_w24 ≝
+λw:word24.match shr_b8 (w24x w) with
+ [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
+ [ pair wl' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore rotazione destra *)
+ndefinition ror_w24 ≝
+λw:word24.match shr_b8 (w24x w) with
+ [ pair wx' c' ⇒ match rcr_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcr_b8 (w24l w) c'' with
+ [ pair wl' c''' ⇒ match c''' with
+ [ true ⇒ mk_word24 (or_b8 (mk_byte8 x8 x0) wx') wh' wl'
+ | false ⇒ mk_word24 wx' wh' wl' ]]]].
+
+(* operatore rotazione destra n-volte *)
+nlet rec ror_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ w
+ | bi_S t' n' ⇒ ror_w24_n (ror_w24 w) t' n' ].
+
+(* operatore rotazione sinistra con carry *)
+ndefinition rcl_w24 ≝
+λw:word24.λc:bool.match rcl_b8 (w24l w) c with
+ [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
+ [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore shift sinistro *)
+ndefinition shl_w24 ≝
+λw:word24.match shl_b8 (w24l w) with
+ [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
+ [ pair wx' c''' ⇒ pair … (mk_word24 wx' wh' wl') c''' ]]].
+
+(* operatore rotazione sinistra *)
+ndefinition rol_w24 ≝
+λw:word24.match shl_b8 (w24l w) with
+ [ pair wl' c' ⇒ match rcl_b8 (w24h w) c' with
+ [ pair wh' c'' ⇒ match rcl_b8 (w24x w) c'' with
+ [ pair wx' c''' ⇒ match c''' with
+ [ true ⇒ mk_word24 wx' wh' (or_b8 (mk_byte8 x0 x1) wl')
+ | false ⇒ mk_word24 wx' wh' wl' ]]]].
+
+(* operatore rotazione sinistra n-volte *)
+nlet rec rol_w24_n (w:word24) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ w
+ | bi_S t' n' ⇒ rol_w24_n (rol_w24 w) t' n' ].
+
+(* operatore not/complemento a 1 *)
+ndefinition not_w24 ≝
+λw:word24.mk_word24 (not_b8 (w24x w)) (not_b8 (w24h w)) (not_b8 (w24l w)).
+
+(* operatore somma con data+carry → data+carry *)
+ndefinition plus_w24_dc_dc ≝
+λw1,w2:word24.λc:bool.
+ match plus_b8_dc_dc (w24l w1) (w24l w2) c with
+ [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
+ [ pair h c'' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c'' with
+ [ pair x c''' ⇒ pair … 〈x;h;l〉 c''' ]]].
+
+(* operatore somma con data+carry → data *)
+ndefinition plus_w24_dc_d ≝
+λw1,w2:word24.λc:bool.
+ match plus_b8_dc_dc (w24l w1) (w24l w2) c with
+ [ pair l c' ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c' with
+ [ pair h c'' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c'';h;l〉 ]].
+
+(* operatore somma con data+carry → c *)
+ndefinition plus_w24_dc_c ≝
+λw1,w2:word24.λc:bool.
+ plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_dc_c (w24l w1) (w24l w2) c)).
+
+(* operatore somma con data → data+carry *)
+ndefinition plus_w24_d_dc ≝
+λw1,w2:word24.
+ match plus_b8_d_dc (w24l w1) (w24l w2) with
+ [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
+ [ pair h c' ⇒ match plus_b8_dc_dc (w24x w1) (w24x w2) c' with
+ [ pair x c'' ⇒ pair … 〈x;h;l〉 c'' ]]].
+
+(* operatore somma con data → data *)
+ndefinition plus_w24_d_d ≝
+λw1,w2:word24.
+ match plus_b8_d_dc (w24l w1) (w24l w2) with
+ [ pair l c ⇒ match plus_b8_dc_dc (w24h w1) (w24h w2) c with
+ [ pair h c' ⇒ 〈plus_b8_dc_d (w24x w1) (w24x w2) c';h;l〉 ]].
+
+(* operatore somma con data → c *)
+ndefinition plus_w24_d_c ≝
+λw1,w2:word24.
+ plus_b8_dc_c (w24x w1) (w24x w2) (plus_b8_dc_c (w24h w1) (w24h w2) (plus_b8_d_c (w24l w1) (w24l w2))).
+
+(* operatore Most Significant Bit *)
+ndefinition MSB_w24 ≝ λw:word24.eq_ex x8 (and_ex x8 (b8h (w24x w))).
+
+(* operatore predecessore *)
+ndefinition pred_w24 ≝
+λw:word24.match eq_b8 (w24l w) (mk_byte8 x0 x0) with
+ [ true ⇒ match eq_b8 (w24h w) (mk_byte8 x0 x0) with
+ [ true ⇒ mk_word24 (pred_b8 (w24x w)) (pred_b8 (w24h w)) (pred_b8 (w24l w))
+ | false ⇒ mk_word24 (w24x w) (pred_b8 (w24h w)) (pred_b8 (w24l w)) ]
+ | false ⇒ mk_word24 (w24x w) (w24h w) (pred_b8 (w24l w)) ].
+
+(* operatore successore *)
+ndefinition succ_w24 ≝
+λw:word24.match eq_b8 (w24l w) (mk_byte8 xF xF) with
+ [ true ⇒ match eq_b8 (w24h w) (mk_byte8 xF xF) with
+ [ true ⇒ mk_word24 (succ_b8 (w24x w)) (succ_b8 (w24h w)) (succ_b8 (w24l w))
+ | false ⇒ mk_word24 (w24x w) (succ_b8 (w24h w)) (succ_b8 (w24l w)) ]
+ | false ⇒ mk_word24 (w24x w) (w24h w) (succ_b8 (w24l w)) ].
+
+(* operatore neg/complemento a 2 *)
+ndefinition compl_w24 ≝
+λw:word24.match MSB_w24 w with
+ [ true ⇒ succ_w24 (not_w24 w)
+ | false ⇒ not_w24 (pred_w24 w) ].
+
+(* operatore x in [inf,sup] o in sup],[inf *)
+ndefinition inrange_w24 ≝
+λx,inf,sup:word24.
+ match le_w24 inf sup with
+ [ true ⇒ and_bool | false ⇒ or_bool ]
+ (le_w24 inf x) (le_w24 x sup).
+
+(* iteratore sulle word *)
+ndefinition forall_w24 ≝
+ λP.
+ forall_b8 (λbx.
+ forall_b8 (λbh.
+ forall_b8 (λbl.
+ P (mk_word24 bx bh bl )))).
| false ⇒ mk_word32 wh' wl' ]]].
(* operatore rotazione destra n-volte *)
-nlet rec ror_w32_n (dw:word32) (n:nat) on n ≝
- match n with
- [ O ⇒ dw
- | S n' ⇒ ror_w32_n (ror_w32 dw) n' ].
+nlet rec ror_w32_n (dw:word32) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ dw
+ | bi_S t' n' ⇒ ror_w32_n (ror_w32 dw) t' n' ].
(* operatore rotazione sinistra con carry *)
ndefinition rcl_w32 ≝
| false ⇒ mk_word32 wh' wl' ]]].
(* operatore rotazione sinistra n-volte *)
-nlet rec rol_w32_n (dw:word32) (n:nat) on n ≝
- match n with
- [ O ⇒ dw
- | S n' ⇒ rol_w32_n (rol_w32 dw) n' ].
+nlet rec rol_w32_n (dw:word32) (t:bitrigesim) (rt:rec_bitrigesim t) on rt ≝
+ match rt with
+ [ bi_O ⇒ dw
+ | bi_S t' n' ⇒ rol_w32_n (rol_w32 dw) t' n' ].
(* operatore not/complemento a 1 *)
ndefinition not_w32 ≝
ndefinition plus_w32_dc_dc ≝
λdw1,dw2:word32.λc:bool.
match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
- [ pair l c ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c with
- [ pair h c' ⇒ pair … 〈h.l〉 c' ]].
+ [ pair l c' ⇒ match plus_w16_dc_dc (w32h dw1) (w32h dw2) c' with
+ [ pair h c'' ⇒ pair … 〈h.l〉 c'' ]].
(* operatore somma con data+carry → data *)
ndefinition plus_w32_dc_d ≝
λdw1,dw2:word32.λc:bool.
match plus_w16_dc_dc (w32l dw1) (w32l dw2) c with
- [ pair l c ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c.l〉 ].
+ [ pair l c' ⇒ 〈plus_w16_dc_d (w32h dw1) (w32h dw2) c'.l〉 ].
(* operatore somma con data+carry → c *)
ndefinition plus_w32_dc_c ≝
]]]]]].
(* divisione senza segno (secondo la logica delle ALU): (quoziente resto) overflow *)
-nlet rec div_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (c:nat) on c ≝
+nlet rec div_w32_w16_aux (divd:word32) (divs:word32) (molt:word16) (q:word16) (e:exadecim) (re:rec_exadecim e) on re ≝
let w' ≝ plus_w32_d_d divd (compl_w32 divs) in
- match c with
- [ O ⇒ match le_w32 divs divd with
+ match re with
+ [ ex_O ⇒ match le_w32 divs divd with
[ true ⇒ triple … (or_w16 molt q) (w32l w') (⊖ (eq_w16 (w32h w') 〈〈x0,x0〉:〈x0,x0〉〉))
| false ⇒ triple … q (w32l divd) (⊖ (eq_w16 (w32h divd) 〈〈x0,x0〉:〈x0,x0〉〉)) ]
- | S c' ⇒ match le_w32 divs divd with
- [ true ⇒ div_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) c'
- | false ⇒ div_w16_aux divd (ror_w32 divs) (ror_w16 molt) q c' ]].
+ | ex_S e' re' ⇒ match le_w32 divs divd with
+ [ true ⇒ div_w32_w16_aux w' (ror_w32 divs) (ror_w16 molt) (or_w16 molt q) e' re'
+ | false ⇒ div_w32_w16_aux divd (ror_w32 divs) (ror_w16 molt) q e' re' ]].
-ndefinition div_w16 ≝
+ndefinition div_w32_w16 ≝
λw:word32.λb:word16.match eq_w16 b 〈〈x0,x0〉:〈x0,x0〉〉 with
(*
la combinazione n/0 e' illegale, segnala solo overflow senza dare risultato
(* 3) ad ogni ciclo il divisore e il moltiplicatore vengono scalati di 1 a dx *)
(* 4) il moltiplicatore e' la quantita' aggiunta al quoziente se il divisore *)
(* puo' essere sottratto al dividendo *)
- | false ⇒ div_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 nat15) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 nat15 ]].
+ | false ⇒ div_w32_w16_aux w (rol_w32_n 〈〈〈x0,x0〉:〈x0,x0〉〉.b〉 ? (bit_to_recbit t0F)) 〈〈x8,x0〉:〈x0,x0〉〉 〈〈x0,x0〉:〈x0,x0〉〉 ? (ex_to_recex xF) ]].
(* operatore x in [inf,sup] o in sup],[inf *)
ndefinition inrange_w32 ≝
(* iteratore sulle word *)
ndefinition forall_w32 ≝
λP.
- forall_w16 (λbh.
- forall_w16 (λbl.
- P (mk_word32 bh bl ))).
+ forall_w16 (λwh.
+ forall_w16 (λwl.
+ P (mk_word32 wh wl ))).
projects / helm.git / commitdiff