Changeset 331


Ignore:
Timestamp:
Nov 29, 2010, 2:32:13 PM (9 years ago)
Author:
mulligan
Message:

More changes to get everything to typecheck.

Location:
Deliverables/D4.1/Matita
Files:
3 edited

Legend:

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

    r329 r331  
    2323                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
    2424                                                           (get_arg_8 s false (REGISTER r)) false in
    25                     let cy_flag ≝ get_index ? flags Z in
    26                     let ac_flag ≝ get_index ? flags one in
    27                     let ov_flag ≝ get_index ? flags two in
     25                    let cy_flag ≝ get_index … flags Z ? in
     26                    let ac_flag ≝ get_index … flags one ? in
     27                    let ov_flag ≝ get_index … flags two ? in
    2828                    let s ≝ set_arg_8 s ACC_A result in
    29                       set_flags s cy_flag (Just? ac_flag) ov_flag
    30                   | DIRECT d ⇒ λdirect: True. ?
    31                   | INDIRECT i ⇒ λindirect: True. ?
    32                   | DATA d ⇒ λdata: True. ?
     29                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     30                  | DIRECT d ⇒ λdirect: True.
     31                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     32                                                           (get_arg_8 s false (DIRECT d)) false in
     33                    let cy_flag ≝ get_index … flags Z ? in
     34                    let ac_flag ≝ get_index … flags one ? in
     35                    let ov_flag ≝ get_index … flags two ? in
     36                    let s ≝ set_arg_8 s ACC_A result in
     37                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     38                  | INDIRECT i ⇒ λindirect: True.
     39                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     40                                                           (get_arg_8 s false (INDIRECT i)) false in
     41                    let cy_flag ≝ get_index … flags Z ? in
     42                    let ac_flag ≝ get_index … flags one ? in
     43                    let ov_flag ≝ get_index … flags two ? in
     44                    let s ≝ set_arg_8 s ACC_A result in
     45                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     46                  | DATA d ⇒ λdata: True.
     47                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     48                                                           (get_arg_8 s false (DATA d)) false in
     49                    let cy_flag ≝ get_index … flags Z ? in
     50                    let ac_flag ≝ get_index … flags one ? in
     51                    let ov_flag ≝ get_index … flags two ? in
     52                    let s ≝ set_arg_8 s ACC_A result in
     53                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     54                  | _ ⇒ λother: False. ?
     55                  ] (subaddressing_modein … addr2)
     56            | _ ⇒ λother: False. ?
     57            ] (subaddressing_modein … addr1)
     58        | ADDC addr1 addr2 ⇒
     59            let old_cy_flag ≝ get_cy_flag s in
     60            match addr1 return λx. bool_to_Prop (is_in … [[ acc_a ]] x) → ? with
     61              [ ACC_A ⇒ λacc_a: True.
     62                match addr2 return λx. bool_to_Prop (is_in … [[ register;
     63                                                                direct;
     64                                                                indirect;
     65                                                                data ]] x) → ? with
     66                  [ REGISTER r ⇒ λregister: True.
     67                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     68                                                           (get_arg_8 s false (REGISTER r)) old_cy_flag in
     69                    let cy_flag ≝ get_index … flags Z ? in
     70                    let ac_flag ≝ get_index … flags one ? in
     71                    let ov_flag ≝ get_index … flags two ? in
     72                    let s ≝ set_arg_8 s ACC_A result in
     73                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     74                  | DIRECT d ⇒ λdirect: True.
     75                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     76                                                           (get_arg_8 s false (DIRECT d)) old_cy_flag in
     77                    let cy_flag ≝ get_index … flags Z ? in
     78                    let ac_flag ≝ get_index … flags one ? in
     79                    let ov_flag ≝ get_index … flags two ? in
     80                    let s ≝ set_arg_8 s ACC_A result in
     81                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     82                  | INDIRECT i ⇒ λindirect: True.
     83                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     84                                                           (get_arg_8 s false (INDIRECT i)) old_cy_flag in
     85                    let cy_flag ≝ get_index … flags Z ? in
     86                    let ac_flag ≝ get_index … flags one ? in
     87                    let ov_flag ≝ get_index … flags two ? in
     88                    let s ≝ set_arg_8 s ACC_A result in
     89                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
     90                  | DATA d ⇒ λdata: True.
     91                    let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 s false ACC_A)
     92                                                           (get_arg_8 s false (DATA d)) old_cy_flag in
     93                    let cy_flag ≝ get_index … flags Z ? in
     94                    let ac_flag ≝ get_index … flags one ? in
     95                    let ov_flag ≝ get_index … flags two ? in
     96                    let s ≝ set_arg_8 s ACC_A result in
     97                      set_flags s cy_flag (Just Bit ac_flag) ov_flag
    3398                  | _ ⇒ λother: False. ?
    3499                  ] (subaddressing_modein … addr2)
  • Deliverables/D4.1/Matita/List.ma

    r330 r331  
    137137        [ Empty ⇒ Nothing (List A)
    138138        | Cons hd tl ⇒
    139             let settail ≝ set_index A tl o a in
     139            let settail ≝ set_index_weak A tl o a in
    140140              match settail with
    141141                [ Nothing ⇒ Nothing (List A)
  • Deliverables/D4.1/Matita/Status.ma

    r329 r331  
    180180                old_clock.
    181181
     182alias id "get_index" = "cic:/matita/ng/Vector/get_index.fix(0,3,2)".
    182183ndefinition get_8051_sfr ≝
    183184  λs: Status.
Note: See TracChangeset for help on using the changeset viewer.