Changeset 414

Timestamp:

Dec 13, 2010, 6:03:05 PM (9 years ago)

Author:

mulligan

Message:

Got a few more cases working.

Location:

Deliverables/D4.1/Matita

Files:

• Assembly.ma (modified) (4 diffs)
• Map.ma (modified) (2 diffs)
• String.ma (modified) (1 diff)
• depends (modified) (2 diffs)

Deliverables/D4.1/Matita/Assembly.ma

@@ -430 +430 @@
           let 〈name, size〉 ≝ preamble in
           let addr_sixteen ≝ bitvector_of_nat sixteen addr in
-            〈insert ? ? addr_sixteen name datalabels, addr + size〉)
+            〈insert ? ? (bitvector_of_string ? name) addr_sixteen datalabels, addr + size〉)
               〈(Stub ? ?), Z〉 preamble in
     let 〈pc_labels, costs〉 ≝
@@ -440 +440 @@
               [ Instruction instr ⇒
                 let code_memory ≝ load_code_memory (assembly1 instr) in
-                let 〈instr_pc', ignore〉  ≝ fetch code_memory (zero sixteen) in
+                let 〈instr_pc', ignore〉 ≝ fetch code_memory (zero sixteen) in
                 let 〈instr', program_counter'〉 ≝ instr_pc' in
                 let program_counter_n' ≝ nat_of_bitvector ? program_counter' in
@@ -446 +446 @@
               | Label label ⇒
                 let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
-                  〈〈program_counter, (insert ? ? program_counter_bv label labels)〉, costs〉
+                  〈〈program_counter, (insert ? ? (bitvector_of_string ? label) program_counter_bv labels)〉, costs〉
               | Cost cost ⇒
                 let program_counter_bv ≝ bitvector_of_nat sixteen program_counter in
@@ -479 +479 @@
                   | Call call ⇒
                     let pc_offset ≝ lookup ? ? (bitvector_of_string ? call) labels (zero ?) in
-                    let address ≝ ADDR16 (bitvector_of_nat sixteen pc_offset) in
-                      assembly1 (LCALL address)
-                  | _ ⇒ ?
+                    let address ≝ ADDR16 pc_offset in
+                      assembly1 (LCALL ? address)
+                  | Mov d trgt ⇒
+                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
+                    let address ≝ DATA16 pc_offset in
+                      assembly1 (MOV ? (Right ? ?(Right ? ? (Right ? ? (Right ? ? (Right ? ? 〈DPTR, address〉))))))
+                  | Instruction instr ⇒ ?
+                  | Jmp jmp ⇒
+                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
+                    let address ≝ ADDR16 pc_offset in
+                      assembly1 (LJMP ? address)
+                  | WithLabel jmp ⇒ ?
                   ]
             ) instr_list

Deliverables/D4.1/Matita/Map.ma

@@ -1 +1 @@
 include "Universes.ma".
 include "Compare.ma".
+include "Maybe.ma".
 
 ninductive Map (A: Type[0]) (B: Type[0]): Type[0] ≝
@@ -7 +8 @@
 | Node: A → B → Map A B → Map A B → Map A B.
 
+(* Greater than or equal to the right, less than to the left.  *)
+
 nlet rec insert (A: Type[0]) (B: Type[0])
-                (key: A) (f: A → A → Compare) (value: B) (map: Map A B) ≝
+                (key: A) (f: A → A → Compare) (value: B) (map: Map A B) on map ≝
   match map with
-    [ Empty ⇒ Leaf key value
+    [ Empty ⇒ Leaf … key value
     | Leaf key' value' ⇒
       match f key key' with
-        [ Equal ⇒ ?
-        | Less ⇒ ?
-        | Greater ⇒ ?
+        [ Equal ⇒ Node … key' value' (Empty …) (Leaf … key value)
+        | Less ⇒ Node … key' value' (Leaf … key value) (Empty …)
+        | Greater ⇒ Node … key' value' (Empty …) (Leaf … key value)
         ]
-    | Node key' value' ⇒
+    | Node key' value' left right ⇒
       match f key key' with
-        [ Equal ⇒ ?
-        | Less ⇒ ?
-        | Greater ?
+        [ Equal ⇒ Node A B key' value' left (insert A B key f value right)
+        | Less ⇒ Node A B key' value' (insert A B key f value left) right
+        | Greater ⇒ Node A B key' value' left (insert A B key f value right)
         ]
     ].
+    
+nlet rec lookup (A: Type[0]) (B: Type[0])
+                (key: A) (f: A → A → Compare) (map: Map A B) on map ≝
+  match map with
+    [ Empty ⇒ Nothing ?
+    | Leaf key' value' ⇒
+      match f key key' with
+        [ Equal ⇒ Just ? value'
+        | _ ⇒ Nothing ?
+        ]
+    | Node key' value' left right ⇒
+      match f key key' with
+        [ Equal ⇒ Just ? value'
+        | Less ⇒ lookup A B key f left
+        | Greater ⇒ lookup A B key f right
+        ]
+    ].

Deliverables/D4.1/Matita/String.ma

@@ -1 +1 @@
 include "Char.ma".
 include "List.ma".
+include "Compare.ma".
 
 ndefinition String ≝ List Char.
+
+naxiom string_lexicographic_ordering: String → String → Compare.

Deliverables/D4.1/Matita/depends

@@ -9 +9 @@
 DoTest.ma Assembly.ma Interpret.ma Test.ma
 ASM.ma BitVector.ma Either.ma String.ma
+Map.ma Compare.ma Maybe.ma Universes.ma
 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
 Char.ma Universes.ma
@@ -15 +16 @@
 Connectives.ma Plogic/equality.ma
 Bool.ma Universes.ma
-Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Status.ma
+Assembly.ma ASM.ma Arithmetic.ma BitVectorTrie.ma Fetch.ma Map.ma Status.ma
 List.ma Maybe.ma Util.ma
 Interpret.ma Fetch.ma Status.ma
 Util.ma Nat.ma
+Compare.ma Universes.ma
 BitVector.ma String.ma Vector.ma
 String.ma Char.ma List.ma