Changeset 256


Ignore:
Timestamp:
Nov 22, 2010, 7:25:53 PM (9 years ago)
Author:
mulligan
Message:

Work on ASM.ma file.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r249 r256  
    33include "Either.ma".
    44include "BitVector.ma".
    5 include "String.ma".
    6 
    7 ninductive Direct: Type[0] ≝
    8   DIRECT: Byte → Direct.
    9 ninductive Indirect: Type[0] ≝
    10   INDIRECT: Bit → Indirect.
    11 ninductive ExtIndirect: Type[0] ≝
    12   EXTINDIRECT: Bit → ExtIndirect.
    13 ninductive Register: Type[0] ≝
    14   REGISTER: Bit → Bit → Bit → Register.
    15 ninductive AccumulatorA: Type[0] ≝
    16   ACCUMULATORA: AccumulatorA.
    17 ninductive AccumulatorB: Type[0] ≝
    18   ACCUMULATORB: AccumulatorB.
    19 ninductive DPointer: Type[0] ≝
    20   DPOINTER: DPointer.
    21 ninductive Data: Type[0] ≝
    22   DATA: Byte → Data.
    23 ninductive Data16: Type[0] ≝
    24   DATA16: Word → Data16.
    25 ninductive AccumulatorDPointer: Type[0] ≝
    26   ACCUMULATORDPOINTER: AccumulatorDPointer.
    27 ninductive AccumulatorProgramCounter: Type[0] ≝
    28   ACCUMULATORPROGRAMCOUNTER: AccumulatorProgramCounter.
    29 ninductive ExternalIndirectDPointer: Type[0] ≝
    30   EXTERNALINDIRECTDPOINTER: ExternalIndirectDPointer.
    31 ninductive IndirectDPointer: Type[0] ≝
    32   INDIRECTDPOINTER: IndirectDPointer.
    33 ninductive Carry: Type[0] ≝
    34   CARRY: Carry.
    35 ninductive BitAddress: Type[0] ≝
    36   BIT: Bit → BitAddress.
    37 ninductive ComplementBitAddress: Type[0] ≝
    38   COMPLEMENTBITADDRESS: Bit → ComplementBitAddress.
    39 ninductive Relative: Type[0] ≝
    40   RELATIVE: Byte → Relative.
    41 ninductive Address11: Type[0] ≝
    42   ADDRESS11: Word11 → Address11.
    43 ninductive Address16: Type[0] ≝
    44   ADDRESS16: Word → Address16.
    45 
    46 ninductive Union2 (A: Type[0]) (B: Type[0]): Type[0] ≝
    47   U2: A → B → Union2 A B.
    48  
    49 ninductive Union3 (A: Type[0]) (B: Type[0]) (C: Type[0]): Type[0] ≝
    50   U3: A → B → C → Union3 A B C.
    51  
    52 ninductive Union6 (A: Type[0]) (B: Type[0])
    53                   (C: Type[0]) (D: Type[0])
    54                   (E: Type[0]) (F: Type[0]): Type[0] ≝
    55   U6: A → B → C → D → E → F → Union6 A B C D E F.
     5include "BitVectorTrie.ma".
     6
     7ninductive all_types : Type[0] ≝
     8   reg: all_types | direct: all_types | indirect:all_types | data:all_types
     9   | acc: all_types | rel: all_types.
     10
     11interpretation "Cartesian" 'product A B = (Cartesian A B).
     12interpretation "Either" 'plus A B = (Either A B).
     13
     14ninductive addressing_mode: Type[0] ≝
     15  DIRECT: Byte → addressing_mode
     16| INDIRECT: Bit → addressing_mode
     17| EXTINDIRECT: Bit → addressing_mode
     18| REGISTER: Bit → Bit → Bit → addressing_mode
     19| ACCUMULATORA: addressing_mode
     20| ACCUMULATORB: addressing_mode
     21| DPOINTER: addressing_mode
     22| DATA: Byte → addressing_mode
     23| DATA16: Word → addressing_mode
     24| ACCUMULATORDPOINTER: addressing_mode
     25| ACCUMULATORPROGRAMCOUNTER: addressing_mode
     26| EXTERNALINDIRECTDPOINTER: addressing_mode
     27| INDIRECTDPOINTER: addressing_mode
     28| CARRY: addressing_mode
     29| BIT: Bit → addressing_mode
     30| COMPLEMENTBITADDRESS: Bit → addressing_mode
     31| RELATIVE: Byte → addressing_mode
     32| ADDRESS11: Word11 → addressing_mode
     33| ADDRESS16: Word → addressing_mode.
     34
     35(* to avoid expansion... *)
     36nlet rec is_a (d:all_types) (A:addressing_mode) on d ≝
     37  match d with
     38   [ reg ⇒ match A with [ REGISTER _ _ _ ⇒ True | _ ⇒ False ]
     39   | data ⇒ match A with [ DATA _ ⇒ True | _ ⇒ False ]
     40   | rel ⇒ match A with [ RELATIVE _ ⇒ True | _ ⇒ False ]
     41   | acc ⇒ match A with [ ACCUMULATORA ⇒ True | _ ⇒ False ]
     42   | direct ⇒ match A with [ DIRECT _ ⇒ True | _ ⇒ False ]
     43   | indirect ⇒ match A with [ INDIRECT _ ⇒ True | _ ⇒ False ]].
     44
     45interpretation "Bool" 'or a b = (inclusive_disjunction a b).
     46
     47nlet rec is_in n (l: Vector all_types (S n)) (A:addressing_mode) on l : Bool ≝
     48 match l return λm.λ_:Vector all_types m .∀K:m=S n.Bool with
     49  [ Empty ⇒ λK.⊥
     50  | Cons m he (tl: Vector all_types m) ⇒ λ_.
     51     match m return λz.m = z → Bool with
     52      [ Z ⇒ λ_.is_a he A
     53      | S p ⇒ λK.is_a he A ∨ is_in p (? tl) A] (?: m=m)] (?: S n = S n).
     54##[##4: #x; ncases K; napply x ]
     55//; ndestruct.
     56nqed.
     57
     58nrecord subaddressing_mode (n) (l: Vector all_types (S n)) : Type[0] ≝
     59 { subaddressing_modeel:> addressing_mode;
     60   subaddressing_modein:
     61    match is_in ? l subaddressing_modeel with [ True ⇒ (? : Prop) | False ⇒ (? : Prop) ]
     62 }.
     63##[ napply True | napply False ]
     64nqed.
     65
     66ncoercion subaddressing_mode : ∀n.∀l:Vector all_types (S n).Type[0]
     67 ≝ subaddressing_mode on _l: Vector all_types (S ?) to Type[0].
     68
     69(*
     70ncoercion mk_subaddressing_mode :
     71 ∀n.∀l:Vector all_types (S n).∀a:addressing_mode.
     72  ∀p:?(*match is_in ? l a return λ_.Prop with [True ⇒ True | False ⇒ False]*).subaddressing_mode n l
     73 ≝ mk_subaddressing_mode on _a:addressing_mode to subaddressing_mode ? ?.
     74*)
    5675
    5776ninductive Jump (A: Type[0]): Type[0] ≝
     
    6382| JZ: A → Jump A
    6483| JNZ: A → Jump A
    65 | CJNE: (Cartesian (Union2 (Cartesian AccumulatorA (Either Direct Data)) (Cartesian (Either Register Indirect) Data)) A) → Jump A
    66 | DJNZ: Cartesian (Either Register Direct) A → Jump A.
    67 
    68 ndefinition Preamble ≝ List (Cartesian String Nat).
     84| CJNE: (([acc] × [direct; data]) + [reg; indirect] × [data]) → A → Jump A
     85| DJNZ: [reg ; direct] → A → Jump A
     86| ADD: [acc] → [reg; direct; indirect; data] → Jump A.
     87
     88ndefinition xxx: Jump Nat.
     89 napply (DJNZ ? (mk_subaddressing_mode ?? (REGISTER [True] [True] [True]) ?) (Z: Nat)).
     90 napply I;
     91nqed.
     92
     93naxiom bar: addressing_mode → Nat.
     94
     95ndefinition barj ≝
     96 λA.λf:A → Nat.λJ:Jump A.
     97  match J with
     98   [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1
     99   | _ ⇒ (Z: Nat)].
     100   
     101ndefinition PreInstruction ≝ λA: Type[0]. Jump A.
     102
     103ndefinition Instruction ≝ PreInstruction [rel].
     104
     105nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
     106   elem:> A;
     107   witness: T elem
     108}.
     109
     110interpretation "Sigma" 'sigma T = (Sigma ? T).
     111
     112ndefinition true: Bool ≝ True.
     113ndefinition false: Bool ≝ False.
     114naxiom daemon: False.
     115
     116naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
     117naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
     118
     119ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
     120 ≝
     121 [mk_Cartesian ??
     122   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
     123     (λl.
     124       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     125             (mk_subaddressing_mode ? ?    (decode_register l) ?));
     126  mk_Cartesian ??
     127   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
     128     (λl.
     129       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     130             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
     131ncases daemon.
     132nqed.
     133
     134
     135naxiom decode_register: List Bool → [reg].
     136naxiom decode_direct: List Bool → [direct].
     137
     138ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
     139 ≝
     140 [mk_Cartesian ??
     141   [ false; false; true; false; true]
     142     (λl.
     143       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     144             (mk_subaddressing_mode ? ?    (decode_register l) ?));
     145  mk_Cartesian ??
     146   [ false; false; true; false; true]
     147     (λl.
     148       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     149             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
     150ncases daemon.
     151nqed.
     152
     153
     154ndefinition decode_tbl1:
     155 List (List Bool × Σaddr:all_types. [addr] → Instruction)
     156 ≝
     157 [mk_Cartesian ??
     158   [ false; false; true; false; true]
     159   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
     160     reg
     161     (λa.
     162       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     163             (mk_subaddressing_mode ? ? a ?))) ].
     164ncases daemon.
     165nqed.
     166             
     167ndefinition decode_tbl2:
     168 List (List Bool × Σaddr:all_types. [addr] → Instruction)
     169 ≝
     170 [mk_Cartesian ??
     171   [ false; false; true; false; false; true; false; true]
     172   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
     173     direct
     174     (λa.
     175       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     176             (mk_subaddressing_mode ? ?     a ?))) ].
     177ncases daemon.
     178nqed.
     179
     180ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
     181
     182decode_addr_mode; ∀addr:all_types. List Bool → [addr].
     183
     184decode ≝
     185 λl:List Bit.
     186  List.iter
     187   (fun l0 addr mk_f →
     188     match split_prefix l l0 with
     189      [ None ⇒ ...
     190      | Some r ⇒ mk_f (decode_addr_mode r) ]
     191     
     192   ) decode_tbl
     193
     194encode ≝
     195
     196ndefinition decode_tbl:
     197 List (List Bool × Σaddr:all_types. [addr] → Instruction)
     198 ≝
     199 [mk_Cartesian ??
     200   [ False; False; True; False; True]
     201   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
     202     reg
     203     (λa:subaddressing_mode ? [reg].
     204       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     205             (mk_subaddressing_mode ? ?     a ?)));
     206  mk_Cartesian ??
     207   [ False; False; True; False; False; True; False; True]
     208   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
     209     direct
     210     (λa:subaddressing_mode ? [direct].
     211       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
     212             (mk_subaddressing_mode ? ?     a ?)))
     213 ].
     214nnormalize;
     215 
     216 ].
  • Deliverables/D4.1/Matita/List.ma

    r248 r256  
    2323
    2424notation "hvbox(hd break :: tl)"
    25   right associative with precedence 47
    26   for @{ 'Cons $hd $tl }.
    27 
    28 interpretation "List empty" 'Empty = (Empty ?).
    29 interpretation "List cons" 'Cons = (Cons ?).
    30  
     25  right associative with precedence 52
     26  for @{ 'cons $hd $tl }.
     27
    3128notation "[ list0 x sep ; ]"
    3229  non associative with precedence 90
    33   for @{ fold right @'Empty rec acc @{ 'Cons $x $acc } }.
     30  for ${fold right @'nil rec acc @{'cons $x $acc}}.
     31
     32interpretation "List empty" 'nil = (Empty ?).
     33interpretation "List cons" 'cons he tl = (Cons ? he tl).
    3434 
    3535notation "hvbox(l break !! break n)"
  • Deliverables/D4.1/Matita/Vector.ma

    r248 r256  
    2626(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    2727
    28 notation "hvbox(hd break :: tl)"
    29   right associative with precedence 52
    30   for @{ 'Cons $hd $tl }.
    31  
    32 interpretation "Vector cons" 'Cons hd tl = (Cons ? ? hd tl).
     28interpretation "Vector nil" 'nil = (Empty ?).
     29interpretation "Vector cons" 'cons hd tl = (Cons ? ? hd tl).
    3330
    3431notation "hvbox (v break !! n)"
Note: See TracChangeset for help on using the changeset viewer.