Changeset 264 for Deliverables/D4.1/Matita/ASM.ma

Timestamp:

Nov 23, 2010, 5:05:07 PM (9 years ago)

Author:

sacerdot

Message:

• new axiomatic data type for Strings
• new file for Assembly

File:

• Deliverables/D4.1/Matita/ASM.ma (modified) (2 diffs)

Deliverables/D4.1/Matita/ASM.ma

@@ -1 @@
-include "Universes.ma".
-include "Plogic/equality.ma".
 include "Either.ma".
-include "BitVector.ma".
 include "BitVectorTrie.ma".
+include "String.ma".
 
 interpretation "Cartesian" 'product A B = (Cartesian A B).
@@ -178 +176 @@
  | NOP: preinstruction A.
 
+ndefinition instruction ≝ preinstruction [[relative]].
 
-ndefinition xxx: jump Nat.
- napply (DJNZ ? (REGISTER [true] [true] [true]) Z).
- napply I;
-nqed.
+ninductive labelled_instruction: Type[0] ≝
+   Instruction: instruction → labelled_instruction
+ | Cost: String → labelled_instruction
+ | Jmp: String → labelled_instruction
+ | Call: String → labelled_instruction
+ | Mov: [[dptr]] × String → labelled_instruction
+ | WithLabel: preinstruction String → labelled_instruction.
 
-naxiom bar: addressing_mode → Nat.
+ndefinition preamble ≝ List (String × Nat).
 
-ndefinition barj ≝
- λA.λf:A → Nat.λJ:Jump A.
-  match J with
-   [ DJNZ arg1 arg2 ⇒ f arg2 + bar arg1
-   | _ ⇒ (Z: Nat)].
-   
-ndefinition PreInstruction ≝ λA: Type[0]. Jump A.
-
-ndefinition Instruction ≝ PreInstruction [rel].
-
-nrecord Sigma (A: Type[0]) (T: A → Type[0]) : Type[0] ≝ {
-   elem:> A;
-   witness: T elem
-}.
-
-interpretation "Sigma" 'sigma T = (Sigma ? T). 
-
-naxiom daemon: False.
-
-naxiom decode_register: Vector Bool (S (S (S Z))) → [reg].
-naxiom decode_direct:   Vector Bool (S (S (S Z))) → [direct].
-
-ndefinition decode_tbl0: List ((Σn.Vector Bool n) × (Vector Bool (S (S (S Z))) → Instruction))
- ≝
- [mk_Cartesian ??
-   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
-     (λl.
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ?    (decode_register l) ?));
-  mk_Cartesian ??
-   (mk_Sigma ? (λn.Vector Bool n) ? [ false; false; true; false; true])
-     (λl.
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
-ncases daemon.
-nqed.
-
-
-naxiom decode_register: List Bool → [reg].
-naxiom decode_direct: List Bool → [direct].
-
-ndefinition decode_tbl0: List (List Bool × (List Bool → Instruction))
- ≝
- [mk_Cartesian ??
-   [ false; false; true; false; true]
-     (λl.
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ?    (decode_register l) ?));
-  mk_Cartesian ??
-   [ false; false; true; false; true]
-     (λl.
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ? (decode_direct l) ?)) ].
-ncases daemon.
-nqed.
-
-
-ndefinition decode_tbl1:
- List (List Bool × Σaddr:all_types. [addr] → Instruction)
- ≝
- [mk_Cartesian ??
-   [ false; false; true; false; true]
-   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
-     reg
-     (λa.
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ? a ?))) ].
-ncases daemon.
-nqed.
-             
-ndefinition decode_tbl2:
- List (List Bool × Σaddr:all_types. [addr] → Instruction)
- ≝
- [mk_Cartesian ??
-   [ false; false; true; false; false; true; false; true]
-   (mk_Sigma ? (λaddr:all_types. [addr] → Instruction)
-     direct
-     (λa.
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ?     a ?))) ].
-ncases daemon.
-nqed.
-
-ndefinition decode_tbl ≝ decode_tbl1 @ decode_tbl2.
-
-decode_addr_mode; ∀addr:all_types. List Bool → [addr].
-
-decode ≝
- λl:List Bit.
-  List.iter
-   (fun l0 addr mk_f →
-     match split_prefix l l0 with
-      [ None ⇒ ...
-      | Some r ⇒ mk_f (decode_addr_mode r) ] 
-      
-   ) decode_tbl
-
-encode ≝
-
-ndefinition decode_tbl:
- List (List Bool × Σaddr:all_types. [addr] → Instruction)
- ≝
- [mk_Cartesian ??
-   [ False; False; True; False; True]
-   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
-     reg
-     (λa:subaddressing_mode ? [reg].
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ?     a ?)));
-  mk_Cartesian ??
-   [ False; False; True; False; False; True; False; True]
-   (mk_Sigma all_types (λaddr:all_types. [addr] → Instruction)
-     direct
-     (λa:subaddressing_mode ? [direct].
-       ADD ? (mk_subaddressing_mode ? [acc] ACCUMULATORA ?)
-             (mk_subaddressing_mode ? ?     a ?)))
- ].
-nnormalize; 
- 
- ].
+ndefinition assembly_program ≝ preamble × (List labelled_instruction).