Changeset 362 for Deliverables/D4.1/Matita/Status.ma
 Timestamp:
 Dec 2, 2010, 11:53:49 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Status.ma
r357 r362 191 191 let sfr ≝ special_function_registers_8051 s in 192 192 let index ≝ sfr_8051_index i in 193 get_index ??sfr index ?.194 napply (sfr8051_index_nineteen i).193 get_index_v … sfr index ?. 194 napply sfr8051_index_nineteen. 195 195 nqed. 196 196 … … 200 200 let sfr ≝ special_function_registers_8052 s in 201 201 let index ≝ sfr_8052_index i in 202 get_index ??sfr index ?.203 napply (sfr8052_index_five i).202 get_index_v … sfr index ?. 203 napply sfr8052_index_five. 204 204 nqed. 205 205 … … 383 383 λs: Status. 384 384 let sfr ≝ special_function_registers_8051 s in 385 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in386 get_index Bool eight psw Z ?.385 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 386 get_index_v Bool eight psw Z ?. 387 387 nnormalize. 388 388 napply (less_than_or_equal_monotone ? ?). … … 395 395 λs: Status. 396 396 let sfr ≝ special_function_registers_8051 s in 397 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in398 get_index Bool eight psw (S Z) ?.397 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 398 get_index_v Bool eight psw (S Z) ?. 399 399 nnormalize. 400 400 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 407 407 λs: Status. 408 408 let sfr ≝ special_function_registers_8051 s in 409 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in410 get_index Bool eight psw two ?.409 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 410 get_index_v Bool eight psw two ?. 411 411 nnormalize. 412 412 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 419 419 λs: Status. 420 420 let sfr ≝ special_function_registers_8051 s in 421 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in422 get_index Bool eight psw three ?.421 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 422 get_index_v Bool eight psw three ?. 423 423 nnormalize. 424 424 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 431 431 λs: Status. 432 432 let sfr ≝ special_function_registers_8051 s in 433 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in434 get_index Bool eight psw four ?.433 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 434 get_index_v Bool eight psw four ?. 435 435 nnormalize. 436 436 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 443 443 λs: Status. 444 444 let sfr ≝ special_function_registers_8051 s in 445 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in446 get_index Bool eight psw five ?.445 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 446 get_index_v Bool eight psw five ?. 447 447 nnormalize. 448 448 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 455 455 λs: Status. 456 456 let sfr ≝ special_function_registers_8051 s in 457 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in458 get_index Bool eight psw six ?.457 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 458 get_index_v Bool eight psw six ?. 459 459 nnormalize. 460 460 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 467 467 λs: Status. 468 468 let sfr ≝ special_function_registers_8051 s in 469 let psw ≝ get_index Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in470 get_index Bool eight psw seven ?.469 let psw ≝ get_index_v Byte nineteen sfr (sfr_8051_index SFR_PSW) ? in 470 get_index_v Bool eight psw seven ?. 471 471 nnormalize. 472 472 nrepeat (napply (less_than_or_equal_monotone ? ?)). … … 482 482 λov: Bit. 483 483 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_PSW) in 484 let old_cy ≝ get_index 485 let old_ac ≝ get_index 486 let old_fo ≝ get_index 487 let old_rs1 ≝ get_index 488 let old_rs0 ≝ get_index 489 let old_ov ≝ get_index 490 let old_ud ≝ get_index 491 let old_p ≝ get_index 484 let old_cy ≝ get_index_v… nu Z ? in 485 let old_ac ≝ get_index_v… nu one ? in 486 let old_fo ≝ get_index_v… nu two ? in 487 let old_rs1 ≝ get_index_v… nu three ? in 488 let old_rs0 ≝ get_index_v… nl Z ? in 489 let old_ov ≝ get_index_v… nl one ? in 490 let old_ud ≝ get_index_v… nl two ? in 491 let old_p ≝ get_index_v… nl three ? in 492 492 let new_ac ≝ match ac with [ Nothing ⇒ old_ac  Just j ⇒ j ] in 493 493 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ; … … 655 655 λs: Status. 656 656 λr: BitVector three. 657 let b ≝ get_index_ bv ?r Z ? in658 let c ≝ get_index_ bv ?r one ? in659 let d ≝ get_index_ bv ?r two ? in657 let b ≝ get_index_v … r Z ? in 658 let c ≝ get_index_v … r one ? in 659 let d ≝ get_index_v … r two ? in 660 660 let 〈 un, ln 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 661 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_ bv four un two ?) (get_index_bvfour un three ?) in661 let 〈 r1, r0 〉 ≝ mk_Cartesian … (get_index_v … four un two ?) (get_index_v … four un three ?) in 662 662 let offset ≝ 663 663 if conjunction (negation r1) (negation r0) then … … 696 696 λs: Status. 697 697 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in 698 let m ≝ get_index_ bv … nu Z ? in699 let r1 ≝ get_index_ bv … nu one ? in700 let r2 ≝ get_index_ bv … nu two ? in701 let r3 ≝ get_index_ bv … nu three ? in698 let m ≝ get_index_v … nu Z ? in 699 let r1 ≝ get_index_v … nu one ? in 700 let r2 ≝ get_index_v … nu two ? in 701 let r3 ≝ get_index_v … nu three ? in 702 702 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 703 703 let memory ≝ … … 719 719 λv: Byte. 720 720 let 〈 nu, nl 〉 ≝ split … four four (get_8051_sfr s SFR_SP) in 721 let bit_zero ≝ get_index 722 let bit_one ≝ get_index 723 let bit_two ≝ get_index 724 let bit_three ≝ get_index 721 let bit_zero ≝ get_index_v… nu Z ? in 722 let bit_one ≝ get_index_v… nu one ? in 723 let bit_two ≝ get_index_v… nu two ? in 724 let bit_three ≝ get_index_v… nu three ? in 725 725 if bit_zero then 726 726 let memory ≝ insert … ([[ bit_one ; bit_two ; bit_three ]] @@ nl) … … 798 798 λdirect: True. 799 799 let 〈 nu, nl 〉 ≝ split … four four d in 800 let bit_one ≝ get_index_ bv … nu one ? in800 let bit_one ≝ get_index_v … nu one ? in 801 801 match bit_one with 802 802 [ true ⇒ … … 810 810 let 〈 nu, nl 〉 ≝ split ? four four (get_register s [[ false; false; i]]) in 811 811 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 812 let bit_one ≝ get_index_ bv … bit_one_v Z ? in812 let bit_one ≝ get_index_v … bit_one_v Z ? in 813 813 match bit_one with 814 814 [ true ⇒ … … 837 837 λdirect: True. 838 838 let 〈 nu, nl 〉 ≝ split … four four d in 839 let bit_one ≝ get_index_ bv … nu one ? in839 let bit_one ≝ get_index_v … nu one ? in 840 840 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 841 841 match bit_one with … … 849 849 let register ≝ get_register s [[ false; false; i ]] in 850 850 let 〈 nu, nl 〉 ≝ split ? four four register in 851 let bit_one ≝ get_index_ bv ?nu one ? in851 let bit_one ≝ get_index_v … nu one ? in 852 852 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 853 853 match bit_one with … … 909 909 λbit_addr: True. 910 910 let 〈 nu, nl 〉 ≝ split … four four b in 911 let bit_one ≝ get_index_ bv … nu one ? in911 let bit_one ≝ get_index_v … nu one ? in 912 912 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 913 913 match bit_one with … … 918 918 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 919 919 let sfr ≝ get_bit_addressable_sfr s ? trans l in 920 get_index_ bv ?sfr m ?920 get_index_v … sfr m ? 921 921  false ⇒ 922 922 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 923 923 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 924 924 let t ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 925 get_index_ bv ?t (modulus address eight) ?925 get_index_v … t (modulus address eight) ? 926 926 ] 927 927  N_BIT_ADDR n ⇒ 928 928 λn_bit_addr: True. 929 929 let 〈 nu, nl 〉 ≝ split … four four n in 930 let bit_one ≝ get_index_ bv … nu one ? in930 let bit_one ≝ get_index_v … nu one ? in 931 931 let 〈 bit_one_v, three_bits 〉 ≝ split ? one three nu in 932 932 match bit_one with … … 937 937 let trans ≝ bitvector_of_nat eight ((d * eight) + one_hundred_and_twenty_eight) in 938 938 let sfr ≝ get_bit_addressable_sfr s ? trans l in 939 negation (get_index_ bv ?sfr m ?)939 negation (get_index_v … sfr m ?) 940 940  false ⇒ 941 941 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 942 942 let address' ≝ bitvector_of_nat seven ((address ÷ eight) + thirty_two) in 943 943 let trans ≝ lookup … seven address' (low_internal_ram s) (zero eight) in 944 negation (get_index_ bv ?trans (modulus address eight) ?)944 negation (get_index_v … trans (modulus address eight) ?) 945 945 ] 946 946  CARRY ⇒ λcarry: True. get_cy_flag s … … 963 963 [ BIT_ADDR b ⇒ λbit_addr: True. 964 964 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 965 let bit_one ≝ get_index_ bv ?nu one ? in965 let bit_one ≝ get_index_v … nu one ? in 966 966 let 〈 ignore, three_bits 〉 ≝ split ? one three nu in 967 967 match bit_one with … … 985 985 λcarry: True. 986 986 let 〈 nu, nl 〉 ≝ split ? four four (get_8051_sfr s SFR_PSW) in 987 let bit_one ≝ get_index 988 let bit_two ≝ get_index 989 let bit_three ≝ get_index 987 let bit_one ≝ get_index_v… nu one ? in 988 let bit_two ≝ get_index_v… nu two ? in 989 let bit_three ≝ get_index_v… nu three ? in 990 990 let new_psw ≝ [[ v; bit_one ; bit_two; bit_three ]] @@ nl in 991 991 set_8051_sfr s SFR_PSW new_psw
Note: See TracChangeset
for help on using the changeset viewer.