--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/ast_base_type_base.ma".
+include "common/comp.ma".
+include "num/bool_lemmas.ma".
+
+(* ************************* *)
+(* dimensioni degli elementi *)
+(* ************************* *)
+
+ndefinition astbasetype_destruct_aux ≝
+Πb1,b2:ast_base_type.ΠP:Prop.b1 = b2 →
+ match eq_astbasetype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
+
+ndefinition astbasetype_destruct : astbasetype_destruct_aux.
+ #b1; #b2; #P; #H;
+ nrewrite < H;
+ nelim b1;
+ nnormalize;
+ napply (λx.x).
+nqed.
+
+nlemma eq_to_eqastbasetype : ∀n1,n2.n1 = n2 → eq_astbasetype n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma neqastbasetype_to_neq : ∀n1,n2.eq_astbasetype n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_astbasetype n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqastbasetype n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
+nlemma eqastbasetype_to_eq : ∀b1,b2.eq_astbasetype b1 b2 = true → b1 = b2.
+ #b1; #b2; ncases b1; ncases b2; nnormalize;
+ ##[ ##1,5,9: #H; napply refl_eq
+ ##| ##*: #H; ndestruct (*napply (bool_destruct … H)*)
+ ##]
+nqed.
+
+nlemma neq_to_neqastbasetype : ∀n1,n2.n1 ≠ n2 → eq_astbasetype n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_astbasetype n1 n2));
+ napply (not_to_not (eq_astbasetype n1 n2 = true) (n1 = n2) ? H);
+ napply (eqastbasetype_to_eq n1 n2).
+nqed.
+
+nlemma decidable_astbasetype : ∀x,y:ast_base_type.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_astbasetype x y = true) (eq_astbasetype x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqastbasetype_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqastbasetype_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqastbasetype : symmetricT ast_base_type bool eq_astbasetype.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_astbasetype n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqastbasetype n1 n2 H);
+ napply (symmetric_eq ? (eq_astbasetype n2 n1) false);
+ napply (neq_to_neqastbasetype n2 n1 (symmetric_neq ? n1 n2 H))
+ ##]
+nqed.
+
+nlemma astbasetype_is_comparable : comparable.
+ @ ast_base_type
+ ##[ napply AST_BASE_TYPE_BYTE8
+ ##| napply forall_astbasetype
+ ##| napply eq_astbasetype
+ ##| napply eqastbasetype_to_eq
+ ##| napply eq_to_eqastbasetype
+ ##| napply neqastbasetype_to_neq
+ ##| napply neq_to_neqastbasetype
+ ##| napply decidable_astbasetype
+ ##| napply symmetric_eqastbasetype
+ ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr astbasetype_is_comparable ≡ ast_base_type.
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ************************* *)
+(* dimensioni degli elementi *)
+(* ************************* *)
+
+(* usato per definire nell'ast *)
+ninductive ast_base_type : Type ≝
+ AST_BASE_TYPE_BYTE8: ast_base_type
+| AST_BASE_TYPE_WORD16: ast_base_type
+| AST_BASE_TYPE_WORD32: ast_base_type.
+
+(* iteratore *)
+ndefinition forall_astbasetype ≝ λP.
+ P AST_BASE_TYPE_BYTE8 ⊗
+ P AST_BASE_TYPE_WORD16 ⊗
+ P AST_BASE_TYPE_WORD32.
+
+ndefinition eq_astbasetype ≝
+λt1,t2:ast_base_type.match t1 with
+ [ AST_BASE_TYPE_BYTE8 ⇒ match t2 with [ AST_BASE_TYPE_BYTE8 ⇒ true | _ ⇒ false ]
+ | AST_BASE_TYPE_WORD16 ⇒ match t2 with [ AST_BASE_TYPE_WORD16 ⇒ true | _ ⇒ false ]
+ | AST_BASE_TYPE_WORD32 ⇒ match t2 with [ AST_BASE_TYPE_WORD32 ⇒ true | _ ⇒ false ]
+ ].
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/ast_type_base.ma".
+
+(* ************************* *)
+(* dimensioni degli elementi *)
+(* ************************* *)
+
+nlemma asttype_destruct_base_base : ∀b1,b2.AST_TYPE_BASE b1 = AST_TYPE_BASE b2 → b1 = b2.
+ #b1; #b2; #H;
+ nchange with (match AST_TYPE_BASE b2 with [ AST_TYPE_BASE a ⇒ b1 = a | _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma asttype_destruct_array_array_1 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → x1 = x2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY a _ ⇒ x1 = a | _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma asttype_destruct_array_array_2 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AST_TYPE_ARRAY x2 y2 → y1 = y2.
+ #x1; #x2; #y1; #y2; #H;
+ nchange with (match AST_TYPE_ARRAY x2 y2 with [ AST_TYPE_ARRAY _ b ⇒ y1 = b | _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma asttype_destruct_struct_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_STRUCT b2 → b1 = b2.
+ #b1; #b2; #H;
+ nchange with (match AST_TYPE_STRUCT b2 with [ AST_TYPE_STRUCT a ⇒ b1 = a | _ ⇒ False ]);
+ nrewrite < H;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+ndefinition asttype_destruct_aux ≝
+Πb1,b2:ast_type.ΠP:Prop.b1 = b2 →
+ match eq_asttype b1 b2 with [ true ⇒ P → P | false ⇒ P ].
+
+ndefinition asttype_destruct : asttype_destruct_aux.
+ #b1; #b2; #P; #H;
+ nrewrite > H;
+ napply (ast_type_index … b2);
+ ##[ ##1: #e; nchange with (match eqc ? e e with [ true ⇒ P → P | false ⇒ P ]);
+ nrewrite > (eq_to_eqc ? e e (refl_eq …));
+ nnormalize; napply (λx.x);
+ ##| ##2: #e; #n; #H; nchange with (match (eq_asttype e e)⊗(eqc ? n n) with [ true ⇒ P → P | false ⇒ P]);
+ nrewrite > (eq_to_eqc ? n n (refl_eq …));
+ nrewrite > (symmetric_andbool (eq_asttype e e) true);
+ nchange with (match eq_asttype e e with [ true ⇒ P → P | false ⇒ P]);
+ napply H;
+ ##| ##3: #e; #H; nchange with (match eq_asttype e e with [ true ⇒ P → P | false ⇒ P]);
+ napply H;
+ ##| ##4: #hh; #tt; #H;
+ nchange with (match bfold_right_neList2 ?? tt tt with [ true ⇒ P → P | false ⇒ P ] →
+ match (eq_asttype hh hh)⊗(bfold_right_neList2 ?? tt tt) with [ true ⇒ P → P | false ⇒ P ]);
+ #H1;
+ ncases (eq_asttype hh hh) in H:(%) ⊢ %; #H;
+ ncases (bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) tt tt) in H1:(%) ⊢ %; #H1;
+ ##[ ##1: nnormalize; napply (λx.x);
+ ##| ##3: nnormalize in H:(%) ⊢ %; napply H
+ ##| ##*: nnormalize in H1:(%) ⊢ %; napply H1
+ ##]
+ ##]
+nqed.
+
+nlemma eq_to_eqasttype_aux1
+ : ∀nl1,nl2.
+ ((eq_asttype (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = true) →
+ ((bfold_right_neList2 ? (λx,y.eq_asttype x y) nl1 nl2) = true).
+ #nl1; #nl2; #H;
+ napply H.
+nqed.
+
+nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_asttype t1 t2 = true.
+ #t1;
+ napply (ast_type_index … t1);
+ ##[ ##1: #b1; #t2; ncases t2;
+ ##[ ##1: #b2; #H; nrewrite > (asttype_destruct_base_base … H);
+ nchange with ((eqc ? b2 b2) = true);
+ nrewrite > (eq_to_eqc ? b2 b2 (refl_eq …));
+ napply refl_eq
+ ##| ##2: #st2; #n2; #H; ndestruct (*napply (asttype_destruct … H)*)
+ ##| ##3: #nl2; #H; ndestruct (*napply (asttype_destruct … H)*)
+ ##]
+ ##| ##2: #st1; #n1; #H; #t2; ncases t2;
+ ##[ ##2: #st2; #n2; #H1; nchange with (((eq_asttype st1 st2)⊗(eqc ? n1 n2)) = true);
+ nrewrite > (H st2 (asttype_destruct_array_array_1 … H1));
+ nrewrite > (eq_to_eqc ? n1 n2 (asttype_destruct_array_array_2 … H1));
+ nnormalize;
+ napply refl_eq
+ ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
+ ##| ##3: #nl2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
+ ##]
+ ##| ##3: #hh1; #H; #t2; ncases t2;
+ ##[ ##3: #nl2; ncases nl2;
+ ##[ ##1: #hh2; #H1; nchange with ((eq_asttype hh1 hh2) = true);
+ nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct … H1)));
+ napply refl_eq
+ ##| ##2: #hh2; #ll2; #H1;
+ (* !!! ndestruct non va *)
+ nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct … H1))
+ ##]
+ ##| ##1: #b2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
+ ##| ##2: #st2; #n2; #H1; ndestruct (*napply (asttype_destruct … H1)*)
+ ##]
+ ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
+ ##[ ##3: #nl2; ncases nl2;
+ ##[ ##1: #hh2; #H2;
+ (* !!! ndestruct non va *)
+ nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct … H2))
+ ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
+ nrewrite > (H hh2 (nelist_destruct_cons_cons_1 … (asttype_destruct_struct_struct … H2)));
+ nrewrite > (eq_to_eqasttype_aux1 ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) ?));
+ ##[ ##1: nnormalize; napply refl_eq
+ ##| ##2: nrewrite > (nelist_destruct_cons_cons_2 … (asttype_destruct_struct_struct … H2));
+ napply refl_eq
+ ##]
+ ##]
+ ##| ##1: #b2; #H2; ndestruct (*napply (asttype_destruct … H2)*)
+ ##| ##2: #st2; #n2; #H2; ndestruct (*napply (asttype_destruct … H2)*)
+ ##]
+ ##]
+nqed.
+
+nlemma neqasttype_to_neq : ∀n1,n2.eq_asttype n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_asttype n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqasttype n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
+nlemma eqasttype_to_eq : ∀t1,t2.eq_asttype t1 t2 = true → t1 = t2.
+ #t1;
+ napply (ast_type_index … t1);
+ ##[ ##1: #b1; #t2; ncases t2;
+ ##[ ##1: #b2; #H; nchange in H:(%) with ((eqc ? b1 b2) = true);
+ nrewrite > (eqc_to_eq ? b1 b2 H);
+ napply refl_eq
+ ##| ##2: #st2; #n2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##3: #nl2; nnormalize; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##]
+ ##| ##2: #st1; #n1; #H; #t2; ncases t2;
+ ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_asttype st1 st2)⊗(eqc ? n1 n2)) = true);
+ nrewrite > (H st2 (andb_true_true_l … H1));
+ nrewrite > (eqc_to_eq ? n1 n2 (andb_true_true_r … H1));
+ napply refl_eq
+ ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##3: #nl2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##]
+ ##| ##3: #hh1; #H; #t2; ncases t2;
+ ##[ ##3: #nl2; ncases nl2;
+ ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_asttype hh1 hh2) = true);
+ nrewrite > (H hh2 H1);
+ napply refl_eq
+ ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##]
+ ##| ##1: #b2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##| ##2: #st2; #n2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
+ ##]
+ ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2;
+ ##[ ##3: #nl2; ncases nl2;
+ ##[ ##1: #hh2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
+ ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_asttype hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_asttype x y) ll1 ll2)) = true);
+ nrewrite > (H hh2 (andb_true_true_l … H2));
+ nrewrite > (asttype_destruct_struct_struct ll1 ll2 (H1 (AST_TYPE_STRUCT ll2) (andb_true_true_r … H2)));
+ napply refl_eq
+ ##]
+ ##| ##1: #b2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
+ ##| ##2: #st2; #n2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
+ ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqasttype : ∀n1,n2.n1 ≠ n2 → eq_asttype n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_asttype n1 n2));
+ napply (not_to_not (eq_asttype n1 n2 = true) (n1 = n2) ? H);
+ napply (eqasttype_to_eq n1 n2).
+nqed.
+
+nlemma decidable_asttype : ∀x,y:ast_type.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_asttype x y = true) (eq_asttype x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqasttype_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqasttype_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqasttype : symmetricT ast_type bool eq_asttype.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_asttype n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqasttype n1 n2 H);
+ napply (symmetric_eq ? (eq_asttype n2 n1) false);
+ napply (neq_to_neqasttype n2 n1 (symmetric_neq ? n1 n2 H))
+ ##]
+nqed.
+
+nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast.
+ #ast;
+ ncases ast;
+ nnormalize;
+ ##[ ##1: #t; #H; napply I
+ ##| ##2: #t; #n; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##3: #t; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##]
+nqed.
+
+nlemma isntbastbasetype_to_isntastbasetype : ∀ast.isntb_ast_base_type ast = true → isnt_ast_base_type ast.
+ #ast;
+ ncases ast;
+ nnormalize;
+ ##[ ##1: #t; #H; ndestruct (*napply (bool_destruct … H)*)
+ ##| ##2: #t; #n; #H; napply I
+ ##| ##3: #l; #H; napply I
+ ##]
+nqed.
+
+nlemma asttype_is_comparable : comparable.
+ @ ast_type
+ ##[ napply (AST_TYPE_BASE AST_BASE_TYPE_BYTE8)
+ ##| napply (λx.false)
+ ##| napply eq_asttype
+ ##| napply eqasttype_to_eq
+ ##| napply eq_to_eqasttype
+ ##| napply neqasttype_to_neq
+ ##| napply neq_to_neqasttype
+ ##| napply decidable_asttype
+ ##| napply symmetric_eqasttype
+ ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr asttype_is_comparable ≡ ast_type.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "compiler/ast_base_type.ma".
+include "common/nelist.ma".
+
+(* ************************* *)
+(* dimensioni degli elementi *)
+(* ************************* *)
+
+ninductive ast_type : Type ≝
+ AST_TYPE_BASE: ast_base_type → ast_type
+| AST_TYPE_ARRAY: ast_type → nat → ast_type
+| AST_TYPE_STRUCT: ne_list ast_type → ast_type.
+
+(* principio di eliminazione arricchito *)
+nlet rec ast_type_index_aux (P:ast_type → Prop)
+ (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (f2:Πt.P t)
+ (t:ne_list ast_type) on t ≝
+ match t return λt.P (AST_TYPE_STRUCT t) with
+ [ ne_nil h ⇒ f h (f2 h)
+ | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_index_aux P f f1 f2 t)
+ ].
+
+nlet rec ast_type_index (P:ast_type → Prop)
+ (f:Πb.P (AST_TYPE_BASE b))
+ (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
+ (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (t:ast_type) on t : P t ≝
+ match t return λt.P t with
+ [ AST_TYPE_BASE b ⇒ f b
+ | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_index P f f1 f2 f3 t')
+ | AST_TYPE_STRUCT nl ⇒ match nl with
+ [ ne_nil h ⇒ f2 h (ast_type_index P f f1 f2 f3 h)
+ | ne_cons h t ⇒ f3 h t (ast_type_index P f f1 f2 f3 h) (ast_type_index_aux P f2 f3 (ast_type_index P f f1 f2 f3) t)
+ ]
+ ].
+
+nlet rec ast_type_rectex_aux (P:ast_type → Type)
+ (f:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f1:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (f2:Πt.P t)
+ (t:ne_list ast_type) on t ≝
+ match t return λt.P (AST_TYPE_STRUCT t) with
+ [ ne_nil h ⇒ f h (f2 h)
+ | ne_cons h t ⇒ f1 h t (f2 h) (ast_type_rectex_aux P f f1 f2 t)
+ ].
+
+nlet rec ast_type_rectex (P:ast_type → Type)
+ (f:Πb.P (AST_TYPE_BASE b))
+ (f1:Πt,n.P t → P (AST_TYPE_ARRAY t n))
+ (f2:Πt.P t → P (AST_TYPE_STRUCT (ne_nil ? t)))
+ (f3:Πh,t.P h → P (AST_TYPE_STRUCT t) → P (AST_TYPE_STRUCT (ne_cons ? h t)))
+ (t:ast_type) on t : P t ≝
+ match t return λt.P t with
+ [ AST_TYPE_BASE b ⇒ f b
+ | AST_TYPE_ARRAY t' n ⇒ f1 t' n (ast_type_rectex P f f1 f2 f3 t')
+ | AST_TYPE_STRUCT nl ⇒ match nl with
+ [ ne_nil h ⇒ f2 h (ast_type_rectex P f f1 f2 f3 h)
+ | ne_cons h t ⇒ f3 h t (ast_type_rectex P f f1 f2 f3 h) (ast_type_rectex_aux P f2 f3 (ast_type_rectex P f f1 f2 f3) t)
+ ]
+ ].
+
+nlet rec eq_asttype (t1,t2:ast_type) on t1 ≝
+ match t1 with
+ [ AST_TYPE_BASE bType1 ⇒ match t2 with
+ [ AST_TYPE_BASE bType2 ⇒ eqc ? bType1 bType2
+ | _ ⇒ false ]
+ | AST_TYPE_ARRAY subType1 dim1 ⇒ match t2 with
+ [ AST_TYPE_ARRAY subType2 dim2 ⇒ (eq_asttype subType1 subType2) ⊗ (eqc ? dim1 dim2)
+ | _ ⇒ false ]
+ | AST_TYPE_STRUCT nelSubType1 ⇒ match t2 with
+ [ AST_TYPE_STRUCT nelSubType2 ⇒ bfold_right_neList2 ? (λx1,x2.eq_asttype x1 x2) nelSubType1 nelSubType2
+ | _ ⇒ false
+ ]
+ ].
+
+ndefinition is_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ True | _ ⇒ False ].
+
+ndefinition isb_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ true | _ ⇒ false ].
+
+ndefinition isnt_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ False | _ ⇒ True ].
+
+ndefinition isntb_ast_base_type ≝
+λast:ast_type.match ast with [ AST_TYPE_BASE _ ⇒ false | _ ⇒ true ].
+
+ndefinition eval_size_base_type ≝
+λast:ast_base_type.match ast with
+ [ AST_BASE_TYPE_BYTE8 ⇒ nat1
+ | AST_BASE_TYPE_WORD16 ⇒ nat2
+ | AST_BASE_TYPE_WORD32 ⇒ nat4
+ ].
+
+nlet rec eval_size_type (ast:ast_type) on ast ≝
+ match ast with
+ [ AST_TYPE_BASE b ⇒ eval_size_base_type b
+ | AST_TYPE_ARRAY sub_ast dim ⇒ (dim + nat1)*(eval_size_type sub_ast)
+ | AST_TYPE_STRUCT nel_ast ⇒ fold_right_neList … (λt,x.(eval_size_type t)+x) O nel_ast
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/string.ma".
+include "compiler/ast_type.ma".
+
+(* ***************** *)
+(* GESTIONE AMBIENTE *)
+(* ***************** *)
+
+(* elemento: name + const + type *)
+nrecord envDsc : Type ≝
+ {
+ nameDsc: aux_str_type;
+ constDsc: bool;
+ typeDsc: ast_type
+ }.
+
+(* ambiente globale: (ambiente base + ambienti annidati) *)
+ninductive env_list : nat → Type ≝
+ env_nil: list envDsc → env_list O
+| env_cons: ∀n.list envDsc → env_list n → env_list (S n).
+
+ndefinition defined_envList ≝
+λd.λl:env_list d.match l with [ env_nil _ ⇒ False | env_cons _ _ _ ⇒ True ].
+
+(* bisogna bypassare la carenza di inversion *)
+nlemma defined_envList_S : ∀d.∀l:env_list (S d).defined_envList (S d) l.
+ #d; #l;
+ ngeneralize in match (refl_eq ? (S d));
+ ncases l in ⊢ (? ? % ? → %);
+ ##[ ##1: #dsc; #H; ndestruct (*nelim (nat_destruct_0_S … H)*)
+ ##| ##2: #n; #dsc; #sub; #H;
+ nnormalize;
+ napply I
+ ##]
+nqed.
+
+ndefinition cut_first_envList_aux : Πd.env_list (S d) → env_list d ≝
+λd.λl:env_list (S d).
+ match l
+ return λX.λY:env_list X.defined_envList X Y → env_list (pred X)
+ with
+ [ env_nil h ⇒ λp:defined_envList O (env_nil h).False_rect_Type0 ? p
+ | env_cons n h t ⇒ λp:defined_envList (S n) (env_cons n h t).t
+ ] (defined_envList_S d l).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "common/string.ma".
+include "compiler/ast_type.ma".
+include "num/word32.ma".
+
+(* ****************** *)
+(* PREALBERO DI TOKEN *)
+(* ****************** *)
+
+(* espressioni *)
+ninductive preast_expr : Type ≝
+ PREAST_EXPR_BYTE8 : byte8 → preast_expr
+| PREAST_EXPR_WORD16: word16 → preast_expr
+| PREAST_EXPR_WORD32: word32 → preast_expr
+
+| PREAST_EXPR_NEG: preast_expr → preast_expr
+| PREAST_EXPR_NOT: preast_expr → preast_expr
+| PREAST_EXPR_COM: preast_expr → preast_expr
+
+| PREAST_EXPR_ADD: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_SUB: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_MUL: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_DIV: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_SHR: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_SHL: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_AND: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_OR: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_XOR: preast_expr → preast_expr → preast_expr
+
+| PREAST_EXPR_GT : preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_GTE: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_LT : preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_LTE: preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_EQ : preast_expr → preast_expr → preast_expr
+| PREAST_EXPR_NEQ: preast_expr → preast_expr → preast_expr
+
+| PREAST_EXPR_B8toW16 : preast_expr → preast_expr
+| PREAST_EXPR_B8toW32 : preast_expr → preast_expr
+| PREAST_EXPR_W16toB8 : preast_expr → preast_expr
+| PREAST_EXPR_W16toW32: preast_expr → preast_expr
+| PREAST_EXPR_W32toB8 : preast_expr → preast_expr
+| PREAST_EXPR_W32toW16: preast_expr → preast_expr
+
+| PREAST_EXPR_ID: preast_var → preast_expr
+
+(* variabile: modificatori di array/struct dell'id *)
+with preast_var : Type ≝
+ PREAST_VAR_ID: aux_str_type → preast_var
+| PREAST_VAR_ARRAY: preast_var → preast_expr → preast_var
+| PREAST_VAR_STRUCT: preast_var → nat → preast_var.
+
+(* -------------------------- *)
+
+(* inizializzatori: ... valori ... *)
+ninductive preast_init_val : Type ≝
+ PREAST_INIT_VAL_BYTE8: byte8 → preast_init_val
+| PREAST_INIT_VAL_WORD16: word16 → preast_init_val
+| PREAST_INIT_VAL_WORD32: word32 → preast_init_val
+| PREAST_INIT_VAL_ARRAY: ne_list preast_init_val → preast_init_val
+| PREAST_INIT_VAL_STRUCT: ne_list preast_init_val → preast_init_val.
+
+(*
+ inizializzatori: ammesse solo due forme, no ibridi
+ 1) var1 = var2
+ 2) var = ... valori ...
+*)
+ninductive preast_init : Type ≝
+ PREAST_INIT_VAR: preast_var → preast_init
+| PREAST_INIT_VAL: preast_init_val → preast_init.
+
+(* -------------------------- *)
+
+(* statement: assegnamento/while/if else if else *)
+ninductive preast_stm : Type ≝
+ PREAST_STM_ASG: preast_var → preast_expr → preast_stm
+| PREAST_STM_WHILE: preast_expr → preast_decl → preast_stm
+| PREAST_STM_IF: ne_list (ProdT preast_expr preast_decl) → option preast_decl → preast_stm
+
+(* dichiarazioni *)
+with preast_decl : Type ≝
+ PREAST_NO_DECL: list preast_stm → preast_decl
+| PREAST_CONST_DECL: aux_str_type → ast_type → preast_init → preast_decl → preast_decl
+| PREAST_VAR_DECL: aux_str_type → ast_type → option preast_init → preast_decl → preast_decl.
+
+(* -------------------------- *)
+
+(* programma *)
+ninductive preast_root : Type ≝
+ PREAST_ROOT: preast_decl → preast_root.
+
+(* -------------------------- *)
+
+(* programma vuoto *)
+ndefinition empty_preast_prog ≝ PREAST_ROOT (PREAST_NO_DECL (nil ?)).
-common/nat.ma common/comp.ma num/bool_lemmas.ma
+compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma
num/word32.ma num/word16.ma
+common/nat.ma common/comp.ma num/bool_lemmas.ma
common/ascii_base.ma num/bool.ma
+emulator/opcodes/HCS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma
num/bitrigesim.ma common/comp.ma num/bool_lemmas.ma
+emulator/opcodes/HC05_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma
+emulator/opcodes/byte_or_word.ma num/word16.ma
+emulator/opcodes/Freescale_pseudo_base.ma num/bool.ma
common/pts.ma
+compiler/ast_type_base.ma common/nelist.ma compiler/ast_base_type.ma
common/prod.ma common/comp.ma common/prod_base.ma num/bool_lemmas.ma
common/prod_base.ma num/bool.ma
universe/universe.ma common/nelist.ma common/prod.ma
num/bool_lemmas.ma num/bool.ma
-common/comp.ma common/hints_declaration.ma num/bool.ma
+emulator/opcodes/Freescale_instr_mode.ma common/comp.ma emulator/opcodes/Freescale_instr_mode_base.ma num/bool_lemmas.ma
num/exadecim.ma num/bool_lemmas.ma num/comp_ext.ma num/oct.ma
+common/comp.ma common/hints_declaration.ma num/bool.ma
num/word24.ma num/byte8.ma
+emulator/opcodes/IP2022_pseudo.ma common/comp.ma emulator/opcodes/IP2022_pseudo_base.ma num/bool_lemmas.ma
common/theory.ma common/pts.ma
+emulator/opcodes/Freescale_pseudo.ma common/comp.ma emulator/opcodes/Freescale_pseudo_base.ma num/bool_lemmas.ma
+emulator/opcodes/HC08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma
+emulator/opcodes/Freescale_instr_mode_base.ma num/bitrigesim.ma num/exadecim.ma
+emulator/opcodes/RS08_table.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/byte_or_word.ma
common/sigma.ma common/theory.ma
num/oct.ma common/comp.ma num/bool_lemmas.ma
-common/hints_declaration.ma common/pts.ma
+compiler/ast_base_type.ma common/comp.ma compiler/ast_base_type_base.ma num/bool_lemmas.ma
num/byte8.ma num/bitrigesim.ma num/comp_num.ma num/exadecim.ma
+common/hints_declaration.ma common/pts.ma
common/option.ma common/comp.ma common/option_base.ma num/bool_lemmas.ma
num/bool.ma common/theory.ma
common/option_base.ma num/bool.ma
+emulator/opcodes/IP2022_instr_mode_base.ma num/bitrigesim.ma num/oct.ma
+compiler/ast_base_type_base.ma num/bool.ma
num/word16.ma common/nat.ma num/byte8.ma
-common/string.ma common/ascii.ma common/list.ma
+compiler/environment.ma common/string.ma compiler/ast_type.ma
common/ascii.ma common/ascii_base.ma common/comp.ma num/bool_lemmas.ma
+emulator/opcodes/pseudo.ma common/list.ma emulator/opcodes/Freescale_instr_mode.ma emulator/opcodes/Freescale_pseudo.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
+common/string.ma common/ascii.ma common/list.ma
common/list.ma common/comp.ma common/nat.ma common/option.ma
+compiler/ast_type.ma compiler/ast_type_base.ma
num/comp_num.ma num/bool_lemmas.ma num/comp_ext.ma
+emulator/opcodes/IP2022_table.ma common/list.ma emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_pseudo.ma emulator/opcodes/byte_or_word.ma
num/comp_ext.ma common/comp.ma common/prod.ma
+emulator/opcodes/IP2022_instr_mode.ma emulator/opcodes/IP2022_instr_mode_base.ma
common/nelist.ma common/list.ma
+emulator/opcodes/IP2022_pseudo_base.ma num/bool.ma
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_instr_mode_base.ma".
+include "common/comp.ma".
+include "num/bool_lemmas.ma".
+
+nlemma eq_to_eqFreescaleim :
+∀n1,n2.n1 = n2 → eq_Freescale_im n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
+ ##[ ##31,32: #o; nrewrite > (eq_to_eqc … (refl_eq …))
+ ##| ##33: #e; nrewrite > (eq_to_eqc … (refl_eq …))
+ ##| ##34: #t; nrewrite > (eq_to_eqc … (refl_eq …)) ##]
+ napply refl_eq.
+nqed.
+
+nlemma neqFreescaleim_to_neq : ∀n1,n2.eq_Freescale_im n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_Freescale_im n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqFreescaleim n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
+(* !!! per brevita... *)
+naxiom eqFreescaleim_to_eq : ∀c1,c2.eq_Freescale_im c1 c2 = true → c1 = c2.
+
+nlemma neq_to_neqFreescaleim : ∀n1,n2.n1 ≠ n2 → eq_Freescale_im n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_Freescale_im n1 n2));
+ napply (not_to_not (eq_Freescale_im n1 n2 = true) (n1 = n2) ? H);
+ napply (eqFreescaleim_to_eq n1 n2).
+nqed.
+
+nlemma decidable_Freescaleim : ∀x,y:Freescale_instr_mode.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_Freescale_im x y = true) (eq_Freescale_im x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqFreescaleim_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqFreescaleim_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqFreescaleim : symmetricT Freescale_instr_mode bool eq_Freescale_im.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_Freescaleim n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqFreescaleim n1 n2 H);
+ napply (symmetric_eq ? (eq_Freescale_im n2 n1) false);
+ napply (neq_to_neqFreescaleim n2 n1 (symmetric_neq ? n1 n2 H))
+ ##]
+nqed.
+
+nlemma Freescaleim_is_comparable : comparable.
+ @ Freescale_instr_mode
+ ##[ napply MODE_INH
+ ##| napply forall_Freescale_im
+ ##| napply eq_Freescale_im
+ ##| napply eqFreescaleim_to_eq
+ ##| napply eq_to_eqFreescaleim
+ ##| napply neqFreescaleim_to_neq
+ ##| napply neq_to_neqFreescaleim
+ ##| napply decidable_Freescaleim
+ ##| napply symmetric_eqFreescaleim
+ ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr Freescaleim_is_comparable ≡ Freescale_instr_mode.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/exadecim.ma".
+include "num/bitrigesim.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+(* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
+ninductive Freescale_instr_mode: Type ≝
+ (* INHERENT = nessun operando *)
+ MODE_INH : Freescale_instr_mode
+ (* INHERENT = nessun operando (A implicito) *)
+| MODE_INHA : Freescale_instr_mode
+ (* INHERENT = nessun operando (X implicito) *)
+| MODE_INHX : Freescale_instr_mode
+ (* INHERENT = nessun operando (H implicito) *)
+| MODE_INHH : Freescale_instr_mode
+
+ (* INHERENT_ADDRESS = nessun operando (HX implicito) *)
+| MODE_INHX0ADD : Freescale_instr_mode
+ (* INHERENT_ADDRESS = nessun operando (HX implicito+0x00bb) *)
+| MODE_INHX1ADD : Freescale_instr_mode
+ (* INHERENT_ADDRESS = nessun operando (HX implicito+0xwwww) *)
+| MODE_INHX2ADD : Freescale_instr_mode
+
+ (* IMMEDIATE = operando valore immediato byte = 0xbb *)
+| MODE_IMM1 : Freescale_instr_mode
+ (* IMMEDIATE_EXT = operando valore immediato byte = 0xbb -> esteso a word *)
+| MODE_IMM1EXT : Freescale_instr_mode
+ (* IMMEDIATE = operando valore immediato word = 0xwwww *)
+| MODE_IMM2 : Freescale_instr_mode
+ (* DIRECT = operando offset byte = [0x00bb] *)
+| MODE_DIR1 : Freescale_instr_mode
+ (* DIRECT = operando offset word = [0xwwww] *)
+| MODE_DIR2 : Freescale_instr_mode
+ (* INDEXED = nessun operando (implicito [X] *)
+| MODE_IX0 : Freescale_instr_mode
+ (* INDEXED = operando offset relativo byte = [X+0x00bb] *)
+| MODE_IX1 : Freescale_instr_mode
+ (* INDEXED = operando offset relativo word = [X+0xwwww] *)
+| MODE_IX2 : Freescale_instr_mode
+ (* INDEXED = operando offset relativo byte = [SP+0x00bb] *)
+| MODE_SP1 : Freescale_instr_mode
+ (* INDEXED = operando offset relativo word = [SP+0xwwww] *)
+| MODE_SP2 : Freescale_instr_mode
+
+ (* DIRECT → DIRECT = carica da diretto/scrive su diretto *)
+| MODE_DIR1_to_DIR1 : Freescale_instr_mode
+ (* IMMEDIATE → DIRECT = carica da immediato/scrive su diretto *)
+| MODE_IMM1_to_DIR1 : Freescale_instr_mode
+ (* INDEXED++ → DIRECT = carica da [X]/scrive su diretto/H:X++ *)
+| MODE_IX0p_to_DIR1 : Freescale_instr_mode
+ (* DIRECT → INDEXED++ = carica da diretto/scrive su [X]/H:X++ *)
+| MODE_DIR1_to_IX0p : Freescale_instr_mode
+
+ (* INHERENT(A) + IMMEDIATE *)
+| MODE_INHA_and_IMM1 : Freescale_instr_mode
+ (* INHERENT(X) + IMMEDIATE *)
+| MODE_INHX_and_IMM1 : Freescale_instr_mode
+ (* IMMEDIATE + IMMEDIATE *)
+| MODE_IMM1_and_IMM1 : Freescale_instr_mode
+ (* DIRECT + IMMEDIATE *)
+| MODE_DIR1_and_IMM1 : Freescale_instr_mode
+ (* INDEXED + IMMEDIATE *)
+| MODE_IX0_and_IMM1 : Freescale_instr_mode
+ (* INDEXED++ + IMMEDIATE *)
+| MODE_IX0p_and_IMM1 : Freescale_instr_mode
+ (* INDEXED + IMMEDIATE *)
+| MODE_IX1_and_IMM1 : Freescale_instr_mode
+ (* INDEXED++ + IMMEDIATE *)
+| MODE_IX1p_and_IMM1 : Freescale_instr_mode
+ (* INDEXED + IMMEDIATE *)
+| MODE_SP1_and_IMM1 : Freescale_instr_mode
+
+ (* DIRECT(mTNY) = operando offset byte(maschera scrittura implicita 3 bit) *)
+ (* ex: DIR3 e' carica b, scrivi b con n-simo bit modificato *)
+| MODE_DIRn : oct → Freescale_instr_mode
+ (* DIRECT(mTNY) + IMMEDIATE = operando offset byte(maschera lettura implicita 3 bit) *)
+ (* + operando valore immediato byte *)
+ (* ex: DIR2_and_IMM1 e' carica b, carica imm, restituisci n-simo bit di b + imm *)
+| MODE_DIRn_and_IMM1 : oct → Freescale_instr_mode
+ (* TINY = nessun operando (diretto implicito 4bit = [0x00000000:0000iiii]) *)
+| MODE_TNY : exadecim → Freescale_instr_mode
+ (* SHORT = nessun operando (diretto implicito 5bit = [0x00000000:000iiiii]) *)
+| MODE_SRT : bitrigesim → Freescale_instr_mode
+.
+
+ndefinition eq_Freescale_im ≝
+λi1,i2:Freescale_instr_mode.
+ match i1 with
+ [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+ | MODE_INHA ⇒ match i2 with [ MODE_INHA ⇒ true | _ ⇒ false ]
+ | MODE_INHX ⇒ match i2 with [ MODE_INHX ⇒ true | _ ⇒ false ]
+ | MODE_INHH ⇒ match i2 with [ MODE_INHH ⇒ true | _ ⇒ false ]
+ | MODE_INHX0ADD ⇒ match i2 with [ MODE_INHX0ADD ⇒ true | _ ⇒ false ]
+ | MODE_INHX1ADD ⇒ match i2 with [ MODE_INHX1ADD ⇒ true | _ ⇒ false ]
+ | MODE_INHX2ADD ⇒ match i2 with [ MODE_INHX2ADD ⇒ true | _ ⇒ false ]
+ | MODE_IMM1 ⇒ match i2 with [ MODE_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IMM1EXT ⇒ match i2 with [ MODE_IMM1EXT ⇒ true | _ ⇒ false ]
+ | MODE_IMM2 ⇒ match i2 with [ MODE_IMM2 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1 ⇒ match i2 with [ MODE_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_DIR2 ⇒ match i2 with [ MODE_DIR2 ⇒ true | _ ⇒ false ]
+ | MODE_IX0 ⇒ match i2 with [ MODE_IX0 ⇒ true | _ ⇒ false ]
+ | MODE_IX1 ⇒ match i2 with [ MODE_IX1 ⇒ true | _ ⇒ false ]
+ | MODE_IX2 ⇒ match i2 with [ MODE_IX2 ⇒ true | _ ⇒ false ]
+ | MODE_SP1 ⇒ match i2 with [ MODE_SP1 ⇒ true | _ ⇒ false ]
+ | MODE_SP2 ⇒ match i2 with [ MODE_SP2 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1_to_DIR1 ⇒ match i2 with [ MODE_DIR1_to_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_IMM1_to_DIR1 ⇒ match i2 with [ MODE_IMM1_to_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_IX0p_to_DIR1 ⇒ match i2 with [ MODE_IX0p_to_DIR1 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1_to_IX0p ⇒ match i2 with [ MODE_DIR1_to_IX0p ⇒ true | _ ⇒ false ]
+ | MODE_INHA_and_IMM1 ⇒ match i2 with [ MODE_INHA_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_INHX_and_IMM1 ⇒ match i2 with [ MODE_INHX_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IMM1_and_IMM1 ⇒ match i2 with [ MODE_IMM1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_DIR1_and_IMM1 ⇒ match i2 with [ MODE_DIR1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX0_and_IMM1 ⇒ match i2 with [ MODE_IX0_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX0p_and_IMM1 ⇒ match i2 with [ MODE_IX0p_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX1_and_IMM1 ⇒ match i2 with [ MODE_IX1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_IX1p_and_IMM1 ⇒ match i2 with [ MODE_IX1p_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_SP1_and_IMM1 ⇒ match i2 with [ MODE_SP1_and_IMM1 ⇒ true | _ ⇒ false ]
+ | MODE_DIRn n1 ⇒ match i2 with [ MODE_DIRn n2 ⇒ eqc ? n1 n2 | _ ⇒ false ]
+ | MODE_DIRn_and_IMM1 n1 ⇒ match i2 with [ MODE_DIRn_and_IMM1 n2 ⇒ eqc ? n1 n2 | _ ⇒ false ]
+ | MODE_TNY e1 ⇒ match i2 with [ MODE_TNY e2 ⇒ eqc ? e1 e2 | _ ⇒ false ]
+ | MODE_SRT t1 ⇒ match i2 with [ MODE_SRT t2 ⇒ eqc ? t1 t2 | _ ⇒ false ]
+ ].
+
+ndefinition forall_Freescale_im ≝ λP:Freescale_instr_mode → bool.
+ P MODE_INH
+⊗ P MODE_INHA
+⊗ P MODE_INHX
+⊗ P MODE_INHH
+
+⊗ P MODE_INHX0ADD
+⊗ P MODE_INHX1ADD
+⊗ P MODE_INHX2ADD
+
+⊗ P MODE_IMM1
+⊗ P MODE_IMM1EXT
+⊗ P MODE_IMM2
+⊗ P MODE_DIR1
+⊗ P MODE_DIR2
+⊗ P MODE_IX0
+⊗ P MODE_IX1
+⊗ P MODE_IX2
+⊗ P MODE_SP1
+⊗ P MODE_SP2
+
+⊗ P MODE_DIR1_to_DIR1
+⊗ P MODE_IMM1_to_DIR1
+⊗ P MODE_IX0p_to_DIR1
+⊗ P MODE_DIR1_to_IX0p
+
+⊗ P MODE_INHA_and_IMM1
+⊗ P MODE_INHX_and_IMM1
+⊗ P MODE_IMM1_and_IMM1
+⊗ P MODE_DIR1_and_IMM1
+⊗ P MODE_IX0_and_IMM1
+⊗ P MODE_IX0p_and_IMM1
+⊗ P MODE_IX1_and_IMM1
+⊗ P MODE_IX1p_and_IMM1
+⊗ P MODE_SP1_and_IMM1
+
+⊗ forallc ? (λo. P (MODE_DIRn o))
+⊗ forallc ? (λo. P (MODE_DIRn_and_IMM1 o))
+⊗ forallc ? (λe. P (MODE_TNY e))
+⊗ forallc ? (λt. P (MODE_SRT t)).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_pseudo_base.ma".
+include "common/comp.ma".
+include "num/bool_lemmas.ma".
+
+nlemma eq_to_eqFreescalepseudo : ∀n1,n2.n1 = n2 → eq_Freescale_pseudo n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma neqFreescalepseudo_to_neq : ∀n1,n2.eq_Freescale_pseudo n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_Freescale_pseudo n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqFreescalepseudo n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
+(* !!! per brevita... *)
+naxiom eqFreescalepseudo_to_eq : ∀c1,c2.eq_Freescale_pseudo c1 c2 = true → c1 = c2.
+
+nlemma neq_to_neqFreescalepseudo : ∀n1,n2.n1 ≠ n2 → eq_Freescale_pseudo n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_Freescale_pseudo n1 n2));
+ napply (not_to_not (eq_Freescale_pseudo n1 n2 = true) (n1 = n2) ? H);
+ napply (eqFreescalepseudo_to_eq n1 n2).
+nqed.
+
+nlemma decidable_Freescalepseudo : ∀x,y:Freescale_pseudo.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_Freescale_pseudo x y = true) (eq_Freescale_pseudo x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqFreescalepseudo_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqFreescalepseudo_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqFreescalepseudo : symmetricT Freescale_pseudo bool eq_Freescale_pseudo.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_Freescalepseudo n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqFreescalepseudo n1 n2 H);
+ napply (symmetric_eq ? (eq_Freescale_pseudo n2 n1) false);
+ napply (neq_to_neqFreescalepseudo n2 n1 (symmetric_neq ? n1 n2 H))
+ ##]
+nqed.
+
+nlemma Freescalepseudo_is_comparable : comparable.
+ @ Freescale_pseudo
+ ##[ napply ADC
+ ##| napply forall_Freescale_pseudo
+ ##| napply eq_Freescale_pseudo
+ ##| napply eqFreescalepseudo_to_eq
+ ##| napply eq_to_eqFreescalepseudo
+ ##| napply neqFreescalepseudo_to_neq
+ ##| napply neq_to_neqFreescalepseudo
+ ##| napply decidable_Freescalepseudo
+ ##| napply symmetric_eqFreescalepseudo
+ ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr Freescalepseudo_is_comparable ≡ Freescale_pseudo.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+(* enumerazione delle istruzioni *)
+ninductive Freescale_pseudo: Type ≝
+ ADC : Freescale_pseudo (* add with carry *)
+| ADD : Freescale_pseudo (* add *)
+| AIS : Freescale_pseudo (* add immediate to SP *)
+| AIX : Freescale_pseudo (* add immediate to X *)
+| AND : Freescale_pseudo (* and *)
+| ASL : Freescale_pseudo (* aritmetic shift left *)
+| ASR : Freescale_pseudo (* aritmetic shift right *)
+| BCC : Freescale_pseudo (* branch if C=0 *)
+| BCLRn : Freescale_pseudo (* clear bit n *)
+| BCS : Freescale_pseudo (* branch if C=1 *)
+| BEQ : Freescale_pseudo (* branch if Z=1 *)
+| BGE : Freescale_pseudo (* branch if N⊙V=0 (great or equal) *)
+| BGND : Freescale_pseudo (* !!background mode!! *)
+| BGT : Freescale_pseudo (* branch if Z|N⊙V=0 clear (great) *)
+| BHCC : Freescale_pseudo (* branch if H=0 *)
+| BHCS : Freescale_pseudo (* branch if H=1 *)
+| BHI : Freescale_pseudo (* branch if C|Z=0, (higher) *)
+| BIH : Freescale_pseudo (* branch if nIRQ=1 *)
+| BIL : Freescale_pseudo (* branch if nIRQ=0 *)
+| BIT : Freescale_pseudo (* flag = and (bit test) *)
+| BLE : Freescale_pseudo (* branch if Z|N⊙V=1 (less or equal) *)
+| BLS : Freescale_pseudo (* branch if C|Z=1 (lower or same) *)
+| BLT : Freescale_pseudo (* branch if N⊙1=1 (less) *)
+| BMC : Freescale_pseudo (* branch if I=0 (interrupt mask clear) *)
+| BMI : Freescale_pseudo (* branch if N=1 (minus) *)
+| BMS : Freescale_pseudo (* branch if I=1 (interrupt mask set) *)
+| BNE : Freescale_pseudo (* branch if Z=0 *)
+| BPL : Freescale_pseudo (* branch if N=0 (plus) *)
+| BRA : Freescale_pseudo (* branch always *)
+| BRCLRn : Freescale_pseudo (* branch if bit n clear *)
+| BRN : Freescale_pseudo (* branch never (nop) *)
+| BRSETn : Freescale_pseudo (* branch if bit n set *)
+| BSETn : Freescale_pseudo (* set bit n *)
+| BSR : Freescale_pseudo (* branch to subroutine *)
+| CBEQA : Freescale_pseudo (* compare (A) and BEQ *)
+| CBEQX : Freescale_pseudo (* compare (X) and BEQ *)
+| CLC : Freescale_pseudo (* C=0 *)
+| CLI : Freescale_pseudo (* I=0 *)
+| CLR : Freescale_pseudo (* operand=0 *)
+| CMP : Freescale_pseudo (* flag = sub (compare A) *)
+| COM : Freescale_pseudo (* not (1 complement) *)
+| CPHX : Freescale_pseudo (* flag = sub (compare H:X) *)
+| CPX : Freescale_pseudo (* flag = sub (compare X) *)
+| DAA : Freescale_pseudo (* decimal adjust A *)
+| DBNZ : Freescale_pseudo (* dec and BNE *)
+| DEC : Freescale_pseudo (* operand=operand-1 (decrement) *)
+| DIV : Freescale_pseudo (* div *)
+| EOR : Freescale_pseudo (* xor *)
+| INC : Freescale_pseudo (* operand=operand+1 (increment) *)
+| JMP : Freescale_pseudo (* jmp word [operand] *)
+| JSR : Freescale_pseudo (* jmp to subroutine *)
+| LDA : Freescale_pseudo (* load in A *)
+| LDHX : Freescale_pseudo (* load in H:X *)
+| LDX : Freescale_pseudo (* load in X *)
+| LSR : Freescale_pseudo (* logical shift right *)
+| MOV : Freescale_pseudo (* move *)
+| MUL : Freescale_pseudo (* mul *)
+| NEG : Freescale_pseudo (* neg (2 complement) *)
+| NOP : Freescale_pseudo (* nop *)
+| NSA : Freescale_pseudo (* nibble swap A (al:ah <- ah:al) *)
+| ORA : Freescale_pseudo (* or *)
+| PSHA : Freescale_pseudo (* push A *)
+| PSHH : Freescale_pseudo (* push H *)
+| PSHX : Freescale_pseudo (* push X *)
+| PULA : Freescale_pseudo (* pop A *)
+| PULH : Freescale_pseudo (* pop H *)
+| PULX : Freescale_pseudo (* pop X *)
+| ROL : Freescale_pseudo (* rotate left *)
+| ROR : Freescale_pseudo (* rotate right *)
+| RSP : Freescale_pseudo (* reset SP (0x00FF) *)
+| RTI : Freescale_pseudo (* return from interrupt *)
+| RTS : Freescale_pseudo (* return from subroutine *)
+| SBC : Freescale_pseudo (* sub with carry*)
+| SEC : Freescale_pseudo (* C=1 *)
+| SEI : Freescale_pseudo (* I=1 *)
+| SHA : Freescale_pseudo (* swap spc_high,A *)
+| SLA : Freescale_pseudo (* swap spc_low,A *)
+| STA : Freescale_pseudo (* store from A *)
+| STHX : Freescale_pseudo (* store from H:X *)
+| STOP : Freescale_pseudo (* !!stop mode!! *)
+| STX : Freescale_pseudo (* store from X *)
+| SUB : Freescale_pseudo (* sub *)
+| SWI : Freescale_pseudo (* software interrupt *)
+| TAP : Freescale_pseudo (* flag=A (transfer A to process status byte *)
+| TAX : Freescale_pseudo (* X=A (transfer A to X) *)
+| TPA : Freescale_pseudo (* A=flag (transfer process status byte to A) *)
+| TST : Freescale_pseudo (* flag = sub (test) *)
+| TSX : Freescale_pseudo (* X:H=SP (transfer SP to H:X) *)
+| TXA : Freescale_pseudo (* A=X (transfer X to A) *)
+| TXS : Freescale_pseudo (* SP=X:H (transfer H:X to SP) *)
+| WAIT : Freescale_pseudo (* !!wait mode!! *)
+.
+
+ndefinition eq_Freescale_pseudo ≝
+λps1,ps2:Freescale_pseudo.
+ match ps1 with
+ [ ADC ⇒ match ps2 with [ ADC ⇒ true | _ ⇒ false ] | ADD ⇒ match ps2 with [ ADD ⇒ true | _ ⇒ false ]
+ | AIS ⇒ match ps2 with [ AIS ⇒ true | _ ⇒ false ] | AIX ⇒ match ps2 with [ AIX ⇒ true | _ ⇒ false ]
+ | AND ⇒ match ps2 with [ AND ⇒ true | _ ⇒ false ] | ASL ⇒ match ps2 with [ ASL ⇒ true | _ ⇒ false ]
+ | ASR ⇒ match ps2 with [ ASR ⇒ true | _ ⇒ false ] | BCC ⇒ match ps2 with [ BCC ⇒ true | _ ⇒ false ]
+ | BCLRn ⇒ match ps2 with [ BCLRn ⇒ true | _ ⇒ false ] | BCS ⇒ match ps2 with [ BCS ⇒ true | _ ⇒ false ]
+ | BEQ ⇒ match ps2 with [ BEQ ⇒ true | _ ⇒ false ] | BGE ⇒ match ps2 with [ BGE ⇒ true | _ ⇒ false ]
+ | BGND ⇒ match ps2 with [ BGND ⇒ true | _ ⇒ false ] | BGT ⇒ match ps2 with [ BGT ⇒ true | _ ⇒ false ]
+ | BHCC ⇒ match ps2 with [ BHCC ⇒ true | _ ⇒ false ] | BHCS ⇒ match ps2 with [ BHCS ⇒ true | _ ⇒ false ]
+ | BHI ⇒ match ps2 with [ BHI ⇒ true | _ ⇒ false ] | BIH ⇒ match ps2 with [ BIH ⇒ true | _ ⇒ false ]
+ | BIL ⇒ match ps2 with [ BIL ⇒ true | _ ⇒ false ] | BIT ⇒ match ps2 with [ BIT ⇒ true | _ ⇒ false ]
+ | BLE ⇒ match ps2 with [ BLE ⇒ true | _ ⇒ false ] | BLS ⇒ match ps2 with [ BLS ⇒ true | _ ⇒ false ]
+ | BLT ⇒ match ps2 with [ BLT ⇒ true | _ ⇒ false ] | BMC ⇒ match ps2 with [ BMC ⇒ true | _ ⇒ false ]
+ | BMI ⇒ match ps2 with [ BMI ⇒ true | _ ⇒ false ] | BMS ⇒ match ps2 with [ BMS ⇒ true | _ ⇒ false ]
+ | BNE ⇒ match ps2 with [ BNE ⇒ true | _ ⇒ false ] | BPL ⇒ match ps2 with [ BPL ⇒ true | _ ⇒ false ]
+ | BRA ⇒ match ps2 with [ BRA ⇒ true | _ ⇒ false ] | BRCLRn ⇒ match ps2 with [ BRCLRn ⇒ true | _ ⇒ false ]
+ | BRN ⇒ match ps2 with [ BRN ⇒ true | _ ⇒ false ] | BRSETn ⇒ match ps2 with [ BRSETn ⇒ true | _ ⇒ false ]
+ | BSETn ⇒ match ps2 with [ BSETn ⇒ true | _ ⇒ false ] | BSR ⇒ match ps2 with [ BSR ⇒ true | _ ⇒ false ]
+ | CBEQA ⇒ match ps2 with [ CBEQA ⇒ true | _ ⇒ false ] | CBEQX ⇒ match ps2 with [ CBEQX ⇒ true | _ ⇒ false ]
+ | CLC ⇒ match ps2 with [ CLC ⇒ true | _ ⇒ false ] | CLI ⇒ match ps2 with [ CLI ⇒ true | _ ⇒ false ]
+ | CLR ⇒ match ps2 with [ CLR ⇒ true | _ ⇒ false ] | CMP ⇒ match ps2 with [ CMP ⇒ true | _ ⇒ false ]
+ | COM ⇒ match ps2 with [ COM ⇒ true | _ ⇒ false ] | CPHX ⇒ match ps2 with [ CPHX ⇒ true | _ ⇒ false ]
+ | CPX ⇒ match ps2 with [ CPX ⇒ true | _ ⇒ false ] | DAA ⇒ match ps2 with [ DAA ⇒ true | _ ⇒ false ]
+ | DBNZ ⇒ match ps2 with [ DBNZ ⇒ true | _ ⇒ false ] | DEC ⇒ match ps2 with [ DEC ⇒ true | _ ⇒ false ]
+ | DIV ⇒ match ps2 with [ DIV ⇒ true | _ ⇒ false ] | EOR ⇒ match ps2 with [ EOR ⇒ true | _ ⇒ false ]
+ | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ] | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ]
+ | JSR ⇒ match ps2 with [ JSR ⇒ true | _ ⇒ false ] | LDA ⇒ match ps2 with [ LDA ⇒ true | _ ⇒ false ]
+ | LDHX ⇒ match ps2 with [ LDHX ⇒ true | _ ⇒ false ] | LDX ⇒ match ps2 with [ LDX ⇒ true | _ ⇒ false ]
+ | LSR ⇒ match ps2 with [ LSR ⇒ true | _ ⇒ false ] | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
+ | MUL ⇒ match ps2 with [ MUL ⇒ true | _ ⇒ false ] | NEG ⇒ match ps2 with [ NEG ⇒ true | _ ⇒ false ]
+ | NOP ⇒ match ps2 with [ NOP ⇒ true | _ ⇒ false ] | NSA ⇒ match ps2 with [ NSA ⇒ true | _ ⇒ false ]
+ | ORA ⇒ match ps2 with [ ORA ⇒ true | _ ⇒ false ] | PSHA ⇒ match ps2 with [ PSHA ⇒ true | _ ⇒ false ]
+ | PSHH ⇒ match ps2 with [ PSHH ⇒ true | _ ⇒ false ] | PSHX ⇒ match ps2 with [ PSHX ⇒ true | _ ⇒ false ]
+ | PULA ⇒ match ps2 with [ PULA ⇒ true | _ ⇒ false ] | PULH ⇒ match ps2 with [ PULH ⇒ true | _ ⇒ false ]
+ | PULX ⇒ match ps2 with [ PULX ⇒ true | _ ⇒ false ] | ROL ⇒ match ps2 with [ ROL ⇒ true | _ ⇒ false ]
+ | ROR ⇒ match ps2 with [ ROR ⇒ true | _ ⇒ false ] | RSP ⇒ match ps2 with [ RSP ⇒ true | _ ⇒ false ]
+ | RTI ⇒ match ps2 with [ RTI ⇒ true | _ ⇒ false ] | RTS ⇒ match ps2 with [ RTS ⇒ true | _ ⇒ false ]
+ | SBC ⇒ match ps2 with [ SBC ⇒ true | _ ⇒ false ] | SEC ⇒ match ps2 with [ SEC ⇒ true | _ ⇒ false ]
+ | SEI ⇒ match ps2 with [ SEI ⇒ true | _ ⇒ false ] | SHA ⇒ match ps2 with [ SHA ⇒ true | _ ⇒ false ]
+ | SLA ⇒ match ps2 with [ SLA ⇒ true | _ ⇒ false ] | STA ⇒ match ps2 with [ STA ⇒ true | _ ⇒ false ]
+ | STHX ⇒ match ps2 with [ STHX ⇒ true | _ ⇒ false ] | STOP ⇒ match ps2 with [ STOP ⇒ true | _ ⇒ false ]
+ | STX ⇒ match ps2 with [ STX ⇒ true | _ ⇒ false ] | SUB ⇒ match ps2 with [ SUB ⇒ true | _ ⇒ false ]
+ | SWI ⇒ match ps2 with [ SWI ⇒ true | _ ⇒ false ] | TAP ⇒ match ps2 with [ TAP ⇒ true | _ ⇒ false ]
+ | TAX ⇒ match ps2 with [ TAX ⇒ true | _ ⇒ false ] | TPA ⇒ match ps2 with [ TPA ⇒ true | _ ⇒ false ]
+ | TST ⇒ match ps2 with [ TST ⇒ true | _ ⇒ false ] | TSX ⇒ match ps2 with [ TSX ⇒ true | _ ⇒ false ]
+ | TXA ⇒ match ps2 with [ TXA ⇒ true | _ ⇒ false ] | TXS ⇒ match ps2 with [ TXS ⇒ true | _ ⇒ false ]
+ | WAIT ⇒ match ps2 with [ WAIT ⇒ true | _ ⇒ false ]
+ ].
+
+ndefinition forall_Freescale_pseudo ≝ λP:Freescale_pseudo → bool.
+ P ADC ⊗ P ADD ⊗ P AIS ⊗ P AIX ⊗ P AND ⊗ P ASL ⊗ P ASR ⊗ P BCC ⊗
+ P BCLRn ⊗ P BCS ⊗ P BEQ ⊗ P BGE ⊗ P BGND ⊗ P BGT ⊗ P BHCC ⊗ P BHCS ⊗
+ P BHI ⊗ P BIH ⊗ P BIL ⊗ P BIT ⊗ P BLE ⊗ P BLS ⊗ P BLT ⊗ P BMC ⊗
+ P BMI ⊗ P BMS ⊗ P BNE ⊗ P BPL ⊗ P BRA ⊗ P BRCLRn ⊗ P BRN ⊗ P BRSETn ⊗
+ P BSETn ⊗ P BSR ⊗ P CBEQA ⊗ P CBEQX ⊗ P CLC ⊗ P CLI ⊗ P CLR ⊗ P CMP ⊗
+ P COM ⊗ P CPHX ⊗ P CPX ⊗ P DAA ⊗ P DBNZ ⊗ P DEC ⊗ P DIV ⊗ P EOR ⊗
+ P INC ⊗ P JMP ⊗ P JSR ⊗ P LDA ⊗ P LDHX ⊗ P LDX ⊗ P LSR ⊗ P MOV ⊗
+ P MUL ⊗ P NEG ⊗ P NOP ⊗ P NSA ⊗ P ORA ⊗ P PSHA ⊗ P PSHH ⊗ P PSHX ⊗
+ P PULA ⊗ P PULH ⊗ P PULX ⊗ P ROL ⊗ P ROR ⊗ P RSP ⊗ P RTI ⊗ P RTS ⊗
+ P SBC ⊗ P SEC ⊗ P SEI ⊗ P SHA ⊗ P SLA ⊗ P STA ⊗ P STHX ⊗ P STOP ⊗
+ P STX ⊗ P SUB ⊗ P SWI ⊗ P TAP ⊗ P TAX ⊗ P TPA ⊗ P TST ⊗ P TSX ⊗
+ P TXA ⊗ P TXS ⊗ P WAIT.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_pseudo.ma".
+include "emulator/opcodes/Freescale_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ***************** *)
+(* TABELLA DELL'HC05 *)
+(* ***************** *)
+
+(* definizione come concatenazione finale di liste per velocizzare il parsing *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
+
+ndefinition opcode_table_HC05_1 ≝
+[
+ quadruple … ADC MODE_IMM1 (Byte 〈xA,x9〉) 〈x0,x2〉
+; quadruple … ADC MODE_DIR1 (Byte 〈xB,x9〉) 〈x0,x3〉
+; quadruple … ADC MODE_DIR2 (Byte 〈xC,x9〉) 〈x0,x4〉
+; quadruple … ADC MODE_IX2 (Byte 〈xD,x9〉) 〈x0,x5〉
+; quadruple … ADC MODE_IX1 (Byte 〈xE,x9〉) 〈x0,x4〉
+; quadruple … ADC MODE_IX0 (Byte 〈xF,x9〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC05_2 ≝
+[
+ quadruple … ADD MODE_IMM1 (Byte 〈xA,xB〉) 〈x0,x2〉
+; quadruple … ADD MODE_DIR1 (Byte 〈xB,xB〉) 〈x0,x3〉
+; quadruple … ADD MODE_DIR2 (Byte 〈xC,xB〉) 〈x0,x4〉
+; quadruple … ADD MODE_IX2 (Byte 〈xD,xB〉) 〈x0,x5〉
+; quadruple … ADD MODE_IX1 (Byte 〈xE,xB〉) 〈x0,x4〉
+; quadruple … ADD MODE_IX0 (Byte 〈xF,xB〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_3 ≝
+[
+ quadruple … AND MODE_IMM1 (Byte 〈xA,x4〉) 〈x0,x2〉
+; quadruple … AND MODE_DIR1 (Byte 〈xB,x4〉) 〈x0,x3〉
+; quadruple … AND MODE_DIR2 (Byte 〈xC,x4〉) 〈x0,x4〉
+; quadruple … AND MODE_IX2 (Byte 〈xD,x4〉) 〈x0,x5〉
+; quadruple … AND MODE_IX1 (Byte 〈xE,x4〉) 〈x0,x4〉
+; quadruple … AND MODE_IX0 (Byte 〈xF,x4〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_4 ≝
+[
+ quadruple … ASL MODE_DIR1 (Byte 〈x3,x8〉) 〈x0,x5〉
+; quadruple … ASL MODE_INHA (Byte 〈x4,x8〉) 〈x0,x3〉
+; quadruple … ASL MODE_INHX (Byte 〈x5,x8〉) 〈x0,x3〉
+; quadruple … ASL MODE_IX1 (Byte 〈x6,x8〉) 〈x0,x6〉
+; quadruple … ASL MODE_IX0 (Byte 〈x7,x8〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_5 ≝
+[
+ quadruple … ASR MODE_DIR1 (Byte 〈x3,x7〉) 〈x0,x5〉
+; quadruple … ASR MODE_INHA (Byte 〈x4,x7〉) 〈x0,x3〉
+; quadruple … ASR MODE_INHX (Byte 〈x5,x7〉) 〈x0,x3〉
+; quadruple … ASR MODE_IX1 (Byte 〈x6,x7〉) 〈x0,x6〉
+; quadruple … ASR MODE_IX0 (Byte 〈x7,x7〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_6 ≝
+[
+ quadruple … BRA MODE_IMM1 (Byte 〈x2,x0〉) 〈x0,x3〉
+; quadruple … BRN MODE_IMM1 (Byte 〈x2,x1〉) 〈x0,x3〉
+; quadruple … BHI MODE_IMM1 (Byte 〈x2,x2〉) 〈x0,x3〉
+; quadruple … BLS MODE_IMM1 (Byte 〈x2,x3〉) 〈x0,x3〉
+; quadruple … BCC MODE_IMM1 (Byte 〈x2,x4〉) 〈x0,x3〉
+; quadruple … BCS MODE_IMM1 (Byte 〈x2,x5〉) 〈x0,x3〉
+; quadruple … BNE MODE_IMM1 (Byte 〈x2,x6〉) 〈x0,x3〉
+; quadruple … BEQ MODE_IMM1 (Byte 〈x2,x7〉) 〈x0,x3〉
+; quadruple … BHCC MODE_IMM1 (Byte 〈x2,x8〉) 〈x0,x3〉
+; quadruple … BHCS MODE_IMM1 (Byte 〈x2,x9〉) 〈x0,x3〉
+; quadruple … BPL MODE_IMM1 (Byte 〈x2,xA〉) 〈x0,x3〉
+; quadruple … BMI MODE_IMM1 (Byte 〈x2,xB〉) 〈x0,x3〉
+; quadruple … BMC MODE_IMM1 (Byte 〈x2,xC〉) 〈x0,x3〉
+; quadruple … BMS MODE_IMM1 (Byte 〈x2,xD〉) 〈x0,x3〉
+; quadruple … BIL MODE_IMM1 (Byte 〈x2,xE〉) 〈x0,x3〉
+; quadruple … BIH MODE_IMM1 (Byte 〈x2,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_7 ≝
+[
+ quadruple … BSETn (MODE_DIRn o0) (Byte 〈x1,x0〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o0) (Byte 〈x1,x1〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o1) (Byte 〈x1,x2〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o1) (Byte 〈x1,x3〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o2) (Byte 〈x1,x4〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o2) (Byte 〈x1,x5〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o3) (Byte 〈x1,x6〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o3) (Byte 〈x1,x7〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o4) (Byte 〈x1,x8〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o4) (Byte 〈x1,x9〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o5) (Byte 〈x1,xA〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o5) (Byte 〈x1,xB〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o6) (Byte 〈x1,xC〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o6) (Byte 〈x1,xD〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o7) (Byte 〈x1,xE〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o7) (Byte 〈x1,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_8 ≝
+[
+ quadruple … BRSETn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x0〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x1〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x2〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x3〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x4〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x5〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x6〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x7〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x8〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x9〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xA〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xB〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xC〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xD〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xE〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_9 ≝
+[
+ quadruple … BIT MODE_IMM1 (Byte 〈xA,x5〉) 〈x0,x2〉
+; quadruple … BIT MODE_DIR1 (Byte 〈xB,x5〉) 〈x0,x3〉
+; quadruple … BIT MODE_DIR2 (Byte 〈xC,x5〉) 〈x0,x4〉
+; quadruple … BIT MODE_IX2 (Byte 〈xD,x5〉) 〈x0,x5〉
+; quadruple … BIT MODE_IX1 (Byte 〈xE,x5〉) 〈x0,x4〉
+; quadruple … BIT MODE_IX0 (Byte 〈xF,x5〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_10 ≝
+[
+ quadruple … MUL MODE_INH (Byte 〈x4,x2〉) 〈x0,xB〉
+; quadruple … RTI MODE_INH (Byte 〈x8,x0〉) 〈x0,x9〉
+; quadruple … RTS MODE_INH (Byte 〈x8,x1〉) 〈x0,x6〉
+; quadruple … SWI MODE_INH (Byte 〈x8,x3〉) 〈x0,xA〉
+; quadruple … STOP MODE_INH (Byte 〈x8,xE〉) 〈x0,x2〉
+; quadruple … WAIT MODE_INH (Byte 〈x8,xF〉) 〈x0,x2〉
+; quadruple … TAX MODE_INH (Byte 〈x9,x7〉) 〈x0,x2〉
+; quadruple … CLC MODE_INH (Byte 〈x9,x8〉) 〈x0,x2〉
+; quadruple … SEC MODE_INH (Byte 〈x9,x9〉) 〈x0,x2〉
+; quadruple … CLI MODE_INH (Byte 〈x9,xA〉) 〈x0,x2〉
+; quadruple … SEI MODE_INH (Byte 〈x9,xB〉) 〈x0,x2〉
+; quadruple … RSP MODE_INH (Byte 〈x9,xC〉) 〈x0,x2〉
+; quadruple … NOP MODE_INH (Byte 〈x9,xD〉) 〈x0,x2〉
+; quadruple … TXA MODE_INH (Byte 〈x9,xF〉) 〈x0,x2〉
+].
+
+ndefinition opcode_table_HC05_11 ≝
+[
+ quadruple … CLR MODE_DIR1 (Byte 〈x3,xF〉) 〈x0,x5〉
+; quadruple … CLR MODE_INHA (Byte 〈x4,xF〉) 〈x0,x3〉
+; quadruple … CLR MODE_INHX (Byte 〈x5,xF〉) 〈x0,x3〉
+; quadruple … CLR MODE_IX1 (Byte 〈x6,xF〉) 〈x0,x6〉
+; quadruple … CLR MODE_IX0 (Byte 〈x7,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_12 ≝
+[
+ quadruple … CMP MODE_IMM1 (Byte 〈xA,x1〉) 〈x0,x2〉
+; quadruple … CMP MODE_DIR1 (Byte 〈xB,x1〉) 〈x0,x3〉
+; quadruple … CMP MODE_DIR2 (Byte 〈xC,x1〉) 〈x0,x4〉
+; quadruple … CMP MODE_IX2 (Byte 〈xD,x1〉) 〈x0,x5〉
+; quadruple … CMP MODE_IX1 (Byte 〈xE,x1〉) 〈x0,x4〉
+; quadruple … CMP MODE_IX0 (Byte 〈xF,x1〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_13 ≝
+[
+ quadruple … COM MODE_DIR1 (Byte 〈x3,x3〉) 〈x0,x5〉
+; quadruple … COM MODE_INHA (Byte 〈x4,x3〉) 〈x0,x3〉
+; quadruple … COM MODE_INHX (Byte 〈x5,x3〉) 〈x0,x3〉
+; quadruple … COM MODE_IX1 (Byte 〈x6,x3〉) 〈x0,x6〉
+; quadruple … COM MODE_IX0 (Byte 〈x7,x3〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_14 ≝
+[
+ quadruple … CPX MODE_IMM1 (Byte 〈xA,x3〉) 〈x0,x2〉
+; quadruple … CPX MODE_DIR1 (Byte 〈xB,x3〉) 〈x0,x3〉
+; quadruple … CPX MODE_DIR2 (Byte 〈xC,x3〉) 〈x0,x4〉
+; quadruple … CPX MODE_IX2 (Byte 〈xD,x3〉) 〈x0,x5〉
+; quadruple … CPX MODE_IX1 (Byte 〈xE,x3〉) 〈x0,x4〉
+; quadruple … CPX MODE_IX0 (Byte 〈xF,x3〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_15 ≝
+[
+ quadruple … DEC MODE_DIR1 (Byte 〈x3,xA〉) 〈x0,x5〉
+; quadruple … DEC MODE_INHA (Byte 〈x4,xA〉) 〈x0,x3〉
+; quadruple … DEC MODE_INHX (Byte 〈x5,xA〉) 〈x0,x3〉
+; quadruple … DEC MODE_IX1 (Byte 〈x6,xA〉) 〈x0,x6〉
+; quadruple … DEC MODE_IX0 (Byte 〈x7,xA〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_16 ≝
+[
+ quadruple … EOR MODE_IMM1 (Byte 〈xA,x8〉) 〈x0,x2〉
+; quadruple … EOR MODE_DIR1 (Byte 〈xB,x8〉) 〈x0,x3〉
+; quadruple … EOR MODE_DIR2 (Byte 〈xC,x8〉) 〈x0,x4〉
+; quadruple … EOR MODE_IX2 (Byte 〈xD,x8〉) 〈x0,x5〉
+; quadruple … EOR MODE_IX1 (Byte 〈xE,x8〉) 〈x0,x4〉
+; quadruple … EOR MODE_IX0 (Byte 〈xF,x8〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_17 ≝
+[
+ quadruple … INC MODE_DIR1 (Byte 〈x3,xC〉) 〈x0,x5〉
+; quadruple … INC MODE_INHA (Byte 〈x4,xC〉) 〈x0,x3〉
+; quadruple … INC MODE_INHX (Byte 〈x5,xC〉) 〈x0,x3〉
+; quadruple … INC MODE_IX1 (Byte 〈x6,xC〉) 〈x0,x6〉
+; quadruple … INC MODE_IX0 (Byte 〈x7,xC〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_18 ≝
+[
+ quadruple … JMP MODE_IMM1EXT (Byte 〈xB,xC〉) 〈x0,x2〉
+; quadruple … JMP MODE_IMM2 (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadruple … JMP MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadruple … JMP MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadruple … JMP MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x2〉
+].
+
+ndefinition opcode_table_HC05_19 ≝
+[
+ quadruple … BSR MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x6〉
+; quadruple … JSR MODE_IMM1EXT (Byte 〈xB,xD〉) 〈x0,x5〉
+; quadruple … JSR MODE_IMM2 (Byte 〈xC,xD〉) 〈x0,x6〉
+; quadruple … JSR MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x7〉
+; quadruple … JSR MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x6〉
+; quadruple … JSR MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_20 ≝
+[
+ quadruple … LDA MODE_IMM1 (Byte 〈xA,x6〉) 〈x0,x2〉
+; quadruple … LDA MODE_DIR1 (Byte 〈xB,x6〉) 〈x0,x3〉
+; quadruple … LDA MODE_DIR2 (Byte 〈xC,x6〉) 〈x0,x4〉
+; quadruple … LDA MODE_IX2 (Byte 〈xD,x6〉) 〈x0,x5〉
+; quadruple … LDA MODE_IX1 (Byte 〈xE,x6〉) 〈x0,x4〉
+; quadruple … LDA MODE_IX0 (Byte 〈xF,x6〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_21 ≝
+[
+ quadruple … LDX MODE_IMM1 (Byte 〈xA,xE〉) 〈x0,x2〉
+; quadruple … LDX MODE_DIR1 (Byte 〈xB,xE〉) 〈x0,x3〉
+; quadruple … LDX MODE_DIR2 (Byte 〈xC,xE〉) 〈x0,x4〉
+; quadruple … LDX MODE_IX2 (Byte 〈xD,xE〉) 〈x0,x5〉
+; quadruple … LDX MODE_IX1 (Byte 〈xE,xE〉) 〈x0,x4〉
+; quadruple … LDX MODE_IX0 (Byte 〈xF,xE〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_22 ≝
+[
+ quadruple … LSR MODE_DIR1 (Byte 〈x3,x4〉) 〈x0,x5〉
+; quadruple … LSR MODE_INHA (Byte 〈x4,x4〉) 〈x0,x3〉
+; quadruple … LSR MODE_INHX (Byte 〈x5,x4〉) 〈x0,x3〉
+; quadruple … LSR MODE_IX1 (Byte 〈x6,x4〉) 〈x0,x6〉
+; quadruple … LSR MODE_IX0 (Byte 〈x7,x4〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_23 ≝
+[
+ quadruple … NEG MODE_DIR1 (Byte 〈x3,x0〉) 〈x0,x5〉
+; quadruple … NEG MODE_INHA (Byte 〈x4,x0〉) 〈x0,x3〉
+; quadruple … NEG MODE_INHX (Byte 〈x5,x0〉) 〈x0,x3〉
+; quadruple … NEG MODE_IX1 (Byte 〈x6,x0〉) 〈x0,x6〉
+; quadruple … NEG MODE_IX0 (Byte 〈x7,x0〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_24 ≝
+[
+ quadruple … ORA MODE_IMM1 (Byte 〈xA,xA〉) 〈x0,x2〉
+; quadruple … ORA MODE_DIR1 (Byte 〈xB,xA〉) 〈x0,x3〉
+; quadruple … ORA MODE_DIR2 (Byte 〈xC,xA〉) 〈x0,x4〉
+; quadruple … ORA MODE_IX2 (Byte 〈xD,xA〉) 〈x0,x5〉
+; quadruple … ORA MODE_IX1 (Byte 〈xE,xA〉) 〈x0,x4〉
+; quadruple … ORA MODE_IX0 (Byte 〈xF,xA〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_25 ≝
+[
+ quadruple … ROL MODE_DIR1 (Byte 〈x3,x9〉) 〈x0,x5〉
+; quadruple … ROL MODE_INHA (Byte 〈x4,x9〉) 〈x0,x3〉
+; quadruple … ROL MODE_INHX (Byte 〈x5,x9〉) 〈x0,x3〉
+; quadruple … ROL MODE_IX1 (Byte 〈x6,x9〉) 〈x0,x6〉
+; quadruple … ROL MODE_IX0 (Byte 〈x7,x9〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_26 ≝
+[
+ quadruple … ROR MODE_DIR1 (Byte 〈x3,x6〉) 〈x0,x5〉
+; quadruple … ROR MODE_INHA (Byte 〈x4,x6〉) 〈x0,x3〉
+; quadruple … ROR MODE_INHX (Byte 〈x5,x6〉) 〈x0,x3〉
+; quadruple … ROR MODE_IX1 (Byte 〈x6,x6〉) 〈x0,x6〉
+; quadruple … ROR MODE_IX0 (Byte 〈x7,x6〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC05_27 ≝
+[
+ quadruple … SBC MODE_IMM1 (Byte 〈xA,x2〉) 〈x0,x2〉
+; quadruple … SBC MODE_DIR1 (Byte 〈xB,x2〉) 〈x0,x3〉
+; quadruple … SBC MODE_DIR2 (Byte 〈xC,x2〉) 〈x0,x4〉
+; quadruple … SBC MODE_IX2 (Byte 〈xD,x2〉) 〈x0,x5〉
+; quadruple … SBC MODE_IX1 (Byte 〈xE,x2〉) 〈x0,x4〉
+; quadruple … SBC MODE_IX0 (Byte 〈xF,x2〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_28 ≝
+[
+ quadruple … STA MODE_DIR1 (Byte 〈xB,x7〉) 〈x0,x4〉
+; quadruple … STA MODE_DIR2 (Byte 〈xC,x7〉) 〈x0,x5〉
+; quadruple … STA MODE_IX2 (Byte 〈xD,x7〉) 〈x0,x6〉
+; quadruple … STA MODE_IX1 (Byte 〈xE,x7〉) 〈x0,x5〉
+; quadruple … STA MODE_IX0 (Byte 〈xF,x7〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC05_29 ≝
+[
+ quadruple … STX MODE_DIR1 (Byte 〈xB,xF〉) 〈x0,x4〉
+; quadruple … STX MODE_DIR2 (Byte 〈xC,xF〉) 〈x0,x5〉
+; quadruple … STX MODE_IX2 (Byte 〈xD,xF〉) 〈x0,x6〉
+; quadruple … STX MODE_IX1 (Byte 〈xE,xF〉) 〈x0,x5〉
+; quadruple … STX MODE_IX0 (Byte 〈xF,xF〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC05_30 ≝
+[
+ quadruple … SUB MODE_IMM1 (Byte 〈xA,x0〉) 〈x0,x2〉
+; quadruple … SUB MODE_DIR1 (Byte 〈xB,x0〉) 〈x0,x3〉
+; quadruple … SUB MODE_DIR2 (Byte 〈xC,x0〉) 〈x0,x4〉
+; quadruple … SUB MODE_IX2 (Byte 〈xD,x0〉) 〈x0,x5〉
+; quadruple … SUB MODE_IX1 (Byte 〈xE,x0〉) 〈x0,x4〉
+; quadruple … SUB MODE_IX0 (Byte 〈xF,x0〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC05_31 ≝
+[
+ quadruple … TST MODE_DIR1 (Byte 〈x3,xD〉) 〈x0,x4〉
+; quadruple … TST MODE_INHA (Byte 〈x4,xD〉) 〈x0,x3〉
+; quadruple … TST MODE_INHX (Byte 〈x5,xD〉) 〈x0,x3〉
+; quadruple … TST MODE_IX1 (Byte 〈x6,xD〉) 〈x0,x5〉
+; quadruple … TST MODE_IX0 (Byte 〈x7,xD〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC05 ≝
+ opcode_table_HC05_1 @ opcode_table_HC05_2 @ opcode_table_HC05_3 @ opcode_table_HC05_4 @
+ opcode_table_HC05_5 @ opcode_table_HC05_6 @ opcode_table_HC05_7 @ opcode_table_HC05_8 @
+ opcode_table_HC05_9 @ opcode_table_HC05_10 @ opcode_table_HC05_11 @ opcode_table_HC05_12 @
+ opcode_table_HC05_13 @ opcode_table_HC05_14 @ opcode_table_HC05_15 @ opcode_table_HC05_16 @
+ opcode_table_HC05_17 @ opcode_table_HC05_18 @ opcode_table_HC05_19 @ opcode_table_HC05_20 @
+ opcode_table_HC05_21 @ opcode_table_HC05_22 @ opcode_table_HC05_23 @ opcode_table_HC05_24 @
+ opcode_table_HC05_25 @ opcode_table_HC05_26 @ opcode_table_HC05_27 @ opcode_table_HC05_28 @
+ opcode_table_HC05_29 @ opcode_table_HC05_30 @ opcode_table_HC05_31.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_pseudo.ma".
+include "emulator/opcodes/Freescale_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ***************** *)
+(* TABELLA DELL'HC08 *)
+(* ***************** *)
+
+(* definizione come concatenazione finale di liste per velocizzare il parsing *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
+
+ndefinition opcode_table_HC08_1 ≝
+[
+ quadruple … ADC MODE_IMM1 (Byte 〈xA,x9〉) 〈x0,x2〉
+; quadruple … ADC MODE_DIR1 (Byte 〈xB,x9〉) 〈x0,x3〉
+; quadruple … ADC MODE_DIR2 (Byte 〈xC,x9〉) 〈x0,x4〉
+; quadruple … ADC MODE_IX2 (Byte 〈xD,x9〉) 〈x0,x4〉
+; quadruple … ADC MODE_IX1 (Byte 〈xE,x9〉) 〈x0,x3〉
+; quadruple … ADC MODE_IX0 (Byte 〈xF,x9〉) 〈x0,x2〉
+; quadruple … ADC MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x9〉〉) 〈x0,x5〉
+; quadruple … ADC MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x9〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_2 ≝
+[
+ quadruple … ADD MODE_IMM1 (Byte 〈xA,xB〉) 〈x0,x2〉
+; quadruple … ADD MODE_DIR1 (Byte 〈xB,xB〉) 〈x0,x3〉
+; quadruple … ADD MODE_DIR2 (Byte 〈xC,xB〉) 〈x0,x4〉
+; quadruple … ADD MODE_IX2 (Byte 〈xD,xB〉) 〈x0,x4〉
+; quadruple … ADD MODE_IX1 (Byte 〈xE,xB〉) 〈x0,x3〉
+; quadruple … ADD MODE_IX0 (Byte 〈xF,xB〉) 〈x0,x2〉
+; quadruple … ADD MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xB〉〉) 〈x0,x5〉
+; quadruple … ADD MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xB〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_3 ≝
+[
+ quadruple … AND MODE_IMM1 (Byte 〈xA,x4〉) 〈x0,x2〉
+; quadruple … AND MODE_DIR1 (Byte 〈xB,x4〉) 〈x0,x3〉
+; quadruple … AND MODE_DIR2 (Byte 〈xC,x4〉) 〈x0,x4〉
+; quadruple … AND MODE_IX2 (Byte 〈xD,x4〉) 〈x0,x4〉
+; quadruple … AND MODE_IX1 (Byte 〈xE,x4〉) 〈x0,x3〉
+; quadruple … AND MODE_IX0 (Byte 〈xF,x4〉) 〈x0,x2〉
+; quadruple … AND MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x4〉〉) 〈x0,x5〉
+; quadruple … AND MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x4〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_4 ≝
+[
+ quadruple … ASL MODE_DIR1 (Byte 〈x3,x8〉) 〈x0,x4〉
+; quadruple … ASL MODE_INHA (Byte 〈x4,x8〉) 〈x0,x1〉
+; quadruple … ASL MODE_INHX (Byte 〈x5,x8〉) 〈x0,x1〉
+; quadruple … ASL MODE_IX1 (Byte 〈x6,x8〉) 〈x0,x4〉
+; quadruple … ASL MODE_IX0 (Byte 〈x7,x8〉) 〈x0,x3〉
+; quadruple … ASL MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x8〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_5 ≝
+[
+ quadruple … ASR MODE_DIR1 (Byte 〈x3,x7〉) 〈x0,x4〉
+; quadruple … ASR MODE_INHA (Byte 〈x4,x7〉) 〈x0,x1〉
+; quadruple … ASR MODE_INHX (Byte 〈x5,x7〉) 〈x0,x1〉
+; quadruple … ASR MODE_IX1 (Byte 〈x6,x7〉) 〈x0,x4〉
+; quadruple … ASR MODE_IX0 (Byte 〈x7,x7〉) 〈x0,x3〉
+; quadruple … ASR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x7〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_6 ≝
+[
+ quadruple … BRA MODE_IMM1 (Byte 〈x2,x0〉) 〈x0,x3〉
+; quadruple … BRN MODE_IMM1 (Byte 〈x2,x1〉) 〈x0,x3〉
+; quadruple … BHI MODE_IMM1 (Byte 〈x2,x2〉) 〈x0,x3〉
+; quadruple … BLS MODE_IMM1 (Byte 〈x2,x3〉) 〈x0,x3〉
+; quadruple … BCC MODE_IMM1 (Byte 〈x2,x4〉) 〈x0,x3〉
+; quadruple … BCS MODE_IMM1 (Byte 〈x2,x5〉) 〈x0,x3〉
+; quadruple … BNE MODE_IMM1 (Byte 〈x2,x6〉) 〈x0,x3〉
+; quadruple … BEQ MODE_IMM1 (Byte 〈x2,x7〉) 〈x0,x3〉
+; quadruple … BHCC MODE_IMM1 (Byte 〈x2,x8〉) 〈x0,x3〉
+; quadruple … BHCS MODE_IMM1 (Byte 〈x2,x9〉) 〈x0,x3〉
+; quadruple … BPL MODE_IMM1 (Byte 〈x2,xA〉) 〈x0,x3〉
+; quadruple … BMI MODE_IMM1 (Byte 〈x2,xB〉) 〈x0,x3〉
+; quadruple … BMC MODE_IMM1 (Byte 〈x2,xC〉) 〈x0,x3〉
+; quadruple … BMS MODE_IMM1 (Byte 〈x2,xD〉) 〈x0,x3〉
+; quadruple … BIL MODE_IMM1 (Byte 〈x2,xE〉) 〈x0,x3〉
+; quadruple … BIH MODE_IMM1 (Byte 〈x2,xF〉) 〈x0,x3〉
+; quadruple … BGE MODE_IMM1 (Byte 〈x9,x0〉) 〈x0,x3〉
+; quadruple … BLT MODE_IMM1 (Byte 〈x9,x1〉) 〈x0,x3〉
+; quadruple … BGT MODE_IMM1 (Byte 〈x9,x2〉) 〈x0,x3〉
+; quadruple … BLE MODE_IMM1 (Byte 〈x9,x3〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC08_7 ≝
+[
+ quadruple … BSETn (MODE_DIRn o0) (Byte 〈x1,x0〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o0) (Byte 〈x1,x1〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o1) (Byte 〈x1,x2〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o1) (Byte 〈x1,x3〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o2) (Byte 〈x1,x4〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o2) (Byte 〈x1,x5〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o3) (Byte 〈x1,x6〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o3) (Byte 〈x1,x7〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o4) (Byte 〈x1,x8〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o4) (Byte 〈x1,x9〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o5) (Byte 〈x1,xA〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o5) (Byte 〈x1,xB〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o6) (Byte 〈x1,xC〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o6) (Byte 〈x1,xD〉) 〈x0,x4〉
+; quadruple … BSETn (MODE_DIRn o7) (Byte 〈x1,xE〉) 〈x0,x4〉
+; quadruple … BCLRn (MODE_DIRn o7) (Byte 〈x1,xF〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_8 ≝
+[
+ quadruple … BRSETn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x0〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x1〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x2〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x3〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x4〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x5〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x6〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x7〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x8〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x9〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xA〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xB〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xC〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xD〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xE〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_9 ≝
+[
+ quadruple … BIT MODE_IMM1 (Byte 〈xA,x5〉) 〈x0,x2〉
+; quadruple … BIT MODE_DIR1 (Byte 〈xB,x5〉) 〈x0,x3〉
+; quadruple … BIT MODE_DIR2 (Byte 〈xC,x5〉) 〈x0,x4〉
+; quadruple … BIT MODE_IX2 (Byte 〈xD,x5〉) 〈x0,x4〉
+; quadruple … BIT MODE_IX1 (Byte 〈xE,x5〉) 〈x0,x3〉
+; quadruple … BIT MODE_IX0 (Byte 〈xF,x5〉) 〈x0,x2〉
+; quadruple … BIT MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x5〉〉) 〈x0,x5〉
+; quadruple … BIT MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x5〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_10 ≝
+[
+ quadruple … MUL MODE_INH (Byte 〈x4,x2〉) 〈x0,x5〉
+; quadruple … DIV MODE_INH (Byte 〈x5,x2〉) 〈x0,x7〉
+; quadruple … NSA MODE_INH (Byte 〈x6,x2〉) 〈x0,x3〉
+; quadruple … DAA MODE_INH (Byte 〈x7,x2〉) 〈x0,x2〉
+; quadruple … RTI MODE_INH (Byte 〈x8,x0〉) 〈x0,x7〉
+; quadruple … RTS MODE_INH (Byte 〈x8,x1〉) 〈x0,x4〉
+; quadruple … SWI MODE_INH (Byte 〈x8,x3〉) 〈x0,x9〉
+; quadruple … TAP MODE_INH (Byte 〈x8,x4〉) 〈x0,x2〉
+; quadruple … TPA MODE_INH (Byte 〈x8,x5〉) 〈x0,x1〉
+; quadruple … PULA MODE_INH (Byte 〈x8,x6〉) 〈x0,x2〉
+; quadruple … PSHA MODE_INH (Byte 〈x8,x7〉) 〈x0,x2〉
+; quadruple … PULX MODE_INH (Byte 〈x8,x8〉) 〈x0,x2〉
+; quadruple … PSHX MODE_INH (Byte 〈x8,x9〉) 〈x0,x2〉
+; quadruple … PULH MODE_INH (Byte 〈x8,xA〉) 〈x0,x2〉
+; quadruple … PSHH MODE_INH (Byte 〈x8,xB〉) 〈x0,x2〉
+; quadruple … STOP MODE_INH (Byte 〈x8,xE〉) 〈x0,x1〉
+; quadruple … WAIT MODE_INH (Byte 〈x8,xF〉) 〈x0,x1〉
+; quadruple … TXS MODE_INH (Byte 〈x9,x4〉) 〈x0,x2〉
+; quadruple … TSX MODE_INH (Byte 〈x9,x5〉) 〈x0,x2〉
+; quadruple … TAX MODE_INH (Byte 〈x9,x7〉) 〈x0,x1〉
+; quadruple … CLC MODE_INH (Byte 〈x9,x8〉) 〈x0,x1〉
+; quadruple … SEC MODE_INH (Byte 〈x9,x9〉) 〈x0,x1〉
+; quadruple … CLI MODE_INH (Byte 〈x9,xA〉) 〈x0,x2〉
+; quadruple … SEI MODE_INH (Byte 〈x9,xB〉) 〈x0,x2〉
+; quadruple … RSP MODE_INH (Byte 〈x9,xC〉) 〈x0,x1〉
+; quadruple … NOP MODE_INH (Byte 〈x9,xD〉) 〈x0,x1〉
+; quadruple … TXA MODE_INH (Byte 〈x9,xF〉) 〈x0,x1〉
+; quadruple … AIS MODE_IMM1 (Byte 〈xA,x7〉) 〈x0,x2〉
+; quadruple … AIX MODE_IMM1 (Byte 〈xA,xF〉) 〈x0,x2〉
+].
+
+ndefinition opcode_table_HC08_11 ≝
+[
+ quadruple … CBEQA MODE_DIR1_and_IMM1 (Byte 〈x3,x1〉) 〈x0,x5〉
+; quadruple … CBEQA MODE_IMM1_and_IMM1 (Byte 〈x4,x1〉) 〈x0,x4〉
+; quadruple … CBEQX MODE_IMM1_and_IMM1 (Byte 〈x5,x1〉) 〈x0,x4〉
+; quadruple … CBEQA MODE_IX1p_and_IMM1 (Byte 〈x6,x1〉) 〈x0,x5〉
+; quadruple … CBEQA MODE_IX0p_and_IMM1 (Byte 〈x7,x1〉) 〈x0,x4〉
+; quadruple … CBEQA MODE_SP1_and_IMM1 (Word 〈〈x9,xE〉:〈x6,x1〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HC08_12 ≝
+[
+ quadruple … CLR MODE_DIR1 (Byte 〈x3,xF〉) 〈x0,x3〉
+; quadruple … CLR MODE_INHA (Byte 〈x4,xF〉) 〈x0,x1〉
+; quadruple … CLR MODE_INHX (Byte 〈x5,xF〉) 〈x0,x1〉
+; quadruple … CLR MODE_IX1 (Byte 〈x6,xF〉) 〈x0,x3〉
+; quadruple … CLR MODE_IX0 (Byte 〈x7,xF〉) 〈x0,x2〉
+; quadruple … CLR MODE_INHH (Byte 〈x8,xC〉) 〈x0,x1〉
+; quadruple … CLR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xF〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_13 ≝
+[
+ quadruple … CMP MODE_IMM1 (Byte 〈xA,x1〉) 〈x0,x2〉
+; quadruple … CMP MODE_DIR1 (Byte 〈xB,x1〉) 〈x0,x3〉
+; quadruple … CMP MODE_DIR2 (Byte 〈xC,x1〉) 〈x0,x4〉
+; quadruple … CMP MODE_IX2 (Byte 〈xD,x1〉) 〈x0,x4〉
+; quadruple … CMP MODE_IX1 (Byte 〈xE,x1〉) 〈x0,x3〉
+; quadruple … CMP MODE_IX0 (Byte 〈xF,x1〉) 〈x0,x2〉
+; quadruple … CMP MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x1〉〉) 〈x0,x5〉
+; quadruple … CMP MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x1〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_14 ≝
+[
+ quadruple … COM MODE_DIR1 (Byte 〈x3,x3〉) 〈x0,x4〉
+; quadruple … COM MODE_INHA (Byte 〈x4,x3〉) 〈x0,x1〉
+; quadruple … COM MODE_INHX (Byte 〈x5,x3〉) 〈x0,x1〉
+; quadruple … COM MODE_IX1 (Byte 〈x6,x3〉) 〈x0,x4〉
+; quadruple … COM MODE_IX0 (Byte 〈x7,x3〉) 〈x0,x3〉
+; quadruple … COM MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x3〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_15 ≝
+[
+ quadruple … STHX MODE_DIR1 (Byte 〈x3,x5〉) 〈x0,x4〉
+; quadruple … LDHX MODE_IMM2 (Byte 〈x4,x5〉) 〈x0,x3〉
+; quadruple … LDHX MODE_DIR1 (Byte 〈x5,x5〉) 〈x0,x4〉
+; quadruple … CPHX MODE_IMM2 (Byte 〈x6,x5〉) 〈x0,x3〉
+; quadruple … CPHX MODE_DIR1 (Byte 〈x7,x5〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_16 ≝
+[
+ quadruple … CPX MODE_IMM1 (Byte 〈xA,x3〉) 〈x0,x2〉
+; quadruple … CPX MODE_DIR1 (Byte 〈xB,x3〉) 〈x0,x3〉
+; quadruple … CPX MODE_DIR2 (Byte 〈xC,x3〉) 〈x0,x4〉
+; quadruple … CPX MODE_IX2 (Byte 〈xD,x3〉) 〈x0,x4〉
+; quadruple … CPX MODE_IX1 (Byte 〈xE,x3〉) 〈x0,x3〉
+; quadruple … CPX MODE_IX0 (Byte 〈xF,x3〉) 〈x0,x2〉
+; quadruple … CPX MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x3〉〉) 〈x0,x5〉
+; quadruple … CPX MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x3〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_17 ≝
+[
+ quadruple … DBNZ MODE_DIR1_and_IMM1 (Byte 〈x3,xB〉) 〈x0,x5〉
+; quadruple … DBNZ MODE_INHA_and_IMM1 (Byte 〈x4,xB〉) 〈x0,x3〉
+; quadruple … DBNZ MODE_INHX_and_IMM1 (Byte 〈x5,xB〉) 〈x0,x3〉
+; quadruple … DBNZ MODE_IX1_and_IMM1 (Byte 〈x6,xB〉) 〈x0,x5〉
+; quadruple … DBNZ MODE_IX0_and_IMM1 (Byte 〈x7,xB〉) 〈x0,x4〉
+; quadruple … DBNZ MODE_SP1_and_IMM1 (Word 〈〈x9,xE〉:〈x6,xB〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HC08_18 ≝
+[
+ quadruple … DEC MODE_DIR1 (Byte 〈x3,xA〉) 〈x0,x4〉
+; quadruple … DEC MODE_INHA (Byte 〈x4,xA〉) 〈x0,x1〉
+; quadruple … DEC MODE_INHX (Byte 〈x5,xA〉) 〈x0,x1〉
+; quadruple … DEC MODE_IX1 (Byte 〈x6,xA〉) 〈x0,x4〉
+; quadruple … DEC MODE_IX0 (Byte 〈x7,xA〉) 〈x0,x3〉
+; quadruple … DEC MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xA〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_19 ≝
+[
+ quadruple … EOR MODE_IMM1 (Byte 〈xA,x8〉) 〈x0,x2〉
+; quadruple … EOR MODE_DIR1 (Byte 〈xB,x8〉) 〈x0,x3〉
+; quadruple … EOR MODE_DIR2 (Byte 〈xC,x8〉) 〈x0,x4〉
+; quadruple … EOR MODE_IX2 (Byte 〈xD,x8〉) 〈x0,x4〉
+; quadruple … EOR MODE_IX1 (Byte 〈xE,x8〉) 〈x0,x3〉
+; quadruple … EOR MODE_IX0 (Byte 〈xF,x8〉) 〈x0,x2〉
+; quadruple … EOR MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x8〉〉) 〈x0,x5〉
+; quadruple … EOR MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x8〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_20 ≝
+[
+ quadruple … INC MODE_DIR1 (Byte 〈x3,xC〉) 〈x0,x4〉
+; quadruple … INC MODE_INHA (Byte 〈x4,xC〉) 〈x0,x1〉
+; quadruple … INC MODE_INHX (Byte 〈x5,xC〉) 〈x0,x1〉
+; quadruple … INC MODE_IX1 (Byte 〈x6,xC〉) 〈x0,x4〉
+; quadruple … INC MODE_IX0 (Byte 〈x7,xC〉) 〈x0,x3〉
+; quadruple … INC MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xC〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_21 ≝
+[
+ quadruple … JMP MODE_IMM1EXT (Byte 〈xB,xC〉) 〈x0,x2〉
+; quadruple … JMP MODE_IMM2 (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadruple … JMP MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadruple … JMP MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadruple … JMP MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HC08_22 ≝
+[
+ quadruple … BSR MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x4〉
+; quadruple … JSR MODE_IMM1EXT (Byte 〈xB,xD〉) 〈x0,x4〉
+; quadruple … JSR MODE_IMM2 (Byte 〈xC,xD〉) 〈x0,x5〉
+; quadruple … JSR MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x6〉
+; quadruple … JSR MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x5〉
+; quadruple … JSR MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_23 ≝
+[
+ quadruple … LDA MODE_IMM1 (Byte 〈xA,x6〉) 〈x0,x2〉
+; quadruple … LDA MODE_DIR1 (Byte 〈xB,x6〉) 〈x0,x3〉
+; quadruple … LDA MODE_DIR2 (Byte 〈xC,x6〉) 〈x0,x4〉
+; quadruple … LDA MODE_IX2 (Byte 〈xD,x6〉) 〈x0,x4〉
+; quadruple … LDA MODE_IX1 (Byte 〈xE,x6〉) 〈x0,x3〉
+; quadruple … LDA MODE_IX0 (Byte 〈xF,x6〉) 〈x0,x2〉
+; quadruple … LDA MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x6〉〉) 〈x0,x5〉
+; quadruple … LDA MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x6〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_24 ≝
+[
+ quadruple … LDX MODE_IMM1 (Byte 〈xA,xE〉) 〈x0,x2〉
+; quadruple … LDX MODE_DIR1 (Byte 〈xB,xE〉) 〈x0,x3〉
+; quadruple … LDX MODE_DIR2 (Byte 〈xC,xE〉) 〈x0,x4〉
+; quadruple … LDX MODE_IX2 (Byte 〈xD,xE〉) 〈x0,x4〉
+; quadruple … LDX MODE_IX1 (Byte 〈xE,xE〉) 〈x0,x3〉
+; quadruple … LDX MODE_IX0 (Byte 〈xF,xE〉) 〈x0,x2〉
+; quadruple … LDX MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xE〉〉) 〈x0,x5〉
+; quadruple … LDX MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xE〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_25 ≝
+[
+ quadruple … LSR MODE_DIR1 (Byte 〈x3,x4〉) 〈x0,x4〉
+; quadruple … LSR MODE_INHA (Byte 〈x4,x4〉) 〈x0,x1〉
+; quadruple … LSR MODE_INHX (Byte 〈x5,x4〉) 〈x0,x1〉
+; quadruple … LSR MODE_IX1 (Byte 〈x6,x4〉) 〈x0,x4〉
+; quadruple … LSR MODE_IX0 (Byte 〈x7,x4〉) 〈x0,x3〉
+; quadruple … LSR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x4〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_26 ≝
+[
+ quadruple … MOV MODE_DIR1_to_DIR1 (Byte 〈x4,xE〉) 〈x0,x5〉
+; quadruple … MOV MODE_DIR1_to_IX0p (Byte 〈x5,xE〉) 〈x0,x4〉
+; quadruple … MOV MODE_IMM1_to_DIR1 (Byte 〈x6,xE〉) 〈x0,x4〉
+; quadruple … MOV MODE_IX0p_to_DIR1 (Byte 〈x7,xE〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_27 ≝
+[
+ quadruple … NEG MODE_DIR1 (Byte 〈x3,x0〉) 〈x0,x4〉
+; quadruple … NEG MODE_INHA (Byte 〈x4,x0〉) 〈x0,x1〉
+; quadruple … NEG MODE_INHX (Byte 〈x5,x0〉) 〈x0,x1〉
+; quadruple … NEG MODE_IX1 (Byte 〈x6,x0〉) 〈x0,x4〉
+; quadruple … NEG MODE_IX0 (Byte 〈x7,x0〉) 〈x0,x3〉
+; quadruple … NEG MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x0〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_28 ≝
+[
+ quadruple … ORA MODE_IMM1 (Byte 〈xA,xA〉) 〈x0,x2〉
+; quadruple … ORA MODE_DIR1 (Byte 〈xB,xA〉) 〈x0,x3〉
+; quadruple … ORA MODE_DIR2 (Byte 〈xC,xA〉) 〈x0,x4〉
+; quadruple … ORA MODE_IX2 (Byte 〈xD,xA〉) 〈x0,x4〉
+; quadruple … ORA MODE_IX1 (Byte 〈xE,xA〉) 〈x0,x3〉
+; quadruple … ORA MODE_IX0 (Byte 〈xF,xA〉) 〈x0,x2〉
+; quadruple … ORA MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xA〉〉) 〈x0,x5〉
+; quadruple … ORA MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xA〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_29 ≝
+[
+ quadruple … ROL MODE_DIR1 (Byte 〈x3,x9〉) 〈x0,x4〉
+; quadruple … ROL MODE_INHA (Byte 〈x4,x9〉) 〈x0,x1〉
+; quadruple … ROL MODE_INHX (Byte 〈x5,x9〉) 〈x0,x1〉
+; quadruple … ROL MODE_IX1 (Byte 〈x6,x9〉) 〈x0,x4〉
+; quadruple … ROL MODE_IX0 (Byte 〈x7,x9〉) 〈x0,x3〉
+; quadruple … ROL MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x9〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_30 ≝
+[
+ quadruple … ROR MODE_DIR1 (Byte 〈x3,x6〉) 〈x0,x4〉
+; quadruple … ROR MODE_INHA (Byte 〈x4,x6〉) 〈x0,x1〉
+; quadruple … ROR MODE_INHX (Byte 〈x5,x6〉) 〈x0,x1〉
+; quadruple … ROR MODE_IX1 (Byte 〈x6,x6〉) 〈x0,x4〉
+; quadruple … ROR MODE_IX0 (Byte 〈x7,x6〉) 〈x0,x3〉
+; quadruple … ROR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x6〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HC08_31 ≝
+[
+ quadruple … SBC MODE_IMM1 (Byte 〈xA,x2〉) 〈x0,x2〉
+; quadruple … SBC MODE_DIR1 (Byte 〈xB,x2〉) 〈x0,x3〉
+; quadruple … SBC MODE_DIR2 (Byte 〈xC,x2〉) 〈x0,x4〉
+; quadruple … SBC MODE_IX2 (Byte 〈xD,x2〉) 〈x0,x4〉
+; quadruple … SBC MODE_IX1 (Byte 〈xE,x2〉) 〈x0,x3〉
+; quadruple … SBC MODE_IX0 (Byte 〈xF,x2〉) 〈x0,x2〉
+; quadruple … SBC MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x2〉〉) 〈x0,x5〉
+; quadruple … SBC MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x2〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_32 ≝
+[
+ quadruple … STA MODE_DIR1 (Byte 〈xB,x7〉) 〈x0,x3〉
+; quadruple … STA MODE_DIR2 (Byte 〈xC,x7〉) 〈x0,x4〉
+; quadruple … STA MODE_IX2 (Byte 〈xD,x7〉) 〈x0,x4〉
+; quadruple … STA MODE_IX1 (Byte 〈xE,x7〉) 〈x0,x3〉
+; quadruple … STA MODE_IX0 (Byte 〈xF,x7〉) 〈x0,x2〉
+; quadruple … STA MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x7〉〉) 〈x0,x5〉
+; quadruple … STA MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x7〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_33 ≝
+[
+ quadruple … STX MODE_DIR1 (Byte 〈xB,xF〉) 〈x0,x3〉
+; quadruple … STX MODE_DIR2 (Byte 〈xC,xF〉) 〈x0,x4〉
+; quadruple … STX MODE_IX2 (Byte 〈xD,xF〉) 〈x0,x4〉
+; quadruple … STX MODE_IX1 (Byte 〈xE,xF〉) 〈x0,x3〉
+; quadruple … STX MODE_IX0 (Byte 〈xF,xF〉) 〈x0,x2〉
+; quadruple … STX MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xF〉〉) 〈x0,x5〉
+; quadruple … STX MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xF〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_34 ≝
+[
+ quadruple … SUB MODE_IMM1 (Byte 〈xA,x0〉) 〈x0,x2〉
+; quadruple … SUB MODE_DIR1 (Byte 〈xB,x0〉) 〈x0,x3〉
+; quadruple … SUB MODE_DIR2 (Byte 〈xC,x0〉) 〈x0,x4〉
+; quadruple … SUB MODE_IX2 (Byte 〈xD,x0〉) 〈x0,x4〉
+; quadruple … SUB MODE_IX1 (Byte 〈xE,x0〉) 〈x0,x3〉
+; quadruple … SUB MODE_IX0 (Byte 〈xF,x0〉) 〈x0,x2〉
+; quadruple … SUB MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x0〉〉) 〈x0,x5〉
+; quadruple … SUB MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x0〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08_35 ≝
+[
+ quadruple … TST MODE_DIR1 (Byte 〈x3,xD〉) 〈x0,x3〉
+; quadruple … TST MODE_INHA (Byte 〈x4,xD〉) 〈x0,x1〉
+; quadruple … TST MODE_INHX (Byte 〈x5,xD〉) 〈x0,x1〉
+; quadruple … TST MODE_IX1 (Byte 〈x6,xD〉) 〈x0,x3〉
+; quadruple … TST MODE_IX0 (Byte 〈x7,xD〉) 〈x0,x2〉
+; quadruple … TST MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xD〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HC08 ≝
+opcode_table_HC08_1 @ opcode_table_HC08_2 @ opcode_table_HC08_3 @ opcode_table_HC08_4 @
+opcode_table_HC08_5 @ opcode_table_HC08_6 @ opcode_table_HC08_7 @ opcode_table_HC08_8 @
+opcode_table_HC08_9 @ opcode_table_HC08_10 @ opcode_table_HC08_11 @ opcode_table_HC08_12 @
+opcode_table_HC08_13 @ opcode_table_HC08_14 @ opcode_table_HC08_15 @ opcode_table_HC08_16 @
+opcode_table_HC08_17 @ opcode_table_HC08_18 @ opcode_table_HC08_19 @ opcode_table_HC08_20 @
+opcode_table_HC08_21 @ opcode_table_HC08_22 @ opcode_table_HC08_23 @ opcode_table_HC08_24 @
+opcode_table_HC08_25 @ opcode_table_HC08_26 @ opcode_table_HC08_27 @ opcode_table_HC08_28 @
+opcode_table_HC08_29 @ opcode_table_HC08_30 @ opcode_table_HC08_31 @ opcode_table_HC08_32 @
+opcode_table_HC08_33 @ opcode_table_HC08_34 @ opcode_table_HC08_35.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_pseudo.ma".
+include "emulator/opcodes/Freescale_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ****************** *)
+(* TABELLA DELL'HCS08 *)
+(* ****************** *)
+
+(* definizione come concatenazione finale di liste per velocizzare il parsing *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
+
+ndefinition opcode_table_HCS08_1 ≝
+[
+ quadruple … ADC MODE_IMM1 (Byte 〈xA,x9〉) 〈x0,x2〉
+; quadruple … ADC MODE_DIR1 (Byte 〈xB,x9〉) 〈x0,x3〉
+; quadruple … ADC MODE_DIR2 (Byte 〈xC,x9〉) 〈x0,x4〉
+; quadruple … ADC MODE_IX2 (Byte 〈xD,x9〉) 〈x0,x4〉
+; quadruple … ADC MODE_IX1 (Byte 〈xE,x9〉) 〈x0,x3〉
+; quadruple … ADC MODE_IX0 (Byte 〈xF,x9〉) 〈x0,x3〉
+; quadruple … ADC MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x9〉〉) 〈x0,x5〉
+; quadruple … ADC MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x9〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_2 ≝
+[
+ quadruple … ADD MODE_IMM1 (Byte 〈xA,xB〉) 〈x0,x2〉
+; quadruple … ADD MODE_DIR1 (Byte 〈xB,xB〉) 〈x0,x3〉
+; quadruple … ADD MODE_DIR2 (Byte 〈xC,xB〉) 〈x0,x4〉
+; quadruple … ADD MODE_IX2 (Byte 〈xD,xB〉) 〈x0,x4〉
+; quadruple … ADD MODE_IX1 (Byte 〈xE,xB〉) 〈x0,x3〉
+; quadruple … ADD MODE_IX0 (Byte 〈xF,xB〉) 〈x0,x3〉
+; quadruple … ADD MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xB〉〉) 〈x0,x5〉
+; quadruple … ADD MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xB〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_3 ≝
+[
+ quadruple … AND MODE_IMM1 (Byte 〈xA,x4〉) 〈x0,x2〉
+; quadruple … AND MODE_DIR1 (Byte 〈xB,x4〉) 〈x0,x3〉
+; quadruple … AND MODE_DIR2 (Byte 〈xC,x4〉) 〈x0,x4〉
+; quadruple … AND MODE_IX2 (Byte 〈xD,x4〉) 〈x0,x4〉
+; quadruple … AND MODE_IX1 (Byte 〈xE,x4〉) 〈x0,x3〉
+; quadruple … AND MODE_IX0 (Byte 〈xF,x4〉) 〈x0,x3〉
+; quadruple … AND MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x4〉〉) 〈x0,x5〉
+; quadruple … AND MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x4〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_4 ≝
+[
+ quadruple … ASL MODE_DIR1 (Byte 〈x3,x8〉) 〈x0,x5〉
+; quadruple … ASL MODE_INHA (Byte 〈x4,x8〉) 〈x0,x1〉
+; quadruple … ASL MODE_INHX (Byte 〈x5,x8〉) 〈x0,x1〉
+; quadruple … ASL MODE_IX1 (Byte 〈x6,x8〉) 〈x0,x5〉
+; quadruple … ASL MODE_IX0 (Byte 〈x7,x8〉) 〈x0,x4〉
+; quadruple … ASL MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x8〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_5 ≝
+[
+ quadruple … ASR MODE_DIR1 (Byte 〈x3,x7〉) 〈x0,x5〉
+; quadruple … ASR MODE_INHA (Byte 〈x4,x7〉) 〈x0,x1〉
+; quadruple … ASR MODE_INHX (Byte 〈x5,x7〉) 〈x0,x1〉
+; quadruple … ASR MODE_IX1 (Byte 〈x6,x7〉) 〈x0,x5〉
+; quadruple … ASR MODE_IX0 (Byte 〈x7,x7〉) 〈x0,x4〉
+; quadruple … ASR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x7〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_6 ≝
+[
+ quadruple … BRA MODE_IMM1 (Byte 〈x2,x0〉) 〈x0,x3〉
+; quadruple … BRN MODE_IMM1 (Byte 〈x2,x1〉) 〈x0,x3〉
+; quadruple … BHI MODE_IMM1 (Byte 〈x2,x2〉) 〈x0,x3〉
+; quadruple … BLS MODE_IMM1 (Byte 〈x2,x3〉) 〈x0,x3〉
+; quadruple … BCC MODE_IMM1 (Byte 〈x2,x4〉) 〈x0,x3〉
+; quadruple … BCS MODE_IMM1 (Byte 〈x2,x5〉) 〈x0,x3〉
+; quadruple … BNE MODE_IMM1 (Byte 〈x2,x6〉) 〈x0,x3〉
+; quadruple … BEQ MODE_IMM1 (Byte 〈x2,x7〉) 〈x0,x3〉
+; quadruple … BHCC MODE_IMM1 (Byte 〈x2,x8〉) 〈x0,x3〉
+; quadruple … BHCS MODE_IMM1 (Byte 〈x2,x9〉) 〈x0,x3〉
+; quadruple … BPL MODE_IMM1 (Byte 〈x2,xA〉) 〈x0,x3〉
+; quadruple … BMI MODE_IMM1 (Byte 〈x2,xB〉) 〈x0,x3〉
+; quadruple … BMC MODE_IMM1 (Byte 〈x2,xC〉) 〈x0,x3〉
+; quadruple … BMS MODE_IMM1 (Byte 〈x2,xD〉) 〈x0,x3〉
+; quadruple … BIL MODE_IMM1 (Byte 〈x2,xE〉) 〈x0,x3〉
+; quadruple … BIH MODE_IMM1 (Byte 〈x2,xF〉) 〈x0,x3〉
+; quadruple … BGE MODE_IMM1 (Byte 〈x9,x0〉) 〈x0,x3〉
+; quadruple … BLT MODE_IMM1 (Byte 〈x9,x1〉) 〈x0,x3〉
+; quadruple … BGT MODE_IMM1 (Byte 〈x9,x2〉) 〈x0,x3〉
+; quadruple … BLE MODE_IMM1 (Byte 〈x9,x3〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HCS08_7 ≝
+[
+ quadruple … BSETn (MODE_DIRn o0) (Byte 〈x1,x0〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o0) (Byte 〈x1,x1〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o1) (Byte 〈x1,x2〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o1) (Byte 〈x1,x3〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o2) (Byte 〈x1,x4〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o2) (Byte 〈x1,x5〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o3) (Byte 〈x1,x6〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o3) (Byte 〈x1,x7〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o4) (Byte 〈x1,x8〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o4) (Byte 〈x1,x9〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o5) (Byte 〈x1,xA〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o5) (Byte 〈x1,xB〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o6) (Byte 〈x1,xC〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o6) (Byte 〈x1,xD〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o7) (Byte 〈x1,xE〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o7) (Byte 〈x1,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HCS08_8 ≝
+[
+ quadruple … BRSETn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x0〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x1〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x2〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x3〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x4〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x5〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x6〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x7〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x8〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x9〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xA〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xB〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xC〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xD〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xE〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HCS08_9 ≝
+[
+ quadruple … BIT MODE_IMM1 (Byte 〈xA,x5〉) 〈x0,x2〉
+; quadruple … BIT MODE_DIR1 (Byte 〈xB,x5〉) 〈x0,x3〉
+; quadruple … BIT MODE_DIR2 (Byte 〈xC,x5〉) 〈x0,x4〉
+; quadruple … BIT MODE_IX2 (Byte 〈xD,x5〉) 〈x0,x4〉
+; quadruple … BIT MODE_IX1 (Byte 〈xE,x5〉) 〈x0,x3〉
+; quadruple … BIT MODE_IX0 (Byte 〈xF,x5〉) 〈x0,x3〉
+; quadruple … BIT MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x5〉〉) 〈x0,x5〉
+; quadruple … BIT MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x5〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_10 ≝
+[
+ quadruple … MUL MODE_INH (Byte 〈x4,x2〉) 〈x0,x5〉
+; quadruple … DIV MODE_INH (Byte 〈x5,x2〉) 〈x0,x6〉
+; quadruple … NSA MODE_INH (Byte 〈x6,x2〉) 〈x0,x1〉
+; quadruple … DAA MODE_INH (Byte 〈x7,x2〉) 〈x0,x1〉
+; quadruple … RTI MODE_INH (Byte 〈x8,x0〉) 〈x0,x9〉
+; quadruple … RTS MODE_INH (Byte 〈x8,x1〉) 〈x0,x6〉
+; quadruple … SWI MODE_INH (Byte 〈x8,x3〉) 〈x0,xB〉
+; quadruple … BGND MODE_INH (Byte 〈x8,x2〉) 〈x0,x5〉
+; quadruple … TAP MODE_INH (Byte 〈x8,x4〉) 〈x0,x1〉
+; quadruple … TPA MODE_INH (Byte 〈x8,x5〉) 〈x0,x1〉
+; quadruple … PULA MODE_INH (Byte 〈x8,x6〉) 〈x0,x3〉
+; quadruple … PSHA MODE_INH (Byte 〈x8,x7〉) 〈x0,x2〉
+; quadruple … PULX MODE_INH (Byte 〈x8,x8〉) 〈x0,x3〉
+; quadruple … PSHX MODE_INH (Byte 〈x8,x9〉) 〈x0,x2〉
+; quadruple … PULH MODE_INH (Byte 〈x8,xA〉) 〈x0,x3〉
+; quadruple … PSHH MODE_INH (Byte 〈x8,xB〉) 〈x0,x2〉
+; quadruple … STOP MODE_INH (Byte 〈x8,xE〉) 〈x0,x2〉
+; quadruple … WAIT MODE_INH (Byte 〈x8,xF〉) 〈x0,x2〉
+; quadruple … TXS MODE_INH (Byte 〈x9,x4〉) 〈x0,x2〉
+; quadruple … TSX MODE_INH (Byte 〈x9,x5〉) 〈x0,x2〉
+; quadruple … TAX MODE_INH (Byte 〈x9,x7〉) 〈x0,x1〉
+; quadruple … CLC MODE_INH (Byte 〈x9,x8〉) 〈x0,x1〉
+; quadruple … SEC MODE_INH (Byte 〈x9,x9〉) 〈x0,x1〉
+; quadruple … CLI MODE_INH (Byte 〈x9,xA〉) 〈x0,x1〉
+; quadruple … SEI MODE_INH (Byte 〈x9,xB〉) 〈x0,x1〉
+; quadruple … RSP MODE_INH (Byte 〈x9,xC〉) 〈x0,x1〉
+; quadruple … NOP MODE_INH (Byte 〈x9,xD〉) 〈x0,x1〉
+; quadruple … TXA MODE_INH (Byte 〈x9,xF〉) 〈x0,x1〉
+; quadruple … AIS MODE_IMM1 (Byte 〈xA,x7〉) 〈x0,x2〉
+; quadruple … AIX MODE_IMM1 (Byte 〈xA,xF〉) 〈x0,x2〉
+].
+
+ndefinition opcode_table_HCS08_11 ≝
+[
+ quadruple … CBEQA MODE_DIR1_and_IMM1 (Byte 〈x3,x1〉) 〈x0,x5〉
+; quadruple … CBEQA MODE_IMM1_and_IMM1 (Byte 〈x4,x1〉) 〈x0,x4〉
+; quadruple … CBEQX MODE_IMM1_and_IMM1 (Byte 〈x5,x1〉) 〈x0,x4〉
+; quadruple … CBEQA MODE_IX1p_and_IMM1 (Byte 〈x6,x1〉) 〈x0,x5〉
+; quadruple … CBEQA MODE_IX0p_and_IMM1 (Byte 〈x7,x1〉) 〈x0,x5〉
+; quadruple … CBEQA MODE_SP1_and_IMM1 (Word 〈〈x9,xE〉:〈x6,x1〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_12 ≝
+[
+ quadruple … CLR MODE_DIR1 (Byte 〈x3,xF〉) 〈x0,x5〉
+; quadruple … CLR MODE_INHA (Byte 〈x4,xF〉) 〈x0,x1〉
+; quadruple … CLR MODE_INHX (Byte 〈x5,xF〉) 〈x0,x1〉
+; quadruple … CLR MODE_IX1 (Byte 〈x6,xF〉) 〈x0,x5〉
+; quadruple … CLR MODE_IX0 (Byte 〈x7,xF〉) 〈x0,x4〉
+; quadruple … CLR MODE_INHH (Byte 〈x8,xC〉) 〈x0,x1〉
+; quadruple … CLR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xF〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_13 ≝
+[
+ quadruple … CMP MODE_IMM1 (Byte 〈xA,x1〉) 〈x0,x2〉
+; quadruple … CMP MODE_DIR1 (Byte 〈xB,x1〉) 〈x0,x3〉
+; quadruple … CMP MODE_DIR2 (Byte 〈xC,x1〉) 〈x0,x4〉
+; quadruple … CMP MODE_IX2 (Byte 〈xD,x1〉) 〈x0,x4〉
+; quadruple … CMP MODE_IX1 (Byte 〈xE,x1〉) 〈x0,x3〉
+; quadruple … CMP MODE_IX0 (Byte 〈xF,x1〉) 〈x0,x3〉
+; quadruple … CMP MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x1〉〉) 〈x0,x5〉
+; quadruple … CMP MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x1〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_14 ≝
+[
+ quadruple … COM MODE_DIR1 (Byte 〈x3,x3〉) 〈x0,x5〉
+; quadruple … COM MODE_INHA (Byte 〈x4,x3〉) 〈x0,x1〉
+; quadruple … COM MODE_INHX (Byte 〈x5,x3〉) 〈x0,x1〉
+; quadruple … COM MODE_IX1 (Byte 〈x6,x3〉) 〈x0,x5〉
+; quadruple … COM MODE_IX0 (Byte 〈x7,x3〉) 〈x0,x4〉
+; quadruple … COM MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x3〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_15 ≝
+[
+ quadruple … CPHX MODE_DIR2 (Byte 〈x3,xE〉) 〈x0,x6〉
+; quadruple … CPHX MODE_IMM2 (Byte 〈x6,x5〉) 〈x0,x3〉
+; quadruple … CPHX MODE_DIR1 (Byte 〈x7,x5〉) 〈x0,x5〉
+; quadruple … CPHX MODE_SP1 (Word 〈〈x9,xE〉:〈xF,x3〉〉) 〈x0,x6〉
+
+; quadruple … LDHX MODE_DIR2 (Byte 〈x3,x2〉) 〈x0,x5〉
+; quadruple … LDHX MODE_IMM2 (Byte 〈x4,x5〉) 〈x0,x3〉
+; quadruple … LDHX MODE_DIR1 (Byte 〈x5,x5〉) 〈x0,x4〉
+; quadruple … LDHX MODE_IX0 (Word 〈〈x9,xE〉:〈xA,xE〉〉) 〈x0,x5〉
+; quadruple … LDHX MODE_IX2 (Word 〈〈x9,xE〉:〈xB,xE〉〉) 〈x0,x6〉
+; quadruple … LDHX MODE_IX1 (Word 〈〈x9,xE〉:〈xC,xE〉〉) 〈x0,x5〉
+; quadruple … LDHX MODE_SP1 (Word 〈〈x9,xE〉:〈xF,xE〉〉) 〈x0,x5〉
+
+; quadruple … STHX MODE_DIR1 (Byte 〈x3,x5〉) 〈x0,x4〉
+; quadruple … STHX MODE_DIR2 (Byte 〈x9,x6〉) 〈x0,x5〉
+; quadruple … STHX MODE_SP1 (Word 〈〈x9,xE〉:〈xF,xF〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HCS08_16 ≝
+[
+ quadruple … CPX MODE_IMM1 (Byte 〈xA,x3〉) 〈x0,x2〉
+; quadruple … CPX MODE_DIR1 (Byte 〈xB,x3〉) 〈x0,x3〉
+; quadruple … CPX MODE_DIR2 (Byte 〈xC,x3〉) 〈x0,x4〉
+; quadruple … CPX MODE_IX2 (Byte 〈xD,x3〉) 〈x0,x4〉
+; quadruple … CPX MODE_IX1 (Byte 〈xE,x3〉) 〈x0,x3〉
+; quadruple … CPX MODE_IX0 (Byte 〈xF,x3〉) 〈x0,x3〉
+; quadruple … CPX MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x3〉〉) 〈x0,x5〉
+; quadruple … CPX MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x3〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_17 ≝
+[
+ quadruple … DBNZ MODE_DIR1_and_IMM1 (Byte 〈x3,xB〉) 〈x0,x7〉
+; quadruple … DBNZ MODE_INHA_and_IMM1 (Byte 〈x4,xB〉) 〈x0,x4〉
+; quadruple … DBNZ MODE_INHX_and_IMM1 (Byte 〈x5,xB〉) 〈x0,x4〉
+; quadruple … DBNZ MODE_IX1_and_IMM1 (Byte 〈x6,xB〉) 〈x0,x7〉
+; quadruple … DBNZ MODE_IX0_and_IMM1 (Byte 〈x7,xB〉) 〈x0,x6〉
+; quadruple … DBNZ MODE_SP1_and_IMM1 (Word 〈〈x9,xE〉:〈x6,xB〉〉) 〈x0,x8〉
+].
+
+ndefinition opcode_table_HCS08_18 ≝
+[
+ quadruple … DEC MODE_DIR1 (Byte 〈x3,xA〉) 〈x0,x5〉
+; quadruple … DEC MODE_INHA (Byte 〈x4,xA〉) 〈x0,x1〉
+; quadruple … DEC MODE_INHX (Byte 〈x5,xA〉) 〈x0,x1〉
+; quadruple … DEC MODE_IX1 (Byte 〈x6,xA〉) 〈x0,x5〉
+; quadruple … DEC MODE_IX0 (Byte 〈x7,xA〉) 〈x0,x4〉
+; quadruple … DEC MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xA〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_19 ≝
+[
+ quadruple … EOR MODE_IMM1 (Byte 〈xA,x8〉) 〈x0,x2〉
+; quadruple … EOR MODE_DIR1 (Byte 〈xB,x8〉) 〈x0,x3〉
+; quadruple … EOR MODE_DIR2 (Byte 〈xC,x8〉) 〈x0,x4〉
+; quadruple … EOR MODE_IX2 (Byte 〈xD,x8〉) 〈x0,x4〉
+; quadruple … EOR MODE_IX1 (Byte 〈xE,x8〉) 〈x0,x3〉
+; quadruple … EOR MODE_IX0 (Byte 〈xF,x8〉) 〈x0,x3〉
+; quadruple … EOR MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x8〉〉) 〈x0,x5〉
+; quadruple … EOR MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x8〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_20 ≝
+[
+ quadruple … INC MODE_DIR1 (Byte 〈x3,xC〉) 〈x0,x5〉
+; quadruple … INC MODE_INHA (Byte 〈x4,xC〉) 〈x0,x1〉
+; quadruple … INC MODE_INHX (Byte 〈x5,xC〉) 〈x0,x1〉
+; quadruple … INC MODE_IX1 (Byte 〈x6,xC〉) 〈x0,x5〉
+; quadruple … INC MODE_IX0 (Byte 〈x7,xC〉) 〈x0,x4〉
+; quadruple … INC MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xC〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_21 ≝
+[
+ quadruple … JMP MODE_IMM1EXT (Byte 〈xB,xC〉) 〈x0,x3〉
+; quadruple … JMP MODE_IMM2 (Byte 〈xC,xC〉) 〈x0,x4〉
+; quadruple … JMP MODE_INHX2ADD (Byte 〈xD,xC〉) 〈x0,x4〉
+; quadruple … JMP MODE_INHX1ADD (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadruple … JMP MODE_INHX0ADD (Byte 〈xF,xC〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_HCS08_22 ≝
+[
+ quadruple … BSR MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x5〉
+; quadruple … JSR MODE_IMM1EXT (Byte 〈xB,xD〉) 〈x0,x5〉
+; quadruple … JSR MODE_IMM2 (Byte 〈xC,xD〉) 〈x0,x6〉
+; quadruple … JSR MODE_INHX2ADD (Byte 〈xD,xD〉) 〈x0,x6〉
+; quadruple … JSR MODE_INHX1ADD (Byte 〈xE,xD〉) 〈x0,x5〉
+; quadruple … JSR MODE_INHX0ADD (Byte 〈xF,xD〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HCS08_23 ≝
+[
+ quadruple … LDA MODE_IMM1 (Byte 〈xA,x6〉) 〈x0,x2〉
+; quadruple … LDA MODE_DIR1 (Byte 〈xB,x6〉) 〈x0,x3〉
+; quadruple … LDA MODE_DIR2 (Byte 〈xC,x6〉) 〈x0,x4〉
+; quadruple … LDA MODE_IX2 (Byte 〈xD,x6〉) 〈x0,x4〉
+; quadruple … LDA MODE_IX1 (Byte 〈xE,x6〉) 〈x0,x3〉
+; quadruple … LDA MODE_IX0 (Byte 〈xF,x6〉) 〈x0,x3〉
+; quadruple … LDA MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x6〉〉) 〈x0,x5〉
+; quadruple … LDA MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x6〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_24 ≝
+[
+ quadruple … LDX MODE_IMM1 (Byte 〈xA,xE〉) 〈x0,x2〉
+; quadruple … LDX MODE_DIR1 (Byte 〈xB,xE〉) 〈x0,x3〉
+; quadruple … LDX MODE_DIR2 (Byte 〈xC,xE〉) 〈x0,x4〉
+; quadruple … LDX MODE_IX2 (Byte 〈xD,xE〉) 〈x0,x4〉
+; quadruple … LDX MODE_IX1 (Byte 〈xE,xE〉) 〈x0,x3〉
+; quadruple … LDX MODE_IX0 (Byte 〈xF,xE〉) 〈x0,x3〉
+; quadruple … LDX MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xE〉〉) 〈x0,x5〉
+; quadruple … LDX MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xE〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_25 ≝
+[
+ quadruple … LSR MODE_DIR1 (Byte 〈x3,x4〉) 〈x0,x5〉
+; quadruple … LSR MODE_INHA (Byte 〈x4,x4〉) 〈x0,x1〉
+; quadruple … LSR MODE_INHX (Byte 〈x5,x4〉) 〈x0,x1〉
+; quadruple … LSR MODE_IX1 (Byte 〈x6,x4〉) 〈x0,x5〉
+; quadruple … LSR MODE_IX0 (Byte 〈x7,x4〉) 〈x0,x4〉
+; quadruple … LSR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x4〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_26 ≝
+[
+ quadruple … MOV MODE_DIR1_to_DIR1 (Byte 〈x4,xE〉) 〈x0,x5〉
+; quadruple … MOV MODE_DIR1_to_IX0p (Byte 〈x5,xE〉) 〈x0,x5〉
+; quadruple … MOV MODE_IMM1_to_DIR1 (Byte 〈x6,xE〉) 〈x0,x4〉
+; quadruple … MOV MODE_IX0p_to_DIR1 (Byte 〈x7,xE〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HCS08_27 ≝
+[
+ quadruple … NEG MODE_DIR1 (Byte 〈x3,x0〉) 〈x0,x5〉
+; quadruple … NEG MODE_INHA (Byte 〈x4,x0〉) 〈x0,x1〉
+; quadruple … NEG MODE_INHX (Byte 〈x5,x0〉) 〈x0,x1〉
+; quadruple … NEG MODE_IX1 (Byte 〈x6,x0〉) 〈x0,x5〉
+; quadruple … NEG MODE_IX0 (Byte 〈x7,x0〉) 〈x0,x4〉
+; quadruple … NEG MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x0〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_28 ≝
+[
+ quadruple … ORA MODE_IMM1 (Byte 〈xA,xA〉) 〈x0,x2〉
+; quadruple … ORA MODE_DIR1 (Byte 〈xB,xA〉) 〈x0,x3〉
+; quadruple … ORA MODE_DIR2 (Byte 〈xC,xA〉) 〈x0,x4〉
+; quadruple … ORA MODE_IX2 (Byte 〈xD,xA〉) 〈x0,x4〉
+; quadruple … ORA MODE_IX1 (Byte 〈xE,xA〉) 〈x0,x3〉
+; quadruple … ORA MODE_IX0 (Byte 〈xF,xA〉) 〈x0,x3〉
+; quadruple … ORA MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xA〉〉) 〈x0,x5〉
+; quadruple … ORA MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xA〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_29 ≝
+[
+ quadruple … ROL MODE_DIR1 (Byte 〈x3,x9〉) 〈x0,x5〉
+; quadruple … ROL MODE_INHA (Byte 〈x4,x9〉) 〈x0,x1〉
+; quadruple … ROL MODE_INHX (Byte 〈x5,x9〉) 〈x0,x1〉
+; quadruple … ROL MODE_IX1 (Byte 〈x6,x9〉) 〈x0,x5〉
+; quadruple … ROL MODE_IX0 (Byte 〈x7,x9〉) 〈x0,x4〉
+; quadruple … ROL MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x9〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_30 ≝
+[
+ quadruple … ROR MODE_DIR1 (Byte 〈x3,x6〉) 〈x0,x5〉
+; quadruple … ROR MODE_INHA (Byte 〈x4,x6〉) 〈x0,x1〉
+; quadruple … ROR MODE_INHX (Byte 〈x5,x6〉) 〈x0,x1〉
+; quadruple … ROR MODE_IX1 (Byte 〈x6,x6〉) 〈x0,x5〉
+; quadruple … ROR MODE_IX0 (Byte 〈x7,x6〉) 〈x0,x4〉
+; quadruple … ROR MODE_SP1 (Word 〈〈x9,xE〉:〈x6,x6〉〉) 〈x0,x6〉
+].
+
+ndefinition opcode_table_HCS08_31 ≝
+[
+ quadruple … SBC MODE_IMM1 (Byte 〈xA,x2〉) 〈x0,x2〉
+; quadruple … SBC MODE_DIR1 (Byte 〈xB,x2〉) 〈x0,x3〉
+; quadruple … SBC MODE_DIR2 (Byte 〈xC,x2〉) 〈x0,x4〉
+; quadruple … SBC MODE_IX2 (Byte 〈xD,x2〉) 〈x0,x4〉
+; quadruple … SBC MODE_IX1 (Byte 〈xE,x2〉) 〈x0,x3〉
+; quadruple … SBC MODE_IX0 (Byte 〈xF,x2〉) 〈x0,x3〉
+; quadruple … SBC MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x2〉〉) 〈x0,x5〉
+; quadruple … SBC MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x2〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_32 ≝
+[
+ quadruple … STA MODE_DIR1 (Byte 〈xB,x7〉) 〈x0,x3〉
+; quadruple … STA MODE_DIR2 (Byte 〈xC,x7〉) 〈x0,x4〉
+; quadruple … STA MODE_IX2 (Byte 〈xD,x7〉) 〈x0,x4〉
+; quadruple … STA MODE_IX1 (Byte 〈xE,x7〉) 〈x0,x3〉
+; quadruple … STA MODE_IX0 (Byte 〈xF,x7〉) 〈x0,x2〉
+; quadruple … STA MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x7〉〉) 〈x0,x5〉
+; quadruple … STA MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x7〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_33 ≝
+[
+ quadruple … STX MODE_DIR1 (Byte 〈xB,xF〉) 〈x0,x3〉
+; quadruple … STX MODE_DIR2 (Byte 〈xC,xF〉) 〈x0,x4〉
+; quadruple … STX MODE_IX2 (Byte 〈xD,xF〉) 〈x0,x4〉
+; quadruple … STX MODE_IX1 (Byte 〈xE,xF〉) 〈x0,x3〉
+; quadruple … STX MODE_IX0 (Byte 〈xF,xF〉) 〈x0,x2〉
+; quadruple … STX MODE_SP2 (Word 〈〈x9,xE〉:〈xD,xF〉〉) 〈x0,x5〉
+; quadruple … STX MODE_SP1 (Word 〈〈x9,xE〉:〈xE,xF〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_34 ≝
+[
+ quadruple … SUB MODE_IMM1 (Byte 〈xA,x0〉) 〈x0,x2〉
+; quadruple … SUB MODE_DIR1 (Byte 〈xB,x0〉) 〈x0,x3〉
+; quadruple … SUB MODE_DIR2 (Byte 〈xC,x0〉) 〈x0,x4〉
+; quadruple … SUB MODE_IX2 (Byte 〈xD,x0〉) 〈x0,x4〉
+; quadruple … SUB MODE_IX1 (Byte 〈xE,x0〉) 〈x0,x3〉
+; quadruple … SUB MODE_IX0 (Byte 〈xF,x0〉) 〈x0,x3〉
+; quadruple … SUB MODE_SP2 (Word 〈〈x9,xE〉:〈xD,x0〉〉) 〈x0,x5〉
+; quadruple … SUB MODE_SP1 (Word 〈〈x9,xE〉:〈xE,x0〉〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_HCS08_35 ≝
+[
+ quadruple … TST MODE_DIR1 (Byte 〈x3,xD〉) 〈x0,x4〉
+; quadruple … TST MODE_INHA (Byte 〈x4,xD〉) 〈x0,x1〉
+; quadruple … TST MODE_INHX (Byte 〈x5,xD〉) 〈x0,x1〉
+; quadruple … TST MODE_IX1 (Byte 〈x6,xD〉) 〈x0,x4〉
+; quadruple … TST MODE_IX0 (Byte 〈x7,xD〉) 〈x0,x3〉
+; quadruple … TST MODE_SP1 (Word 〈〈x9,xE〉:〈x6,xD〉〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_HCS08 ≝
+opcode_table_HCS08_1 @ opcode_table_HCS08_2 @ opcode_table_HCS08_3 @ opcode_table_HCS08_4 @
+opcode_table_HCS08_5 @ opcode_table_HCS08_6 @ opcode_table_HCS08_7 @ opcode_table_HCS08_8 @
+opcode_table_HCS08_9 @ opcode_table_HCS08_10 @ opcode_table_HCS08_11 @ opcode_table_HCS08_12 @
+opcode_table_HCS08_13 @ opcode_table_HCS08_14 @ opcode_table_HCS08_15 @ opcode_table_HCS08_16 @
+opcode_table_HCS08_17 @ opcode_table_HCS08_18 @ opcode_table_HCS08_19 @ opcode_table_HCS08_20 @
+opcode_table_HCS08_21 @ opcode_table_HCS08_22 @ opcode_table_HCS08_23 @ opcode_table_HCS08_24 @
+opcode_table_HCS08_25 @ opcode_table_HCS08_26 @ opcode_table_HCS08_27 @ opcode_table_HCS08_28 @
+opcode_table_HCS08_29 @ opcode_table_HCS08_30 @ opcode_table_HCS08_31 @ opcode_table_HCS08_32 @
+opcode_table_HCS08_33 @ opcode_table_HCS08_34 @ opcode_table_HCS08_35.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/IP2022_instr_mode_base.ma".
+
+nlemma eq_to_eqIP2022im : ∀n1,n2.n1 = n2 → eq_IP2022_im n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
+ ##[ ##4,11,12: #o; nrewrite > (eq_to_eqoct … (refl_eq …))
+ ##| ##6: #t; nrewrite > (eq_to_eqbit … (refl_eq …)) ##]
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma neqIP2022im_to_neq : ∀n1,n2.eq_IP2022_im n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_IP2022_im n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqIP2022im n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
+(* !!! per brevita... *)
+naxiom eqIP2022im_to_eq : ∀c1,c2.eq_IP2022_im c1 c2 = true → c1 = c2.
+
+nlemma neq_to_neqIP2022im : ∀n1,n2.n1 ≠ n2 → eq_IP2022_im n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_IP2022_im n1 n2));
+ napply (not_to_not (eq_IP2022_im n1 n2 = true) (n1 = n2) ? H);
+ napply (eqIP2022im_to_eq n1 n2).
+nqed.
+
+nlemma decidable_IP2022im : ∀x,y:IP2022_instr_mode.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_IP2022_im x y = true) (eq_IP2022_im x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqIP2022im_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqIP2022im_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqIP2022im : symmetricT IP2022_instr_mode bool eq_IP2022_im.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_IP2022im n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqIP2022im n1 n2 H);
+ napply (symmetric_eq ? (eq_IP2022_im n2 n1) false);
+ napply (neq_to_neqIP2022im n2 n1 (symmetric_neq ? n1 n2 H))
+ ##]
+nqed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/oct.ma".
+include "num/bitrigesim.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+(* enumerazione delle modalita' di indirizzamento = caricamento degli operandi *)
+ninductive IP2022_instr_mode: Type ≝
+ (* nessun operando : formato xxxxxxxx xxxxxxxx *)
+ MODE_INH : IP2022_instr_mode
+ (* operando implicito [ADDR] : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDR : IP2022_instr_mode
+ (* operando implicito [ADDR]/ADDR+=2 : formato xxxxxxxx xxxxxxxx *)
+| MODE_INHADDRpp : IP2022_instr_mode
+
+ (* #lit3 → / : formato xxxxxxxx xxxxxkkk *)
+| MODE_IMM3 : oct → IP2022_instr_mode
+ (* W, #lit8 → W : formato xxxxxxxx kkkkkkkk [load 1 byte arg] *)
+| MODE_IMM8 : IP2022_instr_mode
+ (* #lit13 → / : formato xxxkkkkk kkkkkkkk [load 1 byte arg] *)
+| MODE_IMM13 : bitrigesim → IP2022_instr_mode
+
+ (* FR, W → FR : formato xxxxxxx0 ffffffff [load 1 byte arg] *)
+| MODE_FR0_and_W : IP2022_instr_mode
+ (* FR, W → FR : formato xxxxxxx1 ffffffff [load 1 byte arg] *)
+| MODE_FR1_and_W : IP2022_instr_mode
+ (* W, FR → W : formato xxxxxxx0 ffffffff [load 1 byte arg] *)
+| MODE_W_and_FR0 : IP2022_instr_mode
+ (* W, FR → W : formato xxxxxxx1 ffffffff [load 1 byte arg] *)
+| MODE_W_and_FR1 : IP2022_instr_mode
+
+ (* FR(bitN) → FR(bitN) : formato xxxxbbb0 ffffffff [load 1 byte arg] *)
+| MODE_FR0n : oct → IP2022_instr_mode
+ (* FR(bitN) → FR(bitN) : formato xxxxbbb1 ffffffff [load 1 byte arg] *)
+| MODE_FR1n : oct → IP2022_instr_mode
+.
+
+ndefinition eq_IP2022_im ≝
+λi1,i2:IP2022_instr_mode.
+ match i1 with
+ [ MODE_INH ⇒ match i2 with [ MODE_INH ⇒ true | _ ⇒ false ]
+ | MODE_INHADDR ⇒ match i2 with [ MODE_INHADDR ⇒ true | _ ⇒ false ]
+ | MODE_INHADDRpp ⇒ match i2 with [ MODE_INHADDRpp ⇒ true | _ ⇒ false ]
+ | MODE_IMM3 o1 ⇒ match i2 with [ MODE_IMM3 o2 ⇒ eqc ? o1 o2 | _ ⇒ false ]
+ | MODE_IMM8 ⇒ match i2 with [ MODE_IMM8 ⇒ true | _ ⇒ false ]
+ | MODE_IMM13 t1 ⇒ match i2 with [ MODE_IMM13 t2 ⇒ eqc ? t1 t2 | _ ⇒ false ]
+ | MODE_FR0_and_W ⇒ match i2 with [ MODE_FR0_and_W ⇒ true | _ ⇒ false ]
+ | MODE_FR1_and_W ⇒ match i2 with [ MODE_FR1_and_W ⇒ true | _ ⇒ false ]
+ | MODE_W_and_FR0 ⇒ match i2 with [ MODE_W_and_FR0 ⇒ true | _ ⇒ false ]
+ | MODE_W_and_FR1 ⇒ match i2 with [ MODE_W_and_FR1 ⇒ true | _ ⇒ false ]
+ | MODE_FR0n o1 ⇒ match i2 with [ MODE_FR0n o2 ⇒ eqc ? o1 o2 | _ ⇒ false ]
+ | MODE_FR1n o1 ⇒ match i2 with [ MODE_FR1n o2 ⇒ eqc ? o1 o2 | _ ⇒ false ]
+ ].
+
+ndefinition forall_IP2022_im ≝ λP:IP2022_instr_mode → bool.
+ P MODE_INH
+⊗ P MODE_INHADDR
+⊗ P MODE_INHADDRpp
+⊗ forallc ? (λo.P (MODE_IMM3 o))
+⊗ P MODE_IMM8
+⊗ forallc ? (λt.P (MODE_IMM13 t))
+⊗ P MODE_FR0_and_W
+⊗ P MODE_FR1_and_W
+⊗ P MODE_W_and_FR0
+⊗ P MODE_W_and_FR1
+⊗ forallc ? (λo.P (MODE_FR0n o))
+⊗ forallc ? (λo.P (MODE_FR1n o)).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/IP2022_pseudo_base.ma".
+include "common/comp.ma".
+include "num/bool_lemmas.ma".
+
+nlemma eq_to_eqIP2022pseudo : ∀n1,n2.n1 = n2 → eq_IP2022_pseudo n1 n2 = true.
+ #n1; #n2; #H;
+ nrewrite > H;
+ nelim n2;
+ nnormalize;
+ napply refl_eq.
+nqed.
+
+nlemma neqIP2022pseudo_to_neq : ∀n1,n2.eq_IP2022_pseudo n1 n2 = false → n1 ≠ n2.
+ #n1; #n2; #H;
+ napply (not_to_not (n1 = n2) (eq_IP2022_pseudo n1 n2 = true) …);
+ ##[ ##1: napply (eq_to_eqIP2022pseudo n1 n2)
+ ##| ##2: napply (eqfalse_to_neqtrue … H)
+ ##]
+nqed.
+
+(* !!! per brevita... *)
+naxiom eqIP2022pseudo_to_eq : ∀c1,c2.eq_IP2022_pseudo c1 c2 = true → c1 = c2.
+
+nlemma neq_to_neqIP2022pseudo : ∀n1,n2.n1 ≠ n2 → eq_IP2022_pseudo n1 n2 = false.
+ #n1; #n2; #H;
+ napply (neqtrue_to_eqfalse (eq_IP2022_pseudo n1 n2));
+ napply (not_to_not (eq_IP2022_pseudo n1 n2 = true) (n1 = n2) ? H);
+ napply (eqIP2022pseudo_to_eq n1 n2).
+nqed.
+
+nlemma decidable_IP2022pseudo : ∀x,y:IP2022_pseudo.decidable (x = y).
+ #x; #y; nnormalize;
+ napply (or2_elim (eq_IP2022_pseudo x y = true) (eq_IP2022_pseudo x y = false) ? (decidable_bexpr ?));
+ ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqIP2022pseudo_to_eq … H))
+ ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqIP2022pseudo_to_neq … H))
+ ##]
+nqed.
+
+nlemma symmetric_eqIP2022pseudo : symmetricT IP2022_pseudo bool eq_IP2022_pseudo.
+ #n1; #n2;
+ napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_IP2022pseudo n1 n2));
+ ##[ ##1: #H; nrewrite > H; napply refl_eq
+ ##| ##2: #H; nrewrite > (neq_to_neqIP2022pseudo n1 n2 H);
+ napply (symmetric_eq ? (eq_IP2022_pseudo n2 n1) false);
+ napply (neq_to_neqIP2022pseudo n2 n1 (symmetric_neq ? n1 n2 H))
+ ##]
+nqed.
+
+nlemma IP2022pseudo_is_comparable : comparable.
+ @ IP2022_pseudo
+ ##[ napply ADD
+ ##| napply forall_IP2022_pseudo
+ ##| napply eq_IP2022_pseudo
+ ##| napply eqIP2022pseudo_to_eq
+ ##| napply eq_to_eqIP2022pseudo
+ ##| napply neqIP2022pseudo_to_neq
+ ##| napply neq_to_neqIP2022pseudo
+ ##| napply decidable_IP2022pseudo
+ ##| napply symmetric_eqIP2022pseudo
+ ##]
+nqed.
+
+unification hint 0 ≔ ⊢ carr IP2022pseudo_is_comparable ≡ IP2022_pseudo.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/bool.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+(* enumerazione delle istruzioni *)
+ninductive IP2022_pseudo: Type ≝
+ ADD : IP2022_pseudo (* add *)
+| ADDC : IP2022_pseudo (* add with carry *)
+| AND : IP2022_pseudo (* and *)
+| BREAK : IP2022_pseudo (* enter break mode *)
+| BREAKX : IP2022_pseudo (* enter break mode, after skip *)
+| CALL : IP2022_pseudo (* subroutine call *)
+| CLR : IP2022_pseudo (* clear *)
+| CLRB : IP2022_pseudo (* clear bit *)
+| CMP : IP2022_pseudo (* set flags according to sub *)
+| CSE : IP2022_pseudo (* confront & skip if equal *)
+| CSNE : IP2022_pseudo (* confront & skip if not equal *)
+| CWDT : IP2022_pseudo (* clear watch dog -- not impl. ERR *)
+| DEC : IP2022_pseudo (* decrement *)
+| DECSNZ : IP2022_pseudo (* decrement & skip if not zero *)
+| DECSZ : IP2022_pseudo (* decrement & skip if zero *)
+| FERASE : IP2022_pseudo (* flash erase -- not impl. ERR *)
+| FREAD : IP2022_pseudo (* flash read -- not impl. ERR *)
+| FWRITE : IP2022_pseudo (* flash write -- not impl. ERR *)
+| INC : IP2022_pseudo (* increment *)
+| INCSNZ : IP2022_pseudo (* increment & skip if not zero *)
+| INCSZ : IP2022_pseudo (* increment & skip if zero *)
+| INT : IP2022_pseudo (* interrupt -- not impl. ERR *)
+| IREAD : IP2022_pseudo (* memory read *)
+(* NB: ignorata la differenza IREAD/IREADI perche' non e' implementata EXT_MEM
+ IREAD → ADDRX= 0x00 ram, 0x01 flash, 0x80 0x81 ext_mem
+ IREADI → ADDRX= 0x00 ram, 0x01 flash *)
+| IWRITE : IP2022_pseudo (* memory write *)
+(* NB: ignorata la differenza IWRITE/IWRITEI perche' non e' implementata EXT_MEM
+ IREAD → ADDRX= 0x00 ram, 0x80 0x81 ext_mem
+ IREADI → ADDRX= 0x00 ram *)
+| JMP : IP2022_pseudo (* jump *)
+| LOADH : IP2022_pseudo (* load Data Pointer High *)
+| LOADL : IP2022_pseudo (* load Data Pointer Low *)
+| MOV : IP2022_pseudo (* move *)
+| MULS : IP2022_pseudo (* signed mul *)
+| MULU : IP2022_pseudo (* unsigned mul *)
+| NOP : IP2022_pseudo (* nop *)
+| NOT : IP2022_pseudo (* not *)
+| OR : IP2022_pseudo (* or *)
+| PAGE : IP2022_pseudo (* set Page Register *)
+| POP : IP2022_pseudo (* pop *)
+| PUSH : IP2022_pseudo (* push *)
+| RET : IP2022_pseudo (* subroutine ret *)
+| RETI : IP2022_pseudo (* interrupt ret -- not impl. ERR *)
+| RETNP : IP2022_pseudo (* subroutine ret & don't restore Page Register *)
+| RETW : IP2022_pseudo (* subroutine ret & load W Register *)
+| RL : IP2022_pseudo (* rotate left *)
+| RR : IP2022_pseudo (* rotate right *)
+| SB : IP2022_pseudo (* skip if bit set *)
+| SETB : IP2022_pseudo (* set bit *)
+| SNB : IP2022_pseudo (* skip if bit not set *)
+| SPEED : IP2022_pseudo (* set Speed Register *)
+| SUB : IP2022_pseudo (* sub *)
+| SUBC : IP2022_pseudo (* sub with carry *)
+| SWAP : IP2022_pseudo (* swap xxxxyyyy → yyyyxxxx *)
+| TEST : IP2022_pseudo (* set flags according to zero test *)
+| XOR : IP2022_pseudo (* xor *)
+.
+
+ndefinition eq_IP2022_pseudo ≝
+λps1,ps2:IP2022_pseudo.
+ match ps1 with
+ [ ADD ⇒ match ps2 with [ ADD ⇒ true | _ ⇒ false ] | ADDC ⇒ match ps2 with [ ADDC ⇒ true | _ ⇒ false ]
+ | AND ⇒ match ps2 with [ AND ⇒ true | _ ⇒ false ] | BREAK ⇒ match ps2 with [ BREAK ⇒ true | _ ⇒ false ]
+ | BREAKX ⇒ match ps2 with [ BREAKX ⇒ true | _ ⇒ false ] | CALL ⇒ match ps2 with [ CALL ⇒ true | _ ⇒ false ]
+ | CLR ⇒ match ps2 with [ CLR ⇒ true | _ ⇒ false ] | CLRB ⇒ match ps2 with [ CLRB ⇒ true | _ ⇒ false ]
+ | CMP ⇒ match ps2 with [ CMP ⇒ true | _ ⇒ false ] | CSE ⇒ match ps2 with [ CSE ⇒ true | _ ⇒ false ]
+ | CSNE ⇒ match ps2 with [ CSNE ⇒ true | _ ⇒ false ] | CWDT ⇒ match ps2 with [ CWDT ⇒ true | _ ⇒ false ]
+ | DEC ⇒ match ps2 with [ DEC ⇒ true | _ ⇒ false ] | DECSNZ ⇒ match ps2 with [ DECSNZ ⇒ true | _ ⇒ false ]
+ | DECSZ ⇒ match ps2 with [ DECSZ ⇒ true | _ ⇒ false ] | FERASE ⇒ match ps2 with [ FERASE ⇒ true | _ ⇒ false ]
+ | FREAD ⇒ match ps2 with [ FREAD ⇒ true | _ ⇒ false ] | FWRITE ⇒ match ps2 with [ FWRITE ⇒ true | _ ⇒ false ]
+ | INC ⇒ match ps2 with [ INC ⇒ true | _ ⇒ false ] | INCSNZ ⇒ match ps2 with [ INCSNZ ⇒ true | _ ⇒ false ]
+ | INCSZ ⇒ match ps2 with [ INCSZ ⇒ true | _ ⇒ false ] | INT ⇒ match ps2 with [ INT ⇒ true | _ ⇒ false ]
+ | IREAD ⇒ match ps2 with [ IREAD ⇒ true | _ ⇒ false ] | IWRITE ⇒ match ps2 with [ IWRITE ⇒ true | _ ⇒ false ]
+ | JMP ⇒ match ps2 with [ JMP ⇒ true | _ ⇒ false ] | LOADH ⇒ match ps2 with [ LOADH ⇒ true | _ ⇒ false ]
+ | LOADL ⇒ match ps2 with [ LOADL ⇒ true | _ ⇒ false ] | MOV ⇒ match ps2 with [ MOV ⇒ true | _ ⇒ false ]
+ | MULS ⇒ match ps2 with [ MULS ⇒ true | _ ⇒ false ] | MULU ⇒ match ps2 with [ MULU ⇒ true | _ ⇒ false ]
+ | NOP ⇒ match ps2 with [ NOP ⇒ true | _ ⇒ false ] | NOT ⇒ match ps2 with [ NOT ⇒ true | _ ⇒ false ]
+ | OR ⇒ match ps2 with [ OR ⇒ true | _ ⇒ false ] | PAGE ⇒ match ps2 with [ PAGE ⇒ true | _ ⇒ false ]
+ | POP ⇒ match ps2 with [ POP ⇒ true | _ ⇒ false ] | PUSH ⇒ match ps2 with [ PUSH ⇒ true | _ ⇒ false ]
+ | RET ⇒ match ps2 with [ RET ⇒ true | _ ⇒ false ] | RETI ⇒ match ps2 with [ RETI ⇒ true | _ ⇒ false ]
+ | RETNP ⇒ match ps2 with [ RETNP ⇒ true | _ ⇒ false ] | RETW ⇒ match ps2 with [ RETW ⇒ true | _ ⇒ false ]
+ | RL ⇒ match ps2 with [ RL ⇒ true | _ ⇒ false ] | RR ⇒ match ps2 with [ RR ⇒ true | _ ⇒ false ]
+ | SB ⇒ match ps2 with [ SB ⇒ true | _ ⇒ false ] | SETB ⇒ match ps2 with [ SETB ⇒ true | _ ⇒ false ]
+ | SNB ⇒ match ps2 with [ SNB ⇒ true | _ ⇒ false ] | SPEED ⇒ match ps2 with [ SPEED ⇒ true | _ ⇒ false ]
+ | SUB ⇒ match ps2 with [ SUB ⇒ true | _ ⇒ false ] | SUBC ⇒ match ps2 with [ SUBC ⇒ true | _ ⇒ false ]
+ | SWAP ⇒ match ps2 with [ SWAP ⇒ true | _ ⇒ false ] | TEST ⇒ match ps2 with [ TEST ⇒ true | _ ⇒ false ]
+ | XOR ⇒ match ps2 with [ XOR ⇒ true | _ ⇒ false ]
+ ].
+
+ndefinition forall_IP2022_pseudo ≝ λP:IP2022_pseudo → bool.
+ P ADD ⊗ P ADDC ⊗ P AND ⊗ P BREAK ⊗ P BREAKX ⊗ P CALL ⊗ P CLR ⊗ P CLRB ⊗
+ P CMP ⊗ P CSE ⊗ P CSNE ⊗ P CWDT ⊗ P DEC ⊗ P DECSNZ ⊗ P DECSZ ⊗ P FERASE ⊗
+ P FREAD ⊗ P FWRITE ⊗ P INC ⊗ P INCSNZ ⊗ P INCSZ ⊗ P INT ⊗ P IREAD ⊗ P IWRITE ⊗
+ P JMP ⊗ P LOADH ⊗ P LOADL ⊗ P MOV ⊗ P MULS ⊗ P MULU ⊗ P NOP ⊗ P NOT ⊗
+ P OR ⊗ P PAGE ⊗ P POP ⊗ P PUSH ⊗ P RET ⊗ P RETI ⊗ P RETNP ⊗ P RETW ⊗
+ P RL ⊗ P RR ⊗ P SB ⊗ P SETB ⊗ P SNB ⊗ P SPEED ⊗ P SUB ⊗ P SUBC ⊗
+ P SWAP ⊗ P TEST ⊗ P XOR.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/IP2022_pseudo.ma".
+include "emulator/opcodes/IP2022_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ******************* *)
+(* TABELLA DELL'IP2022 *)
+(* ******************* *)
+
+(* definizione come concatenazione finale di liste per velocizzare il parsing *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
+
+ndefinition opcode_table_IP2022_1 ≝
+[
+ quadruple … ADD MODE_FR0_and_W (Byte 〈x1,xE〉) 〈x0,x1〉
+; quadruple … ADD MODE_FR1_and_W (Byte 〈x1,xF〉) 〈x0,x1〉
+; quadruple … ADD MODE_W_and_FR0 (Byte 〈x1,xC〉) 〈x0,x1〉
+; quadruple … ADD MODE_W_and_FR1 (Byte 〈x1,xD〉) 〈x0,x1〉
+; quadruple … ADD MODE_IMM8 (Byte 〈x7,xB〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_2 ≝
+[
+ quadruple … ADDC MODE_FR0_and_W (Byte 〈x5,xE〉) 〈x0,x1〉
+; quadruple … ADDC MODE_FR1_and_W (Byte 〈x5,xF〉) 〈x0,x1〉
+; quadruple … ADDC MODE_W_and_FR0 (Byte 〈x5,xC〉) 〈x0,x1〉
+; quadruple … ADDC MODE_W_and_FR1 (Byte 〈x5,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_3 ≝
+[
+ quadruple … AND MODE_FR0_and_W (Byte 〈x1,x6〉) 〈x0,x1〉
+; quadruple … AND MODE_FR1_and_W (Byte 〈x1,x7〉) 〈x0,x1〉
+; quadruple … AND MODE_W_and_FR0 (Byte 〈x1,x4〉) 〈x0,x1〉
+; quadruple … AND MODE_W_and_FR1 (Byte 〈x1,x5〉) 〈x0,x1〉
+; quadruple … AND MODE_IMM8 (Byte 〈x7,xE〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_4 ≝
+[
+ quadruple … BREAK MODE_INH (Word 〈〈x0,x0〉:〈x0,x1〉〉) 〈x0,x1〉
+; quadruple … BREAKX MODE_INH (Word 〈〈x0,x0〉:〈x0,x5〉〉) 〈x0,x1〉
+; quadruple … CWDT MODE_INH (Word 〈〈x0,x0〉:〈x0,x4〉〉) 〈x0,x1〉
+; quadruple … FERASE MODE_INH (Word 〈〈x0,x0〉:〈x0,x3〉〉) 〈x0,x1〉
+; quadruple … FREAD MODE_INH (Word 〈〈x0,x0〉:〈x1,xB〉〉) 〈x0,x1〉
+; quadruple … FWRITE MODE_INH (Word 〈〈x0,x0〉:〈x1,xA〉〉) 〈x0,x1〉
+; quadruple … INT MODE_INH (Word 〈〈x0,x0〉:〈x0,x6〉〉) 〈x0,x3〉
+; quadruple … IREAD MODE_INHADDR (Word 〈〈x0,x0〉:〈x1,x9〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … IREAD MODE_INHADDRpp (Word 〈〈x0,x0〉:〈x1,xD〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … IWRITE MODE_INHADDR (Word 〈〈x0,x0〉:〈x1,x8〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … IWRITE MODE_INHADDRpp (Word 〈〈x0,x0〉:〈x1,xC〉〉) 〈x0,x4〉 (* only blocking implemented *)
+; quadruple … NOP MODE_INH (Word 〈〈x0,x0〉:〈x0,x0〉〉) 〈x0,x1〉
+; quadruple … RET MODE_INH (Word 〈〈x0,x0〉:〈x0,x7〉〉) 〈x0,x3〉
+; quadruple … RETNP MODE_INH (Word 〈〈x0,x0〉:〈x0,x2〉〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_5 ≝
+[
+ quadruple … CALL (MODE_IMM13 t00) (Byte 〈xC,x0〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t01) (Byte 〈xC,x1〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t02) (Byte 〈xC,x2〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t03) (Byte 〈xC,x3〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t04) (Byte 〈xC,x4〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t05) (Byte 〈xC,x5〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t06) (Byte 〈xC,x6〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t07) (Byte 〈xC,x7〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t08) (Byte 〈xC,x8〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t09) (Byte 〈xC,x9〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0A) (Byte 〈xC,xA〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0B) (Byte 〈xC,xB〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0C) (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0D) (Byte 〈xC,xD〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0E) (Byte 〈xC,xE〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t0F) (Byte 〈xC,xF〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t10) (Byte 〈xD,x0〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t11) (Byte 〈xD,x1〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t12) (Byte 〈xD,x2〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t13) (Byte 〈xD,x3〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t14) (Byte 〈xD,x4〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t15) (Byte 〈xD,x5〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t16) (Byte 〈xD,x6〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t17) (Byte 〈xD,x7〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t18) (Byte 〈xD,x8〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t19) (Byte 〈xD,x9〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1A) (Byte 〈xD,xA〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1B) (Byte 〈xD,xB〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1C) (Byte 〈xD,xC〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1D) (Byte 〈xD,xD〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1E) (Byte 〈xD,xE〉) 〈x0,x3〉
+; quadruple … CALL (MODE_IMM13 t1F) (Byte 〈xD,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_6 ≝
+[
+ quadruple … CLR MODE_FR0_and_W (Byte 〈x0,x6〉) 〈x0,x1〉
+; quadruple … CLR MODE_FR1_and_W (Byte 〈x0,x7〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_7 ≝
+[
+ quadruple … CLRB (MODE_FR0n o0) (Byte 〈x8,x0〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o0) (Byte 〈x8,x1〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o1) (Byte 〈x8,x2〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o1) (Byte 〈x8,x3〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o2) (Byte 〈x8,x4〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o2) (Byte 〈x8,x5〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o3) (Byte 〈x8,x6〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o3) (Byte 〈x8,x7〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o4) (Byte 〈x8,x8〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o4) (Byte 〈x8,x9〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o5) (Byte 〈x8,xA〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o5) (Byte 〈x8,xB〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o6) (Byte 〈x8,xC〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o6) (Byte 〈x8,xD〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR0n o7) (Byte 〈x8,xE〉) 〈x0,x1〉
+; quadruple … CLRB (MODE_FR1n o7) (Byte 〈x8,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_8 ≝
+[
+ quadruple … CMP MODE_W_and_FR0 (Byte 〈x0,x4〉) 〈x0,x1〉
+; quadruple … CMP MODE_W_and_FR1 (Byte 〈x0,x5〉) 〈x0,x1〉
+; quadruple … CMP MODE_IMM8 (Byte 〈x7,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_9 ≝
+[
+ quadruple … CSE MODE_W_and_FR0 (Byte 〈x4,x2〉) 〈x0,x1〉
+; quadruple … CSE MODE_W_and_FR1 (Byte 〈x4,x3〉) 〈x0,x1〉
+; quadruple … CSE MODE_IMM8 (Byte 〈x7,x7〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_10 ≝
+[
+ quadruple … CSNE MODE_W_and_FR0 (Byte 〈x4,x0〉) 〈x0,x1〉
+; quadruple … CSNE MODE_W_and_FR1 (Byte 〈x4,x1〉) 〈x0,x1〉
+; quadruple … CSNE MODE_IMM8 (Byte 〈x7,x6〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_11 ≝
+[
+ quadruple … DEC MODE_FR0_and_W (Byte 〈x0,xE〉) 〈x0,x1〉
+; quadruple … DEC MODE_FR1_and_W (Byte 〈x0,xF〉) 〈x0,x1〉
+; quadruple … DEC MODE_W_and_FR0 (Byte 〈x0,xC〉) 〈x0,x1〉
+; quadruple … DEC MODE_W_and_FR1 (Byte 〈x0,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_12 ≝
+[
+ quadruple … DECSNZ MODE_FR0_and_W (Byte 〈x4,xE〉) 〈x0,x1〉
+; quadruple … DECSNZ MODE_FR1_and_W (Byte 〈x4,xF〉) 〈x0,x1〉
+; quadruple … DECSNZ MODE_W_and_FR0 (Byte 〈x4,xC〉) 〈x0,x1〉
+; quadruple … DECSNZ MODE_W_and_FR1 (Byte 〈x4,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_13 ≝
+[
+ quadruple … DECSZ MODE_FR0_and_W (Byte 〈x2,xE〉) 〈x0,x1〉
+; quadruple … DECSZ MODE_FR1_and_W (Byte 〈x2,xF〉) 〈x0,x1〉
+; quadruple … DECSZ MODE_W_and_FR0 (Byte 〈x2,xC〉) 〈x0,x1〉
+; quadruple … DECSZ MODE_W_and_FR1 (Byte 〈x2,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_14 ≝
+[
+ quadruple … INC MODE_FR0_and_W (Byte 〈x2,xA〉) 〈x0,x1〉
+; quadruple … INC MODE_FR1_and_W (Byte 〈x2,xB〉) 〈x0,x1〉
+; quadruple … INC MODE_W_and_FR0 (Byte 〈x2,x8〉) 〈x0,x1〉
+; quadruple … INC MODE_W_and_FR1 (Byte 〈x2,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_15 ≝
+[
+ quadruple … INCSNZ MODE_FR0_and_W (Byte 〈x5,xA〉) 〈x0,x1〉
+; quadruple … INCSNZ MODE_FR1_and_W (Byte 〈x5,xB〉) 〈x0,x1〉
+; quadruple … INCSNZ MODE_W_and_FR0 (Byte 〈x5,x8〉) 〈x0,x1〉
+; quadruple … INCSNZ MODE_W_and_FR1 (Byte 〈x5,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_16 ≝
+[
+ quadruple … INCSZ MODE_FR0_and_W (Byte 〈x3,xE〉) 〈x0,x1〉
+; quadruple … INCSZ MODE_FR1_and_W (Byte 〈x3,xF〉) 〈x0,x1〉
+; quadruple … INCSZ MODE_W_and_FR0 (Byte 〈x3,xC〉) 〈x0,x1〉
+; quadruple … INCSZ MODE_W_and_FR1 (Byte 〈x3,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_17 ≝
+[
+ quadruple … JMP (MODE_IMM13 t00) (Byte 〈xE,x0〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t01) (Byte 〈xE,x1〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t02) (Byte 〈xE,x2〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t03) (Byte 〈xE,x3〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t04) (Byte 〈xE,x4〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t05) (Byte 〈xE,x5〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t06) (Byte 〈xE,x6〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t07) (Byte 〈xE,x7〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t08) (Byte 〈xE,x8〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t09) (Byte 〈xE,x9〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0A) (Byte 〈xE,xA〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0B) (Byte 〈xE,xB〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0C) (Byte 〈xE,xC〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0D) (Byte 〈xE,xD〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0E) (Byte 〈xE,xE〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t0F) (Byte 〈xE,xF〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t10) (Byte 〈xF,x0〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t11) (Byte 〈xF,x1〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t12) (Byte 〈xF,x2〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t13) (Byte 〈xF,x3〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t14) (Byte 〈xF,x4〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t15) (Byte 〈xF,x5〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t16) (Byte 〈xF,x6〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t17) (Byte 〈xF,x7〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t18) (Byte 〈xF,x8〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t19) (Byte 〈xF,x9〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1A) (Byte 〈xF,xA〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1B) (Byte 〈xF,xB〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1C) (Byte 〈xF,xC〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1D) (Byte 〈xF,xD〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1E) (Byte 〈xF,xE〉) 〈x0,x3〉
+; quadruple … JMP (MODE_IMM13 t1F) (Byte 〈xF,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_18 ≝
+[
+ quadruple … LOADH MODE_IMM8 (Byte 〈x7,x0〉) 〈x0,x1〉
+; quadruple … LOADL MODE_IMM8 (Byte 〈x7,x1〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_19 ≝
+[
+ quadruple … MOV MODE_FR0_and_W (Byte 〈x0,x2〉) 〈x0,x1〉
+; quadruple … MOV MODE_FR1_and_W (Byte 〈x0,x3〉) 〈x0,x1〉
+; quadruple … MOV MODE_W_and_FR0 (Byte 〈x2,x0〉) 〈x0,x1〉
+; quadruple … MOV MODE_W_and_FR1 (Byte 〈x2,x1〉) 〈x0,x1〉
+; quadruple … MOV MODE_IMM8 (Byte 〈x7,xC〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_20 ≝
+[
+ quadruple … MULS MODE_W_and_FR0 (Byte 〈x5,x4〉) 〈x0,x1〉
+; quadruple … MULS MODE_W_and_FR1 (Byte 〈x5,x5〉) 〈x0,x1〉
+; quadruple … MULS MODE_IMM8 (Byte 〈x7,x3〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_21 ≝
+[
+ quadruple … MULU MODE_W_and_FR0 (Byte 〈x5,x0〉) 〈x0,x1〉
+; quadruple … MULU MODE_W_and_FR1 (Byte 〈x5,x1〉) 〈x0,x1〉
+; quadruple … MULU MODE_IMM8 (Byte 〈x7,x2〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_22 ≝
+[
+ quadruple … NOT MODE_FR0_and_W (Byte 〈x2,x6〉) 〈x0,x1〉
+; quadruple … NOT MODE_FR1_and_W (Byte 〈x2,x7〉) 〈x0,x1〉
+; quadruple … NOT MODE_W_and_FR0 (Byte 〈x2,x4〉) 〈x0,x1〉
+; quadruple … NOT MODE_W_and_FR1 (Byte 〈x2,x5〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_23 ≝
+[
+ quadruple … OR MODE_FR0_and_W (Byte 〈x1,x2〉) 〈x0,x1〉
+; quadruple … OR MODE_FR1_and_W (Byte 〈x1,x3〉) 〈x0,x1〉
+; quadruple … OR MODE_W_and_FR0 (Byte 〈x1,x0〉) 〈x0,x1〉
+; quadruple … OR MODE_W_and_FR1 (Byte 〈x1,x1〉) 〈x0,x1〉
+; quadruple … OR MODE_IMM8 (Byte 〈x7,xD〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_24 ≝
+[
+ quadruple … PAGE (MODE_IMM3 o0) (Word 〈〈x0,x0〉:〈x1,x0〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o1) (Word 〈〈x0,x0〉:〈x1,x1〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o2) (Word 〈〈x0,x0〉:〈x1,x2〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o3) (Word 〈〈x0,x0〉:〈x1,x3〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o4) (Word 〈〈x0,x0〉:〈x1,x4〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o5) (Word 〈〈x0,x0〉:〈x1,x5〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o6) (Word 〈〈x0,x0〉:〈x1,x6〉〉) 〈x0,x1〉
+; quadruple … PAGE (MODE_IMM3 o7) (Word 〈〈x0,x0〉:〈x1,x7〉〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_25 ≝
+[
+ quadruple … POP MODE_FR0_and_W (Byte 〈x4,x6〉) 〈x0,x1〉
+; quadruple … POP MODE_FR1_and_W (Byte 〈x4,x7〉) 〈x0,x1〉
+; quadruple … PUSH MODE_W_and_FR0 (Byte 〈x4,x4〉) 〈x0,x1〉
+; quadruple … PUSH MODE_W_and_FR1 (Byte 〈x4,x5〉) 〈x0,x1〉
+; quadruple … PUSH MODE_IMM8 (Byte 〈x7,x4〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_26 ≝
+[
+ quadruple … RETI (MODE_IMM3 o0) (Word 〈〈x0,x0〉:〈x0,x8〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o1) (Word 〈〈x0,x0〉:〈x0,x9〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o2) (Word 〈〈x0,x0〉:〈x0,xA〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o3) (Word 〈〈x0,x0〉:〈x0,xB〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o4) (Word 〈〈x0,x0〉:〈x0,xC〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o5) (Word 〈〈x0,x0〉:〈x0,xD〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o6) (Word 〈〈x0,x0〉:〈x0,xE〉〉) 〈x0,x3〉
+; quadruple … RETI (MODE_IMM3 o7) (Word 〈〈x0,x0〉:〈x0,xF〉〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_IP2022_27 ≝
+[ quadruple … RETW MODE_IMM8 (Byte 〈x7,x8〉) 〈x0,x3〉 ].
+
+ndefinition opcode_table_IP2022_28 ≝
+[
+ quadruple … RL MODE_FR0_and_W (Byte 〈x3,x6〉) 〈x0,x1〉
+; quadruple … RL MODE_FR1_and_W (Byte 〈x3,x7〉) 〈x0,x1〉
+; quadruple … RL MODE_W_and_FR0 (Byte 〈x3,x4〉) 〈x0,x1〉
+; quadruple … RL MODE_W_and_FR1 (Byte 〈x3,x5〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_29 ≝
+[
+ quadruple … RR MODE_FR0_and_W (Byte 〈x3,x2〉) 〈x0,x1〉
+; quadruple … RR MODE_FR1_and_W (Byte 〈x3,x3〉) 〈x0,x1〉
+; quadruple … RR MODE_W_and_FR0 (Byte 〈x3,x0〉) 〈x0,x1〉
+; quadruple … RR MODE_W_and_FR1 (Byte 〈x3,x1〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_30 ≝
+[
+ quadruple … SB (MODE_FR0n o0) (Byte 〈xB,x0〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o0) (Byte 〈xB,x1〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o1) (Byte 〈xB,x2〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o1) (Byte 〈xB,x3〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o2) (Byte 〈xB,x4〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o2) (Byte 〈xB,x5〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o3) (Byte 〈xB,x6〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o3) (Byte 〈xB,x7〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o4) (Byte 〈xB,x8〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o4) (Byte 〈xB,x9〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o5) (Byte 〈xB,xA〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o5) (Byte 〈xB,xB〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o6) (Byte 〈xB,xC〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o6) (Byte 〈xB,xD〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR0n o7) (Byte 〈xB,xE〉) 〈x0,x1〉
+; quadruple … SB (MODE_FR1n o7) (Byte 〈xB,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_31 ≝
+[
+ quadruple … SETB (MODE_FR0n o0) (Byte 〈x9,x0〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o0) (Byte 〈x9,x1〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o1) (Byte 〈x9,x2〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o1) (Byte 〈x9,x3〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o2) (Byte 〈x9,x4〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o2) (Byte 〈x9,x5〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o3) (Byte 〈x9,x6〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o3) (Byte 〈x9,x7〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o4) (Byte 〈x9,x8〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o4) (Byte 〈x9,x9〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o5) (Byte 〈x9,xA〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o5) (Byte 〈x9,xB〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o6) (Byte 〈x9,xC〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o6) (Byte 〈x9,xD〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR0n o7) (Byte 〈x9,xE〉) 〈x0,x1〉
+; quadruple … SETB (MODE_FR1n o7) (Byte 〈x9,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_32 ≝
+[
+ quadruple … SNB (MODE_FR0n o0) (Byte 〈xA,x0〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o0) (Byte 〈xA,x1〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o1) (Byte 〈xA,x2〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o1) (Byte 〈xA,x3〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o2) (Byte 〈xA,x4〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o2) (Byte 〈xA,x5〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o3) (Byte 〈xA,x6〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o3) (Byte 〈xA,x7〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o4) (Byte 〈xA,x8〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o4) (Byte 〈xA,x9〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o5) (Byte 〈xA,xA〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o5) (Byte 〈xA,xB〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o6) (Byte 〈xA,xC〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o6) (Byte 〈xA,xD〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR0n o7) (Byte 〈xA,xE〉) 〈x0,x1〉
+; quadruple … SNB (MODE_FR1n o7) (Byte 〈xA,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_33 ≝
+[ quadruple … SPEED MODE_IMM8 (Byte 〈x0,x1〉) 〈x0,x1〉 ].
+
+ndefinition opcode_table_IP2022_34 ≝
+[
+ quadruple … SUB MODE_FR0_and_W (Byte 〈x0,xA〉) 〈x0,x1〉
+; quadruple … SUB MODE_FR1_and_W (Byte 〈x0,xB〉) 〈x0,x1〉
+; quadruple … SUB MODE_W_and_FR0 (Byte 〈x0,x8〉) 〈x0,x1〉
+; quadruple … SUB MODE_W_and_FR1 (Byte 〈x0,x9〉) 〈x0,x1〉
+; quadruple … SUB MODE_IMM8 (Byte 〈x7,xA〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_35 ≝
+[
+ quadruple … SUBC MODE_FR0_and_W (Byte 〈x4,xA〉) 〈x0,x1〉
+; quadruple … SUBC MODE_FR1_and_W (Byte 〈x4,xB〉) 〈x0,x1〉
+; quadruple … SUBC MODE_W_and_FR0 (Byte 〈x4,x8〉) 〈x0,x1〉
+; quadruple … SUBC MODE_W_and_FR1 (Byte 〈x4,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_36 ≝
+[
+ quadruple … SWAP MODE_FR0_and_W (Byte 〈x3,xA〉) 〈x0,x1〉
+; quadruple … SWAP MODE_FR1_and_W (Byte 〈x3,xB〉) 〈x0,x1〉
+; quadruple … SWAP MODE_W_and_FR0 (Byte 〈x3,x8〉) 〈x0,x1〉
+; quadruple … SWAP MODE_W_and_FR1 (Byte 〈x3,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_37 ≝
+[
+ quadruple … TEST MODE_FR0_and_W (Byte 〈x2,x2〉) 〈x0,x1〉
+; quadruple … TEST MODE_FR1_and_W (Byte 〈x2,x3〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022_38 ≝
+[
+ quadruple … XOR MODE_FR0_and_W (Byte 〈x1,xA〉) 〈x0,x1〉
+; quadruple … XOR MODE_FR1_and_W (Byte 〈x1,xB〉) 〈x0,x1〉
+; quadruple … XOR MODE_W_and_FR0 (Byte 〈x1,x8〉) 〈x0,x1〉
+; quadruple … XOR MODE_W_and_FR1 (Byte 〈x1,x9〉) 〈x0,x1〉
+; quadruple … XOR MODE_IMM8 (Byte 〈x7,xF〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_IP2022 ≝
+ opcode_table_IP2022_1 @ opcode_table_IP2022_2 @ opcode_table_IP2022_3 @ opcode_table_IP2022_4 @
+ opcode_table_IP2022_5 @ opcode_table_IP2022_6 @ opcode_table_IP2022_7 @ opcode_table_IP2022_8 @
+ opcode_table_IP2022_9 @ opcode_table_IP2022_10 @ opcode_table_IP2022_11 @ opcode_table_IP2022_12 @
+ opcode_table_IP2022_13 @ opcode_table_IP2022_14 @ opcode_table_IP2022_15 @ opcode_table_IP2022_16 @
+ opcode_table_IP2022_17 @ opcode_table_IP2022_18 @ opcode_table_IP2022_19 @ opcode_table_IP2022_20 @
+ opcode_table_IP2022_21 @ opcode_table_IP2022_22 @ opcode_table_IP2022_23 @ opcode_table_IP2022_24 @
+ opcode_table_IP2022_25 @ opcode_table_IP2022_26 @ opcode_table_IP2022_27 @ opcode_table_IP2022_28 @
+ opcode_table_IP2022_29 @ opcode_table_IP2022_30 @ opcode_table_IP2022_31 @ opcode_table_IP2022_32 @
+ opcode_table_IP2022_33 @ opcode_table_IP2022_34 @ opcode_table_IP2022_35 @ opcode_table_IP2022_36 @
+ opcode_table_IP2022_37 @ opcode_table_IP2022_38.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_pseudo.ma".
+include "emulator/opcodes/Freescale_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ***************** *)
+(* TABELLA DELL'RS08 *)
+(* ***************** *)
+
+(* definizione come concatenazione finale di liste per velocizzare il parsing *)
+(* ogni riga e' [pseudo] [modalita' indirizzamento] [opcode esadecimale] [#cicli esecuzione] *)
+
+ndefinition opcode_table_RS08_1 ≝
+[
+ quadruple … ADC MODE_IMM1 (Byte 〈xA,x9〉) 〈x0,x2〉
+; quadruple … ADC MODE_DIR1 (Byte 〈xB,x9〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_2 ≝
+[
+ quadruple … ADD MODE_IMM1 (Byte 〈xA,xB〉) 〈x0,x2〉
+; quadruple … ADD MODE_DIR1 (Byte 〈xB,xB〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x0) (Byte 〈x6,x0〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x1) (Byte 〈x6,x1〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x2) (Byte 〈x6,x2〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x3) (Byte 〈x6,x3〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x4) (Byte 〈x6,x4〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x5) (Byte 〈x6,x5〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x6) (Byte 〈x6,x6〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x7) (Byte 〈x6,x7〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x8) (Byte 〈x6,x8〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY x9) (Byte 〈x6,x9〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY xA) (Byte 〈x6,xA〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY xB) (Byte 〈x6,xB〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY xC) (Byte 〈x6,xC〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY xD) (Byte 〈x6,xD〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY xE) (Byte 〈x6,xE〉) 〈x0,x3〉
+; quadruple … ADD (MODE_TNY xF) (Byte 〈x6,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_3 ≝
+[
+ quadruple … AND MODE_IMM1 (Byte 〈xA,x4〉) 〈x0,x2〉
+; quadruple … AND MODE_DIR1 (Byte 〈xB,x4〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_4 ≝
+[
+ quadruple … ASL MODE_INHA (Byte 〈x4,x8〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_RS08_5 ≝
+[
+ quadruple … BRA MODE_IMM1 (Byte 〈x3,x0〉) 〈x0,x3〉
+; quadruple … BCC MODE_IMM1 (Byte 〈x3,x4〉) 〈x0,x3〉
+; quadruple … BCS MODE_IMM1 (Byte 〈x3,x5〉) 〈x0,x3〉
+; quadruple … BNE MODE_IMM1 (Byte 〈x3,x6〉) 〈x0,x3〉
+; quadruple … BEQ MODE_IMM1 (Byte 〈x3,x7〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_6 ≝
+[
+ quadruple … BSETn (MODE_DIRn o0) (Byte 〈x1,x0〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o0) (Byte 〈x1,x1〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o1) (Byte 〈x1,x2〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o1) (Byte 〈x1,x3〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o2) (Byte 〈x1,x4〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o2) (Byte 〈x1,x5〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o3) (Byte 〈x1,x6〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o3) (Byte 〈x1,x7〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o4) (Byte 〈x1,x8〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o4) (Byte 〈x1,x9〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o5) (Byte 〈x1,xA〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o5) (Byte 〈x1,xB〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o6) (Byte 〈x1,xC〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o6) (Byte 〈x1,xD〉) 〈x0,x5〉
+; quadruple … BSETn (MODE_DIRn o7) (Byte 〈x1,xE〉) 〈x0,x5〉
+; quadruple … BCLRn (MODE_DIRn o7) (Byte 〈x1,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_RS08_7 ≝
+[
+ quadruple … BRSETn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x0〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o0) (Byte 〈x0,x1〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x2〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o1) (Byte 〈x0,x3〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x4〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o2) (Byte 〈x0,x5〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x6〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o3) (Byte 〈x0,x7〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x8〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o4) (Byte 〈x0,x9〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xA〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o5) (Byte 〈x0,xB〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xC〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o6) (Byte 〈x0,xD〉) 〈x0,x5〉
+; quadruple … BRSETn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xE〉) 〈x0,x5〉
+; quadruple … BRCLRn (MODE_DIRn_and_IMM1 o7) (Byte 〈x0,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_RS08_8 ≝
+[
+ quadruple … CLC MODE_INH (Byte 〈x3,x8〉) 〈x0,x1〉
+; quadruple … SEC MODE_INH (Byte 〈x3,x9〉) 〈x0,x1〉
+; quadruple … SLA MODE_INH (Byte 〈x4,x2〉) 〈x0,x1〉
+; quadruple … SHA MODE_INH (Byte 〈x4,x5〉) 〈x0,x1〉
+; quadruple … NOP MODE_INH (Byte 〈xA,xC〉) 〈x0,x1〉
+; quadruple … STOP MODE_INH (Byte 〈xA,xE〉) 〈x0,x2〉
+; quadruple … WAIT MODE_INH (Byte 〈xA,xF〉) 〈x0,x2〉
+; quadruple … RTS MODE_INH (Byte 〈xB,xE〉) 〈x0,x3〉
+; quadruple … BGND MODE_INH (Byte 〈xB,xF〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_RS08_9 ≝
+[
+ quadruple … CBEQA MODE_DIR1_and_IMM1 (Byte 〈x3,x1〉) 〈x0,x5〉
+; quadruple … CBEQA MODE_IMM1_and_IMM1 (Byte 〈x4,x1〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_RS08_10 ≝
+[
+ quadruple … CLR MODE_DIR1 (Byte 〈x3,xF〉) 〈x0,x3〉
+; quadruple … CLR MODE_INHA (Byte 〈x4,xF〉) 〈x0,x1〉
+; quadruple … CLR (MODE_SRT t00) (Byte 〈x8,x0〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t01) (Byte 〈x8,x1〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t02) (Byte 〈x8,x2〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t03) (Byte 〈x8,x3〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t04) (Byte 〈x8,x4〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t05) (Byte 〈x8,x5〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t06) (Byte 〈x8,x6〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t07) (Byte 〈x8,x7〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t08) (Byte 〈x8,x8〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t09) (Byte 〈x8,x9〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t0A) (Byte 〈x8,xA〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t0B) (Byte 〈x8,xB〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t0C) (Byte 〈x8,xC〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t0D) (Byte 〈x8,xD〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t0E) (Byte 〈x8,xE〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t0F) (Byte 〈x8,xF〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t10) (Byte 〈x9,x0〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t11) (Byte 〈x9,x1〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t12) (Byte 〈x9,x2〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t13) (Byte 〈x9,x3〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t14) (Byte 〈x9,x4〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t15) (Byte 〈x9,x5〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t16) (Byte 〈x9,x6〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t17) (Byte 〈x9,x7〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t18) (Byte 〈x9,x8〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t19) (Byte 〈x9,x9〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t1A) (Byte 〈x9,xA〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t1B) (Byte 〈x9,xB〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t1C) (Byte 〈x9,xC〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t1D) (Byte 〈x9,xD〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t1E) (Byte 〈x9,xE〉) 〈x0,x2〉
+; quadruple … CLR (MODE_SRT t1F) (Byte 〈x9,xF〉) 〈x0,x2〉
+].
+
+ndefinition opcode_table_RS08_11 ≝
+[
+ quadruple … CMP MODE_IMM1 (Byte 〈xA,x1〉) 〈x0,x2〉
+; quadruple … CMP MODE_DIR1 (Byte 〈xB,x1〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_12 ≝
+[
+ quadruple … COM MODE_INHA (Byte 〈x4,x3〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_RS08_13 ≝
+[
+ quadruple … DBNZ MODE_DIR1_and_IMM1 (Byte 〈x3,xB〉) 〈x0,x7〉
+; quadruple … DBNZ MODE_INHA_and_IMM1 (Byte 〈x4,xB〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_RS08_14 ≝
+[
+ quadruple … DEC MODE_DIR1 (Byte 〈x3,xA〉) 〈x0,x5〉
+; quadruple … DEC MODE_INHA (Byte 〈x4,xA〉) 〈x0,x1〉
+; quadruple … DEC (MODE_TNY x0) (Byte 〈x5,x0〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x1) (Byte 〈x5,x1〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x2) (Byte 〈x5,x2〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x3) (Byte 〈x5,x3〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x4) (Byte 〈x5,x4〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x5) (Byte 〈x5,x5〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x6) (Byte 〈x5,x6〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x7) (Byte 〈x5,x7〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x8) (Byte 〈x5,x8〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY x9) (Byte 〈x5,x9〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY xA) (Byte 〈x5,xA〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY xB) (Byte 〈x5,xB〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY xC) (Byte 〈x5,xC〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY xD) (Byte 〈x5,xD〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY xE) (Byte 〈x5,xE〉) 〈x0,x4〉
+; quadruple … DEC (MODE_TNY xF) (Byte 〈x5,xF〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_RS08_15 ≝
+[
+ quadruple … EOR MODE_IMM1 (Byte 〈xA,x8〉) 〈x0,x2〉
+; quadruple … EOR MODE_DIR1 (Byte 〈xB,x8〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_16 ≝
+[
+ quadruple … INC MODE_DIR1 (Byte 〈x3,xC〉) 〈x0,x5〉
+; quadruple … INC MODE_INHA (Byte 〈x4,xC〉) 〈x0,x1〉
+; quadruple … INC (MODE_TNY x0) (Byte 〈x2,x0〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x1) (Byte 〈x2,x1〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x2) (Byte 〈x2,x2〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x3) (Byte 〈x2,x3〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x4) (Byte 〈x2,x4〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x5) (Byte 〈x2,x5〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x6) (Byte 〈x2,x6〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x7) (Byte 〈x2,x7〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x8) (Byte 〈x2,x8〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY x9) (Byte 〈x2,x9〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY xA) (Byte 〈x2,xA〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY xB) (Byte 〈x2,xB〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY xC) (Byte 〈x2,xC〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY xD) (Byte 〈x2,xD〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY xE) (Byte 〈x2,xE〉) 〈x0,x4〉
+; quadruple … INC (MODE_TNY xF) (Byte 〈x2,xF〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_RS08_17 ≝
+[
+ quadruple … JMP MODE_IMM2 (Byte 〈xB,xC〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_RS08_18 ≝
+[
+ quadruple … BSR MODE_IMM1 (Byte 〈xA,xD〉) 〈x0,x3〉
+; quadruple … JSR MODE_IMM2 (Byte 〈xB,xD〉) 〈x0,x4〉
+].
+
+ndefinition opcode_table_RS08_19 ≝
+[
+ quadruple … LDA MODE_IMM1 (Byte 〈xA,x6〉) 〈x0,x2〉
+; quadruple … LDA MODE_DIR1 (Byte 〈xB,x6〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t00) (Byte 〈xC,x0〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t01) (Byte 〈xC,x1〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t02) (Byte 〈xC,x2〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t03) (Byte 〈xC,x3〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t04) (Byte 〈xC,x4〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t05) (Byte 〈xC,x5〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t06) (Byte 〈xC,x6〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t07) (Byte 〈xC,x7〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t08) (Byte 〈xC,x8〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t09) (Byte 〈xC,x9〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t0A) (Byte 〈xC,xA〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t0B) (Byte 〈xC,xB〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t0C) (Byte 〈xC,xC〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t0D) (Byte 〈xC,xD〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t0E) (Byte 〈xC,xE〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t0F) (Byte 〈xC,xF〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t10) (Byte 〈xD,x0〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t11) (Byte 〈xD,x1〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t12) (Byte 〈xD,x2〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t13) (Byte 〈xD,x3〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t14) (Byte 〈xD,x4〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t15) (Byte 〈xD,x5〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t16) (Byte 〈xD,x6〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t17) (Byte 〈xD,x7〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t18) (Byte 〈xD,x8〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t19) (Byte 〈xD,x9〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t1A) (Byte 〈xD,xA〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t1B) (Byte 〈xD,xB〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t1C) (Byte 〈xD,xC〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t1D) (Byte 〈xD,xD〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t1E) (Byte 〈xD,xE〉) 〈x0,x3〉
+; quadruple … LDA (MODE_SRT t1F) (Byte 〈xD,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_20 ≝
+[
+ quadruple … LSR MODE_INHA (Byte 〈x4,x4〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_RS08_21 ≝
+[
+ quadruple … MOV MODE_IMM1_to_DIR1 (Byte 〈x3,xE〉) 〈x0,x4〉
+; quadruple … MOV MODE_DIR1_to_DIR1 (Byte 〈x4,xE〉) 〈x0,x5〉
+].
+
+ndefinition opcode_table_RS08_22 ≝
+[
+ quadruple … ORA MODE_IMM1 (Byte 〈xA,xA〉) 〈x0,x2〉
+; quadruple … ORA MODE_DIR1 (Byte 〈xB,xA〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_23 ≝
+[
+ quadruple … ROL MODE_INHA (Byte 〈x4,x9〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_RS08_24 ≝
+[
+ quadruple … ROR MODE_INHA (Byte 〈x4,x6〉) 〈x0,x1〉
+].
+
+ndefinition opcode_table_RS08_25 ≝
+[
+ quadruple … SBC MODE_IMM1 (Byte 〈xA,x2〉) 〈x0,x2〉
+; quadruple … SBC MODE_DIR1 (Byte 〈xB,x2〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08_26 ≝
+[
+ quadruple … STA MODE_DIR1 (Byte 〈xB,x7〉) 〈x0,x3〉
+; quadruple … STA (MODE_SRT t00) (Byte 〈xE,x0〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t01) (Byte 〈xE,x1〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t02) (Byte 〈xE,x2〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t03) (Byte 〈xE,x3〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t04) (Byte 〈xE,x4〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t05) (Byte 〈xE,x5〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t06) (Byte 〈xE,x6〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t07) (Byte 〈xE,x7〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t08) (Byte 〈xE,x8〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t09) (Byte 〈xE,x9〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t0A) (Byte 〈xE,xA〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t0B) (Byte 〈xE,xB〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t0C) (Byte 〈xE,xC〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t0D) (Byte 〈xE,xD〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t0E) (Byte 〈xE,xE〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t0F) (Byte 〈xE,xF〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t10) (Byte 〈xF,x0〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t11) (Byte 〈xF,x1〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t12) (Byte 〈xF,x2〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t13) (Byte 〈xF,x3〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t14) (Byte 〈xF,x4〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t15) (Byte 〈xF,x5〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t16) (Byte 〈xF,x6〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t17) (Byte 〈xF,x7〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t18) (Byte 〈xF,x8〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t19) (Byte 〈xF,x9〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t1A) (Byte 〈xF,xA〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t1B) (Byte 〈xF,xB〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t1C) (Byte 〈xF,xC〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t1D) (Byte 〈xF,xD〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t1E) (Byte 〈xF,xE〉) 〈x0,x2〉
+; quadruple … STA (MODE_SRT t1F) (Byte 〈xF,xF〉) 〈x0,x2〉
+].
+
+ndefinition opcode_table_RS08_27 ≝
+[
+ quadruple … SUB MODE_IMM1 (Byte 〈xA,x0〉) 〈x0,x2〉
+; quadruple … SUB MODE_DIR1 (Byte 〈xB,x0〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x0) (Byte 〈x7,x0〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x1) (Byte 〈x7,x1〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x2) (Byte 〈x7,x2〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x3) (Byte 〈x7,x3〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x4) (Byte 〈x7,x4〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x5) (Byte 〈x7,x5〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x6) (Byte 〈x7,x6〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x7) (Byte 〈x7,x7〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x8) (Byte 〈x7,x8〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY x9) (Byte 〈x7,x9〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY xA) (Byte 〈x7,xA〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY xB) (Byte 〈x7,xB〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY xC) (Byte 〈x7,xC〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY xD) (Byte 〈x7,xD〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY xE) (Byte 〈x7,xE〉) 〈x0,x3〉
+; quadruple … SUB (MODE_TNY xF) (Byte 〈x7,xF〉) 〈x0,x3〉
+].
+
+ndefinition opcode_table_RS08 ≝
+opcode_table_RS08_1 @ opcode_table_RS08_2 @ opcode_table_RS08_3 @ opcode_table_RS08_4 @
+opcode_table_RS08_5 @ opcode_table_RS08_6 @ opcode_table_RS08_7 @ opcode_table_RS08_8 @
+opcode_table_RS08_9 @ opcode_table_RS08_10 @ opcode_table_RS08_11 @ opcode_table_RS08_12 @
+opcode_table_RS08_13 @ opcode_table_RS08_14 @ opcode_table_RS08_15 @ opcode_table_RS08_16 @
+opcode_table_RS08_17 @ opcode_table_RS08_18 @ opcode_table_RS08_19 @ opcode_table_RS08_20 @
+opcode_table_RS08_21 @ opcode_table_RS08_22 @ opcode_table_RS08_23 @ opcode_table_RS08_24 @
+opcode_table_RS08_25 @ opcode_table_RS08_26 @ opcode_table_RS08_27.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "num/word16.ma".
+
+(* raggruppamento di byte e word in un tipo unico *)
+ninductive byte8_or_word16 : Type ≝
+ Byte: byte8 → byte8_or_word16
+| Word: word16 → byte8_or_word16.
+
+ndefinition eq_b8w16 ≝
+λbw1,bw2:byte8_or_word16.
+ match bw1 with
+ [ Byte b1 ⇒ match bw2 with [ Byte b2 ⇒ eqc ? b1 b2 | Word _ ⇒ false ]
+ | Word w1 ⇒ match bw2 with [ Byte _ ⇒ false | Word w2 ⇒ eqc ? w1 w2 ]
+ ].
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* ********************************************************************** *)
+(* Progetto FreeScale *)
+(* *)
+(* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
+(* Sviluppo: 2008-2010 *)
+(* *)
+(* ********************************************************************** *)
+
+include "emulator/opcodes/Freescale_pseudo.ma".
+include "emulator/opcodes/Freescale_instr_mode.ma".
+include "emulator/opcodes/IP2022_pseudo.ma".
+include "emulator/opcodes/IP2022_instr_mode.ma".
+include "emulator/opcodes/byte_or_word.ma".
+include "common/list.ma".
+
+(* ********************************************** *)
+(* MATTONI BASE PER DEFINIRE LE TABELLE DELLE MCU *)
+(* ********************************************** *)
+
+(* enumerazione delle ALU *)
+ninductive mcu_type: Type ≝
+ HC05 : mcu_type
+| HC08 : mcu_type
+| HCS08 : mcu_type
+| RS08 : mcu_type
+| IP2022 : mcu_type.
+
+ndefinition eq_mcutype ≝
+λm1,m2:mcu_type.
+ match m1 with
+ [ HC05 ⇒ match m2 with [ HC05 ⇒ true | _ ⇒ false ]
+ | HC08 ⇒ match m2 with [ HC08 ⇒ true | _ ⇒ false ]
+ | HCS08 ⇒ match m2 with [ HCS08 ⇒ true | _ ⇒ false ]
+ | RS08 ⇒ match m2 with [ RS08 ⇒ true | _ ⇒ false ]
+ | IP2022 ⇒ match m2 with [ IP2022 ⇒ true | _ ⇒ false ]
+ ].
+
+ndefinition aux_pseudo_type ≝
+λmcu:mcu_type.match mcu with
+ [ HC05 ⇒ Freescale_pseudo
+ | HC08 ⇒ Freescale_pseudo
+ | HCS08 ⇒ Freescale_pseudo
+ | RS08 ⇒ Freescale_pseudo
+ | IP2022 ⇒ IP2022_pseudo
+ ].
+
+ndefinition aux_im_type ≝
+λmcu:mcu_type.match mcu with
+ [ HC05 ⇒ Freescale_instr_mode
+ | HC08 ⇒ Freescale_instr_mode
+ | HCS08 ⇒ Freescale_instr_mode
+ | RS08 ⇒ Freescale_instr_mode
+ | IP2022 ⇒ IP2022_instr_mode
+ ].
+
+(* ********************************************* *)
+(* STRUMENTI PER LE DIMOSTRAZIONI DI CORRETTEZZA *)
+(* ********************************************* *)
+
+ndefinition aux_table_type ≝ λmcu:mcu_type.Prod4T (aux_pseudo_type mcu) (aux_im_type mcu) byte8_or_word16 byte8.
+
+ndefinition pseudo_is_comparable ≝
+λmcu:mcu_type.match mcu with
+ [ HC05 ⇒ Freescalepseudo_is_comparable
+ | HC08 ⇒ Freescalepseudo_is_comparable
+ | HCS08 ⇒ Freescalepseudo_is_comparable
+ | RS08 ⇒ Freescalepseudo_is_comparable
+ | IP2022 ⇒ IP2022pseudo_is_comparable
+ ].
+
+(* come suggerire di unificare?
+ carr (pseudo_is_comparable M) = aux_pseudo_type M *)
+
+(* su tutta la lista quante volte compare lo pseudocodice *)
+nlet rec get_pseudo_count (m:mcu_type) (o:aux_pseudo_type m) (c:word16) (l:list (aux_table_type m)) on l ≝
+ match l with
+ [ nil ⇒ c
+ | cons hd tl ⇒ match eqc ? o (fst4T … hd) with
+ [ true ⇒ get_pseudo_count m o (succc ? c) tl
+ | false ⇒ get_pseudo_count m o c tl
+ ]
+ ].
projects / helm.git / commitdiff