From: Cosimo Oliboni Date: Mon, 25 Jan 2010 06:56:56 +0000 (+0000) Subject: freescale porting X-Git-Tag: make_still_working~3095 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b886a562ccbfc3f63b8f64a135bcf70e4b189999;p=helm.git freescale porting --- diff --git a/helm/software/matita/contribs/ng_assembly/common/option.ma b/helm/software/matita/contribs/ng_assembly/common/option.ma index 244f087f3..62da65900 100644 --- a/helm/software/matita/contribs/ng_assembly/common/option.ma +++ b/helm/software/matita/contribs/ng_assembly/common/option.ma @@ -31,7 +31,7 @@ ninductive option (A:Type) : Type ≝ | 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 ] diff --git a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma index 144733fe9..7e73870bf 100644 --- a/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/option_lemmas.ma @@ -54,10 +54,10 @@ nlemma option_destruct_none_some : ∀T.∀x:T.None T = Some T x → False. 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; @@ -70,10 +70,10 @@ nlemma symmetric_eqoption : 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; @@ -91,10 +91,10 @@ nlemma eq_to_eqoption : 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; @@ -132,17 +132,17 @@ nlemma decidable_option : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:option T. 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 …)) ##] @@ -150,22 +150,22 @@ nlemma neq_to_neqoption : 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) ##] ##] diff --git a/helm/software/matita/contribs/ng_assembly/common/prod.ma b/helm/software/matita/contribs/ng_assembly/common/prod.ma index fca58bc22..1080533d1 100644 --- a/helm/software/matita/contribs/ng_assembly/common/prod.ma +++ b/helm/software/matita/contribs/ng_assembly/common/prod.ma @@ -36,8 +36,9 @@ ndefinition snd ≝ λ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)). @@ -54,8 +55,9 @@ ndefinition thd3T ≝ λ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)). @@ -76,8 +78,9 @@ ndefinition fth4T ≝ λ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)) ⊗ @@ -102,8 +105,9 @@ ndefinition fft5T ≝ λ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)) ⊗ diff --git a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma index 29998a836..ecf12f382 100644 --- a/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/common/prod_lemmas.ma @@ -48,12 +48,13 @@ nlemma pair_destruct_2 : 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; @@ -68,12 +69,13 @@ nlemma symmetric_eqpair : 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; @@ -86,12 +88,13 @@ nlemma eq_to_eqpair : 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; @@ -130,12 +133,13 @@ nlemma decidable_pair 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; @@ -166,14 +170,15 @@ nlemma pair_destruct 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; @@ -220,13 +225,14 @@ nlemma triple_destruct_3 : 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; @@ -246,13 +252,14 @@ nlemma symmetric_eqtriple : 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; @@ -267,13 +274,14 @@ nlemma eq_to_eqtriple : 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; @@ -324,13 +332,14 @@ nlemma decidable_triple 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; @@ -368,16 +377,17 @@ nlemma triple_destruct 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; @@ -435,14 +445,15 @@ nlemma quadruple_destruct_4 : 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; @@ -467,14 +478,15 @@ nlemma symmetric_eqquadruple : 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; @@ -491,14 +503,15 @@ nlemma eq_to_eqquadruple : 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; @@ -560,14 +573,15 @@ nlemma decidable_quadruple 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; @@ -613,8 +627,9 @@ nlemma quadruple_destruct 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)) → @@ -623,8 +638,8 @@ nlemma neq_to_neqquadruple : (∀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; @@ -693,15 +708,16 @@ nlemma quintuple_destruct_5 : 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; @@ -731,15 +747,16 @@ nlemma symmetric_eqquintuple : 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; @@ -758,15 +775,16 @@ nlemma eq_to_eqquintuple : 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; @@ -839,15 +857,16 @@ nlemma decidable_quintuple 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; @@ -899,8 +918,9 @@ nlemma quintuple_destruct 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)) → @@ -911,9 +931,8 @@ nlemma neq_to_neqquintuple : (∀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; diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends index 4de80ff8f..a54a98e1e 100644 --- a/helm/software/matita/contribs/ng_assembly/depends +++ b/helm/software/matita/contribs/ng_assembly/depends @@ -10,7 +10,7 @@ compiler/ast_type_lemmas.ma common/list_utility_lemmas.ma compiler/ast_type.ma 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 @@ -23,8 +23,8 @@ num/word32_lemmas.ma num/word16_lemmas.ma num/word32.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 @@ -40,7 +40,8 @@ emulator/opcodes/HCS08_opcode.ma num/bool.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 @@ -54,6 +55,7 @@ common/ascii.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 diff --git a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma index 0e023b5a1..213c68b0a 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_struct.ma @@ -44,6 +44,18 @@ nrecord Array16T (T:Type) : Type ≝ ; 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 *) @@ -335,6 +347,14 @@ nrecord Array8T (T:Type) : Type ≝ { 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 ≝ @@ -357,303 +377,56 @@ let e05 ≝ (a8_6 T p) in 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))). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma index 4e73b5762..b6367ab52 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/HC05_status.ma @@ -68,6 +68,190 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' 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 *) (* ***************** *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma index 8c6ab8f85..dd8234161 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/HC08_status.ma @@ -63,6 +63,231 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' 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 *) (* ***************** *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma new file mode 100755 index 000000000..caea9011c --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/IP2022_status.ma @@ -0,0 +1,518 @@ +(**************************************************************************) +(* ___ *) +(* ||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)). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma index a02971f4c..2b84717f8 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/RS08_status.ma @@ -68,6 +68,101 @@ notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' 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 *) (* ***************** *) diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma index ae5c97c7c..deaf39aad 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma @@ -24,6 +24,7 @@ include "emulator/memory/memory_abs.ma". 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". (* *********************************** *) @@ -39,7 +40,8 @@ ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_op_type m) (aux_im_t 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; @@ -64,15 +66,18 @@ ndefinition eq_alu ≝ 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] *) @@ -83,8 +88,8 @@ nlet rec forall_memory_ranged (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) ]. diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma index 75bb46e31..1f4e5aa5a 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_getter.ma @@ -20,7 +20,7 @@ (* *) (* ********************************************************************** *) -include "emulator/status/status.ma". +include "emulator/status/status_setter.ma". (* **************** *) (* GETTER SPECIFICI *) @@ -28,7 +28,8 @@ include "emulator/status/status.ma". (* 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 *) @@ -40,7 +41,8 @@ ndefinition get_acc_8_low_reg ≝ [ 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 *) @@ -51,7 +53,8 @@ ndefinition get_indX_8_low_reg ≝ [ 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 *) @@ -62,7 +65,8 @@ ndefinition get_indX_8_high_reg ≝ [ 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 *) @@ -73,7 +77,8 @@ ndefinition get_indX_16_reg ≝ [ 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 *) @@ -84,7 +89,8 @@ ndefinition get_sp_reg ≝ [ 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 *) @@ -95,7 +101,8 @@ ndefinition get_pc_reg ≝ [ 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 *) @@ -106,10 +113,149 @@ ndefinition get_spc_reg ≝ [ 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 ≝ @@ -119,7 +265,8 @@ 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 *) @@ -130,7 +277,20 @@ ndefinition get_ps_map ≝ [ 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 *) @@ -143,7 +303,8 @@ ndefinition get_v_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 *) @@ -154,7 +315,8 @@ ndefinition get_h_flag ≝ [ 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 *) @@ -165,7 +327,8 @@ ndefinition get_i_flag ≝ [ 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 *) @@ -176,7 +339,8 @@ ndefinition get_n_flag ≝ [ 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 *) @@ -187,7 +351,8 @@ ndefinition get_z_flag ≝ [ 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 *) @@ -198,7 +363,8 @@ ndefinition get_c_flag ≝ [ 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 *) @@ -209,5 +375,6 @@ ndefinition get_irq_flag ≝ [ 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). diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma index 5a89d2f01..3f1a62839 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status_setter.ma @@ -28,15 +28,19 @@ include "emulator/status/status.ma". (* 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 *) @@ -63,54 +67,6 @@ ndefinition set_clk_desc ≝ (* 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. @@ -120,45 +76,11 @@ ndefinition set_acc_8_low_reg ≝ | 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. @@ -166,7 +88,8 @@ ndefinition set_indX_8_low_reg ≝ [ 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 *) @@ -177,23 +100,6 @@ ndefinition setweak_indX_8_low_reg ≝ (* 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. @@ -201,7 +107,8 @@ ndefinition set_indX_8_high_reg ≝ [ 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 *) @@ -212,23 +119,6 @@ ndefinition setweak_indX_8_high_reg ≝ (* 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. @@ -236,7 +126,8 @@ ndefinition set_indX_16_reg ≝ [ 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 *) @@ -247,41 +138,6 @@ ndefinition setweak_indX_16_reg ≝ (* 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. @@ -289,7 +145,8 @@ ndefinition set_sp_reg ≝ [ 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 *) @@ -300,54 +157,6 @@ ndefinition setweak_sp_reg ≝ (* 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. @@ -357,23 +166,11 @@ ndefinition set_pc_reg ≝ | 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. @@ -381,7 +178,8 @@ ndefinition set_spc_reg ≝ [ 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 *) @@ -390,20 +188,195 @@ ndefinition setweak_spc_reg ≝ 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 ≝ @@ -412,7 +385,8 @@ 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 *) @@ -423,19 +397,6 @@ ndefinition setweak_x_map ≝ (* 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. @@ -443,7 +404,8 @@ ndefinition set_ps_map ≝ [ 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 *) @@ -452,24 +414,26 @@ ndefinition setweak_ps_map ≝ 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 ≝ @@ -478,7 +442,8 @@ 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 *) @@ -489,41 +454,6 @@ ndefinition setweak_v_flag ≝ (* 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. @@ -531,7 +461,8 @@ ndefinition set_h_flag ≝ [ 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 *) @@ -542,41 +473,6 @@ ndefinition setweak_h_flag ≝ (* 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. @@ -584,7 +480,8 @@ ndefinition set_i_flag ≝ [ 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 *) @@ -595,41 +492,6 @@ ndefinition setweak_i_flag ≝ (* 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. @@ -637,7 +499,8 @@ ndefinition set_n_flag ≝ [ 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 *) @@ -648,54 +511,6 @@ ndefinition setweak_n_flag ≝ (* 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. @@ -705,58 +520,11 @@ ndefinition set_z_flag ≝ | 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. @@ -766,45 +534,11 @@ ndefinition set_c_flag ≝ | 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. @@ -812,7 +546,8 @@ ndefinition set_irq_flag ≝ [ 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 *) diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8.ma b/helm/software/matita/contribs/ng_assembly/num/byte8.ma index d759181ce..61da004ee 100755 --- a/helm/software/matita/contribs/ng_assembly/num/byte8.ma +++ b/helm/software/matita/contribs/ng_assembly/num/byte8.ma @@ -85,23 +85,23 @@ ndefinition rcr_b8 ≝ (* 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 ≝ @@ -111,23 +111,23 @@ 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 ≝ @@ -137,14 +137,14 @@ 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 ≝ @@ -306,6 +306,33 @@ ndefinition daa_b8 ≝ 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. diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma index e75c80bd6..62de47a89 100755 --- a/helm/software/matita/contribs/ng_assembly/num/exadecim.ma +++ b/helm/software/matita/contribs/ng_assembly/num/exadecim.ma @@ -713,10 +713,10 @@ ndefinition ror_ex ≝ | 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 ≝ @@ -762,10 +762,10 @@ ndefinition rol_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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/word16.ma b/helm/software/matita/contribs/ng_assembly/num/word16.ma index e89e64f3d..7523ec918 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word16.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word16.ma @@ -80,27 +80,27 @@ ndefinition xor_w16 ≝ 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 ≝ @@ -110,23 +110,23 @@ 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 ≝ @@ -136,14 +136,14 @@ 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 ≝ @@ -207,17 +207,17 @@ ndefinition mul_b8 ≝ ]]]]]]. (* 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 @@ -231,7 +231,7 @@ ndefinition div_b8 ≝ (* 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 ≝ diff --git a/helm/software/matita/contribs/ng_assembly/num/word24.ma b/helm/software/matita/contribs/ng_assembly/num/word24.ma new file mode 100755 index 000000000..70e407c37 --- /dev/null +++ b/helm/software/matita/contribs/ng_assembly/num/word24.ma @@ -0,0 +1,236 @@ +(**************************************************************************) +(* ___ *) +(* ||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 )))). diff --git a/helm/software/matita/contribs/ng_assembly/num/word32.ma b/helm/software/matita/contribs/ng_assembly/num/word32.ma index bc81cac17..7463b56c5 100755 --- a/helm/software/matita/contribs/ng_assembly/num/word32.ma +++ b/helm/software/matita/contribs/ng_assembly/num/word32.ma @@ -97,10 +97,10 @@ ndefinition ror_w32 ≝ | 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 ≝ @@ -123,10 +123,10 @@ ndefinition rol_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 ≝ @@ -136,14 +136,14 @@ 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 ≝ @@ -207,17 +207,17 @@ ndefinition mul_w16 ≝ ]]]]]]. (* 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 @@ -231,7 +231,7 @@ ndefinition div_w16 ≝ (* 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 ≝ @@ -243,6 +243,6 @@ 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 ))).