Changeset 364 for Deliverables
 Timestamp:
 Dec 2, 2010, 4:36:35 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Interpret.ma
r363 r364 5 5 λb. 6 6 zero eight @@ b. 7 8 naxiom daemon: False. 9 7 8 naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool. 9 10 nlemma execute_1_technical: 11 ∀n,m: Nat. 12 ∀v: Vector addressing_mode_tag (S n). 13 ∀q: Vector addressing_mode_tag (S m). 14 ∀a: addressing_mode. 15 bool_to_Prop (is_in ? v a) → 16 bool_to_Prop (subvector_with ? ? ? eq_a v q) → 17 bool_to_Prop (is_in ? q a). 18 #n m v q a. 19 ncases a. 20 nnormalize. 21 10 22 ndefinition execute_1: Status → Status ≝ 11 23 λs. … … 189 201 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 190 202 let new_cy_flag ≝ get_index' ? Z ? old_acc in 191 let new_acc ≝ shift_left _bveight one old_acc old_cy_flag in203 let new_acc ≝ shift_left ? eight one old_acc old_cy_flag in 192 204 let s ≝ set_arg_1 s CARRY new_cy_flag in 193 205 set_8051_sfr s SFR_ACC_A new_acc … … 196 208 let old_acc ≝ get_8051_sfr s SFR_ACC_A in 197 209 let new_cy_flag ≝ get_index' ? seven ? old_acc in 198 let new_acc ≝ shift_right _bveight one old_acc old_cy_flag in210 let new_acc ≝ shift_right ? eight one old_acc old_cy_flag in 199 211 let s ≝ set_arg_1 s CARRY new_cy_flag in 200 212 set_8051_sfr s SFR_ACC_A new_acc … … 486 498 in 487 499 s. 488 ##[ ##2,3,4,8,9,10,14,15,16,43,104,106:489 nnormalize;490 nrepeat (napply (less_than_or_equal_monotone));491 napply (less_than_or_equal_zero);492 ####23,28,29,30,31,32,33,34,35,36,37,38,39,40,64,65,66,493 67,68,69,70,71,72,73,74,75,76,79,80,81,82,117,118,119,494 120,121,122,123,124,125,126,127,128,129,130,131,132,495 133,139,140,141,142,143,144,145,146,147,148,149,150,496 151,152,153,154,155,156,162,163,164,165,166,167,168,497 169,170,171,172,173,174,175,176,177,178,179,180,181,498 182,183,184,185,186,187,188,189,190,191,192,193,194,499 195,196,197,198,199,200,201,202,203,204,205,206,207,500 208,209,210,211,212,213:501 nassumption;500 ##[ ntry 501 nassumption; 502 ## ntry ( 503 nnormalize 504 nrepeat (napply (less_than_or_equal_monotone)) 505 napply (less_than_or_equal_zero) 506 ); 507 ## ntry ( 508 nnormalize 509 // 510 ); 511 ## ntry ( 512 nnormalize 513 //); 502 514 ## 503 515 nqed. 
Deliverables/D4.1/Matita/List.ma
r357 r364 53 53 for @{ 'append $l $r }. 54 54 55 interpretation "List append" 'append = (append ?). 55 interpretation "List append" 'append = (append ?). 56 57 (* ===================================== *) 58 (* Maps and zips. *) 59 (* ===================================== *) 60 61 nlet rec map (A: Type[0]) (B: Type[0]) 62 (f: A → B) (l: List A) on l ≝ 63 match l with 64 [ Empty ⇒ Empty B 65  Cons hd tl ⇒ f hd :: map A B f tl 66 ]. 67 68 nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝ 69 match l with 70 [ Empty ⇒ Empty A 71  Cons hd tl ⇒ hd @ (flatten A tl) 72 ]. 73 74 ndefinition map_flatten ≝ 75 λA: Type[0]. 76 λf: A → List A. 77 λl: List A. 78 flatten A (map A (List A) f l). 56 79 57 80 (* ===================================== *) … … 69 92 [ Empty ⇒ Empty A 70 93  Cons hd tl ⇒ reverse A tl @ (hd :: Empty A) 94 ]. 95 96 nlet rec power_list (A: Type[0]) (l: List A) on l ≝ 97 match l with 98 [ Empty ⇒ [ [ ] ] 99  Cons hd tl ⇒ 100 let r ≝ power_list A tl in 101 (map ? ? (λx. hd :: x) r) @ r 71 102 ]. 72 103 … … 284 315 285 316 (* ===================================== *) 286 (* Maps and zips. *)287 (* ===================================== *)288 289 nlet rec map (A: Type[0]) (B: Type[0])290 (f: A → B) (l: List A) on l ≝291 match l with292 [ Empty ⇒ Empty B293  Cons hd tl ⇒ f hd :: map A B f tl294 ].295 296 nlet rec flatten (A: Type[0]) (l: List (List A)) on l ≝297 match l with298 [ Empty ⇒ Empty A299  Cons hd tl ⇒ hd @ (flatten A tl)300 ].301 302 ndefinition map_flatten ≝303 λA: Type[0].304 λf: A → List A.305 λl: List A.306 flatten A (map A (List A) f l).307 308 (* ===================================== *)309 317 (* Setlike operations. *) 310 318 (* ===================================== *) … … 340 348 λm: Nat. 341 349 reverse A (rotate_left A (reverse A l) m). 350 351 (* ===================================== *) 352 (* Decidable equality. *) 353 (* ===================================== *) 354 355 nlet rec eq_l (A: Type[0]) (f: A → A → Bool) (l: List A) (m: List A) on l ≝ 356 match l with 357 [ Empty ⇒ 358 match m with 359 [ Empty ⇒ true 360  Cons hd tl ⇒ false 361 ] 362  Cons hd tl ⇒ 363 match m with 364 [ Empty ⇒ false 365  Cons hd' tl' ⇒ conjunction (f hd hd') (eq_l A f tl tl') 366 ] 367 ]. 342 368 343 369 (* ===================================== *) 
Deliverables/D4.1/Matita/Vector.ma
r363 r364 410 410 napply tl' ] 411 411 nqed. 412 413 (* ===================================== *) 414 (* Subvectors. *) 415 (* ===================================== *) 416 417 ndefinition subvector_with ≝ 418 λA: Type[0]. 419 λn: Nat. 420 λm: Nat. 421 λf: A → A → Bool. 422 λv: Vector A n. 423 λq: Vector A m. 424 let list_q ≝ list_of_vector A m q in 425 let list_v ≝ list_of_vector A n v in 426 let power ≝ power_list A list_q in 427 member_with ? list_v (λx, y. eq_l ? f x y) power. 412 428 413 429 (* ===================================== *) 
Deliverables/D4.1/Matita/depends
r357 r364 1 Exponential.ma Nat.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 1 3 Arithmetic.ma BitVector.ma Exponential.ma 2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma3 Exponential.ma Nat.ma4 4 BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma 5 5 Cartesian.ma Universes.ma 6 Universes.ma 6 7 Maybe.ma Bool.ma Plogic/equality.ma 7 8 Either.ma Bool.ma 8 Universes.ma 9 DoTest.ma Interpret.ma Test.ma 9 DoTest.ma Assembly.ma Interpret.ma Test.ma 10 10 ASM.ma BitVector.ma Either.ma String.ma 11 Vector.ma List.ma Nat.ma12 11 Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma 13 12 Char.ma Universes.ma 14 13 Test.ma ASM.ma 14 Vector.ma List.ma Nat.ma 15 15 Connectives.ma Plogic/equality.ma 16 16 Bool.ma Universes.ma 17 17 Assembly.ma ASM.ma 18 18 List.ma Maybe.ma Util.ma 19 Interpret.ma Fetch.ma Status.ma 19 20 Util.ma Nat.ma 20 Interpret.ma Fetch.ma Status.ma21 21 BitVector.ma Vector.ma 22 22 String.ma Char.ma List.ma
Note: See TracChangeset
for help on using the changeset viewer.