From: Cosimo Oliboni Date: Thu, 23 Jul 2009 18:18:28 +0000 (+0000) Subject: freescale porting, work in progress X-Git-Tag: make_still_working~3627 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03ebff6c48be2253ad32b3b57f4e1d2b02acda86;p=helm.git freescale porting, work in progress --- diff --git a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma index d7948c386..b6042164c 100755 --- a/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma +++ b/helm/software/matita/contribs/ng_assembly/compiler/ast_type_lemmas.ma @@ -21,6 +21,7 @@ (* ********************************************************************** *) include "compiler/ast_type.ma". +include "utility/utility_lemmas.ma". (* ************************* *) (* dimensioni degli elementi *) @@ -100,7 +101,7 @@ nlemma asttype_destruct_array_array_2 : ∀x1,x2,y1,y2.AST_TYPE_ARRAY x1 y1 = AS napply (refl_eq ??). nqed. -nlemma asttype_destruct_struc_struct : ∀b1,b2.AST_TYPE_STRUCT b1 = AST_TYPE_STRUCT b2 → b1 = b2. +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; @@ -203,8 +204,102 @@ nlemma symmetric_eqasttype : symmetricT ast_type bool eq_ast_type. ##] nqed. -... +nlemma eqasttype_to_eq : ∀t1,t2.eq_ast_type t1 t2 = true → t1 = t2. + #t1; + napply (ast_type_index ????? t1); + ##[ ##1: #b1; #t2; ncases t2; + ##[ ##1: #b2; #H; nchange in H:(%) with ((eq_ast_base_type b1 b2) = true); + nrewrite > (eqastbasetype_to_eq b1 b2 H); + napply (refl_eq ??) + ##| ##2: #st2; #n2; nnormalize; #H; napply (bool_destruct ??? H) + ##| ##3: #nl2; nnormalize; #H; napply (bool_destruct ??? H) + ##] + ##| ##2: #st1; #n1; #H; #t2; ncases t2; + ##[ ##2: #st2; #n2; #H1; nchange in H1:(%) with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = true); + nrewrite > (H st2 (andb_true_true_l ?? H1)); + nrewrite > (eqnat_to_eq n1 n2 (andb_true_true_r ?? H1)); + napply (refl_eq ??) + ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct ??? H1) + ##| ##3: #nl2; nnormalize; #H1; napply (bool_destruct ??? H1) + ##] + ##| ##3: #hh1; #H; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; #H1; nchange in H1:(%) with ((eq_ast_type hh1 hh2) = true); + nrewrite > (H hh2 H1); + napply (refl_eq ??) + ##| ##2: #hh2; #ll2; nnormalize; #H1; napply (bool_destruct ??? H1) + ##] + ##| ##1: #b2; nnormalize; #H1; napply (bool_destruct ??? H1) + ##| ##2: #st2; #n2; nnormalize; #H1; napply (bool_destruct ??? H1) + ##] + ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; nnormalize; #H2; napply (bool_destruct ??? H2) + ##| ##2: #hh2; #ll2; #H2; nchange in H2:(%) with (((eq_ast_type hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_ast_type 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; napply (bool_destruct ??? H2) + ##| ##2: #st2; #n2; nnormalize; #H2; napply (bool_destruct ??? H2) + ##] + ##] +nqed. + +nlemma eq_to_eqasttype_aux1 + : ∀nl1,nl2. + ((eq_ast_type (AST_TYPE_STRUCT nl1) (AST_TYPE_STRUCT nl2)) = true) → + ((bfold_right_neList2 ? (λx,y.eq_ast_type x y) nl1 nl2) = true). + #nl1; #nl2; #H; + napply H. +nqed. +nlemma eq_to_eqasttype : ∀t1,t2.t1 = t2 → eq_ast_type 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 ((eq_ast_base_type b2 b2) = true); + nrewrite > (eq_to_eqastbasetype b2 b2 (refl_eq ??)); + napply (refl_eq ??) + ##| ##2: #st2; #n2; #H; napply (asttype_destruct ??? H) + ##| ##3: #nl2; #H; napply (asttype_destruct ??? H) + ##] + ##| ##2: #st1; #n1; #H; #t2; ncases t2; + ##[ ##2: #st2; #n2; #H1; nchange with (((eq_ast_type st1 st2)⊗(eq_nat n1 n2)) = true); + nrewrite > (H st2 (asttype_destruct_array_array_1 ???? H1)); + nrewrite > (eq_to_eqnat n1 n2 (asttype_destruct_array_array_2 ???? H1)); + nnormalize; + napply (refl_eq ??) + ##| ##1: #b2; #H1; napply (asttype_destruct ??? H1) + ##| ##3: #nl2; #H1; napply (asttype_destruct ??? H1) + ##] + ##| ##3: #hh1; #H; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; #H1; nchange with ((eq_ast_type hh1 hh2) = true); + nrewrite > (H hh2 (nelist_destruct_nil_nil ? hh1 hh2 (asttype_destruct_struct_struct ?? H1))); + napply (refl_eq ??) + ##| ##2: #hh2; #ll2; #H1; nelim (nelist_destruct_nil_cons ? hh1 hh2 ll2 (asttype_destruct_struct_struct ?? H1)) + ##] + ##| ##1: #b2; #H1; napply (asttype_destruct ??? H1) + ##| ##2: #st2; #n2; #H1; napply (asttype_destruct ??? H1) + ##] + ##| ##4: #hh1; #ll1; #H; #H1; #t2; ncases t2; + ##[ ##3: #nl2; ncases nl2; + ##[ ##1: #hh2; #H2; nelim (nelist_destruct_cons_nil ? hh1 hh2 ll1 (asttype_destruct_struct_struct ?? H2)) + ##| ##2: #hh2; #ll2; #H2; nchange with (((eq_ast_type hh1 hh2)⊗(bfold_right_neList2 ? (λx,y.eq_ast_type 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; napply (asttype_destruct ??? H2) + ##| ##2: #st2; #n2; #H2; napply (asttype_destruct ??? H2) + ##] + ##] +nqed. nlemma isbastbasetype_to_isastbasetype : ∀ast.isb_ast_base_type ast = true → is_ast_base_type ast. #ast; diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma index 8e9f08c05..17cadf037 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_abs.ma @@ -34,18 +34,6 @@ ninductive memory_impl : Type ≝ | MEM_TREE: memory_impl | MEM_BITS: memory_impl. -(*ndefinition memory_impl_ind : ΠP:memory_impl → Prop.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝ -λP:memory_impl → Prop.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl. - match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ]. - -ndefinition memory_impl_rec : ΠP:memory_impl → Set.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝ -λP:memory_impl → Set.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl. - match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ]. - -ndefinition memory_impl_rect : ΠP:memory_impl → Type.P MEM_FUNC → P MEM_TREE → P MEM_BITS → Πm:memory_impl.P m ≝ -λP:memory_impl → Type.λp:P MEM_FUNC.λp1:P MEM_TREE.λp2:P MEM_BITS.λm:memory_impl. - match m with [ MEM_FUNC ⇒ p | MEM_TREE ⇒ p1 | MEM_BITS ⇒ p2 ].*) - (* ausiliario per il tipo della memoria *) ndefinition aux_mem_type ≝ λt:memory_impl.match t with diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma index 0ba7735af..38966a668 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma @@ -33,18 +33,6 @@ ninductive memory_type : Type ≝ | MEM_READ_WRITE: memory_type | MEM_OUT_OF_BOUND: memory_type. -(*ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ -λP:memory_type → Prop.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. - match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. - -ndefinition memory_type_rec : ΠP:memory_type → Set.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ -λP:memory_type → Set.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. - match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. - -ndefinition memory_type_rect : ΠP:memory_type → Type.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ -λP:memory_type → Type.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. - match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. -*) (* **************** *) (* TIPO ARRAY DA 16 *) (* **************** *) @@ -55,27 +43,6 @@ array_16T : T → T → T → T → T → T → T → T → T → T → T → T → T → T → T → T → Array16T T. -(*ndefinition Array16T_ind - : ΠT:Type.ΠP:Array16T T → Prop. - (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ -λT:Type.λP:Array16T T → Prop. -λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. - match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. - -ndefinition Array16T_rec - : ΠT:Type.ΠP:Array16T T → Set. - (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ -λT:Type.λP:Array16T T → Set. -λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. - match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. - -ndefinition Array16T_rect - : ΠT:Type.ΠP:Array16T T → Type. - (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ -λT:Type.λP:Array16T T → Type. -λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. - match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. -*) (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array16T ≝ @@ -337,27 +304,6 @@ ninductive Array8T (T:Type) : Type ≝ array_8T : T → T → T → T → T → T → T → T → Array8T T. -(*ndefinition Array8T_ind - : ΠT:Type.ΠP:Array8T T → Prop. - (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ -λT:Type.λP:Array8T T → Prop. -λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. - match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. - -ndefinition Array8T_rec - : ΠT:Type.ΠP:Array8T T → Set. - (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ -λT:Type.λP:Array8T T → Set. -λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. - match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. - -ndefinition Array8T_rect - : ΠT:Type.ΠP:Array8T T → Type. - (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ -λT:Type.λP:Array8T T → Type. -λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. - match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. -*) (* abbiamo gia' gli ottali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array8T ≝ diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma index 5dad70809..adafa40f3 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma @@ -31,18 +31,6 @@ ninductive HC05_mcu_model : Type ≝ MC68HC05J5A: HC05_mcu_model (*..*). -ndefinition HC05_mcu_model_ind : ΠP:HC05_mcu_model → Prop.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝ -λP:HC05_mcu_model → Prop.λp:P MC68HC05J5A.λh:HC05_mcu_model. - match h with [ MC68HC05J5A ⇒ p ]. - -ndefinition HC05_mcu_model_rec : ΠP:HC05_mcu_model → Set.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝ -λP:HC05_mcu_model → Set.λp:P MC68HC05J5A.λh:HC05_mcu_model. - match h with [ MC68HC05J5A ⇒ p ]. - -ndefinition HC05_mcu_model_rect : ΠP:HC05_mcu_model → Type.P MC68HC05J5A → Πh:HC05_mcu_model.P h ≝ -λP:HC05_mcu_model → Type.λp:P MC68HC05J5A.λh:HC05_mcu_model. - match h with [ MC68HC05J5A ⇒ p ]. - (* modelli di HC08 *) ninductive HC08_mcu_model : Type ≝ MC68HC08AB16A: HC08_mcu_model diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma index a92c4a6e0..b20d2e814 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma @@ -64,35 +64,6 @@ nrecord alu_HC05: Type ≝ irq_flag_HC05 : bool }. -(*ndefinition alu_HC05_ind : - ΠP:alu_HC05 → Prop.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝ -λP:alu_HC05 → Prop.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05. - match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ]. - -ndefinition alu_HC05_rec : - ΠP:alu_HC05 → Set.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝ -λP:alu_HC05 → Set.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05. - match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ]. - -ndefinition alu_HC05_rect : - ΠP:alu_HC05 → Type.(Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7)) → Πa:alu_HC05.P a ≝ -λP:alu_HC05 → Type.λf:Πb,b1,w,w1,w2,w3,w4,b2,b3,b4,b5,b6,b7.P (mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7).λa:alu_HC05. - match a with [ mk_alu_HC05 b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ⇒ f b b1 w w1 w2 w3 w4 b2 b3 b4 b5 b6 b7 ]. - -ndefinition acc_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 x _ _ _ _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition indX_low_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition sp_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition sp_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition sp_fix_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition pc_reg_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ]. -ndefinition pc_mask_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ]. -ndefinition h_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ]. -ndefinition i_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ]. -ndefinition n_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ]. -ndefinition z_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ]. -ndefinition c_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ]. -ndefinition irq_flag_HC05 ≝ λalu.match alu with [ mk_alu_HC05 _ _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ]. -*) notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'Sp_Reg' ≝ sp ; break 'Sp_Mask' ≝ spm ; break 'Sp_Fix' ≝ spf ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}" non associative with precedence 80 for @{ 'mk_alu_HC05 $acclow $indxlow $sp $spm $spf $pc $pcm $hfl $ifl $nfl $zfl $cfl $irqfl }. @@ -130,34 +101,6 @@ nrecord alu_HC08: Type ≝ irq_flag_HC08 : bool }. -(*ndefinition alu_HC08_ind : - ΠP:alu_HC08 → Prop.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝ -λP:alu_HC08 → Prop.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08. - match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ]. - -ndefinition alu_HC08_rec : - ΠP:alu_HC08 → Set.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝ -λP:alu_HC08 → Set.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08. - match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ]. - -ndefinition alu_HC08_rect : - ΠP:alu_HC08 → Type.(Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9)) → Πa:alu_HC08.P a ≝ -λP:alu_HC08 → Type.λf:Πb,b1,b2,w,w1,b3,b4,b5,b6,b7,b8,b9.P (mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9).λa:alu_HC08. - match a with [ mk_alu_HC08 b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ⇒ f b b1 b2 w w1 b3 b4 b5 b6 b7 b8 b9 ]. - -ndefinition acc_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 x _ _ _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition indX_low_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ x _ _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition indX_high_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ x _ _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition sp_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ x _ _ _ _ _ _ _ _ ⇒ x ]. -ndefinition pc_reg_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ x _ _ _ _ _ _ _ ⇒ x ]. -ndefinition v_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ x _ _ _ _ _ _ ⇒ x ]. -ndefinition h_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ x _ _ _ _ _ ⇒ x ]. -ndefinition i_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ x _ _ _ _ ⇒ x ]. -ndefinition n_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ x _ _ _ ⇒ x ]. -ndefinition z_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ x _ _ ⇒ x ]. -ndefinition c_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ x _ ⇒ x ]. -ndefinition irq_flag_HC08 ≝ λalu.match alu with [ mk_alu_HC08 _ _ _ _ _ _ _ _ _ _ _ x ⇒ x ]. -*) notation "{hvbox('A_Reg' ≝ acclow ; break 'X_Reg' ≝ indxlow ; break 'H_Reg' ≝ indxhigh ; break 'Sp_Reg' ≝ sp ; break 'Pc_Reg' ≝ pc ; break 'V_Flag' ≝ vfl ; break 'H_Flag' ≝ hfl ; break 'I_Flag' ≝ ifl ; break 'N_Flag' ≝ nfl ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl ; break 'IRQ_Flag' ≝ irqfl)}" non associative with precedence 80 for @{ 'mk_alu_HC08 $acclow $indxlow $indxhigh $sp $pc $vfl $hfl $ifl $nfl $zfl $cfl $irqfl }. @@ -200,30 +143,6 @@ nrecord alu_RS08: Type ≝ c_flag_RS08 : bool }. -(*ndefinition alu_RS08_ind : - ΠP:alu_RS08 → Prop.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝ -λP:alu_RS08 → Prop.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08. - match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ]. - -ndefinition alu_RS08_rec : - ΠP:alu_RS08 → Set.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝ -λP:alu_RS08 → Set.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08. - match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ]. - -ndefinition alu_RS08_rect : - ΠP:alu_RS08 → Type.(Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4)) → Πa:alu_RS08.P a ≝ -λP:alu_RS08 → Type.λf:Πb,w,w1,w2,b1,b2,b3,b4.P (mk_alu_RS08 b w w1 w2 b1 b2 b3 b4).λa:alu_RS08. - match a with [ mk_alu_RS08 b w w1 w2 b1 b2 b3 b4 ⇒ f b w w1 w2 b1 b2 b3 b4 ]. - -ndefinition acc_low_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 x _ _ _ _ _ _ _ ⇒ x ]. -ndefinition pc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ x _ _ _ _ _ _ ⇒ x ]. -ndefinition pc_mask_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ x _ _ _ _ _ ⇒ x ]. -ndefinition spc_reg_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ x _ _ _ _ ⇒ x ]. -ndefinition x_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ x _ _ _ ⇒ x ]. -ndefinition ps_map_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ x _ _ ⇒ x ]. -ndefinition z_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ x _ ⇒ x ]. -ndefinition c_flag_RS08 ≝ λalu.match alu with [ mk_alu_RS08 _ _ _ _ _ _ _ x ⇒ x ]. -*) notation "{hvbox('A_Reg' ≝ acclow ; break 'Pc_Reg' ≝ pc ; break 'Pc_Mask' ≝ pcm ; break 'Spc_Reg' ≝ spc ; break 'X_Map' ≝ xm ; break 'Ps_Map' ≝ psm ; break 'Z_Flag' ≝ zfl ; break 'C_Flag' ≝ cfl)}" non associative with precedence 80 for @{ 'mk_alu_RS08 $acclow $pc $pcm $spc $xm $psm $zfl $cfl }. diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma index 8ef0d5234..94d254bf2 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma @@ -76,21 +76,6 @@ full_info_of_word16_aux m borw (opcode_table m). ninductive t_byte8 (m:mcu_type) : Type ≝ TByte : byte8 → t_byte8 m. -(*ndefinition t_byte8_ind - : Πm:mcu_type.ΠP:t_byte8 m → Prop.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝ -λm:mcu_type.λP:t_byte8 m → Prop.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m. - match t with [ TByte (b:byte8) ⇒ f b ]. - -ndefinition t_byte8_rec - : Πm:mcu_type.ΠP:t_byte8 m → Set.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝ -λm:mcu_type.λP:t_byte8 m → Set.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m. - match t with [ TByte (b:byte8) ⇒ f b ]. - -ndefinition t_byte8_rect - : Πm:mcu_type.ΠP:t_byte8 m → Type.(Πb:byte8.P (TByte m b)) → Πt:t_byte8 m.P t ≝ -λm:mcu_type.λP:t_byte8 m → Type.λf:Πb:byte8.P (TByte m b).λt:t_byte8 m. - match t with [ TByte (b:byte8) ⇒ f b ].*) - nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2. #m; #b1; #b2; #H; nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]); @@ -137,114 +122,6 @@ ninductive MA_check : instr_mode → Type ≝ | maSRT : ∀t.MA_check (MODE_SRT t) . -ndefinition instr_mode_ind - : Πi:instr_mode.ΠP:Πj.MA_check j → Prop. - P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) → - (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) → - (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) → - (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) → - (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) → - (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) → - (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) → - (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) → - (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) → - Πma:MA_check i.P i ma ≝ -λi:instr_mode.λP:Πj.MA_check j → Prop. -λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD. -λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b). -λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0. -λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w). -λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2). -λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b). -λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2). -λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b). -λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2). -λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2). -λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2). -λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i. - match ma with - [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4 - | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b - | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b - | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2 - | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b - | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2 - | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b - | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2 - | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ]. - -(*ndefinition instr_mode_rec - : Πi:instr_mode.ΠP:Πj.MA_check j → Set. - P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) → - (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) → - (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) → - (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) → - (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) → - (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) → - (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) → - (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) → - (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) → - Πma:MA_check i.P i ma ≝ -λi:instr_mode.λP:Πj.MA_check j → Set. -λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD. -λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b). -λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0. -λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w). -λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2). -λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b). -λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2). -λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b). -λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2). -λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2). -λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2). -λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i. - match ma with - [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4 - | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b - | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b - | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2 - | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b - | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2 - | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b - | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2 - | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ]. - -ndefinition instr_mode_rect - : Πi:instr_mode.ΠP:Πj.MA_check j → Type. - P ? maINH → P ? maINHA → P ? maINHX → P ? maINHH → P ? maINHX0ADD → (Πb.P ? (maINHX1ADD b)) → - (Πw.P ? (maINHX2ADD w)) → (Πb.P ? (maIMM1 b)) → (Πb.P ? (maIMM1EXT b)) → (Πw.P ? (maIMM2 w)) → - (Πb.P ? (maDIR1 b)) → (Πw.P ? (maDIR2 w)) → P ? maIX0 → (Πb.P ? (maIX1 b)) → (Πw.P ? (maIX2 w)) → - (Πb.P ? (maSP1 b)) → (Πw.P ? (maSP2 w)) → (Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2)) → - (Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2)) → (Πb.P ? (maIX0p_to_DIR1 b)) → (Πb.P ? (maDIR1_to_IX0p b)) → - (Πb.P ? (maINHA_and_IMM1 b)) → (Πb.P ? (maINHX_and_IMM1 b)) → (Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2)) → - (Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2)) → (Πb.P ? (maIX0_and_IMM1 b)) → (Πb.P ? (maIX0p_and_IMM1 b)) → - (Πb1,b2.P ? (maIX1_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2)) → (Πb1,b2.P ? (maSP1_and_IMM1 b1 b2)) → - (Πn,b.P ? ((maDIRn n) b)) → (Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2)) → (Πe.P ? (maTNY e)) → (Πt.P ? (maSRT t)) → - Πma:MA_check i.P i ma ≝ -λi:instr_mode.λP:Πj.MA_check j → Type. -λp:P ? maINH.λp1:P ? maINHA.λp2:P ? maINHX.λp3:P ? maINHH.λp4:P ? maINHX0ADD. -λf:Πb.P ? (maINHX1ADD b).λf1:Πw.P ? (maINHX2ADD w).λf2:Πb.P ? (maIMM1 b).λf3:Πb.P ? (maIMM1EXT b). -λf4:Πw.P ? (maIMM2 w).λf5:Πb.P ? (maDIR1 b).λf6:Πw.P ? (maDIR2 w).λp5:P ? maIX0. -λf7:Πb.P ? (maIX1 b).λf8:Πw.P ? (maIX2 w).λf9:Πb.P ? (maSP1 b).λf10:Πw.P ? (maSP2 w). -λf11:Πb1,b2.P ? (maDIR1_to_DIR1 b1 b2).λf12:Πb1,b2.P ? (maIMM1_to_DIR1 b1 b2). -λf13:Πb.P ? (maIX0p_to_DIR1 b).λf14:Πb.P ? (maDIR1_to_IX0p b).λf15:Πb.P ? (maINHA_and_IMM1 b). -λf16:Πb.P ? (maINHX_and_IMM1 b).λf17:Πb1,b2.P ? (maIMM1_and_IMM1 b1 b2). -λf18:Πb1,b2.P ? (maDIR1_and_IMM1 b1 b2).λf19:Πb.P ? (maIX0_and_IMM1 b). -λf20:Πb.P ? (maIX0p_and_IMM1 b).λf21:Πb1,b2.P ? (maIX1_and_IMM1 b1 b2). -λf22:Πb1,b2.P ? (maIX1p_and_IMM1 b1 b2).λf23:Πb1,b2.P ? (maSP1_and_IMM1 b1 b2). -λf24:Πn,b.P ? ((maDIRn n) b).λf25:Πn,b1,b2.P ? ((maDIRn_and_IMM1 n) b1 b2). -λf26:Πe.P ? (maTNY e).λf27:Πt.P ? (maSRT t).λma:MA_check i. - match ma with - [ maINH ⇒ p | maINHA ⇒ p1 | maINHX ⇒ p2 | maINHH ⇒ p3 | maINHX0ADD ⇒ p4 - | maINHX1ADD b ⇒ f b | maINHX2ADD w ⇒ f1 w | maIMM1 b ⇒ f2 b | maIMM1EXT b ⇒ f3 b - | maIMM2 w ⇒ f4 w | maDIR1 b ⇒ f5 b | maDIR2 w ⇒ f6 w | maIX0 ⇒ p5 | maIX1 b ⇒ f7 b - | maIX2 w ⇒ f8 w | maSP1 b ⇒ f9 b | maSP2 w ⇒ f10 w | maDIR1_to_DIR1 b1 b2 ⇒ f11 b1 b2 - | maIMM1_to_DIR1 b1 b2 ⇒ f12 b1 b2 | maIX0p_to_DIR1 b ⇒ f13 b | maDIR1_to_IX0p b ⇒ f14 b - | maINHA_and_IMM1 b ⇒ f15 b | maINHX_and_IMM1 b ⇒ f16 b | maIMM1_and_IMM1 b1 b2 ⇒ f17 b1 b2 - | maDIR1_and_IMM1 b1 b2 ⇒ f18 b1 b2 | maIX0_and_IMM1 b ⇒ f19 b | maIX0p_and_IMM1 b ⇒ f20 b - | maIX1_and_IMM1 b1 b2 ⇒ f21 b1 b2 | maIX1p_and_IMM1 b1 b2 ⇒ f22 b1 b2 | maSP1_and_IMM1 b1 b2 ⇒ f23 b1 b2 - | maDIRn n b ⇒ f24 n b | maDIRn_and_IMM1 n b1 b2 ⇒ f25 n b1 b2 | maTNY e ⇒ f26 e | maSRT t ⇒ f27 t ]. -*) (* picker: trasforma l'argomento necessario in input a bytes_of_pseudo_instr_mode_param: MA_check i → list (t_byte8 m) *) ndefinition args_picker ≝ @@ -329,10 +206,10 @@ ndefinition defined_option ≝ ndefinition compile ≝ λmcu:mcu_type.λi:instr_mode.λop:opcode.λarg:MA_check i. match bytes_of_pseudo_instr_mode_param mcu (anyOP mcu op) i arg - return λres:option (list (t_byte8 mcu)).defined_option (list (t_byte8 mcu)) res → (list (t_byte8 mcu)) + return λres:option ?.defined_option ? res → ? with - [ None ⇒ λp:defined_option (list (t_byte8 mcu)) (None ?).False_rect ? p - | Some x ⇒ λp:defined_option (list (t_byte8 mcu)) (Some ? x).x + [ None ⇒ λp:defined_option ? (None ?).False_rect_Type0 ? p + | Some x ⇒ λp:defined_option ? (Some ? x).x ]. (* detipatore del compilato: (t_byte8 m) → byte8 *)