Changeset 1598


Ignore:
Timestamp:
Dec 12, 2011, 5:53:36 PM (8 years ago)
Author:
mulligan
Message:

changes over the last couple of days

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1597 r1598  
    3838qed.
    3939
     40axiom o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p:
     41  ∀m, n, o, p: nat.
     42    p < o → m < n - o → m < n - p.
     43
     44lemma pair_eq_1_jmeq:
     45  ∀a, b: Type[0].
     46  ∀a1, a2: a.
     47  ∀b1, b2: b.
     48    〈a1, b1〉 ≃ 〈a2, b2〉 → a1 = a2.
     49  #a #b #a1 #a2 #b1 #b2 #assm
     50  cases daemon (* XXX: no jm discrimination for pairs *)
     51qed.
     52   
     53lemma prod_fst_jmeq:
     54  ∀a, b: Type[0].
     55  ∀p: a × b.
     56  ∀l: a.
     57  ∀r: b.
     58    p ≃ 〈l, r〉 → l = fst … p.
     59  #a #b #p #l #r
     60  cases p #aa #bb #assm @sym_eq
     61  lapply (pair_eq_1_jmeq a b aa l bb r assm)
     62  #assm assumption
     63qed.
     64
     65lemma lt_to_le:
     66  ∀m, n: nat.
     67    m < n → m ≤ n.
     68  #m #n #assm /2 by le_S_to_le/
     69qed.
     70
     71lemma Prod_inv_rect_Type0:
     72 ∀A,B. ∀P: A × B → Type[0].∀ab.
     73  (∀a,b. ab = 〈a,b〉 → P 〈a,b〉) → P ab.
     74 #A #B #P * /2/
     75qed.
     76
     77notation > "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
     78 with precedence 10
     79for @{ Prod_inv_rect_Type0 ??? $t (λ${ident x}.λ${ident y}.λ${ident H}.$s) }.
     80
     81notation < "hvbox('let' 〈ident x,ident y〉 {ident H} ≝ t 'in' s)"
     82 with precedence 10
     83for @{ Prod_inv_rect_Type0 $z $w $r $t (λ${ident x}:$X.λ${ident y}:$Y.λ${ident H}:$h.$s) }.
     84
     85lemma breakup_pair' : ∀A,B,C:Type[0].∀x. ∀R:C → Prop. ∀P:∀a:A.∀b:B. x=〈a,b〉 → C.
     86  R (P (\fst x) (\snd x) ?) → R (let 〈a,b〉 {H} ≝ x in P a b H).
     87[2: // ]
     88#A #B #C *; normalize /2/
     89qed.
     90
    4091(* timings taken from SIEMENS *)
    4192
    4293definition fetch0: BitVectorTrie Byte 16 → ∀program_counter: Word. Byte →
    4394  nat_of_bitvector … program_counter < code_memory_size - 24 (* 3 bytes *) →
    44   Σret: instruction × Word × nat. nat_of_bitvector … program_counter < nat_of_bitvector … (\snd (\fst ret)) ≝
     95  Σret: instruction × Word × nat. nat_of_bitvector … program_counter nat_of_bitvector … (\snd (\fst ret)) ≝
    4596  λpmem.
    4697  λpc.
     
    59110         else
    60111          let 〈b,v〉≝  head … v in if b then
    61            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
     112           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
    62113          else
    63114           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
     
    67118         else
    68119          let 〈b,v〉≝  head … v in if b then
    69            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     120           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    70121          else
    71122           〈〈RealInstruction (MOVX … (inr … 〈EXT_INDIRECT_DPTR,ACC_A〉)), pc〉, 2〉
     
    79130         else
    80131          let 〈b,v〉≝  head … v in if b then
    81            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
     132           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DIRECT b1〉)))))), pc〉, 1〉
    82133          else
    83134           〈〈RealInstruction (CLR … ACC_A), pc〉, 1〉
     
    87138         else
    88139          let 〈b,v〉≝  head … v in if b then
    89            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
     140           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, 2〉
    90141          else
    91142           〈〈RealInstruction (MOVX … (inl … 〈ACC_A,EXT_INDIRECT_DPTR〉)), pc〉, 2〉
     
    93144      let 〈b,v〉≝  head … v in if b then
    94145       let 〈b,v〉≝  head … v in if b then
    95         let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
     146        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, 2〉
    96147       else
    97148        let 〈b,v〉≝  head … v in if b then
     
    100151         else
    101152          let 〈b,v〉≝  head … v in if b then
    102            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
     153           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, 2〉
    103154          else
    104155           〈〈RealInstruction (DA … ACC_A), pc〉, 1〉
     
    108159           〈〈RealInstruction (SETB … CARRY), pc〉, 1〉
    109160          else
    110            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
    111          else
    112           let 〈b,v〉≝  head … v in if b then
    113            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    114           else
    115            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
     161           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SETB … (BIT_ADDR b1)), pc〉, 1〉
     162         else
     163          let 〈b,v〉≝  head … v in if b then
     164           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     165          else
     166           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (POP … (DIRECT b1)), pc〉, 2〉
    116167      else
    117168       let 〈b,v〉≝  head … v in if b then
     
    123174         else
    124175          let 〈b,v〉≝  head … v in if b then
    125            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
     176           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XCH … ACC_A (DIRECT b1)), pc〉, 1〉
    126177          else
    127178           〈〈RealInstruction (SWAP … ACC_A), pc〉, 1〉
     
    131182           〈〈RealInstruction (CLR … CARRY), pc〉, 1〉
    132183          else
    133            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
    134          else
    135           let 〈b,v〉≝  head … v in if b then
    136            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
    137           else
    138            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
     184           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CLR … (BIT_ADDR b1)), pc〉, 1〉
     185         else
     186          let 〈b,v〉≝  head … v in if b then
     187           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, 2〉
     188          else
     189           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (PUSH … (DIRECT b1)), pc〉, 2〉
    139190    else
    140191     let 〈b,v〉≝  head … v in if b then
    141192      let 〈b,v〉≝  head … v in if b then
    142193       let 〈b,v〉≝  head … v in if b then
    143         let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    144        else
    145         let 〈b,v〉≝  head … v in if b then
    146          let 〈b,v〉≝  head … v in if b then
    147           let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    148          else
    149           let 〈b,v〉≝  head … v in if b then
    150            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
    151           else
    152            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     194        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inr … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     195       else
     196        let 〈b,v〉≝  head … v in if b then
     197         let 〈b,v〉≝  head … v in if b then
     198          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inr … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, 2〉
     199         else
     200          let 〈b,v〉≝  head … v in if b then
     201           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE …  (inl … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, 2〉
     202          else
     203           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (CJNE … (inl … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, 2〉
    153204        else
    154205         let 〈b,v〉≝  head … v in if b then
     
    156207           〈〈RealInstruction (CPL … CARRY), pc〉, 1〉
    157208          else
    158            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
    159          else
    160           let 〈b,v〉≝  head … v in if b then
    161            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    162           else
    163            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    164       else
    165        let 〈b,v〉≝  head … v in if b then
    166         let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
    167        else
    168         let 〈b,v〉≝  head … v in if b then
    169          let 〈b,v〉≝  head … v in if b then
    170           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
     209           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (CPL … (BIT_ADDR b1)), pc〉, 1〉
     210         else
     211          let 〈b,v〉≝  head … v in if b then
     212           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     213          else
     214           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     215      else
     216       let 〈b,v〉≝  head … v in if b then
     217        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DIRECT b1〉)))))), pc〉, 2〉
     218       else
     219        let 〈b,v〉≝  head … v in if b then
     220         let 〈b,v〉≝  head … v in if b then
     221          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DIRECT b1〉)))))), pc〉, 2〉
    171222         else
    172223          〈〈RealInstruction (MUL … ACC_A ACC_B), pc〉, 4〉
     
    176227           〈〈RealInstruction (INC … DPTR), pc〉, 2〉
    177228          else
    178            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
    179          else
    180           let 〈b,v〉≝  head … v in if b then
    181            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
    182           else
    183            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
     229           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inr … 〈CARRY,BIT_ADDR b1〉))), pc〉, 1〉
     230         else
     231          let 〈b,v〉≝  head … v in if b then
     232           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, 2〉
     233          else
     234           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,N_BIT_ADDR b1〉)), pc〉, 2〉
    184235     else
    185236      let 〈b,v〉≝  head … v in if b then
     
    192243         else
    193244          let 〈b,v〉≝  head … v in if b then
    194            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
    195           else
    196            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
     245           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DIRECT b1)), pc〉, 1〉
     246          else
     247           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (SUBB … ACC_A (DATA b1)), pc〉, 1〉
    197248        else
    198249         let 〈b,v〉≝  head … v in if b then
     
    200251           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, 2〉
    201252          else
    202            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
    203          else
    204           let 〈b,v〉≝  head … v in if b then
    205            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    206           else
    207            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
    208       else
    209        let 〈b,v〉≝  head … v in if b then
    210         let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
    211        else
    212         let 〈b,v〉≝  head … v in if b then
    213          let 〈b,v〉≝  head … v in if b then
    214           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
    215          else
    216           let 〈b,v〉≝  head … v in if b then
    217            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
     253           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inr … 〈BIT_ADDR b1,CARRY〉)), pc〉, 2〉
     254         else
     255          let 〈b,v〉≝  head … v in if b then
     256           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     257          else
     258           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inr … 〈DPTR,DATA16 (b1 @@ b2)〉)))), pc〉, 2〉
     259      else
     260       let 〈b,v〉≝  head … v in if b then
     261        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,REGISTER v〉))))), pc〉, 2〉
     262       else
     263        let 〈b,v〉≝  head … v in if b then
     264         let 〈b,v〉≝  head … v in if b then
     265          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,INDIRECT (from_singl … v)〉))))), pc〉, 2〉
     266         else
     267          let 〈b,v〉≝  head … v in if b then
     268           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DIRECT b2〉))))), pc〉, 2〉
    218269          else
    219270           〈〈RealInstruction (DIV … ACC_A ACC_B), pc〉, 4〉
     
    223274           〈〈MOVC … ACC_A (ACC_PC), pc〉, 2〉
    224275          else
    225            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    226          else
    227           let 〈b,v〉≝  head … v in if b then
    228            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
    229           else
    230            let 〈pc,b1〉≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
     276           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
     277         else
     278          let 〈b,v〉≝  head … v in if b then
     279           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, 2〉
     280          else
     281           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈SJMP … (RELATIVE b1), pc〉, 2〉
    231282   else
    232283    let 〈b,v〉≝  head … v in if b then
     
    234285      let 〈b,v〉≝  head … v in if b then
    235286       let 〈b,v〉≝  head … v in if b then
    236         let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
    237        else
    238         let 〈b,v〉≝  head … v in if b then
    239          let 〈b,v〉≝  head … v in if b then
    240           let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
    241          else
    242           let 〈b,v〉≝  head … v in if b then
    243            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
    244           else
    245            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
     287        let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈REGISTER v,DATA b1〉)))))), pc〉, 1〉
     288       else
     289        let 〈b,v〉≝  head … v in if b then
     290         let 〈b,v〉≝  head … v in if b then
     291          let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inr … 〈INDIRECT (from_singl … v),DATA b1〉)))))), pc〉, 1〉
     292         else
     293          let 〈b,v〉≝  head … v in if b then
     294           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,DATA b2〉))))), pc〉, 3〉
     295          else
     296           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inl … (inl … 〈ACC_A,DATA b1〉)))))), pc〉, 1〉
    246297        else
    247298         let 〈b,v〉≝  head … v in if b then
     
    249300           〈〈JMP … INDIRECT_DPTR, pc〉, 2〉
    250301          else
    251            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
    252          else
    253           let 〈b,v〉≝  head … v in if b then
    254            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    255           else
    256            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
     302           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inr … 〈CARRY,BIT_ADDR b1〉)), pc〉, 2〉
     303         else
     304          let 〈b,v〉≝  head … v in if b then
     305           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     306          else
     307           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNZ … (RELATIVE b1)), pc〉, 2〉
    257308      else
    258309       let 〈b,v〉≝  head … v in if b then
     
    264315         else
    265316          let 〈b,v〉≝  head … v in if b then
    266            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
    267           else
    268            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
    269         else
    270          let 〈b,v〉≝  head … v in if b then
    271           let 〈b,v〉≝  head … v in if b then
    272            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
    273           else
    274            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
    275          else
    276           let 〈b,v〉≝  head … v in if b then
    277            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
    278           else
    279            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
     317           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DIRECT b1〉)), pc〉, 1〉
     318          else
     319           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inl … 〈ACC_A,DATA b1〉)), pc〉, 1〉
     320        else
     321         let 〈b,v〉≝  head … v in if b then
     322          let 〈b,v〉≝  head … v in if b then
     323           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,DATA b2〉)), pc〉, 2〉
     324          else
     325           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (XRL … (inr … 〈DIRECT b1,ACC_A〉)), pc〉, 1〉
     326         else
     327          let 〈b,v〉≝  head … v in if b then
     328           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, 2〉
     329          else
     330           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JZ … (RELATIVE b1)), pc〉, 2〉
    280331     else
    281332      let 〈b,v〉≝  head … v in if b then
     
    288339         else
    289340          let 〈b,v〉≝  head … v in if b then
    290            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
    291           else
    292            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
    293         else
    294          let 〈b,v〉≝  head … v in if b then
    295           let 〈b,v〉≝  head … v in if b then
    296            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    297           else
    298            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    299          else
    300           let 〈b,v〉≝  head … v in if b then
    301            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    302           else
    303            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
     341           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     342          else
     343           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     344        else
     345         let 〈b,v〉≝  head … v in if b then
     346          let 〈b,v〉≝  head … v in if b then
     347           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     348          else
     349           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ANL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     350         else
     351          let 〈b,v〉≝  head … v in if b then
     352           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     353          else
     354           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JNC … (RELATIVE b1)), pc〉, 2〉
    304355      else
    305356       let 〈b,v〉≝  head … v in if b then
     
    311362         else
    312363          let 〈b,v〉≝  head … v in if b then
    313            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
    314           else
    315            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
    316         else
    317          let 〈b,v〉≝  head … v in if b then
    318           let 〈b,v〉≝  head … v in if b then
    319            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
    320           else
    321            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
    322          else
    323           let 〈b,v〉≝  head … v in if b then
    324            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
    325           else
    326            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
     364           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DIRECT b1〉))), pc〉, 1〉
     365          else
     366           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inl … 〈ACC_A,DATA b1〉))), pc〉, 1〉
     367        else
     368         let 〈b,v〉≝  head … v in if b then
     369          let 〈b,v〉≝  head … v in if b then
     370           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,DATA b2〉))), pc〉, 2〉
     371          else
     372           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ORL … (inl … (inr … 〈DIRECT b1,ACC_A〉))), pc〉, 1〉
     373         else
     374          let 〈b,v〉≝  head … v in if b then
     375           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, 2〉
     376          else
     377           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (JC … (RELATIVE b1)), pc〉, 2〉
    327378    else
    328379     let 〈b,v〉≝  head … v in if b then
     
    336387         else
    337388          let 〈b,v〉≝  head … v in if b then
    338            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
    339           else
    340            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
     389           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DIRECT b1)), pc〉, 1〉
     390          else
     391           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADDC … ACC_A (DATA b1)), pc〉, 1〉
    341392        else
    342393         let 〈b,v〉≝  head … v in if b then
     
    347398         else
    348399          let 〈b,v〉≝  head … v in if b then
    349            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    350           else
    351            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     400           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     401          else
     402           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    352403      else
    353404       let 〈b,v〉≝  head … v in if b then
     
    359410         else
    360411          let 〈b,v〉≝  head … v in if b then
    361            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
    362           else
    363            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
     412           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DIRECT b1)), pc〉, 1〉
     413          else
     414           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (ADD … ACC_A (DATA b1)), pc〉, 1〉
    364415        else
    365416         let 〈b,v〉≝  head … v in if b then
     
    370421         else
    371422          let 〈b,v〉≝  head … v in if b then
    372            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
    373           else
    374            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     423           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;true]]) @@ b1)), pc〉, 2〉
     424          else
     425           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    375426     else
    376427      let 〈b,v〉≝  head … v in if b then
     
    383434         else
    384435          let 〈b,v〉≝  head … v in if b then
    385            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
     436           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (DEC … (DIRECT b1)), pc〉, 1〉
    386437          else
    387438           〈〈RealInstruction (DEC … ACC_A), pc〉, 1〉
     
    391442           〈〈RealInstruction (RRC … ACC_A), pc〉, 1〉
    392443          else
    393            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    394          else
    395           let 〈b,v〉≝  head … v in if b then
    396            let 〈pc,b1〉≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    397           else
    398            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
     444           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LCALL … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     445         else
     446          let 〈b,v〉≝  head … v in if b then
     447           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     448          else
     449           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈RealInstruction (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, 2〉
    399450      else
    400451       let 〈b,v〉≝  head … v in if b then
     
    406457         else
    407458          let 〈b,v〉≝  head … v in if b then
    408            let 〈pc,b1〉≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
     459           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈RealInstruction (INC … (DIRECT b1)), pc〉, 1〉
    409460          else
    410461           〈〈RealInstruction (INC … ACC_A), pc〉, 1〉
     
    414465           〈〈RealInstruction (RR … ACC_A), pc〉, 1〉
    415466          else
    416            let 〈pc,b1〉≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
    417          else
    418           let 〈b,v〉≝  head … v in if b then
    419            let 〈pc,b1〉≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
     467           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in let 〈pc,b2〉≝ next pmem pc ? in 〈〈LJMP … (ADDR16 (b1 @@ b2)), pc〉, 2〉
     468         else
     469          let 〈b,v〉≝  head … v in if b then
     470           let 〈pc,b1〉 {EQ} ≝ next pmem pc ? in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, 2〉
    420471          else
    421472           〈〈RealInstruction (NOP …), pc〉, 1〉.
    422473  try %
     474  try (
     475    @(o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p
     476      (nat_of_bitvector 16 pc) code_memory_size 24 1
     477      (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof)
     478  )
     479  [1,2,3,4,5,6,7,8:
     480    @breakup_pair' cases (next pmem pc ?)
     481    normalize * normalize #pc' #byte @lt_to_le
     482  |3:
     483    @breakup_pair' cases (next pmem pc ?)
     484    normalize * normalize #pc' #byte @lt_to_le
     485  |2:
     486    @breakup_pair' cases(next pmem pc ?)
     487    normalize * normalize #pc' #byte @lt_to_le
     488  [
     489  | 92:
     490    cases (next ???) in EQ; * #pc' #content #H #EQ whd in EQ:(??%?); destruct
     491   
     492   
     493    lapply(eq_pair_fst_snd ? ? (next pmem pc ?))
     494    #assm >assm
     495    cut(nat_of_bitvector … pc < nat_of_bitvector …
     496      (\fst  (next pmem pc
     497                (o_lt_p_to_m_lt_n_minus_o_to_m_lt_n_minus_p (nat_of_bitvector 16 pc)
     498                 code_memory_size 24 1 (le_S_S 1 23 (le_S_S O 22 (le_O_n 22))) proof))))
     499    [ @sig2
     500    | #assm @lt_to_le assumption
     501    ]
     502  |92:
     503    check next.
     504    lapply pc -pc
     505    @sig2
    423506  cases daemon (* XXX: requires rewrite of the above to make it more russell friendly *)
    424507qed.
  • src/ASM/FoldStuff.ma

    r1062 r1598  
    4848 ≝ λA,P,l,H,acc. foldr_strong_internal A P l H [ ] l acc (refl …).
    4949
    50 lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
     50lemma pair_destruct: ∀A,B,a1,a2,b1,b2. mk_Prod A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
    5151 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
    5252qed.
  • src/ASM/Util.ma

    r1516 r1598  
    688688notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
    689689with precedence 90 for @{ 'triple $a $b $c}.
    690 interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
     690interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
    691691
    692692notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
    693693with precedence 90 for @{ 'quadruple $a $b $c $d}.
    694 interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
     694interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
    695695
    696696notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
     
    802802definition divide_with_remainder ≝
    803803  λm, n: nat.
    804     pair ? ? (m ÷ n) (modulus m n).
     804    mk_Prod … (m ÷ n) (modulus m n).
    805805   
    806806let rec exponential (m: nat) (n: nat) on n ≝
  • src/ASM/Vector.ma

    r1524 r1598  
    274274  λv: Vector A n.
    275275  λq: Vector B n.
    276     zip_with A B (A × B) n (pair A B) v q.
     276    zip_with A B (A × B) n (mk_Prod A B) v q.
    277277
    278278(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
  • src/common/Errors.ma

    r1355 r1598  
    6060definition bind2 ≝ λA,B,C: Type[0]. λf: res (A × B). λg: A → B → res C.
    6161  match f with
    62   [ OK v ⇒ match v with [ pair x y ⇒ g x y ]
     62  [ OK v ⇒ g (fst … v) (snd … v)
    6363  | Error msg => Error ? msg
    6464  ].
     
    6666definition bind3 ≝ λA,B,C,D: Type[0]. λf: res (A × B × C). λg: A → B → C → res D.
    6767  match f with
    68   [ OK v ⇒ match v with [ pair xy z ⇒ match xy with [ pair x y ⇒ g x y z ] ]
     68  [ OK v ⇒ g (fst … (fst … v)) (snd … (fst … v)) (snd … v)
    6969  | Error msg => Error ? msg
    7070  ].
     
    9393  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
    9494
     95lemma Prod_extensionality:
     96  ∀a, b: Type[0].
     97  ∀p: a × b.
     98    p = 〈fst … p, snd … p〉.
     99  #a #b #p //
     100qed.
     101
    95102definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
    96103λA,B,C,P,e,f.
    97104  match e with
    98   [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ]
     105  [ OK v ⇒ match v with [ dp v' p ⇒ f (fst … v') (snd … v') ? ]
    99106  | Error msg ⇒ Error ? msg
    100107  ].
     108  <(Prod_extensionality A B v')
     109  assumption
     110qed.
    101111
    102112notation > "vbox('do' «ident v1, ident v2, ident H» ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
  • src/utilities/pair.ma

    r1316 r1598  
    33notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
    44 with precedence 10
    5 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
     5for @{ match $t with [ mk_Prod ${ident x} ${ident y} ⇒ $s ] }.
    66
    77(* Also extracts an equality proof (useful when not using Russell). *)
    88notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
    99 with precedence 10
    10 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
     10for @{ match $t return λx.x = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
    1111        λ${ident E}.$s ] (refl ? $t) }.
    1212
    1313notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    1414 with precedence 10
    15 for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
    16        match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
     15for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
     16       match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
    1717        λ${ident E}.$s ] ] (refl ? $t) }.
    1818
Note: See TracChangeset for help on using the changeset viewer.