Changeset 421 for Deliverables/D4.1/Matita/Assembly.ma

Timestamp:

Dec 14, 2010, 4:13:55 PM (10 years ago)

Author:

mulligan

Message:

Removed duplicate "assembly1" function. Removed Ocaml code from file.

File:

• Deliverables/D4.1/Matita/Assembly.ma (modified) (1 diff)

Deliverables/D4.1/Matita/Assembly.ma

@@ -528 +528 @@
 
 (*
-let load_code_memory = fold_lefti (fun i mem v -> WordMap.add (vect_of_int i `Sixteen) v mem) WordMap.empty
-
-let load_mem mem status = { status with code_memory = mem }
-let load l = load_mem (load_code_memory l)
-
-module StringMap = Map.Make(String);;
-module IntMap = Map.Make(struct type t = int let compare = compare end);;
-
-
-let assembly_jump addr_of =
- function
-    `JC a1 -> `JC (addr_of a1)
-  | `JNC a1 -> `JNC (addr_of a1)
-  | `JB (a1,a2) -> `JB (a1,addr_of a2)
-  | `JNB (a1,a2) -> `JNB (a1,addr_of a2)
-  | `JBC (a1,a2) -> `JBC (a1,addr_of a2)
-  | `JZ a1 -> `JZ (addr_of a1)
-  | `JNZ a1 -> `JNZ (addr_of a1)
-  | `CJNE (a1,a2) -> `CJNE (a1,addr_of a2)
-  | `DJNZ (a1,a2) -> `DJNZ (a1,addr_of a2)
-;;
-
-let assembly (preamble,l) =
- let datalabels,_ =
-  List.fold_left
-   (fun (datalabels,addr) (name,size) ->
-     let addr16 = vect_of_int addr `Sixteen in
-      StringMap.add name addr16 datalabels, addr+size
-   ) (StringMap.empty,0) preamble
- in
- let pc,labels,costs =
-  List.fold_left
-   (fun (pc,labels,costs) i ->
-     match i with
-        `Label s -> pc, StringMap.add s pc labels, costs
-      | `Cost s -> pc, labels, IntMap.add pc s costs
-      | `Mov (_,_) -> pc, labels, costs
-      | `Jmp _ 
-      | `Call _ -> pc + 3, labels, costs  (*CSC: very stupid: always expand to worst opcode *)
-      | `WithLabel i ->
-          let fake_addr _ = `REL (zero `Eight) in
-          let fake_jump = assembly_jump fake_addr i in
-          let i',pc',_ = fetch (load_code_memory (assembly1 fake_jump)) (vect_of_int 0 `Sixteen) in
-           assert (fake_jump = i');
-           (pc + int_of_vect pc',labels, costs)
-      | #instruction as i ->
-        let i',pc',_ = fetch (load_code_memory (assembly1 i)) (vect_of_int 0 `Sixteen) in
-         assert (i = i');
-         (pc + int_of_vect pc',labels, costs)
-   ) (0,StringMap.empty,IntMap.empty) l
- in
-  if pc >= 65536 then
-   raise CodeTooLarge
-  else
-      List.flatten (List.map
-         (function
-            `Label _
-          | `Cost _ -> []
-          | `WithLabel i ->
-              let addr_of (`Label s) =
-               let addr = StringMap.find s labels in
-               (* NOT IMPLEMENTED YET; NEEDS SMART ALGORITHM *)
-                assert (addr < 256);
-                `REL (vect_of_int addr `Eight)
-              in
-               assembly1 (assembly_jump addr_of i)
-          | `Mov (`DPTR,s) ->
-              let addrr16 = StringMap.find s datalabels in
-               assembly1 (`MOV (`U4 (`DPTR,`DATA16 addrr16)))
-          | `Jmp s ->
-              let pc_offset = StringMap.find s labels in
-                assembly1 (`LJMP (`ADDR16 (vect_of_int pc_offset `Sixteen)))
-          | `Call s ->
-              let pc_offset = StringMap.find s labels in
-                assembly1 (`LCALL (`ADDR16 (vect_of_int pc_offset `Sixteen)))
-          | #instruction as i -> assembly1 i) l), costs
-;;
-*)
-
 ndefinition assembly: List instruction → List Byte ≝
  fold_right … (λi,l. assembly1 i @ l) [].
+*)