Changeset 290 for Deliverables/D4.1/Matita/Status.ma
- Timestamp:
- Nov 25, 2010, 12:48:34 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/Matita/Status.ma
r289 r290 410 410 nrepeat (napply (less_than_or_equal_monotone ? ?)). 411 411 napply (less_than_or_equal_zero). 412 nqed. 413 414 ndefinition set_flags ≝ 415 λs: Status. 416 λcy: Bit. 417 λac: Maybe Bit. 418 λov: Bit. 419 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in 420 let old_cy ≝ get_index … nu Z ? in 421 let old_ac ≝ get_index … nu one ? in 422 let old_fo ≝ get_index … nu two ? in 423 let old_rs1 ≝ get_index … nu three ? in 424 let old_rs0 ≝ get_index … nl Z ? in 425 let old_ov ≝ get_index … nl one ? in 426 let old_ud ≝ get_index … nl two ? in 427 let old_p ≝ get_index … nl three ? in 428 let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in 429 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; 430 old_rs0 ; old_ov ; old_ud ; old_p ]] in 431 set_8051_sfr s SFR_PSW new_psw. 432 ##[##1,2,3,4,5,6,7,8: 433 nnormalize; 434 nrepeat (napply less_than_or_equal_monotone); 435 napply (less_than_or_equal_zero); 436 ##] 412 437 nqed. 413 438 … … 600 625 set_low_internal_ram s new_low_internal_ram. 601 626 602 ndefinition set_flags ≝603 λs: Status.604 λcy: Bit.605 λac: Maybe Bit.606 λov: Bit.607 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in608 let old_cy ≝ get_index … nu Z ? in609 let old_ac ≝ get_index … nu one ? in610 let old_fo ≝ get_index … nu two ? in611 let old_rs1 ≝ get_index … nu three ? in612 let old_rs0 ≝ get_index … nl Z ? in613 let old_ov ≝ get_index … nl one ? in614 let old_ud ≝ get_index … nl two ? in615 let old_p ≝ get_index … nl three ? in616 let new_ac ≝ match ac with [ Nothing ⇒ old_ac | Just j ⇒ j ] in617 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;618 old_rs0 ; old_ov ; old_ud ; old_p ]] in619 set_8051_sfr s SFR_PSW new_psw.620 ##[##1,2,3,4,5,6,7,8:621 nnormalize;622 nrepeat (napply less_than_or_equal_monotone);623 napply (less_than_or_equal_zero);624 ##]625 nqed.626 627 627 ndefinition read_at_stack_pointer ≝ 628 628 λs: Status.
Note: See TracChangeset
for help on using the changeset viewer.