Changeset 279


Ignore:
Timestamp:
Nov 24, 2010, 5:19:38 PM (9 years ago)
Author:
sacerdot
Message:

Notation moved to Cartesian.

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

Legend:

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

    r272 r279  
    11include "ASM.ma".
    2 
    3 (*
    4 ndefinition from_addressing_mode_tag ≝
    5  λT:Type[0].λt:addressing_mode_tag.
    6   match t with
    7    [ direct ⇒ Byte → T
    8    | indirect ⇒ Bit → T
    9    | ext_indirect ⇒ Bit → T
    10    | register ⇒ Bit → Bit → Bit → T
    11    | acc_a ⇒ T
    12    | acc_b ⇒ T
    13    | dptr ⇒ T
    14    | data ⇒ Byte → T
    15    | data16 ⇒ Word → T
    16    | acc_dptr ⇒ T
    17    | acc_pc ⇒ T
    18    | ext_indirect_dptr ⇒ T
    19    | indirect_dptr ⇒ T
    20    | carry ⇒ T
    21    | bit_addr ⇒ Bit → T
    22    | n_bit_addr ⇒ Bit → T
    23    | relative ⇒ Byte → T
    24    | addr11 ⇒ Word11 → T
    25    | addr16 ⇒ Word → T ].
    26 *)
    27 (*
    28 nlet rec elim_addr (T:addressing_mode → Type[0]) n l on l
    29 : subaddressing_mode n l → Type[0] ≝
    30  match l
    31   return λm.λl:Vector addressing_mode_tag m.
    32    ∀proof:m = S n.
    33     subaddressing_mode n (match proof with [refl ⇒ l]) → Type[0] with
    34   [ Empty ⇒ λK.λ_.Nat
    35   | Cons o he tl ⇒ λK.λv.Nat(*
    36      match o
    37       return λy.∀p:S y = S n.
    38        subaddressing_mode y
    39         (v⌈Vector addressing_mode_tag (S y) ↦ Vector addressing_mode_tag (S n)⌉)
    40         → Type[0]
    41      with
    42       [ Z ⇒ λK.λv.(? : Type[0])
    43       | S p ⇒ λK.λv.(? : Type[0])
    44       ]*)
    45   ] (?: S n = S n).
    46 ##[##1: @
    47   | ndestruct
    48   |##7: //
    49   | normalize;
    50 
    51 nlet rec elim_addr n (v: Vector addressing_mode_tag (S n)) on v
    52 : subaddressing_mode n v Type[0]
    53 
    54  match v return λx.λ_.x = S n. Type[0] with
    55   [ Empty ⇒ λK.⊥
    56   | Cons o he tl ⇒ λK.
    57      match o with
    58       [ Z ⇒
    59       | S m ⇒
    60       ]
    61   ] (? : S n = S n).
    62 *)
    63 
    64 notation "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    65  with precedence 10
    66 for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
    67 
    68 ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).
    692
    703ndefinition assembly1 ≝
  • Deliverables/D4.1/Matita/Cartesian.ma

    r268 r279  
    88interpretation "Cartesian product" 'pair l r = (mk_Cartesian ? ? l r).
    99interpretation "Cartesian" 'product A B = (Cartesian A B).
     10
     11notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     12 with precedence 10
     13for @{ match $t with [ mk_Cartesian ${ident x} ${ident y} ⇒ $s ] }.
     14
     15(*ncheck (let 〈x,z〉 ≝ 〈Z,Z〉 in 〈x,z〉).*)
     16
Note: See TracChangeset for help on using the changeset viewer.