Changeset 264


Ignore:
Timestamp:
Nov 23, 2010, 5:05:07 PM (9 years ago)
Author:
sacerdot
Message:
  • new axiomatic data type for Strings
  • new file for Assembly
Location:
Deliverables/D4.1/Matita
Files:
1 added
4 edited

Legend:

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

    r262 r264  
    1 include "Universes.ma".
    2 include "Plogic/equality.ma".
    31include "Either.ma".
    4 include "BitVector.ma".
    52include "BitVectorTrie.ma".
     3include "String.ma".
    64
    75interpretation "Cartesian" 'product A B = (Cartesian A B).
     
    178176 | NOP: preinstruction A.
    179177
     178ndefinition instruction ≝ preinstruction [[relative]].
    180179
    181 ndefinition xxx: jump Nat.
    182  napply (DJNZ ? (REGISTER [true] [true] [true]) Z).
    183  napply I;
    184 nqed.
     180ninductive labelled_instruction: Type[0] ≝
     181   Instruction: instruction → labelled_instruction
     182 | Cost: String → labelled_instruction
     183 | Jmp: String → labelled_instruction
     184 | Call: String → labelled_instruction
     185 | Mov: [[dptr]] × String → labelled_instruction
     186 | WithLabel: preinstruction String → labelled_instruction.
    185187
    186 naxiom bar: addressing_mode → Nat.
     188ndefinition preamble ≝ List (String × Nat).
    187189
    188 ndefinition barj ≝
    189  λA.λf:A → Nat.λJ:Jump A.
    190   match J with
    191    [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1
    192    | _ ⇒ (Z: Nat)].
    193    
    194 ndefinition PreInstruction ≝ λA: Type[0]. Jump A.
    195 
    196 ndefinition Instruction ≝ PreInstruction [rel].
    197 
    198 nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
    199    elem:> A;
    200    witness: T elem
    201 }.
    202 
    203 interpretation "Sigma" 'sigma T = (Sigma ? T).
    204 
    205 naxiom daemon: False.
    206 
    207 naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
    208 naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
    209 
    210 ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
    211  ≝
    212  [mk_Cartesian ??
    213    (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
    214      (λl.
    215        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    216              (mk_subaddressing_mode ? ?    (decode_register l) ?));
    217   mk_Cartesian ??
    218    (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
    219      (λl.
    220        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    221              (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
    222 ncases daemon.
    223 nqed.
    224 
    225 
    226 naxiom decode_register: List Bool → [reg].
    227 naxiom decode_direct: List Bool → [direct].
    228 
    229 ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
    230  ≝
    231  [mk_Cartesian ??
    232    [ false; false; true; false; true]
    233      (λl.
    234        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    235              (mk_subaddressing_mode ? ?    (decode_register l) ?));
    236   mk_Cartesian ??
    237    [ false; false; true; false; true]
    238      (λl.
    239        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    240              (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
    241 ncases daemon.
    242 nqed.
    243 
    244 
    245 ndefinition decode_tbl1:
    246  List (List Bool × Σaddr:all_types. [addr] → Instruction)
    247  ≝
    248  [mk_Cartesian ??
    249    [ false; false; true; false; true]
    250    (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
    251      reg
    252      (λa.
    253        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    254              (mk_subaddressing_mode ? ? a ?))) ].
    255 ncases daemon.
    256 nqed.
    257              
    258 ndefinition decode_tbl2:
    259  List (List Bool × Σaddr:all_types. [addr] → Instruction)
    260  ≝
    261  [mk_Cartesian ??
    262    [ false; false; true; false; false; true; false; true]
    263    (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
    264      direct
    265      (λa.
    266        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    267              (mk_subaddressing_mode ? ?     a ?))) ].
    268 ncases daemon.
    269 nqed.
    270 
    271 ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
    272 
    273 decode_addr_mode; ∀addr:all_types. List Bool → [addr].
    274 
    275 decode ≝
    276  λl:List Bit.
    277   List.iter
    278    (fun l0 addr mk_f →
    279      match split_prefix l l0 with
    280       [ None ⇒ ...
    281       | Some r ⇒ mk_f (decode_addr_mode r) ]
    282      
    283    ) decode_tbl
    284 
    285 encode ≝
    286 
    287 ndefinition decode_tbl:
    288  List (List Bool × Σaddr:all_types. [addr] → Instruction)
    289  ≝
    290  [mk_Cartesian ??
    291    [ False; False; True; False; True]
    292    (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
    293      reg
    294      (λa:subaddressing_mode ? [reg].
    295        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    296              (mk_subaddressing_mode ? ?     a ?)));
    297   mk_Cartesian ??
    298    [ False; False; True; False; False; True; False; True]
    299    (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
    300      direct
    301      (λa:subaddressing_mode ? [direct].
    302        ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
    303              (mk_subaddressing_mode ? ?     a ?)))
    304  ].
    305 nnormalize;
    306  
    307  ].
     190ndefinition assembly_program ≝ preamble × (List labelled_instruction).
  • Deliverables/D4.1/Matita/Char.ma

    r249 r264  
    11include "Universes.ma".
    22
     3(*
    34ninductive Char: Type[0] ≝
    45  a: Char
     
    5455| Y: Char
    5556| Z: Char.
     57*)
  • Deliverables/D4.1/Matita/String.ma

    r249 r264  
    22include "List.ma".
    33
    4 ndefinition String ≝ List Char.
     4(*ndefinition String ≝ List Char.*)
     5naxiom String: Type[0].
  • Deliverables/D4.1/Matita/depends

    r261 r264  
     1Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    12Exponential.ma Connectives.ma Equality.ma Nat.ma
    2 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    33BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    44Cartesian.ma Universes.ma
    5 Universes.ma
    65Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    76Either.ma Bool.ma Maybe.ma Universes.ma
    8 ASM.ma BitVector.ma BitVectorTrie.ma Either.ma Plogic/equality.ma Universes.ma
     7Universes.ma
     8ASM.ma BitVectorTrie.ma Either.ma String.ma
     9Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    910Char.ma Universes.ma
    10 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    1111Connectives.ma Plogic/equality.ma
    1212Bool.ma Universes.ma
     13Assembly.ma ASM.ma
    1314List.ma Bool.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
    1415Util.ma Nat.ma
    1516Interpret.ma Arithmetic.ma BitVectorTrie.ma
    16 String.ma Char.ma List.ma
    1717BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1818Compare.ma Universes.ma
     19String.ma Char.ma List.ma
    1920Plogic/equality.ma Universes.ma
    2021Nat.ma Bool.ma Cartesian.ma Connectives.ma
Note: See TracChangeset for help on using the changeset viewer.