freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / multivm.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
index 4ae8093d1b00a3aa3ace848b0e3fe3b0fa0d9852..e0277386cb7f1902c42fac5c6c56820973606d99 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
@@ -1131,18 +1131,6 @@ ninductive susp_type : Type ≝
 | STOP_MODE: susp_type
 | WAIT_MODE: susp_type.
 
-ndefinition susp_type_ind : ΠP:susp_type → Prop.P BGND_MODE → P STOP_MODE → P WAIT_MODE → Πs:susp_type.P s ≝
-λP:susp_type → Prop.λp:P BGND_MODE.λp1:P STOP_MODE.λp2:P WAIT_MODE.λs:susp_type.
- match s with [ BGND_MODE ⇒ p | STOP_MODE ⇒ p1 | WAIT_MODE ⇒ p2 ].
-
-ndefinition susp_type_rec : ΠP:susp_type → Set.P BGND_MODE → P STOP_MODE → P WAIT_MODE → Πs:susp_type.P s ≝
-λP:susp_type → Set.λp:P BGND_MODE.λp1:P STOP_MODE.λp2:P WAIT_MODE.λs:susp_type.
- match s with [ BGND_MODE ⇒ p | STOP_MODE ⇒ p1 | WAIT_MODE ⇒ p2 ].
-
-ndefinition susp_type_rect : ΠP:susp_type → Type.P BGND_MODE → P STOP_MODE → P WAIT_MODE → Πs:susp_type.P s ≝
-λP:susp_type → Type.λp:P BGND_MODE.λp1:P STOP_MODE.λp2:P WAIT_MODE.λs:susp_type.
- match s with [ BGND_MODE ⇒ p | STOP_MODE ⇒ p1 | WAIT_MODE ⇒ p2 ].
-
 (* un tipo opzione ad hoc
    - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
    - sospensione: sospensione+stato (seguira' resume o ??)
@@ -1153,27 +1141,6 @@ ninductive tick_result (A:Type) : Type ≝
 | TickSUSP  : A → susp_type → tick_result A
 | TickOK    : A → tick_result A.
 
-ndefinition tick_result_ind
- : ΠA:Type.ΠP:tick_result A → Prop.(Πa:A.Πn:error_type.P (TickERR A a n)) →
-   (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Prop.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
-ndefinition tick_result_rec
- : ΠA:Type.ΠP:tick_result A → Set.(Πa:A.Πn:error_type.P (TickERR A a n)) →
-   (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Set.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
-ndefinition tick_result_rect
- : ΠA:Type.ΠP:tick_result A → Type.(Πa:A.Πn:error_type.P (TickERR A a n)) →
-   (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Type.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
 (* sostanazialmente simula
    - fetch/decode/execute
    - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
@@ -1301,7 +1268,7 @@ ndefinition tick_execute ≝
 
 ndefinition tick ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.
- let opt_info ≝ get_clk_desc m t s in
+ let opt_info ≝ clk_desc m t s in
  match opt_info with
   (* e' il momento del fetch *)
   [ None ⇒ match fetch m t s with