Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/ASM

  • Deliverables/D3.3/id-lookup-branch/ASM/I8051.ma

    r1153 r1197  
    147147definition RegisterSPL ≝ Register06.
    148148definition RegisterSPH ≝ Register07.
    149 definition RegisterForbidden: list Register ≝
    150   [ RegisterSST; RegisterST0; RegisterST1;
    151     RegisterSPL; RegisterSPH ].
    152149definition RegisterParams: list Register ≝
    153150  [ Register30; Register31; Register32; Register33;
     
    173170  [Register20; Register21; Register22; Register23; Register24;
    174171   Register25; Register26; Register27].
     172definition RegistersForbidden ≝
     173  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
     174   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
     175   RegisterST2; RegisterST3; RegisterSST].
     176(* registers minus forbidden *)
     177definition RegistersAllocatable ≝
     178  [Register00; Register01; Register02; Register03; Register04;
     179   Register05; Register06; Register07; Register10; Register11;
     180   Register12; Register13; Register14; Register15; Register16;
     181   Register17; Register20; Register21; Register22; Register23;
     182   Register24; Register25; Register26; Register27; Register30;
     183   Register31; Register32; Register33; Register34; Register35;
     184   Register36; Register37].
    175185
    176186definition register_address: Register → [[ acc_a; direct; registr ]] ≝
  • Deliverables/D3.3/id-lookup-branch/ASM/Util.ma

    r1098 r1197  
    1111example not_implemented: False. cases daemon qed.
    1212
     13notation "⊥" with precedence 90
     14  for @{ match ? in False with [ ] }.
     15
    1316notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    1417 with precedence 10
    1518for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     19
     20(*
     21notation > "hvbox('let' 〈ident x, ident y, ident z〉 ≝ t 'in' s)"
     22 with precedence 10
     23for @{
     24  match $t with
     25  [ pair ${ident x} y' ⇒
     26    match y' with
     27    [ pair ${ident y} ${ident z} ⇒ $s ]
     28  ]
     29}.
     30*)
    1631
    1732definition ltb ≝
     
    3247  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
    3348  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
     49  ].
     50
     51let rec forall
     52  (A: Type[0]) (f: A → bool) (l: list A)
     53    on l ≝
     54  match l with
     55  [ nil        ⇒ true
     56  | cons hd tl ⇒ f hd ∧ forall A f tl
    3457  ].
    3558
     
    614637  ]
    615638qed.
     639
     640lemma nth_append_first:
     641 ∀A:Type[0].
     642 ∀n:nat.∀l1,l2:list A.∀d:A.
     643   n < |l1| → nth n A (l1@l2) d = nth n A l1 d.
     644 #A #n #l1 #l2 #d
     645 generalize in match n; -n; elim l1
     646 [ normalize #k #Hk @⊥ @(absurd … Hk) @not_le_Sn_O
     647 | #h #t #Hind #k normalize
     648   cases k -k
     649   [ #Hk normalize @refl
     650   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
     651   ] 
     652 ]
     653qed.
     654
     655lemma nth_append_second:
     656 ∀A: Type[0].∀n.∀l1,l2:list A.∀d.n ≥ length A l1 ->
     657  nth n A (l1@l2) d = nth (n - length A l1) A l2 d.
     658 #A #n #l1 #l2 #d
     659 generalize in match n; -n; elim l1
     660 [ normalize #k #Hk <(minus_n_O) @refl
     661 | #h #t #Hind #k normalize
     662   cases k -k;
     663   [ #Hk @⊥ @(absurd (S (|t|) ≤ 0)) [ @Hk | @not_le_Sn_O ]
     664   | #k #Hk normalize @(Hind k) @le_S_S_to_le @Hk
     665   ]
     666 ]
     667qed.
     668
    616669   
    617670notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
     
    699752qed.
    700753
    701 
    702 notation "⊥" with precedence 90
    703   for @{ match ? in False with [ ] }.
    704754
    705755let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
Note: See TracChangeset for help on using the changeset viewer.