Changeset 856


Ignore:
Timestamp:
May 30, 2011, 1:44:45 PM (8 years ago)
Author:
sacerdot
Message:
  1. if_then_else is now a notation for match with (to allow Russell to work better)
  2. notation for destructuring let fixed to work in pretty printing mode too
Location:
src/ASM
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r855 r856  
    11include "ASM/Assembly.ma".
    22include "ASM/Interpret.ma".
    3 
    4 (*
    5 axiom append_cons_commute:
    6   ∀A: Type[0].
    7   ∀l, r: list A.
    8   ∀h: A.
    9     l @ h::r = l @ [h] @ r.
    10 *)
    11 (*
    12 axiom append_associative:
    13   ∀A: Type[0].
    14   ∀l, c, r: list A.
    15     (l @ c) @ r = l
    16 *)
    173
    184let rec foldl_strong_internal
     
    4228    foldl_strong_internal A P l H [ ] l acc (refl …).
    4329
    44 (* RUSSEL **)
    45 
    4630definition bit_elim: ∀P: bool → bool. bool ≝
    4731  λP.
     
    7559qed.
    7660
     61(*
    7762lemma subvector_hd_tl:
    7863  ∀A: Type[0].
     
    185170  | @ (instruction_elim INSTR)
    186171  ].
     172*)
    187173 
    188     (* > append_cons_commute
    189     @
     174(* RUSSEL **)
    190175
    191176include "basics/jmeq.ma".
     
    218203 #A #P #p cases p #w #q @q
    219204qed.
     205
     206lemma jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. x≃y → x=y.
     207 #A #x #y #JMEQ @(jmeq_elim ? x … JMEQ) %
     208qed.
     209
     210coercion jmeq_to_eq: ∀A:Type[0]. ∀x,y:A. ∀p:x≃y.x=y ≝ jmeq_to_eq on _p:?≃? to ?=?.
    220211
    221212(* END RUSSELL **)
     
    270261   | Some r ⇒ λ_.r] (policy_ok p).
    271262 cases abs //
     263qed.
     264
     265lemma length_append:
     266 ∀A.∀l1,l2:list A.
     267  |l1 @ l2| = |l1| + |l2|.
     268 #A #l1 elim l1
     269  [ //
     270  | #hd #tl #IH #l2 normalize <IH //]
    272271qed.
    273272
     
    308307   let 〈pc, costs〉 ≝ pc_costs in
    309308    〈labels, costs〉.
    310  [
    311  |
     309 [ whd cases construct in p3 #PC #CODE #JMEQ whd #pc #Hpc
     310   generalize in match (sig2 … t) whd in ⊢ (% → ?)
     311   >p whd in ⊢ (% → ?) >p1 whd in ⊢ (% → ?) #IH1
     312   >length_append in Hpc <plus_n_Sm in ⊢ (% → ?) <plus_n_O in ⊢ (% → ?) #Hpc
     313   whd in ⊢ (??(????%?)?) -labels1;
     314   cases label
     315    [ whd in ⊢ (??(????%?)?)
     316      cases (le_to_or_lt_eq … Hpc)
     317      [ #H1 >(IH1 pc) [2: @(le_S_S_to_le … H1)]
     318        (* lemmas needed here *)
     319      | #H1 generalize in match (injective_S … H1) -H1 #H1
     320        (* ??? *)
     321      ]
     322    | -label #label whd in ⊢ (??(????%?)?)
     323     
     324    ]
     325 | (* dummy case *)
    312326 | whd #pc normalize in ⊢ (% → ?) #abs @⊥ // ]
    313327qed.
     
    343357 #A #P
    344358qed.*)
    345 
    346 lemma length_append:
    347  ∀A.∀l1,l2:list A.
    348   |l1 @ l2| = |l1| + |l2|.
    349  #A #l1 elim l1
    350   [ //
    351   | #hd #tl #IH #l2 normalize <IH //]
    352 qed.
    353359
    354360lemma rev_preserves_length:
  • src/ASM/Fetch.ma

    r820 r856  
    2929           let 〈pc,b1〉≝ next pmem pc in 〈〈RealInstruction (MOV … (inl … (inl … (inl … (inr … 〈DIRECT b1,ACC_A〉))))), pc〉, 1〉
    3030          else
    31            〈〈CPL … ACC_A, pc〉, 1〉
     31           〈〈RealInstruction (CPL … ACC_A), pc〉, 1〉
    3232        else
    3333         let 〈b,v〉≝  head … v in if b then
  • src/ASM/Interpret.ma

    r843 r856  
    505505        ].
    506506    try assumption
    507     try (
    508       normalize
    509       repeat (@ (le_S_S))
    510       @ (le_O_n)
    511     )
     507    try @I
    512508    try (
    513509      @ (execute_1_technical … (subaddressing_modein …))
    514       @ I
    515     )
    516     try (
    517       normalize
    518510      @ I
    519511    )
  • src/ASM/Util.ma

    r782 r856  
    138138    foldl ? ? (append ?) [ ] l.
    139139
    140 definition if_then_else ≝
     140(*definition if_then_else ≝
    141141  λA: Type[0].
    142142  λb: bool.
     
    146146  [ true ⇒ t
    147147  | false ⇒ f
    148   ].
     148  ].*)
    149149
    150150let rec rev (A: Type[0]) (l: list A) on l ≝
     
    159159  for @{ 'if_then_else $b $t $f }.
    160160*)
    161 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    162 notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
    163 
    164 interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
     161notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
     162 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
     163notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19
     164 for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
     165
     166(*interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).*)
    165167
    166168let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
     
    207209 with precedence 10
    208210for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
     211
     212notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
     213 with precedence 10
     214for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
    209215
    210216notation "⊥" with precedence 90
Note: See TracChangeset for help on using the changeset viewer.