Changeset 1515 for src/ASM/Interpret.ma

Timestamp:

Nov 18, 2011, 1:03:14 PM (9 years ago)

Author:

campbell

Message:

Add type of maps on positive binary numbers, and use them for identifers.

Also:

• fix interpretation for - on positives
• move eq_nat_dec to a more appropriate place
• split out costs from other identifiers in ASM
• use identifier abstractions in back-end

File:

• src/ASM/Interpret.ma (modified) (1 diff)

src/ASM/Interpret.ma

@@ -686 +686 @@
       let preamble ≝ \fst (code_memory ? s) in
       let data_labels ≝ construct_datalabels (map … (fst …) preamble) in
-        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup ? ? ident data_labels (zero ?)))) dptr
+        set_arg_16 ? s (get_arg_16 ? s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
     ]
   in