matita/contribs/assembly/freescale/fix-with-left-params.diff

   1 Index: load_write.ma
   2 ===================================================================
   3 --- load_write.ma       (revision 8243)
   4 +++ load_write.ma       (working copy)
   5 @@ -260,10 +260,12 @@
   6  λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
   7   get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
   8
   9 -let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
  10 +definition filtered_plus_w16 := \lambda m : mcu_type.
  11 +let rec aux (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
  12   match n with
  13    [ O ⇒ w
  14 -  | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
  15 +  | S n' ⇒ aux t s (filtered_inc_w16 m t s w) n' ]
  16 +  in aux.
  17
  18  (*
  19     errore1: non esiste traduzione ILL_OP
  20 Index: multivm.ma
  21 ===================================================================
  22 --- multivm.ma  (revision 8243)
  23 +++ multivm.ma  (working copy)
  24 @@ -1304,12 +1304,13 @@
  25  (* ESECUZIONE *)
  26  (* ********** *)
  27
  28 -let rec execute (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
  29 +definition execute := \lambda m : mcu_type.
  30 +let rec aux (t:memory_impl) (s:tick_result (any_status m t)) (n:nat) on n ≝
  31   match s with
  32    [ TickERR s' error ⇒ TickERR ? s' error
  33    | TickSUSP s' susp ⇒ TickSUSP ? s' susp
  34 -  | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ execute m t (tick m t s') n' ]
  35 -  ].
  36 +  | TickOK s'        ⇒ match n with [ O ⇒ TickOK ? s' | S n' ⇒ aux t (tick m t s') n' ]
  37 +  ] in aux.
  38
  39  lemma breakpoint:
  40   ∀m,u,s,n1,n2. execute m u s (n1 + n2) = execute m u (execute m u s n1) n2.
  41 Index: medium_tests_lemmas.ma
  42 ===================================================================
  43 --- medium_tests_lemmas.ma      (revision 8241)
  44 +++ medium_tests_lemmas.ma      (working copy)
  45 @@ -126,7 +126,7 @@
  46  axiom MSB16_of_make_word16 :
  47   ∀bh,bl:byte8.
  48    MSB_w16 (mk_word16 bh bl) = MSB_b8 bh.
  49 -
  50 +(*
  51  lemma execute_HCS08_LDHX_maIMM2 :
  52   ∀t:memory_impl.∀s:any_status HCS08 t.∀bhigh,blow:byte8.
  53    (get_clk_desc HCS08 t s = None ?) →
  54 @@ -436,3 +436,4 @@
  55   [2: elim H; reflexivity ]
  56   reflexivity.
  57  qed.
  58 +*)
  59 \ No newline at end of file
  60 Index: medium_tests.ma
  61 ===================================================================
  62 --- medium_tests.ma     (revision 8241)
  63 +++ medium_tests.ma     (working copy)
  64 @@ -800,34 +800,37 @@
  65       ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ; 〈x0,x0〉 ].
  66
  67  (* esecuzione execute k*(n+2) *)
  68 -let rec dTest_HCS08_gNum_execute1 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
  69 +definition dTest_HCS08_gNum_execute1 := \lambda m : mcu_type.
  70 +let rec aux (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
  71   match s with
  72    [ TickERR s' error ⇒ TickERR ? s' error
  73    | TickSUSP s' susp ⇒ TickSUSP ? s' susp
  74    | TickOK s' ⇒ match n with
  75     [ O ⇒ TickOK ? s'
  76 -   | S n' ⇒ dTest_HCS08_gNum_execute1 m t (execute m t (TickOK ? s') (ntot+2)) n' ntot ]
  77 -  ].
  78 +   | S n' ⇒ aux t (execute m t (TickOK ? s') (ntot+2)) n' ntot ]
  79 +  ] in aux.
  80
  81  (* esecuzione execute k*(n+1)*(n+2) *)
  82 -let rec dTest_HCS08_gNum_execute2 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
  83 +definition dTest_HCS08_gNum_execute2 := \lambda m : mcu_type.
  84 +let rec aux (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
  85   match s with
  86    [ TickERR s' error ⇒ TickERR ? s' error
  87    | TickSUSP s' susp ⇒ TickSUSP ? s' susp
  88    | TickOK s' ⇒ match n with
  89     [ O ⇒ TickOK ? s'
  90 -   | S n' ⇒ dTest_HCS08_gNum_execute2 m t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot+1) ntot) n' ntot ]
  91 -  ].
  92 +   | S n' ⇒ aux t (dTest_HCS08_gNum_execute1 m t (TickOK ? s') (ntot+1) ntot) n' ntot ]
  93 +  ] in aux.
  94
  95  (* esecuzione execute k*n*(n+1)*(n+2) *)
  96 -let rec dTest_HCS08_gNum_execute3 (m:mcu_type) (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
  97 +definition dTest_HCS08_gNum_execute3 := \lambda m : mcu_type.
  98 +let rec aux (t:memory_impl) (s:tick_result (any_status m t)) (n,ntot:nat) on n ≝
  99   match s with
 100    [ TickERR s' error ⇒ TickERR ? s' error
 101    | TickSUSP s' susp ⇒ TickSUSP ? s' susp
 102    | TickOK s' ⇒ match n with
 103     [ O ⇒ TickOK ? s'
 104 -   | S n' ⇒ dTest_HCS08_gNum_execute3 m t (dTest_HCS08_gNum_execute2 m t (TickOK ? s') ntot ntot) n' ntot ]
 105 -  ].
 106 +   | S n' ⇒ aux t (dTest_HCS08_gNum_execute2 m t (TickOK ? s') ntot ntot) n' ntot ]
 107 +  ] in aux.
 108
 109  (* esecuzione execute 80+11*n*(n+1)*(n+2) *)
 110  definition dTest_HCS08_gNum_execute4 ≝
 111 Index: opcode.ma
 112 ===================================================================
 113 --- opcode.ma   (revision 8241)
 114 +++ opcode.ma   (working copy)
 115 @@ -385,56 +385,60 @@
 116  (* ********************************************* *)
 117
 118  (* su tutta la lista quante volte compare il byte *)
 119 -let rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
 120 +definition get_byte_count := \lambda m : mcu_type.
 121 +let rec aux (b:byte8) (c:nat)
 122   (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
 123   match l with
 124    [ nil ⇒ c
 125    | cons hd tl ⇒ match thd4T ???? hd with
 126     [ Byte b' ⇒ match eq_b8 b b' with
 127 -    [ true ⇒ get_byte_count m b (S c) tl
 128 -    | false ⇒ get_byte_count m b c tl
 129 +    [ true ⇒  aux b (S c) tl
 130 +    | false ⇒ aux b c tl
 131      ]
 132 -   | Word _ ⇒ get_byte_count m b c tl
 133 +   | Word _ ⇒ aux b c tl
 134     ]
 135 -  ].
 136 +  ] in aux.
 137
 138  (* su tutta la lista quante volte compare la word (0x9E+byte) *)
 139 -let rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
 140 +definition get_word_count := \lambda m : mcu_type.
 141 +let rec aux (b:byte8) (c:nat)
 142   (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
 143   match l with
 144    [ nil ⇒ c
 145    | cons hd tl ⇒ match thd4T ???? hd with
 146 -   [ Byte _ ⇒ get_word_count m b c tl
 147 +   [ Byte _ ⇒ aux b c tl
 148     | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
 149 -    [ true ⇒ get_word_count m b (S c) tl
 150 -    | false ⇒ get_word_count m b c tl
 151 +    [ true ⇒ aux b (S c) tl
 152 +    | false ⇒ aux b c tl
 153      ]
 154     ]
 155 -  ].
 156 +  ] in aux.
 157
 158  (* su tutta la lista quante volte compare lo pseudocodice *)
 159 -let rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
 160 +definition get_pseudo_count := \lambda m : mcu_type.
 161 +let rec aux (o:opcode) (c:nat)
 162   (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
 163   match l with
 164    [ nil ⇒ c
 165    | cons hd tl ⇒ match fst4T ???? hd with
 166     [ anyOP o' ⇒ match eqop m (anyOP m o) (anyOP m o') with
 167 -    [ true ⇒ get_pseudo_count m o (S c) tl
 168 -    | false ⇒ get_pseudo_count m o c tl
 169 +    [ true ⇒ aux o (S c) tl
 170 +    | false ⇒ aux o c tl
 171      ]
 172     ]
 173 -  ].
 174 +  ] in aux.
 175
 176  (* su tutta la lista quante volte compare la modalita' *)
 177 -let rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
 178 +definition get_mode_count:= \lambda m : mcu_type.
 179 +let rec aux (i:instr_mode) (c:nat)
 180   (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
 181   match l with
 182    [ nil ⇒ c
 183    | cons hd tl ⇒ match eqim (snd4T ???? hd) i with
 184 -   [ true ⇒ get_mode_count m i (S c) tl
 185 -   | false ⇒ get_mode_count m i c tl
 186 +   [ true ⇒ aux i (S c) tl
 187 +   | false ⇒ aux i c tl
 188     ]
 189 -  ].
 190 +  ] in aux.
 191
 192  (* b e' non implementato? *)
 193  let rec test_not_impl_byte (b:byte8) (l:list byte8) on l ≝
 194 @@ -467,17 +471,18 @@
 195    ].
 196
 197  (* su tutta la lista quante volte compare la coppia opcode,instr_mode *)
 198 -let rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
 199 +definition get_OpIm_count := \lambda m : mcu_type.
 200 +let rec aux (o:any_opcode m) (i:instr_mode) (c:nat)
 201   (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
 202   match l with
 203    [ nil ⇒ c
 204    | cons hd tl ⇒
 205     match (eqop m o (fst4T ???? hd)) ⊗
 206           (eqim i (snd4T ???? hd)) with
 207 -    [ true ⇒ get_OpIm_count m o i (S c) tl
 208 -    | false ⇒ get_OpIm_count m o i c tl
 209 +    [ true ⇒ aux o i (S c) tl
 210 +    | false ⇒ aux o i c tl
 211      ]
 212 -  ].
 213 +  ] in aux.
 214
 215  (* iteratore sugli opcode *)
 216  definition forall_opcode ≝ λP.